transactions: check the lifecycle invariant at load (T-12); one Agda pin across CI

.github/workflows/dashboard-check.yml

@@ -24,20 +24,63 @@ jobs:
     runs-on: ubuntu-latest
     timeout-minutes: 30
     # PROVEN rows of the PROOF-NEEDS claims ledger run their checker, so this
-    # job needs Idris2 (the same pinned image as idris-abi.yml) and Agda.
-    container:
-      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
+    # job needs Idris2 and Agda. Each runs from the image its own proof job
+    # pins, so a green dashboard re-runs the same prover version as the
+    # receipt: Idris2 from idris-abi.yml's image, Agda 2.6.4.3 from
+    # agda-proofs.yml's Debian image (before 2026-11-09 this job installed
+    # Ubuntu's Agda 2.6.3, a second, different pin). `agda` and `idris2` on
+    # PATH are wrappers that run those images over the checkout.
+    env:
+      IDRIS2_IMAGE: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
+      AGDA_BASE: debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f
     steps:
-      - name: Install Agda, and curl for rustup
-        run: |
-          apt-get update
-          apt-get install --no-install-recommends -y ca-certificates curl agda-bin=2.6.3-1build1
-          agda --version
-          idris2 --version
-
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
 
+      - name: Provers from the pinned images (Agda 2.6.4.3, Idris2)
+        run: |
+          printf 'FROM %s\nRUN apt-get update && apt-get install --no-install-recommends -y agda-bin=2.6.4.3-1+b2 && rm -rf /var/lib/apt/lists/*\n' \
+            "$AGDA_BASE" | docker build -t januskey-agda:2.6.4.3 -
+          docker pull -q "$IDRIS2_IMAGE"
+          mkdir -p "$RUNNER_TEMP/provers"
+          # Agda runs as the runner user. The Idris2 image keeps its toolchain
+          # under /root, so idris2 runs as root, and the wrapper then hands any
+          # root-owned file it left in the working tree back to the runner: a
+          # checker that cannot clean up its scratch copy would fail its row.
+          # The Agda gate writes its dependency graphs under mktemp -d, so the
+          # temporary directory is mounted too. It reads the prover's own
+          # lib/prim (Agda.Primitive, Agda.Builtin.*) on the host, at the path
+          # `agda --print-agda-dir` reports, so that directory is copied out of
+          # the image to the same path here.
+          cat > "$RUNNER_TEMP/provers/agda" <<'WRAP'
+          #!/usr/bin/env bash
+          tmp="${TMPDIR:-/tmp}"
+          exec docker run --rm --user "$(id -u):$(id -g)" -e HOME=/tmp -e LC_ALL=C.UTF-8 \
+            -v "$PWD:$PWD" -v "$tmp:$tmp" -w "$PWD" --entrypoint agda januskey-agda:2.6.4.3 "$@"
+          WRAP
+          agda_dir="$(docker run --rm --entrypoint agda januskey-agda:2.6.4.3 --print-agda-dir)"
+          sudo mkdir -p "$agda_dir/lib"
+          sudo chown "$(id -u):$(id -g)" "$agda_dir/lib"
+          cid="$(docker create januskey-agda:2.6.4.3)"
+          docker cp "$cid:$agda_dir/lib/prim" "$agda_dir/lib/prim"
+          docker rm -f "$cid" >/dev/null
+          test -f "$agda_dir/lib/prim/Agda/Primitive.agda"
+          cat > "$RUNNER_TEMP/provers/idris2" <<'WRAP'
+          #!/usr/bin/env bash
+          docker run --rm -e LC_ALL=C.UTF-8 -v "$PWD:$PWD" -w "$PWD" --entrypoint "" "$IDRIS2_IMAGE" idris2 "$@"
+          rc=$?
+          docker run --rm -v "$PWD:$PWD" --entrypoint "" "$IDRIS2_IMAGE" \
+            find "$PWD" -xdev -uid 0 -exec chown -h "$(id -u):$(id -g)" {} +
+          exit "$rc"
+          WRAP
+          chmod +x "$RUNNER_TEMP"/provers/*
+          echo "$RUNNER_TEMP/provers" >> "$GITHUB_PATH"
+
+      - name: Verify the prover versions
+        run: |
+          test "$(agda --version)" = 'Agda version 2.6.4.3'
+          idris2 --version
+
       - uses: dtolnay/rust-toolchain@v1
         with:
           toolchain: stable

.machine_readable/6a2/STATE.a2ml

@@ -44,7 +44,7 @@ property-tests = "9 (2026-04-03 assessment, not re-derived)"
 regression-tests = "5 (2026-04-03 assessment, not re-derived)"
 idris2-proofs = "12 PROVEN ledger rows (the former 30 counted lemmas before the tautology purge; PROOF-NEEDS.adoc is authoritative)"
 benchmarks = "5 Criterion groups (no baseline recorded)"
-total = "5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check"
+total = "143 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check"
 
 [proof-grades]
 # Proof Witness Grades, standards 3-practice/PROOF-POLICY.adoc §8 (the
@@ -55,7 +55,7 @@ receipt-commit = "see docs/theory/PROOF-GRADES.adoc, The PWG-3 receipt (the 4afb
 receipt-prover = "Agda 2.6.4.3 (agda-bin=2.6.4.3-1+b2); no standard library; resource-algebra pinned at cf9235c"
 receipt-flags = "--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check (PROOF-POLICY §2.1 canonical, plus two stricter flags)"
 not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §8.1); all 33 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows"
-open-obligations = "Rocq and Lean legs for the four PWG-3 rows (PROOF-POLICY §2); one Agda version across CI (agda-proofs pins 2.6.4.3, dashboard-check installs 2.6.3); no Creusot or Verus proof on the Rust, so no Rust behaviour is proved"
+open-obligations = "Rocq and Lean legs for the four PWG-3 rows (PROOF-POLICY §2); no Creusot or Verus proof on the Rust, so no Rust behaviour is proved"
 claimed-higher = "PWG-2ii for T-1 only (Rocq and Lean legs re-proved and reconciled); no PWG-2i or PWG-1 is claimed"
 
 [test-categories-complete]

CHANGELOG.adoc

@@ -17,6 +17,12 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 ==== Added
 
+* feat(transactions): a transaction log read from disk is checked against the
+lifecycle invariant the Agda theorems preserve, and refused if it breaks it
+(T-12, TESTED, evidence towards T-10 at the load boundary); the unused
+`TransactionManager::active_mut` is removed
+* ci(dashboard): the dashboard job runs Agda 2.6.4.3 from the proof job's
+pinned image (one Agda version across CI, owner decision 2026-11-09)
 * feat(proofs): `Epistemic.agda` replaces the vacuous Idris `Knows` modality with
 knowledge as indiscriminability: ignorance, obliteration and rotation-forgetting
 become propositions, with two expected-rejection fixtures; new ledger row E-1m

PROOF-NEEDS.adoc

@@ -72,13 +72,14 @@ tables must agree.
 | T-2 | In any single-active log (records with a decidable key and an active or settled phase), opening a fresh active record, a key- and phase-preserving edit, and a settling transition each preserve the invariant and rewrite only the active record, so a settled one is never modified | PROVEN | `+SingleActiveLog.{begin-good,modify-good,finish-good,update-active}+`; `+tests/reject-agda/SettleWithoutSettling.agda+` refused; januskey's instance is `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused
 | T-3 | In any single-active log satisfying the invariant, at most one record is active, and exactly one when the pointer is set | PROVEN | `+SingleActiveLog.at-most-one-active+` (januskey's transactions are an instance)
 | T-4 | A rollback that fails part-way can be retried to completion | TESTED | `+rollback_resume_test+` drives the real `+jk+`: after one undo error and a repair, `+jk rollback+` skips the already undone operation and finishes (before the fix the retry stopped at it every time, reproduced 2026-10-26); fixed in `+cmd_rollback+`
-| T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by rename rather than overwritten in place, with an fsync before the rename by construction (no test observes the fsync) (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins)
+| T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by rename rather than overwritten in place, with an fsync before the rename by construction (no test observes the fsync) (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort (owner decision 2026-11-09), because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins)
 | 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 replaced by rename, never overwritten in place (the sync before the rename is there by construction; no test observes it); a log edit (`+mark_undone+`, `+prune+`, `+purge_path_entries+`) whose save fails is not applied in memory and applies exactly once on retry; an append whose save fails keeps its record for the next save | TESTED | `+metadata::tests::{failed_save_leaves_every_mutation_unapplied,a_failed_append_keeps_its_record_for_the_next_save,save_replaces_the_log_atomically,save_replaces_rather_than_overwrites_the_log}+` and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+`, each checked against a mutant in #168. Not claimed: a failure after the temporary file exists (during the write, sync or rename) is not injected; the rename's atomicity is the filesystem's guarantee
-| T-9 | A forward file change is never left without a log record: `+execute_*+` changes the filesystem and then appends, so a crash or failed save between the two leaves a change the log does not know about | OPEN | needs a write-ahead intent record (a design decision); split out of T-8 in #168
+| T-9 | A forward file change is never left without a log record: `+execute_*+` changes the filesystem and then appends, so a crash or failed save between the two leaves a change the log does not know about | OPEN | needs a write-ahead intent record: owner decision 2026-11-09 to close it with a write-ahead intent log (an intent record written before the file change, completed or undone at startup), not built yet; split out of T-8 in #168
 | T-11 | An undo whose `+mark_undone+` fails to persist can be retried safely: `+undo+` records the inverse as its own operation (each helper calls `+execute+`), then marks the original, so a failed mark leaves the original unmarked and a retry re-applies the inverse or fails against the changed filesystem | OPEN | the inverse is recorded, unlike T-9; the fix is an idempotent undo (find the existing inverse record before re-applying), not write-ahead intent
 | T-10 | januskey's TransactionManager is an instance of the single-active log: the Rust begin, add_operation, commit and mark_rolled_back refine the abstract open, edit and settle transitions, as the hand-written instance in `+TransactionAtomicity.agda+` Part B assumes | OPEN | engineering (PROOF-POLICY §1): Creusot/Pearlite or Verus contracts on `+crates/reversible-core/src/transaction.rs+`; the instance itself is a transcription, like G-2
+| T-12 | A transaction log read from disk satisfies the invariant `+Good+` that T-2 and T-3 preserve, so their premise holds for a loaded log as well as for one this code wrote; a log that breaks it is refused as corrupted, not loaded | TESTED | `+transaction::tests::a_loaded_log_that_breaks_the_invariant_is_refused+` (five ways of breaking `+Good+`: a pointer to a missing or a settled transaction, an Active one with no pointer, two Active, a pointer whose first transaction with that id is settled) and the positive control `+a_log_the_manager_wrote_loads_back+`; mutants (no check at load, last-with-id instead of first, no stray-Active scan) each fail the first test. The unused `+active_mut+`, which could change a transaction outside the four transitions, is removed. Evidence towards T-10 at the load boundary, not the refinement itself
 | 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)
@@ -289,6 +290,8 @@ the status table above.
 |T-9: A forward file change is never left without a log record (execute changes the filesystem, then appends; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |-
 |T-11: An undo whose mark_undone fails to persist can be retried safely (the inverse is recorded as its own operation before the mark; needs an idempotent undo) |OPEN |`crates/januskey-cli/src/operations.rs` |-
 |T-10: januskey's TransactionManager refines the single-active log (Rust begin, add_operation, commit, mark_rolled_back against the abstract transitions; engineering, for Creusot or Verus) |OPEN |`crates/reversible-core/src/transaction.rs` |-
+|T-12: A transaction log read from disk that breaks the lifecycle invariant (pointer to a missing or settled transaction, an Active one with no pointer, two Active, or a settled first transaction with the active id) is refused as corrupted |TESTED |`crates/reversible-core/src/transaction.rs::a_loaded_log_that_breaks_the_invariant_is_refused` |`cargo test --locked -p reversible-core --lib a_loaded_log_that_breaks_the_invariant_is_refused`
+|T-12: Logs the manager writes, idle and busy, satisfy the invariant and load back (the positive control) |TESTED |`crates/reversible-core/src/transaction.rs::a_log_the_manager_wrote_loads_back` |`cargo test --locked -p reversible-core --lib a_log_the_manager_wrote_loads_back`
 |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` |-
 |Every operation is reversible (MPR), as a theorem linked to the Rust (needs G-2 made mechanical, and G-3) |OPEN |`verification/proofs/agda/Reversibility.agda` |-

READINESS.adoc

@@ -8,7 +8,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 
 === CRG Grade: D (Alpha — Unstable)
 
-*Justification:* 142 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
+*Justification:* 143 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
 Idris2 ABI typechecks and 12 proofs are checked (PROVEN ledger rows: ABI, grade, transaction-model and epistemic-model lemmas, not the
 security obligations); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 241 unwrap() calls, E2E mostly skips,
@@ -65,7 +65,7 @@ handling
 (run by idris-abi.yml, agda-proofs.yml and dashboard-check)
 |===
 
-*Total declared:* 141 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five are theory theorems under PROOF-POLICY §8: four at PWG-3 and T-1 at PWG-2ii — see `docs/theory/PROOF-GRADES.adoc`) *Total
+*Total declared:* 143 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five are theory theorems under PROOF-POLICY §8: four at PWG-3 and T-1 at PWG-2ii — see `docs/theory/PROOF-GRADES.adoc`) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix

TOPOLOGY.adoc

@@ -79,7 +79,7 @@ INTERFACES & RESEARCH
   MPR Methodology                   ████░░░░░░  ~40%   Design documented; FORMAL PROOFS PENDING
                                                         (Idris2 ABI typechecks; 12 proofs checked: ABI, grade, transaction-model and epistemic-model
                                                         lemmas, not the security obligations; MPR not linked to the Rust)
-  Testing (READINESS matrix)        ██████░░░░  ~60%   142 tests + 5 benches; missing fuzz, mutation,
+  Testing (READINESS matrix)        ██████░░░░  ~60%   143 tests + 5 benches; missing fuzz, mutation,
                                                         chaos, compatibility (Grade D)
 
 REPO INFRASTRUCTURE