diff --git a/.github/workflows/standards-build.yml b/.github/workflows/standards-build.yml new file mode 100644 index 000000000..8a13bc820 --- /dev/null +++ b/.github/workflows/standards-build.yml @@ -0,0 +1,152 @@ +name: standards workspaces build + test + +# Build gate for every Rust workspace in the repo. +# +# It started as three. Then a toolchain bump compiled the rest for the first +# time and found FIVE more that did not build — smart-byte (47k LOC), openpay +# (six separate breakages across five crates), eoc, mesh and joule-ui — all +# broken by the same handful of upstream migrations (hmac -> KeyInit, reqwest +# feature-gating, cipher 0.4 -> 0.5, a struct gaining fields), and all invisible +# because nothing ever compiled them. Partial coverage is how that happens, so +# the matrix now covers everything. +# +# The original case, still the clearest: smart-byte-rs had never been compiled by +# anything, and it did not build. A single wrong `rand` pin — 0.10 against code +# written for 0.8, whose crypto stack requires rand_core 0.6 — silently disabled +# the entire identity pillar, BBS+ included. `cargo check` would have caught it +# on day one. An unbuilt standard is not a standard, so this workflow is the +# floor under every claim the specs make. +# +# One workflow with a matrix rather than sixteen files: the bootstrap step is +# identical everywhere, and a shared dependency change should rebuild all of +# them anyway. `fail-fast: false` so one red workspace does not mask the others. + +on: + push: + branches: [main] + pull_request: + +# Deliberately NO `paths:` filter. +# +# The first attempt used `**/*.rs` and `**/Cargo.toml`, and the workflow then +# silently did not fire — pushes touching exactly those files triggered other +# workflows but not this one, so `**`-prefixed globs evidently do not match here +# the way they do on GitHub. A build gate that quietly fails to run is worse than +# no gate at all: it reports nothing and everyone assumes green. +# +# This is the repo-wide floor, so it runs on every push and every PR. The cost is +# CI minutes on doc-only changes. The alternative cost is what this branch spent +# a day fixing — five workspaces silently broken because nothing compiled them. + +jobs: + build: + name: ${{ matrix.name }} + # Spread across the fleet's runners rather than pinning every job to `linux`. + # For most of these the runner is a capacity choice, not a correctness one — + # and 17 jobs on a single runner queue behind whatever else is using it. + # `jouleclaw-rs` is the exception: see its matrix entry. + runs-on: ${{ matrix.runner }} + strategy: + fail-fast: false + matrix: + include: + - { name: jcp-rs, dir: jcp/jcp-rs, runner: linux } + - { name: sandbox-rs, dir: sandbox/sandbox-rs, runner: linux } + - { name: smart-byte-rs, dir: smart-byte/smart-byte-rs, runner: linux } + - { name: openpay, dir: openpay, runner: linux-arm64 } + - { name: joule-code-rs, dir: joule-code/joule-code-rs, runner: linux-arm64 } + - { name: map-rs, dir: map/map-rs, runner: linux-arm64 } + - { name: aac-rs, dir: aac/aac-rs, runner: linux-arm64 } + - { name: joulecontract-rs, dir: joulecontract/joulecontract-rs, runner: linux-arm64, z3: true } + - { name: jouledesk-rs, dir: jouledesk/jouledesk-rs, runner: macos } + - { name: arl-rs, dir: arl/arl-rs, runner: macos } + - { name: sense-rs, dir: sense/sense-rs, runner: macos } + - { name: proof-rs, dir: proof/proof-rs, runner: linux, z3: true } + - { name: joulehook-rs, dir: joulehook/joulehook-rs, runner: macos } + - { name: eoc-rs, dir: eoc/eoc-rs, runner: linux } + - { name: mesh-rs, dir: mesh/mesh-rs, runner: linux-arm64 } + - { name: joule-ui-rs, dir: joule-ui/joule-ui-rs, runner: macos } + # jouleclaw-rs is the one entry whose runner IS a correctness choice. + # It reaches candle → ug → gemm, which uses inline aarch64 assembly + # (`fmla {0:v}.8h, ...`) requiring the ARMv8.2 FP16 extension. + # `aarch64-apple-darwin` carries target_feature="fp16" in its baseline + # because Apple Silicon guarantees it; `aarch64-unknown-linux-gnu` + # baselines at ARMv8.0-A and does not, so the same asm fails to + # ASSEMBLE — a codegen error `cargo check` never reaches. Verified on a + # native arm64 Linux container (rustc 1.98.0): without the flag, 12 + # errors; with it, 4457 tests pass. + # + # CAPACITY: this is by far the largest entry — its target tree is + # ~16 GB, against a 120 GB volume on tx-dev-linux-arm64 that already + # holds ~74 GB of other workspaces' caches. If linux-arm64 jobs start + # failing for no apparent reason, check `df -h /mnt/lima-colima-txarm` + # on the txarm VM before suspecting the code: a full cache volume + # fails whatever happens to be building, not whatever changed. + - { name: jouleclaw-rs, dir: jouleclaw/jouleclaw-rs, runner: linux-arm64, rustflags: "-C target-feature=+fp16" } + steps: + - uses: actions/checkout@v5 + + # Two workspaces shell out to `z3`, and the runner image has no solver. + # + # This step used to be load-bearing for correctness: without a solver the + # ladder escalated past its real rungs into a model STAND-IN that reported + # Proved, so every goal on a solverless machine came back proved. That is + # now fixed at the source — the real ladders hold decision procedures only + # and an absent rung yields Unproved (proof-solvers `ladder_is_sound` and + # `ladder_never_fabricates_a_proof_when_a_rung_is_absent`). + # + # So the suites pass with or without z3, and this step is kept purely for + # COVERAGE: with a solver present the real T1 rung actually runs, and the + # SMT paths are exercised rather than skipped. The absent-rung semantics + # stay covered either way — that regression test uses a goal z3 cannot + # parse, so it asserts the same thing on a machine that has one. + # + # Both z3 jobs are pinned to Linux runners deliberately: the macOS runner is + # a host executor with no apt. `sudo` may or may not exist depending on + # whether the container runs as root, so fall back to a bare invocation. + - name: Install z3 + if: matrix.z3 + shell: bash + run: | + SUDO=""; [ "$(id -u)" -ne 0 ] && SUDO="sudo" + $SUDO apt-get update -qq + $SUDO apt-get install -y -qq z3 + z3 --version + + # The docker runner image ships no Rust at all, so rustup is bootstrapped + # here. dtolnay/rust-toolchain cannot be used: it shells out to `rustup`, + # which the image lacks. Harmless where cargo already exists. + - name: Install Rust (workspace pin) + shell: bash + run: | + export PATH="$HOME/.cargo/bin:$PATH" + command -v rustup >/dev/null 2>&1 || \ + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + + - name: Cache cargo registry + target + uses: actions/cache@v4 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + ${{ matrix.dir }}/target + key: standards-${{ matrix.name }}-${{ hashFiles(format('{0}/Cargo.lock', matrix.dir), 'rust-toolchain.toml') }} + restore-keys: | + standards-${{ matrix.name }}- + + # --all-targets is load-bearing: a plain `cargo check` does not build test + # targets, and smart-byte's dev-dependencies drifted independently of its + # normal ones (rand_chacha 0.10 against rand 0.8). The library compiled + # while the tests did not. + - name: Check (all targets) + working-directory: ${{ matrix.dir }} + env: + RUSTFLAGS: ${{ matrix.rustflags }} + run: cargo check --workspace --all-targets + + - name: Test + working-directory: ${{ matrix.dir }} + env: + RUSTFLAGS: ${{ matrix.rustflags }} + run: cargo test --workspace diff --git a/jcp/conformance/v1/action_receipt.json b/jcp/conformance/v1/action_receipt.json new file mode 100644 index 000000000..b030cdc23 --- /dev/null +++ b/jcp/conformance/v1/action_receipt.json @@ -0,0 +1,379 @@ +{ + "vectors": [ + { + "core_hex": "b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590422b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458401ea0820e7bd612d95b106aed237731422872f7f8fb6f5ea6304c9001bfd1bfcb12d78b3744cad517085786986965a556f5b74fa951322cf41c57e2994f02bf0b", + "expect": "verify", + "id_hex": "c5b0e62aecf6bab69a0434216fa989a9d1935a299a50dd48855743071f7eb580", + "name": "reversible-local", + "note": "Read-modify-write resolved on-device. Nothing left the machine, so egress is `none` with zero bytes.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a265636c617373646e6f6e656674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a059038bb1647469657262533566656666656374a265636c617373646e6f6e656674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458405acb134e4267a5e8e0909dd36cc41194f5c0b796e36039f8d39108e7f9e9619dc5acdeb45368ee620d9f3c15f7f3f919e10bb656e4793e1d1a03abd23825320b", + "expect": "verify", + "id_hex": "318270be152d0a33ed88c8de6ae622ba12d019703c56554f8e347f32fc2f4da8", + "name": "read-only", + "note": "A query that changed nothing. Safe to replay; no before/after state to record.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "class": "none", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736b636f6d70656e7361626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626b636f6d70656e7361746f7278406561626436306166366361303332336436396161633538666639346262313538616133643862356337616133363633303231373138663264396439396338636166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590471b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736b636f6d70656e7361626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626b636f6d70656e7361746f7278406561626436306166366361303332336436396161633538666639346262313538616133643862356337616133363633303231373138663264396439396338636166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e745840808826b8524ace60d9f2cbb24abc8b284ab8d1181429c65b952f88a37424da5b31e6c4e3dc16bd079a200806b92ecfd26dc86b2e8c3abcfbbb31b19132889b06", + "expect": "verify", + "id_hex": "8843e43c0f4591985d9d96c5ad319d63fca7c4baaca3af7bcd606f2cc6835b9b", + "name": "compensable-with-compensator", + "note": "Cannot be undone, but the grant that could compensate is named at the time of acting — not discovered afterwards.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "compensable", + "compensator": "eabd60af6ca0323d69aac58ff94bb158aa3d8b5c7aa3663021718f2d9d99c8ca", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736c697272657665727369626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626c706c616e5f7265636569707478406466383635316564316434653064356264393936623963363337323531316432373136396265333363336237386237393334336636376531346665636462393166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590473b1647469657262533566656666656374a565616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736c697272657665727369626c65666265666f7265784062626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262667461726765747840643733376233653539376632353233346234616563373134393366313133653435363061336135633937306431366237393130363961363233643331343233626c706c616e5f7265636569707478406466383635316564316434653064356264393936623963363337323531316432373136396265333363336237386237393334336636376531346665636462393166656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458409fc1a7362b97f0ce75f2e2afb695e4ac78567bc3ef4af4c3e935ea9c64a77912959bdc1870c5f052ba992aced3eff720a232344130b025de11c094e5af443f04", + "expect": "verify", + "id_hex": "f84610524e627953f2023e4af155958c61861e530f3e4dcdcfe030d515c836be", + "name": "irreversible-with-plan", + "note": "An irreversible commit carrying the plan receipt that preceded it. This is the only shape in which `irreversible` is well-formed.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "irreversible", + "plan_receipt": "df8651ed1d4e0d5bd996b9c6372511d27169be33c3b78b79343f67e14fecdb91", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a3647065657278403135643161323961656661653564646337323437633438356437613539306538376635616633343034626130333163653031386630386230386236316633306365627974657319100065636c6173737061747465737465645f656e636c617665677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590477b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a3647065657278403135643161323961656661653564646337323437633438356437613539306538376635616633343034626130333163653031386630386230386236316633306365627974657319100065636c6173737061747465737465645f656e636c617665677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458403695157a344c7aa68dc768507a195225d1a6fa4d843a5e6a4969fb421d600c94718da5ae12a09780cb4093b0e676c1fe7425e1a523da33cfa64b91459bbc7805", + "expect": "verify", + "id_hex": "aee95ef630da5356efb75c8cd40b029eefd5023a8014e257f218b5ed1e87cdd2", + "name": "egress-attested-enclave", + "note": "Work left the device to somewhere that proved what it was running. The peer attestation is bound in the receipt.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 4096, + "class": "attested_enclave", + "peer": "15d1a29aefae5ddc7247c485d7a590e87f5af3404ba031ce018f08b08b61f30c" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533066656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319200065636c6173736b74686972645f7061727479677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e6768736f667477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a059042bb1647469657262533066656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319200065636c6173736b74686972645f7061727479677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e6768736f667477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e74584048e3a978439989c20d7ad5122f1d35fb4e50afae506c7b19a65c9d6b03781888de9e7bf2d1fbda44c1816cec11dc3d6a8ca6fa980cb0c141428777f6b0bce006", + "expect": "verify", + "id_hex": "cb9cb90ed902a8ede09ee56e57f76ab10e3f50f88915c11ea8868150aae24b33", + "name": "egress-third-party-honest", + "note": "An unattested destination, honestly recorded rather than upgraded. Trust is not an egress class.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 8192, + "class": "third_party" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "software", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S0", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "core_hex": "b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a00124f806a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e636569457374696d61746f72", + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590424b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a00124f806a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e636569457374696d61746f725840e3b4480fdddf8664bc505b94d1597fda6e391234be07435ae9e11ffefa646c7013d57d75f1f05613a897c9f55f8f0e28824ca4d7b6dde814dcc45a8295963d06", + "expect": "verify", + "id_hex": "37ad6db4defd7ec0e248cc5cdacc61a16f962aa5adba9bdee0dd0f8989356c1f", + "name": "estimated-energy", + "note": "Energy from an estimator, not a hardware counter. `HwShunt` and `Estimator` are different claims and must never collapse into one number.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "Estimator", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 1200000, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590424b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736c697272657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a26562797465730065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e7458406c575b828bc2baea9c27d8e4cf60fbd17a6961bb75f8927ee19d0b4e3b1a5e6b43731523c13f819023bf8af5bc29afa405b57cf379f737f75ccc2582a84ad90a", + "expect": "reject:irreversible-without-plan", + "name": "irreversible-without-plan", + "note": "Correctly signed, structurally invalid: an irreversible effect with no plan receipt. A verifier that only checks signatures accepts this.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "irreversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 0, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590424b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319100065636c617373646e6f6e65677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e745840d2c9adfe8cd2c27cf19d717f2fc1357cbfa949bda511e76cd2e407d0aa326e159931c9142cb0d1510f70f715f6f99fb6f755ca02c63ab3f2d62cb4cd6f3e330c", + "expect": "reject:egress-none-with-bytes", + "name": "egress-none-with-bytes", + "note": "Claims nothing left the device while counting 4096 bytes that did. The claim is falsified by its own byte count.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 4096, + "class": "none" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + }, + { + "envelope_hex": "d284581ea201270458186469643a6578616d706c653a61722d7265666572656e6365a0590430b1647469657262533566656666656374a465616674657278406363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636363636365636c6173736a72657665727369626c65666265666f72657840626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626262626674617267657478406437333762336535393766323532333462346165633731343933663131336534353630613361356339373064313662373931303639613632336433313432336266656772657373a265627974657319100065636c6173737061747465737465645f656e636c617665677374657761726478186469643a6578616d706c653a61722d7265666572656e6365677665726469637465616c6c6f77686772616e745f696478403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376169636861696e5f6964738278403638356362636634396464346232316530616264383766376563353233346664373765373937306434653762386235643464356237383961616461616538376178403938663862363936613365383733306163343236393431383538663134333066386135633466616631343861636439613635346639626430653565353835393969636c6f7365645f617474323032362d30382d32355431323a30303a30305a6967726f756e64696e67686861726477617265696a6f756c65735f756a1a012a21686a61725f726563656970746a61722f312d64726166746a696e7075745f686173687840616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616161616c776f726b5f726563656970747840663234393233393436356434386237366265313538636532366630383237636563353739666334396265383330303237353064353538376636306164353634666d70726f6f665f63656c6c5f69647840396637356165393638333165653062653663316238653930633863613535633664343564653361633838333237353831663361623865393030666332626132666e6174746573746174696f6e5f696478403439656632363965623033343833636334666465396239336666333134363530623331333765396333373331616161653366306265363636653663643937623971617574686f726974795f7265636569707478406134366235393539353665313963613132623039363962396666616331383165383861636533323764363164323761643334366466383661663063613133636371656e657267795f70726f76656e616e63656748775368756e745840c81d8fe4462d5834f802bd0a0d7c11a547f488dd237a941df6cbf0bae37d58ec6d225ff22b1517e03a48b9495eb46192c4787652e3e3219fb18bcf0c9cdc8009", + "expect": "reject:attested-egress-without-peer", + "name": "attested-egress-without-peer", + "note": "Claims an attested destination with no peer attestation to bind. The router may not claim a stronger class than its evidence supports.", + "wire": { + "ar_receipt": "ar/1-draft", + "attestation_id": "49ef269eb03483cc4fde9b93ff314650b3137e9c3731aaae3f0be666e6cd97b9", + "authority_receipt": "a46b595956e19ca12b0969b9ffac181e88ace327d61d27ad346df86af0ca13cc", + "chain_ids": [ + "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "98f8b696a3e8730ac426941858f1430f8a5c4faf148acd9a654f9bd0e5e58599" + ], + "closed_at": "2026-08-25T12:00:00Z", + "effect": { + "after": "cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "before": "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", + "class": "reversible", + "target": "d737b3e597f25234b4aec71493f113e4560a3a5c970d16b791069a623d31423b" + }, + "egress": { + "bytes": 4096, + "class": "attested_enclave" + }, + "energy_provenance": "HwShunt", + "grant_id": "685cbcf49dd4b21e0abd87f7ec5234fd77e7970d4e7b8b5d4d5b789aadaae87a", + "grounding": "hardware", + "input_hash": "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "joules_uj": 19538280, + "proof_cell_id": "9f75ae96831ee0be6c1b8e90c8ca55c6d45de3ac88327581f3ab8e900fc2ba2f", + "steward": "did:example:ar-reference", + "tier": "S5", + "verdict": "allow", + "work_receipt": "f249239465d48b76be158ce26f0827cec579fc49be83002750d5587f60ad564f" + } + } + ] +} diff --git a/jcp/conformance/v1/action_receipt_meta.json b/jcp/conformance/v1/action_receipt_meta.json new file mode 100644 index 000000000..f9f2c7c59 --- /dev/null +++ b/jcp/conformance/v1/action_receipt_meta.json @@ -0,0 +1,9 @@ +{ + "alg": "EdDSA (COSE -8)", + "negatives": 3, + "note": "Fixture key, published deliberately so third parties can verify. Never use it for anything real.", + "positives": 7, + "profile": "ar/1-draft", + "pubkey_hex": "197f6b23e16c8532c6abc838facd5ea789be0c76b2920334039bfa8b3d368d61", + "steward": "did:example:ar-reference" +} diff --git a/jcp/jcp-rs/Cargo.lock b/jcp/jcp-rs/Cargo.lock index 22204c44d..7c0c0ffcb 100644 --- a/jcp/jcp-rs/Cargo.lock +++ b/jcp/jcp-rs/Cargo.lock @@ -503,6 +503,23 @@ dependencies = [ "thiserror 2.0.20", ] +[[package]] +name = "jcp-action-receipt" +version = "0.1.0" +dependencies = [ + "ed25519-dalek", + "hex", + "jcp-grant", + "jcp-receipt", + "jcp-runtime", + "jcp-schema", + "sandbox-meter", + "sandbox-schema", + "serde", + "serde_json", + "thiserror 2.0.20", +] + [[package]] name = "jcp-bridge" version = "0.1.0" diff --git a/jcp/jcp-rs/Cargo.toml b/jcp/jcp-rs/Cargo.toml index c413f9104..d82761317 100644 --- a/jcp/jcp-rs/Cargo.toml +++ b/jcp/jcp-rs/Cargo.toml @@ -5,6 +5,7 @@ members = [ "crates/jcp-grant", "crates/jcp-runtime", "crates/jcp-receipt", + "crates/jcp-action-receipt", "crates/jcp-bridge", "crates/jcp-energy", "crates/jcp-wire", @@ -37,6 +38,7 @@ jcp-schema = { path = "crates/jcp-schema" } jcp-grant = { path = "crates/jcp-grant" } jcp-runtime = { path = "crates/jcp-runtime" } jcp-receipt = { path = "crates/jcp-receipt" } +jcp-action-receipt = { path = "crates/jcp-action-receipt" } jcp-bridge = { path = "crates/jcp-bridge" } jcp-energy = { path = "crates/jcp-energy" } diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml new file mode 100644 index 000000000..0fe61c3e0 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "jcp-action-receipt" +version.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true +repository.workspace = true +description = "Action Receipt (AR-1) — the composition envelope binding authority, environment, work and effect into one verifiable artifact. Introduces no new cryptography: canonical det-CBOR and COSE_Sign1 are reused verbatim from JCR-1. Binds by content-id so each existing receipt family keeps its own encoding and signer." + +[dependencies] +jcp-schema = { workspace = true } +jcp-receipt = { workspace = true } +ed25519-dalek = { workspace = true } +serde = { workspace = true } +serde_json = { workspace = true } +hex = { workspace = true } +thiserror = { workspace = true } + +[dev-dependencies] +hex = { workspace = true } +jcp-receipt = { workspace = true } +jcp-grant = { workspace = true } +jcp-runtime = { workspace = true } +sandbox-meter = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-meter" } +sandbox-schema = { path = "../../../../sandbox/sandbox-rs/crates/sandbox-schema" } diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md b/jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md new file mode 100644 index 000000000..9c00c7cba --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/docs/AR-1-spec.md @@ -0,0 +1,208 @@ +# Action Receipt Specification (AR-1) — Draft + +**Status:** Draft. Profile tag `ar/1-draft`. Field names are settled against the +existing canonical projections; the tag becomes `ar/1` when the vector pack has +been reviewed. + +**Conformance pack:** `jcp/conformance/v1/action_receipt.json`, +`action_receipt_meta.json` — 7 positive and 3 negative vectors, signed with a +published fixture key. + +--- + +## 0. Why this exists + +Three receipt families already ship in this tree. Each records one quarter of +what an audit actually asks for, and **none of them binds to the others**: + +| Family | Records | Carries | +|---|---|---| +| `jcp-receipt` | authority | grant chain, verdict, budget drawn | +| `sandbox-proof` | environment | attestation, isolation tier, substrate | +| JCR-1 | work | input hash, measured joules, energy provenance | +| *(nothing)* | **effect** | what changed, and whether it can be undone | + +So no single artifact answers: *under what authority did this agent do that, +where did it run, what did it cost, and what did it change?* + +The receipt encoding is implemented six independent times across the tree. That +is evidence the **encoding** is portable, and evidence the **composition** was +never specified. AR-1 specifies it. + +Two of the three families already gesture at the chain — the sandbox proof cell +carries a `receipt_id`, the authority receipt carries a `payload_hash`. The +intent was there. The binding was not. + +## 1. Design invariants + +1. **Envelope, not replacement.** Each family keeps its own canonical encoding + and its own signer. AR-1 reaches into them by content-id; they never reach + back. Every existing verifier continues to work unchanged. +2. **No new cryptography.** Canonical det-CBOR (RFC 8949 §4.2.1) and the tagged + COSE_Sign1 envelope are reused verbatim from JCR-1. If AR-1 ever appears to + need a novel primitive, the design has gone wrong. +3. **Refusal over record-keeping.** A format that merely records claims is a + log. AR-1 defines three shapes that MUST be refused at verification, so a + violation is *detectable* rather than a matter of trust. +4. **Never claim beyond the evidence.** Every field that asserts a property must + be falsifiable from the receipt itself or from an artifact it binds. + +## 2. The signed core + +Canonical projection, det-CBOR encoded, signed as COSE_Sign1 with EdDSA +(COSE `alg` −8). Absent optional fields are **omitted, not nulled** — JCR-1 §3.1 +drops nulls from the signed core, so an emitted null would not round-trip. + +``` +ActionReceipt { + ar_receipt: "ar/1-draft" // profile tag + closed_at: Timestamp // RFC 3339 + + // binding 1 — authority + grant_id: ContentId + chain_ids: [ContentId]? // root first; omitted when empty + authority_receipt: ContentId + verdict: "allow" | "deny" + + // binding 2 — environment + attestation_id: ContentId + proof_cell_id: ContentId? + tier: "S0".."S7" + grounding: "hardware" | "software" + + // binding 3 — work + work_receipt: ContentId + input_hash: Hash + joules_uj: u64 + energy_provenance: "HwShunt" | "ModelBased" | "Estimator" + + // binding 4 — effect (new; nothing else records this) + effect: { + class: "none" | "reversible" | "compensable" | "irreversible" + target: ContentId + before: Hash? + after: Hash? + compensator: ContentId? + plan_receipt: ContentId? + } + + // binding 5 — egress (the router's per-request privacy contract) + egress: { + class: "none" | "attested_enclave" | "third_party" + bytes: u64 + peer: ContentId? + } + + steward: String // REQUIRED, as in JCR-1 §2.1 +} +``` + +**Receipt id** = BLAKE3 over the canonical signed core. + +### 2.1 `grounding` is carried, never upgraded + +`grounding` reports whether the bound attestation is rooted in silicon or in +software. It is copied verbatim from that attestation. An implementation MUST +NOT promote `software` to `hardware` under any circumstance — the field exists +precisely so that a software-rooted claim stays legible as one. + +### 2.2 `energy_provenance` never collapses + +`HwShunt`, `ModelBased` and `Estimator` are three different claims about how a +joule figure was obtained. An implementation MUST NOT sum or average across +them into a single undifferentiated number. A measured figure and an estimated +one are not interchangeable, and a receipt that treats them as such is lying by +arithmetic. + +## 3. The three rules + +These MUST be enforced at verification, re-derived from the wire projection — +**not** from a caller-supplied struct. A receipt hand-forged to violate them +signs correctly and must be rejected anyway. The negative vectors in the pack +exist to prove an implementation does this. + +| # | Rule | Rationale | +|---|---|---| +| 1 | `effect.class == "irreversible"` REQUIRES `effect.plan_receipt` | The cascade's body-tier design already separates plan from commit for actions that touch the world. AR-1 binds that discipline into the evidence: an irreversible commit with no preceding plan is a protocol violation, not a missing nicety. | +| 2 | `egress.class == "none"` REQUIRES `egress.bytes == 0` | A claim that nothing left the machine is falsified by its own byte count. | +| 3 | `egress.class == "attested_enclave"` REQUIRES `egress.peer` | The router may never claim a stronger class than it can bind evidence for. An unattested destination is `third_party` even when the operator believes it trustworthy. **Trust is not an egress class.** | + +## 4. Effect classes + +| Class | Contract | Enforcement | +|---|---|---| +| `none` | Read-only. Nothing changed. | Trivially safe to replay | +| `reversible` | `before` recorded; prior state restorable. | Undo is a state transition | +| `compensable` | Cannot be undone, but a compensating action exists and **its grant is named at the time of acting** — not discovered afterwards. | `compensator` bound in the receipt | +| `irreversible` | Once committed, permanent. | Rule 1: plan/commit separation | + +AR-1 does not solve effect revocation — **nothing does, in general**. Revoking +authority does not un-send an email or un-move funds. What AR-1 does is make the +distinction explicit and machine-readable *at the moment of action*, which is +the precondition for any system that wants to reason about it afterwards. + +## 5. Egress classes + +| Class | Means | Verifiable by | +|---|---|---| +| `none` | Resolved on-device. | Rule 2, plus tier and attestation | +| `attested_enclave` | Left the device to somewhere that proved what it was running. | Rule 3 — the peer attestation id | +| `third_party` | Left the device to an unattested destination. | Named and counted, honestly marked unverifiable | + +## 6. Verification flow + +1. Parse the tagged COSE_Sign1 envelope; reject any `alg` other than EdDSA (−8). +2. Check `kid` against the expected steward. +3. Verify the signature over the canonical signed core. +4. Decode the core as canonical det-CBOR. Reject trailing bytes — a signed core + is exactly one item, and anything appended is corruption or an attempt to + smuggle data past a verifier that stops at the first complete value. +5. Check the profile tag. +6. **Apply the three rules to the decoded projection.** +7. Optionally resolve each bound content-id and verify the underlying receipt in + its own family's verifier. AR-1 binds; it does not re-verify on their behalf. + +Steps 1–6 require only the envelope and a public key. That is what makes a +standalone verifier possible, and shipping that verifier is what turns an +internal convention into something a third party can adopt. + +## 7. Conformance + +An implementation conforms at **AR-1/basic** when, given the published pack: + +- every positive vector verifies, and the re-derived receipt id and canonical + core match the published `id_hex` and `core_hex` byte-for-byte; +- every negative vector is **rejected**, despite carrying a genuine signature. + +The negatives are the substance. An implementation that checks signatures and +skips the structural rules passes the positives and fails the pack — which is +exactly the failure mode the pack is designed to catch. + +## 8. What AR-1 deliberately does not do + +- **Key custody and recovery.** Unsolved everywhere; AR-1 must not be built in a + way that presumes a solution. +- **Re-verifying bound receipts.** Each family owns its own verification. AR-1 + binds content-ids and stops there. +- **Proving the energy figure is honest.** It carries provenance so a reader can + judge; it does not adjudicate. +- **Undoing effects.** See §4. + +## 9. Security considerations + +**A valid signature is not a valid receipt.** The three rules exist because +signature verification alone accepts well-formed lies. The negative vectors +demonstrate this concretely: each is signed with the real fixture key and each +must be refused. + +**Content-id binding is only as strong as the bound artifacts.** AR-1 proves +*which* authority receipt, attestation and work receipt were referenced. It does +not prove those artifacts are themselves sound — that is their own verifiers' +job, and a complete audit runs all of them. + +**The energy cross-check is a consistency check, not a proof.** An attestation +asserts; joules are measured. Binding both means a forged attestation must also +maintain a plausible energy profile across an independently sampled counter, and +that the failure is visible rather than silent. An adversary with physical +access who can forge a quote can also influence measurement. Claiming more than +this would be exactly the overreach the design exists to avoid. diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs b/jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs new file mode 100644 index 000000000..c898d5421 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/examples/emit_vectors.rs @@ -0,0 +1,244 @@ +//! Emit the AR-1 conformance vector pack. +//! +//! ```text +//! cargo run -p jcp-action-receipt --example emit_vectors -- jcp/conformance/v1 +//! ``` +//! +//! Writes `action_receipt.json` and `action_receipt_meta.json`, following the +//! shape the existing JCP packs use: a `meta` file declaring the algorithm, +//! profile, public key and steward, and a vectors file carrying signed +//! envelopes as hex. +//! +//! The signing key is a **published fixture**, deliberately: a conformance +//! vector nobody else can verify is not a conformance vector. It is the +//! all-`0x2a` key and must never be used for anything real. +//! +//! Both positive and negative vectors ship. The negatives are the point — they +//! pin the three structural rules, so an implementation that accepts a +//! well-signed but ill-formed receipt fails the pack rather than passing it. + +use ed25519_dalek::SigningKey; +use jcp_action_receipt::{ + ActionReceipt, Effect, EffectClass, Egress, EgressClass, verify, +}; +use jcp_receipt::jcr1; +use jcp_schema::ContentId; +use serde_json::{Value, json}; + +/// Published fixture key. Not a secret; never use it for anything real. +const FIXTURE_SEED: [u8; 32] = [0x2a; 32]; + +const STEWARD: &str = "did:example:ar-reference"; + +fn cid(tag: &str) -> ContentId { + ContentId::of_bytes(tag.as_bytes()) +} + +fn base() -> ActionReceipt { + ActionReceipt { + closed_at: "2026-08-25T12:00:00Z".into(), + grant_id: cid("grant/root"), + chain_ids: vec![cid("grant/root"), cid("grant/delegated")], + authority_receipt: cid("jcp-receipt/allow"), + verdict: "allow".into(), + attestation_id: cid("attest/eat"), + proof_cell_id: Some(cid("proof/cell")), + tier: "S5".into(), + grounding: "hardware".into(), + work_receipt: cid("jcr1/resolution"), + input_hash: "a".repeat(64), + joules_uj: 19_538_280, + energy_provenance: "HwShunt".into(), + effect: Effect { + class: EffectClass::Reversible, + target: cid("target/document"), + before: Some("b".repeat(64)), + after: Some("c".repeat(64)), + compensator: None, + plan_receipt: None, + }, + egress: Egress { + class: EgressClass::None, + bytes: 0, + peer: None, + }, + steward: STEWARD.into(), + } +} + +/// A signed vector plus the properties a verifier must reproduce. +fn positive(name: &str, note: &str, r: &ActionReceipt, key: &SigningKey) -> Value { + let env = r.seal(key).expect("valid receipt must seal"); + // Prove the vector before publishing it — a pack that ships an + // unverifiable vector is worse than no pack. + let v = verify(&env, &key.verifying_key(), STEWARD).expect("emitted vector must verify"); + assert_eq!(v.id, r.id().unwrap()); + json!({ + "name": name, + "note": note, + "expect": "verify", + "id_hex": r.id().unwrap().to_hex(), + "core_hex": hex::encode(r.signed_core().unwrap()), + "envelope_hex": hex::encode(&env), + "wire": r.to_wire(), + }) +} + +/// A negative vector: correctly signed, structurally invalid. Built by signing +/// a hand-edited projection so the signature is genuine — an implementation +/// that only checks signatures will accept it, which is exactly what the pack +/// is designed to catch. +fn negative(name: &str, note: &str, expect: &str, wire: Value, key: &SigningKey) -> Value { + let core = jcr1::signed_core_bytes(&wire).expect("core"); + let env = jcr1::cose_sign1_envelope(&core, key, STEWARD); + // The signature really is valid... + jcr1::verify_cose_sign1(&env, STEWARD, key.verifying_key().as_bytes()) + .expect("negative vector must carry a genuine signature"); + // ...and AR-1 must still refuse it. + assert!( + verify(&env, &key.verifying_key(), STEWARD).is_err(), + "negative vector `{name}` was accepted — the rule it pins is not enforced" + ); + json!({ + "name": name, + "note": note, + "expect": expect, + "envelope_hex": hex::encode(&env), + "wire": wire, + }) +} + +fn main() -> Result<(), Box> { + let out_dir = std::env::args().nth(1).unwrap_or_else(|| ".".into()); + let key = SigningKey::from_bytes(&FIXTURE_SEED); + + let mut vectors = Vec::new(); + + // ── positives: one per effect class, one per egress class ────────── + vectors.push(positive( + "reversible-local", + "Read-modify-write resolved on-device. Nothing left the machine, so egress is `none` with zero bytes.", + &base(), + &key, + )); + + let mut r = base(); + r.effect.class = EffectClass::None; + r.effect.before = None; + r.effect.after = None; + vectors.push(positive( + "read-only", + "A query that changed nothing. Safe to replay; no before/after state to record.", + &r, + &key, + )); + + let mut r = base(); + r.effect.class = EffectClass::Compensable; + r.effect.compensator = Some(cid("grant/refund")); + vectors.push(positive( + "compensable-with-compensator", + "Cannot be undone, but the grant that could compensate is named at the time of acting — not discovered afterwards.", + &r, + &key, + )); + + let mut r = base(); + r.effect.class = EffectClass::Irreversible; + r.effect.plan_receipt = Some(cid("plan/receipt")); + vectors.push(positive( + "irreversible-with-plan", + "An irreversible commit carrying the plan receipt that preceded it. This is the only shape in which `irreversible` is well-formed.", + &r, + &key, + )); + + let mut r = base(); + r.egress.class = EgressClass::AttestedEnclave; + r.egress.bytes = 4_096; + r.egress.peer = Some(cid("attest/peer-enclave")); + vectors.push(positive( + "egress-attested-enclave", + "Work left the device to somewhere that proved what it was running. The peer attestation is bound in the receipt.", + &r, + &key, + )); + + let mut r = base(); + r.egress.class = EgressClass::ThirdParty; + r.egress.bytes = 8_192; + r.egress.peer = None; + r.tier = "S0".into(); + r.grounding = "software".into(); + vectors.push(positive( + "egress-third-party-honest", + "An unattested destination, honestly recorded rather than upgraded. Trust is not an egress class.", + &r, + &key, + )); + + let mut r = base(); + r.energy_provenance = "Estimator".into(); + r.joules_uj = 1_200_000; + vectors.push(positive( + "estimated-energy", + "Energy from an estimator, not a hardware counter. `HwShunt` and `Estimator` are different claims and must never collapse into one number.", + &r, + &key, + )); + + // ── negatives: the three structural rules ────────────────────────── + let mut w = base().to_wire(); + w["effect"]["class"] = json!("irreversible"); + vectors.push(negative( + "irreversible-without-plan", + "Correctly signed, structurally invalid: an irreversible effect with no plan receipt. A verifier that only checks signatures accepts this.", + "reject:irreversible-without-plan", + w, + &key, + )); + + let mut w = base().to_wire(); + w["egress"]["bytes"] = json!(4_096u64); + vectors.push(negative( + "egress-none-with-bytes", + "Claims nothing left the device while counting 4096 bytes that did. The claim is falsified by its own byte count.", + "reject:egress-none-with-bytes", + w, + &key, + )); + + let mut w = base().to_wire(); + w["egress"]["class"] = json!("attested_enclave"); + w["egress"]["bytes"] = json!(4_096u64); + vectors.push(negative( + "attested-egress-without-peer", + "Claims an attested destination with no peer attestation to bind. The router may not claim a stronger class than its evidence supports.", + "reject:attested-egress-without-peer", + w, + &key, + )); + + let meta = json!({ + "alg": "EdDSA (COSE -8)", + "profile": jcp_action_receipt::AR_PROFILE, + "pubkey_hex": hex::encode(key.verifying_key().as_bytes()), + "steward": STEWARD, + "note": "Fixture key, published deliberately so third parties can verify. Never use it for anything real.", + "positives": vectors.iter().filter(|v| v["expect"] == "verify").count(), + "negatives": vectors.iter().filter(|v| v["expect"] != "verify").count(), + }); + + let vpath = format!("{out_dir}/action_receipt.json"); + let mpath = format!("{out_dir}/action_receipt_meta.json"); + std::fs::write(&vpath, serde_json::to_string_pretty(&json!({ "vectors": vectors }))? + "\n")?; + std::fs::write(&mpath, serde_json::to_string_pretty(&meta)? + "\n")?; + + println!("wrote {vpath}"); + println!("wrote {mpath}"); + println!( + " {} positive, {} negative", + meta["positives"], meta["negatives"] + ); + Ok(()) +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs b/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs new file mode 100644 index 000000000..414b77a44 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/examples/end_to_end.rs @@ -0,0 +1,234 @@ +//! End-to-end Action Receipt on real hardware. +//! +//! ```text +//! cargo run -p jcp-action-receipt --example end_to_end -- /tmp/action.hex +//! ``` +//! +//! Implements §5 step 6 of the blueprint: **one agent action, under a real +//! delegated grant, with energy read off this host's own counters, sealed into +//! an AR-1 receipt that a third party verifies from the published spec alone.** +//! +//! Only the workload is a stand-in, so the example runs anywhere. Everything +//! around it is the real machinery: +//! +//! - the grant is **really issued** and **really attenuated**, and amplification +//! is really refused; +//! - the authorisation is a **real `decide` call** against a real budget, and +//! the receipt records the verdict that call returned; +//! - the joules are **measured**, and the meter's provenance is carried through +//! verbatim. On a host with no counter it reports `Estimator` and this example +//! says so rather than inventing `HwShunt`; +//! - the tier is stamped from what is **actually running**. This is in-process +//! with no isolation boundary crossed, so it is `S0`. Claiming `S5` without a +//! microVM is exactly the overreach the ladder exists to prevent. + +use ed25519_dalek::SigningKey; +use jcp_action_receipt::{ActionReceipt, Effect, EffectClass, Egress, EgressClass, verify}; +use jcp_grant::{attenuate, issue}; +use jcp_receipt as authority; +use jcp_runtime::Runtime; +use jcp_schema::{ + Capability, ContentId, Did, Energy, Frame, FrameKind, Grant, Trust, Verdict, +}; +use sandbox_meter::{DeviceEnergy, PowerMeter, Receipt as WorkReceipt}; +use sandbox_schema::Tier; + +const STEWARD: &str = "did:example:ar-e2e"; + +fn main() -> Result<(), Box> { + let out = std::env::args().nth(1).unwrap_or_else(|| "action.hex".into()); + + // ── 1. A real grant, really delegated ──────────────────────────── + let issuer = SigningKey::from_bytes(&[11u8; 32]); + let agent = SigningKey::from_bytes(&[22u8; 32]); + let subagent = SigningKey::from_bytes(&[33u8; 32]); + let agent_did = Did::from_verifying_key(&agent.verifying_key()); + let sub_did = Did::from_verifying_key(&subagent.verifying_key()); + + let resource = ContentId::of_bytes(b"resource/quarterly-report"); + let root = Grant { + issuer: Did::from_verifying_key(&issuer.verifying_key()), + subject: agent_did, + capability: Capability::new(resource, ["read", "summarise"]), + budget_uj: 50_000_000, + budget_funds: None, + caveats: Vec::new(), + expiry: 0, + parent: None, + delegate_depth: None, + nonce: [1u8; 16], + }; + let sg = issue(&issuer, root.clone())?; + + // Strictly narrower: read only, one fifth of the ceiling. + let delegated = attenuate( + &sg, + &agent, + sub_did, + Capability::new(resource, ["read"]), + 10_000_000, + 0, + [2u8; 16], + )?; + // And prove the runtime really refuses amplification, rather than asserting it. + let amplified = attenuate( + &sg, + &agent, + sub_did, + Capability::new(resource, ["read", "delete"]), + 10_000_000, + 0, + [3u8; 16], + ); + assert!(amplified.is_err(), "amplification must be refused"); + println!("1. grant issued, attenuated to read-only — amplification refused: {}", + amplified.unwrap_err()); + + // ── 2. A real authorisation decision ───────────────────────────── + let mut rt = Runtime::new(); + let frame = Frame { + kind: FrameKind::ToolCall, + trust: Trust::Control, + grant_id: delegated.grant.id(), + action: "read".into(), + resource, + payload_hash: ContentId::of_bytes(b"input/quarterly-report"), + }; + let decision = rt.decide(&frame, &delegated, sub_did, Energy::measured(250_000), 0); + let verdict = match decision.verdict { + Verdict::Allow => "allow", + Verdict::Deny(_) => "deny", + }; + // Seal the REAL authority receipt from the decision that just happened, and + // take its content id from the bytes rather than naming a placeholder. + let steward_key = SigningKey::from_bytes(&[44u8; 32]); + let authority_env = + authority::seal(&frame, &delegated.grant, &decision, &steward_key, STEWARD)?; + let authority_core = + authority::signed_core(&frame, &delegated.grant, &decision, STEWARD)?; + let authority_id = ContentId::of_bytes(&authority_core); + // Prove it verifies on its own terms before binding it. + authority::verify( + &frame, + &delegated.grant, + &decision, + &authority_env, + STEWARD, + steward_key.verifying_key().as_bytes(), + )?; + println!( + "2. decide() → {verdict}, {} µJ remaining; authority receipt sealed + verified, id {}", + decision.budget_remaining_uj, + &authority_id.to_hex()[..12] + ); + + // ── 3. Real work, really measured ──────────────────────────────── + let mut meter = PowerMeter::detect(); + let sources = meter.sources().join(","); + let is_hw = meter.is_hardware(); + + let span = meter.start(); + let mut acc: u64 = 0; + for i in 0..40_000_000u64 { + acc = acc.wrapping_add(i ^ (acc >> 7)).rotate_left(3); + } + let measurement = span.stop(&mut meter); + std::hint::black_box(acc); + + let joules_uj = measurement.total_uj(); + let provenance = if is_hw { "HwShunt" } else { "Estimator" }; + println!( + "3. work metered — {joules_uj} µJ [{provenance}] over {:.2}s via {sources}", + measurement.wall.as_secs_f64() + ); + if !is_hw { + println!(" note: no hardware counter here; provenance is Estimator, not HwShunt"); + } + + // Build the REAL work receipt from the devices the meter actually reported. + // `Receipt::build` enforces the provenance/measured coupling itself, so a + // mislabelled device is refused here rather than propagating into AR-1. + let devices: Vec = measurement + .devices + .iter() + .map(|d| DeviceEnergy { + class: d.class, + measured_uj: d.measured_uj, + estimated_uj: d.estimated_uj, + provenance: d.provenance, + }) + .collect(); + let work = WorkReceipt::build( + sandbox_schema::ContentId::of_bytes(b"unit/quarterly-report-summarise"), + Tier::S0, + devices, + 1, + [7u8; 8], + )?; + work.validate()?; + // The two families agree on BLAKE3 and disagree only on presentation: + // sandbox renders `b3:`, jcp carries raw 32 bytes. Re-addressing + // the same canonical core with jcp's hasher yields the identical digest, so + // the binding is exact rather than a hash of a hash. + let work_id = ContentId::of_bytes(&work.canonical_core()); + debug_assert_eq!( + work.content_id().as_str().trim_start_matches("b3:").len(), + 43, + "sandbox content id should be b3:" + ); + println!( + " work receipt sealed over {} metered device(s), id {}", + measurement.devices.len(), + &work_id.to_hex()[..12] + ); + + // ── 4. Seal the Action Receipt ─────────────────────────────────── + let receipt = ActionReceipt { + closed_at: "2026-08-25T12:00:00Z".into(), + grant_id: delegated.grant.id(), + chain_ids: vec![sg.grant.id(), delegated.grant.id()], + authority_receipt: authority_id, + verdict: verdict.into(), + attestation_id: ContentId::of_bytes(b"attest/e2e-local"), + proof_cell_id: None, + tier: "S0".into(), + grounding: if is_hw { "hardware" } else { "software" }.into(), + work_receipt: work_id, + input_hash: ContentId::of_bytes(b"input/quarterly-report").to_hex(), + joules_uj, + energy_provenance: provenance.into(), + effect: Effect { + // read-and-summarise changed nothing in the world + class: EffectClass::None, + target: resource, + before: None, + after: None, + compensator: None, + plan_receipt: None, + }, + egress: Egress { + // resolved entirely in this process + class: EgressClass::None, + bytes: 0, + peer: None, + }, + steward: STEWARD.into(), + }; + + let envelope = receipt.seal(&steward_key)?; + println!("4. sealed — receipt id {}", receipt.id()?.to_hex()); + + // ── 5. Verify it back, as a third party would ──────────────────── + let v = verify(&envelope, &steward_key.verifying_key(), STEWARD)?; + assert_eq!(v.id, receipt.id()?); + println!("5. verified from the envelope alone — {} byte canonical core", v.core.len()); + + std::fs::write(&out, hex::encode(&envelope))?; + println!(); + println!("wrote {out}"); + println!( + "verify independently:\n ar-verify {out} --pubkey {} --steward {STEWARD}", + hex::encode(steward_key.verifying_key().as_bytes()) + ); + Ok(()) +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs b/jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs new file mode 100644 index 000000000..cc952201d --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/src/bin/ar-verify.rs @@ -0,0 +1,374 @@ +//! `ar-verify` — the standalone Action Receipt verifier. +//! +//! This is the deliverable that makes AR-1 matter to anyone outside this tree. +//! A format nobody else can check is a convention; a format with a verifier a +//! third party can run is a standard. Everything it needs arrives on the command +//! line — an envelope, a public key, a steward — and it reaches the network +//! never. +//! +//! ```text +//! ar-verify --pubkey --steward +//! ar-verify --pack # check a whole conformance pack +//! ar-verify ... --json +//! ``` +//! +//! It reports **each binding separately**, because "invalid" is not a useful +//! audit finding. An auditor needs to know *which* claim failed and why. +//! +//! Exit codes: `0` all checks passed · `1` a check failed · `2` bad usage. + +use ed25519_dalek::VerifyingKey; +use jcp_action_receipt::{ArError, verify}; +use serde_json::Value; +use std::process::ExitCode; + +fn main() -> ExitCode { + let args: Vec = std::env::args().skip(1).collect(); + if args.is_empty() || args.iter().any(|a| a == "-h" || a == "--help") { + usage(); + return ExitCode::from(2); + } + + let json_out = args.iter().any(|a| a == "--json"); + + if let Some(i) = args.iter().position(|a| a == "--pack") { + let Some(dir) = args.get(i + 1) else { + eprintln!("--pack needs a directory"); + return ExitCode::from(2); + }; + return verify_pack(dir, json_out); + } + + let path = &args[0]; + let Some(pubkey) = flag(&args, "--pubkey") else { + eprintln!("--pubkey is required"); + return ExitCode::from(2); + }; + let Some(steward) = flag(&args, "--steward") else { + eprintln!("--steward is required"); + return ExitCode::from(2); + }; + + let envelope = match read_envelope(path) { + Ok(b) => b, + Err(e) => { + eprintln!("{path}: {e}"); + return ExitCode::from(2); + } + }; + let vk = match parse_key(&pubkey) { + Ok(k) => k, + Err(e) => { + eprintln!("--pubkey: {e}"); + return ExitCode::from(2); + } + }; + + verify_one(&envelope, &vk, &steward, json_out) +} + +fn usage() { + eprintln!( + "ar-verify — independently check an Action Receipt (AR-1)\n\ + \n\ + USAGE\n \ + ar-verify --pubkey --steward [--json]\n \ + ar-verify --pack [--json]\n\ + \n\ + Reads only what you give it. Never touches the network." + ); +} + +fn flag(args: &[String], name: &str) -> Option { + args.iter() + .position(|a| a == name) + .and_then(|i| args.get(i + 1)) + .cloned() +} + +/// Accept either a hex text file or raw envelope bytes — an auditor should not +/// have to know which form the sender chose. +fn read_envelope(path: &str) -> Result, String> { + let raw = std::fs::read(path).map_err(|e| e.to_string())?; + if let Ok(text) = std::str::from_utf8(&raw) { + let t: String = text.split_whitespace().collect(); + if !t.is_empty() && t.len() % 2 == 0 && t.bytes().all(|c| c.is_ascii_hexdigit()) { + return hex::decode(&t).map_err(|e| e.to_string()); + } + } + Ok(raw) +} + +fn parse_key(hexstr: &str) -> Result { + let raw = hex::decode(hexstr.trim()).map_err(|e| e.to_string())?; + let arr: [u8; 32] = raw + .as_slice() + .try_into() + .map_err(|_| format!("expected 32 bytes, got {}", raw.len()))?; + VerifyingKey::from_bytes(&arr).map_err(|e| e.to_string()) +} + +/// One line per checked property. `ok` is what an auditor reads; `detail` is +/// what they quote when it fails. +struct Check { + ok: bool, + name: &'static str, + detail: String, +} + +fn verify_one(envelope: &[u8], vk: &VerifyingKey, steward: &str, json_out: bool) -> ExitCode { + let mut checks: Vec = Vec::new(); + + let result = verify(envelope, vk, steward); + + match &result { + Ok(v) => { + checks.push(Check { + ok: true, + name: "signature", + detail: format!("COSE_Sign1 EdDSA verified, kid = {steward}"), + }); + checks.push(Check { + ok: true, + name: "canonical-core", + detail: format!("{} bytes decoded as canonical det-CBOR, no trailing data", v.core.len()), + }); + checks.push(Check { + ok: true, + name: "profile", + detail: v.wire["ar_receipt"].as_str().unwrap_or("?").to_string(), + }); + checks.push(Check { + ok: true, + name: "receipt-id", + detail: v.id.to_hex(), + }); + + // The four bindings, reported individually. + let w = &v.wire; + checks.push(Check { + ok: true, + name: "binding:authority", + detail: format!( + "grant {} · verdict {} · chain depth {}", + short(w, "grant_id"), + w["verdict"].as_str().unwrap_or("?"), + w["chain_ids"].as_array().map(|a| a.len()).unwrap_or(0) + ), + }); + checks.push(Check { + ok: true, + name: "binding:environment", + detail: format!( + "tier {} · grounding {} · attestation {}", + w["tier"].as_str().unwrap_or("?"), + w["grounding"].as_str().unwrap_or("?"), + short(w, "attestation_id") + ), + }); + checks.push(Check { + ok: true, + name: "binding:work", + detail: format!( + "{} µJ [{}] · receipt {}", + w["joules_uj"].as_u64().unwrap_or(0), + w["energy_provenance"].as_str().unwrap_or("?"), + short(w, "work_receipt") + ), + }); + let eff = &w["effect"]; + checks.push(Check { + ok: true, + name: "binding:effect", + detail: format!( + "class {}{}", + eff["class"].as_str().unwrap_or("?"), + if eff.get("plan_receipt").is_some() { + " · plan bound" + } else if eff.get("compensator").is_some() { + " · compensator bound" + } else { + "" + } + ), + }); + let eg = &w["egress"]; + checks.push(Check { + ok: true, + name: "binding:egress", + detail: format!( + "class {} · {} bytes{}", + eg["class"].as_str().unwrap_or("?"), + eg["bytes"].as_u64().unwrap_or(0), + if eg.get("peer").is_some() { " · peer attested" } else { "" } + ), + }); + + // The three rules held, or verify() would have refused. + checks.push(Check { + ok: true, + name: "rule:irreversible-needs-plan", + detail: "satisfied".into(), + }); + checks.push(Check { + ok: true, + name: "rule:egress-none-zero-bytes", + detail: "satisfied".into(), + }); + checks.push(Check { + ok: true, + name: "rule:attested-needs-peer", + detail: "satisfied".into(), + }); + + // Honest caveat, always printed. AR-1 binds; it does not re-verify. + checks.push(Check { + ok: true, + name: "note:bound-artifacts", + detail: "content-ids bound but NOT resolved — run each family's own verifier for a complete audit".into(), + }); + } + Err(e) => { + // Name the specific failure rather than a generic "invalid". + let (name, detail): (&'static str, String) = match e { + ArError::IrreversibleWithoutPlan => ( + "rule:irreversible-needs-plan", + "REFUSED — irreversible effect with no plan receipt. The signature is valid; the receipt is not.".into(), + ), + ArError::EgressNoneWithBytes(n) => ( + "rule:egress-none-zero-bytes", + format!("REFUSED — egress class `none` while counting {n} bytes that left the device"), + ), + ArError::AttestedEgressWithoutPeer => ( + "rule:attested-needs-peer", + "REFUSED — `attested_enclave` claimed with no peer attestation to bind".into(), + ), + ArError::UnknownProfile(p) => ("profile", format!("REFUSED — unknown profile `{p}`")), + ArError::Jcr1(inner) => ("signature", format!("REFUSED — {inner}")), + ArError::Decode(inner) => ("canonical-core", format!("REFUSED — {inner}")), + ArError::MissingField(f) => ("canonical-core", format!("REFUSED — missing field `{f}`")), + }; + checks.push(Check { ok: false, name, detail }); + } + } + + let failed = checks.iter().filter(|c| !c.ok).count(); + if json_out { + let arr: Vec = checks + .iter() + .map(|c| serde_json::json!({ "check": c.name, "ok": c.ok, "detail": c.detail })) + .collect(); + println!( + "{}", + serde_json::to_string_pretty(&serde_json::json!({ + "verified": failed == 0, + "checks": arr, + })) + .unwrap() + ); + } else { + for c in &checks { + println!("{} {:<32} {}", if c.ok { " ok " } else { " FAIL " }, c.name, c.detail); + } + println!(); + println!( + "{}", + if failed == 0 { + "VERIFIED — every binding and rule checked from the envelope alone." + } else { + "NOT VERIFIED" + } + ); + } + + if failed == 0 { ExitCode::SUCCESS } else { ExitCode::from(1) } +} + +/// Verify a whole conformance pack: positives must verify, negatives must be +/// refused. This is how an implementer proves conformance to themselves. +fn verify_pack(dir: &str, json_out: bool) -> ExitCode { + let meta_p = format!("{dir}/action_receipt_meta.json"); + let vec_p = format!("{dir}/action_receipt.json"); + + let meta: Value = match std::fs::read(&meta_p).ok().and_then(|b| serde_json::from_slice(&b).ok()) { + Some(v) => v, + None => { + eprintln!("cannot read {meta_p}"); + return ExitCode::from(2); + } + }; + let pack: Value = match std::fs::read(&vec_p).ok().and_then(|b| serde_json::from_slice(&b).ok()) { + Some(v) => v, + None => { + eprintln!("cannot read {vec_p}"); + return ExitCode::from(2); + } + }; + + let vk = match meta["pubkey_hex"].as_str().map(parse_key) { + Some(Ok(k)) => k, + _ => { + eprintln!("{meta_p}: bad or missing pubkey_hex"); + return ExitCode::from(2); + } + }; + let steward = meta["steward"].as_str().unwrap_or_default().to_string(); + + let empty = vec![]; + let vectors = pack["vectors"].as_array().unwrap_or(&empty); + let mut pass = 0usize; + let mut fail = 0usize; + let mut lines = Vec::new(); + + for v in vectors { + let name = v["name"].as_str().unwrap_or(""); + let expect_verify = v["expect"].as_str().unwrap_or("verify") == "verify"; + let Some(env) = v["envelope_hex"].as_str().and_then(|h| hex::decode(h).ok()) else { + lines.push((false, name.to_string(), "unreadable envelope_hex".to_string())); + fail += 1; + continue; + }; + let got = verify(&env, &vk, &steward); + let ok = got.is_ok() == expect_verify; + let detail = match (&got, expect_verify) { + (Ok(_), true) => "verified as expected".to_string(), + (Err(e), false) => format!("refused as expected — {e}"), + (Ok(_), false) => "ACCEPTED a vector that must be refused".to_string(), + (Err(e), true) => format!("REJECTED a valid vector — {e}"), + }; + if ok { pass += 1 } else { fail += 1 } + lines.push((ok, name.to_string(), detail)); + } + + if json_out { + let arr: Vec = lines + .iter() + .map(|(ok, n, d)| serde_json::json!({ "vector": n, "ok": ok, "detail": d })) + .collect(); + println!( + "{}", + serde_json::to_string_pretty(&serde_json::json!({ + "conformant": fail == 0, "pass": pass, "fail": fail, "vectors": arr + })) + .unwrap() + ); + } else { + for (ok, n, d) in &lines { + println!("{} {:<34} {}", if *ok { " ok " } else { " FAIL " }, n, d); + } + println!(); + println!("{pass} passed, {fail} failed"); + if fail == 0 { + println!("CONFORMANT — AR-1/basic. Positives verify; negatives are refused despite valid signatures."); + } + } + + if fail == 0 { ExitCode::SUCCESS } else { ExitCode::from(1) } +} + +fn short(w: &Value, key: &str) -> String { + w[key] + .as_str() + .map(|s| s.chars().take(12).collect::() + "…") + .unwrap_or_else(|| "?".into()) +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs b/jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs new file mode 100644 index 000000000..71e12e733 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/src/decode.rs @@ -0,0 +1,228 @@ +//! Canonical det-CBOR decoder for the AR-1 subset. +//! +//! `jcp_receipt::jcr1` ships a canonical *encoder* and no decoder, because +//! nothing downstream of it needed to read a signed core back. A verifier does: +//! the point of AR-1 is that a third party holding only an envelope can check +//! the structural rules for themselves, and that requires recovering the +//! projection from the bytes. +//! +//! Rather than take a CBOR dependency — AR-1's whole claim is that it adds no +//! new primitives — this is the exact inverse of the encoder's subset, and +//! nothing more. The encoder emits four major types (RFC 8949 §4.2.1: maps, +//! arrays, text strings, unsigned integers; no floats, bools, nulls or tags), +//! so those four are all this decodes. Anything else is refused rather than +//! guessed at, which is the same discipline the encoder applies on the way out. +//! +//! `decode_roundtrips_every_encoded_shape` pins the two halves together. + +use serde_json::{Map, Value}; + +/// Why a canonical decode failed. +#[derive(Debug, thiserror::Error)] +pub enum DecodeError { + /// Input ended mid-item. + #[error("truncated input at byte {0}")] + Truncated(usize), + /// A major type outside the canonical subset appeared. + #[error("major type {0} is outside the canonical subset at byte {1}")] + UnsupportedMajor(u8, usize), + /// An additional-information value the canonical form never emits. + #[error("non-canonical length encoding at byte {0}")] + NonCanonicalLength(usize), + /// A text string was not valid UTF-8. + #[error("invalid utf-8 in text string at byte {0}")] + BadUtf8(usize), + /// A map key was not a text string. + #[error("non-text map key at byte {0}")] + NonTextKey(usize), + /// Bytes remained after the top-level item. + #[error("{0} trailing byte(s) after top-level item")] + Trailing(usize), +} + +/// Decode canonical det-CBOR produced by `jcr1::canonical_cbor` back to JSON. +/// +/// Rejects trailing bytes: a signed core is exactly one item, and anything +/// appended to it is either corruption or an attempt to smuggle data past a +/// verifier that stops reading at the first complete value. +pub fn from_canonical_cbor(bytes: &[u8]) -> Result { + let mut p = Parser { b: bytes, i: 0 }; + let v = p.value()?; + if p.i != bytes.len() { + return Err(DecodeError::Trailing(bytes.len() - p.i)); + } + Ok(v) +} + +struct Parser<'a> { + b: &'a [u8], + i: usize, +} + +impl<'a> Parser<'a> { + fn byte(&mut self) -> Result { + let b = *self.b.get(self.i).ok_or(DecodeError::Truncated(self.i))?; + self.i += 1; + Ok(b) + } + + fn take(&mut self, n: usize) -> Result<&'a [u8], DecodeError> { + let end = self.i.checked_add(n).ok_or(DecodeError::Truncated(self.i))?; + let s = self.b.get(self.i..end).ok_or(DecodeError::Truncated(self.i))?; + self.i = end; + Ok(s) + } + + /// Argument of a head byte, enforcing the shortest-form rule the canonical + /// encoder guarantees. A longer-than-necessary encoding is a different byte + /// string for the same value, which would break content addressing. + fn arg(&mut self, ai: u8) -> Result { + let at = self.i - 1; + Ok(match ai { + 0..=23 => ai as u64, + 24 => { + let v = self.byte()? as u64; + if v < 24 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + 25 => { + let s = self.take(2)?; + let v = u16::from_be_bytes([s[0], s[1]]) as u64; + if v <= u8::MAX as u64 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + 26 => { + let s = self.take(4)?; + let v = u32::from_be_bytes([s[0], s[1], s[2], s[3]]) as u64; + if v <= u16::MAX as u64 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + 27 => { + let s = self.take(8)?; + let v = u64::from_be_bytes([s[0], s[1], s[2], s[3], s[4], s[5], s[6], s[7]]); + if v <= u32::MAX as u64 { + return Err(DecodeError::NonCanonicalLength(at)); + } + v + } + _ => return Err(DecodeError::NonCanonicalLength(at)), + }) + } + + fn value(&mut self) -> Result { + let at = self.i; + let head = self.byte()?; + let major = head >> 5; + let ai = head & 0x1f; + match major { + 0 => Ok(Value::from(self.arg(ai)?)), + 3 => { + let n = self.arg(ai)? as usize; + let s = self.take(n)?; + Ok(Value::String( + std::str::from_utf8(s) + .map_err(|_| DecodeError::BadUtf8(at))? + .to_owned(), + )) + } + 4 => { + let n = self.arg(ai)? as usize; + let mut out = Vec::with_capacity(n.min(1024)); + for _ in 0..n { + out.push(self.value()?); + } + Ok(Value::Array(out)) + } + 5 => { + let n = self.arg(ai)? as usize; + let mut out = Map::new(); + for _ in 0..n { + let kat = self.i; + let k = match self.value()? { + Value::String(s) => s, + _ => return Err(DecodeError::NonTextKey(kat)), + }; + out.insert(k, self.value()?); + } + Ok(Value::Object(out)) + } + m => Err(DecodeError::UnsupportedMajor(m, at)), + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use jcp_receipt::jcr1; + use serde_json::json; + + /// The property that matters: whatever the canonical encoder emits, this + /// reads back identically. If these two ever drift, a verifier and a signer + /// disagree about what a receipt says. + #[test] + fn decode_roundtrips_every_encoded_shape() { + let cases = vec![ + json!({}), + json!({"a": 0}), + json!({"a": 23, "b": 24, "c": 255, "d": 256, "e": 65535, "f": 65536}), + json!({"big": 4_294_967_296u64, "huge": 19_538_280u64}), + json!({"s": "", "t": "hello", "u": "a".repeat(64)}), + json!({"arr": [1, 2, 3], "empty": []}), + json!({"nested": {"deep": {"deeper": [1, {"x": "y"}]}}}), + json!({"unicode": "joules — ⚡ 変換"}), + json!({"long": "x".repeat(300)}), + ]; + for c in cases { + let enc = jcr1::canonical_cbor(&c).expect("encode"); + let dec = from_canonical_cbor(&enc).expect("decode"); + assert_eq!(dec, c, "round-trip mismatch for {c}"); + } + } + + #[test] + fn rejects_trailing_bytes() { + let mut enc = jcr1::canonical_cbor(&json!({"a": 1})).unwrap(); + enc.push(0x00); + assert!(matches!( + from_canonical_cbor(&enc), + Err(DecodeError::Trailing(1)) + )); + } + + #[test] + fn rejects_truncated_input() { + let enc = jcr1::canonical_cbor(&json!({"key": "value"})).unwrap(); + assert!(from_canonical_cbor(&enc[..enc.len() - 2]).is_err()); + } + + #[test] + fn rejects_non_canonical_length() { + // 0x18 0x05 encodes 5 in two bytes where one would do. Same value, + // different bytes — which would break content addressing. + assert!(matches!( + from_canonical_cbor(&[0x18, 0x05]), + Err(DecodeError::NonCanonicalLength(0)) + )); + } + + #[test] + fn rejects_types_outside_the_subset() { + // 0xf5 is `true` (major 7), which the canonical encoder never emits. + assert!(matches!( + from_canonical_cbor(&[0xf5]), + Err(DecodeError::UnsupportedMajor(7, 0)) + )); + // 0x40 is a byte string (major 2) — also outside the subset. + assert!(matches!( + from_canonical_cbor(&[0x40]), + Err(DecodeError::UnsupportedMajor(2, 0)) + )); + } +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs b/jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs new file mode 100644 index 000000000..9a80a9004 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/src/lib.rs @@ -0,0 +1,564 @@ +//! # Action Receipt (AR-1) +//! +//! **The composition envelope.** Three receipt families already ship, and each +//! holds one quarter of the answer to the question an auditor actually asks — +//! *under what authority did this agent do that, where did it run, and what did +//! it cost?* None of them binds to the others. +//! +//! | Family | Records | Carries | +//! |---|---|---| +//! | `jcp-receipt` | authority | grant chain, verdict, budget drawn | +//! | `sandbox-proof` | environment | attestation, isolation tier, substrate | +//! | JCR-1 | work | input hash, measured joules, energy provenance | +//! | *(nothing)* | **effect** | what changed, and whether it can be undone | +//! +//! AR-1 binds the first three **by content-id** and supplies the fourth. It is +//! an envelope, not a replacement: every existing family keeps its own canonical +//! encoding and its own signer, and every existing verifier keeps working +//! unchanged. +//! +//! ## No new cryptography +//! +//! Canonical det-CBOR (RFC 8949 §4.2.1) and the tagged COSE_Sign1 envelope are +//! reused verbatim from [`jcp_receipt::jcr1`]. This crate adds a field layout +//! and three structural rules — nothing else. If AR-1 ever needs a novel +//! primitive, that is a signal the design went wrong. +//! +//! ## The three rules that carry the weight +//! +//! A receipt format that merely *records* claims is a log. What makes AR-1 +//! evidence is that certain shapes are refused at verification, so a violation +//! is detectable rather than a matter of trust: +//! +//! 1. **`effect: irreversible` requires a prior plan receipt.** The cascade's +//! body-tier design already separates plan from commit for actions that touch +//! the world. AR-1 binds that discipline into the artifact: an irreversible +//! effect with no `plan_receipt` fails verification. +//! 2. **`egress: none` requires zero bytes.** A claim that nothing left the +//! machine is falsifiable by its own byte count. +//! 3. **`egress: attested_enclave` requires a peer attestation.** The router may +//! never claim a stronger class than it can bind evidence for. An unattested +//! destination is `third_party` even when the operator believes it +//! trustworthy — trust is not an egress class. +//! +//! ## Status +//! +//! Draft. Field names are settled against the existing canonical projections but +//! the profile tag is `ar/1-draft` until the vector pack is reviewed. + +mod decode; +pub use decode::{DecodeError, from_canonical_cbor}; + +use jcp_receipt::jcr1::{self, Jcr1Error}; +use jcp_schema::ContentId; +use serde::{Deserialize, Serialize}; +use serde_json::{Map, Value, json}; + +/// Profile tag carried in every AR-1 receipt. +pub const AR_PROFILE: &str = "ar/1-draft"; + +/// Errors surfaced by AR-1 construction or verification. +#[derive(Debug, thiserror::Error)] +pub enum ArError { + /// The underlying JCR-1 canonical encoding or envelope layer failed. + #[error("jcr1: {0}")] + Jcr1(#[from] Jcr1Error), + /// An `irreversible` effect arrived without the plan receipt that the + /// plan/commit split requires. See the module docs, rule 1. + #[error("irreversible effect requires a plan receipt (AR-1 §4)")] + IrreversibleWithoutPlan, + /// `egress: none` was claimed alongside a non-zero byte count. + #[error("egress class `none` claims {0} bytes left the device (AR-1 §3)")] + EgressNoneWithBytes(u64), + /// `egress: attested_enclave` was claimed with no peer attestation to bind. + #[error("egress class `attested_enclave` requires a peer attestation (AR-1 §3)")] + AttestedEgressWithoutPeer, + /// The receipt did not carry the profile tag this crate understands. + #[error("unknown profile: expected `{AR_PROFILE}`, found `{0}`")] + UnknownProfile(String), + /// A field required by the canonical projection was absent. + #[error("missing required field: {0}")] + MissingField(&'static str), + /// The signed core did not decode as canonical CBOR. + #[error("canonical decode: {0}")] + Decode(#[from] DecodeError), +} + +/// What an action did to the world, and whether it can be taken back. +/// +/// This is the only genuinely new field group in AR-1 — nothing in the three +/// existing families records it. The classes are ordered by how much of the +/// action survives a change of mind. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "lowercase")] +pub enum EffectClass { + /// Read-only. Nothing changed; the action is safe to replay. + None, + /// Prior state is recoverable. Undo is a state transition. + Reversible, + /// Cannot be undone, but a compensating action exists and its grant is + /// named at the time of acting — not discovered afterwards. + Compensable, + /// Once committed, permanent. Requires plan/commit separation. + Irreversible, +} + +impl EffectClass { + /// Wire spelling, pinned so the projection cannot drift with serde config. + pub fn wire_tag(self) -> &'static str { + match self { + Self::None => "none", + Self::Reversible => "reversible", + Self::Compensable => "compensable", + Self::Irreversible => "irreversible", + } + } +} + +/// Where the work went, and what evidence backs that claim. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum EgressClass { + /// Resolved on-device. Nothing left the machine. + None, + /// Left the device to somewhere that proved what it was running. + AttestedEnclave, + /// Left the device to an unattested destination. Named and counted — + /// and honestly marked as unverifiable. + ThirdParty, +} + +impl EgressClass { + /// Wire spelling, pinned. + pub fn wire_tag(self) -> &'static str { + match self { + Self::None => "none", + Self::AttestedEnclave => "attested_enclave", + Self::ThirdParty => "third_party", + } + } +} + +/// The effect record: binding four, and the piece no existing family carries. +#[derive(Debug, Clone)] +pub struct Effect { + /// How much of this action survives a change of mind. + pub class: EffectClass, + /// What was acted on. + pub target: ContentId, + /// State hash before the action, where observable. + pub before: Option, + /// State hash after the action, where observable. + pub after: Option, + /// A grant that could undo this, for `Compensable` effects. + pub compensator: Option, + /// The plan receipt that preceded an `Irreversible` commit. Required for + /// that class; its absence is a protocol violation, not a missing nicety. + pub plan_receipt: Option, +} + +/// The egress record: binding five, the router's per-request privacy contract. +#[derive(Debug, Clone)] +pub struct Egress { + /// The strongest class the available evidence supports — never stronger. + pub class: EgressClass, + /// Bytes that left the device. + pub bytes: u64, + /// Attestation of the receiving side, for `AttestedEnclave`. + pub peer: Option, +} + +/// One agent action, with every binding needed to check it independently. +#[derive(Debug, Clone)] +pub struct ActionReceipt { + /// RFC 3339 close time. + pub closed_at: String, + + // -- binding 1: authority ------------------------------------------- + /// The grant that permitted this action. + pub grant_id: ContentId, + /// The full delegation chain, root first. Empty for a root grant. + pub chain_ids: Vec, + /// The `jcp-receipt` recording the authorisation decision. + pub authority_receipt: ContentId, + /// The decision itself, carried here so a verifier need not fetch the + /// authority receipt to learn whether the action was permitted. + pub verdict: String, + + // -- binding 2: environment ----------------------------------------- + /// The attestation covering the execution environment. + pub attestation_id: ContentId, + /// The signed sandbox proof cell, where one exists. + pub proof_cell_id: Option, + /// Isolation tier, `S0`..`S7`. + pub tier: String, + /// Whether the attestation is rooted in silicon or in software. Carried + /// verbatim from the attestation; never upgraded here. + pub grounding: String, + + // -- binding 3: work ------------------------------------------------ + /// The JCR-1 resolution receipt for the work performed. + pub work_receipt: ContentId, + /// Hash of the input the work consumed. + pub input_hash: String, + /// Measured cost in microjoules. + pub joules_uj: u64, + /// How that figure was obtained. Never collapsed into a single number: + /// `HwShunt` and `Estimator` are not the same claim. + pub energy_provenance: String, + + // -- bindings 4 and 5 ----------------------------------------------- + /// What changed in the world. + pub effect: Effect, + /// What left the device. + pub egress: Egress, + + /// The party accountable for this receipt. Required, as in JCR-1 §2.1. + pub steward: String, +} + +impl ActionReceipt { + /// Check the three structural rules. Called by both [`Self::seal`] and + /// [`verify`], so an invalid receipt can be neither produced nor accepted. + pub fn check_discipline(&self) -> Result<(), ArError> { + if self.effect.class == EffectClass::Irreversible && self.effect.plan_receipt.is_none() { + return Err(ArError::IrreversibleWithoutPlan); + } + if self.egress.class == EgressClass::None && self.egress.bytes != 0 { + return Err(ArError::EgressNoneWithBytes(self.egress.bytes)); + } + if self.egress.class == EgressClass::AttestedEnclave && self.egress.peer.is_none() { + return Err(ArError::AttestedEgressWithoutPeer); + } + Ok(()) + } + + /// The canonical JSON projection a third party canonicalises and hashes. + /// + /// Absent optionals are omitted rather than emitted as null, matching + /// JCR-1 §3.1 — `signed_core_bytes` drops nulls, so emitting them would + /// produce a projection that does not round-trip. + pub fn to_wire(&self) -> Value { + let mut o = Map::new(); + o.insert("ar_receipt".into(), json!(AR_PROFILE)); + o.insert("closed_at".into(), json!(self.closed_at)); + + o.insert("grant_id".into(), json!(self.grant_id.to_hex())); + if !self.chain_ids.is_empty() { + let chain: Vec = self.chain_ids.iter().map(|c| json!(c.to_hex())).collect(); + o.insert("chain_ids".into(), Value::Array(chain)); + } + o.insert("authority_receipt".into(), json!(self.authority_receipt.to_hex())); + o.insert("verdict".into(), json!(self.verdict)); + + o.insert("attestation_id".into(), json!(self.attestation_id.to_hex())); + if let Some(p) = &self.proof_cell_id { + o.insert("proof_cell_id".into(), json!(p.to_hex())); + } + o.insert("tier".into(), json!(self.tier)); + o.insert("grounding".into(), json!(self.grounding)); + + o.insert("work_receipt".into(), json!(self.work_receipt.to_hex())); + o.insert("input_hash".into(), json!(self.input_hash)); + o.insert("joules_uj".into(), json!(self.joules_uj)); + o.insert("energy_provenance".into(), json!(self.energy_provenance)); + + let mut e = Map::new(); + e.insert("class".into(), json!(self.effect.class.wire_tag())); + e.insert("target".into(), json!(self.effect.target.to_hex())); + if let Some(b) = &self.effect.before { + e.insert("before".into(), json!(b)); + } + if let Some(a) = &self.effect.after { + e.insert("after".into(), json!(a)); + } + if let Some(c) = &self.effect.compensator { + e.insert("compensator".into(), json!(c.to_hex())); + } + if let Some(p) = &self.effect.plan_receipt { + e.insert("plan_receipt".into(), json!(p.to_hex())); + } + o.insert("effect".into(), Value::Object(e)); + + let mut g = Map::new(); + g.insert("class".into(), json!(self.egress.class.wire_tag())); + g.insert("bytes".into(), json!(self.egress.bytes)); + if let Some(p) = &self.egress.peer { + g.insert("peer".into(), json!(p.to_hex())); + } + o.insert("egress".into(), Value::Object(g)); + + o.insert("steward".into(), json!(self.steward)); + Value::Object(o) + } + + /// Canonical signed-core bytes — det-CBOR over [`Self::to_wire`], via the + /// JCR-1 encoder. These are exactly the bytes the envelope signs. + pub fn signed_core(&self) -> Result, ArError> { + Ok(jcr1::signed_core_bytes(&self.to_wire())?) + } + + /// Content id of this receipt: BLAKE3 over the canonical signed core. + pub fn id(&self) -> Result { + Ok(ContentId::of_bytes(&self.signed_core()?)) + } + + /// Seal into a tagged COSE_Sign1 envelope. Refuses to sign a receipt that + /// violates the discipline rules — an invalid AR-1 cannot be produced by + /// this crate, only hand-forged. + pub fn seal( + &self, + signing_key: &ed25519_dalek::SigningKey, + ) -> Result, ArError> { + self.check_discipline()?; + let core = self.signed_core()?; + Ok(jcr1::cose_sign1_envelope(&core, signing_key, &self.steward)) + } +} + +/// The outcome of verifying an AR-1 envelope: the signed core it carried, plus +/// the wire projection parsed back out of it. +#[derive(Debug, Clone)] +pub struct Verified { + /// The canonical bytes that were signed. + pub core: Vec, + /// The projection recovered from those bytes. + pub wire: Value, + /// Content id of the receipt. + pub id: ContentId, +} + +/// Verify an AR-1 envelope end to end. +/// +/// Checks, in order: COSE_Sign1 signature and `kid` against `expected_steward`; +/// the profile tag; then the three discipline rules **re-derived from the wire +/// projection**, not from a caller-supplied struct. A receipt that was +/// hand-forged to violate them is rejected here even though it signs correctly. +pub fn verify( + envelope: &[u8], + verifying_key: &ed25519_dalek::VerifyingKey, + expected_steward: &str, +) -> Result { + let core = jcr1::verify_cose_sign1(envelope, expected_steward, verifying_key.as_bytes())?; + // jcr1 exposes an encoder but no decoder, so the projection is read back + // here. The signature has already been checked against `core`; this only + // reads structure out of bytes that are known-good. + let wire: Value = from_canonical_cbor(&core)?; + + let profile = wire + .get("ar_receipt") + .and_then(Value::as_str) + .ok_or(ArError::MissingField("ar_receipt"))?; + if profile != AR_PROFILE { + return Err(ArError::UnknownProfile(profile.to_string())); + } + + let effect = wire.get("effect").ok_or(ArError::MissingField("effect"))?; + let eclass = effect + .get("class") + .and_then(Value::as_str) + .ok_or(ArError::MissingField("effect.class"))?; + if eclass == "irreversible" && effect.get("plan_receipt").is_none() { + return Err(ArError::IrreversibleWithoutPlan); + } + + let egress = wire.get("egress").ok_or(ArError::MissingField("egress"))?; + let gclass = egress + .get("class") + .and_then(Value::as_str) + .ok_or(ArError::MissingField("egress.class"))?; + let bytes = egress.get("bytes").and_then(Value::as_u64).unwrap_or(0); + if gclass == "none" && bytes != 0 { + return Err(ArError::EgressNoneWithBytes(bytes)); + } + if gclass == "attested_enclave" && egress.get("peer").is_none() { + return Err(ArError::AttestedEgressWithoutPeer); + } + + let id = ContentId::of_bytes(&core); + Ok(Verified { core, wire, id }) +} + +#[cfg(test)] +mod tests { + use super::*; + use ed25519_dalek::SigningKey; + + fn cid(b: u8) -> ContentId { + ContentId([b; 32]) + } + + fn key() -> SigningKey { + SigningKey::from_bytes(&[7u8; 32]) + } + + fn base() -> ActionReceipt { + ActionReceipt { + closed_at: "2026-08-25T00:00:00Z".into(), + grant_id: cid(1), + chain_ids: vec![cid(2)], + authority_receipt: cid(3), + verdict: "allow".into(), + attestation_id: cid(4), + proof_cell_id: Some(cid(5)), + tier: "S5".into(), + grounding: "hardware".into(), + work_receipt: cid(6), + input_hash: "a".repeat(64), + joules_uj: 19_538_280, + energy_provenance: "HwShunt".into(), + effect: Effect { + class: EffectClass::Reversible, + target: cid(7), + before: Some("b".repeat(64)), + after: Some("c".repeat(64)), + compensator: None, + plan_receipt: None, + }, + egress: Egress { + class: EgressClass::None, + bytes: 0, + peer: None, + }, + steward: "did:example:ar-reference".into(), + } + } + + #[test] + fn seals_and_verifies_round_trip() { + let r = base(); + let env = r.seal(&key()).unwrap(); + let v = verify(&env, &key().verifying_key(), &r.steward).unwrap(); + assert_eq!(v.core, r.signed_core().unwrap()); + assert_eq!(v.id, r.id().unwrap()); + assert_eq!(v.wire["tier"], "S5"); + assert_eq!(v.wire["joules_uj"], 19_538_280u64); + } + + #[test] + fn canonical_core_is_stable_across_encodes() { + let r = base(); + assert_eq!(r.signed_core().unwrap(), r.signed_core().unwrap()); + assert_eq!(r.id().unwrap(), r.id().unwrap()); + } + + #[test] + fn absent_optionals_are_omitted_not_nulled() { + // JCR-1 §3.1 drops nulls from the signed core, so emitting an explicit + // null would produce a projection that does not round-trip. + let r = base(); + let w = r.to_wire(); + assert!(w["effect"].get("compensator").is_none()); + assert!(w["egress"].get("peer").is_none()); + } + + // ── rule 1: irreversible requires a plan ───────────────────────── + + #[test] + fn irreversible_without_plan_refuses_to_seal() { + let mut r = base(); + r.effect.class = EffectClass::Irreversible; + r.effect.plan_receipt = None; + assert!(matches!( + r.seal(&key()), + Err(ArError::IrreversibleWithoutPlan) + )); + } + + #[test] + fn irreversible_with_plan_seals() { + let mut r = base(); + r.effect.class = EffectClass::Irreversible; + r.effect.plan_receipt = Some(cid(9)); + let env = r.seal(&key()).unwrap(); + let v = verify(&env, &key().verifying_key(), &r.steward).unwrap(); + assert_eq!(v.wire["effect"]["class"], "irreversible"); + } + + // ── rule 2: egress none means zero bytes ───────────────────────── + + #[test] + fn egress_none_with_bytes_refuses_to_seal() { + let mut r = base(); + r.egress.bytes = 4096; + assert!(matches!( + r.seal(&key()), + Err(ArError::EgressNoneWithBytes(4096)) + )); + } + + // ── rule 3: attested egress needs a peer ───────────────────────── + + #[test] + fn attested_egress_without_peer_refuses_to_seal() { + let mut r = base(); + r.egress.class = EgressClass::AttestedEnclave; + r.egress.bytes = 1024; + r.egress.peer = None; + assert!(matches!( + r.seal(&key()), + Err(ArError::AttestedEgressWithoutPeer) + )); + } + + #[test] + fn third_party_egress_needs_no_peer() { + // An unattested destination is honestly recorded, not blocked. + let mut r = base(); + r.egress.class = EgressClass::ThirdParty; + r.egress.bytes = 1024; + r.egress.peer = None; + assert!(r.seal(&key()).is_ok()); + } + + // ── the rules bind at verification, not just construction ──────── + + #[test] + fn hand_forged_violation_is_rejected_at_verify() { + // Seal a valid receipt, then rebuild the core with an irreversible + // effect and no plan and sign it directly — bypassing `seal`. A verifier + // that only checked the signature would accept this. + let mut r = base(); + r.effect.class = EffectClass::Reversible; + let mut wire = r.to_wire(); + wire["effect"]["class"] = json!("irreversible"); + let core = jcr1::signed_core_bytes(&wire).unwrap(); + let forged = jcr1::cose_sign1_envelope(&core, &key(), &r.steward); + + // The signature is perfectly valid... + assert!(jcr1::verify_cose_sign1(&forged, &r.steward, key().verifying_key().as_bytes()).is_ok()); + // ...and AR-1 rejects it anyway. + assert!(matches!( + verify(&forged, &key().verifying_key(), &r.steward), + Err(ArError::IrreversibleWithoutPlan) + )); + } + + #[test] + fn wrong_steward_is_rejected() { + let r = base(); + let env = r.seal(&key()).unwrap(); + assert!(verify(&env, &key().verifying_key(), "did:example:someone-else").is_err()); + } + + #[test] + fn tampered_envelope_is_rejected() { + let r = base(); + let mut env = r.seal(&key()).unwrap(); + let n = env.len(); + env[n - 1] ^= 0xff; + assert!(verify(&env, &key().verifying_key(), &r.steward).is_err()); + } + + #[test] + fn energy_provenance_survives_the_round_trip_verbatim() { + // HwShunt and Estimator are different claims and must never collapse. + for prov in ["HwShunt", "ModelBased", "Estimator"] { + let mut r = base(); + r.energy_provenance = prov.into(); + let env = r.seal(&key()).unwrap(); + let v = verify(&env, &key().verifying_key(), &r.steward).unwrap(); + assert_eq!(v.wire["energy_provenance"], prov); + } + } +} diff --git a/jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs b/jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs new file mode 100644 index 000000000..e2939bb36 --- /dev/null +++ b/jcp/jcp-rs/crates/jcp-action-receipt/tests/conformance.rs @@ -0,0 +1,113 @@ +//! Consume the published AR-1 conformance pack. +//! +//! This is the test that makes the pack mean something. It reads +//! `jcp/conformance/v1/action_receipt.json` from disk — the same bytes a third +//! party would download — resolves the public key from the meta file, and +//! checks every vector against the stated expectation. +//! +//! Crucially it consumes the *published artifact*, not in-memory values. A pack +//! that only its own generator can read is not a conformance pack. + +use ed25519_dalek::VerifyingKey; +use jcp_action_receipt::verify; +use serde_json::Value; + +fn pack_dir() -> std::path::PathBuf { + std::path::Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../../conformance/v1") + .canonicalize() + .expect("conformance dir must exist next to the spec") +} + +fn load(name: &str) -> Value { + let p = pack_dir().join(name); + let bytes = std::fs::read(&p).unwrap_or_else(|e| panic!("read {}: {e}", p.display())); + serde_json::from_slice(&bytes).unwrap_or_else(|e| panic!("parse {}: {e}", p.display())) +} + +fn key_and_steward() -> (VerifyingKey, String) { + let meta = load("action_receipt_meta.json"); + let hex_key = meta["pubkey_hex"].as_str().expect("meta.pubkey_hex"); + let raw = hex::decode(hex_key).expect("pubkey hex"); + let arr: [u8; 32] = raw.as_slice().try_into().expect("32-byte pubkey"); + let steward = meta["steward"].as_str().expect("meta.steward").to_string(); + (VerifyingKey::from_bytes(&arr).expect("valid pubkey"), steward) +} + +#[test] +fn every_positive_vector_verifies() { + let (vk, steward) = key_and_steward(); + let pack = load("action_receipt.json"); + let vectors = pack["vectors"].as_array().expect("vectors array"); + + let mut checked = 0; + for v in vectors { + if v["expect"] != "verify" { + continue; + } + let name = v["name"].as_str().unwrap_or(""); + let env = hex::decode(v["envelope_hex"].as_str().expect("envelope_hex")) + .unwrap_or_else(|e| panic!("{name}: envelope hex: {e}")); + + let ok = verify(&env, &vk, &steward) + .unwrap_or_else(|e| panic!("positive vector `{name}` failed to verify: {e}")); + + // The receipt id in the pack must match what a verifier re-derives from + // the bytes — otherwise the published id is decorative. + let want = v["id_hex"].as_str().expect("id_hex"); + assert_eq!(ok.id.to_hex(), want, "{name}: id mismatch"); + + // And the canonical core must match byte-for-byte, which is what makes + // the content address reproducible on another implementation. + let want_core = v["core_hex"].as_str().expect("core_hex"); + assert_eq!(hex::encode(&ok.core), want_core, "{name}: core mismatch"); + + checked += 1; + } + assert!(checked >= 7, "expected at least 7 positive vectors, saw {checked}"); +} + +#[test] +fn every_negative_vector_is_rejected_despite_a_valid_signature() { + let (vk, steward) = key_and_steward(); + let pack = load("action_receipt.json"); + let vectors = pack["vectors"].as_array().expect("vectors array"); + + let mut checked = 0; + for v in vectors { + let expect = v["expect"].as_str().unwrap_or("verify"); + if expect == "verify" { + continue; + } + let name = v["name"].as_str().unwrap_or(""); + let env = hex::decode(v["envelope_hex"].as_str().expect("envelope_hex")) + .unwrap_or_else(|e| panic!("{name}: envelope hex: {e}")); + + // The signature is genuine — these vectors exist precisely because a + // signature-only verifier would accept them. + let sig_ok = jcp_receipt::jcr1::verify_cose_sign1(&env, &steward, vk.as_bytes()); + assert!( + sig_ok.is_ok(), + "{name}: negative vector should carry a genuine signature" + ); + + // AR-1 must refuse it anyway. + assert!( + verify(&env, &vk, &steward).is_err(), + "negative vector `{name}` was accepted — the rule it pins is not enforced" + ); + checked += 1; + } + assert!(checked >= 3, "expected at least 3 negative vectors, saw {checked}"); +} + +#[test] +fn pack_declares_the_profile_this_build_implements() { + let meta = load("action_receipt_meta.json"); + assert_eq!( + meta["profile"].as_str().expect("meta.profile"), + jcp_action_receipt::AR_PROFILE, + "vector pack was generated for a different profile than this build implements" + ); + assert_eq!(meta["alg"].as_str().expect("meta.alg"), "EdDSA (COSE -8)"); +} diff --git a/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs b/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs index e1b06227c..545e7e21a 100644 --- a/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs +++ b/joule-code/joule-code-rs/crates/joule-code-remediate/examples/formal_fix.rs @@ -39,7 +39,7 @@ use joulecontract_proof::{discharge, DischargeStatus, Formalization}; use joulecontract_schema::{Ceiling, Contract, ContentAddress, Rigor}; use proof_cascade::{ProofCache, Router}; use proof_schema::{GoalKind, SpecGrounding}; -use proof_solvers::{z3_available, Propositional, Z3Smt}; +use proof_solvers::{real_ladder, z3_available}; // SOUNDNESS NOTE — why this example uses a decision-procedure ladder. // @@ -51,15 +51,23 @@ use proof_solvers::{z3_available, Propositional, Z3Smt}; // `FrontierModel` proves ANY goal unconditionally — so a disproof was // fabricated into a proof. // -// That is now fixed in the proof crate: `Verdict::Refuted` exists, `Z3Smt` -// emits it on `sat`, and the router HALTS on a refutation instead of escalating -// (regression test in proof-cascade). So `real_ladder()` no longer fabricates a -// proof of candidate A — it halts at `Z3Smt` with a refutation. +// That was fixed in the proof crate: `Verdict::Refuted` exists, `Z3Smt` emits +// it on `sat`, and the router HALTS on a refutation instead of escalating +// (regression test in proof-cascade). // -// We still use the decision-procedure ladder `[Propositional, Z3Smt]` here, on -// purpose: a formal *gate* must not depend on a model stand-in even for goals -// z3 returns `unknown` on (the stubs would still claim `proved` there). The -// gate's guarantee is "a decision procedure decided this", nothing weaker. +// A SECOND hole survived that fix, and this note used to describe the local +// workaround for it: escalation past a rung that *could not run at all*. With +// `z3` absent, `Z3Smt` returned `Unproved`, the router escalated, and +// `FrontierModel` closed the goal — so on any machine without `z3`, every goal +// came back proved at ~50 J of imaginary energy. This example dodged it by +// hand-building `[Propositional, Z3Smt]` instead of calling `real_ladder()`. +// +// That is now fixed at the source rather than at this call site: +// `real_ladder()` IS the decision-procedure ladder, the stand-ins live only in +// the `reference_*` fixtures, and `Solver::is_decision_procedure` makes the +// distinction machine-checkable (`ladder_is_sound` in proof-solvers). So the +// hand-rolled ladder is gone and the guarantee is unchanged: "a decision +// procedure decided this", nothing weaker. /// The contract over the netting function: one precondition, one postcondition /// (the property the fix must honor), one frame. Same spec for both candidates @@ -109,10 +117,10 @@ fn judge(label: &str, net_definition: &str) -> bool { grounding: SpecGrounding::CrossChecked, }; // A fresh cascade + cache per candidate so the joules reported are this - // candidate's own proof work, not a cache hit from the other. The ladder is - // decision-procedures only (see the SOUNDNESS NOTE at the top) — a formal + // candidate's own proof work, not a cache hit from the other. `real_ladder` + // is decision-procedures only (see the SOUNDNESS NOTE at the top) — a formal // gate may not fall through to a model stand-in that fabricates a proof. - let router = Router::new(vec![Box::new(Propositional), Box::new(Z3Smt)]); + let router = Router::new(real_ladder()); let mut cache = ProofCache::new(); let d = discharge(&contract, &[formalization], &router, &mut cache) .expect("discharge runs (bookkeeping is well-formed)"); @@ -129,10 +137,17 @@ fn judge(label: &str, net_definition: &str) -> bool { true } DischargeStatus::Unproved(result) => { - println!( - " UNPROVED — z3 found a counter-model; the postcondition can fail ({} µJ measured)", - result.total_uj - ); + // "Unproved" has two very different causes and they must not read + // the same: z3 ran and refuted the claim, or z3 was never there to + // ask. Printing "found a counter-model" in the second case would + // report evidence that was never gathered — the exact failure this + // example exists to demonstrate. + let why = if z3_available() { + "z3 found a counter-model; the postcondition can fail" + } else { + "no decision procedure available to decide it (z3 absent)" + }; + println!(" UNPROVED — {why} ({} µJ measured)", result.total_uj); println!(" → formal gate REFUSES this fix (it would be reverted, never shipped)."); false } diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs index e00167013..4bf95c59b 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/l0_cache.rs @@ -174,6 +174,13 @@ impl Default for L0Cache { } impl Tier for L0Cache { + /// An exact-match hit is served from this process's own memory, so L0 can + /// honestly declare that nothing left the device. This is the one tier in + /// the base cascade entitled to claim `None`. + fn egress(&self) -> crate::types::Egress { + crate::types::Egress::None + } + fn id(&self) -> TierId { TierId::L0 } diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs index e2c044c2c..e119fb961 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/tier.rs @@ -44,6 +44,23 @@ pub trait Tier: Send { budget_remaining: f64, ) -> Result; + /// Where this tier's work goes. + /// + /// The runtime stamps the returned value onto the trace of every answer + /// this tier produces, so declaring it is not optional in practice even + /// though the method is defaulted. + /// + /// Default: [`Egress::Undeclared`]. Legacy tiers are recorded as + /// undeclared rather than assumed local — "we did not ask" and "nothing + /// left the device" are different facts, and only the second is a privacy + /// claim. A tier that resolves entirely in-process should override this + /// with [`Egress::None`]; one that calls out should return + /// [`Egress::AttestedEnclave`] or [`Egress::ThirdParty`] with a real byte + /// count. + fn egress(&self) -> crate::types::Egress { + crate::types::Egress::Undeclared + } + /// The Synthesis coordinate of this tier, if known. /// `⟨Z, E, T, P, I, V, R⟩` from the Periodic Stack. /// @@ -419,6 +436,7 @@ impl Runtime { let estimate = l0.estimate_cost(&q).unwrap(); let remaining = q.budget.remaining(spent); if estimate.joules <= remaining { + let l0_egress = l0.egress(); let l0_answer = l0.try_answer(&q, remaining)?; match &l0_answer.output { AnswerOutput::Refused(_) => { @@ -430,8 +448,11 @@ impl Runtime { }); } _ => { - // L0 hit. Merge our walk's trace and return. + // L0 hit. Merge our walk's trace and return. The + // egress goes on the trace the runtime returns, not the + // tier's own — that one is discarded by the spread below. spent += l0_answer.joules_spent; + trace.egress = l0_egress; trace.attempts.push(TraceEntry { tier: TierId::L0, outcome: TraceOutcome::Hit, @@ -589,6 +610,7 @@ impl Runtime { } // Dispatch. + let tier_egress = tier.egress(); let dispatch_result = tier.try_answer(&q, remaining); // Record calibration data on every dispatch outcome. // The `actual` is the tier's self-reported spend; we charge @@ -664,6 +686,10 @@ impl Runtime { continue; } spent += actual; + // The answering tier's declaration goes on the trace + // the runtime returns; the spread below discards the + // tier's own copy. + trace.egress = tier_egress; trace.attempts.push(TraceEntry { tier: tier_id, outcome: TraceOutcome::Hit, diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs index 43e6dfb02..0ff05763f 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/src/types.rs @@ -205,11 +205,73 @@ impl RefusalReason { } } +/// Where a resolution's work went, and what evidence backs that claim. +/// +/// A router that decides between on-device and remote execution and never says +/// which is the gap this closes: today a user cannot tell, per request, whether +/// their query left the machine. Recording it only helps if the record is +/// trustworthy, so the single rule is that **a class is never stronger than the +/// evidence for it**. +/// +/// [`Egress::Undeclared`] is the default, and exists so that silence cannot be +/// mistaken for `None`. A tier that has not declared its egress is recorded as +/// undeclared, never as "nothing left the device" — not knowing and knowing +/// nothing happened are different facts, and only one of them is a claim. +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub enum Egress { + /// The tier has not declared a class. Never promote this to `None`: an + /// undeclared tier may well have made a network call. + #[default] + Undeclared, + /// Resolved on-device. Nothing left the machine. + None, + /// Left the device to a peer that attested what it was running. Carries + /// the peer's attestation id, so the claim is checkable rather than taken + /// on faith. + AttestedEnclave { peer: String, bytes: u64 }, + /// Left the device to an unattested destination. Named and counted, and + /// honestly marked unverifiable. Trust is not an egress class: a + /// destination the operator believes reputable is still `ThirdParty`. + ThirdParty { destination: String, bytes: u64 }, +} + +impl Egress { + /// Bytes that left the device. Zero for `None`, and zero for `Undeclared` + /// too — which is exactly why `Undeclared` must never be read as `None`. + pub fn bytes(&self) -> u64 { + match self { + Self::Undeclared | Self::None => 0, + Self::AttestedEnclave { bytes, .. } | Self::ThirdParty { bytes, .. } => *bytes, + } + } + + /// Whether this carries enough evidence to publish as a privacy claim. + /// `Undeclared` does not: a receipt built from it would assert something + /// nobody measured. + pub fn is_publishable(&self) -> bool { + !matches!(self, Self::Undeclared) + } + + /// Stable wire spelling for receipts and logs. + pub fn wire_tag(&self) -> &'static str { + match self { + Self::Undeclared => "undeclared", + Self::None => "none", + Self::AttestedEnclave { .. } => "attested_enclave", + Self::ThirdParty { .. } => "third_party", + } + } +} + /// A record of which tier(s) were attempted, in order, with per-tier /// joule spend. The successful tier (if any) is last. #[derive(Debug, Clone, Default)] pub struct ExecutionTrace { pub attempts: Vec, + /// Where the answering tier's work went. Stamped by the runtime from the + /// tier's own declaration, so a tier cannot quietly omit it and a reader + /// cannot be misled by its absence. + pub egress: Egress, } #[derive(Debug, Clone)] @@ -672,3 +734,62 @@ impl std::fmt::Display for AnswerError { } impl std::error::Error for AnswerError {} + +#[cfg(test)] +mod egress_tests { + use super::Egress; + + #[test] + fn default_is_undeclared_not_none() { + // The whole point: silence must not read as a privacy claim. + assert_eq!(Egress::default(), Egress::Undeclared); + assert_ne!(Egress::default(), Egress::None); + } + + #[test] + fn undeclared_is_not_publishable() { + // A receipt built from Undeclared would assert something nobody + // measured, so it must be refused upstream rather than defaulted. + assert!(!Egress::Undeclared.is_publishable()); + assert!(Egress::None.is_publishable()); + assert!( + Egress::ThirdParty { destination: "api.example".into(), bytes: 10 }.is_publishable() + ); + } + + #[test] + fn undeclared_and_none_both_report_zero_bytes() { + // They agree on the number and disagree on the meaning, which is + // exactly why the class must be read rather than the byte count. + assert_eq!(Egress::Undeclared.bytes(), 0); + assert_eq!(Egress::None.bytes(), 0); + } + + #[test] + fn remote_classes_carry_their_byte_count() { + assert_eq!( + Egress::AttestedEnclave { peer: "b3:peer".into(), bytes: 4096 }.bytes(), + 4096 + ); + assert_eq!( + Egress::ThirdParty { destination: "api.example".into(), bytes: 8192 }.bytes(), + 8192 + ); + } + + #[test] + fn wire_tags_are_pinned() { + // These strings cross a standards boundary into AR-1 receipts; drift + // here silently changes what a published receipt means. + assert_eq!(Egress::Undeclared.wire_tag(), "undeclared"); + assert_eq!(Egress::None.wire_tag(), "none"); + assert_eq!( + Egress::AttestedEnclave { peer: String::new(), bytes: 0 }.wire_tag(), + "attested_enclave" + ); + assert_eq!( + Egress::ThirdParty { destination: String::new(), bytes: 0 }.wire_tag(), + "third_party" + ); + } +} diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs index 120cd0c14..fbc5c3aff 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-cascade/tests/r1_cascade.rs @@ -344,3 +344,49 @@ fn print_trace(a: &Answer) { format!("{:?}", entry.tier), entry.outcome, entry.joules); } } + + +// ── egress contract (AR-1 §3) ──────────────────────────────────────── + +#[test] +fn runtime_stamps_the_answering_tier_egress_onto_the_trace() { + use jouleclaw_cascade::types::Egress; + + // MockL4 does not override `egress()`, so it is Undeclared — and the point + // is that this is NOT silently reported as "nothing left the device". + let mut cascade = Cascade::new(); + cascade.register(Box::new(MockL4::new(0.5, "Paris"))); + let mut rt = Runtime::new(cascade); + + let a = rt.answer(text_query("capital of France?")).unwrap(); + assert_eq!(a.tier_used, TierId::L4(L4ModelId(0))); + assert_eq!( + a.trace.egress, + Egress::Undeclared, + "a tier that never declared its egress must not be recorded as local" + ); + assert!( + !a.trace.egress.is_publishable(), + "Undeclared carries no evidence, so it cannot become a privacy claim" + ); +} + +#[test] +fn a_local_cache_hit_is_recorded_as_local() { + use jouleclaw_cascade::types::Egress; + + // L0 overrides `egress()` with None because a hit is served from this + // process's own memory. The runtime stamps it — the tier does not write it + // into its own Answer — so a tier cannot forge the claim by construction. + let mut cascade = Cascade::new(); + cascade.register(Box::new(MockL4::new(0.5, "Paris"))); + let mut rt = Runtime::new(cascade); + + let q = text_query("capital of France?"); + let _ = rt.answer(q.clone()).unwrap(); // miss → L4 populates the cache + let hit = rt.answer(q).unwrap(); // hit → served by L0 + + assert_eq!(hit.tier_used, TierId::L0); + assert_eq!(hit.trace.egress, Egress::None); + assert!(hit.trace.egress.is_publishable()); +} diff --git a/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs b/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs index d435055b0..6b50a6cb1 100644 --- a/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs +++ b/jouleclaw/jouleclaw-rs/crates/jouleclaw-fabric/src/detect.rs @@ -131,6 +131,7 @@ fn probe_metal_gpu() -> Option { /// caller falls back, so it simply never records here). /// Seeded at the quiet-box measurement (~6 mJ/GFLOP, M4/M5); /// a per-box `mpp_energy` run overlays the Measured value. +#[cfg(target_os = "macos")] fn probe_metal_mpp() -> Option { let name = jouleclaw_backend_apple::mps_device_name()?; let mut energy = BTreeMap::new(); diff --git a/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs b/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs index aaaeac718..f7c88f26f 100644 --- a/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs +++ b/jouledesk/jouledesk-rs/crates/jouledesk/src/lib.rs @@ -313,7 +313,15 @@ mod tests { other => panic!("expected budget Denied, got {other:?}"), } assert_eq!(t.spent_uj("summarizer"), 100_000, "only the funded task ran"); - assert_eq!(t.verify_ledger(), Ok(1), "the one dispatched decision sealed + verifies"); + // BOTH decisions seal. A budget refusal is a decision made against a real + // grant — the teammate held the capability and was stopped by the ceiling — + // so it is evidence and seals like any other (see `TagOutcome`: "every + // variant sealed to the ledger"). Contrast the unheld-capability case + // above, which never reaches dispatch and leaves the ledger empty. Only + // one task *ran*, which is what `spent_uj` asserts; two decisions were + // *made*, which is what the ledger records. + assert_eq!(t.ledger().len(), 2, "the allow and the budget denial both sealed"); + assert_eq!(t.verify_ledger(), Ok(2), "and both verify under the steward key"); } #[test] diff --git a/proof/proof-rs/Cargo.lock b/proof/proof-rs/Cargo.lock index c0d1c1e72..8fcdfca75 100644 --- a/proof/proof-rs/Cargo.lock +++ b/proof/proof-rs/Cargo.lock @@ -302,6 +302,7 @@ dependencies = [ name = "proof-solvers" version = "0.1.0" dependencies = [ + "proof-cascade", "proof-schema", ] diff --git a/proof/proof-rs/crates/proof-conformance/tests/soundness.rs b/proof/proof-rs/crates/proof-conformance/tests/soundness.rs index 70f22e83f..b1a85103c 100644 --- a/proof/proof-rs/crates/proof-conformance/tests/soundness.rs +++ b/proof/proof-rs/crates/proof-conformance/tests/soundness.rs @@ -40,19 +40,33 @@ fn a_refutation_must_carry_a_witness() { } } +/// A goal no real rung can decide. Used by both tests below, which are the two +/// halves of one guarantee. +fn open_conjecture() -> ProofGoal { + ProofGoal::new( + "every even integer greater than 2 is the sum of two primes", + "demo", + GoalKind::Hard, + ) +} + /// The reference stand-ins must admit what they are. The top rung returns /// `Proved` for *any* goal, with the hash of the goal's own statement as the /// "artifact" — the claim offered as its own evidence — and `seal()` will sign /// that into a receipt that verifies. The receipt is not forged; it is honestly /// signed and substantively empty, which is worse, because it verifies. +/// +/// This exercises `reference_ladder()`. It used to exercise `real_ladder()`, +/// because the stand-ins sat on that ladder too — which is precisely the defect +/// since fixed: a solverless machine escalated past both real rungs into T3 and +/// proved everything. Detection was the right answer while the fabrication was +/// reachable in production; now it is prevented there and only has to be +/// detectable where stand-ins legitimately live. The companion test below pins +/// the other half. #[test] fn a_stand_in_proof_is_detectable_before_it_is_trusted() { - let goal = ProofGoal::new( - "every even integer greater than 2 is the sum of two primes", - "demo", - GoalKind::Hard, - ); - let r = Router::new(proof_solvers::real_ladder()); + let goal = open_conjecture(); + let r = Router::new(proof_solvers::reference_ladder()); let mut cache = ProofCache::new(); let res = r.prove(&goal, &mut cache); @@ -79,6 +93,39 @@ fn a_stand_in_proof_is_detectable_before_it_is_trusted() { assert!(again.require_substantive_proof().is_err()); } +/// The other half: on the real ladder that same goal is never closed at all. +/// +/// Detection (above) is a relying party's last line of defence, and it only +/// works if the relying party remembers to call it. Not reaching a stand-in in +/// the first place is the guarantee that does not depend on anyone remembering. +/// A missing rung must yield a weaker claim, never a stronger one. +#[test] +fn the_real_ladder_never_reaches_a_stand_in() { + let goal = open_conjecture(); + let r = Router::new(proof_solvers::real_ladder()); + let mut cache = ProofCache::new(); + let res = r.prove(&goal, &mut cache); + + assert!( + !res.proved, + "an open conjecture came back proved, closed by {:?}", + res.closed_by + ); + assert!(res.closed_by.is_none()); + assert!( + !res.closed_by_stub, + "nothing closed it, stand-in or otherwise" + ); + assert_eq!(res.require_substantive_proof(), Err("not proved")); + assert!( + !res.attempts.iter().any(|a| matches!( + a.tier, + proof_schema::Tier::SmallModel | proof_schema::Tier::BigModel + )), + "a model stand-in ran on the real ladder" + ); +} + /// A real rung is not marked, so the check is not vacuous. #[test] fn a_real_solver_is_not_flagged() { diff --git a/proof/proof-rs/crates/proof-schema/src/lib.rs b/proof/proof-rs/crates/proof-schema/src/lib.rs index d4eeda9dc..3ce2b4702 100644 --- a/proof/proof-rs/crates/proof-schema/src/lib.rs +++ b/proof/proof-rs/crates/proof-schema/src/lib.rs @@ -318,6 +318,12 @@ pub trait Solver { /// dangerous case, so the trait cannot be relied on alone — the reference /// stand-ins in `proof-solvers` all override it, and a new one MUST. /// + /// Because that default cannot be trusted on its own, the real ladders do + /// not rely on it to stay clean: they are built from decision procedures + /// only, and `ladder_is_sound` in `proof-solvers` pins both their membership + /// and their exact tiers — so a stand-in that forgot to override this still + /// cannot slip into a ladder whose verdict is read as evidence. + /// /// `Provenance` qualifies the *energy* of an attempt and `SpecGrounding` /// qualifies its *intent*; neither says anything about whether a verdict was /// earned. This does. diff --git a/proof/proof-rs/crates/proof-solvers/Cargo.toml b/proof/proof-rs/crates/proof-solvers/Cargo.toml index db0066719..6b02fa855 100644 --- a/proof/proof-rs/crates/proof-solvers/Cargo.toml +++ b/proof/proof-rs/crates/proof-solvers/Cargo.toml @@ -9,5 +9,12 @@ rust-version.workspace = true [dependencies] proof-schema = { workspace = true } +# Test-only: `ladder_never_fabricates_a_proof_when_a_rung_is_absent` drives the +# real router, because the fabrication bug lived in the *composition* of router +# and ladder, not in either alone. proof-cascade does not depend on this crate, +# so there is no cycle. +[dev-dependencies] +proof-cascade = { workspace = true } + [lints] workspace = true diff --git a/proof/proof-rs/crates/proof-solvers/src/lib.rs b/proof/proof-rs/crates/proof-solvers/src/lib.rs index ea9685dcc..7cbd8568f 100644 --- a/proof/proof-rs/crates/proof-solvers/src/lib.rs +++ b/proof/proof-rs/crates/proof-solvers/src/lib.rs @@ -7,18 +7,23 @@ //! truth-table, in process. //! - [`Z3Smt`] (T1) → shells out to `z3` on an SMT-LIB2 goal (assert the //! negation; `unsat` ⇒ valid). [`Z3Server`] keeps `z3` resident across goals. +//! - [`LeanVerifier`] → runs Lean and reports what the kernel accepted. //! -//! The model rungs are honest stand-ins that gate on `GoalKind` until the real -//! backends are wired behind the identical [`Solver`] trait: +//! The model rungs are stand-ins that gate on `GoalKind` until real backends are +//! wired behind the identical [`Solver`] trait: //! //! - [`SmallModel`] (T2) → a distilled in-domain prover. //! - [`FrontierModel`] (T3) → a frontier reasoning model; the last resort. //! - [`Automation`] / [`Smt`] → the original `GoalKind`-gated stand-ins, kept for //! [`reference_ladder`]. //! -//! A solver returns `Proved` only when a verifier would accept the artifact — -//! correctness is never traded for energy. The real rungs run the tool and -//! report what actually happened; the stand-ins model the rung's reach. +//! **A solver returns `Proved` only when a verifier would accept the artifact — +//! correctness is never traded for energy.** The stand-ins cannot honour that on +//! their own: they check nothing, and their "artifact" is a hash of the goal +//! restated. So the contract is held at the *ladder* level instead, by +//! [`Solver::is_reference_stub`] and the two ladder families described below — +//! a stand-in is a routing fixture, never evidence, and never sits beneath a +//! real rung where the router would escalate into it. pub mod prop; @@ -555,8 +560,37 @@ impl Solver for LeanVerifier { } } +// ── Two families of ladder, and why they must not be mixed ────────────── +// +// A ladder's verdict is only as sound as its weakest rung, because the router +// escalates until something says `Proved` and then stops. Put a fabricating +// stand-in below a real rung and the ladder proves *everything*: the real rungs +// decline, the stand-in obliges, and the cascade reports success. +// +// That is not hypothetical — it shipped twice. The first instance was a +// refutation escalated into a proof (fixed by `Verdict::Refuted` halting the +// router). The second was this one: with `z3` absent, `Z3Smt` returned +// `Unproved`, the router escalated, and `FrontierModel` — which proves any goal +// unconditionally — closed the goal at T3. Every goal on a machine without `z3` +// came back proved, at ~50 J of imaginary energy. +// +// So the families are kept apart by construction and checked by +// `ladder_is_sound`: +// +// * **real** — no rung is a reference stand-in. Exhausting the ladder +// yields `Unproved`, which is the honest answer to "nothing here could +// decide this". An absent tool must produce a weaker claim, never a +// stronger one. +// * **reference** — stand-ins that gate on `GoalKind`. Total by design, which +// is what makes routing and receipt vectors deterministic. Sound as a +// fixture, never as evidence. + /// The pure stand-in ladder, cheapest-first — every rung a `GoalKind`-gated /// model, used by conformance to exercise routing deterministically. +/// +/// **Fixture only.** No rung here checks anything: `Proved` carries a hash of +/// the goal restated, and [`FrontierModel`] closes *any* goal. Use it to pin +/// routing and receipt encoding, never to decide whether something is true. pub fn reference_ladder() -> Vec> { vec![ Box::new(Automation), @@ -566,8 +600,13 @@ pub fn reference_ladder() -> Vec> { ] } -/// A ladder with a real propositional decider at T0 over the stand-ins above. -pub fn real_t0_ladder() -> Vec> { +/// The reference ladder with a real propositional decider at T0. +/// +/// **Fixture only**, like [`reference_ladder`]: T0 is real, but the rungs above +/// it are stand-ins, so the ladder is still total and its verdict still is not +/// evidence. Renamed from `real_t0_ladder` — a mixed ladder under a `real_` +/// name is exactly the confusion that produced the fabrication bug. +pub fn reference_ladder_with_real_t0() -> Vec> { vec![ Box::new(Propositional), Box::new(Smt), @@ -576,25 +615,27 @@ pub fn real_t0_ladder() -> Vec> { ] } -/// Two real rungs: the propositional decider (T0) and `z3` (T1), over the model -/// stand-ins. +/// The real ladder: the propositional decider (T0) and `z3` (T1) — every rung a +/// decision procedure, so a `Proved` verdict is backed by something a verifier +/// would accept. +/// +/// There is no T2/T3 rung because no real one exists yet. When a model backend +/// lands behind the same [`Solver`] trait and can emit a checkable artifact, it +/// joins here; until then the ladder ends at T1 and unreachable goals come back +/// `Unproved`. **A missing rung must never be papered over with a stand-in** — +/// that converts "we could not decide" into "we decided", which is the one +/// error a proof system may not make. +/// +/// With `z3` absent this ladder decides only propositional goals and returns +/// `Unproved` for the rest. That is the intended behaviour: see +/// [`z3_available`] to report the reduced reach honestly rather than hide it. pub fn real_ladder() -> Vec> { - vec![ - Box::new(Propositional), - Box::new(Z3Smt), - Box::new(SmallModel), - Box::new(FrontierModel), - ] + vec![Box::new(Propositional), Box::new(Z3Smt)] } /// Like [`real_ladder`] but with `z3` kept resident at T1. pub fn resident_z3_ladder() -> Vec> { - vec![ - Box::new(Propositional), - Box::new(Z3Server::new()), - Box::new(SmallModel), - Box::new(FrontierModel), - ] + vec![Box::new(Propositional), Box::new(Z3Server::new())] } /// Whether a working `z3` is on PATH — lets callers/tests adapt honestly. @@ -612,6 +653,134 @@ pub fn z3_available() -> bool { mod tests { use super::*; + /// Every rung of a ladder that calls itself real must be a decision + /// procedure. This is the structural guard: the fabrication bug was a + /// stand-in sitting where the router could escalate into it, and a shape + /// test catches that at compile-and-test time rather than in an audit. + #[test] + fn ladder_is_sound() { + for (name, ladder) in [ + ("real_ladder", real_ladder()), + ("resident_z3_ladder", resident_z3_ladder()), + ] { + assert!(!ladder.is_empty(), "{name}: a real ladder needs a rung"); + for rung in &ladder { + assert!( + !rung.is_reference_stub(), + "{name}: rung {:?} is not a decision procedure — a stand-in \ + here lets the router escalate a failure into a fabricated proof", + rung.tier() + ); + } + } + + // `is_reference_stub` defaults to `false`, so a stand-in that forgets to + // override it would pass the loop above unnoticed. Pin the exact tiers + // too: adding any rung to a real ladder trips this even if the new rung + // lies about what it is. Update these deliberately when a real T2/T3 + // backend actually lands. + assert_eq!( + real_ladder().iter().map(|r| r.tier()).collect::>(), + vec![Tier::Automation, Tier::Smt], + "real_ladder membership changed — is the new rung a decision procedure?" + ); + assert_eq!( + resident_z3_ladder() + .iter() + .map(|r| r.tier()) + .collect::>(), + vec![Tier::Automation, Tier::Smt], + "resident_z3_ladder membership changed — is the new rung a decision procedure?" + ); + + // And the fixture ladders are honestly declared as such, so the marker + // means something in both directions. + assert!( + reference_ladder() + .iter() + .all(|r| r.is_reference_stub()), + "reference_ladder must be entirely stand-ins" + ); + assert!( + reference_ladder_with_real_t0() + .iter() + .filter(|r| r.is_reference_stub()) + .count() + == 3, + "reference_ladder_with_real_t0 is one real rung under three stand-ins" + ); + } + + /// The regression itself, driven through the real router. + /// + /// A goal no decision procedure can discharge must come back `Unproved`. + /// Before the fix this returned **Proved, closed by `BigModel`, at ~50 J** — + /// on any machine without `z3`, every goal did. The energy figure was as + /// invented as the proof. + /// + /// Holds with or without `z3` on PATH: `z3` cannot parse prose, so it + /// declines either way, which is what makes this a stable assertion rather + /// than one that changes meaning with the runner image. + #[test] + fn ladder_never_fabricates_a_proof_when_a_rung_is_absent() { + use proof_cascade::{ProofCache, Router}; + + let unreachable = ProofGoal::new( + "every even integer > 2 is the sum of two primes", + "lean4", + GoalKind::Hard, + ); + + let mut cache = ProofCache::default(); + let out = Router::new(real_ladder()).prove(&unreachable, &mut cache); + + assert!( + !out.proved, + "a goal no decision procedure decided came back proved, closed by {:?}", + out.closed_by + ); + assert!( + out.closed_by.is_none(), + "nothing may close a goal it did not decide (closed_by = {:?})", + out.closed_by + ); + assert!( + !out.attempts.iter().any(|a| a.proved), + "no rung may report success here" + ); + // No model rung may even be on this ladder to be escalated into. + assert!( + !out.attempts + .iter() + .any(|a| matches!(a.tier, Tier::SmallModel | Tier::BigModel)), + "a model stand-in ran on the real ladder" + ); + } + + /// The reference ladder is *total* — it closes every goal, including the one + /// above that no real solver can touch. That totality is exactly why it is + /// useful for pinning routing determinism and exactly why it must never sit + /// under a real rung. Kept as a test so the property is asserted rather than + /// assumed by the ladder-family split. + #[test] + fn reference_ladder_is_total_which_is_why_it_is_fixture_only() { + use proof_cascade::{ProofCache, Router}; + + let unreachable = ProofGoal::new( + "every even integer > 2 is the sum of two primes", + "lean4", + GoalKind::Hard, + ); + let mut cache = ProofCache::default(); + let out = Router::new(reference_ladder()).prove(&unreachable, &mut cache); + + assert!( + out.proved, + "the stand-in ladder closes everything by design" + ); + assert_eq!(out.closed_by, Some(Tier::BigModel)); + } + #[test] fn each_rung_reaches_its_kind() { let triv = ProofGoal::new("x = x", "lean4", GoalKind::Trivial); @@ -641,7 +810,7 @@ mod tests { .attempt(&ProofGoal::new("∀ n, n+0 = n", "lean4", GoalKind::General)) .verdict .is_proved()); - assert_eq!(real_t0_ladder().len(), 4); + assert_eq!(reference_ladder_with_real_t0().len(), 4); } #[test] @@ -652,7 +821,7 @@ mod tests { GoalKind::Decidable, ); let a = Z3Smt.attempt(&valid); - assert_eq!(real_ladder().len(), 4); + assert_eq!(real_ladder().len(), 2); // decision procedures only if z3_available() { assert!(a.verdict.is_proved()); assert!(a.energy.uj() >= 1); @@ -717,7 +886,7 @@ mod tests { assert!(server.attempt(&comm).verdict.is_proved()); assert!(server.attempt(&thm).verdict.is_proved()); // still healthy after prose } - assert_eq!(resident_z3_ladder().len(), 4); + assert_eq!(resident_z3_ladder().len(), 2); // decision procedures only assert!(looks_like_smt("(assert (> x 0))")); assert!(!looks_like_smt("∃ continuous f")); assert!(!looks_like_smt("(unbalanced"));