The preceding mutable cell and recursive-function compiler has correct lexical behavior on tested inputs, but each variable read searches scope dictionaries by its name. It also relies on source-level type checking without independently checking the stack and control-flow structure of the generated bytecode. Both limitations expose a boundary between parsing a well-typed source program and executing a structurally valid virtual-machine program. This chapter adds a second, opt-in backend that resolves lexical variables to slots and verifies instruction sequences before they are executed [1][3].

The previous backend remains intact and serves as an independently implemented runtime oracle. The new backend reuses the same parser, AST and source-level type checker, which means the two machines are not independent at the front-end. Their instruction representations and execution strategies differ, however, allowing meaningful cross-checks of code generation and closure behavior.

Lexical addresses: binding identity before execution#

A lexical address is a pair (distance, index). Distance counts the number of scope frames between the current lexical frame and the frame that declares a variable; index identifies that variable's position within the declaring frame. Both coordinates are nonnegative integers. For example, in let x:Int=10 in let f:Fn(Int)->Int=fn(y:Int)->Int=>x+y in f(2), the function body has parameter y at address (0,0), while outer x is at (1,0): one frame above the parameter scope [1].

A compiler can calculate this address statically by keeping a list of lexical scope descriptors. Each descriptor records the binding name, static type, write permission, whether a binding is recursive and whether initialization has completed. On a name reference, the resolver scans descriptors from the innermost outward, choosing the first matching name, then embeds its numerical address into the instruction LOAD_SLOT. An assignment similarly becomes STORE_SLOT (distance,index). This search happens once during compilation, rather than once every time the instruction runs.

A source-level name is therefore a convenient interface for the programmer, not a requirement for VM lookup. The reference is resolved using lexical structure, not the current call stack or a process-wide global dictionary. Distinct bindings with the same name produce different addresses: shadowing is not an overwrite of the earlier slot. This is the same engineering distinction made when compilers resolve locals and upvalues ahead of execution [1][2].

Runtime frames and retained mutable locations#

The indexed VM stores each lexical scope as a list of slots, instead of a dictionary keyed by variable names. A variable read accesses scopes[-1-distance][index], where the two indices have been checked by the verifier. This is constant-time abstract indexing in Python lists; it removes linear name search from the VM's instruction dispatch. It does not make the total cost of every closure operation constant, since scopes are still copied at closure creation and function entry.

Immutable bindings store their values directly in the scope's list. A mutable binding stores a shared Cell object. Copying the scope list preserves the identity of each retained cell, so distinct closures that capture the same var binding see one shared location. Two different declarations of x, by contrast, allocate different slots and cells. Recursive function creation uses DECLARE_REC_SLOT to allocate an initially unreadable, nonwritable cell, CLOSURE_SLOT to capture that cell, and INIT_REC_SLOT to store the completed closure exactly once.

An activation frame still owns its instruction pointer, operand stack and lexical scopes. A call removes the function and its arguments from the caller's operand stack and starts a new activation frame whose parameter slots appear after the captured lexical scopes. Returning a result resumes the caller's independent stack. This preserves lexical scoping even when a closure outlives the activation record that allocated its original mutable cell [2].

Why a bytecode verifier is necessary#

Even a correct source program can encounter bugs in a compiler backend or a serializer. Imagine an instruction sequence that performs ADD with one operand, jumps into the middle of a scope without executing ENTER, reads slot 3 from a frame containing only one slot, or returns a Boolean from code statically declared to return Int. These errors need to be rejected before execution, rather than left entirely to unpredictable VM failures.

The example verifier operates on a bounded in-memory VerifiedProgram representation containing SlotCode objects. It checks instruction tuple shapes, accepted opcodes, typed immediates, lexical slot bounds, write permissions, operand-stack underflow, function argument types, return types, balanced scopes and the ordering of recursive initialization. It also checks nested closure bodies against the lexical environment they capture. The notion of verification follows the broad goal of the JVM's class-file verifier: reject invalid code according to a defined type and control-flow discipline before executing it [3]. This implementation does not verify JVM class files or implement the JVM's complete verification algorithms.

The verifier additionally rejects unrecognized instructions, loops introduced by backward jumps, unreachable instruction payloads and code structures above configured instruction/object budgets. Backward bytecode jumps are absent from the teaching compiler's output because recursion is represented by function calls; only forward jumps implement conditionals. This simplifies abstract interpretation without claiming that a general-purpose VM could omit backward branches.

Abstract interpretation and control-flow joins#

The verifier does not evaluate user arithmetic. Instead, at each reachable instruction index it records an abstract state: (operand stack of types, lexical scope descriptors). For instance, after PUSH_INT 3 the stack type becomes [Int], and after a second integer push followed by ADD it again becomes [Int]. A division of two numeric operands returns a static Rat. The abstract transfer for STORE_SLOT requires the assigned expression type to equal the destination slot type and the destination to be writable, while leaving the assigned type on the stack because assignment is an expression [4].

For JUMP_IF_FALSE, the verifier requires a Boolean on top of the stack, removes it and explores both successor instruction indices. Each successor carries the resulting abstract stack and scope information. When different control-flow paths reach the same instruction, their abstract states must agree: mismatched stack heights, stack types or lexical scopes indicate invalid bytecode. JUMP has a single target, and both jump opcodes require a strictly forward in-range destination. This worklist procedure eventually processes every reachable instruction because the verified control-flow graph is finite and forward-only.

RETURN requires exactly one value matching the block's declared return type, and no local scopes remaining open. A nested SlotCode object declares its parameter types, expected return type and captured lexical descriptors. CALL checks the number and types of argument values against the function-type value on the operand stack, not just a raw instruction count. These rules detect corruption that ordinary integer-only stack-height checks would miss.

Recursive cells and initialization order#

A subtle case is a recursive function that captures an as-yet-uninitialized reference to itself. A function body may legitimately contain LOAD_SLOT of that captured recursive slot: the function will run after initialization. But an immediate direct read of the same slot, before INIT_REC_SLOT, must be forbidden.

The verifier therefore requires the adjacent sequence DECLARE_REC_SLOT, CLOSURE_SLOT, INIT_REC_SLOT for a fresh recursive binding. It permits a nested closure to retain that placeholder descriptor but disallows a direct top-level load before initialization. The instruction INIT_REC_SLOT transitions the scope descriptor to initialized only after checking that the stack contains a function of the expected type. Independently, the VM rejects any runtime read of an uninitialized cell. The conjunction of source restrictions, structural verification and runtime checks is narrower than a formal, general recursive-bytecode safety proof.

This limitation matters. The verifier assumes its own trusted in-memory SlotCode representation and disallows cyclic/shared nested code-object graphs. It does not authenticate bytes, defend against malicious changes after verification, or prove resource safety. The verifier is an engineering teaching tool, not a safe arbitrary-code execution service.

Executable verification against the previous VM#

The slot compiler and verifier implementation exports compile_slots, verify_slots, run_slots, evaluate_slots, SlotInfo and BytecodeError. The demonstration below exercises lexical capture, shared state, static verification and rejection of malformed bytecode.

from fractions import Fraction
from examples.python.lexical_slot_verifier import (
    compile_slots, verify_slots, run_slots, evaluate_slots,
    SlotInfo, SlotCode, VerifiedProgram, BytecodeError,
)

source = ("var x:Int=1 in "
          "let f:Fn()->Int=fn()->Int=>set x=x+1 in "
          "f()+f()")
program = compile_slots(source)
assert verify_slots(program)
assert run_slots(program) == Fraction(5)
assert evaluate_slots(source) == ("Int", Fraction(5))

bad = VerifiedProgram(
    "Int", SlotCode((), (), "Int", (
        ("LOAD_SLOT", (0, 0), 0),
        ("RETURN", None, 0),
    ))
)
try:
    verify_slots(bad)
    assert False, "out-of-bounds slot must fail verification"
except BytecodeError:
    pass

The independent contract suite executes the earlier name-based VM, the new slot-based VM and a separate direct AST interpreter on selected identical programs. It also generates deterministic counter and factorial cases and fabricates invalid instruction streams with underflow, incompatible types, invalid addresses, bad control flow, unbalanced scopes and recursive initialization errors. Tests cover both positive equivalence and negative rejection. They remain finite tests and cannot establish perfect compiler correctness.

Complexity, safety boundaries and next prerequisites#

Let n be the AST size, d the number of visible lexical scopes, m the number of emitted instructions and c the number of captured environment entries. Resolving one variable by scanning descriptors takes worst-case O(d) scope visits, plus searching bindings within each scope; this cost occurs at compile time. Runtime LOAD_SLOT is O(1) abstract indexing, assuming a valid address and constant-time Python list access. Closure creation and call entry can still copy O(c) slots, while compiling and verifying the remaining code involves more work than one abstract machine step. A basic worklist verifier visits forward control-flow instructions with state sizes dependent on stack height and scope descriptors; because those immutable abstract states are materialized at joins, a blanket O(m) runtime claim would be misleading.

The VM continues to apply explicit instruction and call-frame budgets. Verifying structural and type invariants is not equivalent to enforcing a CPU, heap, filesystem or process security boundary. Arbitrary-precision rational calculations can be expensive, and captured cells may outlive their creating frames. Code-object graph sharing, persistent bytecode formats, bytecode signatures, exception edges, backward control flow, concurrent mutability and native machine-code generation remain unsupported.

Exercises and verification#

  1. Resolve both reads in fn(y:Int)->Int=>x+y when x belongs to the immediately enclosing captured frame. Check: x is at (1,0), while y is at (0,0).
  2. Construct code that executes ADD after only one PUSH_INT. Check: the verifier rejects operand-stack underflow before VM execution.
  3. Make a conditional's branches reach the same instruction with stacks [Int] and [Bool]. Check: the control-flow join is rejected even if one branch would be skipped at runtime.
  4. Replace a valid STORE_SLOT address with an address to an immutable binding. Check: verification rejects the write despite the numeric value fitting the target type.
  5. Explain why the verifier allows a recursive closure to capture an uninitialized slot but forbids immediate reads before INIT_REC_SLOT. Check: the cell's identity must exist before constructing its self-referential closure, but its value becomes readable only after initialization.
  6. Compare compile-time name resolution with runtime slot indexing. Check: name search moves to compilation; capturing and copying environment data still has a separate cost.

The next stage should make scope descriptors more compact, introduce a serialized bytecode format with versioned verification, and eventually study heap reachability and memory management. None of these topics can be treated as implemented by the current in-memory verifier.