P1-0 (B): claims ledger — run every TESTED row, reconcile test/proof counts

.github/workflows/e2e.yml

@@ -21,16 +21,17 @@ jobs:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
         with:
-          toolchain: v1
+          toolchain: stable
+          components: clippy, rustfmt
       - uses: Swatinem/rust-cache@v2.9.2
       - name: Build
         run: cargo build --release
       - name: Unit + P2P tests
         run: cargo test --all -- --test-threads=1
       - name: Clippy
-        run: cargo clippy --all -- -D warnings || true
+        run: cargo clippy --all --all-targets -- -D warnings
       - name: Format check
-        run: cargo fmt --all -- --check || true
+        run: cargo fmt --all -- --check
 
   benchmarks:
     name: Criterion Benchmarks
@@ -39,6 +40,8 @@ jobs:
     steps:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
+        with:
+          toolchain: stable
       - uses: Swatinem/rust-cache@v2.9.2
       - name: Run benchmarks
         run: cargo bench -- --output-format bencher 2>/dev/null || echo "Benchmarks completed"
@@ -50,6 +53,8 @@ jobs:
     steps:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
+        with:
+          toolchain: stable
       - uses: Swatinem/rust-cache@v2.9.2
       - name: Build release
         run: cargo build --release
@@ -89,6 +94,8 @@ jobs:
     steps:
       - uses: actions/checkout@v7.0.1
       - uses: dtolnay/rust-toolchain@v1
+        with:
+          toolchain: stable
       - name: Install panic-attack
         run: cargo install --git https://github.com/hyperpolymath/panic-attacker.git 2>/dev/null || echo "panic-attack unavailable"
       - name: Run assail scan

PROOF-NEEDS.adoc

@@ -1,3 +1,3 @@
 == PROOF-NEEDS.md — januskey
 
 === Current State
@@ -45,6 +45,35 @@
 januskey-cli
 |===
 
+=== Claims ledger
+
+Every claim JanusKey makes about its own correctness is a row here, with one
+of five statuses: PROVEN (a checker accepts a proof), TESTED (a named test
+passes), ASSUMED (relied on, not checked), DESIGNED (specified, not built) or
+OPEN (not true yet). `cargo run -p dashboard-check -- --check .` runs the
+command of every PROVEN and TESTED row and fails unless it exits 0 and, for
+TESTED, prints the named test passing. The counts on README, EXPLAINME,
+TOPOLOGY and READINESS must equal what that checker measures: tests by
+`cargo test --workspace --locked -- --list`, proofs by the PROVEN rows below.
+Each row is one line; the checker rejects a wrapped row.
+
+There are no PROVEN rows: the Idris2 ABI does not typecheck (#145), so no
+proof in this repository is checked by anything.
+
+[cols="3,1,3,3",options="header"]
+|===
+|Claim |Status |Artefact |Command
+|Obliterating a path shreds its unshared blobs and log entries, and undo then has nothing |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::obliterate_scrubs_blobs_log_and_undo` |`cargo test --locked -p januskey --test obliteration_cas_test obliterate_scrubs_blobs_log_and_undo`
+|Obliteration keeps a blob another path still references |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::obliterate_keeps_blob_shared_with_another_path` |`cargo test --locked -p januskey --test obliteration_cas_test obliterate_keeps_blob_shared_with_another_path`
+|`jk obliterate` scrubs the store end to end through the CLI |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::cli_obliterate_scrubs_store_and_undo_has_nothing` |`cargo test --locked -p januskey --test obliteration_cas_test cli_obliterate_scrubs_store_and_undo_has_nothing`
+|Execute then undo restores the prior state (property test over generated ops) |TESTED |`crates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity` |`cargo test --locked -p januskey --test property_tests execute_then_undo_is_identity`
+|Content store round-trips arbitrary bytes (property test) |TESTED |`crates/reversible-core/tests/property_tests.rs::content_store_roundtrip` |`cargo test --locked -p reversible-core --test property_tests content_store_roundtrip`
+|A transaction rolled back ends RolledBack with none active (property test) |TESTED |`crates/reversible-core/tests/property_tests.rs::transaction_begin_rollback_roundtrip` |`cargo test --locked -p reversible-core --test property_tests transaction_begin_rollback_roundtrip`
+|The audit log verifies an untampered three-entry chain as valid (tamper detection is not tested) |TESTED |`crates/januskey-cli/src/attestation.rs::test_audit_log_chain_integrity` |`cargo test --locked -p januskey --lib test_audit_log_chain_integrity`
+|The Idris2 ABI typechecks and its six security claims are proved |OPEN |#145 |-
+|Every operation is reversible (MPR), as a theorem linked to the Rust |OPEN |#145 |-
+|===
+
 === Recommended Prover
 
 *Idris2* — Create `+src/abi/+` with dependent type proofs for

READINESS.adoc

@@ -8,8 +8,8 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 
 === CRG Grade: D (Alpha — Unstable)
 
-*Justification:* Tests exist and pass (67 total), proofs exist (30
-Idris2, unchecked in CI), benchmarks exist (5 Criterion groups). But: no
+*Justification:* 119 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
+Idris2 ABI does not typecheck, so 0 proofs are checked (#145); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips,
 benchmarks measured fake crypto until this session. RSR compliance
 present. Deep annotation incomplete (TOPOLOGY.md exists but
@@ -60,11 +60,11 @@ handling
 
 |15 |Compatibility |MISSING |0 |— |No version migration tests
 
-|16 |Proof regression |✓ |30 proofs |`+just test-proofs+` |Idris2 –check
+|16 |Proof regression |✗ |0 checked (#145) |`+just test-proofs+` |Idris2 –check
 (requires idris2 binary)
 |===
 
-*Total passing:* 67 tests + 5 benchmark groups + 30 Idris2 proofs *Total
+*Total declared:* 119 tests + 5 benchmark groups; 0 Idris2 proofs checked (#145) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix

TOPOLOGY.adoc

@@ -1,5 +1,5 @@
 == JanusKey — Project Topology
-// Last updated: 2026-07-02 (completion dashboard reconciled to STATE.a2ml / READINESS; date carried over from TOPOLOGY.md, dropped by the md-to-adoc migration #102)
+// Last updated: 2026-10-02 (test and proof counts reconciled to the PROOF-NEEDS claims ledger by dashboard-check)
 
 === System Architecture
 
@@ -77,9 +77,9 @@ SECURITY (honest)
 INTERFACES & RESEARCH
   CLI Interface (jk)                ████████░░  ~85%   Full command set; no user testing yet
   MPR Methodology                   ████░░░░░░  ~40%   Design documented; FORMAL PROOFS PENDING
-                                                        (30 Idris2 proofs unchecked in CI; not linked
+                                                        (Idris2 ABI does not typecheck, #145; 0 proofs checked; not linked
                                                         to the Rust)
-  Testing (READINESS matrix)        ██████░░░░  ~60%   67 tests + 5 benches; missing fuzz, mutation,
+  Testing (READINESS matrix)        ██████░░░░  ~60%   119 tests + 5 benches; missing fuzz, mutation,
                                                         chaos, compatibility (Grade D)
 
 REPO INFRASTRUCTURE

benches/januskey_benchmarks.rs

@@ -117,9 +117,8 @@ fn bench_transactions(c: &mut Criterion) {
 
     group.bench_function("begin_commit", |b| {
         b.iter(|| {
-            let mut active = false;
             // Begin
-            active = true;
+            let mut active = true;
             black_box(active);
             // Commit
             active = false;
@@ -156,7 +155,7 @@ fn bench_key_derivation(c: &mut Criterion) {
 
             for _ in 0..1000 {
                 let mut hasher = Sha256::new();
-                hasher.update(&hash);
+                hasher.update(hash);
                 hash.copy_from_slice(&hasher.finalize());
             }
             black_box(hash);