Skip to main content

Module verifier

shape_vm::bytecode

Module verifier 

Source
Expand description

Bytecode verifier for trusted and v2 typed opcodes.

Validates that trusted opcode invariants hold:

  • Every trusted opcode carries the operand shape its handler requires (LoadLocalTrusted → Operand::Local, JumpIfFalseTrusted → Operand::Offset).

Also validates v2 typed opcode invariants:

  • Typed array ops require a FrameDescriptor with non-Unknown slots
  • Typed field ops have FieldOffset operands with reasonable byte offsets
  • Sized integer (i32) ops require a FrameDescriptor with non-Unknown slots

§WS-10b — stale MissingFrameDescriptor rule removed (2026-05-22)

verify_trusted_opcodes previously errored MissingFrameDescriptor / UnknownSlotKind for any trusted opcode in a function whose Function.frame_descriptor was None / empty. That rule encoded the pre-ADR-006 §2.7.7 trusted-opcode contract, when trusted opcodes skipped runtime tag-bit validation and relied on descriptor-supplied slot-kind metadata to justify the skip.

Post-§2.7.7 only two trusted opcodes survive — LoadLocalTrusted (0xD7) and JumpIfFalseTrusted (0xD8). Their executors (executor/variables/mod.rs::op_load_local_trusted, executor/control_flow/mod.rs::op_jump_if_false_trusted) source slot kind from the §2.7.7 stack parallel-Vec<NativeKind> track, NOT the FrameDescriptor. LoadLocalTrusted is byte-for-byte identical to non-trusted LoadLocal; JumpIfFalseTrusted pops the kinded condition slot directly. current_frame_descriptor() has zero VM executor call sites — the descriptor is consumed at runtime only by the JIT, which already has an explicit absent-descriptor fallback (shape-jit::worker.rs, mir_compiler/v2_call_abi.rs).

The stale rule fired 16 false positives on every program run (stdlib prelude functions with an unannotated / any-typed local whose whole frame the storage-hint pass could not prove). It enforced nothing — load_program only eprintln!’d — but printed “Bytecode verification failed” on a clean prelude. The rule is dropped; verify_trusted_opcodes now verifies the still-meaningful invariant (operand shape). The verify_v2_typed_opcodes pass — which checks real v2 invariants — is unchanged and keeps its enforcement structure.

Enums§

VerifyError
Errors produced by the bytecode verifier.

Functions§

verify_trusted_opcodes
Verify that all trusted opcodes in a program are well-formed.
verify_v2_typed_opcodes
Verify that all v2 typed opcodes have valid invariants.