Production BamTS bytecode: a verified instruction set, strict codec, and definite-initialization verifier with an unforgeable Verified typestate.

Relation to the formal five-op core

The proven structural core in formal/lean/Bamti/Bytecode/Model.lean (Load, Add, Jump, Suspend, Halt) is preserved exactly as a subset of this ISA:

• Load -> [Instruction::LoadConst] (now names the loaded constant).
• Add -> [Instruction::Binary] with [BinaryOp::Add] (generalized to the full closed operator algebra).
• Jump -> [Instruction::Jump] (identical control transfer).
• Suspend -> [Instruction::Suspend] (refined with an out register for the resumed value and an in register for the yielded value).
• Halt -> [Instruction::Halt] (identical terminator).

Every additional opcode extends that core. The verifier here mirrors the structure proven in Bytecode/Verify.lean -- a real entry, valid CFG targets, nested (non-partially-overlapping) handlers, and a syntactic definite-initialization witness across CFG joins -- before the Verified typestate can be constructed. Number constants use Bamti.canonical_nan, and persisted constants carry no heap or runtime identity, matching no_serialized_runtime_identity.

Dynamic-computation ISA

Unlike a fixed-key/fixed-window shape, this ISA expresses the dynamic runtime kernel of the corpus without special-casing syntax:

• Property access is register-keyed. [Instruction::GetProperty], [Instruction::SetProperty], and [Instruction::DeleteProperty] take the key in a Register, so computed access (obj[e]), string/number keys, Symbol keys, and private names (via [Instruction::CreatePrivateName]) are one uniform operation. [Instruction::DefineAccessor] installs a getter or setter descriptor under a register key.
• Calls are variadic. [Instruction::Call] and [Instruction::Construct] receive one arguments-array Register, so spread (f(...xs)) and any arity -- far beyond 127 -- lower identically. The runtime validates that the register holds a dynamic array.
• Closures capture explicitly. [Instruction::CreateClosure] binds a function together with a captures-array Register. On entry, a callee's leading [Function::capture_count] registers are the captured cells, followed by its [Function::parameter_count] parameters; both count as definitely initialized on entry.
• Aggregate building blocks. [Instruction::ArrayPush], [Instruction::ArrayExtend] (iterable spread), [Instruction::ObjectSpread], and [Instruction::SetPrototype] build non-empty arrays, objects, and class prototype chains incrementally.
• Iteration protocol. [Instruction::GetIterator] (with a closed [IteratorKind]) and the two-write [Instruction::IteratorNext] model for/of, for/await/of, for/in, destructuring, and array/call spread against the ECMAScript iterator protocol.
• Environment access. [Instruction::LoadGlobal], [Instruction::StoreGlobal], [Instruction::TypeOfGlobal] (the last models typeof g without throwing on an undeclared global), [Instruction::LoadThis], [Instruction::LoadArguments], and [Instruction::LoadNewTarget] name the ambient bindings a function body observes.
• Modules. [Instruction::Import] is dynamic and names a dependency by string constant; static bindings and exports live in [Program] linkage metadata so they identify live cells rather than activation registers.
• Regular expressions. [Instruction::CreateRegExp] materializes a RegExp from string-constant pattern and flags.

Resume contract (async / generators)

[Instruction::Suspend] { dst, src, resume } is the single suspension primitive; [FunctionFlags::is_async] and [FunctionFlags::is_generator] select how a suspension is driven, but the wire form is identical:

1. The activation yields the value in src (a produced item for a generator; an awaited operand for an async function) to its driver.
2. When the driver resumes the activation, control continues at resume with the resumed value written to dst (the argument of .next(v) for a generator; the settled result of the awaited value for await).
3. resume is a normal CFG successor and the only successor of Suspend, so the definite-initialization witness treats every register live across a suspension as it would across any join: dst is initialized on the resume edge, and registers not provably initialized before the suspension are not assumed initialized after it.

A generator's completion is an ordinary [Instruction::Return]; an uncaught throw during drive routes to an enclosing [ExceptionHandler] exactly as in synchronous code.

The wire format is a deliberate superset departure from the formal single seven-bit-group encoding: integer fields are canonical unsigned LEB128 u32 (functions and modules may exceed 127 instructions, constants, registers, captures, and arguments), bounded by explicit decode and structural resource limits. Its round-trip guarantees -- totality over hostile bytes, canonical re-encoding, and decode/encode identity -- are fresh properties of this codec, proven by the tests in this module, not the Lean single-byte theorems (decode_total, decode_encode_canonical, encode_decode_identity), which remain scoped to the formal five-op wire.