keleusma 0.2.0

Total Functional Stream Processor with definitive WCET and WCMU verification, targeting no_std + alloc embedded scripting
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
//! Abstract interpretation lattice for tracking text-size bounds
//! through Keleusma bytecode.
//!
//! The WCMU pass needs to bound the worst-case bytes that
//! text-producing opcodes allocate from the arena's top region during
//! a single Stream-to-Reset iteration. `Op::Add` on text operands and
//! the bundled `to_string`, `concat`, and `slice` natives all
//! allocate a `KString` whose length depends on the operand lengths
//! at runtime. The verifier cannot inspect the runtime values, so it
//! tracks an upper bound through abstract interpretation over a
//! per-slot lattice.
//!
//! ## Lattice
//!
//! The lattice has two elements:
//!
//! - `TextSize::Known(n)`: the slot carries a text value whose UTF-8
//!   byte length is at most `n`.
//! - `TextSize::Unbounded`: the slot carries a text value whose
//!   length the analysis cannot bound, or carries a non-text value
//!   for which size tracking is meaningless. Both interpretations
//!   collapse to the conservative top of the lattice.
//!
//! The lattice has `Known(0)` as its bottom and `Unbounded` as its
//! top. Join is the maximum of two `Known` values, saturating to
//! `Unbounded` if either argument is `Unbounded`. Addition is the
//! saturating sum, propagating `Unbounded` if either argument is
//! `Unbounded` or if the integer sum would exceed `u32::MAX`.
//!
//! ## Scope of the present implementation
//!
//! V0.2.0 ships the lattice, the arithmetic primitives, and a
//! conservative linear analysis (`chunk_text_heap_alloc`) that
//! tracks text sizes through straight-line code. The analysis is
//! integrated with [`crate::verify::wcmu_stream_iteration`] so that
//! programs whose text-producing opcodes exceed the arena's top
//! region are rejected at the safe constructor under the default
//! [`crate::vm::OverflowPolicy::Reject`].
//!
//! ## Conservative cases
//!
//! Text operations inside a loop body or inside an If/Else branch
//! widen the produced lattice value to [`TextSize::Unbounded`],
//! which propagates an unbounded heap contribution. Calls produce
//! `Unbounded` return values because the analysis does not propagate
//! per-slot information across call boundaries; native attestation
//! through `Vm::set_native_bounds` is the load-bearing source of
//! truth for the heap contribution of registered natives.

use alloc::vec::Vec;

use crate::bytecode::{Chunk, ConstValue, NOMINAL_COST_MODEL, Op, OpCost, OpCostContext};

/// Upper bound on the UTF-8 byte length of a text value carried in
/// an operand-stack slot or local variable.
///
/// See the module-level documentation for the lattice semantics.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum TextSize {
    /// The slot carries a value whose static type is known to be
    /// non-text (integer, boolean, float, unit, composite). Text
    /// operations against this value contribute zero to the heap.
    NotText,
    /// The slot carries a text value whose length is at most `n`
    /// bytes.
    Known(u32),
    /// The slot carries a text value whose length the analysis
    /// cannot bound, or whose static type is uncertain. Text
    /// operations against this value contribute the saturated
    /// upper bound (`u32::MAX`) to the heap.
    Unbounded,
}

impl TextSize {
    /// The bottom of the text lattice. Equivalent to `Known(0)`.
    pub const ZERO: TextSize = TextSize::Known(0);

    /// The top of the text lattice.
    pub const UNBOUNDED: TextSize = TextSize::Unbounded;

    /// Saturating addition of two text-size bounds.
    ///
    /// `NotText + NotText` is `NotText` (no text value involved).
    /// `NotText + text` and `text + NotText` are the text operand,
    /// preserving its bound (this case arises in incomplete tracking
    /// rather than in well-typed Add, since the Keleusma type
    /// checker rejects mixed-type Add). Two text operands sum
    /// saturating to `Unbounded` on overflow or on either operand
    /// being `Unbounded`.
    pub fn saturating_add(self, other: TextSize) -> TextSize {
        match (self, other) {
            (TextSize::NotText, TextSize::NotText) => TextSize::NotText,
            (TextSize::NotText, t) | (t, TextSize::NotText) => t,
            (TextSize::Unbounded, _) | (_, TextSize::Unbounded) => TextSize::Unbounded,
            (TextSize::Known(a), TextSize::Known(b)) => match a.checked_add(b) {
                Some(sum) if sum < u32::MAX => TextSize::Known(sum),
                _ => TextSize::Unbounded,
            },
        }
    }

    /// Saturating join (maximum) of two text-size bounds.
    ///
    /// `NotText` joined with anything yields that thing: the join
    /// represents the value at a control-flow merge, and a non-text
    /// merging with a text indicates the analysis lost track of the
    /// static type. The conservative reading is to preserve the
    /// text operand's bound.
    pub fn join(self, other: TextSize) -> TextSize {
        match (self, other) {
            (TextSize::NotText, t) | (t, TextSize::NotText) => t,
            (TextSize::Unbounded, _) | (_, TextSize::Unbounded) => TextSize::Unbounded,
            (TextSize::Known(a), TextSize::Known(b)) => TextSize::Known(a.max(b)),
        }
    }

    /// Project the lattice value to a `u32` for use as an operand
    /// length in an [`OpCostContext`]. `Unbounded` and `NotText`
    /// both project to `u32::MAX`; the dynamic-cost evaluator
    /// receives the projection only for genuine text operations and
    /// callers must filter `NotText` operands before evaluation.
    pub fn as_u32(self) -> u32 {
        match self {
            TextSize::Known(n) => n,
            TextSize::Unbounded | TextSize::NotText => u32::MAX,
        }
    }
}

/// Build an [`OpCostContext`] from a pair of [`TextSize`] operand
/// bounds. Convenience helper for the integration point where the
/// abstract interpretation pass evaluates an `OpCost::Dynamic` cost.
pub fn op_cost_context(lhs: TextSize, rhs: TextSize) -> OpCostContext {
    OpCostContext {
        lhs_text_len: lhs.as_u32(),
        rhs_text_len: rhs.as_u32(),
    }
}

/// Result of the per-chunk text-allocation analysis.
///
/// `heap_alloc` is the upper bound on bytes allocated to the arena's
/// top region by text-producing opcodes in the chunk. `returns_text`
/// is `true` if any execution path through the chunk leaves a value
/// of text type (Known or Unbounded) on top of the abstract stack at
/// a `Return` op or at the end of the chunk's ops. `yields_text` is
/// `true` if any execution path leaves a text value on top of the
/// abstract stack at an `Op::Yield`.
///
/// The `returns_text` flag is used by callers of this analysis to
/// propagate accurate per-callee text-ness through the module-level
/// WCMU pass. A chunk that returns a non-text scalar (Word, Bool,
/// fixed) does not contribute text to its caller through the call's
/// return value. The previous policy treated every `Op::Call` return
/// as `Unbounded`, which forced any later `Op::Add` between two
/// such return values to saturate the heap cost to `u32::MAX`. With
/// per-callee text-ness information, calls returning non-text scalars
/// push `NotText`, restoring the type-checker's "either operand
/// NotText implies result NotText" invariant.
///
/// The `yields_text` flag is used by the ephemerality refinement.
/// A Stream chunk that never yields a text-typed value across the
/// host-VM boundary may be admitted as ephemeral even when the
/// surface signature declares a `Text` yield type but every concrete
/// yield path produces a non-text value.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct ChunkTextAnalysis {
    /// Upper bound on text heap allocation for the chunk.
    pub heap_alloc: u32,
    /// Whether the chunk may return a text-typed value.
    pub returns_text: bool,
    /// Whether the chunk may yield a text-typed value across the
    /// host-VM boundary at any `Op::Yield`.
    pub yields_text: bool,
}

/// Conservative upper bound on the bytes allocated to the arena's
/// top region by text-producing opcodes in `chunk`.
///
/// See [`analyze_chunk_text`] for the underlying analysis. This
/// function preserves the original API by calling
/// `analyze_chunk_text(chunk, &[])`, which uses the conservative
/// default that every callee may return text.
pub fn chunk_text_heap_alloc(chunk: &Chunk) -> u32 {
    analyze_chunk_text(chunk, &[]).heap_alloc
}

/// Per-chunk text-allocation analysis with optional per-callee
/// text-ness information.
///
/// Walks the chunk's ops linearly, maintaining a per-slot
/// [`TextSize`] lattice over an abstract operand stack and local
/// variables. For each text-producing opcode, evaluates the dynamic
/// [`OpCost`] from [`NOMINAL_COST_MODEL`] against the operand lattice
/// values and accumulates the cost into the returned heap total.
///
/// At each `Op::Call(callee_idx, _)`, the analysis pushes
/// `TextSize::Unbounded` if `callee_returns_text` reports the callee
/// as text-returning, or `TextSize::NotText` otherwise. An out-of-
/// range `callee_idx` defaults to the conservative `Unbounded`. An
/// empty `callee_returns_text` slice (the default when no callgraph
/// information is available) collapses to the original conservative
/// policy.
///
/// At each `Op::Return`, the analysis peeks the top of the abstract
/// stack. If the peeked value is not `NotText`, the chunk's
/// `returns_text` flag is set. At end of ops, the same check is
/// applied to handle chunks with implicit return through fall-
/// through.
///
/// ## Soundness
///
/// The pass is sound for straight-line code, where stack and local
/// state at each program point is well-defined. Control flow is
/// handled conservatively: text values written inside a loop body or
/// inside an If/Else branch saturate to [`TextSize::Unbounded`],
/// causing any subsequent `Op::Add` against them to report the
/// dynamic cost as `u32::MAX`.
///
/// The accumulated heap total saturates at `u32::MAX`. A returned
/// `heap_alloc` of `u32::MAX` signals that the analysis could not
/// bound the text allocation and the caller should treat the chunk's
/// text heap as unbounded.
pub fn analyze_chunk_text(chunk: &Chunk, callee_returns_text: &[bool]) -> ChunkTextAnalysis {
    let mut state = TextAnalysis::new(chunk.local_count as usize);
    let mut total: u32 = 0;
    let mut loop_depth: u32 = 0;
    let mut branch_depth: u32 = 0;
    let mut returns_text = false;
    let mut yields_text = false;

    for op in &chunk.ops {
        // Track structural depth so writes inside any conditional or
        // looping region produce Unbounded results. Increment before
        // dispatch so opcodes that delimit the region see the new
        // depth.
        match op {
            Op::Loop(_) => loop_depth = loop_depth.saturating_add(1),
            Op::If(_) => branch_depth = branch_depth.saturating_add(1),
            _ => {}
        }
        let conservative = loop_depth > 0 || branch_depth > 0;

        // Peek the boundary-crossing value before apply_op pops it.
        // `Op::Return` crosses out of a function back to its caller
        // (or out of the entry chunk back to the host). `Op::Yield`
        // crosses out of a Stream iteration back to the host. Both
        // are arena-boundary events for the ephemerality refinement.
        match op {
            Op::Return => {
                let top = state.peek();
                if !matches!(top, TextSize::NotText) {
                    returns_text = true;
                }
            }
            Op::Yield => {
                let top = state.peek();
                if !matches!(top, TextSize::NotText) {
                    yields_text = true;
                }
            }
            _ => {}
        }

        let contribution = state.apply_op(op, chunk, conservative, callee_returns_text);
        total = total.saturating_add(contribution);
        if total == u32::MAX {
            return ChunkTextAnalysis {
                heap_alloc: u32::MAX,
                returns_text,
                yields_text,
            };
        }
        match op {
            Op::EndLoop(_) => loop_depth = loop_depth.saturating_sub(1),
            Op::EndIf => branch_depth = branch_depth.saturating_sub(1),
            _ => {}
        }
    }

    // Implicit return through end of ops: peek the final stack top.
    let final_top = state.peek();
    if !matches!(final_top, TextSize::NotText) {
        returns_text = true;
    }

    ChunkTextAnalysis {
        heap_alloc: total,
        returns_text,
        yields_text,
    }
}

/// Internal abstract state for `chunk_text_heap_alloc`.
///
/// Mirrors the operand stack and local-variable bindings as
/// [`TextSize`] lattice values. Non-text values are tracked as
/// [`TextSize::Unbounded`] for simplicity. Stack-effect overflow
/// (e.g. popping from an empty abstract stack) is treated as a
/// best-effort scenario and yields [`TextSize::Unbounded`] for the
/// popped value, matching the conservative reading.
struct TextAnalysis {
    stack: Vec<TextSize>,
    locals: Vec<TextSize>,
}

impl TextAnalysis {
    fn new(local_count: usize) -> Self {
        Self {
            stack: Vec::new(),
            // Locals start as `NotText`. The compiler initialises
            // each slot before any read, so this is the value a
            // newly entered chunk sees before the first SetLocal.
            // Parameter slots are also `NotText` initially; tighter
            // tracking would require the caller to supply per-param
            // bounds.
            locals: alloc::vec![TextSize::NotText; local_count],
        }
    }

    fn pop(&mut self) -> TextSize {
        self.stack.pop().unwrap_or(TextSize::NotText)
    }

    fn push(&mut self, size: TextSize) {
        self.stack.push(size);
    }

    fn peek(&self) -> TextSize {
        self.stack.last().copied().unwrap_or(TextSize::NotText)
    }

    /// Apply the stack effect of `op` and return the heap bytes
    /// allocated by `op` for text. Non-text-producing opcodes return
    /// zero and update only the abstract stack/local state.
    ///
    /// When `conservative` is true, every value written to the
    /// abstract stack or to a local is saturated to
    /// [`TextSize::Unbounded`]. Used inside loops and conditional
    /// branches where the pass cannot reliably narrow the value.
    ///
    /// `callee_returns_text` is the per-chunk text-ness array used
    /// for `Op::Call`. An empty slice or an out-of-range index
    /// defaults to `true` (conservative).
    fn apply_op(
        &mut self,
        op: &Op,
        chunk: &Chunk,
        conservative: bool,
        callee_returns_text: &[bool],
    ) -> u32 {
        // `sat` widens a tracked text bound to `Unbounded` when the
        // op runs inside a loop or branch. `NotText` is preserved
        // because non-text values do not change category under
        // control-flow widening.
        let sat = |size: TextSize| -> TextSize {
            if conservative {
                match size {
                    TextSize::NotText => TextSize::NotText,
                    _ => TextSize::Unbounded,
                }
            } else {
                size
            }
        };
        match op {
            Op::Const(idx) => {
                let size = match chunk.constants.get(*idx as usize) {
                    Some(ConstValue::StaticStr(s)) => {
                        let len = u32::try_from(s.len()).unwrap_or(u32::MAX - 1);
                        TextSize::Known(len.min(u32::MAX - 1))
                    }
                    Some(_) => TextSize::NotText,
                    None => TextSize::NotText,
                };
                self.push(sat(size));
                0
            }
            Op::Add => {
                let b = self.pop();
                let a = self.pop();
                // The Keleusma type checker rules out mixed
                // text/non-text Add at the surface. Both operands of
                // a well-typed `Op::Add` therefore share the same
                // surface type, so a single operand being
                // statically `NotText` is sufficient evidence that
                // the partner is also non-text in the type-system
                // sense, regardless of whether the partner is
                // tracked as `Unbounded` because of upstream
                // imprecision (e.g. a `Call` return widened to
                // `Unbounded`). The previous policy demanded both
                // operands carry `NotText` and conservatively
                // treated any `Unbounded` operand as text, which
                // forced every chunk that combined a function-call
                // result with an integer to saturate its heap bound
                // to `u32::MAX`.
                //
                // Adversarial bytecode that violates the type-
                // checker invariant could under-report its heap
                // here, but actual runtime allocation is still
                // bounded by the arena and surfaces as
                // `VmError::OutOfArena` on exhaustion. The static
                // bound is therefore an over- or under-approximation
                // only relative to the type-checker invariant; the
                // safety contract remains intact.
                let (result, dynamic_cost) =
                    if matches!(a, TextSize::NotText) || matches!(b, TextSize::NotText) {
                        (TextSize::NotText, 0)
                    } else {
                        let context = op_cost_context(a, b);
                        let cost = match NOMINAL_COST_MODEL.heap_alloc_cost(op, chunk) {
                            OpCost::Dynamic(f) => f(&context),
                            OpCost::Fixed(n) => n,
                        };
                        (a.saturating_add(b), cost)
                    };
                self.push(sat(result));
                dynamic_cost
            }
            Op::GetLocal(i) => {
                let size = self
                    .locals
                    .get(*i as usize)
                    .copied()
                    .unwrap_or(TextSize::NotText);
                self.push(sat(size));
                0
            }
            Op::SetLocal(i) => {
                let value = self.pop();
                if let Some(slot) = self.locals.get_mut(*i as usize) {
                    *slot = sat(value);
                }
                0
            }
            Op::PopN(n) => {
                for _ in 0..*n {
                    self.pop();
                }
                0
            }
            Op::Dup => {
                let top = self.peek();
                self.push(top);
                0
            }
            Op::Call(callee_idx, n_args) => {
                for _ in 0..*n_args {
                    self.pop();
                }
                // Look up the callee's text-ness. The module-level
                // analysis builds this array in topological order
                // before each caller runs. If the callee is known to
                // return a non-text value (Word, Bool, fixed), we
                // push `NotText` so the type-checker's invariant
                // ("either operand NotText implies result NotText"
                // in Op::Add) restores correctly. If the callee
                // returns text, or if the array does not yet carry
                // the callee's entry, we push `Unbounded` as the
                // conservative default.
                let returns_text = callee_returns_text
                    .get(*callee_idx as usize)
                    .copied()
                    .unwrap_or(true);
                let pushed = if returns_text {
                    TextSize::Unbounded
                } else {
                    TextSize::NotText
                };
                self.push(sat(pushed));
                0
            }
            Op::CallVerifiedNative(_, n_args) | Op::CallExternalNative(_, n_args) => {
                for _ in 0..*n_args {
                    self.pop();
                }
                self.push(TextSize::Unbounded);
                0
            }
            Op::Yield => {
                self.pop();
                0
            }
            Op::Return => {
                self.pop();
                0
            }
            Op::If(_) => {
                // If consumes a boolean.
                self.pop();
                0
            }
            Op::Else(_) | Op::EndIf | Op::Loop(_) | Op::EndLoop(_) => 0,
            Op::Break(_) => 0,
            Op::BreakIf(_) => {
                self.pop();
                0
            }
            _ => {
                // Other opcodes do not produce text. Apply the
                // recorded stack growth and shrink and treat any
                // pushed value as non-text.
                let shrink = op.stack_shrink() as usize;
                for _ in 0..shrink {
                    self.pop();
                }
                let growth = op.stack_growth() as usize;
                for _ in 0..growth {
                    self.push(TextSize::NotText);
                }
                0
            }
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn add_known_values() {
        assert_eq!(
            TextSize::Known(3).saturating_add(TextSize::Known(5)),
            TextSize::Known(8)
        );
        assert_eq!(
            TextSize::ZERO.saturating_add(TextSize::ZERO),
            TextSize::ZERO
        );
    }

    #[test]
    fn add_saturates_to_unbounded_on_overflow() {
        assert_eq!(
            TextSize::Known(u32::MAX - 1).saturating_add(TextSize::Known(1)),
            TextSize::Unbounded
        );
        assert_eq!(
            TextSize::Known(u32::MAX / 2 + 1).saturating_add(TextSize::Known(u32::MAX / 2 + 1)),
            TextSize::Unbounded
        );
    }

    #[test]
    fn add_propagates_unbounded() {
        assert_eq!(
            TextSize::Unbounded.saturating_add(TextSize::Known(5)),
            TextSize::Unbounded
        );
        assert_eq!(
            TextSize::Known(5).saturating_add(TextSize::Unbounded),
            TextSize::Unbounded
        );
        assert_eq!(
            TextSize::Unbounded.saturating_add(TextSize::Unbounded),
            TextSize::Unbounded
        );
    }

    #[test]
    fn join_known_takes_max() {
        assert_eq!(
            TextSize::Known(3).join(TextSize::Known(5)),
            TextSize::Known(5)
        );
        assert_eq!(
            TextSize::Known(7).join(TextSize::Known(2)),
            TextSize::Known(7)
        );
    }

    #[test]
    fn join_propagates_unbounded() {
        assert_eq!(
            TextSize::Unbounded.join(TextSize::Known(5)),
            TextSize::Unbounded
        );
        assert_eq!(
            TextSize::Known(5).join(TextSize::Unbounded),
            TextSize::Unbounded
        );
    }

    #[test]
    fn as_u32_projects_unbounded_to_max() {
        assert_eq!(TextSize::Known(42).as_u32(), 42);
        assert_eq!(TextSize::Unbounded.as_u32(), u32::MAX);
        assert_eq!(TextSize::ZERO.as_u32(), 0);
    }

    #[test]
    fn op_cost_context_carries_lattice_values() {
        let ctx = op_cost_context(TextSize::Known(10), TextSize::Known(20));
        assert_eq!(ctx.lhs_text_len, 10);
        assert_eq!(ctx.rhs_text_len, 20);
        let ctx_unbounded = op_cost_context(TextSize::Unbounded, TextSize::Known(5));
        assert_eq!(ctx_unbounded.lhs_text_len, u32::MAX);
        assert_eq!(ctx_unbounded.rhs_text_len, 5);
    }

    use crate::bytecode::{BlockType, Chunk, ConstValue, Op};
    use alloc::string::String as StdString;
    use alloc::vec;

    fn make_chunk(ops: Vec<Op>, constants: Vec<ConstValue>, locals: u16) -> Chunk {
        Chunk {
            name: StdString::from("test"),
            ops,
            constants,
            struct_templates: Vec::new(),
            local_count: locals,
            param_count: 0,
            block_type: BlockType::Func,
            param_types: Vec::new(),
        }
    }

    #[test]
    fn text_heap_alloc_empty_chunk_is_zero() {
        let chunk = make_chunk(vec![Op::Return], vec![], 0);
        assert_eq!(chunk_text_heap_alloc(&chunk), 0);
    }

    #[test]
    fn text_heap_alloc_static_literal_alone_is_zero() {
        // Pushing a string literal does not allocate from the arena;
        // static strings live in the rodata region.
        let chunk = make_chunk(
            vec![Op::Const(0), Op::Return],
            vec![ConstValue::StaticStr(StdString::from("hello"))],
            0,
        );
        assert_eq!(chunk_text_heap_alloc(&chunk), 0);
    }

    #[test]
    fn text_heap_alloc_single_concat_returns_sum_of_lengths() {
        // "ab" + "cdef" allocates 6 bytes.
        let chunk = make_chunk(
            vec![Op::Const(0), Op::Const(1), Op::Add, Op::Return],
            vec![
                ConstValue::StaticStr(StdString::from("ab")),
                ConstValue::StaticStr(StdString::from("cdef")),
            ],
            0,
        );
        assert_eq!(chunk_text_heap_alloc(&chunk), 6);
    }

    #[test]
    fn text_heap_alloc_doubling_pattern_accumulates_geometric_series() {
        // s = "a"; s = s + s; s = s + s; allocates 2 + 4 = 6 bytes.
        // Geometric series 2 + 4 + 8 + ... starts after the first
        // assignment.
        let chunk = make_chunk(
            vec![
                Op::Const(0),    // push "a"  -> stack: [Known(1)]
                Op::SetLocal(0), // s = "a"   -> locals[0] = Known(1)
                Op::GetLocal(0),
                Op::GetLocal(0),
                Op::Add,         // s + s     -> allocates 2 bytes
                Op::SetLocal(0), // s = s + s -> locals[0] = Known(2)
                Op::GetLocal(0),
                Op::GetLocal(0),
                Op::Add,         // s + s     -> allocates 4 bytes
                Op::SetLocal(0), // s = s + s -> locals[0] = Known(4)
                Op::Return,
            ],
            vec![ConstValue::StaticStr(StdString::from("a"))],
            1,
        );
        assert_eq!(chunk_text_heap_alloc(&chunk), 6);
    }

    #[test]
    fn text_heap_alloc_saturates_for_long_doubling_chain() {
        // The FAQ exponential-string-concat example. Sixty doublings
        // of a 1-byte string cumulatively allocate more than u32::MAX
        // bytes; the analysis saturates to u32::MAX at the moment the
        // produced size crosses the lattice's representable range.
        let mut ops = vec![Op::Const(0), Op::SetLocal(0)];
        for _ in 0..60 {
            ops.push(Op::GetLocal(0));
            ops.push(Op::GetLocal(0));
            ops.push(Op::Add);
            ops.push(Op::SetLocal(0));
        }
        ops.push(Op::Return);
        let chunk = make_chunk(ops, vec![ConstValue::StaticStr(StdString::from("a"))], 1);
        assert_eq!(chunk_text_heap_alloc(&chunk), u32::MAX);
    }

    #[test]
    fn text_heap_alloc_inside_loop_saturates_to_unbounded() {
        // Op::Add inside a loop body cannot be tightly bounded by the
        // linear pass, so the contribution saturates to u32::MAX.
        let chunk = make_chunk(
            vec![
                Op::Loop(6), // 0
                Op::Const(0),
                Op::Const(0),
                Op::Add,
                Op::PopN(1),
                Op::EndLoop(0), // 5
                Op::Return,
            ],
            vec![ConstValue::StaticStr(StdString::from("a"))],
            0,
        );
        assert_eq!(chunk_text_heap_alloc(&chunk), u32::MAX);
    }

    #[test]
    fn text_heap_alloc_call_native_result_is_unbounded() {
        // A native function call produces an Unbounded return that
        // any subsequent Op::Add against will saturate to u32::MAX.
        let chunk = make_chunk(
            vec![
                Op::Const(0),
                Op::CallVerifiedNative(0, 1), // some host-attested native
                Op::Const(0),
                Op::Add, // adds an Unbounded native result to "a"
                Op::Return,
            ],
            vec![ConstValue::StaticStr(StdString::from("a"))],
            0,
        );
        assert_eq!(chunk_text_heap_alloc(&chunk), u32::MAX);
    }

    #[test]
    fn doubling_pattern_saturates_after_thirty_two_iterations() {
        // The FAQ exponential-string-concat example doubles a 1-byte
        // string sixty times. Tracking the size lattice through the
        // doubling chain reaches `Unbounded` once the size exceeds
        // u32::MAX, which happens at the thirty-second doubling
        // (2^31 = 2_147_483_648, 2^32 - 1 = u32::MAX).
        let mut size = TextSize::Known(1);
        for _ in 0..31 {
            size = size.saturating_add(size);
        }
        assert_eq!(size, TextSize::Known(1u32 << 31));
        // The next doubling crosses the u32::MAX boundary.
        size = size.saturating_add(size);
        assert_eq!(size, TextSize::Unbounded);
        // Further doublings stay at Unbounded.
        for _ in 0..30 {
            size = size.saturating_add(size);
            assert_eq!(size, TextSize::Unbounded);
        }
    }
}