Bytecode, Verifier, and Native VMs

Product pipeline

exact source
  -> reader and hygienic normalizer
  -> lispex.core-ir/v1
  -> deterministic bytecode compiler
  -> lispex.bytecode/v1
  -> strict reader and verifier
  -> lispex-rust-vm/v1
  -> ordinary Lispex outcome, output, warning, and diagnostic

This pipeline compiles the existing lispex-profile-1.5 and preserves its syntax, datum kinds, primitives, and semantics. The tree interpreter remains the reference and default Rust engine.

Fixed identities

The header binds the exact source identity, Core IR hash, primitive-registry tag and hash, profile, instruction/source-map/cost identities, producer, and sorted requirements. Tooling records the product version alongside the stable semantic bytes.

The artifact identity is computed like this.

SHA-256("lispex/bytecode-hash/v1" || 0x00 || canonical-bytecode-bytes)

Producer identity records provenance for the recipient's trust policy.

Canonical binary envelope

The binary has one eight-byte magic/version prefix, one fixed section count, strictly increasing known section tags, a big-endian u32 length for each payload, and no padding or trailer.

The canonical section order is shown below.

identity
strings
constants
anchors
bindings
globals
scopes
functions
guards
blocks
roots

Indexes and counts are big-endian u32. Text is exact UTF-8 prefixed by its byte length. Strings, constants, anchors, IDs, and table references have one canonical order and representation. The strict reader bounds before allocation, uses checked arithmetic, validates UTF-8 and every typed table, then re-encodes and requires byte-for-byte equality.

Instruction families

Blocks contain linear instructions. Jump operands are decoded instruction indexes, not byte offsets. Source order is preserved. The compiler performs no constant folding, dead-code elimination, reordering, inlining, numeric reassociation, or fresh tail inference. It copies Core IR's resolved contract.

Verification order

Before constants, globals, closures, input, or VM state can exist, the verifier checks the following, in order.

1. magic, sections, lengths, canonical encoding, and all fixed identities
2. sorted unique pools, exact datum rendering, contiguous IDs, table roles, and every reference
3. primitive/global identity, lexical visibility, forwarding overlays, function captures, guard descriptors, and source anchors
4. reachable control flow, legal jump targets, stack and outcome shapes, scope balance, branch joins, terminal tail calls, and complete returns
5. instruction charges and aggregate resource limits

An unknown opcode, dangling reference, noncanonical constant, invalid merge, residual stack, unbalanced scope, missing return, or unreachable instruction fails closed. Validation establishes structural admissibility. Signed artifact workflows identify producers, and engine comparison records semantic agreement.

Fixed bounds and resource model

• artifact size, at most 32 MiB
• each major pool or table, at most 100,000 entries
• each variable-width operand list, at most 100,000 entries
• static verification work, which is checked linear work over instructions and edges

Every executed instruction, primitive dispatch, and guest-procedure transition has a nonnegative versioned charge. Runtime reports selected limits, transitions used, output bytes, peak explicit-control frames, completed roots, and forbidden fallback count. Output limits cover primitive effects and top-level auto-print in their exact order.

Resource exhaustion produces a terminal engine status. Tree recursion depth and VM transitions publish separate resource profiles.

Source maps and diagnostics

Every instruction names one positive line-and-column anchor inherited from Core IR. Paths, host names, timestamps, and platform newline choices belong to the host-application record. Runtime faults use the current instruction anchor, so tree/VM comparison can check diagnostic code, location, message, partial output, and warnings as semantic axes.

Rust VM execution model

The VM uses explicit code activations, lexical scopes, return frames, handlers, guard state, wind state, and one-shot continuations. Tail calls replace the current activation rather than growing a host call stack. Closures retain shared mutable cells, including forwarding overlays for dynamic definitions.

All 205 current primitive rows are dispatchable. Ordinary primitive leaves share the installed Rust value, number, aggregate, rendering, diagnostic, and writer code. The 18 primitives that call guest procedures use VM-owned iterative state machines, including mapping, folds, apply, call-with-values, exception handlers, continuations, and dynamic-wind. The tree interpreter uses the reference path for these primitives.

The VM and tree interpreter remain part of the same Rust product lineage and form a differential execution route.

Exact Topaz VM boundary

The Topaz route consumes the same canonical bytes through a separate checked reader, verifier, and explicit-control VM written in Topaz. It is available in Native macOS ARM64 with an exact separately installed Topaz 5.11 product root.

Before invocation, Lispex checks the fixed provider manifest, Topaz artifact, executable, wrapper, managed files, source/compiler lineage, target, primitive registry, and five zero fallback counters. The closed request binds the exact source, Core IR, bytecode, optional canonical input, full u64 transition limit, structural limits, and product identities. Private staging is mode 0700. The child receives a cleared environment with a fixed system PATH and C locale. The provider profile sets process-output, result-JSON, and timeout limits.

Lispex accepts the result after validating its request hash, invocation, identities, canonical decimal u64, status/exit pair, output accounting, structural counts, target, lineage, and fallback counters. Closed product selection keeps each failure on the selected Topaz route.

Static Topaz AOT branch

Native macOS ARM64 can instead emit the verified control graph as readable Topaz source and build a source-free executable with the exact installed Topaz 5.11 compiler and exact Rust tool proxies. AOT stands for ahead-of-time compilation, which turns the rule into a standalone program before it runs, so nothing compiles it at run time. The installed product binds source, Core IR, bytecode, generated-source bundle, source map, topaz.artifact.v1, executable, producer, target, resource request, and five zero fallback counters. Runtime executes the installed executable directly.

This is a complete-profile correctness route with an explicit calling convention. Use lispex aot build|inspect|validate|run, and see Build a Product Compiled Ahead of Time for the exact installed-product workflow.

Engine selection and comparison

• lispex run --backend rust defaults to --engine tree.
• --engine vm performs source → Core IR → bytecode → verify → VM in memory.
• A selected VM compile, verification, resource, or runtime failure returns on the selected VM route.
• LIL and LIT are selected through their backend families.
• lispex compare-engines --receipt FILE SOURCE records exact intermediate identities and semantic mismatch axes in lispex.rust-engine-comparison/v1.
• lispex bytecode run --engine topaz --topaz-vm ROOT --bytecode FILE selects the exact installed Topaz product.
• lispex compare-vms --topaz-vm ROOT --receipt FILE SOURCE derives bytecode once and records Rust/Topaz mismatch axes in lispex.topaz-vm-comparison/v1.

A report is atomically published diagnostic material for inspection and comparison.

Product support

Each product returns its documented command status and preserves the selected engine.

How verified bytecode enters Vouch

Vouch derives compiled evidence from exact source or a canonical Lispex Image that recovers it. Producer authentication, recipient policy, consumer input, engine agreement, and the decision gate each keep their explicit record in the workflow.

Native can explicitly build lispex.vouch-compiled-artifact/v1 from that exact source. A compiled Vouch invocation authenticates and pins the request, re-derives the artifact's Core IR and bytecode, preserves current tree/Meaning agreement, and only then compares the verified Rust VM transcript. The source and input remain explicit alongside the container. Inspection, validation, re-execution, and gate reports keep their own artifact roles.

The Topaz VM route publishes its request, result, hashes, executable identity, output, and comparison receipt as route evidence. The compiled Vouch path uses the Rust VM artifact derived from the consumer-pinned source.

Keep going

Use the guided workflow for commands and recovery, and the Core IR reference for the resolved input contract.

Run Verified Bytecode · Core IR Contract · Checked Surfaces