Skip to content
(Lispex)2.0Specification · not released

Search documentation

Searches the English specification

Enter a question, symbol, diagnostic code, or command.

Contents

Search the specification
Lispex 2.0 · Tools · IV.13

IV.13

Meaning graph

Inspect resolved bindings, control flow, source locations, and recorded execution paths while preserving the rule outcome.

Scope

Use a meaning graph to inspect how a prepared rule binds names and selects work. A meaning graph is a read-only projection of the resolved program.

A source map connects a canonical program site to its location in the submitted source. A trace records the path taken by one execution within a separately reserved finite capacity.

Evaluation and bindings defines lexical binding and evaluation order. Identity, receipt, replay defines the records used to compare executions.

See Concrete entry declaration and admission, Module grammar and initialization, Concrete command forms.

Resolved bindings

The graph starts with the resolved program produced by preparation. It follows lexical binding references through the closed module bundle. A shared spelling can therefore refer to different bindings.

Inspecting the graph reveals how the rule uses its input. The calling application evaluates the rule through the same semantic request.

13.1 Project resolved bindings

A meaning graph projects the prepared resolved program. Every displayed name use retains its resolved binding and source anchor. Reading the graph leaves the program unchanged.

Why

Readers need to distinguish bindings that share a spelling. Using resolved bindings connects each use to the declaration that evaluation actually selects.

Follow a shadowed name

lispex.example.v2.meaning-graph.shadowed-binding · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (item)
      (let ((original item))
        (let ((item 7))
          (+ original item))))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "3"
      },
      "observation": {
        "graph": "resolved-projection"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Result10
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "10"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "projection": {
    "bindingUses": [
      {
        "use": "original initializer",
        "binding": "entry parameter item"
      },
      {
        "use": "left addition argument",
        "binding": "original binding"
      },
      {
        "use": "right addition argument",
        "binding": "inner item binding"
      }
    ],
    "sourceAnchorsRetained": true,
    "programChangedByInspection": false
  }
}
Product invocation

Expected result

Input 3 produces the exact integer 10. The graph resolves the two uses of item to their different lexical bindings. Product invocation awaits its 2.0 adapter.

The parameter item supplies 3. The inner binding named item supplies 7. The graph preserves that distinction. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Branches and dataflow

Data dependencies show which values an operation consumes. Branch edges show alternatives. Call relations retain the resolved operator expression and its argument dependencies. Recursive relationships remain visible.

A static graph retains both arms of a conditional. A trace can identify the selected arm for a specific input. Evaluation and bindings determines which operations run and in what order.

13.2 Preserve dependencies and control flow

The graph preserves data dependencies, conditional branches, procedure calls, and recursive calls. Evaluation follows the language order and selects the same branch when the graph is displayed.

Why

A reader needs to see both the available paths and the path a request takes. Keeping the graph separate from execution prevents a view from scheduling extra work.

Inspect both branches and execute one

lispex.example.v2.meaning-graph.chosen-branch · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (flag)
      (if flag
          42
          (car '())))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "boolean",
        "value": true
      },
      "observation": {
        "graph": "resolved-projection",
        "trace": "on",
        "reservation": "separate finite capacity sufficient for the complete execution trace"
      }
    },
    {
      "input": {
        "kind": "boolean",
        "value": false
      },
      "observation": {
        "graph": "resolved-projection",
        "trace": "on",
        "reservation": "separate finite capacity sufficient for the complete execution trace"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Result42
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "projection": {
    "branches": [
      "then arm returning 42",
      "else arm calling car"
    ],
    "testDependsOn": "entry parameter flag",
    "bothBranchesRetained": true
  },
  "paths": [
    {
      "input": true,
      "selectedBranch": "then",
      "unselectedBranchEvaluated": false
    },
    {
      "input": false,
      "selectedBranch": "else",
      "unselectedBranchEvaluated": false
    }
  ]
}
Product invocation

Expected result

True produces the exact integer 42. False produces a car domain failure. The graph retains both branches and each trace follows only its selected branch. Product invocation awaits its 2.0 adapter.

A static branch remains visible even when a particular input does not select it. The traces describe the two separate evaluations. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Follow a recursive tail call

lispex.example.v2.meaning-graph.recursive-call · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (count)
      (let loop ((n count) (total 0))
        (if (= n 0)
            total
            (loop (- n 1) (+ total n)))))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "3"
      },
      "observation": {
        "graph": "resolved-projection"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Result6
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "6"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "projection": {
    "recursiveCall": {
      "site": "recursive loop call",
      "target": "named let loop",
      "tail": true
    },
    "dataDependencies": [
      {
        "argument": "next n",
        "dependsOn": "current n"
      },
      {
        "argument": "next total",
        "dependsOn": [
          "current total",
          "current n"
        ]
      }
    ],
    "branches": [
      "base arm returning total",
      "recursive arm calling loop"
    ],
    "sourceAnchorsRetained": true
  }
}
Product invocation

Expected result

Input 3 produces the exact integer 6. The graph connects the recursive call to the named let binding and retains its tail position. Product invocation awaits its 2.0 adapter.

The loop carries n and total as new argument values. Its recursive call is a tail call in the source program. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Occurrences and tail positions

A viewer may group repeated structures or fold a region. Each original occurrence and its tail position remains recoverable from that view.

A display node can summarize several occurrences. Its shape does not replace their canonical program sites or alter the resource events required by Resources.

13.3 Keep original sites in grouped views

Grouping or folding the graph preserves access to every original occurrence and its tail position. The display choice leaves evaluation events and the canonical outcome unchanged.

Why

Identical source expressions can occupy different evaluation sites. Preserving their occurrences lets a reader locate the first failure and distinguish tail calls.

Group repeated expressions without losing sites

lispex.example.v2.meaning-graph.repeated-sites · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (items)
      (+ (car items) (car items)))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "list",
        "items": [
          {
            "kind": "integer",
            "value": "3"
          }
        ]
      },
      "observation": {
        "graphView": "expanded"
      }
    },
    {
      "input": {
        "kind": "list",
        "items": [
          {
            "kind": "integer",
            "value": "3"
          }
        ]
      },
      "observation": {
        "graphView": "grouped"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Result6
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "6"
  }
}
Result6
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "6"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "projection": {
    "originalOccurrences": [
      {
        "site": "left car call",
        "tail": false
      },
      {
        "site": "right car call",
        "tail": false
      },
      {
        "site": "addition call",
        "tail": true
      }
    ],
    "distinctCarOccurrences": 2,
    "groupedViewPreservesOriginalSites": true
  },
  "comparison": {
    "canonicalOutcomesEqual": true,
    "evaluationResourceEventsEqual": true
  }
}
Product invocation

Expected result

Both evaluations return the exact integer 6. Grouping keeps the left and right car occurrences distinct and preserves their non-tail positions. Product invocation awaits its 2.0 adapter.

Both calls have the same source spelling and use the same input. Their occurrence identities remain distinct in expanded and grouped views. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Graph records

13.4 Read one canonical graph record

A graph record contains the verified program identity and its canonical resolved/1 bytes. The prepared record schema defines every module, binding, node, group, and clause. The relation table below derives the inspection view from those records. A reader preserves every original occurrence and tail flag. Graph export and inspection run no guest initialization or entry. Source locations, layout, explanatory labels, and trace records remain outside the graph record.

Why

One canonical graph preserves the meaning already fixed by preparation. Reusing its records prevents another graph schema from assigning different binding or control meaning. An outer identity binds the projection without placing its own digest inside the program.

Project all prepared forms into one graph

lispex.example.v2.meaning-graph.graph-record-roundtrip · rev. 1

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input)))
spaced.scm
(module main (import) (export rule) (entry rule)
  (define rule
    (lambda (input)
      input)))
Request and files
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 limits sufficient for the stated format checks",
    "evaluate": "finite limits sufficient for the stated calculation"
  },
  "requests": [
    {
      "source": "source.scm",
      "moduleSources": [
        {
          "name": "main",
          "source": "source.scm"
        }
      ],
      "input": {
        "kind": "integer",
        "value": "7"
      },
      "graphInput": "source",
      "displayLabels": "first presentation"
    },
    {
      "source": "spaced.scm",
      "moduleSources": [
        {
          "name": "main",
          "source": "spaced.scm"
        }
      ],
      "input": {
        "kind": "integer",
        "value": "7"
      },
      "graphInput": "resolved/1",
      "displayLabels": "second presentation"
    },
    {
      "source": "source.scm",
      "moduleSources": [
        {
          "name": "main",
          "source": "source.scm"
        }
      ],
      "input": {
        "kind": "integer",
        "value": "7"
      },
      "graphInput": "bytecode/1",
      "displayLabels": "third presentation"
    }
  ]
}
Specification outcome
Result7
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}
Result7
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}
Result7
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "graph": {
    "format": "lispex.graph/1",
    "headerHex": "4c584d4701",
    "payloadFormat": "resolved/1",
    "allGraphBytesEqual": true,
    "allProgramIdentitiesEqual": true,
    "sourceBytesSerialized": false,
    "displayLabelsSerialized": false,
    "projectionRunsGuestCode": false
  },
  "relations": {
    "entryBindingPreserved": true,
    "parameterUseResolvesToEntryParameter": true,
    "bodyNodeRetained": true,
    "tailPositionRetained": true
  }
}
Product invocation

Expected result

All three evaluations return 7. Source, resolved, and bytecode inputs produce identical graph bytes. Product invocation awaits its 2.0 adapter.

The prepared dependency identities are the same in every case. Graph labels stay in the calling application. The source and graph choices use documentation notation. The comparison uses the complete serialized graph.

Reject malformed graph associations and frames

lispex.example.v2.meaning-graph.graph-format-refusal · rev. 1

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input)))
Request and files
mutations.json
[
  {
    "case": "site unknown occurrence kind",
    "inputHex": "4c58530105000a6f6363757272656e636500",
    "reason": "invalid-format"
  },
  {
    "case": "site nonminimal index",
    "inputHex": "4c5853010080000a6f6363757272656e636500",
    "reason": "invalid-format"
  },
  {
    "case": "documentation label used as event role",
    "inputHex": "4c58530100000d6c656674206361722063616c6c00",
    "reason": "invalid-format"
  },
  {
    "case": "graph valid payload with another program identity",
    "mutation": "replace outer ProgramIdentity with a different valid program identity",
    "reason": "identity-mismatch"
  },
  {
    "case": "prepared node reuses another occurrence site",
    "mutation": "replace one node Site with another node Site",
    "reason": "invalid-format"
  },
  {
    "case": "source map wrong byte span",
    "mutation": "change the selected name token StartByte to the following scalar boundary",
    "reason": "invalid-integrity"
  },
  {
    "case": "source map duplicate occurrence",
    "mutation": "repeat one Mapping and increment the Mapping count",
    "reason": "invalid-format"
  },
  {
    "case": "trace partial event frame",
    "inputHex": "011400124c58530100000a6f6363757272656e6365",
    "reason": "invalid-format"
  },
  {
    "case": "trace unknown event tag",
    "inputHex": "010107",
    "reason": "invalid-format"
  },
  {
    "case": "trace event after Terminal",
    "mutation": "append an Enter frame after Terminal before the footer",
    "reason": "invalid-format"
  }
]
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 limits sufficient for the stated format checks",
    "evaluate": "finite limits sufficient for the stated calculation"
  },
  "operation": "validate-graph-field-and-envelope-mutations",
  "mutations": "mutations.json",
  "baseline": "the corresponding valid graph, site field, source map, or trace for the selected request"
}
Specification outcome
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "identity-mismatch"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-integrity"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}
Diagnosticartifact.invalid
Outcome details
{
  "kind": "admission-failure",
  "valueCount": 0,
  "diagnostic": {
    "phase": "admission",
    "code": "artifact.invalid",
    "data": {
      "kind": "graph",
      "reason": "invalid-format"
    }
  },
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "caseOrder": [
    "site unknown occurrence kind",
    "site nonminimal index",
    "documentation label used as event role",
    "graph valid payload with another program identity",
    "prepared node reuses another occurrence site",
    "source map wrong byte span",
    "source map duplicate occurrence",
    "trace partial event frame",
    "trace unknown event tag",
    "trace event after Terminal"
  ],
  "acceptedCount": 0,
  "entryEvaluated": false,
  "existingPreparedHandleChanged": false,
  "previousCanonicalOutcomeChanged": false
}
Product invocation

Expected result

Every malformed field or association is refused before guest execution. Existing handles and completed outcomes remain unchanged. Product invocation awaits its 2.0 adapter.

Case labels describe independently authored mutations. They are not wire fields. Each whole-record mutation starts from a separately valid record. Hex cases supply a field or frame to its enclosing decoder.

Graph encoding

EBNF
GraphBytes = "4c", "58", "4d", "47", "01", ProgramIdentity, ResolvedPayload ;
ProgramIdentity = Count, IdentityBytes ;
ResolvedPayload = Count, Resolved ;
Count = UVar ;

The grammar terminals are hexadecimal octets. Count gives the exact number of following octets or list items. The enclosing production determines which count applies.

ItemEncoding
Graph formatlispex.graph/1
Graph header4c 58 4d 47 01
Site formatlispex.site/1
Site header4c 58 53 01
Qualified site formatlispex.qualified-site/1
Qualified site header4c 58 51 01
Source map formatlispex.source-map/1
Source map header4c 58 53 4d 01
Trace formatlispex.trace/1
Trace header4c 58 54 52 01
UVar and TextThe shortest unsigned integer and strict UTF-8 Text forms in the prepared grammar
Indices and offsetsMathematical nonnegative integers
IdentityBytesThe canonical bytes for the identity domain required by the field
ResolvedThe complete canonical resolved/1 encoding
SourceBundleBytesThe canonical source bundle packet from Embedding
End of inputExactly after the last declared field or trace footer
ExtensionsUnknown headers, versions, tags, roles, and trailing bytes are rejected

Preparation defines UVar, Text, and Resolved. Identity encoding defines IdentityBytes. Source bundles define SourceBundleBytes. Every counted foreign field contains one complete canonical value of its declared type. Its count includes all of that value's header and payload octets. No field permits a second value or padding. The count prefix does not change the foreign encoding.

GraphBytes always uses resolved/1 for its payload. A verified bytecode/1 input is projected through the same canonical records and then encoded as resolved/1. Program identity is checked against that payload under its own identity contract. It occurs only in the outer graph envelope. The format fixes no digest algorithm, tariff coefficient, default limit, or native kernel count.

These are logical relations derived from the prepared records. They are not additional wire fields. Each row is visited in its source table order. Ordered node fields retain their written child order.

RelationTyped fieldsConstruction
Module dependencyModule index, target module index, required identityEach Module dependency row
Import aliasLocal binding index, target binding indexEach Import row
ExportModule index, decoded export name, binding indexEach Export row
DeclarationBinding index, declaration occurrence, binding roleThe canonical declaration walk
Binding useUse node index, binding indexEach use node
Data dependenceConsumer node index, ordered input node indicesThe declared payload children
CallCall node index, operator node index, ordered argument node indices, tail flagEach call node
Direct targetCall occurrence, lambda node or namedlet node or native bindingThe direct target rule below
Named let initial callNamedlet occurrence, loop binding, ordered initializer nodes, enclosing tail flagEach namedlet node
Receiver callClause occurrence, receiver node, test node, enclosing tail flagEach arrow clause
If branchIf node index, test node, written true and false branch nodesEach if node
Clause branchControl node index, ordered clause occurrences and typed childrenEach cond or guard node
Short circuitAnd or or node index, ordered operand nodesEach and or or node
Result sequenceBody or sequence node index, ordered expression nodesEach body or sequence node

A declaration occurrence is the containing module, group, or node from the prepared declaration walk. Imports and native bindings use their Module occurrence. Module and internal definitions use their Group occurrence. Parameters and local bindings use their declaring node occurrence. Binding indices remain distinct when their names have equal scalars. Import aliases retain their targets. Data dependence records structural operands without asserting that every branch runs. The language decides which child is evaluated.

A literal lambda operator has that lambda as its direct target. A use operator follows imported aliases to its declared binding. A lambda initializer, named let loop binding, or native binding supplies a direct target. Every other operator keeps its expression and has no static target. The actual target then appears in the call trace record. An absent static target says only that execution selects the procedure value. Recursive relations follow binding references and direct call targets. They never turn recursive calls into child-graph cycles.

The projection preserves every admitted branch and every original occurrence. It retains body nodes, sequence nodes, groups, clause kinds, and implicit call origins. Grouping is a viewer operation over those immutable records. It adds no serialized label, replacement occurrence, or alternate ordering.

A consumer applies these checks before using supplied graph data. Each applicable reservation follows Resources. An exhausted reservation precedes the check it would fund.

OrderCheck
0Capture the submitted bytes as an immutable input
1Check the header and each canonical count in wire order
2Decode each counted field completely under its declared contract
3Check exact end of input
4Validate embedded prepared records and recompute local sites
5Verify the outer program identity against the resolved payload
6For a source map verify source identity and reconstruct its program and spans
7Check graph associations and record order under the tables below

Inspection uses finite preparation limits and no guest execution. It cannot create a verified evaluator handle from an unchecked graph. Any later execution follows the existing prepared validation and handle rules.

RefusalExisting diagnostic
Malformed bytes, noncanonical rows, unknown role, or invalid siteadmission and artifact.invalid with kind graph and reason invalid-format
A well-formed outer identity names another objectadmission and artifact.invalid with kind graph and reason identity-mismatch
A source map span differs from reconstructed source provenanceadmission and artifact.invalid with kind graph and reason invalid-integrity

The diagnostic catalog defines those identities and fields. A refused graph or map produces no canonical evaluation outcome or evaluation receipt. It does not modify an existing handle or a previously completed evaluation.

Canonical sites

13.5 Encode a local occurrence and event role

CanonicalSiteBytes identifies one occurrence, one semantic event role, and its ordered subject path. Prepared node, group, and clause records use the occurrence role and an empty path. Event sites retain that occurrence and use the exact resource event name. A qualified site attaches program identity outside CanonicalSiteBytes. The local bytes contain no program digest, source coordinate, execution count, or documentation label. A prepared validator recomputes each local occurrence and rejects a mismatched site.

Why

An occurrence remains stable when source spacing or graph layout changes. The event role separates checks that share that occurrence. A typed path identifies the inspected value part. External qualification avoids a digest cycle and distinguishes equal local bytes in different programs.

Encode typed local site vectors

lispex.example.v2.meaning-graph.site-byte-vectors · rev. 1

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input)))
Request and files
site-vectors.json
[
  {
    "kind": "node",
    "index": "0",
    "role": "occurrence",
    "path": []
  },
  {
    "kind": "node",
    "index": "128",
    "role": "occurrence",
    "path": []
  },
  {
    "kind": "group",
    "index": "0",
    "role": "occurrence",
    "path": []
  },
  {
    "kind": "clause",
    "index": "2",
    "role": "occurrence",
    "path": []
  },
  {
    "kind": "node",
    "index": "2",
    "role": "result-check",
    "path": [
      [
        "field",
        "output"
      ]
    ]
  }
]
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 limits sufficient for the stated format checks",
    "evaluate": "finite limits sufficient for the stated calculation"
  },
  "operation": "check-canonical-site-field-vectors",
  "vectors": "site-vectors.json",
  "association": "check occurrence membership separately against a supplied verified program"
}
Specification outcome
Result{"kind":"format-success","valueCount":0,"canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}
Outcome details
{
  "kind": "format-success",
  "valueCount": 0,
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "siteVectors": [
    {
      "record": {
        "kind": "node",
        "index": "0",
        "role": "occurrence",
        "path": []
      },
      "hex": "4c58530100000a6f6363757272656e636500"
    },
    {
      "record": {
        "kind": "node",
        "index": "128",
        "role": "occurrence",
        "path": []
      },
      "hex": "4c5853010080010a6f6363757272656e636500"
    },
    {
      "record": {
        "kind": "group",
        "index": "0",
        "role": "occurrence",
        "path": []
      },
      "hex": "4c58530101000a6f6363757272656e636500"
    },
    {
      "record": {
        "kind": "clause",
        "index": "2",
        "role": "occurrence",
        "path": []
      },
      "hex": "4c58530102020a6f6363757272656e636500"
    },
    {
      "record": {
        "kind": "node",
        "index": "2",
        "role": "result-check",
        "path": [
          [
            "field",
            "output"
          ]
        ]
      },
      "hex": "4c58530100020c726573756c742d636865636b0107066f7574707574"
    }
  ],
  "programDigestInSiteBytes": false,
  "documentationLabelsSerialized": false,
  "qualification": {
    "sameLocalBytesAndSameProgram": "equal-site",
    "sameLocalBytesAndDifferentProgram": "different-site"
  }
}
Product invocation

Expected result

The typed field vectors have the listed exact bytes. A qualified comparison also checks the outer program identity. Product invocation awaits its 2.0 adapter.

These vectors test local field encoding before program association. The typed record names are fixture notation. A prepared validator separately checks the occurrence index and allowed event path. No program digest is chosen here.

Site encoding

EBNF
CanonicalSiteBytes = "4c", "58", "53", "01", OccurrenceKind, Index, Role, SubjectPath ;
OccurrenceKind = "00" | "01" | "02" | "03" | "04" ;
Role = Text ;
SubjectPath = Count, { PathStep } ;
PathStep = "00", Index | "01", Index | "02" | "03" | "04", Index | "05", Index | "06", Index | "07", Text ;
QualifiedSiteBytes = "4c", "58", "51", "01", ProgramIdentity, Site ;
ProgramIdentity = Count, IdentityBytes ;
Site = Count, CanonicalSiteBytes ;
Index = UVar ;
Count = UVar ;

The first index belongs to the table selected by OccurrenceKind. All numbering starts at zero.

Kind octetOccurrenceIndex
00NodeThe existing prepared node index
01GroupModule initializer groups in module order, then internal definition groups in node order
02ClauseContaining node order, then written clause order
03ModuleThe existing prepared module index
04BindingThe existing prepared binding index

Group and clause ordinals count only records of their own kind. Each present internal definition group receives one group ordinal. An absent internal group receives none. Library records precede source records according to the prepared tables. The module index preserves the separate library and source namespaces. Decoded names retain their raw scalars, including an empty Identifier name.

Path tagComponentMeaning
00argument and IndexThe argument at that zero-based position
01result and IndexThe result at that zero-based position
02carThe pair's car
03cdrThe pair's cdr
04element and IndexThe member of an ordered collection at that position
05scalar and IndexThe Unicode scalar at that position
06byte and IndexThe octet at that position
07field and TextThe exact field name defined by the containing record schema

SubjectPath orders components from the outer subject to the inspected part. Element covers vector members and other ordered buffers named by the event catalog. The Rest argument pair row in the Resources site table selects the lambda occurrence and result(0) followed by element(i). This path uses no field name. Field names are schema identifiers, not human explanations. Role is either the exact UTF-8 text occurrence or an event name from the closed resource catalog. The occurrence role requires an empty path. An event's allowed occurrence kind and path follow its resource table. The same occurrence may therefore have different event sites. Repeated execution of one event at one site keeps the same local bytes.

A prepared node stores its own node index with the occurrence role and an empty path. A prepared group or clause stores its assigned ordinal in the same form. Different node, group, and clause occurrences have different typed indices. The validator reconstructs those indices from the canonical prepared tables. Serialized indices cannot replace that reconstruction.

A sequential module group follows the Module definition row in Resources. Its result-check site uses that group occurrence and the complete path element(0). This association excludes recursive module groups and internal definition groups.

Module and binding sites support source provenance and catalog events that explicitly use those kinds. Binding declaration sites do not redirect a use away from its resolved binding. An entry boundary event uses the selected entry lambda occurrence. A call event uses its original call node. An implicit named let call uses the namedlet node. An implicit receiver call uses its clause occurrence. Further event and subject choices follow Resources.

QualifiedSiteBytes pairs one program IdentityBytes value with one local Site value. Its identity must name the program whose canonical tables contain that occurrence. An enclosing graph, map, trace, or outcome can supply the same qualification through its program field. That enclosing field is outside the canonical prepared bytes. Comparing qualified sites compares both the program identity and the complete local bytes. Equal local bytes from distinct programs do not denote the same qualified site.

A source-bound preparation location is a different record. Before a canonical program exists it uses the exact submitted source and its source coordinates. A prepared-byte decoder may instead identify the immutable submitted wire offset. Neither case invents a program identity or a CanonicalSiteBytes value.

Source maps

Source maps translate canonical sites into locations in the submitted source. Human labels and explanatory nodes help readers navigate the graph.

Use source identity to retain exact source provenance. Render evaluation failures at the canonical sites recorded in their canonical outcomes. A source map supplies the module and exact byte coordinates. The caller attaches its displayed filename.

A read or normalization failure uses a source-bound preparation report. A resolved graph requires a successfully resolved program.

13.6 Keep source maps outside semantic identity

Source maps associate canonical program sites with exact source locations. Source coordinates, display annotations, and layout remain separate from canonical program identity. Changing only those records preserves the evaluation outcome and resource events.

Why

Reformatting source can move a displayed location while preserving the resolved program. Separating the records keeps replay comparisons and canonical failure sites stable.

Replay after source locations move

lispex.example.v2.meaning-graph.source-map-replay · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (items)
      (car items))))
spaced.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule

    (lambda (items)

      (car
        items))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "list",
        "items": []
      },
      "source": "source.scm",
      "observation": {
        "graph": "resolved-projection",
        "sourceMap": "submitted-source"
      },
      "rootModule": "main",
      "moduleSources": [
        {
          "name": "main",
          "source": "source.scm"
        }
      ]
    },
    {
      "input": {
        "kind": "list",
        "items": []
      },
      "source": "spaced.scm",
      "observation": {
        "graph": "resolved-projection",
        "sourceMap": "submitted-source"
      },
      "rootModule": "main",
      "moduleSources": [
        {
          "name": "main",
          "source": "spaced.scm"
        }
      ]
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "comparison": {
    "canonicalProgramsEqual": true,
    "semanticRequestsEqual": true,
    "canonicalOutcomesEqual": true,
    "evaluationResourceEventsEqual": true
  },
  "provenance": {
    "exactSourceIdentitiesEqual": false,
    "displayedSourceLocationsEqual": false,
    "canonicalFailureSitesEqual": true
  }
}
Product invocation

Expected result

Both source spellings produce the same car domain failure at the same canonical site. Their exact source identities and displayed source locations differ. Product invocation awaits its 2.0 adapter.

Only whitespace and the source filename change. Preparation records retain each submitted source. Evaluation compares the same resolved program and canonical failure site. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

13.7 Bind byte spans to exact submitted source

A source map pairs the program identity with the exact source identity and the submitted source bundle. Each mapping names one source occurrence and its exact half-open UTF-8 byte span. The table below fixes span construction for written and implicit nodes. Validation reconstructs the prepared records and these spans without running guest code. A mismatched map is refused as graph data. It cannot replace the prepared program, canonical failure site, or completed outcome. Caller display paths remain separate annotations.

Why

Exact source bytes let a reader verify a displayed location. Byte spans remain unambiguous across Unicode scalars and newline spellings. Separating the map preserves canonical program comparisons after source presentation changes.

Map escaped names to exact UTF-8 spans

lispex.example.v2.meaning-graph.source-map-utf8 · rev. 1

source.scm
(module |주|
  (import)
  (export |규칙|)
  (entry |규칙|)
  (define |규칙| (lambda (|값|) |값|)))
crlf.scm
(module |주|
  (import)
  (export |규칙|)
  (entry |규칙|)
  (define |규칙| (lambda (|값|) |값|)))
Request and files
request.json
{
  "notation": "documentation-request",
  "source": "source.scm",
  "rootModule": "주",
  "moduleSources": [
    {
      "name": "주",
      "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 limits sufficient for the stated format checks",
    "evaluate": "finite limits sufficient for the stated calculation"
  },
  "requests": [
    {
      "source": "source.scm",
      "moduleSources": [
        {
          "name": "주",
          "source": "source.scm"
        }
      ],
      "input": {
        "kind": "integer",
        "value": "7"
      },
      "sourceMap": "lispex.source-map/1"
    },
    {
      "source": "crlf.scm",
      "moduleSources": [
        {
          "name": "주",
          "source": "crlf.scm"
        }
      ],
      "input": {
        "kind": "integer",
        "value": "7"
      },
      "sourceMap": "lispex.source-map/1"
    }
  ],
  "mappingSelection": {
    "nodeKind": "use",
    "decodedName": "값",
    "bindingRole": "entry-fixed-parameter"
  }
}
Specification outcome
Result7
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}
Result7
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "7"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "sourceMap": {
    "format": "lispex.source-map/1",
    "headerHex": "4c58534d01",
    "usesSourceBundleBytes": true,
    "decodedModuleName": "주",
    "decodedBindingName": "값",
    "nameUseSpans": [
      {
        "startByte": "99",
        "endByte": "104",
        "tokenHex": "7ceab0927c"
      },
      {
        "startByte": "103",
        "endByte": "108",
        "tokenHex": "7ceab0927c"
      }
    ],
    "offsetUnit": "utf8-octet",
    "documentationLabelsSerialized": false
  },
  "comparison": {
    "canonicalProgramsEqual": true,
    "canonicalLocalSitesEqual": true,
    "canonicalOutcomesEqual": true,
    "evaluationResourceEventsEqual": true,
    "exactSourceIdentitiesEqual": false,
    "sourceMapBytesEqual": false
  }
}
Product invocation

Expected result

Both newline spellings return 7 at the same canonical sites. The source map keeps the different exact byte spans. Product invocation awaits its 2.0 adapter.

The source uses bars around each Unicode Identifier. Mapping selection is documentation notation. The serialized mapping uses its reconstructed numeric occurrence. The complete token span includes both bars.

Source map encoding

EBNF
SourceMapBytes = "4c", "58", "53", "4d", "01", ProgramIdentity, SourceIdentity, Bundle, Mappings ;
ProgramIdentity = Count, IdentityBytes ;
SourceIdentity = Count, IdentityBytes ;
Bundle = Count, SourceBundleBytes ;
Mappings = Count, { Mapping } ;
Mapping = Site, StartByte, EndByte ;
Site = Count, CanonicalSiteBytes ;
StartByte = UVar ;
EndByte = UVar ;
Count = UVar ;

SourceMapBytes carries the original source bundle as one canonical packet. The bundle's accepted module names are unique. Its root agrees with the prepared root by decoded name. Each submitted source module matches the prepared source module with that exact name. Library modules remain in their separate namespace.

FieldRequirement
ProgramIdentityThe identity of the canonical resolved records
SourceIdentityThe identity of the exact submitted source bundle under the source identity contract
BundleOne accepted SourceBundleBytes packet
Mapping SiteThe occurrence role and empty path
StartByteThe included first UTF-8 octet
EndByteThe excluded octet after the source span
Mapping orderKind octet, then mathematical index
Mapping membershipExactly every node, group, clause, module, and binding declared by a submitted source module
Library occurrencesNo mapping in this submitted-source map

The target occurrence determines its owning module. A binding uses its declaration module, including a local imported alias. The module name selects the exact source bytes in Bundle. Every span satisfies StartByte less than EndByte and EndByte at most the module's source byte length. Both boundaries occur between complete UTF-8 scalars. CR and LF retain their original octets. Line and column display is derived from these exact bytes. The caller can attach a display path to the module name outside this format.

The decoder rejects missing, duplicate, extra, or unsorted mappings. It reconstructs source spans using the reader and canonical construction rules. It verifies the source identity and compares the reconstructed program with ProgramIdentity. Every supplied Mapping must equal the reconstructed occurrence and span. Replacing only the source bundle or map cannot replace the program or its evaluation identity.

A reader span starts at the first octet of its token or opening delimiter. It ends immediately after the token or matching closing delimiter. Whitespace and comments between the endpoints remain inside the span. Surrounding whitespace and comments remain outside it.

Canonical occurrenceSource span
Written expression nodeIts complete reader form
Name use nodeIts complete Identifier token, including bars and escapes
Literal from quotationIts complete quote form, including the quote prefix when written
Explicit lambda nodeIts complete lambda form
Lambda from procedure definition shorthandIts complete define form
Implicit body nodeThe first leading definition or expression through the last body expression
Module initializer groupThe first member define form through the last member define form
Internal definition groupThe first leading define form through the last leading define form
ClauseThe complete written clause form
ModuleThe complete module form
Binding declarationThe Identifier token that declares the local binding
Plain import bindingThe imported Identifier token
Renamed import bindingThe local alias Identifier token
Rest parameterIts Identifier token, excluding the dotted-list separator

Body and group spans may contain several written forms. Their endpoints still identify one exact byte interval. An omitted branch or absent internal group creates no mapping. An implicit named let call shares its namedlet occurrence. An implicit receiver call shares its clause occurrence. Their event roles distinguish the call from other work at that occurrence. An event subject path does not invent a new source location. Source presentation uses its enclosing occurrence mapping. Source-bound decode or read failures use their preparation report before this map exists.

Execution trace

Trace recording observes one execution. The caller selects its finite capacity before evaluation and keeps that reservation separate from guest resource limits.

A full trace records the selected execution path. An incomplete trace records only a prefix and marks that limit. The complete evaluation still produces its own outcome.

The first semantic failure and resource stop follow the same event order with tracing enabled or disabled. The trace supplies no extra guest calls, allocation charges, or guard branches.

13.8 Keep trace capacity separate from evaluation

Apply the separate account and stop rules from trace reservations. This chapter defines the trace packet, whole record frames, and completion footer. The command result carries the separate host trace status. Trace state preserves the evaluation outcome, first failure, resource axis, and canonical site.

Why

A trace helps explain an execution. Separating its storage and exhaustion from guest evaluation preserves the request that the caller chose to run.

Finish evaluation after trace capacity fills

lispex.example.v2.meaning-graph.trace-success · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (items)
      (+ (car items) 1))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "list",
        "items": [
          {
            "kind": "integer",
            "value": "9"
          }
        ]
      },
      "observation": {
        "trace": "off"
      }
    },
    {
      "input": {
        "kind": "list",
        "items": [
          {
            "kind": "integer",
            "value": "9"
          }
        ]
      },
      "observation": {
        "trace": "on",
        "reservation": "separate finite capacity sufficient for the complete execution trace"
      }
    },
    {
      "input": {
        "kind": "list",
        "items": [
          {
            "kind": "integer",
            "value": "9"
          }
        ]
      },
      "observation": {
        "trace": "on",
        "reservation": "separate finite capacity for a proper prefix of the execution trace"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Result10
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "10"
  }
}
Result10
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "10"
  }
}
Result10
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "10"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "trace": [
    {
      "state": "off"
    },
    {
      "state": "complete"
    },
    {
      "state": "incomplete",
      "reason": "capacity-exhausted",
      "evaluationContinued": true
    }
  ],
  "comparison": {
    "canonicalOutcomesEqual": true,
    "evaluationResourceEventsEqual": true,
    "guestCallsAdded": false,
    "guestAllocationChargesAdded": false,
    "guestGuardBranchesAdded": false
  }
}
Product invocation

Expected result

All three evaluations return the exact integer 10. The third trace becomes incomplete while evaluation continues with unchanged guest events. Product invocation awaits its 2.0 adapter.

Run the same request with tracing off, with enough reserved trace capacity, and with capacity for only a prefix. The capacity choices affect trace completeness. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Preserve a failure after tracing stops

lispex.example.v2.meaning-graph.trace-failure · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (items)
      (+ (car items) 1))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "list",
        "items": []
      },
      "observation": {
        "trace": "off"
      }
    },
    {
      "input": {
        "kind": "list",
        "items": []
      },
      "observation": {
        "trace": "on",
        "reservation": "separate finite capacity sufficient for the complete execution trace"
      }
    },
    {
      "input": {
        "kind": "list",
        "items": []
      },
      "observation": {
        "trace": "on",
        "reservation": "separate finite capacity for a proper prefix of the execution trace"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "trace": [
    {
      "state": "off"
    },
    {
      "state": "complete"
    },
    {
      "state": "incomplete",
      "reason": "capacity-exhausted",
      "evaluationContinued": true
    }
  ],
  "comparison": {
    "canonicalOutcomesEqual": true,
    "evaluationResourceEventsEqual": true,
    "guestCallsAdded": false,
    "guestAllocationChargesAdded": false,
    "guestGuardBranchesAdded": false,
    "firstFailuresEqual": true,
    "canonicalFailureSitesEqual": true
  }
}
Product invocation

Expected result

All three evaluations produce the same car domain failure. Filling trace capacity preserves the first failure and its canonical site. Product invocation awaits its 2.0 adapter.

The input is the empty list. The later addition is not reached. Trace storage exhaustion leaves the car failure as the first semantic failure. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Preserve a terminal resource stop

lispex.example.v2.meaning-graph.trace-resource-stop · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (input)
      (let loop ()
        (loop)))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient to enter the loop"
  },
  "requests": [
    {
      "input": {
        "kind": "integer",
        "value": "0"
      },
      "observation": {
        "trace": "off"
      }
    },
    {
      "input": {
        "kind": "integer",
        "value": "0"
      },
      "observation": {
        "trace": "on",
        "reservation": "separate finite capacity sufficient for the complete execution trace"
      }
    },
    {
      "input": {
        "kind": "integer",
        "value": "0"
      },
      "observation": {
        "trace": "on",
        "reservation": "separate finite capacity for a proper prefix of the execution trace"
      }
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Resultresource-stop
Outcome details
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true
}
Resultresource-stop
Outcome details
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true
}
Resultresource-stop
Outcome details
{
  "kind": "resource-stop",
  "valueCount": 0,
  "terminal": true
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "trace": [
    {
      "state": "off"
    },
    {
      "state": "complete"
    },
    {
      "state": "incomplete",
      "reason": "capacity-exhausted",
      "evaluationContinued": true
    }
  ],
  "comparison": {
    "canonicalOutcomesEqual": true,
    "evaluationResourceEventsEqual": true,
    "guestCallsAdded": false,
    "guestAllocationChargesAdded": false,
    "guestGuardBranchesAdded": false,
    "exhaustedResourceAxesEqual": true,
    "canonicalStopSitesEqual": true
  },
  "returnedControl": true
}
Product invocation

Expected result

All three evaluations end with the same terminal resource stop and no result datum. The exhausted resource axis and canonical stop site remain equal. Product invocation awaits its 2.0 adapter.

The loop continues until evaluation reaches a finite resource limit. The resource model determines the exact axis and site. Trace capacity cannot select a different semantic stop. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

See Resource model numbers, Channel units and terminal reporting.

13.9 Record a complete prefix of execution events

A trace records the admitted request through the event tags below. Recording starts after canonical input admission and before module initialization. Each record uses canonical sites and metadata already available from the observed event. The trace reservation contract reserves one complete framed record before storing it. The first trace reservation failure permanently stops recording. A reserved footer marks the retained prefix incomplete. Evaluation continues with unchanged checks, charges, first failure, and outcome. Trace records contain no guest value payloads or host timing data.

Why

Complete frames let every reader consume the same prefix. A separate footer records exhaustion without a second allocation after the buffer fills. Observing existing metadata avoids guest traversal and leaves the semantic request unchanged.

Conditional forms use written alternatives.

Reserve complete trace frames and one footer

lispex.example.v2.meaning-graph.trace-byte-prefix · rev. 1

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule (lambda (input) input)))
Request and files
trace-vectors.json
[
  {
    "kind": "enter",
    "site": {
      "kind": "node",
      "index": "0",
      "role": "occurrence",
      "path": []
    }
  },
  {
    "kind": "terminal",
    "outcome": "success",
    "site": null
  }
]
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 limits sufficient for the stated format checks",
    "evaluate": "finite limits sufficient for the stated calculation"
  },
  "operation": "check-trace-frame-vectors",
  "vectors": "trace-vectors.json",
  "traceCapacity": "symbolic finite octet capacity at each complete record boundary"
}
Specification outcome
Result{"kind":"format-success","valueCount":0,"canonicalOutcomeProduced":false,"evaluationReceiptEligible":false}
Outcome details
{
  "kind": "format-success",
  "valueCount": 0,
  "canonicalOutcomeProduced": false,
  "evaluationReceiptEligible": false
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "frameVectors": [
    {
      "event": {
        "kind": "enter",
        "site": {
          "kind": "node",
          "index": "0",
          "role": "occurrence",
          "path": []
        }
      },
      "frameHex": "011400124c58530100000a6f6363757272656e636500"
    },
    {
      "event": {
        "kind": "terminal",
        "outcome": "success",
        "site": null
      },
      "frameHex": "0103060000"
    }
  ],
  "prefixCases": [
    {
      "capacity": "header and footer only",
      "recordHex": "",
      "footerHex": "0001"
    },
    {
      "capacity": "header and footer plus the first complete record",
      "recordHex": "011400124c58530100000a6f6363757272656e636500",
      "footerHex": "0001"
    },
    {
      "capacity": "complete observation stream",
      "footerHex": "0000"
    },
    {
      "capacity": "host interrupted before Terminal with space remaining",
      "footerHex": "0002"
    }
  ],
  "reservationUnit": "marker plus shortest payload length plus entire payload",
  "partialRecordsWritten": false,
  "recordingRestarts": false,
  "guestChargesAdded": false,
  "canonicalOutcomeChanged": false
}
Product invocation

Expected result

The frame vectors use the listed exact bytes. An exhausted trace retains only complete frames and its reserved footer. Product invocation awaits its 2.0 adapter.

Each vector is an isolated event frame. They are not a complete execution trace. Program and request IdentityBytes remain in the enclosing header. Capacity choices are symbolic and set no tariff or default limit.

Trace encoding

EBNF
TraceBytes = "4c", "58", "54", "52", "01", ProgramIdentity, RequestIdentity, { TraceRecord }, TraceEnd ;
ProgramIdentity = Count, IdentityBytes ;
RequestIdentity = Count, IdentityBytes ;
TraceRecord = "01", Count, TraceEvent ;
TraceEnd = "00", Completion ;
Completion = "00" | "01" | "02" ;
TraceEvent = Enter | Branch | Call | Return | Condition | Reservation | Terminal ;
Enter = "00", Site ;
Branch = "01", Site, Choice ;
Choice = "00", NodeIndex | "01" ;
Call = "02", Site, ProcedureTarget, Tail ;
ProcedureTarget = "00", NodeIndex | "01", NodeIndex | "02", BindingIndex ;
Return = "03", Site, ValueCount ;
Condition = "04", Site, Code ;
Reservation = "05", Site, ReservationResult ;
ReservationResult = "00" | "01", Axis ;
Axis = "00" | "01" | "02" | "03" | "04" | "05" ;
Terminal = "06", TerminalKind, OptionalSite ;
TerminalKind = "00" | "01" | "02" | "03" ;
OptionalSite = "00" | "01", Site ;
Site = Count, CanonicalSiteBytes ;
Tail = "00" | "01" ;
Code = Text ;
NodeIndex = UVar ;
BindingIndex = UVar ;
ValueCount = UVar ;
Count = UVar ;

The header supplies the program and request identities once. Every local site in the stream is qualified by that program identity. Record position gives stream order. No execution counter occurs inside a site.

Event tagEventFields after the tag
00EnterThe occurrence Site
01BranchThe controlling occurrence Site and Choice
02CallThe call occurrence Site, actual ProcedureTarget, and tail flag
03ReturnThe call occurrence Site and number of returned values
04ConditionThe committed occurrence Site and its condition code
05ReservationThe catalog event Site and ReservationResult
06TerminalTerminalKind and OptionalSite
VariantTagFields or meaning
Choice00The selected next node index
Choice01No next child is selected by this control decision
ProcedureTarget00The lambda node index
ProcedureTarget01The namedlet node index
ProcedureTarget02The native member binding index
ReservationResult00Reservation accepted before its associated check or effect
ReservationResult01Reservation refused, followed by the exhausted Axis
Axis00work
Axis01allocation
Axis02frames
Axis03input
Axis04result
Axis05diagnostic
TerminalKind00Successful Datum result
TerminalKind01Uncaught guest condition
TerminalKind02Evaluation resource stop
TerminalKind03Entry result boundary failure
Completion00All admitted evaluation events through Terminal are recorded
Completion01Recording stopped at the first event that did not fit
Completion02Host interruption prevented a complete evaluation trace

Enter, Branch, Call, and Return use occurrence sites with empty paths. Condition uses the canonical failure site of the new condition occurrence. Reservation uses the exact catalog event role and subject path. Terminal success has no site. Every other Terminal has the canonical failure or stop site. Code is a guest code from the Condition catalog. Condition data and result values stay in their existing records. Trace metadata never copies or traverses guest data to populate a trace field.

These emission points preserve the language's existing event order. They add no evaluation checks or reservations. At each point a trace record is attempted only while recording remains active.

ObservationEmission point
ReservationImmediately after atomic acceptance or refusal and before the associated check or effect
EnterOn reaching the expression node, before its first operation event, child evaluation, or produced value
BranchAfter the controlling test and its required checks, before the selected next child
CallAfter the accepted call reservation, before parameter binding or procedure execution
ReturnAfter accepted call-return and release of active call capacity, before forwarding the result sequence or caller result-check
ConditionAfter required diagnostic-payload reservation and creation of a new condition occurrence
TerminalAfter the admitted evaluation's canonical result or failure is fixed

Every entered expression emits Enter, including written body and sequence nodes. Those observations add no resource event to implicit body nodes. Initialization visits the fixed library and source modules in their existing order. An implicit named let or receiver call uses the original occurrence fixed by preparation. Call and Return use the occurrences of their observed call and call-return events. Tracing adds no Return for a caller whose capacity was replaced by a tail transfer. It retains no extra continuation to pair those observations. The entry Call uses the selected entry lambda occurrence and a false tail flag. Any entry Return follows the existing call-return event and its canonical occurrence.

The following table fixes each Branch emission and its site.

ControlSiteEmission and choice
IfThe if node occurrenceAfter the test selects one of its two written branches
Nonfinal and or or operandThe and or or node occurrenceAfter result-check and branch-select select the next operand or no child
Final and or or operandThe and or or node occurrenceWhen the final operand returns, select no child before forwarding its result sequence
Empty and or orThe and or or node occurrenceAfter its branch-select selects no child
Cond or guard test clauseThat clause occurrenceAfter its test selects a body or receiver, or no child
Else clauseThat clause occurrenceWhen reached selects its body before body entry

The final and or or observation inspects no returned value or value count. It adds no result-check or branch-select event. A false clause selects no child for that clause. Normal dispatch then visits the next clause under the language rules. A selected test-only clause also selects no further child. An unmatched guard follows its existing outward propagation rule. The records observe those decisions without adding tests or fallback results.

Condition propagation retains the original occurrence. It does not emit a new Condition record unless another condition occurrence is created. A failure to reserve a condition payload produces its resource stop before any new Condition record. The corresponding refused Reservation record precedes that stop. Terminal is the final admitted evaluation event. Later qualification, evidence, and output transport work stays outside this stream. Input decoding before request identity exists also stays outside this admitted trace.

A TraceRecord count gives the exact number of TraceEvent payload octets. Its reservation unit includes the 01 marker, the count prefix, and the entire payload. The header and complete two-octet footer are reserved before admitted evaluation starts. Resources defines that separate trace account.

The first record that cannot fit contributes no bytes. The recorder then stops permanently and retains the already complete prefix. It writes the reserved 00 01 footer when returning the trace. A complete trace ends with 00 00. A host interruption before Terminal uses 00 02 unless capacity exhaustion already stopped recording. Once Terminal is stored, the complete stream retains 00 00. A later output or trace delivery failure does not change that stream. The recorder allocates no failure text after exhaustion. It adds no guest event, call, guard branch, or resource charge. It keeps no growing trace-only counter after recording stops.

A complete trace has exactly one Terminal record in final position. An incomplete trace contains a proper prefix and may have no Terminal record. An event after Terminal, a duplicate footer, a partial frame, or trailing bytes is invalid. Unknown event tags and fields are rejected. The stream header must agree with the enclosing request and program when those are supplied. The format gives an observed path and does not itself establish evaluator conformance. Examples retain separate not-run product plans until the product adapter exists.

Independent graph evaluation

A graph viewer reads the projection. An independent graph evaluator is another engine that must meet the same sandbox contract.

The product checks its supported requests before dispatch. It follows the admission-before-entry rule for unsupported capability.

Projection checks establish the relations shown by the graph. Independent execution cases establish agreement of outcomes and resource events. Execution evidence remains separate from the portable receipt.

13.10 Require conformance from a graph evaluator

A separate graph evaluator follows the same-request rule and resource event order for every admitted request. Unsupported requests follow the admission-before-entry rule. Its conformance requires execution evidence separate from graph projection.

Why

A graph describes a program, while an evaluator performs its operations. Independent execution evidence checks that another evaluator preserves the same failures and resource boundaries.

Compare an independent graph evaluator

lispex.example.v2.meaning-graph.graph-engine-replay · rev. 2

source.scm
(module main
  (import)
  (export rule)
  (entry rule)
  (define rule
    (lambda (flag)
      (if flag
          42
          (car '())))))
Request and files
request.json
{
  "notation": "documentation-request",
  "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 each supplied source",
    "evaluate": "finite values sufficient for the stated finite calculation"
  },
  "requests": [
    {
      "input": {
        "kind": "boolean",
        "value": true
      },
      "execution": "product evaluator"
    },
    {
      "input": {
        "kind": "boolean",
        "value": true
      },
      "execution": "independent graph evaluator"
    },
    {
      "input": {
        "kind": "boolean",
        "value": false
      },
      "execution": "product evaluator"
    },
    {
      "input": {
        "kind": "boolean",
        "value": false
      },
      "execution": "independent graph evaluator"
    }
  ],
  "rootModule": "main",
  "moduleSources": [
    {
      "name": "main",
      "source": "source.scm"
    }
  ]
}
Specification outcome
Result42
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
Result42
Outcome details
{
  "kind": "value",
  "valueCount": 1,
  "datum": {
    "kind": "integer",
    "value": "42"
  }
}
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}
Condition{"category":"domain","operation":"car","required":"pair","received":"empty-list"}
Outcome details
{
  "kind": "language-failure",
  "valueCount": 0,
  "condition": {
    "category": "domain",
    "operation": "car",
    "required": "pair",
    "received": "empty-list"
  }
}

Specification outcome. Product runs are pending the 2.0 adapter.

Semantic details
{
  "comparison": {
    "canonicalOutcomesEqualForEachInput": true,
    "evaluationResourceEventsEqualForEachInput": true
  }
}
Product invocation

Expected result

Both evaluators return 42 for true and the same car domain failure for false. Each admitted request preserves the same evaluation resource event order. Product invocation awaits its 2.0 adapter.

Each evaluator needs its own product execution evidence. The plan compares admitted requests after the corresponding evaluator exists. A graph view by itself supplies no execution observation. The request and graph relations use documentation notation. Site labels name source occurrences for this example. Serialized records follow the graph contract. Product invocation awaits its 2.0 adapter.

Related chapters

Evaluation and bindings

Preparation and modules

Identity, receipt, replay