Run a rule with explicit data and finite limits. The same semantic request has the same outcome in every conforming product.
Scope
Lispex is a sandboxed rule language. Every program follows the same three guarantees.
The same semantic request produces the same outcome. A program receives outside information through supplied data. Finite limits end execution when the request cannot finish.
These are Lispex 2.0 rules. The product plans remain not run until a suitable 2.0 product and observation adapter are available.
Sandbox guarantees
1.1 Every program uses the sandbox contract
Every Lispex program has deterministic outcomes, no access to external resources, and finite execution limits. Every public product applies this contract.
A semantic request fixes the canonical program and input Datum. It also fixes the language, library, Unicode semantics, resource model, and finite limits. Compare completed evaluations using their canonical outcomes.
Preparation defines the resolved program. Identity domains distinguish that program from exact source bytes and engine artifact bytes.
Two different programs can compute the same value and use different resources. Determinism compares the same semantic request.
The examples use request.json as documentation notation. The CLI and value interchange chapters define the concrete product forms.
1.2 Repeat the same semantic request
Every conforming execution of the same semantic request produces the same outcome. This includes the first semantic failure and any resource stop.
The calling application gathers external facts before it invokes a rule. It supplies them through the entry boundary and presents the returned Datum.
The closed-bundle rule governs dependencies supplied during preparation.
1.3 Pass outside facts as data
A rule receives outside information through its input datum. Guest code cannot perform file, network, clock, random, or display operations. Host callbacks cannot cross the input boundary.
Every public entry point applies the finite-limit rule. Separate phase budgets govern preparation and evaluation. These limits end uncompleted requests with a defined failure.
The symbolic limits in these examples stand for finite values. The tariff and default numeric limits will be fixed after implementation and attack tests.
A profile chooses which programs and data it accepts. A product packages an implementation. An engine evaluates the accepted program.
Native, npm, and WASM have separate product plans. Every supported engine must meet the same request contract. A recorded observation identifies the product and engine that supplied it.
Source text, tokens, literals, and the normalized form of a Lispex rule.
Scope
Write a rule as UTF-8 source and supply its input separately. Preparation reads the source and resolves its names before evaluation begins.
UTF-8 source
Source text is the UTF-8 spelling supplied for a module. Decoded characters use Unicode scalar values. Source identity retains the original bytes. The resolved program has its separate program identity. Values and text defines the text values that a rule can return.
2.1 Preserve source spelling
Source reading applies the raw Unicode rule to names and string literals. The resulting spellings determine source identifiers and literal text.
Each module must satisfy the byte grammar before reading starts. Reject every malformed UTF-8 sequence. Decoding never inserts a replacement scalar. A byte order mark has no special treatment. A leading mark therefore fails the reader grammar. The same scalar is permitted inside a string, a quoted identifier, or a comment.
Tokens distinguish identifiers, literal data, and the delimiters of a form. Reading produces syntax for preparation. Evaluation uses the lexical binding selected during preparation. Quotation uses the decoded name as data. The complete grammar below fixes token boundaries and escapes.
2.3 Read one fixed syntax
The complete reader grammar below determines every source token and datum. Bare identifiers use ASCII characters. Vertical bars admit every Unicode scalar sequence through literal characters or escapes. Identifiers compare by their decoded scalar sequence. Spelling escapes do not create a different name. Only the listed separators end tokens. Block comments nest. A datum comment reads and discards the next datum. Discarded data must satisfy the reader grammar but undergo no normalization. Reader directives and unlisted token prefixes are rejected.
Explicit character sets avoid host locale and Unicode classification differences. Quoted names retain arbitrary text without adding invisible token boundaries. Nested comments remain readable while discarded syntax receives the same finite reading checks.
Use the token and literal boundaries in the reader grammar. A comment marker is recognized outside String, BarredIdentifier, and Character tokens. A semicolon inside an admitted literal remains part of that literal.
The indicated scalar value or inclusive scalar range
Other quoted terminals
Literal scalar sequences
end-of-input
A zero width test for the end of the decoded module
& and !
Positive and negative lookahead without consumption
-
Exclude the right operand from the language on the left
Use the longest complete atomic token. A token beginning with a decimal digit is numeric. A sign or dot followed by decimal digits also starts a numeric candidate. Radix prefixes commit to their numeric grammar. A malformed candidate cannot fall back to an identifier. The standalone dot is permitted only in a nonempty list before its single tail datum. Parentheses pair exactly. Brackets and braces have no alternate list meaning.
Input form
Decoded meaning or restriction
\n, \r, \t in a string
Line feed, carriage return, tab
\u{...}
The hexadecimal scalar value
A scalar escape in the surrogate range or above U+10FFFF
Reader failure
Literal control scalars in strings or barred identifiers
Use an escape instead
||
The empty identifier name
#\space, #\newline, #\tab, #\return, #\null
U+0020, U+000A, U+0009, U+000D, U+0000
A direct character scalar after #\
Exactly one scalar followed by a token boundary
#b, #o, #d, #x
Lowercase radix prefixes with a following optional sign
A numeric rational
An unsigned nonzero denominator in the selected radix
Decimal leading zeroes and hexadecimal letter case
Preserve the same exact numeric value
#e, #i, +inf.0, -inf.0, +nan.0, -nan.0, +i, -i
Reader failure
Complex tokens that begin as numeric candidates
Reader failure
#!, #lang, a shebang, datum labels, backquote, comma
Reader failure outside literal text or comments
A leading or repeated byte order mark
Reader failure
Other whitespace and a lone carriage return
Reader failure outside literal text or comments
An escaped identifier and a literal identifier with the same decoded scalar sequence name the same binding. A barred numeric spelling is an identifier. It is not a number. Comment and radix prefixes are ordinary text where the literal grammar admits their characters. Block comment delimiters nest even when their surrounding comment text contains quote characters. A datum comment skips trivia before reading its one discarded datum. This includes nested datum comments. An unfinished comment, escape, string, list, or quoted datum fails reading. Syntax inside a discarded datum must still be complete.
The quote prefix becomes the ordinary quote form during normalization. Lists, pairs, vectors, and bytevectors retain their element order. Decimal fractions and exponents reduce to the exact values defined by Exact numbers. The reader creates no cyclic datum.
The reader checks an escape when its final scalar is read. It checks literal control scalars when they are read. Atomic token grammar and numeric value checks occur at the completed token. A bytevector element receives its integer and octet range checks before the next element is read. A malformed numeric token fails before its value checks. A zero denominator fails before a bytevector range check. If reading reaches source end, its end test reserves one read-step.
Literals and surface forms
A literal denotes an immutable value. Quoted names are symbols. Quoted lists are data. Decimal spelling denotes an exact number. Exact numbers defines its arithmetic and rounding contracts. Datum defines the data allowed at the rule boundary.
Strings and quoted identifiers use only the listed escapes. A scalar escape must name a Unicode scalar value. Every numeric token denotes an exact integer or a reduced rational. A decimal exponent scales by an exact power of ten. A rational denominator must be nonzero. Radix prefixes select the digit alphabet in the grammar. Numeric candidates that fail that grammar are errors. They cannot become identifiers. Bytevector elements must denote exact integers from 0 through 255.
One lexical interpretation prevents malformed numbers from becoming accidental names. Exact literals give every product the same data before arithmetic or admission begins.
Normalization follows the canonical source construction. That table defines the admitted rewrites and preserved semantic nodes. Preparation resolves their references to lexical bindings. A normalizer preserves quoted data and follows the evaluation rules. Source maps retain source positions for display.
2.7 Preserve meaning through normalization
Normalization preserves lexical bindings, literal values, evaluation order, and the first observable failure. A generated binding cannot capture a source reference.
An invalid source cannot provide a valid program identity. Keeping the failure with its source preserves a useful diagnostic without inventing an evaluation.
Source decoding, reading, and normalization use the preparation account defined by Resources. The finite-limit rule applies before any entry evaluation.
Preparation follows the complete reading order. Normalization visits forms in source order. It checks a binding group when that traversal reaches the group. The shallow checks finish before any initializer or body in that group is normalized. Each required check reserves its event before inspecting syntax. A refused reservation stops before that inspection. An observed error stops before any later reservation. The event and check tables below fix this order. The reservation axis rule applies within each event.
A complete group check gives each binding one static meaning. Local prechecks preserve the order of unrelated forms. Reservations bound the work needed to discover an error without moving a later event before that error.
Event
Next operation
Order
prepare.decode-step
Decode the next UTF-8 scalar or confirm source end
Complete the module before reading
prepare.read-step
Inspect the next decoded scalar or confirm source end
Left to right with each scalar inspected once
prepare.read-enter
Enter a list, vector, bytevector, quote, block comment, or datum comment
After its opening marker and before its contents
prepare.read-node
Validate and construct a completed datum
Children before their containing datum
prepare.normalize-node
Inspect the next source form
Source order with children after their parent checks
prepare.binding-check
Inspect the group envelope or the next member check
Before that inspection
prepare.binding-publish
Record a checked lexical binding
Member order after all group checks
Reading completes before normalization starts. Reader lookahead reuses scalars already inspected and adds no second read event. A nested marker selects its enter event before any child event. A closing marker is read before its completed datum event. A block comment has enter events and scalar events but no datum node. A completed atomic token reserves its node event before token and numeric value checks. Its bytevector element checks finish before reading the next element. Datum comments retain every event of their discarded datum. Each event reserves all required axes before its effect. Reader enter events include required frame capacity. These events follow the grammar rather than implementation scanner loops. A comment or discarded datum still requires its reading events. The resource model names the requirements for each event. Its coefficients and finite defaults follow the cost model freeze.
Check
Failure selection
Group envelope
Reject a malformed group before visiting a member
Member shape
Reject the first malformed binding or parameter
Identifier
Reject a binding position that is not an identifier
Duplicate
Reject a repeated name in the same binding scope
Recursive lambda head
Require the lambda head where recursive bindings require it
Run these member checks from left to right. Skip the lambda check for a nonrecursive binding. Stop at the first failed check. Parameter lists include their rest parameter in the same duplicate check. A parallel let, named let, letrec, or recursive definition group checks all members before descending. Each let* binding forms its own nested group. Its initializer is normalized before the next binding group.
Publishing a binding records its identity. The lexical scope rules determine where that binding is visible. A parallel let initializer and a named let initializer retain their enclosing scope. All checks finish during preparation. They execute no guest initializer.
2.12 Read the complete module before normalization
For one module, preparation decodes UTF-8 before reading syntax. Reading completes before normalization starts. A reader failure takes precedence over a normalization failure in that module. Normalization checks source forms in their written order.
A fixed phase order makes the first failure reproducible. An earlier form with invalid meaning cannot hide a later reader failure in an unread part of the module.
Build immutable data, compare values, and preserve exact Unicode text across rule boundaries.
Scope
This chapter defines Datum, scalar values, portable data, and equality. It also defines raw Unicode text and the constraints on mapping host records into data. Exact numbers defines numeric meaning. Procedures defines executable values and entry calls.
Datum
A Datum is a finite portable value. A scalar is a Boolean, an exact number, a character, a symbol, or the empty list. Aggregate Datum values are pairs, strings, vectors, and bytevectors. Every element of an aggregate Datum is itself a Datum. A list is a chain of pairs ending in the empty list.
Portable data has no cycles or executable components. A pair can hold another Datum in either position. A vector holds an ordered sequence of Datum values. A bytevector holds an ordered sequence of bytes. Strings and symbols preserve the Unicode scalar sequences described below.
Procedures defines internal callable values. Placing one inside a pair or vector does not make it portable data. The value interchange contract supplies the concrete encoding for admitted data.
3.1 Keep executable values inside evaluation
A Datum contains only the scalar and aggregate data defined here. Every nested element must also be Datum. A procedure cannot cross the input or result boundary, even inside an aggregate.
A value boundary can be reproduced without carrying code, storage addresses, or host capabilities. Checking nested elements closes the same boundary for a list or vector as for a single value.
Constructing a new value can reuse unchanged data internally. That storage choice does not grant a mutation operation or an observable address. Logical work and allocation remain governed by the resource contract.
3.2 Transform data without changing it
Values cannot be changed after construction. No public aggregate mutation operation is available. A transformation returns a value without changing its input values. Internal sharing follows the event-preservation rule.
Immutable input and result data keep separate evaluations independent. A product can share storage while preserving the language meaning and the resource contract.
Use eq? and eqv? for scalars. Use equal? for portable data, including aggregate data. None of these operations compares storage addresses or procedure identity.
Scalar equality follows the value of a Boolean, exact number, character, symbol, or empty list. String content is aggregate data even though a string may look like one item in source.
3.3 Compare only scalars with eq? and eqv?
The operands of eq? and eqv? must be scalars. These procedures compare scalar values. An aggregate or procedure operand produces a domain failure even when both operands refer to the same internal value.
Allocation and compiler choices must not change a comparison. Restricting these procedures to scalar values removes observable aggregate and procedure addresses.
3.4 Validate data before returning structural equality
The operands of equal? must be portable data. It compares scalar values and corresponding aggregate contents. Before it returns a Boolean, both operands must be valid Datum values throughout. A procedure inside either operand produces a domain failure. Shared storage cannot bypass that check.
A procedure must not become comparable by wrapping it in a list or sharing that list. Domain validation also prevents a short circuit from hiding an invalid component.
The equal? procedure validates the complete left operand before starting validation of the right operand. A failure ends validation at the first invalid component. Validation follows depth-first order with each pair car before its cdr and vector elements in ascending index order. After both operands pass, structural comparison follows that component order. Strings compare scalar positions from first to last and bytevectors compare byte positions from first to last.
Two operands can contain different invalid components. Fixing validation and traversal order gives those requests one first failure. The same order also constrains optimizations and the placement of logical resource events.
Equality validation follows a fixed operand and component order.
A character is one Unicode scalar value. A string is a finite sequence of those scalar values. A symbol preserves an exact scalar sequence and distinguishes case. Visually similar text can contain different sequences.
The Unicode semantics version belongs to the fixed language meaning. A host locale, operating system, or compiler update cannot select a different transformation. Explicit normalization and case operations require the exact tables and algorithms named by that contract.
3.6 Preserve Unicode scalar sequences
Strings, characters, and symbols preserve their raw Unicode scalar values. Reading or comparing text performs no implicit normalization or case folding. Text transformations use the specification-owned Unicode version and exact operation. Host locale cannot change their meaning.
Unrequested normalization can merge distinct keys or names. Fixing Unicode operations in the language contract keeps host text libraries from choosing a different meaning.
Unicode operations use Unicode 17.0.0 and the operation tables below. Products use these archived data and algorithms. Host locale, operating system, compiler, and text library defaults cannot select another meaning.
The following table fixes the Unicode property operations. Each accepts one character.
Procedure
Result
char-alphabetic?
The Alphabetic Boolean
char-numeric?
True exactly for General_Category = Nd
char-whitespace?
The White_Space Boolean
char-upper-case?
The Uppercase Boolean
char-lower-case?
The Lowercase Boolean
digit-value
The exact decimal digit value from zero through nine for Nd, otherwise #f
The complete Unicode transformation repertoire is fixed below. Its signatures belong to the public procedure catalog.
Composition exclusions and normalization properties
Every Unicode scalar is accepted by the appropriate character or string operation. Unassigned, private-use, and noncharacter scalars use the frozen defaults. A later Unicode assignment does not change those defaults. New data, errata, or tailoring require a new language semantics revision. The source grammar defines its own whitespace separately from char-whitespace?.
The call first completes expression evaluation and checks arity. It then checks argument types from left to right. Unicode work starts only after those checks succeed. Type and arity failures are language conditions. Resource exhaustion follows the reservation order. A procedure returns its complete result or the first failure.
The resource event catalog defines these event names, reservation points, and canonical sites. This table selects the events used by each operation.
Work
Resource events
Property queries and simple case mapping
text-scalar-scanunicode-map
Full string mapping
text-scalar-scanunicode-mapdatum-allocate
Normalization
text-scalar-scanunicode-normalizedatum-allocate
Folded comparison
Folding events followed by compare-scalar
Coefficients, allocation units, limits, and physical envelopes remain with the cost model freeze.
A scalar property query or simple case mapping performs one scalar scan and one unicode-map. Its map extent is one. For digit-value, that map reserves the complete exact integer representation and value slot before creating the digit result. A nondecimal input returns #f within the same event. Neither result adds a datum-allocate event. Booleans and characters retain their declared scalar representation requirements.
A completed string mapping or normalization reserves one datum-allocate before materializing its immutable result. Its extent is m, the actual number of output scalars. The complete requirements include the string header, value slot, and space for up to 4 times m UTF-8 octets. They also include encoding work and any temporary storage used for materialization. The extent remains m when input length, decomposition capacity, or UTF-8 octet length differs. Extent zero still reserves an empty string result. Refusal publishes no partial string and refunds no earlier charge.
The same text must produce the same classification and transformation on every product. A fixed repertoire also subjects each operation to the same finite resource contract.
Complete storage and work are assigned to the declared Unicode events. Original scalar counts, generated scalar counts, and typed result sites preserve reservation order across physical representations.
The four normalization procedures apply the named Unicode 17.0.0 form. NFC, NFD, NFKC, and NFKD are distinct explicit choices. Reading, equality, case conversion, and case folding do not normalize text implicitly.
Each procedure takes exactly one string and returns a string.
Procedure
Unicode 17.0.0 result
string-normalize-nfc
NFC(input)
string-normalize-nfd
NFD(input)
string-normalize-nfkc
NFKC(input)
string-normalize-nfkd
NFKD(input)
Chapter 3 sections 3.11 and 3.12 define the algorithms. UAX #15 revision 57 fixes the normalization conformance requirements. They include canonical ordering, composition exclusions, and Hangul decomposition and composition.
The empty string returns the empty string. A normalization procedure neither changes case nor inserts Stream-Safe separator characters. Long combining sequences keep their specified result and consume the declared resource events. Exhaustion stops the operation before a partial result becomes visible.
After the complete original scalar scan and required end, each normalization call performs one unicode-normalize at argument(0). Its extent is the original scalar count n. D is 4 for NFC and NFD, and 18 for NFKC and NFKD. Its complete requirements cover two scalar buffers, each with capacity D times n, and 256 canonical-combining-class counters. Bound arithmetic, decomposition lookup, ordering, composition, and all intermediate storage belong to this reservation. It succeeds before transformation or scratch materialization starts.
Fully decompose the input under the selected form. Use stable counting order within each maximal nonstarter run. A scalar with combining class zero separates runs. Equal combining classes retain their original order. Compose NFC and NFKC in place under the Unicode blocking, exclusion, and Hangul rules. With decomposed length L and r runs of at least two nonstarters, ordering work has the structural bound O(1 + L + 256r). L is at most D times n and r is at most floor(L / 2). Reserve from n, D, and these upper bounds before decomposition; discovering actual L or r is transformation work. The selected model covers fixed workspace setup and every complete lookup, counter pass, scalar visit, and movement, including their coefficients. It cannot hide a recursive walk, comparison sort, or quadratic insertion pass outside the reservation.
The empty string still has one unicode-normalize with extent zero, followed by one datum-allocate with extent zero. The fixed workspace and empty-result requirements remain part of those reservations.
A completed string mapping or normalization reserves one datum-allocate before materializing its immutable result. Its extent is m, the actual number of output scalars. The complete requirements include the string header, value slot, and space for up to 4 times m UTF-8 octets. They also include encoding work and any temporary storage used for materialization. The extent remains m when input length, decomposition capacity, or UTF-8 octet length differs. Extent zero still reserves an empty string result. Refusal publishes no partial string and refunds no earlier charge.
Canonical and compatibility equivalence answer different questions. Explicit forms preserve the original scalar value until the program requests a transformation.
Complete storage and work are assigned to the declared Unicode events. Original scalar counts, generated scalar counts, and typed result sites preserve reservation order across physical representations.
Character case operations use simple mappings. String case operations use full mappings and the specified original-input contexts. Folding and folded comparisons use the fixed non-Turkic mappings. These operations perform no normalization or locale tailoring.
The unary case operations accept one value of the indicated type.
Procedure
Input and result
Mapping
char-upcase
Character to character
Simple_Uppercase_Mapping
char-downcase
Character to character
Simple_Lowercase_Mapping
char-foldcase
Character to character
CaseFolding.txt statuses C and S
string-upcase
String to string
Full Uppercase_Mapping
string-downcase
String to string
Full Lowercase_Mapping
string-foldcase
String to string
CaseFolding.txt statuses C and F
Simple mappings always produce one scalar. A missing mapping returns the input scalar. A product must not truncate a full mapping to implement a character operation.
String case conversion uses Default Case Conversion. It combines UnicodeData.txt with SpecialCasing.txt. It applies unconditional mappings and language-independent conditions, including Final_Sigma. Every context is tested against the original string. Language-tagged mappings are excluded. Case folding excludes status T and uses one pass over the original scalars. The empty string maps to itself.
Each comparison accepts at least two arguments of its own type. After type validation, it folds all arguments from left to right. It then compares adjacent pairs from left to right. For each folded string pair, comparison starts at index zero. At each position, inspect the left sequence and then the right. Decide whether to stop only after both reads. Stop that pair at unequal scalars or an end. The result is true exactly when every pair satisfies the named relation. The first false pair ends comparison. Scalar order is numeric code point order. String order is lexicographic scalar order with the shorter equal prefix first. Comparison does not apply normalization or locale collation.
Let n be the number of original input scalars. Full string mapping first scans all n scalars and the required end. It then maps the original scalars in ascending index order. Each unicode-map has extent n. The first map reserves one scratch buffer with capacity D times n scalars. D is 3 for uppercase, 2 for lowercase, and 3 for folding. That reservation succeeds before either scratch storage or the first mapped scalar is created. Later maps reuse that capacity. They reserve their own mapping work without another scratch allocation. An empty input performs its end scan and result allocation, with no map or mapping scratch reservation.
The map requirement includes exact bound calculation, table lookup, expansion, and retained scalar storage. These counts are mathematical integers. A host word width cannot add a domain limit or change the first failure.
Lowercasing keeps a preceding-cased state while visiting the original scalars. Case_Ignorable scalars leave that state unchanged, including a scalar that is also Cased. Every other original scalar sets the state to its Cased property. A U+03A3 map tests the state before that scalar updates it. If the state is true, inspect the original suffix in ascending index order. Skip Case_Ignorable before testing Cased. The first remaining scalar, or the required end, determines whether a following cased scalar exists. Final_Sigma selects U+03C2 exactly when the preceding state is true and no such following cased scalar exists. Otherwise U+03A3 maps to U+03C3.
The current map includes the preceding-state work and every required suffix visit in its complete requirements. At most n original scalars are visited for that map's context work. These visits create no additional text-scalar-scan events. Earlier mapped results never supply context.
All argument domain checks finish before folding or replacing any retained argument. Fold each argument in ascending argument order. Retain its completed folded value in the same logical operand-sequence position already reserved for that call. A character replacement belongs to its unicode-map. A string replacement belongs to its completed result allocation. This replacement changes no caller binding or immutable input value. It adds no argument-store or traversal-state event and requires no separate descriptor sequence. Every folded value remains available until comparison finishes or the call fails. Repeated references to the same input still perform each argument's full folding schedule and result reservation.
For a unary string transformation, the result allocation site is result(0). For a folded string comparison, the folded result of argument i is allocated at result(i) of the invoking comparison call. The site role is datum-allocate. All scans and maps continue to select the original argument(i) and its scalar positions.
After all folding and retention, each folded character pair performs one compare-scalar. For strings, each visited position performs one compare-scalar. Reserve before reading the left scalar or end, then the right scalar or end at that same position. Both reads belong to that event, including when the left sequence has ended. Only after both reads does the pair stop at unequal scalars or an end. No additional text-scalar-scan accompanies these folded reads. String comparison sites use field(compare), argument(i), scalar(j), where i is the left argument of the adjacent pair and j starts at zero for each pair. Character comparison selects field(compare), argument(i). The first false pair ends comparison after every argument has already been folded.
Full mappings preserve expansions needed for string matching. Simple character mappings preserve the character result domain. Fixed context and folding rules reproduce these choices without host locale state.
Complete storage and work are assigned to the declared Unicode events. Original scalar counts, generated scalar counts, and typed result sites preserve reservation order across physical representations.
A host record is a collection of named fields supplied by the calling application. A profile can map it to an immutable association list. An association list is an ordinary list of pairs whose first component is a key and whose second component is the associated value.
The example below explicitly selects string keys and association-list mapping in its documentation request. It does not introduce a separate guest map kind or establish a public codec. The profiles chapter owns the concrete admission and interchange forms.
3.10 Map admitted records in canonical key order
Apply the host record conversion rule when a caller selects record admission. That rule defines exact key preservation, duplicate checks, and canonical ordering. The resulting value is ordinary association data under the Datum definition here. The record input contract fixes the separate host account and later evaluator decode.
A record must produce the same data regardless of insertion order or host map storage. Duplicate rejection prevents the host from silently choosing one value for a repeated key.
Calculate with exact integers, rational numbers, and decimals. Choose scale and rounding explicitly and keep numeric work within finite limits.
Scope
This chapter defines exact numeric values, division, scale, and rounding. It also describes the resource obligations of growing numeric values. Source and normalization owns literal syntax. Values and text owns scalar and structural equality.
Number values
An exact integer has no fractional part. An exact rational denotes a quotient of integers with a nonzero denominator. A reduced rational has a positive denominator and no common factor between its numerator and denominator.
An exact decimal is source notation for an exact integer or reduced rational. The spelling 0.1 denotes one tenth. A decimal point does not request an inexact number. Trailing decimal zeros do not create an observable scale on the numeric value.
Numeric values are immutable scalars. The notation used in these examples describes values and does not specify codec bytes or product output formatting.
4.1 Preserve exact numeric meaning
Integers, rational numbers, and decimal literals denote exact values. A successful arithmetic operation returns its exact mathematical result. It does not introduce binary floating point or perform implicit rounding.
Rules can compare amounts and ratios without depending on a platform math library or a hidden precision setting. A decimal literal expresses the stated value exactly.
A rational value is reduced to coprime numerator and denominator with a positive denominator. A negative sign belongs to the numerator. Equivalent fractions denote the same exact mathematical value.
A reduced form gives each nonintegral fraction one mathematical description. It prevents unreduced source spellings from becoming different numeric values.
Numeric equality and ordering compare exact mathematical values. A decimal spelling and a rational spelling for the same value compare numerically equal. Ordering must not round either operand through a host numeric format.
A decimal literal denotes an exact integer or reduced rational. Its source scale is not observable as numeric state. Mixed arithmetic uses these exact values. The scalar procedures eq? and eqv? compare their mathematical values across numeric spellings. A decimal scale needed for rounding must be supplied explicitly.
One mathematical value should not acquire a hidden scale from its source spelling. Using integer and reduced-rational values keeps decimal notation exact while making a rounding policy a separate explicit choice.
The language has no inexact numeric value kind. Inexact literals, floating point inputs, and requests for implicit inexact conversion must be rejected. A product cannot approximate a value and report a successful exact result.
Exact division can produce a rational that has no finite decimal expansion. That value remains exact. A caller that needs a finite decimal scale must request an explicit rounding operation.
A zero divisor is a language domain failure. It does not produce infinity, an inexact value, or a successful result. Conditions defines how a rule handles ordinary language failures.
4.6 Keep a quotient exact and reject zero divisors
Division by a nonzero exact number preserves the exact quotient. A quotient need not have a finite decimal expansion. Division by zero produces domain.division-by-zero and returns no result datum.
A repeating decimal is still an exact rational. Keeping that value avoids a hidden precision choice. Zero division has a defined failure cause instead of an inexact special value.
A decimal scale specifies the place at which a value is rounded. Scale one uses tenths and scale two uses hundredths. Scale zero uses integers. Negative scales use decimal multiples. The exact numeric value does not preserve display scale.
Quantize receives its scale and mode explicitly. The named integer procedures fix their direction and scale zero. The public catalog lists their complete procedure contracts.
4.7 Choose scale and rounding explicitly
An operation that rounds an exact number must identify its decimal scale and rounding mode in the program or input. Quantize takes both as arguments. The names floor, ceiling, and truncate identify fixed scale-zero policies. Ordinary exact arithmetic does not apply rounding implicitly. Host settings cannot choose the scale or mode.
Different scales and rounding modes answer different questions about the same amount. Making the policy explicit lets the same rule reproduce that choice.
Choose tenths and hundredths in ordinary rule code
The public rounding procedures use exact arithmetic. Every exact integer is an admitted scale. A scale has no host word bound. Finite evaluation limits govern the required work and storage.
Procedure form
Argument domain
Result
(quantize x scale mode)
Exact number, exact integer, and a listed mode symbol
Selected exact grid value
(floor x)
One exact number
Greatest integer no greater than the input
(ceiling x)
One exact number
Least integer no less than the input
(truncate x)
One exact number
Integer part toward zero
Quantize requires all its arguments. The unary procedures fix scale zero and select the mode named by the procedure. They are separate procedures with the stated unary signatures.
Name
Exact definition
q
10^(-scale)
y
x / q
n
Integer selected from y by the mode rule
Result
n * q
Positive scales select decimal fractions. Negative scales select decimal multiples. An integral result is an integer. Other results are reduced rationals with positive denominators. Zero is the integer zero. The result retains neither display scale nor a zero sign.
An integer scale describes the grid independently of host precision. Exact results preserve the adopted numeric value model. Named integer procedures express their fixed policy without a hidden default.
Mode symbols match the exact spellings below. Case folding and symbol aliases do not apply. An integral scaled value selects itself in every mode.
Name
Definition for a nonintegral scaled value
a
Greatest integer less than y
b
a + 1
t
y - a
Nearest without a tie
Select a when t < 1/2 and b when t > 1/2
Mode symbol
Selected integer
Tie at t = 1/2
floor
a
a
ceiling
b
b
truncate
a for positive y and b for negative y
Same sign rule
away-from-zero
b for positive y and a for negative y
Same sign rule
half-even
Nearest without a tie
The even integer among a and b
half-away-from-zero
Nearest without a tie
b for positive y and a for negative y
half-toward-zero
Nearest without a tie
a for positive y and b for negative y
exact
domain.numeric with rounding-required
domain.numeric with rounding-required
Distance and tie tests use exact arithmetic. The exact mode succeeds only when the input already lies on the grid. A host rounding mode, locale, or numeric library cannot change this selection.
Directed modes serve explicit lower and upper bounds. Nearest modes state their tie policy for both signs. The exact mode lets a rule require lossless quantization.
Operator and operand evaluation follows the call order. An operand failure ends that evaluation before procedure checks. After operand evaluation, check arity before checking argument domains. Quantize checks the number, scale, and mode in that order. Unary rounding checks its single exact number.
Check
Failure
Quantize receives exactly three arguments
runtime.arity
A unary rounding procedure receives exactly one argument
runtime.arity
The number is exact numeric data
domain.type with expected type number
The scale is an exact integer
domain.type with expected type integer
The mode is one listed symbol
domain.type for a non-symbol. domain.numeric with invalid-rounding-mode for an unlisted symbol
The exact mode input lies on the grid
domain.numeric with rounding-required
After arity succeeds, the operation follows the event order below. Argument checks repeat in argument order. Unary procedures have no synthetic scale or mode argument checks.
Event
Work governed by the event
argument-check
Validate the current argument domain
decimal-scale
Form the exact grid step from the scale
exact-divide
Form the scaled value and adjacent integer candidates
rounding-select
Select an integer or report rounding-required
rational-reduce
Form and reduce the exact result
datum-allocate
Reserve and create the result datum
Each event applies reservation before effect. It uses the fixed resource axis order. The first domain failure or refused reservation ends the call. Later events do not run. A refusal returns no rounded substitute or partial datum. Successful grid points and zero still follow the declared event stages. Optimization preserves their semantic charges and first failure.
These names identify operation families. The resource event catalog defines their reservation points and canonical sites. The selected resource model supplies their requirement vectors. Resource coefficients and limits remain under the cost model freeze decision.
Validation order fixes which invalid argument a program observes. Reserving numeric work before its effect keeps enormous scales within finite execution. A failed call cannot silently replace the requested policy with an approximation.
Reject invalid rounding calls in the declared order
Exactness does not promise unlimited computation. Operand sizes, intermediate products, rational reduction, division, comparison, and encoding all require bounded work. The resource contract governs logical allocation and reservations.
Host integer width is not a numeric rule. A product must either support an admitted exact calculation under its fixed semantic limits or report the specified failure. It cannot wrap a value, saturate it, or substitute a rounded approximation.
4.11 Bound numeric work without changing its meaning
Exact numeric operations apply work limits, logical allocation, and the terminal-failure rule. Numeric growth and intermediate values contribute their declared events. A failed numeric operation returns no wrapped, truncated, or rounded result. Host word size cannot change an admitted calculation.
Exact arithmetic can grow beyond the size of its source literals. Charging that growth preserves finite execution while keeping numeric meaning independent of machine word width.
Evaluation order, lexical scope, immutable bindings, and recursion.
Scope
This chapter covers evaluation order, lexical scope, and immutable bindings. It also covers duplicate definitions, recursive procedures, and tail calls.
Evaluation order
Evaluation computes values by following the program. A first failure ends the current evaluation path unless a permitted guard handles it. Each later expression stays unevaluated until the preceding expression has completed.
The cases use symbolic finite limits large enough to reach the stated language result. Resource event order is defined in Resources.
5.1 Evaluate the operator and arguments in order
An application evaluates its operator first. It then evaluates every argument from left to right. After those evaluations complete, it checks that the operator is a procedure and that the argument count is accepted. The called operation checks its argument domains in the specified order. The first failure takes precedence over every later check.
An if form has one test and two written branches. A cond form ends with one nonempty else clause. The conditional grammar fixes these source forms. A conditional evaluates its test before the selected branch. Only #f is false in a test. Every other value is true, including the empty list and exact zero. A conditional does not evaluate an unselected branch. The selected branch forwards its complete internal result sequence. An author may explicitly return zero values with values. A missing branch never supplies an implicit result. The and and or forms evaluate operands from left to right and stop when the result is determined. A begin body evaluates its expressions in order and returns the values of its final expression.
Selecting a branch must also select which failures and resource events can occur. Evaluating unused expressions would change the meaning of the rule.
Only #f is false.
Written alternatives make the result policy explicit for every conditional path. They preserve internal multiple values without inventing an unmatched result.
Cond tests run once in source order. Each test requires one value. Only #f selects the next clause. A selected test-only clause returns that test value. A selected body returns the values of its final expression. An arrow clause evaluates its recipient once and calls it with the saved test value. The recipient requires one procedure value and follows the ordinary call checks. No later clause runs after a match or a failure. The final else body runs when every test is false. Selected branches may explicitly return zero, one, or many internal values. The single-value context rule and entry result rule still apply at their boundaries.
The else and arrow markers use the binding-independent clause interpretation from Conditions. Preparation rejects malformed conditional forms under the existing source order. The reached form is checked before its child expressions. Cond clause shape checks follow source order. The final else requirement is checked after those clause shape checks. A reservation failure keeps its existing precedence.
Malformed form
Phase
Code
Data
If without exactly three operands
normalize
syntax.form
form = if and reason = expected-shape
Cond without a final else clause
normalize
syntax.form
form = cond and reason = expected-shape
Empty or improper cond clause
normalize
syntax.form
form = cond and reason = clause-shape
Else before another cond clause
normalize
syntax.form
form = cond and reason = else-position
Cond else without an expression
normalize
syntax.form
form = cond and reason = else-body
Cond arrow without exactly one recipient
normalize
syntax.form
form = cond and reason = arrow-shape
These are existing fields and reasons from the diagnostic catalog. An empty cond has no final else and fails with expected-shape. Neither source normalization nor prepared validation synthesizes an alternative. The resource event catalog supplies the existing conditional schedule.
The imported expression is a reader datum admitted as an expression. The imported clause uses the guard grammar. A clause has a test and body, a test alone, a test and recipient, or an else body. The cond form requires the else clause exactly once and last. Its body must be nonempty. Every preceding clause is a test clause. The if form requires both branches. Keywords compare decoded identifier values under the reader grammar. These restrictions concern ordinary conditionals. Guard keeps its own optional else and unmatched propagation rule.
Scope and bindings
A binding associates a name with one value. Its scope is the region of source where that association is visible. Lexical scope follows the written nesting of bindings.
A procedure retains access to the bindings visible where it is defined. A call introduces fresh argument bindings. Procedures defines parameter counts and returned values.
5.3 Resolve a name in its lexical scope
A name refers to the nearest enclosing lexical binding with that name. A nested scope may introduce a new binding with the same spelling. A procedure uses its captured lexical bindings when it is called. A caller cannot change those bindings by declaring a name in its own scope.
The let form evaluates its initializers from left to right in the enclosing scope. It introduces the new bindings for the body after all initializers succeed. The let form evaluates each initializer with the preceding new bindings in scope. Each let binding introduces a nested scope. A later binding with the same name shadows the earlier binding. Each initializer follows the single-value context rule.
A binding keeps its value for its lifetime. The language does not provide set! to replace that value. Passing a value to another procedure or capturing it in a closure does not grant an operation that changes the binding.
A definition introduces a new binding in its definition scope. Defining the same name again in that scope is a static error. Repeated names in one parallel binding group are also rejected. An enclosing binding and a nested binding remain separate definitions.
A recursive procedure can call itself. Mutually recursive procedures can call one another. Recursion creates new calls with new argument bindings. It does not assign new values to earlier bindings.
5.7 Tie recursive names only to procedures
Each initializer in letrec must be a lambda expression. The procedure bodies can refer to every name in the recursive group. The bindings are established before any of those bodies is called. Recursive internal definitions follow the same restriction. Calculate other values with let or let*.
A named let evaluates its initializer expressions from left to right in the enclosing scope. The new loop binding is visible in the loop body. It introduces a recursive procedure for that body and makes an initial call with the initializer values. Each recursive call creates new parameter bindings. The loop body can call the named procedure without replacing an earlier binding.
5.9 Transfer a tail result without retaining a caller frame
The final expression of a procedure body is in tail position. A selected conditional branch and the final expression of a begin or binding body inherit tail position from the enclosing expression. A guard body is not in tail position. The final expression of a selected handler clause body inherits tail position from the guard expression. A tail call passes its result directly to the pending caller. Its frame capacity follows the semantic-frame rule. Its work and logical allocation use those resource accounts.
The implicit target call of apply inherits the tail position of that apply call. The consumer call of call-with-values inherits the tail position of that call-with-values call. In tail position, the implicit call takes over the native call's frame and pending return. The replaced native call emits no call-return. The producer call and every other library callback are outside tail position.
The number of completed tail steps must not become a hidden host stack limit. A loop expressed through apply has the same guarantee. Charging each step still guarantees finite execution.
An active guard must keep protecting its body. The enclosing call keeps its pending return if that body fails. Handler tail transfer is possible after guard deactivation.
Complete many tail calls with a fixed frame budget
Procedure arguments, application, internal values, and the rule entry boundary.
Scope
This chapter covers procedure parameters and application. It also covers internal multiple values and the single input and result at a rule entry.
Fixed and rest parameters
A procedure is an internal callable value. A lambda expression creates a procedure whose body uses its lexical bindings. An argument is a value supplied to a call. A parameter is the binding that receives an argument.
A procedure may be passed to another procedure inside a rule. It is excluded from Datum, the portable data allowed at the external boundary. Evaluation and bindings defines lexical scope and immutable bindings.
6.1 Match fixed parameters to arguments
A procedure with fixed parameters accepts exactly one argument for each parameter. It binds the argument values in parameter order for the body. Parameter names must be distinct. A count mismatch is a language failure and does not call the body.
A procedure may have fixed parameters followed by one rest parameter. The fixed prefix is required. The rest parameter receives a list of all remaining arguments in order. A lambda with only a rest parameter accepts any finite argument count, including zero. The rest list is immutable.
Rest pair allocation follows the Rest argument pair row in the Resources site table.
A call evaluates its operator and arguments in the order defined by Evaluation and bindings. The calling syntax does not change the procedure body or its lexical environment.
6.3 Expand a final argument list with apply
The apply procedure takes a procedure, any explicit arguments, and a final proper list. It places the list elements after the explicit arguments in their existing order. It calls the procedure with that combined argument sequence. A final value that is not a proper list produces a language failure before the called body runs.
The target call inherits this call's tail position under the tail-call rule.
6.5 Pass an internal value sequence to its receiver
The values procedure returns its arguments as an internal sequence of returned values. The sequence may contain zero, one, or several values. The call-with-values procedure calls its producer with no arguments and calls its consumer with the returned values in order. The consumer must accept that argument count.
The producer is outside tail position. The consumer inherits this call's tail position under the tail-call rule.
A procedure can return several intermediate values without giving the host a second output channel. An explicit receiver determines how those values are used.
An operator position, an argument position, a conditional test, and a binding initializer each require one value. Producing zero or several values in one of those positions is a language failure. A receiver cannot silently choose one value or turn the sequence into a list.
Identifier is defined by the reader grammar. The module grammar places this clause after the export clause and before definitions. The identifier names the public export. Its spelling is not a host selector. The preparation diagnostic mapping gives entry failures their catalog identities. The diagnostic phase does not change the prescribed check order.
Rule entry
The entry is the one procedure selected by the root module for an external rule request. Its input is an ordinary lexical argument. There is no reserved input global. A list containing several facts is still one Datum.
Source declarations select the entry. Each fixture names its root module in request.json as documentation notation. This notation does not define a public host schema or a CLI option. Preparation and modules owns module and export syntax. Profiles and value interchange owns canonical input and result encoding.
6.7 Validate each declared entry
A module may have at most one entry declaration in the entry slot of the module grammar. Its identifier names a public export of that module. Preparation resolves the export to one lexical binding. It checks that export, the resolved lambda form, and the accepted argument count in that order. The binding initializer must be a lambda after definition shorthand is normalized. An imported or reexported binding follows the same check at its original declaration. The lambda must accept one argument. Preparation validates declarations in dependency modules too. It does not execute an initializer to discover an entry.
A declared entry fixes the binding that the program exposes. Static checks prevent a factory or module initialization from choosing a different boundary. The same check applies to every submitted declaration.
6.8 Select the declared root entry
A closed bundle selects one root module. After module validation, preparation requires exactly one entry declaration in that root. The prepared program retains the resolved target of that declaration. Evaluation performs the required module initialization and invokes only the selected root entry. A dependency entry declaration does not trigger a call. No export name is a default entry. A host or command selector names the root module and cannot replace its declared target with another export. The host interface and command forms own selector representations.
Selecting the root fixes one program boundary before evaluation. Export additions and dependency entry declarations cannot silently change the procedure that receives the input.
6.9 Supply one input datum to the entry
An external rule request supplies exactly one Datum to one selected entry. The procedure receives the input through ordinary lexical parameter binding. An entry may have fixed or rest parameters when its accepted argument counts include one. A request with no argument or more than one argument is rejected. A caller supplies several facts by placing them inside one datum.
One explicit input makes the request reproducible and gives every product the same boundary. The host does not fill missing arguments from hidden state.
An entry may use any parameter shape that accepts one argument.
A successful entry call returns exactly one Datum. Zero or several returned values cause a boundary failure. The portable-data rule determines result membership. A failed boundary check returns no partial result.
Internal procedures and multiple values cannot acquire host authority or become extra external outputs. One complete result gives replay a well defined outcome.
Handle domain failures with lexical guards. Preserve structured conditions and terminal resource failures.
Scope
A rule can recover from a domain failure with a lexical guard. A terminal failure ends the request.
This chapter defines conditions and guards. Resources defines resource events. CLI and diagnostics defines diagnostic presentation.
Condition codes and data
A condition contains a stable phase, code, and typed data. A guard reads those fields through the condition accessors. Presentation follows CLI and diagnostics.
A raised occurrence carries its own canonical program site. The canonical-outcome rule reports that site. Source maps connect it to source text. A Condition value carries neither source coordinates nor a program site.
7.1 Expose stable condition data
A condition exposes a stable phase, code, and canonical typed data. Its raised occurrence supplies the canonical failure site. Presentation choices preserve those fields.
Rules need to branch on the same failure across products and locales. Source paths and message wording would make that decision depend on presentation.
A Condition is an immutable internal value. Every code in this catalog has phase evaluate. The diagnostic catalog uses the same codes and field meanings.
A field record is a proper association list of dotted pairs. Each pair has a string key as its car and a field value as its cdr. Keys are unique. The constructor sorts them by unsigned UTF-8 bytes. This representation uses ordinary Datum values.
Form
Meaning
(make-condition code fields)
Validate the closed schema and return a Condition. Construction does not raise that Condition.
(condition? value)
Return #t for a Condition and #f for every other value.
(condition-phase condition)
Return the string evaluate.
(condition-code condition)
Return the exact code string.
(condition-data condition)
Return the canonical immutable field record.
(raise condition)
Raise that Condition at the current canonical program site.
The constructor uses the exact fields below. Each field is required. No additional field is accepted. Construction validates the data. It does not perform the operation named by a field.
Code
Semantic fields
Meaning
runtime.not-callable
actual uses TypeTag
The evaluated operator is not a procedure.
runtime.arity
minimum uses Nat, maximum uses NatOrFalse, actual uses Nat
The call has an unsupported argument count. A false maximum means no upper arity bound.
runtime.value-count
expected uses Nat, actual uses Nat
A context receives the wrong number of internal values.
An exact numeric operation fails the stated numeric requirement.
domain.condition
reason uses ConditionReason, field uses StringOrFalse
Condition construction rejects a code or field record. A false field names the whole input.
domain.application
tag uses String, data uses Datum
The program supplies its own tag and portable data.
For unequal list lengths, identify the first list argument whose length differs from the first list. Check list arguments in argument order. Invalid slice ordering identifies the ending bound argument. Invalid UTF-8 identifies the bytevector argument. The owning library Rule determines when each value constraint fails.
Argument and entry positions start at zero. Counts and indices are exact integers. They never depend on host word size.
Type
Semantic domain
Nat
An exact nonnegative integer
Integer
Any exact integer
NatOrFalse
Nat or #f
String
A raw Unicode string
StringOrFalse
String or #f
Operation
A string. An automatically raised condition uses the exact public procedure binding name. A constructed condition preserves its supplied string.
After ordinary call evaluation and arity checks, construction follows the order below. The first failed check ends construction.
Order
Check
Failure
1
The code is a string
domain.type for argument 0 with expected type string
2
The code belongs to this catalog
domain.condition with unknown-code or terminal-code and false field
3
The outer field list is proper
domain.condition with payload-shape and false field
4
Visit each entry in list order. Check its pair shape, string key, and key uniqueness before advancing.
A nonpair uses payload-shape. A nonstring key uses key-type. Both use false field. A repeated key uses duplicate-field and that key.
5
Every required key is present. Scan required keys in canonical order.
domain.condition with missing-field and the first missing key
6
Every supplied key belongs to the schema. Scan supplied keys in canonical order.
domain.condition with extra-field and the first unknown key
7
Every value has its declared type. Scan keys in canonical order.
domain.condition with field-type and the first invalid field key
Enum values must match exactly. Paths have the exact segment shapes above. Portable data validation follows the Datum traversal order. Field values cannot contain a procedure or another Condition.
Each typed accessor and raise accepts one Condition. A different argument raises domain.type with expected type condition. condition? accepts any one internal value.
A Condition contains no source path, message, stack, or failure site. It is not a Datum. Data copied from its accessors remains ordinary portable data. Equality applied to a Condition follows the existing comparison domain rules.
A raised occurrence carries the Condition and its canonical program site. An unmatched guard propagates that same occurrence. Explicit raise creates an occurrence at its own site even when it uses a captured Condition.
Preparation, resource, admission, qualification, evidence, operational, and internal diagnostics have no guest Condition constructor. Boundary decoding and result validation also run outside an active guest guard. Their known codes cause terminal-code when passed to make-condition.
Construction, inspection, and raising use the ordinary resource accounts. Payload limits use the named resource model limits. A failed reservation ends evaluation without truncating fields or running guest recovery.
A closed code catalog gives every product the same recoverable failures. Typed fields make recovery independent of message text and host details. Ordinary association lists keep condition data inside the existing portable value model. A separate raised occurrence preserves useful failure locations without exposing source identity to guest code.
guard = "(" "guard" "(" identifier clause* ")" body ")"
body = definition* expression+
clause = "(" test expression+ ")"
| "(" test ")"
| "(" test "=>" recipient ")"
| "(" "else" expression+ ")"
test = expression
recipient = expression
Identifiers follow Source and normalization. Definitions and expressions follow Evaluation. Recursive body definitions follow the lambda initializer restriction.
Lexical guard
A lexical guard protects evaluation of its body, including calls made while that body runs. Its condition name is a lexical binding for its clauses. A matching clause computes the replacement value. Evaluation does not resume at the failed operation.
Structured raise propagates a condition. It cannot create a continuation or install a dynamic handler.
7.3 Recover from an ordinary condition
A lexical guard may catch a runtime or domain condition from its body. It abandons the failed body and returns the selected clause result. That result preserves its internal value count. The result reaches the guard expression's continuation. A body failure preserves the enclosing call's pending return. The tail-position rule governs the protected body and selected handler clause.
Structured raise signals a Condition with its stable phase, code, and data. It records the site of that explicit raise. It never resumes the operation that produced an earlier occurrence.
Explicit propagation preserves a failure that the current rule cannot handle. A resumable signal would add control behavior outside the adopted surface.
A guard uses the guard grammar. A body follows the ordinary definition and expression rules.
The condition name is bound only in the clauses. Body definitions are visible only inside the body. Clauses use the surrounding lexical scope.
Part
Required behavior
Protected body
Evaluate in source order with the guard active. Pass a normal result through unchanged.
Test
Evaluate once. Require exactly one value. Only #f is false.
Test and body
Evaluate the selected expressions in source order. Return the final result packet.
Test alone
Return the true test value.
Test and recipient
After a true test, evaluate the recipient once. Require exactly one procedure value. Call it with the test value.
Default clause
Use else once at most. Place it last. Its expression sequence must be nonempty.
Empty clause list
Propagate the original raised occurrence outward.
Normal or selected result
Preserve zero, one, or many internal values for the enclosing context.
A clause beginning with else is the default clause. In every other clause, => in the second position marks a recipient. These markers do not depend on bindings.
Clause tests, recipients, and bodies run with the handling guard inactive. A new failure reaches an outer guard. An unmatched condition preserves its original occurrence and failure site. A terminal failure ends guest evaluation.
An arrow call uses the ordinary procedure checks. A test or recipient with a wrong value count raises the ordinary value count condition. Later clauses do not run after a match or a failure.
Preparation rejects malformed guards in source order. Each rejection has phase normalize and code syntax.form. Its fields are fixed below.
Malformed part
form
reason
Missing or nonidentifier condition name
guard
guard-variable
Empty body or definition after an expression
guard
guard-body
Empty clause or improper clause list
guard
clause-shape
Default clause before another clause
guard
else-position
Default clause without an expression
guard
else-body
Arrow clause without exactly one recipient expression
Familiar conditional clauses express recovery without resumable control. Explicit evaluation order gives every product the same first failure. An inactive handling guard prevents recovery from catching itself. Internal value packets remain usable inside ordinary procedure composition.
Active protection and handler execution have different control lifetimes.
Guard clauses are tested in source order. The first matching clause supplies the replacement result. An unmatched condition propagates outward. The handling guard is inactive while clause tests, recipients, and bodies run. The guard event schedule fixes failure unwinding. Selected clause tail positions follow the tail-position rule.
A failing recovery clause must not repeatedly catch its own failure. Ordered clauses and outward propagation give nested recovery one deterministic path.
Guard clauses follow a fixed order and propagate unmatched conditions outward.
Discarding failed calls must preserve the enclosing call's pending return.
A terminal failure returns control to the calling application. Guest guards cannot intercept preparation, admission, resource, operational, or internal failures.
Resource exhaustion preserves the first resource cause. The evaluator runs no guest recovery or cleanup after that stop. A host interruption and an engine defect stay distinct from a deterministic language failure.
7.7 Keep terminal failures outside guards
Preparation, admission, resource, operational, and internal failures end the request outside guest recovery. A resource stop preserves its first cause.
Programs cannot use procedural handlers, continuable raise, call/cc, or dynamic-wind. Preparation rejects these removed control operations. The diagnostic uses phase resolve and code library.reference. Its reason is removed-operation. Its name identifies the removed operation. The failure mapping applies the diagnostic catalog.
The evaluation rules order the operator, arguments, and call checks. The resource rules order reservations at their semantic sites. A guard sees the first catchable condition reached by those events.
Later arguments do not run after an earlier argument fails. A guard may select a recovery clause. A terminal resource stop preserves its first cause.
A work unit measures normative computation. The tariff assigns work to semantic events, including native computation and encoding. Instruction counts and wall time do not define that work.
Logical allocation counts the cumulative objects and intermediate storage required by the semantic computation. It includes exact number limbs, aggregates, closures, environments, arguments, frames, conditions, and encoded results. Host capacity, pointer width, sharing, interning, and garbage collection do not change those charges.
A frame represents active semantic control state. Returning releases active frame capacity. It does not refund cumulative work or allocation. A channel budget limits the data processed or emitted by its declared channel. Input, results, and diagnostics have explicit finite budgets.
8.1 Identify model data before resolving budgets
ResourceModelDefinition is the complete canonical declarative Datum for one versioned resource model. The declaration fixes the semantic parameters consumed by its supported event schedules. It is supplied explicitly and validated against the selected supported model. The identity contract wraps that declaration in ContractInput. That contract defines ResourceModelIdentity and its bytes.
Declaration component
Required meaning
Event contracts
The supported versioned event catalog and each complete requirement function
Requirement inputs
Only the semantic operands fixed by the event schedules
Units and representations
Work and logical allocation units and exact finite representation bounds
Default axis data
Complete finite axis values before any model identity is attached
Channel and reporting bounds
The declared channel units and complete terminal and framing requirements
Host support
The supported ingress, egress, trace, and physical envelope declarations
This table defines composition requirements for the complete declaration. It does not introduce a second model byte codec or select a published model name. Concrete coefficients, units, defaults, bounds, and physical capacities remain with cost model freeze. A fixture parameter is documentation notation and cannot replace concrete admitted model data.
Default axis data contains values and axis names without resource_model metadata. Its definition is known before ResourceModelIdentity is computed. The complete model declaration contains that data or already verified independent semantic definitions. After the model identity is verified, preset resolution constructs the effective budget records. The ProfileHostBudget wrapper then attaches resource_model to its six axis values. The fixed selection carries the model for preparation and evaluation limits. No resolved budget wrapper is fed back into its model declaration.
Limit record
Exact required fields
PrepareLimits
allocation, diagnostic, frames, input, result, work
EvaluationLimits
allocation, diagnostic, frames, input, result, work
Each field is an exact nonnegative Datum integer. The two records use separate phase accounts. Neither contains a format field or a resource_model field. Missing and unknown fields, negative values, nonintegers, and unlimited values are refused. The selected model supplies their finite representation bounds. Profiles owns its different host axis record and required model metadata. TraceOptions remains the separate record from trace reservations.
A model definition excludes its own digest and any identity derived using that model. This excludes module, library, program, preparation request, evaluation request, and profile work identities. It also excludes later outcomes, receipts, reports, and evidence. Each referenced semantic definition is verified before its dependent identity. The resulting dependency graph is finite and acyclic. No identity authorizes registry, filesystem, or network discovery.
The model supplies requirement vectors and cannot change event order or canonical site selection. The event catalog selects events and occurrence paths. The canonical site contract encodes those program-local sites. Program and request identities are attached only by the surrounding outcome or report. Runtime operands and sites are inputs to requirement functions and are not captured program definitions inside the model.
A model must be identifiable before a program or host request can use it. Default axis data therefore precedes the wrapper that names the model. Program-local sites keep this dependency order finite.
8.2 Resolve finite budgets before execution
Every public entry point uses finite limits for each phase it performs. Preparation and evaluation use separate accounts. A convenience call resolves the common default preset before the requested phases begin. Explicit unlimited limits are rejected.
A program can enter through a CLI, API, or browser. Each path must terminate under the same resource contract.
8.3 Charge normative work
The evaluator charges work units for every normative computation. Native arithmetic, traversal, decoding, and encoding remain metered. Host time and instruction count do not replace the tariff.
A single native call can perform input sized work. A portable work model must account for that work before it happens.
8.4 Count cumulative logical allocation
Every guest object and intermediate allocation contributes to cumulative logical allocation. Sharing and collection do not reduce that charge. Returning from a call does not refund it.
Physical memory reuse depends on the host. Charging semantic allocation gives the same stop for the same request on every implementation.
8.5 Limit active semantic frames
Frame limits count active semantic control state. A tail call replaces its current call frame. Nontail calls and active guard control consume their declared frames. Host stack layout does not change the limit. The tail-position rule determines which call replaces the current frame.
A reservation checks that the next semantic event fits its applicable budgets. The evaluator reserves before the event performs work or creates data. A refused reservation commits no effect for that event.
Successful work and logical allocation charges accumulate for the request. They are never refunded. Incremental work reserves each next step before performing it. Each operation declares its checks, traversals, charges, and failure sites.
8.6 Reserve before the semantic effect
Each event reserves its required work, logical allocation, frame capacity, and channel budget before its effect. A refusal stops that event before the effect. Committed cumulative charges are never refunded.
Evaluation follows the application-order rule. Arity, domain, traversal, and reservation events occur in the order declared for the operation. Work needed to perform a check is itself metered.
A later reservation cannot move ahead of an earlier check. A resource stop prevents later guest work and recovery. When a domain condition is reached first, a guard may handle it under the remaining budget.
Equivalent physical implementations preserve the semantic events of the same canonical program. Different programs that compute the same value may have different costs.
8.7 Keep checks and reservations in order
Checks and reservations follow the declared semantic event order. A later charge cannot hide an earlier domain failure. Work required for an earlier check may itself exhaust a budget.
Reordering a reservation can change the condition a guard receives or turn a language failure into a resource stop.
8.8 Preserve the first exhausted axis and site
Optimizations preserve the first failure, exhausted axis, and canonical site for the same semantic request. Inlining, native fast paths, and constant sharing preserve normative work and allocation events.
Equal final totals alone allow an implementation to stop at a different event. The caller observes the first stop and its location.
8.9 Use the ordered semantic event catalog
Every operation follows the schedules below. Each named event reserves its complete requirement vector before its check or effect. The atomic axis order applies unchanged. The selected resource model supplies the requirement vector from the declared semantic operands. It cannot add, remove, split, or reorder these events.
An accepted reservation commits its charges before the associated check. A refused reservation commits neither those charges nor that effect. A failed check enters the diagnostic protocol before its failure is committed. No later operation event runs after a committed failure.
EventIdentity is an exact case-sensitive event name from this chapter. The evaluation, library, preparation, graph, and codec schedules define those names and their reservation points. Other chapters select these events for their operations. Unknown names are rejected. Profile host families and trace reservations retain their separate account definitions. A tariff coefficient, allocation unit, finite default, representation bound, or physical envelope remains under cost-model-freeze.
A program event uses the canonical site bytes. Its role is its exact EventIdentity. The occurrence is the original semantic occurrence. A program identity is attached outside those local bytes.
Subject
Occurrence
Path suffix
Explicit call and its shared checks
Call node
Empty for the call, field(operator) for its operator, argument(i) for an argument
Entry input and result
The selected entry lambda node
field(input) or field(output) before the component path
Binding creation
Binding record
Empty
Environment or recursive group
Stored Group record when present. Otherwise the owning let, letstar, letrec, namedlet, or lambda node
The member position as element(i) when one member is selected
Implicit named let call
Namedlet node
field(initial-call)
Clause test or receiver call
Clause record
field(test) or field(receiver)
Rest argument pair
The invoked lambda node
result(0) followed by element(i) in argument order
Public procedure event
Its invoking call occurrence
The argument or result path followed by the visited component
Guest library inner call
The inner call in the fixed library graph
Its own operator and argument paths
Pair component
The owning operation occurrence
car before cdr
Vector or internal sequence element
The owning operation occurrence
element(i) in the declared order
Text scalar or octet
The owning operation occurrence
scalar(i) or byte(i)
Cross-argument check
The owning operation occurrence
The first argument selected by that check
Comparison
The owning operation occurrence
field(compare) followed by the left argument and compared component path
Generated result
The owning operation occurrence
result(i) followed by its component path
The first rest pair has index zero. Each following pair has the next index. This path adds no schema field.
Indices are mathematical nonnegative integers. A path selects a semantic component. A host address, source line, temporary register, or fixture label cannot select it. Repeated visits keep the same site. Event order distinguishes those visits. An inlined library call retains the site of its fixed library occurrence.
The resource model receives the operation name, exact input sizes, result shape when known, traversal direction, and selected component. Those parameters determine requirements. They do not create additional events. A rejected event retains its exact name and path.
The following fixed prefixes select implicit calls. They precede the operator, argument, result, or component suffix of every shared call event. Call-return uses the same prefix as call.
Parameter initialization still names its declared binding occurrence. A callback body still uses its own program nodes. The prefix does not become a call stack or a source label.
For a unary string transformation, the result allocation site is result(0). For a folded string comparison, the folded result of argument i is allocated at result(i) of the invoking comparison call. The site role is datum-allocate. All scans and maps continue to select the original argument(i) and its scalar positions.
A folded string comparison uses field(compare), argument(i), scalar(j). Its paired left and right reads have that single site. A folded character comparison uses field(compare), argument(i). A normalization event selects argument(i) once for the complete string transformation.
The evaluation and procedure Rules select the work. This table places reservations around that work.
Operation
Ordered schedule
Site
Literal or quote
literal-value, then expose the immutable value
Literal node
Name use
binding-read, then fetch the resolved binding
Use node
Lambda expression
closure-create, then capture its lexical environment
Lambda node
Body or explicit begin
Run any leading recursive group, then visit expressions in source order. Discard every nonfinal result sequence. Forward the final sequence
Child occurrences. A body wrapper adds no event
Application operands
Evaluate the operator, result-check, argument-sequence, then each argument expression, result-check, argument-store
Call node and its operator or argument path
Application dispatch
callable-check, arity-check, call, then parameter binding and the called operation
Call occurrence
Fixed parameters
environment-create, then binding-initialize in parameter order
Lambda node, then parameter bindings
Rest parameters
Fixed parameter binding, then datum-allocate per rest pair in argument order, then binding-initialize for the rest binding
The Rest argument pair row in the site table, then the rest binding
Normal call return
call-return, release the active call capacity, and forward the result sequence
The invoked call occurrence
Tail call
The ordinary operand and dispatch schedule, or the implicit call schedule below. call replaces the current call capacity under the tail-call rule
Tail call occurrence
Parallel let
Each initializer, result-check, and traversal-state retention from left to right, then environment-create, then binding-initialize in member order, then body
Let node paths and bindings
Let*
Initializer, result-check, environment-create, binding-initialize, then the next nested binding
Letstar node and member path, then its binding
Module definition
Evaluate its non-lambda initializer, then result-check, environment-create, and binding-initialize. No intermediate sequence is retained
The initializer occurrence, then its stored group with element(0) for result-check, then that group and its declared binding
Recursive group
environment-create, each closure-create, then each binding-initialize, all in member order, then body
Stored group or letrec node, then lambda nodes and bindings
Named let
Each initializer, result-check, and traversal-state retention in the enclosing scope, then recursive environment and closure events, then the implicit call schedule on those saved values
Namedlet node and its loop and parameter bindings
If
Test, result-check, branch-select, then only the selected child
If node and test path
And or or
Each nonfinal operand, result-check, branch-select until selected. Forward the final operand sequence if reached. An empty form uses one branch-select
Form node and operand path
Cond clause
Test, result-check, branch-select, then its selected body, test value, or receiver schedule
Clause record
Default clause
branch-select, then its body. No test or synthetic result-check
Default clause record
Clause receiver
Receiver expression, result-check, then the ordinary call checks with the saved test as its argument
Clause receiver path
Guard
guard-enter, protected body, then guard-leave on normal return. A final body call completes call-return before guard-leave
Guard node
Caught occurrence
Discard frames above the handling guard without call-return and release their frame capacity. guard-bind, deactivate the guard, then the declared clause schedule
Guard binding and clause records
Unmatched guard
guard-propagate with the original occurrence and site
Guard node. The propagated failure site is unchanged
Module initialization
Fixed library prefix, then every source module in dependency order. Use Module definition for a non-lambda definition and Recursive group for a lambda group
Module, group, and binding records
A module definition uses one sequential binding step. Its result-check requires one value and uses the complete path element(0) on its sequential module group. Adjacent lambda definitions use the Recursive group row.
The result-check in an operator, argument, initializer, test, or receiver context requires one value. It reserves before reading the count. A body or begin does not impose that check on discarded or final values. A result sequence is created by its producing operation and forwarded without copying.
The argument-sequence event creates an empty logical operand sequence. Each argument-store reserves before retaining one completed argument. A failed argument never enters that sequence. Callability and arity remain after every operand. Parameter events follow successful call checks. Frame requirements come from the selected model. The table fixes no frame size. A replaced tail call has no later call-return event of its own.
An implicit call starts with already computed values. It runs argument-sequence and argument-store without reevaluating expressions or adding argument result-count checks. It then runs the ordinary callability, arity, call, and parameter events. This applies to entry, callbacks, named let, and clause receivers. Entry uses its selected lambda occurrence and the entry field path. A named let uses its own node for the implicit closure and parameter environment. No synthetic lambda node is created.
Under the tail-call rule, apply targets and call-with-values consumers inherit the invoking call's tail position. A tail transfer passes the native frame and pending return to the target. The replaced native call has no call-return. The producer and every other library callback remain nontail.
A library callback precheck is a distinct arity-check at the invoking operation. It does not remove the ordinary arity check of a later callback call. This preserves both the empty-input precheck and the complete call contract.
Body and handler tail positions follow the tail-position rule. Deactivating the guard releases its active guard control. The handler result reaches the guard expression's continuation. The enclosing call keeps its pending return when the body fails. A handler tail call replaces that enclosing call's frame. Unmatched clauses follow the guard propagation rule. Unwinding does not refund work or allocation. A terminal resource refusal runs no guard event after the refusal.
For every procedure in the closed library catalog, expand the shared call schedule first. Then expand its domain protocol and its row events in their written order. The specialized constructor and traversal protocols take precedence where the library Rule names them. A row with no later events still performs its shared checks.
Event
Reservation point
Repetition and site
argument-check
Before starting an argument domain or a prescribed value constraint
Argument order. Finish that domain's nested traversal before the next argument
list-step
Before inspecting a pair spine position, selected component, or final tail
A domain spine pass visits the head through the final tail. Later row passes visit only their declared components, using the corresponding car or cdr path
sequence-step
Before inspecting a stored length, selected element, or required sequence end
Each declared length, element, or end visit in the row order. Stored length uses field(length)
datum-validate
Before classifying the next portable-data component
Depth-first, pair car before cdr, vector elements in ascending index order
compare-scalar
Before comparing the selected scalar pair or sequence ends
Adjacent pair order and the declared left-before-right position order
compare-datum
Before comparing the current pair of Datum nodes
Preorder with car before cdr and ascending vector elements
exact-arithmetic
Before the next result in the declared arithmetic reduction
Each left reduction step. Unary operations have their single declared step
rational-reduce
Before reducing the declared exact result
Immediately after the arithmetic stage that requires it
decimal-scale
Before forming the exact grid step
The rounding call
exact-divide
Before forming its declared quotient and remainder or adjacent candidates
The numeric call or current reduction step
rounding-select
Before choosing the rounded integer or detecting a required rounding failure
The rounding call after scale and division
text-scalar-scan
Before inspecting the next scalar or required sequence end
The exact pass and scalar order in the string or Values Rule
unicode-map
Before the property query or case mapping
Original scalar order after the required input scan. Original text determines contextual mappings
unicode-normalize
Before the complete declared normalization of one validated string
Argument order after its complete scalar scan
traversal-state
Before creating or advancing the declared logical cursor or internal value sequence
List argument order and the stated element order for traversal. A constructor uses its declared result index order
callback-call
Before beginning the ordinary call protocol for the selected callback
The implicit call occurrence and prefix from the site table. Guest body events retain their own occurrences
result-check
Before checking a required callback result count
Callback call occurrence and tuple index
datum-allocate
Before creating the declared immutable result or aggregate component
The row's result order. Reuse and interning retain every event
condition-construct
Before creating the fully validated Condition and canonical field record
Constructor call after every required field check
condition-inspect
Before reading a requested immutable field
Accessor call and field(code), field(phase), or field(data)
condition-raise
Before creating the explicit raised occurrence
Raise call. The diagnostic payload protocol completes before the occurrence commits
Scalar predicates use their argument check as the type classification. They add no fabricated allocation for an already defined Boolean or empty list. A literal event still accounts for exposing a source literal. Numeric event requirements include their exact intermediate storage. A single semantic arithmetic event cannot hide unreserved host work.
Text passes use field(scan), field(map), or field(compare) before the scalar index. A length scan and a later selected-range scan remain distinct visits. Full string mapping scans the complete original input before mapping its scalars. Mapping retains all required contextual work in the named map requirements. Normalization is one semantic transformation event per argument. Its complete intermediate requirement is reserved before transformation. The following allocation event materializes its result.
An exact arithmetic row with several stages does not reserve a later stage before an earlier check. The empty addition, multiplication, gcd, and lcm cases have their declared identity result. They perform no nonexistent reduction step and still perform any result allocation stated by their row.
The list, sequence append, and UTF-8 rows in the library catalog fix the following event boundaries. Make-list repeats traversal-state then datum-allocate for each result index after all domains. Count zero performs neither. List-ref and list-tail perform their full domain spine pass before bounds and the subsequent selected-component walk. List-tail zero performs no later movement.
Vector-append and bytevector-append complete all domains, then read every stored length in argument order, then reserve the complete result, then visit the elements in argument and index order. Every length read and exact total update belongs to its sequence-step requirements. An empty argument has a length event and no element event.
UTF-8 decoding allocates one result scalar after its complete valid byte sequence. Encoding allocates one result octet at a time after its scalar visit. An empty conversion visits its required end before one empty-aggregate allocation. A malformed prefix fails at the byte that first proves it invalid. A missing continuation fails at the required end position. Its ordinary diagnostic payload follows that detecting visit. Bytevector->list reads its stored length once and then reserves each octet integer and result pair in one combined datum-allocate before constructing either.
In these schedules and their examples, a reservation extent is a declared count of semantic components consumed, created, or retained by the operation. A pair has two component positions. A scalar or octet has one. One make-list cursor position has extent one. A combined octet integer and pair has extent three. An aggregate extent is its element count. For a full string map or normalization, extent n counts original input scalars. It does not count scratch capacity or context visits. A Unicode string result extent m counts its actual output scalars. The operation and result shape distinguish these counts. Extents are exact mathematical integers, not allocation tariff units or host storage sizes.
An extent of zero still reserves the complete requirements for the empty aggregate. A null extent in a trace means that no component-count extent applies to that event. It does not omit its reservation or assign zero requirements. Every event reserves its complete requirement vector from its exact semantic inputs and shape. This includes headers, cursor state, exact integer representation, temporary storage, and all work before the effect. Diagnostic-payload uses its complete typed payload and diagnostic codec. These example fields are documentation notation and add no field to a canonical site or public report schema.
A scalar property query or simple case mapping performs one scalar scan and one unicode-map. Its map extent is one. For digit-value, that map reserves the complete exact integer representation and value slot before creating the digit result. A nondecimal input returns #f within the same event. Neither result adds a datum-allocate event. Booleans and characters retain their declared scalar representation requirements.
Let n be the number of original input scalars. Full string mapping first scans all n scalars and the required end. It then maps the original scalars in ascending index order. Each unicode-map has extent n. The first map reserves one scratch buffer with capacity D times n scalars. D is 3 for uppercase, 2 for lowercase, and 3 for folding. That reservation succeeds before either scratch storage or the first mapped scalar is created. Later maps reuse that capacity. They reserve their own mapping work without another scratch allocation. An empty input performs its end scan and result allocation, with no map or mapping scratch reservation.
The map requirement includes exact bound calculation, table lookup, expansion, and retained scalar storage. These counts are mathematical integers. A host word width cannot add a domain limit or change the first failure.
Lowercasing keeps a preceding-cased state while visiting the original scalars. Case_Ignorable scalars leave that state unchanged, including a scalar that is also Cased. Every other original scalar sets the state to its Cased property. A U+03A3 map tests the state before that scalar updates it. If the state is true, inspect the original suffix in ascending index order. Skip Case_Ignorable before testing Cased. The first remaining scalar, or the required end, determines whether a following cased scalar exists. Final_Sigma selects U+03C2 exactly when the preceding state is true and no such following cased scalar exists. Otherwise U+03A3 maps to U+03C3.
The current map includes the preceding-state work and every required suffix visit in its complete requirements. At most n original scalars are visited for that map's context work. These visits create no additional text-scalar-scan events. Earlier mapped results never supply context.
After the complete original scalar scan and required end, each normalization call performs one unicode-normalize at argument(0). Its extent is the original scalar count n. D is 4 for NFC and NFD, and 18 for NFKC and NFKD. Its complete requirements cover two scalar buffers, each with capacity D times n, and 256 canonical-combining-class counters. Bound arithmetic, decomposition lookup, ordering, composition, and all intermediate storage belong to this reservation. It succeeds before transformation or scratch materialization starts.
Fully decompose the input under the selected form. Use stable counting order within each maximal nonstarter run. A scalar with combining class zero separates runs. Equal combining classes retain their original order. Compose NFC and NFKC in place under the Unicode blocking, exclusion, and Hangul rules. With decomposed length L and r runs of at least two nonstarters, ordering work has the structural bound O(1 + L + 256r). L is at most D times n and r is at most floor(L / 2). Reserve from n, D, and these upper bounds before decomposition; discovering actual L or r is transformation work. The selected model covers fixed workspace setup and every complete lookup, counter pass, scalar visit, and movement, including their coefficients. It cannot hide a recursive walk, comparison sort, or quadratic insertion pass outside the reservation.
The empty string still has one unicode-normalize with extent zero, followed by one datum-allocate with extent zero. The fixed workspace and empty-result requirements remain part of those reservations.
A completed string mapping or normalization reserves one datum-allocate before materializing its immutable result. Its extent is m, the actual number of output scalars. The complete requirements include the string header, value slot, and space for up to 4 times m UTF-8 octets. They also include encoding work and any temporary storage used for materialization. The extent remains m when input length, decomposition capacity, or UTF-8 octet length differs. Extent zero still reserves an empty string result. Refusal publishes no partial string and refunds no earlier charge.
All argument domain checks finish before folding or replacing any retained argument. Fold each argument in ascending argument order. Retain its completed folded value in the same logical operand-sequence position already reserved for that call. A character replacement belongs to its unicode-map. A string replacement belongs to its completed result allocation. This replacement changes no caller binding or immutable input value. It adds no argument-store or traversal-state event and requires no separate descriptor sequence. Every folded value remains available until comparison finishes or the call fails. Repeated references to the same input still perform each argument's full folding schedule and result reservation.
After all folding and retention, each folded character pair performs one compare-scalar. For strings, each visited position performs one compare-scalar. Reserve before reading the left scalar or end, then the right scalar or end at that same position. Both reads belong to that event, including when the left sequence has ended. Only after both reads does the pair stop at unequal scalars or an end. No additional text-scalar-scan accompanies these folded reads. String comparison sites use field(compare), argument(i), scalar(j), where i is the left argument of the adjacent pair and j starts at zero for each pair. Character comparison selects field(compare), argument(i). The first false pair ends comparison after every argument has already been folded.
The following expansions complete the traversal reservation positions. They preserve the already adopted validation order. Implicit call positions follow the tail-call rule.
Operation
Ordered expansion
Stop rule
equal?
Left argument-check with all left datum-validate visits, right argument-check with all right visits, then compare-datum visits
No comparison before both complete validations
eq?, eqv?
Left scalar argument-check, right scalar argument-check, then the scalar comparison schedule
A procedure or Condition is a domain failure before comparison
Datum comparison
compare-datum at current nodes, then compare-scalar for scalar contents or sequence lengths, then child comparisons
Stop at the first unequal component
String Datum contents
Each position has left and right text-scalar-scan, then compare-scalar
Stop at first mismatch or sequence end
Bytevector Datum contents
Left and right sequence-step, then compare-scalar per byte
Stop at first mismatch or sequence end
Proper-list domain
argument-check, then list-step at every pair and the final tail
No element validation or callback before the whole spine succeeds
Datum, character, or octet list domain
Complete spine, then required element checks from the head
Each element completes before advancing
Association-list domain
Complete spine, then each entry pair check and complete key Datum validation
All entries finish before search
Multiple-list callbacks
Procedure check, complete list domains in argument order, argument-check per length comparison, arity-check for callback
The callback arity check runs even for empty lists
Ascending callback loop
Per tuple traversal-state, callback-call, required result-check, then any selected result datum-allocate
Allocation precedes the next callback
Fold-right
traversal-state for the complete logical state in list argument and ascending index order, then descending callbacks and result checks
No callback before state reservation succeeds
For-each
Per tuple traversal-state, callback-call, discard the returned sequence
No single-value check is added
Apply
Complete final-list validation, then its selected list-step and traversal-state steps to assemble arguments, then arity-check and callback-call
No body before final-list and target-arity success
Call-with-values
Producer arity-check, producer callback-call, traversal-state for the returned sequence, consumer arity-check, consumer callback-call
Preserve every producer result in order
Values
traversal-state for its complete returned sequence
Zero and multiple values remain internal values
Make-condition
Code type and membership checks, whole field-list spine, then each entry's pair, key, and duplicate checks, then canonical required keys, supplied keys, and field values, then condition-construct
Every constructor check follows the existing Condition protocol
Constructor string-key comparisons scan scalars and compare them in key encounter order. Each new key checks prior keys in their list order. After duplicate checks, one traversal-state establishes the canonical key order. Its requirement depends on the complete key collection. Required-key, supplied-key, and field-value checks then use that canonical order. Portable field data uses datum-validate. No constructor field is truncated.
Traversal workspace belongs to the event that first needs it. A child visit reserves any added logical cursor storage before descent. Finishing a visit can release active cursor storage but never refunds cumulative allocation. Tail traversal does not depend on the host stack. Sharing does not skip validation or comparison visits.
Semantic event boundaries make a limit independent of host instructions. Ordered checks preserve the same first failure across products. Named size functions allow the measured tariff to change without inventing a new execution order.
A module definition uses the same event order as one sequential binding step.
A rest list belongs to its lambda occurrence. Its ordered pair path reuses the existing result and element components.
Normal return order and the release of abandoned frames must be explicit.
Library event rules fix per-component reservations and the first detecting visit. They preserve the full argument checks, exact mathematical indices, and complete event requirements. An implementation can change storage without changing these event boundaries.
Complete storage and work are assigned to the declared Unicode events. Original scalar counts, generated scalar counts, and typed result sites preserve reservation order across physical representations.
8.10 Reserve source and prepared-program work in order
Preparation uses its own finite account. The source event names, module order, and prepared validation order apply unchanged. The tables below supply the remaining event roles and locations. No source event runs guest code.
An event before a program exists has a preparation location. It does not invent a program identity or a canonical evaluation outcome. Source locations use the immutable submitted source. Prepared-input locations use the captured immutable byte snapshot.
Stage
Ordered events
Location
Bundle admission
prepare.bundle-order, then prepare.bundle-check for duplicates in canonical name order, then the root check
Selected decoded name. The root check selects the submitted root name
Fixed library
Its required prepared validation events before any source front end
The fixed library operand and its wire or record position
Source capture
prepare.capture-source before retaining each immutable module span
Module name and the entire submitted span
Decode
prepare.decode-step per next scalar attempt and final end check
Module name and starting byte offset
Read
prepare.read-step, prepare.read-enter, and prepare.read-node in the adopted reader order
Module name and decoded scalar offset. A completed datum uses its opening offset
Normalize
prepare.normalize-node before each visited form
Module name and the form's reader-tree path
Module clauses
prepare.module-check before each wrapper, name, import, export, and entry syntax check
Module name and selected clause or field path
Binding prechecks
prepare.binding-check before the envelope and each prescribed member check, then prepare.binding-publish per member
Group reader-tree path and member index
Missing imports
prepare.dependency-check per import in canonical module and clause order
Import spec reader-tree path
Cycle traversal
prepare.cycle-enter once per visited module, then prepare.cycle-edge per dependency edge in canonical order
Module name and selected dependency name
Resolution
prepare.resolve-import, prepare.resolve-use, prepare.resolve-export, then prepare.entry-check in the adopted resolution order
Selected import, use, export, or entry reader-tree path
Canonical records
prepare.record before each module, binding, node, group, or clause in the canonical construction order
Its canonical table kind and index
Fresh verification
The structural, scope, event-role, identity, and seal steps of prepared validation
The constructed record or field
prepare.binding-check retains its individual envelope, shape, identifier, duplicate, and recursive-lambda checks. It never combines them into an implementation-dependent scan. Module definition prechecks still finish before child normalization. Reader lookahead, comments, discarded data, and completed token checks retain every event fixed by Source.
A reader-tree path starts at the module datum. It selects list car and cdr or vector elements in structural order. Shorthand and escape spellings retain their exact source span for preparation failures. Canonical program sites are assigned only after canonical construction.
Source capture charges its actual source span to the preparation input channel once. Decode and read visits retain their work and storage charges without charging the same source octets again. The source span excludes host paths and presentation metadata.
Existing event
Reservation placement
Location
prepared.capture-input
Before immutable capture and any validation read
The complete submitted prepared byte span
prepared.read-header
Before each header octet attempt
Wire offset, including a missing octet position
prepared.begin-record
Before each compound record, list header, and list item
Opening wire offset and schema field path
prepared.read-field
Before each later octet attempt and final end check
Wire offset
prepared.check-record
Before each ordered record, count, kind, canonical-position, child, tail, or site check
Record kind, index, and checked field
prepared.check-reference
Before each declared reference or reconstructed lexical use check
Record kind, index, and checked field
prepared.check-identity
Before each required dependency or semantics check and optional requested program identity check
Header or dependency field
prepared.seal-handle
Before creating the complete immutable verified handle
Whole verified program
prepared.write-header
Before each canonical output header octet
Output wire offset
prepared.write-field
Before each remaining canonical output octet
Output wire offset
The existing prepared validator fixes the interleaving of record and byte events. This table adds no second read or record boundary. Capture charges the submitted prepared span to the preparation input channel once. Subsequent validation reads keep their work and storage requirements. Fresh typed records run the validation checks that apply to records. They do not fabricate an incoming byte stream.
Export first sizes the selected canonical prepared encoding from its verified records. Each record-sizing step uses prepared.check-record with field(encoded-size). A complete result-channel reservation covers its output span before the first write event. Writes follow the selected resolved or bytecode grammar. A failed preparation or export publishes no new handle or complete artifact.
Requirement functions use the caller-selected trusted preparation model. A resource model identity found inside unverified bytes cannot select the budget for parsing those bytes. A cache can reuse a verified preparation result under its handle contract. It cannot remove evaluation initialization or evaluation events.
Graph and source-map work uses preparation limits. The graph validation order selects the checks. It runs no initialization or entry.
Stage
Ordered events
Location
Capture
graph.capture-input before retaining the immutable packet
Complete graph or source-map span
Framing
graph.begin-record at the exact outer boundaries below. graph.read-header per outer magic and version octet. graph.read-field per outer field octet attempt
Wire offset and schema field path
Local canonical checks
graph.check-record after each decoded count, tag, or field, then at exact end of input
Selected field or final wire offset
Embedded resolved payload
Existing prepared capture and decoding events, followed at the graph validation stage by prepared record, reference, site, and identity checks
Embedded payload coordinates and records
Outer identity
graph.check-identity after embedded validation
Outer program identity field
Source-map reconstruction
graph.check-identity for source identity, then the ordinary source and preparation events for the captured bundle
Source identity field, then exact module source coordinates
Map comparison
graph.map-check once per expected mapping against the next supplied row in canonical site order, then one final end-of-mappings check
Mapping record and selected site
Projection
graph.project before each canonical prepared compound record in resolved/1 wire order
Its original canonical occurrence and relation path
Output sizing
One graph.size-record before sizing the complete GraphBytes or SourceMapBytes packet
Output record path
Output reservation
result-channel for the complete GraphBytes or SourceMapBytes packet, then codec-allocation for its buffer
Whole output packet
Output encoding
graph.write-byte before each output octet in grammar order
Output wire offset
Foreign identity and site byte fields are checked at their graph.check-record event under their imported canonical decoder. Their complete work and workspace are covered by that event. A malformed count stops before its collection. Embedded prepared decoding follows its own exact event boundaries. The surrounding graph end check precedes the later prepared semantic validation stage required by the graph Rule.
Graph capture charges its complete input span once. A nested validated span keeps its capture, work, and allocation events but adds no second input-channel charge for octets already captured by its outer packet. Source reconstruction keeps source decoding and preparation work. Its source spans are already included in the captured source-map input packet.
Graph export from an existing handle projects only its verified records. A supplied source map is checked before it can annotate that projection. Neither graph data nor a source map can replace a handle or a completed outcome. Output is published only after the entire graph or map packet succeeds.
Projection compound records are Header, Module, Dependency, Import, Export, Binding, Node, Group, Clause, and a present internal definition group. Deriving inspection relations from a record belongs to that record's graph.project requirement. Derived display rows add no separately metered events. An absent optional record adds no record event.
Outer graph.begin-record boundary
Exact occurrence
GraphBytes
Once after capture and before its first header octet
SourceMapBytes
Once after capture and before its first header octet
Mappings collection
Once before its count
Mapping item
Once per item before its first Site count
Mapping compound record
Once immediately after its item event and before that same Site count
Counted IdentityBytes, CanonicalSiteBytes, SourceBundleBytes, and ResolvedPayload fields add no outer record boundary. Their count digits are outer field octets. Embedded prepared payload octets use prepared.read-header and prepared.read-field instead of another graph.read-field event. Its compound and collection boundaries use the existing prepared.begin-record inventory exactly once. Other foreign byte fields use graph.read-field for their octets and graph.check-record for their complete canonical foreign checks.
The sole graph.size-record requirement includes the entire size pass over the verified output structure. The packet boundary is its location. No rendered relation row, optional absent record, host buffer chunk, or serializer loop adds another size event.
A projected Header uses the root module occurrence with field(header). A Dependency, Import, or Export uses its owning module occurrence with field(dependencies), field(imports), or field(exports), followed by its table position as element(i). Every other projected compound uses its own module, binding, node, group, or clause occurrence. A present internal group uses its retained group occurrence. These paths carry the graph.project role.
A mapping comparison is one event, not separate expected-row and supplied-row passes. Missing or misordered rows stop at that expected mapping event. After the last expected row, the final graph.map-check rejects any extra row. Each paired comparison uses the expected occurrence with role graph.map-check. The final check uses the root module occurrence with field(mappings). The sizing and output-reservation events use the root module occurrence with field(packet).
Source and prepared bytes need finite checks before they are trusted. Keeping their event order separate from evaluation prevents caches and alternate prepared forms from changing a guest receipt.
8.11 Keep ingress, codec, and failure reservations explicit
The host selects a trusted finite ingress envelope before reading an untrusted request. Incoming fields cannot enlarge that envelope. The host interface defines the input records. The ingress account covers transport capture and record parsing. It does not replace the preparation or evaluation account.
Canonical guest input decoding and materialization spend EvaluationLimits from their first event. This remains true before a request identity exists. A failed input decode starts no entry and produces no canonical evaluation outcome or evaluation receipt. The diagnostic catalog fixes the admission phase of that refusal.
After input acceptance, the same evaluation account continues through module initialization, entry, result checks, and result encoding. There is no reset or refund at request identity creation. Profile-only schema and evidence work retain their separate host account.
Operation
Ordered events
Account and location
Transport capture
ingress.capture-input before acquiring an immutable bounded span
Trusted ingress account and operand span
Request record parse
ingress.read-byte before each octet attempt, then ingress.check-field at each completed field
Trusted ingress account and wire offset or field path
Request record construction
ingress.materialize before retaining each validated record or sequence item
Trusted ingress account and record path
Limits and dependency selection
ingress.check-field before validating each field in the interface grammar order
The submitted record field. Trusted defaults remain external to that record
Native value convenience call
The same record validation and immutable capture requirements
Its typed argument path
Ingress capture reserves the actual supplied span before copying it. A borrowed span requires exclusive or protected access during capture. Parsing keeps the captured snapshot. It cannot reread mutable host data. Length digits consume ingress work before their value is trusted. A checked count cannot allocate unchecked contents.
IngressLimits names finite work, allocation, input, and diagnostic ceilings from the trusted product envelope. Their numeric values remain under cost-model-freeze. A byte protocol that uses Datum framing for its records still uses ingress events for that outer transport. The nested canonical guest input uses the codec events below exactly once.
A refused logical ingress reservation returns admission and host.envelope. Its contract is the trusted ingress envelope identity. Its reason is unsupported-limits. Failure to secure that envelope before parsing uses physical-capacity. Neither refusal creates request identity, a canonical evaluation outcome, or an evaluation receipt. A product returns the complete refusal report when the reserved terminal area remains available. An actual loss of host infrastructure remains a host failure.
Host output operation
Ordered events
Account
Count a report, artifact wrapper, or command envelope
egress.measure before each record and field sizing step
Trusted EgressLimits
Retain the complete output span
egress.reserve-output for the measured complete span, then physical output allocation
Trusted EgressLimits
Encode its bytes
egress.write-byte per octet
Trusted EgressLimits
Publish a completed span
egress.publish
Trusted EgressLimits
Normal egress follows one order: measure the complete candidate record and its fields, reserve the complete output, allocate its physical backing, write all octets, then publish. Each egress.measure precedes its sizing effect. Visit a record before its fields, fields in unsigned UTF-8 wire key order, and each field before its nested record value. Visit vectors in index order. An already retained, validated bytevector packet contributes its exact stored length. Other packet inspection or sizing requires previously secured host work. A cached packet length never skips the normal candidate's named record and field measurements. Lengths and intermediate sums use exact nonnegative integers. Host address width changes neither the size nor the traversal.
Before conversion or measurement, secure finite host conversion workspace from the admitted bounds. It covers traversal and ordering state, metadata conversion, exact size arithmetic, and any required nested-packet sizing. Its effects still follow their declared host reservations. Conversion work remains charged to its host account. The workspace is separate from the physical output buffer and borrows no guest evaluation or result capacity.
After every record and field measurement succeeds, egress.reserve-output atomically reserves the complete output span and remaining host requirements. Successful reservation permits physical output allocation. Each egress.write-byte then reserves its work before writing that octet. It does not charge the reserved output octets again. egress.publish follows the last successful byte write and publishes one complete packet. A refused measurement or output reservation performs none of its effects or later steps. Physical allocation or writing failure publishes no normal packet prefix. Previously committed charges remain; discarding an unpublished candidate gives no refund.
Logical output bounds are admitted before ordinary operation work, as required by the channel-forms Rule. An insufficient logical bound is an admission refusal there. It cannot become a new admission failure after evaluation. A later physical allocation failure is a host failure and preserves completed data. Normal output allocation and writing retain the separately secured emergency support.
EgressLimits names finite work, allocation, output, and diagnostic ceilings. Their values remain under the cost model freeze. The host secures support for the admitted output bounds before execution. Wrapper bytes, package metadata, localized text, and command framing never spend the guest result channel. A host output failure preserves every already completed language outcome and receipt eligibility. It is reported through the existing host transport contract and the reserved terminal representation.
codec-allocation per Datum node in depth-first car, cdr, and element order
Datum component path
Host record order
record-order for the complete finite name collection
Whole record path
Host record keys
record-key per name in canonical UTF-8 order
field(key) and canonical field index
Host record values
record-field, recursively convert the value, then codec-allocation for its association data
Canonical field index and value path
Input acceptance
request-seal after canonical validation and materialization
Selected entry input boundary
Entry result count
result-check after entry and its guards have returned
Selected entry output boundary
Result Datum validation
datum-validate for the complete result in depth-first order
Selected entry output component path
Encoding size pass
codec-value per node, codec-integer per numeric or value length field, codec-scalar per text scalar, then codec-integer for the completed payload length
Output component and field path, then field(frame-length)
Result packet reservation
result-channel, then codec-allocation for the complete encoded buffer
field(packet)
Packet emission
codec-byte per output octet in grammar order, then codec-frame at completion
Output byte offset, then field(close)
The input boundary uses the selected entry lambda occurrence when a verified program is available. Before request identity creation it remains a program-local site with no request identity. A transport or preparation report without a verified program uses its operand and byte coordinates. It cannot fabricate a qualified program site.
The first missing octet attempt still has its work reservation. It consumes no input octet. Every consumed input packet octet has one input-channel charge. Packet boundary and end checks do not consume another octet. Codec traversal state uses logical allocation, not guest call-frame capacity.
All structural and canonical validation finishes before decoded Datum materialization. No announced length allocates a result container before that validation. Materialization reserves the parent node before descending to its children. Physical assembly may differ without changing these events.
Encoding validates the Datum before its size pass. An entry's complete result validation supplies that check. Standalone encoding runs the same datum-validate traversal. The size pass precedes the complete result-channel reservation for evaluation output. Record admission uses the profile report axis for its conversion output instead. Its profile-report reservation covers the complete packet before emission. Output octet events keep their work requirements without charging that channel a second time. No result bytes are published until all emission events succeed.
Host record key ordering reserves the whole ordering operation before it starts. Its requirement depends on the complete name collection. Native enumeration and sorting algorithms add no semantic events. Host record adaptation and its output encoding use the profile host account and yield canonical input bytes. It never adds conversion events to the base evaluation stream. The evaluator then decodes those canonical bytes once under EvaluationLimits. An already canonical association list follows that same evaluation stream. Profile-only checks retain the profile host account.
Situation
Ordered action
Result
Check detects a source, admission, language, or boundary failure
Stop ordinary events, then attempt diagnostic-payload
Commit that detected failure only if its payload reservation succeeds
Automatic guest Condition
The successful diagnostic-payload constructs its typed fields, Condition, and raised occurrence
No second condition-construct charge for the same automatic payload
Explicit make-condition
Its field checks, then condition-construct
An immutable Condition with no raised occurrence
Explicit raise
condition-raise, then diagnostic-payload, then commit the new occurrence
The current raise site supplies its failure location
Payload reservation refused
Commit the refusal at diagnostic-payload
No truncated original Condition and no guest recovery
Resource reservation refused
Commit its axis, event, and site in the reserved emergency area
Do not attempt another diagnostic-payload reservation
Already committed first failure
Preserve it during trace, presentation, and transport
A later host report cannot replace that semantic cause
diagnostic-payload belongs to the account that performs the failed check. Its site keeps that occurrence and component path with role diagnostic-payload. It reserves the complete typed diagnostic payload and any required internal Condition storage before construction. The selected diagnostic codec determines its exact payload octets. All fields remain complete.
Before canonical input acceptance, payload exhaustion uses admission and input.resource. After acceptance it uses evaluate and resource.exhausted. Preparation payload exhaustion uses prepare and resource.exhausted. The stage keeps the interrupted preparation or evaluation stage. These are the existing diagnostic identities.
The emergency terminal representation uses no new guest reservation. Its finite area is secured before the corresponding work begins. Human rendering and optional trace are separate from committing the canonical first cause.
The failure stage follows the operation that was interrupted. Diagnostic-payload keeps that stage.
Source normalization, module form checks, binding prechecks and publishing
normalize
Dependency, cycle, import, name-use, and export resolution
resolve
Bundle names, fixed library validation, entry checks, canonical record construction, every prepared event, and graph capture, validation, projection, and export
prepare
Canonical input decoding, materialization, and request-seal
input-decode
Module initialization, ordinary evaluation, library operations, and entry invocation
entry
External result count and complete Datum validation
result-check
Output codec size pass, result-channel, packet allocation, and output emission
result-encode
Profile and ingress work keep their own host phase and account. They do not acquire a canonical evaluation outcome by using the same payload construction protocol.
Untrusted bytes cannot provide their own parsing allowance. Charging canonical input work before identity creation closes a free decoding path. A separate failure payload reservation preserves the first cause even when reporting is expensive.
Complete records and fields are measured, and host conversion support stays separate from output backing.
Charge input decoding before request identity exists
This order applies only when evaluation reaches the atomic event. Earlier arity, domain, and traversal checks keep their own event order. Each atomic event reserves at most one semantic channel. Work across several channels uses a declared sequence of events.
Optional trace saturation and emergency reporting remain separate. Returning or replacing a frame updates active capacity. It never reverses earlier cumulative charges.
8.12 Order the axes within one reservation
At one atomic event, check work first, logical allocation next, frames next, and the event channel last. Skip axes the event does not require. Commit the event charges and effect only after every required check succeeds.
Several budgets can be insufficient at the same event. One ordered check and atomic commitment preserve the same first axis without refunding a partial event.
Resource axes have a fixed check order and atomic commitment.
A reservation succeeds when the resulting charge is equal to its limit. It fails when the resulting charge exceeds the limit. Limits and charges use exact arithmetic with checked accounting.
Boundary examples name symbolic positive totals from the selected model. The future adapter must derive those totals from the contract. An observed execution does not supply an expected total.
8.13 Accept equality and reject an excess
A reservation accepts a resulting charge equal to the limit. It rejects a resulting charge above the limit before the event effect. Accounting arithmetic cannot wrap or depend on host word size.
Boundary requests need one portable answer. Exact checked accounting prevents overflow from admitting work outside the limit.
The result is atomic. Encoding reserves before creating or emitting result data. Exceeding the result budget ends with a resource stop and no successful result prefix.
The host reserves a separate finite emergency area for a terminal report before evaluation. Diagnostic expansion cannot hide the first resource cause. Optional trace follows the trace-isolation rule. Its reserved capacity is separate from guest resource accounts.
8.14 Reserve channels and return one atomic outcome
Input, result, and diagnostic processing use finite channel budgets. A result budget failure returns no successful result prefix. Terminal reporting uses reserved emergency space. Optional tracing follows the trace-isolation rule.
A final wire size check does not bound work already spent constructing a result. Trace must not create a second execution semantics.
8.15 Count canonical channel octets
Input, result, and diagnostic channels count octets. Each complete encoded packet includes the framing assigned to it below. Counters and limits are exact nonnegative integers. The inclusive limit Rule applies unchanged.
A host character count, memory capacity, pointer width, compressed representation, or rendered text length cannot replace the canonical count. A channel reservation happens at its named event. A reservation never charges the same semantic octet twice.
Account and channel
Counted octets
Reservation
Preparation input from source
Each exact submitted module source span
prepare.capture-source
Preparation input from prepared bytes
The complete selected resolved/1 or bytecode/1 payload
prepared.capture-input
Preparation input from graph or map
The complete GraphBytes or SourceMapBytes packet
graph.capture-input
Preparation result from program export
The selected canonical resolved/1 or bytecode/1 payload
result-channel before the first prepared write
Preparation result from graph or map export
The complete GraphBytes or SourceMapBytes packet
result-channel before the first graph write
Evaluation input
One complete canonical lispex.datum/2 packet
codec-byte for each consumed octet
Evaluation result
One complete canonical lispex.datum/2 packet
result-channel after sizing and before output buffer allocation
Preparation or evaluation diagnostic
Complete DiagnosticPayloadBytes for the selected typed diagnostic
diagnostic-payload before the failure commits
Profile host input adaptation
Its canonical host conversion and encoding work under the profile host contract
record and codec events assigned to that host account
Host transport input
The exact selected ABI or command operand frame
Trusted IngressLimits
Host transport output
The complete report, command, or artifact wrapper span
Trusted EgressLimits
Optional trace
Its complete header, record frames, and footer
The separate trace reservation Rule
The report contract defines DiagnosticPayloadBytes. The diagnostic channel counts that complete packet. The outer report and command framing use the host envelope.
The input Datum count includes its magic, payload length, tag bytes, and every field byte. A failed attempt to read beyond the captured end charges work but no absent octet. Source, prepared, and graph captures charge their whole span once. Nested validated spans retain their work and storage events without a second input charge.
The successful result packet is atomic. Its full result-channel reservation precedes allocation and emission. Later codec-byte events charge their work without charging output octets again. A failed encoder publishes no successful result prefix.
Artifact metadata, package records, command framing, and delivery buffers belong to the trusted host transport envelope. They cannot change evaluation channel counts. The host secures those finite envelopes before performing the corresponding work. Normal report and command encoding follows complete record/field measurement, output reservation, physical allocation, byte writing, and publication. The boundary event Rule fixes that order. Prepaid finite conversion workspace belongs to the host account. Neither conversion workspace nor wrapper output debits the guest result account. A logical egress envelope refusal occurs during admission from the complete admitted bounds. It cannot become a new admission failure after a language value or cause has committed. A later physical or delivery failure retains the completed outcome and its receipt eligibility. Host record adaptation produces canonical input bytes under its separate host work contract. The evaluator then processes those bytes by the same input schedule as any other canonical input.
Channel octets are distinct from logical allocation units. This Rule selects no tariff coefficient, allocation size, default limit, representation maximum, or physical envelope. Those values remain under cost-model-freeze.
Canonical octets provide one measurable unit on every product. Explicit packet boundaries prevent wrappers and display choices from changing a language result. Separate host and trace accounts retain their own finite bounds.
Before each performed phase, the host secures a finite emergency area for its terminal core and the complete surrounding report framing. The area uses the admitted limits and the trusted host envelope. Its physical backing, finite cursor state, and serialization work capacity exist before any ordinary conversion, measurement, reservation, allocation, or effect in that phase.
EmergencyTerminalBytes has the exact schema below. The command result contract places it in Reports.terminal as the final failure payload. It is never a replacement ABI protocol. A complete reply keeps the host interface success status even when this payload reports a refusal or terminal failure.
The first committed cause for a phase is immutable. A later phase can report its own refusal while preserving the completed evaluation cause, outcome, receipt, and evaluation classification. Emergency serialization preserves its complete diagnostic bytes and exact location. It cannot truncate fields, choose another code, or create guest recovery. A resource refusal constructs its fixed terminal diagnostic from the already available stage, axis, event, and location metadata. It requests no further guest reservation.
EmergencyTerminalBytes is one canonical lispex.datum/2 packet. Its root is the closed record below. A record is an ordinary proper association list of dotted pairs. Keys are strings in unsigned UTF-8 order. Byte fields are bytevectors. Every field is required. Unknown fields, duplicate fields, and noncanonical order are rejected.
Field in wire key order
Type
Meaning
cause
Bytevector
Complete DiagnosticPayloadBytes for the committed first cause
format
String
Exactly lispex.terminal/1
location
TerminalLocation
The exact source, wire, or canonical location below
program
False or bytevector
Verified IdentityBytes for ProgramIdentity when known
request
False or bytevector
Accepted IdentityBytes for RequestIdentity when known
The identity bytes use the identity contract. Unknown identities use false. No guessed digest, local handle number, source label, or self digest is allowed. A request identity appears only after canonical input acceptance. The enclosing report keeps the existing outcome and receipt eligibility rules.
TerminalLocation kind
Exact fields in wire key order
Field types
none
kind
String none
program
kind, site
String program and a bytevector containing exact CanonicalSiteBytes
source
kind, module, offset
String source, the decoded module name string, and NatText for the exact event target octet fixed below
wire
kind, offset, operand
String wire, NatText for the exact wire offset, and an InputOperand string
NatText is the exact nonnegative decimal string from the diagnostic field grammar. InputOperand uses the existing diagnostic enum. A missing octet uses the attempted end offset. A source coordinate uses the immutable submitted module. The surrounding preparation report binds that source submission. A program location requires a verified program identity in the outer program field.
CanonicalSiteBytes is the program-local site record. Program and request identities stay outside that record. A failure path is retained in full. Repeated visits do not add a counter or call stack to it.
The cause bytevector decodes to the already committed phase, code, and typed data. The original diagnostic codec remains fixed. A consumer checks that imported payload under its canonical decoder. Emergency wrapping cannot repair it. A malformed product observation remains an engine defect under the existing diagnostic contract.
Source offsets start at zero in the exact immutable module source. The event retains this coordinate before inspecting its target. No final report rescans source to find it.
Failed source event
Exact source offset
prepare.capture-source
Zero
prepare.decode-step
The initial octet of the next scalar attempt, or source byte length for the final end check
prepare.read-step
The initial octet of the next decoded scalar, or source byte length for the final end check
prepare.read-enter
The initial octet of the opening marker
prepare.read-node
The initial octet of the completed token, datum, or abbreviation
prepare.normalize-node
The initial octet of the selected form
Group envelope or member shape
The initial octet of that group or member form
Binding identifier, duplicate, or publish check
The initial octet of the selected name-position datum. A duplicate selects the later declaration
Recursive lambda-head check
The initial octet of the selected initializer
Clause or member envelope check
The opening octet of that clause or member form
Import module target or cycle-closing edge
The initial octet of that import module identifier
Imported public name
The initial octet of that imported name identifier
Local import alias check
The initial octet of that local alias identifier
Export local-name or public-name check
The initial octet of the specific local or public identifier being checked
Entry target check
The initial octet of the declared entry identifier
Missing root entry
The initial octet of the root module form
Resolved name use
The initial octet of that use token
A failed check that has no selected module-source target uses wire or none. A failed reservation and its later diagnostic-payload event keep the retained target coordinate. The diagnostic-payload role does not move the original source target.
Wire offsets start at zero in the complete named immutable public operand. That operand includes its public packet header. The following table selects the base.
Public operand being checked
InputOperand and offset base
Outer HostRequestBytes
request, first request packet octet
Selected SourceBundleBytes
bundle, first bundle packet octet
Selected PreparedArtifactBytes or evaluator artifact
artifact, first artifact packet octet
Selected GraphBytes or SourceMapBytes
graph, first graph or map packet octet
Selected canonical Datum input packet
input, first Datum packet octet
Separately submitted limits, profile, receipt, evidence, or trust operand
Its exact InputOperand name, first complete operand octet
Selecting a public operand is part of the host request grammar. A nested foreign field does not select a new operand. The parser retains each nested bytevector's payload base while reading it. It adds that retained base to a nested decoder offset. An embedded prepared failure therefore uses its exact position in the selected artifact or graph packet. Count and field checks use the first octet of that field. Compound checks use the first octet of that record. Final end checks use the complete operand length. A missing field uses the attempted end offset. These offsets require no postfailure copy, scan, or digest.
The none location is allowed only when the operation has not selected a program site, source target, or wire operand coordinate. Its typed diagnostic data still preserves any command argument or host field identity.
The host determines a finite bound before starting the corresponding work. These names denote bounds supplied by the selected resource and transport model. They do not assign numeric values.
Bound
Required coverage
IdentityBound
Every identity that can appear in the selected interface and report contracts
LocationBound
Every canonical site, source coordinate, and wire coordinate allowed by the admitted program, input, and limits
DiagnosticBound
The complete committed diagnostic payload allowed by that phase's diagnostic limit, plus the closed resource and host refusal forms
EmergencyTerminalBound
The maximum canonical packet size of the exact terminal schema for those bounded fields
EmergencyFramingBound
The complete enclosing report and command framing for that terminal payload
EmergencyCursorBound
Finite traversal and continuation state for every record and field in the terminal and its complete surrounding framing
EmergencyWorkBound
Finite metadata inspection, exact size arithmetic, record framing, and copying needed to serialize those bounded bytes
EmergencyTerminalBound is the maximum encoded length over those admitted fields. EmergencyFramingBound includes every required outer field and delimiter. It also covers retained outcome and receipt packets, completed report slots, and separate trace framing. The command envelope fixes their fields. The terminal core is the smallest closed EmergencyTerminalBytes record for its admitted fields. Complete record framing embeds that exact core in Reports.terminal and supplies every required CommandResult field. Copying a prebuilt core into retained framing and writing the framing directly must produce the same canonical bytes and preserve the same data and cause. A channel requiring CommandResultBytes receives that complete record, not a bare terminal core.
Terminal backing, framing backing, EmergencyCursorBound, and EmergencyWorkBound are secured before the first normal operation. Ordinary work begins only after all four requirements succeed. Byte capacity alone is insufficient. Cursor growth, metadata conversion, size arithmetic, backing growth, and all work after refusal fit the secured support. Emergency serialization requires no postfailure acquisition, normal egress retry, or guest reservation. These bounds borrow no guest work, allocation, input, result, or diagnostic capacity. Their numeric values and physical representation remain under cost-model-freeze.
Before request identity exists, the trusted ingress envelope and selected input limits bound the report. Before source or prepared work, the preparation envelope bounds it. Before admitted evaluation, the verified program and EvaluationLimits bound it. Profile work and host output retain their own finite emergency support.
A phase is not admitted when terminal backing, framing backing, cursor state, or serialization work support cannot be secured. No ordinary phase event begins. Partial support never counts as a complete reply. The existing admission/host.envelope diagnostic with reason physical-capacity reports that inability when an already available reporting boundary can produce a complete refusal. An actual loss of host infrastructure remains a host failure. The host never silently lowers a requested semantic limit.
Emergency serialization reads only bounded metadata and already retained diagnostic bytes. It cannot traverse guest data, format a new message, or invoke guest code. The failed event's path is already represented in the reserved location state. Resource reporting uses its closed diagnostic fields. The emergency area is written once for that phase's committed terminal cause. Before entering the failing work, the host binds retained payload, receipt, completed report slots, standalone evidence, and trace to the same immutable operation. Emergency framing consumes those retained bindings without postfailure rehashing, revalidation, or discovery.
If a guest Condition has already committed, its payload remains complete even when later human expansion or transport fails. If diagnostic-payload itself was refused, the core records that resource refusal. An ordinary diagnostic limit can be zero and the reserved terminal representation still exists. This does not grant ordinary diagnostics extra capacity.
A later qualification, evidence, trace, or delivery failure keeps every completed report slot, primary payload, receipt packet, and completed trace snapshot. A trace still in progress follows its existing reservation, saturation, and footer rules until its snapshot completes. Incomplete normal report slots remain absent. Emergency framing keeps every completed slot within its secured bound. The completed language outcome and receipt eligibility remain unchanged. An emergency payload alone creates no evaluation receipt.
A completed language failure keeps outer status 20; a completed resource stop keeps outer status 21. A later qualification or evidence refusal preserves that exact status, including when normal profile reporting fails and requires emergency framing. The later phase retains its own first refusal in its report or terminal payload. The completed evaluation diagnostic, qualified site, outcome bytes, and receipt bytes remain unchanged. Status selection uses retained evaluation classification without reparsing the receipt or inferring it from the emergency diagnostic. The profile contract still determines which later work is performed. This framing rule adds no returned-Datum schema traversal after failed evaluation. Physical delivery and packet replacement follow the command result contract.
A final resource failure must remain reportable after an ordinary channel is full. A pre-reserved finite representation keeps that guarantee without allowing a new unlimited formatting path. Preserving the original bytes keeps failure identity independent of presentation.
Terminal core bytes and complete record framing share one byte contract. Backing, cursor state, and work capacity are secured before ordinary work. Retained evaluation classification preserves status 20 or 21 during a later profile refusal.
Keep a resource cause when ordinary diagnostics have no capacity
8.17 Reserve whole trace frames in a separate account
TraceOptions is false or a closed record with allocation, capacity, and work. False disables trace. Each record field is an exact finite nonnegative integer. Capacity counts encoded trace octets. Work and allocation use their separate trace requirement functions. They never debit the semantic request.
The trace record contract fixes the header, record frames, and footer. The recorder reserves the header and complete footer before admitted evaluation. It then reserves one complete framed record at a time. The first trace reservation failure permanently stops recording. The already complete prefix remains available.
Trace exhaustion changes no guest check, event, first failure, result, canonical outcome, or evaluation receipt. The recorder adds no guest event after saturation and keeps no growing trace-only counter. It allocates no saturation message.
The following reservation names belong only to the trace account. They are not guest EventIdentity values and are not traced recursively.
Trace reservation
Reserved work and storage
Capacity unit
trace.open
Bounded header metadata, identities, encoder state, and final footer
Complete header and two-octet footer
trace.measure
Bounded inspection of the next event's existing metadata and exact frame-length calculation
No stored frame
trace.record
Encoding and retaining the complete measured frame
The 01 marker, its minimal length prefix, and the entire event payload
trace.close
Work already reserved by trace.open for writing the selected footer
The footer already reserved by trace.open
Trace work is reserved before metadata inspection. The measure reservation checks work and allocation atomically before that bounded scan or its workspace. Frame calculation reads no guest payload. The remaining record reservation checks work, allocation, then capacity. It commits those requirements atomically. Earlier successful trace work is not refunded if that reservation fails.
The stored record unit is the complete TraceRecord byte span. It is not an event count, guest work unit, UTF-16 count, or unframed payload size. The marker and every length digit count. The header and footer also consume capacity. A record fits when its total leaves exactly the reserved footer capacity. A rejected record contributes no bytes.
If the header and footer cannot fit, no TraceBytes value is created. The separate host trace status reports unavailable. The requested language evaluation retains its original request and limits. If trace is not requested, the host reports disabled and creates no trace state.
Once a stream is open, a work, allocation, or capacity refusal marks its reserved footer with completion 01. Every later observation is ignored. A complete stream uses completion 00. Host interruption before Terminal uses completion 02 unless saturation already fixed completion 01. A stored Terminal keeps completion 00 despite later delivery failure.
The only separate host trace status values are disabled, unavailable, complete, capacity-exhausted, and host-interrupted. Complete and interrupted streams still use their exact TraceBytes encoding. Status metadata is not part of the canonical evaluation outcome or receipt.
Trace storage may be provisioned before input decoding. Recording begins only after canonical input admission supplies the verified program and request identities. It begins before module initialization. Input decoding before request identity and later profile or transport work remain outside that stream.
Trace requirement coefficients, allocation units, finite defaults, maximum capacity, and physical backing remain under cost-model-freeze. No implementation-specific chunk size is selected.
Host trace status
Exact condition
disabled
TraceOptions is false
unavailable
trace.open cannot reserve the complete header and footer
complete
A produced TraceBytes ends with 00 00
capacity-exhausted
A produced TraceBytes ends with 00 01 after any trace work, allocation, or capacity refusal
host-interrupted
A produced TraceBytes ends with 00 02
The capacity-exhausted status names a stopped recording account. It does not select a guest resource axis. Status metadata remains separate from the complete trace packet and the semantic result.
A whole frame can be retained or omitted without producing a broken stream. A separate finite account prevents observation from changing the computation it records. Reserving the footer first makes saturation reportable without another allocation.
Reserve a trace marker and its length with the payload
Before execution the host checks that it can safely support the admitted logical limits. A host that cannot reserve the required physical envelope rejects admission. It does not silently lower the request limits.
For an admitted request, logical limits must stop resource growth before physical protection does. A host interruption or engine defect remains a distinct failure. The portable receipt rule defines which completed outcomes a receipt can bind.
8.18 Admit only a supported physical envelope
The host admits a request only when it can support the selected logical limits within its physical envelope. It preserves those limits. A physical failure does not become a deterministic resource stop.
Use public procedures to inspect and construct immutable data. Guest library code and the native kernel share one resource contract.
Scope
Rule authors use public procedures to inspect and construct immutable data. Each procedure follows the Lispex 2.0 value, condition, and resource rules.
A public procedure is a callable binding supplied by the standard library. Its public name describes a language operation. Its implementation can use guest code or a native kernel operation.
These semantic examples use symbolic finite limits. Native, npm, and WASM plans remain not run until their 2.0 products and observation adapters are available.
Procedure contracts
A procedure contract names its argument count and domain. It defines the returned value and the first applicable condition. It also defines traversal order and the resource events needed for its work.
Procedures defines calls and internal values. Conditions defines catchable failures and terminal stops. Resources defines reservations and finite budgets.
A public name does not require a native handler. The procedure catalog fixes every public name. Its public alias list is empty. The number of public names and the number of native operations are separate quantities.
9.1 Public procedure contracts
Every public procedure follows its declared argument domain, result, failure, and evaluation order. The complete catalog fixes the exported names and their contracts. The standard library supplies data operations and guest procedure composition. Removed guest effects are unavailable.
A procedure must keep its meaning when its implementation moves between guest code and the native kernel. Library access cannot introduce an external capability.
Complete operator and operand evaluation before procedure checks. Check the declared arity first. Then check argument domains from left to right. Finish all required structural checks for one argument before advancing to the next. Apply the row checks in their written order. Make-condition uses its separate constructor protocol.
Domain check
Traversal
L
Visit the entire pair spine and its final tail
DL, CL, OL
Finish the spine, then check element domains from the head
A
Finish the spine, then check each entry pair and its complete Datum key in list order
D
Use the Values depth-first Datum traversal
S, numeric, and scalar types
Check the current value before the next argument
A constructor accepts internal Values wherever its table uses V. Portable-data checks occur only where a domain requires them. Proper-list checks finish before any callback. Datum equality validates the complete left operand before the complete right operand.
An invalid argument produces the declared language condition. A resource refusal can precede that condition only at an earlier required reservation. The first failure ends the procedure. Later argument checks, comparisons, callbacks, and allocations do not run after that failure.
Domain checks emit argument-check and their required traversal events. The row resource events describe the subsequent checks and result work. Derived procedure calls retain the events of their specified inner calls.
The resource event catalog defines event names, reservation points, and canonical sites. Numbers and Values select those events for their operation schedules. The library rows here apply the same event definitions.
Every event uses reservation before effect and the resource axis order. A refusal produces no partial result and refunds no committed work. Storage reuse and native fast paths preserve these semantic events.
The selected resource model supplies complete requirement vectors. Coefficients, allocation units, default finite limits, physical envelopes, and final native kernel membership retain their separate pending contracts.
Pure procedures can still expose different first failures. Completing the declared checks fixes that choice before result work starts. Named resource events place expensive validation, arithmetic, text work, and callback results inside finite execution.
9.3 Use the complete public procedure catalog
The tables below define every public standard library procedure. Their argument domains, arities, results, failures, and resource events are normative. An unlisted standard library export is unavailable. The public alias list is empty. Source forms and user-defined procedures follow their own binding contracts. A host registry cannot add a public library procedure. This inventory does not select native kernel membership.
The tables use the domains below. Arity counts supplied arguments. A trailing plus in an arity admits every greater finite count.
Domain
Values
V
Any single internal value, including a procedure or Condition
D
Portable Datum
S
A Boolean, exact number, character, symbol, or empty list
B
Boolean
N
Exact number
I
Exact integer
U
Exact nonnegative integer
O
Exact integer from zero through 255
C
Unicode scalar character
T
Raw scalar string
Y
Raw scalar symbol
P
Procedure
R
Pair with arbitrary internal components
L
Finite proper list with arbitrary internal elements
DL
Proper list whose elements are Datum
CL
Proper list whose elements are characters
OL
Proper list whose elements are octets
A
Proper list of pairs with Datum keys and arbitrary internal cdr values
F
Vector with arbitrary internal elements
X
Bytevector
Q
Condition
Scalar and Datum domains use the Values definitions. A vector or list may contain a procedure internally. That aggregate then fails the Datum predicate and portable boundary validation.
All constructors create immutable values. Constructors with a count require an explicit fill value. Empty construction still validates every supplied argument. Counts have no host word limit. Finite work and logical allocation govern construction.
Each listed procedure returns one value unless its row specifies an internal result sequence or no normal result. The values, apply, and call-with-values procedures can return any finite count of internal values.
Arithmetic uses exact numbers. Successful results are integers or reduced rationals. Arithmetic never preserves a display scale.
Variadic addition starts from zero. Variadic multiplication starts from one. Subtraction and division start from their first operand when more than one is supplied. Each proceeds from left to right. A unary division checks its sole operand as the divisor. A longer division checks every operand after the first as a divisor.
All numeric argument domains are checked before zero-divisor checks. The zero-divisor checks finish in argument order before arithmetic begins. An earlier zero, false comparison, or selected minimum does not skip a later argument check.
The remainder has the dividend sign when nonzero. Modulo has the divisor sign when nonzero. Both return zero as the integer zero. The gcd and lcm results are nonnegative. The power with exponent zero is one, including zero raised to zero. The expt catalog row defines the failure for a zero base with a negative exponent.
The number->string procedure uses the canonical text forms below. Its arity is exactly one. It performs no rounding or locale formatting.
Value
Text
Integer zero
0
Positive integer
ASCII decimal digits with no leading zero
Negative integer
- followed by the positive magnitude digits
Nonintegral rational
Canonical numerator text, /, and canonical positive denominator text
The rational form has a nonzero numerator and a denominator greater than one. Source decimal spelling never changes this text.
Indices count elements from zero. Strings count Unicode scalars. Bytevectors count octets. They use exact integer indices independent of host width.
Reference operations require an index below the length. List-tail also admits the length and returns the empty suffix. A slice admits endpoints from zero through the length. Its start is included and its end is excluded. Slice checks run after argument domains. They check start bounds, end bounds, then start order. A start greater than end produces domain.range with invalid-slice-order on the ending bound argument. Equal endpoints return an empty sequence of the same kind.
String-length, string-ref, and substring first scan the entire input in scalar order to establish its length. String-ref checks bounds after that scan, then scans from the start through its selected scalar. Substring checks both bounds and start order after the length scan. It next visits scalar indices from zero up to but excluding end. It copies indices from start up to but excluding end. Metadata length caches preserve these scan events.
Vector and bytevector length checks read their stored element count through sequence-step. An indexed call reads that count once for its bounds checks. A successful reference then visits its selected element. A successful slice visits its selected elements in ascending index order after allocation. Each slice endpoint must satisfy 0 <= endpoint <= length before checking start <= end.
Append accepts only proper lists. It returns a proper list even when given no arguments. Member validates its needle and every list element as Datum before comparing. Assoc validates every entry pair and Datum key before comparing. Missing matches return #f. Search uses structural equality and stops at the first matching element or key.
Raw string and symbol comparisons inspect exact scalar sequences. String order is lexicographic scalar order with the shorter equal prefix first. Character order is numeric scalar order. Every argument type is validated before a comparison can return false.
Each adjacent string or symbol comparison starts at scalar index zero. It inspects the left position before the right position. Raw comparisons emit text-scalar-scan for each scalar visited. A paired comparison emits compare-scalar and stops that pair at its first unequal scalar or its first sequence end. Sequence ends supply the shorter-prefix comparison. The next adjacent pair begins only when the required relation holds. Otherwise the procedure returns false. Folded comparisons use the same paired positions after all folding work. Their paired visits use compare-scalar.
The UTF-8 conversion procedures preserve every scalar. The bytevector contains only UTF-8 text bytes. Encoding uses the shortest representation and adds no marker. Decoding retains U+FEFF even at the start. It rejects overlong forms, isolated continuation bytes, truncation, surrogates, and scalars above U+10FFFF. Unassigned scalars and noncharacters remain valid data.
The decoder scans from the start. Each byte check rejects as soon as the inspected prefix cannot begin a valid shortest UTF-8 scalar. This includes the second-byte bounds imposed by E0, ED, F0, and F4. The first such check produces domain.range with invalid-utf8 on the bytevector argument. Its detection site is that byte's sequence-step, even when an earlier byte began the sequence. If a required continuation is missing, the detecting visit uses the next required byte index at the input end. The diagnostic-payload event keeps that occurrence and path with its own role. The Condition retains its existing fields and carries no byte position. It never substitutes replacement text. These procedures run during evaluation and their domain failures are ordinary language conditions. A result appears only after the complete conversion succeeds.
The six condition procedures use the Condition catalog. That catalog defines their internal value, field schemas, constructor order, accessors, and raised occurrences. The public rows here select their signatures and resource events. The constructor applies the imported validation order after ordinary operand evaluation and its arity check. Resources defines each selected event and reservation point.
The following table defines type predicates.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
boolean?
1
V
Boolean for membership in the Boolean domain
None after the shared checks
None after the shared checks
number?
1
V
Boolean for membership in the exact number domain
None after the shared checks
None after the shared checks
integer?
1
V
Boolean for membership in the exact integer domain
None after the shared checks
None after the shared checks
pair?
1
V
Boolean for membership in the pair domain
None after the shared checks
None after the shared checks
null?
1
V
Boolean for membership in the empty list domain
None after the shared checks
None after the shared checks
symbol?
1
V
Boolean for membership in the symbol domain
None after the shared checks
None after the shared checks
char?
1
V
Boolean for membership in the character domain
None after the shared checks
None after the shared checks
string?
1
V
Boolean for membership in the string domain
None after the shared checks
None after the shared checks
vector?
1
V
Boolean for membership in the vector domain
None after the shared checks
None after the shared checks
bytevector?
1
V
Boolean for membership in the bytevector domain
None after the shared checks
None after the shared checks
procedure?
1
V
Boolean for membership in the procedure domain
None after the shared checks
None after the shared checks
scalar?
1
V
Boolean for membership in the scalar domain
None after the shared checks
None after the shared checks
list?
1
V
True for a proper list and false at the first nonpair tail
None after the shared checks
list-step along the spine through the final tail
datum?
1
V
True for Datum and false at the first non-Datum component
None after the shared checks
datum-validate in the Values traversal order
The following table defines booleans and equality.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
not
1
V
True exactly for #f
None after the shared checks
None after the shared checks
boolean=?
2+
B...
True when every adjacent Boolean is equal
None after the shared checks
compare-scalar on adjacent arguments until the first false comparison
eq?
2
S, S
Scalar value equality under the Values rule
None after the shared checks
compare-scalar
eqv?
2
S, S
Scalar value equality under the Values rule
None after the shared checks
compare-scalar
equal?
2
D, D
Structural equality under the Values rule
Validate the whole left Datum before the whole right Datum
compare-datum in the Values traversal order
The following table defines exact arithmetic.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
+
0+
N...
Left sum with identity zero
None after the shared checks
exact-arithmetic then rational-reduce for each declared result, then datum-allocate
*
0+
N...
Left product with identity one
None after the shared checks
exact-arithmetic then rational-reduce for each declared result, then datum-allocate
-
1+
N...
Unary negation or left subtraction from the first operand
None after the shared checks
exact-arithmetic then rational-reduce for each declared result, then datum-allocate
/
1+
N...
Unary reciprocal or left division from the first operand
After every numeric domain check, reject zero divisors from left to right
exact-arithmetic then rational-reduce for each declared result, then datum-allocate
=
2+
N...
True when each argument is equal to its successor
None after the shared checks
compare-scalar on adjacent arguments until the first false comparison
<
2+
N...
True when each argument is less than its successor
None after the shared checks
compare-scalar on adjacent arguments until the first false comparison
>
2+
N...
True when each argument is greater than its successor
None after the shared checks
compare-scalar on adjacent arguments until the first false comparison
<=
2+
N...
True when each argument is no greater than its successor
None after the shared checks
compare-scalar on adjacent arguments until the first false comparison
>=
2+
N...
True when each argument is no less than its successor
None after the shared checks
compare-scalar on adjacent arguments until the first false comparison
abs
1
N
Nonnegative magnitude
None after the shared checks
exact-arithmeticrational-reducedatum-allocate
min
1+
N...
The least value with the first argument retained on a tie
None after the shared checks
compare-scalar against the running selected value from left to right
max
1+
N...
The greatest value with the first argument retained on a tie
None after the shared checks
compare-scalar against the running selected value from left to right
numerator
1
N
Numerator of the reduced value, including its sign
None after the shared checks
exact-arithmeticdatum-allocate
denominator
1
N
Positive reduced denominator, or one for an integer
None after the shared checks
exact-arithmeticdatum-allocate
quotient
2
I n, I d
Integer n / d rounded toward zero
Reject zero d
exact-dividedatum-allocate
remainder
2
I n, I d
n - d * quotient(n, d)
Reject zero d
exact-divideexact-arithmeticdatum-allocate
modulo
2
I n, I d
n - d * floor(n / d)
Reject zero d
exact-divideexact-arithmeticdatum-allocate
gcd
0+
I...
Nonnegative greatest common divisor, with empty result zero
None after the shared checks
exact-arithmetic on the left reduction from zero, then datum-allocate
lcm
0+
I...
Nonnegative least common multiple, with empty result one and any zero producing zero
None after the shared checks
exact-arithmetic on the left reduction from one, then datum-allocate
expt
2
N base, I exponent
Exact integer power, with exponent zero returning one
Reject exact zero base with a negative exponent using domain.division-by-zero with argument 0
exact-arithmeticrational-reducedatum-allocate
zero?
1
N
True exactly when the input is equal to zero
None after the shared checks
compare-scalar
positive?
1
N
True exactly when the input is greater than zero
None after the shared checks
compare-scalar
negative?
1
N
True exactly when the input is less than zero
None after the shared checks
compare-scalar
even?
1
I
True exactly when the input is divisible by two
None after the shared checks
exact-divide
odd?
1
I
True exactly when the input is not divisible by two
None after the shared checks
exact-divide
quantize
3
N, I, mode symbol
Exact selected decimal grid value
The ordered checks in the Numbers rounding contract
exact-arithmetic for decimal digits, then datum-allocate
The following table defines pairs and lists.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
cons
2
V, V
Pair whose car and cdr are the two arguments
None after the shared checks
datum-allocate
car
1
R
First component
None after the shared checks
list-step
cdr
1
R
Second component
None after the shared checks
list-step
caar
1
V x
(car (car x))
car x then car of that result with each called operation retaining its own failure name
The declared call, argument-check, and list-step events of both nested procedures
cadr
1
V x
(car (cdr x))
cdr x then car of that result with each called operation retaining its own failure name
The declared call, argument-check, and list-step events of both nested procedures
cdar
1
V x
(cdr (car x))
car x then cdr of that result with each called operation retaining its own failure name
The declared call, argument-check, and list-step events of both nested procedures
cddr
1
V x
(cdr (cdr x))
cdr x then cdr of that result with each called operation retaining its own failure name
The declared call, argument-check, and list-step events of both nested procedures
list
0+
V...
Proper list of arguments in their supplied order
None after the shared checks
datum-allocate in argument order
make-list
2
U count, V fill
Proper list containing count copies of fill
None after the shared checks
traversal-state then datum-allocate for each result index in ascending order
length
1
L
Exact number of pairs counted by spine validation
None after the shared checks
datum-allocate
append
0+
L...
Proper list formed by concatenating every list in argument order
None after the shared checks
list-step and datum-allocate in argument and element order
reverse
1
L
Proper list with the elements in reverse order
None after the shared checks
list-step from the head and datum-allocate for each new front pair
list-ref
2
L, I index
Element at the zero-based index
Require 0 <= index < length
list-step for each cdr movement, then one for the selected car
list-tail
2
L, I index
Suffix after index elements
Require 0 <= index <= length
list-step for each cdr movement to the selected suffix
member
2
D needle, DL haystack
First matching suffix under equal?, or #f
Complete both Datum domains before searching
list-step then compare-datum in list order
assoc
2
D key, A entries
First pair with an equal? key, or #f
Validate every pair and Datum key before searching
list-step then compare-datum in entry order
Make-list completes both argument domains before construction, including when count is zero. For each result index i, it reserves one logical cursor position with traversal-state at result(0), element(i). It next reserves and creates that pair with datum-allocate at the same component path. Their extents are one retained position and two pair components. The next index starts only after that pair allocation succeeds. Count zero returns the empty list without either construction event. Counts remain exact mathematical integers.
List-ref and list-tail first complete the entire L domain, including its final tail. They next check the index domain and reserve a separate argument-check for its bounds. After successful bounds checks, each actual cdr movement emits list-step at the reached cdr path. List-ref then emits one list-step at the selected car path. List-tail returns the reached suffix directly. Index zero therefore adds no movement event for list-tail and only the car visit for list-ref. Neither operation adds a separate endpoint visit after this walk.
The following table defines list traversal.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
map
2+
P, L...
Proper list of one callback result per tuple
All list spines, equal lengths, callback arity, then one result per callback
traversal-statecallback-callresult-checkdatum-allocate per ascending index
for-each
2+
P, L...
One empty list after all callbacks
All list spines, equal lengths, then callback arity
traversal-statecallback-call per ascending index, discarding all callback values
fold-left
3+
P, V seed, L...
Final accumulator, or seed for empty lists
All list spines, equal lengths, callback arity, then one result per callback
traversal-statecallback-callresult-check per ascending index
fold-right
3+
P, V seed, L...
Final accumulator, or seed for empty lists
All list spines, equal lengths, callback arity, then one result per callback
traversal-state before descending callback-call and result-check events
filter
2
P, L
Proper list of elements whose callback result is not #f
Whole list spine, unary callback arity, then one result per callback
traversal-statecallback-callresult-check and datum-allocate for each retained element
find
2
P, L
First element whose callback result is not #f, or #f
Whole list spine, unary callback arity, then one result per callback
traversal-statecallback-callresult-check until the first true result
any
2
P, L
First non-#f callback value, or #f for no match or an empty list
Whole list spine, unary callback arity, then one result per callback
traversal-statecallback-callresult-check until the first true result
every
2
P, L
First #f, otherwise the last callback value, with #t for an empty list
Whole list spine, unary callback arity, then one result per callback
traversal-statecallback-callresult-check until the first false result
The following table defines vectors.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
vector
0+
V...
Vector of the arguments in order
None after the shared checks
datum-allocate then sequence-step in result order
make-vector
2
U count, V fill
Vector containing count copies of fill
None after the shared checks
datum-allocate then sequence-step in result order
vector-length
1
F
Exact element count
None after the shared checks
sequence-stepdatum-allocate
vector-ref
2
F, I index
Element at the zero-based index
Require 0 <= index < length
sequence-step
vector->list
1
F
Proper list of vector elements in order
None after the shared checks
sequence-step then datum-allocate per element
list->vector
1
L
Vector of list elements in order
None after the shared checks
datum-allocate then list-step and sequence-step in order
vector-append
0+
F...
Concatenated vector in argument and element order
None after the shared checks
Length sequence-step for every argument, complete result datum-allocate, then element sequence-step in argument and element order
vector-slice
3
F, I start, I end
Vector for the half-open range
Check start bounds, end bounds, then start <= end
datum-allocate then sequence-step in the selected range
Vector-append completes every argument domain before its length pass. In argument order it emits sequence-step at argument(i), field(length) before reading each stored length. It computes the exact total within those reserved steps. It then reserves and creates the complete result at result(0), with extent equal to that total. Only then does it visit the elements of each argument in ascending index order. Empty arguments retain their domain and length events but have no element visits. With no arguments, the only row event is datum-allocate at result(0) with extent zero. The bytevector-append row follows the same two passes with byte component paths.
The following table defines bytevectors and utf-8.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
bytevector
0+
O...
Bytevector of the octets in order
None after the shared checks
datum-allocate then sequence-step in result order
make-bytevector
2
U count, O fill
Bytevector containing count copies of fill
None after the shared checks
datum-allocate then sequence-step in result order
bytevector-length
1
X
Exact octet count
None after the shared checks
sequence-stepdatum-allocate
bytevector-u8-ref
2
X, I index
Octet at the zero-based index as an exact integer
Require 0 <= index < length
sequence-stepdatum-allocate
bytevector->list
1
X
Proper list of octet integers in order
None after the shared checks
Length sequence-step, then byte sequence-step and one combined integer-and-pair datum-allocate per octet
list->bytevector
1
OL
Bytevector of the listed octets in order
None after the shared checks
datum-allocate then list-step and sequence-step in order
bytevector-append
0+
X...
Concatenated bytevector in argument and octet order
None after the shared checks
Length sequence-step for every argument, complete result datum-allocate, then byte sequence-step in argument and octet order
bytevector-slice
3
X, I start, I end
Bytevector for the half-open range
Check start bounds, end bounds, then start <= end
datum-allocate then sequence-step in the selected range
utf8->string
1
X
String decoded with strict UTF-8
Reject at the first byte or required end that makes the current UTF-8 prefix invalid
Byte sequence-step through each complete scalar, then one datum-allocate for that scalar. Finish with the required end visit
string->utf8
1
T
Shortest UTF-8 bytes for the unchanged scalar sequence
None after the shared checks
One text-scalar-scan per scalar, then one datum-allocate per encoded octet. Finish with the required end visit
Bytevector-append uses the length and element passes defined with vector-append. Its allocation extent is the exact total octet count. Its element visits use argument(i), byte(j). Empty arguments still participate in the length pass.
Bytevector->list emits sequence-step at argument(0), field(length) once after its domain check. It then visits each octet at argument(0), byte(i) in ascending index order. Each visit is followed by one datum-allocate at result(0), element(i). That event reserves the complete exact integer and pair together before creating either. Its extent is three, comprising one integer component and the pair's two components. The next byte is visited only after that combined event succeeds. A zero length returns the empty list after the length visit with no component allocation or extra end visit.
UTF-8 conversion uses sequential input visits through the required end. Decoding visits bytes at argument(0), byte(i). As soon as one complete valid scalar is known, datum-allocate at result(0), scalar(j) reserves that result component with extent one. It finishes that allocation before visiting the next byte. Encoding visits scalars at argument(0), field(scan), scalar(i). It then reserves each encoded octet separately at result(0), byte(j), with extent one, before visiting the next scalar. Output indices increase across the complete result.
A successful nonempty conversion visits its required input end after its last component allocation. It adds no final allocation event. An empty conversion first visits byte zero or scalar zero as its required end. It then emits exactly one datum-allocate at result(0) with extent zero for the empty aggregate. Each input visit reserves all decoding or encoding work and temporary storage for that visit. The first result allocation includes the aggregate header and storage required for that component. Every later allocation includes its complete component and growth requirements. These extents use the library reservation convention.
The following table defines strings and symbols.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
string
0+
C...
String of the supplied scalars in order
None after the shared checks
datum-allocate then text-scalar-scan in result order
make-string
2
U count, C fill
String containing count copies of the scalar
None after the shared checks
datum-allocate then text-scalar-scan in result order
string-length
1
T
Exact Unicode scalar count
None after the shared checks
text-scalar-scandatum-allocate
string-ref
2
T, I index
Scalar at the zero-based scalar index
Require 0 <= index < scalar length
text-scalar-scan in scalar order
substring
3
T, I start, I end
String for the half-open scalar range
Check start bounds, end bounds, then start <= end
text-scalar-scan then datum-allocate
string-append
0+
T...
Concatenated raw scalar sequences in argument order
None after the shared checks
text-scalar-scan in argument order, then datum-allocate
string->list
1
T
Proper list of characters in scalar order
None after the shared checks
text-scalar-scan then datum-allocate per character
list->string
1
CL
String of the listed characters in order
None after the shared checks
list-step then datum-allocate
string=?
2+
T...
Boolean for adjacent equality under raw scalar lexicographic comparison
None after the shared checks
text-scalar-scan and compare-scalar until the first false adjacent comparison
string<?
2+
T...
Boolean for adjacent increasing order under raw scalar lexicographic comparison
None after the shared checks
text-scalar-scan and compare-scalar until the first false adjacent comparison
string>?
2+
T...
Boolean for adjacent decreasing order under raw scalar lexicographic comparison
None after the shared checks
text-scalar-scan and compare-scalar until the first false adjacent comparison
string<=?
2+
T...
Boolean for adjacent nondecreasing order under raw scalar lexicographic comparison
None after the shared checks
text-scalar-scan and compare-scalar until the first false adjacent comparison
string>=?
2+
T...
Boolean for adjacent nonincreasing order under raw scalar lexicographic comparison
None after the shared checks
text-scalar-scan and compare-scalar until the first false adjacent comparison
string->symbol
1
T
Symbol with exactly the same scalars
None after the shared checks
text-scalar-scandatum-allocate
symbol->string
1
Y
String with exactly the same scalars
None after the shared checks
text-scalar-scandatum-allocate
symbol=?
2+
Y...
True when adjacent symbols have equal raw scalar sequences
None after the shared checks
text-scalar-scan and compare-scalar until the first false adjacent comparison
The following table defines characters.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
char=?
2+
C...
Boolean for adjacent equality by numeric Unicode scalar value
None after the shared checks
compare-scalar until the first false adjacent comparison
char<?
2+
C...
Boolean for adjacent increasing order by numeric Unicode scalar value
None after the shared checks
compare-scalar until the first false adjacent comparison
char>?
2+
C...
Boolean for adjacent decreasing order by numeric Unicode scalar value
None after the shared checks
compare-scalar until the first false adjacent comparison
char<=?
2+
C...
Boolean for adjacent nondecreasing order by numeric Unicode scalar value
None after the shared checks
compare-scalar until the first false adjacent comparison
char>=?
2+
C...
Boolean for adjacent nonincreasing order by numeric Unicode scalar value
None after the shared checks
compare-scalar until the first false adjacent comparison
char->integer
1
C
Exact Unicode scalar value
None after the shared checks
datum-allocate
integer->char
1
I
Character at that Unicode scalar value
Require 0 <= value <= 1114111 and exclude 55296 <= value <= 57343
datum-allocate
The following table defines unicode operations.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
char-alphabetic?
1
C
Unicode 17.0.0 Alphabetic Boolean
None after the shared checks
text-scalar-scanunicode-map
char-numeric?
1
C
True exactly for Unicode 17.0.0 General_Category Nd
None after the shared checks
text-scalar-scanunicode-map
char-whitespace?
1
C
Unicode 17.0.0 White_Space Boolean
None after the shared checks
text-scalar-scanunicode-map
char-upper-case?
1
C
Unicode 17.0.0 Uppercase Boolean
None after the shared checks
text-scalar-scanunicode-map
char-lower-case?
1
C
Unicode 17.0.0 Lowercase Boolean
None after the shared checks
text-scalar-scanunicode-map
digit-value
1
C
Exact decimal digit zero through nine for Nd, otherwise #f
None after the shared checks
text-scalar-scanunicode-map
char-upcase
1
C
Simple uppercase character under Unicode 17.0.0
None after the shared checks
text-scalar-scanunicode-map
char-downcase
1
C
Simple lowercase character under Unicode 17.0.0
None after the shared checks
text-scalar-scanunicode-map
char-foldcase
1
C
Simple non-Turkic folded character under Unicode 17.0.0
None after the shared checks
text-scalar-scanunicode-map
string-upcase
1
T
Full default uppercase string under Unicode 17.0.0
None after the shared checks
text-scalar-scanunicode-mapdatum-allocate
string-downcase
1
T
Full default lowercase string under Unicode 17.0.0
None after the shared checks
text-scalar-scanunicode-mapdatum-allocate
string-foldcase
1
T
Full non-Turkic folded string under Unicode 17.0.0
None after the shared checks
text-scalar-scanunicode-mapdatum-allocate
string-normalize-nfc
1
T
Unicode 17.0.0 NFC string
None after the shared checks
text-scalar-scanunicode-normalizedatum-allocate
string-normalize-nfd
1
T
Unicode 17.0.0 NFD string
None after the shared checks
text-scalar-scanunicode-normalizedatum-allocate
string-normalize-nfkc
1
T
Unicode 17.0.0 NFKC string
None after the shared checks
text-scalar-scanunicode-normalizedatum-allocate
string-normalize-nfkd
1
T
Unicode 17.0.0 NFKD string
None after the shared checks
text-scalar-scanunicode-normalizedatum-allocate
char-ci=?
2+
C...
Boolean for adjacent equality of simple-folded scalars
Fold every argument from left to right before any comparison
text-scalar-scanunicode-map on every argument, then compare-scalar until the first false comparison
char-ci<?
2+
C...
Boolean for adjacent increasing order of simple-folded scalars
Fold every argument from left to right before any comparison
text-scalar-scanunicode-map on every argument, then compare-scalar until the first false comparison
char-ci>?
2+
C...
Boolean for adjacent decreasing order of simple-folded scalars
Fold every argument from left to right before any comparison
text-scalar-scanunicode-map on every argument, then compare-scalar until the first false comparison
char-ci<=?
2+
C...
Boolean for adjacent nondecreasing order of simple-folded scalars
Fold every argument from left to right before any comparison
text-scalar-scanunicode-map on every argument, then compare-scalar until the first false comparison
char-ci>=?
2+
C...
Boolean for adjacent nonincreasing order of simple-folded scalars
Fold every argument from left to right before any comparison
text-scalar-scanunicode-map on every argument, then compare-scalar until the first false comparison
string-ci=?
2+
T...
Boolean for adjacent equality of full-folded scalar sequences
Fold every argument from left to right before any comparison
text-scalar-scanunicode-mapdatum-allocate on every argument, then compare-scalar until the first false comparison
string-ci<?
2+
T...
Boolean for adjacent increasing order of full-folded scalar sequences
Fold every argument from left to right before any comparison
text-scalar-scanunicode-mapdatum-allocate on every argument, then compare-scalar until the first false comparison
string-ci>?
2+
T...
Boolean for adjacent decreasing order of full-folded scalar sequences
Fold every argument from left to right before any comparison
text-scalar-scanunicode-mapdatum-allocate on every argument, then compare-scalar until the first false comparison
string-ci<=?
2+
T...
Boolean for adjacent nondecreasing order of full-folded scalar sequences
Fold every argument from left to right before any comparison
text-scalar-scanunicode-mapdatum-allocate on every argument, then compare-scalar until the first false comparison
string-ci>=?
2+
T...
Boolean for adjacent nonincreasing order of full-folded scalar sequences
Fold every argument from left to right before any comparison
text-scalar-scanunicode-mapdatum-allocate on every argument, then compare-scalar until the first false comparison
The Unicode rows use the following complete reservation schedules.
A scalar property query or simple case mapping performs one scalar scan and one unicode-map. Its map extent is one. For digit-value, that map reserves the complete exact integer representation and value slot before creating the digit result. A nondecimal input returns #f within the same event. Neither result adds a datum-allocate event. Booleans and characters retain their declared scalar representation requirements.
Let n be the number of original input scalars. Full string mapping first scans all n scalars and the required end. It then maps the original scalars in ascending index order. Each unicode-map has extent n. The first map reserves one scratch buffer with capacity D times n scalars. D is 3 for uppercase, 2 for lowercase, and 3 for folding. That reservation succeeds before either scratch storage or the first mapped scalar is created. Later maps reuse that capacity. They reserve their own mapping work without another scratch allocation. An empty input performs its end scan and result allocation, with no map or mapping scratch reservation.
The map requirement includes exact bound calculation, table lookup, expansion, and retained scalar storage. These counts are mathematical integers. A host word width cannot add a domain limit or change the first failure.
After the complete original scalar scan and required end, each normalization call performs one unicode-normalize at argument(0). Its extent is the original scalar count n. D is 4 for NFC and NFD, and 18 for NFKC and NFKD. Its complete requirements cover two scalar buffers, each with capacity D times n, and 256 canonical-combining-class counters. Bound arithmetic, decomposition lookup, ordering, composition, and all intermediate storage belong to this reservation. It succeeds before transformation or scratch materialization starts.
Fully decompose the input under the selected form. Use stable counting order within each maximal nonstarter run. A scalar with combining class zero separates runs. Equal combining classes retain their original order. Compose NFC and NFKC in place under the Unicode blocking, exclusion, and Hangul rules. With decomposed length L and r runs of at least two nonstarters, ordering work has the structural bound O(1 + L + 256r). L is at most D times n and r is at most floor(L / 2). Reserve from n, D, and these upper bounds before decomposition; discovering actual L or r is transformation work. The selected model covers fixed workspace setup and every complete lookup, counter pass, scalar visit, and movement, including their coefficients. It cannot hide a recursive walk, comparison sort, or quadratic insertion pass outside the reservation.
The empty string still has one unicode-normalize with extent zero, followed by one datum-allocate with extent zero. The fixed workspace and empty-result requirements remain part of those reservations.
A completed string mapping or normalization reserves one datum-allocate before materializing its immutable result. Its extent is m, the actual number of output scalars. The complete requirements include the string header, value slot, and space for up to 4 times m UTF-8 octets. They also include encoding work and any temporary storage used for materialization. The extent remains m when input length, decomposition capacity, or UTF-8 octet length differs. Extent zero still reserves an empty string result. Refusal publishes no partial string and refunds no earlier charge.
All argument domain checks finish before folding or replacing any retained argument. Fold each argument in ascending argument order. Retain its completed folded value in the same logical operand-sequence position already reserved for that call. A character replacement belongs to its unicode-map. A string replacement belongs to its completed result allocation. This replacement changes no caller binding or immutable input value. It adds no argument-store or traversal-state event and requires no separate descriptor sequence. Every folded value remains available until comparison finishes or the call fails. Repeated references to the same input still perform each argument's full folding schedule and result reservation.
For a unary string transformation, the result allocation site is result(0). For a folded string comparison, the folded result of argument i is allocated at result(i) of the invoking comparison call. The site role is datum-allocate. All scans and maps continue to select the original argument(i) and its scalar positions.
After all folding and retention, each folded character pair performs one compare-scalar. For strings, each visited position performs one compare-scalar. Reserve before reading the left scalar or end, then the right scalar or end at that same position. Both reads belong to that event, including when the left sequence has ended. Only after both reads does the pair stop at unequal scalars or an end. No additional text-scalar-scan accompanies these folded reads. String comparison sites use field(compare), argument(i), scalar(j), where i is the left argument of the adjacent pair and j starts at zero for each pair. Character comparison selects field(compare), argument(i). The first false pair ends comparison after every argument has already been folded.
The original-input context rule in default case algorithms determines every Final_Sigma visit within its map requirements.
The following table defines procedure composition.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
values
0+
V...
The supplied values in order as an internal result sequence
None after the shared checks
traversal-state for the result sequence
apply
2+
P, V..., L
All values returned by one call with prefix arguments followed by the final list elements. The target inherits this call's tail position under the tail-call rule
Validate the whole final list, then check the procedure accepts the assembled argument count
list-steptraversal-statecallback-call
call-with-values
2
P producer, P consumer
All values returned by the consumer. The producer is nontail and the consumer inherits this call's tail position under the tail-call rule
Check the producer accepts zero arguments, call it, then check the consumer accepts its result count
callback-call for producer, traversal-state, then callback-call for consumer
The following table defines conditions.
Procedure
Arity
Domains
Result
Checks and failures
Resource events
make-condition
2
T code, field record
Validated immutable Condition without raising it
Use the complete ordered condition-constructor protocol
A closed pure library exposes the data operations and procedure composition needed by rules. A host extension would leave behavior and resource accounting outside the language contract. The two scalar equality names keep their respective failure operation names. Equal successful results do not erase that observable distinction.
A zero base raised to a negative exponent requires division by zero. The failing argument is the base.
Library event rules fix per-component reservations and the first detecting visit. They preserve the full argument checks, exact mathematical indices, and complete event requirements. An implementation can change storage without changing these event boundaries.
Complete storage and work are assigned to the declared Unicode events. Original scalar counts, generated scalar counts, and typed result sites preserve reservation order across physical representations.
Use the pair and list definitions when applying car. A nonempty proper list is a pair. The empty list is a distinct value.
The domain of car concerns its argument. A component returned inside a program can still be subject to the separate Datum boundary. Selecting a component does not make an internal procedure portable.
The call follows the application-order rule. Domain inspection and selection follow the reservation rule. A resource stop ends the request when a required reservation fails.
9.4 Select the first component of a pair
The procedure car accepts exactly one pair and returns its first component. The tail may be a pair, the empty list, or another value. An empty list or another nonpair produces a domain condition.
Exact numbers defines integers, rationals, decimal notation, scale, and rounding. Values and text defines equality and Unicode text. Public procedures use those definitions.
The native kernel can implement the arithmetic and text leaves needed by guest code. Work for large arithmetic, text traversal, and encoding remains subject to the common resource model.
A guest callback is a Lispex procedure supplied to another Lispex procedure. It executes with the same evaluation limits. Procedures defines its argument and value rules.
List validation, traversal, callback invocation, and result construction each contribute their required resource events. A library implementation preserves their specified order when it moves traversal into guest code.
Internal hash iteration cannot choose the visible order of results or failures. Operations on mapped records follow the canonical key order defined in Values and text.
9.7 Validate lists before ordered callbacks
A traversal that requires a proper list validates that list before invoking its first guest callback. The list traversal protocol fixes all list signatures, length checks, callback arities, and result counts. Map invokes callbacks from the first element toward the tail. Fold-right invokes them from the tail toward the first element. The first failure ends the traversal.
9.8 Validate complete list tuples before callbacks
Map and for-each accept a procedure followed by one or more proper lists. Folds also require an explicit seed. The callback signatures and empty results are fixed below.
Procedure form
Callback form
Required callback results
Empty result
(map p xs1 ... xsm)
(p x1 ... xm)
One
Empty list
(for-each p xs1 ... xsm)
(p x1 ... xm)
Any finite count, discarded
Empty list
(fold-left p seed xs1 ... xsm)
(p accumulator x1 ... xm)
One
Seed
(fold-right p seed xs1 ... xsm)
(p x1 ... xm accumulator)
One
Seed
Each tuple takes one element from every list in list argument order. After the procedure domain check, validate every list spine completely from left to right. Then compare list lengths against the first list in argument order. The first mismatch produces domain.range with unequal-lengths. No list is truncated.
After equal lengths are established, check that the callback accepts the required argument count. This check also runs for empty lists. It precedes the first callback. Fixed and rest procedures use the same accepted-arity rule from Procedures.
Map, for-each, and fold-left invoke callbacks in ascending element order. Fold-right invokes them in descending element order. Each fold uses the previous callback result as its next accumulator. The seed starts that sequence. A wrong callback result count is a runtime.value-count condition at result-check.
Map checks one callback result and allocates its result pair before advancing to the next tuple. That allocation can stop evaluation before a later callback failure. For-each discards every callback result sequence and returns one empty list after completion. It produces no guest output.
Fold-right reserves its logical traversal state before its first callback. The state follows list argument and ascending index order. Callback execution then proceeds from the last index toward the first. Host stack size cannot change that order or introduce another recursion bound.
Filter, find, any, and every accept exactly one procedure and one proper list. They validate the whole list and unary callback arity before invoking a callback. Every callback must return one value. Only #f is false.
Filter retains the original elements for true results in their original order. It allocates each retained result pair before continuing. Find returns the first matching element. Any returns the first true callback value. Every returns the first false value or the last true callback value. Any returns #f for an empty list. Every returns #t for an empty list.
These procedures stop at the first failure. Find, any, and every may stop callbacks at their stated result. That early result never skips initial proper-list or callback-arity checks.
Rejecting unequal lengths prevents a rule from silently dropping input data. Complete list validation fixes failure priority before guest code runs. Explicit accumulator positions and callback order make folds reproducible. Checking callback arity on empty input keeps the accepted call contract independent of list length.
The native kernel is the set of host operations needed by the prepared language and library. Derived operations use ordinary guest code. The kernel can provide value access and construction, exact arithmetic leaves, Unicode operations, and codec work. Its final membership remains pending.
The prepared bundle fixes library source and verified code under one library identity. Preparation and modules defines resolution and cache validation. Identity, receipt, replay defines the corresponding identities.
A primitive classification selects its accounting method. It does not replace tests of the operation paths.
9.9 Prepare closed guest library code
Derived library procedures run as ordinary Lispex code in the prepared bundle. Preparation resolves their library references lexically and binds the fixed library identity to the program. User bindings do not replace those resolved references. Reused library preparation follows the cache-preservation rule.
Guest code inherits the common call, branch, allocation, and callback events. Fixed lexical references preserve library meaning when a user shadows a public name.
Every native primitive has exactly one declared class. The classes are Fixed, Precharged, Incremental, GuestCalling, and Deferred. A missing class has no default. An unresolved class or a required Deferred operation prevents admission before evaluation.
Every native path performs host work that needs an explicit accounting method. Rejecting an unaccounted operation closes a route around finite execution.
Class
Required behavior
Fixed
Reserve a fixed bound before a fixed amount of work. Input growth cannot hide additional work.
Precharged
Establish and reserve the complete charge before the operation effect. Determining the charge also uses metered work.
Incremental
Reserve each defined increment before performing it. Preserve the specified increment and failure order.
GuestCalling
Account for native work and invoke guest procedures through the common evaluator and budget.
Deferred
Reject a request that requires the operation before evaluation.
Large integer arithmetic, structural traversal, and complete encoding depend on input size. Their classification accounts for that growth. A Fixed label cannot make variable host work constant.
Equal results alone do not preserve a request near a finite limit. Moving a reservation can change whether a domain failure or resource stop happens first.
Select profile admission and evidence requirements while preserving Lispex meaning. Exchange exact data through a canonical codec.
Scope
The calling application selects a profile and supplies canonical input data. An admitted rule keeps the language meaning and resource limits of its semantic request.
This chapter defines admission, base, vouch/2, schemas, and canonical value interchange. Sandbox contract defines language, profile, product, and engine. Values and text defines Datum.
Admission
Admission checks whether the selected product and profile can accept a proposed execution. It accepts the submitted request or refuses it before guest entry. A refusal preserves the declared program, input, semantics, and limits.
Engine support and library permission are explicit checks. A product reports missing support instead of changing execution meaning. Preparation and modules defines the closed program that admission inspects.
10.1 Refuse unsupported requests before entry
Admission checks the selected profile and the product’s supported semantics before guest entry. Unsupported engine features or excluded library operations cause admission refusal. A product cannot repair refusal by changing semantics or silently selecting another engine.
An accepted request has one declared meaning. Refusal identifies an unsupported request before a different implementation can produce a different result.
The profile host budget bounds additional profile admission, schema checks, output qualification, and evidence work. It is finite and separate from the language preparation and evaluation budgets. Canonical input decoding and canonical result or failure encoding remain evaluation work.
An early host refusal prevents guest entry. A later qualification or evidence refusal preserves the completed canonical outcome. Profile work cannot reduce the evaluation budget, move the first language failure, or rerun guest code.
Profile work identity and reports identify these checks separately from the semantic request. Before entry, a refusal uses an admission report. After evaluation, qualification or evidence refusal uses a profile work report tied to the completed canonical outcome.
10.2 Keep profile work separate
Additional profile admission, schema checks, qualification, and evidence work use the separate finite profile host budget. Canonical input decoding and canonical result or failure encoding remain evaluation work. Profile checks preserve the semantic request and cannot debit its budgets or change its first language failure. A host check can refuse admission before entry or qualification after evaluation. A completed canonical outcome remains unchanged.
A narrower profile may perform more checks than base. Accounting for those checks separately preserves the evaluation meaning and limits of requests accepted by both.
The profile host budget has every field below. Each of its six budget axes is an exact nonnegative integer. The format and resource_model fields are metadata. Zero is finite. Missing fields, unknown fields, nonintegers, unlimited values, and values outside the selected model's admitted range fail admission. Host integer width does not choose that range.
One account covers all performed profile stages. It starts before profile operand checks and continues through qualification and evidence. Stage changes do not refill it. Committed work, allocation, input, report, and evidence charges are never refunded. Logical traversal frames are released only when their traversal returns.
Every event reserves all required fields before its check or effect. Simultaneous shortages choose work, allocation, frames, input, report, then evidence. A refused reservation changes no charged total and performs no partial effect. The first committed failure ends later profile work.
Profile wrapper decoding, record conversion, schema checks, declaration checks, library inspection, hashing, evidence verification, and report construction use this account. Canonical input decoding runs once under EvaluationLimits. Schema checks then inspect that immutable decoded Datum under the host account. After admission, evaluation continues with its existing decoding charges and state. It initializes modules and invokes the entry only after input schema acceptance. Canonical result encoding remains evaluation work.
Before evaluation, the host secures the terminal report capacity required by the selected finite limits and model. The reservation covers a complete refusal diagnostic and the largest eligible receipt and profile report permitted by those limits. The model names that bound. A shortage refuses admission. Its numeric bound remains under the cost model freeze.
After evaluation, the canonical outcome and eligible receipt remain immutable. A later schema, budget, or evidence failure produces its separate report. It does not rerun the guest, replace a language failure, or revoke receipt eligibility. Later report transport failure cannot change the committed first cause.
The resource_model metadata selects the host model independently of the evaluation model. Only the six numeric limit fields are budget axes. Operations without a declaration skip profile schema and qualification stages. Their separate command contracts retain the same finite host account.
A finite shared host account bounds every additional check. A fixed reservation order gives the same first refusal across products. Reserved reporting capacity protects a completed result while profile work is refused.
Operation
Complete terminal capacity bound
run
The requested finite evaluation result and diagnostic limits, eligible receipt framing, and complete profile report
verify
The captured receipt and evidence operand sizes and the complete verification report
replay
The expected receipt size, recorded finite evaluation result and diagnostic limits, actual eligible receipt, and complete comparison report
record-admission
The finite captured input bound, canonical converted input packet, and complete admission refusal report
The host secures its terminal reporting slot before work can publish a result. Run and replay reserve the complete eligible receipt capacity before guest evaluation. Record admission reserves complete conversion output capacity before conversion. The selected host model defines the required finite reservation from these inputs. The reservation uses report capacity and its required work and logical allocation. A shortage refuses the operation before its unprotected stage begins. The committed first cause stays fixed. Later physical delivery failure leaves every completed immutable outcome and receipt available. The model's numeric bounds and physical capacity proof remain under the cost model freeze.
The command result contract imports the complete outer emergency framing and separate trace state. Those fields are covered before normal work begins.
Host operation
Profile contract
Declaration
Schema and evidence work
run
The selected base or vouch/2 builtin
The generated base declaration or explicit vouch/2 declaration
The complete admission, qualification, and required evidence schedule
verify
Absent
Absent
Receipt comparison and explicitly requested evidence under the command contract
replay
Absent
Absent
Recorded-request binding and explicitly requested expected-receipt evidence before authoritative input decoding
record-admission
The explicitly selected base or vouch/2 builtin
Absent
Record key admission and canonical conversion only
Record admission requires no program, library, input schema, output schema, or evidence. Both builtin profiles use the same record key policy. Conversion ends with CanonicalInputBytes. Later evaluation admission checks its selected schema against a verified program. That later operation has its own host work identity and account. Record admission produces no canonical evaluation outcome or evaluation receipt.
Standalone verify and replay do not synthesize a base declaration. They skip profile schema membership and output qualification. Their host work still uses the complete finite ProfileHostBudget. The profile and declaration options in ProfileWorkInput are absent. For record admission only the profile option is present. For run both options are present.
Prepare and graph use their existing preparation and tool contracts. They do not acquire profile arguments or a ProfileWorkIdentity through this rule.
This exact descriptor denotes the complete check schedule and schema traversal in this chapter. Its resource model supplies host tariff and allocation parameters. The definition resource_model equals the validated budget metadata. The schema language and format strings are fixed. Extra fields and alternate schedules are invalid. The product verifies the complete descriptor against its supported version before marking the contract identity verified.
The identity contract encodes and hashes this declarative value. The definition is independent of document prose and product implementation bytes. The numeric model choices remain frozen until implementation and product evidence support them.
10.4 Inspect schemas in a fixed order
Schema validation visits each finite tree occurrence in depth-first order. It checks a node's tag and exact shape before its children. Pair children use car then cdr order. Vectors use ascending index order. A record node checks all field names, field shapes, ordering, and required markers before validating any child schema. It then validates child schemas in key order. Enum canonical order and duplicates are checked before membership.
Membership follows the table below. Each entered schema and data occurrence reserves its work and logical frame before inspection. A completed child releases its frame before its next sibling begins. Shared physical storage never skips an occurrence.
Complete the prescribed shape checks before testing child membership. Stop at the first failed shape, key, membership test, or earlier reservation. A successful earlier comparison cannot suppress required later checks. No remaining child is visited after a committed failure.
A mismatch is reported by the schema boundary diagnostic. It does not invoke a guest Condition or a handler. The semantic request and completed outcome remain unchanged.
Membership order can decide whether a schema mismatch or a host budget refusal happens first. A fixed traversal preserves that choice across recursive and iterative implementations. Structural prechecks avoid partial acceptance of malformed data.
The resource_model field selects the explicit host work model. It is required metadata and is not a budget axis. The format field is required metadata. The host model may differ from the evaluation resource model. It does not change evaluation charges or RequestIdentity. A change to either host model or host limits changes ProfileWorkIdentity.
The selected common-default preset resolves this complete record. An explicit profile-limits operand supplies the complete record. No product fills missing metadata from its engine or another operand. A supported model is verified from the complete model definition. Default host axis data is known before the model identity. Preset resolution adds resource_model only after that identity is verified. No network or registry discovery supplies that declaration.
Field
Quantity bounded
work
Cumulative normative host work
allocation
Cumulative logical host allocation
frames
Simultaneously active logical host traversal frames
input
Total captured operand packet bytes used by this host operation
report
Complete host report and conversion output capacity
evidence
Total complete evidence packet bytes processed by this operation
Operation
Captured packet operands counted by input
run
The explicit profile request and canonical input packets, plus every other submitted packet read by its host checks
verify
Expected receipt, actual receipt, supplied evidence, and supplied trust policy packets
replay
Recorded request, expected receipt, supplied evidence, and supplied trust policy packets, plus every submitted packet read by its host checks
record-admission
The complete explicit record input packet
Each submitted operand occurrence contributes its complete byte length once. Repeated inspection does not add another input charge. It retains the required work and allocation events. Nested evidence and trust packets already contained in a profile request do not add another input occurrence when extracted. An independently supplied operand is a new occurrence even when it reuses the same physical buffer. The evidence field also bounds evidence packet bytes contained in an input operand. Host checks that read source or prepared operands include those bytes in input. Preparation retains its separate resource account.
Malformed metadata or budget values use request.invalid under the existing catalog. An unsupported host model uses product.unsupported with subject resource-model. No fallback model is selected.
Tariffs, allocation units, numeric range bounds, defaults, terminal capacity bounds, physical capacity values, and the final native kernel inventory remain under cost model freeze. The field names, exact types, occurrence rules, reservation order, and traversal schedule are fixed here.
Stage
Ordered work
Result boundary
Host setup
Validate the complete budget and acquire the finite physical safety envelope. Reserve terminal report capacity
A refusal precedes guest entry
Snapshot
Bind the complete explicit operand snapshot and charge its input and evidence bytes
No issuer or configuration lookup
Declaration
Decode the profile request, validate its wrapper, validate the declaration, then validate input and output schemas
Unknown or malformed data is refused
Library
Verify the selected fixed library identity, validate allowed names, then inspect resolved source references in canonical order
The first excluded binding refuses admission
Prerequisites
Check supported engine semantics, explicit evidence and trust presence, and their supported structure
Missing prerequisites refuse admission
Canonical input
Decode the canonical packet exactly once under EvaluationLimits
Malformed data or decoding exhaustion follows the existing input diagnostic contract
Input schema
Apply the schema to the immutable decoded Datum under the host account
No guest entry on schema refusal
Evaluation
Continue the admitted evaluation state with module initialization and entry. Retain the input decoding charges
Complete the canonical outcome and eligible receipt
Qualification
Apply the output schema to the immutable returned Datum. Skip membership for language failure and resource stop
A refusal preserves the completed outcome and receipt
Evidence
Check the declared requirement against the completed actual receipt in the evidence contract order
No evidence work after an earlier profile refusal
Report
Commit the complete separate host report in its reserved capacity
Preserve the first cause and the receipt bytes
Standalone verify and replay use the same host fields. Their command order chooses when evidence is checked. Replay evaluation retains its separate account.
Event family
Required logical work
profile-input
Account for an explicit operand occurrence before inspecting it
profile-declaration
Visit the next declaration component in its prescribed order
profile-library
Check the next allowed binding or resolved source reference
profile-schema
Enter, inspect, or leave the next schema and data occurrence
profile-compare
Compare canonical names or enum bytes in their declared order
profile-hash
Hash the next required byte sequence under the identity contract
profile-signature
Perform the next required canonical key or signature check
profile-report
Reserve and encode a complete report before publication
Record admission uses the codec and record events from the boundary event schedule. Wrapper decoding, record adaptation, and encoding the converted packet all charge the host account. Reserve that complete packet against report before emitting its octets. The evaluator later performs its complete input decode and result encode in the evaluation account. The selected host resource model supplies each host reservation size. Product caching and pointer sharing preserve every required logical event.
Node
Shape checks
Child or comparison order
datum
The value has completed canonical Datum validation
No child schema
kind
Compare the current Datum kind
No child schema
enum
Use the complete canonical Datum bytes of the value
Members in declared byte order. Compare unsigned octets from zero. Stop on equality or after the final member
pair
Require a pair
Complete car membership, then cdr membership
list
Inspect the complete spine and require the empty final tail
Element schemas from the head
vector
Require a vector
Elements from index zero
tuple
Require a vector and exact declared length
Corresponding schemas from index zero
record
Require a proper list. Inspect all entry pair shapes and string keys in list order. Require strictly increasing keys. Merge actual and schema keys in UTF-8 order to check required and unknown names
After all key checks, visit present values in key order
The first absent required or unknown supplied key in the merged order fails before any field value check. Absent optional fields have no child value to inspect. Required and optional markers change membership only. They never insert data.
The logical frame count includes the current traversal occurrence and its unfinished ancestors. Implementation call stacks, iterators, cached hashes, and shared objects do not change that count.
Input decoding has one authoritative result. It uses EvaluationLimits before schema membership. A malformed packet uses admission and input.codec. An exhausted decode uses admission and input.resource. Host schema work cannot replace either failure. Successful decoding supplies an immutable Datum and preserves the charged evaluation state. Schema acceptance resumes that state without decoding again.
A replay command can compare outer recorded-request bytes before this step. That comparison does not mark the canonical input or evaluation request verified. The replay contract completes expected evidence checks before the authoritative decode. The corresponding verified markers appear only after decoding succeeds.
Base names the common Lispex 2.0 language contract. Its programs use exact data, the shared condition rules, and finite resources. Every admitted program has the sandbox guarantees defined in Sandbox contract.
A narrower profile can accept fewer inputs or libraries and require additional evidence. It preserves the meaning of the requests it accepts.
10.5 Use one base language
Base applies the default sandbox contract to every program. A narrower profile applies those same guarantees to its admitted requests. Selecting a product or engine follows the same-request rule.
Every accepted program begins with the same sandbox contract. Profile admission can express application requirements without becoming a second language.
The vouch/2 profile adds declared admission and evidence requirements to the base language. A declaration fixes its accepted input and output schemas, allowed library set, and required evidence.
Base and vouch/2 produce the same canonical outcome when both admit the same semantic request. Their evaluation limits and charges remain unchanged. A profile cannot replace a language failure or resource stop with a decision datum.
The vouch/2 profile applies the execution evidence rule. Its declaration determines the evidence required for a Vouch result. Evidence work uses the profile host budget and preserves the canonical outcome and evaluation charges.
A profile declaration uses the exact fields below. Every field is required. The selected profile name must match the declaration. Unknown formats, fields, and values fail admission. An explicit declaration supplies no defaults.
Base is the fixed declaration generated from the request's verified library identity. Its input and output schemas accept every Datum. Its library entry contains the complete public catalog. Its evidence requirement is none. A declaration with narrower fields cannot use the base name.
A vouch/2 declaration supplies its complete input schema, output schema, and allowed public bindings. Its evidence requirement is signed-execution. It preserves the request's fixed library identity. An empty binding list admits source that uses no public library binding.
The sole allowed library identity is the fixed Lispex 2.0 library selected by the semantic request. Each binding name must appear in the public catalog. The vector is strictly increasing by unsigned UTF-8 name bytes. Internal library dependencies keep their fixed meaning. Source modules and source-defined bindings are outside this allowlist.
Admission checks resolved library references in every supplied source module. It follows canonical module and node order. An alias retains the identity of its resolved binding. Unused definitions and unselected branches still take part in this check. The first excluded reference refuses admission. No library procedure runs during this inspection.
The request wrapper carries the explicit declaration and its evidence operands. Base uses empty evidence and trust options. Vouch/2 requires both options. Missing operands refuse admission. Evidence verification follows output qualification and binds the completed actual receipt.
The profile host budget is a separate request input. The command's profile-limits operand or selected finite preset supplies it. The declaration wrapper cannot replace that budget.
A complete declaration makes acceptance reproducible. A fixed base declaration preserves the common language. A narrower declaration records each additional restriction. Resolved references keep aliases and source shadowing precise. Explicit evidence operands keep trust outside ambient host state.
10.9 Use finite structural schemas
A schema is a finite tree in the grammar below. Each vector has its exact declared length. Schema validation completes before the schema is applied. Unknown nodes, extra fields, and invalid field types refuse admission. There are no references or implicit schema imports.
Membership inspects an already validated Datum. It preserves every value and raw scalar. It never coerces a number, normalizes text, inserts a field, or invokes guest or host code. The schema contract contains no executable predicate.
An enum contains at least one Datum. Its members are strictly increasing by their complete canonical Datum bytes. Repeated members are invalid. A record schema has exact string names in unsigned UTF-8 order. Each field appears once. Its Boolean marks whether the field is required. A false value allows absence without supplying a replacement.
A record schema accepts only a proper association list of string-keyed pairs in canonical key order. Its keys are unique. Every supplied key must occur in the schema. An ordinary association list keeps its original Datum meaning outside a record schema.
The schema traversal rule fixes validation and membership order. A mismatch uses profile.admission before entry or profile.qualification after evaluation. The profile field identifies the selected builtin profile contract. The rule field identifies the verified canonical program.
Structural schemas express finite data restrictions without a second evaluator. Canonical set and field order remove host ordering choices. Explicit optional fields preserve absence as input data.
10.10 Admit explicit records with string keys
Base and vouch/2 admit the named record input below. The caller selects record conversion explicitly. A field key is an exact Unicode string. Empty strings and all Unicode scalar strings are admitted. Symbols, numbers, bytevectors, and host object keys are not field names. No coercion or normalization supplies a name.
Each field vector has a name and one child. The complete name collection is checked before any child value is converted. The adopted record conversion rule sorts names, rejects duplicates, and converts values in that order. Nested records use the same rule. A datum node preserves its enclosed Datum. A record node becomes ordinary association data with each unchanged name as a string key.
The record packet is a finite value tree. It contains no callback, accessor, identity-bearing object, cycle, or live host reference. A typed host adapter rejects such values without invoking them.
Record adaptation, wrapper decoding, and conversion output encoding use the profile host budget. The result is one complete canonical input packet. The evaluation boundary then decodes that packet under EvaluationLimits. Direct input and converted input with identical bytes have identical evaluation events. Evaluation also encodes its result under EvaluationLimits. A cached conversion does not remove evaluation events.
The command input operand still takes canonical Datum bytes. A record wrapper supplied as an ordinary Datum remains that Datum. The format name never selects conversion by inspecting guest data.
Explicit conversion keeps host records distinct from ordinary lists. String keys preserve the adopted Unicode and codec contracts. Lowering before evaluation gives identical association data the same evaluation request and charges.
D encodes one complete lispex.datum/2 packet. R is a proper association list with exact string keys in unsigned UTF-8 order. The shared wire notation defines these forms.
The evidence option contains the complete named evidence packet. The trust option contains the complete named trust policy packet. The evidence envelope contract defines those bytes.
The profile-declaration command operand contains ProfileRequestBytes. An omitted base operand selects the generated base declaration and empty options. Vouch/2 requires this operand. An explicit base operand must equal the generated base declaration and its empty options.
Failure
Diagnostic
Field
Missing declaration field
request.invalid with missing-field
profile-declaration. followed by the exact missing name
Unknown declaration field
request.invalid with unknown-field
profile-declaration. followed by the exact supplied name
Invalid declaration value
request.invalid with invalid-value
profile-declaration. followed by its top-level field name
Invalid input schema subtree
request.invalid with invalid-value
profile-declaration.input_schema
Invalid output schema subtree
request.invalid with invalid-value
profile-declaration.output_schema
Malformed declaration record or packet
request.invalid with invalid-value
profile-declaration
Excluded resolved library binding
profile.admission with library-exclusion
The catalog payload names the builtin profile contract and verified program identities
Missing required evidence or trust
profile.admission with evidence-prerequisite
The catalog payload names the builtin profile contract and verified program identities
Check record shape first. Then merge the required and supplied field names in unsigned UTF-8 order. The first missing or unknown name wins before field values are checked. Validate field values in unsigned UTF-8 name order. Validate input_schema before output_schema. Malformed wrapper fields use the same rule with profile-request as their field prefix. Budget shortages use the phase and field from the host work contract.
A declaration packet has no verified declaration identity until all declaration checks succeed. The selected builtin profile contract is verified before parsing. Profile budget diagnostics use that builtin identity. The report keeps declaration verification separate.
The exact Datum kind. Number admits integers and reduced nonintegral rationals
enum
One exact canonical member
pair
A pair whose car and cdr satisfy the two child schemas
list
A proper list whose elements satisfy the child schema
vector
A vector whose elements satisfy the child schema
tuple
A vector with the declared length and corresponding child schemas
record
Closed canonical association data with the declared required and optional fields
Rational selects the nonintegral rational kind. Integer selects the integer kind. Empty record schemas accept only the empty list. Empty tuple schemas accept only an empty vector.
Form
Exact shape
RecordInputBytes
D(R{format = "lispex.record/2", value = RecordNode})
RecordNode
#("record" #(RecordField...))
RecordField
#(Text InputNode)
InputNode
#("datum" Datum) | RecordNode
Check
Required result
Wrapper and node shape
Exact tags and vector lengths
Field shape and key type
Inspect field positions from zero before ordering names
Key type failure
record.key with the first invalid submitted field position
Name collection
Apply the existing UTF-8 order and duplicate check
Duplicate positions
first and second are the adjacent positions of the first equal name in the sorted name sequence
Key Datum
The unchanged name as a string
Field value
Recursively convert in canonical name order
Converted input
D of the resulting association Datum
A missing or malformed structural slot uses request.invalid with invalid-value. A nonstring field name uses record.key. Duplicate keys use record.duplicate. Conversion ends with CanonicalInputBytes. Later evaluation admission checks its selected schema against a verified program. Record admission performs no evidence work.
The builtin profile contract is fixed before the request declaration is parsed. Its identity selects the contract applied by every profile diagnostic. The declaration has its own identity and verification marker.
An unrecognized selector cannot produce a builtin identity. It uses the existing request or unsupported-product diagnostic. No profile declaration identity is inferred from an unchecked packet.
A schema describes accepted data. An input schema chooses which input data the rule may receive. An output schema describes the result data accepted by a profile.
A decision label such as allow or deny is ordinary returned data. The calling application chooses any external action. The language does not turn the label into a host command.
Input schema checks inspect decoded input before guest entry. Canonical input decoding remains evaluation work. The additional schema check uses the profile host budget.
After evaluation, host qualification checks a returned datum against the output schema. It records profile acceptance separately from the canonical outcome. Canonical result or failure encoding remains evaluation work.
10.11 Validate data without coercion
A schema specifies accepted input and output data. An input outside the selected schema is refused before guest entry. Validation preserves exact values and text. Decision labels remain ordinary data. Profile schema checks use the profile host budget.
Schema membership describes which data the application accepts. Coercing an input or interpreting a label as an engine command would change the rule request.
Finite host work stays separate from language evaluation.
After evaluation, a profile checks the returned Datum against its output schema. A mismatch refuses qualification as a profile result and preserves the canonical outcome. Qualification uses the profile host budget under the profile work rule. It does not rerun guest code. A language failure or resource stop keeps its original outcome.
A returned datum already has language meaning. Separate qualification expresses application acceptance without changing that meaning or moving the first evaluation stop.
The canonical Datum codec lispex.datum/2 defines the byte representation used for interchange. It preserves the values defined in Values and text. Exact numeric forms follow Exact numbers.
Text retains its scalar sequence. Admitted host records become immutable association data under the conversion rule below. A host object does not become a guest capability.
Canonical interchange lets products compare the same data across platforms. Exact numbers and text remain independent of host numeric width and locale.
The codec identifier is lispex.datum/2. A packet contains the fixed magic, a minimal payload length, and one Datum. The byte grammar and tag table below define every accepted representation. Strings and symbols use strict UTF-8. Pairs preserve both components. Vectors preserve element order. Sharing has no byte representation.
CanonicalDatumBytes names one complete packet for a Datum. CanonicalInputBytes names those same complete bytes when supplied as evaluation input. Both names include the magic, length, and payload. A record field that carries either packet uses an explicit bytevector. A record wrapper is not part of those packet bytes.
A small closed grammar assigns one representation to every portable value. Distinct tags keep text, symbols, and characters distinct. One frame gives later identity and receipt formats an exact byte boundary.
The byte grammar uses hexadecimal octets and scalar bounds. Arithmetic constants are decimal. U encodes an exact natural number. Z encodes an exact integer.
Field
Encoding equation
Packet
magic U(payload-byte-length) value EOF
Magic
6c 69 73 70 65 78 2e 64 61 74 75 6d 2f 32 00
Unsigned integer
U(n) = b[0] ... b[k-1], k >= 1
Integer value
n = sum((b[i] & 0x7f) * 128^i)
Continuation octet
b[i] in 0x80..0xff for i < k-1
Final octet
b[k-1] in 0x00..0x7f
Minimal form
k > 1 requires b[k-1] != 0x00
Nonnegative integer
Z(n) = U(2*n) for n >= 0
Negative integer
Z(n) = U(-2*n-1) for n < 0
Text payload
U(byte-length) UTF8[byte-length]
Pair
08 value value
Vector
09 U(element-count) value[element-count]
Bytevector
0a U(byte-length) octet[byte-length]
Datum
Tag
Payload
Required form
Empty list
00
Empty
One empty list value
False
01
Empty
Boolean false
True
02
Empty
Boolean true
Integer
03
Z(n)
Exact integer
Rational
04
Z(n) U(d)
n != 0, d > 1, gcd(abs(n), d) = 1
Character
05
U(scalar)
0000..d7ff or e000..10ffff
String
06
text
Exact scalar sequence
Symbol
07
text
Exact scalar sequence
Pair
08
value value
Car then cdr
Vector
09
U(count) value[count]
Index order
Bytevector
0a
U(length) octet[length]
Byte order
All other tag octets are invalid. A list uses pair tags ending in the empty list tag. An improper pair remains valid Datum.
Lengths count octets except the vector count. A text length counts its UTF-8 payload, not its scalars. Empty strings and symbols are valid.
Unsigned integers have no machine width limit. The signed mapping gives zero one representation. It has no negative zero code.
Strict UTF-8 uses the shortest encoding of each Unicode scalar. Surrogate values and values above U+10FFFF are invalid. Unassigned scalars, noncharacters, and U+FEFF inside text remain data. The codec performs no normalization or case conversion.
The outer length covers only the encoded value. Every packet includes the magic and length. Nested values include neither. Repeated equal subvalues are encoded in full. Reference tags, cycles, extension tags, and implicit record conversion are invalid.
An integer uses the integer tag and the signed mapping in the grammar. A nonintegral rational uses the rational tag. Its numerator is nonzero. Its denominator exceeds one. Their greatest common divisor is one. Equal decimal, rational, and integer values receive equal bytes. The codec stores no decimal scale or signed zero.
Numeric spelling does not change a Lispex value. Encoding the reduced value keeps input identities and result bytes independent of presentation. Exact integers avoid a host numeric width or floating point conversion.
Decode the frame before its Datum. Within a Datum, follow the field order in the grammar. Visit a pair car before its cdr and vector elements in index order. Reject the first malformed or noncanonical field. Reject unknown tags, excess bytes, invalid scalars, and every alternate integer or rational encoding. Decoding never repairs input. Complete structural and canonical validation precedes result Datum materialization. An unchecked length or count cannot trigger a bulk result reservation. A rejected input does not invoke entry or produce an evaluation receipt.
Accepting alternate spellings would give one value several input byte identities. A fixed validation order also preserves the first failure. Rejecting a packet as a whole prevents a partial value from crossing the input boundary.
The decoder follows this order. Resource reservations use the shared event rules before the corresponding work or allocation.
Step
Validation
Rejection cause
Magic
Compare each magic octet from the start
magic at the first mismatch or missing octet
Frame length
Read one terminating minimal U
unterminated-integer or nonminimal-integer
Frame boundary
Compare the declared payload length with all remaining octets
truncated-frame or trailing-frame-data
Value tag
Read the next tag in traversal order
missing-value or unknown-tag
Integer field
Read a terminating minimal U before interpreting it
unterminated-integer or nonminimal-integer
Rational fields
Read numerator then denominator, then check denominator, numerator, and reduction
rational-denominator, rational-zero, or unreduced-rational
Character
Check the scalar after decoding U
invalid-scalar
Text or bytes
Read the length, check remaining bytes, then consume that exact slice
truncated-sequence
Text scalar
Check UTF-8 from the start of the declared slice
invalid-utf8 at the first invalid sequence
Pair
Decode car completely, then cdr completely
The first child failure
Vector
Read the count, then decode that many children
The first child failure
Root end
Require the root to consume the payload exactly
trailing-value-data
Materialization
Reserve and construct the validated Datum in depth-first car, cdr, and index order
A resource stop
The decoder completes structural and canonical validation before materializing its result Datum. It does not reserve or allocate a result container from an unchecked length or count. Validation workspace, traversal, and exact numeric checks still consume metered work and storage. Every event reserves its resources before the corresponding check or effect. After validation, result reservations and materialization follow depth-first car, cdr, and index order.
Text validation rejects overlong encodings, isolated continuation bytes, truncated sequences, surrogates, and out-of-range scalars. It does not substitute replacement characters. A missing UTF-8 continuation fails within the declared text slice.
The cause names describe codec failures. The diagnostic catalog supplies public codes and reports.
Every malformed input is refused before entry. It produces no canonical evaluation outcome or evaluation receipt. Canonical decoding still uses the evaluation resource account. A resource stop follows the shared resource rules.
Event name
Required work
codec-frame
Open or finish one packet
codec-byte
Consume or emit an octet in byte order
codec-value
Visit a Datum in depth-first order
codec-integer
Interpret or size an exact integer field
codec-scalar
Validate or encode one text scalar
codec-rational-check
Check a rational in the stated field order
codec-allocation
Reserve logical data and buffer allocation before materialization
record-order
Establish canonical field order from the complete name collection
record-key
Check the next name in canonical order
record-field
Convert the next value in canonical order
Encoding validates the Datum and determines its payload length before emitting a packet. It follows the same value and field order as decoding. Result bytes become available only when the complete packet succeeds.
Host widths, caching, sharing, and allocation strategies do not change semantic events. The resource event catalog owns their accounting details. Tariffs, allocation units, finite defaults, and physical envelopes remain under the cost model freeze.
10.17 Convert admitted records into ordered association data
The record input contract supplies fields with exact Unicode string names. Each key Datum is that unchanged string. Order fields by unsigned UTF-8 name bytes. Reject duplicate names before visiting any value. Then convert values in that order. Emit a proper list of pairs with the key in car and the value in cdr. An empty record becomes the empty list. Encoding an ordinary association list preserves its existing order.
Records need deterministic conversion without adding a guest map kind. Sorting exact names makes host enumeration irrelevant. Checking all keys first gives duplicate keys priority over failures in field values. Keeping ordinary lists ordered preserves their existing Datum meaning.
The record input contract admits the explicit packet and its string keys. The codec applies this conversion after that admission.
Stage
Required behavior
Name view
Use the complete finite collection of exact Unicode string field names
Order
Compare unsigned UTF-8 bytes lexicographically, with the shorter prefix first
Key check
Reject the first duplicate name in sorted order before inspecting any field value
Value conversion
Visit field values in sorted name order and convert nested admitted records by the same rule
Association data
Construct one dotted pair per field and a proper list containing those pairs
Encoding
Encode that ordinary Datum with lispex.datum/2
The key policy preserves names without normalization, case folding, or string coercion. An inadmissible name or nonpreserving key policy fails profile admission. Field values must become Datum. Callbacks, accessors, cycles, inexact numbers, and other host capabilities are refused without invocation.
The record-order reservation covers ordering work for the whole name collection. Its event parameters depend on the collection, not host enumeration. Key checks and value conversion follow the resulting order. Different source enumerations produce the same association data and host conversion events.
The mapping uses no record byte tag. Decoding the resulting packet returns association data. An ordinary list can contain repeated keys or any element order. The Datum decoder preserves that list without record checks.
Profile declarations select the public host forms and admitted key kinds. Record adaptation and its complete output encoding use the profile host budget. The report axis covers the converted input packet. The boundary event schedule selects the account for each codec operation. The evaluator decodes that packet under EvaluationLimits. It uses the same evaluation events as a caller that supplies those canonical bytes directly. Schema work remains in the profile host budget.
Retain a request and its outcome to repeat a rule evaluation. Keep source identity and execution evidence separate.
Scope
Keep a semantic request and its canonical outcome to repeat a rule evaluation. Use separate records for exact source bytes and execution evidence.
The sandbox contract defines the semantic request. Profiles and value interchange defines the canonical value codec. The cases here use documentation notation for inputs, identities, and limits. Their fields do not establish a public byte format.
Program, source, request, and artifact
An identity names one object under a versioned contract. Source identity names the exact submitted source bytes. Program identity names the canonical resolved program under its fixed dependencies. Request identity names the complete semantic request. Artifact identity names the bytes of an engine artifact.
Source and normalization defines how source becomes canonical code. Preparation and modules defines the closed bundle and resolved program. Whitespace can change source identity while leaving program identity unchanged. An equal result for one input does not establish that two programs are equivalent.
Profile work identity identifies the submitted request data, the versioned profile work contract, and the finite profile host budget. The profile work contract fixes the declared profile, schemas, evidence requirements, and host check rules. Changing that contract or its host budget changes profile work identity. It leaves the base preparation and evaluation requests unchanged.
A report records only the semantic identities already verified at its stage. An early refusal does not invent a canonical input or program identity. Later qualification and evidence reports retain the same profile work identity for that submission.
11.1 Keep source, program, and artifact identities separate
Source identity identifies the exact source bytes. Program identity identifies canonical resolved code under its fixed dependencies. Artifact identity identifies engine bytes. These identities use separate versioned domains. A 1.x identity retains its historical meaning. A 2.0 record uses a new domain. Canonicalization identifies one canonical form. It does not decide equivalence between different programs. Profile work has a separate identity for the submitted request data, versioned profile work contract, and profile host budget. It does not replace the semantic request identity.
A source edit can preserve the program that runs. An engine can carry that program in different bytes. Separate identities keep those changes distinguishable.
Request identity binds the complete semantic request. Changing any of its semantic inputs makes a different request. Product, engine, platform, cache state, and source presentation do not change the identity of an admitted semantic request.
Limits can change whether the same rule returns or stops. Recording them makes the request reproducible. The same request has the same meaning across products.
Every named record in this chapter uses the exact lispex.datum/2 packet. A record is an immutable proper list of dotted pairs. Its keys are strings in unsigned UTF-8 byte order. Each declared field occurs exactly once. All fields are mandatory. An optional value uses the empty or singleton vector from the table. Reject duplicate, missing, unknown, or unordered fields. A decoder does not repair a record. A nested byte packet is a bytevector containing the complete packet.
One value codec gives identities, reports, receipts, and evidence the same exact framing. Closed records prevent products from silently ignoring a field. Explicit absence cannot be confused with false, an empty list, or an empty string.
11.4 Use separated SHA-256 identity domains
An identity uses lispex.identity/2. Its digest is SHA-256 of the complete domain-separated input packet in the table. Use the SHA-256 algorithm in the August 2015 edition of FIPS 180-4. Every supported domain has one payload schema. Reject another digest length, an unknown domain, or a payload outside that schema. IdentityBytes is the complete canonical identity packet. A claimed digest remains unverified until its complete captured input and the required domain checks have been verified.
A complete record can determine a candidate hash while its quoted semantic identities remain claims. A candidate RequestIdentity does not verify its program, library, resource model, or canonical input. Their owning checks must finish before a semantic request marker is issued. A locally verified record identity does not promote nested identity claims. A byte comparison and semantic verification remain distinct even when their digest values agree.
A domain prevents one kind of object from standing in for another. One algorithm and one packet remove product choices from the digest input. A digest authenticates neither the program semantics nor its issuer by itself.
The identity comparison examples give complete compared packets and name the preimages each case actually checks. Fixed library and model claims are explicit when their semantic preimages are unavailable.
11.5 Identify the validated canonical module meaning
Project the validated prepared graph into the meaning records below. Preserve every supplied module, decoded name, binding relation, literal value, node kind, ordered child, group, clause, entry declaration, and tail flag. The two prepared encodings project to the same meaning. Compute module identities in dependency order. A dependency identity names its target module meaning. It never names source bytes or prepared bytes. Source and library modules retain distinct namespaces. Program identity binds the whole ordered module collection and the selected root entry.
Local numbering removes unrelated table offsets from a module digest. Explicit dependency meaning keeps source spelling and artifact encoding outside that digest. Retaining the canonical graph structure preserves occurrence order and the resource event contract without attempting arbitrary program equivalence.
Conditional forms use written alternatives.
11.6 Bind each request to its complete inputs
The tables define source, submission, preparation, evaluation, and profile work identity inputs. A semantic request includes the program, canonical input bytes, fixed semantics, resource model, and every evaluation limit. Profile work binds the captured submission, the verified profile work contract, and the effective finite profile host budget. It keeps that identity through admission, output qualification, and evidence work. Changing only the profile declaration, check contract, evidence inputs, or host budget leaves the base preparation and evaluation request unchanged. Reports include only identities whose domain checks completed.
For PrepareRequestRecord, validate the input identity according to its domain and the complete finite preparation limits. A source-bundle identity requires its name table, selected root, and captured source bytes; it does not require successful source reading. The fixed Unicode, library, and resource model need verified immutable witnesses for this request. expected_program is a domain-checked submitted claim. Keep a supplied claim in the request even if a later comparison rejects its digest. Its presence never creates a verified program marker. A completed program is not an extra prerequisite for a preparation request seal.
Different limits can change a deterministic stop. Host qualification has its own inputs and budget. Binding both requests separately makes each check reproducible without adding profile policy or host evidence to the canonical outcome.
The notation below describes Datum values. It is not a second wire codec.
Notation
Exact meaning
D(x)
The complete lispex.datum/2 encoding of Datum x
R{a=x,b=y}
A proper list of dotted string-keyed pairs in unsigned UTF-8 key order
Record key order
Compare unsigned UTF-8 octets lexicographically with the shorter equal prefix first
#(x...)
A vector in the declared order
Option(T) absent
#()
Option(T) present
#(value) with exactly one value of type T
Bytes
A bytevector
Text
A string preserving its exact Unicode scalars
Nat
A nonnegative exact integer
Bool
#f or #t
Named encoding
D(record) with the exact mandatory format string declared for that record
Nested identity
The Identity record itself rather than a display string
Nested named bytes
A bytevector holding the complete named packet including its magic and length
The notation is order-independent inside braces. The encoded record is ordered. For example, R{b=#f,a=0} denotes (("a" . 0) ("b" . #f)). Tables define the exact fields of each record. Extra extension fields are rejected. A variant has exactly the fields in its selected row. Lists used as language data retain their original order and meaning.
Canonical packet decoding finishes before named-record checks. For a decoded record, check the proper-list spine first. Then visit entries in list order and check pair shape, string key, duplicate key, and increasing key order. For a named record, next require a string format field and the expected supported format. For a variant, next require its typed discriminator and a supported variant. Then check missing fields, extra fields, and field types in key order. Required keys and extra keys are checked before interpreting the remaining field values. The first failed check ends validation. No unknown format receives a fallback interpretation.
Diagnostic values keep their catalog types. Its Nat and Integer payloads remain canonical decimal strings. Its DatumBytes payloads remain lowercase hexadecimal strings. Its Identity and ContractIdentity fields contain the nested identity record. These catalog fields do not become the Nat type in this table.
Record or operation
Exact value
Domain
Exactly one domain string from the identity domain table
Payload
The payload value required by the selected domain row
Exactly 32 octets with digest words in their specified order and the most significant octet first within each word
Hash input bound
Fewer than 2^64 bits under the SHA-256 algorithm
IdentityHex
Lowercase hexadecimal for every octet of IdentityBytes with no prefix or separators
Equality
Equal domain strings and equal digest octets
The SHA-256 definition is the Secure Hash Standard. IdentityHex is a transport spelling only where another contract requires text. A binary identity field contains Identity rather than IdentityHex. A digest field never contains hexadecimal text. No salt, source path, timestamp, host width, product label, or secret is added to a hash input. New contracts use a new versioned name or domain. A 1.x record keeps its original identity rules.
A hash input bound is a format bound rather than a work allowance. Reject an identity preimage whose bit length is at least 2^64. Do not truncate the input, reduce its length modulo a word size, or publish a prefix digest. If length checking, encoding, or hashing cannot complete within its finite account, no identity is verified. Complete byte capture alone does not produce an identity. A later identity failure does not replace an earlier committed diagnostic or a completed canonical outcome.
A failed identity reservation keeps the diagnostic of its owning account and phase. Profile admission, qualification, and evidence use their corresponding phase with profile.budget. Standalone verification work uses verify/verification.budget. Their budget field identifies the denied host axis; a work reservation uses work. A physical host failure follows the host diagnostic contract. Source/preparation or evaluation account failures keep their own existing diagnostics. Identity encoding introduces no universal hash-failure code and never transfers work to a guest account. An earlier committed failure remains first.
Each identity in the table is H(domain,payload) for its row. The payload is the exact value shown in the final column.
IdentityArtifactKind is exactly product, engine, or prepared. Its format field identifies the versioned artifact format being admitted. Its bytes field contains that artifact alone. A source sidecar, signature, package path, or transport wrapper is excluded unless it is part of the identified artifact format itself. Artifact identity does not assert that those bytes implement the claimed program. IdentityArtifactKind is local to this identity schema. The diagnostic catalog retains its distinct ArtifactKind values.
CanonicalInputBytes must pass the canonical Datum decoder. A source identity can be verified for an unreadable source stream. A module, program, input, or profile identity requires that domain's semantic validation. An outcome or receipt identity requires its complete canonical shape and local field checks. That verification does not establish execution or verify objects merely named in its identity fields. Hashing a complete but invalid record cannot mark that semantic identity as verified.
The kind selects the owning contract family. The table gives the definitions owned or consumed here. Other kinds use their owning chapter's versioned declarative definition. The name is the versioned name of the definition. The definition is the canonical declarative value for that name. It is not a document's prose, an engine binary, or a caller's replacement definition. A product verifies the supplied definition against the selected supported contract before marking its identity verified.
R{format="lispex.evidence-requirement/2",mode="none"} or R{format="lispex.evidence-requirement/2",mode="signed-execution"}
The base/2 name requires profile base in its definition. The vouch/2 name requires profile vouch/2. These two fixed profile contracts can be checked before reading a submitted declaration. Their identity differs from the identity of that declaration.
The Unicode definition denotes the complete adopted Unicode operation rules. It does not allow a product to substitute its host Unicode tables. The profile work definition denotes the complete check schedule and schema traversal in Profiles. Its resource model supplies the host tariffs and units for that schedule. For one ProfileWorkInput, this model identity must equal budget.resource_model. The selected host model must support every event and finite field of the profile work contract. A mismatched or unsupported host model is refused before that model is used. The host model need not equal the preparation or evaluation resource model. It never replaces either model implicitly. The evidence requirement mode has the complete meaning specified in Profiles and the evidence envelope rule.
Resources defines the complete model declaration and default axis data. Identity encoding consumes that declaration without adding its digest to the preimage. The model definition rule fixes the order before budget wrappers are resolved. A missing, unsupported, or mismatched declaration is refused.
An unsupported requested capability can still appear as submitted identity data in a diagnostic. That quotation does not verify the capability or its contract. A claimed engine contract identity is distinct from the identity of actual engine artifact bytes. A report does not promote quoted diagnostic data into its verified identity bindings.
The Unicode contract is a prior semantic input. It excludes its own identity and identities that depend on it. Resources owns the corresponding model dependency requirements. Every dependent identity uses already verified explicit semantic inputs. An identity does not authorize a host lookup or dependency discovery.
The input is the validated canonical graph from Preparation. This projection does not add a source form or change that graph.
Projection step
Required mapping
Module ownership
An import, native member, or declaration walk belongs to its containing module
Local bindings
Filter the canonical binding table to that module and number the retained entries from zero
Local nodes
Filter canonical node preorder to that module and number the retained entries from zero
Omit their serialized bytes from the meaning projection after validating them
Site records are derived from the retained node, group, and clause occurrences under the fixed event contract. The prepared validator still checks every site and role before this projection. Dropping a site field here does not permit an invalid or altered site in an artifact. No program identity or global program offset enters a module digest through a site field. Every occurrence remains separate in the local node table and its structural parent relation.
All binding references are translated by their declaration owner. Do not chase an imported alias beyond the binding selected by the canonical graph. An imported target and its declared public export remain explicit in the import record. A reference into the library names its actual verified library module. An external reference must be authorized by the original dependency or library enclosure rules.
Binding and use names remain in the meaning record. Changing a local binding name can therefore change program identity. Equivalent reader escapes and delimiter spelling preserve the decoded name. The source rules alone decide which source forms share a canonical graph. No optimizer equivalence, alpha renaming, constant folding, or unused-code removal is added here.
The following records use only the fields in their rows. Collections use vectors. Indices are the local indices from the projection table.
A source module has exactly one present library identity. A library module has an absent library identity. Every module keeps the fixed Unicode and resource model identities used by its canonical graph. Library modules depend only on library modules. Their digests never include the identity of the whole library that contains them.
Dependencies use ModuleRef values for every original dependency. Sort those values by the UTF-8 bytes of kind and then name. Reject repeated namespace and name pairs. Imports retain written clause order. Exports retain unsigned UTF-8 public-name order. Native bindings, groups, bindings, and nodes retain the canonical Preparation order. A declared entry keeps its public export name and the graph's resolved binding.
The binding role is the exact role number from Preparation. Role 7 has one present native semantic member name. All other roles have an absent member value. Local declaration lists contain local BindingRef values only. A target ModuleRef must match the computed meaning identity of that target. These records select no native kernel members and no final kernel count.
NodeKind is exactly one tag in this table. The fields column is the complete vector stored in NodeMeaning. The existing prepared graph validation fixes the child arities and admitted source forms. An if records its test and both branch indices. Cond retains its required final else clause under the conditional grammar.
NodeKind
Fields vector
literal
#(Datum)
use
#(Text BindingRef)
lambda
#(#(BindingRef...) Option(BindingRef) Nat)
call
#(Nat #(Nat...))
if
#(Nat Nat Nat)
sequence
#(#(Nat...))
let
#(#(BindingRef...) #(Nat...) Nat)
letrec
#(#(BindingRef...) #(Nat...) Nat)
guard
#(BindingRef Nat #(ClauseMeaning...))
body
#(Option(InternalGroupMeaning) #(Nat...))
letstar
#(#(BindingRef...) #(Nat...) Nat)
namedlet
#(BindingRef #(BindingRef...) #(Nat...) Nat)
and
#(#(Nat...))
or
#(#(Nat...))
cond
#(#(ClauseMeaning...))
Clause kind
Fields vector
0
#(test-node body-node)
1
#(test-node)
2
#(test-node receiver-node)
3
#(else-body-node)
Node indices are structural references within the same module. Binding references retain the exact lexical target selected by Preparation. A sequential group has its single binding and initializer. A recursive group retains every adjacent lambda binding and initializer. A present internal group retains every leading internal definition. This encoding does not flatten bodies, synthesize calls, or merge equal literals.
LibraryMeaning contains the complete fixed library closure in its canonical dependency order. Its enclosure contains every public lexical library binding in unsigned UTF-8 name order. Each binding names the verified module and local binding index that supply it. The public inventory and aliases remain those fixed by the Standard library chapter. The semantic library record is independent of the engine's native or guest implementation strategy. A private replacement must implement the same selected canonical library meaning.
ProgramMeaning contains the full library closure followed by every submitted source module. The module order is the canonical initialization order from Preparation. All root and entry fields must match the declared root entry in that graph. The root is a source ModuleRef. The entry name is the declared public export name. Its ProgramBinding is the actual binding already selected by the entry contract. There is no host entry override.
Compute library module digests in dependency order. Then compute LibraryIdentity from the full library record. Next compute source module digests in source dependency order. Finally compute ProgramIdentity. Every dependency record uses the computed target ModuleIdentity. The dependency graph is acyclic under Preparation. No step includes its own digest.
The library and program header identities must match every corresponding child record. Their resource model is the model of the prepared semantic graph. A profile host budget never substitutes its separate host model into these records. A resource model change can change module, library, and program identities. Changing only a finite evaluation limit leaves those identities unchanged. The distinct request identity still binds the selected model and limits explicitly.
The prepared wire formats retain their own bytes. Their dependency IdentityBytes fields contain the target ModuleIdentity packet from this contract. A resolved/1 encoding and a bytecode/1 encoding of the same validated graph have equal ProgramIdentity. Their artifact identities differ when their exact bytes differ.
Convert one explicit external record into canonical input Datum bytes
verify
Receipt comparison and any requested evidence work
replay
Exact replay against the recorded request and receipt
graph
Meaning graph production without guest evaluation
OperandRole is exactly one of the names below.
OperandRole
Captured bytes
bundle
Exact submitted source bundle packet
artifact
Exact submitted prepared artifact packet
input
Exact submitted input bytes through their complete end
request
Exact recorded semantic request packet
expected
Exact expected receipt packet
actual
Exact actual receipt packet
profile-declaration
Exact profile request packet
prepare-limits
Exact supplied preparation limit packet
evaluate-limits
Exact supplied evaluation limit packet
profile-limits
Exact supplied profile host budget packet
evidence
Exact explicitly supplied evidence packet
trust
Exact explicitly supplied trust policy packet
SourceBundleInput requires a valid unique source name table and a selected root in that table. It uses unsigned UTF-8 module-name order. It retains each source's exact octets through SourceIdentity. It need not have readable or valid source syntax. Transport ordering and host paths are not part of SourceBundleInput.
SubmissionRecord captures supplied operands before interpreting their content. The operand vector uses unsigned UTF-8 role order with no repeated role. An omitted operand has no vector member. The selection options retain their supplied exact text. An omitted selector has an absent Option even when a fixed default will later apply. The CLI command run maps to operation evaluate. The record-admission operation uses the explicit record request format from Profiles. Its input operand contains that request packet rather than an assumed canonical input packet. This operation name does not add a CLI command. Argument order, file paths, output destinations, environment data, and display preferences are excluded. Only the declared input bytes and selections are included.
A typed API obtains the same operand bytes from the named input encodings. A callback, accessor, opaque host object, or partially captured stream has no invented byte representation. If complete immutable capture fails, the report has no verified SubmissionIdentity. If capture completes but a packet is malformed, its exact bytes still have SubmissionIdentity. Missing input bytes are never represented as an empty packet. An invalid source name table can have SubmissionIdentity without SourceBundleIdentity or ProgramIdentity.
The preparation input identity and expected program field describe the performed preparation check. The expected program field is absent when no expected identity was supplied. Its presence does not mark that claimed program identity as verified. PrepareLimits is the complete validated finite preparation record owned by Resources. EvaluationLimits is that chapter's complete validated finite evaluation record. All symbolic fixture limit labels stand for concrete records in a submitted request. A limit name is not the serialized limit value.
Profiles defines CanonicalInputBytes. RequestRecord contains that full packet as a bytevector. Its program and fixed semantics fields must agree with the validated program meaning. Its limits are effective values after the selected preset is resolved. Changing a limit changes RequestIdentity even if the result happens to match. Preparation limits, source provenance, engine selection, profile declarations, and host work budgets are excluded from RequestRecord. The selected program already fixes its root and entry.
ProfileWorkInput accepts only evaluate, record-admission, verify, and replay submissions. For evaluate, ProfileWorkInput has one present builtin ProfileContractIdentity for base/2 or vouch/2 and one present declaration packet. For record-admission, the builtin profile identity is present and the declaration packet is absent. For verify and replay, both fields are absent. These are the only admitted presence combinations. Standalone record-admission performs the fixed record conversion only. Input schema and evidence requirements wait for evaluation admission with a verified program. The submitted selection text remains in SubmissionRecord. The prepare and graph commands perform no profile work and produce no ProfileWorkIdentity. A present ProfileDeclarationBytes value is D of the captured declaration Datum in the profile request. The outer packet must pass canonical Datum decoding before this extraction. The declaration can still fail the profile declaration schema. For an evaluate request using base without an explicit declaration it contains the canonical base declaration. Verify and replay do not synthesize a declaration from unavailable program or library inputs. The complete supplied profile request packet remains in SubmissionRecord. ProfileHostBudget contains its required resource_model identity and the six finite Nat limit fields. The model field is metadata rather than a seventh charged axis. An explicit profile-limits operand supplies that complete record. Otherwise common-default resolves that complete record before work begins. The profile work contract definition must use the same resource_model identity as that record. Its definition and budget are verified before their bounded ProfileWorkIdentity computation can complete. Changing this host model changes the profile work binding. It changes no field in PrepareRequestRecord, RequestRecord, or ProgramMeaning. Standalone verify and record-admission therefore need no evaluation request to select their host model. The selected profile declaration can still fail its later schema checks. Its raw declaration bytes do not invent a verified ProfileDeclarationIdentity.
A generated report, receipt, evidence envelope, or signature is not added to the submitted input. The work identity therefore stays constant as those outputs become available. Explicitly supplied evidence and trust bytes are already bound through SubmissionRecord. A signature's optional profile work identity names the original issuance work. It is not required to equal a later verify or replay operation's work identity.
Before replay evaluation, the host can decode the outer RequestRecord and keep input_bytes opaque. It can compute a candidate H value from those exact bytes and compare it with the expected receipt's request field. That check proves a serialized byte binding only. It does not create a verified InputIdentity or RequestIdentity. Replay verifies the expected receipt's requested evidence after that byte comparison. Only then does the authoritative canonical input decoder spend EvaluationLimits. Successful decoding completes InputIdentity and RequestIdentity verification before guest entry. An input decoding failure leaves both verified markers absent. There is no second host decoder and no transfer of canonical decoding work to the profile account.
Preparation request sealing consumes the fixed dependency witnesses described by the preparation report rule. A supplied expected_program is checked for the ProgramIdentity domain and canonical record shape. Equality with the prepared program belongs to the later requested comparison. Removing a disagreeing claim would change the request that was performed. A failure reporter retains an existing seal and does not start witness verification or hash work to fill an absent field.
Every row also requires complete bounded encoding and SHA-256 computation for that identity. A captured input or a decoded digest packet alone does not satisfy a row.
Available validation
Verified identities that can be reported
Complete immutable operand capture and its completed digest
SubmissionIdentity
Complete exact source octets and their completed digest
SourceIdentity
Valid unique source name table and root
SourceBundleIdentity
Complete checked semantic contract definition
The matching typed ContractIdentity
Checked fixed library closure and enclosure
LibraryIdentity
Checked canonical module graph and dependency meanings
Program, canonical input, matching fixed semantics, and effective evaluation limits
RequestIdentity
Complete submission identity, operation-appropriate profile fields, matching checked host model and work contract, and effective host budget
ProfileWorkIdentity
Completed profile declaration validation
ProfileDeclarationIdentity
Canonical outcome or receipt packet with valid closed fields
OutcomeIdentity or ReceiptIdentity for that record
An identity has no verified flag inside its digest packet. A report's verified marker records which of these checks completed. A caller's asserted identity, a decoded digest packet, and a recomputed semantic identity are distinct states. A report never promotes an asserted identity by copying a Boolean from submitted data. If a stage cannot complete capture, domain checks, encoding, or hashing, its identity field is absent and it has no verified marker. This applies to submission and source identities as well as semantic identities. A report can include a source member or source span only after that source identity is verified. The report format owns the reason for that absence.
Identity work uses the finite account of the stage that performs it. Profile checks use the separate profile host account. Neither this encoding nor a cached digest changes the canonical semantic event schedule. Tariff coefficients, allocation units, finite defaults, and physical envelopes remain with Resources.
Receipt record validation checks its own canonical fields and identity packet shapes. It does not establish that a claimed program ran or that a claimed request was valid. A receipt operand alone cannot verify the program or request preimages named inside it. It also cannot verify membership of a claimed site in an unavailable program. Verify therefore compares those recorded claims without adding them to verified semantic bindings. It can recompute the receipt identity from the complete canonical receipt packet. Requested signature verification then authenticates that exact record under the supplied trust policy.
A replay byte-binding comparison is distinct from a verified semantic request. The canonical input decoder remains authoritative for the inner input packet. Before a canonical input is accepted, malformed input uses admission and input.codec. Exhaustion before RequestIdentity exists uses admission and input.resource. The charged account remains EvaluationLimits under the diagnostic catalog.
For evaluate, operation-appropriate fields require the checked builtin profile contract and captured declaration bytes. For record-admission, the builtin profile contract is present and declaration bytes are absent. That operation performs the fixed record conversion without program schema or evidence qualification. For verify and replay, both are absent and no profile declaration identity is invented. Standalone receipt verification can therefore identify its host work without possessing the program or its library.
A finite capture or hash refusal keeps the phase and first cause selected by the diagnostic catalog. The absence of a submission identity does not turn that refusal into an operational failure. Incomplete input transport keeps its separate attempt-report boundary. A hash format overflow produces no digest and no verified marker. If an outcome already completed, later identity or report work preserves that outcome and its eligible receipt. A product never finishes a digest by exceeding its budget merely to populate a report field.
A canonical outcome records what happened to the rule evaluation. Success contains exactly one Datum. A deterministic failure contains its stable phase, code, and typed data. A resource failure also identifies its exhausted axis.
An evaluation failure uses a stable site in the canonical program. Source paths, line numbers, translated messages, and stacks are presentation data. CLI and diagnostics defines their presentation. A failure before canonical code exists is recorded against the exact source instead.
11.7 Compare the complete semantic outcome
A successful evaluation returns one datum. A deterministic failure records its stable phase, code, typed parameters, and canonical program site. A resource failure also records the exhausted axis. Human messages, source coordinates, host paths, and stacks remain outside the canonical outcome.
A display setting must not change which failure occurred. Stable data lets callers compare results across products. The canonical outcome stays separate from execution evidence.
11.8 Bind early preparation failures to their source
A read or normalization failure before canonical code exists produces a source-bound preparation report. Include the exact source identity only after its bounded identity computation completed; otherwise leave that binding absent and preserve the first diagnostic. The report does not invent a program identity or a canonical evaluation site. Source coordinates belong to the report for that source.
When the source identity is computed, retain the exact original byte length with its local verification witness. A whole-member span uses byte_start = 0 and that retained byte length as byte_end. It counts original UTF-8 octets and line endings before decoding or normalization. Check both bounds against that witness without rereading the failed source or allocating a replacement source copy. Use exact natural arithmetic independent of host word width. A received source digest and claimed length alone remain assertions; a separate verifier needs the exact preimage and its own finite validation account to establish them.
An unreadable source has no resolved program to identify. Keeping its source binding preserves the evidence needed to diagnose it. Exact source stays distinct from canonical code.
Keeping the original extent with the source witness makes failure reporting independent of a mutable file, a stopped source stream, or normalized text. The length is local verification data; it adds no field to Identity or PrepareReport.
A preparation failure before program identity exists
Encode an outcome with the closed record below. A value outcome contains exactly one Datum. A failure outcome contains the complete diagnostic and a qualified canonical site. Its phase is evaluate. Use the existing diagnostic catalog without coercion or renamed codes. The site program must equal the verified program for the request. Malformed input before a request identity exists produces an admission report. Operational failures use an attempt report. Both retain their existing phase boundaries.
A typed value keeps exact numbers and aggregate shape. A qualified site identifies the same semantic failure across products. Separate reports prevent an incomplete attempt from becoming an evaluation result.
11.10 Portable receipt bytes
A receipt contains its program identity, semantic request identity, and exact canonical outcome packet. Receipt decoding validates its own fields and nested packet shapes. A failure site must name the receipt program. When complete program and request operands are available, check their bindings and site membership too. A receipt operand alone does not verify those preimages. Standalone verify compares the recorded program and request assertions. An admitted receipt has one complete canonical encoding. A value, an uncaught language failure, and a deterministic resource stop are eligible. Admission and preparation reports are not eligible. Preserve the completed receipt when qualification, evidence, or delivery later fails.
The receipt records the semantic result under the complete request. It remains portable when the product, engine, signer, cache, or host presentation changes.
11.11 Preparation report fields
Preparation returns the source report below for success or a deterministic preparation failure. Include a submission identity only after complete capture and bounded identity computation succeed. A preparation request needs immutable verified witnesses for its fixed Unicode, library, and resource model. Bind those witnesses to the performed preparation input and complete finite limits before sealing the request. Before those witnesses or the bounded request hash complete, prepare_request is absent. Reusing an already verified immutable dependency is permitted; copying a received identity record is insufficient. Preserve a completed request seal if a later preparation check fails. Include a program identity only after complete program verification succeeds. A failure in one source member identifies that source only after its identity computation succeeds. The canonical span covers the whole original source member using its retained exact byte length. Reporting performs no new source read, identity hash, or dependency check after the first failure. An unavailable identity never replaces that diagnostic. No preparation failure receives an evaluation site or evaluation receipt.
Complete source bytes can remain identifiable when decoding or reading fails. Bounded hashing must finish before a report claims that binding. Whole member spans give every product the same source binding without making editor coordinates part of program meaning.
Fixed dependency witnesses can exist before the complete program. A read failure therefore leaves prepare_request absent when no seal exists, but preserves a seal already completed for that same immutable request. Neither a diagnostic quotation nor a received verified array supplies those witnesses.
11.12 One command result packet
Every CLI or direct host result that emits a report uses one complete packet from the table below. Select its numeric status through the exit mapping. Secure the complete emergency payload and outer framing before normal work. Serialize the packet before publishing it. Keep trace status and optional trace bytes in the separate outer trace field. Keep eligible outcome and receipt packets in the result even when a later report records refusal or interruption. The receipt output file contains exactly the same receipt packet. A process killed before reporting has no completed command record. Product labels, human messages, paths, and counters are not canonical result fields.
Once the first primary-channel octet is delivered, freeze the complete selected packet and its serialized status. Continue only with unchanged bytes of that same packet where delivery can continue. Report a later interruption through the existing transport or process error boundary. A status 50 replacement is eligible only with confirmed zero delivery, no pending write, and a complete canonical candidate preserving every completed component. The command/CLI completion classification follows the existing exit mapping. A complete ABI reply retains transport success 0.
One envelope gives all products the same command boundary. Distinct report slots preserve the first completed semantic result and the later host failure.
Selected packet bytes are immutable and stay separate from later transport completion. Confirmed zero with no pending write prevents two replies from reaching one primary channel.
The common record notation and identity records come from Identity encoding. Each named byte form is one complete lispex.datum/2 packet.
The exact lowercase hexadecimal string required by Diagnostics
Identity
The nested Identity record
Text, enum, or Boolean
The same string or Boolean
DataPath
A vector of the declared tagged R records
The typed fields keep their existing values and checks. Only the enclosing object and array representations are supplied here. DiagnosticPayloadBytes includes its own complete Datum framing. It contains the typed diagnostic alone. DiagnosticBytes adds the standalone diagnostic record and its format field. Resource diagnostic channels and terminal causes use DiagnosticPayloadBytes. Surrounding reports import Diagnostic as a record value when their field is not bytes. CanonicalSiteBytes follows the site contract. It is program local. QualifiedSite adds the program identity outside those local bytes.
Outcome check
Requirement
Value
Exactly format, kind, and value
Failure
Exactly format, kind, diagnostic, and site
Failure phase
evaluate
Failure code
An evaluation row from the diagnostic catalog
Resource failure
resource.exhausted with its complete stage, axis, and event data
Receipt program with a verified request operand
Equal to that request program
Receipt request with a complete recorded request operand
Equal to its recomputed candidate byte binding. A verified marker also requires canonical input validation
Failure site program
Equal to the receipt program
Receipt outcome packet
Complete canonical closed fields and canonical site encoding. Check site membership when the program is available
Admission checks packet framing before record shape. It then checks fields in unsigned UTF-8 key order. It checks nested packets when reaching their field. It completes local type checks before cross field identity checks. Cross field checks follow program, request, then outcome. A receipt alone verifies its own record identity. Its nested program and request identities remain recorded assertions until their preimages are checked. Unknown diagnostic identities use artifact.invalid with unknown-diagnostic. Other format defects use artifact.invalid with invalid-format. An inconsistent supplied identity uses artifact.invalid with identity-mismatch. All three use phase admission and the catalog artifact kind.
Preparation work, profile work, evidence, elapsed time, and work_used are absent from Receipt. There is no success-only receipt filter.
Form
Exact shape
VerifiedIdentity
the verified identity marker from Admission reports
Present only after complete immutable capture and bounded identity computation succeed
prepare_request
Present only after input and limits validation, verified fixed Unicode/library/model witnesses, and bounded request hashing complete; otherwise absent
sources
Verified source members in module name UTF-8 order
sources before a valid source name table
Empty vector
program on prepared
Present and verified
program on failed
Absent
diagnostic on prepared
Absent
diagnostic on failed
One existing decode, read, normalize, resolve, or prepare diagnostic
source_span for a failure in one verified source member
Present with that member identity and exact byte length
source_span for a whole bundle failure or prepared input
Absent
byte_start
Zero
byte_end
Exact original source byte length retained with the source witness
verified
Only completed identity checks under the separate marker rule
Member selection follows the existing preparation order. The span identifies original source bytes before UTF-8 decoding. The report has no invented program identity after a read failure. Source paths, line numbers, and columns are host presentation linked to this source span. A complete captured operand can still have no computed identity. Sources includes only source identities whose bounded computations completed. Omit a source span if its source identity is unavailable. A missing submission or source identity does not change the original phase or first diagnostic. Incomplete input transport uses the separate attempt report.
SourceSpan validation uses the retained original extent. It performs no post-failure source traversal, decoding, rehash, or copy allocation. The SourceIdentity wire record carries no byte length. A received source_span and verified marker do not establish the original extent without the corresponding verified source preimage.
prepared with the selected prepared program packet
run completes evaluation
outcome with CanonicalOutcomeBytes
verify compares admitted receipts
verification with ComparisonReportBytes
graph succeeds
graph with the named graph packet
replay compares completed evaluation
replay with ComparisonReportBytes
replay completes evaluation but later host work stops comparison
outcome with CanonicalOutcomeBytes
Any command before a primary payload exists
Absent
Direct host calls use the same envelope with an empty command option. The Command enum names only CLI commands. Host operation names do not extend it.
Host operation
Successful primary payload
Reports and receipt
Open
Absent
Status 0 and no receipt. The typed result separately returns its local Product
Build
No command packet
The typed result returns its local constructed value
prepare or load
prepared with PreparedArtifactBytes
Preparation report and no receipt
evaluate or profile evaluation
outcome with CanonicalOutcomeBytes
Eligible receipt and any required profile report
export
prepared with PreparedArtifactBytes
No new preparation request or evaluation receipt
graph
graph with GraphBytes
No evaluation receipt
record admission
input with CanonicalInputBytes
No evaluation outcome or receipt
A refused Open or Build returns CommandResultBytes with an admission report. Other direct calls use the report for their actual failing phase. Open, Build, and export leave submission absent when no defined SubmissionRecord applies. They create no substitute submission identity. Export failure during its preparation account uses a failed preparation report. Its prepare_request remains absent. A successful export does not claim to seal or prepare another program.
Prepared and graph payload bytes retain their own formats. The enclosing command record still uses lispex.datum/2. Every other payload bytevector contains the complete named Datum packet.
Report slot
Presence
preparation
Whenever preparation or loading completes, or a preparation-account export fails
admission
When an admission refusal ends the operation
profile
Whenever required qualification or evidence work completes or refuses after evaluation
evidence
When standalone verify or replay checks supplied evidence
attempt
When invocation, ingestion, render, or host activity fails. Also when standalone verify or replay host work exhausts its verification budget
terminal
The complete EmergencyTerminalBytes when reserved emergency reporting supplies the final failure payload
A slot contains at most one report. The terminal slot imports the emergency terminal schema. It is the final failure payload in Reports. If normal reporting cannot complete within its account, that unfinished slot is absent. The terminal payload retains the complete first cause and location. Already completed report slots, outcome bytes, and receipt bytes remain unchanged. The outer status follows the existing diagnostic phase mapping. A terminal payload does not create an evaluation receipt.
The outer trace option is separate from Reports, Outcome, and Receipt. It is absent before the evaluation trace stage is reached. After that stage it contains the host trace status. Disabled and unavailable have no trace bytes. The other three statuses contain the complete TraceBytes with the required footer. Trace saturation changes only this separate state. It never creates a terminal language failure or changes command status.
Before normal work, secure EmergencyTerminalBound and EmergencyFramingBound under the emergency capacity rule. The outer bound covers all required fields, retained payload and receipt packets, report slots, trace framing, and transport framing. Requested trace storage remains in its separate finite account. Ordinary work starts only after both emergency areas are backed. These reservations cannot borrow evaluation or ordinary diagnostic capacity. The selected reports describe the same immutable submission. A report status and its diagnostic must agree. An attempt report with incomplete ingestion has no submission identity. A completed evaluation always retains its receipt packet. Verify never emits a new evaluation receipt. Replay retains its actual evaluation receipt after comparison mismatch. The expected receipt remains inside the comparison report. After output interruption, retain the complete selected packet and every completed report, payload, receipt, and trace in memory. Delivery state belongs to the existing host interface; it is not a new CommandResult field.
The first delivered primary-channel octet freezes the selected packet, including its serialized status. Subsequent writes, if permitted by the transport, use only the unchanged remaining bytes of that packet. Do not patch its status, replace its bytes, restart it as a second packet, or append another packet on that channel. The same rule applies after all packet octets were written and a later flush or completion acknowledgment fails.
Before any primary octet is delivered, a complete status 50 candidate may replace the pending packet only when every guard below holds. An attempted replacement never edits the original in place.
Replacement guard
Required observation
Delivery count
The adapter confirms exactly zero primary octets delivered
Pending delivery
No queued or in-flight write can later publish bytes from the old packet
Complete candidate
One complete canonical CommandResultBytes packet with status 50 and valid closed fields, nested packets, diagnostics, and report relationships
Operation binding
The same already retained operation, command option, and immutable submission binding, including an absent submission when appropriate
Completed data
Every completed report slot, payload kind and bytes, receipt bytes, and trace state and bytes remains byte-for-byte unchanged
Added failure report
New render or host failure data fits an available slot or the reserved terminal path without overwriting a completed slot
Reserved support
Construction, local checks, and publication fit the previously secured host and emergency support
Zero in a local counter is insufficient while a write remains pending. An unknown delivered count is not confirmed zero. An adapter must finish or withdraw pending delivery and confirm zero before permitting replacement. The retained operation binding was established before failure. Replacement consumes it without rehashing source, revalidating program or request identities, or inventing a new submission.
The candidate must satisfy the complete closed contract before the atomic selection change. Typed construction may establish that validity; decoding a serialized candidate again is not required. Candidate construction failure, incomplete bytes, invalid fields, a binding mismatch, or any changed completed component leaves the original packet selected and retained. In particular, a completed attempt or terminal slot cannot be discarded to make room for a newer delivery diagnostic. When no complete preserving candidate fits, report delivery failure through the existing host boundary.
The command/CLI completion classification for interrupted delivery is 50 even when the retained or already delivered packet carries 0, 20, 21, or another earlier status. After output starts, that command completion classification is not written back into the packet. A complete packet received before a failing flush retains its original serialized status. The exit mapping still preserves evaluation status 20 or 21 against later qualification or evidence refusal; delivery interruption is the separate command completion case.
The transport adapter supplies truthful delivery counts, pending-write state, write/flush results, and the existing transport-error observation. These physical observations do not follow merely from constructing or checking a result packet.
Use the existing numeric statuses. The envelope adds no new status or diagnostic code. All reports use their named byte contracts. Nested records use their record values rather than an extra packet unless the field is explicitly bytes. Receipt output adds no banner, newline, or second packet.
Envelope invariant
Exact requirement
Recognized command token
The command option contains that exact command
Missing or unknown CLI command token
The command option is empty and the status is 2
Direct host operation
The command option is empty and status follows the operation result
Known command with invalid options
Preserve the recognized command in the option
Attempt report command
Equal to the outer command option
Attempt stage outside host phase
Equal to diagnostic.phase
Attempt stage for host phase
Equal to diagnostic.data.stage
Attempt verification budget failure
Phase verify with verification.budget and status 42
Outcome payload and outer receipt
Payload bytes equal the receipt outcome_bytes exactly
Replay comparison and outer receipt
Comparison actual_receipt_bytes equals the outer receipt exactly
Profile report and outer receipt
Profile report receipt_bytes equals the outer receipt exactly
Comparison and standalone evidence report
The two evidence verification records are equal when both are present
Verify evidence target
The actual receipt
Replay evidence target
The expected receipt
Prepare, graph, and verify outer receipt
Empty option
Run, replay, or direct host evaluation after eligible evaluation
Present option with the actual receipt
A verification budget failure before comparison completion has no partial comparison payload. After replay evaluation, this failure retains an outcome payload and its actual receipt. The expected receipt remains an unchanged supplied operand. Quoted requested identities inside diagnostics are input data. They do not create verified report markers.
The command/CLI completion classification does not change the host ABI transport call-status enum, which remains 0, 1, or 2. A complete ABI reply still uses transport success 0, including a complete refusal or failure report. The delivery rule introduces no status field, channel, or API. The physical adapter maps its existing transport-error observation to the existing command/CLI classification.
A portable receipt binds a semantic request to its completed canonical outcome. The same request and outcome produce the same portable semantic record. The request includes the finite limits and resource model needed to interpret a resource stop.
Keep exact source provenance, engine artifact identity, and issuance details alongside the receipt. The resource contract defines semantic resource events. Operational usage counters describe an execution and stay outside the portable receipt.
11.13 Bind a receipt to the request and outcome
A portable receipt binds the semantic request identity to the completed canonical outcome. Deterministic language failures and resource stops retain their failure outcomes. The receipt excludes work_used, cache state, wall time, host paths, engine identity, and issuance details. Source provenance and execution evidence attach separately.
Resource usage and timing describe how a host ran the request. They cannot change the result being replayed. Resource usage and timing stay outside the portable record.
Admission refusals stay separate from evaluation receipts.
Keep admission refusal, language failure, resource exhaustion, operational interruption, and engine defect distinct. Admission refusal produces an admission report tied to the submitted request data. It produces no canonical evaluation outcome and no evaluation receipt. The report records the refused submission and the identities that admission has verified. A deterministic resource stop is a terminal semantic failure. Operational interruption and engine defect produce no canonical evaluation outcome or semantic receipt. They cannot be recorded as successful rule evaluations. A qualification or evidence refusal after evaluation produces a separate profile work report. It preserves the completed canonical outcome and evaluation receipt eligibility.
An admission report identifies a refused submission without claiming an evaluation. A host interruption says that an attempt did not complete. Treating either as a rule result would invent an outcome. Admission and host interruption reports stay separate from evaluation outcomes.
Admission refusals stay separate from evaluation receipts.
A verified marker records a recomputed identity and its checked role. Include it only after the complete identity input and its declared contract pass validation and bounded hashing completes. The marker never copies an unverified claim from an operand. Missing knowledge uses an absent option or empty vector. A verified evidence identity identifies its canonical bytes. Authentication still requires the separate signature and trust checks. Sort markers by role and then index. Reject repeated role and index pairs. A diagnostic may quote a requested identity as submitted data. Such a quotation is not a verified identity binding.
A reader can distinguish a byte binding from a claim made by an untrusted input. Keeping authentication separate prevents a digest check from implying issuer trust.
11.16 Admission report bytes
An admission refusal uses the closed admission report below. Its submission identity is present only after complete immutable capture and bounded identity computation succeed. A profile work identity is present only after its captured input, effective budget, and check contract pass their identity checks. A captured declaration can still fail its later schema checks. Standalone verify and replay carry no selected profile declaration. The report carries the first admission diagnostic. It carries no evaluation outcome or receipt. An identity computation refusal leaves that binding absent and keeps the original diagnostic phase. Incomplete host ingestion uses an attempt report instead. Failed program verification never supplies a verified program marker.
When profile admission cannot reserve the next required identity hash within its admitted finite host work account, use admission/profile.budget. Its profile field names the selected builtin profile contract, and budget is work. This rule assumes that profile contract is already known. The hash produces no identity or verified marker unless its reservation, complete computation, and domain checks finish. The identity helper does not choose a different phase, charge EvaluationLimits, or replace the refusal with input.resource. Which hash occurs next follows the profile work schedule; reporting adds no hash or check.
Admission describes whether a submitted operation can begin. A completed bounded hash identifies exact submitted data while semantic identities may still be unavailable. An absent hash cannot imply a verified binding.
A profile admission identity hash refused by its host work budget uses admission/profile.budget. Other operations retain their own work accounts. A hash algorithm does not decide which operation failed. Effective host budgets, the profile checks, and their complete event schedule remain with the profile work contract.
11.17 Profile work reports preserve the receipt
A profile work report binds its verified profile work and semantic request to the exact completed receipt packet. Check output qualification before required evidence. A failed evaluation skips output qualification and retains its failure outcome. Required evidence may still examine that receipt. Stop at the first required profile refusal. The report records the checks that completed and those not reached. Preserve the original outcome and receipt bytes for every report status.
Profile qualification has its own result and budget. Carrying the original receipt makes that boundary visible and prevents a later refusal from rewriting language meaning.
The index is zero for a singleton role. Source indices select the verified source member table. Only the source role can have several entries. Every marker must match the report field or admitted operand with that role. An omitted marker means its verification did not complete. The strings claimed, trusted, and unknown are not marker states. An authenticated issuer appears only in an evidence verification report.
These are the marker roles used by the reports in this chapter. Other checked identities can occur within their validated preimages without gaining an additional marker role. An identity verification table states when a binding is known. It does not add fields or roles to a report.
The diagnostic phase is admission. AdmissionOperation names a report operation and adds no CLI command. Direct host calls use their exact operation name. Profile evaluation uses run because it performs that profile work operation. Its data keeps the exact fields from the existing catalog. Malformed declarations use request.invalid before a profile identity exists. A submitted claimed identity stays within the submission bytes until verified. The report has no outcome, receipt, or signature field. No adapter may fill these missing fields with a false success value. Report construction follows the existing diagnostic reservation order. The first committed diagnostic remains fixed. Submission is present only after complete capture and bounded identity computation succeed. A completed capture with an unfinished hash leaves submission absent. An absent submission identity also leaves profile_work absent. The identity fields never use a zero digest or a digest prefix as a placeholder.
Completed has no diagnostic. Refused has one diagnostic from its report stage. The evidence_report field is absent until evidence verification produces a report. A host budget refusal can precede that report. No skipped check is marked passed. The receipt request and program equal the corresponding report fields. The embedded outcome remains the exact completed language outcome. The profile work identity remains separate from the semantic request identity.
Before guest entry, reserve the terminal report capacity required by the profile host contract. That reservation includes the complete receipt packet and all required diagnostic fields. The selected finite evaluation limits bound the possible result and diagnostic sizes. The host keeps the immutable receipt even if later physical delivery fails. Reservation amounts and physical capacity proofs stay with the cost model freeze.
The report contains no signature over itself. An evidence envelope may bind the profile work identity and receipt. It never embeds the final profile work report or its own verification result. This prevents a circular signature input.
Keep a claimed program identity out of verified markers
Execution evidence describes the product and artifact that performed an evaluation. It binds that description to the request and outcome being reported. An evidence envelope can add an issuer, issuance time, and signature.
A signature authenticates the signed record and its signer under the selected trust policy. Product conformance evidence establishes whether the implementation follows the language contract. The calling application decides which external actions to permit.
A profile work report records qualification or evidence work after evaluation. It identifies the profile work, its stage, and whether the required host work completed. It binds the report to the verified semantic request and completed canonical outcome. A schema mismatch or exhausted profile host budget refuses the profile result. It preserves the canonical outcome and evaluation receipt eligibility.
A refusal before guest entry uses the admission report under the termination rule. That report identifies the same profile work and only the identities already verified. It produces no canonical evaluation outcome or evaluation receipt.
11.18 Verify evidence against its request and outcome
Execution evidence binds the product and engine artifact record to the reported request and outcome. Issuer identity and signatures belong to a separate envelope. The named envelope has no issuance time field. Signature verification authenticates that signed record under the caller's trust policy. It does not establish policy correctness or authorize external actions.
An evidence envelope contains one execution statement and one Ed25519 signature. Encode both records with the closed field tables below. The signed message is the complete Datum packet for the statement. The statement binds the exact portable receipt bytes and the asserted product and artifact identities. Its optional profile work identity describes the work being attested. It is not the identity of a later verification or replay. The envelope carries no profile work report.
One signed representation prevents products from authenticating different interpretations of a record. Binding exact receipt bytes preserves the completed language result. Keeping the report outside the statement prevents a signature from containing its own verification result.
11.20 Verify evidence under explicit offline trust
Verification uses the supplied policy and the fixed check order below. Every required check must succeed. A key is trusted only for its listed product and artifact tuple. An empty policy trusts no key. The verifier performs no issuer lookup and reads no clock. Evidence verification uses the finite profile host budget. Its report records an authenticated issuer only after binding, signature, and trust checks succeed. A refusal preserves every completed canonical outcome and portable receipt.
The same envelope can be accepted under one explicit policy and refused under another. Recording the policy makes that difference reproducible. A fixed check order preserves the first refusal and bounds cryptographic work. Signature authentication remains separate from language conformance and application authority.
The notation uses the identity encoding rule. D is one complete lispex.datum/2 packet. R is a closed record with canonical string keys. Every field is required. Options use the empty vector or a vector with one value.
Record
Field
Value
EvidenceStatement
format
"lispex.execution-statement/2"
EvidenceStatement
algorithm
"ed25519"
EvidenceStatement
issuer
Issuer identity derived from algorithm and public_key
EvidenceStatement
public_key
Bytevector with exactly 32 octets
EvidenceStatement
product
"native", "npm", or "wasm"
EvidenceStatement
product_artifact
Artifact identity computed with kind product
EvidenceStatement
engine_artifact
Artifact identity computed with kind engine
EvidenceStatement
receipt_bytes
Bytevector containing one complete PortableReceiptBytes packet
EvidenceStatement
source
Optional source or source bundle identity
EvidenceStatement
profile_work
Optional identity of the original attested profile work
EvidenceEnvelope
format
"lispex.evidence/2"
EvidenceEnvelope
statement
EvidenceStatement as a nested record
EvidenceEnvelope
signature
Bytevector with exactly 64 octets
Named bytes
Definition
EvidenceSignedBytes
D(EvidenceStatement)
EvidenceEnvelopeBytes
D(EvidenceEnvelope)
TrustPolicyBytes
D(TrustPolicy)
EvidenceVerificationBytes
D(EvidenceVerificationRecord)
The signature covers the statement packet including its framing. It does not sign the envelope packet or a display string. The public key uses raw octets. The format has no algorithm negotiation, certificate chain, timestamp, or extension field.
The statement authenticates the issuer's assertions about product and artifact identities. A verifier does not infer artifact content validation from that authentication. The signed profile_work remains an assertion about its original work. A later verifier preserves that scope and records its own work separately.
The optional source field declares its scope through its identity domain. A source identity names one exact source stream. A source bundle identity names the complete source set and root.
The deterministic signing procedure in RFC 8032 section 5.1.6
Message M
EvidenceSignedBytes
Public point A
Decode public_key with RFC 8032 section 5.1.3
Public subgroup
A != O and [L]A = O
Signature split
ENC(R) || ENC(S) with 32 octets in each part
Point encoding
Canonical RFC 8032 decoding with y < p and the required sign bit
Scalar
Little endian integer S with 0 <= S < L
Challenge
k = LE(SHA-512(ENC(R) || public_key || M)) mod L
Equation
[S]B = R + [k]A
Parameters
B, L, p, and O use the Ed25519 definitions in RFC 8032
Both points must decode successfully. A point with zero x coordinate uses a zero sign bit. The unmultiplied equation is required. Ed25519ctx and Ed25519ph are not accepted. Signing is a host operation over explicit data. This contract adds no guest primitive or implicit signer.
Trust is supplied as complete data. It has no implicit entries.
Record
Field
Value
TrustPolicy
format
"lispex.trust-policy/2"
TrustPolicy
issuers
Vector of TrustedIssuer records
TrustedIssuer
issuer
Issuer identity for its public key
TrustedIssuer
public_key
Bytevector with exactly 32 octets
TrustedIssuer
executions
Vector of TrustedExecution records
TrustedExecution
product
"native", "npm", or "wasm"
TrustedExecution
product_artifact
Artifact identity for the permitted product bytes
TrustedExecution
engine_artifact
Artifact identity for the permitted engine bytes
EvidenceRequirement
format
"lispex.evidence-requirement/2"
EvidenceRequirement
mode
"none" or "signed-execution"
Order issuer entries by unsigned IdentityBytes. Reject duplicate issuer identities before checking entry contents. Recompute every issuer from its raw public key. Check each key with the same canonical point and subgroup predicate used for signatures. Order each execution vector by the unsigned bytes of D(TrustedExecution). Reject duplicate execution records. The empty execution vector permits no execution.
none requires no envelope. signed-execution requires exactly one lispex.evidence/2 envelope verified under one explicit lispex.trust-policy/2 policy. Its target is the completed actual receipt for the profile request. A successful schema qualification cannot satisfy this evidence requirement.
The requirement identity is the contract identity with kind evidence-requirement, name lispex.evidence-requirement/2, and the exact requirement record as its definition. No issuer, key, product artifact, or engine artifact is trusted by default.
Checks run in the following order after the command reaches its evidence stage. Each step reserves profile host resources before its work. A failure ends this verification and preserves the first diagnostic.
Step
Check
Standalone refusal
1
Decode and validate the complete trust policy and its canonical order
verify, verification.failed, check = "trust"
2
Decode and validate the envelope and statement fields
verify, verification.failed, check = "evidence"
3
Require statement.receipt_bytes to equal the exact target receipt bytes
Recompute the issuer identity from the raw key and require equality
verify, verification.failed, check = "evidence"
5
Decode the public key and require the fixed subgroup predicate
verify, verification.failed, check = "signature"
6
Require the issuer, raw public key, and complete execution tuple in the policy
verify, verification.failed, check = "trust"
7
Decode the signature and check the fixed Ed25519 equation
verify, verification.failed, check = "signature"
8
Complete the evidence verification record
The appropriate report budget failure
profile-input covers the supplied policy and envelope bytes. profile-hash covers issuer, policy, envelope, and signature message hashing in byte order. profile-signature covers one public point or signature predicate in table order. profile-report covers report encoding. The profile work contract owns reservations. Numeric tariffs remain with the resource model.
Standalone verification budget exhaustion uses verify and verification.budget. Required profile evidence uses evidence and profile.budget. A missing required envelope or policy fails profile admission with profile.admission and evidence-prerequisite. An evidence producer that becomes unavailable after an admitted evaluation uses profile.evidence with unavailable-evidence. A target mismatch uses profile.evidence with evidence-mismatch. Other evidence refusal uses profile.evidence with invalid-evidence.
Verify checks supplied evidence only after the complete receipt comparison succeeds. Its target is the actual receipt. Replay checks supplied evidence against the expected receipt before evaluation. Profile evidence checks the completed actual receipt after output qualification. Profile admission can validate required input presence and trust policy structure before entry. It does not claim that a signature matches a result that has not completed.
The evidence record begins with an admitted target receipt. Its identity has already been checked. A refusal before that point uses the surrounding admission or profile work report.
Field
Value
format
"lispex.evidence-verification/2"
target_receipt
The admitted target receipt identity
evidence
Optional identity of the complete submitted envelope byte snapshot
trust_policy
Optional identity of the validated trust policy
status
"verified" or "refused"
authenticated_issuer
Optional issuer identity
diagnostic
Optional diagnostic field record
A verified record has an authenticated issuer and no diagnostic. A refused record has no authenticated issuer and has one diagnostic. An input identity appears only after the complete corresponding bytes have been hashed. The evidence byte identity does not claim a valid signature. The trust policy identity appears only after its canonical structure has been checked.
A profile work report may contain this record. It binds its own profile work identity to the same completed receipt. The evidence statement does not contain that final report. Refusal never removes or rewrites the canonical outcome or the receipt. An evaluation failure retains its existing command status when later evidence work also refuses.
Replay reconstructs the complete semantic request and compares canonical outcomes. Keep the canonical program, input, semantics, resource model, and finite limits available. Check those identities before treating a new evaluation as a replay.
An admitted engine can use a different artifact while evaluating that same request. Cache state, host paths, and display settings remain outside the comparison. Compare successful values and deterministic failures with the same care.
11.21 Replay only the complete same request
Replay reconstructs the complete semantic request and compares the complete canonical outcome. An admitted product must reproduce the value or the same failure phase, code, typed parameters, canonical site, and exhausted resource axis. Missing request components prevent exact replay. Changed semantic inputs identify a different request even when its result happens to match.
A matching result for one input cannot recover the request that produced it. Retaining every semantic input makes replay meaningful. The same semantic request requires the same outcome.
11.22 Replay an explicit complete recorded request
The replay byte request has exactly the fields below. Its recorded request supplies all semantic inputs. It supplies no replacement input, profile, resource model, or evaluation limit. Preparation of a source bundle is a separate step under PrepareLimits. The resulting prepared bytes enter this replay record. Validate the prepared program and recorded request against the expected receipt before guest entry. Verify supplied evidence against the expected receipt before evaluation. An admitted replay uses the recorded canonical input and EvaluationLimits without alteration.
A replay must reconstruct the request that produced the receipt. Explicit retained inputs prevent host defaults from changing that request. Keeping preparation and host work separate permits a different product to reproduce the same language result.
11.23 Encode the whole ordered comparison
Verify and replay use the shared comparison record below. Compare program identity first. Compare complete request identity only after program identity matches. Compare the complete canonical outcome only after both identities match. Stop at the first unequal component. Preserve both receipt packets. Verify checks requested evidence after a successful semantic comparison and binds it to the actual receipt. Replay includes the evidence result obtained for the expected receipt before evaluation. Evidence status does not rewrite the semantic comparison fields.
A value match cannot hide a changed program or request. Ordered comparison gives every product the same first mismatch. Separate evidence status preserves the distinction between an authenticated record and a reproduced outcome.
CanonicalRequestBytes is the complete recorded semantic request from identity encoding. The replay record adds only explicit operands and its finite host work budget.
Field
Value
format
"lispex.replay-request/2"
prepared_program_bytes
Bytevector containing one complete resolved/1 or bytecode/1 prepared program
request_bytes
Bytevector containing one complete CanonicalRequestBytes packet
expected_receipt_bytes
Bytevector containing one complete PortableReceiptBytes packet
evidence_bytes
Optional bytevector containing the supplied evidence envelope
trust_policy_bytes
Optional bytevector containing the supplied trust policy
profile_host_budget
The complete effective ProfileHostBudget record
ReplayRequestBytes = D(ReplayRequest).
Both evidence options are empty or both have one bytevector. They remain explicit inputs until their scheduled checks. Every operand is an immutable snapshot. Unknown fields and missing fields are refused. Contract identities select exact supported versions. A missing or unsupported semantic contract never selects a newer version or a product default.
The --request command operand remains CanonicalRequestBytes. It is not this enclosing record. The other command operands supply the other fields. A --bundle command prepares its bundle with the separate preparation limits before forming this record. A prepared artifact supplies the validated prepared bytes through its artifact contract. Source bundle and artifact containers keep their definition homes.
The recorded request fixes its program, canonical input bytes, language, Unicode and library semantics, resource model, and EvaluationLimits. The selected product and engine can differ from the original execution. That choice does not replace a recorded semantic input. Source spelling, source maps, package bytes, and engine bytes are not additional semantic equality requirements.
Replay uses the following order. Existing source, prepared program, diagnostic, and resource rules still apply.
Step
Required action
Failure boundary
1
Admit the finite host envelope and effective profile host budget
Admission report
2
Validate the replay record and its immutable operand snapshots
Admission report
3
Validate and seal the prepared program under the prepared program contract
Admission report
4
Decode the outer request record, retain input_bytes as opaque bytes, resolve exact contracts, and compute its candidate request digest
Admission report
5
Admit the expected receipt and require its program and candidate request bindings to agree
Admission report
6
Verify supplied evidence and trust against the expected receipt
Evidence verification report
7
Decode input under the recorded EvaluationLimits, verify the input and request identities, then invoke entry
Canonical outcome or the applicable input or attempt report
8
Form an eligible actual receipt and compare it with the expected receipt
Comparison report
Preparation of a source bundle precedes this table. Its failure uses the source report. It does not produce an evaluation receipt.
Outer request decoding and candidate digest checks use the profile host account. The candidate digest establishes a byte binding. It is not a verified semantic request identity. The verified input and request markers remain empty until the canonical input decoder succeeds. That decoder runs once in the evaluation account after expected evidence verification. An invalid input or an input decoding budget failure prevents guest entry and an actual evaluation receipt. The host does not debit the recorded EvaluationLimits for schema, signature, trust, or comparison work.
A mismatched supplied program or expected receipt uses admission and artifact.invalid with identity-mismatch. An unavailable semantic contract uses the existing product.unsupported diagnostic. A missing recorded request field uses request.invalid with missing-field. These refusals occur before entry and produce no new canonical outcome or evaluation receipt.
A well formed envelope bound to another receipt uses verify and verification.failed with evidence-binding. It has command status 42 and prevents replay evaluation. Its target remains the expected receipt. It produces no actual receipt and no comparison record.
The profile host budget covers all replay host work in this table. Exhaustion uses verify and verification.budget. A completed actual outcome and receipt remain available if later comparison work cannot finish.
VerificationReportBytes and ReplayComparisonBytes use the same encoding. Their operation field distinguishes them. A comparison record exists only when both admitted receipts are available.
Field
Value
format
"lispex.comparison/2"
operation
"verify" or "replay"
expected_receipt_bytes
Complete expected receipt packet as a bytevector
actual_receipt_bytes
Complete actual receipt packet as a bytevector
program
"equal", "different", or "not-compared"
request
"equal", "different", or "not-compared"
outcome
"equal", "different", or "not-compared"
evidence
"not-requested", "not-checked", "verified", or "refused"
evidence_report
Optional nested EvidenceVerificationRecord
first_mismatch
Optional "program", "request", or "outcome"
diagnostic
Optional diagnostic field record
ComparisonReportBytes is D of the ComparisonRecord defined above. VerificationReportBytes is that encoding with operation verify. ReplayComparisonBytes is that encoding with operation replay.
Condition
Required fields
Program identities differ
program = "different", later components "not-compared", first mismatch "program"
Request identities differ
Program "equal", request "different", outcome "not-compared", first mismatch "request"
Outcomes differ
Program and request "equal", outcome "different", first mismatch "outcome"
Whole semantic comparison matches
All three components "equal", empty first mismatch
Evidence was not requested
Evidence "not-requested", empty evidence report
Verify stopped before scheduled evidence checks
Evidence "not-checked", empty evidence report
Supplied evidence was verified
Evidence "verified", one verified evidence report
Verify evidence was refused after semantic match
Evidence "refused", one refused evidence report, all semantic components remain "equal"
The report compares the program and request identities carried by the receipts. It compares the complete outcome_bytes packets. Verify has no program or request operand. Its identity equality check does not mark those nested assertions as independently verified. Its site check validates shape and equality without claiming program membership. Every success datum and every failure field participates. This includes phase, code, typed data, canonical site, and resource axis.
For verify, the first mismatch uses verification.failed with program-identity, request-identity, or outcome. For replay, it uses replay.mismatch with the matching component. An evidence refusal uses the diagnostic from its evidence report. A complete semantic match with no evidence refusal has no diagnostic.
Both report forms preserve the exact receipt packets. They perform no text normalization or approximate numeric comparison. Human presentation and usage counters remain outside the receipt schema.
Verify succeeds for a value or a deterministic failure
0
Both supplied receipts are retained
Replay matches a successful value
0
The actual receipt is retained
Replay matches a language failure
20
The actual failure receipt is retained
Replay matches a resource stop
21
The actual failure receipt is retained
Admitted verification or comparison fails
42
Every available receipt is retained
Program, recorded request, or expected receipt is refused before replay
30
No actual evaluation receipt is created
An evidence failure before replay evaluation has no actual receipt to compare. A preparation or admission failure has no canonical evaluation outcome. An operational interruption before completion has no new canonical outcome or receipt. Each uses its existing report boundary.
A comparison budget failure cannot replace a completed language outcome. Report output is complete or refused. A partial comparison record is not published. Numeric tariffs and report capacity values remain under the cost model freeze.
Prepare a closed program before evaluating it. Modules preserve lexical bindings and caches preserve evaluation meaning.
Scope
The calling application submits a closed source bundle and prepares it under finite limits. It can then evaluate the prepared program through the entry with an input Datum.
This chapter defines modules, preparation, resolved programs, and preparation caches. Resources defines reservations and resource events. Identity, receipt, replay defines program and source identities.
Closed source bundle
A source module groups lexical bindings and declares the names that other source modules may import. A closed bundle supplies each source module name separately from its source bytes. The module declaration must have the same decoded name. This name table makes preparation order independent of file paths and submission order.
Source modules and fixed library modules have separate name spaces. Source import clauses use only the supplied source module name space. The fixed library supplies enclosing lexical bindings through its submitted identity and bytes. Source imports and definitions share the inner module scope and may shadow those library bindings. Library code cannot depend on source modules.
The calling application selects one source root module. Every supplied source module is part of the program, including modules that the root does not import. Module names never authorize filesystem or network discovery. The moduleSources and rootModule fields in request.json are documentation notation. They do not define a public host schema.
12.1 Supply every dependency
Preparation resolves every module and standard library dependency from the submitted closed bundle. An unresolved dependency causes a preparation failure. Guest evaluation cannot discover dependencies or evaluate newly supplied code.
Preparation first checks the source module name table and the selected root name. It verifies the fixed library before starting any source module. It orders source modules by unsigned lexicographic UTF-8 bytes of their decoded names. It completes decoding, reading, and normalization for each module before starting the next module. It then checks that every import names a supplied source module and rejects dependency cycles. Name resolution follows dependency order with the least canonical name selected among ready modules. The order table fixes graph traversal and failure precedence. Every supplied module is checked. A source module cannot become a library module by declaring a library name.
An explicit name table breaks the dependence between reading source and choosing which source to read first. Acyclic dependencies admit one complete initialization order without partially available imported values. Submission order and host paths cannot select the first error.
Stage
Ordered work
First failure
Bundle names
Sort decoded source names by unsigned UTF-8 bytes. Check duplicates. Check that the selected root is present
The least duplicated name precedes a missing root
Fixed library
Verify the fixed identity and closed library graph in dependency order
A failed library check stops before source module reading
Source front end
For each canonical name finish decode, read, and normalize before the next name
The first failing step of the current module
Module form
Check the wrapper and matching name. Check import forms and aliases. Check export forms and public names. Check entry syntax. Precheck all definition names. Normalize children in source order
The first failed shallow check precedes every child check
Import targets
Visit modules in canonical name order and import specs in source order
The first missing source module
Cycles
Visit graph roots in canonical order. Depth-first traversal visits dependency names in canonical order
The first edge to an active ancestor. The cycle starts at that ancestor and ends with the closing edge
Resolution
Repeatedly choose the least canonical ready source name. Resolve imports in clause order, definition items in source order, exports in clause order, then entry
The first failure in that module. All dependencies must already be resolved
A ready module has no unresolved dependency. Each graph module is visited once by cycle detection. Lambda group bodies resolve in definition order after the group names are established. The fixed library has its own name space and cannot depend on source modules. Its dependency order also uses canonical name ties. Reservations follow Source and Resources. This table fixes order without fixing tariff values.
The preparation diagnostic mapping gives module failures their catalog identities. The diagnostic phase does not change this check order.
Identifier comes from the reader grammar. EntryClause comes from Procedures. Expression is a reader datum admitted by Evaluation and bindings. Grammar keywords compare decoded identifier values. Definition shorthand has the same normalized lambda as an explicit procedure definition. Internal definitions follow the existing lambda recursion restriction.
Imports and exports
12.3 Declare a closed source module
A source file contains exactly one module form from the grammar. Module names compare their decoded identifier scalars without normalization or case folding. The import and export clauses are mandatory and occur once in that order. Each imported module occurs once in the import clause. An import names a public export and may give it a local alias. An export names a local definition or imported binding and may give it a public alias. Import local names and export public names must be unique. A definition cannot repeat an import local name or another definition name in the module. Preparation checks the module binding names before normalizing any definition initializer. It follows the local group order in Source. It does not precheck nested groups before reaching them. The entry rules govern the optional entry clause.
Explicit imports and exports keep each reference tied to its selected binding. Raw names preserve the reader contract. A module name has no authority to locate code outside the submitted bundle.
Form
First name
Second name
Binding effect
Plain import binding
Public export
Same local name
Preserve the exporting binding
Renamed import binding
Public export
Local alias
Preserve the exporting binding
Plain export binding
Local binding
Same public name
Expose that binding
Renamed export binding
Local binding
Public alias
Expose that binding
Several distinct aliases may refer to the same binding. Local import names remain unique across the entire import clause. Public export names remain unique across the entire export clause. Export validation follows export clause order. It checks the completed module binding table and never evaluates a value.
12.4 Import exported lexical bindings
An import names an exported binding in a supplied module. Module private bindings remain local. Preparation rejects an import that does not name an export.
Preparation resolves definitions and does not run their initializers. Every evaluation initializes the fixed library and then every supplied source module. Dependencies precede importers and canonical names break ties. Definitions follow source order within a module. Adjacent definitions whose normalized initializers are lambdas form one maximal recursive group. That group sees imports, preceding definitions, and its own procedure names. Each other definition evaluates one initializer in the preceding scope and then introduces its binding. It follows the Module definition row in the evaluation event table. No initializer or procedure body sees a later group. Imports retain the initialized binding from their source module. A failure stops initialization before later definitions, modules, or the root entry. Successful initialization is followed by the declared root entry. Cached preparation never skips initialization or changes its evaluation events.
The full bundle is the prepared program. Explicit initialization of all its modules preserves a visible order for failures and resource events. Sequential values and lambda recursion avoid observable partially initialized bindings. Repeating initialization keeps cache state outside the semantic request.
Definition item
Visible bindings
Evaluation effect
Maximal adjacent lambda group
Enclosing library, imports, preceding definitions, own group
The module binding name precheck still rejects duplicate declarations across all definition items. Adjacent lambda groups do not grant forward scope across another definition item. An initializer is a single-value context. All source modules are initialized even when the root does not import them. A dependency entry declaration creates no independent invocation.
Preparation reads and normalizes source, resolves bindings, combines modules and the fixed standard library, lowers code, validates it, and computes canonical identities. These steps use the preparation budget.
Evaluation decodes its canonical input, performs any required initialization, invokes the entry, and encodes its Datum or failure. These steps use the evaluation budget. Resources defines the reservations for both phases.
A resolved program records the selected bindings and semantic operations. Its source map supplies display locations. Source and normalization defines the source transformations. Identity, receipt, replay defines the separate identities.
12.6 Prepare before evaluation
Preparation finishes before evaluation and does not execute guest computation. Evaluation repeats any required program initialization and charges it on every request. Each phase uses the independent finite account defined in Resources.
Resolution records each name’s lexical binding and preserves the specified evaluation order. Canonical programs exclude source display locations. Spacing and comments ignored by the reader preserve the resolved program when tokens and literal values stay fixed.
A prepared program uses the resolved/1 record graph and its fixed dependency identities. The grammar defines resolved/1 bytes and bytecode/1 bytes. Both encodings reconstruct the same graph. Only the node tag encoding differs. The canonical graph retains the typed source forms in the construction table. The records preserve lexical bindings, ordered children, semantic occurrences, and tail positions. Each occurrence has its own node. Source maps remain separate from these bytes.
One graph gives products one meaning to validate and encode. Typed control edges make validation finite. Exact reconstruction avoids a proof of arbitrary optimizer equivalence.
The grammar terminals are hexadecimal octets. Each quoted pair denotes one octet. A count prefixes every list and byte string. It gives the exact number of following items or octets. Each byte string ends at that count. Each prepared value ends after its final node.
Item
Encoding rule
Format names
resolved/1 and bytecode/1
Resolved header
4c 58 52 50 01
Bytecode header
4c 58 42 43 01
Language
The counted UTF-8 bytes for 2.0
UVar
Unsigned base 128 digits in least significant digit order
Continuation
Every nonfinal digit has its high bit set
Final digit
The final digit has its high bit clear
Minimal form
Zero uses 00. A multi-octet value has a nonzero final digit
Arithmetic
Counts and indices use mathematical nonnegative integers
Text
Strict UTF-8 for Unicode scalars without normalization
Frame checks
The declared count must fit the remaining submitted bytes and the selected finite limits
End of input
Trailing bytes are rejected
Extensions
Unknown versions, tags, fields, and flags are rejected
IdentityBytes uses identity encoding. CanonicalSiteBytes uses canonical sites. CanonicalDatumBytes uses the canonical-codec contract. These imported byte strings must pass their own canonical decoders. Their enclosing counts do not change their encoding. No identity digest or source location occurs implicitly in a field. CanonicalSiteBytes is the program-local occurrence and event-role record. The surrounding program identity is attached outside the prepared bytes. A program digest cannot occur inside its own canonical site records.
Field order is fixed by the grammar. Indices start at zero in their own tables. Every record index equals its table position.
Local binding, target module, exported name, target binding
Export
Exported name and local binding
Group
Canonical occurrence site record and its typed initializer group
Sequential group
Binding and initializer node
Recursive group
Binding list and lambda node list
Binding
Index, name, and role
Name
The decoded Identifier scalar sequence from the reader
Optional binding 00
No binding
Optional binding 01
One binding index
Optional entry 00
No entry declaration
Optional entry 01
The declared public export name and its resolved binding index
Internal definitions 00
No leading internal definitions
Internal definitions 01
One site record, binding list, and lambda initializer list
Node
Index, canonical occurrence site record, tail flag, typed body
Clause
Canonical occurrence site record and its typed fields
Tail flag 00
Outside tail position
Tail flag 01
In tail position
Binding role
Meaning
00
Module definition
01
Imported alias
02
Fixed parameter
03
Rest parameter
04
Local binding in let or let*
05
Recursive local binding
06
Guard condition binding
07
Native member named by the following Text field
08
Internal definition
09
Named let procedure binding
Name fields contain decoded Identifier scalar values without normalization or case folding. Reader delimiter bars and escape notation stay in source provenance. The scalar produced by an escape remains part of the name. This applies to module names, binding names, imported names, public export names, and entry names. Different token spellings with the same decoded name produce the same Name bytes.
Native members must belong to the fixed library identity. Only a verified library module may declare them. A member name is a semantic library name. It is never a host address or linker instruction. The library contract selects membership. This format assigns no native kernel count.
A required dependency identity denotes the target module's canonical resolved meaning under its fixed semantic dependencies. LibraryIdentity denotes the fixed semantic library and its declared binding environment. Neither field denotes exact source bytes, an engine artifact, or the selected prepared encoding. Ignored spacing or comments in a dependency preserve its meaning identity and the enclosing prepared bytes. Source hashes, engine hashes, signatures, issuance details, and package locations belong outside the canonical graph.
The resolved tag is the counted UTF-8 spelling in the first column. The bytecode tag is the single octet in the second column. Node payloads have the same field order in both formats.
Resolved tag
Bytecode tag
Payload and child order
literal
00
One canonical Datum
use
01
Name and its resolved binding
lambda
02
Fixed parameters, optional rest parameter, body node
call
03
Operator node followed by argument nodes in order
if
04
Test node, true branch node, false branch node
sequence
05
The written begin children in order
let
06
Binding list, initializer list in order, body node
letrec
07
Binding list, lambda initializer list in order, body node
guard
08
Condition binding, protected body node, ordered clauses
body
09
Optional leading recursive internal group followed by expressions in written order
letstar
0a
Binding list, initializer list in order, body node
namedlet
0b
Loop binding, fixed parameters, initializers in order, body node
and
0c
Operands in written order
or
0d
Operands in written order
cond
0e
Ordered clauses
Clause tag
Fields in order
00
Test expression and clause body
01
One test expression without a written body
02
Test expression and receiver expression after the arrow
03
Else body
The clause tags retain syntax kind and order. Evaluation and Conditions decide which clause kinds the source form admits. A record tag does not add a source form or supply an unstated fallback value. An if node records its test and both written branches. The conditional grammar requires those three children. It also requires one final else clause in cond. Source and prepared validation apply these forms before admitting the graph.
Each lambda body uses its lexical parameter scope. A let initializer uses the enclosing scope. Its body sees the complete new group. A letrec group contains only lambda initializers. Each lambda body sees every binding in that group. Leading internal definitions form one recursive lambda-only group under the evaluation contract. That group retains its declaration and initializer order. Each letstar initializer sees the preceding new bindings. Each such binding introduces a nested scope. A namedlet initializer uses the enclosing scope. Its body sees the loop procedure and its parameter bindings. A guard condition binding is visible only in its clauses. The handling guard is inactive while dispatch runs. An unmatched guard retains its condition and propagates it under the condition rules.
Library operations use ordinary resolved bindings and call nodes. This includes apply, values, call-with-values, and structured raise. The graph encodes no host call, mutation, continuation, or arbitrary jump instruction. Each call keeps its operator and every argument occurrence. Validation checks those references without evaluating them.
The reader's datum structure fixes the canonical source form. Resolution records bindings without replacing a semantic surface form with another form. The following construction is mandatory before assigning table indices.
Admitted source form
Canonical construction
Literal or quotation
One literal node containing its decoded Datum
Name use
One use node retaining its decoded Identifier name and resolved binding
Lambda
One lambda node with the written parameter order and one body node
Procedure definition shorthand
The same lambda and body construction as its explicit lambda initializer
Body
Exactly one body node retaining its optional leading recursive group and expression list
Singleton body
A body node with one expression child
Explicit begin
One sequence node with the written children
Application
One call node with the operator followed by every argument
If
One if node retaining the test and both written branches
Let
One let node retaining the parallel group and its body
Let*
One letstar node retaining every sequential binding and its body
Letrec
One letrec node retaining the recursive lambda group and its body
Named let
One namedlet node retaining the loop name, parameter group, initializers, and body
And
One and node retaining the written operand list
Or
One or node retaining the written operand list
Cond
One cond node retaining each written clause and its kind
Guard
One guard node retaining the condition name, protected body, and each written clause
Clause body
Exactly one body node
Test-only clause
Its test child without a synthetic body
Arrow clause
Its test and receiver children without a synthetic call node
Prefix quote and full quote use the same literal construction. A shorthand procedure definition and its explicit lambda form use the same binding and body construction. No other sugar is expanded in the canonical graph. No body or sequence node is flattened or removed. A body node records the existing body sequence and binding scope. It adds no guest operation. No constant is folded. No occurrence is merged. No unused source definition is removed. Every submitted module and every admitted branch remains in the graph. Identical reader structure and fixed dependencies therefore produce identical canonical records.
A semantic surface node retains its original resource event contract. Namedlet records retain the initial call and recursive procedure roles. Clause kinds retain test, selected body, receiver call, and outward propagation roles. Their node, group, and clause site records preserve those semantic event origins. These roles select events from the fixed resource model and use CanonicalSiteBytes for their site encoding. They do not acquire the events of a compiler-generated if, let, or call.
A private engine may lower these records into other instructions. It preserves the original binding relations, event roles, occurrence sites, and normalization contract. Its private temporaries and optimized instructions never replace the canonical records in either public format.
Source module order follows module preparation. The verified library closure precedes every source module. Library and source names occupy distinct namespaces. Names are unique within each namespace. The same spelling may appear in both.
Table or relation
Canonical order
Library modules
Fixed library dependency order with the unsigned UTF-8 module name tie rule
Source modules
Source dependency order with the module name tie rule
Dependencies
Target module index
Imports
Written clause order
Exports
Unsigned lexicographic UTF-8 order of the exported name
Initializer groups
Written definition order
Group members
Written binding order
Nodes
Preorder of initializer roots in module and group order
Node children
The payload order in the node table
Body children
Internal lambda initializers in definition order followed by the written expressions
Clause children
Test then body or receiver, in written clause order
Binding declarations
Imports, native members, then the declaration walk for each initializer group
Declaration walk
Declare a group's names before visiting its initializers and body
Lambda declarations
Fixed parameters in order, then the rest parameter, then the body
Guard declaration
Condition name before the protected body and clauses
Named let declarations
Loop name, parameters in order, then the initializer and body walk
Native declarations
Unsigned lexicographic UTF-8 order of the fixed member name
Declaration numbering does not grant initializer visibility. Visibility follows the binding and module rules. Source imports resolve only within the source module namespace. Library dependencies resolve only within the fixed library closure. A library module cannot depend on a source module. The header's library identity supplies the lexical enclosure of each source module. Library binding access requires no invented source import or host lookup. The selected root must be a source module.
Every expression occurrence has exactly one structural parent or initializer root. Child references follow preorder and form finite trees. Recursive calls refer to bindings. They do not create cycles in the child graph. Equal literal values may share physical storage while their occurrence records remain distinct. No structurally unreachable node, undeclared binding record, repeated declaration, or extra table record is accepted. A declared binding may have no uses.
Source paths, source offsets, comments, display labels, cache state, and product details stay outside these records. Exact source hashes, source map contents, engine build identifiers, timestamps, signatures, and packaging choices also stay outside them. A source map may accompany them as a separate sidecar under Meaning graph. Removing or replacing that sidecar cannot change evaluation or prepared bytes. Private optimized artifacts may use another internal representation. A product emits resolved/1 or bytecode/1 only through the canonical record encoding defined here.
Bytecode validation
Validation establishes that a prepared program has a supported structure and compatible semantics. It checks referenced bindings, library dependencies, and the entry before evaluation. An immutable verified handle may carry those checks. Imported program bytes require validation.
The embedding contract defines the host interface and evaluator artifact admission. This chapter defines validation of the prepared guest program.
12.9 Validate prepared programs
Evaluation accepts only a validated prepared program compatible with the requested semantics and library. Validation checks bytecode structure and referenced bindings before guest entry. Serialized or cached programs must satisfy the same validation requirements.
A prepared program can be reused only while its validated meaning remains fixed. Invalid instructions or incompatible dependencies cannot enter evaluation through a cache.
Validation follows the ordered checks below under preparation limits. It rejects unsupported versions, malformed records, invalid references, and incompatible dependencies before entry. It reconstructs lexical scopes, tail positions, occurrence sites, and the selected resource event contracts. Callability, argument counts, value counts, and domains remain evaluation checks where the language places them. A valid replacement graph must match the requested program identity.
A format label cannot establish that submitted code is valid. Checking structure and references closes paths around the language contract. Keeping runtime checks in their declared order preserves the first observable failure.
Conditional forms use written alternatives.
Prepared guard annotations must follow the evaluation rule.
Validation stops at the first failed check or reservation in this order. Each repeated step follows wire order, table order, or node preorder as declared below. A reservation succeeds before the corresponding step reads, traverses, or creates data.
Order
Reservation name
Check
0
prepared.capture-input
Acquire the immutable submitted byte snapshot and dependency references before any validation read
1
prepared.read-header
Reserve before requesting each magic or version octet, then check that octet or source end
2
prepared.begin-record
Reserve before each compound record, list header, and list item in wire order
3
prepared.read-field
Reserve before requesting each later octet, including every count digit, payload octet, and final end check
4
prepared.check-record
Check each decoded record's counts, kind, index, and canonical table position
5
prepared.check-reference
Check each module, import, export, initializer, and entry reference in table order
6
prepared.check-reference
Check each declaration and use while reconstructing lexical scopes in canonical traversal order
7
prepared.check-record
Check each node, group, and clause for valid child structure, tail positions, sites, and event roles
8
prepared.check-identity
Verify each dependency and each fixed semantics identity in header and module order
9
prepared.check-identity
Compute and compare the requested program identity when one is supplied
10
prepared.seal-handle
Create the complete immutable verified handle
The caller supplies immutable bytes or transfers unaliased ownership before validation starts. A copy requires exclusive or protected read access throughout capture. The capture reservation covers the actual submitted byte span under the selected preparation model. The snapshot and any declared submission identity are fixed together before parsing. A declared identity remains untrusted until its verification step. Every later read and the final handle use that exact immutable snapshot. A validator cannot check borrowed mutable bytes and copy them only after those checks. Capture failure exposes no handle.
Steps 2 and 3 interleave according to the wire grammar until decoding ends. Compound records are Header, Module, Dependency, Import, Export, Binding, Node, Group, Clause, and a present internal definition group. Each compound record begins once at its opening boundary. Each count-prefixed list begins once before its count. Byte strings are fields rather than lists for this event. Type aliases, optional scalar fields, and node payload alternatives add no second compound record boundary. Each list item also begins before its first field. Every consumed octet has exactly one read reservation. At coincident boundaries the list item reservation precedes the reservation for its contained compound record. Header octets use prepared.read-header. Every later octet uses prepared.read-field. An attempted read that encounters source end still has its preceding reservation. A final prepared.read-field reservation checks end of input after the final node. A trailing octet fails that check without being treated as another field. Count digits consume that budget before a length is known. Each count is checked before its contents are allocated or visited. Storage is introduced by the corresponding successful record, item, or octet reservation. The decoder cannot allocate an entire unchecked list from its announced count. Validation uses the caller-selected verified preparation resource model for every reservation. The serialized ResourceModelIdentity remains untrusted data until its compatibility check succeeds. It checks shortest integer encodings, strict UTF-8, complete foreign codec frames, and end of input. It rejects duplicate indices and declarations even when their record contents agree. Module and binding checks use the module contract. Every source use must name its nearest visible binding, including the fixed library's lexical enclosure. Import targets must match the named export and its dependency identity. A kernel name must match the fixed library's member registry.
Structural child references must name the required child occurrence. Branch targets must be children of that if node or the declared clause body. Lambda bodies and call operands must remain in their declared scopes. A let, letstar, or letrec has equal binding and initializer counts. Those local groups may be empty. A namedlet has equal parameter and initializer counts. The loop name is visible only in its body. A recursive module group is nonempty and contains a maximal adjacent run of lambda initializers. A sequential module group has one non-lambda initializer. Leading internal definitions form one nonempty recursive group when present. Every initializer in it must be a lambda. A body has exactly its admitted prefix definitions and a nonempty expression list. An if node has exactly three expression children. Both branches are required. A cond has one final else clause with a nonempty body. The conditional grammar applies to imported records too. Each clause retains its admitted kind and exactly its written children. The form's condition or evaluation contract rejects unsupported clauses and invalid else positions. A lambda may have no fixed parameters and may have one rest parameter. Repeated parameters and duplicate parallel bindings are rejected. The selected entry must satisfy entry declarations and root selection. The entry record retains its declared public export name and that export's resolved binding. The root record and header binding must agree. Another alias for the same binding cannot replace the declared export name.
Tail flags are recomputed from the language's tail positions. Module initializers start outside tail position. A lambda body starts in tail position. Conditional branches, the last body or sequence child, and binding bodies inherit their enclosing tail position. The last operand of and or or inherits that position. Earlier operands do not. A namedlet body starts in tail position within the named procedure. Its initial call retains the namedlet node's enclosing tail position. Operators, arguments, tests, and initializers are outside tail position. Guard body and selected handler clause flags follow the tail-position rule. Lexical binding scopes are preserved. Clause tests and receiver expressions are outside tail position. An admitted arrow clause's implicit receiver call retains the enclosing conditional or guard tail position. Native implicit calls follow the tail-call rule. The target of apply and the consumer of call-with-values inherit the invoking call's tail position. The producer and every other library callback are outside tail position. CanonicalSiteBytes must match the occurrence mapping defined by Meaning graph. Two distinct node, group, or clause occurrences cannot share one occurrence identity.
Each node, group, and clause selects its original semantic event roles under the fixed resource model. Implicit namedlet calls and clause receiver calls retain their own roles and canonical sites. Bytes cannot supply replacement tariffs, skip checks, or remove required reservations. Validation preserves all dynamic call and result checks at their declared semantic sites. It does not evaluate guest initializers or infer away a runtime failure.
Resources orders the applicable axes within every reservation. Tariff coefficients, logical allocation units, finite limits, and physical envelopes remain under cost-model-freeze. The wire fields, counts, and version bytes are fixed by this grammar. A failed validation returns no handle and runs no entry. Its refusal or preparation stop produces no canonical evaluation outcome or evaluation receipt.
The preparation diagnostic mapping gives each rejected artifact its catalog identity and typed fields. Case names identify fixture mutations.
Admission acquires an immutable snapshot of submitted bytes and fixed dependencies before the first validation read. Validation checks that exact snapshot under the selected preparation limits. Successful preparation returns an opaque handle sealed by the receiving evaluator instance. The handle owns the same validated code and dependency references. Caller changes to submitted storage cannot change that code. Only the issuing instance accepts the handle as verified. Transport uses the versioned program bytes and repeats validation. Each evaluation creates fresh initialization state and its own finite accounts.
A private seal distinguishes completed validation from caller supplied fields. Immutable ownership prevents a later byte change from replacing validated code. Fresh evaluation state keeps initialization costs and outcomes independent of cache history.
The verified handle is an opaque local value. The fields below describe private evaluator state. They are not a constructor, a public object layout, or serializable fields.
Private component
Required meaning
Issuer seal
Unforgeable membership in the issuing evaluator instance
Program snapshot
Owned immutable canonical records
Dependencies
Owned immutable references to verified supplied dependencies
Fixed contracts
The validated language, Unicode, library, and resource model identities
Selection
The validated root module and entry binding
Validation
The completed checks for these exact records and dependencies
Copying visible fields or setting a verified flag cannot create the issuer seal. A handle is not a Datum and cannot enter guest data. The public value-only boundary remains unchanged. The caller supplies immutable bytes or transfers unaliased ownership before the first validation read. Copying holds exclusive or protected read access until the snapshot is complete. Finite preparation limits apply before snapshot storage is acquired. Validation reads that snapshot and seals only the same snapshot. Changes to the original caller buffer cannot race with validation or replace its checked code. A mutable borrowed buffer cannot become verified through a copy made after validation. Imported bytes repeat capture and validation before a new seal is issued. Failed validation destroys its partial state without exposing a handle.
Serialization emits canonical program bytes and omits the local seal. Another evaluator validates those bytes and creates its own handle. A reused handle still checks compatibility with the requested fixed semantics. Each evaluate call creates fresh module initialization, argument bindings, and evaluation accounts. A handle never stores guest initialization results for a later request. Product APIs and outer package containers use the embedding contract.
A preparation cache stores verified work for later reuse. A hit must match the program dependencies and fixed semantics that produced the stored work. A library or semantics mismatch cannot be hidden by the cache.
Reusing preparation may change preparation work. Each evaluation still starts with its declared limits and performs its required initialization. Cache state never changes evaluation charges or the first semantic failure.
12.12 Preserve evaluation across caches
Cache hits, cache misses, and precompiled standard library paths preserve evaluation charges and the canonical outcome for the same semantic request. They preserve the first failure, its resource axis, and its canonical site. A cache may reuse verified preparation work.
The calling application supplies one semantic request with one set of evaluation limits. The preparation path cannot grant extra evaluation work or move its first stop.
Inspect resolved bindings, control flow, source locations, and recorded execution paths while preserving the rule outcome.
Scope
Use a meaning graph to inspect how a prepared rule binds names and selects work. A meaning graph is a read-only projection of the resolved program.
A source map connects a canonical program site to its location in the submitted source. A trace records the path taken by one execution within a separately reserved finite capacity.
The graph starts with the resolved program produced by preparation. It follows lexical binding references through the closed module bundle. A shared spelling can therefore refer to different bindings.
Inspecting the graph reveals how the rule uses its input. The calling application evaluates the rule through the same semantic request.
13.1 Project resolved bindings
A meaning graph projects the prepared resolved program. Every displayed name use retains its resolved binding and source anchor. Reading the graph leaves the program unchanged.
Readers need to distinguish bindings that share a spelling. Using resolved bindings connects each use to the declaration that evaluation actually selects.
Data dependencies show which values an operation consumes. Branch edges show alternatives. Call relations retain the resolved operator expression and its argument dependencies. Recursive relationships remain visible.
A static graph retains both arms of a conditional. A trace can identify the selected arm for a specific input. Evaluation and bindings determines which operations run and in what order.
13.2 Preserve dependencies and control flow
The graph preserves data dependencies, conditional branches, procedure calls, and recursive calls. Evaluation follows the language order and selects the same branch when the graph is displayed.
A reader needs to see both the available paths and the path a request takes. Keeping the graph separate from execution prevents a view from scheduling extra work.
A viewer may group repeated structures or fold a region. Each original occurrence and its tail position remains recoverable from that view.
A display node can summarize several occurrences. Its shape does not replace their canonical program sites or alter the resource events required by Resources.
13.3 Keep original sites in grouped views
Grouping or folding the graph preserves access to every original occurrence and its tail position. The display choice leaves evaluation events and the canonical outcome unchanged.
Identical source expressions can occupy different evaluation sites. Preserving their occurrences lets a reader locate the first failure and distinguish tail calls.
A graph record contains the verified program identity and its canonical resolved/1 bytes. The prepared record schema defines every module, binding, node, group, and clause. The relation table below derives the inspection view from those records. A reader preserves every original occurrence and tail flag. Graph export and inspection run no guest initialization or entry. Source locations, layout, explanatory labels, and trace records remain outside the graph record.
One canonical graph preserves the meaning already fixed by preparation. Reusing its records prevents another graph schema from assigning different binding or control meaning. An outer identity binds the projection without placing its own digest inside the program.
The grammar terminals are hexadecimal octets. Count gives the exact number of following octets or list items. The enclosing production determines which count applies.
Item
Encoding
Graph format
lispex.graph/1
Graph header
4c 58 4d 47 01
Site format
lispex.site/1
Site header
4c 58 53 01
Qualified site format
lispex.qualified-site/1
Qualified site header
4c 58 51 01
Source map format
lispex.source-map/1
Source map header
4c 58 53 4d 01
Trace format
lispex.trace/1
Trace header
4c 58 54 52 01
UVar and Text
The shortest unsigned integer and strict UTF-8 Text forms in the prepared grammar
Indices and offsets
Mathematical nonnegative integers
IdentityBytes
The canonical bytes for the identity domain required by the field
Resolved
The complete canonical resolved/1 encoding
SourceBundleBytes
The canonical source bundle packet from Embedding
End of input
Exactly after the last declared field or trace footer
Extensions
Unknown headers, versions, tags, roles, and trailing bytes are rejected
Preparation defines UVar, Text, and Resolved. Identity encoding defines IdentityBytes. Source bundles define SourceBundleBytes. Every counted foreign field contains one complete canonical value of its declared type. Its count includes all of that value's header and payload octets. No field permits a second value or padding. The count prefix does not change the foreign encoding.
GraphBytes always uses resolved/1 for its payload. A verified bytecode/1 input is projected through the same canonical records and then encoded as resolved/1. Program identity is checked against that payload under its own identity contract. It occurs only in the outer graph envelope. The format fixes no digest algorithm, tariff coefficient, default limit, or native kernel count.
These are logical relations derived from the prepared records. They are not additional wire fields. Each row is visited in its source table order. Ordered node fields retain their written child order.
Call occurrence, lambda node or namedlet node or native binding
The direct target rule below
Named let initial call
Namedlet occurrence, loop binding, ordered initializer nodes, enclosing tail flag
Each namedlet node
Receiver call
Clause occurrence, receiver node, test node, enclosing tail flag
Each arrow clause
If branch
If node index, test node, written true and false branch nodes
Each if node
Clause branch
Control node index, ordered clause occurrences and typed children
Each cond or guard node
Short circuit
And or or node index, ordered operand nodes
Each and or or node
Result sequence
Body or sequence node index, ordered expression nodes
Each body or sequence node
A declaration occurrence is the containing module, group, or node from the prepared declaration walk. Imports and native bindings use their Module occurrence. Module and internal definitions use their Group occurrence. Parameters and local bindings use their declaring node occurrence. Binding indices remain distinct when their names have equal scalars. Import aliases retain their targets. Data dependence records structural operands without asserting that every branch runs. The language decides which child is evaluated.
A literal lambda operator has that lambda as its direct target. A use operator follows imported aliases to its declared binding. A lambda initializer, named let loop binding, or native binding supplies a direct target. Every other operator keeps its expression and has no static target. The actual target then appears in the call trace record. An absent static target says only that execution selects the procedure value. Recursive relations follow binding references and direct call targets. They never turn recursive calls into child-graph cycles.
The projection preserves every admitted branch and every original occurrence. It retains body nodes, sequence nodes, groups, clause kinds, and implicit call origins. Grouping is a viewer operation over those immutable records. It adds no serialized label, replacement occurrence, or alternate ordering.
A consumer applies these checks before using supplied graph data. Each applicable reservation follows Resources. An exhausted reservation precedes the check it would fund.
Order
Check
0
Capture the submitted bytes as an immutable input
1
Check the header and each canonical count in wire order
2
Decode each counted field completely under its declared contract
3
Check exact end of input
4
Validate embedded prepared records and recompute local sites
5
Verify the outer program identity against the resolved payload
6
For a source map verify source identity and reconstruct its program and spans
7
Check graph associations and record order under the tables below
Inspection uses finite preparation limits and no guest execution. It cannot create a verified evaluator handle from an unchecked graph. Any later execution follows the existing prepared validation and handle rules.
Refusal
Existing diagnostic
Malformed bytes, noncanonical rows, unknown role, or invalid site
admission and artifact.invalid with kind graph and reason invalid-format
A well-formed outer identity names another object
admission and artifact.invalid with kind graph and reason identity-mismatch
A source map span differs from reconstructed source provenance
admission and artifact.invalid with kind graph and reason invalid-integrity
The diagnostic catalog defines those identities and fields. A refused graph or map produces no canonical evaluation outcome or evaluation receipt. It does not modify an existing handle or a previously completed evaluation.
Canonical sites
13.5 Encode a local occurrence and event role
CanonicalSiteBytes identifies one occurrence, one semantic event role, and its ordered subject path. Prepared node, group, and clause records use the occurrence role and an empty path. Event sites retain that occurrence and use the exact resource event name. A qualified site attaches program identity outside CanonicalSiteBytes. The local bytes contain no program digest, source coordinate, execution count, or documentation label. A prepared validator recomputes each local occurrence and rejects a mismatched site.
An occurrence remains stable when source spacing or graph layout changes. The event role separates checks that share that occurrence. A typed path identifies the inspected value part. External qualification avoids a digest cycle and distinguishes equal local bytes in different programs.
CanonicalSiteBytes = "4c", "58", "53", "01", OccurrenceKind, Index, Role, SubjectPath ;
OccurrenceKind = "00" | "01" | "02" | "03" | "04" ;
Role = Text ;
SubjectPath = Count, { PathStep } ;
PathStep = "00", Index | "01", Index | "02" | "03" | "04", Index | "05", Index | "06", Index | "07", Text ;
QualifiedSiteBytes = "4c", "58", "51", "01", ProgramIdentity, Site ;
ProgramIdentity = Count, IdentityBytes ;
Site = Count, CanonicalSiteBytes ;
Index = UVar ;
Count = UVar ;
The first index belongs to the table selected by OccurrenceKind. All numbering starts at zero.
Kind octet
Occurrence
Index
00
Node
The existing prepared node index
01
Group
Module initializer groups in module order, then internal definition groups in node order
02
Clause
Containing node order, then written clause order
03
Module
The existing prepared module index
04
Binding
The existing prepared binding index
Group and clause ordinals count only records of their own kind. Each present internal definition group receives one group ordinal. An absent internal group receives none. Library records precede source records according to the prepared tables. The module index preserves the separate library and source namespaces. Decoded names retain their raw scalars, including an empty Identifier name.
Path tag
Component
Meaning
00
argument and Index
The argument at that zero-based position
01
result and Index
The result at that zero-based position
02
car
The pair's car
03
cdr
The pair's cdr
04
element and Index
The member of an ordered collection at that position
05
scalar and Index
The Unicode scalar at that position
06
byte and Index
The octet at that position
07
field and Text
The exact field name defined by the containing record schema
SubjectPath orders components from the outer subject to the inspected part. Element covers vector members and other ordered buffers named by the event catalog. The Rest argument pair row in the Resources site table selects the lambda occurrence and result(0) followed by element(i). This path uses no field name. Field names are schema identifiers, not human explanations. Role is either the exact UTF-8 text occurrence or an event name from the closed resource catalog. The occurrence role requires an empty path. An event's allowed occurrence kind and path follow its resource table. The same occurrence may therefore have different event sites. Repeated execution of one event at one site keeps the same local bytes.
A prepared node stores its own node index with the occurrence role and an empty path. A prepared group or clause stores its assigned ordinal in the same form. Different node, group, and clause occurrences have different typed indices. The validator reconstructs those indices from the canonical prepared tables. Serialized indices cannot replace that reconstruction.
A sequential module group follows the Module definition row in Resources. Its result-check site uses that group occurrence and the complete path element(0). This association excludes recursive module groups and internal definition groups.
Module and binding sites support source provenance and catalog events that explicitly use those kinds. Binding declaration sites do not redirect a use away from its resolved binding. An entry boundary event uses the selected entry lambda occurrence. A call event uses its original call node. An implicit named let call uses the namedlet node. An implicit receiver call uses its clause occurrence. Further event and subject choices follow Resources.
QualifiedSiteBytes pairs one program IdentityBytes value with one local Site value. Its identity must name the program whose canonical tables contain that occurrence. An enclosing graph, map, trace, or outcome can supply the same qualification through its program field. That enclosing field is outside the canonical prepared bytes. Comparing qualified sites compares both the program identity and the complete local bytes. Equal local bytes from distinct programs do not denote the same qualified site.
A source-bound preparation location is a different record. Before a canonical program exists it uses the exact submitted source and its source coordinates. A prepared-byte decoder may instead identify the immutable submitted wire offset. Neither case invents a program identity or a CanonicalSiteBytes value.
Source maps
Source maps translate canonical sites into locations in the submitted source. Human labels and explanatory nodes help readers navigate the graph.
Use source identity to retain exact source provenance. Render evaluation failures at the canonical sites recorded in their canonical outcomes. A source map supplies the module and exact byte coordinates. The caller attaches its displayed filename.
A read or normalization failure uses a source-bound preparation report. A resolved graph requires a successfully resolved program.
13.6 Keep source maps outside semantic identity
Source maps associate canonical program sites with exact source locations. Source coordinates, display annotations, and layout remain separate from canonical program identity. Changing only those records preserves the evaluation outcome and resource events.
Reformatting source can move a displayed location while preserving the resolved program. Separating the records keeps replay comparisons and canonical failure sites stable.
A source map pairs the program identity with the exact source identity and the submitted source bundle. Each mapping names one source occurrence and its exact half-open UTF-8 byte span. The table below fixes span construction for written and implicit nodes. Validation reconstructs the prepared records and these spans without running guest code. A mismatched map is refused as graph data. It cannot replace the prepared program, canonical failure site, or completed outcome. Caller display paths remain separate annotations.
Exact source bytes let a reader verify a displayed location. Byte spans remain unambiguous across Unicode scalars and newline spellings. Separating the map preserves canonical program comparisons after source presentation changes.
SourceMapBytes carries the original source bundle as one canonical packet. The bundle's accepted module names are unique. Its root agrees with the prepared root by decoded name. Each submitted source module matches the prepared source module with that exact name. Library modules remain in their separate namespace.
Field
Requirement
ProgramIdentity
The identity of the canonical resolved records
SourceIdentity
The identity of the exact submitted source bundle under the source identity contract
Bundle
One accepted SourceBundleBytes packet
Mapping Site
The occurrence role and empty path
StartByte
The included first UTF-8 octet
EndByte
The excluded octet after the source span
Mapping order
Kind octet, then mathematical index
Mapping membership
Exactly every node, group, clause, module, and binding declared by a submitted source module
Library occurrences
No mapping in this submitted-source map
The target occurrence determines its owning module. A binding uses its declaration module, including a local imported alias. The module name selects the exact source bytes in Bundle. Every span satisfies StartByte less than EndByte and EndByte at most the module's source byte length. Both boundaries occur between complete UTF-8 scalars. CR and LF retain their original octets. Line and column display is derived from these exact bytes. The caller can attach a display path to the module name outside this format.
The decoder rejects missing, duplicate, extra, or unsorted mappings. It reconstructs source spans using the reader and canonical construction rules. It verifies the source identity and compares the reconstructed program with ProgramIdentity. Every supplied Mapping must equal the reconstructed occurrence and span. Replacing only the source bundle or map cannot replace the program or its evaluation identity.
A reader span starts at the first octet of its token or opening delimiter. It ends immediately after the token or matching closing delimiter. Whitespace and comments between the endpoints remain inside the span. Surrounding whitespace and comments remain outside it.
Canonical occurrence
Source span
Written expression node
Its complete reader form
Name use node
Its complete Identifier token, including bars and escapes
Literal from quotation
Its complete quote form, including the quote prefix when written
Explicit lambda node
Its complete lambda form
Lambda from procedure definition shorthand
Its complete define form
Implicit body node
The first leading definition or expression through the last body expression
Module initializer group
The first member define form through the last member define form
Internal definition group
The first leading define form through the last leading define form
Clause
The complete written clause form
Module
The complete module form
Binding declaration
The Identifier token that declares the local binding
Plain import binding
The imported Identifier token
Renamed import binding
The local alias Identifier token
Rest parameter
Its Identifier token, excluding the dotted-list separator
Body and group spans may contain several written forms. Their endpoints still identify one exact byte interval. An omitted branch or absent internal group creates no mapping. An implicit named let call shares its namedlet occurrence. An implicit receiver call shares its clause occurrence. Their event roles distinguish the call from other work at that occurrence. An event subject path does not invent a new source location. Source presentation uses its enclosing occurrence mapping. Source-bound decode or read failures use their preparation report before this map exists.
Execution trace
Trace recording observes one execution. The caller selects its finite capacity before evaluation and keeps that reservation separate from guest resource limits.
A full trace records the selected execution path. An incomplete trace records only a prefix and marks that limit. The complete evaluation still produces its own outcome.
The first semantic failure and resource stop follow the same event order with tracing enabled or disabled. The trace supplies no extra guest calls, allocation charges, or guard branches.
13.8 Keep trace capacity separate from evaluation
Apply the separate account and stop rules from trace reservations. This chapter defines the trace packet, whole record frames, and completion footer. The command result carries the separate host trace status. Trace state preserves the evaluation outcome, first failure, resource axis, and canonical site.
A trace records the admitted request through the event tags below. Recording starts after canonical input admission and before module initialization. Each record uses canonical sites and metadata already available from the observed event. The trace reservation contract reserves one complete framed record before storing it. The first trace reservation failure permanently stops recording. A reserved footer marks the retained prefix incomplete. Evaluation continues with unchanged checks, charges, first failure, and outcome. Trace records contain no guest value payloads or host timing data.
Complete frames let every reader consume the same prefix. A separate footer records exhaustion without a second allocation after the buffer fills. Observing existing metadata avoids guest traversal and leaves the semantic request unchanged.
The header supplies the program and request identities once. Every local site in the stream is qualified by that program identity. Record position gives stream order. No execution counter occurs inside a site.
Event tag
Event
Fields after the tag
00
Enter
The occurrence Site
01
Branch
The controlling occurrence Site and Choice
02
Call
The call occurrence Site, actual ProcedureTarget, and tail flag
03
Return
The call occurrence Site and number of returned values
04
Condition
The committed occurrence Site and its condition code
05
Reservation
The catalog event Site and ReservationResult
06
Terminal
TerminalKind and OptionalSite
Variant
Tag
Fields or meaning
Choice
00
The selected next node index
Choice
01
No next child is selected by this control decision
ProcedureTarget
00
The lambda node index
ProcedureTarget
01
The namedlet node index
ProcedureTarget
02
The native member binding index
ReservationResult
00
Reservation accepted before its associated check or effect
ReservationResult
01
Reservation refused, followed by the exhausted Axis
Axis
00
work
Axis
01
allocation
Axis
02
frames
Axis
03
input
Axis
04
result
Axis
05
diagnostic
TerminalKind
00
Successful Datum result
TerminalKind
01
Uncaught guest condition
TerminalKind
02
Evaluation resource stop
TerminalKind
03
Entry result boundary failure
Completion
00
All admitted evaluation events through Terminal are recorded
Completion
01
Recording stopped at the first event that did not fit
Completion
02
Host interruption prevented a complete evaluation trace
Enter, Branch, Call, and Return use occurrence sites with empty paths. Condition uses the canonical failure site of the new condition occurrence. Reservation uses the exact catalog event role and subject path. Terminal success has no site. Every other Terminal has the canonical failure or stop site. Code is a guest code from the Condition catalog. Condition data and result values stay in their existing records. Trace metadata never copies or traverses guest data to populate a trace field.
These emission points preserve the language's existing event order. They add no evaluation checks or reservations. At each point a trace record is attempted only while recording remains active.
Observation
Emission point
Reservation
Immediately after atomic acceptance or refusal and before the associated check or effect
Enter
On reaching the expression node, before its first operation event, child evaluation, or produced value
Branch
After the controlling test and its required checks, before the selected next child
Call
After the accepted call reservation, before parameter binding or procedure execution
Return
After accepted call-return and release of active call capacity, before forwarding the result sequence or caller result-check
Condition
After required diagnostic-payload reservation and creation of a new condition occurrence
Terminal
After the admitted evaluation's canonical result or failure is fixed
Every entered expression emits Enter, including written body and sequence nodes. Those observations add no resource event to implicit body nodes. Initialization visits the fixed library and source modules in their existing order. An implicit named let or receiver call uses the original occurrence fixed by preparation. Call and Return use the occurrences of their observed call and call-return events. Tracing adds no Return for a caller whose capacity was replaced by a tail transfer. It retains no extra continuation to pair those observations. The entry Call uses the selected entry lambda occurrence and a false tail flag. Any entry Return follows the existing call-return event and its canonical occurrence.
The following table fixes each Branch emission and its site.
Control
Site
Emission and choice
If
The if node occurrence
After the test selects one of its two written branches
Nonfinal and or or operand
The and or or node occurrence
After result-check and branch-select select the next operand or no child
Final and or or operand
The and or or node occurrence
When the final operand returns, select no child before forwarding its result sequence
Empty and or or
The and or or node occurrence
After its branch-select selects no child
Cond or guard test clause
That clause occurrence
After its test selects a body or receiver, or no child
Else clause
That clause occurrence
When reached selects its body before body entry
The final and or or observation inspects no returned value or value count. It adds no result-check or branch-select event. A false clause selects no child for that clause. Normal dispatch then visits the next clause under the language rules. A selected test-only clause also selects no further child. An unmatched guard follows its existing outward propagation rule. The records observe those decisions without adding tests or fallback results.
Condition propagation retains the original occurrence. It does not emit a new Condition record unless another condition occurrence is created. A failure to reserve a condition payload produces its resource stop before any new Condition record. The corresponding refused Reservation record precedes that stop. Terminal is the final admitted evaluation event. Later qualification, evidence, and output transport work stays outside this stream. Input decoding before request identity exists also stays outside this admitted trace.
A TraceRecord count gives the exact number of TraceEvent payload octets. Its reservation unit includes the 01 marker, the count prefix, and the entire payload. The header and complete two-octet footer are reserved before admitted evaluation starts. Resources defines that separate trace account.
The first record that cannot fit contributes no bytes. The recorder then stops permanently and retains the already complete prefix. It writes the reserved 00 01 footer when returning the trace. A complete trace ends with 00 00. A host interruption before Terminal uses 00 02 unless capacity exhaustion already stopped recording. Once Terminal is stored, the complete stream retains 00 00. A later output or trace delivery failure does not change that stream. The recorder allocates no failure text after exhaustion. It adds no guest event, call, guard branch, or resource charge. It keeps no growing trace-only counter after recording stops.
A complete trace has exactly one Terminal record in final position. An incomplete trace contains a proper prefix and may have no Terminal record. An event after Terminal, a duplicate footer, a partial frame, or trailing bytes is invalid. Unknown event tags and fields are rejected. The stream header must agree with the enclosing request and program when those are supplied. The format gives an observed path and does not itself establish evaluator conformance. Examples retain separate not-run product plans until the product adapter exists.
Independent graph evaluation
A graph viewer reads the projection. An independent graph evaluator is another engine that must meet the same sandbox contract.
The product checks its supported requests before dispatch. It follows the admission-before-entry rule for unsupported capability.
Projection checks establish the relations shown by the graph. Independent execution cases establish agreement of outcomes and resource events. Execution evidence remains separate from the portable receipt.
A graph describes a program, while an evaluator performs its operations. Independent execution evidence checks that another evaluator preserves the same failures and resource boundaries.
Call a prepared rule with canonical data and finite limits. Validate its artifacts and package before evaluation.
Scope
Calling applications embed Lispex by supplying data to a prepared rule and receiving its canonical outcome. This chapter defines the host interface, artifact admission, packages, and the Topaz connection.
The examples pair rule source with a documentation request. The request names fixed semantics and symbolic finite limits. Artifact descriptions and limit defects describe cases for a future product adapter. They do not define public JSON fields, executable artifacts, or a byte encoding.
Value interface
The host interface is the public surface through which a calling application prepares a rule and submits an input. The value-only ABI carries canonical data across that surface. Host objects and callable host functions are outside its data domain.
The calling application supplies one canonical Datum as input. Public embedding interfaces reject host callbacks and host object references. Guest code receives values without access to host services.
A callable host function could read external state or perform work outside the language resource model. Passing captured values keeps authority with the calling application.
The public API separates prepare and evaluate. Preparation returns an opaque verified handle to an immutable rule. A product that transports versioned prepared bytes validates them before use. The caller supplies the canonical input and named evaluation limits for each call.
The caller can first select record admission. Record adaptation and its output encoding use the profile host account. The evaluator then decodes the resulting canonical input under EvaluationLimits. Its result encoding uses the same evaluation account. The boundary event schedule is the definition home for those events. Identical canonical input gives identical evaluation events under the same program, fixed semantics, and limits. The input construction path does not change those events.
Preparation and modules defines the closed source bundle, dependency resolution, and cache behavior. Resources defines work, logical allocation, frames, and channel budgets. Result encoding and diagnostic production follow those resource rules. A raw interpreter interface cannot bypass the public value and limit checks.
When a profile requires additional host checks, the caller supplies the separate finite profile host budget. The host records profile work identity without adding that budget to either base request.
The host returns an admission report for a refusal before entry. After evaluation it returns qualification and evidence results in a separate profile work report. That report preserves the completed canonical outcome and evaluation receipt eligibility.
14.2 Prepare a rule and evaluate an input
Preparation accepts a closed source bundle and preparation limits. Evaluation accepts an immutable prepared rule, one canonical input, and evaluation limits. Success returns one canonical Datum. A convenience call performs the same two phases.
A prepared rule fixes its program and dependencies before evaluation. Separate requests can reuse that rule while supplying independent inputs and evaluation budgets.
SourceBundleBytes is one canonical lispex.datum/2 packet containing the record below. The Datum codec defines every tag, count, and UTF-8 octet. A record is a proper association list of pairs from exact String keys to their field values. Each entry has its key in car and its value in cdr. Keys occur once in unsigned UTF-8 byte order. Every listed field is required. Unknown fields are refused. Vectors preserve the order shown by their schema.
Record
Exact fields
Datum types
SourceBundle
format, modules, root
String, Vector of ModuleSource, String
ModuleSource
name, source
String, Bytevector
SourceBundle format
lispex.source-bundle/2
Exact String
name and root contain decoded Identifier scalars. They may be empty. They preserve case and normalization. The source token for a Unicode name uses the barred identifier grammar. The bars and escapes are absent from the name field. The source field preserves all submitted source octets. Paths, timestamps, and display labels are absent from this record.
ModuleSource records use nondecreasing unsigned UTF-8 name order. Typed callers sort this vector before encoding it. Equal adjacent names remain representable until the existing duplicate module check rejects them. Every submitted source module participates in preparation. The fixed package supplies the matching immutable library bytes as a separate dependency. Preparation performs no dependency lookup or file access.
The closed bundle checks retain their existing order. Duplicate module names, missing root membership, and source declaration mismatches keep their existing preparation failures. A root field is required even for one source module. The root module's source declaration selects its entry under the entry rule. There is no host entry override.
Product operand
Exact submitted bytes
Selection
CLI --bundle FILE
SourceBundleBytes
Required bundle root
CLI --artifact FILE
PreparedArtifactBytes
Validated prepared root and entry
Typed prepare
Canonical SourceBundleBytes from the typed record
Required bundle root
Typed load
Exact immutable PreparedArtifactBytes
Validated prepared root and entry
The CLI grammar is unchanged. The product reads these bytes before entering the value-only evaluator.
Native exposes Rust and C bindings. npm and browser WASM expose the TypeScript binding. Every binding uses the same byte ABI below. Datum input is supplied as canonical bytes. Host functions, object references, implicit string conversion, and callable properties are refused.
Private issuer-bound immutable verified program handle
PrepareReply
Complete command result and a handle only on successful sealing
TraceOptions
Closed Nat fields allocation, capacity, work under Resources
The following local byte names specify the C spans and the shared encoders. D is the complete Datum packet encoding from Identity. Each local encoding imports its record meaning from the type table.
Encoding
Exact packet
FixedSelectionBytes
D of FixedSelection
PrepareLimitsBytes
D of PrepareLimits
EvaluationLimitsBytes
D of EvaluationLimits
PreparedFormatBytes
D of the PreparedFormat String
TraceOptionsBytes
D of false or the TraceOptions record
ProfileSelectionBytes
D of the ProfileSelection String
SourceBundleBytes and PreparedArtifactBytes retain their existing input contracts. RecordInputBytes, ProfileRequestBytes, and ProfileHostBudgetBytes retain their Profiles definitions. CanonicalInputBytes is a complete packet. It is not an extra bytevector wrapper around that packet.
FixedSelection identifies the package's fixed Unicode 17.0.0 and library contracts. Each identifier must equal the corresponding validated package dependency. Limits are required for every performed phase. Each Nat is a Datum integer with the integer tag and exact nonnegative value. Nat fields are never decimal Strings or rational values. Zero is finite and follows the inclusive limit rule. Missing fields, unknown fields, negative values, nonintegers, and unlimited values fail admission. An integer beyond the selected model's representation limit uses the existing overflow refusal. The common preset expands to the same complete limit records before these calls. The cost freeze owns all numeric values.
The signature fixture defines the host signatures. Its byte parameters use the complete packets named in the type table. Rust Bytes owns a byte slice. Rust Nat has a private exact integer representation. Rust nat returns BuildResult from canonical unsigned decimal text without a machine integer cast. Its accepted text is 0 or a nonzero ASCII digit followed by ASCII digits. Signs, whitespace, leading zeroes, and empty text are refused. TypeScript Bytes is a copied Uint8Array. TypeScript Nat is a bigint validated before encoding. TypeScript constructors take the validated Product and return BuildResult. They issue privately branded records from primitive arguments and copied byte views. Encoders read the private records without calling user properties or iterators. Forged records and shared mutable backing storage are refused before encoding. Byte copying uses typed array internal slots. It performs no numeric coercion or user callback. The C binding uses opaque types and byte spans for the same records.
BuildResult contains either the constructed value or one complete CommandResultBytes with its admission report. The host result mapping also defines Open, load, and export reports. A constructor validates arguments from left to right under the Product ingress bounds. A value, type, brand, or ownership failure uses admission and request.invalid. The field is the parameter name and the reason is invalid-value. The Rust Nat constructor uses field text. Constructors check exact syntax and trusted ingress bounds. The phase invocation checks its selected model's representation limits and uses reason overflow when needed. No failed constructor enters a guest or creates an evaluation receipt. TypeScript throws only TransportFailure for a transport failure. Completed admission refusals and semantic failures remain command result data. Rust drop, TypeScript dispose, and C destroy revoke the handle. TypeScript disposal and C destruction are idempotent. A disposed, forged, or foreign handle returns admission and request.invalid before guest entry. Its field is rule and its reason is invalid-value. A C caller supplies valid live spans and writable output pointers. Invalid native pointers violate the transport precondition. The wrapper associates each handle with its issuing Product. It exposes no pointer, seal, numeric handle ID, or verified flag as portable data. Export produces portable bytes. Load validates those bytes again under preparation limits.
Each evaluation initializes every admitted module under the initialization rule. Reuse retains only verified immutable program data. It preserves the complete evaluation event sequence and canonical receipt. A convenience run performs prepare or load followed by evaluate with both phase limits. It returns the first phase failure and never evaluates after preparation refusal. The explicit profile wrappers use the same private Product and PreparedRule types. They keep the profile host account separate from evaluation.
Wrapper
Rust
TypeScript
C
Record admission
admit_record
admitRecord
lispex_v2_admit_record
Profile evaluation
evaluate_profile
evaluateProfile
lispex_v2_evaluate_profile
Record admission takes RecordInputBytes, an explicit ProfileSelection, and ProfileHostBudget. It requires no program handle, library, declaration, schema, or evidence. Its successful CommandResultBytes has payload kind input and the complete CanonicalInputBytes. It has no canonical evaluation outcome or evaluation receipt. Its command option is empty. The report envelope owns this mapping. Record admission remains a host operation. It adds no evaluator operation or CLI command.
Profile evaluation takes a PreparedRule, CanonicalInputBytes, EvaluationLimits, ProfileRequestBytes, ProfileHostBudget, and the existing trace selection. The profile request is required even for base. It uses the canonical base declaration when base is selected. The wrapper creates the ProfileEvaluation record defined in the byte ABI below. The call decodes canonical input once under the evaluation account. It checks the input schema under the host account. It then resumes the same evaluation state for module initialization and entry. Qualification and required evidence follow the existing Profiles schedule. The result uses complete CommandResultBytes and preserves the canonical outcome and eligible receipt. No callback, public continuation, or repeated decoder joins these stages.
The two wrappers create separate host operations and accounts. Record admission does not transfer its remaining budget into profile evaluation. Its returned canonical bytes are an explicit input to the later call. Their different submissions have different profile work bindings. Changing only the selected host model leaves the program and evaluation request unchanged.
The ProfileHostBudget type fixes its format to lispex.profile-host-budget/2. Its resource_model field comes from the explicit IdentityBytes argument. Its six numeric axes retain the exact meanings and order defined in Profiles. The TypeScript profileHostBudget constructor requires that model argument. The Rust record requires the resource_model field. The C budget span contains complete ProfileHostBudgetBytes. No binding substitutes the evaluation model for missing host metadata. The selected host model must support the profile work contract before that account is used. Construction uses the trusted Product ingress account. The constructed budget selects only the subsequent profile host account.
Named input packets preserve the same boundary across host languages. Explicit record admission makes conversion and its budget visible. The host model remains separate from evaluation semantics. One coordinated call preserves input decoding charges and schema order.
The ABI identifier is lispex.host/2. HostRequestBytes is one canonical lispex.datum/2 packet containing a closed record. It uses the record representation in SourceBundle. All nested records use the same representation. Bytes(T) is a Bytevector containing one complete canonical T packet. The outer packet adds no normalization or alternate encoding to imported bytes.
Record
Required fields and values
HostRequest
body as the selected body record, format as String lispex.host/2, operation as the operation String
prepare body
bundle as Bytes(SourceBundleBytes), limits as PrepareLimits, selection as FixedSelection
load body
artifact as Bytes(PreparedArtifactBytes), limits as PrepareLimits, selection as FixedSelection
evaluate body
input as Bytes(CanonicalInputBytes), limits as EvaluationLimits, profile as false or ProfileEvaluation, trace as false or TraceOptions
The profile field is required. The base evaluate API supplies false. The evaluate_profile wrapper supplies ProfileEvaluation. Its budget retains the required host resource_model metadata from Profiles. The nested profile request remains a complete imported packet. The evaluator validates its host work contract before using that account. It performs the authoritative input decode under EvaluationLimits. Input schema work then uses the host account before module initialization. The same charged evaluation state resumes after schema acceptance. This coordination happens inside the existing evaluate call. No host callback or public continuation participates. The separate record admission wrapper never enters this byte ABI.
The operation Strings are exactly prepare, load, evaluate, export, and graph. false uses the Datum false tag. Empty records use the empty list. A reply is exactly one complete CommandResultBytes packet. The host result mapping defines each operation and its empty CLI command option. EmergencyTerminalBytes uses the final terminal report slot in that envelope. The caller secures the complete outer emergency framing before normal work. The reply carries the prepared artifact, graph, canonical outcome, or phase report for that operation. Evaluation receipts and optional trace data use their named fields in that imported result contract. No host handle enters either packet. Evaluation projects the sealed program, canonical input, fixed semantics, and EvaluationLimits into the semantic request. TraceOptions, ABI framing, transport bounds, product selection, local handles, and instance history are excluded. The request identity never hashes HostRequestBytes as a whole. The profile field contributes to its separate host work binding. It contributes no field to the canonical evaluation RequestRecord. An evaluate_profile refusal uses the existing run admission operation. A successful explicit record admission uses the existing record-admission operation.
The evaluator exports transport these packets. A new instance is empty. Successful prepare or load seals exactly one program. Only prepare and load are allowed while empty. Only evaluate, export, and graph are allowed while sealed. There is at most one active call and one pending complete reply. Release removes transfer buffers and leaves the program state unchanged. Another program requires a new instance.
Preparation seals its private immutable snapshot and publishes its complete reply atomically. Failure discards partial program state and leaves the instance empty. Evaluation always starts with fresh guest state and fresh evaluation counters. It never retains guest results, module values, or initialization state for the next call. A trap invalidates the instance and returns transport host-failure. The wrapper creates the existing operational attempt report under its reserved host envelope. A trapped evaluator does not serialize its own report. A new evaluation receipt is absent after that transport failure. Previously delivered outcomes and receipts remain unchanged. State misuse uses admission and request.invalid with field operation and reason invalid-value.
The admitted package establishes finite ingress and egress bounds before accepting transport bytes. Logical transport exhaustion uses the package host.envelope refusal and a complete report when the emergency envelope remains available. The caller's unvalidated fields cannot select those bounds. The fixed resource model names their representation and work ceilings under the cost freeze. Transport framing and host record checks follow boundary events. Source, prepared, and canonical Datum packets then use their existing phase accounts. Canonical input decode charges evaluation even before request identity exists. Malformed input produces its existing pre-entry refusal and no evaluation receipt.
The decoder first validates the outer Datum packet. It checks that the root is a record before inspecting its fields. For each record it visits the supplied entries in list order. It checks the entry pair, String key, canonical key order, and membership in that order. Only then does it check the field value's type. After supplied fields it checks missing fields in unsigned UTF-8 key order. The top-level body value is first checked only for record shape. It then checks the exact format, operation, and instance state in that order. Only then does it validate the selected body schema recursively in field order. Every complete imported byte packet keeps its own decoder order. An invalid outer packet or record uses the existing request.invalid admission diagnostic. The field identifies the first failing path. The root path is the empty String. Wrong format, duplicate keys, nonstring keys, and out-of-order keys use reason invalid-value. Unsorted module names use field body/bundle/modules and reason invalid-value. These checks never decode source bytes or enforce source module uniqueness. Nested foreign packet contents stay opaque until their owning phase starts. This preserves source preparation order and evaluation input decode order. It snapshots every bytevector before validation reads. Its successful reply becomes visible only after complete serialization.
Failure
Existing diagnostic
Missing required host field
admission, request.invalid, field path, missing-field
Unknown host field
admission, request.invalid, field path, unknown-field
Wrong type or unsupported operation
admission, request.invalid, field path, invalid-value
Invalid nested prepared artifact
The existing prepared artifact refusal
Malformed canonical input
The existing canonical input decode refusal
Field paths use exact record keys separated by /. The root field path is the empty String. Vector indices use minimal unsigned decimal text. The diagnostic catalog owns payload fields and codes. The exit mapping owns CLI status.
Artifact admission is the host check that determines whether a submitted or installed artifact can execute under the requested contracts. It checks identity, interface compatibility, dependencies, and the physical resources needed to honor finite limits. A host that cannot provide that envelope refuses admission.
A lexical source import selects a module from the closed submitted bundle. An evaluator artifact import links the evaluator to host functionality. Preparation resolves lexical imports before evaluation. The preferred evaluator artifact has no host imports. Host file discovery and network loading cannot supply a missing guest dependency during evaluation.
14.6 Validate artifacts before execution
Artifact admission checks the evaluator interface, supported contracts, dependencies, and resource envelope before execution. A transported prepared artifact is validated before use. Admission rejects host capabilities that grant ambient authority. The preferred evaluator artifact has no host imports.
An unverified artifact can carry behavior outside the submitted rule. Admission keeps the data interface and resource limits effective for every accepted artifact.
Each container is one canonical lispex.datum/2 record packet. PreparedArtifactBytes encodes the complete PreparedArtifact packet. EvaluatorArtifactBytes encodes the complete EvaluatorArtifact packet. PackageBytes encodes the complete Package packet. It uses the exact record representation in the host ABI. The following tables list every field in unsigned UTF-8 order. Bytevectors contain exact octets. A false optional field uses the Datum false tag. Unknown fields, duplicate fields, wrong types, and trailing bytes are refused.
PreparedArtifact field
Exact type and value
format
String lispex.prepared-artifact/2
payload
Bytevector of one complete prepared program
payload-format
String resolved/1 or bytecode/1
program
Bytevector of canonical program IdentityBytes
source-map
False or Bytevector of complete SourceMapBytes
The prepared grammar defines the payload unchanged. The payload header must agree with payload-format. Its dependency identities, root, entry, lexical references, sites, and event roles retain their existing validation order. The program field must equal the program identity computed by Identity. It is outside the prepared payload and outside program-local site bytes. A present source map must pass the source map contract against that program. It never changes the program or evaluation request identity.
Every successful prepare or load reply emits resolved/1 with source-map false. Load normalizes the reply format even when its input used bytecode/1 or carried a source map. The CLI prepare command uses that same default. Explicit typed export selects either supported payload format and emits source-map false. Equal verified programs produce equal export bytes for the same selected format. A source map travels as a separately constructed sidecar or an explicitly supplied container field. Changing its source provenance can change container identity while preserving program identity.
EvaluatorArtifact field
Exact type and value
abi
String lispex.host/2
format
String lispex.evaluator-artifact/2
payload
Bytevector of one complete admitted WebAssembly core module
physical-envelope
Bytevector of the installed physical envelope IdentityBytes
Evaluator payload bytes pass the export contract. An evaluator artifact has no guest program entry or host callback field. Its identity uses the external artifact identity contract. No container contains its own artifact digest.
Package field
Exact type and value
evaluator
Bytevector of complete EvaluatorArtifactBytes
format
String lispex.package/2
library
Bytevector of the exact fixed installed library image
metadata
Bytevector of complete PackageMetadataBytes
The library image is an opaque immutable dependency of the admitted evaluator. Its complete bytes and artifact identity must match the evaluator's installed supported library image. The semantic LibraryIdentity remains the identity of resolved library meaning. The separate library-image field pins exact image bytes without changing that semantic identity. It supplies the fixed library module bytes and kernel bindings required by preparation. It is not parsed as a source bundle with an invented root. The procedure catalog determines the public library surface. Final native membership remains under kernel and cost model.
Artifact admission first captures the immutable container under the trusted host envelope. It validates the outer packet and exact record schema. It then checks the container format and required field types in table order. For a prepared artifact it checks payload-format and then runs the existing prepared validator. The outer program field supplies the requested program identity at the prepared validator's existing identity check. After that validator succeeds, the wrapper validates any source map. A failed sidecar discards the private handle and exposes no sealed instance. The wrapper publishes the complete reply and instance seal together. For an evaluator artifact it checks ABI and physical envelope identity compatibility before module inspection. It establishes actual physical capacity only after the package dependencies pass their checks. For a package it validates metadata, evaluator, and library in that order after framing. An enclosing bytevector count never admits an unchecked payload allocation. Wrapper checks cannot reorder the checks inside a prepared payload.
Refusal
Existing diagnostic
Malformed PreparedArtifact or EvaluatorArtifact, or mismatched payload format
Package and metadata schema failures use the Open refusal table. Preparation meters the raw selected prepared payload under preparation events. The host transport envelope meters container framing and command result framing separately. Loading validates before sealing. Copying a verified flag or local handle is never an admission path.
The standard evaluator is one WebAssembly core module with zero imports and no start section. It has exactly the exports below and no others. Its memory is one unshared memory32 with a declared finite maximum. Tables and globals remain private. Shared memory, memory64, and additional memories are refused. The physical envelope identity supplies memory and stack ceilings after implementation measurement. This Rule assigns no page count or physical capacity.
Export
WebAssembly kind and exact signature
memory
The single unshared memory32
lispex_v2_alloc
Function i32 -> i32
lispex_v2_call
Function i32 i32 -> i32
lispex_v2_response_ptr
Function () -> i32
lispex_v2_response_len
Function () -> i32
lispex_v2_release
Function () -> ()
The i32 length and address bit patterns are interpreted as unsigned integers. Address zero is reserved as allocation failure. Lengths must fit the installed finite transport envelope before allocation. A zero request length is invalid transport input. The caller may have one allocated request span at a time. Alloc returns the span start or zero. It runs under the trusted host envelope. Alloc while busy or while an input span or reply remains live returns zero without changing any state. The wrapper checks lifecycle state and reserves the known span size under the trusted envelope before calling alloc. Zero after that valid admitted allocation request is a host failure. A known size or reservation refusal produces the existing host.envelope report before alloc. The evaluator does not allocate from an unchecked count inside request bytes.
Call accepts exactly the start and length of that live span. It checks nonwrapping end arithmetic and the whole span before reading any request octet. It captures an immutable private snapshot before parsing. Output storage never aliases input storage or the sealed program. After call returns zero, both response getters expose the complete retained reply. Repeated getters return the same span without evaluation or further semantic charge. The response remains valid until release. Getters before a complete reply return zero.
Call status
Meaning
Reply
0
One complete reply, including any admission or semantic failure
Complete CommandResultBytes
1
Invalid span, pending reply, reentry, or other transport lifecycle misuse
No new reply
2
Host allocation or infrastructure failure
None
Status 1 preserves any existing live request, complete reply, and sealed program. It never substitutes that old reply for a newly completed call. These statuses are transport values. They never substitute for CLI exit statuses. A WebAssembly trap is handled as status 2 by the wrapper and revokes the instance. The wrapper uses its reserved envelope for the existing operational attempt report. It produces no new evaluation receipt for the failed attempt. Earlier delivered reports stay unchanged.
Release frees the request and reply spans and resets their addresses and lengths to zero. It preserves the private sealed program. Release is idempotent when there is no pending call. Calls and release are never reentrant. After physical failure the wrapper destroys the instance instead of reusing partial state.
The typed wrapper keeps raw evaluator memory private. It writes only its allocated request span and reads only the returned response span. A JavaScript wrapper reacquires memory views after any export that can grow memory. It copies the complete response before releasing it. It never invokes guest code once to learn an output size and again to obtain output bytes. The host state contract governs empty and sealed instances.
Admission checks the complete immutable module before instantiation. It validates core module structure, imports, start section, export names and signatures, and memory shape in that order. Each list uses binary section order. Missing exports are checked in the table order. Duplicate or extra exports fail the same exact export check. An import uses artifact.invalid with kind evaluator and reason host-import. Other shape failures use kind evaluator and reason invalid-format. Unsupported physical limits use the existing host.envelope diagnostic.
Only an explicitly installed supported evaluator identity can be instantiated. Its conformance evidence and measured physical envelope must cover the admitted request. Export shape and identity checks do not authorize an arbitrary uploaded evaluator. A separate engine keeps the same public contract and requires its own conformance evidence.
A small export set makes ownership and call state explicit. Supported identities and measured envelopes keep unchecked evaluator code outside admission.
Topaz will update its std.lispex adapter to follow this host interface. Topaz owns that adapter and its concrete calls. The interface carries a prepared immutable rule, canonical input, and finite limits, then returns the canonical outcome.
Topaz captures time, exchange rates, random results, and other external facts before evaluation when a rule needs them. Those captured values become part of the canonical input and the recorded request. A later live value becomes a new input. Topaz displays the result and applies its own policy before performing an external action.
Identity, receipt, replay defines how the request, outcome, and execution evidence are recorded. The result is data for the host policy. Guest evaluation does not itself authorize or perform the host action.
14.9 Keep external facts and actions with Topaz
Topaz supplies a prepared immutable rule, captured canonical input, and finite limits through its host interface. Lispex returns a canonical outcome. Topaz decides any external action separately from that outcome.
Capturing time, rates, and other external facts as values makes them part of the replayable request. A returned decision gives Topaz data to assess under its own action policy.
A package distributes an evaluator with its standard library and declared interface and semantic identities. Admission checks the evaluator, standard library, ABI, value codec, language and Unicode semantics, profile, and resource model. The installed components must match the package declaration and support the submitted request.
Native, npm, and WASM use the same language contract. A shared evaluator artifact is preferred for these products. An additional engine supplies its own conformance evidence. Package and engine identities attach to execution evidence. They do not permit a changed result for the same semantic request.
14.10 Check the components of a package
A package verifies its evaluator, standard library, ABI, codec, semantics, profile, and resource model identities. A mismatched or unsupported component causes admission refusal. The package does not substitute another component silently.
A package name alone does not identify the components that execute a rule. Component checks keep the installed product aligned with the requested semantics.
PackageMetadataBytes is one canonical lispex.datum/2 closed record. Every field below is required and uses the host record representation. Metadata declares exact installed contracts. It supplies no fallback or discovery instruction.
Field
Exact value type
abi
String lispex.host/2
datum-codec
String lispex.datum/2
engine
Bytevector of engine IdentityBytes
evaluator
Bytevector of the supplied EvaluatorArtifactBytes identity
format
String lispex.package-metadata/2
language
String 2.0
library
Bytevector of the semantic LibraryIdentity for resolved library meaning
library-image
Bytevector of the artifact identity of the complete fixed library image bytes
physical-envelope
Bytevector of the installed physical envelope identity
prepared-formats
Vector containing String bytecode/1 then String resolved/1
product
String native, npm, or wasm
product-version
ReleaseVersion String
profiles
Vector of ProfileSupport records in unsigned UTF-8 name order
resource-models
Vector of resource model IdentityBytes bytevectors in unsigned byte order
unicode
Bytevector of the fixed Unicode 17.0.0 identity
Nested type
Exact shape
ProfileSupport
Record fields identity as an IdentityBytes bytevector and name as String base or vouch/2
ReleaseVersion
Three minimal unsigned decimal components separated by .
Minimal component
0 or one ASCII digit from 1 through 9 followed by zero or more ASCII digits
The support vectors are nonempty and have no duplicate elements or profile names. The base profile is required. A vouch/2 entry requires its own admitted profile support. Every identity passes its imported canonical decoder. Resource model, profile, Unicode, and library identities refer to their existing contracts. The metadata adds no new profile meaning or cost numbers. It contains no package path, URL, time, host locale, account, license, signer, or publishing instruction. Actual release names and ownership remain outside this format decision.
Open takes the complete package bytes and an expected metadata identity from the caller. That expected identity uses the artifact domain over complete PackageMetadataBytes. The installed product has an immutable supported component catalog before this operation. That catalog supplies trusted finite ingress and egress bounds before any package field is decoded. It also supplies the supported evaluator, library, and physical envelope identities. The supplied metadata cannot enlarge that catalog or its bounds.
Open snapshots the package and validates its outer schema. It decodes metadata and checks exact field types and canonical support order. It compares the expected metadata identity before accepting any selected contract. It checks the installed product and product version before checking the requested contract tuple. It checks language, ABI, Datum codec, prepared formats, engine, Unicode, semantic library, library image, resource models, and profiles in that order. The selected identities must form one supported installed compatibility tuple with the physical envelope. Independent membership in separate support lists is insufficient. Every declared profile and resource model pair must be covered with the same fixed engine, library, Unicode, and physical envelope. It then validates the evaluator shape and supported identity, the supplied library bytes, and the physical envelope. It returns a Product only after every check succeeds. No guest preparation or evaluation runs during Open. Failure returns an admission report and no Product.
Existing refusal
Use
request.invalid with field package and reason invalid-value
Malformed package or metadata schema
artifact.invalid with kind evaluator and reason identity-mismatch
Expected metadata or selected component identity mismatch
artifact.invalid with kind evaluator and reason unverified-content
Unsupported evaluator conformance evidence
request.invalid with reason invalid-value
Installed product or release mismatch at field package/metadata/product or package/metadata/product-version
product.unsupported
Unsupported contract using only the existing ProductSubject enumeration
host.envelope with reason unsupported-limits
Trusted ingress or egress reservation cannot admit the work
host.envelope with reason physical-capacity
The host cannot establish the installed physical envelope
The contract field of host.envelope is the trusted ingress, egress, or physical envelope identity that refused the operation. Trusted egress admission uses bounds derived from the complete admitted phase and channel limits before guest entry. It reserves the final report envelope before normal work. Later report delivery cannot replace a completed canonical outcome with a new admission refusal. A physical delivery failure follows the attempt report contract and preserves completed outcome and receipt eligibility. An admission refusal before evaluation has no evaluation request identity or evaluation receipt. A complete refusal report still uses transport status zero. Actual physical failure during a call uses the separate operational failure path.
The package signature fixture defines Open for every host. It uses the same complete PackageBytes and IdentityBytes on each product. The Product returned by Open issues every later private handle and checked constructor record. Product labels and product versions remain execution evidence. They never enter the prepared program, base semantic request, canonical outcome, or evaluation receipt.
The semantic request fixes the program, input, semantics, model, and limits. Selecting a product changes the execution evidence while preserving the requested meaning. A profile may narrow admission without changing the accepted request.
A missing capability or unsupported contract produces an explicit admission refusal. Operational interruption and engine defect remain distinct outcomes for the host to handle. Identity, receipt, replay defines their evidence and receipt eligibility. CLI and diagnostics defines product presentation and exit mapping.
14.12 Resolve finite limits before entry
Every public execution entry applies the finite-limit rule to each phase it performs. Limits use named fields. An explicit limit record with a missing required field, an unknown field, or an overflow is refused before entry. Convenience defaults select the common finite preset.
Complete finite limits make a request comparable across products. Named fields prevent a changed field order from silently changing the resource budget.
Every product preserves the outcome of the same admitted semantic request. This includes the first failure, exhausted resource axis, and canonical failure site. Each additional engine needs conformance evidence for the same contract.
Selecting a package or engine must preserve what a rule means. Independent product evidence checks that the installed components satisfy the shared language contract.
Compare a value and a domain failure across products
A product refuses an unsupported contract before guest evaluation. It preserves the requested semantics and limits when deciding admission. It does not retry the request with a different meaning or a reduced budget.
A refusal tells the caller that the selected product cannot execute this request. A silent retry would answer a different question while appearing to preserve the original request.
Prepare, run, and verify commands, finite presets, outcomes, and diagnostics.
Scope
Use the command forms below to prepare a rule, supply one explicit input, and receive one result under finite limits. The host reads explicit files and transports the result.
Every product uses the same argument grammar, numeric display, result framing, and numeric command status. Named value, artifact, receipt, report, and graph formats supply their bytes.
Each terminal is one argument after shell processing. Each imported argument is one nonempty string. An argument cannot contain NUL. A file is an explicit local path other than the single hyphen. Identity arguments name installed capabilities. Name arguments select the named finite preset. The option table supplies cardinality and compatibility rules.
The numerator and denominator are coprime. The denominator is greater than one. An integral value uses integer display. The spelling represents the exact mathematical value.
Prepare
Preparation reads the supplied closed source bundle and resolves its entry and dependencies. Its finite budget is separate from evaluation. A prepared rule records the fixed program needed by a later request. See Preparation and modules.
The root source uses the module grammar and declares its entry. Each alternative source case selects its own closed bundle.
15.1 Prepare before evaluating
The command applies the phase separation rule to the submitted source bundle. A preparation failure stops command dispatch before entry evaluation. Reused preparation follows the cache-preservation rule.
A caller needs to distinguish an invalid submission from an evaluated rule. Separate budgets keep preparation work and cache state from changing the rule outcome.
Use the command grammar for every product. The language and product arguments precede the command. Command options may appear in any order. Each option occurs at most once. Each option takes exactly one following argument.
Unknown options, missing arguments, duplicate options, and extra positional arguments fail during invocation. Short options, attached values, response files, and environment substitutions are outside this grammar. The command reads no implicit configuration file. Shell processing finishes before this contract applies.
Validate the complete argument vector before opening input files. Scan lexical errors from left to right. Then check required operands in the command table order. Finally check option conflicts in the option table order. A value error identifies its introducing option. A conflict identifies its later option. A missing required option identifies the end of the argument vector. Argument positions start at zero after the executable token.
Command
Required operands
Successful payload
prepare
One bundle
Prepared program artifact
run
One bundle or one artifact and one input
Canonical evaluation outcome
verify
One expected receipt and one actual receipt
Verification report
graph
One bundle or one artifact
Meaning graph
replay
One bundle or one artifact, one recorded request, and one expected receipt
Replay comparison report
Option
Meaning
Default or restriction
--language
Require Lispex 2.0 semantics
Required before the command
--product
Select the installed native, npm, or wasm product
Required before the command
--engine
Select an exact installed engine identity
Use the engine pinned by the selected product
--bundle
Read one closed source bundle
Excludes --artifact
--artifact
Read one prepared artifact
Excludes --bundle
--input
Read exact canonical input bytes
Required for run
--output
Write the primary result
Default is the single hyphen for stdout
--receipt-output
Write an eligible evaluation receipt to a separate file
Available for run and replay
--profile
Select base or vouch/2
base
--profile-declaration
Supply explicit profile declaration data
Required when the selected profile requires request declarations
--preset
Select one named finite preset for the performed phases
common-default
--prepare-limits
Supply PrepareLimits for preparation
Replace only that complete phase scope
--evaluate-limits
Supply EvaluationLimits for evaluation
Replace only that complete phase scope
--profile-limits
Supply ProfileHostBudget for host profile work
Replace only that complete phase scope
--request
Supply the complete recorded semantic request
Required for replay
--expected
Supply the recorded receipt to compare
Required for verify and replay
--actual
Supply the second receipt to compare
Required for verify
--evidence
Supply the explicit evidence envelope to verify
Pair with --trust
--trust
Supply fixed verification policy and trust inputs
Pair with --evidence
The selected bundle or artifact declares its single entry. A command cannot override that declaration. All three products use the same semantic input. The product and engine selectors affect execution evidence. They do not change the semantic request. Missing products, missing engines, and incompatible package identities fail admission. The command never installs a product or changes engines after refusal.
The host snapshots explicit file operands before using them. Only the input operand accepts stdin through the single hyphen. Stdin is read through EOF as one canonical value. A second encoded value or trailing bytes fail canonical decoding. Other operands do not consume stdin. The input bytes are never evaluated as source text. File paths remain host presentation data. Guest code receives the decoded Datum.
An explicit preset excludes all three phase limit files. Without an explicit preset, a phase file replaces its own complete scope. Other performed phases use common-default. A limit option for an unperformed phase fails invocation. Unknown fields, missing fields, nonfinite limits, and out-of-range fields fail admission. A missing or invalid file never triggers a preset fallback. The resource contract defines the finite scopes. The profile host budget remains separate. Numeric coefficients and defaults follow the cost model freeze.
Prepare resolves and verifies the bundle without guest evaluation. Graph projects the prepared canonical program without guest evaluation. A graph engine used for replay must be an explicitly selected installed engine with the required conformance support. A graph command does not select an execution engine by producing a graph.
Verify admits both receipts and checks their program and complete request identities before comparing whole canonical outcomes. Source provenance stays separate from the canonical comparison. Evidence verification uses only supplied evidence and trust inputs. It performs no issuer lookup or trust store discovery. Verify performs no guest evaluation. Check supplied evidence after the whole outcome comparison succeeds. A supplied evidence envelope authenticates the actual receipt. A different receipt binding fails verification. Successful outcome comparison does not excuse an evidence failure. Without evidence and trust operands, evidence verification is not requested.
Verification work uses the separate finite profile host budget. Exhaustion before a new evaluation uses phase verify and status 42. Recorded receipts and outcomes stay unchanged.
Replay obtains canonical input, evaluation limits, resource model, and semantic identities exclusively from the recorded request. It admits the supplied program and expected receipt against that request before guest entry. Their program and request identities must agree. An inconsistent expected receipt is an admission refusal with status 30. A supplied evidence envelope authenticates the expected receipt. Its verification completes before replay evaluation. A well formed envelope bound to another receipt fails verification with status 42. Replay accepts no input, profile, preset, or evaluation limit override. Preparation and profile host limits cover only their separate host work. The comparison preserves both recorded and recomputed outcomes. Command statuses follow the numeric mapping.
The primary output contains exactly one complete command result record. Its named byte contract carries the payload or reports for that command. The command adds no banner, separator, newline, or second record. A file output leaves stdout empty. Human diagnostics use stderr. A preparation failure uses its source report. Admission refusal uses its admission report. A later profile refusal preserves the evaluation outcome with its separate profile work report. Operational failures use their attempt report.
For the same admitted semantic request and format versions, every product emits the same canonical payload and evaluation receipt bytes. Product labels, host paths, and locale text stay outside those bytes. Execution evidence retains its separate identity.
Serialization completes before the primary record is published. Semantic failure never publishes a truncated success value. Interrupted output delivery is an operational failure. Receipt files are written only for eligible completed evaluation outcomes. Qualification or evidence refusal preserves that eligibility. Distinct output operands must name distinct destinations and must not overwrite an input operand.
Explicit operands make the same request available to every product. Separate phase limits preserve preparation and evaluation accounting. Exact replay operands prevent silent changes to the recorded request. One result record keeps machine output independent of host presentation.
Every CLI numeric display uses the numeric display grammar. Integers use decimal digits. Every nonintegral value uses a reduced fraction with a positive denominator. Zero is written as 0. Source scale is absent.
Exact value or source spelling
Display
0
0
-0.00
0
1.00
1
6/3
2
1.50
3/2
-0.125
-1/8
1/3
1/3
9007199254740993
9007199254740993
The display contains no leading plus, leading zeroes, exponent, decimal point, grouping mark, or locale variation. It performs no rounding. Canonical value bytes still follow the value codec. Display spelling never selects a different numeric value or semantic identity.
A number has one mathematical value after normalization. Reduced fractions give that value one exact spelling across products. The display needs neither source scale nor rounding policy.
Supply a source bundle or prepared artifact and one canonical input to lispex run. The selected program declares its entry. The command uses the single Datum boundary. The host reads files or standard input and displays the result. Guest code receives the input as an ordinary argument. The canonical codec defines the data representation.
Explicit input records the facts used by a rule. One result lets every caller handle the same decision without reconstructing a stream of guest effects.
15.5 Fresh requests in interactive tools
Each interactive execution uses a fresh finite request. Source editing state belongs to the host. An earlier value or failure does not become hidden input to the next rule.
Verification uses the recorded request and canonical outcome. Replay compares the language result. Signature verification checks the attached issuer evidence. The calling application separately decides whether to trust that issuer or act on the result.
Use the profile work report for qualification or evidence refusal after evaluation. Report the profile work identity and completed canonical outcome separately. A refusal before guest entry uses the admission report and has no canonical evaluation outcome.
15.6 Keep replay and evidence checks distinct
The verify command compares two supplied receipts. It performs no guest evaluation. The replay command evaluates the recorded request and compares its actual receipt with the expected receipt. Both use the comparison contract. They report issuer evidence checks separately. A valid signature does not replace semantic comparison or authorize a host action.
Execution agreement and issuer authentication answer different questions. Reporting each result preserves the information a caller needs to judge a receipt.
A preset names a complete finite limit selection. The command resolves that selection before admission and records the effective limits in the request. Products use the same common preset. The Resources chapter defines the resource axes and event order. A malformed explicit limit record is refused.
Public execution requests use finite limits for every phase they perform. A preparation request uses preparation limits. A run uses separate preparation and evaluation limits. Omitting an explicit selection chooses the common finite preset. Malformed explicit selections cause refusal before evaluation. A product cannot silently reduce the requested limits.
A default is still part of the request. Resolving it explicitly makes the same request reproducible across products and prevents malformed options from opening an unlimited path.
An exit class tells the caller how the command finished. A returned Datum is successful evaluation, including an application decision named deny or review. Language and resource failures, request refusal, profile refusal, and operational failure remain distinguishable.
The numeric mapping below distinguishes source preparation, admission, qualification, and required evidence. The command preserves a completed canonical outcome. A failed evaluation keeps its status when later profile host work refuses.
15.8 Common command outcomes
Products report common exit classes for a returned Datum, a deterministic language or resource failure, a request refusal, a profile refusal, and an operational failure. Application decision labels remain ordinary result data. After a successful evaluation, qualification or required evidence refusal uses the profile refusal class. The command reports the completed canonical outcome and the separate profile work report. A deterministic evaluation failure retains its failure class when later profile work also refuses.
Scripts need to distinguish a completed decision from a request that never produced a language result. Common classes make that distinction independent of the chosen product.
A caller needs to distinguish a completed language evaluation from delivery of a qualified profile result. A separate profile refusal class exposes that failure without rewriting the language outcome.
Each completed command uses the numeric status in this table. The status describes command completion. The canonical outcome remains separate.
Status
Phase
Completion
Exit class
0
Any completed operation
The requested operation succeeds
success
2
invocation or ingestion
Command arguments or input transport fail
request-refusal
10
decode, read, normalize, resolve, or prepare
Complete submitted source fails preparation
deterministic-failure
11
prepare
A finite preparation limit stops preparation
deterministic-failure
20
evaluate
An uncaught condition or value boundary failure ends evaluation
deterministic-failure
21
evaluate
A finite evaluation limit stops evaluation
deterministic-failure
30
admission
Artifact, package, request, or profile admission refuses entry
request-refusal
40
qualification
Qualification or its host budget refuses a successful evaluation
profile-refusal
41
evidence
Required evidence or its host budget refuses a successful evaluation
profile-refusal
42
verify or replay
Admitted records fail verification or comparison
request-refusal
50
render or host
Output delivery or host execution is interrupted
operational-failure
51
host
The product reports an engine defect
operational-failure
The preparation resource diagnostic uses phase prepare. Its stage identifies the interrupted source step. Status 11 produces no canonical evaluation outcome or evaluation receipt. Status 30 also produces neither.
Status 20 or 21 retains precedence over later qualification or evidence refusal. After successful evaluation, the first required profile refusal determines status 40 or 41. Both preserve the completed canonical outcome and its evaluation receipt eligibility.
A successful verification command returns 0 even when its operand records a language or resource failure. An exact replay preserves status 20 or 21 for a reproduced evaluation failure. A replay mismatch returns 42. The report preserves both the recorded outcome and the recomputed outcome. Operand admission failure uses 30 before comparison begins.
Output delivery failure uses command/CLI completion classification 50 even when evaluation has completed. Preserve the completed outcome and receipt. Qualification or evidence refusal still leaves completed evaluation status 20 or 21 unchanged; this precedence does not convert a delivery interruption into a profile refusal.
CommandResult.status is the status serialized in the selected packet. Delivery completion can be learned after that packet was fixed. Before the first primary octet, a complete preserving status 50 replacement may be selected under the command result guards. After the first octet, retain the packet's original status and bytes and classify command/CLI completion as 50 from the existing transport-error observation. A full packet followed by a flush failure obeys the same rule. Unknown delivery count or an in-flight write cannot establish the confirmed zero needed for replacement. A rejected replacement retains the original complete packet and completed data.
The delivery packet examples supply complete packets for these boundaries. An operational failure or engine defect never becomes a language failure receipt. An external process termination without a completion report supplies no portable command status. Other numeric command statuses are reserved.
This command/CLI classification preserves the existing ABI transport call-status enum 0, 1, and 2. A complete ABI reply uses transport success 0 even when its complete command record reports a refusal or failure. No extra status field, channel, or API is introduced.
Callers need to distinguish invalid source, exhausted preparation limits, rejected entry, and failed evaluation. Separate profile statuses show which later obligation failed. Fixed numbers let every product report the same completion without changing the language outcome.
Transport completion stays separate from bytes already delivered. Status 50 reports interruption without retroactively changing an earlier packet or its canonical evaluation outcome.
Diagnostic phases, stable codes, condition data, and failure reports.
Scope
Use a diagnostic phase and stable code to identify a failure. Canonical condition data carries its meaning. Source paths, translated messages, and stack displays help locate and explain it.
The reader and evaluation cases have distinct phase identities. Their 2.0 expectations follow exact number semantics. Conditions defines guest recovery and terminal failure.
Phase and code
A diagnostic identity combines its phase and stable code. Its data follows the closed catalog. Reading and resolving belong to preparation. Guest Conditions use phase evaluate. Resource exhaustion, admission refusal, profile work, host interruption, and engine defects retain separate identities.
16.1 Identify a failure by phase and code
A diagnostic has a phase, a stable code, and typed canonical parameters. A code alone does not identify the failure. Reader failures and evaluation failures have distinct phase identities. Translated messages and file names do not replace those fields.
A diagnostic identity is the pair of its phase and code. Every identity uses exactly one schema below. A code alone is insufficient.
Phase
Meaning
invocation
Command arguments are being checked.
ingestion
The product is reading an explicitly supplied host operand.
decode
Preparation is decoding source text.
read
Preparation is reading source forms.
normalize
Preparation is checking and normalizing forms.
resolve
Preparation is resolving lexical and module names.
prepare
Preparation is completing entry or resource checks.
admission
The product is checking a request before an admitted evaluation exists.
evaluate
An admitted request is decoding values, executing, or checking and encoding its result.
qualification
The selected profile is checking a completed language result.
evidence
The selected profile is producing or checking required evidence.
verify
The product is checking supplied verification operands under its finite host budget.
replay
A rerun differs from its required replay operand.
render
The product is writing a command result or another requested output.
host
An operational interruption or engine defect ended the attempt.
Source and binding failures follow their source, binding, and preparation rules. This table classifies those failures. It adds no source syntax or module loading behavior.
Phase
Code
Exact data fields
decode
source.encoding
reason uses SourceEncodingReason
read
source.token
reason uses SourceTokenReason
read
source.delimiter
reason uses SourceDelimiterReason
read
source.number
reason uses SourceNumberReason
normalize
syntax.form
form uses Text, reason uses SyntaxReason
normalize
binding.initializer
form uses InitializerForm, name uses Text, expected uses InitializerExpectation
normalize
binding.immutable
name uses Text
normalize, resolve
binding.duplicate
name uses Text, scope uses BindingScope
resolve
binding.unresolved
name uses Text
resolve
module.reference
module uses Text, name uses TextOrFalse, reason uses ModuleReason
resolve
library.reference
name uses Text, reason uses LibraryReason
prepare
entry.declaration
reason uses EntryReason
The condition catalog defines every guest Condition code and its exact semantic field schema. Each becomes a diagnostic with phase evaluate. This chapter imports those codes and schemas without adding members or fields. The typed field rule defines their wire projection.
Condition field type
Diagnostic field type
String
Text
StringOrFalse
TextOrFalse
Datum
DatumBytes
Every other catalog type
The same named type with the serialized form below
Entry result checks and terminal resource failures have separate identities. They have no guest Condition constructor.
A preparation limit failure uses phase prepare. Its stage records the interrupted preparation step. An evaluation limit failure uses phase evaluate. Its stage records the interrupted evaluation step.
Before a canonical input has been accepted, malformed input uses admission and input.codec. Invalid UTF-8 inside a canonical input packet uses reason invalid-utf8. Source UTF-8 failures use decode and source.encoding. Guest bytevector text conversion uses domain.range with reason invalid-utf8. Input decoding still spends EvaluationLimits. Exhaustion before request identity exists uses admission and input.resource. The charged account does not select the diagnostic phase.
Record identities describe host record mapping. They do not create a guest record value kind. A missing field is reported only when the selected mapping requires that field.
Admission produces no canonical evaluation outcome or evaluation receipt. Qualification and evidence reports preserve the completed language outcome and its receipt eligibility. Profile budget failure uses the phase of the interrupted profile work.
The command argument position starts at zero after the executable token. A missing option value names its introducing option. A missing required option names the end of the argument vector. Input and output transport failures belong to host activity. They do not become guest conditions.
For value.boundary, a count failure has count other than 1, an empty path, and false actual. A non-Datum result uses count 1, its first invalid path, and its type tag. Result checks run after the entry and its guards have returned.
Rows sharing a code have the same field schema. Their phases still distinguish their identities. Unknown pairs are rejected. No historical code is silently renamed.
The typed field rule defines serialized values. Exit mapping maps these phases and failure classes to command status.
Standalone verification uses verify and verification.budget when its finite host budget is exhausted. It preserves recorded outcomes and receipts. It creates no new evaluation receipt.
Evidence bound to another receipt uses verification.failed with evidence-binding. Replay operands bound to different requests use artifact.invalid with identity-mismatch before entry.
Identity work uses the diagnostic of the operation that owns its finite account. A refused host work reservation during profile admission uses admission/profile.budget; during qualification or evidence it uses that phase and profile.budget. The required profile field is the already selected builtin ProfileContractIdentity, and budget is work. Standalone verification work uses verify/verification.budget with budget = work. These closed catalog pairs also apply when hashing, rather than another host check, is the rejected work. Identity helpers do not reclassify such refusals as input.resource or spend EvaluationLimits. Physical host failures retain the host rows. Preparation and evaluation account refusals retain their own resource rows. This mapping selects no new hash event, coefficient, budget default, or check order.
The phase distinguishes failures that have different request and receipt boundaries. Stable codes and typed fields make product behavior comparable. Keeping host admission and profile work separate preserves the result already computed by the language.
Identity hashing uses the host work account of the operation that requests it. The complete event schedule and effective profile host budget remain in Profiles, while the diagnostic catalog fixes their wire observations.
These productions describe string contents. The report contract supplies their surrounding serialization. A hexadecimal string must also decode as the selected canonical Datum codec when used as DatumBytes.
Condition data
Present condition data through the exact phase, code, and typed data fields defined here. Human messages, locale, paths, and stack displays belong to presentation. The source map connects canonical sites to the supplied source.
16.3 Keep condition meaning separate from display
Evaluation reports preserve the canonical failure site and structured condition meaning. Changing a source map, message locale, host path or stack display leaves the canonical outcome unchanged. Guest recovery uses condition data under the Conditions contract.
Callers can replay a failure even when their source layout and diagnostic language differ. A host path or translated sentence should not change a rule decision.
16.4 Serialize typed diagnostic fields without coercion
A diagnostic field record has exactly the fields below. The data object has exactly the keys in its catalog schema. Every key is required.
Field
Serialized value
phase
A string from PhaseTag
code
The exact string from the selected catalog schema
data
The typed object declared by that schema
Field keys use unsigned UTF-8 byte order. DiagnosticPayloadBytes names the encoding of this field record. The same contract defines the surrounding command envelope. This rule fixes the wire projection of semantic field values.
Type
Serialized form
Text
A Unicode scalar string with exact case and no normalization
Operation
Text with the meaning given by the condition catalog
The canonical codec defines the complete CanonicalDatumBytes packet nested inside DatumBytes. Diagnostic serialization encodes those bytes as lowercase hexadecimal. It performs no decimal display rounding or alternate value conversion.
Path segment
Exact object fields
Pair car
kind equals car
Pair cdr
kind equals cdr
Vector index
kind equals index, index uses Nat
Record key
kind equals key, key uses Text
An empty path selects the whole value. Paths retain segment order. The condition catalog gives the ordinary list representation of these segments inside guest data.
Unknown phases, codes, fields, enum strings, and mistyped values are rejected. Extra fields and missing fields are rejected. Products reject numbers where exact integer strings are required. They do not normalize text or repair malformed paths.
An unknown diagnostic identity in a submitted artifact uses artifact.invalid with unknown-diagnostic. Other malformed diagnostic fields use artifact.invalid with invalid-format. A product that emits an invalid diagnostic has an engine.defect with invalid-product-observation.
Source coordinates and canonical sites belong to their source report and outcome envelopes. They are not data fields. Message text, locale, host paths, stacks, elapsed time, and work usage counters stay outside this field record.
The failing event reserves its required diagnostic payload under the resource event order. The failure is committed only after that reservation succeeds. Once committed, its first cause remains fixed. Emergency reporting and human formatting cannot replace it with another semantic failure.
Payload limits use the named resource model limits. No field is silently truncated. Product rendering failure remains a separate host report.
Exact field types prevent host numeric widths and message formats from changing a failure. Explicit paths preserve the first invalid component. The selected canonical codec keeps application data portable while report envelopes remain separately versioned.
A read or normalization failure can occur before any valid canonical program exists. Its preparation report is bound to the exact submitted source. Such a report carries the source location needed for repair. Evaluation locations use canonical sites after preparation succeeds. The identity chapter defines the separate records.
16.5 Bind an early report to source
A read or normalization failure produces a source bound preparation report. It identifies the exact submitted source and stops before entry evaluation. It does not invent a canonical program identity or canonical evaluation site for that failed source.
A malformed source still needs a useful report. Binding the report to submitted bytes preserves its meaning without pretending that program resolution succeeded.
16.6 Source and preparation diagnostic mapping
Source and preparation failures use the catalog identities below. The owning Rules still determine the first failed check. Mapping a failure adds no check and changes no reservation order.
The source order and module order remain authoritative. A diagnostic phase identifies its catalog family. It does not move a check to another step.
Reader check
Phase
Code
Exact data
Invalid source UTF-8
decode
source.encoding
reason = invalid-utf8
Invalid bare identifier, character token, token boundary, Boolean token, bracket, or quotation prefix
read
source.token
reason = invalid-token
Unknown string or identifier escape
read
source.token
reason = invalid-escape
Invalid scalar escape or literal control scalar
read
source.token
reason = invalid-scalar
Unterminated string or barred identifier
read
source.token
reason = unterminated-string
Unexpected source scalar, including a byte order mark
read
source.token
reason = unexpected-source-scalar
Unsupported reader prefix or directive
read
source.token
reason = unsupported-reader-prefix
Invalid bytevector element or unsupported unit imaginary literal
read
source.token
reason = unsupported-literal
Unfinished list or block comment, or missing quoted or commented datum
read
source.delimiter
reason = unexpected-end
Unmatched closing parenthesis
read
source.delimiter
reason = unexpected-close
Invalid dotted tail or vector element shape
read
source.delimiter
reason = improper-form
Invalid numeric spelling
read
source.number
reason = invalid-number
Zero literal denominator
read
source.number
reason = zero-denominator
Infinity or NaN spelling
read
source.number
reason = inexact-number
Numeric token classification follows the reader grammar. A token that enters numeric scanning keeps that classification. An unsupported exactness prefix uses the reader prefix row.
Binding or form check
Phase
Code
Exact data
Malformed parameter group or parameter identifier
normalize
syntax.form
form = lambda or the written procedure shorthand head define. reason = invalid-formals
Malformed binding group, member, or binding identifier
normalize
syntax.form
form is the written owning form head. reason = invalid-binding
Missing procedure body
normalize
syntax.form
form = lambda or define. reason = missing-body
Definition after an expression outside a guard body
normalize
syntax.form
form = define. reason = unexpected-definition
Assignment to an immutable binding
normalize
binding.immutable
name is the assigned identifier
Duplicate parameter
normalize
binding.duplicate
name is the repeated identifier. scope = parameters
Duplicate parallel let binding
normalize
binding.duplicate
name is the repeated identifier. scope = let
Duplicate recursive binding
normalize
binding.duplicate
name is the repeated identifier. scope = letrec
Duplicate internal definition
normalize
binding.duplicate
name is the repeated identifier. scope = body
Duplicate module definition or import and definition collision
normalize
binding.duplicate
name is the repeated identifier. scope = module
Duplicate import local name
normalize
binding.duplicate
name is the repeated local identifier. scope = imports
Duplicate export public name
normalize
binding.duplicate
name is the repeated public identifier. scope = exports
Non-lambda recursive initializer
normalize
binding.initializer
form = letrec or internal-definition. name is the binding. expected = lambda
Unresolved lexical name
resolve
binding.unresolved
name is the unresolved identifier
Removed library operation
resolve
library.reference
name is the removed public binding. reason = removed-operation
For syntax.form, form is the decoded source keyword. Procedure shorthand uses define. Guard clauses and bodies keep the reasons from the guard grammar.
All names preserve their decoded scalar values. Sequential let shadowing remains valid. Its repeated names do not enter a duplicate row.
Module check
Phase
Code
Exact data
Missing selected root or import target
resolve
module.reference
module is the absent module. name = false. reason = missing-module
Duplicate source module name
resolve
module.reference
module is the least duplicated name. name = false. reason = duplicate-module
Declared module name differs from the submitted name
normalize
syntax.form
form = module. reason = invalid-binding
Repeated module in one import clause
normalize
syntax.form
form = import. reason = invalid-binding
Invalid wrapper or clause order
normalize
syntax.form
form = module. reason = expected-shape
Invalid module name, import or export binding, or rename member
normalize
syntax.form
form = module, import, or export. reason = invalid-binding
Malformed import or export clause
normalize
syntax.form
form = import or export. reason = expected-shape
Imported public name is absent
resolve
module.reference
module is the target module. name is the requested public name. reason = missing-export
Export has no local binding
resolve
module.reference
module is the exporting module. name is the missing local name. reason = missing-export
Dependency cycle or self dependency
resolve
module.reference
module is the active ancestor reached by the first closing edge. name = false. reason = invalid-import
Cycle selection follows the existing canonical graph traversal. The reported module is the start of that selected cycle.
Entry check
Phase
Code
Exact data
Malformed entry clause
normalize
syntax.form
form = entry. reason = invalid-entry
Root has no entry declaration
prepare
entry.declaration
reason = missing-entry
Module repeats its entry declaration
prepare
entry.declaration
reason = duplicate-entry
Declared entry has no matching public export
prepare
entry.declaration
reason = unknown-entry
Entry initializer is a non-procedure literal
prepare
entry.declaration
reason = non-procedure
Entry initializer does not have the required lambda form
prepare
entry.declaration
reason = invalid-initializer
Entry lambda does not accept one argument
prepare
entry.declaration
reason = arity
Entry selection follows the entry Rules. A factory call fails the initializer check without running that call.
Prepared artifact check
Phase
Code
Exact data
Unsupported version or encoding contract
admission
artifact.invalid
kind = prepared. reason = unsupported-contract
Malformed framing, record, index, binding, child, site, tail flag, or event role
admission
artifact.invalid
kind = prepared. reason = invalid-format
Missing required submitted dependency
admission
artifact.invalid
kind = prepared. reason = missing-dependency
Incompatible fixed identity, dependency identity, or requested program identity
admission
artifact.invalid
kind = prepared. reason = identity-mismatch
Reused handle lacks its verified local issuer seal
admission
artifact.invalid
kind = prepared. reason = unverified-content
Malformed magic uses invalid-format. An understood format with an unsupported version uses unsupported-contract. Artifact mutation labels identify test cases. They are not additional diagnostic reasons.
The validation order decides the first artifact failure. Validation still leaves dynamic call and result checks at evaluation. Preparation exhaustion uses prepare and resource.exhausted. Its data contain the interrupted stage, rejected axis, and required event from the selected resource model.
Some examples leave model fields or host fault details symbolic. Their diagnosticIdentity selects only a phase and code. A separate reason constrains that catalog reason when specified. These are documentation selectors. A product supplies every required typed field in its complete diagnostic. The selectors do not define a report encoding.
Guest failures use the Condition schema. Preparation and admission failures have no guest Condition. Generic resource cases retain their named finite limits under cost-model-freeze.
One identity and one field schema let every product report the same failed check. Existing reasons cover the source and prepared artifact failures. More codes would duplicate their validation families. Product aliases would make equivalent failures differ. The mapping preserves the adopted check order and its resource boundaries.
A caller needs the actual cause of a stopped request. Replacing it with cleanup output or a fallback value would hide the boundary that ended execution.
Use one rule to select the first item of an input list. Change the input, inspect a failure, and repeat a request.
Scope
The examples state the Lispex 2.0 outcome. Native, npm, and WASM product plans are not run.
Every example keeps the same first-item definition. The request.json file shows the entry, input, and finite limits in documentation notation. The CLI and interchange chapters specify the concrete product forms.
The application displays that result. The rule needs no printing procedure.
17.1 Pass one input and receive one result
The root module declares first-item as its entry. The request supplies one list datum. For a nonempty list, first-item returns its first element as one result datum.
Read source.scm as the rule source for this chapter. Its module exports first-item and declares it as the entry. The parameter items receives the input datum. The body calls car with that value.
Every fixture contains this same module. The request selects main as its root module.
Replace the input with the empty list. Keep the rule source unchanged. The call to car fails because it requires a pair.
The condition catalog identifies this failure as domain.type in phase evaluate. The diagnostic field rule defines its serialized fields. Human message text does not change the canonical outcome.
17.2 Report an empty input as a failure
Passing the empty list to first-item produces a domain failure from car. The failed request returns no result datum.
The same replay procedure applies to the empty-input failure.
17.4 Repeat the complete request
Apply the exact-replay rule to first-item. Repeating the success request returns the same Datum. Repeating the empty-input request produces the same domain failure.
A recorded decision can be checked only when the program, input, semantics, and limits stay fixed. Separating the outcome from execution evidence makes that comparison precise.