1
use std::mem::offset_of;
2

            
3
use anodized::spec;
4
use scripting_format::{
5
    DEBUG_VALUE_DATA_SIZE, DebugValueData, ENTITY_HEADER_SIZE, EntityHeader, EntityType,
6
    MAGIC_OUTP, OUTPUT_HEADER_SIZE, Operation, OutputHeader, TAG_DATA_SIZE, TagData, ValueType,
7
};
8
use tracing::debug;
9

            
10
use super::emit::FunctionEmitter;
11

            
12
pub struct GcLocals {
13
    pub type_idx: u32,
14
    pub arr: u32,
15
    pub idx: u32,
16
}
17

            
18
pub struct TagGcData {
19
    pub name_data_idx: u32,
20
    pub name_len: u32,
21
    pub value_data_idx: u32,
22
    pub value_len: u32,
23
}
24

            
25
pub struct OutputSerializer {
26
    cursor: u32,
27
    entity_count: u32,
28
    output_start_idx: u32,
29
    output_base_local: u32,
30
    strings_end: u32,
31
}
32

            
33
impl OutputSerializer {
34
39320
    pub fn new(output_base_local: u32) -> Self {
35
39320
        Self {
36
39320
            cursor: 0,
37
39320
            entity_count: 0,
38
39320
            output_start_idx: 0,
39
39320
            output_base_local,
40
39320
            strings_end: 0,
41
39320
        }
42
39320
    }
43

            
44
    #[spec(
45
20251
        requires: [self.cursor == 0, self.entity_count == 0],
46
20251
        ensures: [self.cursor == OUTPUT_HEADER_SIZE as u32],
47
    )]
48
20251
    pub fn begin_output(&mut self, emit: &mut FunctionEmitter) {
49
20251
        debug!(cursor = self.cursor, "writing output header");
50
20251
        let local = self.output_base_local;
51
20251
        emit.store_i32_dynamic(
52
20251
            local,
53
20251
            self.cursor + offset_of!(OutputHeader, magic) as u32,
54
20251
            MAGIC_OUTP as i32,
55
        );
56
20251
        emit.store_i32_dynamic(
57
20251
            local,
58
20251
            self.cursor + offset_of!(OutputHeader, output_entity_count) as u32,
59
            0,
60
        );
61
20251
        emit.store_i32_dynamic(
62
20251
            local,
63
20251
            self.cursor + offset_of!(OutputHeader, output_start_idx) as u32,
64
20251
            self.output_start_idx as i32,
65
        );
66
20251
        emit.store_i32_dynamic(
67
20251
            local,
68
20251
            self.cursor + offset_of!(OutputHeader, next_write_pos) as u32,
69
20251
            OUTPUT_HEADER_SIZE as i32,
70
        );
71
20251
        self.cursor += OUTPUT_HEADER_SIZE as u32;
72
    }
73

            
74
    #[spec(
75
        captures: [self.entity_count as prev_count, self.cursor as prev_cursor],
76
        ensures: [
77
18708
            self.entity_count == prev_count + 1,
78
18708
            self.cursor == prev_cursor + ENTITY_HEADER_SIZE as u32,
79
18708
            *output == prev_cursor + ENTITY_HEADER_SIZE as u32,
80
        ],
81
    )]
82
    fn append_entity_header(
83
        &mut self,
84
        emit: &mut FunctionEmitter,
85
        entity_type: EntityType,
86
        operation: Operation,
87
        flags: u8,
88
        parent_idx: i32,
89
        data_size: u32,
90
18708
    ) -> u32 {
91
18708
        debug!(
92
            cursor = self.cursor,
93
            ?entity_type,
94
            "appending entity header"
95
        );
96
18708
        let local = self.output_base_local;
97
18708
        let data_offset = self.cursor + ENTITY_HEADER_SIZE as u32;
98

            
99
18708
        emit.store_u8_dynamic(
100
18708
            local,
101
18708
            self.cursor + offset_of!(EntityHeader, entity_type) as u32,
102
18708
            entity_type as u8,
103
        );
104
18708
        emit.store_u8_dynamic(
105
18708
            local,
106
18708
            self.cursor + offset_of!(EntityHeader, operation) as u32,
107
18708
            operation as u8,
108
        );
109
18708
        emit.store_u8_dynamic(
110
18708
            local,
111
18708
            self.cursor + offset_of!(EntityHeader, flags) as u32,
112
18708
            flags,
113
        );
114
18708
        emit.store_i32_dynamic(
115
18708
            local,
116
18708
            self.cursor + offset_of!(EntityHeader, parent_idx) as u32,
117
18708
            parent_idx,
118
        );
119
        // data_offset is relative — the runtime adds output_base
120
18708
        emit.store_i32_dynamic(
121
18708
            local,
122
18708
            self.cursor + offset_of!(EntityHeader, data_offset) as u32,
123
18708
            data_offset as i32,
124
        );
125
18708
        emit.store_i32_dynamic(
126
18708
            local,
127
18708
            self.cursor + offset_of!(EntityHeader, data_size) as u32,
128
18708
            data_size as i32,
129
        );
130

            
131
18708
        self.cursor += ENTITY_HEADER_SIZE as u32;
132
18708
        self.entity_count += 1;
133
18708
        emit.store_i32_dynamic(
134
18708
            local,
135
18708
            offset_of!(OutputHeader, output_entity_count) as u32,
136
18708
            self.entity_count as i32,
137
        );
138
18708
        data_offset
139
    }
140

            
141
18708
    fn begin_debug_value_entity(&mut self, emit: &mut FunctionEmitter) -> u32 {
142
18708
        self.append_entity_header(
143
18708
            emit,
144
18708
            EntityType::DebugValue,
145
18708
            Operation::Nop,
146
            0,
147
            -1,
148
18708
            DEBUG_VALUE_DATA_SIZE as u32,
149
        )
150
18708
    }
151

            
152
    #[spec(
153
        captures: [self.entity_count as prev_count],
154
1234
        ensures: [self.entity_count == prev_count + 1],
155
    )]
156
1234
    pub fn write_debug_nil(&mut self, emit: &mut FunctionEmitter) {
157
1234
        let data_start = self.begin_debug_value_entity(emit);
158
1234
        debug!(data_start, "writing nil value");
159
1234
        let local = self.output_base_local;
160
1234
        emit.store_u8_dynamic(
161
1234
            local,
162
1234
            data_start + offset_of!(DebugValueData, value_type) as u32,
163
1234
            ValueType::Nil as u8,
164
        );
165
1234
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
166
1234
        self.finalize_cursor(emit);
167
    }
168

            
169
    #[spec(
170
        captures: [self.entity_count as prev_count],
171
794
        ensures: [self.entity_count == prev_count + 1],
172
    )]
173
794
    pub fn write_debug_bool(&mut self, emit: &mut FunctionEmitter, value: bool) {
174
794
        let data_start = self.begin_debug_value_entity(emit);
175
794
        debug!(data_start, value, "writing bool value");
176
794
        let local = self.output_base_local;
177
794
        emit.store_u8_dynamic(
178
794
            local,
179
794
            data_start + offset_of!(DebugValueData, value_type) as u32,
180
794
            ValueType::Bool as u8,
181
        );
182
794
        emit.store_i64_dynamic(
183
794
            local,
184
794
            data_start + offset_of!(DebugValueData, data1) as u32,
185
794
            i64::from(value),
186
        );
187
794
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
188
794
        self.finalize_cursor(emit);
189
    }
190

            
191
    #[spec(
192
        captures: [self.entity_count as prev_count],
193
3741
        ensures: [self.entity_count == prev_count + 1],
194
    )]
195
3741
    pub fn write_debug_number(&mut self, emit: &mut FunctionEmitter, numer: i64, denom: i64) {
196
3741
        let data_start = self.begin_debug_value_entity(emit);
197
3741
        debug!(data_start, numer, denom, "writing number value");
198
3741
        let local = self.output_base_local;
199
3741
        emit.store_u8_dynamic(
200
3741
            local,
201
3741
            data_start + offset_of!(DebugValueData, value_type) as u32,
202
3741
            ValueType::Number as u8,
203
        );
204
3741
        emit.store_i64_dynamic(
205
3741
            local,
206
3741
            data_start + offset_of!(DebugValueData, data1) as u32,
207
3741
            numer,
208
        );
209
3741
        emit.store_i64_dynamic(
210
3741
            local,
211
3741
            data_start + offset_of!(DebugValueData, data2) as u32,
212
3741
            denom,
213
        );
214
3741
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
215
3741
        self.finalize_cursor(emit);
216
    }
217

            
218
    #[spec(
219
        captures: [self.entity_count as prev_count],
220
10475
        ensures: [self.entity_count == prev_count + 1],
221
    )]
222
    pub fn write_debug_string_gc(
223
        &mut self,
224
        emit: &mut FunctionEmitter,
225
        value_type: ValueType,
226
        data_idx: u32,
227
        len: u32,
228
        gc: &GcLocals,
229
10475
    ) {
230
10475
        debug!(
231
            cursor = self.cursor,
232
            ?value_type,
233
            data_idx,
234
            len,
235
            "writing string value with GC"
236
        );
237
10475
        let local = self.output_base_local;
238
10475
        let data_start = self.begin_debug_value_entity(emit);
239
10475
        let strings_pool = data_start + DEBUG_VALUE_DATA_SIZE as u32;
240

            
241
10475
        emit.store_u8_dynamic(
242
10475
            local,
243
10475
            data_start + offset_of!(DebugValueData, value_type) as u32,
244
10475
            value_type as u8,
245
        );
246
10475
        emit.store_i64_dynamic(
247
10475
            local,
248
10475
            data_start + offset_of!(DebugValueData, data1) as u32,
249
            0,
250
        );
251
10475
        emit.store_i64_dynamic(
252
10475
            local,
253
10475
            data_start + offset_of!(DebugValueData, data2) as u32,
254
10475
            i64::from(len),
255
        );
256

            
257
10475
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
258

            
259
10475
        self.copy_data_gc(emit, data_idx, len, strings_pool, gc);
260

            
261
10475
        self.cursor += len;
262
10475
        self.strings_end = strings_pool;
263
10475
        self.finalize_cursor(emit);
264
    }
265

            
266
    #[spec(
267
        captures: [self.entity_count as prev_count, self.cursor as prev_cursor],
268
        ensures: [
269
            self.entity_count == prev_count + 1,
270
            self.cursor == prev_cursor + ENTITY_HEADER_SIZE as u32 + TAG_DATA_SIZE as u32 + name_len + value_len,
271
            self.strings_end >= self.cursor,
272
        ],
273
    )]
274
    pub fn write_tag_gc(
275
        &mut self,
276
        emit: &mut FunctionEmitter,
277
        name_data_idx: u32,
278
        name_len: u32,
279
        value_data_idx: u32,
280
        value_len: u32,
281
        gc: &GcLocals,
282
    ) {
283
        let local = self.output_base_local;
284
        let total_data_size = TAG_DATA_SIZE as u32 + name_len + value_len;
285
        let data_start = self.append_entity_header(
286
            emit,
287
            EntityType::Tag,
288
            Operation::Create,
289
            0,
290
            -1,
291
            total_data_size,
292
        );
293

            
294
        let strings_start = data_start + TAG_DATA_SIZE as u32;
295
        let name_start = strings_start;
296
        let value_start = name_start + name_len;
297
        let strings_end = value_start + value_len;
298
        let name_offset = strings_end - name_start;
299
        let value_offset = strings_end - value_start;
300

            
301
        emit.store_i32_dynamic(
302
            local,
303
            data_start + offset_of!(TagData, name_offset) as u32,
304
            name_offset as i32,
305
        );
306
        emit.store_i32_dynamic(
307
            local,
308
            data_start + offset_of!(TagData, value_offset) as u32,
309
            value_offset as i32,
310
        );
311
        emit.store_i32_dynamic(
312
            local,
313
            data_start + offset_of!(TagData, name_len) as u32,
314
            ((value_len as i32) << 16) | (name_len as i32),
315
        );
316
        emit.store_i32_dynamic(local, data_start + offset_of!(TagData, reserved) as u32, 0);
317

            
318
        self.copy_data_gc(emit, name_data_idx, name_len, name_start, gc);
319
        self.copy_data_gc(emit, value_data_idx, value_len, value_start, gc);
320

            
321
        self.cursor = strings_end;
322
        self.strings_end = strings_end;
323
        self.finalize_cursor(emit);
324
    }
325

            
326
    #[spec(
327
        captures: [self.entity_count as prev_count, self.cursor as prev_cursor],
328
        ensures: [
329
176
            self.entity_count == prev_count + 1,
330
176
            self.cursor == prev_cursor + ENTITY_HEADER_SIZE as u32,
331
176
            *output == prev_cursor + ENTITY_HEADER_SIZE as u32,
332
        ],
333
    )]
334
    fn append_entity_header_dynamic_parent(
335
        &mut self,
336
        emit: &mut FunctionEmitter,
337
        entity_type: EntityType,
338
        operation: Operation,
339
        parent_idx_local: u32,
340
        data_size: u32,
341
176
    ) -> u32 {
342
176
        let local = self.output_base_local;
343
176
        let data_offset = self.cursor + ENTITY_HEADER_SIZE as u32;
344

            
345
176
        emit.store_u8_dynamic(
346
176
            local,
347
176
            self.cursor + offset_of!(EntityHeader, entity_type) as u32,
348
176
            entity_type as u8,
349
        );
350
176
        emit.store_u8_dynamic(
351
176
            local,
352
176
            self.cursor + offset_of!(EntityHeader, operation) as u32,
353
176
            operation as u8,
354
        );
355
176
        emit.store_u8_dynamic(
356
176
            local,
357
176
            self.cursor + offset_of!(EntityHeader, flags) as u32,
358
            0,
359
        );
360
        // parent_idx from WASM local
361
176
        emit.local_get(local);
362
176
        emit.i32_const((self.cursor + offset_of!(EntityHeader, parent_idx) as u32) as i32);
363
176
        emit.i32_add();
364
176
        emit.local_get(parent_idx_local);
365
176
        emit.i32_store_raw();
366
176
        emit.store_i32_dynamic(
367
176
            local,
368
176
            self.cursor + offset_of!(EntityHeader, data_offset) as u32,
369
176
            data_offset as i32,
370
        );
371
176
        emit.store_i32_dynamic(
372
176
            local,
373
176
            self.cursor + offset_of!(EntityHeader, data_size) as u32,
374
176
            data_size as i32,
375
        );
376

            
377
176
        self.cursor += ENTITY_HEADER_SIZE as u32;
378
176
        self.entity_count += 1;
379
176
        emit.store_i32_dynamic(
380
176
            local,
381
176
            offset_of!(OutputHeader, output_entity_count) as u32,
382
176
            self.entity_count as i32,
383
        );
384
176
        data_offset
385
    }
386

            
387
    #[spec(
388
        captures: [self.entity_count as prev_count, self.cursor as prev_cursor],
389
        ensures: [
390
176
            self.entity_count == prev_count + 1,
391
176
            self.cursor == prev_cursor + ENTITY_HEADER_SIZE as u32 + TAG_DATA_SIZE as u32 + tag.name_len + tag.value_len,
392
176
            self.strings_end >= self.cursor,
393
        ],
394
    )]
395
    pub fn write_tag_gc_dynamic_parent(
396
        &mut self,
397
        emit: &mut FunctionEmitter,
398
        parent_idx_local: u32,
399
        tag: &TagGcData,
400
        gc: &GcLocals,
401
176
    ) {
402
176
        let local = self.output_base_local;
403
176
        let total_data_size = TAG_DATA_SIZE as u32 + tag.name_len + tag.value_len;
404
176
        let data_start = self.append_entity_header_dynamic_parent(
405
176
            emit,
406
176
            EntityType::Tag,
407
176
            Operation::Create,
408
176
            parent_idx_local,
409
176
            total_data_size,
410
        );
411

            
412
176
        let strings_start = data_start + TAG_DATA_SIZE as u32;
413
176
        let name_start = strings_start;
414
176
        let value_start = name_start + tag.name_len;
415
176
        let strings_end = value_start + tag.value_len;
416
176
        let name_offset = strings_end - name_start;
417
176
        let value_offset = strings_end - value_start;
418

            
419
176
        emit.store_i32_dynamic(
420
176
            local,
421
176
            data_start + offset_of!(TagData, name_offset) as u32,
422
176
            name_offset as i32,
423
        );
424
176
        emit.store_i32_dynamic(
425
176
            local,
426
176
            data_start + offset_of!(TagData, value_offset) as u32,
427
176
            value_offset as i32,
428
        );
429
176
        emit.store_i32_dynamic(
430
176
            local,
431
176
            data_start + offset_of!(TagData, name_len) as u32,
432
176
            ((tag.value_len as i32) << 16) | (tag.name_len as i32),
433
        );
434
176
        emit.store_i32_dynamic(local, data_start + offset_of!(TagData, reserved) as u32, 0);
435

            
436
176
        self.copy_data_gc(emit, tag.name_data_idx, tag.name_len, name_start, gc);
437
176
        self.copy_data_gc(emit, tag.value_data_idx, tag.value_len, value_start, gc);
438

            
439
176
        self.cursor = strings_end;
440
176
        self.strings_end = strings_end;
441
176
        self.finalize_cursor(emit);
442
    }
443

            
444
10827
    fn copy_data_gc(
445
10827
        &self,
446
10827
        emit: &mut FunctionEmitter,
447
10827
        data_idx: u32,
448
10827
        len: u32,
449
10827
        dst_offset: u32,
450
10827
        gc: &GcLocals,
451
10827
    ) {
452
10827
        let local = self.output_base_local;
453
10827
        emit.i32_const(0);
454
10827
        emit.i32_const(len as i32);
455
10827
        emit.array_new_data(gc.type_idx, data_idx);
456
10827
        emit.local_set(gc.arr);
457

            
458
10827
        emit.i32_const(0);
459
10827
        emit.local_set(gc.idx);
460

            
461
10827
        emit.block_start();
462
10827
        emit.loop_start();
463

            
464
10827
        emit.local_get(gc.idx);
465
10827
        emit.i32_const(len as i32);
466
10827
        emit.i32_ge_u();
467
10827
        emit.br_if(1);
468

            
469
10827
        emit.local_get(local);
470
10827
        emit.i32_const(dst_offset as i32);
471
10827
        emit.i32_add();
472
10827
        emit.local_get(gc.idx);
473
10827
        emit.i32_add();
474

            
475
10827
        emit.local_get(gc.arr);
476
10827
        emit.local_get(gc.idx);
477
10827
        emit.array_get_u(gc.type_idx);
478

            
479
10827
        emit.i32_store8_raw();
480

            
481
10827
        emit.local_get(gc.idx);
482
10827
        emit.i32_const(1);
483
10827
        emit.i32_add();
484
10827
        emit.local_set(gc.idx);
485

            
486
10827
        emit.br(0);
487
10827
        emit.block_end();
488
10827
        emit.block_end();
489
10827
    }
490

            
491
    pub fn write_debug_string_from_stack(&mut self, emit: &mut FunctionEmitter, gc: &GcLocals) {
492
        emit.local_set(gc.arr);
493
        let data_start = self.begin_debug_value_entity(emit);
494
        let local = self.output_base_local;
495

            
496
        emit.store_u8_dynamic(
497
            local,
498
            data_start + offset_of!(DebugValueData, value_type) as u32,
499
            ValueType::String as u8,
500
        );
501
        emit.store_i64_dynamic(
502
            local,
503
            data_start + offset_of!(DebugValueData, data1) as u32,
504
            0,
505
        );
506
        // data2 = array.len (runtime)
507
        emit.local_get(local);
508
        emit.i32_const((data_start + offset_of!(DebugValueData, data2) as u32) as i32);
509
        emit.i32_add();
510
        emit.local_get(gc.arr);
511
        emit.array_len();
512
        emit.i64_extend_i32_u();
513
        emit.i64_store_raw();
514

            
515
        let strings_pool = data_start + DEBUG_VALUE_DATA_SIZE as u32;
516
        // Copy GC array bytes to output
517
        emit.i32_const(0);
518
        emit.local_set(gc.idx);
519
        emit.block_start();
520
        emit.loop_start();
521
        emit.local_get(gc.idx);
522
        emit.local_get(gc.arr);
523
        emit.array_len();
524
        emit.i32_ge_u();
525
        emit.br_if(1);
526
        emit.local_get(local);
527
        emit.i32_const(strings_pool as i32);
528
        emit.i32_add();
529
        emit.local_get(gc.idx);
530
        emit.i32_add();
531
        emit.local_get(gc.arr);
532
        emit.local_get(gc.idx);
533
        emit.array_get_u(gc.type_idx);
534
        emit.i32_store8_raw();
535
        emit.local_get(gc.idx);
536
        emit.i32_const(1);
537
        emit.i32_add();
538
        emit.local_set(gc.idx);
539
        emit.br(0);
540
        emit.block_end();
541
        emit.block_end();
542

            
543
        emit.store_i32_dynamic(
544
            local,
545
            offset_of!(OutputHeader, strings_offset) as u32,
546
            strings_pool as i32,
547
        );
548
        // next_write_pos = strings_pool + array.len
549
        emit.local_get(local);
550
        emit.i32_const(offset_of!(OutputHeader, next_write_pos) as i32);
551
        emit.i32_add();
552
        emit.i32_const(strings_pool as i32);
553
        emit.local_get(gc.arr);
554
        emit.array_len();
555
        emit.i32_add();
556
        emit.i32_store_raw();
557

            
558
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
559
    }
560

            
561
1276
    pub fn write_debug_number_from_stack(
562
1276
        &mut self,
563
1276
        emit: &mut FunctionEmitter,
564
1276
        ratio_type_idx: u32,
565
1276
        ratio_local: u32,
566
1276
    ) {
567
1276
        emit.local_set(ratio_local);
568
1276
        let data_start = self.begin_debug_value_entity(emit);
569
1276
        let local = self.output_base_local;
570
1276
        emit.store_u8_dynamic(
571
1276
            local,
572
1276
            data_start + offset_of!(DebugValueData, value_type) as u32,
573
1276
            ValueType::Number as u8,
574
        );
575
1276
        emit.local_get(local);
576
1276
        emit.i32_const((data_start + offset_of!(DebugValueData, data1) as u32) as i32);
577
1276
        emit.i32_add();
578
1276
        emit.local_get(ratio_local);
579
1276
        emit.struct_get(ratio_type_idx, 0);
580
1276
        emit.i64_store_raw();
581
1276
        emit.local_get(local);
582
1276
        emit.i32_const((data_start + offset_of!(DebugValueData, data2) as u32) as i32);
583
1276
        emit.i32_add();
584
1276
        emit.local_get(ratio_local);
585
1276
        emit.struct_get(ratio_type_idx, 1);
586
1276
        emit.i64_store_raw();
587
1276
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
588
1276
        self.finalize_cursor(emit);
589
1276
    }
590

            
591
1188
    pub fn write_debug_i32_from_stack(&mut self, emit: &mut FunctionEmitter, i32_local: u32) {
592
1188
        emit.local_set(i32_local);
593
1188
        let data_start = self.begin_debug_value_entity(emit);
594
1188
        let local = self.output_base_local;
595
1188
        emit.store_u8_dynamic(
596
1188
            local,
597
1188
            data_start + offset_of!(DebugValueData, value_type) as u32,
598
1188
            ValueType::Number as u8,
599
        );
600
1188
        emit.local_get(local);
601
1188
        emit.i32_const((data_start + offset_of!(DebugValueData, data1) as u32) as i32);
602
1188
        emit.i32_add();
603
1188
        emit.local_get(i32_local);
604
1188
        emit.i64_extend_i32_u();
605
1188
        emit.i64_store_raw();
606
1188
        emit.store_i64_dynamic(
607
1188
            local,
608
1188
            data_start + offset_of!(DebugValueData, data2) as u32,
609
            1,
610
        );
611
1188
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
612
1188
        self.finalize_cursor(emit);
613
1188
    }
614

            
615
    pub fn write_debug_bool_from_stack(&mut self, emit: &mut FunctionEmitter, bool_local: u32) {
616
        emit.local_set(bool_local);
617
        let data_start = self.begin_debug_value_entity(emit);
618
        let local = self.output_base_local;
619
        emit.store_u8_dynamic(
620
            local,
621
            data_start + offset_of!(DebugValueData, value_type) as u32,
622
            ValueType::Bool as u8,
623
        );
624
        emit.local_get(local);
625
        emit.i32_const((data_start + offset_of!(DebugValueData, data1) as u32) as i32);
626
        emit.i32_add();
627
        emit.local_get(bool_local);
628
        emit.i64_extend_i32_u();
629
        emit.i64_store_raw();
630
        self.cursor = data_start + DEBUG_VALUE_DATA_SIZE as u32;
631
        self.finalize_cursor(emit);
632
    }
633

            
634
    #[spec(
635
        captures: [self.entity_count as prev_count, self.cursor as prev_cursor],
636
        ensures: [
637
132
            self.entity_count == prev_count + 1,
638
132
            self.cursor == prev_cursor + ENTITY_HEADER_SIZE as u32,
639
        ],
640
    )]
641
    pub fn write_delete_entity(
642
        &mut self,
643
        emit: &mut FunctionEmitter,
644
        entity_type_local: u32,
645
        input_header_local: u32,
646
132
    ) {
647
132
        let local = self.output_base_local;
648
132
        let header_start = self.cursor;
649

            
650
        // entity_type from runtime local
651
132
        emit.local_get(local);
652
132
        emit.i32_const((header_start + offset_of!(EntityHeader, entity_type) as u32) as i32);
653
132
        emit.i32_add();
654
132
        emit.local_get(entity_type_local);
655
132
        emit.i32_store8_raw();
656

            
657
132
        emit.store_u8_dynamic(
658
132
            local,
659
132
            header_start + offset_of!(EntityHeader, operation) as u32,
660
132
            Operation::Delete as u8,
661
        );
662
132
        emit.store_u8_dynamic(
663
132
            local,
664
132
            header_start + offset_of!(EntityHeader, flags) as u32,
665
            0,
666
        );
667

            
668
        // Copy 16-byte id (4 × i32)
669
528
        for i in 0..4u32 {
670
528
            emit.local_get(local);
671
528
            emit.i32_const((header_start + offset_of!(EntityHeader, id) as u32 + i * 4) as i32);
672
528
            emit.i32_add();
673
528
            emit.local_get(input_header_local);
674
528
            emit.i32_load((offset_of!(EntityHeader, id) + (i as usize) * 4) as u64);
675
528
            emit.i32_store_raw();
676
528
        }
677

            
678
132
        emit.store_i32_dynamic(
679
132
            local,
680
132
            header_start + offset_of!(EntityHeader, parent_idx) as u32,
681
            -1,
682
        );
683
132
        let data_offset = header_start + ENTITY_HEADER_SIZE as u32;
684
132
        emit.store_i32_dynamic(
685
132
            local,
686
132
            header_start + offset_of!(EntityHeader, data_offset) as u32,
687
132
            data_offset as i32,
688
        );
689
132
        emit.store_i32_dynamic(
690
132
            local,
691
132
            header_start + offset_of!(EntityHeader, data_size) as u32,
692
            0,
693
        );
694

            
695
132
        self.cursor += ENTITY_HEADER_SIZE as u32;
696
132
        self.entity_count += 1;
697
132
        emit.store_i32_dynamic(
698
132
            local,
699
132
            offset_of!(OutputHeader, output_entity_count) as u32,
700
132
            self.entity_count as i32,
701
        );
702
132
        self.finalize_cursor(emit);
703
    }
704

            
705
    #[spec(
706
19016
        requires: [self.cursor > 0],
707
    )]
708
19016
    fn finalize_cursor(&self, emit: &mut FunctionEmitter) {
709
19016
        let local = self.output_base_local;
710
19016
        let end = self.cursor.max(self.strings_end);
711
19016
        emit.store_i32_dynamic(
712
19016
            local,
713
19016
            offset_of!(OutputHeader, strings_offset) as u32,
714
19016
            self.strings_end as i32,
715
        );
716
19016
        emit.store_i32_dynamic(
717
19016
            local,
718
19016
            offset_of!(OutputHeader, next_write_pos) as u32,
719
19016
            end as i32,
720
        );
721
    }
722
}