Runtime and Backends

How to reason about it

• Evaluation uses explicit outcomes, signals, and a trampoline instead of host unwind.
• Backend descriptors record interpreter kind, invocation protocol, artifact identity, supported axes, provenance, and resource profile.
• External admission is fail-closed. The joint receipt binds each of the 144 cases to executed Rust, LIL, and LIT product-runner artifacts, limits, observations, and replay.
• Vouch product capabilities are surface-specific: Native provides key/engine/source/input identity, policy tooling, issuance, authentication, re-execution, a local gate, inspection, and opt-in exact-source compiled VM agreement; npm provides the same identity tools, policy tooling, authentication, inspection, and corpus replay; WASM and Playground evaluate without exposing Vouch.
• Lispex Images are an official source representation implemented by one Rust product core shared by Native and WASM surfaces. After exact recovery, ordinary reader and evaluator semantics are unchanged; LIL or LIT can be selected only as the existing execution path for that recovered source.

Language requirement and backend support are different

The current language contract contains 205 required capability rows. Every one has the normative disposition profile-required. That says what a conforming implementation must eventually provide; it does not pretend every backend already provides it.

Source formatting is a Native tool

lispex fmt, fmt --check, and fmt --write are Native CLI capabilities. The VS Code/Open VSX extension delegates Format Document to that installed binary. npm, public WASM, and the Playground do not expose formatting, and the extension does not hide an unavailable Native executable with a fallback. Formatting changes source atmosphere only; it is not another evaluator, backend family, semantic profile, or evidence source.

Core IR, bytecode, and backend family are separate axes

Native can lower the complete normalized profile to canonical lispex.core-ir/v1, strictly validate those bytes, and show the resolved cells, captures, tail positions, requirements, source anchors, and identities. The core-ir build, validate, and inspect commands always report that execution did not run and authority is integrity-only.

Native can then compile strict Core IR to canonical lispex.bytecode/v1, verify the binary before state exists, and execute it in lispex-rust-vm/v1. The VM directly covers the current profile, including all 205 primitive rows and the 18 guest-calling rows. Tree remains the default Rust engine; --engine vm is explicit and never falls back.

Native macOS ARM64 can also send those exact verified bytes to the exact separately installed lispex-topaz-vm/v1 product. That route has its own Topaz reader, verifier, and explicit-control machine. Lispex admits only the fixed Topaz 5.11 product tuple through a closed request/result contract, full-u64 transition accounting, bounded execution, and five zero fallback counters. compare-vms records the two VM observations without making Topaz the default or a Vouch engine.

On macOS ARM64, Native can also generate a readable static Topaz control graph, compile it with only the exact installed Topaz 5.11 toolchain, and install a closed source-free AOT product. aot inspect and validate do not execute it; aot run does not compile it. Product, source map, artifact, executable, input, full-u64 resources, observations, and five zero fallback counters remain bound. This route is outside every Vouch constructor.

compare-routes joins these explicit routes without merging their identities. It derives source, Core IR, and bytecode once, checks that the AOT product matches them, then runs tree, Rust VM, Topaz VM, and AOT without retry. The no-clobber receipt compares semantic observations and only genuinely comparable resource fields; the tree's unavailable transition and frame counters remain unavailable. The receipt is local diagnostic evidence, not a new backend family or Vouch input.

Core IR is non-executing meaning material; verified bytecode is the VM's execution artifact. Rust tree and Rust VM share values and primitive leaves. The Topaz VM is structurally separate source but compiled by Topaz Rust Stage 0; it is tracked as a separate VM lineage rather than silently counted as a fourth established backend family. The historical family receipt remains Rust, LIL, and LIT. The older Meaning Graph commands and receipts also remain a distinct checked-subset path.

Compiled Vouch does not add a backend family. It admits only a dedicated container exactly re-derived from the consumer's pinned source, after authentication and before the current Rust VM comparison. A general bytecode file or report remains outside the authority path.

Selecting LIL or LIT is strict. An unsupported operation never falls back to Rust or to a convenient host procedure. This makes partial implementations useful for verification without disguising them as complete ones.

LIL implements the complete composed pair-accessor family from caar through cddddr. For example, (caddr x) means (car (cdr (cdr x))). The composition is evaluated inside LIL; it is not delegated to a host callback.

LIL also composes abs, square, the three sign/zero predicates, and typed boolean=? and symbol=? from its admitted numeric, comparison, and type operations. For example, (abs -3/2) returns 3/2, while (boolean=? #t #t #f) returns #f. Operand validation and errors remain the same as the Rust reference.

Under the current finite-real number profile, complex?, rational?, and real? all reduce to the total number? question. LIL also performs structural !=, eqv-based memv, structural-key assoc, and eqv-key assq/assv itself. For example, (memv 2 '(1 2 3)) returns the tail (2 3), while (assoc '(a b) '(((a b) . ok))) returns the matching pair.

LIL implements char<?, char<=?, char>?, char>=? by Unicode scalar value and string<?, string<=?, string>?, string>=? lexicographically by those scalars. Thus (char<? #\a #\b) and (string<? "a" "aa" "b") are true. This is deterministic code-point order, not locale collation, normalization, or case-insensitive comparison.

LIL now also handles everyday aggregate navigation and conversion itself. list-copy makes a fresh shallow spine, list-ref and nth select an item, and list-tail returns the shared tail. make-list defaults to 0, while make-string defaults to a space. string->vector and vector->string use character—not byte—indices, so (vector->string (string->vector "aλ🙂")) returns the same text. Converted vectors are fresh and mutable.

Unicode case operations use the explicitly recorded character/string host kernel. This covers char-ci<? and the other char-ci comparisons, char-lower-case?, char-upper-case?, char-whitespace?, char-upcase, char-downcase, char-foldcase, string-ci<? and the other string-ci order comparisons, string-upcase, string-downcase, and string-foldcase. Character conversion returns one simple-mapped character; string conversion uses the full mapping and may change length, as in (string-upcase "Straße") → "STRASSE". Case-insensitive ordering validates the whole chain before comparing. In the current profile, foldcase is a lowercase-based approximation—simple for characters and full for strings—not the complete Unicode CaseFolding table. None of these operations performs locale collation or normalization.

LIL also exposes the profile's everyday scalar number tools. floor, ceiling, and truncate move in their named direction; round resolves an exact halfway tie toward the even integer. They preserve the input's exactness, so (floor 1.8) is 1.0 while (floor 9/5) is 1. exact and inexact->exact recover the exact binary value of a finite inexact number—(exact 0.5) is 1/2; this is not decimal-text parsing. inexact and exact->inexact perform the reverse finite conversion. even? and odd? require an integer. min and max compare mixed exact and inexact values with the numeric tower's exact ordering, keep the first value on a tie, and return an inexact result when any input is inexact. Guest validation and the min/max folds live in LIL; rounding, exactness conversion, and parity use the explicitly recorded numeric host kernel, not a hidden fallback or an independent implementation.

The exact-integer family now follows the same rule without converting a mixed integer pair to binary64 first. quotient/remainder truncate toward zero; floor-quotient/floor-remainder round toward negative infinity. This is why (remainder -7 3) is -1, while (modulo -7 3) is 2. floor/ and truncate-quotient/truncate-remainder name the two truncated components explicitly, while floor/ and truncate/ return their quotient and remainder as two values: (call-with-values (lambda () (floor/ -7 3)) list) is (-3 2). gcd and lcm are non-negative variadic folds with identities 0 and 1. An inexact integer operand makes the final result inexact. expt permits only an exact-integer exponent; general transcendental exponentiation remains outside the profile. exact-integer-sqrt returns the floor root and its remainder as two exact values. Division and Euclidean folds are Lispex-written; only expt and exact-integer-sqrt use the declared advanced numeric host kernel.

The collection HOF surface is now complete in LIL. all? and any? short-circuit on strict booleans; map, filter, reduce, fold-left, and fold-right enforce one callback value; list, string, and vector for-each (for-each, string-for-each, and vector-for-each) discard any callback values and return zero values. string-map and vector-map preserve their collection kind. String and vector inputs are snapshotted before the first call. Every call travels through a guest continuation frame, so handlers, one-shot escapes, and resource accounting stay in the LIL machine rather than a host callback.

LIL's four output procedures—display, write, newline, and println—use the same canonical guest renderers and a bounded private effect sink. Explicit output and CLI auto-print remain in one ordered stdout stream, but root value projection is recorded separately so arbitrary display text is never parsed as a result. Output does not cross into host stdout, and a later error does not erase bytes already written.

The three deprecated compatibility names are implemented without widening the profile. % delegates to modulo; list-first and list-rest delegate to car and cdr. LIL records the same W330/W331 warning as Rust once per source call site, in first-occurrence order. Shadowed names do not warn, and a warning is retained if the canonical operation then fails. This ordered warning channel is separate from stdout, values, and the error diagnostic.

Runner admission fields

A common mistake

A packaging or generated-code target is not automatically a separate implementation or independent witness.

Current boundaries

• LIT interpreter, generated Rust, generated Python, and Web routes are host variants of one Topaz source. Their bounded four-host agreement does not extend the 144-case joint receipt or establish source independence.
• The admitted Topaz bytecode VM is Native macOS ARM64 only, explicit, exact-product-bound, and outside Vouch. Its comparison receipt establishes no whole-profile proof or automatic family-count change.

Keep going

Use this page while writing code. For a guided explanation, return to the syntax map or the corresponding manual.

Bytecode and Rust VM · Core IR Contract · Choosing a Runtime Surface