Keleusma V0.2.0

[0.2.0] - 2026-05-21

V0.2.0 is the first publicly released line. V0.1.x circulated as a pre-release. The headline additions are cryptographic module signing, the V0.2.0 ISA reset, information-flow labels including negative labels, calibrated WCET cost models from the new keleusma-bench crate, and a substantial documentation reorganization. The wire format is incompatible with V0.1.x; recompile artefacts. The release also retires closures, f-strings, and the text bundled DSL; programs that used those features need rewrites under host-registered natives. See the breaking-change subsections below for the migration surface; the V0.1.x line had narrow adoption so the discontinuity is acceptable.

Cryptographic module signing (R42)

V0.2.0 adds optional Ed25519 signing of compiled bytecode. The mechanism enforces origin authenticity and tamper resistance for modules delivered to embedded targets; the motivating use case is the mothership-to-daughtership UAV scenario where a mothership compiles per-mission scripts and a daughtership verifies them over a bandwidth-constrained link.

• Surface syntax. A new signed modifier on the entry function declaration (signed fn main, signed yield main, signed loop main) emits FLAG_REQUIRES_SIGNATURE = 0x02 in the module header flags. The modifier is admissible only on the entry function; a signed modifier on a helper rejects at compile time with a diagnostic naming the offending declaration.
• Wire format. The framing header extends through the existing header_length: u16 field. Unsigned modules retain the 64-byte base; signed modules grow to 64 + 8 (signature metadata) + signature_length + padding-to-8 bytes. Bytes 64..72 hold the signature metadata (scheme_id byte, reserved byte, signature_length: u16, reserved u32); the signature payload follows. Ed25519 (scheme_id = 1) is the only V0.2.0 scheme; the byte is the substrate for future migrations to ECDSA / ML-DSA / LMS without an ABI break.
• Message convention. The signature covers the full framed buffer with the signature payload bytes and the CRC trailer bytes zeroed. Both signer and verifier reconstruct that view.
• Cargo gate. A new optional signatures feature, off by default, brings ed25519-dalek 2 under no_std + alloc + zeroize. Builds without the feature accept unsigned bytecode normally and reject signed bytecode with LoadError::SignaturesUnsupported. The signed surface keyword still parses without the feature so source files remain portable across configurations.
• Runtime API. New Vm::load_signed_bytes(bytes, arena, &keys) for the initial signed load. New Vm::replace_module_from_bytes(bytes, initial_data) for signed hot-swap that consults the VM's trust matrix. New Vm::register_verifying_key, Vm::clear_verifying_keys, Vm::verifying_keys_len to manage the matrix. Vm::new rejects modules carrying FLAG_REQUIRES_SIGNATURE directly because the signature info is lost when the Module is decoded; callers use the byte-aware entry points. Vm::new_unchecked skips the check consistent with its existing trust-skip semantics.
• Wire-format API. New wire_format::module_to_signed_wire_bytes(module, signing_key), wire_format::verify_module_signature(bytes, &keys), wire_format::parse_signature_metadata(bytes, header_length), wire_format::header_requires_signature(bytes).
• CLI. keleusma compile script.kel --signing-key seed.bin -o out.bin signs (requires signed on the entry function). keleusma run out.bin --verifying-key key.pub (repeatable) populates the trust matrix. keleusma keygen --seed seed.bin --public pub.bin generates a fresh Ed25519 keypair; the seed file is written with 0o600 permissions on Unix; existing files are not overwritten. Key file format is raw 32-byte Ed25519 seed and public key respectively.
• Hardware verification. examples/rtos gains a keleusma-signatures feature passthrough and a boot-time setup::run_signed_self_test path. The N6 binary built with the feature on flashes, verifies an embedded signed fixture at boot via verify_module_signature, logs signed self-test: verify_module_signature succeeded, and enters the scheduler loop. Without the feature, the firmware behaviour is unchanged.

Documentation lives in R42 (docs/decisions/RESOLVED.md), the wire-format spec (docs/spec/WIRE_FORMAT.md), and the migration matrix for future schemes (secret/SIGNATURE_SCHEME_MIGRATION.md, internal).

Wire-format reset

V0.2.0 publishes a new bytecode wire format and the framing-header version field resets to 1. The format is the result of an ISA audit covering opcode consolidation, opcode addition, encoding regularization, and a section-partitioned body layout. See docs/spec/INSTRUCTION_SET.md for the full opcode listing and docs/architecture/EXECUTION_MODEL.md for the wire format specification.

V0.1.x runtimes cannot read V0.2.0 bytecode. V0.2.0 runtimes cannot read V0.1.x bytecode. The version-field reset signals the discontinuity to hosts; existing artefacts must be recompiled against the V0.2.0 toolchain.

The reset is acceptable because the V0.1.x line has narrow adoption. Future wire-format changes will continue to bump the version field rather than reset it.

ISA changes (V0.1.x → V0.2.0)

• Consolidations. PushTrue, PushFalse, PushUnit, PushNone, WrapSome, and Pop are removed. PushImmediate(u8) replaces the four constant-pushing variants and additionally encodes small Int literals (Int(0) through Int(15)) inline. PopN(u8) replaces Pop; single-slot pops emit PopN(1). Op::Add, Op::Sub, Op::Mul, and Op::Neg remain in the instruction set but no longer accept Value::Int operands; the compiler routes Int arithmetic through CheckedAdd / CheckedSub / CheckedMul / CheckedNeg followed by PopN(2) to discard the unused high and flag outputs. The unchecked opcodes retain their Byte, Fixed, and Float arms.
• Drops. CallIndirect, PushFunc, MakeClosure, MakeRecursiveClosure are removed along with the corresponding Value::Func runtime variant. Closure-shaped surface expressions and first-class function values are rejected at the type-checker stage with a diagnostic that names the construct. The closure-hoisting compiler pass is retired.
• Splits. CallNative is removed; every native call compiles to either CallVerifiedNative or CallExternalNative. The two are distinguished by the source-level use declaration: use module::name produces CallVerifiedNative; use external module::name produces CallExternalNative. The host's registration ABI mirrors the distinction through Vm::register_verified_native(name, fn, wcet, wcmu_bytes) and Vm::register_external_native(name, fn, max_invocations_per_iteration); the new Vm::verify_native_classifications walks every call site and rejects a classification mismatch as VmError::VerifyError at the entry of Vm::call_function (cached after the first successful walk). Vm::register_native and Vm::register_fn continue to ascribe the verified classification, preserving backward compatibility for hosts that do not need external semantics. External natives' per-call WCMU contribution is explicitly zeroed at the verifier handoff; chunk-level integration of max_invocations_per_iteration is forward-looking.
• Additions. Five bitwise opcodes: BitAnd, BitOr, BitXor, Shl, Shr. Enables script-level bit manipulation and is a prerequisite for the deferred B19 Multiword work.
• Operand narrowing. Control-flow opcodes (If, Else, Loop, EndLoop, Break, BreakIf) carry u16 jump targets instead of u32. Chunks are capped at 65,535 ops as a hard CompileError; the compiler emits a CompileWarning at 80% of the cap (52,428 ops) prompting decomposition into helpers. The new compile_with_warnings entry point returns (Module, Vec<CompileWarning>); compile and compile_with_target discard the warnings for callers that do not need them.

Total opcode count at the close of Phase 5 is 69. The audit's aspirational target of 65 anticipated dropping Add / Sub / Mul / Neg (Consolidation B) and CallIndirect / PushFunc / MakeClosure / MakeRecursiveClosure (Phase 4); Phase 5 additionally retired CallNative in favor of the verified-versus-external split. Consolidation B narrowed Add / Sub / Mul / Neg to Byte / Fixed / Float operand types rather than removing them, because the runtime still needs entry points for those non-Int wrapping or IEEE 754 arithmetic forms. The remaining gap of four opcodes against the aspirational target is the cost of preserving direct script-level support for Byte, Fixed, and Float arithmetic alongside the checked-Int family.

Wire format changes

• Fixed-size opcode records. Each opcode is a 4-byte record: 7-bit opcode_id plus a 1-bit parity in byte zero, 3 bytes inline operand or operand pool index in bytes one through three. Inline operand fields cover 65 of 69 V0.2.0 opcodes; the remaining 4 reference an operand pool.
• Separate operand pool. Compound operands ((u16, u16) and (u16, u16, u8)) live in 8-byte aligned pool entries with a type tag and parity byte.
• Section-partitioned body. The framing header carries offsets and lengths for the opcode stream, operand pool, and auxiliary body. Each section is independently relocatable.
• Framing header grows from 32 bytes to 64 bytes to carry the new section offsets and lengths.

The rkyv-archived encoding survives only for the auxiliary body. V0.2.0 Phase 7a publishes the specification and the wire-format types. Phase 7b ships wire_format::module_to_wire_bytes and module_from_wire_bytes as a parallel route. Phase 7c cuts the default Module::to_bytes / Module::from_bytes / Module::access_bytes over to the wire format: to_bytes delegates to module_to_wire_bytes; from_bytes delegates to module_from_wire_bytes; access_bytes returns &ArchivedWireAuxBody. The VM's zero-copy execution path reads opcodes through the opcode stream section and accesses the auxiliary body via the wire-format header offsets. The legacy 32-byte framing header, the op_from_archived conversion, and the legacy CRC residue constants retire alongside the cutover. Phase 8 drops the Archive, Serialize, Deserialize derives from Module, Chunk, and Op now that the wire format owns serialization; the user-facing FAQ, cookbook, embedding guide, and rejection guide are realigned with the V0.2.0 ISA.

Changed

• Surface text type renamed String to Text. The Keleusma surface keyword for textual data is now Text. The former name persistently confused readers given Rust's owned String type. The runtime representation (Value::StaticStr, Value::KStr) is unchanged. Existing scripts must rename String to Text in parameter and return-type annotations.
• Op::Add on text operands is now arena-resident. Concatenation through + no longer routes through the global allocator; the result is Value::KStr allocated through KString::alloc in the arena's top region. Allocation failure surfaces as VmError::OutOfArena. The bundled to_string, concat, and slice natives likewise produce arena-allocated KStr results.
• Value::DynStr removed. The global-heap dynamic-string variant present in V0.1.x is gone. All dynamic strings are arena-resident via Value::KStr. The cross-yield prohibition continues to apply.
• register_utility_natives is now arena-aware by default. The non-context variants of to_string, concat, and slice were removed. register_utility_natives_with_ctx is retained as a deprecated alias for compatibility.

Changed

• B17 resolved as not actionable. A cargo-bloat profiling pass on the STM32N6570-DK bare-metal binary confirmed that embassy-stm32 contributes essentially nothing to the image footprint: 1.9 KiB across all three feature modes, less than 2% of the smallest mode and 0.3% of the full-pipeline mode. The dominant contributors are inside the keleusma crate itself: Vm::run (49.8 KiB), compile_with_target (38.4 KiB), typecheck::run_check (23.5 KiB), typecheck::type_of_expr (22.3 KiB), and the parser / monomorphizer methods. Recorded future-pass targets: opcode-dispatch splitting in Vm::run, BTreeMap monomorphization consolidation, gating the monomorphizer behind a feature for workloads that do not use generics, and auditing residual Debug impl retention. None require embassy changes.

Added

• B13 final follow-ons: Byte/Fixed literal coercion, match-arm range narrowing, widening for recursive function summaries. Three independent extensions to the refinement-elision pass. (1) The type checker now coerces a bare integer literal to Byte (when in [0, 255]) or Fixed<N> in comparison and arithmetic against a counterpart of that type. The literal is wrapped in an explicit Expr::Cast node so the operator's existing same-type dispatch sees matching types and downstream emit produces the correct conversion. Byte-typed refinement predicates (fn in_range(x: Byte) -> bool { x >= 0 and x <= 100 }) now compile, unlocking the Byte natural-range work for actual refinement-elision customers. (2) infer_arg_range_with gained a shadow map parameter and a new Expr::Match arm that walks each match arm, intersects the scrutinee range with the arm's pattern range, binds a variable pattern to the narrowed range in the shadow, and unions the arm body's range. The summary-pass equivalent in eval_expr_to_range gained parallel Expr::If and Expr::Match handling. (3) New Interval::widen and IntervalSet::widen operators (Cousot-Cousot style) widen growing bounds to infinity. The function-summary pass now seeds every function to IntervalSet::empty and uses widening after WIDEN_AFTER_ITERATIONS rounds to converge on recursive bodies. Recursive functions get a sound compile-time summary even though the WCMU verifier rejects them at load time in V0.2; the widening infrastructure is in place for future passes that admit a relaxed WCMU bound or trust-skip recursion. Five new VM tests cover Byte refinement-predicate compilation, Byte literal-coercion elision, match-arm literal-pattern narrowing, match-arm variable-pattern narrowing, and an If-expression summary. 5 new lattice unit tests for widening. 717 lib tests pass. STM32N6570-DK FLASH bumped to 768 KB / RAM 256 KB / HEAP 192 KB to fit the expanded full-pipeline image.
• B13 lattice follow-ons closed: Byte natural-range parameter tracking and cross-function return-range summaries. Byte-typed function parameters populate local_ranges with [0, 255]; the cast b as Word carries the range through to a newtype constructor. A new fixed-point pass computes per-function return-range summaries (TypeInfo::function_return_ranges) over the function table at the top of compile; the constructor-emit site's infer_arg_range consults the summary at Expr::Call sites. Customers include Counter(some_function()) patterns where some_function's body is decidable under the lattice. Recursive functions and bodies with unhandled expression shapes (if, match, etc.) remain unsummarized and fall through to the runtime check. Three new VM tests cover function-call summary admission, function-call summary rejection on disjoint, and chained constructor-through-function admission. Byte and Fixed<N> refinement-predicate surface remains blocked by a separate type-checker gap (integer literals default to Word); the lattice infrastructure is ready when the surface supports it.
• B13 Tier 3: interval lattice and parameter-range refinement elision. New keleusma::interval module carries a closed-signed-interval lattice on i64 with Option<i64> bounds for the infinity directions. Constructors: full, empty, singleton, at_least, at_most, range. Predicates: is_empty, contains, is_subset_of. Lattice operations: intersect, union. Transfer functions for neg, add, sub. The constructor emission path consults the lattice when constant-fold fails: predicate_true_set decomposes a refinement predicate body into the interval of values for which it returns true (handles true / false literals, comparison against the parameter on either side, and as intersection, and not over a single comparison as operator inversion); infer_arg_range walks the argument expression and returns its inferred interval (literals, identifiers via local_const_values and local_ranges, unary negation, addition, subtraction, newtype-to-underlying casts); when the inferred range is a subset of the true set, the runtime check is elided; when the ranges are disjoint, the compile fails. Function parameters declared as refined newtypes populate local_ranges with the predicate's true set, providing the principal source of non-singleton ranges. The lattice is reserved for future use by B12 (helper-function WCMU precision) and B14 (CallIndirect flow analysis). 19 lattice unit tests plus 3 integration tests cover parameter-range elision, disjoint-range rejection, and graceful fall-through on undecidable predicates. 676 lib tests pass.
• B13 Tiers 1 and 2: refinement elision extended to constant-folded arguments and let-bound integers. The evaluator at the constructor emit site now folds the argument through a small closure-driven eval_expr_with that handles integer arithmetic, comparison, logical operators, unary negation, and identifier lookup. Tier 1 (fold_to_int(arg, &|_| None)) handles arithmetic over literals; Counter(2 + 40), Counter(0 - 1), and similar chains all fold and route through the predicate evaluator. Tier 2 adds a local_const_values: BTreeMap<u16, i64> table on FuncCompiler that records each let-binding whose value expression constant-folds to an integer; the lookup closure at the constructor site resolves identifier references through this map. Chained constants (let a = 2; let b = a * 21; Counter(b)) walk the chain via the recorded values. Non-constant lets (let n = neg_one(); Counter(n)) do not register and fall through to the runtime check. Six new VM tests cover the folded-arithmetic admission, the chain-of-lets admission, the compile-time rejection on a folded provable-failure, the compile-time rejection on a let-bound provable-failure, and the runtime-trap fall-through for non-foldable identifiers. 654 lib tests pass.
• B13 MVP closed: literal-argument refinement elision. When a refined newtype constructor Name(literal) is called with a direct integer literal that the compile-time evaluator can prove satisfies the predicate, the runtime call and trap are skipped and the constructor reduces to the inner value. When the literal provably fails the predicate, the compile rejects the construction at the source span with a diagnostic naming the predicate, the newtype, and the argument. Implementation: TypeInfo::refinement_bodies caches each predicate's (parameter_name, body_expr) for the eligible subset (single bare-variable parameter, no statements, tail-expression body). A small structural evaluator (eval_predicate_at_int) handles literals, identifier substitution, integer arithmetic, comparison, logical operators, and unary negation. Anything outside this subset returns None and the runtime path is preserved. The compile-time path is engaged only for direct-literal arguments; let-bound constants, arithmetic on literals, and values returned from atomic-total functions all retain the runtime check (follow-on work documented in BACKLOG B13). Three new VM tests cover the elision, the compile-time rejection, and continued runtime-trap fall-through for non-literal arguments. 645 lib tests pass.
• Op::CheckedDiv and Op::CheckedMod with (h, l, flag) shape. Closes the i64::MIN / -1 and i64::MIN % -1 corner cases noted in the V0.2 design pass. The checked construct's / and % paths now emit dedicated opcodes that compute the true result in i128 and route through the standard outcome-class arms. For CheckedDiv, the only overflow case is i64::MIN / -1 (true result 2^63, decomposed as high=0, low=i64::MIN with flag=1); all other divisions route through ok with high=0 and the quotient as low. For CheckedMod, the corner is i64::MIN % -1 (true result 0, but the underlying division step overflows); the construct flags it through the overflow arm with high=0, low=0. Division by zero continues to trap with VmError::DivisionByZero; the construct does not catch it because the opcode itself fails before arm dispatch runs. The two new variants are appended after Op::CheckedNeg so no existing rkyv discriminants shift; the wire format version stays at 1. Four new VM tests cover the corners. The compiler's checked-construct emission path drops the stamped-zero-flag fallback in favour of the new opcodes.
• B15 closed: Type::Unknown removed from the type system. The permissive wildcard sentinel that anchored runtime-only dispatch positions in the V0.1 inference pass is gone. The refactor proceeded in three phases. (1) The Type::Newtype variant changed from Newtype(String, Box<Type>) to Newtype(String); the authoritative underlying lives in Ctx::newtypes and the boxed placeholder was dead weight. This eliminated the largest Type::Unknown producer at the structural resolver. (2) The two remaining producers in the newtype-construction paths now route through ctx.fresh() when the newtype is not yet recorded. (3) The types_compatible wildcard short-circuit and the variant itself were dropped; every consumer arm collapsed into the surrounding Type::Var(_) arm, the cast wildcard became (Type::Var(_), _) | (_, Type::Var(_)) => ..., and standalone Type::Unknown => ctx.fresh() arms were deleted as redundant. Every unannotated position now produces a fresh Type::Var and inference proceeds uniformly through unification. 642 lib tests pass; bare-metal STM32N6570-DK full-pipeline build verified.

Changed

• Type::Newtype variant shape. Changed from Newtype(String, Box<Type>) to Newtype(String). The variant carried a placeholder that was never authoritative; the real underlying is in Ctx::newtypes. Existing destructuring sites that ignored the underlying field through Type::Newtype(name, _) were updated mechanically to Type::Newtype(name).

Added (continued)

• B18 closed: big-number arithmetic worked example, integration test, and guide. New standalone script at examples/scripts/09_big_numbers.kel demonstrating two adoption patterns for the V0.2 pattern-arm checked construct. mul_full(a, b) reads the high half of Op::CheckedMul's i128 intermediate directly; worked input 2^32 * 2^32 = 2^64 yields (high=1, low=0). add_with_carry(a, b) returns a carry-out flag derived from the overflow class; worked input i64::MAX + 1 yields carry=1 with low=i64::MIN. New integration test tests/big_number_arithmetic.rs (big_number_example_returns_1) compiles and runs the script end to end. New guide doc docs/guide/BIG_NUMBERS.md walks through the patterns with a chained two-digit-addition example, discusses the signed/unsigned i64 caveats, and cross-references the grammar and language-design sections.
• Pattern-matched checked-arithmetic arms with high/low bindings and match-arm guards (breaking syntax change). The numeric-overflow construct's arms are now pattern matches. Each arm carries one outcome class (ok, overflow, underflow) with patterns in every value position and an optional when expr guard. Pattern positions admit _ (wildcard), a bare identifier (binds a Word), or a signed integer literal (matches by equality). The ok arm binds one pattern against the in-range result; overflow and underflow bind two patterns against the high and low halves of an i128 intermediate result. The runtime computes (high, low, flag) for Op::CheckedAdd, Op::CheckedSub, Op::CheckedMul, and Op::CheckedNeg; the high half is the load-bearing value for big-number multiplication and the carry word for big-number addition. The construct exhaustiveness rule shifts from "exactly one of each outcome" to "each outcome's last covering arm is an unguarded catch-all (bare identifier or wildcard in every position)". The pipe-combined overflow|underflow => body form is removed; rewrite as two arms with the same body. Match expressions in general gain optional when expr guards through MatchArm::guard: Option<Expr>; the guard is checked in the pattern's binding scope, must evaluate to Bool, and falls through to the next arm when false. Exhaustiveness analysis treats guarded arms as non-catch-all regardless of pattern shape. Bytecode-level stack effect on the four checked opcodes is (pop 2, push 3) for the binary forms and (pop 1, push 3) for unary negation; division and modulo continue to use the stamped-zero-flag pattern (high = 0, flag = 0) so the existing Op::Div/Op::Mod cover the construct's needs. Compiler dispatch is a virtual loop over arms with literal-pattern equality tests, optional guard evaluation, and variable-pattern binding, mirroring the lowering of match arms. Migration: every existing checked-construct site rewrites overflow => body to overflow(_, _) => body and underflow => body to underflow(_, _) => body; the microkernel heartbeat script and the bundled VM/typecheck tests are updated in place. Six new VM tests cover the high-half exposure for multiplication, the literal-high pattern specialization, and the guard fall-through; three new VM tests cover match-arm guard dispatch, fall-through, and exhaustiveness rejection of a guarded catch-all. 642 lib tests pass.
• Refined-newtype saturation contracts (closes Item 2 of the V0.2 gap list). Newtype declarations now accept an optional with saturate_max = N and with saturate_min = M clause: newtype Limited = Word where nonneg with saturate_max = 100, saturate_min = 0;. The saturate_max and saturate_min keywords inside a numeric overflow construct are now context-determined. When the surrounding expected type (top of a new expected-type stack maintained by the type checker, pushed by annotated let bindings and by function return types) is a refined newtype declared with the matching clause, the keyword is mutated in place to a constructor call against the declared literal. The refinement predicate is verified at runtime on that literal exactly as for any other constructor invocation. When the surrounding expected type is Word (the default), the keywords retain the legacy Word::MAX and Word::MIN semantics. Implementation: NewtypeDef.saturate_max and NewtypeDef.saturate_min carry the declared values through the AST; parser recognises the with clause and admits leading-minus integer literals; type checker populates Ctx::newtype_saturate_max and Ctx::newtype_saturate_min during pass 1a' and consults them at the saturate keyword site after stripping any information-flow labels from the expected type; type_of_expr, type_of_block, check_stmt, and check_function signatures now thread &mut to permit the AST mutation. Three new VM tests cover function-return context, annotated-let context, and the fall-back-to-Word::MAX/MIN path. docs/spec/GRAMMAR.md Section 7.5 EBNF and docs/architecture/LANGUAGE_DESIGN.md Section "Surface Extensions Added in V0.2" both updated. 637 lib tests pass.
• Third gap-closing pass: GRAMMAR.md and MANUAL.md sync, Type::Unknown role clarification. docs/spec/GRAMMAR.md gains a new Section 7.5 "V0.2 Surface Extensions" with formal EBNF for newtype declarations, the numeric overflow construct, and information-flow labels, plus worked examples. The keyword table is updated (newtype, where, overflow, underflow, saturate_max, saturate_min added; the lexer-vs-parser distinction for classify/declassify is documented). The operator table gains @ (label separator) and | (arm alternation). examples/rtos/MANUAL.md gains Sections 5.5 and 5.6: the heartbeat task's adoption of the numeric overflow construct is documented with the live snippet and runtime-cost analysis; the remaining V0.2 surface extensions are surveyed with adoption suggestions for newtypes (time-precision discipline), refinement types (input validation), and information-flow labels (telemetry separation). The Type::Unknown doc comment is rewritten to describe its three current valid roles (newtype underlying placeholder, cast dispatch fallback, types_compatible wildcard) rather than marking it as legacy; removal would touch 26 call sites with risk of inference regressions and is deferred to a dedicated session. Item 4 (refinement-type compile-time elision through range analysis) remains on the backlog. 670 lib tests pass workspace-wide.
• Second gap-closing pass: tuple label propagation, newtype extraction, doc sync, microkernel adoption. Per-position information-flow label checking via new recursive flow_admissible helper that descends through Tuple, Array, and Option. Structural unifier now strips outer labels at every recursive entry so nested Labelled types unify cleanly. Three new tests confirm tuples preserve per-element labels, destructuring preserves the labels, and reading a labeled field into an unlabeled slot is rejected. Newtype value extraction via T as Underlying cast is now supported: the type checker consults ctx.newtypes to find the authoritative underlying and admits the cast in both directions; the compiler emits no opcode for newtype-related casts because newtypes are transparent at the bytecode level. docs/architecture/LANGUAGE_DESIGN.md gains a new "Surface Extensions Added in V0.2" section covering newtypes, refinement types, the overflow construct, and information-flow labels. The microkernel's heartbeat task adopts the overflow construct on its counter increment, demonstrating the saturate-on-overflow pattern in a live demonstrator; the std and N6 platform implementations of log_event now surface the counter value. 670 lib tests pass workspace-wide (was 666, +4 new tests). Bare-metal STM32N6570-DK trust-load .text is 146 KB.
• QIF gap-closing: arithmetic label propagation, branching taint, additional checked ops, newtype cycle detection. Closes the gaps identified after the design-decision pass. Arithmetic on labeled values (BinOp::Add, BinOp::Sub, BinOp::Mul, BinOp::Div, BinOp::Mod, UnaryOp::Neg) now unions the operands' labels and applies the union to the result; the previous implementation silently stripped labels at every arithmetic site and constituted a soundness gap. Branching propagation: if cond@L { ... } and match scrutinee@L { ... } now propagate the condition's labels to the result through apply_labels, because an observer of the branch result can infer information about the condition. The branch arms unify structurally and union their own labels in addition. New apply_labels, strip_labels, and labels_of helpers on the type checker. New checked-arithmetic opcodes Op::CheckedMul and Op::CheckedNeg extend the overflow construct's supported set to +, -, *, /, %, and unary - on Word; division and modulo route through the existing Op::Div/Op::Mod plus a stamped Value::Int(0) flag because the only arithmetic-overflow case on Word division is the i64::MIN / -1 corner which the regular wrap handles. Newtype dependency cycles (newtype A = B; newtype B = A;) are now detected at pass 1a'' and rejected with a diagnostic naming the participating type. Native function signatures with labels (use host::transmit(Word@Open) -> bool) admit labeled-source rejection at call sites; the existing native-signature machinery handles this without further extension. 666 lib tests pass (was 651, +15 new). Cross-feature clippy clean.
• Module::flags (u8) and the FLAG_EPHEMERAL constant. New header bit set when the verifier proves the module is ephemeral. Reserved bit positions are zero and the runtime ignores any unrecognised bits. Mirrored in the framing header at offset 13.
• Module::shared_data_bytes (u32) and Module::private_data_bytes (u32). Verifier-populated byte counts for the shared and private partitions of the data segment. Mirrored in the framing header at offsets 24 and 28. Shared data lives in the Vm's slot storage and is host-visible through Vm::set_data and Vm::get_data as today. Private data lives in the arena's persistent (.data) region added in keleusma-arena 0.3.0 and is not exposed through the host API.
• shared and private modifiers on data declarations. New keywords. shared data ctx { ... } is equivalent to today's bare data ctx { ... } and is host-visible; the explicit form documents the intent. private data state { ... } declares a data block that lives in the arena's persistent region and is not exposed through Vm::set_data or Vm::get_data. The compiler and runtime wiring that gives the partition runtime effect lands in phase 4; for now the AST and the parser accept the modifier and the type checker enforces the shape.
• ephemeral modifier on entry-point function declarations. ephemeral fn main, ephemeral yield main, and ephemeral loop main assert the producer's intent that the module is provably ephemeral, meaning at every yield or return that crosses the host-VM boundary no arena-resident value is observed, and at every resume or entry no value loaded from arena memory allocated prior to that resume or entry is read. The type checker rejects the modifier on any function whose name is not main. Modules without the modifier still receive the bit when the verifier infers the property.
• SlotVisibility enum (Shared, Private) on bytecode::DataSlot. Mirrors the source DataVisibility at the bytecode layer so the runtime can enforce the host-API boundary without reading the source AST. Serialized as part of the data layout in the bytecode body.
• Compiler partitions the data segment by visibility. Shared slots occupy the low index range, private slots the high range; slot indices in data_fields reference the unified space. Module::shared_data_bytes and Module::private_data_bytes are populated from the partition (one VALUE_SLOT_SIZE_BYTES-sized slot per slot).
• R28 relaxed to "at most one data block per visibility class". A program may declare one shared block and one private block. Two blocks of the same visibility remain rejected.
• Vm::set_data and Vm::get_data reject private slots. Returns VmError::NativeError with a message indicating that the slot is private and not accessible through the host API. The opcode-level Op::GetData and Op::SetData continue to admit both kinds, so the script can read and write its own private slots.
• Verifier sets FLAG_EPHEMERAL (under verify feature). Sufficient rule: private_data_bytes == 0 AND the entry function's signature carries no Text (which compiles to arena-resident Value::KStr). The compile pipeline rejects programs that declare ephemeral on main but whose proof fails, with a diagnostic naming the reason. Modules without the modifier still receive the bit when the inference holds.
• Private data lives in the arena's persistent region. The Vm separates the data segment into shared slots (Vm-owned Vec<Value>) and private slots (raw Value storage in the arena's persistent region). Op::GetData, Op::SetData, Op::GetDataIndexed, and Op::SetDataIndexed dispatch by slot index relative to the shared count. The Vm carries shared_slot_count: u16 and private_slot_count: u16 cached at construction. Private slots are initialised to Value::Unit at Vm::new and again at Vm::replace_module (hot swap). A new Drop impl on Vm runs the destructors on every private slot when the VM is dropped so owned resources do not leak.
• vm::required_persistent_capacity_for(&module) -> usize. New public helper that returns the actual byte count needed in arena.persistent_capacity() to back the module's private data. Differs from module.private_data_bytes because the latter is in VALUE_SLOT_SIZE_BYTES-sized logical units for WCMU accounting while the former is in actual Value storage units. Hosts call arena.resize_persistent(required_persistent_capacity_for(&module)) before constructing the VM.
• Vm::new rejects when the arena's persistent capacity is too small. Returns VmError::VerifyError with a message naming the required capacity and the call hosts should make. Modules without private data continue to work with the default zero persistent capacity unchanged.
• Vm::replace_module (hot swap) honours the partition. The host supplies initial_data of the full slot count; the implementation splits the prefix into shared and the suffix into private. The arena's persistent capacity must be at least the new module's storage requirement; if not, replace fails. Old private slots are dropped before the new ones are written.
• const data declaration form. New keyword. Surface syntax const data palette { red: Byte = 255, green: Byte = 128 }. Fields carry compile-time literal initializers; field reads compile to Op::Const loads from the per-chunk constant pool; field writes are compile errors. Const data does not allocate runtime data-segment slots and does not appear in shared_data_bytes or private_data_bytes. The compile pipeline rejects shared and private data fields that carry initializers (only const data admits them) and rejects const data fields that are missing initializers. The R28 constraint extends to "at most one data block per visibility class", so a program may declare one shared, one private, and one const block simultaneously. Initializers are restricted to scalar primitive literals (Word, Byte, Float, Bool, Text, unit) plus a leading minus on numeric literals; tuple, array, struct, and enum initializers are queued for a later iteration.
• Compiler rejects private data blocks where no slot is ever mutated. Diagnostic recommends rewriting as const data. An unmutated private slot is wasted memory; the programmer almost certainly meant the constant form. Const data is exempt from the check because its values are compile-time and never written; shared data is exempt because the host can mutate slots through Vm::set_data without leaving a SetData in the bytecode.
• docs/spec/INSTRUCTION_SET.md resynchronised with the live Op enum. Closures (CallIndirect, PushFunc, MakeClosure, MakeRecursiveClosure), indexed data access (GetDataIndexed, SetDataIndexed, BoundsCheck), and the numeric-conversion family (WordToByte, ByteToWord, WordToFixed, FixedToWord, FixedMul, FixedDiv) are now documented with operands, costs, and behaviour. The cost summary table extends accordingly. The Data Segment section documents the shared/private/const partition.
• Stronger ephemeral inference: parameter-usage refinement. Phase 7 tightens the verifier rule so that a Text-typed parameter that the entry function's body never references no longer disqualifies the module from ephemerality. The refinement walks the entry function's body AST and checks whether each Text-typed parameter's binding name appears in any expression, statement, match arm, for-loop iterable, or block-tail. Unused Text parameters are dropped from the signature-uses-text test; return-type analysis continues to be conservative because proving "no Text actually returns" requires dataflow on every return path. The CHANGELOG records this as the practical implementation of the spec rule; further tightening (per-yield arena dataflow over the operand stack) is queued for a future iteration when a real script benefits from it.
• Const data: tuple and array composite initializers. const data fields whose declared type is a tuple (T1, T2, ...) or an array [T; N] may now carry composite initializers in the form (init, init, ...) or [init, init, ...]. Element counts and types are validated against the declared field type at compile time. Indexed read access (lut.table[i]) on a const array field compiles to a constant load followed by Op::GetIndex; writes remain compile errors. Struct and enum initializers stay reserved for a later iteration.
• Const data: struct and enum composite initializers. const data fields whose declared type is a struct or an enum may now carry struct-literal (Name { field: init, ... }) and enum-variant (Enum::Variant or Enum::Variant(arg, ...)) initializers. The parser recognises both shapes inside const initializer position; the compiler validates the type name against the declared field type and rejects mismatches with a diagnostic. Nested composite initializers are admitted through a permissive inner recursion that falls back to type-agnostic literal-to-ConstValue conversion when the precise inner type cannot be determined from the surface context. This completes the const-data initializer matrix for V0.2 (scalar, tuple, array, struct, enum).
• RTOS microkernel: production patterns demonstrated. Four new patterns landed on the microkernel to lift it from "language headline" to "adaptable cooperative-scheduling RTOS demonstrator". Per-task WCET budget on Task::wcet_budget_cycles rejects load and hot-swap attempts whose declared module.wcet_cycles exceeds the budget. Per-task supervised-restart policy on Task::max_restarts: on VmError::Halt the kernel resets the VM's transient state through Vm::reset_after_error, increments the restart counter, and re-dispatches the task until the budget is exhausted. Platform trait gains feed_watchdog() (default no-op) called once per scheduler iteration. Kernel gains post_event(event_id) and an internal enable_event_tick(event_id, period_ms) ticker that simulates an ISR cadence for the demonstrator; tasks wait on events through the existing yield (2, event_id) form, which the scheduler maps to TaskState::WaitingFor. Two new demonstrator tasks: event_listener waits on event id 1 (kernel posts every 2500 ms) and logs each wake, faulty triggers DivisionByZero at every fifth iteration to exercise the supervised-restart path. Bare-metal .text grew by roughly 3 KB to 140 KB trust-load and 160 KB precompile-plus-verify; FLASH headroom for user code and NPU weights is now 480-500 KB out of 640.
• floats cargo feature, default on. Gates the surface support for floating-point arithmetic. With the feature off the lexer rejects float literals (3.14, 4.75f64) at lex time, the parser accepts Float as a type expression but emission of ConstValue::Float and Value::Float is compiled out, Op::IntToFloat and Op::FloatToInt arms surface as VmError::InvalidBytecode (the variants stay defined to preserve wire-format stability), the f64 arm in Vm::binary_arith and the comparison op are gated out, KeleusmaType for f64 is omitted, and the audio_natives and stddsl modules are not compiled. The soft-float compiler_builtins routines (__divdf3, __adddf3, __muldf3) drop entirely once nothing in the runtime references them. On the bare-metal STM32N6570-DK build this is roughly 12 KB; the microkernel disables the feature and now ships in 137 KB trust-load and 157 KB precompile-plus-verify. Default on for backwards compatibility with hosts that need float arithmetic.
• Native function signature declarations on use imports. The surface form use host::name(T1, T2, ...) -> R declares the parameter types and return type of a registered native at the type-checker level. Call sites validate parameter arity and per-parameter types against the declaration and inherit the declared return type. Native names imported through the bare use host::name form continue to take the legacy permissive path that admits any argument types and assigns a fresh return-type variable. New ast::NativeSignature struct, parser extension on parse_use_decl, new Ctx::native_signatures map populated during pass 1c0, and a new check_native_call_with_signature helper. The microkernel's scripts/prelude.kel now declares signatures for all 17 host natives. (B1 foundation; removing Type::Unknown entirely remains backlog work.)
• Strict schema check on hot swap. New Module::schema_hash: u32 field (CRC-32 of the canonical serialisation of (slot_name, visibility) per slot in declaration order). Vm::replace_module now rejects swaps where the new module's schema_hash differs from the loaded module's; the rejection carries the two hash values for diagnostic clarity. A companion Vm::replace_module_unchecked skips the schema check for hosts that intend to swap across incompatible data layouts (e.g. song-A to song-B in an audio demonstrator). Hot-swap test renumbering: the prior hot_swap_new_schema_replaced test is now hot_swap_strict_rejects_schema_mismatch, a new hot_swap_unchecked_admits_new_schema covers the escape hatch, and a new hot_swap_strict_admits_schema_compatible covers the same-schema admit path. Bytecode body grew by 4 bytes; golden test regenerated, examples/zero_copy_demo.kel.bin regenerated.
• VmError::category method. New VmErrorCategory enum with Halt, SoftScript, SoftHost variants. Method returns the coarse retry-or-halt policy without storing per-error bytes. Hosts that need finer policy continue to match on the variant directly. The microkernel kernel-error path uses the category to map errors to a single event-code lookup rather than format!("{:?}", e), eliminating ~15 KB of float-formatter code from the bare-metal image.
• Bare Option::None type-checker tightening. The EnumVariant site for Option::None previously returned Option<Unknown>, which could not unify against a concrete Option<T> because the unifier does not narrow Unknown through Option's recursive arm. The fix splits the Some/None cases: Some(t) uses the payload's inferred type as the inner; None uses a fresh type variable that the surrounding context (function return type, let-binding annotation, match-arm sibling, function-call argument position) unifies. Programs of the form fn f() -> Option<T> { Option::None } are now admitted. The previously-blocked positive test for the per-yield arena dataflow refinement (ephemeral_bit_set_when_declared_text_return_never_produced) is re-enabled.
• Microkernel flash savings: ~43 KB on STM32N6570-DK. Three coordinated changes shrank the precompiled-bytecode bare-metal .text from 192 KB (V0.2 baseline) to 149 KB trust-load and from 211 KB to 169 KB precompile-plus-verify. Largest contributor (~32 KB): kernel-side format!("{:?}", vmerror) calls were replaced with Platform::log_event(category_code, data), removing the chain of Debug derives on VmError, Value, and ConstValue that pulled in core::fmt::float (flt2dec::dragon, flt2dec::grisu, CACHED_POW10), compiler_builtins::__divdf3/__adddf3, and char::escape_debug_ext. Release profile gained panic = "abort" to drop unwinding tables (~1-2 KB). Three new kernel event codes (EV_KERNEL_VM_ERROR, EV_KERNEL_UNKNOWN_YIELD, EV_KERNEL_TASK_FINISHED, EV_KERNEL_UNEXPECTED_STATE) with per-platform format-string arms preserve diagnostic visibility through the new logging surface. The full-pipeline mode is essentially unchanged (621 KB, was 614 KB) because the source compiler dominates that image; the savings concentrate in the embedded production modes.
• Target-scaled Fixed defaults for sub-64-bit targets. The surface form Fixed (no explicit <N> argument) now resolves through the target descriptor's new Target::fixed_default_frac_bits() helper rather than the host-hard-coded DEFAULT_FIXED_FRAC_BITS = 32. Cross-compilation to a 32-bit target picks up Q15.16 (frac=16), to a 16-bit target Q7.8 (frac=8), and to an 8-bit target Q3.4 (frac=4); the fraction-bit count is the lower half of the target word width. Threaded into both the type checker (new check_with_target entry point, called by compile_with_target) and the compiler (new normalize_fixed_defaults AST normalization pass that rewrites every PrimType::Fixed(None) to PrimType::Fixed(Some(target_frac_bits)) before downstream consumers read the immediate at Op::WordToFixed, Op::FixedToWord, Op::FixedMul, and Op::FixedDiv emission sites). The bare check entry point keeps the host-default behaviour for backwards compatibility. Two new tests cover the lattice (fixed_default_frac_bits_scales_with_target_word_width) and the end-to-end opcode emission (fixed_default_changes_when_targeting_embedded_16).
• RTOS microkernel: text feature disabled and logging via registered native. The microkernel runtime keleusma dependency drops the text cargo feature. Task scripts no longer use string literals or f-string interpolation. Diagnostic logging routes through a new host::log_event(code: Word, data: Word) native that forwards to a new Platform::log_event(code: u32, data: i64) method; the per-event format string lives on the host side in each platform implementation (std println!, N6 defmt::info!). The script and host agree on the numeric event discriminants by convention through the EV_HEARTBEAT_OK, EV_LED_GPIO_FAIL, and EV_SENSOR_ABOVE constants in src/natives.rs. register_utility_natives is no longer called because f-strings are not used. Two embassy-stm32 features (exti, unstable-pac) are also dropped because the kernel does not exercise them. Resulting bare-metal .text on the STM32N6570-DK: 180 KB trust-load (was 192 KB, -12 KB), 199 KB precompile-plus-verify (was 211 KB, -12 KB). The full-pipeline build at 622 KB is roughly unchanged because the parser and type checker dominate that image.
• Stronger ephemeral inference: per-yield arena dataflow refinement. Phase 8 extends the verifier rule that determines whether a module is admissible as ephemeral. The text-size abstract interpretation pass already tracks per-stack-slot TextSize lattice values through the compiled bytecode in topological call order for WCMU heap-allocation bounding. The pass now also reports per-chunk yields_text and returns_text flags, computed by peeking the abstract operand stack at every Op::Yield and Op::Return and at the implicit end-of-chunk return. The compiler's ephemerality check consults the entry chunk's analysis result: if the entry's declared return or yield type carries Text but every concrete boundary-crossing path peeks a non-text value, the module is admitted as ephemeral. The previous signature-only rule disqualified such modules; the new rule is a strict tightening that admits more programs while preserving the soundness invariant. A new public helper verify::module_chunk_text_analyses(&Module) -> Result<Vec<ChunkTextAnalysis>, VerifyError> exposes the per-chunk analysis result for hosts that want to inspect the dataflow result independently.
• docs/spec/GRAMMAR.md synced. Reserved keyword set extended with shared, private, const, ephemeral. The data_decl and function_def EBNF productions extended with visibility modifiers and the ephemeral modifier respectively; const_initializer production added.
• docs/architecture/LANGUAGE_DESIGN.md synced. Memory Model section gained Data Segment Partition and Ephemeral Modules subsections documenting the three visibility classes, the storage and lifecycle of each, and the verifier rule with rationale.
• examples/rtos/MANUAL.md synced. New section 5 "Data partitioning: shared, private, and const" walks through the three classes with code snippets from the heartbeat task. The heartbeat script itself was updated to demonstrate const data cfg { period_ms: Word = 5000 } in place of the previous inline literal.
• #![deny(missing_docs)] on every published crate. keleusma, keleusma-arena, keleusma-bench, keleusma-cli, and keleusma-macros each carry the deny attribute at their crate root. Approximately 357 previously-undocumented public items in keleusma and keleusma-bench gained doc comments covering every public module, type, field, variant, function, and trait method. Two enums (ast::Expr and ast::BinOp) and the rkyv-generated archived siblings in bytecode.rs carry per-item #[allow(missing_docs)] with explicit justification because the variants mirror the grammar's productions one-to-one or because the items are macro-generated. Pre-existing broken intra-doc links in eight modules' header doc-comments (referencing MutVisitor, Visitor, Library, Math, Audio, Shell, Interval, IntervalSet, FunctionDef, unify, Subst, Type::Var, chunk_text_heap_alloc, WideWord) were fixed by rewriting them as either fully-qualified intra-doc paths or plain backtick code. keleusma's crate-root doc comment was previously empty; it now carries a multi-section preface (what Keleusma is, a verified quickstart, the Cargo feature overview) so docs.rs/keleusma's landing page reflects the crate's purpose. CI's Doc job and the per-crate cargo-doc invocation enforce the lint under RUSTDOCFLAGS="-D warnings -A rustdoc::redundant-explicit-links".

Changed

• Wire format BYTECODE_VERSION rolled from 2 back to 1. Pre-release builds briefly used version 2 before this crate achieved public adoption. Bytecode produced under any version-2 build is rejected at load through the CRC trailer mismatch on the new 32-byte header, which is the desired behaviour given there are no known consumers of the version-2 format outside this repository.
• Framing header grew from 24 bytes to 32 bytes. The flags byte at offset 13 fills the previous one-byte reservation; the shared and private data byte counts occupy the new 8 bytes between offsets 24 and 32. The header length stays divisible by 8 so the rkyv body remains 8-byte-aligned when the buffer base is 8-byte-aligned. The golden-bytes test was updated; the precompiled examples/zero_copy_demo.kel.bin was regenerated.

Added (continued)

• compile and verify cargo features, default on. Two new orthogonal features gate the source-to-bytecode pipeline and the load-time verifier respectively. With compile off, the runtime image no longer contains the lexer, parser, type checker, monomorphizer, and compiler; hosts that ship precompiled bytecode pay only for the VM and bytecode-format machinery. With verify off, Vm::new skips the structural verifier and the resource-bounds check; the host attests that an equivalent verification ran at the artefact-ingestion step. Both features are in default, so existing consumers see no behaviour change. The compiler still invokes the verifier at the end of compile_with_target when both features are on and populates the WCET and WCMU header fields exactly as before; with verify off the compiler leaves those fields at 0 (auto). Measured impact on the RTOS-microkernel example bare-metal binary: 614 KB .text with both features on, 211 KB with verify only, 192 KB with neither. The combination compile without verify is allowed but rarely useful because the resulting bytecode then carries 0 in the header bounds. Vm::new_unchecked retains its existing semantics under either feature combination; Vm::auto_arena_capacity, Vm::verify_resources, and the free function auto_arena_capacity_for are gated behind verify because their bodies route through the verifier.

• Cooperative RTOS microkernel example. New standalone crate at examples/rtos/ (intentionally detached from the parent workspace because of heavy bare-metal git dependencies). The kernel core is no_std + alloc; every task is a Keleusma loop main script. Two demonstrators ship: three-task-std on the development host, and three-task-n6 on the STM32N6570-DK through embassy-stm32, embassy-executor, embassy-time, defmt-rtt, cortex-m-rt, and embedded-alloc::LlffHeap. Three tasks (LED blinker, sensor poller, heartbeat) dispatch cooperatively. The Platform trait abstracts time, sleep, log, and GPIO/sensor/UART/SPI/I2C/ADC access; resource counts live in an associated PlatformResources constant. DSL natives validate indices against PlatformResources and return a shared script-side Status enum (Ok = 0, Err(Word) = 1) whose payload is a StatusErrorCode discriminant. Verified end-to-end on the STM32N6570-DK on 2026-05-18 with the boot banner, scheduler entry at t≈215 ms, and four heartbeat ticks at five-second intervals across fifteen seconds of capture. Operator manual at examples/rtos/MANUAL.md; architectural rationale at examples/rtos/SPEC.md.

• Indexed access for data-segment array fields. Data-segment fields declared as [T; N] now occupy N consecutive slots and admit indexed read and write through state.field[i] and state.field[i] = value. Nested array types flatten to a single contiguous slab and the script descends with state.field[i][j]. Three new opcodes carry the access at the bytecode level: Op::GetDataIndexed(base, len) and Op::SetDataIndexed(base, len) perform the indexed slot read and write with a built-in bounds check against the field's total length, and Op::BoundsCheck(bound) is emitted by the compiler between levels of a multi-dimensional access so an out-of-range inner index traps rather than silently addressing a different sub-array. for x in state.field { ... } over a scalar-element data array lowers to a numeric loop issuing Op::GetDataIndexed per element rather than materialising the array as a Value::Array on the operand stack. Naked field access against an array field (a bare state.field reference outside an indexed or for-in context) is rejected with a diagnostic pointing at the indexed-access form. The data layout for non-array fields is unchanged; scalar and other composite fields continue to occupy a single slot whose Value representation carries the structure internally.

• OpCost::{Fixed(u32), Dynamic(fn)} enum. Cost-model surface for opcodes whose cost depends on runtime data. CostModel::heap_alloc_cost returns the new type; Op::Add on text operands reports OpCost::Dynamic because the resulting KString length is the sum of operand lengths. Hosts that need the pre-V0.2.0 fixed view continue to call CostModel::heap_alloc_bytes, which saturates dynamic costs to zero. The WCMU text-size tracking pass scheduled for V0.2.x evaluates OpCost::Dynamic against an OpCostContext populated from the abstract-interpretation lattice.

• text cargo feature, default off. Gates the surface use of strings in scripts. With the feature off, the lexer rejects string literals ("...") and f-strings (f"..."), and the parser does not recognise the Text primitive type. The keleusma-cli crate enables the feature on the runtime dependency so the script runner and the REPL continue to handle strings. Hosts that want the V0.1.x default surface enable the feature explicitly: keleusma = { version = "0.2", features = ["text"] }. Embedding hosts that target very small runtimes get a smaller compiled artifact by leaving the feature off. See the FAQ entry "Enabling text support" for details.

• Vm::new_with_options and overflow policy knob. New constructor accepting a VmOptions value with an overflow_policy field. The policy decides what happens when a module's declared WCET or WCMU header field saturated to u32::MAX during compilation. OverflowPolicy::Reject (default) treats overflow as a VmError::VerifyError, preserving the historic strict admissibility. OverflowPolicy::Warn admits the module and returns a Vec<VerifyWarning> describing the overflow. OverflowPolicy::Allow admits the module silently. The bare Vm::new is now a thin wrapper around new_with_options(VmOptions::default()) and continues to reject overflow.

• WCMU text-size tracking via abstract interpretation. New keleusma::text_size module introduces the TextSize::{NotText, Known(u32), Unbounded} lattice with saturating addition, join, and projection into the OpCostContext consumed by OpCost::Dynamic cost evaluators. The chunk_text_heap_alloc function walks each chunk's bytecode linearly, mirroring the operand stack and local variables as TextSize lattice values, and accumulates the dynamic heap cost of every text-producing Op::Add. verify::compute_chunk_wcmu calls this pass and adds its result to the chunk's heap WCMU bound. Programs whose text allocations saturate the bound to u32::MAX are rejected at Vm::new under the default OverflowPolicy::Reject. The FAQ exponential-string-concat example is correctly rejected when written as a Stream block; the analysis is conservative for text operations inside loops, behind conditional branches, and against native-produced text.

• Parser recursion-depth limit prevents stack overflow (reviewer report). A deeply nested parenthesised expression (a few thousand parens in release mode, around thirty in a debug build with a 2 MiB stack) used to panic the parser. The parser now bails with a typed ParseError at MAX_PARSE_DEPTH = 32. The limit applies at the three recursive entry points (parse_expr, parse_type_expr, parse_pattern) and is chosen to fit comfortably inside the default cargo-test thread stack with headroom for the type checker, compiler, and VM passes that follow.

• Vm::call validates argument count and types (reviewer report). Passing too few or too many arguments, or arguments of the wrong type, used to default missing slots to Value::Unit and then surface a confusing TypeError at the first use site (cannot add Int and Unit). The runtime now validates args.len() == param_count and each argument's runtime type against the parameter's declared TypeTag before any bytecode runs, producing a clear VmError::TypeError like function 'main' expected 2 arguments, got 1 or parameter 0 expected Word, got Float. The chunk format gains a param_types: Vec<TypeTag> field that the compiler populates from the function's declared parameter types; primitives map to their concrete tag, composites collapse to TypeTag::Composite which the runtime accepts without further checking.

• Vm::resume validates the resume value's type (reviewer report). For Stream blocks, resuming with a Float against a loop main(x: Word) signature used to flow the wrong type into the parameter slot and produce a confusing error at the first use site. The runtime now validates the resume value against the loop's parameter type (the same type the yield expression evaluates to) and rejects the wrong type with loop 'main' resume expected Word, got Float.

• Integer literal overflow is now LexError (reviewer report). Integer literals that do not fit in i64 (such as 99999999999999999999999999999) previously parsed to Value::Int(0) and silently disappeared. The lexer now reports integer literal does not fit in i64 with the literal's span at lex time. Decimal, hexadecimal, and binary literal paths all share the typed-overflow rejection; float literals are likewise wrapped in a typed LexError.

• Untyped parameters are inferred from context. Writing fn main(x) -> Word { x } previously parsed but the inferred parameter type did not flow through to the chunk, so Vm::call(&[Value::Float(1.5)]) was silently accepted. The type checker now writes inferred primitive types back into the AST after each function body is checked. The compiler's type_tag_for_param reads from the filled-in param.type_expr, so the chunk's param_types carries the inferred tag and the runtime call validator rejects wrong-typed arguments at the boundary. Parameters whose type cannot be inferred fall back to TypeTag::Composite.

• Duplicate function heads are rejected for every category, entry point or not. Two function definitions that share the same name and whose parameter signatures cannot be disambiguated as multi-headed pattern matching previously kept the first head and silently discarded the rest. A multi-headed function whose second head has the same literal pattern as an earlier head was likewise accepted with the second head as dead code. The compiler now applies a pattern_shape_eq check across heads (ignoring guards) and reports function head is dead code at the offending later definition. The rule applies to fn, yield, and loop categories alike, and to helpers as well as the entry point.

• Multi-headed entry points are accepted for fn, yield, and loop. The compile pipeline previously rejected multi-headed loop main(...) Stream blocks with "multiheaded stream (loop) functions are not supported". Multi-headed Stream dispatch is now wrapped in Op::Loop/Op::EndLoop so each matched head can Op::Pop its tail value and Op::Break out to the shared Op::Reset epilogue. The Stream block continues to contain exactly one Op::Stream and exactly one Op::Reset, preserving the structural verifier's invariants. The productivity rule continues to require that every reachable iteration path passes through a Yield.

• Modules without an entry point are now rejected at Vm::new (reviewer report). A module compiled from source that omits fn main, yield main, or loop main previously surfaced as VmError::InvalidBytecode("no entry point") at the first Vm::call. The constructor Vm::new and Vm::new_unchecked now reject the module with VmError::VerifyError("module has no entry point") at the API boundary. The Vm::call check is retained as defense-in-depth for the zero-copy entry path that skips the structural check.

• VmError::NotSuspended for premature Vm::resume (reviewer report). Calling vm.resume(value) before vm.call(args) previously surfaced as VmError::InvalidBytecode("cannot resume: VM not suspended"), which conflated API misuse with corrupt bytecode. The runtime now returns the dedicated VmError::NotSuspended variant.

• Source spans threaded through compile-time structural-verification errors (reviewer report). The compile-pipeline rejections for CallIndirect, MakeRecursiveClosure, and any structural-verifier failure used to attach Span::default(), which hid the offending source position. The compiler now builds a name-to-span lookup from the original (and hoisted) function definitions and attaches the originating span to each CompileError, so callers and IDEs can underline the offending construct.

• Bytecode wire format bumped to version 2. The param_types field is the only addition; the V0.1 wire format (version 1) is rejected at load time. Recompile any V0.1 bytecode artefacts to upgrade.

• Option::Some(x) => and Option::None => pattern matching. The compiler's pattern-test path now special-cases Option::None to use a direct equality check against Value::None rather than IsEnum (which fails because Value::None is not a Value::Enum). Option::Some(p) continues to use IsEnum because the compiler emits Op::NewEnum for Option::Some(x) constructions and the runtime convention is that Some(v) is Value::Enum { type_name: "Option", variant: "Some", fields: [v] }. Type checker's check_pattern_against_type and check_exhaustiveness paths now handle Type::Option(_) scrutinees. As a consequence, shell::getenv now correctly returns Option<Text> (matching the design choice from the prior round) — Value::None for unset variables and Value::Enum { type_name: "Option", variant: "Some", fields: [Value::StaticStr(value)] } for set variables.

• Standard DSL libraries: stddsl::{Math, Audio, Text, Shell}. New keleusma::stddsl module introduces the Library trait. Hosts register a bundle of native functions through Vm::register_library<L: Library>(lib: L). Four bundled libraries: stddsl::Math (libm-backed math), stddsl::Audio (DSP utilities), stddsl::Text (text utilities, gated on the text feature), stddsl::Shell (shell utilities, gated on the new shell cargo feature). Third-party crates implement Library on their own types to ship reusable bundles. The previous direct entry points (utility_natives::register_utility_natives, audio_natives::register_audio_natives) continue to work for backwards compatibility.

• shell cargo feature, default off. New cargo feature that compiles stddsl::Shell. Requires std::env and std::process::Command; therefore incompatible with no_std builds. The keleusma-cli crate enables the feature so the CLI runner has shell access. Shell functions: shell::getenv(name: Text) -> Option<Text> (returns Option::Some(value) when set, Option::None when unset; companion shell::has_env(name: Text) -> bool for presence checking when the caller does not want to unwrap an Option), shell::run(cmd: Text) -> (Word, Text) (executes through sh -c, returns exit code and stdout), shell::run_checked(cmd: Text) -> Text (returns stdout, traps on non-zero exit), shell::exit(code: Word) (terminates the host process).

• Fixed<N> parameterised form. The default Fixed surface keyword continues to mean the target-scaled Q-format (Q31.32 on the host). Fixed<N> explicitly pins the fraction-bit count to a literal integer N in [0, 62]. The parser accepts the new generic-numeric-argument syntax; PrimType::Fixed(Option<u8>) carries the count through the AST (None for the default form). The type checker resolves both forms to Type::Fixed(u8); the unifier requires equal fraction-bit counts. The compiler emits the new opcodes (Op::WordToFixed, Op::FixedToWord, Op::FixedMul, Op::FixedDiv) with the correct fraction-bit immediate. Three integration tests cover Fixed<16> Q15.16 cast and multiply, plus the default-form Q31.32 cast. Target-scaled defaults for sub-64-bit targets are still deferred to a follow-on that threads the target descriptor into the type checker.

• Canonical numeric types Phase 3: Fixed (Q-format). New Fixed primitive type, signed Q-format fixed-point. The default form uses target-scaled fraction bits: Q31.32 on a 64-bit host runtime (32 fraction bits), Q15.16 on a 32-bit target (16 fraction bits), Q7.8 on a 16-bit target. The fraction-bit count is the lower half of the word width. Surface keyword recognised by the parser. Arithmetic uses Q-format semantics: Add and Sub are integer add/sub on the fixed-point bits; Mul shifts the i128 product right by the fraction-bit count and saturates; Div left-shifts the i128 dividend by the fraction-bit count before dividing and saturates. New opcodes Op::WordToFixed(u8), Op::FixedToWord(u8), Op::FixedMul(u8), Op::FixedDiv(u8) carry the fraction-bit count as an immediate operand. Value::Fixed(i64) runtime variant. ConstValue::Fixed(i64) compile-time constant. The compiler emits the cast and Fixed-multiply/divide opcodes with a hard-coded 32-bit fraction count matching the host runtime; threading the target descriptor through the function compiler for sub-64-bit targets is a follow-on. Explicit Fixed<N> parameterisation is also follow-on work. Eight integration tests cover round-trip casts, addition, subtraction, Q-format multiply, Q-format divide, negation, and signed comparison.

• Canonical numeric types Phase 2: Byte (u8). New Byte primitive type, 8-bit unsigned, range [0, 255]. Surface keyword recognised by the parser. Arithmetic uses wrapping u8 semantics (Add, Sub, Mul, Neg wrap modulo 256; Div and Mod use unsigned semantics; comparisons use unsigned ordering). New Op::WordToByte (truncates Word to low eight bits) and Op::ByteToWord (zero-extends Byte to Word) cast opcodes. Value::Byte(u8) runtime variant. ConstValue::Byte(u8) compile-time constant. KeleusmaType for u8 marshalling on the Rust side. Seven integration tests cover cast truncation, wrapping arithmetic, and unsigned comparison.

• Canonical numeric types (Phase 1, hard break). The surface keywords i64 and f64 are removed in favour of Word and Float. Word is the target word size (signed, 64-bit on the host runtime); Float is the target floating-point width (IEEE 754 binary64 on the host). Existing scripts that use i64 or f64 as type names fail to parse. The numeric-literal suffix forms 42i64 and 3.14f64 remain accepted for legacy notation, but they are an inference hint and do not change the surface type names. Byte (8-bit unsigned) and Fixed (signed Q-format with target-scaled fraction bits and optional Fixed<N> parameterisation) are introduced in subsequent commits.

• Opaque type support. New keleusma::opaque module introduces the HostOpaque marker trait and the Value::Opaque(Arc<dyn HostOpaque>) runtime variant. Host applications register Rust types as opaque values from the script's perspective; the script declares the type by name in function signatures (the type checker resolves unknown named types as Type::Opaque). Native functions produce opaque values through the host_arc constructor; consumers extract a typed reference through dyn HostOpaque::downcast_ref. Opaque values are host-managed through Arc, have a lifetime independent of the arena, may flow through the dialogue type at a yield, and contribute zero to the script-side WCMU bound. Equality is by Arc pointer identity. A small sealed supertrait surfaces the concrete TypeId without requiring core::any::Any.