keleusma 0.2.2

//! 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,
    }
}

/// Per-op WCET extra cycles from text-length-dependent string operations (#49).
///
/// Returns a vector parallel to `chunk.ops`: entry `i` is the extra WCET cycles
/// op `i` incurs beyond its flat `op_cycles` cost because it runs in time
/// proportional to a string length, which the per-opcode table cannot capture.
/// A text comparison (`Op::CmpEq`/`Op::CmpNe`) costs
/// `text_byte_cycles * min(len_a, len_b)` (the VM compares length-first through
/// `string_content_eq`, so the shorter operand bounds the work); a text
/// concatenation (`Op::Add` on text) costs `text_byte_cycles * (len_a + len_b)`;
/// `Op::Len` on text costs `text_byte_cycles * len`. Every other op contributes
/// `0`. An entry of `u32::MAX` marks a text op whose length cannot be statically
/// bounded (a comparison of two unbounded operands, or a concatenation or
/// `Len` of an unbounded operand); the WCET pass rejects such a chunk as
/// non-boundable.
///
/// The analysis maintains the same per-slot [`TextSize`] abstract stack and
/// locals as [`analyze_chunk_text`], reusing its stack discipline through
/// `TextAnalysis::apply_op` for ops that are not length-bearing. It differs in
/// two ways tuned for WCET rather than the heap over-approximation: a `Const`
/// string literal keeps its `Known` length even inside a loop or branch (a
/// literal's bytes are fixed, so `if x == "admin"` in a loop stays bounded via
/// the `min` against the literal), and it emits the per-op cycle term above.
/// Loop-carried and derived text still saturate to `Unbounded` inside control
/// flow, so an accumulation `s = s + x` or a comparison of two such values is
/// rejected.
pub fn chunk_text_wcet_cycles(chunk: &Chunk, text_byte_cycles: u32) -> alloc::vec::Vec<u32> {
    let mut state = TextAnalysis::new(chunk.local_count as usize);
    let mut out: alloc::vec::Vec<u32> = alloc::vec::Vec::with_capacity(chunk.ops.len());
    let mut loop_depth: u32 = 0;
    let mut branch_depth: u32 = 0;
    for op in &chunk.ops {
        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;
        out.push(state.apply_op_wcet(op, chunk, conservative, text_byte_cycles));
        match op {
            Op::EndLoop(_) => loop_depth = loop_depth.saturating_sub(1),
            Op::EndIf => branch_depth = branch_depth.saturating_sub(1),
            _ => {}
        }
    }
    out
}

/// WCET cycles for a text operand of statically-known or unbounded length.
/// `Known(n)` is `text_byte_cycles * n`; `Unbounded` is `u32::MAX`; `NotText`
/// is zero (no text work).
fn len_cycles(t: TextSize, text_byte_cycles: u32) -> u32 {
    match t {
        TextSize::Known(n) => text_byte_cycles.saturating_mul(n),
        TextSize::Unbounded => u32::MAX,
        TextSize::NotText => 0,
    }
}

/// WCET cycles for a text comparison, bounded by the shorter operand (the VM
/// compares length-first). Either operand being `Known` bounds the work; only
/// two `Unbounded` operands are non-boundable (`u32::MAX`).
fn min_len_cycles(a: TextSize, b: TextSize, text_byte_cycles: u32) -> u32 {
    match (a, b) {
        (TextSize::Known(x), TextSize::Known(y)) => text_byte_cycles.saturating_mul(x.min(y)),
        (TextSize::Known(n), TextSize::Unbounded) | (TextSize::Unbounded, TextSize::Known(n)) => {
            text_byte_cycles.saturating_mul(n)
        }
        (TextSize::Unbounded, TextSize::Unbounded) => u32::MAX,
        // A `NotText` operand means a non-text comparison by the type-checker
        // invariant; the caller filters those before reaching here.
        _ => 0,
    }
}

/// 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
            }
        }
    }

    /// Stack-effect of `op` for the WCET length walk, returning the op's extra
    /// WCET cycles (#49). Mirrors [`Self::apply_op`]'s stack discipline but: a
    /// `Const` string literal is not saturated under `conservative` (its byte
    /// length is fixed regardless of control flow), and `Op::CmpEq`/`Op::CmpNe`,
    /// `Op::Add` on text, and `Op::Len` on text emit the length-scaled cycle
    /// term (`u32::MAX` for an unbounded length). Every op that does not bear a
    /// text length delegates to [`Self::apply_op`] for the identical stack
    /// discipline and contributes zero cycles; the heap byte total that delegate
    /// returns is discarded.
    fn apply_op_wcet(
        &mut self,
        op: &Op,
        chunk: &Chunk,
        conservative: bool,
        text_byte_cycles: u32,
    ) -> u32 {
        let sat = |size: TextSize| -> TextSize {
            if conservative {
                match size {
                    TextSize::NotText => TextSize::NotText,
                    _ => TextSize::Unbounded,
                }
            } else {
                size
            }
        };
        match op {
            // A string literal keeps its Known length through control flow; its
            // bytes are fixed, so a comparison against it stays bounded even
            // inside a loop. This is the one place the WCET walk diverges from
            // the saturating heap walk.
            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))
                    }
                    _ => TextSize::NotText,
                };
                self.push(size);
                0
            }
            Op::Add => {
                let b = self.pop();
                let a = self.pop();
                // By the type-checker invariant both operands of a well-typed
                // Add share a type, so a single NotText operand means a non-text
                // (numeric) Add: no text work, NotText result.
                if matches!(a, TextSize::NotText) || matches!(b, TextSize::NotText) {
                    self.push(TextSize::NotText);
                    0
                } else {
                    let result = a.saturating_add(b);
                    self.push(sat(result));
                    // Concatenation copies both operands.
                    len_cycles(result, text_byte_cycles)
                }
            }
            Op::CmpEq | Op::CmpNe => {
                let b = self.pop();
                let a = self.pop();
                // The comparison produces a Bool.
                self.push(TextSize::NotText);
                // A NotText operand means a non-text comparison by the
                // type-checker invariant (both operands share a type); only a
                // text-vs-text comparison bears a length cost.
                if matches!(a, TextSize::NotText) || matches!(b, TextSize::NotText) {
                    0
                } else {
                    min_len_cycles(a, b, text_byte_cycles)
                }
            }
            Op::Len => {
                let a = self.pop();
                // Len yields an Int. Only Len on text walks the bytes
                // (`chars().count()`); Len on a boxed array/tuple is O(1), which
                // `len_cycles(NotText)` reports as zero.
                self.push(TextSize::NotText);
                len_cycles(a, text_byte_cycles)
            }
            // Every other op carries no text length; reuse the shared stack
            // discipline (which saturates loop-carried values as today) and
            // contribute zero cycles. `callee_returns_text` is empty here, so a
            // Call result is conservatively `Unbounded`, which a downstream text
            // op then rejects.
            _ => {
                let _ = self.apply_op(op, chunk, conservative, &[]);
                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(),
            debug_pool: None,
        }
    }

    #[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);
        }
    }

    fn stream_chunk(ops: alloc::vec::Vec<Op>, constants: alloc::vec::Vec<ConstValue>) -> Chunk {
        Chunk {
            name: alloc::string::String::from("main"),
            ops,
            constants,
            struct_templates: alloc::vec::Vec::new(),
            local_count: 0,
            param_count: 0,
            block_type: crate::bytecode::BlockType::Stream,
            param_types: alloc::vec::Vec::new(),
            debug_pool: None,
        }
    }

    #[test]
    fn wcet_literal_comparison_stays_known_inside_a_loop() {
        // The Option-A refinement (#49): inside a loop body a `Const` string
        // literal keeps its `Known` length rather than saturating to
        // `Unbounded` the way the heap walk treats loop-carried values, so a
        // comparison against it is bounded. Two five-byte literals compared in a
        // loop cost `min(5, 5) = 5` cycles, not `u32::MAX`.
        let chunk = stream_chunk(
            alloc::vec![
                Op::Loop(6),
                Op::Const(0),
                Op::Const(1),
                Op::CmpEq,
                Op::PopN(1),
                Op::EndLoop(0),
            ],
            alloc::vec![
                ConstValue::StaticStr(alloc::string::String::from("admin")),
                ConstValue::StaticStr(alloc::string::String::from("admin")),
            ],
        );
        let cycles = chunk_text_wcet_cycles(&chunk, 1);
        assert_eq!(
            cycles[3], 5,
            "CmpEq of two five-byte literals in a loop costs min(5,5), not unbounded"
        );
    }

    #[test]
    fn wcet_comparison_of_two_unbounded_texts_is_unbounded() {
        // Two native-returned texts (`Unbounded`) compared cannot be bounded;
        // the op's WCET term is `u32::MAX`, which the verifier rejects.
        let chunk = stream_chunk(
            alloc::vec![
                Op::CallExternalNative(0, 0),
                Op::CallExternalNative(0, 0),
                Op::CmpEq,
                Op::PopN(1),
            ],
            alloc::vec::Vec::new(),
        );
        let cycles = chunk_text_wcet_cycles(&chunk, 1);
        assert_eq!(
            cycles[2],
            u32::MAX,
            "two unbounded operands are non-boundable"
        );
    }

    #[test]
    fn wcet_comparison_against_a_literal_is_bounded_by_the_literal() {
        // A native text (`Unbounded`) compared against a four-byte literal is
        // bounded at four cycles: the shorter operand caps the work.
        let chunk = stream_chunk(
            alloc::vec![
                Op::CallExternalNative(0, 0),
                Op::Const(0),
                Op::CmpEq,
                Op::PopN(1),
            ],
            alloc::vec![ConstValue::StaticStr(alloc::string::String::from("yyyy"))],
        );
        let cycles = chunk_text_wcet_cycles(&chunk, 1);
        assert_eq!(cycles[2], 4, "min(unbounded, 4) = 4");
    }
}