Lispex 2.0 specification · not released · Tested product not run · Examples not run # Source and normalization Source text, tokens, literals, and the normalized form of a Lispex rule. Canonical: /v2.0/en/docs/language/source Document revision: 2.0-draft-1. Content locale: en. Translation: current. - language: `lispex` - languageVersion: `2.0` ## Scope Write a rule as UTF-8 source and supply its input separately. Preparation reads the source and resolves its names before evaluation begins. ## UTF-8 source Source text is the UTF-8 spelling supplied for a module. Decoded characters use [Unicode scalar values](/v2.0/en/docs/language/values#lispex.section.v2.values.unicode-text). [Source identity](/v2.0/en/docs/profiles/receipt-and-replay#lispex.section.v2.receipt-and-replay.identities) retains the original bytes. The resolved program has its separate program identity. [Values and text](/v2.0/en/docs/language/values#lispex.section.v2.values.datum) defines the text values that a rule can return. ### Preserve source spelling Source reading applies the [raw Unicode rule](/v2.0/en/docs/language/values#lispex.rule.v2.values.raw-unicode) to names and string literals. The resulting spellings determine source identifiers and literal text. **Why** Distinct decoded scalar sequences remain distinct across products. A host locale or compiler table must not silently rename a binding or alter data. Claim: `lispex.claim.v2.source.raw-spelling` · structural · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "source-reading", "encoding": "UTF-8", "content": [ "identifier", "string-literal" ] }, "result": { "kind": "raw-scalar-preservation", "implicitNormalization": false, "implicitCaseFolding": false }, "pendingCases": [ "The grammar and module contracts are fixed. Every product, engine, architecture, and resource boundary still needs direct execution." ] } ``` ### Keep two Unicode spellings distinct Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (let ((|é| 1) (|é| 2)) (list |é| |é|)))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The two names denote different bindings and the result is the list of exact integers 1 and 2. Product invocation awaits its 2.0 adapter." } ``` The first name contains one scalar. The second contains an e followed by a combining accent. Normalizing the names would merge distinct bindings. ### Preserve text inside a string Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) "A (; B)")) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The rule returns the exact string A followed by a space, an opening parenthesis, a semicolon, a space, B, and a closing parenthesis. Product invocation awaits its 2.0 adapter." } ``` Delimiters and a comment marker inside the quoted text belong to the string value. ### Decode exact UTF-8 source bytes Each module must satisfy the byte grammar before reading starts. Reject every malformed UTF-8 sequence. Decoding never inserts a replacement scalar. A byte order mark has no special treatment. A leading mark therefore fails the reader grammar. The same scalar is permitted inside a string, a quoted identifier, or a comment. **Why** Exact decoding keeps the submitted bytes and their meaning reproducible. Repair and automatic marker removal would silently change an input. Claim: `lispex.claim.v2.source.utf8-source` · boundary · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "source-byte-admission", "encoding": "UTF-8" }, "result": { "kind": "strict-utf8-decoding", "overlong": "reject", "surrogate": "reject", "outOfRange": "reject", "truncated": "reject", "replacement": false, "bomStripping": false, "decodeCompletesBeforeReading": true }, "pendingCases": [ "Every product, supported engine, architecture, and finite resource boundary needs direct execution." ] } ``` ### Reject malformed source octets Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `invalid-utf8.json` ```lispex { "notation": "documentation-reader-cases", "cases": [ { "case": "overlong", "sourceOctetsHex": "c080", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } }, { "case": "surrogate", "sourceOctetsHex": "eda080", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } }, { "case": "out-of-range", "sourceOctetsHex": "f4908080", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } }, { "case": "stray-continuation", "sourceOctetsHex": "80", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } }, { "case": "truncated", "sourceOctetsHex": "e282", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } }, { "case": "invalid-leading-byte", "sourceOctetsHex": "ff", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } }, { "case": "decode-before-reader", "sourceOctetsHex": "29ff", "moduleName": "main", "diagnostic": { "phase": "decode", "code": "source.encoding", "data": { "reason": "invalid-utf8" } } } ] } ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "invalid-utf8.json", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "caseInput": "submit-each-listed-source-independently" } ``` Fixture inputs and environment: ```json { "entry": "invalid-utf8.json", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Every byte sequence is rejected during decoding. The final case does not reach its earlier unmatched parenthesis. Product invocation awaits its 2.0 adapter." } ``` The text fixture lists independent source inputs. Hex octets describe exact submitted bytes. This notation is not a public input codec. ### Preserve a mark inside literal text Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) ""))) ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "source.scm", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The result contains the literal U+FEFF scalar. Product invocation awaits its 2.0 adapter." } ``` The UTF-8 decoder preserves the mark as a scalar. The string grammar admits it as data. ## Tokens Tokens distinguish identifiers, literal data, and the delimiters of a form. Reading produces syntax for preparation. Evaluation uses the lexical binding selected during preparation. Quotation uses the decoded name as data. The complete grammar below fixes token boundaries and escapes. ### Read one fixed syntax The complete reader grammar below determines every source token and datum. Bare identifiers use ASCII characters. Vertical bars admit every Unicode scalar sequence through literal characters or escapes. Identifiers compare by their decoded scalar sequence. Spelling escapes do not create a different name. Only the listed separators end tokens. Block comments nest. A datum comment reads and discards the next datum. Discarded data must satisfy the reader grammar but undergo no normalization. Reader directives and unlisted token prefixes are rejected. **Why** Explicit character sets avoid host locale and Unicode classification differences. Quoted names retain arbitrary text without adding invisible token boundaries. Nested comments remain readable while discarded syntax receives the same finite reading checks. Claim: `lispex.claim.v2.source.reader-grammar` · structural · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "complete-reader-grammar", "grammar": "lispex.grammar.v2.source.reader" }, "result": { "kind": "fixed-reader-language", "bareIdentifiers": "ASCII", "quotedIdentifiers": "raw-Unicode-scalars", "whitespace": [ "U+0020", "U+0009", "U+000A", "U+000D U+000A" ], "blockComments": "nested", "datumComments": "read-one-datum-after-trivia", "directives": "reject", "loneCarriageReturnOutsideText": "reject", "implicitCaseFolding": false, "implicitUnicodeNormalization": false }, "pendingCases": [ "Every product, supported engine, architecture, and finite resource boundary needs direct execution." ] } ``` ### Read exact names with bars and escapes Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (let ((|caf\u{e9}| 1) (|café| 2)) (list |café| |café| '|a b| '|| '|1|))))) ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "source.scm", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The escaped and literal spellings of café select the same binding. The decomposed name remains distinct. Product invocation awaits its 2.0 adapter." } ``` A numeric spelling inside bars denotes a symbol. The empty barred spelling also denotes a symbol. ### Read nested comments and discard complete data Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (list 1#| outer #| nested |# end |#2 #;#;(ignored) (set! input 9) 3)))) ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "source.scm", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The rule returns the exact integers 1, 2, and 3 in order. Product invocation awaits its 2.0 adapter." } ``` The inner datum comment discards its datum. The outer datum comment then discards the mutation form before normalization. ### Reject unlisted source syntax Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `reader-rejections.json` ```lispex { "notation": "documentation-reader-cases", "cases": [ { "case": "bare-nonascii", "source": "café", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-token" } } }, { "case": "nbsp-separator", "source": "a b", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-token" } } }, { "case": "lone-carriage-return", "source": "a\rb", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-token" } } }, { "case": "leading-mark", "source": "(define x 1)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unexpected-source-scalar" } } }, { "case": "double-mark", "source": "", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unexpected-source-scalar" } } }, { "case": "case-directive", "source": "#!fold-case", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "language-directive", "source": "#lang lispex", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "shebang", "source": "#!/usr/bin/lispex", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "unterminated-block", "source": "#| outer #| inner |#", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.delimiter", "data": { "reason": "unexpected-end" } } }, { "case": "missing-discard", "source": "#;", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.delimiter", "data": { "reason": "unexpected-end" } } }, { "case": "invalid-discard", "source": "#; (", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.delimiter", "data": { "reason": "unexpected-end" } } }, { "case": "datum-label", "source": "#0=(a . #0#)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "alternate-brackets", "source": "[1 2]", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-token" } } }, { "case": "quasiquote", "source": "`x", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-token" } } }, { "case": "empty-dotted-list", "source": "(. a)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.delimiter", "data": { "reason": "improper-form" } } }, { "case": "extra-dotted-tail", "source": "(a . b c)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.delimiter", "data": { "reason": "improper-form" } } }, { "case": "vector-dot", "source": "#(a . b)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.delimiter", "data": { "reason": "improper-form" } } }, { "case": "wrong-boolean", "source": "#true", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-token" } } } ] } ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "reader-rejections.json", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "caseInput": "submit-each-listed-source-independently" } ``` Fixture inputs and environment: ```json { "entry": "reader-rejections.json", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Each source fails reading before normalization begins. Product invocation awaits its 2.0 adapter." } ``` The text fixture lists independent source inputs. Hex octets describe exact submitted bytes. This notation is not a public input codec. ### Separate tokens outside literals Use the token and literal boundaries in the [reader grammar](/v2.0/en/docs/language/source#lispex.rule.v2.source.reader-grammar). A comment marker is recognized outside String, BarredIdentifier, and Character tokens. A semicolon inside an admitted literal remains part of that literal. **Why** Explicit separators make a source file independent of a host tokenizer. Keeping comments outside literals preserves the data written inside a string. Token boundaries specify separators and line comments. Claim: `lispex.claim.v2.source.token-boundaries` · structural · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "source-token-boundaries", "separators": [ "U+0020", "U+0009", "U+000A", "U+000D U+000A" ], "lineComment": "semicolon-outside-string" }, "result": { "kind": "token-separation", "commentEndsAt": [ "defined-line-ending", "end-of-source" ], "literalContentPreserved": true }, "pendingCases": [ "The grammar and module contracts are fixed. Every product, engine, architecture, and resource boundary still needs direct execution." ] } ``` ### Ignore a comment between forms Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (+ input ; the supplied value 1))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The comment and separators leave an addition that returns the exact integer 42. Product invocation awaits its 2.0 adapter." } ``` The tab separates two tokens. The line comment ends before the second operand. ## Complete reader grammar ### EBNF · reader · complete · transcribed - language: `lispex` - languageVersion: `2.0` ```ebnf SourceBytes = { Utf8Scalar } ; Utf8Scalar = "00" .. "7F" | "C2" .. "DF" Continuation | "E0" "A0" .. "BF" Continuation | "E1" .. "EC" Continuation Continuation | "ED" "80" .. "9F" Continuation | "EE" .. "EF" Continuation Continuation | "F0" "90" .. "BF" Continuation Continuation | "F1" .. "F3" Continuation Continuation Continuation | "F4" "80" .. "8F" Continuation Continuation ; Continuation = "80" .. "BF" ; Document = Gap { Datum Gap } End ; Datum = List | Vector | Bytevector | Abbreviation | String TokenEnd | Character TokenEnd | Boolean TokenEnd | Number TokenEnd | Identifier TokenEnd ; List = "(" Gap [ Datum Gap { Datum Gap } [ "." TokenEnd Gap Datum Gap ] ] ")" ; Vector = "#(" Gap { Datum Gap } ")" ; Bytevector = "#u8(" Gap { Number TokenEnd Gap } ")" ; Abbreviation = "'" Gap Datum ; Gap = { White | LineComment | BlockComment | DatumComment } ; White = "U+0020" | "U+0009" | LineEnd ; LineEnd = "U+000A" | "U+000D" "U+000A" ; LineComment = ";" { !LineEnd Scalar } [ LineEnd ] ; BlockComment = "#|" { BlockComment | BlockScalar } "|#" ; BlockScalar = !( "#|" | "|#" ) Scalar ; DatumComment = "#;" Gap Datum ; Delimiter = White | "(" | ")" | "'" | "U+0022" | ";" | "#|" | "#;" ; TokenEnd = &( Delimiter | End ) ; End = "end-of-input" ; Identifier = BareIdentifier | BarredIdentifier ; BareIdentifier = ( Initial { Subsequent } ) - NumericCandidate - ReservedNumber - "." ; Initial = "A" .. "Z" | "a" .. "z" | "!" | "$" | "%" | "&" | "*" | "/" | ":" | "<" | "=" | ">" | "?" | "^" | "_" | "~" | "+" | "-" | "." | "@" ; Subsequent = Initial | DecimalDigit ; NumericCandidate = [ Sign ] ( DecimalDigit { Subsequent } | "." DecimalDigit { Subsequent } ) ; ReservedNumber = InexactWord | "+i" | "-i" ; InexactWord = "+inf.0" | "-inf.0" | "+nan.0" | "-nan.0" ; BarredIdentifier = "|" { BarredScalar | IdentifierEscape } "|" ; BarredScalar = Scalar - Control - "|" - "U+005C" ; IdentifierEscape = "U+005C" ( "|" | "U+005C" | ScalarEscape ) ; String = "U+0022" { StringScalar | StringEscape } "U+0022" ; StringScalar = Scalar - Control - "U+0022" - "U+005C" ; StringEscape = "U+005C" ( "U+0022" | "U+005C" | "n" | "r" | "t" | ScalarEscape ) ; ScalarEscape = "u{" HexDigits "}" ; HexDigits = HexDigit [ HexDigit [ HexDigit [ HexDigit [ HexDigit [ HexDigit ] ] ] ] ] ; Character = "#" "U+005C" ( CharacterName | ScalarEscape | CharacterScalar ) ; CharacterName = "space" | "newline" | "tab" | "return" | "null" ; CharacterScalar = Scalar - Control - "U+0020" ; Boolean = "#t" | "#f" ; Number = [ Sign ] DecimalMagnitude | "#d" [ Sign ] DecimalMagnitude | "#b" [ Sign ] BinaryMagnitude | "#o" [ Sign ] OctalMagnitude | "#x" [ Sign ] HexMagnitude ; Sign = "+" | "-" ; DecimalMagnitude = DecimalInteger [ "/" DecimalInteger ] | DecimalInteger "." [ DecimalInteger ] [ Exponent ] | "." DecimalInteger [ Exponent ] | DecimalInteger Exponent ; Exponent = ( "e" | "E" ) [ Sign ] DecimalInteger ; DecimalInteger = DecimalDigit { DecimalDigit } ; BinaryMagnitude = BinaryInteger [ "/" BinaryInteger ] ; BinaryInteger = BinaryDigit { BinaryDigit } ; OctalMagnitude = OctalInteger [ "/" OctalInteger ] ; OctalInteger = OctalDigit { OctalDigit } ; HexMagnitude = HexInteger [ "/" HexInteger ] ; HexInteger = HexDigit { HexDigit } ; BinaryDigit = "0" | "1" ; OctalDigit = "0" .. "7" ; DecimalDigit = "0" .. "9" ; HexDigit = DecimalDigit | "a" .. "f" | "A" .. "F" ; Control = "U+0000" .. "U+001F" | "U+007F" .. "U+009F" ; Scalar = "U+0000" .. "U+D7FF" | "U+E000" .. "U+10FFFF" ; ``` Imported productions: known; . Omitted productions: known; . | Notation | Meaning | | --- | --- | | `SourceBytes` | Match all submitted octets before scalar decoding | | Hex pairs in `Utf8Scalar` and `Continuation` | One octet or an inclusive octet range | | `U+` terminals | The indicated scalar value or inclusive scalar range | | Other quoted terminals | Literal scalar sequences | | `end-of-input` | A zero width test for the end of the decoded module | | `&` and `!` | Positive and negative lookahead without consumption | | `-` | Exclude the right operand from the language on the left | Use the longest complete atomic token. A token beginning with a decimal digit is numeric. A sign or dot followed by decimal digits also starts a numeric candidate. Radix prefixes commit to their numeric grammar. A malformed candidate cannot fall back to an identifier. The standalone dot is permitted only in a nonempty list before its single tail datum. Parentheses pair exactly. Brackets and braces have no alternate list meaning. | Input form | Decoded meaning or restriction | | --- | --- | | `\n`, `\r`, `\t` in a string | Line feed, carriage return, tab | | `\u{...}` | The hexadecimal scalar value | | A scalar escape in the surrogate range or above U+10FFFF | Reader failure | | Literal control scalars in strings or barred identifiers | Use an escape instead | | `||` | The empty identifier name | | `#\space`, `#\newline`, `#\tab`, `#\return`, `#\null` | U+0020, U+000A, U+0009, U+000D, U+0000 | | A direct character scalar after `#\` | Exactly one scalar followed by a token boundary | | `#b`, `#o`, `#d`, `#x` | Lowercase radix prefixes with a following optional sign | | A numeric rational | An unsigned nonzero denominator in the selected radix | | Decimal leading zeroes and hexadecimal letter case | Preserve the same exact numeric value | | `#e`, `#i`, `+inf.0`, `-inf.0`, `+nan.0`, `-nan.0`, `+i`, `-i` | Reader failure | | Complex tokens that begin as numeric candidates | Reader failure | | `#!`, `#lang`, a shebang, datum labels, backquote, comma | Reader failure outside literal text or comments | | A leading or repeated byte order mark | Reader failure | | Other whitespace and a lone carriage return | Reader failure outside literal text or comments | An escaped identifier and a literal identifier with the same decoded scalar sequence name the same binding. A barred numeric spelling is an identifier. It is not a number. Comment and radix prefixes are ordinary text where the literal grammar admits their characters. Block comment delimiters nest even when their surrounding comment text contains quote characters. A datum comment skips trivia before reading its one discarded datum. This includes nested datum comments. An unfinished comment, escape, string, list, or quoted datum fails reading. Syntax inside a discarded datum must still be complete. The quote prefix becomes the ordinary quote form during normalization. Lists, pairs, vectors, and bytevectors retain their element order. Decimal fractions and exponents reduce to the exact values defined by [Exact numbers](/v2.0/en/docs/language/numbers#lispex.rule.v2.numbers.decimal-value). The reader creates no cyclic datum. The reader checks an escape when its final scalar is read. It checks literal control scalars when they are read. Atomic token grammar and numeric value checks occur at the completed token. A bytevector element receives its integer and octet range checks before the next element is read. A malformed numeric token fails before its value checks. A zero denominator fails before a bytevector range check. If reading reaches source end, its end test reserves one read-step. ## Literals and surface forms A literal denotes an immutable value. Quoted names are symbols. Quoted lists are data. Decimal spelling denotes an exact number. [Exact numbers](/v2.0/en/docs/language/numbers) defines its arithmetic and rounding contracts. [Datum](/v2.0/en/docs/language/values#lispex.section.v2.values.datum) defines the data allowed at the rule boundary. ### Read numeric literals exactly Numeric literals follow the [exact arithmetic rule](/v2.0/en/docs/language/numbers#lispex.rule.v2.numbers.exact-arithmetic) and the [exact-only rule](/v2.0/en/docs/language/numbers#lispex.rule.v2.numbers.exact-only). Reading a decimal spelling uses the [decimal value contract](/v2.0/en/docs/language/numbers#lispex.rule.v2.numbers.decimal-value). **Why** The same source must denote the same value on every architecture. Decimal notation must retain the value that the author wrote. Claim: `lispex.claim.v2.source.exact-literals` · boundary · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "numeric-literal-reading", "forms": [ "integer", "rational", "decimal", "explicit-inexact" ] }, "result": { "kind": "exact-literal-values", "decimalExact": true, "implicitInexactConversion": false, "explicitInexact": "reject" }, "pendingCases": [ "The grammar and module contracts are fixed. Every product, engine, architecture, and resource boundary still needs direct execution." ] } ``` ### Add exact decimal literals Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (= (+ 0.1 0.2) 3/10))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The exact decimal sum equals three tenths and the rule returns true. Product invocation awaits its 2.0 adapter." } ``` The comparison checks exact arithmetic. Decimal representation and codec bytes remain separate contracts. ### Reject an inexact literal Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) #i0.1)) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Preparation rejects the explicitly inexact literal and the entry is not evaluated. Product invocation awaits its 2.0 adapter." } ``` The [reader mapping](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.source-prepare-mapping) uses read and source.token with reason unsupported-reader-prefix. Rejection does not convert this spelling to a supported float. ### Give literals exact values Strings and quoted identifiers use only the listed escapes. A scalar escape must name a Unicode scalar value. Every numeric token denotes an exact integer or a reduced rational. A decimal exponent scales by an exact power of ten. A rational denominator must be nonzero. Radix prefixes select the digit alphabet in the grammar. Numeric candidates that fail that grammar are errors. They cannot become identifiers. Bytevector elements must denote exact integers from 0 through 255. **Why** One lexical interpretation prevents malformed numbers from becoming accidental names. Exact literals give every product the same data before arithmetic or admission begins. Claim: `lispex.claim.v2.source.literal-spellings` · boundary · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "reader-literal-values", "grammar": "lispex.grammar.v2.source.reader" }, "result": { "kind": "exact-literal-decoding", "radices": [ "binary", "octal", "decimal", "hexadecimal" ], "prefixCase": "lowercase", "decimalExponent": "exact-power-of-ten", "signedDenominator": false, "zeroDenominator": "reject", "exactnessPrefixes": "reject", "nonfiniteSpellings": "reject", "unknownEscape": "reject", "scalarEscape": "one-to-six-hex-digits-valid-scalar", "bytevectorDomain": "exact-integer-octet" }, "pendingCases": [ "Every product, supported engine, architecture, and finite resource boundary needs direct execution." ] } ``` ### Read escaped scalars and delimiters Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (list "line\n\u{1F642}\\\"" #\u{1F642} '|a\|b|)))) ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "source.scm", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The result preserves the decoded newline, supplementary scalar, quote, backslash, and barred name. Product invocation awaits its 2.0 adapter." } ``` Escapes name Unicode scalar values. They do not normalize or case fold the result. ### Read exact values in every radix Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (list #b101 #o17 #x-ff #d+12 0.125 12e-1 #xA/F .5 1.)))) ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "source.scm", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Every spelling becomes its stated exact integer or reduced rational. Product invocation awaits its 2.0 adapter." } ``` The source scale and radix do not become observable numeric state. ### Read pair tails, vectors, and bytevectors Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) '((a . b) #(1 #t) #u8(0 255))))) ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "source.scm", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The quote returns its ordered pair, vector, and bytevector data. Product invocation awaits its 2.0 adapter." } ``` A dot denotes one list tail. Vectors and bytevectors have no dotted tail syntax. ### Reject malformed literal values Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `literal-rejections.json` ```lispex { "notation": "documentation-reader-cases", "cases": [ { "case": "unknown-string-escape", "source": "\"\\q\"", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-escape" } } }, { "case": "unknown-identifier-escape", "source": "|a\\n|", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-escape" } } }, { "case": "surrogate-escape", "source": "\"\\u{d800}\"", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-scalar" } } }, { "case": "out-of-range-escape", "source": "#\\u{110000}", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-scalar" } } }, { "case": "too-long-escape", "source": "\"\\u{0000000}\"", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-scalar" } } }, { "case": "raw-newline", "source": "\"a\nb\"", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "invalid-scalar" } } }, { "case": "binary-digit", "source": "#b102", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "invalid-number" } } }, { "case": "uppercase-prefix", "source": "#Xff", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "radix-decimal", "source": "#x1.2", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "invalid-number" } } }, { "case": "zero-denominator", "source": "1/0", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "zero-denominator" } } }, { "case": "signed-denominator", "source": "1/-2", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "invalid-number" } } }, { "case": "unfinished-exponent", "source": "1e+", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "invalid-number" } } }, { "case": "numeric-name", "source": "+12abc", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "invalid-number" } } }, { "case": "inexact-prefix", "source": "#i1.0", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "exactness-prefix", "source": "#e1", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "infinity", "source": "+inf.0", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "inexact-number" } } }, { "case": "nan", "source": "-nan.0", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "inexact-number" } } }, { "case": "complex", "source": "1+2i", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.number", "data": { "reason": "invalid-number" } } }, { "case": "octet-range", "source": "#u8(256)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-literal" } } }, { "case": "octet-fraction", "source": "#u8(1/2)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-literal" } } }, { "case": "invalid-discard-number", "source": "#; #i1.0", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-reader-prefix" } } }, { "case": "unit-imaginary", "source": "+i", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-literal" } } }, { "case": "octet-before-later-token", "source": "#u8(256 #b2)", "moduleName": "main", "diagnostic": { "phase": "read", "code": "source.token", "data": { "reason": "unsupported-literal" } } } ] } ``` File: `request.json` ```lispex { "notation": "documentation-request", "source": "literal-rejections.json", "rootModule": "main", "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "caseInput": "submit-each-listed-source-independently" } ``` Fixture inputs and environment: ```json { "entry": "literal-rejections.json", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Each malformed literal is rejected. No token is reinterpreted as an identifier. Product invocation awaits its 2.0 adapter." } ``` The text fixture lists independent source inputs. Hex octets describe exact submitted bytes. This notation is not a public input codec. ## Normalization Normalization follows the [canonical source construction](/v2.0/en/docs/tools/prepare#lispex.grammar.v2.prepare.prepared-records). That table defines the admitted rewrites and preserved semantic nodes. [Preparation](/v2.0/en/docs/tools/prepare#lispex.section.v2.prepare.resolved-program) resolves their references to lexical bindings. A normalizer preserves quoted data and follows the [evaluation rules](/v2.0/en/docs/language/evaluation). [Source maps](/v2.0/en/docs/tools/meaning-graph#lispex.section.v2.meaning-graph.source-maps) retain source positions for display. ### Preserve meaning through normalization Normalization preserves lexical bindings, literal values, evaluation order, and the first observable failure. A generated binding cannot capture a source reference. **Why** Surface syntax is a way to write the rule. Changing its spelling must not give the normalizer permission to change the rule being evaluated. Claim: `lispex.claim.v2.source.preserve-meaning` · structural · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "surface-normalization", "target": "resolved-program" }, "result": { "kind": "meaning-preservation", "preserves": [ "lexical-binding", "literal-value", "evaluation-order", "first-failure", "resource-event-order" ], "generatedBindingCapture": false }, "pendingCases": [ "Each surface form needs scope, evaluation count, first failure, and resource boundary cases in every product and supported engine." ] } ``` ### Read both quotation forms as data Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (equal? '(a b) (quote (a b))))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The two quoted lists have equal data and the rule returns true. Product invocation awaits its 2.0 adapter." } ``` Quotation preserves the symbols a and b as data. These spellings do not look up procedure bindings. ### Preserve a binding through conditional sugar Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (let ((saved input)) (cond (#f 0) (else saved))))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The conditional reads the surrounding saved binding and returns the exact integer 42. Product invocation awaits its 2.0 adapter." } ``` Lowering the conditional must preserve the surrounding lexical scope. ### Resolve only submitted source Source submission follows the [closed-bundle rule](/v2.0/en/docs/tools/prepare#lispex.rule.v2.prepare.closed-bundle). Reading or normalization cannot add a dependency outside that submitted bundle. **Why** A rule must use the source and library identities fixed by its request. Runtime discovery would introduce an unstated input and an external authority. Claim: `lispex.claim.v2.source.closed-source` · rejection · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "source-dependency-resolution", "phase": "prepare" }, "result": { "kind": "closed-source-resolution", "runtimeLoad": false, "runtimeEval": false, "externalDiscovery": false, "unresolvedDependency": "reject" }, "pendingCases": [ "The grammar and module contracts are fixed. Every product, engine, architecture, and resource boundary still needs direct execution." ] } ``` ### Reject runtime source loading Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (load "other.scm"))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The runtime load request fails without reading a file or accessing a network. Product invocation awaits its 2.0 adapter." } ``` The string names no granted capability. The source bundle determines which dependencies preparation can resolve. ## Preparation failures Reader and normalization failures use [source-bound preparation reports](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.source-bound-report). [Preparation and modules](/v2.0/en/docs/tools/prepare#lispex.section.v2.prepare.source-bundle) defines the closed bundle. The [entry](/v2.0/en/docs/language/procedures#lispex.section.v2.procedures.rule-entry) runs only after preparation succeeds. The [preparation diagnostic mapping](/v2.0/en/docs/diagnostics#lispex.rule.v2.cli-and-diagnostics.diagnostics.source-prepare-mapping) gives each failure its catalog identity and typed fields. ### Reject invalid source before evaluation A reader or normalization failure stops preparation before entry. Record it under the [source-bound preparation report rule](/v2.0/en/docs/profiles/receipt-and-replay#lispex.rule.v2.receipt-and-replay.source-bound-report). **Why** An invalid source cannot provide a valid program identity. Keeping the failure with its source preserves a useful diagnostic without inventing an evaluation. Claim: `lispex.claim.v2.source.source-bound-failure` · rejection · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "preparation-failure", "stages": [ "reader", "normalization" ] }, "result": { "kind": "source-bound-prepare-failure", "entryEvaluated": false, "valueCount": 0, "validProgramIdentity": false }, "pendingCases": [ "Multiple reader and normalization failures need the adopted first failure order. Every product, engine, and architecture needs exact source association cases." ] } ``` ### Reject an unfinished source form Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) input) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The unfinished form fails preparation and produces no rule result. Product invocation awaits its 2.0 adapter." } ``` The definition is complete. The enclosing module is unfinished, so reading fails before preparation can continue. ### Account for preparation separately Source decoding, reading, and normalization use the preparation account defined by [Resources](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.separate-phases). The [finite-limit rule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.finite-entrypoints) applies before any entry evaluation. **Why** Deep or large source can require work before any rule runs. A finite evaluation budget alone cannot bound that work. Claim: `lispex.claim.v2.source.finite-preparation` · boundary · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "source-preparation-resources", "operations": [ "read", "normalize" ] }, "result": { "kind": "finite-separate-preparation", "finite": true, "sharesEvaluationBudget": false, "exhaustion": "terminal-before-evaluation" }, "pendingCases": [ "Before, at, and after every preparation reservation need product cases once the cost model is frozen. All supported architectures and engines remain unexecuted." ] } ``` ### Stop when preparation has insufficient budget Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) input)) ) ``` File: `request.json` ```lispex { "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 limits below a required preparation reservation", "evaluate": "finite values sufficient for the identity rule" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "An insufficient preparation budget causes a terminal resource stop before entry evaluation. Product invocation awaits its 2.0 adapter." } ``` The request describes a relation to a required reservation. It does not freeze a numeric tariff or a default limit. ### Check a binding group before its children Preparation follows the [complete reading order](/v2.0/en/docs/language/source#lispex.rule.v2.source.read-before-normalize). Normalization visits forms in source order. It checks a binding group when that traversal reaches the group. The shallow checks finish before any initializer or body in that group is normalized. Each required check reserves its event before inspecting syntax. A refused reservation stops before that inspection. An observed error stops before any later reservation. The event and check tables below fix this order. The [reservation axis rule](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.atomic-axis-order) applies within each event. **Why** A complete group check gives each binding one static meaning. Local prechecks preserve the order of unrelated forms. Reservations bound the work needed to discover an error without moving a later event before that error. Claim: `lispex.claim.v2.source.preparation-order` · interaction · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "source-binding-precheck-order", "phase": "normalize", "traversal": "source-order" }, "result": { "kind": "local-precheck-before-children", "steps": [ "reserve-normalize-node", "reserve-and-check-group-envelope", "reserve-and-check-members-in-order", "reserve-and-publish-bindings", "normalize-initializers-and-body-in-order" ], "checksPerMember": [ "shape", "identifier", "duplicate", "recursive-lambda-head-when-required" ], "wholeModuleNestedPrepass": false, "letStarGroups": "one-binding-per-nested-scope", "reservationFailure": "before-own-inspection", "detectedError": "before-later-reservations" }, "pendingCases": [ "Every product and engine needs malformed group and reservation boundary execution. Concrete charges remain with the resource model freeze decision." ] } ``` | Event | Next operation | Order | | --- | --- | --- | | `prepare.decode-step` | Decode the next UTF-8 scalar or confirm source end | Complete the module before reading | | `prepare.read-step` | Inspect the next decoded scalar or confirm source end | Left to right with each scalar inspected once | | `prepare.read-enter` | Enter a list, vector, bytevector, quote, block comment, or datum comment | After its opening marker and before its contents | | `prepare.read-node` | Validate and construct a completed datum | Children before their containing datum | | `prepare.normalize-node` | Inspect the next source form | Source order with children after their parent checks | | `prepare.binding-check` | Inspect the group envelope or the next member check | Before that inspection | | `prepare.binding-publish` | Record a checked lexical binding | Member order after all group checks | Reading completes before normalization starts. Reader lookahead reuses scalars already inspected and adds no second read event. A nested marker selects its enter event before any child event. A closing marker is read before its completed datum event. A block comment has enter events and scalar events but no datum node. A completed atomic token reserves its node event before token and numeric value checks. Its bytevector element checks finish before reading the next element. Datum comments retain every event of their discarded datum. Each event reserves all required axes before its effect. Reader enter events include required frame capacity. These events follow the grammar rather than implementation scanner loops. A comment or discarded datum still requires its reading events. The resource model names the requirements for each event. Its coefficients and finite defaults follow the [cost model freeze](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers). | Check | Failure selection | | --- | --- | | Group envelope | Reject a malformed group before visiting a member | | Member shape | Reject the first malformed binding or parameter | | Identifier | Reject a binding position that is not an identifier | | Duplicate | Reject a repeated name in the same binding scope | | Recursive lambda head | Require the lambda head where recursive bindings require it | Run these member checks from left to right. Skip the lambda check for a nonrecursive binding. Stop at the first failed check. Parameter lists include their rest parameter in the same duplicate check. A parallel let, named let, letrec, or recursive definition group checks all members before descending. Each let* binding forms its own nested group. Its initializer is normalized before the next binding group. Publishing a binding records its identity. The [lexical scope rules](/v2.0/en/docs/language/evaluation#lispex.rule.v2.evaluation.lexical-scope) determine where that binding is visible. A parallel let initializer and a named let initializer retain their enclosing scope. All checks finish during preparation. They execute no guest initializer. ### Find a duplicate before an initializer error Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (let ((x (set! input 1)) (x 2)) x)))) ``` File: `request.json` ```lispex { "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The duplicate x is rejected before normalization enters the first initializer. Product invocation awaits its 2.0 adapter." } ``` The expected meaning is authored for Lispex 2.0. Product execution remains not-run. ### Check every recursive initializer head first Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (letrec ((f (lambda (x) (set! x 0))) (g 1)) f)))) ``` File: `request.json` ```lispex { "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The initializer of g is rejected before normalization enters the body of f. Product invocation awaits its 2.0 adapter." } ``` The expected meaning is authored for Lispex 2.0. Product execution remains not-run. ### Keep an earlier form ahead of a later group Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (begin (set! input 1) (let ((x 1) (x 2)) x))))) ``` File: `request.json` ```lispex { "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The earlier mutation form is rejected before the later binding group is inspected. Product invocation awaits its 2.0 adapter." } ``` The expected meaning is authored for Lispex 2.0. Product execution remains not-run. ### Reserve only the next required check Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (let ((x (set! input 1)) (x 2)) x)))) ``` File: `request.json` ```lispex { "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "reservationCases": [ { "case": "refuse-required-duplicate-check", "limits": "the work reservation for the second x duplicate check is refused" }, { "case": "permit-error-check-refuse-later-work", "limits": "all group checks fit but the first initializer normalization would be refused" } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "A refused check stops before discovering the duplicate. A discovered duplicate prevents every later reservation. Product invocation awaits its 2.0 adapter." } ``` The fixture selects symbolic reservation boundaries. It assigns no tariff coefficient or finite default. ### Keep sequential bindings in separate scopes Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (let* ((x 1) (x (+ x 1))) x)))) ``` File: `request.json` ```lispex { "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 for the stated checks", "evaluate": "finite values sufficient for the stated calculation" }, "requests": [ { "input": { "kind": "integer", "value": "0" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Each x belongs to a separate nested scope and the rule returns the exact integer 2. Product invocation awaits its 2.0 adapter." } ``` The expected meaning is authored for Lispex 2.0. Product execution remains not-run. See [Resource model numbers](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers). ### Read the complete module before normalization For one module, preparation decodes UTF-8 before reading syntax. Reading completes before normalization starts. A reader failure takes precedence over a normalization failure in that module. Normalization checks source forms in their written order. **Why** A fixed phase order makes the first failure reproducible. An earlier form with invalid meaning cannot hide a later reader failure in an unread part of the module. Each module follows a fixed preparation order. Claim: `lispex.claim.v2.source.read-before-normalize` · interaction · coverage partial · verification not-run - language: `lispex` - languageVersion: `2.0` ```json { "predicate": { "kind": "single-module-preparation-order", "resources": "sufficient-for-all-stated-checks" }, "result": { "kind": "preparation-order", "phases": [ "decode", "read", "normalize" ], "readerBeforeNormalizer": true, "normalizationForms": "source-order" }, "pendingCases": [ "Module ordering follows Preparation and modules. Every product and engine needs malformed source and resource boundary execution." ] } ``` ### Finish reading before checking recursive bindings Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (letrec ((x 1)) x))) ) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "The trailing closing parenthesis causes the reader failure before normalization can reject the recursive binding. Product invocation awaits its 2.0 adapter." } ``` The first form is readable but its letrec initializer is not a lambda. The later reader failure takes precedence. The diagnostic catalog gives this failure its phase, code, and typed reason. ### Check recursive forms in source order Mode: illustrative. Stage: semantic-request. Verification: not-run. - language: `lispex` - languageVersion: `2.0` File: `source.scm` ```lispex (module main (import) (export rule) (entry rule) (define rule (lambda (input) (begin (letrec ((x 1)) x) (letrec ((y 2)) y)))) ) ``` File: `request.json` ```lispex { "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" } } ], "rootModule": "main", "moduleSources": [ { "name": "main", "source": "source.scm" } ] } ``` Fixture inputs and environment: ```json { "entry": "source.scm", "argv": [], "stdin": "", "cwd": ".", "environment": [], "wrapper": null, "packageRef": null, "lockRef": null, "generatedBindingRefs": { "knowledgeState": "not-applicable", "values": [] } } ``` #### Expected result ```json { "status": "unspecified", "reason": "Normalization rejects the initializer of x before it reaches the initializer of y. Product invocation awaits its 2.0 adapter." } ``` Both forms violate the lambda requirement. The first form determines this failure. Finite preparation limits are sufficient to reach the stated checks. ## Related chapters [Values and text](/v2.0/en/docs/language/values) [Evaluation and bindings](/v2.0/en/docs/language/evaluation) [Preparation and modules](/v2.0/en/docs/tools/prepare) [Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay) ### Pending · Resource model numbers The 2.0 tariff coefficients, logical allocation units, bit-size accounting, detailed frame accounting, finite defaults, representation limits, and physical memory envelopes remain open. This includes preparation, calls, values, exact arithmetic, equality, text, record conversion, and canonical encoding. Profile host budget coefficients and defaults remain separate from language preparation and evaluation budgets. Trace capacity, reservation sizes, and host memory requirements retain their separate reporting scope. Each budget retains its own identity and accounting boundary. Implementation and attack tests must support these choices. [Resource event declarations](/v2.0/en/docs/language/resources#lispex.rule.v2.resources.event-catalog) and [native kernel membership](/v2.0/en/docs/library#lispex.pending.v2.standard-library.kernel-and-cost-model) remain separate contracts. ### Pending · Native kernel membership The final native kernel list and count remain open. Implementation and product attack tests must support these choices. [Tariff coefficients, allocation units, finite defaults, and physical envelopes](/v2.0/en/docs/language/resources#lispex.pending.v2.resources.model-numbers) are tracked once with the resource numbers. ## Related [Values and text](/v2.0/en/docs/language/values) [Evaluation and bindings](/v2.0/en/docs/language/evaluation) [Preparation and modules](/v2.0/en/docs/tools/prepare) [Identity, receipt, replay](/v2.0/en/docs/profiles/receipt-and-replay)