Skip to content
Topaz6.0 · Before release
Download

Search documentation

Specification 6.0 · Not released · Tested product 5.21.3

Use arrow keys to choose a result. Press Enter to open.

Type an API name, diagnostic number, rule, or project topic.

    Library · std.lispex

    LispexRequest

    Preserve the complete semantic request needed for exact replay.

    LispexRequest { identity: LispexIdentity, program: LispexIdentity, entry: string, input: LispexValue, contract: LispexSemanticContract, limits: LispexLimits }
    Receiver
    Not applicable
    Minimum arity
    0
    Maximum arity
    0

    Declaration and parameters

    Link

    Availability

    Included by default: no

    Import std.lispex from an application package with a verified lock. Packages with [lispex] require --locked. Application profile topaz/lispex-decision-application/1 uses evaluator profile lispex/r7rs-rule-embedded-core/1. Application profile topaz/lispex-decision-application/2 uses evaluator profile lispex/r7rs-rule-current-profile-bounded/1.

    The generated-module resolver gate starts at language mode 5.18. Compatibility of this API with earlier released editions remains Pending. Target deployment conditions are native (native-only), web (web-isolated-workers), web-worker (web-isolated-workers). Runtime payload follows checker-reached rules. An empty reached-rule set includes no runtime payload. Application quotas are required. Lock-only packages do not receive these application modules.

    Source evidence

    Receiver

    Not applicable

    Parameter constraints

    Additional contracts are Pending.

    LispexIdentity is a typed immutable identity in a versioned domain. Its domain identifies the contract under which its value is interpreted. Equality compares the domain and the complete identity value under that contract. Matching display text from different domains does not establish identity equality.

    Source identity identifies the exact submitted source bytes under the source contract. A source edit can change that identity while leaving canonical program identity unchanged. Source identity remains available for failures that occur before a canonical program exists.

    Program identity identifies the canonical resolved program under its fixed dependencies. Canonicalization identifies one resolved form. It does not establish arbitrary program equivalence from equal values on one or more inputs.

    Artifact identity identifies the exact bytes of an engine artifact under its artifact domain. It remains distinct from source and program identity. Two admitted engine artifacts can execute the same semantic request and produce the same canonical outcome.

    LispexRequest.identity binds the complete evaluation request. That request fixes the canonical program, selected entry, input Datum, language and library semantics, Unicode semantics, resource model, and finite evaluation limits. Changing any semantic input creates a different request even when the result remains equal.

    The request records effective limits after preset selection and before evaluation. Equal final values under different declared limits do not make the requests identical. A host cannot change the limits and preserve the original request identity.

    Preparation and evaluation retain their own requests and budgets. Preparation reuse, a warm cache, and source presentation do not change the identity or charges of the admitted evaluation request. A preparation report does not stand in for an evaluation request.

    Product, engine, platform, host paths, cache state, source layout, and display settings are outside the identity of an admitted semantic evaluation request. Their observations belong to source provenance or execution evidence as applicable.

    Profile work identity binds the submitted request data, versioned profile work contract, and separate finite host budget. The profile work contract identifies the profile, schemas, required evidence, and host check rules. Changing that contract or host budget changes profile work identity without altering the base preparation or evaluation request.

    Admission and later qualification or evidence reports retain the profile work identity of their submission. Each report cites only semantic identities already verified at its stage. An early refusal cannot manufacture a canonical input or program identity to complete its report.

    Lispex 2.0 records use new identity domains. Historical Lispex 1.x records retain their original domains and meanings. Reading a historical record never promotes its identity or execution observations into Lispex 2.0 evidence.

    Canonical Lispex value equality preserves exact mathematical numbers and raw Unicode scalar sequences. Aggregates compare their canonical kinds and ordered elements. Procedures, host references, physical storage identity, and floating point coercion do not participate in canonical value equality.

    Canonical settlement equality compares the complete successful value or complete structured failure. It does not compare source formatting, diagnostic wording, engine selection, runtime counters, or evidence issuer. Identity equality and settlement equality answer different questions.

    Inspection returns identity data already verified for the inspected object. Reading those fields performs no guest evaluation, fresh replay, network discovery, or authority acquisition. A caller supplied label cannot replace validation of an artifact or package identity.

    Identity domain tags, digest algorithms, and serialized inputs follow their selected Lispex 2.0 contracts. The Topaz binding neither derives them from current Lispex 1.x encodings nor assigns hashes to contracts whose encoding remains unresolved.

    LispexSemanticContract.standardLibrary names the selected library semantic contract. It is distinct from the standard library artifact bytes checked during package admission. The additional host profile selector belongs to LispexProfileRequest and profile work identity rather than the base semantic request.

    LispexRuleIdentity.source is Some of the exact submitted source identity when source provenance was verified and None for a transported rule without verified source provenance. program identifies the canonical resolved code. artifact identifies the prepared artifact bytes returned by preparedBytes. contract names the verified semantic contracts. The evaluator artifact identity remains separate package and execution evidence.

    LispexIdentity and LispexCanonicalSite are sealed values. Callers can compare them but cannot construct a verified identity or site from arbitrary text. Record inspections expose detached values and never change the sealed rule, request or artifact.

    The opaque identity type exposes equality rather than a constructor from text. Each named field states its identity domain. A dependency submission uses a manifest name and raw bytes so admission can establish its identity without a caller forging a verified value.

    Related rule: Identify source, programs, requests, artifacts, and profile work

    Result

    Pending

    Effects

    Pending

    Failures

    Pending

    Result and effects

    Link

    Preserve the complete semantic request needed for exact replay.

    Why

    Link

    The identities contract gives this operation one explicit input boundary and preserves the distinct result and failure cases.

    Related entries

    Link

    std.lispex

    Identify source, programs, requests, artifacts, and profile work

    Link
    Ruletopaz.stdlib.contract.lispex-identities.rule

    Identify source, programs, requests, artifacts, and profile work

    LispexIdentity is a typed immutable identity in a versioned domain. Its domain identifies the contract under which its value is interpreted. Equality compares the domain and the complete identity value under that contract. Matching display text from different domains does not establish identity equality.

    Source identity identifies the exact submitted source bytes under the source contract. A source edit can change that identity while leaving canonical program identity unchanged. Source identity remains available for failures that occur before a canonical program exists.

    Program identity identifies the canonical resolved program under its fixed dependencies. Canonicalization identifies one resolved form. It does not establish arbitrary program equivalence from equal values on one or more inputs.

    Artifact identity identifies the exact bytes of an engine artifact under its artifact domain. It remains distinct from source and program identity. Two admitted engine artifacts can execute the same semantic request and produce the same canonical outcome.

    LispexRequest.identity binds the complete evaluation request. That request fixes the canonical program, selected entry, input Datum, language and library semantics, Unicode semantics, resource model, and finite evaluation limits. Changing any semantic input creates a different request even when the result remains equal.

    The request records effective limits after preset selection and before evaluation. Equal final values under different declared limits do not make the requests identical. A host cannot change the limits and preserve the original request identity.

    Preparation and evaluation retain their own requests and budgets. Preparation reuse, a warm cache, and source presentation do not change the identity or charges of the admitted evaluation request. A preparation report does not stand in for an evaluation request.

    Product, engine, platform, host paths, cache state, source layout, and display settings are outside the identity of an admitted semantic evaluation request. Their observations belong to source provenance or execution evidence as applicable.

    Profile work identity binds the submitted request data, versioned profile work contract, and separate finite host budget. The profile work contract identifies the profile, schemas, required evidence, and host check rules. Changing that contract or host budget changes profile work identity without altering the base preparation or evaluation request.

    Admission and later qualification or evidence reports retain the profile work identity of their submission. Each report cites only semantic identities already verified at its stage. An early refusal cannot manufacture a canonical input or program identity to complete its report.

    Lispex 2.0 records use new identity domains. Historical Lispex 1.x records retain their original domains and meanings. Reading a historical record never promotes its identity or execution observations into Lispex 2.0 evidence.

    Canonical Lispex value equality preserves exact mathematical numbers and raw Unicode scalar sequences. Aggregates compare their canonical kinds and ordered elements. Procedures, host references, physical storage identity, and floating point coercion do not participate in canonical value equality.

    Canonical settlement equality compares the complete successful value or complete structured failure. It does not compare source formatting, diagnostic wording, engine selection, runtime counters, or evidence issuer. Identity equality and settlement equality answer different questions.

    Inspection returns identity data already verified for the inspected object. Reading those fields performs no guest evaluation, fresh replay, network discovery, or authority acquisition. A caller supplied label cannot replace validation of an artifact or package identity.

    Identity domain tags, digest algorithms, and serialized inputs follow their selected Lispex 2.0 contracts. The Topaz binding neither derives them from current Lispex 1.x encodings nor assigns hashes to contracts whose encoding remains unresolved.

    LispexSemanticContract.standardLibrary names the selected library semantic contract. It is distinct from the standard library artifact bytes checked during package admission. The additional host profile selector belongs to LispexProfileRequest and profile work identity rather than the base semantic request.

    LispexRuleIdentity.source is Some of the exact submitted source identity when source provenance was verified and None for a transported rule without verified source provenance. program identifies the canonical resolved code. artifact identifies the prepared artifact bytes returned by preparedBytes. contract names the verified semantic contracts. The evaluator artifact identity remains separate package and execution evidence.

    LispexIdentity and LispexCanonicalSite are sealed values. Callers can compare them but cannot construct a verified identity or site from arbitrary text. Record inspections expose detached values and never change the sealed rule, request or artifact.

    The opaque identity type exposes equality rather than a constructor from text. Each named field states its identity domain. A dependency submission uses a manifest name and raw bytes so admission can establish its identity without a caller forging a verified value.

    Why

    Source provenance, program meaning, submitted requests, engine bytes, and profile checks identify different objects. Equal results do not erase those distinct intents. Separate identities let callers change presentation or execution products while retaining the exact semantic request they intend to compare.

    Examples Repeat the same request and outcomeDistinguish requests with equal returned values

    Source evidence

    Repeat the same request and outcome

    Link

    run · running · Verification: not-run

    main.tpzRepeat the same request and outcomeOpen in Playground
    1. import std.bytes { Bytes }
    2. import std.io
    3. import std.test
    4. import std.lispex {
    5. LispexPackage,
    6. LispexBoundaryReport,
    7. LispexLimitPreset,
    8. LispexLimits,
    9. LispexSource,
    10. LispexSourceBundle,
    11. PreparedLispexRule,
    12. LispexPreparationError,
    13. LispexDatumView,
    14. LispexValue,
    15. LispexValueError,
    16. LispexEvaluation,
    17. LispexAttemptError,
    18. LispexSettlement,
    19. LispexRuleIdentity,
    20. inspectRule,
    21. applicationPackage,
    22. defaultLimits,
    23. prepare,
    24. valueFromDatum,
    25. canonicalBytes,
    26. evaluate,
    27. }
    29. export function main(args: Array<string>, stdin: string) -> Result<int, string> {
    30. let packageResult: Result<LispexPackage, LispexBoundaryReport> = applicationPackage()
    31. let application: LispexPackage = test.assertOk(packageResult)
    32. let preset: LispexLimitPreset = defaultLimits()
    33. let source: LispexSource = LispexSource {
    34. name: "source.scm",
    35. bytes: "(define rule (lambda (input) input))\n".encodeUtf8(),
    36. }
    37. let bundle: LispexSourceBundle = LispexSourceBundle {
    38. entryModule: "source.scm",
    39. entryBinding: "rule",
    40. sources: [source],
    41. }
    42. let prepared: Result<PreparedLispexRule, LispexPreparationError> = prepare(application, bundle, preset.preparation)
    43. let rule: PreparedLispexRule = test.assertOk(prepared)
    44. let identity: LispexRuleIdentity = inspectRule(rule)
    45. let converted: Result<LispexValue, LispexValueError> = valueFromDatum(application, LispexDatumView.Boolean(true), preset.host)
    46. let input: LispexValue = test.assertOk(converted)
    47. let firstAttempt: Result<LispexEvaluation, LispexAttemptError> = evaluate(rule, input, preset.evaluation)
    48. let first: LispexEvaluation = test.assertOk(firstAttempt)
    49. let secondAttempt: Result<LispexEvaluation, LispexAttemptError> = evaluate(rule, input, preset.evaluation)
    50. let second: LispexEvaluation = test.assertOk(secondAttempt)
    51. io.writeLine("{first.request.identity == second.request.identity}")
    52. match (first.settlement) {
    53. case Complete(left) => {
    54. match (second.settlement) {
    55. case Complete(right) => {
    56. let leftBytes: Bytes = canonicalBytes(left)
    57. let rightBytes: Bytes = canonicalBytes(right)
    58. io.writeLine("{leftBytes.toHex() == rightBytes.toHex()}")
    59. }
    60. case _ => io.writeLine("unexpected second outcome")
    61. }
    62. }
    63. case _ => io.writeLine("unexpected first outcome")
    64. }
    65. io.writeLine("{first.request.program == identity.program}")
    66. return Ok(0)
    67. }
    Expected outputexit 0
    true
true
true
    $ topaz run main.tpz --locked · target product 5.21.3
    Expected result

    Expected result

    Execution completes. Exit code 0.

    No stderr.

    Expected stdout
    1. true
    2. true
    3. true

    This exact example has not been executed.

    Run this source inside the verified Lispex application supplied through TOPAZ_LISPEX_APPLICATION. The example expects the Lispex 2.0 host contract.

    Source evidence

    Distinguish requests with equal returned values

    Link

    run · running · Verification: not-run

    main.tpzDistinguish requests with equal returned valuesOpen in Playground
    1. import std.bytes { Bytes }
    2. import std.io
    3. import std.test
    4. import std.lispex {
    5. LispexPackage,
    6. LispexBoundaryReport,
    7. LispexLimitPreset,
    8. LispexLimits,
    9. LispexSource,
    10. LispexSourceBundle,
    11. PreparedLispexRule,
    12. LispexPreparationError,
    13. LispexDatumView,
    14. LispexValue,
    15. LispexValueError,
    16. LispexEvaluation,
    17. LispexAttemptError,
    18. LispexSettlement,
    19. applicationPackage,
    20. defaultLimits,
    21. prepare,
    22. valueFromDatum,
    23. canonicalBytes,
    24. evaluate,
    25. }
    27. export function main(args: Array<string>, stdin: string) -> Result<int, string> {
    28. let packageResult: Result<LispexPackage, LispexBoundaryReport> = applicationPackage()
    29. let application: LispexPackage = test.assertOk(packageResult)
    30. let preset: LispexLimitPreset = defaultLimits()
    31. let source: LispexSource = LispexSource {
    32. name: "source.scm",
    33. bytes: "(define rule (lambda (input) #t))\n".encodeUtf8(),
    34. }
    35. let bundle: LispexSourceBundle = LispexSourceBundle {
    36. entryModule: "source.scm",
    37. entryBinding: "rule",
    38. sources: [source],
    39. }
    40. let prepared: Result<PreparedLispexRule, LispexPreparationError> = prepare(application, bundle, preset.preparation)
    41. let rule: PreparedLispexRule = test.assertOk(prepared)
    42. let converted: Result<LispexValue, LispexValueError> = valueFromDatum(application, LispexDatumView.Boolean(true), preset.host)
    43. let input: LispexValue = test.assertOk(converted)
    44. let otherResult: Result<LispexValue, LispexValueError> = valueFromDatum(application, LispexDatumView.Boolean(false), preset.host)
    45. let otherInput: LispexValue = test.assertOk(otherResult)
    46. let firstAttempt: Result<LispexEvaluation, LispexAttemptError> = evaluate(rule, input, preset.evaluation)
    47. let first: LispexEvaluation = test.assertOk(firstAttempt)
    48. let secondAttempt: Result<LispexEvaluation, LispexAttemptError> = evaluate(rule, otherInput, preset.evaluation)
    49. let second: LispexEvaluation = test.assertOk(secondAttempt)
    50. io.writeLine("{first.request.identity == second.request.identity}")
    51. match (first.settlement) {
    52. case Complete(left) => {
    53. match (second.settlement) {
    54. case Complete(right) => {
    55. let leftBytes: Bytes = canonicalBytes(left)
    56. let rightBytes: Bytes = canonicalBytes(right)
    57. io.writeLine("{leftBytes.toHex() == rightBytes.toHex()}")
    58. }
    59. case _ => io.writeLine("unexpected second outcome")
    60. }
    61. }
    62. case _ => io.writeLine("unexpected first outcome")
    63. }
    64. return Ok(0)
    65. }
    Expected outputexit 0
    false
true
    $ topaz run main.tpz --locked · target product 5.21.3
    Expected result

    Expected result

    Execution completes. Exit code 0.

    No stderr.

    Expected stdout
    1. false
    2. true

    This exact example has not been executed.

    Run this source inside the verified Lispex application supplied through TOPAZ_LISPEX_APPLICATION. The example expects the Lispex 2.0 host contract.

    Source evidence

    Menu

    Download