Run Verified Bytecode

Prepare a rule and an input

Save this as refund-window.lspx:

(define (decide days)
  (if (<= days 30) 'refund 'review))

(decide input)

Save the single input datum as request.lspx:

14

input is not a file or environment lookup. It is an explicit requirement recorded in Core IR and bytecode, then supplied by the command below.

Build Core IR, then bytecode

lispex core-ir build \
  --source refund-window.lspx \
  --out refund-window.lpxir

lispex bytecode build \
  --ir refund-window.lpxir \
  --out refund-window.lpxbc

The first command resolves names, cells, captures, tail positions, and source anchors without executing the rule. The second command lowers that canonical Core IR to lispex.bytecode/v1, verifies the result, and writes a new binary artifact. Neither command overwrites an existing destination.

Inspect or validate before running

lispex bytecode inspect --bytecode refund-window.lpxbc
lispex bytecode validate --bytecode refund-window.lpxbc

inspect prints identities, bounded table counts, requirements, opcode counts, root anchors, and source-map coverage. validate is the quieter automation boundary: it strictly decodes, verifies, re-encodes, and accepts only the one canonical byte representation.

Both commands are integrity checks. They do not authenticate the producer, approve the rule, bind a consumer request, or execute a decision.

Run only after verification

lispex bytecode run \
  --bytecode refund-window.lpxbc \
  --input request.lspx

refund

The Native CLI verifies the complete artifact before it creates VM state. Malformed bytes fail before input use, output, primitive dispatch, or a VM step. If the artifact declares input, omitting --input fails; supplying input to an artifact that does not declare it also fails.

One stdin stream cannot carry both inputs. This is rejected:

lispex bytecode run --bytecode - --input -

Use a named file for either the bytecode or the datum instead.

Run the same artifact in the Topaz VM

Rust is built in and remains the default. On macOS ARM64, you can explicitly select the exact admitted Topaz 5.11 product:

lispex bytecode run \
  --engine topaz \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --bytecode refund-window.lpxbc \
  --input request.lspx

The product root must be an absolute path to the separately installed lispex-topaz-vm/v1 product. Lispex checks its manifest, Topaz artifact, executable, wrapper, managed files, compiler/source lineage, target, resource contract, and zero-fallback declaration. It never searches PATH, a sibling checkout, the network, or an older installation. A missing, changed, timed-out, or malformed Topaz product is reported as that route's failure; Rust is not retried.

Select the VM for source

For a self-contained source file, the shorter route is:

lispex run --backend rust --engine vm rule.lspx

tree remains the default:

lispex run --backend rust --engine tree rule.lspx

An explicit vm request never retries through tree. --engine belongs only to the Rust backend; combining it with LIL, LIT, or an external backend registry is a usage error.

Compare both Rust engines

lispex compare-engines \
  --receipt tree-vm.json \
  rule.lspx

The no-clobber report records exact source, Core IR, and bytecode identities, both semantic observations, mismatch axes, VM resource measurements, and the fallback count. It is useful regression evidence, but both engines share Rust values and primitive leaves. Agreement is not an independent implementation witness or a proof of equivalence.

To compare the two bytecode VMs instead:

lispex compare-vms \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --receipt rust-topaz.json \
  rule.lspx

This derives bytecode once, runs Rust and Topaz explicitly, and compares status, output, values, warnings, diagnostics, resource observations, and completed roots. The Topaz source is structurally separate, but its executable was produced by Topaz Rust Stage 0. Agreement is differential evidence, not proof or Vouch authority.

When you have also built the matching AOT product, compare every Native route:

lispex compare-routes \
  --topaz-vm /absolute/path/to/aarch64-apple-darwin \
  --aot-product /absolute/path/to/refund-window-aot \
  --receipt four-routes.json \
  --input request.lspx \
  refund-window.lspx

The command uses one frontend result and one verified bytecode artifact for tree, Rust VM, Topaz VM, and AOT. A source/Core IR/bytecode mismatch rejects the AOT product before any route runs. The receipt is no-clobber, records semantic and comparable-resource mismatch axes separately, exposes every lineage and fallback counter, and has no Vouch authority.

Choose the right product

npm, public WASM, and Playground continue to run source with their documented tree execution and Exact Image support. They do not contain a JavaScript bytecode reader, verifier, or VM.

Opt into compiled Vouch without promoting bytecode

A canonical bytecode hash identifies exact bytes. Verification establishes bounded structural admissibility. Local VM execution establishes only what that Native run observed. An ordinary .lpxbc file still cannot issue or authenticate an envelope, satisfy trust policy, choose source or input, or grant a gate.

When a consumer deliberately wants VM agreement in addition to the existing Vouch checks, Native builds a separate source-bound container:

lispex vouch compiled build \
  --source refund-window.lspx \
  --out refund-window.lpxvca

lispex vouch compiled validate \
  --artifact refund-window.lpxvca \
  --source refund-window.lspx

vouch verify --reexecute --compiled-artifact refund-window.lpxvca and vouch gate --compiled-artifact refund-window.lpxvca still require the consumer's exact external source and input, trust policy, authentication, and current tree/Meaning agreement. Native re-derives the Core IR and bytecode from that source before running the verified VM. The container, its hashes, inspection or validation output, and the VM result cannot skip or recreate any live authority transition.

Keep going

Use the reference for the exact binary and verifier contract, or return to Core IR to inspect resolved meaning before compilation.

Bytecode and Rust VM Reference · Compile to Topaz AOT · Native CLI