diff --git a/.github/workflows/dashboard-check.yml b/.github/workflows/dashboard-check.yml index 4475ee4..9f605de 100644 --- a/.github/workflows/dashboard-check.yml +++ b/.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 diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 52721cd..44682e5 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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] diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d2b3b84..dca218a 100644 --- a/CHANGELOG.adoc +++ b/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 diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 2044d30..ea2c068 100644 --- a/PROOF-NEEDS.adoc +++ b/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` |- diff --git a/READINESS.adoc b/READINESS.adoc index b24d504..686e2fd 100644 --- a/READINESS.adoc +++ b/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 diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index a836445..ba10832 100644 --- a/TOPOLOGY.adoc +++ b/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 diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index 4e9bca2..4a2ba58 100644 --- a/crates/reversible-core/src/transaction.rs +++ b/crates/reversible-core/src/transaction.rs @@ -106,6 +106,54 @@ impl TransactionLog { } } +/// Check the lifecycle invariant `Good` of +/// `verification/proofs/agda/SingleActiveLog.agda` (januskey's instance in +/// `TransactionAtomicity.agda` Part B) on a log read from disk. +/// +/// The Agda theorems (ledger rows T-2 and T-3) prove that begin, add_operation, +/// commit and mark_rolled_back preserve `Good`, so a log this code wrote +/// satisfies it. A log read from disk is not guaranteed to — it may have been +/// edited, or written by another version — and without this check the proved +/// invariant would rest on an unchecked premise at load (row T-12; the +/// refinement itself is T-10, OPEN). +/// +/// `Good` holds when either the active pointer is unset and no transaction is +/// Active, or the pointer names an id whose *first* transaction is Active and +/// every other transaction is Committed or RolledBack. `begin`, the update path +/// and the rollback path all select the first transaction with the active id, +/// which is why "first" is the one checked. +fn check_invariant(log: &TransactionLog) -> std::result::Result<(), String> { + let active_at = match &log.active_transaction_id { + None => None, + Some(id) => { + let at = log + .transactions + .iter() + .position(|t| t.id == *id) + .ok_or_else(|| format!("active transaction {id} is not in the log"))?; + if !log.transactions[at].is_active() { + return Err(format!( + "active transaction {id} is {:?}, not Active", + log.transactions[at].state + )); + } + Some(at) + } + }; + match log + .transactions + .iter() + .enumerate() + .find(|(i, t)| t.is_active() && Some(*i) != active_at) + { + Some((_, t)) => Err(format!( + "transaction {} is Active but the active pointer is {:?}", + t.id, log.active_transaction_id + )), + None => Ok(()), + } +} + /// Build a sibling temporary pathname that is unique to this save. /// /// A random component, not a process id, so writers in different PID @@ -233,8 +281,10 @@ impl TransactionManager { Ok(buf) }) })?; - serde_json::from_str(&content) - .map_err(|e| ReversibleError::MetadataCorrupted(e.to_string()))? + let log: TransactionLog = serde_json::from_str(&content) + .map_err(|e| ReversibleError::MetadataCorrupted(e.to_string()))?; + check_invariant(&log).map_err(ReversibleError::MetadataCorrupted)?; + log } else { TransactionLog::new() }; @@ -330,12 +380,6 @@ impl TransactionManager { .and_then(|id| self.log.transactions.iter().find(|t| t.id == *id)) } - /// Get mutable active transaction - pub fn active_mut(&mut self) -> Option<&mut Transaction> { - let active_id = self.log.active_transaction_id.clone()?; - self.log.transactions.iter_mut().find(|t| t.id == active_id) - } - /// Append an operation ID to the active transaction and persist the log. /// /// IDs are recorded in the supplied order without validation or deduplication. @@ -826,4 +870,85 @@ mod tests { .expect("failed to begin first transaction"); assert!(manager.begin(None).is_err()); } + + /// Write `log` where a manager will load it, and try to load it. + fn load(log: &TransactionLog) -> Result { + let tmp = TempDir::new().expect("temp dir"); + let path = tmp.path().join("transactions.json"); + std::fs::write(&path, serde_json::to_string(log).expect("serialise")).expect("write"); + TransactionManager::new(path) + } + + fn tx_in(state: TransactionState, id: &str) -> Transaction { + let mut t = Transaction::new(None); + t.id = id.to_string(); + t.state = state; + t + } + + fn log_of(txs: Vec, active: Option<&str>) -> TransactionLog { + TransactionLog { + version: "1.0".to_string(), + transactions: txs, + active_transaction_id: active.map(str::to_string), + } + } + + /// T-12: a log read from disk must satisfy the invariant `Good` that the + /// Agda lifecycle theorems (T-2, T-3) preserve; each way of breaking it is + /// refused as corrupted rather than loaded. + #[test] + fn a_loaded_log_that_breaks_the_invariant_is_refused() { + use TransactionState::{Active, Committed, RolledBack}; + let cases = [ + ( + "pointer to a missing transaction", + log_of(vec![tx_in(Committed, "a")], Some("b")), + ), + ( + "pointer to a settled transaction", + log_of(vec![tx_in(Committed, "a")], Some("a")), + ), + ( + "Active with no pointer", + log_of(vec![tx_in(Active, "a")], None), + ), + ( + "two Active transactions", + log_of(vec![tx_in(Active, "a"), tx_in(Active, "b")], Some("a")), + ), + ( + "pointer id whose first transaction is settled", + log_of(vec![tx_in(RolledBack, "a"), tx_in(Active, "a")], Some("a")), + ), + ]; + for (what, log) in cases { + match load(&log) { + Err(ReversibleError::MetadataCorrupted(_)) => {} + Err(e) => panic!("{what}: refused with the wrong error: {e}"), + Ok(_) => panic!("{what}: a log that breaks the invariant was loaded"), + } + } + } + + /// T-12, the positive control: logs the manager writes satisfy the + /// invariant, idle and busy, and load back unchanged. + #[test] + fn a_log_the_manager_wrote_loads_back() { + let tmp = TempDir::new().expect("temp dir"); + let path = tmp.path().join("transactions.json"); + let mut manager = TransactionManager::new(path.clone()).expect("new"); + manager.begin(None).expect("begin"); + manager.add_operation("op-1".to_string()).expect("add"); + manager.commit().expect("commit"); + manager.begin(None).expect("begin again"); + manager.mark_rolled_back().expect("roll back"); + let idle = TransactionManager::new(path.clone()).expect("an idle log loads"); + assert_eq!(idle.all().len(), 2); + assert!(!idle.has_active()); + + manager.begin(None).expect("begin a third"); + let busy = TransactionManager::new(path).expect("a busy log loads"); + assert_eq!(busy.active_id(), manager.active_id()); + } } diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 92a2445..a2cea73 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -259,12 +259,14 @@ exists: the table in §The PWG-3 receipt cites run 42076969251, which ran the canonical invocation on all three modules, and the receipts from before the flag changed are marked `superseded` there. -One related inconsistency is an open obligation, not a claim: the Agda version -is pinned twice in CI and the two pins differ — `agda-proofs.yml` installs -2.6.4.3 (the receipt above), while `dashboard-check.yml` installs 2.6.3 on the -Idris2 image so it can run the PROVEN rows' checkers. A green dashboard -therefore does not extend the receipt at 2.6.4.3. One version, one receipt: -pinning the dashboard job to the same Agda is the fix. +Until 2026-11-09 the Agda version was pinned twice in CI: `agda-proofs.yml` +installed 2.6.4.3 (the receipt above), while `dashboard-check.yml` installed +Ubuntu's 2.6.3 on the Idris2 image so it could run the PROVEN rows' checkers. +Resolved by owner decision on 2026-11-09. The dashboard job now runs Agda from +the image `agda-proofs.yml` pins: the same `debian:trixie-slim` digest and +`agda-bin=2.6.4.3-1+b2`. It runs Idris2 from the image `idris-abi.yml` pins, +and asserts the version string exactly as the proof job does. One version, one +receipt. === Upgrade path, measured @@ -310,7 +312,12 @@ repeated the counts, and the two copies drifted apart. | E-1m | In a world model, an agent whose observation excludes the store does not know what the store holds; obliteration leaves nothing to recover; rotation to a different key (premise `old ≠ new`) leaves no agent — the system included - — able to use the old one (true by the definition of `rotate` in the model) | + — able to use the old one (true by the definition of `rotate` in the model). + `adversary-ignorant` and `obliterate-ignorance` are proved for two particular + worlds whose stores differ and whose adversary observations are both empty; + the general form is `different-store-unknown`, which takes such a pair as its + hypothesis, so these show ignorance is expressible and true in the model, not + that the adversary is ignorant in every januskey state | `Epistemic.agda::adversary-ignorant`, `obliterate-cuts-recovery`, `obliterate-ignorance`, `rotate-forgets-old` |===