I.8
Resources
Run every request with finite budgets. Preserve the first resource stop across products, caches, and optimizations.
Scope
Callers select finite limits for each requested phase. The same semantic request has the same resource outcome across supported products.
Sandbox contract defines the semantic request. Conditions defines terminal failures. Preparation defines the prepared program.
Resource axes
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.
Why
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.
Why
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.
Why
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.
Why
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.
Why
A host stack has platform specific behavior. Explicit semantic frames preserve recursion and failure locations across products.
Active guard protection must remain in the frame count.
Resolve the shared finite preset
lispex.example.v2.resources.common-default · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "the shared finite prepare preset sufficient for this source",
"evaluate": "the shared finite evaluation preset sufficient for this datum"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"limitSelection": "the documented common default preset",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"resolvedLimits": {
"prepareFinite": true,
"evaluateFinite": true,
"commonPreset": true
}
}Product invocation
Expected result
The convenience request resolves finite limits for both phases and returns 42. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Reject an unlimited request
lispex.example.v2.resources.unlimited-rejected · rev. 3
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"requestedLimits": {
"evaluateWork": {
"fixtureValue": "unlimited"
}
},
"operationUnderTest": "Submit an explicitly unlimited evaluation work limit.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
{"kind":"admission-failure","valueCount":0}Outcome details
{
"kind": "admission-failure",
"valueCount": 0
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"entryEvaluated": false,
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Product invocation
Expected result
Admission rejects the unlimited limit before guest evaluation. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Meter work inside exact multiplication
lispex.example.v2.resources.native-arithmetic-work · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(* input input)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "work sufficient through operand and domain checks but below a required multiplication work reservation, with every other axis sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "18446744073709551616"
}
}
],
"siteNotation": {
"multiply-step": "the first multiplication work event whose cumulative work exceeds the chosen limit"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · workOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "work",
"site": {
"fixtureSite": "multiply-step"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"unmeteredNativeWork": false
}Product invocation
Expected result
Exact multiplication exhausts work at the designated arithmetic event before a result is returned. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Keep discarded allocation charges
lispex.example.v2.resources.allocation-no-refund · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(begin
(cons input '())
(cons input '())
input)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "allocation sufficient through all events before second-pair but less than the cumulative reservation for second-pair, with every other axis sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
}
},
{
"input": {
"kind": "integer",
"value": "1"
}
},
{
"input": {
"kind": "integer",
"value": "1"
}
}
],
"executionContexts": [
"ordinary allocation",
"eager collection of discarded values",
"physical interning or sharing"
],
"siteNotation": {
"second-pair": "the second cons allocation event in source order"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "second-pair"
}
}resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "second-pair"
}
}resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "second-pair"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"comparison": {
"canonicalOutcomeEqual": true,
"evaluationChargesEqual": true,
"allocationRefunded": false
}
}Product invocation
Expected result
All three paths stop at the second pair allocation. Discarding or sharing the first pair does not refund its logical charge. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Replace the frame in a tail loop
lispex.example.v2.resources.tail-frame-replacement · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop ((n input))
(if (= n 0)
1
(loop (- n 1))))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite work and allocation sufficient for the complete request including input decoding, eight recursive calls, the base case, and result encoding, with all channels sufficient and frames sufficient for one active loop call and its declared expression events"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "8"
}
}
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
1Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "1"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"frameBehavior": {
"recursiveTailCallsAddCallFrames": false
}
}Product invocation
Expected result
The tail loop returns 1. Each recursive tail call replaces its current call frame. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Stop before an additional nontail frame
lispex.example.v2.resources.nontail-frame-stop · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(letrec ((count
(lambda (n)
(if (= n 0)
0
(+ 1 (count (- n 1)))))))
(count input))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "frame capacity sufficient through all prior semantic events but insufficient for the designated next recursive-count call before the base case, with every other axis sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "8"
}
}
],
"siteNotation": {
"recursive-count": "the recursive call to count inside the addition"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · framesOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "frames",
"site": {
"fixtureSite": "recursive-count"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"hostStackDeterminesStop": false
}Product invocation
Expected result
The next nontail call exceeds active frame capacity and stops at the recursive count site. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Resolve model metadata after the axis data
lispex.example.v2.resources.model-definition-order · rev. 1
{
"notation": "documentation-request",
"operation": "validate model declaration and resolve common-default",
"model": "one supported complete symbolic model fixture",
"defaultAxes": "concrete finite values chosen only after cost model freeze",
"checks": "Inspect the model identity preimage, then resolve the host budget with that verified identity."
}
Semantic detailsSpecification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"dependencyOrder": [
"independent-semantic-definitions",
"default-axis-data",
"complete-model-definition",
"resource-model-identity",
"resolved-budget-wrapper",
"profile-work-identity"
],
"modelPreimage": {
"selfDigest": false,
"moduleIdentity": false,
"libraryIdentity": false,
"programIdentity": false,
"requestIdentity": false,
"profileWorkIdentity": false,
"resolvedBudgetWrapper": false
},
"resolvedHostBudget": {
"resourceModelPresent": true,
"axisCount": 6,
"metadataCount": 2
},
"canonicalSite": {
"programDigestInside": false,
"qualifiedByOuterReport": true
}
}Product invocation
Expected result
The model preimage contains independent defaults and no identity derived from that model. Product invocation awaits its 2.0 adapter.
These cases use symbolic finite limits and independently authored expectations. They remain not-run until the 2.0 products and observation adapter exist.
Reservation
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.
Why
Charging after allocation or computation would let the host perform work beyond the admitted bound.
Refuse a pair before its allocation effect
lispex.example.v2.resources.refused-allocation · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cons input '())))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "logical allocation sufficient through prior events but below the pair-construction reservation, with every other axis sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
}
}
],
"siteNotation": {
"pair-construction": "the cons allocation event"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "pair-construction"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"refusedEvent": {
"effectCommitted": false
}
}Product invocation
Expected result
The pair allocation reservation fails. The event creates no logical pair and returns no datum. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Resource event order
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.
Why
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.
Why
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.
| Implicit call | Occurrence and prefix |
|---|---|
| Selected entry | Entry lambda node, field(entry) |
| List traversal callback | Invoking call node, field(callback), element(tuple index) |
| Apply target | Invoking call node, field(target) |
| Call-with-values producer | Invoking call node, field(producer) |
| Call-with-values consumer | Invoking call node, field(consumer) |
| Named let initial call | Namedlet node, field(initial-call) |
| Clause receiver | Clause record, field(receiver) |
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.
Why
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.
Reserve every equality validation visit
lispex.example.v2.resources.equality-reservation-path · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(equal? (cons 0 (lambda (x) x)) (cons 1 (lambda (x) x)))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "complete-left-check",
"input": {
"kind": "list",
"items": []
},
"limits": "sufficient through the left domain failure"
},
{
"case": "left-tail-reservation",
"input": {
"kind": "list",
"items": []
},
"limits": "work below the left cdr datum-validate reservation"
}
]
}
domain.equalityOutcome details
{
"kind": "language-failure",
"condition": {
"phase": "evaluate",
"code": "domain.equality",
"data": {
"operation": "equal?",
"operand": "0",
"path": [
{
"kind": "cdr"
}
],
"actual": "procedure"
}
}
}resource-stop · workOutcome details
{
"kind": "resource-stop",
"terminal": true,
"axis": "work",
"event": "datum-validate",
"site": {
"fixtureSite": "equal-call",
"role": "datum-validate",
"path": [
{
"kind": "argument",
"index": "0"
},
{
"kind": "cdr"
}
]
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"leftValidationOrder": [
"root",
"car",
"cdr"
],
"rightValidationStarted": false,
"comparisonStarted": false
}
}Product invocation
Expected result
The left operand is validated completely before any right validation or comparison. A refused visit stops before its type inspection. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Finish list validation before a callback
lispex.example.v2.resources.list-tail-reservation · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(map (lambda (x) (car '())) (cons 1 2))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"input": {
"kind": "list",
"items": []
},
"limits": "sufficient through the final improper-tail check"
}
]
}
domain.typeOutcome details
{
"kind": "language-failure",
"condition": {
"phase": "evaluate",
"code": "domain.type",
"data": {
"operation": "map",
"argument": "1",
"path": [
{
"kind": "cdr"
}
],
"expected": "proper-list",
"actual": "integer"
}
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"listVisits": [
"pair",
"final-tail"
],
"callbackArityChecked": false,
"callbackCalled": false,
"laterAllocation": false
}
}Product invocation
Expected result
The final list tail fails before callback arity and before the callback can raise another condition. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Check callback results before result allocation
lispex.example.v2.resources.callback-result-reservation · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(map (lambda (x) (values x x)) '(1 2))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"input": {
"kind": "list",
"items": []
},
"limits": "sufficient through the first callback result-count failure"
}
]
}
runtime.value-countOutcome details
{
"kind": "language-failure",
"condition": {
"phase": "evaluate",
"code": "runtime.value-count",
"data": {
"expected": "1",
"actual": "2"
}
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"tupleOrder": [
"0"
],
"afterCallback": [
"result-check",
"diagnostic-payload"
],
"resultPairAllocated": false,
"nextCallbackCalled": false
}
}Product invocation
Expected result
The first callback returns two values. Its result-check fails before constructing the first output pair or calling the second callback. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
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).
Why
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.
Reserve a source precheck before inspecting it
lispex.example.v2.resources.source-check-reservation · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let ((x (car '())) (x 2)) x)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "duplicate",
"input": {
"kind": "list",
"items": []
},
"prepareLimits": "sufficient through duplicate detection"
},
{
"case": "reservation",
"input": {
"kind": "list",
"items": []
},
"prepareLimits": "work below the second member duplicate-check reservation"
}
]
}
{"kind":"preparation-failure","phase":"normalize","code":"binding.duplicate","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "preparation-failure",
"phase": "normalize",
"code": "binding.duplicate",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}{"kind":"preparation-resource-stop","phase":"prepare","stage":"normalize","axis":"work","event":"prepare.binding-check","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "preparation-resource-stop",
"phase": "prepare",
"stage": "normalize",
"axis": "work",
"event": "prepare.binding-check",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"groupChecks": [
"envelope",
"member-0-shape",
"member-0-identifier",
"member-0-duplicate",
"member-1-shape",
"member-1-identifier",
"member-1-duplicate"
],
"initializerNormalized": false,
"entryEvaluated": false
}
}Product invocation
Expected result
The duplicate check is reached before either initializer. A refused reservation prevents that same check from inspecting the duplicate. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Capture prepared bytes before validation reads
lispex.example.v2.resources.prepared-capture-reservation · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "capture-stop",
"input": {
"kind": "integer",
"value": "42"
},
"preparedOperand": "canonical prepared bytes for this source",
"prepareLimits": "allocation below prepared.capture-input"
},
{
"case": "captured-snapshot",
"input": {
"kind": "integer",
"value": "42"
},
"preparedOperand": "the same immutable prepared bytes",
"hostAction": "mutate only the caller copy after successful capture",
"prepareLimits": "sufficient for validation"
}
]
}
{"kind":"preparation-resource-stop","event":"prepared.capture-input","axis":"allocation","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "preparation-resource-stop",
"event": "prepared.capture-input",
"axis": "allocation",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}{"kind":"prepared-handle","immutable":true,"canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "prepared-handle",
"immutable": true,
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"refusedCaptureReads": [],
"acceptedCaptureFirstRead": "prepared.read-header",
"validatedAndSealedSnapshotEqual": true,
"callerCopyChangesHandle": false
}
}Product invocation
Expected result
A refused capture performs no validation read. An accepted capture binds all later checks and the handle to one immutable snapshot. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Bound graph export without executing the program
lispex.example.v2.resources.graph-output-reservation · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"operation": "graph",
"verifiedProgram": "the prepared handle for this source",
"prepareLimits": "result below the exact GraphBytes packet and earlier budgets sufficient"
}
]
}
{"kind":"preparation-resource-stop","phase":"prepare","stage":"prepare","axis":"result","event":"result-channel","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "preparation-resource-stop",
"phase": "prepare",
"stage": "prepare",
"axis": "result",
"event": "result-channel",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"projectionCompleted": true,
"outputSized": true,
"outputOctets": "0",
"entryEvaluated": false,
"existingHandleChanged": false
}
}Product invocation
Expected result
The graph projection and size pass complete before the full output reservation. A refused graph packet publishes no bytes and runs no guest code. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
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.
The canonical Datum grammar and validation order apply unchanged. These events supply their reservation positions.
| Operation | Ordered events | Site suffix |
|---|---|---|
| Packet open | codec-frame before any magic read or encoding size pass | field(open) |
| Magic | codec-byte before each octet read, then its fixed magic check | byte(i) |
| Integer or length field | codec-byte per digit, then codec-integer before canonical interpretation and the required span or count check | Schema field path and digit offset |
| Packet boundary | codec-frame before comparing payload length with the remaining captured span | field(boundary) |
| Value decode | codec-value before the next tag, then its codec-byte and fields in grammar order | Datum component path |
| Text decode | codec-scalar before each scalar attempt, then codec-byte per consumed octet and scalar validation | Scalar start and byte offsets |
| Bytevector decode | codec-byte per payload octet after its checked length | byte(i) |
| Rational validation | codec-rational-check for denominator, numerator, then reduction after their integer fields | field(denominator), field(numerator), field(reduction) |
| Packet close | codec-frame before the exact root-end check | field(close) |
| Decoded Datum materialization | 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.
| Event family | ResourceStage |
|---|---|
| Source capture and prepare.decode-step | decode |
| prepare.read-step, prepare.read-enter, prepare.read-node | read |
| 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.
Why
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
lispex.example.v2.resources.input-codec-before-identity · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "input-stop",
"canonicalInputHex": "6c69737065782e646174756d2f32000100",
"evaluationLimits": "input below the complete canonical packet"
},
{
"case": "work-stop",
"canonicalInputHex": "6c69737065782e646174756d2f32000100",
"evaluationLimits": "work below the codec-frame boundary check"
}
]
}
{"kind":"admission-failure","phase":"admission","code":"input.resource","axis":"input","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "admission-failure",
"phase": "admission",
"code": "input.resource",
"axis": "input",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}{"kind":"admission-failure","phase":"admission","code":"input.resource","axis":"work","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "admission-failure",
"phase": "admission",
"code": "input.resource",
"axis": "work",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"accounting": {
"chargedAccount": "evaluate",
"identityCreated": false,
"accountReset": false,
"entryEvaluated": false,
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
},
"inputHex": "6c69737065782e646174756d2f32000100"
}Product invocation
Expected result
Both refusals spend the evaluation account before request identity. Neither produces a canonical evaluation outcome or an evaluation receipt. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Reserve a failure payload before committing a Condition
lispex.example.v2.resources.diagnostic-payload-reservation · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(guard (c (else 7)) (car '()))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "catchable",
"input": {
"kind": "list",
"items": []
},
"limits": "sufficient for the failed check and complete diagnostic payload"
},
{
"case": "payload-stop",
"input": {
"kind": "list",
"items": []
},
"limits": "diagnostic below the complete automatic Condition payload"
}
]
}
7Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "7"
}
}resource-stop · diagnosticOutcome details
{
"kind": "resource-stop",
"terminal": true,
"axis": "diagnostic",
"event": "diagnostic-payload",
"site": {
"fixtureSite": "car-call",
"role": "diagnostic-payload",
"path": [
{
"kind": "argument",
"index": "0"
}
]
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"failureCommit": {
"successfulPayloadRunsGuard": true,
"refusedPayloadRunsGuard": false,
"partialConditionPublished": false,
"terminalUsesAnotherDiagnosticReservation": false
}
}Product invocation
Expected result
The guard catches the domain condition only after its payload reservation succeeds. Payload exhaustion is terminal and uses the reserved final report. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Reserve the complete result packet before emitting bytes
lispex.example.v2.resources.result-codec-order · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"input": {
"kind": "string",
"value": "é"
},
"limits": "result below the exact complete lispex.datum/2 packet and all prior budgets sufficient"
}
]
}
resource-stop · resultOutcome details
{
"kind": "resource-stop",
"terminal": true,
"axis": "result",
"event": "result-channel",
"site": {
"fixtureSite": "entry-result",
"role": "result-channel",
"path": [
{
"kind": "field",
"name": "output"
},
{
"kind": "field",
"name": "packet"
}
]
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"order": [
"result-check",
"datum-validate",
"codec-frame",
"codec-value",
"codec-integer",
"codec-scalar",
"codec-integer",
"result-channel"
],
"codecAllocationForOutput": false,
"emittedResultOctets": "0",
"successfulResultPrefix": false
}
}Product invocation
Expected result
The result count, Datum validation, and size pass finish before the packet reservation. A refused packet reservation emits no successful result prefix. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Measure every record before reserving host output
lispex.example.v2.resources.host-egress-record-order · rev. 1
{
"notation": "documentation-request",
"operation": "host-egress-projection",
"candidateDatum": "R{command=#(),format=\"lispex.command-result/2\",payload=#(),receipt=#(),reports=R{admission=#(),attempt=#(),evidence=#(),preparation=#(),profile=#(),terminal=#()},status=0,trace=#()}",
"candidateBytesHex": "6c69737065782e646174756d2f3200c40108080607636f6d6d616e64090008080606666f726d617406176c69737065782e636f6d6d616e642d726573756c742f32080806077061796c6f6164090008080607726563656970740900080806077265706f7274730808060961646d697373696f6e090008080607617474656d707409000808060865766964656e636509000808060b7072657061726174696f6e09000808060770726f66696c650900080806087465726d696e616c090000080806067374617475730300080806057472616365090000",
"conversionWorkspace": "finite host backing and work secured before the first measurement; this Open candidate has no guest account",
"emergencySupport": "complete terminal and record framing support secured separately",
"requests": [
{
"case": "complete",
"admission": "accepted",
"outputLimit": "213",
"physicalOutputAllocation": "available"
},
{
"case": "logical-output-refusal",
"admission": "pending; inspect this possible reply before ordinary Open work",
"outputLimit": "212",
"physicalOutputAllocation": "not-attempted"
},
{
"case": "physical-output-refusal",
"admission": "accepted",
"outputLimit": "213",
"physicalOutputAllocation": "unavailable-after-successful-reservation"
}
]
}
{"case":"complete","kind":"complete-packet","status":0}Outcome details
{
"case": "complete",
"kind": "complete-packet",
"status": 0
}{"case":"logical-output-refusal","kind":"admission-failure","diagnosticIdentity":{"phase":"admission","code":"host.envelope"},"reason":"unsupported-limits","ordinaryOperationStarted":false}Outcome details
{
"case": "logical-output-refusal",
"kind": "admission-failure",
"diagnosticIdentity": {
"phase": "admission",
"code": "host.envelope"
},
"reason": "unsupported-limits",
"ordinaryOperationStarted": false
}{"case":"physical-output-refusal","kind":"host-failure","diagnosticIdentity":{"phase":"host","code":"host.interrupted"},"reason":"physical-exhaustion","stage":"render","completedDataPreserved":true}Outcome details
{
"case": "physical-output-refusal",
"kind": "host-failure",
"diagnosticIdentity": {
"phase": "host",
"code": "host.interrupted"
},
"reason": "physical-exhaustion",
"stage": "render",
"completedDataPreserved": true
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"measurement": {
"events": [
{
"kind": "record",
"path": []
},
{
"kind": "field",
"path": [
"command"
]
},
{
"kind": "field",
"path": [
"format"
]
},
{
"kind": "field",
"path": [
"payload"
]
},
{
"kind": "field",
"path": [
"receipt"
]
},
{
"kind": "field",
"path": [
"reports"
]
},
{
"kind": "record",
"path": [
"reports"
]
},
{
"kind": "field",
"path": [
"reports",
"admission"
]
},
{
"kind": "field",
"path": [
"reports",
"attempt"
]
},
{
"kind": "field",
"path": [
"reports",
"evidence"
]
},
{
"kind": "field",
"path": [
"reports",
"preparation"
]
},
{
"kind": "field",
"path": [
"reports",
"profile"
]
},
{
"kind": "field",
"path": [
"reports",
"terminal"
]
},
{
"kind": "field",
"path": [
"status"
]
},
{
"kind": "field",
"path": [
"trace"
]
}
],
"recordCount": "2",
"fieldCount": "13",
"payloadOctets": "196",
"packetLengthOctets": "2",
"completePacketOctets": "213"
},
"operationProjection": [
{
"case": "complete",
"order": [
"egress.measure(all-15)",
"egress.reserve-output",
"physical-output-allocation",
"egress.write-byte(0..212)",
"egress.publish"
],
"reservedOutputOctets": "213",
"writtenOctets": "213",
"publishedBytesHex": "6c69737065782e646174756d2f3200c40108080607636f6d6d616e64090008080606666f726d617406176c69737065782e636f6d6d616e642d726573756c742f32080806077061796c6f6164090008080607726563656970740900080806077265706f7274730808060961646d697373696f6e090008080607617474656d707409000808060865766964656e636509000808060b7072657061726174696f6e09000808060770726f66696c650900080806087465726d696e616c090000080806067374617475730300080806057472616365090000",
"normalPacketsPublished": "1",
"guestResultDebited": false
},
{
"case": "logical-output-refusal",
"order": [
"egress.measure(all-15)",
"egress.reserve-output(refused)"
],
"reservedOutputOctets": "0",
"physicalOutputAllocationAttempted": false,
"writtenOctets": "0",
"normalPacketsPublished": "0",
"guestResultDebited": false
},
{
"case": "physical-output-refusal",
"order": [
"egress.measure(all-15)",
"egress.reserve-output",
"physical-output-allocation(refused)"
],
"reservedOutputOctets": "213",
"writtenOctets": "0",
"normalPacketsPublished": "0",
"refund": false,
"emergencySupportRetained": true,
"guestResultDebited": false
}
]
}Product invocation
Expected result
The complete Open reply has a 196-octet root, two-octet U(196)=c4 01 length, and 15-octet magic: 213 octets. Product invocation awaits its 2.0 adapter.
The complete Open reply has a 196-octet root, two-octet U(196)=c4 01 length, and 15-octet magic: 213 octets.
The displayed hex follows the Datum grammar and closed CommandResult schema. Fifteen measurements visit two records and thirteen fields in depth-first wire order. The write range denotes one egress.write-byte for each offset 0 through 212. Physical output allocation is an effect, not a new semantic event. The order strings are documentation projection labels.
The 212-octet case checks the possible reply during admission, before ordinary Open work. The 213-octet physical case has already admitted and reserved the exact output. Backing failure retains its charge and uses separate emergency support. These ceilings illustrate the inclusive boundary; product defaults and tariffs remain with the resource model. The diagnosticIdentity and reason fields are report projections. Complete diagnostic records also retain their catalog fields.
Keep a domain check before later arithmetic work
lispex.example.v2.resources.domain-before-later-charge · rev. 3
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(* input input)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient through the required checks and encoding of their domain condition"
},
"requests": [
{
"input": {
"kind": "symbol",
"value": "invalid"
}
},
{
"input": {
"kind": "symbol",
"value": "invalid"
}
}
],
"executionContexts": [
"ordinary primitive path",
"candidate precharged path"
],
"operationUnderTest": "A candidate precharge must not perform or reserve multiplication work before the earlier numeric domain check.",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
domain.typeOutcome details
{
"kind": "language-failure",
"valueCount": 0,
"condition": {
"phase": "evaluate",
"code": "domain.type",
"data": {
"operation": "*",
"argument": "0",
"path": [],
"expected": "number",
"actual": "symbol"
}
}
}domain.typeOutcome details
{
"kind": "language-failure",
"valueCount": 0,
"condition": {
"phase": "evaluate",
"code": "domain.type",
"data": {
"operation": "*",
"argument": "0",
"path": [],
"expected": "number",
"actual": "symbol"
}
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"laterArithmeticEventEntered": false,
"comparison": {
"canonicalOutcomeEqual": true,
"canonicalFailureSiteEqual": true
}
}Product invocation
Expected result
The numeric domain check reports the symbol input. A charge for later multiplication cannot replace that condition. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Preserve the stop through constant sharing
lispex.example.v2.resources.optimized-first-stop · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(list (cons input '()) (cons input '()))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "logical allocation sufficient through prior events but below the second-pair reservation, with every other axis sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
}
},
{
"input": {
"kind": "integer",
"value": "1"
}
}
],
"executionContexts": [
"unoptimized evaluation",
"optimized evaluation with physical sharing"
],
"siteNotation": {
"second-pair": "the second cons allocation event in source order"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "second-pair"
}
}resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "second-pair"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"comparison": {
"firstFailureEqual": true,
"exhaustedAxisEqual": true,
"canonicalSiteEqual": true,
"evaluationChargesEqual": true
}
}Product invocation
Expected result
Both paths stop on logical allocation at the second pair site. Sharing cannot skip that semantic event. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
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.
Why
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.
Choose the first insufficient axis at one event
lispex.example.v2.resources.two-insufficient-axes · rev. 3
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(cons input '())))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "each boundary covers all prior events and varies only the specified reservations at pair-construction, with other applicable axes sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "1"
},
"boundary": "both work and logical allocation are insufficient at pair-construction"
},
{
"input": {
"kind": "integer",
"value": "1"
},
"boundary": "work fits but logical allocation is insufficient at pair-construction"
}
],
"siteNotation": {
"pair-construction": "the atomic pair construction event requiring work and logical allocation"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · workOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "work",
"site": {
"fixtureSite": "pair-construction"
}
}resource-stop · logical-allocationOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "logical-allocation",
"site": {
"fixtureSite": "pair-construction"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"reservation": {
"refusedEventChargesCommitted": false,
"refusedEventEffectCommitted": false,
"priorCommittedChargesPreserved": true
}
}Product invocation
Expected result
The first request stops on work. The second stops on logical allocation at the same site. Neither commits the refused event charges or effect. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Initialize one module definition in event order
lispex.example.v2.resources.module-definition-events · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define saved 7)
(define rule (lambda (input) saved)))
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the complete request and result encoding"
},
"requests": [
{
"input": {
"kind": "list",
"items": []
}
}
],
"fixtureSites": {
"saved-definition-group": "The stored sequential module group for saved in main."
}
}
7Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "7"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"definition": "saved",
"events": [
"literal-value",
"result-check",
"environment-create",
"binding-initialize"
],
"resultCheckSite": {
"fixtureSite": "saved-definition-group",
"role": "result-check",
"path": [
{
"kind": "element",
"index": "0"
}
]
},
"intermediateSequenceRetained": false
}
}Product invocation
Expected result
The saved definition returns 7 after one single-value check and one binding step. Its result-check names element zero of the sequential module group. No intermediate sequence is retained. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Allocate rest pairs at the lambda site
lispex.example.v2.resources.rest-list-sites · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
((lambda (head . rest) rest) 10 20 30))))
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the complete request and result encoding"
},
"requests": [
{
"input": {
"kind": "list",
"items": []
}
}
],
"fixtureSites": {
"rest-lambda": "The lambda occurrence with fixed parameter head and rest parameter rest."
}
}
(20 30)Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "list",
"items": [
{
"kind": "integer",
"value": "20"
},
{
"kind": "integer",
"value": "30"
}
]
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"operationProjection": {
"restPairSites": [
{
"fixtureSite": "rest-lambda",
"role": "datum-allocate",
"path": [
{
"kind": "result",
"index": "0"
},
{
"kind": "element",
"index": "0"
}
]
},
{
"fixtureSite": "rest-lambda",
"role": "datum-allocate",
"path": [
{
"kind": "result",
"index": "0"
},
{
"kind": "element",
"index": "1"
}
]
}
]
}
}Product invocation
Expected result
The rest list contains 20 and 30. Both pair allocations name the invoked lambda and result zero. Their element indices are zero and one. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Limit boundaries
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.
Why
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.
Why
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.
Why
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.
Count a multibyte string packet by octets
lispex.example.v2.resources.channel-octet-boundary · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "below",
"canonicalInputHex": "6c69737065782e646174756d2f3200040602c3a9",
"limits": "result N minus one, with all other limits sufficient"
},
{
"case": "exact",
"canonicalInputHex": "6c69737065782e646174756d2f3200040602c3a9",
"limits": "result N, with all other limits sufficient"
},
{
"case": "above",
"canonicalInputHex": "6c69737065782e646174756d2f3200040602c3a9",
"limits": "result N plus one, with all other limits sufficient"
}
]
}
resource-stop · resultOutcome details
{
"kind": "resource-stop",
"axis": "result",
"event": "result-channel",
"terminal": true
}"é"Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "string",
"value": "é"
}
}"é"Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "string",
"value": "é"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"packet": {
"hex": "6c69737065782e646174756d2f3200040602c3a9",
"octets": "20",
"textScalars": "1"
},
"boundary": {
"N": "complete canonical packet octet count",
"exactLimitAccepted": true,
"belowLimitResultOctets": "0",
"successfulPacketsEqual": true
}
}Product invocation
Expected result
The complete packet has twenty octets. A single Unicode scalar does not make the channel charge one. The exact packet limit succeeds. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
8.16 Reserve one complete terminal representation
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.
Why
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
lispex.example.v2.resources.emergency-resource-cause · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (* input input)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "17"
},
"limits": "work below exact-arithmetic at multiply and diagnostic zero",
"emergency": "the admitted complete terminal and framing bounds are reserved"
}
]
}
resource-stop · workOutcome details
{
"kind": "resource-stop",
"phase": "evaluate",
"code": "resource.exhausted",
"stage": "entry",
"axis": "work",
"event": "exact-arithmetic",
"terminal": true
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"terminalView": {
"format": "lispex.terminal/1",
"causePreserved": true,
"program": "the verified program identity bytes",
"request": "the accepted request identity bytes",
"location": {
"kind": "program",
"site": "the exact refused multiply event CanonicalSiteBytes"
}
},
"reporting": {
"ordinaryDiagnosticReservationAttempted": false,
"guestReservationAfterCause": false,
"completeTerminalPayload": true,
"completeReportFraming": true,
"causeChangedByFormatting": false,
"terminalSlot": "reports.terminal",
"outerFramingReservedBeforeNormalWork": true,
"traceInsideTerminal": false
}
}Product invocation
Expected result
The work refusal remains the first cause. The pre-reserved terminal and framing bytes remain available with no ordinary diagnostic capacity. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Report an input refusal without inventing request identity
lispex.example.v2.resources.emergency-before-identity · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"canonicalInputHex": "6c69737065782e646174756d2f32000100",
"limits": "input below the next codec-byte reservation before packet acceptance",
"emergency": "the trusted pre-identity terminal bound is reserved"
}
]
}
{"kind":"admission-failure","phase":"admission","code":"input.resource","axis":"input","canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}Outcome details
{
"kind": "admission-failure",
"phase": "admission",
"code": "input.resource",
"axis": "input",
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"terminalView": {
"format": "lispex.terminal/1",
"program": "the verified program identity bytes",
"request": false,
"location": {
"kind": "program",
"site": "the exact codec-byte site at the selected entry input boundary"
},
"completeCause": true
},
"identity": {
"requestIdentityInvented": false,
"handleNumberSerialized": false,
"entryEvaluated": false
},
"traceReportPresent": false
}Product invocation
Expected result
The terminal preserves the input refusal and program-local location. Its request field is false because no canonical request has been accepted. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Retain complete committed diagnostic bytes
lispex.example.v2.resources.emergency-preserves-payload · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(raise (make-condition "domain.application"
(list (cons "tag" "é") (cons "data" input))))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"input": {
"kind": "string",
"value": "é"
},
"limits": "sufficient to construct and commit the complete uncaught Condition",
"hostPresentation": "host delivery is interrupted during later human diagnostic expansion after the cause commits"
}
]
}
domain.applicationOutcome details
{
"kind": "language-failure",
"condition": {
"phase": "evaluate",
"code": "domain.application",
"data": {
"tag": "é",
"data": "6c69737065782e646174756d2f3200040602c3a9"
}
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"terminalView": {
"format": "lispex.terminal/1",
"cause": "byte-for-byte identical committed DiagnosticPayloadBytes",
"location": "the exact explicit raise CanonicalSiteBytes"
},
"preservation": {
"diagnosticFieldsTruncated": false,
"diagnosticRenamed": false,
"sourceLabelSerialized": false,
"completedOutcomeChanged": false,
"receiptEligibilityChanged": false
}
}Product invocation
Expected result
The emergency payload retains the complete committed condition and explicit raise site. Later human formatting cannot truncate or replace them. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Secure backing, cursor state, and work before starting
lispex.example.v2.resources.emergency-framing-admission · rev. 1
{
"notation": "documentation-request",
"operation": "secure-emergency-record-framing",
"bounds": {
"terminal": "EmergencyTerminalBound",
"framing": "EmergencyFramingBound",
"cursor": "EmergencyCursorBound",
"work": "EmergencyWorkBound"
},
"boundMeaning": "complete finite bounds of the checked admitted interface",
"requests": [
{
"case": "missing-terminal-backing",
"unsecuredRequirement": "terminal-backing",
"otherRequirements": "secured to their complete admitted bound",
"firstOrdinaryEvent": "permitted only after all four requirements are secured"
},
{
"case": "missing-framing-backing",
"unsecuredRequirement": "framing-backing",
"otherRequirements": "secured to their complete admitted bound",
"firstOrdinaryEvent": "permitted only after all four requirements are secured"
},
{
"case": "missing-cursor",
"unsecuredRequirement": "cursor",
"otherRequirements": "secured to their complete admitted bound",
"firstOrdinaryEvent": "permitted only after all four requirements are secured"
},
{
"case": "missing-work",
"unsecuredRequirement": "work",
"otherRequirements": "secured to their complete admitted bound",
"firstOrdinaryEvent": "permitted only after all four requirements are secured"
},
{
"case": "all-secured",
"unsecuredRequirement": "none",
"otherRequirements": "secured to their complete admitted bound",
"firstOrdinaryEvent": "permitted only after all four requirements are secured"
}
]
}
{"case":"missing-terminal-backing","ordinaryPhaseStarted":false,"normalReservationsAttempted":false,"guestReservationAttempted":false,"completeEmergencySupport":false,"partialReplyPublished":false,"diagnosticIdentity":{"phase":"admission","code":"host.envelope"},"reason":"physical-capacity","fullRefusalReport":"only-if-an-already-available-reporting-boundary-can-complete-it","phaseReceiptProduced":false}Outcome details
{
"case": "missing-terminal-backing",
"ordinaryPhaseStarted": false,
"normalReservationsAttempted": false,
"guestReservationAttempted": false,
"completeEmergencySupport": false,
"partialReplyPublished": false,
"diagnosticIdentity": {
"phase": "admission",
"code": "host.envelope"
},
"reason": "physical-capacity",
"fullRefusalReport": "only-if-an-already-available-reporting-boundary-can-complete-it",
"phaseReceiptProduced": false
}{"case":"missing-framing-backing","ordinaryPhaseStarted":false,"normalReservationsAttempted":false,"guestReservationAttempted":false,"completeEmergencySupport":false,"partialReplyPublished":false,"diagnosticIdentity":{"phase":"admission","code":"host.envelope"},"reason":"physical-capacity","fullRefusalReport":"only-if-an-already-available-reporting-boundary-can-complete-it","phaseReceiptProduced":false}Outcome details
{
"case": "missing-framing-backing",
"ordinaryPhaseStarted": false,
"normalReservationsAttempted": false,
"guestReservationAttempted": false,
"completeEmergencySupport": false,
"partialReplyPublished": false,
"diagnosticIdentity": {
"phase": "admission",
"code": "host.envelope"
},
"reason": "physical-capacity",
"fullRefusalReport": "only-if-an-already-available-reporting-boundary-can-complete-it",
"phaseReceiptProduced": false
}{"case":"missing-cursor","ordinaryPhaseStarted":false,"normalReservationsAttempted":false,"guestReservationAttempted":false,"completeEmergencySupport":false,"partialReplyPublished":false,"diagnosticIdentity":{"phase":"admission","code":"host.envelope"},"reason":"physical-capacity","fullRefusalReport":"only-if-an-already-available-reporting-boundary-can-complete-it","phaseReceiptProduced":false}Outcome details
{
"case": "missing-cursor",
"ordinaryPhaseStarted": false,
"normalReservationsAttempted": false,
"guestReservationAttempted": false,
"completeEmergencySupport": false,
"partialReplyPublished": false,
"diagnosticIdentity": {
"phase": "admission",
"code": "host.envelope"
},
"reason": "physical-capacity",
"fullRefusalReport": "only-if-an-already-available-reporting-boundary-can-complete-it",
"phaseReceiptProduced": false
}{"case":"missing-work","ordinaryPhaseStarted":false,"normalReservationsAttempted":false,"guestReservationAttempted":false,"completeEmergencySupport":false,"partialReplyPublished":false,"diagnosticIdentity":{"phase":"admission","code":"host.envelope"},"reason":"physical-capacity","fullRefusalReport":"only-if-an-already-available-reporting-boundary-can-complete-it","phaseReceiptProduced":false}Outcome details
{
"case": "missing-work",
"ordinaryPhaseStarted": false,
"normalReservationsAttempted": false,
"guestReservationAttempted": false,
"completeEmergencySupport": false,
"partialReplyPublished": false,
"diagnosticIdentity": {
"phase": "admission",
"code": "host.envelope"
},
"reason": "physical-capacity",
"fullRefusalReport": "only-if-an-already-available-reporting-boundary-can-complete-it",
"phaseReceiptProduced": false
}{"case":"all-secured","ordinaryPhaseStarted":true,"normalReservationsAttempted":true,"guestReservationAttempted":false,"completeEmergencySupport":true,"partialReplyPublished":false}Outcome details
{
"case": "all-secured",
"ordinaryPhaseStarted": true,
"normalReservationsAttempted": true,
"guestReservationAttempted": false,
"completeEmergencySupport": true,
"partialReplyPublished": false
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"framing": {
"terminalCoreAloneIsCommandResult": false,
"existingReportsTerminalSlot": true,
"sameBytesForCopyOrDirectFraming": true,
"postfailureBackingAcquisition": false,
"postfailureCursorGrowth": false,
"postfailureWorkReservation": false
}
}Product invocation
Expected result
Each row varies one required emergency support component while the other three are fully secured. Ordinary work begins only in the all-secured row. Product invocation awaits its 2.0 adapter.
Each row varies one required emergency support component while the other three are fully secured. Ordinary work begins only in the all-secured row.
The cases use the checked finite bounds, leaving numeric capacities, storage layout, and tariffs with the selected resource model. The diagnosticIdentity and reason fields are a report projection. A complete refusal also carries the selected trusted envelope contract. A previously available reporting boundary delivers the refusal only when it can encode the complete reply. A prebuilt terminal core and direct record framing preserve identical canonical fields and retained data.
Keep status 20 and 21 during later emergency profile reports
lispex.example.v2.resources.emergency-profile-failure-status · rev. 1
{
"notation": "documentation-request",
"operation": "emergency-framing-after-completed-evaluation",
"profileContractInputBytesHex": "6c69737065782e646174756d2f3200d9010808060a646566696e6974696f6e080806126465636c61726174696f6e5f666f726d617406106c69737065782e70726f66696c652f3208080606666f726d617406196c69737065782e70726f66696c652d636f6e74726163742f320808060770726f66696c650604626173650808060d736368656d615f666f726d6174060f6c69737065782e736368656d612f320808060d776f726b5f636f6e747261637406156c69737065782e70726f66696c652d776f726b2f3200080806046b696e64060770726f66696c65080806046e616d650606626173652f3200",
"profileContractIdentityBytesHex": "6c69737065782e646174756d2f320067080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f3200",
"normalOutputBytesDelivered": "0",
"emergencySupport": "terminal backing, complete framing backing, cursor state, and work secured before the later phase",
"requests": [
{
"case": "language-failure-then-qualification",
"completedEvaluationKind": "language-failure",
"completedStatus": 20,
"committedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007008080604636f64650612646f6d61696e2e6170706c69636174696f6e0808060464617461080806046461746106223663363937333730363537383265363436313734373536643266333230303031303108080603746167060273350008080605706861736506086576616c7561746500",
"laterPhase": "qualification",
"laterRefusalDiagnosticBytesHex": "6c69737065782e646174756d2f3200be0108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060d7175616c696669636174696f6e00",
"normalProfileReport": "unfinished because its report reservation was refused",
"retainedOwnerInputs": [
"completed outcome payload and its original receipt",
"every already completed report slot, including standalone evidence",
"trace state and any completed trace bytes"
],
"inputAuthority": "completed typed owner observations bound to the same immutable operation"
},
{
"case": "language-failure-then-evidence",
"completedEvaluationKind": "language-failure",
"completedStatus": 20,
"committedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007008080604636f64650612646f6d61696e2e6170706c69636174696f6e0808060464617461080806046461746106223663363937333730363537383265363436313734373536643266333230303031303108080603746167060273350008080605706861736506086576616c7561746500",
"laterPhase": "evidence",
"laterRefusalDiagnosticBytesHex": "6c69737065782e646174756d2f3200b90108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060865766964656e636500",
"normalProfileReport": "unfinished because its report reservation was refused",
"retainedOwnerInputs": [
"completed outcome payload and its original receipt",
"every already completed report slot, including standalone evidence",
"trace state and any completed trace bytes"
],
"inputAuthority": "completed typed owner observations bound to the same immutable operation"
},
{
"case": "resource-stop-then-qualification",
"completedEvaluationKind": "resource-stop",
"completedStatus": 21,
"committedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007a08080604636f646506127265736f757263652e657868617573746564080806046461746108080604617869730606726573756c74080806056576656e74060e726573756c742d6368616e6e656c080806057374616765060d726573756c742d656e636f64650008080605706861736506086576616c7561746500",
"laterPhase": "qualification",
"laterRefusalDiagnosticBytesHex": "6c69737065782e646174756d2f3200be0108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060d7175616c696669636174696f6e00",
"normalProfileReport": "unfinished because its report reservation was refused",
"retainedOwnerInputs": [
"completed outcome payload and its original receipt",
"every already completed report slot, including standalone evidence",
"trace state and any completed trace bytes"
],
"inputAuthority": "completed typed owner observations bound to the same immutable operation"
},
{
"case": "resource-stop-then-evidence",
"completedEvaluationKind": "resource-stop",
"completedStatus": 21,
"committedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007a08080604636f646506127265736f757263652e657868617573746564080806046461746108080604617869730606726573756c74080806056576656e74060e726573756c742d6368616e6e656c080806057374616765060d726573756c742d656e636f64650008080605706861736506086576616c7561746500",
"laterPhase": "evidence",
"laterRefusalDiagnosticBytesHex": "6c69737065782e646174756d2f3200b90108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060865766964656e636500",
"normalProfileReport": "unfinished because its report reservation was refused",
"retainedOwnerInputs": [
"completed outcome payload and its original receipt",
"every already completed report slot, including standalone evidence",
"trace state and any completed trace bytes"
],
"inputAuthority": "completed typed owner observations bound to the same immutable operation"
}
]
}
{"case":"language-failure-then-qualification","status":20,"completedEvaluationDiagnosticBytesHex":"6c69737065782e646174756d2f32007008080604636f64650612646f6d61696e2e6170706c69636174696f6e0808060464617461080806046461746106223663363937333730363537383265363436313734373536643266333230303031303108080603746167060273350008080605706861736506086576616c7561746500","terminalCauseBytesHex":"6c69737065782e646174756d2f3200be0108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060d7175616c696669636174696f6e00","normalProfileSlotPresent":false,"terminalSlotPresent":true,"completedOutcomeChanged":false,"completedReceiptBytesChanged":false,"completedReportSlotsChanged":false,"standaloneEvidenceSlotChanged":false,"traceStateOrBytesChanged":false,"reparsedReceiptForStatus":false,"newEvaluationReceiptProduced":false,"newGuestReservation":false,"primaryPackets":"1"}Outcome details
{
"case": "language-failure-then-qualification",
"status": 20,
"completedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007008080604636f64650612646f6d61696e2e6170706c69636174696f6e0808060464617461080806046461746106223663363937333730363537383265363436313734373536643266333230303031303108080603746167060273350008080605706861736506086576616c7561746500",
"terminalCauseBytesHex": "6c69737065782e646174756d2f3200be0108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060d7175616c696669636174696f6e00",
"normalProfileSlotPresent": false,
"terminalSlotPresent": true,
"completedOutcomeChanged": false,
"completedReceiptBytesChanged": false,
"completedReportSlotsChanged": false,
"standaloneEvidenceSlotChanged": false,
"traceStateOrBytesChanged": false,
"reparsedReceiptForStatus": false,
"newEvaluationReceiptProduced": false,
"newGuestReservation": false,
"primaryPackets": "1"
}{"case":"language-failure-then-evidence","status":20,"completedEvaluationDiagnosticBytesHex":"6c69737065782e646174756d2f32007008080604636f64650612646f6d61696e2e6170706c69636174696f6e0808060464617461080806046461746106223663363937333730363537383265363436313734373536643266333230303031303108080603746167060273350008080605706861736506086576616c7561746500","terminalCauseBytesHex":"6c69737065782e646174756d2f3200b90108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060865766964656e636500","normalProfileSlotPresent":false,"terminalSlotPresent":true,"completedOutcomeChanged":false,"completedReceiptBytesChanged":false,"completedReportSlotsChanged":false,"standaloneEvidenceSlotChanged":false,"traceStateOrBytesChanged":false,"reparsedReceiptForStatus":false,"newEvaluationReceiptProduced":false,"newGuestReservation":false,"primaryPackets":"1"}Outcome details
{
"case": "language-failure-then-evidence",
"status": 20,
"completedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007008080604636f64650612646f6d61696e2e6170706c69636174696f6e0808060464617461080806046461746106223663363937333730363537383265363436313734373536643266333230303031303108080603746167060273350008080605706861736506086576616c7561746500",
"terminalCauseBytesHex": "6c69737065782e646174756d2f3200b90108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060865766964656e636500",
"normalProfileSlotPresent": false,
"terminalSlotPresent": true,
"completedOutcomeChanged": false,
"completedReceiptBytesChanged": false,
"completedReportSlotsChanged": false,
"standaloneEvidenceSlotChanged": false,
"traceStateOrBytesChanged": false,
"reparsedReceiptForStatus": false,
"newEvaluationReceiptProduced": false,
"newGuestReservation": false,
"primaryPackets": "1"
}{"case":"resource-stop-then-qualification","status":21,"completedEvaluationDiagnosticBytesHex":"6c69737065782e646174756d2f32007a08080604636f646506127265736f757263652e657868617573746564080806046461746108080604617869730606726573756c74080806056576656e74060e726573756c742d6368616e6e656c080806057374616765060d726573756c742d656e636f64650008080605706861736506086576616c7561746500","terminalCauseBytesHex":"6c69737065782e646174756d2f3200be0108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060d7175616c696669636174696f6e00","normalProfileSlotPresent":false,"terminalSlotPresent":true,"completedOutcomeChanged":false,"completedReceiptBytesChanged":false,"completedReportSlotsChanged":false,"standaloneEvidenceSlotChanged":false,"traceStateOrBytesChanged":false,"reparsedReceiptForStatus":false,"newEvaluationReceiptProduced":false,"newGuestReservation":false,"primaryPackets":"1"}Outcome details
{
"case": "resource-stop-then-qualification",
"status": 21,
"completedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007a08080604636f646506127265736f757263652e657868617573746564080806046461746108080604617869730606726573756c74080806056576656e74060e726573756c742d6368616e6e656c080806057374616765060d726573756c742d656e636f64650008080605706861736506086576616c7561746500",
"terminalCauseBytesHex": "6c69737065782e646174756d2f3200be0108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060d7175616c696669636174696f6e00",
"normalProfileSlotPresent": false,
"terminalSlotPresent": true,
"completedOutcomeChanged": false,
"completedReceiptBytesChanged": false,
"completedReportSlotsChanged": false,
"standaloneEvidenceSlotChanged": false,
"traceStateOrBytesChanged": false,
"reparsedReceiptForStatus": false,
"newEvaluationReceiptProduced": false,
"newGuestReservation": false,
"primaryPackets": "1"
}{"case":"resource-stop-then-evidence","status":21,"completedEvaluationDiagnosticBytesHex":"6c69737065782e646174756d2f32007a08080604636f646506127265736f757263652e657868617573746564080806046461746108080604617869730606726573756c74080806056576656e74060e726573756c742d6368616e6e656c080806057374616765060d726573756c742d656e636f64650008080605706861736506086576616c7561746500","terminalCauseBytesHex":"6c69737065782e646174756d2f3200b90108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060865766964656e636500","normalProfileSlotPresent":false,"terminalSlotPresent":true,"completedOutcomeChanged":false,"completedReceiptBytesChanged":false,"completedReportSlotsChanged":false,"standaloneEvidenceSlotChanged":false,"traceStateOrBytesChanged":false,"reparsedReceiptForStatus":false,"newEvaluationReceiptProduced":false,"newGuestReservation":false,"primaryPackets":"1"}Outcome details
{
"case": "resource-stop-then-evidence",
"status": 21,
"completedEvaluationDiagnosticBytesHex": "6c69737065782e646174756d2f32007a08080604636f646506127265736f757263652e657868617573746564080806046461746108080604617869730606726573756c74080806056576656e74060e726573756c742d6368616e6e656c080806057374616765060d726573756c742d656e636f64650008080605706861736506086576616c7561746500",
"terminalCauseBytesHex": "6c69737065782e646174756d2f3200b90108080604636f6465060e70726f66696c652e62756467657408080604646174610808060662756467657406067265706f72740808060770726f66696c65080806066469676573740a20ee922f05c6247a298f4dcabadaf65f819ee3f3f3a9d15abeda3c9ff704056ab108080606646f6d61696e06116c69737065782e636f6e74726163742f3208080606666f726d617406116c69737065782e6964656e746974792f320000080806057068617365060865766964656e636500",
"normalProfileSlotPresent": false,
"terminalSlotPresent": true,
"completedOutcomeChanged": false,
"completedReceiptBytesChanged": false,
"completedReportSlotsChanged": false,
"standaloneEvidenceSlotChanged": false,
"traceStateOrBytesChanged": false,
"reparsedReceiptForStatus": false,
"newEvaluationReceiptProduced": false,
"newGuestReservation": false,
"primaryPackets": "1"
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"phaseBoundary": {
"profileOwnerSuppliesCommittedRefusal": true,
"failedEvaluationRequiresReturnedDatumSchemaTraversal": false,
"framingRevalidatesBindings": false,
"firstRefusalReplacedDuringEmergency": false
}
}Product invocation
Expected result
Four rows combine completed language-failure status 20 or resource-stop status 21 with a later qualification or evidence report-axis refusal. Product invocation awaits its 2.0 adapter.
Four rows combine completed language-failure status 20 or resource-stop status 21 with a later qualification or evidence report-axis refusal.
The supplied diagnostic packets follow the catalog and Datum grammar. The base/2 ContractInput bytes and identity bytes provide a complete SHA-256 recipe through the canonical identity-input record. The language diagnostic has tag s5 and the canonical false packet as data. The resource diagnostic fixes result-encode/result/result-channel. The later diagnostic fixes profile.budget/report in its own phase.
Emergency framing retains the later phase's first refusal. The completed evaluation diagnostic, qualified site, outcome, receipt, and status stay unchanged. This example projects framing over already completed, same-operation typed owner observations. The profile work contract determines which later work runs. The normal profile slot here is unfinished; every previously completed report slot and trace value remains intact. Status selection consumes retained classification without parsing the receipt again.
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.
Why
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
lispex.example.v2.resources.trace-whole-record-boundary · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) (+ input 1)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "short-frame",
"input": {
"kind": "integer",
"value": "41"
},
"traceLimits": "header and footer plus first complete frame minus one octet"
},
{
"case": "exact-frame",
"input": {
"kind": "integer",
"value": "41"
},
"traceLimits": "header and footer plus exactly the first complete frame"
},
{
"case": "measure-work",
"input": {
"kind": "integer",
"value": "41"
},
"traceLimits": "header and footer fit but work refuses the first trace.measure"
},
{
"case": "record-allocation",
"input": {
"kind": "integer",
"value": "41"
},
"traceLimits": "header and footer fit but allocation refuses the first trace.record"
}
]
}
42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"tracePrefixes": [
{
"records": "0",
"footerHex": "0001"
},
{
"records": "1",
"footerHex": "0001"
},
{
"records": "0",
"footerHex": "0001"
},
{
"records": "0",
"footerHex": "0001"
}
],
"reservation": {
"unit": "01 marker plus minimal payload length plus complete event payload",
"partialFrames": false,
"laterRecordsAfterRefusal": false,
"growingCounterAfterRefusal": false
},
"comparison": {
"canonicalOutcomeEqual": true,
"evaluationChargesEqual": true,
"evaluationReceiptEqual": true
}
}Product invocation
Expected result
Every trace retains only complete frames and its reserved saturation footer. Trace capacity, work, and allocation refusals preserve the same evaluation and receipt. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
Keep evaluation when a trace header cannot fit
lispex.example.v2.resources.trace-header-unavailable · rev. 1
(module main
(import)
(export rule)
(entry rule)
(define rule (lambda (input) input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
],
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "Unicode 17.0.0",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient for the selected preparation case",
"evaluate": "finite values selected by each case"
},
"requests": [
{
"case": "not-requested",
"input": {
"kind": "integer",
"value": "42"
},
"trace": false
},
{
"case": "header-refused",
"input": {
"kind": "integer",
"value": "42"
},
"traceLimits": "capacity below the complete header and reserved footer"
}
]
}
42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"trace": [
{
"status": "disabled",
"traceBytesProduced": false
},
{
"status": "unavailable",
"traceBytesProduced": false
}
],
"comparison": {
"semanticRequestEqual": true,
"evaluationChargesEqual": true,
"canonicalOutcomeEqual": true,
"evaluationReceiptEqual": true
}
}Product invocation
Expected result
A trace whose header and footer cannot fit produces no malformed trace bytes. Evaluation keeps the same semantic request and receipt as an untraced run. Product invocation awaits its 2.0 adapter.
Event projections and fixture labels are documentation notation. They select the stated operation within the complete event stream. A product serializes canonical sites and never serializes these labels. Symbolic finite limits come from the selected resource model. These examples remain not-run.
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.
Why
The resource contract must bound the host before allocation or protection fails. Relabeling a host failure would hide an unsupported request.
Reject a result that exceeds its channel
lispex.example.v2.resources.result-channel-stop · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "result channel below the complete canonical encoding size of the returned datum, with every other axis sufficient and emergency reporting space reserved"
},
"requests": [
{
"input": {
"kind": "string",
"value": "result"
}
}
],
"siteNotation": {
"result-encoding": "the first result encoding reservation beyond the result channel budget"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · result-channelOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "result-channel",
"site": {
"fixtureSite": "result-encoding"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"output": {
"successfulResultPrefix": false,
"terminalReportAvailable": true
}
}Product invocation
Expected result
A result encoding reservation exceeds the channel limit before the complete result can be delivered. The request stops without a successful prefix. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Keep a full trace separate from the result
lispex.example.v2.resources.trace-saturation · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(+ input 1)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "41"
}
},
{
"input": {
"kind": "integer",
"value": "41"
}
}
],
"executionContexts": [
"trace disabled",
"trace enabled with finite reserved trace capacity that fills before execution ends"
],
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"comparison": {
"canonicalOutcomeEqual": true,
"evaluationChargesEqual": true,
"traceSaturationChangesGuestControl": false
},
"traceSaturationReported": true
}Product invocation
Expected result
Both executions return 42 with equal evaluation charges. Filling the optional trace does not change guest control or the result. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Compare limits around the complete work charge
lispex.example.v2.resources.work-boundary · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "the work limit stated for each request, with every other axis sufficient"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
},
"workLimit": "Q minus one work unit"
},
{
"input": {
"kind": "integer",
"value": "42"
},
"workLimit": "Q"
},
{
"input": {
"kind": "integer",
"value": "42"
},
"workLimit": "Q plus one work unit"
}
],
"symbolicContract": {
"Q": "the positive total evaluation work required for this complete request under the selected model, including encoding"
},
"siteNotation": {
"final-work-event": "the last positive work reservation of the complete identity request"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · workOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "work",
"site": {
"fixtureSite": "final-work-event"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}42Outcome details
{
"kind": "value",
"valueCount": 1,
"datum": {
"kind": "integer",
"value": "42"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"boundary": {
"exactLimitAccepted": true,
"aboveLimitEffectCommitted": false
}
}Product invocation
Expected result
The request below Q stops at its final work event. Requests at Q and above Q return 42. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Reject an unsupported physical envelope
lispex.example.v2.resources.insufficient-host-envelope · rev. 3
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
input))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "42"
}
}
],
"hostSetup": {
"physicalEnvelope": "insufficient for the requested finite logical limits"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
{"kind":"admission-failure","valueCount":0}Outcome details
{
"kind": "admission-failure",
"valueCount": 0
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"entryEvaluated": false,
"requestedLimitsChanged": false,
"canonicalOutcomeProduced": false,
"evaluationReceiptEligible": false
}Product invocation
Expected result
The host rejects admission before evaluation because it cannot support the requested limits. It does not silently lower them. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Keep a host interruption distinct from resource exhaustion
lispex.example.v2.resources.host-interruption · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(+ input 1)))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "finite values sufficient to prepare this source",
"evaluate": "finite values sufficient for the stated finite calculation"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "41"
}
}
],
"hostSetup": {
"interruption": "external host termination after admission and before an evaluation outcome is available"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
{"kind":"operational-interruption","valueCount":0}Outcome details
{
"kind": "operational-interruption",
"valueCount": 0
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"deterministicResourceOutcome": false
}Product invocation
Expected result
The host interruption produces no language result and is not reported as deterministic resource exhaustion. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.
Preparation and evaluation
The phase separation contract assigns work to preparation and evaluation. Each phase uses its independent resource account. Reused libraries and caches follow the cache-preservation rule.
8.19 Keep preparation and evaluation budgets separate
Preparation and evaluation use independent budgets. Preparation assigns work to the two phases. Reuse follows the cache-preservation rule.
Why
Cache state belongs to the host. It must not change how much evaluation a caller receives under the same limits.
Preserve evaluation work through preparation reuse
lispex.example.v2.resources.cache-budget-stop · rev. 2
(module main
(import)
(export rule)
(entry rule)
(define rule
(lambda (input)
(let loop () (loop))))
)
Request and files
{
"notation": "documentation-request",
"source": "source.scm",
"semantics": {
"language": "Lispex 2.0",
"standardLibrary": "one fixed library identity",
"unicode": "one fixed Unicode semantics version",
"resourceModel": "one fixed finite resource model"
},
"limits": {
"prepare": "independent finite values sufficient on every preparation path",
"evaluate": "one fixed finite work limit sufficient through all earlier events but below a designated positive work reservation at recursive-call, with every other axis sufficient through that stop"
},
"requests": [
{
"input": {
"kind": "integer",
"value": "0"
}
},
{
"input": {
"kind": "integer",
"value": "0"
}
},
{
"input": {
"kind": "integer",
"value": "0"
}
}
],
"executionContexts": [
"cold preparation cache",
"warm preparation cache",
"precompiled standard library"
],
"siteNotation": {
"recursive-call": "the loop call whose work reservation first exceeds the fixed evaluation budget"
},
"rootModule": "main",
"moduleSources": [
{
"name": "main",
"source": "source.scm"
}
]
}
resource-stop · workOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "work",
"site": {
"fixtureSite": "recursive-call"
}
}resource-stop · workOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "work",
"site": {
"fixtureSite": "recursive-call"
}
}resource-stop · workOutcome details
{
"kind": "resource-stop",
"valueCount": 0,
"terminal": true,
"axis": "work",
"site": {
"fixtureSite": "recursive-call"
}
}Specification outcome. Product runs are pending the 2.0 adapter.
Semantic details
{
"comparison": {
"evaluationChargesEqual": true,
"canonicalOutcomeEqual": true,
"exhaustedAxisEqual": true,
"canonicalSiteEqual": true,
"unusedPrepareBudgetTransferred": false
}
}Product invocation
Expected result
All three preparation paths reach the same evaluation work stop at the same canonical loop site. Product invocation awaits its 2.0 adapter.
The request and site labels are documentation notation. Symbolic finite limits come from the selected resource contract. They are not measurements copied from a run.