Lispex Bytecode and VM Reference

Follow Run Verified Bytecode for a complete source-to-result example. Its refund-window.lpxbc file contains instructions. Inspection and comparison JSON describe that file or a run.

Read an inspection report

The guide's refund rule produces these fields in the bytecode inspect report.

{
  "requirements": ["explicit-input"],
  "source_map_coverage": {
    "complete": true,
    "mapped_instructions": 22,
    "referenced_anchors": 11,
    "schema": "lispex.bytecode-source-map/v1",
    "total_anchors": 11,
    "total_instructions": 22
  }
}

The file requires an explicit input. All 22 instructions have source positions, using 11 distinct anchors. An anchor is a line and column in the original source.

The full report also contains source, Core IR, and bytecode identifiers, table counts, an instruction histogram, and root positions. A root is a top-level expression. The report says execution: "not-run" and authority: "integrity-only". bytecode validate returns valid: true after strict decoding, verification, and re-encoding.

Compilation and identifiers

Native reads source, rewrites shorthand into Core forms, and resolves names in lispex.core-ir/v1. The bytecode compiler turns that file into lispex.bytecode/v1. The reader and verifier check the bytecode before the Lispex VM executes it.

This implements lispex-profile-1.5, including its syntax, data kinds, builtin procedures, and language behavior. Lispex Interpreter is the reference engine and the default for source execution.

The header records exact source and Core IR identifiers, the registry tag and hash, and the language profile. It also records instruction, source-map, cost-model, and producer identifiers, plus sorted input requirements. Tool reports record the product version alongside these stable identifiers. The producer identifier describes the compilation origin for recipient policy.

The bytecode identifier uses this hash domain.

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

Canonical means one prescribed byte representation for all recorded information, including exact source identity. Programs with equal results can have different source and bytecode identifiers.

Binary encoding

The file starts with an eight-byte magic/version prefix and a fixed section count. Known section tags must increase strictly. Each payload has a big-endian u32 byte length, with no padding or trailer. Big-endian places the most significant byte first.

The section order is fixed.

identity
strings
constants
anchors
bindings
globals
scopes
functions
guards
blocks
roots

Indexes and counts are big-endian u32 values. Text is exact UTF-8 preceded by its byte length. Strings, constants, anchors, IDs, and references each have a prescribed order and representation.

The reader checks limits before allocation and checks arithmetic for overflow. It validates UTF-8 and each table's expected types. It then re-encodes the file and requires byte-for-byte equality.

Instructions and verification

A block contains a sequence of instructions. Jumps address decoded instruction indexes, rather than byte offsets. The compiler preserves source order and Core IR's resolved references and tail-call positions. It performs no constant folding, dead-code removal, reordering, inlining, numeric reassociation, or new tail-position inference.

Before creating runtime constants, globals, closures, input bindings, or VM state, verification checks these items in order.

1. Magic, sections, lengths, canonical encoding, and fixed identifiers.
2. Sorted unique pools of shared data, exact datum rendering, contiguous IDs, table roles, and references.
3. Primitive and global IDs, lexical visibility, forwarding cells, function captures, guard descriptors, and source anchors.
4. Reachable control flow, jump targets, stack and result shapes, scope balance, branch joins, terminal tail calls, and complete returns.
5. Instruction charges and total resource limits.

A capture is an outer variable cell retained by a function. Forwarding cells connect references to definitions activated during execution. Guard descriptors record exception-handling regions. At a branch join, the incoming stack and scope states must agree.

Unknown opcodes, dangling references, noncanonical constants, invalid joins, leftover stack values, unbalanced scopes, missing returns, and unreachable instructions are rejected. Verification establishes structural validity. Signed distribution identifies producers. Engine comparison records whether execution results agree.

Resource limits and diagnostics

A guest procedure is a procedure defined by the Lispex program. Runtime reports selected limits, transitions used, output bytes, peak control frames, completed roots, and forbidden fallback count. Output limits cover primitive effects and top-level automatic printing in execution order. Resource exhaustion terminates the engine. Tree recursion depth and VM transitions use separate resource profiles.

Each instruction carries a positive line-and-column anchor from Core IR. The calling application records paths, host names, timestamps, and platform newline choices. Runtime faults use the current instruction's anchor. Tree/VM comparison can therefore compare diagnostic code, location, message, partial output, and warnings.

Lispex VM execution

The VM keeps explicit records for active code, lexical scopes, returns, exception handlers, guards, and dynamic-wind. It also supports one-shot continuations. A tail call replaces the active code record without growing the host call stack. Closures share mutable cells, including forwarding cells for dynamic definitions.

All 205 primitive entries are dispatchable. Ordinary primitives share Rust code for values, numbers, aggregates, rendering, diagnostics, and writing. The 18 primitives that call guest procedures use iterative VM state machines. These include mapping, folds, apply, call-with-values, exception handlers, continuations, and dynamic-wind. The Lispex Interpreter uses its reference implementations for those procedures.

Tree and VM belong to the same Rust product family. Their comparison records results from two execution methods within that family.

Select an engine and compare

Selected VM failures return on that execution method without fallback. The engine reference describes current Lispex execution and LIL/LIT retirement. Comparison reports are written in one step to new paths.

Native platforms provide bytecode tools and the Lispex VM. npm, public WASM, and the Playground provide source tree execution and Lispex Images. See the product catalog for platform details.

Compiled bytecode in Lispex Vouch

Lispex Vouch builds lispex.vouch-compiled-artifact/v1 from source accepted by csk.checked-profile/v1. Save this complete source as vouch-rule.lspx, then create and validate its container.

(if (exact-integer? input) (decision-approve) (decision-deny))

lispex vouch compiled build --source vouch-rule.lspx --out vouch-rule.lpxvca
lispex vouch compiled validate --artifact vouch-rule.lpxvca --source vouch-rule.lspx

Both commands exit 0. The first creates vouch-rule.lpxvca and prints a lispex.vouch-compiled-artifact-build/v1 report. The second prints a validation report with these fields.

{
  "compiled_artifact_validation": "lispex.vouch-compiled-artifact-validation/v1",
  "derivation": "exact-source",
  "execution": "not-run",
  "valid": true
}

The refund source from the guide does not follow csk.checked-profile/v1. This build command rejects it with compiled-artifact-source-invalid and exit 1. Write the source for that profile when you prepare a compiled container.

A compiled Vouch request retains exact external source and consumer input. Source can also be recovered from a canonical Lispex Image. Issuer authentication, recipient policy, request binding, engine agreement, and the decision gate each have separate records.

The --compiled-artifact option on vouch verify --reexecute and vouch gate selects this container. Native authenticates and pins the request, re-derives Core IR and bytecode from the source, and checks current tree/Meaning agreement. It then compares the verified Lispex VM execution record. Inspection, validation, re-execution, and gate reports describe their respective steps.

The compiled Vouch workflow uses the Lispex VM artifact derived from the consumer's exact source.