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. It adds no syntax, datum, primitive, ambient I/O, or semantic profile. 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. Product version is reported by tooling but does not change stable semantic bytes.

The artifact identity is:

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

Producer identity records provenance, not trust.

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 only accepted section order is:

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:

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; and
5. instruction charges and aggregate resource bounds.

An unknown opcode, dangling reference, noncanonical constant, invalid merge, residual stack, unbalanced scope, missing return, or unreachable instruction fails closed. Validation proves structural admissibility, not semantic equivalence or producer trust.

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; and
• static verification work: 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 is an engine failure, not a catchable Lispex condition. Tree recursion depth and VM transitions are different host resource profiles; equal semantics do not imply equal numeric ceilings.

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 are not stored. 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. They never enter the tree evaluator.

The VM therefore differs structurally from the tree engine, but it is still the same Rust product lineage. It is a differential execution route, not a fourth independent backend family.

Exact Topaz VM boundary

The optional Topaz route consumes the same canonical bytes through a separate checked reader, verifier, and explicit-control VM written in Topaz. It is available only 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, process output and result JSON are bounded, and execution has a fixed timeout.

The result is untrusted until its request hash, invocation, identities, canonical decimal u64, status/exit pair, output accounting, structural counts, target, lineage, and fallback counters all validate. Any failure stays on the Topaz route. There is no discovery through PATH, repository lookup, network access, retry in Rust/tree/LIL/LIT, or older-Topaz fallback.

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. 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 does not parse bytecode or contact another engine.

This is a complete-profile correctness route, not an optimized ABI or a proof that compilation preserved every meaning. Use lispex aot build|inspect|validate|run; see the Topaz AOT guide 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 never falls back to tree.
• LIL and LIT remain backend families; --engine cannot select an engine for them.
• 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 no-clobber diagnostic material. It cannot be executed or promoted into authority.

Product support

Unsupported products do not emulate the binary format in JavaScript and do not silently downgrade to another engine.

Integrity enters Vouch only through exact derivation

Bytecode canonicality and verification do not prove that compilation preserved meaning, authenticate a producer, approve a rule, select consumer input, establish current multi-family agreement, or grant a decision. The Vouch authority root remains exact source or a fully proved Lispex Image that recovers it. General bytecode bytes and hashes, inspections, validation reports, VM results, and tree/VM comparison reports are not Vouch inputs.

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 container is never accepted in place of source or input, and its inspection, validation, re-execution, or gate report cannot mint live evidence.

The general Topaz VM route is deliberately outside that chain. Its request, result, hashes, executable identity, output, and comparison receipt cannot be used as a compiled Vouch artifact, re-execution observation, evidence handle, or gate grant.

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