proofs: write the receipt under the new PROOF-POLICY 8.5 and add APP-1 to APP-4

.github/workflows/agda-proof-policy.yml

@@ -125,15 +125,18 @@ jobs:
           git init -q "$r"
           git -C "$r" remote add origin https://github.com/metadatastician/standards.git
           git -C "$r" config core.sparseCheckout true
-          printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout"
-          git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4
+          printf '1-formats/deed/tools/\nscripts/check-proof-receipt.sh\nscripts/proof-inputs-sha256.sh\n' > "$r/.git/info/sparse-checkout"
+          git -C "$r" fetch -q --depth 1 origin e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d
           git -C "$r" checkout -q FETCH_HEAD
 
       - name: Golden path (just check), then its controls
         if: ${{ !cancelled() && steps.toolchain.outcome == 'success' }}
         env:
           MATHESIS_STANDARDS: ${{ runner.temp }}/receipt-reader
         run: |
+          # The receipt's git checks (PROOF-POLICY §8.5.3) need origin/main with its
+          # history: the checkout is shallow.
+          git fetch -q --no-tags --unshallow origin +refs/heads/main:refs/remotes/origin/main
           guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- sh -euc '
             just --version
             bun --version

.github/workflows/hypatia-scan.yml

@@ -31,7 +31,7 @@ jobs:
       contents: read
       security-events: write
     env:
-      HYPATIA_SHA: 'd73f76b5cb7a35e1aa1024c916aee7cb4f9b141e'
+      HYPATIA_SHA: '6693f9aed8e4383f78a3d01b600b32663bf7a45c'
     steps:
       - name: Checkout repository
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
@@ -53,7 +53,7 @@ jobs:
             ~/hypatia
             ~/.hex
             ~/.mix
-          key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-d73f76b5cb7a35e1aa1024c916aee7cb4f9b141e
+          key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-6693f9aed8e4383f78a3d01b600b32663bf7a45c
 
       - name: Build pinned Hypatia scanner
         run: |

.github/workflows/proven-tests.yml

@@ -56,8 +56,8 @@ jobs:
           git init -q "$r"
           git -C "$r" remote add origin https://github.com/metadatastician/standards.git
           git -C "$r" config core.sparseCheckout true
-          printf '1-formats/deed/tools/\n' > "$r/.git/info/sparse-checkout"
-          git -C "$r" fetch -q --depth 1 origin be39f900665fb7c042c05d1165da018adc1860f4
+          printf '1-formats/deed/tools/\nscripts/check-proof-receipt.sh\nscripts/proof-inputs-sha256.sh\n' > "$r/.git/info/sparse-checkout"
+          git -C "$r" fetch -q --depth 1 origin e5a39d7e5c66f9d24d7e0ffa3f8dbd01f2d42d9d
           git -C "$r" checkout -q FETCH_HEAD
           for f in verification/receipts/*_praxis.deed; do
             bun "$r/1-formats/deed/tools/deed_lint.js" --proof-receipt-json "$f"

Justfile

@@ -707,7 +707,7 @@ uncloak:
 # The Mathesis golden path (re-anchoring plan WO 2.5). CI runs it in the pinned
 # Guix (agda-proof-policy.yml). A stale view or a failing proof fails.
 # Golden path: every generated view matches its data, every gated proof checks
-check: check-views site-check check-proofs
+check: check-views site-check check-proofs receipt-check
 
 # Needs bun, network for the receipts, and MATHESIS_STANDARDS (see `registry`).
 # Views current: catalogue, census tests, atlas, claims registry, bridges and
@@ -772,6 +772,14 @@ registry-check:
     bun scripts/registry/theory-ledger.mjs verify
     bun test tests/registry/
 
+# The git checks of PROOF-POLICY §8.5.3 on the receipt of Mathesis: its
+# :source-commit is on origin/main, each current receipt's inputs manifest holds
+# at its commit, and each echo's witness holds. The shared checker of the pinned
+# standards commit runs them (MATHESIS_STANDARDS, as above). Needs origin/main
+# with its history.
+receipt-check:
+    bun scripts/registry/claims-registry.mjs receipt
+
 # Append each change of the theory shelf to docs/theory/ledger.jsonl, the only
 # way the ledger changes (needs MATHESIS_STANDARDS, as above). A note tells the
 # story: just theory-ledger "THY-2 admitted after its Lean leg landed"

build/manifest.scm

@@ -13,6 +13,9 @@
 (specifications->manifest
  (list "git" "bash" "coreutils" "nss-certs" "just" "mise"
        "shellcheck" "chez-scheme" "gmp" "gcc-toolchain" "zig"
+       ;; jq: the shared git checker of proof receipts (PROOF-POLICY §8.5.3) reads
+       ;; the reader's JSON with it.
+       "jq"
        ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)).
        ;; No agda-stdlib: its Guix package does not build, and no proof here
        ;; imports it (owner ruling 2026-11-10).

docs/atlas/claims/claims.jsonl

@@ -1,12 +1,12 @@
-{"agda":{"module":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference","names":["eval-low"]},"claim":"N-2","id":"hyperpolymath/secret-types#N-2","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Public expressions read the same in low-equivalent stores","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference","names":["confine"]},"claim":"N-3","id":"hyperpolymath/secret-types#N-3","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Confinement: under a secret program counter the public variable is unchanged, loops included","status_doc":"PROOF-STATUS.adoc"}
-{"agda":null,"claim":"N-4","id":"hyperpolymath/secret-types#N-4","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks","status_doc":"PROOF-STATUS.adoc"}
-{"agda":null,"claim":"N-5","id":"hyperpolymath/secret-types#N-5","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another","status_doc":"PROOF-STATUS.adoc"}
-{"agda":null,"claim":"N-6","id":"hyperpolymath/secret-types#N-6","kind":"demonstration","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate)","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference.Generic","names":["tini"]},"claim":"N-7","id":"hyperpolymath/secret-types#N-7","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Countermodels","names":["NoUpper₁.refutes","NoUpper₂.refutes","NoDownClosure.refutes","NoTrans.refutes"]},"claim":"N-8","id":"hyperpolymath/secret-types#N-8","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers","status_doc":"PROOF-STATUS.adoc"}
-{"agda":{"module":"SecretTypes.Noninterference.OutcomeVisibility","names":["termination-sensitive-fails"]},"claim":"N-9","id":"hyperpolymath/secret-types#N-9","kind":"theorem","receipt":{"path":"verification/receipts/agda-grade3_praxis.deed","sha256":"72525272e723ac23a62ef22914a6b1777b8a6f639682ef2c69c12129c2356025"},"repo":"hyperpolymath/secret-types","source_commit":"eee4e4038503f098c31181e792f66834eda5f523","statement":"If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference","names":["tini"]},"claim":"N-1","id":"hyperpolymath/secret-types#N-1","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"TINI at the two-point lattice: two finishing runs of a well-typed command from low-equivalent stores end low-equivalent, fuels independent","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference","names":["eval-low"]},"claim":"N-2","id":"hyperpolymath/secret-types#N-2","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Public expressions read the same in low-equivalent stores","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference","names":["confine"]},"claim":"N-3","id":"hyperpolymath/secret-types#N-3","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Confinement: under a secret program counter the public variable is unchanged, loops included","status_doc":"PROOF-STATUS.adoc"}
+{"agda":null,"claim":"N-4","id":"hyperpolymath/secret-types#N-4","kind":"demonstration","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"The typing side-condition is load-bearing: an explicit and an implicit flow are each refused and each actually leaks","status_doc":"PROOF-STATUS.adoc"}
+{"agda":null,"claim":"N-5","id":"hyperpolymath/secret-types#N-5","kind":"demonstration","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another","status_doc":"PROOF-STATUS.adoc"}
+{"agda":null,"claim":"N-6","id":"hyperpolymath/secret-types#N-6","kind":"demonstration","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Laws census: generic TINI uses exactly the two upper-bound laws and the observer's down-closure (law-ablation certificate)","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference.Generic","names":["tini"]},"claim":"N-7","id":"hyperpolymath/secret-types#N-7","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"TINI over the Lattice record: for every variable set with decidable equality, lattice, labelling and down-closed observer, two finishing runs of a well-typed command from stores agreeing on what the observer sees end agreeing on it","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Countermodels","names":["NoUpper₁.refutes","NoUpper₂.refutes","NoDownClosure.refutes","NoTrans.refutes"]},"claim":"N-8","id":"hyperpolymath/secret-types#N-8","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"Each census law is necessary: dropping an upper-bound law or observer down-closure admits a well-typed leaking program; transitivity is necessary for principal observers","status_doc":"PROOF-STATUS.adoc"}
+{"agda":{"module":"SecretTypes.Noninterference.OutcomeVisibility","names":["termination-sensitive-fails"]},"claim":"N-9","id":"hyperpolymath/secret-types#N-9","kind":"theorem","receipt":{"path":"verification/receipts/agda_praxis.deed","sha256":"4ed7e550e399074cc8a93bd190f193a0fea78de97d54e27889263b9d386ce9cc"},"repo":"hyperpolymath/secret-types","source_commit":"4ed067220f1357b37f7d54c5ae0690ff35b292bd","statement":"If an observer sees finishing versus not finishing, termination-sensitive noninterference is false for the current typing rules","status_doc":"PROOF-STATUS.adoc"}
 {"agda":{"module":"Lintel.Lattice","names":["⊑-refl","⊑-trans","⊑-antisym","⊔-upper₁","⊔-upper₂","⊔-least","⊓-lower₁","⊓-lower₂","⊓-greatest","anyone-least","no-one-greatest","no-one-⋢-anyone","_⊑?_"]},"claim":"L-1","id":"metadatastician/lintel#L-1","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"A lattice, not just a poset: ⊑ is a decidable partial order, ⊔ and ⊓ are least upper and greatest lower bounds, anyone is least and no-one greatest","status_doc":"README.adoc"}
 {"agda":{"module":"Lintel.Lattice","names":["⊑-readers","readers-⊑","observes-flow","flow-observes"]},"claim":"L-2","id":"metadatastician/lintel#L-2","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"⊑ is reverse inclusion of reader sets; a role sees a label exactly when the label may flow to that role's observer level","status_doc":"README.adoc"}
 {"agda":{"module":"Lintel.Instance","names":["reader-sets"]},"claim":"L-3","id":"metadatastician/lintel#L-3","kind":"theorem","receipt":null,"repo":"metadatastician/lintel","source_commit":"a0f2bae9cac07cd97b2395d10d0eb05f8ae1c7d1","statement":"The laws secret-types' generic TINI needs hold here, packed as an instance of its Lattice record","status_doc":"README.adoc"}