Crate bamts_bytecode

Expand description

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:

The activation yields the value in src (a produced item for a generator; an awaited operand for an async function) to its driver.
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).
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.

Structs§

BigIntLiteral: A canonical BigInt literal in decimal text form. Constructed only through BigIntLiteral::new, so a BigIntLiteral value is always a canonical decimal integer: optional leading -, no redundant leading zeros, no -0.
Binding: One named module binding. A binding identifies a live cell, never an activation register.
BindingId: Index of a binding within a module’s binding table.
Certificate: Forward-dataflow definite-initialization facts, mirroring Lean’s Certificate.facts. Construction is private, so certificates are unforgeable.
ConstantId: Index into a module’s constant pool.
DecodeError
DecodeLimits: Decoder allocation/input ceilings, enforced before any allocation.
EcmaString: An immutable ECMAScript string represented exactly as UTF-16 code units.
EcmaStringBuilder: The owned accumulation path for exact ECMAScript strings.
Edge: One canonicalized module dependency.
EdgeId: Index of an edge within a module’s linkage table.
ExceptionHandler: A half-open protected range [start, end), its handler entry PC, and the register that receives the thrown value on dispatch.
Export: One named export.
Function: An explicit function record: metadata, code, and handlers. On entry the leading capture_count registers hold the closure’s captured cells and the next parameter_count registers hold the parameters; all capture_count + parameter_count are initialized on entry.
FunctionFlags: Compact function flags record.
FunctionId: Index into a module’s function table.
IllFormedUtf16: The first unpaired surrogate encountered while validating UTF-16.
InvalidCodePoint: A code point outside the Unicode scalar-value range.
Module: Explicit constant pool, function table, and entry function, with typestate.
ModuleId: Index of a module within a program.
NumberBits: Canonical IEEE-754 bits. Every positive or negative NaN payload collapses to the unique arithmetic NaN from Bamti.canonical_nan.
Pc: A program counter: an instruction index within a function’s code.
Program: The sole self-contained executable wire value.
ProgramDecodeError
ProgramDecodeLimits: Strict program-level resource ceilings, applied before allocation.
ProgramModule: A canonical module blob and its program-only identity/linkage metadata.
ProgramVerifyError
Register: Index of a virtual register within a function’s register file.
Unverified: Marker for decoded or newly assembled, untrusted bytecode.
Verified: Unforgeable marker proving verification completed.
VerifyError: A structural verification failure, located at a function and/or instruction.

Enums§

AccessorKind: Which half of an accessor descriptor Instruction::DefineAccessor installs. A property with both a getter and a setter is defined by two instructions on the same key.
BinaryOp: Closed set of binary operators. BinaryOp::Add is the formal core’s Add.
BindingKind: The initialization and linkage role of a module binding.
Constant: Persistable values. Heap references, holes, and uninitialized sentinels are intentionally absent because they are runtime identities/states. String constants back property keys, global names, private-name descriptions, regular-expression pattern/flags, module specifiers, and export names.
DecodeErrorKind
EdgeKind: The runtime roles represented by one canonicalized module dependency.
EdgeTarget: A module dependency. External dependencies deliberately have no path or host identity.
ExportSource: The source of an exported name.
Instruction: The production instruction algebra. Opcodes 0..=36 are stable wire tags.
IteratorKind: Closed set of iterator acquisition protocols for Instruction::GetIterator.
LoadError
ProgramDecodeErrorKind
ProgramLoadError
ProgramVerifyErrorKind
ResolvedExport: A verified export resolution with no copied names or paths.
UnaryOp: Closed set of unary operators.
VerifyErrorKind

Constants§

FORMAT_VERSION: The sole supported wire version.
MAGIC: BMTBC\0\0\1, matching Bamti.Bytecode.magicBytes.
MAX_CONSTANTS: Structural verify-time ceiling on a module’s constant count.
MAX_FUNCTIONS: Structural verify-time ceiling on a module’s function count.
MAX_HANDLERS: Structural verify-time ceiling on a function’s handler count.
MAX_INSTRUCTIONS: Structural verify-time ceiling on a function’s instruction count.
MAX_REGISTERS: Structural verify-time ceiling on a function’s register count. Generous enough for real code yet bounds definite-initialization bitset allocation.
MAX_VERIFIER_FACTS_WORDS: Combined verify-time ceiling on the total definite-initialization fact storage a module may force the verifier to allocate, in 64-bit words. Each function needs instructions * ceil(registers / 64) words, so independent per-function maxima (MAX_INSTRUCTIONS * (MAX_REGISTERS / 64) alone is 2^30 words = 8 GiB, and modules hold many functions) would permit multi-GiB allocations from untrusted input. This bound caps that transient storage at MAX_VERIFIER_FACTS_WORDS * 8 bytes (64 MiB) while remaining generous enough for large real modules with far more than 127 functions.
PROGRAM_MAGIC: BMTPC\0\0\1: the canonical whole-program container, distinct from module magic.
PROGRAM_VERSION: The sole supported program-envelope version.

Functions§

decode: Strictly decodes untrusted bytes. Every length is checked before allocation; semantic validity remains represented by the Unverified typestate.
decode_program: Strictly decodes a program envelope while retaining unverified typestate.
decode_verified: Decodes and verifies in one boundary operation.
decode_verified_program: Decodes and verifies a whole program in one boundary operation.