본문으로 이동
(Lispex)2.0명세 · 출시 전

문서 검색

영어 명세를 검색합니다

질문, 심볼, 진단 코드, 명령을 입력하세요.

차례

명세 검색
리스펙스 2.0 · 언어 · I.8장

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 componentRequired meaning
Event contractsThe supported versioned event catalog and each complete requirement function
Requirement inputsOnly the semantic operands fixed by the event schedules
Units and representationsWork and logical allocation units and exact finite representation bounds
Default axis dataComplete finite axis values before any model identity is attached
Channel and reporting boundsThe declared channel units and complete terminal and framing requirements
Host supportThe 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 recordExact required fields
PrepareLimitsallocation, diagnostic, frames, input, result, work
EvaluationLimitsallocation, 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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    input))
)
요청과 파일
request.json
{
  "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"
    }
  ]
}
명세상 결과
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "resolvedLimits": {
    "prepareFinite": true,
    "evaluateFinite": true,
    "commonPreset": true
  }
}
제품 실행

예상 결과

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 · 3판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    input))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "kind": "admission-failure",
  "valueCount": 0
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "entryEvaluated": false,
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (* input input)))
)
요청과 파일
request.json
{
  "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 · work
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "work",
  "site": {
    "fixtureSite": "multiply-step"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "unmeteredNativeWork": false
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (begin
      (cons input '())
      (cons input '())
      input)))
)
요청과 파일
request.json
{
  "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-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "second-pair"
  }
}
결과resource-stop · logical-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "second-pair"
  }
}
결과resource-stop · logical-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "second-pair"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "comparison": {
    "canonicalOutcomeEqual": true,
    "evaluationChargesEqual": true,
    "allocationRefunded": false
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (let loop ((n input))
      (if (= n 0)
          1
          (loop (- n 1))))))
)
요청과 파일
request.json
{
  "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"
    }
  ]
}
명세상 결과
결과1
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "1"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "frameBehavior": {
    "recursiveTailCallsAddCallFrames": false
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(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.json
{
  "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 · frames
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "frames",
  "site": {
    "fixtureSite": "recursive-count"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "hostStackDeterminesStop": false
}
제품 실행

예상 결과

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 · 1판

lispex · request.json
{
  "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."
}
명세상 결과
예상의미 상세

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (cons input '())))
)
요청과 파일
request.json
{
  "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-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "pair-construction"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "refusedEvent": {
    "effectCommitted": false
  }
}
제품 실행

예상 결과

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.

SubjectOccurrencePath suffix
Explicit call and its shared checksCall nodeEmpty for the call, field(operator) for its operator, argument(i) for an argument
Entry input and resultThe selected entry lambda nodefield(input) or field(output) before the component path
Binding creationBinding recordEmpty
Environment or recursive groupStored Group record when present. Otherwise the owning let, letstar, letrec, namedlet, or lambda nodeThe member position as element(i) when one member is selected
Implicit named let callNamedlet nodefield(initial-call)
Clause test or receiver callClause recordfield(test) or field(receiver)
Rest argument pairThe invoked lambda noderesult(0) followed by element(i) in argument order
Public procedure eventIts invoking call occurrenceThe argument or result path followed by the visited component
Guest library inner callThe inner call in the fixed library graphIts own operator and argument paths
Pair componentThe owning operation occurrencecar before cdr
Vector or internal sequence elementThe owning operation occurrenceelement(i) in the declared order
Text scalar or octetThe owning operation occurrencescalar(i) or byte(i)
Cross-argument checkThe owning operation occurrenceThe first argument selected by that check
ComparisonThe owning operation occurrencefield(compare) followed by the left argument and compared component path
Generated resultThe owning operation occurrenceresult(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 callOccurrence and prefix
Selected entryEntry lambda node, field(entry)
List traversal callbackInvoking call node, field(callback), element(tuple index)
Apply targetInvoking call node, field(target)
Call-with-values producerInvoking call node, field(producer)
Call-with-values consumerInvoking call node, field(consumer)
Named let initial callNamedlet node, field(initial-call)
Clause receiverClause 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.

OperationOrdered scheduleSite
Literal or quoteliteral-value, then expose the immutable valueLiteral node
Name usebinding-read, then fetch the resolved bindingUse node
Lambda expressionclosure-create, then capture its lexical environmentLambda node
Body or explicit beginRun any leading recursive group, then visit expressions in source order. Discard every nonfinal result sequence. Forward the final sequenceChild occurrences. A body wrapper adds no event
Application operandsEvaluate the operator, result-check, argument-sequence, then each argument expression, result-check, argument-storeCall node and its operator or argument path
Application dispatchcallable-check, arity-check, call, then parameter binding and the called operationCall occurrence
Fixed parametersenvironment-create, then binding-initialize in parameter orderLambda node, then parameter bindings
Rest parametersFixed parameter binding, then datum-allocate per rest pair in argument order, then binding-initialize for the rest bindingThe Rest argument pair row in the site table, then the rest binding
Normal call returncall-return, release the active call capacity, and forward the result sequenceThe invoked call occurrence
Tail callThe ordinary operand and dispatch schedule, or the implicit call schedule below. call replaces the current call capacity under the tail-call ruleTail call occurrence
Parallel letEach initializer, result-check, and traversal-state retention from left to right, then environment-create, then binding-initialize in member order, then bodyLet node paths and bindings
Let*Initializer, result-check, environment-create, binding-initialize, then the next nested bindingLetstar node and member path, then its binding
Module definitionEvaluate its non-lambda initializer, then result-check, environment-create, and binding-initialize. No intermediate sequence is retainedThe initializer occurrence, then its stored group with element(0) for result-check, then that group and its declared binding
Recursive groupenvironment-create, each closure-create, then each binding-initialize, all in member order, then bodyStored group or letrec node, then lambda nodes and bindings
Named letEach 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 valuesNamedlet node and its loop and parameter bindings
IfTest, result-check, branch-select, then only the selected childIf node and test path
And or orEach nonfinal operand, result-check, branch-select until selected. Forward the final operand sequence if reached. An empty form uses one branch-selectForm node and operand path
Cond clauseTest, result-check, branch-select, then its selected body, test value, or receiver scheduleClause record
Default clausebranch-select, then its body. No test or synthetic result-checkDefault clause record
Clause receiverReceiver expression, result-check, then the ordinary call checks with the saved test as its argumentClause receiver path
Guardguard-enter, protected body, then guard-leave on normal return. A final body call completes call-return before guard-leaveGuard node
Caught occurrenceDiscard frames above the handling guard without call-return and release their frame capacity. guard-bind, deactivate the guard, then the declared clause scheduleGuard binding and clause records
Unmatched guardguard-propagate with the original occurrence and siteGuard node. The propagated failure site is unchanged
Module initializationFixed library prefix, then every source module in dependency order. Use Module definition for a non-lambda definition and Recursive group for a lambda groupModule, 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.

EventReservation pointRepetition and site
argument-checkBefore starting an argument domain or a prescribed value constraintArgument order. Finish that domain's nested traversal before the next argument
list-stepBefore inspecting a pair spine position, selected component, or final tailA 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-stepBefore inspecting a stored length, selected element, or required sequence endEach declared length, element, or end visit in the row order. Stored length uses field(length)
datum-validateBefore classifying the next portable-data componentDepth-first, pair car before cdr, vector elements in ascending index order
compare-scalarBefore comparing the selected scalar pair or sequence endsAdjacent pair order and the declared left-before-right position order
compare-datumBefore comparing the current pair of Datum nodesPreorder with car before cdr and ascending vector elements
exact-arithmeticBefore the next result in the declared arithmetic reductionEach left reduction step. Unary operations have their single declared step
rational-reduceBefore reducing the declared exact resultImmediately after the arithmetic stage that requires it
decimal-scaleBefore forming the exact grid stepThe rounding call
exact-divideBefore forming its declared quotient and remainder or adjacent candidatesThe numeric call or current reduction step
rounding-selectBefore choosing the rounded integer or detecting a required rounding failureThe rounding call after scale and division
text-scalar-scanBefore inspecting the next scalar or required sequence endThe exact pass and scalar order in the string or Values Rule
unicode-mapBefore the property query or case mappingOriginal scalar order after the required input scan. Original text determines contextual mappings
unicode-normalizeBefore the complete declared normalization of one validated stringArgument order after its complete scalar scan
traversal-stateBefore creating or advancing the declared logical cursor or internal value sequenceList argument order and the stated element order for traversal. A constructor uses its declared result index order
callback-callBefore beginning the ordinary call protocol for the selected callbackThe implicit call occurrence and prefix from the site table. Guest body events retain their own occurrences
result-checkBefore checking a required callback result countCallback call occurrence and tuple index
datum-allocateBefore creating the declared immutable result or aggregate componentThe row's result order. Reuse and interning retain every event
condition-constructBefore creating the fully validated Condition and canonical field recordConstructor call after every required field check
condition-inspectBefore reading a requested immutable fieldAccessor call and field(code), field(phase), or field(data)
condition-raiseBefore creating the explicit raised occurrenceRaise 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.

OperationOrdered expansionStop rule
equal?Left argument-check with all left datum-validate visits, right argument-check with all right visits, then compare-datum visitsNo comparison before both complete validations
eq?, eqv?Left scalar argument-check, right scalar argument-check, then the scalar comparison scheduleA procedure or Condition is a domain failure before comparison
Datum comparisoncompare-datum at current nodes, then compare-scalar for scalar contents or sequence lengths, then child comparisonsStop at the first unequal component
String Datum contentsEach position has left and right text-scalar-scan, then compare-scalarStop at first mismatch or sequence end
Bytevector Datum contentsLeft and right sequence-step, then compare-scalar per byteStop at first mismatch or sequence end
Proper-list domainargument-check, then list-step at every pair and the final tailNo element validation or callback before the whole spine succeeds
Datum, character, or octet list domainComplete spine, then required element checks from the headEach element completes before advancing
Association-list domainComplete spine, then each entry pair check and complete key Datum validationAll entries finish before search
Multiple-list callbacksProcedure check, complete list domains in argument order, argument-check per length comparison, arity-check for callbackThe callback arity check runs even for empty lists
Ascending callback loopPer tuple traversal-state, callback-call, required result-check, then any selected result datum-allocateAllocation precedes the next callback
Fold-righttraversal-state for the complete logical state in list argument and ascending index order, then descending callbacks and result checksNo callback before state reservation succeeds
For-eachPer tuple traversal-state, callback-call, discard the returned sequenceNo single-value check is added
ApplyComplete final-list validation, then its selected list-step and traversal-state steps to assemble arguments, then arity-check and callback-callNo body before final-list and target-arity success
Call-with-valuesProducer arity-check, producer callback-call, traversal-state for the returned sequence, consumer arity-check, consumer callback-callPreserve every producer result in order
Valuestraversal-state for its complete returned sequenceZero and multiple values remain internal values
Make-conditionCode 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-constructEvery 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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (equal? (cons 0 (lambda (x) x)) (cons 1 (lambda (x) x)))))
)
요청과 파일
request.json
{
  "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.equality
결과 상세
{
  "kind": "language-failure",
  "condition": {
    "phase": "evaluate",
    "code": "domain.equality",
    "data": {
      "operation": "equal?",
      "operand": "0",
      "path": [
        {
          "kind": "cdr"
        }
      ],
      "actual": "procedure"
    }
  }
}
결과resource-stop · work
결과 상세
{
  "kind": "resource-stop",
  "terminal": true,
  "axis": "work",
  "event": "datum-validate",
  "site": {
    "fixtureSite": "equal-call",
    "role": "datum-validate",
    "path": [
      {
        "kind": "argument",
        "index": "0"
      },
      {
        "kind": "cdr"
      }
    ]
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "operationProjection": {
    "leftValidationOrder": [
      "root",
      "car",
      "cdr"
    ],
    "rightValidationStarted": false,
    "comparisonStarted": false
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (map (lambda (x) (car '())) (cons 1 2))))
)
요청과 파일
request.json
{
  "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.type
결과 상세
{
  "kind": "language-failure",
  "condition": {
    "phase": "evaluate",
    "code": "domain.type",
    "data": {
      "operation": "map",
      "argument": "1",
      "path": [
        {
          "kind": "cdr"
        }
      ],
      "expected": "proper-list",
      "actual": "integer"
    }
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "operationProjection": {
    "listVisits": [
      "pair",
      "final-tail"
    ],
    "callbackArityChecked": false,
    "callbackCalled": false,
    "laterAllocation": false
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (map (lambda (x) (values x x)) '(1 2))))
)
요청과 파일
request.json
{
  "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-count
결과 상세
{
  "kind": "language-failure",
  "condition": {
    "phase": "evaluate",
    "code": "runtime.value-count",
    "data": {
      "expected": "1",
      "actual": "2"
    }
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "operationProjection": {
    "tupleOrder": [
      "0"
    ],
    "afterCallback": [
      "result-check",
      "diagnostic-payload"
    ],
    "resultPairAllocated": false,
    "nextCallbackCalled": false
  }
}
제품 실행

예상 결과

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.

StageOrdered eventsLocation
Bundle admissionprepare.bundle-order, then prepare.bundle-check for duplicates in canonical name order, then the root checkSelected decoded name. The root check selects the submitted root name
Fixed libraryIts required prepared validation events before any source front endThe fixed library operand and its wire or record position
Source captureprepare.capture-source before retaining each immutable module spanModule name and the entire submitted span
Decodeprepare.decode-step per next scalar attempt and final end checkModule name and starting byte offset
Readprepare.read-step, prepare.read-enter, and prepare.read-node in the adopted reader orderModule name and decoded scalar offset. A completed datum uses its opening offset
Normalizeprepare.normalize-node before each visited formModule name and the form's reader-tree path
Module clausesprepare.module-check before each wrapper, name, import, export, and entry syntax checkModule name and selected clause or field path
Binding prechecksprepare.binding-check before the envelope and each prescribed member check, then prepare.binding-publish per memberGroup reader-tree path and member index
Missing importsprepare.dependency-check per import in canonical module and clause orderImport spec reader-tree path
Cycle traversalprepare.cycle-enter once per visited module, then prepare.cycle-edge per dependency edge in canonical orderModule name and selected dependency name
Resolutionprepare.resolve-import, prepare.resolve-use, prepare.resolve-export, then prepare.entry-check in the adopted resolution orderSelected import, use, export, or entry reader-tree path
Canonical recordsprepare.record before each module, binding, node, group, or clause in the canonical construction orderIts canonical table kind and index
Fresh verificationThe structural, scope, event-role, identity, and seal steps of prepared validationThe 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 eventReservation placementLocation
prepared.capture-inputBefore immutable capture and any validation readThe complete submitted prepared byte span
prepared.read-headerBefore each header octet attemptWire offset, including a missing octet position
prepared.begin-recordBefore each compound record, list header, and list itemOpening wire offset and schema field path
prepared.read-fieldBefore each later octet attempt and final end checkWire offset
prepared.check-recordBefore each ordered record, count, kind, canonical-position, child, tail, or site checkRecord kind, index, and checked field
prepared.check-referenceBefore each declared reference or reconstructed lexical use checkRecord kind, index, and checked field
prepared.check-identityBefore each required dependency or semantics check and optional requested program identity checkHeader or dependency field
prepared.seal-handleBefore creating the complete immutable verified handleWhole verified program
prepared.write-headerBefore each canonical output header octetOutput wire offset
prepared.write-fieldBefore each remaining canonical output octetOutput 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.

StageOrdered eventsLocation
Capturegraph.capture-input before retaining the immutable packetComplete graph or source-map span
Framinggraph.begin-record at the exact outer boundaries below. graph.read-header per outer magic and version octet. graph.read-field per outer field octet attemptWire offset and schema field path
Local canonical checksgraph.check-record after each decoded count, tag, or field, then at exact end of inputSelected field or final wire offset
Embedded resolved payloadExisting prepared capture and decoding events, followed at the graph validation stage by prepared record, reference, site, and identity checksEmbedded payload coordinates and records
Outer identitygraph.check-identity after embedded validationOuter program identity field
Source-map reconstructiongraph.check-identity for source identity, then the ordinary source and preparation events for the captured bundleSource identity field, then exact module source coordinates
Map comparisongraph.map-check once per expected mapping against the next supplied row in canonical site order, then one final end-of-mappings checkMapping record and selected site
Projectiongraph.project before each canonical prepared compound record in resolved/1 wire orderIts original canonical occurrence and relation path
Output sizingOne graph.size-record before sizing the complete GraphBytes or SourceMapBytes packetOutput record path
Output reservationresult-channel for the complete GraphBytes or SourceMapBytes packet, then codec-allocation for its bufferWhole output packet
Output encodinggraph.write-byte before each output octet in grammar orderOutput 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 boundaryExact occurrence
GraphBytesOnce after capture and before its first header octet
SourceMapBytesOnce after capture and before its first header octet
Mappings collectionOnce before its count
Mapping itemOnce per item before its first Site count
Mapping compound recordOnce 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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (let ((x (car '())) (x 2)) x)))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "kind": "preparation-resource-stop",
  "phase": "prepare",
  "stage": "normalize",
  "axis": "work",
  "event": "prepare.binding-check",
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "kind": "preparation-resource-stop",
  "event": "prepared.capture-input",
  "axis": "allocation",
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
결과{"kind":"prepared-handle","immutable":true,"canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}
결과 상세
{
  "kind": "prepared-handle",
  "immutable": true,
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "operationProjection": {
    "refusedCaptureReads": [],
    "acceptedCaptureFirstRead": "prepared.read-header",
    "validatedAndSealedSnapshotEqual": true,
    "callerCopyChangesHandle": false
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "kind": "preparation-resource-stop",
  "phase": "prepare",
  "stage": "prepare",
  "axis": "result",
  "event": "result-channel",
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "operationProjection": {
    "projectionCompleted": true,
    "outputSized": true,
    "outputOctets": "0",
    "entryEvaluated": false,
    "existingHandleChanged": false
  }
}
제품 실행

예상 결과

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.

OperationOrdered eventsAccount and location
Transport captureingress.capture-input before acquiring an immutable bounded spanTrusted ingress account and operand span
Request record parseingress.read-byte before each octet attempt, then ingress.check-field at each completed fieldTrusted ingress account and wire offset or field path
Request record constructioningress.materialize before retaining each validated record or sequence itemTrusted ingress account and record path
Limits and dependency selectioningress.check-field before validating each field in the interface grammar orderThe submitted record field. Trusted defaults remain external to that record
Native value convenience callThe same record validation and immutable capture requirementsIts 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 operationOrdered eventsAccount
Count a report, artifact wrapper, or command envelopeegress.measure before each record and field sizing stepTrusted EgressLimits
Retain the complete output spanegress.reserve-output for the measured complete span, then physical output allocationTrusted EgressLimits
Encode its bytesegress.write-byte per octetTrusted EgressLimits
Publish a completed spanegress.publishTrusted 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.

OperationOrdered eventsSite suffix
Packet opencodec-frame before any magic read or encoding size passfield(open)
Magiccodec-byte before each octet read, then its fixed magic checkbyte(i)
Integer or length fieldcodec-byte per digit, then codec-integer before canonical interpretation and the required span or count checkSchema field path and digit offset
Packet boundarycodec-frame before comparing payload length with the remaining captured spanfield(boundary)
Value decodecodec-value before the next tag, then its codec-byte and fields in grammar orderDatum component path
Text decodecodec-scalar before each scalar attempt, then codec-byte per consumed octet and scalar validationScalar start and byte offsets
Bytevector decodecodec-byte per payload octet after its checked lengthbyte(i)
Rational validationcodec-rational-check for denominator, numerator, then reduction after their integer fieldsfield(denominator), field(numerator), field(reduction)
Packet closecodec-frame before the exact root-end checkfield(close)
Decoded Datum materializationcodec-allocation per Datum node in depth-first car, cdr, and element orderDatum component path
Host record orderrecord-order for the complete finite name collectionWhole record path
Host record keysrecord-key per name in canonical UTF-8 orderfield(key) and canonical field index
Host record valuesrecord-field, recursively convert the value, then codec-allocation for its association dataCanonical field index and value path
Input acceptancerequest-seal after canonical validation and materializationSelected entry input boundary
Entry result countresult-check after entry and its guards have returnedSelected entry output boundary
Result Datum validationdatum-validate for the complete result in depth-first orderSelected entry output component path
Encoding size passcodec-value per node, codec-integer per numeric or value length field, codec-scalar per text scalar, then codec-integer for the completed payload lengthOutput component and field path, then field(frame-length)
Result packet reservationresult-channel, then codec-allocation for the complete encoded bufferfield(packet)
Packet emissioncodec-byte per output octet in grammar order, then codec-frame at completionOutput 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.

SituationOrdered actionResult
Check detects a source, admission, language, or boundary failureStop ordinary events, then attempt diagnostic-payloadCommit that detected failure only if its payload reservation succeeds
Automatic guest ConditionThe successful diagnostic-payload constructs its typed fields, Condition, and raised occurrenceNo second condition-construct charge for the same automatic payload
Explicit make-conditionIts field checks, then condition-constructAn immutable Condition with no raised occurrence
Explicit raisecondition-raise, then diagnostic-payload, then commit the new occurrenceThe current raise site supplies its failure location
Payload reservation refusedCommit the refusal at diagnostic-payloadNo truncated original Condition and no guest recovery
Resource reservation refusedCommit its axis, event, and site in the reserved emergency areaDo not attempt another diagnostic-payload reservation
Already committed first failurePreserve it during trace, presentation, and transportA 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 familyResourceStage
Source capture and prepare.decode-stepdecode
prepare.read-step, prepare.read-enter, prepare.read-noderead
Source normalization, module form checks, binding prechecks and publishingnormalize
Dependency, cycle, import, name-use, and export resolutionresolve
Bundle names, fixed library validation, entry checks, canonical record construction, every prepared event, and graph capture, validation, projection, and exportprepare
Canonical input decoding, materialization, and request-sealinput-decode
Module initialization, ordinary evaluation, library operations, and entry invocationentry
External result count and complete Datum validationresult-check
Output codec size pass, result-channel, packet allocation, and output emissionresult-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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "kind": "admission-failure",
  "phase": "admission",
  "code": "input.resource",
  "axis": "work",
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "accounting": {
    "chargedAccount": "evaluate",
    "identityCreated": false,
    "accountReset": false,
    "entryEvaluated": false,
    "canonicalOutcomeProduced": false,
    "evaluationReceiptEligible": false
  },
  "inputHex": "6c69737065782e646174756d2f32000100"
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (guard (c (else 7)) (car '()))))
)
요청과 파일
request.json
{
  "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"
    }
  ]
}
명세상 결과
결과7
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}
결과resource-stop · diagnostic
결과 상세
{
  "kind": "resource-stop",
  "terminal": true,
  "axis": "diagnostic",
  "event": "diagnostic-payload",
  "site": {
    "fixtureSite": "car-call",
    "role": "diagnostic-payload",
    "path": [
      {
        "kind": "argument",
        "index": "0"
      }
    ]
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "failureCommit": {
    "successfulPayloadRunsGuard": true,
    "refusedPayloadRunsGuard": false,
    "partialConditionPublished": false,
    "terminalUsesAnotherDiagnosticReservation": false
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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 · result
결과 상세
{
  "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"
      }
    ]
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "operationProjection": {
    "order": [
      "result-check",
      "datum-validate",
      "codec-frame",
      "codec-value",
      "codec-integer",
      "codec-scalar",
      "codec-integer",
      "result-channel"
    ],
    "codecAllocationForOutput": false,
    "emittedResultOctets": "0",
    "successfulResultPrefix": false
  }
}
제품 실행

예상 결과

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 · 1판

lispex · request.json
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "case": "physical-output-refusal",
  "kind": "host-failure",
  "diagnosticIdentity": {
    "phase": "host",
    "code": "host.interrupted"
  },
  "reason": "physical-exhaustion",
  "stage": "render",
  "completedDataPreserved": true
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
    }
  ]
}
제품 실행

예상 결과

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 · 3판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (* input input)))
)
요청과 파일
request.json
{
  "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.type
결과 상세
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "phase": "evaluate",
    "code": "domain.type",
    "data": {
      "operation": "*",
      "argument": "0",
      "path": [],
      "expected": "number",
      "actual": "symbol"
    }
  }
}
조건domain.type
결과 상세
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "phase": "evaluate",
    "code": "domain.type",
    "data": {
      "operation": "*",
      "argument": "0",
      "path": [],
      "expected": "number",
      "actual": "symbol"
    }
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "laterArithmeticEventEntered": false,
  "comparison": {
    "canonicalOutcomeEqual": true,
    "canonicalFailureSiteEqual": true
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (list (cons input '()) (cons input '()))))
)
요청과 파일
request.json
{
  "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-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "second-pair"
  }
}
결과resource-stop · logical-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "second-pair"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "comparison": {
    "firstFailureEqual": true,
    "exhaustedAxisEqual": true,
    "canonicalSiteEqual": true,
    "evaluationChargesEqual": true
  }
}
제품 실행

예상 결과

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 · 3판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (cons input '())))
)
요청과 파일
request.json
{
  "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 · work
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "work",
  "site": {
    "fixtureSite": "pair-construction"
  }
}
결과resource-stop · logical-allocation
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "logical-allocation",
  "site": {
    "fixtureSite": "pair-construction"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "reservation": {
    "refusedEventChargesCommitted": false,
    "refusedEventEffectCommitted": false,
    "priorCommittedChargesPreserved": true
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define saved 7)
  (define rule (lambda (input) saved)))
요청과 파일
request.json
{
  "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."
  }
}
명세상 결과
결과7
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      ((lambda (head . rest) rest) 10 20 30))))
요청과 파일
request.json
{
  "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)
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "list",
    "items": [
      {
        "kind": "integer",
        "value": "20"
      },
      {
        "kind": "integer",
        "value": "30"
      }
    ]
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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"
          }
        ]
      }
    ]
  }
}
제품 실행

예상 결과

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 channelCounted octetsReservation
Preparation input from sourceEach exact submitted module source spanprepare.capture-source
Preparation input from prepared bytesThe complete selected resolved/1 or bytecode/1 payloadprepared.capture-input
Preparation input from graph or mapThe complete GraphBytes or SourceMapBytes packetgraph.capture-input
Preparation result from program exportThe selected canonical resolved/1 or bytecode/1 payloadresult-channel before the first prepared write
Preparation result from graph or map exportThe complete GraphBytes or SourceMapBytes packetresult-channel before the first graph write
Evaluation inputOne complete canonical lispex.datum/2 packetcodec-byte for each consumed octet
Evaluation resultOne complete canonical lispex.datum/2 packetresult-channel after sizing and before output buffer allocation
Preparation or evaluation diagnosticComplete DiagnosticPayloadBytes for the selected typed diagnosticdiagnostic-payload before the failure commits
Profile host input adaptationIts canonical host conversion and encoding work under the profile host contractrecord and codec events assigned to that host account
Host transport inputThe exact selected ABI or command operand frameTrusted IngressLimits
Host transport outputThe complete report, command, or artifact wrapper spanTrusted EgressLimits
Optional traceIts complete header, record frames, and footerThe 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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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 · result
결과 상세
{
  "kind": "resource-stop",
  "axis": "result",
  "event": "result-channel",
  "terminal": true
}
결과"é"
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "string",
    "value": "é"
  }
}
결과"é"
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "string",
    "value": "é"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "packet": {
    "hex": "6c69737065782e646174756d2f3200040602c3a9",
    "octets": "20",
    "textScalars": "1"
  },
  "boundary": {
    "N": "complete canonical packet octet count",
    "exactLimitAccepted": true,
    "belowLimitResultOctets": "0",
    "successfulPacketsEqual": true
  }
}
제품 실행

예상 결과

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 orderTypeMeaning
causeBytevectorComplete DiagnosticPayloadBytes for the committed first cause
formatStringExactly lispex.terminal/1
locationTerminalLocationThe exact source, wire, or canonical location below
programFalse or bytevectorVerified IdentityBytes for ProgramIdentity when known
requestFalse or bytevectorAccepted 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 kindExact fields in wire key orderField types
nonekindString none
programkind, siteString program and a bytevector containing exact CanonicalSiteBytes
sourcekind, module, offsetString source, the decoded module name string, and NatText for the exact event target octet fixed below
wirekind, offset, operandString 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 eventExact source offset
prepare.capture-sourceZero
prepare.decode-stepThe initial octet of the next scalar attempt, or source byte length for the final end check
prepare.read-stepThe initial octet of the next decoded scalar, or source byte length for the final end check
prepare.read-enterThe initial octet of the opening marker
prepare.read-nodeThe initial octet of the completed token, datum, or abbreviation
prepare.normalize-nodeThe initial octet of the selected form
Group envelope or member shapeThe initial octet of that group or member form
Binding identifier, duplicate, or publish checkThe initial octet of the selected name-position datum. A duplicate selects the later declaration
Recursive lambda-head checkThe initial octet of the selected initializer
Clause or member envelope checkThe opening octet of that clause or member form
Import module target or cycle-closing edgeThe initial octet of that import module identifier
Imported public nameThe initial octet of that imported name identifier
Local import alias checkThe initial octet of that local alias identifier
Export local-name or public-name checkThe initial octet of the specific local or public identifier being checked
Entry target checkThe initial octet of the declared entry identifier
Missing root entryThe initial octet of the root module form
Resolved name useThe 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 checkedInputOperand and offset base
Outer HostRequestBytesrequest, first request packet octet
Selected SourceBundleBytesbundle, first bundle packet octet
Selected PreparedArtifactBytes or evaluator artifactartifact, first artifact packet octet
Selected GraphBytes or SourceMapBytesgraph, first graph or map packet octet
Selected canonical Datum input packetinput, first Datum packet octet
Separately submitted limits, profile, receipt, evidence, or trust operandIts 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.

BoundRequired coverage
IdentityBoundEvery identity that can appear in the selected interface and report contracts
LocationBoundEvery canonical site, source coordinate, and wire coordinate allowed by the admitted program, input, and limits
DiagnosticBoundThe complete committed diagnostic payload allowed by that phase's diagnostic limit, plus the closed resource and host refusal forms
EmergencyTerminalBoundThe maximum canonical packet size of the exact terminal schema for those bounded fields
EmergencyFramingBoundThe complete enclosing report and command framing for that terminal payload
EmergencyCursorBoundFinite traversal and continuation state for every record and field in the terminal and its complete surrounding framing
EmergencyWorkBoundFinite 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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) (* input input)))
)
요청과 파일
request.json
{
  "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 · work
결과 상세
{
  "kind": "resource-stop",
  "phase": "evaluate",
  "code": "resource.exhausted",
  "stage": "entry",
  "axis": "work",
  "event": "exact-arithmetic",
  "terminal": true
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "kind": "admission-failure",
  "phase": "admission",
  "code": "input.resource",
  "axis": "input",
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (raise (make-condition "domain.application"
        (list (cons "tag" "é") (cons "data" input))))))
)
요청과 파일
request.json
{
  "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.application
결과 상세
{
  "kind": "language-failure",
  "condition": {
    "phase": "evaluate",
    "code": "domain.application",
    "data": {
      "tag": "é",
      "data": "6c69737065782e646174756d2f3200040602c3a9"
    }
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
  }
}
제품 실행

예상 결과

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 · 1판

lispex · request.json
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "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}
결과 상세
{
  "case": "all-secured",
  "ordinaryPhaseStarted": true,
  "normalReservationsAttempted": true,
  "guestReservationAttempted": false,
  "completeEmergencySupport": true,
  "partialReplyPublished": false
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "framing": {
    "terminalCoreAloneIsCommandResult": false,
    "existingReportsTerminalSlot": true,
    "sameBytesForCopyOrDirectFraming": true,
    "postfailureBackingAcquisition": false,
    "postfailureCursorGrowth": false,
    "postfailureWorkReservation": false
  }
}
제품 실행

예상 결과

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 · 1판

lispex · request.json
{
  "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"}
결과 상세
{
  "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"}
결과 상세
{
  "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"}
결과 상세
{
  "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"}
결과 상세
{
  "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"
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "phaseBoundary": {
    "profileOwnerSuppliesCommittedRefusal": true,
    "failedEvaluationRequiresReturnedDatumSchemaTraversal": false,
    "framingRevalidatesBindings": false,
    "firstRefusalReplacedDuringEmergency": false
  }
}
제품 실행

예상 결과

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 reservationReserved work and storageCapacity unit
trace.openBounded header metadata, identities, encoder state, and final footerComplete header and two-octet footer
trace.measureBounded inspection of the next event's existing metadata and exact frame-length calculationNo stored frame
trace.recordEncoding and retaining the complete measured frameThe 01 marker, its minimal length prefix, and the entire event payload
trace.closeWork already reserved by trace.open for writing the selected footerThe 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 statusExact condition
disabledTraceOptions is false
unavailabletrace.open cannot reserve the complete header and footer
completeA produced TraceBytes ends with 00 00
capacity-exhaustedA produced TraceBytes ends with 00 01 after any trace work, allocation, or capacity refusal
host-interruptedA 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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) (+ input 1)))
)
요청과 파일
request.json
{
  "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"
    }
  ]
}
명세상 결과
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "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
  }
}
제품 실행

예상 결과

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 · 1판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input))
)
요청과 파일
request.json
{
  "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"
    }
  ]
}
명세상 결과
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "trace": [
    {
      "status": "disabled",
      "traceBytesProduced": false
    },
    {
      "status": "unavailable",
      "traceBytesProduced": false
    }
  ],
  "comparison": {
    "semanticRequestEqual": true,
    "evaluationChargesEqual": true,
    "canonicalOutcomeEqual": true,
    "evaluationReceiptEqual": true
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    input))
)
요청과 파일
request.json
{
  "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-channel
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "result-channel",
  "site": {
    "fixtureSite": "result-encoding"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "output": {
    "successfulResultPrefix": false,
    "terminalReportAvailable": true
  }
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (+ input 1)))
)
요청과 파일
request.json
{
  "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"
    }
  ]
}
명세상 결과
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "comparison": {
    "canonicalOutcomeEqual": true,
    "evaluationChargesEqual": true,
    "traceSaturationChangesGuestControl": false
  },
  "traceSaturationReported": true
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    input))
)
요청과 파일
request.json
{
  "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 · work
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "work",
  "site": {
    "fixtureSite": "final-work-event"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
결과42
결과 상세
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "boundary": {
    "exactLimitAccepted": true,
    "aboveLimitEffectCommitted": false
  }
}
제품 실행

예상 결과

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 · 3판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    input))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "kind": "admission-failure",
  "valueCount": 0
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "entryEvaluated": false,
  "requestedLimitsChanged": false,
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (+ input 1)))
)
요청과 파일
request.json
{
  "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}
결과 상세
{
  "kind": "operational-interruption",
  "valueCount": 0
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "deterministicResourceOutcome": false
}
제품 실행

예상 결과

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 · 2판

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
(define rule
  (lambda (input)
    (let loop () (loop))))
)
요청과 파일
request.json
{
  "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 · work
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "work",
  "site": {
    "fixtureSite": "recursive-call"
  }
}
결과resource-stop · work
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "work",
  "site": {
    "fixtureSite": "recursive-call"
  }
}
결과resource-stop · work
결과 상세
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true,
  "axis": "work",
  "site": {
    "fixtureSite": "recursive-call"
  }
}

명세상 결과입니다. 2.0 어댑터가 준비되면 제품에서 실행합니다.

의미 상세
{
  "comparison": {
    "evaluationChargesEqual": true,
    "canonicalOutcomeEqual": true,
    "exhaustedAxisEqual": true,
    "canonicalSiteEqual": true,
    "unusedPrepareBudgetTransferred": false
  }
}
제품 실행

예상 결과

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.

Related chapters

Sandbox contract

Conditions

Preparation and modules

Identity, receipt, replay