ci: re-pin standards callers to metadatastician/standards@a797d30; record the proof audit; propose crypto-shredding (ADR-0002)

.github/workflows/actions.lock

@@ -15,7 +15,7 @@ workflows:
         - 'actions/upload-pages-artifact@v5.0.0'
         - 'haskell-actions/setup@v2.12.1'
     '.github/workflows/codeql.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/dashboard-check.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
@@ -30,21 +30,21 @@ workflows:
         - 'dtolnay/rust-toolchain@v1'
         - 'swatinem/rust-cache@v2.9.3'
     '.github/workflows/governance.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/hypatia-scan.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/idris-abi.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
     '.github/workflows/mirror.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/rust-ci.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/scorecard.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/secret-scanner.yml':
-        - 'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/squabble.yml':
         - 'actions/checkout@v7.0.1'
         - 'hyperpolymath/cicd-squabbler@79d7dbacc8a02b4a4388b4a36fe46893b5b7ce73'
@@ -79,6 +79,11 @@ dependencies:
         commit: 'sha1-368f82528645a54fb793d4d04e342629a3f51346'
         owner_id: 44036562
         repo_id: 438112499
+    'actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333':
+        ref: 'v8.0.2'
+        commit: 'sha1-9000827ccba6bdab643e8b6fd33ac0654aef8333'
+        owner_id: 44036562
+        repo_id: 192626254
     'actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f':
         ref: 'v7.0.0'
         commit: 'sha1-bbbca2ddaa5d8feaa63e36b76fdaad77386f024f'
@@ -156,14 +161,15 @@ dependencies:
         commit: 'sha1-c1a34884054fabf0e9de81dbf68f4ba7874e85f1'
         owner_id: 6759885
         repo_id: 1275650185
-    'hyperpolymath/standards@a85aa8e70326cceedae169013a47daee554918b7':
-        ref: 'a85aa8e70326cceedae169013a47daee554918b7'
-        commit: 'sha1-a85aa8e70326cceedae169013a47daee554918b7'
-        owner_id: 6759885
+    'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12':
+        ref: 'a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
+        commit: 'sha1-a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
+        owner_id: 297579217
         repo_id: 1116521501
         uses:
             - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9'
             - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+            - 'actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333'
             - 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9'
             - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed'
             - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8'
@@ -173,7 +179,7 @@ dependencies:
             - 'goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406'
             - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e'
             - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6'
-            - 'swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6'
+            - 'swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0'
             - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555'
     'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e':
         ref: 'v2.5.0'
@@ -185,9 +191,9 @@ dependencies:
         commit: 'sha1-0c5077e51419868618aeaa5fe8019c62421857d6'
         owner_id: 108928776
         repo_id: 512644635
-    'swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6':
-        ref: 'v2'
-        commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6'
+    'swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0':
+        ref: 'v2.9.3'
+        commit: 'sha1-d1527c8f67ef9af357290475d4af4b0fab8f12e0'
         owner_id: 580492
         repo_id: 298565987
     'swatinem/rust-cache@v2.9.3':

.github/workflows/codeql.yml

@@ -32,10 +32,10 @@ permissions:
 
 jobs:
   codeql-actions:
-    uses: hyperpolymath/standards/.github/workflows/codeql-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
+    uses: metadatastician/standards/.github/workflows/codeql-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
     with:
       language: actions
   codeql-rust:
-    uses: hyperpolymath/standards/.github/workflows/codeql-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
+    uses: metadatastician/standards/.github/workflows/codeql-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
     with:
       language: rust

.github/workflows/governance.yml

@@ -34,7 +34,7 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
+    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
     permissions:
       actions: read
       contents: read

.github/workflows/hypatia-scan.yml

@@ -28,5 +28,9 @@ permissions:
 
 jobs:
   hypatia:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
-    secrets: inherit
+    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
+    # Named, not `inherit`: GitHub refuses inheritance from a user account
+    # (hyperpolymath) into an organisation (metadatastician). The reusable
+    # declares this one optional secret.
+    secrets:
+      HYPATIA_SCAN_PAT: ${{ secrets.HYPATIA_SCAN_PAT }}

.github/workflows/mirror.yml

@@ -14,8 +14,21 @@ permissions:
 
 jobs:
   mirror:
-    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
-    secrets: inherit
+    uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
+    # Named, not `inherit`: metadatastician is an organisation and hyperpolymath a
+    # user account, and GitHub refuses `secrets: inherit` across that boundary.
+    # These are the ten secrets mirror-reusable.yml declares (all optional).
+    secrets:
+      GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }}
+      BITBUCKET_SSH_KEY: ${{ secrets.BITBUCKET_SSH_KEY }}
+      CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }}
+      SOURCEHUT_SSH_KEY: ${{ secrets.SOURCEHUT_SSH_KEY }}
+      DISROOT_SSH_KEY: ${{ secrets.DISROOT_SSH_KEY }}
+      GITEA_SSH_KEY: ${{ secrets.GITEA_SSH_KEY }}
+      RADICLE_KEY: ${{ secrets.RADICLE_KEY }}
+      R2_ACCESS_KEY_ID: ${{ secrets.R2_ACCESS_KEY_ID }}
+      R2_SECRET_ACCESS_KEY: ${{ secrets.R2_SECRET_ACCESS_KEY }}
+      R2_AGE_RECIPIENT: ${{ secrets.R2_AGE_RECIPIENT }}
     permissions:
       actions: read
       contents: read

.github/workflows/rust-ci.yml

@@ -21,7 +21,7 @@ permissions:
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
+    uses: metadatastician/standards/.github/workflows/rust-ci-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
     permissions:
       actions: read
       contents: read

.github/workflows/scorecard.yml

@@ -17,5 +17,6 @@ jobs:
       contents: read
       security-events: write
       id-token: write
-    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
-    secrets: inherit
+    uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12
+    # No `secrets:` block: scorecard-reusable.yml declares none, and GitHub
+    # refuses `secrets: inherit` from a user account into an organisation.

.github/workflows/secret-scanner.yml

@@ -22,4 +22,4 @@ jobs:
       actions: read
       security-events: write
       contents: read
-    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@a85aa8e70326cceedae169013a47daee554918b7 # standards main, 2026-10-19 (#1296)
+    uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12

PROOF-NEEDS.adoc

@@ -75,6 +75,11 @@ tables must agree.
 | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path
 | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked
 | T-8 | The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried | OPEN | by inspection: the log now takes the same write, sync, rename path as the transaction log (`+crate::transaction::write_atomic+`), and `+metadata::tests::save_replaces_the_log_atomically+` asserts it, but the crate has not been built since that edit, so the row stays OPEN until the test is green in CI. Retry is unchanged: `+undo+` still runs the undo before `+mark_undone+` persists, so a failed persist still leaves the file undone and the log not
+| S-1 | A content hash that is not `+sha256:+` plus 64 lowercase hex digits never resolves to a path outside the store root | TESTED | `+content_store::tests::malformed_hash_never_leaves_the_store_root+`; fixed in #163 after audit probe P5 showed `+delete+` removing a file outside the store (`+docs/reports/audit/proof-statement-audit-2026-10-27.adoc+`)
+| S-2 | `+store+` repairs a blob a crash left damaged instead of deduplicating against it, and a successful store leaves no temporary file behind | TESTED | not claimed: cleanup after a failed write or rename, whose removal error `+store+` ignores, so a temporary file can remain; not claimed: that the write itself is atomic. `+store+` writes by temporary file, sync and rename, but by construction only; no test injects a failure mid-write. `+content_store::tests::store_repairs_a_blob_truncated_by_a_crash+`, `+store_leaves_no_temp_files_and_count_ignores_strays+`; fixed in #163 (probe P4)
+| L-1 | Editing any field of any audit-log entry makes `+verify_integrity+` fail | OPEN | false today, probes P1 and P2: algorithm, purpose, old_state, new_state, rotated_to and rotated_from are in neither the MAC nor the chain hash, and key_id, fingerprint and reason are chain-hashed only, so on the last entry nothing protects them. The fix is a MAC over every field (a scheme version bump)
+| L-2 | Removing trailing audit-log entries makes `+verify_integrity+` fail | OPEN | false today, probe P3: every prefix of a valid log verifies. Needs an anchor held outside the log (a design decision: signed head, external counter, or witness)
+| O-1 | An `+ObliterationProof+` attests that the content it names was erased | OPEN | false today, probe P6: `+ObliterationProof::generate+` sets `+storage_cleared: true+` unconditionally and `+verify_commitment+` holds for content that was never stored. Either compute the field from the erasure, or stop calling the object a proof
 | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted
 | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved
 | V-3 | aletheia consumes `+reversible-core+` | DESIGNED | ARCHITECTURE.adoc §Deferred — Phase 0 research, no operation types yet
@@ -119,17 +124,21 @@ their artefact is Agda (`+verification/proofs/agda/+`). They are **Grade 3**:
 each type-checks in Agda and none has been translated to an independent
 foundational system, which is mathesis §5's definition as written. The receipt
 is a green `+agda-proofs.yml+` run
-(https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509])
-at commit `+4afb710e86646658f667f10bd6274ee47416bfc7+`, Agda 2.6.4.3, with
-`+resource-algebra+` pinned at `+cf9235c+`. The modules, the gate script, the
-sibling fetch and the workflow are byte-identical at that commit and at this
-one, so the receipt covers these rows as they stand. Mathesis status for them:
+(https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055])
+at commit `+fc188c4+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at
+`+cf9235c+`. That run used the current gate (`+Reversibility+`,
+`+TransactionAtomicity+` and `+Epistemic+` under `+--safe --without-K
+--cubical-compatible+`), and the modules, the gate script, the sibling fetch and
+the workflow are byte-identical at that commit and at this one, so the receipt
+covers these rows, E-1m included, as they stand. (An earlier receipt cited here,
+run 40867211509 at `+4afb710+`, predates `+Epistemic.agda+` and the
+`+--cubical-compatible+` flag, so it never covered E-1m.) Mathesis status for them:
 `+AGDA-VERIFIED+`.
 
 The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under
 PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does
 not grade them: they are PROVEN in the vocabulary above and nothing more. The
-same holds for the 23 TESTED rows, which record observed behaviour and never
+same holds for the 27 TESTED rows, which record observed behaviour and never
 grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not
 Idris2); no Creusot contract exists in this tree, which is why no Rust row is
 graded.
@@ -175,11 +184,11 @@ below are still open.
 |Weak keys break the key store's security model. **Off the `jk` path** — tracked
 here only while `+keys.rs+` remains in this tree (ADR-0001)
 
-|Attestation chain |Chain of custody proofs are unforgeable |Tampered
+|Attestation chain |Chain of custody proofs are unforgeable (false as written: L-1 and L-2 are OPEN, see the 2026-10-27 proof-statement audit) |Tampered
 attestations undermine trust
 
 |Content store integrity |Content-addressed storage never returns wrong
-content |Hash collisions or bugs corrupt stored data
+content (paths confined to the store and damaged blobs repaired: S-1 and S-2 are TESTED; the write is atomic by construction, not by test; reads verify the hash) |Hash collisions or bugs corrupt stored data
 
 |Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log, T-8, now saves by rename but that is unverified)
 |Partial transactions corrupt state
@@ -243,12 +252,19 @@ the status table above.
 |T-5: A save whose temporary file already exists (another writer's) fails without deleting that file or writing the log |TESTED |`crates/reversible-core/src/transaction.rs::a_save_never_removes_a_temporary_file_it_did_not_create` |`cargo test --locked -p reversible-core --lib a_save_never_removes_a_temporary_file_it_did_not_create`
 |T-5: The temporary file has the log's permissions from creation, before any content is written |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_restricted_before_any_content_is_written` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_restricted_before_any_content_is_written`
 |T-5: The temporary file is opened with the log's mode, so it is never more readable than the log at any instant, not only after a later chmod (checked where the umask leaves owner read-write, the usual 022) |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_opened_with_the_logs_mode` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_opened_with_the_logs_mode`
+|S-1: A malformed content hash never resolves to a path outside the store root |TESTED |`crates/reversible-core/src/content_store.rs::malformed_hash_never_leaves_the_store_root` |`cargo test --locked -p reversible-core --lib malformed_hash_never_leaves_the_store_root`
+|S-1: A well-formed content hash keeps the existing two-level blob layout |TESTED |`crates/reversible-core/src/content_store.rs::well_formed_hash_keeps_the_existing_layout` |`cargo test --locked -p reversible-core --lib well_formed_hash_keeps_the_existing_layout`
+|S-2: Storing content again repairs a blob a crash left truncated |TESTED |`crates/reversible-core/src/content_store.rs::store_repairs_a_blob_truncated_by_a_crash` |`cargo test --locked -p reversible-core --lib store_repairs_a_blob_truncated_by_a_crash`
+|S-2: A successful store leaves no temporary file behind, and count ignores stray ones |TESTED |`crates/reversible-core/src/content_store.rs::store_leaves_no_temp_files_and_count_ignores_strays` |`cargo test --locked -p reversible-core --lib store_leaves_no_temp_files_and_count_ignores_strays`
 |G-2: The Idris2 IsCNO / ReversibleOp pair corresponds to the Agda ReversiblePair (by transcription) |ASSUMED |`verification/proofs/agda/Reversibility.agda` |-
 |X-1: Hash one-wayness and physical erasure (cryptographic and physical assumptions) |ASSUMED |`src/abi/JanusKey/ABI/Proofs.idr` |-
 |G-3: The FFI bridge preserves grade 𝟙 (a homomorphism; resource-algebra lists homomorphisms as OPEN) |OPEN |`verification/proofs/agda/Reversibility.agda` |-
 |E-1: An attacker cannot recover obliterated content or use a revoked key (adversaryCannotKnow holds only by construction of the model) |OPEN |`src/abi/JanusKey/ABI/Types.idr` |-
 |E-1m: In a world model, an adversary whose observation excludes the store does not know what it holds (adversary-ignorant), obliteration leaves nothing to recover (obliterate-cuts-recovery, obliterate-ignorance), and rotation leaves no agent — the system included — able to use the old key (rotate-forgets-old); the fixtures AdversaryKnows and OldKeyStillUsable are refused |PROVEN |`verification/proofs/agda/Epistemic.agda::adversary-ignorant` |`bash scripts/check-agda.sh`
 |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |-
+|L-1: Editing any field of any audit-log entry makes verify_integrity fail (false today: audit probes P1, P2) |OPEN |`crates/januskey-cli/src/attestation.rs` |-
+|L-2: Removing trailing audit-log entries makes verify_integrity fail (false today: audit probe P3; needs an external anchor) |OPEN |`crates/januskey-cli/src/attestation.rs` |-
+|O-1: An ObliterationProof attests that the content it names was erased (false today: storage_cleared is hard-coded, audit probe P6) |OPEN |`crates/januskey-cli/src/obliteration.rs` |-
 |T-8: The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried (by inspection: `+MetadataStore::save+` calls `+crate::transaction::write_atomic+`, the path `+transaction.rs+` already tests in T-5; `+metadata::tests::save_replaces_the_log_atomically+` covers the log itself and has not been run) |OPEN |`crates/reversible-core/src/metadata.rs` |-
 |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |-
 |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |-