Reference implementation

Lispex Vouch

The first reference implementation of CSK.

Lispex Vouch is the first and reference implementation of CSK. It runs on the checked subset of the Lispex language, and now defines Vouch Bridge for conversion evidence emitted by external engines.

01Portable decision receipts
02Vouch Bridge
03Offline verify
04Rule-change replay

01
```
lispex run program.lspx
```
Run a program on the same WebAssembly reference core the playground uses. Receipt generation lives in the native Rust reference path, not in this CLI.
02
```
lispex verify receipt.json
```
Check an existing receipt offline with the published verifier. It inspects bytes and hashes without executing source. Exit 0 means the artifact holds.
03
```
lispex verify-bridge report.json
```
Check an external-engine conversion evidence report. The checker confirms the shape, bytes, linked hashes, and boundary lists.
04
```
lispex replay <corpus> --against <pin>
```
Compare a decision corpus against a version pin or receipt set, offline, and report every flip.

Vouch Bridge

Commercial conversion can leave public evidence.

Vouch Bridge is a public evidence format for engines that convert code outside Lispex. An engine runs its own pipeline and gates, then emits a report that binds source bytes, target bytes, engine identity, and linked proof hashes in a Vouch shape. The Lispex checker reads that report offline and confirms the shape and the byte bindings. It does not run the engine and does not judge whether the target code is correct.

Lena Engine performs the commercial conversion. Lispex Vouch supplies the public evidence shape and the checker boundary for the conversion evidence it emits.

lispex verify-bridge conversion.bridge.json

Verify a real receipt in your own terminal. The commands below run the published verifier, not a demo.

age-threshold.receipt.jsonDownload the receipt

{
  "boundary": {
    "attests": [
      "source-bytes",
      "profile-input-hash-binding",
      "canonical-core-v0-bytes",
      "meaning-graph-v0-hash-binding",
      "reference-transcript-bytes",
      "meaning-env-transcript-bytes",
      "lowered-subset-transcript-agreement"
    ],
    "excludes": [
      "semantic-equivalence",
      "independent-witness",
      "substrate-independence",
      "error-agreement",
      "input-provenance",
      "topaz-reporting",
      "full-cskernel-coverage",
      "target-code-generation",
      "private-implementation-detail"
    ]
  },
  "canonical": {
    "byte_len": 117,
    "hash": {
      "algo": "sha-256",
      "domain": "lispex/core-hash/v0",
      "hex": "0166138fc6f17a1ce016adcc8470a29a0e2d368dccab41ed1340211ecfd36c7b"
    },
    "status": "ok"
  },
  "comparison": {
    "blockers": [],
    "fault_class": null,
    "first_divergence": null,
    "reason": "transcript-bytes-equal",
    "status": "agree",
    "substrate": "shared-rust-reference"
  },
  "diagnostics": [],
  "differential_receipt": "csk.differential-receipt/v0",
  "engine": {
    "canonical_format": "lispex.core.canonical/v0",
    "commit": {
      "dirty": false,
      "hex": "1b19dcfe7b97db842a6850dd8d4bea1d8030c136",
      "vcs": "git"
    },
    "name": "lispex-rust-reference",
    "version": "1.3.8"
  },
  "graph": {
    "byte_len": 1514,
    "hash": {
      "algo": "sha-256",
      "domain": "csk/meaning-graph-hash/v0",
      "hex": "94a5e0e686d28601c20a4825ab97c3699cc19b226031ff701ee105f4c4f844c9"
    },
    "status": "ok"
  },
  "input": {
    "byte_len": 4,
    "datum": "(20)",
    "hash": {
      "algo": "sha-256",
      "domain": "csk/profile-input-hash/v0",
      "hex": "110af5fa552beb95424869a04b48937f7ebe323198aeb2dbb68c8e27f8966c28"
    },
    "name": "input",
    "path": "profile-gallery/decision-gallery/inputs/age-threshold.datum",
    "status": "bound"
  },
  "meaning_env": {
    "fault": null,
    "hash": {
      "algo": "sha-256",
      "domain": "csk/meaning-env-transcript-hash/v0",
      "hex": "f0dfd43e2b272c0ec36731090325f53e11b41d5b8a80ecc682355b83e158ac51"
    },
    "status": "ok",
    "steps": {
      "limit": 65536,
      "used": 9
    },
    "transcript": [
      "(decision allow)"
    ],
    "transcript_byte_len": 17
  },
  "reference": {
    "hash": {
      "algo": "sha-256",
      "domain": "lispex/runtime-hash/v0",
      "hex": "dafb01565d181ad602e7a31d83aede59aa10462cf4723daab00edfb49b007abb"
    },
    "status": "ok",
    "transcript": [
      "(decision allow)"
    ],
    "transcript_byte_len": 17
  },
  "source": {
    "byte_len": 78,
    "hash": {
      "algo": "sha-256",
      "domain": "lispex/source-hash/v0",
      "hex": "d5ca57e06197ed1dd0fbd2fdb3f82225492bca5c86a2f3858ff92670e4f79eac"
    },
    "path": "profile-gallery/decision-gallery/cases/age-threshold.lspx"
  }
}

npx lispex verify age-threshold.receipt.json
receipt is artifact-consistent
# verify-report: "status": "pass" · exit 0

# flip one hex nibble in the receipt, then verify again
npx lispex verify tampered.receipt.json
receipt is not artifact-consistent
- meaning-env-hash-mismatch
# exit 1

The verify button runs the exact verifier file published in the lispex package on npm, byte for byte, inside the browser.