diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index dfe9cd1..21d815c 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,7 +6,7 @@ [metadata] project = "januskey" version = "1.0.0" -last-updated = "2026-06-12" +last-updated = "2026-11-01" status = "active" crg-grade = "D" @@ -19,6 +19,12 @@ phase = "Core tests complete; 2026-04..06 wave was CI/governance/license hardeni session-date = "2026-06-12" work = "Estate standardization merged (flat contractiles, bot_directives, 6a2/anchor, self-validating, GOVERNANCE/MAINTAINERS/CODEOWNERS, flake.nix removed); CodeQL cron weekly→monthly cherry-picked; governance checkpoint layer (STATE refresh, bot_directives trio, Dust/Bust flat port, k9 template set)" +[recent-work.since-2026-11-01] +identity = "ADR-0001 (docs/adr/0001-identity-and-scope.md): identity resolved from code. The product is `jk`; measured coupling between the reversibility path and the key subsystem is zero in both directions, and the audit chain is library-only (main.rs never builds an AuditLog). Applied: `key-lifecycle` feature gates the jk-keys binary out of the default build; identity statements corrected in README, PROOF-NEEDS, ARCHITECTURE, januskey-cli/src/lib.rs, KEY_LIFECYCLE; V-1..V-3 ledger rows pin downstream consumption (valence-shell, ochrance, aletheia) as DESIGNED, since no repository outside this workspace depends on reversible-core. Not applied: the module move into crates/januskey-keys, which needs a toolchain this session does not have (no rustc, no crates.io) — steps and acceptance criteria in ADR-0001 §5." +human-action = "Two files contradict ADR-0001 and are agent-denied by the Trustfile (@trust-deny: modify-trustfile, modify-threat-model): contractiles/Trustfile.a2ml line 8 calls januskey \"a key-management tool\"; threat-model.a2ml [primitives.mac] still describes the removed home-rolled HMAC. Both need an owner edit." + +claim-surfaces = "Estate consistency audit (docs/estate/2026-11-01-handoff-and-consistency-audit.md) found the structural model intact and the drift in this repo's own published surfaces. Corrected for over-claim only: wiki theory pages (rmo, rmr, mpr, maa-framework, formal-model, index) restated at the strength of the claims ledger; security/THREAT_MODEL.adoc compliance mapping rewritten and its '256-bit ECC' and BLAKE3 rows removed (neither is in the tree); CLI about/long_about and the Obliterate help no longer claim provable reversibility or a GDPR determination; crate descriptions and module headers aligned; TOPOLOGY diagram label de-claimed. No ledger row changed status and no test or proof count changed." + [recent-work.since-2026-04-04] ci-standardization = "Reusable-workflow wrappers: rust-ci (#39), hypatia-scan (#40, canonical sync #31/#32, workdir fix #29, repin #46), mirror (#42), secret-scanner (#43), scorecard (#44, job-level perms #48); cargo-audit + workflow-linter prevention workflows; concurrency-cancel guards (#34/#35); SHA repins (#27/#28/#33/#50); Dependabot security path + auto-merge restored; actions bumps (#36/#47/#53)" license = "PMPL-1.0-or-later → MPL-2.0 migration (a740439); Cargo.toml license aligned to LICENSE (#52)" @@ -28,15 +34,30 @@ docs = "CHANGELOG.md seeded, Keep-a-Changelog (#45); tech-debt audit recorded (# structure = "contractiles: bust/ added + k9 → svc/ per ADR-001 2026-04-18 (4094646, 9f05e98); 6SCM → 6A2 metadata migration" [test-coverage] -# As assessed in READINESS.md (2026-04-03); no test-suite changes landed since. -unit-tests = "36" -p2p-property-tests = "8" +# Reconciled 2026-11-01. The per-category counts are the 2026-04-03 assessment and +# have NOT been re-derived; the two aggregates below are the figures READINESS.adoc +# declares and dashboard-check measures. Quote the aggregates, not the categories. +unit-tests = "36 (2026-04-03 assessment, not re-derived)" +p2p-property-tests = "8 (2026-04-03 assessment, not re-derived)" e2e-integration-tests = "1 script (mostly skips without pre-built binary)" -property-tests = "9" -regression-tests = "5" -idris2-proofs = "30" -benchmarks = "5 Criterion groups" -total = "67 tests + 5 benchmark groups + 30 Idris2 proofs (READINESS.md matrix)" +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 = "136 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check" + +[proof-grades] +# mathesis (estate-mathematical-architecture §5/§6) + standards +# 3-practice/PROOF-POLICY.adoc. A grade is a second axis over the PROVEN/TESTED +# ledger vocabulary, never a percentage. Detail: docs/theory/PROOF-GRADES.adoc. +grade-3 = "G-1, T-1, T-2, T-3 — Agda theory modules under verification/proofs/agda; AGDA-VERIFIED" +grade-3-pending = "E-1m — Epistemic.agda; no receipt yet, because the receipt-commit predates this module" +receipt-commit = "4afb710e86646658f667f10bd6274ee47416bfc7 (agda-proofs.yml run 40867211509, success)" +receipt-prover = "Agda 2.6.4.3 (agda-bin=2.6.4.3-1+b2); resource-algebra pinned at cf9235c" +receipt-flags = "--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check (canonical per PROOF-POLICY §2.1 since 2026-11-01; the 4afb710 CI receipt predates the flag, so the next agda-proofs.yml run is its receipt)" +not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §1); all 23 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows" +open-obligations = "re-earn the Agda receipt in CI under the canonical flag set; one Agda version across CI (agda-proofs pins 2.6.4.3, dashboard-check installs 2.6.3); no Creusot contract on the Rust, and neither rustc nor crates.io is reachable from the agent sandbox (docs/estate/environment-toolchains.md), so no Rust behaviour is graded" +claimed-higher = "none — no Grade 2i, 2ii or 1 is claimed" [test-categories-complete] unit = true diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 1f210f8..199996a 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -23,7 +23,11 @@ These 6 SCM files MUST exist in `.machine_readable/` directory ONLY: **CRITICAL:** If ANY of these files exist in the root directory, this is an ERROR. -### Bot Directives: `.bot_directives/` ONLY +Bot directives live under `.machine_readable/bot_directives/`, not in a root +`.bot_directives/` (corrected 2026-11-01; the path had been stale since the estate +standardization merge). + +### Bot Directives: `.machine_readable/bot_directives/` ONLY Bot-specific instructions for: - rhodibot - Git operations @@ -55,7 +59,7 @@ This repo contains: ``` januskey/ ├── 0-AI-MANIFEST.a2ml # THIS FILE (start here) -├── README.md # Project overview +├── README.adoc # Project overview ├── [your source files] # Main code ├── .machine_readable/ # SCM files (6 files) │ ├── .machine_readable/6a2/STATE.a2ml @@ -64,13 +68,13 @@ januskey/ │ ├── .machine_readable/6a2/AGENTIC.a2ml │ ├── .machine_readable/6a2/NEUROSYM.a2ml │ └── .machine_readable/6a2/PLAYBOOK.a2ml -└── .bot_directives/ # Bot instructions +└── .machine_readable/bot_directives/ # Bot instructions ``` ## SESSION STARTUP CHECKLIST ✅ Read THIS file (0-AI-MANIFEST.a2ml) first -✅ Understand canonical locations (.machine_readable/, .bot_directives/) +✅ Understand canonical locations (.machine_readable/, .machine_readable/bot_directives/) ✅ Know the invariants (no SCM duplication, etc.) ✅ Check for MCP enforcement (if applicable) ✅ Read `.machine_readable/6a2/STATE.a2ml` for current status @@ -105,7 +109,7 @@ When ending a session: After reading this file, demonstrate understanding by stating: -**"I have read the AI manifest. SCM files are located in `.machine_readable/` ONLY, bot directives in `.bot_directives/`, and I will not create duplicate files in the root directory."** +**"I have read the AI manifest. SCM files are located in `.machine_readable/` ONLY, bot directives in `.machine_readable/bot_directives/`, and I will not create duplicate files in the root directory."** ## META diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc index 693ac8d..38c59a9 100644 --- a/ARCHITECTURE.adoc +++ b/ARCHITECTURE.adoc @@ -14,9 +14,11 @@ maa-framework (policy vision) JanusKey is the *junction point* where absolute-zero’s theoretical work on Certified Null Operations (CNOs) was first applied to practical file -operations. The three downstream applications independently implemented -reversibility, but shared no code — until the `+reversible-core+` -extraction described below. +operations. The three downstream applications each implemented reversibility +and shared no code. `+reversible-core+` was extracted (Phase 1, 2026-03-21) so +that they *could* share it — **none of them does yet**, and nothing below should +be read as consumption until a dependency edge and a green test exist in the +consuming repository (ADR-0001 §4). === Workspace Structure @@ -32,19 +34,25 @@ januskey/ │ │ └── lib — ReversibleExecutor trait │ │ │ └── januskey-cli/ ← CLI TOOL (depends on reversible-core) -│ ├── operations — FileOperation executor (actual filesystem ops) -│ ├── keys — Key management (AES-GCM, Argon2) -│ ├── attestation — Audit trail -│ ├── obliteration — Secure deletion -│ ├── delta — Differential operations -│ ├── main — jk CLI binary -│ └── keys_cli — jk-keys CLI binary +│ ├── operations — FileOperation executor (actual filesystem ops) ON THE jk PATH +│ ├── obliteration — Secure deletion (the deliberate exception) ON THE jk PATH +│ ├── delta — Differential operations ON THE jk PATH +│ ├── main — jk CLI binary ON THE jk PATH +│ ├── attestation — HMAC-SHA256 audit chain library-only: jk never builds one +│ ├── keys — key store (Argon2id, AES-256-GCM wrap, rotate, +│ │ revoke, backup) OFF-PATH: no call edge to jk; see ADR-0001 +│ └── keys_cli — jk-keys binary OFF-PATH: behind feature `key-lifecycle` .... +`link:docs/adr/0001-identity-and-scope.md[ADR-0001]` records the identity +decision: the product is `jk`; the key lifecycle manager is not part of it and +awaits extraction; the audit chain is library-only and not wired into the CLI. + === reversible-core: The Shared Foundation `+reversible-core+` is a lean Rust library crate (no CLI deps) that -provides the types all three downstream applications share: +provides the types the three downstream applications are *intended* to share. +None consumes the crate today (see Consumption status below): ==== ReversibleExecutor Trait @@ -87,10 +95,13 @@ Per absolute-zero, every `+OperationType+` has a known inverse: Manifest header (version, subsystem, timestamp, Merkle root) - Refs (one per operation, with content hash) - Policy (verification mode) -Ochrance parses these and produces `+VerificationProof+` witnesses: - -`+LaxProof+` — manifest is well-formed - `+CheckedProof+` — all content -hashes verified via BLAKE3 - `+AttestedProof+` — manifest is signed -(Ed25519) +Ochrance is *designed* to parse these and produce `+VerificationProof+` +witnesses: - `+LaxProof+` — manifest is well-formed - `+CheckedProof+` — all +content hashes verified (BLAKE3 on its side; this side hashes SHA-256, and the +mismatch is unresolved) - `+AttestedProof+` — manifest is signed (Ed25519) + +It has never parsed one. Treat this paragraph as a specification of an intended +boundary, not as an integration. === Integration Status @@ -100,7 +111,7 @@ Extracted core types from januskey into `+reversible-core+`. Workspace builds, 44 tests pass. januskey-cli re-exports all types for backward compatibility. -==== Phase 2: valence-shell integration — NEXT +==== Phase 2: valence-shell integration — NOT STARTED (no consumer exists) Wire valence-shell (`+impl/rust-cli/+`) to depend on `+reversible-core+`: - Add `+ContentStore+` to `+ShellState+` for @@ -109,7 +120,7 @@ content-addressed undo data - Replace inline `+a2ml_emitter.rs+` for manifest generation - Replace `+verification.rs+` stubs with `+ReversibleExecutor+` implementation -==== Phase 3: ochrance ABI extension — PENDING +==== Phase 3: ochrance ABI extension — NOT STARTED (no consumer exists) Add reversibility types to ochrance’s Idris2 ABI: - `+src/abi/Ochrance/ABI/Reversibility.idr+` — `+ReversibleOp+`, @@ -122,6 +133,32 @@ Add reversibility types to ochrance’s Idris2 ABI: - Update ARCHITECTURE.md and ECOSYSTEM.a2ml in all three repos with cross-references. +==== Consumption status (2026-11-01) + +What is *claimed* here is deliberately narrow, because the estate's recurring +defect is a plan becoming a fact in prose. + +[cols="2,2,4",options="header"] +|=== +| Claim | Status | Evidence required to change it + +| valence-shell depends on `reversible-core` +| NOT TRUE — no consumer outside this workspace +| A dependency edge in valence-shell's manifest, plus a test there that drives `ReversibleExecutor` + +| ochrance verifies januskey manifests +| NOT TRUE — `ManifestEmitter` has never been parsed by it +| An ochrance-side parse of a generated manifest, and a decision on the hash algorithm (SHA-256 here; BLAKE3 believed to be used there) + +| aletheia uses `reversible-core` +| NOT TRUE — explicitly deferred (Phase 0 research) +| same as valence-shell +|=== + +These three are also ledger rows `V-1`, `V-2` and `V-3` in `PROOF-NEEDS.adoc`, +so their status is machine-checked against the dashboards rather than maintained +by memory. + ==== Deferred * *aletheia*: Too early (Phase 0 research, no operation types yet) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 5e33ac5..d2b3b84 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -17,6 +17,10 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Added +* 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 +(PROVEN, Grade 3), E-1 stays OPEN * feat(crg): add crg-grade and crg-badge justfile recipes * feat(crg): add Current Grade badge anchor to READINESS.md * feat: add idrisiser Idris2 proof wrappers for JanusKey cryptographic @@ -32,6 +36,12 @@ benchmarks, READINESS.md ==== Fixed +* fix(reversible-core): the operation metadata log saves through the shared +atomic writer (`write_atomic`), with `save_replaces_the_log_atomically`; ledger +row T-8 stays OPEN until the unbuilt test runs +* fix(proofs): the Agda gate runs PROOF-POLICY §2.1's canonical invocation +(`--safe --without-K --cubical-compatible`); measured green locally with Agda +2.6.4.3 before the change, replacing an unverified prediction that it would fail * fix(ci): bump a2ml/k9-validate-action pins to canonical (#33) * fix(ci): sync hypatia-scan.yml to canonical (#32) * fix(ci): adopt canonical hypatia-scan.yml (#31) @@ -54,6 +64,10 @@ placeholder ==== Documentation +* docs(theory): proof grades under mathesis and PROOF-POLICY — four Agda rows +are Grade 3 with a receipt at 4afb710; one recorded divergence from the +canonical Agda invocation (`docs/theory/PROOF-GRADES.adoc`) + * docs(security): draft MCP-exposure threat model (AI-authored, pending human sign-off) * docs: add M2 estate audit report (2026-04-04) @@ -66,6 +80,10 @@ human sign-off) ==== CI +* ci(proofs): record what the agent sandbox can and cannot install (Agda and Zig +from PyPI wheels; Rust, Creusot and Idris2 blocked by egress), +`docs/estate/environment-toolchains.md` + * ci(rust): convert rust-ci.yml to thin wrapper (standards#174) (#39) * ci: redistribute concurrency-cancel guard to read-only check workflows (#35) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 86bb1c2..901f60a 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -8,21 +8,54 @@ The README makes claims. This file backs them up. == Claims Substantiation -=== Claim 1: "100% Reversible - Every operation can be undone, always" - -**How it works:** JanusKey implements architectural reversibility by storing inverted operations alongside each mutation. The delete operation, implemented in `crates/januskey-cli/src/obliteration.rs`, calculates and stores a full restoration record before removing file content. The `delta.rs` module generates inverse metadata that sufficient to reconstruct the pre-operation state. Every operation in the transaction layer (`crates/januskey-cli/src/metadata.rs`) maintains a "prior state" record, enabling perfect reversal through the `undo` pathway. - -**Caveat:** Reversibility is strong only when the operation log remains intact. If `.jk/` metadata store is corrupted or lost, recovery becomes impossible. The system trades **write amplification** (each operation doubles metadata I/O) for guaranteed recoverability. - -**Evidence:** `crates/januskey-cli/src/lib.rs` (public API) delegates to `obliteration.rs` and `delta.rs` for operation logic; see `Reversible` trait (if present) or reversibility-proof comments in `attestation.rs`. - -=== Claim 2: "Complete Audit Trail - Every change tracked automatically" - -**How it works:** The metadata store (`crates/januskey-cli/src/metadata.rs`) maintains an append-only operation log. The `attestation.rs` module calculates cryptographic commitments (SHA256 hashes) of each operation, creating a tamper-evident chain. Content-addressed storage (`crates/januskey-cli/src/content_store.rs`) ensures deduplication by content hash, preventing duplicate storage while maintaining full history. - -**Caveat:** The audit trail is only as trustworthy as the append-only mechanism. If the log is truncated or rewritten on-disk, the chain breaks. For forensic-grade auditing, integrate with an external append-only store (database, blockchain). - -**Evidence:** `crates/januskey-cli/src/metadata.rs` defines the log structure; `attestation.rs` computes cryptographic bindings; `content_store.rs` handles SHA256 hashing. +=== Claim 1: "Operations carry their own inverse — undo without a backup" + +**How it works:** each operation captures what its inverse needs *before* it +mutates anything, and records it in an append-only log. Delete stores the content +in the content store and the file metadata in the log; modify stores the original +hash (plus a delta or full copy in `delta.rs`); move stores the source path; +copy stores the destination. Undo is then a lookup in the log followed by the +operation-specific inverse — no filesystem scan, no tape restore. + +**Caveat (the honest one):** this is an engineering mechanism, not a proved +theorem. The ledger row "every operation is reversible, as a theorem linked to +the Rust" is **OPEN**; the Agda proof covers a transaction *model* (T-1..T-3) +whose step-level premise is tested, not proved (T-6), and the operation metadata +log now saves by rename but that change is unbuilt (T-8, OPEN). Reversibility also fails +outright if the store is lost, and `jk obliterate` and `jk gc` are deliberate +exceptions that destroy what undo would need. What has been restored, and what +has not, is tabulated in `docs/wiki/theory/rmr-primitive.md` §2. + +**Evidence:** `crates/januskey-cli/src/operations.rs` (the executors — +`execute_delete`, `execute_modify`, …), `crates/januskey-cli/src/delta.rs` +(inverse members), `crates/reversible-core/src/metadata.rs` (the log), +`crates/reversible-core/src/content_store.rs` (SHA-256 content addressing), +`crates/reversible-core/src/lib.rs` (`ReversibleExecutor`), +`crates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity`. + +=== Claim 2: "Audit trail — every tracked change is recorded and chained" + +**How it works:** the operation log (`crates/reversible-core/src/metadata.rs`) is +append-only: new operations are appended, existing entries are not edited in +place. `attestation.rs` chains entries with a real HMAC-SHA256 +(`hmac` crate, RFC 2104): the MAC covers the entry data and the previous entry's +hash, with a scheme label bound in as a domain separator, keyed on a +store-derived key. It **refuses** to write an entry when no key is set rather +than falling back to an unkeyed hash (the former +`SHA256(key‖data‖prev)` construction was not a MAC and has been removed). Content is addressed by SHA-256, so +duplicate content is stored once. + +**Caveat:** "every change" is too strong in both directions. `jk obliterate` +purges the log entries for a path on purpose, `jk gc` prunes old entries, and the +obliteration ledger (`obliterations.json`) is **unkeyed** — its records are not in +the HMAC chain yet (deferred, J2-3). The chain detects edits to entries it covers; +it does not make the file immutable, and an attacker with write access can delete +the whole log. + +**Evidence:** `crates/reversible-core/src/metadata.rs` (log structure and +`save` — see the T-8 caveat), `crates/januskey-cli/src/attestation.rs` (HMAC +chain, `AuditLog`), `crates/reversible-core/src/content_store.rs` (hashing and +dedup). == Technology Choices @@ -37,19 +70,29 @@ The README makes claims. This file backs them up. == File Map +The receipt, file by file. Paths are the ones that exist today: the content +store, metadata log and transaction layer live in `reversible-core`, not in the +CLI crate (they were extracted in Phase 1, 2026-03-21). + [cols="1,3"] |=== | Path | Purpose -| `crates/januskey-cli/src/main.rs` | CLI entry point, command dispatch (delete, modify, move, copy, undo, begin, commit, rollback, preview) -| `crates/januskey-cli/src/lib.rs` | Public API: init, delete, modify, move, copy, undo, transaction logic -| `crates/januskey-cli/src/obliteration.rs` | Delete operation with restoration metadata -| `crates/januskey-cli/src/delta.rs` | Computes inverse operations (modify undo, move undo, copy undo) -| `crates/januskey-cli/src/metadata.rs` | Append-only operation log, transaction tracking, rollback state -| `crates/januskey-cli/src/content_store.rs` | SHA256 content hashing, deduplication, storage management -| `crates/januskey-cli/src/attestation.rs` | Cryptographic commitments, audit trail, tamper detection -| `crates/januskey-cli/src/keys.rs` | Cryptographic key management (if key-based reversibility) -| `crates/januskey-cli/src/error.rs` | Error types and propagation +| `crates/januskey-cli/src/main.rs` | CLI entry point; command dispatch (`init, delete, modify, move, copy, rename, obliterate, undo, begin, commit, rollback, preview, history, status, gc`) +| `crates/januskey-cli/src/lib.rs` | Public API: `init`, the file operations, undo, transaction wiring +| `crates/januskey-cli/src/operations.rs` | `OperationExecutor`: the actual filesystem operations and their metadata capture +| `crates/januskey-cli/src/delta.rs` | Line/block deltas and the inverse content for modify +| `crates/januskey-cli/src/obliteration.rs` | `jk obliterate`: secure overwrite, store scrub, obliteration records +| `crates/januskey-cli/src/attestation.rs` | HMAC-SHA256 audit chain over operations +| `crates/januskey-cli/src/keys.rs`, `keys_cli.rs` | AES-256-GCM key store (Argon2id), key lifecycle; the `jk-keys` binary +| `crates/reversible-core/src/content_store.rs` | SHA-256 content-addressed storage, deduplication +| `crates/reversible-core/src/metadata.rs` | Append-only operation log (`MetadataStore`); it now calls the shared atomic writer, unbuilt — ledger row T-8 +| `crates/reversible-core/src/transaction.rs` | Transaction lifecycle and the atomic write→fsync→rename log save +| `crates/reversible-core/src/manifest.rs` | A2ML manifest emitter (the intended ochrance boundary) +| `crates/reversible-core/src/lib.rs` | `ReversibleExecutor` trait — `execute`, `undo`, `generate_manifest` +| `src/abi/JanusKey/ABI/*.idr` | Idris2 ABI layer (types, layout, FFI codes, proved lemmas) +| `verification/proofs/agda/*.agda` | Agda kernel: reversibility as a `Loss` grade; transaction atomicity +| `crates/dashboard-check` | Runs every PROVEN/TESTED ledger row and reconciles the dashboards against `STATE.a2ml` |=== == Dogfooted Across The Account @@ -62,4 +105,9 @@ The README makes claims. This file backs them up. == Readiness -**CRG Grade:** C (Beta) - Reversibility architecture sound, append-only log working, needs edge-case testing around symlinks and special files. +**CRG Grade: D — Alpha, Unstable.** The machine-readable status is +`.machine_readable/6a2/STATE.a2ml` (completion 60%, grade D) and `READINESS.adoc` +(Grade D, promotion path to C recorded there). `just check-dashboard` fails the +build if this file, TOPOLOGY or READINESS print a grade or count that disagrees +with STATE or with the claims ledger, so this line is checked rather than +maintained by hand. diff --git a/GLOSSARY.adoc b/GLOSSARY.adoc index aa1d7a3..9e9cc20 100644 --- a/GLOSSARY.adoc +++ b/GLOSSARY.adoc @@ -44,7 +44,7 @@ Transaction manager:: == Exceptions [[secure-obliteration]] -Secure obliteration (`jk shred`):: +Secure obliteration (`jk obliterate`):: The deliberate exception to reversibility. Attempts overwrite-in-place to destroy file contents. Best-effort only: cannot guarantee physical erasure on SSD (wear leveling), CoW (ZFS, Btrfs), or journaling filesystems. Physical destruction is the only guaranteed obliteration on modern media. *Classification:* **project-specific** (operation). diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index ad0738e..32ae62f 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -65,7 +65,7 @@ tables must agree. | G-1 | Reversibility as a Loss grade: lossless traces have only lossless steps; obliteration absorbs; wrap/unwrap is grade 𝟙 given cancellation | PROVEN | `+verification/proofs/agda/Reversibility.agda+` (Agda kernel, resource-algebra pinned at `+cf9235c+`); `+tests/reject-agda/*+` refused; the cancellation premise is the TESTED row `+execute_then_undo_is_identity+` | G-2 | The Idris2 `+IsCNO+`/`+ReversibleOp+` pair corresponds to Agda `+ReversiblePair+` (by transcription) | ASSUMED | no mechanical link claimed | G-3 | The FFI bridge preserves grade 𝟙 (homomorphism) | OPEN | resource-algebra lists homomorphisms OPEN; to file from JNK-01 -| E-1 | An attacker cannot recover obliterated content or use a revoked key | OPEN | `+Types.adversaryCannotKnow+` holds only because `+Knows+` has no Adversary constructor (#145 item 3) +| E-1 | An attacker cannot recover obliterated content or use a revoked key | OPEN | `+Types.adversaryCannotKnow+` holds only because `+Knows+` has no Adversary constructor; the *model-level* half is now proved in Agda as row E-1m (#145 item 3) | X-1 | Hash one-wayness; physical erasure (cryptographic and physical assumptions, external to this repository) | ASSUMED | not theorems of this repo | T-1 | Undoing a fully executed transaction's operations in reverse order restores the state it began in, given each step's undo restores its execute (the sequential Theorem 3.4) | PROVEN | `+TransactionAtomicity.rollback-restores+`; `+tests/reject-agda/ForwardRollback.agda+` refused | T-2 | begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction, so a completed one is never modified | PROVEN | `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused @@ -74,7 +74,10 @@ tables must agree. | T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (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-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: `+MetadataStore::save+` is the same plain `+fs::write+`; `+undo+` runs the undo, then `+mark_undone+` persists, so a failed persist leaves the file undone but the log not +| 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 +| 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 |=== Removed, with the reason recorded beside the replacement in source: @@ -102,6 +105,43 @@ IO do-notation at all. The dashboards (README, TOPOLOGY, READINESS) carry the proof count that `+dashboard-check+` measures from the PROVEN rows of the ledger below. +=== Proof grades under mathesis (2026-11-01) + +The five statuses above are this repository's claim vocabulary — the estate's +README-EXPLAINME ledger, as used across it. A *proof grade* is a second, +orthogonal axis, governed by `+hyperpolymath/mathesis+` +(`+estate-mathematical-architecture+` §5 and §6) and by +`+hyperpolymath/standards+` `+3-practice/PROOF-POLICY.adoc+`. Neither uses a +confidence percentage and this repository does not publish one. + +Of the 12 PROVEN rows, five are the theory rows — **G-1, T-1, T-2, T-3, E-1m** — and +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: +`+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 +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. + +No row of this ledger is Grade 2i, Grade 2ii or Grade 1, and none is claimed to +be. The row-by-row mapping and the receipt in full are in +`+docs/theory/PROOF-GRADES.adoc+`. Since 2026-11-01 the gate runs +PROOF-POLICY §2.1's canonical invocation +(`+--safe --without-K --cubical-compatible …+`), which was verified locally +with Agda 2.6.4.3 before being committed; the CI receipt for that flag set is +the next `+agda-proofs.yml+` run, not the older one. + === Current State _Re-verified 2026-06-29 (idris2 0.8.0); paths updated 2026-10-12 to the @@ -114,9 +154,11 @@ NOT the security proofs listed below. * **generated/idrisiser/**: removed 2026-10-14 (owner decision). It never typechecked (lowercase generated module names), so nothing in it was verified; no ledger row depended on it. -* *Dangerous patterns*: *265* `+unwrap()+` calls across the Rust -codebase. -* *LOC*: ~12,200 (Rust) +* *Dangerous patterns*: *241* `+unwrap()+` calls across the Rust codebase + (measured 2026-11-01; the previous 265 and 225 figures in this file and + READINESS agreed with neither the code nor each other). +* *LOC*: 11,160 Rust lines in the tree (8,495 in `crates/*/src`; measured 2026-11-01). + The previous figure, ~12,200, was not reproducible. * *ABI layer*: present (`+src/abi/JanusKey/ABI/{Types,Foreign,Layout,Proofs}.idr+`, package `+src/abi/januskey-abi.ipkg+`) but carries no load-bearing security proof yet — the real obligations below are still open. @@ -130,7 +172,8 @@ below are still open. |Core feature: must guarantee data is unrecoverable |Key derivation |Key generation produces cryptographically sound keys -|Weak keys break entire security model +|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 attestations undermine trust @@ -138,7 +181,7 @@ attestations undermine trust |Content store integrity |Content-addressed storage never returns wrong content |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 and the metadata log, T-8, is open) +|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 |reversible-core |Undo/redo preserves data integrity |Core crate used by @@ -204,11 +247,15 @@ the status table above. |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` |- -|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+` is a plain `+fs::write+`) |OPEN |`crates/reversible-core/src/metadata.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` |- |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` |- +|V-1: valence-shell depends on reversible-core for reversible operation data (ARCHITECTURE Phase 2) |DESIGNED |`ARCHITECTURE.adoc` |- +|V-2: ochrance verifies januskey A2ML manifests (ARCHITECTURE Phase 3) |DESIGNED |`crates/reversible-core/src/manifest.rs` |- +|V-3: aletheia consumes reversible-core (ARCHITECTURE, deferred) |DESIGNED |`ARCHITECTURE.adoc` |- |=== === Recommended Prover @@ -219,12 +266,19 @@ ABI/runtime layer (ruling 2026-10-12): kernel statements live in (`+scripts/fetch-siblings.sh+`); the ABI lives in `+src/abi/+`. Transaction atomicity is stated there for the model (`+verification/proofs/agda/TransactionAtomicity.agda+`, rows T-1 to T-3; the Rust fixes behind T-4 and T-5 are tested, not proved); -obliteration completeness and attestation chain integrity are still to be stated. The 225 `+unwrap()+` calls should +obliteration completeness and attestation chain integrity are still to be stated. The 241 `+unwrap()+` calls should be systematically replaced with proven error handling. === Priority -*HIGH* — JanusKey handles cryptographic key management, attestation -chains, and data obliteration. Any correctness bug in obliteration or -key derivation is a critical security vulnerability. The ABI layer now -typechecks, but none of the security obligations above is proved. +*HIGH* — reversibility is the product, and its exceptions are destructive: +obliteration destroys data on purpose, and the operation log is the only thing +that makes undo possible (row T-8 is open). Any correctness bug in either is a +critical vulnerability. The ABI layer now typechecks, but none of the security +obligations above is proved. + +The workspace also contains a key store with lifecycle management +(`+keys.rs+`, `+jk-keys+`). It is **not on the `jk` path**, has no call edge to or +from it, protects no file content, and is not part of this repository's identity; +its obligations are tracked here only while the module remains in this tree. See +`link:docs/adr/0001-identity-and-scope.md[ADR-0001]`. diff --git a/READINESS.adoc b/READINESS.adoc index a4cd32d..d8561e8 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -8,10 +8,10 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0 === CRG Grade: D (Alpha — Unstable) -*Justification:* 135 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the -Idris2 ABI typechecks and 11 proofs are checked (PROVEN ledger rows: ABI, grade and transaction-model lemmas, not the +*Justification:* 136 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, 225 unwrap() calls, E2E mostly skips, +fuzz testing, no mutation testing, 241 unwrap() calls, E2E mostly skips, benchmarks measured fake crypto until this session. RSR compliance present. Deep annotation incomplete (TOPOLOGY.md exists but per-directory orientation missing → blocks C). @@ -61,11 +61,11 @@ handling |15 |Compatibility |MISSING |0 |— |No version migration tests -|16 |Proof regression |✓ |11 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections +|16 |Proof regression |✓ |12 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections (run by idris-abi.yml, agda-proofs.yml and dashboard-check) |=== -*Total declared:* 135 tests + 5 benchmark groups; 11 proofs checked (PROVEN ledger rows) *Total +*Total declared:* 136 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five of them Grade 3 under mathesis — see `docs/theory/PROOF-GRADES.adoc`) *Total missing:* Fuzz, mutation, chaos, compatibility === Aspect Matrix @@ -127,7 +127,7 @@ recording. === Known Debt -* 225 unwrap() calls (tracked in PROOF-NEEDS.md) +* 241 unwrap() calls (tracked in PROOF-NEEDS.adoc; measured 2026-11-01) * E2E test needs pre-built binary to exercise full lifecycle * idris-abi.yml and agda-proofs.yml run on every PR but are not yet required checks * No code coverage measurement diff --git a/README.adoc b/README.adoc index d6feac8..044daa8 100644 --- a/README.adoc +++ b/README.adoc @@ -20,6 +20,31 @@ Every `jk delete`, `jk modify`, or `jk move` stores the inverse operation in an **Formal proofs of complete reversibility are pending.** The engineering mechanism (inversion metadata) is implemented in Rust. The mathematical guarantee that this construction makes data loss impossible under all allowed operations has not yet been mechanically verified. See link:EXPLAINME.adoc#_reversibility_guarantee[EXPLAINME §Reversibility guarantee]. ==== +== What this repository is, and what else it contains + +The product is `jk`: reversible file operations whose inversion metadata lives in +an append-only, content-addressed log. Its implementation is `main.rs` + `lib.rs` + +`operations.rs` + `delta.rs` + `obliteration.rs` over `reversible-core`. + +The workspace contains two further things that are **not** on that path. They are +listed here because the repository's name invites the wrong inference, and because +"what the code does" is the only boundary that survives review: + +* **A key store with lifecycle management** (`crates/januskey-cli/src/keys.rs`, + built as a second binary `jk-keys`). It is behind the opt-in `key-lifecycle` + feature, so a default build produces `jk` only. It has no call edge to or from the + reversibility path, and it protects no file content — the content store is + plaintext. Being feature-gated removes the *binary*; the module is still compiled + into the library and still pulls its crypto crates until it is moved out (ADR-0001 + §5). Key custody is not part of this project's identity and is scheduled to + move; see link:docs/adr/0001-identity-and-scope.md[ADR-0001]. +* **An HMAC-SHA256-chained audit log** (`attestation.rs`). Library-only today: the + `jk` binary never constructs an audit log, and the key it requires is supplied by + the caller, not derived from the key store. + +`reversible-core` is *intended* to be shared with ochrance, valence-shell and +aletheia. None of them depends on it yet; see ARCHITECTURE §Consumption status. + == What is standard and what is ours [cols="1,2,2", options="header"] @@ -76,10 +101,10 @@ Rollback is an lookup-then-execute operation against the append-only log, bounde == The secure obliteration exception -Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate, explicit exception. It is best-effort only: +Reversibility is the default. Secure obliteration (`jk obliterate`) is the deliberate, explicit exception. It is best-effort only: * Overwrite-in-place cannot guarantee physical erasure on SSDs (wear leveling), CoW filesystems (ZFS, Btrfs), or journaling filesystems. -* The threat model for `shred` assumes spinning-rust physical media. On modern media, physical destruction is the only guaranteed obliteration. +* The threat model for overwriting assumes rotating magnetic media. On modern media, physical destruction is the only guaranteed obliteration. == Commands @@ -99,6 +124,12 @@ Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate | `jk move ` | Move/rename files +| `jk rename ` +| Rename in place (reversible) + +| `jk obliterate ` +| Overwrite then remove (NOT reversible; best-effort) + | `jk copy ` | Copy files @@ -122,6 +153,9 @@ Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate | `jk status` | Show current status + +| `jk gc` +| Prune old operations |=== == Architecture @@ -147,7 +181,7 @@ Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate [CAUTION] ==== -**Secure obliteration is best-effort.** `jk shred` cannot guarantee physical erasure on SSD, CoW, or journaling filesystems. This is a physical constraint, not a software bug. +**Secure obliteration is best-effort.** `jk obliterate` cannot guarantee physical erasure on SSD, CoW, or journaling filesystems. This is a physical constraint, not a software bug. ==== [CAUTION] @@ -162,6 +196,9 @@ Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate # Build from source (requires Rust) cargo build --workspace --release +# Include the off-path key lifecycle binary as well +cargo build --workspace --release --features key-lifecycle + # Initialize jk init diff --git a/TESTING-REPORT.adoc b/TESTING-REPORT.adoc index a974b79..ecee66d 100644 --- a/TESTING-REPORT.adoc +++ b/TESTING-REPORT.adoc @@ -465,11 +465,16 @@ The following features exist in the codebase but lack dedicated tests: * Block-based diff computation * Delta application -2. **Obliteration Module** (`src/obliteration.rs`) +2. **Obliteration Module** (`crates/januskey-cli/src/obliteration.rs`) * Secure file overwrite - * GDPR Article 17 compliance proofs + * Obliteration records (commitment, pass count, `storage_cleared`) * Batch obliteration + (Overwrite and store-scrub behaviour is exercised by + `tests/obliteration_cas_test.rs`; what is untested is the record's + verification surface. There are no "compliance proofs" to test — see + `PROOF-NEEDS.adoc` row X-1.) + 3. **Garbage Collection** (`jk gc` command) * Cleanup of old operations * Content store pruning diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index 54828c0..52b61ba 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -1,5 +1,5 @@ == JanusKey — Project Topology -// Last updated: 2026-10-13 (proof count reconciled to the PROOF-NEEDS claims ledger by dashboard-check) +// Last updated: 2026-11-01 (diagram label de-claimed; proof/test counts unchanged — see the PROOF-NEEDS claims ledger) === System Architecture @@ -35,7 +35,7 @@ ▼ ┌─────────────────────────────────────────┐ │ TARGET FILESYSTEM │ - │ (Provably Reversible State) │ + │ (Reversible, proofs pending) │ └─────────────────────────────────────────┘ ┌─────────────────────────────────────────┐ @@ -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 - (Idris2 ABI typechecks; 11 proofs checked: ABI, grade and transaction-model + (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% 135 tests + 5 benches; missing fuzz, mutation, + Testing (READINESS matrix) ██████░░░░ ~60% 136 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D) REPO INFRASTRUCTURE diff --git a/crates/januskey-cli/Cargo.toml b/crates/januskey-cli/Cargo.toml index 49bbc2c..3c98b8f 100644 --- a/crates/januskey-cli/Cargo.toml +++ b/crates/januskey-cli/Cargo.toml @@ -4,7 +4,7 @@ [package] name = "januskey" version = "1.0.0" -description = "Provably reversible file operations through Maximal Principle Reduction" +description = "Reversible file operations with inversion metadata (formal proofs pending)" keywords = ["reversible", "filesystem", "transactions", "undo", "backup"] categories = ["command-line-utilities", "filesystem"] edition.workspace = true @@ -12,6 +12,13 @@ license.workspace = true repository.workspace = true authors.workspace = true +[features] +# The key store + lifecycle manager (`jk-keys`) is NOT part of this repo's +# identity: it has no call edge to or from the `jk` reversibility path. +# It is kept working behind a feature while it awaits extraction. +# See docs/adr/0001-identity-and-scope.md. +key-lifecycle = [] + [dependencies] reversible-core = { path = "../reversible-core" } clap = { version = "4", features = ["derive"] } @@ -62,3 +69,4 @@ path = "src/main.rs" [[bin]] name = "jk-keys" path = "src/keys_cli.rs" +required-features = ["key-lifecycle"] diff --git a/crates/januskey-cli/src/lib.rs b/crates/januskey-cli/src/lib.rs index f7d39c0..d1407d9 100644 --- a/crates/januskey-cli/src/lib.rs +++ b/crates/januskey-cli/src/lib.rs @@ -2,20 +2,29 @@ // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell // -// JanusKey CLI: Provably Reversible File Operations +// JanusKey CLI: reversible file operations with inversion metadata // Through Maximal Principle Reduction (MPR) // -// Core types are provided by reversible-core. This crate adds: -// - Filesystem operation execution (operations.rs) -// - Key management (keys.rs) -// - Audit trail (attestation.rs) -// - Secure deletion (obliteration.rs, delta.rs) -// - CLI interface (main.rs, keys_cli.rs) +// Identity: reversible file operations. The `jk` binary is the product. Its whole +// implementation is main.rs + lib.rs + operations.rs + delta.rs + obliteration.rs +// over reversible-core; nothing else is on that path. +// +// Also in this crate, but NOT on the `jk` path (docs/adr/0001-identity-and-scope.md): +// - keys.rs / keys_cli.rs — a key store with lifecycle management (Argon2id, +// AES-256-GCM key wrapping, rotate/revoke/backup), built as the separate +// `jk-keys` binary behind the `key-lifecycle` feature. There is no call edge in +// either direction between it and `jk`, and it protects no file content: the +// content store is plaintext. Candidate for extraction. +// - attestation.rs — an HMAC-SHA256-chained audit log. Library-only: `jk` never +// constructs an AuditLog, and the key it needs is an opaque `[u8; 32]` handed in +// by the caller, never derived from keys.rs. #![forbid(unsafe_code)] pub mod attestation; pub mod delta; +/// Key store and lifecycle manager. Not used by the `jk` reversibility path — +/// see the module map at the top of this file and docs/adr/0001-identity-and-scope.md. pub mod keys; pub mod obliteration; pub mod operations; diff --git a/crates/januskey-cli/src/main.rs b/crates/januskey-cli/src/main.rs index 864413c..b422e86 100644 --- a/crates/januskey-cli/src/main.rs +++ b/crates/januskey-cli/src/main.rs @@ -2,8 +2,7 @@ // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell // -// JanusKey CLI: Provably Reversible File Operations -// "Never lose data again" +// JanusKey CLI: reversible file operations with inversion metadata use anyhow::{Context, Result}; use clap::{Parser, Subcommand}; @@ -22,10 +21,13 @@ use std::path::{Path, PathBuf}; name = "jk", version = "1.0.0", author = "Jonathan D.A. Jewell ", - about = "JanusKey: Provably reversible file operations", - long_about = "JanusKey makes every file operation reversible through Maximal Principle Reduction.\n\ - Delete files, modify content, move things around—and always be able to undo.\n\n\ - Data loss is architecturally impossible." + about = "JanusKey: reversible file operations with inversion metadata", + long_about = "JanusKey stores the inverse of each file operation in an append-only, \ + content-addressed log, so a delete, modify, move or copy can be undone by \ + metadata lookup rather than restored from a backup.\n\n\ + Reversibility is an engineering mechanism here, not a proved theorem: the \ + obligations in PROOF-NEEDS.adoc are still open, and obliteration is \ + best-effort on modern media." )] struct Cli { #[command(subcommand)] @@ -108,8 +110,9 @@ enum Commands { new_name: PathBuf, }, - /// Obliterate a file: securely overwrite then remove it (NOT reversible). - /// Implements GDPR Article 17 "right to erasure". + /// Obliterate a file: overwrite then remove it (NOT reversible). + /// Best-effort erasure, not a guarantee of physical erasure and not a + /// compliance determination. See PROOF-NEEDS.adoc row X-1. Obliterate { /// File(s) to obliterate #[arg(required = true)] diff --git a/crates/januskey-cli/src/obliteration.rs b/crates/januskey-cli/src/obliteration.rs index c00f8fd..73996e0 100644 --- a/crates/januskey-cli/src/obliteration.rs +++ b/crates/januskey-cli/src/obliteration.rs @@ -3,7 +3,9 @@ // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell // // RMO: Obliterative Wipe Primitive -// Implements GDPR Article 17 "Right to Erasure" with formal obliteration proofs +// The erasure use case. There are no formal obliteration proofs: overwriting is +// best effort (see PROOF-NEEDS.adoc row X-1), and an ObliterationProof records +// what was claimed destroyed, not that it is unrecoverable. // // The RMO primitive provides: // 1. A best-effort DoD 5220.22-M-style multi-pass overwrite of the file's @@ -433,7 +435,8 @@ fn entry_hashes(op: &OperationMetadata) -> impl Iterator { } /// Obliterate every recoverable trace of `path` inside a JanusKey store -/// (GDPR Article 17 "right to erasure" for a tracked file): +/// (the erasure use case for a tracked file; this is not a compliance claim — +/// see PROOF-NEEDS.adoc row X-1 on physical erasure): /// /// 1. shred and remove the working file, if it still exists; /// 2. shred every content-store blob referenced by an operation-log entry diff --git a/crates/reversible-core/Cargo.toml b/crates/reversible-core/Cargo.toml index 3782f6d..8b83aa5 100644 --- a/crates/reversible-core/Cargo.toml +++ b/crates/reversible-core/Cargo.toml @@ -4,7 +4,7 @@ [package] name = "reversible-core" version = "0.1.0" -description = "Core types for provably reversible operations — content-addressed storage, operation metadata, and transaction management" +description = "Core types for reversible operations — content-addressed storage, operation metadata, and transaction management (proofs pending)" keywords = ["reversible", "content-addressed", "transactions", "undo", "formal-verification"] categories = ["data-structures", "filesystem"] edition.workspace = true diff --git a/crates/reversible-core/src/content_store.rs b/crates/reversible-core/src/content_store.rs index 437fb7b..0e9b097 100644 --- a/crates/reversible-core/src/content_store.rs +++ b/crates/reversible-core/src/content_store.rs @@ -77,8 +77,9 @@ impl std::fmt::Display for ContentHash { /// Stores content by SHA256 hash with optional gzip compression. /// Automatic deduplication: identical content is stored once. /// -/// This is the shared storage backend that both januskey-cli and -/// valence-shell use for reversible operation data. +/// Used by januskey-cli for its undo data. valence-shell is an *intended* +/// consumer and does not depend on this crate yet; see +/// docs/adr/0001-identity-and-scope.md §4. pub struct ContentStore { /// Root directory for content storage root: PathBuf, diff --git a/crates/reversible-core/src/lib.rs b/crates/reversible-core/src/lib.rs index fa0ab25..2962d4d 100644 --- a/crates/reversible-core/src/lib.rs +++ b/crates/reversible-core/src/lib.rs @@ -2,18 +2,22 @@ // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell // -// reversible-core: Shared types for provably reversible operations +// reversible-core: Shared types for reversible operations (proofs pending) // // Extracted from JanusKey — the development proof-of-concept for // reversibility theory established in absolute-zero (maa-framework). // // Lineage: // maa-framework (policy) → absolute-zero (theory) → januskey (PoC) -// → ochrance, valence-shell, aletheia (applications) +// → ochrance, valence-shell, aletheia (intended consumers) // -// This crate provides the shared foundation that all three applications -// use: content-addressed storage, operation metadata, and the -// ReversibleExecutor trait. +// This crate is *intended* to be the shared basis for reversible operation data: +// content-addressed storage, operation metadata, and the ReversibleExecutor +// trait. It is not yet shared: no repository outside this workspace depends on +// it, ARCHITECTURE.adoc Phase 2 (valence-shell) and Phase 3 (ochrance) are +// unstarted, and the hash algorithm at the manifest boundary is unresolved +// (SHA-256 here, BLAKE3 believed there). See +// docs/adr/0001-identity-and-scope.md §4 for what may and may not be claimed. #![forbid(unsafe_code)] @@ -34,7 +38,9 @@ pub use transaction::{ /// Trait that any reversible operation system must implement. /// -/// This is the Rust-side mirror of ochrance's `VerifiedSubsystem` interface. +/// This is *intended* as the Rust-side mirror of ochrance's +/// `VerifiedSubsystem` interface; no ochrance-side implementation or consumer +/// exists yet, and none has been tested against this trait. /// Implementations provide: /// - Forward execution of operations with metadata for reversal /// - Undo of previously executed operations diff --git a/crates/reversible-core/src/manifest.rs b/crates/reversible-core/src/manifest.rs index 26503a7..439cc81 100644 --- a/crates/reversible-core/src/manifest.rs +++ b/crates/reversible-core/src/manifest.rs @@ -5,10 +5,15 @@ // A2ML Manifest Emitter // // Generates A2ML (Attestation & Audit Markup Language) manifests from -// operation logs. These manifests can be consumed by ochrance's -// VerifiedSubsystem::verify to produce VerificationProof witnesses. +// operation logs. These manifests are *intended* to be consumed by ochrance's +// VerifiedSubsystem::verify, which would produce VerificationProof witnesses. +// It has never happened: nothing in this repository has been verified by +// ochrance, the crate is not consumed outside this workspace, and the hash +// algorithm at this boundary is unresolved (SHA-256 here, BLAKE3 believed +// there). Do not describe the manifest as an interoperability result. +// See docs/adr/0001-identity-and-scope.md §4. // -// Format follows ochrance-core/Ochrance/A2ML/Types.idr: +// Format is written against ochrance-core/Ochrance/A2ML/Types.idr: // Manifest { manifestData, refs, attestation, policy } use crate::content_store::ContentHash; @@ -22,10 +27,12 @@ use sha2::{Digest, Sha256}; /// - Refs: one entry per operation, keyed by operation ID with content hash /// - Merkle root: SHA256 hash chain of all operation hashes in order /// -/// Ochrance can parse this manifest and verify: +/// Ochrance is *designed* to parse this manifest and verify: /// - Lax: manifest is well-formed /// - Checked: all content hashes match the content store /// - Attested: manifest is signed (requires external signing step) +/// +/// None of those three checks has been run by ochrance. pub struct ManifestEmitter; impl ManifestEmitter { diff --git a/crates/reversible-core/src/metadata.rs b/crates/reversible-core/src/metadata.rs index fe44d8a..600519d 100644 --- a/crates/reversible-core/src/metadata.rs +++ b/crates/reversible-core/src/metadata.rs @@ -284,13 +284,23 @@ impl MetadataStore { self.save() } - /// Save the log to disk + /// Save the log to disk. + /// + /// Replaces the log using [`crate::transaction::write_atomic`]. Parent + /// directory sync is best effort, so success does not guarantee that the + /// rename will survive a crash. + /// + /// # Errors + /// + /// Returns errors from creating the parent directory, serialising the log, + /// or creating, setting permissions on, writing, syncing or renaming the + /// temporary file. fn save(&self) -> Result<()> { if let Some(parent) = self.path.parent() { fs::create_dir_all(parent)?; } let content = serde_json::to_string_pretty(&self.log)?; - fs::write(&self.path, content)?; + crate::transaction::write_atomic(&self.path, content.as_bytes())?; Ok(()) } @@ -555,4 +565,44 @@ mod tests { assert_eq!(store2.count(), 1); assert!(store2.get(&id).is_some()); } + + /// T-8: a save replaces the log by rename, so a reader never sees a torn + /// log and no temporary file survives the save. A stale temporary file left + /// by an earlier crash is not read and does not stop the next save. + #[test] + fn save_replaces_the_log_atomically() { + let tmp = TempDir::new().unwrap(); + let dir = tmp.path(); + let path = dir.join("metadata.json"); + + let mut store = MetadataStore::new(path.clone()).unwrap(); + store.append(modify_entry("/a.txt", b"a0", b"a1")).unwrap(); + + let leftovers = |dir: &Path| -> Vec { + fs::read_dir(dir) + .expect("read dir") + .filter_map(|e| e.ok()) + .map(|e| e.file_name().to_string_lossy().into_owned()) + .filter(|n| n.ends_with(".tmp")) + .collect() + }; + assert_eq!( + leftovers(dir), + Vec::::new(), + "a save's own temporary file is renamed away" + ); + + // A torn temporary file from an earlier crash must not matter. + let stale = "metadata.json.99999.0.tmp"; + fs::write(dir.join(stale), b"{ torn").expect("plant stale tmp"); + store.append(modify_entry("/b.txt", b"b0", b"b1")).unwrap(); + assert_eq!( + leftovers(dir), + vec![stale.to_string()], + "the next save leaves the stale file alone and cleans up after itself" + ); + + let reopened = MetadataStore::new(path).expect("log parses after atomic saves"); + assert_eq!(reopened.count(), 2); + } } diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index 06dd3f4..8a182df 100644 --- a/crates/reversible-core/src/transaction.rs +++ b/crates/reversible-core/src/transaction.rs @@ -156,16 +156,17 @@ fn create_tmp(tmp: &Path, like: &Path) -> std::io::Result { /// Replace `path` with `content` so a reader sees the old file or the new one, /// never a torn write: write a uniquely named sibling temporary file, flush it -/// to disk, then rename it over `path`. The file keeps the permissions of the -/// one it replaces, from the moment it is created. +/// to disk, then rename it over `path`. If the existing file's metadata can be +/// read, its permissions are applied to the temporary file before writing. /// /// # Errors /// -/// Returns temporary-file creation, write, sync or rename errors. A temporary -/// file this call created is removed on failure; one it did not create is left -/// alone. Cleanup and parent-directory sync errors are ignored, so success does -/// not guarantee the rename will survive a crash. -fn write_atomic(path: &Path, content: &[u8]) -> std::io::Result<()> { +/// Returns temporary-file creation, permission, write, sync or rename errors. +/// A temporary file this call created is removed on a best-effort basis after +/// failure; one it did not create is left alone. Cleanup and parent-directory +/// sync errors are ignored, so success does not guarantee the rename will +/// survive a crash. +pub(crate) fn write_atomic(path: &Path, content: &[u8]) -> std::io::Result<()> { write_atomic_via(path, &unique_tmp_path(path), content) } diff --git a/docs/adr/0001-identity-and-scope.md b/docs/adr/0001-identity-and-scope.md new file mode 100644 index 0000000..e076a23 --- /dev/null +++ b/docs/adr/0001-identity-and-scope.md @@ -0,0 +1,172 @@ +# ADR-0001 — Repository identity: reversible file operations, and what the key store is for + +- **Status:** accepted, partially applied +- **Date:** 2026-11-01 +- **Supersedes:** nothing formal. Corrects the identity claims in `README.adoc`, + `PROOF-NEEDS.adoc` §Priority, `ARCHITECTURE.adoc`, `crates/januskey-cli/src/lib.rs` + and `.machine_readable/contractiles/Trustfile.a2ml` (the last needs a human; see §6). +- **Related:** estate audit `docs/estate/2026-11-01-handoff-and-consistency-audit.md`, + invariant 7 ("januskey is reversible file operations with inversion metadata; it is + **not** a cryptographic key system"). + +## 1. Context + +The estate rule is that semantic boundaries follow implementation, not repository +names. `epistemic-types@5422cd5` is the current example of that rule being applied to +another repo; this ADR applies it here. + +JanusKey's name contains "Key", its README describes reversible file operations, its +workspace builds a second binary called `jk-keys`, and its Trustfile asserts +"Januskey is a key-management tool". At least one of those four is wrong, and the +name is the least trustworthy of them. + +So: measure the coupling rather than argue about it. + +## 2. What the code actually contains + +| Component | Lines | Binary | Used by `jk`? | Evidence | +|---|---:|---|---|---| +| `operations.rs`, `delta.rs`, `obliteration.rs` | 1,900 | `jk` | yes | `main.rs` dispatch | +| `reversible-core` (store, log, transaction, manifest) | 2,202 | — | yes | `lib.rs` re-exports | +| `main.rs` + `lib.rs` | 1,220 | `jk` | — | — | +| `attestation.rs` (HMAC-chained audit log) | 627 | — | **no** | `main.rs` contains no `AuditLog` or `attestation::` reference | +| `keys.rs` (key store: Argon2id, AES-256-GCM wrap, rotate, revoke, backup) | 735 | **`jk-keys`** | **no** | `main.rs` contains no `keys::`, `KeyManager` or `keys_cli` reference | +| `keys_cli.rs` | 701 | **`jk-keys`** | **no** | separate `[[bin]]` | +| `docs/security/KEY_LIFECYCLE.adoc` | 554 | — | — | documents `jk-keys` only | + +Dependency direction, from `use` statements: + +``` +main.rs (jk) → operations / delta / obliteration → reversible-core +keys.rs → attestation.rs (AuditLog) → hmac, sha2 +keys_cli.rs → keys.rs, attestation.rs +``` + +There is **no edge in either direction** between the reversibility path and the key +subsystem. `AttestationKey` is an opaque `[u8; 32]` handed to `AuditLog::init`; it is +not derived from `KeyManager` anywhere in the tree, and nothing in `jk` ever sets one. +`KeyManager` owns an `AuditLog`, not the other way round. + +Two further facts that the identity statement has to survive: + +1. **The audit chain is not wired into the CLI.** The `jk` binary never constructs an + `AuditLog`, so "every change is tracked automatically" was never true of the CLI. + The chain is exercised by unit tests only, and obliteration records go to an + unkeyed JSON ledger (`obliterations.json`). +2. **The key store protects nothing on the reversibility path.** Content-store blobs + are plaintext, gzip-optionally-compressed files addressed by SHA-256. AES-256-GCM + is used to wrap *key material inside the key store*, not file content. + +## 3. Decision + +**JanusKey's identity is reversible file operations.** Concretely: + +- The product is the `jk` binary: `init, delete, modify, move, copy, rename, + obliterate, undo, begin, commit, rollback, preview, history, status, gc`. +- SHA-256 content addressing and the append-only operation log are part of that + product. They are not "crypto" in the identifying sense; they are storage. +- **The key lifecycle manager is not part of the product.** `jk-keys` is a separate + binary with its own store format, its own lifecycle state machine (generated / + active / rotating / suspended / revoked / obliterated), and zero coupling to + reversibility. It stays in this repository *for now* behind an opt-in feature + (`key-lifecycle`), so nothing is lost, and it leaves the default binary set and the + default identity. + Be precise about what that gate does and does not do: it stops `cargo build + --workspace` from producing `jk-keys`; it does not stop `keys.rs` from compiling + into the library, and it does not remove `aes-gcm`/`argon2` from the dependency + graph. Those go with the module move in §5. A feature gate is a statement about + the product, not a security boundary. +- The HMAC-chained audit log stays in the library and is honestly described as + **library-only, not wired into the CLI**. Wiring it is a separate decision and + requires a key-provisioning story that does not exist yet. + +The invariant "not a cryptographic key system" is therefore treated as **mandatory +for the product, and aspirational for the module**: the shipped default build no +longer offers key custody, and the remaining module is recorded here as a candidate +for extraction rather than being described as the repo's purpose. + +Why not simply move the module today: this sandbox has no `rustc`, no `cargo` and no +crates.io access, so a crate move could not be built or tested. The estate rule is +that a claim must be checkable; "the split compiles" is not checkable from here. +§5 gives the exact steps for whoever has a toolchain. + +Why not keep it and rewrite the identity as "a key-management tool that also does +reversibility": because the measurement in §2 says the reverse — reversibility is the +product, the key manager is a detached appendage with no callers. Rewriting the +identity to match the Trustfile's sentence would be inferring purpose from a name and +a comment, which is the error this ADR exists to correct. + +## 4. Valence Shell: what may and may not be claimed + +`reversible-core` was extracted on 2026-03-21 (Phase 1) so that three downstream +projects could consume it. **None of them does.** There is no `Cargo.toml` in this +tree depending on it from outside the workspace, no test that exercises a downstream +consumer, and no way from here to see another repo's dependency graph. + +Therefore, from now on: + +- **May be claimed:** the crate exists, builds in this workspace, is `#![forbid(unsafe_code)]`, and is *intended* to be the shared basis for reversible operation data. +- **May not be claimed:** that valence-shell, ochrance or aletheia use it, partly use it, or are "wired" to it. `ARCHITECTURE.adoc` Phase 2/3 are unstarted; the Merkle/hash mismatch (SHA-256 here vs BLAKE3 believed there) is unresolved, and is itself a reason a consumer cannot yet be wired. +- **Evidence that would make it claimable:** a dependency edge in the consuming repo's manifest, a passing test there that exercises `ReversibleExecutor`, and — for ochrance — a settled hash algorithm at the manifest boundary. + +The same rule applies to the A2ML manifest: `ManifestEmitter` produces text that +ochrance *is intended* to parse. Ochrance has never parsed it. The format doc comment +now says so. + +## 5. Consequences and the remaining split + +Applied now (verifiable by inspection, no build required): + +- `crates/januskey-cli/Cargo.toml`: `[features] key-lifecycle = []`; `[[bin]] jk-keys` + gains `required-features = ["key-lifecycle"]`. Default `cargo build --workspace` + therefore produces `jk` and `dashboard-check`, and omits `jk-keys`. +- Identity corrected in `README.adoc`, `PROOF-NEEDS.adoc`, `ARCHITECTURE.adoc`, + `crates/januskey-cli/src/lib.rs`, `docs/security/KEY_LIFECYCLE.adoc`, + `.machine_readable/6a2/STATE.a2ml`. +- Consumption status pinned in `ARCHITECTURE.adoc` and as ledger rows `V-1`, `V-2` in + `PROOF-NEEDS.adoc`, so "valence-shell consumes reversible-core" cannot drift back + into prose without a row changing status. + +Not applied — needs a toolchain: + +1. Create `crates/januskey-keys` with `keys.rs`, `keys_cli.rs` and their dependencies + (`aes-gcm`, `argon2`, `rand`, `zeroize`, `uuid`, `chrono`, `base64`, `subtle`), + depending on `januskey` for `attestation::AuditLog`. +2. Cut the two import edges: `use crate::attestation::AuditLog` → `use januskey::attestation::AuditLog`; + `use januskey::keys::…` → `use januskey_keys::…`. +3. Remove the three `KeyAlgorithm` references in `attestation.rs`'s test module (lines + ~524, ~568, ~611) to avoid a dev-dependency cycle, or make them a dev-dependency of + the key crate. +4. Drop `pub mod keys;` and the `pub use keys::{…}` re-export from `januskey`, and the + key dependencies from `crates/januskey-cli/Cargo.toml`. +5. **Acceptance:** `cargo build -p januskey` does not compile `keys.rs`; `cargo tree -p januskey` + lists neither `aes-gcm` nor `argon2`; `cargo test --workspace` green; the Trustfile + rule `no-metadata-only-key-types` passes in the repo that ends up owning the module. + +After that, `jk-keys` can move to whichever repo needs key custody. That is not this one. + +## 6. What a human has to do + +Two files contradict this ADR and are **agent-denied** by the Trustfile +(`@trust-deny: [modify-trustfile, modify-threat-model]`). An agent must not edit them, +and this ADR does not: + +| File | Line | Wrong statement | Needed | +|---|---|---|---| +| `.machine_readable/contractiles/Trustfile.a2ml` | 8–10 | "Januskey is a key-management tool: any LLM/agent interaction with it must treat every key, audit entry…" | One sentence from the owner; the crypto-specific deny-list is still correct if the key module stays | +| `.machine_readable/threat-model.a2ml` | `[primitives.mac]` | Still describes the home-rolled `SHA256(key‖data‖prev)` as the live construction | Mark resolved: `attestation.rs` now uses real HMAC-SHA256 | + +Also owner-decided, out of agent scope: the crate version `1.0.0` against README's +alpha/D-phase status, and whether `jk-keys` should be published at all once split. + +## 7. Rejected alternatives + +- **Rename the repo.** Names do not fix coupling; `jk-keys` in a repo called + `reversible-fs` is the same defect. +- **Delete `keys.rs` outright.** It is 1,436 lines of working, tested code with a + legitimate future owner, and deletion here would be unverifiable (no build) and + irreversible in the estate's sense. +- **Keep it and call the repo a key-management tool.** Contradicted by §2: no caller, + no content encryption, no CLI wiring. +- **Declare the invariant satisfied today.** It is not: `keys.rs` is still in the + library's public API (`pub mod keys`). §3 says so rather than claiming the win. diff --git a/docs/estate/2026-11-01-handoff-and-consistency-audit.md b/docs/estate/2026-11-01-handoff-and-consistency-audit.md new file mode 100644 index 0000000..2ccb98c --- /dev/null +++ b/docs/estate/2026-11-01-handoff-and-consistency-audit.md @@ -0,0 +1,655 @@ +# JanusKey — estate handoff and consistency audit + +**Date:** 2026-11-01 +**Branch:** `arena/ed943c46-januskey` (base = `main` @ `4afb710`, 2026-10-29, "chore(deps): Bump the actions group with 2 updates (#165)") +**Subject:** re-recon of `hyperpolymath/januskey`, division of concern between this repo and the other estate chats, a 16-item consistency audit against the proven invariants, and one paste-ready prompt per relevant sibling repo. + +--- + +## 0. What this audit can and cannot stand on + +Stated first, because the whole point of the invariant list is that claims get checked against source: + +| Fact | Consequence | +|---|---| +| The checkout is **shallow (depth 1)** — `git log` returns exactly one commit. | No commit archaeology. "Recent work" cannot be reconstructed from history. | +| **`cargo`, `rustc`, `idris2`, `agda` are not installed**, and crates.io is not reachable from this sandbox. | I could **not re-run any gate**. Where I write PROVEN below I mean *"the ledger names a theorem and the theorem text exists in the named file, and the gate script that would check it exists"* — not *"I re-ran it and it passed"*. | +| Only `januskey` is checked out. No sibling repo is present. | Every statement I make about another repo is either (a) the user-supplied invariant, or (b) an explicit quotation of what **januskey's source asserts about them**. Nothing about a sibling's internals is derived from its name. | +| This branch contains **no agent commits** — `HEAD` is `main`'s tip. | There is no prior "recent output" of mine to audit. The audit below is therefore an audit of (i) the model I am about to work from and (ii) the repo's own published claims as they stand today. I have flagged that distinction wherever it matters. | + +**Held disconfirmed-able:** every claim in §3 has a file, line or section behind it, listed inline. + +--- + +## 1. Re-recon in one page + +### 1.1 What the code says januskey is + +`README.adoc` title is *"JanusKey — Reversible File Operations"*; `crates/reversible-core/src/lib.rs` defines the identity as a `ReversibleExecutor` trait (`execute` / `undo` / `generate_manifest`); the binary is `jk` with subcommands `init, delete, modify, move, copy, rename, obliterate, undo, begin, commit, rollback, preview, history, status, gc` (`crates/januskey-cli/src/main.rs:54-160`). Reversibility is the product; content-addressed storage (`SHA-256`, `crates/reversible-core/src/content_store.rs:17-32`) plus an append-only operation log is the mechanism. + +### 1.2 Actual module map (three crates, not two) + +``` +crates/reversible-core/ content_store · metadata · transaction · manifest · error · lib(trait) +crates/januskey-cli/ operations · delta · attestation · obliteration · keys · keys_cli · main +crates/dashboard-check/ claims.rs (claims-ledger parser + runner) · main.rs (dashboard reconciliation) +src/abi/JanusKey/ABI/ Types · Layout · Foreign · Proofs (Idris2 0.8.0, one tree, .ipkg beside it) +verification/proofs/agda/ Reversibility · TransactionAtomicity (Agda 2.6.4.3, --safe --without-K) +ffi/zig/ jk_* C-ABI surface + januskey.h +tests/reject-agda/ 4 fixtures tests/reject-idris/ 3 fixtures (negative controls) +``` + +The proof split is a **kernel ruling dated 2026-10-12**: Agda is the kernel, Idris2 the runtime/ABI layer (`verification/proofs/agda/Reversibility.agda:14-18`, `PROOF-NEEDS.adoc §Recommended Prover`). The only external proof dependency is **`resource-algebra`, pinned at `cf9235c`** (`scripts/fetch-siblings.sh:9`), consumed through `ResourceAlgebra.Instances.Loss`. + +### 1.3 The instruments that make this repo trustworthy — and are its best export + +1. **A claims ledger** (`PROOF-NEEDS.adoc §Claims ledger`): one row per claim, one of five statuses `PROVEN | TESTED | ASSUMED | DESIGNED | OPEN`, each with an artefact and the command that discharges it. +2. **`dashboard-check`** (`crates/dashboard-check/src/claims.rs`): runs every PROVEN/TESTED command, and fails the build if the counts printed on README/EXPLAINME/TOPOLOGY/READINESS disagree with what it measured. Its own header names the motive: *"the estate's #1 recurring defect is 'dashboards that lie'"* (`main.rs:7`). +3. **Negative controls with expect-text matching** (`scripts/check-agda.sh:29-44`): a fixture must be refused *with the specific error it exists for*; a fixture refused for an unrelated reason fails the gate. This is the pattern the estate should steal. +4. **Removal discipline**: lemmas that were tautologies are deleted with the reason recorded in place, not left as decoration (`PROOF-NEEDS.adoc §Removed` — 18 entries, e.g. `identityIsCNO` "(`s = s`)", `hashOneWay` "(`Void -> Void`)"). + +### 1.4 True state (per the repo's own reconciled dashboards) + +`STATE.a2ml`: completion 60 %, CRG grade **D**, phase *"Core tests complete; 2026-04..06 wave was CI/governance/license hardening, not feature work; API stability review still pending"*. READINESS: **D — Alpha, Unstable**, 135 tests + 5 Criterion groups + **11 PROVEN** ledger rows. The eleven are ABI/model lemmas (A-1, A-2, C-1..C-5, G-1, T-1, T-2, T-3); **none of the six security obligations is proved**, and the row *"Every operation is reversible (MPR)… " is `OPEN`*. + +That is the single most important sentence in the repo: **the headline claim is still a ledger row marked OPEN.** + +--- + +## 2. Division of concern — mine here, theirs elsewhere + +### 2.1 Belongs to this repo (my work) + +| Concern | Where | Why it is mine | +|---|---|---| +| Reversibility semantics (`execute ∘ undo ≡ CNO`) in the Rust | `crates/reversible-core`, `crates/januskey-cli/operations.rs`, `delta.rs` | Only januskey can change its own executor | +| Metadata/transaction atomicity (T-5 done, **T-8 open**: `metadata.rs:288-293` was a plain `fs::write` when this was measured; it now calls `write_atomic`, unbuilt — see the Addendum) | `reversible-core` | Internal invariant, and the concrete asymmetry I would fix next | +| Attestation chain, now a real HMAC-SHA256 (`attestation.rs:9,189-212`; STATE marks `homerolled-hmac` RESOLVED — `threat-model.a2ml` §primitives.mac is stale on this point) | `januskey-cli/attestation.rs` | Internal | +| Obliteration / CAS scrubbing (TESTED end-to-end, `tests/obliteration_cas_test.rs`) | `januskey-cli/obliteration.rs` | Internal | +| Key store (AES-256-GCM + Argon2id; Ed25519/X25519 refused at the CLI, `keys_cli.rs:282-291`) | `januskey-cli/keys.rs`, `keys_cli.rs` | Internal, and *scope-adjacent* — see audit §7 | +| Idris2 ABI + Agda kernel + the claims ledger + `dashboard-check` | `src/abi`, `verification/`, `crates/dashboard-check` | Internal | +| Doc-surface drift (§4) | README, EXPLAINME, TOPOLOGY, STATE, `0-AI-MANIFEST`, `docs/` | Internal, and currently the largest defect mass | + +### 2.2 Belongs to other chats (I can state the interaction, not the truth of their internals) + +| Repo | Relation to januskey, as recorded **here** | Whose call it is | +|---|---|---| +| `resource-algebra` | **Hard dependency.** Pinned `cf9235c`; supplies the `Loss` grade + `IsSeqMonoid` structure the Agda proofs are stated in; its homomorphisms are listed OPEN, which is why januskey's G-3 is OPEN | theirs | +| `absolute-zero` | Lineage only: *"maa-framework → absolute-zero (CNO theory) → januskey"* (`Types.idr:7`, `lib.rs:12`, `ARCHITECTURE.adoc §Lineage`). januskey **re-proves** CNO composition locally (`Proofs.idr::seqCNO`) instead of importing it | theirs | +| `ochrance` | Intended consumer of `ManifestEmitter` A2ML. **Hash mismatch is unresolved**: `ContentHash` is hard-coded `sha256:` (`content_store.rs:17-32`) and its doc comment claims correspondence to *"ochrance's `Hash` type with `algorithm = SHA256`"*, while ARCHITECTURE §Deferred says *"ochrance uses BLAKE3 height-indexed trees"* | shared; theirs to confirm | +| `valence-shell` | **Downstream.** ARCHITECTURE §Phase 2 (NEXT): shell depends on `reversible-core`, `ContentStore` into `ShellState`, replace inline `undo_data: Option>`, replace `verification.rs` stubs | theirs, once we publish the trait | +| `VeriSimDB` (`nextgen-databases`) | One declaration, no code: `.machine_readable/integrations/verisimdb.a2ml`, `type = "data-feed"`, destination `verisimdb-data/feeds/`, **`format = "hexad"`** | theirs | +| `hypatia` | Scan config only; `NEUROSYM.a2ml` sets `report-format = "logtalk"` | theirs | +| `boj-server` | A `januskey-mcp` cartridge is **blocked**: threat model is `draft-pending-human-review` since 2026-04-19 (`STATE.a2ml §blockers`) | owner sign-off + boj-server | +| `panic-attacker` | `just assail` shell-out (`Justfile:135-136`); 241 `unwrap()` sites currently | theirs (tooling) | +| `aletheia` | Third downstream, **deferred**: *"Too early (Phase 0 research, no operation types yet)"* | theirs | +| `tropical-types`, `epistemic-types`, `choreographic-types`, `echo-types`, `residual-evidence-types`, `JtV`, `ephapax`, `ECHIDNA`, `proof-burrower` | **No dependency, no pin, no code.** Only three incidental prose/comment mentions (see audit §5, §8, §12, §14) | theirs | + +### 2.3 Boundary items that need an agreed answer from both sides + +1. **Hash function at the manifest boundary** (SHA-256 here vs BLAKE3 alleged there). +2. **ABI struct layout** — `ObliterationProof` is 112 bytes, `ContentHash` 32, `KeyId` 16, 8-byte aligned (`Layout.idr`, PROVEN C-5). Any sibling embedding these must agree, and `scripts/check-abi-layout.sh` is the only guard. +3. **Log format** — `OperationLog` JSON is januskey's own; nothing else may read it without a version. + +--- + +## 3. Consistency audit + +Format: **STATUS** / one-line evidence / action. + +### Structural invariants + +**1. Central substrate (VeriSimDB octad, VCL, no point-to-point).** +**STATUS: ✅** — one flag. +*Evidence:* `grep` for `reqwest|hyper|TcpStream|UdpSocket|ureq|curl|http` across `crates/` returns **zero** hits; januskey contains no VCL implementation and no subsystem-to-subsystem protocol. Its only outbound artefact is a *string* (`ManifestEmitter`), plus a declared file-drop feed. +*Flag (not a contradiction):* the declared feed says `format = "hexad"` — six, not eight — and is not VCL-mediated. It is inert today (nothing writes it). +*Action:* either delete `.machine_readable/integrations/verisimdb.a2ml` as dead config, or restate it as an octad/VCL feed. Do not implement it as written. + +**2. Echo↔Resource is E→R only; Echo is not a resource instance.** +**STATUS: ✅** (with a name-collision caveat). +*Evidence:* januskey has no Echo integration of any kind; `echo` occurs once, as *"the echo loss grade"* in `Reversibility.agda:6-7`, naming a grade in `resource-algebra`'s `Loss` instance. No conversion in either direction, so no bidirectional assumption could have crept in. +*Caveat:* I do **not** know that this "echo" and `echo-types` are the same thing. Treated as unresolved, not as an identity. +*Action:* none in code; ask echo-types (§4.9). + +**3. No universal adapter (`hub_ceiling`).** +**STATUS: ✅**, one watch item. +*Evidence:* `ReversibleExecutor` is a *generic interface with per-backend implementations* (`lib.rs:52-72`), which is the shape a no-go theorem permits; it transduces nothing by itself, and `generate_manifest` is per-implementation. Not a universal adapter. +*Watch item:* the phrase *"the shared foundation that all three applications use"* (`lib.rs:15-17`) is a **code-sharing** claim that none of the three has yet exercised, and the A2ML manifest is exactly where a "one format fits all" assumption could form — indeed `ContentHash` already hard-codes `sha256:` while the deferred note says ochrance is BLAKE3. +*Action:* keep one executor per backend; make the hash algorithm an associated type before any second implementor appears; do not advertise manifest portability until §2.3(1) is settled. + +**4. absolute-zero is a consumer of proof infrastructure with 61 undischarged axioms; OND-6 open by design.** +**STATUS: ✅.** +*Evidence:* absolute-zero appears only as lineage (`Types.idr:7-9`, `lib.rs:12-14`) and as a *local re-proof* — `Proofs.idr::seqCNO` proves CNO composition inside januskey's own model; nothing imports an absolute-zero theorem, and no januskey row cites an absolute-zero Qed count. External assumptions are held explicitly as ASSUMED `X-1` (hash one-wayness, physical erasure). +*Action:* keep it; never let an absolute-zero result become a januskey ledger receipt. + +**5. K-CUT is OPEN; VCL-UT L8 blocked; choreographic-types is research-blocked.** +**STATUS: ✅.** +*Evidence:* `choreographic-types` appears twice, both as a **pattern citation** — `.github/workflows/agda-proofs.yml:3` ("Pattern: choreographic-types / residual-evidence-types (pinned Debian prover, sibling fetched by commit)") and `scripts/fetch-siblings.sh:4`. No code, no pin, no dependency, no deployability claim. +*Action:* reword those two comments to say "pattern, no dependency" so a future reader cannot mistake a citation for a link. + +**6. Epistemic model is discrete-constructive; no continuous confidence; no bind/extract.** +**STATUS: ✅** — and this is the strongest match in the audit. +*Evidence:* januskey's own model is discrete too: `data Knows : Agent -> Type -> Type` with three constructors, no numeric confidence anywhere in `Types.idr:378-400`, and `KeyState` is a six-constructor sum (`keys.rs:110-117`). The ledger states plainly that `Knows Adversary a` being uninhabited is *"a modelling choice, not a security proof"* and that E-1 is **OPEN**. There is no monadic bind and no comonadic extract — it is an inductive family, not a modality. +*Action:* none; and do not ask epistemic-types for a 0–1 confidence model (§4.6). + +**7. januskey is file-level reversibility, not key management; part of Valence Shell.** +**STATUS: ✅ on identity / ⚠️ on two particulars.** +*Evidence:* identity is reversibility (title, `lib.rs`, CLI surface). But: +(a) **`keys.rs` is 735 real lines** — AES-256-GCM wrap, Argon2id (64 MiB/3/4), rotation, revocation, obliteration, plus a second binary `jk-keys` (701 lines) and a 550-line `docs/security/KEY_LIFECYCLE.adoc`. "Not a key system" is true of its *purpose*, false of its *surface*. `PROOF-NEEDS.adoc §Priority` even says *"JanusKey handles cryptographic key management…"* — that framing is drift. +(b) **Direction of containment is inverted.** `ARCHITECTURE.adoc §Lineage` puts `valence-shell` **downstream** of januskey (`januskey → {ochrance, valence-shell, aletheia}`), with `reversible-core` as the shared library the shell will consume in Phase 2. januskey is a *sibling ancestor*, not a component of the shell. +*Action:* keep treating the work as file-level reversibility; correct the model to "upstream of valence-shell"; stop describing januskey as a key-management system in PROOF-NEEDS. + +**8. JtV v2 is a separate research program; convergence monitored, not depended on.** +**STATUS: ✅.** +*Evidence:* zero references to JtV / ReversalToken / `reversaltoken` anywhere in the tree (case-insensitive, excluding `.git`). +*Action:* none. + +**9. Ephapax legacy preservation is provably false; the `Admitted` is durable.** +**STATUS: ✅.** +*Evidence:* zero references to ephapax; nothing in `src/abi` or `verification/` attempts such a closure. The only `Admitted`-class markers in the tree are the *deliberately removed* tautologies listed in `PROOF-NEEDS.adoc §Removed`. +*Action:* none. Respect the negative result. + +**10. VSH trust boundary is the extraction gap (Lean→Rust); vsh proves algorithmic, not thermodynamic, reversibility; RMO is an engineering primitive, not GDPR compliance.** +**STATUS: ⚠️ — my model is correct, but januskey's own docs contradict it in three places.** +*Evidence:* januskey has no Lean at all; its gap is Agda/Idris2 → Rust, and it is scrupulous about it — G-2 (Idris↔Agda correspondence) is `ASSUMED`, *"no mechanical link claimed"*, and X-1 keeps crypto/physical assumptions outside the theorem set. **But:** +1. `docs/wiki/theory/rmo-primitive.md:8` — *"…implements GDPR Article 17 'Right to Erasure' **with mathematical certainty**"*, with a "Theorem" whose proof is four informal steps and a `∎`. +2. `docs/security/THREAT_MODEL.adoc:287` — compliance table claims *"256-bit symmetric, **256-bit ECC**"*, while `keys.rs:66-76` says Ed25519/X25519 are *"Reserved / NOT IMPLEMENTED"* and `keys_cli.rs:282-291` refuses to generate them. +3. `docs/wiki/theory/maa-framework.md:193-199` maps GDPR Art. 17/5/30 onto RMO/RMR as though the mapping were established. +*Action (in this repo, next):* rewrite the three surfaces to engineering-primitive language; state explicitly that GDPR compliance is a *controller-level* determination and that RMO supplies (i) best-effort overwrite and (ii) a commitment record, neither of which is an erasure guarantee on SSD/CoW/journaled media (already correctly stated in README §"secure obliteration exception" and GLOSSARY — the wiki contradicts the README). + +### Architectural consistency + +**11. Logtalk was removed; `.lgt` files are dead; the live rule system is Elixir.** +**STATUS: ⚠️ (one live-looking reference).** +*Evidence:* zero `.lgt`/`.logtalk` files. But `.machine_readable/6a2/NEUROSYM.a2ml` still carries `report-format = "logtalk"` — a machine-readable config value naming a removed system, in the file `0-AI-MANIFEST.a2ml` declares authoritative. +*Action:* confirm with `hypatia` whether `logtalk` is still a valid report-format enum; if not, change it to the current value. Do not treat Logtalk as live in prose anywhere else (I do not). + +**12. tropical-types is Lean-pure: Lean Init only, zero sorry, zero Classical.choice, zero Mathlib.** +**STATUS: ✅.** +*Evidence:* **no `.lean` file, no `lakefile`, no `lean-toolchain` anywhere in januskey.** The only tropical content is 6 lines of Idris2 min-plus inside the ABI (`Types.idr:337-380`), and both "proofs" are `Refl` over literals (`Proofs.idr:196-201`: `tropAdd`/`tropMul` restated) — which is precisely the class of row this repo *deletes* elsewhere. +*Action:* never propose porting januskey's Idris tropical block into tropical-types; a Lean dependency introduced there on januskey's behalf would break the purity constraint outright. Offer the negative lesson only (§4.5). + +**13. echo-types' identity claim is OPEN by design; the repo is built to falsify itself.** +**STATUS: ✅.** +*Evidence:* no echo-types dependency; januskey applies the same discipline to its *own* claim — the MPR row ("Every operation is reversible … as a theorem linked to the Rust") is `OPEN`, and the CLI's own `about` string over-claims it (see §4 finding D3). +*Action:* do not cite `resource-algebra`'s "echo loss grade" as support for echo-types' claim. + +**14. residual-evidence-types is early research with no stable API; distinctness from echo+epistemic unanswered.** +**STATUS: ✅.** +*Evidence:* one comment mention (`scripts/fetch-siblings.sh:4`, "pattern: choreographic-types, residual-evidence-types"), no pin, no import, no API use. +*Action:* none; keep it out of januskey's dependency set until that repo publishes an API. + +### Meta-level + +**15. Name vs code.** +**STATUS: ✅ — and the discipline paid off: it found seven defects *inside* this repo.** +*Evidence:* every claim above cites a file/line or a ledger row read from source. The name-driven errors I found are all in januskey's own surfaces (appendix §4): a `docs/wiki` GDPR theorem, a `256-bit ECC` compliance row, a missing `jk shred` command that README documents, `EXPLAINME` file paths that no longer exist, three different `unwrap()` counts, and a `hexad` feed in an octad estate. +*Action:* fix the surfaces (§4), and keep the rule: no claim about a sibling that does not quote januskey source or the user's invariant. + +**16. Invented connections.** +**STATUS: ✅.** +*Evidence — connections I am proposing, all source-backed:* `resource-algebra` (pinned commit), `ochrance` (manifest + unresolved hash algorithm), `valence-shell` (Phase 2, downstream), `verisimdb-data` (declared feed, inert), `hypatia` (scan config), `boj-server` (MCP cartridge, blocked), `panic-attacker` (Justfile shell-out), `aletheia` (deferred). +*Evidence — connections I explicitly decline:* Echo↔Resource bidirectional; any universal adapter; Echo-as-resource; a tropical-types dependency; an epistemic-types dependency; a choreographic-types dependency; any VCL implementation inside januskey. +*Only residual risk:* the A2ML "shared manifest" phrase (§3, item 3). + +### Audit verdict on the model + +**The structural model is intact. All sixteen invariants are consistent with what I found; none is contradicted by code.** The drift is elsewhere — in januskey's *published surfaces*, which over-claim against januskey's *own* instruments. Three items carry real uncertainty and are listed as such rather than resolved by inference: `hexad` vs octad (§1), whether `resource-algebra`'s "echo" is `echo-types`' echo (§2, §13), and whether `report-format = "logtalk"` is still a live enum (§11). + +--- + +## 4. Defects found in this repo (the actual regression surface) + +Ranked by hazard. Each is fixable here, by me, without touching any sibling. + +| # | Defect | Receipt | Hazard | +|---|---|---|---| +| D1 | Wiki asserts GDPR Art. 17 compliance "with mathematical certainty" and a hand-waved theorem | `docs/wiki/theory/rmo-primitive.md:8,199-215` | **High** — legal/ethical over-claim, contradicts README + GLOSSARY + `X-1` | +| D2 | Security doc claims "256-bit ECC" | `docs/security/THREAT_MODEL.adoc:287` vs `keys.rs:66-76`, `keys_cli.rs:282-291` | **High** — claims an unimplemented primitive | +| D3 | CLI `about` says "Provably reversible file operations" while the MPR ledger row is `OPEN` | `main.rs:25` vs `PROOF-NEEDS.adoc §Claims ledger` (last row) | **High** — ships the over-claim in the binary | +| D4 | `EXPLAINME.adoc` describes a tree that no longer exists (`januskey-cli/src/metadata.rs`, `content_store.rs`), claims "100% Reversible", and prints "CRG Grade: C" | `EXPLAINME.adoc:11,29-41,65` vs `reversible-core/src/*.rs`, `STATE.a2ml` (D) | **Med** — it is the *receipts* document and it is stale | +| D5 | VeriSimDB feed declares `format = "hexad"` | `.machine_readable/integrations/verisimdb.a2ml` | **Med** — wrong arity in a machine-readable file | +| D6 | Three different `unwrap()` counts: 225 / 265 / 241 (measured) | `READINESS.adoc:14,130`, `PROOF-NEEDS.adoc §Current State` (265) vs `grep -c 'unwrap()'` = 241 | **Med** — dashboards that lie, in a repo whose thesis is "dashboards that lie" | +| D7 | `STATE.a2ml [test-coverage] total = 67 tests, 30 Idris2 proofs` — stale (READINESS/TOPOLOGY say 135 / 11 PROVEN) | `STATE.a2ml` (assessed 2026-04-03) vs `READINESS.adoc`, `TOPOLOGY.adoc` | **Med** — the machine-readable source of truth is the stale one | +| D8 | `0-AI-MANIFEST.a2ml` points at `.bot_directives/` (actual: `.machine_readable/bot_directives/`) and `README.md` (actual: `README.adoc`) | `0-AI-MANIFEST.a2ml` §Bot Directives / §Repository Structure | **Med** — the first file an agent reads is wrong | +| D9 | README documents `jk shred`; no `Shred` subcommand exists (it is `jk obliterate`), and `rename`/`obliterate`/`gc` are undocumented | `README.adoc §Commands`, `GLOSSARY.adoc` vs `main.rs:54-160` | **Low–Med** — name-vs-code, in the README | +| D10 | `threat-model.a2ml` still describes a home-rolled HMAC as the live state | `.machine_readable/threat-model.a2ml §primitives.mac` vs `attestation.rs:9,189-212`, `STATE.a2ml §blockers` (RESOLVED) | **Low** — stale in the security-critical direction (harmless, but wrong) | +| D11 | Ledger says "265" and "225" `unwrap()` calls in two places in the *same file* | `PROOF-NEEDS.adoc §Current State` / `§Recommended Prover` | **Low** | + +Open technical gap I would take next after the surfaces: **T-8** — `MetadataStore::save` is a plain `fs::write` (`metadata.rs:288-293`) while `TransactionLog::save` already has the tested write→permission-copy→fsync→rename path (`transaction.rs:159-193`). Porting that one function closes a ledger row and removes an asymmetry no reader would guess from the module names. *(Done later the same day — see the Addendum. The row stays OPEN until the test runs.)* + +### 4.1 Corrections applied (same day) + +D1–D3 are fixed in the working tree, together with every other instance of the +same two claim classes (a guarantee of reversibility; a GDPR/erasure +determination). No ledger row changed status, and no test or proof count +changed, so `dashboard-check`'s dashboards/ledger reconciliation is unaffected. + +| Defect | Change | Files | +|---|---|---| +| D1 | RMO page rewritten: what `jk obliterate` does (3 passes with `sync_all`, unlink, shared-blob rule, log purge), that the commitment is a tamper-evident record and not a proof of absence, that `storage_cleared` is self-asserted, a PROVEN/TESTED/ASSUMED/OPEN table, and an erasure-request table that states what a controller still has to determine. The invented `∎` theorem and the three CLI commands that do not exist (`--hash`, `obliteration-history`, `verify-obliteration`) are gone | `docs/wiki/theory/rmo-primitive.md` | +| D1 (siblings) | RMR page rewritten to the strength of the ledger (T-1..T-8), including what `FileMetadata::apply` actually restores — permissions yes, owner/group/mtime/symlink identity no — and that transactions provide resumable rollback, not isolation. MPR, MAA and formal-model pages de-claimed, and MAA's compliance table became a requirements table with a "what this does not establish" column | `rmr-primitive.md`, `mpr.md`, `maa-framework.md`, `formal-model.md`, `theory/index.md`, `Home.md`, `architecture/index.md` | +| D2 | Compliance mapping rewritten as design intent with a "what exists" column; the `256-bit ECC` row replaced (Ed25519/X25519 refused at the CLI); BLAKE3 removed from the primitives table (not a dependency); content store noted as unencrypted; the executive summary no longer claims MPR achieves guarantees | `docs/security/THREAT_MODEL.adoc` | +| D3 | `about` / `long_about` restated; the `Obliterate` help no longer claims a GDPR determination; module headers and both crate descriptions aligned | `crates/januskey-cli/src/main.rs`, `lib.rs`, `obliteration.rs`, `crates/reversible-core/src/lib.rs`, both `Cargo.toml` | +| D4 | EXPLAINME rewritten: the phantom "100% Reversible — every operation can be undone, always" heading (a claim the README does not actually make) became the mechanism it can defend; the file map now points at the files that exist (`reversible-core` for store/log/transaction, `operations.rs` for the executors); the audit-trail claim states what is purged by `obliterate`/`gc` and that the obliteration ledger is unkeyed; the phantom CRG "C (Beta)" line now matches STATE/READINESS (D) and says the checker enforces it | `EXPLAINME.adoc` | +| D5-adjacent | TOPOLOGY's diagram label `(Provably Reversible State)` → `(Reversible, proofs pending)`, width preserved; STATE records this session's work; the TOPOLOGY date is bumped so it does not predate STATE | `TOPOLOGY.adoc`, `.machine_readable/6a2/STATE.a2ml` | + +Superseded by §4.2: D6, D7, D8 and D9 are closed; D10, the Trustfile +sentence, T-8 and the module move are blocked for the reasons tabulated there. + +### 4.2 Identity resolved, and the mechanical defects (same day, second pass) + +**ADR-0001 (`docs/adr/0001-identity-and-scope.md`)** resolves the identity from code +rather than from the name, the README or the Trustfile: + +- The `jk` binary's implementation is `main.rs + lib.rs + operations.rs + delta.rs + + obliteration.rs` over `reversible-core`. That is the product. +- Measured coupling to the key subsystem is **zero in both directions** (`main.rs` + contains no `keys::`, `KeyManager` or `keys_cli` reference; `keys.rs` imports only + `attestation::AuditLog`). The audit chain is **library-only** — `main.rs` never + constructs an `AuditLog` — and the content store is plaintext, so the key store + protects no file content. +- Decision: key lifecycle is not part of the product. The `jk-keys` binary is gated + behind the opt-in `key-lifecycle` feature (default `cargo build --workspace` + produces `jk` only); the module move to `crates/januskey-keys` is specified in + ADR-0001 §5 with acceptance criteria, and is **not** applied because this session + has no toolchain to build or test it. +- The invariant "not a cryptographic key system" is therefore satisfied for the + *product* and not yet for the *module*; ADR-0001 §7 says so rather than claiming + the win. + +**Consumption claims pinned.** `reversible-core`'s "shared foundation that all three +applications use" was false. Ledger rows **V-1** (valence-shell), **V-2** (ochrance +verification) and **V-3** (aletheia) now carry status `DESIGNED` with a one-line +condition for changing it, the `ContentStore`/`ManifestEmitter`/`ReversibleExecutor` +doc comments say "intended, not consumed", and ARCHITECTURE has a +§Consumption status table. The ledger re-parses clean (46 rows, 4 cells each, all +non-run rows `-`, all artefacts present) and the PROVEN count is unchanged at 11. + +**Mechanical defects closed:** **D6** (241 `unwrap()` calls, one number in both +files, with the measurement command; Rust LOC corrected from "~12,200" to the +measured 11,160), **D7** (STATE's test-coverage block rewritten to the reconciled +135 tests / 11 PROVEN rows, per-category figures marked as the un-re-derived +2026-04-03 assessment), **D8** (AI manifest paths: `.machine_readable/bot_directives/`, +`README.adoc`), **D9** (README and GLOSSARY now say `jk obliterate`; `rename`, +`obliterate`, `gc` documented; `KEY_LIFECYCLE` marks `obliterate`, +`verify-obliteration`, `restore` and `recover` as specified-but-not-implemented and +carries a scope banner). + +**Still blocked, with the reason recorded rather than worked around:** + +| Item | Blocked on | +|---|---| +| **T-8** (atomic metadata log) — the one open ledger row a second implementor would inherit | No `rustc`/`cargo`/crates.io in this sandbox. **Attempted later the same day** (Addendum): `write_atomic` need not move — it became `pub(crate)` and `save` calls it — so no T-5 test moved. Still unbuilt, so still OPEN | +| **D10** (`threat-model.a2ml` still describes the removed home-rolled HMAC) | Agent-denied: Trustfile `@trust-deny: modify-threat-model` | +| **Trustfile's "key-management tool" sentence** (its lines 8–10 contradict ADR-0001) | Agent-denied: Trustfile `@trust-deny: modify-trustfile`. Owner edit, ADR-0001 §6 | +| D5 (`hexad` feed in an octad estate) | Needs VeriSimDB's answer on whether `hexad` is a live format (prompt §5.5) | +| The `crates/januskey-keys` move | Toolchain (ADR-0001 §5) | + +--- + +## 5. Handoff prompts — one per repo + +Each is written to be pasted into its own chat verbatim. They carry the januskey facts the other side cannot see, ask only questions that repo can answer, and offer only things januskey actually has. + +### 5.1 `resource-algebra` — the only hard proof dependency + +``` +Context: I am working in hyperpolymath/januskey (base commit 4afb710, 2026-10-29). Update from here, all receipts from source. + +januskey's Agda kernel is stated in YOUR Loss instance, pinned at cf9235c ("Loss/MaxPlus/HWM as read 2026-10-12"), fetched by scripts/fetch-siblings.sh. Kernel flags are --safe --without-K --no-libraries --ignore-interfaces --double-check. Our ledger (PROOF-NEEDS.adoc) currently has three rows that depend on you: +- G-1 PROVEN locally: lossless traces have only lossless steps; obliteration absorbs; wrap/unwrap is grade 1 given cancellation. Our cancellation premise is a TESTED property test, not a proof. +- G-2 ASSUMED: our Idris2 IsCNO/ReversibleOp pair corresponds to your ReversiblePair "by transcription — no mechanical link claimed". +- G-3 OPEN: the FFI bridge preserves grade 1 (a homomorphism). We record that YOU list homomorphisms as OPEN, so G-3 is blocked on your side as much as ours. + +What I need from you: +1. Is G-3 still open in your tree, and is there a statement shape you would accept as the homomorphism obligation so we can state it once, in your vocabulary, instead of twice? +2. Does the Loss instance intend to absorb a *failed* step (execute errors before mutation)? Our T-6 says "a failed execute leaves the filesystem unchanged" and is ASSUMED, so we cannot currently state a grade for the failure path. +3. Is "echo loss grade" (our Reversibility.agda header uses that phrase) your terminology for something with a fixed meaning? We cite it; we do not want to be citing a name we invented. + +What I can offer: januskey's claims-ledger + dashboard-check pattern — every claim is a row with a status (PROVEN/TESTED/ASSUMED/DESIGNED/OPEN), an artefact and the command that discharges it, and CI fails if the counts printed on the dashboards disagree with what was measured. Also our negative-control gate: each rejection fixture must fail *with the specific error it exists for*, so a fixture that breaks for the wrong reason also fails the gate. Both are small and portable if useful. + +Boundary: I will not infer your internals from repo names; everything above is what januskey's source asserts about you. Correct anything I have misquoted. +``` + +### 5.2 `absolute-zero` — lineage, not ground truth + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +Our docs place januskey downstream of you: maa-framework (policy) -> absolute-zero (CNO theory) -> januskey (PoC) -> {ochrance, valence-shell, aletheia}. src/abi/JanusKey/ABI/Types.idr:7 and crates/reversible-core/src/lib.rs:12 both record that lineage. + +But we do NOT import your theorems. We re-prove what we use inside our own model: Proofs.idr::seqCNO ("composition of CNOs is a CNO") is PROVEN locally, and Layout.idr::copyIsCNO is stated over a (path,hash) log model — not over contents. Our ledger holds external assumptions explicitly as ASSUMED X-1 (hash one-wayness, physical erasure) rather than borrowing your Qed. + +I understand your status as: CNO (Certified Null Effect) + OND (Observational Null Disclosure), 115 Coq Qed with 61 undischarged axioms, a consumer of proof infrastructure rather than a provider of ground truth, and OND-6 open by design. I am treating it that way — as a proof-bearing system with known open obligations — and I am not going to cite your Qed count as evidence for anything in januskey. + +Questions: +1. Is there a canonical statement of the CNO identity (op ; inv ≡ CNO) in your tree that we should *point at* as lineage, even while proving our own? A stable name/commit would let us replace the folklore citation with a reference. +2. Does OND-6 have a target shape that a *grade*-based formulation could express? We state reversibility as a Loss grade (lossless = 1, loss = fin n, obliteration = absorbing) in Agda over resource-algebra, not as a Boolean. If OND-6 wants an observational statement, a grade may be the wrong or the right carrier and we would rather ask than assume. +3. Which of your open obligations are you content to have *downstream consumers silently ignore*? We currently ignore all of them by construction; if any are load-bearing for a consumer that claims CNO-composition, name them and we will mark them ASSUMED in our ledger. + +What I can offer: our "removal with reason recorded in place" discipline. We deleted 18 lemmas that were tautologies or restatements (identityIsCNO was `s = s`; hashOneWay was `Void -> Void`) and left the reason beside the replacement in source, plus a fixed five-status vocabulary so "proven" cannot drift into "we think so". If any of your 61 undischarged axioms are of the restatement class, that census may be cheaper than discharging them. + +Boundary: everything above is either januskey source or your stated status as given to me; I have not read your tree from here. +``` + +### 5.3 `ochrance` — the manifest bridge and an unresolved hash + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +januskey names you as the verifier in three places, and `ReversibleExecutor::generate_manifest` exists specifically to emit A2ML that you parse (crates/reversible-core/src/lib.rs:52-72, crates/reversible-core/src/manifest.rs). ARCHITECTURE.adoc §Phase 3 lists the pending work as adding Reversibility.idr types (ReversibleOp, ReversibilityProof) plus an OperationLog VerifiedSubsystem to your Idris2 ABI. + +The blocker I want to resolve with you: hash algorithm. Our ContentHash is hard-coded SHA-256 with a "sha256:" prefix (content_store.rs:17-32) and its doc comment claims it "corresponds to ochrance's Hash type with algorithm = SHA256". ARCHITECTURE §Deferred says you use BLAKE3 height-indexed Merkle trees and that "the Rust side needs a compatible implementation". Those two statements cannot both be right. Until this is settled I am refusing to call the manifest portable — the manifest is exactly where a "one format fits all backends" assumption would form, and the estate's no-go theorem says that shape is impossible. + +Questions: +1. What is your Hash type today: is `algorithm` a parameter, a fixed BLAKE3, or SHA-256? Please answer from your source. +2. At what level do you need agreement — the leaf hash, the Merkle shape, or only the A2ML field names? If only the field names, we can be honest that the bytes differ and stop pretending the trees match. +3. Do you want Lax/Checked/Attested as an ordered strengthening (each implies the last), or as independent witnesses? Our docs currently describe them as three witnesses; if you have specified an ordering, we are describing you wrongly. +4. Your VerifiedSubsystem interface: is `verify` total over malformed manifests, or may it fail? We would rather generate fewer manifests than generate ones your checker has to reject. + +What I can offer: (a) an A2ML emitter with a frozen field list and a version field you can gate on; (b) our ABI-layout guard (scripts/check-abi-layout.sh) — it checks Idris2 struct sizes/enum order/exported symbols against a C header and the Zig FFI, with a negative control that perturbs one code and requires FAIL. If you carry an Idris2 ABI, that guard is the cheap way to stop transcription drift. + +Boundary: I have not read your tree; the above is januskey's own claims about you, and I expect some of them to be stale. +``` + +### 5.4 `valence-shell` — you are downstream; also, the direction is inverted in my model + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +Two things, one of which is a correction to my own model. + +1. Correction: I had been carrying the belief that januskey is "part of Valence Shell". Our own ARCHITECTURE.adoc §Lineage says the opposite — januskey is upstream of you (maa-framework -> absolute-zero -> januskey -> {ochrance, valence-shell, aletheia}), and reversible-core is the library extracted in Phase 1 (2026-03-21, workspace builds, 44 tests) for you to consume. If your tree says something different, that is worth knowing now, because one of us is describing the dependency graph backwards. + +2. Phase 2 is listed as NEXT and unstarted from our side: wire valence-shell (impl/rust-cli/) to depend on reversible-core; add ContentStore to ShellState so undo data is content-addressed instead of the inline `undo_data: Option>`; add a2ml_emitter.rs; replace verification.rs stubs with a ReversibleExecutor impl. Nothing in januskey currently requires you to move; the trait is stable enough to read but has never had a second implementor, and I would rather you be the one to find its seams. + +What I would ask you to check before I publish anything as stable: +- Does execute/undo returning Metadata (rather than a handle) fit the shell's undo stack, or do you need the pre-state handed back? +- Our undo takes a metadata_id: &str, i.e. it looks the operation up in our log. Is that a workable contract for a shell that wants to undo *its own* last action, or does it force you to keep a parallel index? +- We record our trust boundary explicitly: the Agda/Idris2 -> Rust step is not mechanical (ledger row G-2 is ASSUMED: "transcription, no mechanical link claimed"), and the FFI grade-preservation obligation (G-3) is OPEN. If VSH's selling point is the extraction gap from Lean, ours is a different gap in a different pair of provers — please do not let the two be conflated in write-ups, in either direction. + +What I can offer: the ReversibleExecutor trait, the content store (SHA-256, dedup), the operation log with a tested atomic save (write -> permission-preserving open -> fsync -> rename, with mutants that each fail a test), and the claims-ledger discipline so that "proved" in VSH means a named artefact ran in CI, not a claim in a README. + +Boundary: I have not read your tree from here. +``` + +### 5.5 `VeriSimDB` / `nextgen-databases` — a feed declaration that is inert and the wrong arity + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +januskey declares exactly one integration with you: .machine_readable/integrations/verisimdb.a2ml — type "data-feed", data-store "verisimdb-data", destination "verisimdb-data/feeds/", with emit-scan-results, emit-build-metrics, emit-dependency-graph all true. Two problems I want to fix on my side rather than leave as a lie in machine-readable metadata: + +1. Nothing emits it. There is no network code anywhere in crates/ (no reqwest/hyper/TcpStream/ureq; grep returns zero), and no writer for that destination. The declaration is aspirational. +2. It says format = "hexad". My understanding of the estate is that VeriSimDB is an 8-modal octad engine. A hexad feed into an octad store is either a subset I should declare as such, or dead config from before the arity changed. I am not going to guess which. + +Questions: +1. Is "hexad" still a valid feed format, and if so what is it a projection of? If it is retired, what is the current identifier? +2. For a file-level reversibility tool, which of the three declared emitters are actually useful to you — build metrics and dependency graph are estate-wide scan outputs, not januskey's own data. Would scan results alone be the honest minimum? +3. Do you ingest by file drop into feeds/, or is there a VCL-shaped path you would prefer? My working model of the estate is that subsystems communicate *through* VeriSimDB via VCL and never point-to-point, so if a plain file drop into verisimdb-data counts as a bypass, I want to know before implementing it. +4. What does a *correct* januskey feed even contain? The obvious candidates are operation-log records (op kind, content hash, timestamp, transaction id) — but our ledger is explicit that operation metadata is a plain fs::write today (row T-8, OPEN), so until that is fixed any feed would be reporting from a non-atomic source. Tell me if you would rather receive nothing until T-8 closes. + +What I can offer: the concrete shape of an operation record and its content hashes, plus the caution that a feed is unverifiable provenance unless the emitting side can show its own log integrity. I would rather give you a small honest feed than a broad fake one. + +Boundary: I have not read your tree; the octad/hexad framing above is my model of the estate, not a quotation from your source. +``` + +### 5.6 `epistemic-types` — the concrete defect our model has, which your model may be able to state + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +januskey has a small epistemic model in its Idris2 ABI (src/abi/JanusKey/ABI/Types.idr:378-400): `data Knows : Agent -> Type -> Type` with OwnerKnows/SystemKnows/AuditorKnows, over agents Owner/System/Auditor/Adversary. It is discrete-constructive — no 0.0-1.0 confidence anywhere, and I am not asking you for one, since I understand your model to be discrete too (FactiveModality has reflect = knowledge; BeliefModality has no reflect = belief), with monadic bind and comonadic extract as future commitments rather than provided. + +Two obligations our model provably cannot state, both recorded in our ledger as OPEN: +- E-1: "an attacker cannot recover obliterated content or use a revoked key." We cannot state it because `Knows Adversary a` is simply uninhabited — the comment in Proofs.idr says so outright: it holds "only by construction of the model", which we classify as "a modelling choice, not a security proof". +- "The system forgets the old key" after rotation. We deleted the lemma (systemForgetsOldKey) because Knows has no negative form: it could only return knowledge of the new key and say nothing about the old. Our ledger records the deletion. + +That is the concrete question I would like to put to you: is there a modality shape — in your vocabulary, without inventing anything — that expresses *ignorance* or *forgetting* as a positive claim rather than as an absence of a constructor? Two sub-questions: +1. Does your non-reflective side (belief) help at all here, or is belief-about-X still a positive knowledge claim about X? +2. If bind/extract do not exist yet, is there a *weaker* structural property you would already stand behind (e.g. that forgetting is monotone, or that a revoked-key state is not reachable from a believing state)? + +What I can offer: a real, small consumer with a ledger that would mark any such lemma PROVEN/TESTED/ASSUMED/OPEN and would fail CI if we claimed more than we discharged — i.e. a place where a statement from you would be *used*, not just added to a pile. Also our negative-control fixtures: three Idris2 files that must be refused (double close, forgotten close, unknown-status-as-Ok) with the specific error named in the file. + +Boundary: I have not read your tree. I am treating your model as discrete and bind/extract as unprovided, and if either is wrong, say so before answering the question above. +``` + +### 5.7 `tropical-types` — a name collision, and nothing more + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +Short version: januskey does not depend on tropical-types, and after this recon I am going to keep it that way. I am writing partly to record that, and partly because januskey currently contains a *name-level* lookalike that could confuse the estate later. + +The lookalike: src/abi/JanusKey/ABI/Types.idr §"Level 11: Tropical Cost-Tracking" defines `TropCost n` with tropAdd = min, tropMul = +, copyCost n = n, oblitCost n = 3n, and Proofs.idr §8 states two lemmas — sequentialCostAdditive and parallelCostMin — whose proofs are both `Refl` over literals. In other words it is min-plus arithmetic restated, and by our own ledger rules (we deleted 18 rows of this class, e.g. identityIsCNO was `s = s`) it is not evidence of anything. It exists because an older Idris ABI wanted cost bounds in the operation types. + +What that means for you: +1. I will not propose porting it, importing it, or citing it as a tropical-anything result. If a Lean file appeared downstream on januskey's account, that would break your purity constraint (Lean Init only, zero sorry, zero Classical.choice, zero Mathlib) for no gain. +2. If januskey ever needs a real cost bound, the right move is to ask you for the statement in your vocabulary and consume it the way we consume resource-algebra — pinned by commit, never re-declared. That is the pattern we already use for our one genuine proof dependency. +3. If you would rather the lookalike not exist at all, say so and I will delete Level 11 from the ABI and record the removal with the reason in place, which is our house style. + +What I can offer: the pinned-sibling pattern (fetch by commit, verify the prover version, never vendor), and the negative-control discipline — the fixture must be refused with the error it exists for, otherwise the gate fails. If your purity constraint is currently enforced only by review, that is a cheap gate to add: grep for Mathlib/Classical.choice/sorry and fail on any hit. + +Boundary: I have not read your tree; "zero sorry / zero Classical.choice / zero Mathlib" is your stated constraint as I understand it, not something I verified from here. +``` + +### 5.8 `choreographic-types` — K-CUT is yours; januskey only borrows your CI pattern + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +No dependency, no pin, no code. The only mentions of you in januskey are two comments describing your *build pattern*: .github/workflows/agda-proofs.yml:3 ("Pattern: choreographic-types / residual-evidence-types (pinned Debian prover, sibling fetched by commit)") and scripts/fetch-siblings.sh:4. So this is a courtesy update plus one genuine question, not a request for a dependency. + +My model: K-CUT ("grading and transport commute with endpoint projection across a consistent frontier") is an OPEN CONJECTURE in your repo; VCL-UT L8 is blocked until it resolves; K-CUT-LOSS and K-CUT-WARRANT are both OPEN. I am treating choreographic-types as research-blocked and L8 as not deployable, and I am not going to cite you as infrastructure anywhere. + +The genuine question — an analogy I do not want to overstate. We have a structurally similar obligation called G-3: "the FFI bridge preserves grade 1 (homomorphism)", i.e. a property that a bridge commutes with the algebraic structure, open on both sides (resource-algebra lists homomorphisms as OPEN). We got there the honest way: our ledger row G-2 says the Idris2 and Agda presentations correspond "by transcription — no mechanical link claimed", so the bridge property has nothing to lean on. + +1. Has the K-CUT work produced a *statement shape* for "grading commutes with projection" that is generic enough to be worth restating for a grade-preserving FFI boundary? I am asking for shape, not proof. +2. Is there a formulation in which K-CUT being false would be *informative* rather than fatal — e.g. a frontier condition that names exactly where it fails? That is the style we now prefer: we keep four rejection fixtures that must fail with a named error, because a broken proof attempt is only useful if it fails for the reason you intended. +3. If we reword our two comments to "pattern, no dependency", is there a form of words you would prefer, so that the citation does not read as an integration? + +What I can offer: the pinned-sibling + pinned-prover pattern in concrete form (Debian agda-bin=2.6.4.3-1+b2 with the version asserted at runtime, sibling fetched by commit, --safe --without-K --double-check --ignore-interfaces), and the expect-text rejection harness, which is about 30 lines of bash and has already caught fixtures that were passing for the wrong reason. + +Boundary: I have not read your tree; K-CUT/L8 status above is my model, and I would like it corrected if it has moved. +``` + +### 5.9 `echo-types` — a word I use that may not be mine + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +januskey has no code relationship with echo-types: no import, no pin, no reference in any Rust or Idris file. But it has one *word*, and I would rather ask than assume. + +verification/proofs/agda/Reversibility.agda:6-7 says: "januskey's operations are graded in resource-algebra's Loss instance (the echo loss grade): a reversible step costs 1 = fin 0, information loss is fin n, obliteration is inf = 0." That phrase — "the echo loss grade" — is ours, not quoted from anyone, and I do not know whether the echo in it refers to echo-types or is internal vocabulary of resource-algebra's Loss instance. + +What I am treating as fixed, so you can correct me: +- EchoBridge proves the bridge is E->R only; NotResourceInstance proves Echo is not a resource instance. So: one-directional, no bidirectional conversion, and Echo is not a resource. +- echo-types' own identity claim is OPEN by design (criterion 2 unmet) and the repo is built to falsify its own claim. I am not treating it as established, and I am not citing our "echo loss grade" as support for it. + +Questions: +1. Is "echo loss grade" your term, resource-algebra's, or neither? If it is yours, what does the grade attach to, and does our usage (cost of a trace step) misdescribe it? +2. Since Echo is not a resource instance and the bridge is E->R only, is there any legitimate direction in which a *file-operation* log could be an echo input — i.e. an observational trace that Echo consumes? I am asking before building anything, not after. +3. Is there a one-line statement of the E->R-only result you would like quoted when other repos mention it, so the directionality does not get flattened into "Echo and resources interoperate"? + +What I can offer: nothing that depends on you, which is the point. If a plausible-looking januskey -> echo-types link ever appears, it would be an invented connection of exactly the kind the estate's separation theorems refute. + +Boundary: I have not read your tree, and I will not restate your theorems from memory beyond the two named above. +``` + +### 5.10 `residual-evidence-types` — cited once, depended on never + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +There is exactly one mention of you in januskey: a comment in scripts/fetch-siblings.sh:4 — "Fetch the proof sibling at a pinned commit (pattern: choreographic-types, residual-evidence-types)". It is a citation of a build pattern, not an import; our only pinned sibling is resource-algebra at cf9235c. No API is used, no type is named, nothing is expected to be stable. + +My model: residual-evidence-types is early research with no stable API, and its key open question is whether it is distinct from echo + epistemic or subsumed by them. So I am treating it as research, not infrastructure, and januskey will not take a dependency until that question resolves. + +The only thing I would ask: when the distinctness question resolves, whichever way it goes, a one-line note in your repo would be enough for me to stop guessing — and if the answer is "subsumed", then januskey has no business citing the name at all and I will delete the mention. + +What I can offer in the meantime, if it is useful: januskey's evidence discipline for exactly this problem — the thing that makes a claim unusable downstream is that nobody can see which part was checked. Our claims ledger forces every claim into one of five statuses (PROVEN/TESTED/ASSUMED/DESIGNED/OPEN) with an artefact and the command that discharges it, and CI fails if a dashboard prints a count that the checker did not measure. A research repo can use the same table with mostly OPEN rows; the value is that the OPEN rows are visible instead of implied. + +Boundary: I have not read your tree; the distinctness question above is my model of your open problem, not a quotation. +``` + +### 5.11 `hypatia` — one config value that may name a removed system + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +Two items, both small, both about januskey's config describing you correctly. + +1. .machine_readable/6a2/NEUROSYM.a2ml (last updated 2026-03-16, declared authoritative by 0-AI-MANIFEST.a2ml) carries `[hypatia-config] scan-enabled = true, scan-depth = "standard", report-format = "logtalk"`. My understanding of the estate is that Logtalk was removed and that the live rule system is Elixir (rules/hypatia-elixir/), with the .lgt files dead artefacts. januskey has zero .lgt files. So either "logtalk" is still a valid report-format identifier in your current tool and I should leave it, or that value is naming a removed system and is exactly the kind of dead pointer that later gets mistaken for a live dependency. Please answer from your source which it is. + +2. .hypatia/state is stale in this repo: activity.jsonl has a single entry (2026-03-08, hypatia-autofix, scan, fixes=0) and last-visit.json reports visits_total = 1. If the scanner has run since, the state file is not being written; if it has not, that is worth knowing too. Also worth flagging: the estate tech-debt scan of 2026-05-26 recorded "Idr-blv = 1" for januskey — one believe_me-class marker in a proof-bearing file — while our ledger row asserts no believe_me in src/abi (enforced by .machine_readable/contractiles/Mustfile.a2ml:110-111, which greps only src/abi/). So the marker is probably outside the guarded path. If your scanner can name the file:line, that one finding is worth more to me than the aggregate count. + +What I can offer: a claims-ledger-shaped target for scan output — if a scan finding carried claim-id, status, artefact and command, it could be reconciled by the same checker that reconciles our dashboards (crates/dashboard-check), instead of being a number a human has to trust. Also our negative-control pattern for scanner fixtures. + +Boundary: I have not read your tree; the Logtalk removal and Elixir rules path are my model of the estate. +``` + +### 5.12 `aletheia` — deferred on purpose + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +januskey lists you as the third downstream application of its reversibility work (maa-framework -> absolute-zero -> januskey -> {ochrance, valence-shell, aletheia}) and then defers you explicitly: "aletheia: Too early (Phase 0 research, no operation types yet)". I am keeping it deferred — no wiring, no expectations, and I am not going to design your operation types from here. + +What januskey actually has that you may eventually want, stated with its limits: +- reversible-core: content store (SHA-256, dedup), operation metadata, transaction log with a tested atomic save (write -> open with the log's mode -> fsync -> rename, with six mutants that each fail a test) and a ReversibleExecutor trait (execute/undo/generate_manifest). +- The limits matter more than the features: transaction atomicity is proved only for the *model* (three Agda rows over a log model), the metadata store's own save is still a plain fs::write (our row T-8, OPEN), the Idris2-to-Agda correspondence is ASSUMED not mechanical, and the headline "every operation is reversible" is an OPEN row in our ledger despite what our README and CLI banner say. I would rather you inherit an accurate picture than an optimistic one. +- OS-level operations are a different problem from file-level ones: our proofs are about a (path, hash) log, not about block devices, and our secure-overwrite path is best-effort only (SSD wear levelling, CoW, journaling). If aletheia's claim is OS-level reversibility, the gap between our model and your domain is not a porting exercise. + +What I would ask, whenever you get to Phase 1: tell me which of execute/undo/metadata is the wrong shape for an OS operation, rather than fitting your design to our trait. A trait with one implementor that nobody has stress-tested should not become the estate's interface by default. + +Boundary: I have not read your tree. +``` + +### 5.13 `boj-server` — a cartridge blocked on a signature, not on code + +``` +Context: I am working in hyperpolymath/januskey (base 4afb710). Update from here, receipts from source. + +A `januskey-mcp` cartridge is recorded in our STATE as blocked, not by engineering but by governance: .machine_readable/threat-model.a2ml is status "draft-pending-human-review" (authored 2026-04-19) and cannot be signed off by an agent. So nothing is coming to you yet, and I will not route around the block. + +What the draft already establishes, from source, so you can judge the exposure: AES-256-GCM key wrapping with per-key fresh nonces and the key UUID as AAD; Argon2id at 64 MiB / 3 iterations / 4 lanes / 16-byte salt; SHA-256 fingerprints and audit-chain linking; a second binary jk-keys that manages key lifecycle including revocation and obliteration. Two of the draft's findings are now stale in the safe direction and one in the unsafe direction: the home-rolled HMAC (H(key||data||prev)) has been replaced with real HMAC-SHA256 via the hmac crate (attestation.rs:9,189-212), but Ed25519/X25519 remain enum labels only — generation is refused at the CLI (keys_cli.rs:282-291) — while docs/security/THREAT_MODEL.adoc:287 still advertises "256-bit ECC" in a compliance table. + +What I would ask of you, before any cartridge exists: +1. What is boj-server's minimum threat-model bar for a cartridge — a signed document, a specific findings list closed, or a review record? I would rather close the right list than sign the wrong one. +2. Does a cartridge need to expose obliteration at all? Our obliteration path is irreversible by design and best-effort physically; exposing it over MCP converts a local file tool into a remote data-destruction primitive, and I think that should be a separate decision from exposing reversible operations. +3. Would you accept a cartridge that exposes only read-only history/status first, so the surface is small while the draft is unsigned? + +What I can offer: the draft's primitive inventory as a file:line-anchored document you can review directly, plus the ledger discipline so "the threat model is approved" cannot quietly become "the cartridge has no open findings". + +Boundary: I have not read boj-server's source; the above is januskey's own blocked state. +``` + +--- + +## 6. No prompt needed — deliberately out of scope for januskey + +| Repo | Why no prompt | +|---|---| +| `JtV` (v2, ReversalToken) | Zero references in januskey. Separate research programme; convergence monitored, not depended on. A prompt would be manufactured contact. | +| `ephapax` | Zero references. Legacy preservation is provably false (`Counterexample.v`, 5 Qed); the `Admitted` is durable, and januskey attempts nothing here. | +| `ECHIDNA`, `proof-burrower` | Zero references. `echidnabot` appears once, in `0-AI-MANIFEST.a2ml`, as an estate code-quality bot — a different role from the VCL peer in the invariant list, and not something januskey configures. | +| `gv-clade-index` | `.machine_readable/CLADE.a2ml` is a registry record (uuid `e216170e…`, clade `fv`, phase `active` since 2026-03-16). Nothing to discuss; it is a correct declaration. | +| `panic-attacker`, `reposystem`, `proof-of-work`, `vql-ut` | The first is a real shell-out (`Justfile:135`, 241 `unwrap()` sites to feed it); the other three appear only in `EXPLAINME.adoc` as "Dogfooted Across The Account" speculation — which is itself D4-class drift and should be deleted rather than acted on. | + +--- + +## 7. Summary + +**Intent.** januskey is a file-reversibility tool with an unusually honest verification apparatus: a claims ledger, a dashboard checker that fails the build when prose disagrees with measurement, prover-version-pinned gates, and rejection fixtures that must fail for the right reason. It is at 60 % / grade D, alpha, with the headline claim still an OPEN ledger row. + +**Audit result.** All sixteen invariants are consistent with what the code actually does; none is contradicted. The three items I am not fully certain about are stated as uncertainties rather than resolved by inference: the `hexad` feed in an octad estate (§1), whether `resource-algebra`'s "echo loss grade" is `echo-types`' echo (§2, §13), and whether `report-format = "logtalk"` is a live enum or dead config (§11). + +**Where the drift actually is.** Not in the structural model — in januskey's own published surfaces, which over-claim against januskey's own instruments: a wiki that asserts GDPR Article 17 "with mathematical certainty", a security doc advertising an ECC implementation that is refused at the CLI, a CLI banner claiming "provably reversible" over an OPEN row, a receipts file describing a directory tree that no longer exists, and three different `unwrap()` counts. That is the same failure mode this repo was built to detect, one layer up from the code. + +**Next, in this repo, in order:** (1) ~~the three over-claims D1–D3~~ — **done, see §4.1**; (2) the stale surfaces D4–D8; (3) T-8 — point `MetadataStore::save` at the already-tested atomic path — because it is the one open ledger row that a second implementor (valence-shell, ochrance) would inherit; (4) reword the two sibling "pattern" citations so a citation cannot be read as a dependency. + +**Cross-repo posture.** One hard proof dependency (`resource-algebra`), one intended verifier (`ochrance`), one intended consumer (`valence-shell`), one inert data feed (`VeriSimDB`), one blocked cartridge (`boj-server`). Everything else in the invariant list is a sibling I read about and do not depend on — which is, on this evidence, the correct relationship. + +--- + +## Addendum — same day, later, on this branch + +The body above is left as the record of what was true when it was measured. +Two things changed afterwards. + +**T-8 is attempted, and still OPEN.** `MetadataStore::save` +(`crates/reversible-core/src/metadata.rs`) now calls +`crate::transaction::write_atomic`, the write → sync → rename path that +`transaction.rs` already used and that T-5 already tests; `write_atomic` became +`pub(crate)` for the purpose, so nothing moved out of `transaction.rs` and no +T-5 test changed. A new test, +`metadata::tests::save_replaces_the_log_atomically`, asserts that a save leaves +no temporary file behind, ignores a torn one planted from an earlier crash, and +that the log parses on reopen. The ledger row stays **OPEN**: no toolchain in +this session built or ran the test, so the evidence is "written" and not +"observed". The retry half of the row — an undo whose `mark_undone` fails to +persist — is untouched. Declared test count moves 135 → 136 in `STATE.a2ml`, +`READINESS.adoc` and `TOPOLOGY.adoc`, which is the figure `dashboard-check` +measures with `cargo test -- --list`. + +**The proof claims are now graded, and the grade is Grade 3 for four rows.** +`docs/theory/PROOF-GRADES.adoc` maps the 47-row ledger onto +`hyperpolymath/mathesis` §5/§6 and `hyperpolymath/standards` +`3-practice/PROOF-POLICY.adoc` §1/§2. The result is not a relabel: of the 11 +PROVEN rows, the four whose artefact is Agda (G-1, T-1, T-2, T-3) type-check +in Agda and have not been translated to another foundational system, which is +mathesis's definition of Grade 3. The receipt is a green `agda-proofs.yml` run +(40867211509) at commit `4afb710` with Agda 2.6.4.3 and `resource-algebra` +pinned at `cf9235c`; the modules, the sibling fetch and the workflow are +byte-identical at that commit and here. The gate script is not: it gained +`--cubical-compatible` after the receipt. The other seven PROVEN +rows are Idris2 interface/ABI theorems, which PROOF-POLICY §1 classifies as +engineering rather than theory, so the grade ladder does not apply to them. +Nothing is claimed at Grade 2i, 2ii or 1. Two obligations are recorded rather +than skipped: the canonical invocation's `--cubical-compatible` is absent +because the flag is infectious and the pinned sibling is `--without-K`; and CI +pins Agda twice, at 2.6.4.3 (the receipt) and 2.6.3 (the dashboard job). + +**Toolchains, and what that changed.** The sandbox's egress allowlist decides +which prover can be run at all. Measured, with the exact failures, in +`docs/estate/environment-toolchains.md`: Agda (2.6.4.3, the CI pin) and Zig +(0.13.0, the e2e pin) install from PyPI wheels and both gates now run here — +`check-agda.sh` green, `ffi/zig` building with 15/15 integration tests passing — +while Rust, Creusot and Idris2 cannot be installed, because +`static.rust-lang.org`, `crates.io`, `deb.debian.org` and the GitHub release-asset +host are all outside the allowlist. Idris2 is anyway already pinned at its latest +release (v0.8.0). Running the Agda gate locally is what turned the §2.1 question +from an inference into a measurement: the canonical invocation +(`--safe --without-K --cubical-compatible`) type-checks both modules, so the gate +now uses it and the earlier prediction that it would fail on the pinned +`--without-K` sibling is withdrawn. + +**Out-of-scope findings, written as separate prompts.** Four, in +`docs/estate/prompts/`, one per repository, none of them touching januskey: +`standards` (four gaps in PROOF-POLICY §2.1/§2.2 that implementing it exposed), +`mathesis` (whether a Grade 3 receipt may be local, how to record non-axiom +caveats, what a checker change does to an existing grade), `resource-algebra` +(the OPEN homomorphism that blocks row G-3, plus `--cubical-compatible` in its +pragmas), and `the-metadatastician` (whether it ingests A2ML manifests — the +question behind ledger row V-2). Two of the three repositories named in the +request do not resolve: `hyperpolymath/stuff-of-awesome` and +`hyperpolymath/catachresis-colloquium` both return 404 to an authenticated +`gh api`, and neither name appears among the owner's 360 public repositories; the +nearest match for the third is `the-metadatastician`. No prompt was written for a +repository that could not be found and read. + +**The epistemic inheritance is rewritten, not relabelled.** The Idris `Knows` +modality (§5.6 below) could not state either of the two obligations attributed +to it, so it has been replaced on the theory side rather than annotated: +`verification/proofs/agda/Epistemic.agda` models knowledge as +indiscriminability over a per-agent observation, which makes ignorance a +proposition to be proved (`adversary-ignorant`), makes obliteration a store +operation with an empty recovery set (`obliterate-cuts-recovery`, +`obliterate-ignorance`) and makes forgetting a Bool-valued statement that is +false after rotation (`rotate-forgets-old`). Two new fixtures pin the refusals. +Ledger row E-1m is `PROVEN` and Grade 3; row E-1 stays `OPEN`, because a model +of channels is not a model of cryptography. The Idris module is unchanged apart +from comments pointing at the Agda record, and it keeps its deleted +`systemForgetsOldKey` — the gap is now visible in two places instead of one. + diff --git a/docs/estate/environment-toolchains.md b/docs/estate/environment-toolchains.md new file mode 100644 index 0000000..f4e7918 --- /dev/null +++ b/docs/estate/environment-toolchains.md @@ -0,0 +1,97 @@ +# Toolchains in the agent sandbox — measured 2026-11-01 + +What can be installed to check this repository's artefacts, what cannot, and the +exact evidence for each. Written because the honest status of a proof row now +depends on which prover could actually be run, and the next session should not +have to rediscover the sandbox's edges. + +Base image: Debian 12 (bookworm), Python 3.11.2, Node present, `gcc`/`g++`/`make` +present, `cmake` absent, user in `sudo` — but `apt` is useless here (see below). + +## What works: a Python venv, and PyPI wheels that ship real binaries + +Nothing may be installed into the repository; every toolchain lives in a venv +under `/tmp`, which is **not persisted** across sessions. The commands below are +the record, not the artefacts. + +```bash +python3 -m venv /tmp/tc +/tmp/tc/bin/pip install "agda==2.6.4.3.post1" "ziglang==0.13.0" +``` + +| Tool | Version installed | Source | Evidence it works | +|---|---|---|---| +| Agda | `Agda version 2.6.4.3-56f5f56` — the same 2.6.4.3 that `agda-proofs.yml` pins | PyPI wheel `agda==2.6.4.3.post1` | `AGDA=/tmp/tc/bin/agda bash scripts/check-agda.sh` → both modules check, four fixtures refused as expected, `[check-agda] OK` | +| Zig | `0.13.0` — the version `e2e.yml` pins | PyPI wheel `ziglang==0.13.0` (binary at `lib/python3.11/site-packages/ziglang/zig`) | `zig build test --summary all` in `ffi/zig` → `3/3 steps succeeded; 15/15 tests passed`; `zig build` also installs `libjanuskey-ffi.a` and `januskey.h` | + +Two caveats worth knowing before trusting the versions: + +* `agda==2.6.4.3` (without `.post1`) is **yanked** and its binary reports + `Agda version 2.6.4.1-14f5317`. Use `.post1`, which reports `2.6.4.3`. +* `agda==2.7.0.1` installs but dies with `The lib directory …/agda/data/lib does + not exist` — the wheel ships without the primitive library. Symlinking + `/tmp/tc/lib/python3.11/site-packages/agda/data` into the 2.7 venv makes it + run; with that, **both modules also type-check under 2.7.0.1** (exit 0). That + is a measured upgrade path, not a recommendation: the CI pin is Debian's + 2.6.4.3 and moving it means a new container, a new pin and a new receipt. + +Zig 0.17.0 (the newest on PyPI) does **not** build this tree: `build.zig` is +0.13-era and fails at `build.zig:10` (`standardTargetOptions` on a +pointer-deref'd `Build`). Upgrading Zig means editing `build.zig`, which is a +separate change with its own evidence. + +## What does not work, and exactly why + +Egress is allowlisted. Reachable: `pypi.org`, `files.pythonhosted.org`, +`registry.npmjs.org`, `github.com`, `api.github.com`, `codeload.github.com`. +Blocked at TLS/connect (measured with `curl`, and again through the tools that +would use them): + +| Blocked host | Needed for | Concrete failure | +|---|---|---| +| `static.rust-lang.org` | rustup toolchain download | `rustup default stable` → `could not download file from 'https://static.rust-lang.org/dist/channel-rust-stable.toml.sha256' … tls handshake eof` | +| `crates.io`, `index.crates.io`, `static.crates.io` | any `cargo build` of this workspace (serde, chrono, uuid, clap, hmac, sha2, argon2, aes-gcm …) | registry unreachable | +| `deb.debian.org` | `apt-get install agda-bin idris2 why3 …` | `apt-get update` → `Connection failed`; no cached debs | +| `release-assets.githubusercontent.com`, `objects.githubusercontent.com`, `raw.githubusercontent.com` | GitHub release binaries (a rustup-init or a prebuilt prover) | connection fails; `curl -L` stops at the 302 | +| `hackage.haskell.org`, `downloads.haskell.org`, `opam.ocaml.org` | GHC (for Idris2 and Agda from source), why3 (for Creusot) | — | + +Consequences for this repository's rows, in the ledger's vocabulary: + +* **Rust behaviour cannot be graded.** `pip install rustup` succeeds and puts + *shims* in `bin/` (`rustc`, `cargo`, `rustfmt` …), but each is a 215-byte + rustup proxy that needs a toolchain it cannot download. Even with a compiler, + the workspace needs the registry. So no `cargo test`, no Clippy, no Creusot. +* **Creusot cannot be installed.** It needs `cargo`, `rustc`, and `why3` (OCaml, + distributed through opam) — three blocked dependencies, not one. +* **Idris2 cannot be installed.** It needs GHC. Note the pinned version in + `.github/workflows/idris-abi.yml` (`idris2-pack@sha256:f0758996…`, Idris2 + 0.8.0) is already the latest release (`v0.8.0`), so nothing on the Idris2 side + is out of date — it simply has to run in CI. +* **Agda and Zig can be graded here.** Both are installable as wheels from + PyPI, at exactly the versions CI pins. + +## To unblock the rest + +The allowlist entries, smallest first: + +1. `static.rust-lang.org` + `index.crates.io` + `static.crates.io` → `rustup + default stable`, `cargo test --workspace --locked`. Creusot also needs `why3` + from step 2 or step 3. +2. `deb.debian.org` → `agda-bin` (2.6.4.3 on trixie, i.e. the pinned prover from + a signed archive rather than a PyPI wheel), `idris2`, `why3`. +3. `opam.ocaml.org` + `hackage.haskell.org` → why3 and GHC from source, if the + Debian route is not wanted. + +With (1) the Rust rows become verifiable — including the T-8 test added on this +branch, which is currently written and unrun. With (2) Idris2 and Creusot +become runnable, which is what PROOF-POLICY §1 asks for on the ABI and on +first-party Rust behaviour respectively. + +## Provenance note, for the receipt discipline + +A PyPI wheel is not the same provenance as a Debian package from a signed +archive, and PROOF-POLICY §2.3 wants receipts that name their prover and its +version. The local runs recorded in `docs/theory/PROOF-GRADES.adoc` therefore +say "PyPI wheel, version string `2.6.4.3-56f5f56`" and are marked as +**reproduction**, not as a replacement for the CI receipt produced by +`agda-proofs.yml` on the pinned Debian package. diff --git a/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md b/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md new file mode 100644 index 0000000..c7c10be --- /dev/null +++ b/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md @@ -0,0 +1,50 @@ +# Paste-ready prompt — `hyperpolymath/mathesis` (`estate-mathematical-architecture`) + +Scope: **this repo only.** Do not edit `januskey`. Latest stable versions only +(Agda 2.8.0.2; Rocq/Lean only if §2's transport work is in scope). + +--- + +Context: I am grading the proof claims of `hyperpolymath/januskey` under §5 and +§6 of `estate-mathematical-architecture`, at HEAD. Four of my eleven `PROVEN` +ledger rows have an Agda artefact and type-check; nothing has been translated. +By §5's sentence they are Grade 3. Three questions about the *receipt*, because +§6 asks for commit hashes and §2.3 of the estate's PROOF-POLICY puts executions +in CI: + +1. **Does a Grade 3 receipt have to come from CI?** §5 says a proof "type-checks + locally in Agda". Taken literally, a local type-check is the grade, and CI is + how the estate records it. I have a green CI run at commit `4afb710` + (`agda-proofs.yml`, Agda 2.6.4.3, pinned sibling `cf9235c`), and separately a + local run of the same modules under the same prover version after I changed + the gate's flag set to PROOF-POLICY §2.1's canonical form. Which is the + receipt for the current bytes — the CI run for the old flags, or the local + run for the new ones, or neither until CI runs again? I am currently claiming + "AGDA-VERIFIED, receipt pending re-run" and would rather use your rule. + +2. **How are non-axiom caveats recorded?** My modules type-check with + `-W[no]UnsupportedIndexedMatch` warnings: clauses that will not compute + under cubical transports. They are not axioms and not holes, so they do not + belong in the axiom list, but they are exactly the kind of caveat a consumer + would want before citing a Grade 3 result as if it were fully computational. + Does §6's axiom tracking have a slot for this, or is a separate line the + convention? + +3. **What happens to a grade when the checker changes but the artefact does + not?** I added `--cubical-compatible` to the gate; the two `.agda` files are + byte-identical before and after. §6 says a grade that stops applying is + marked `Superseded` or `Regressed` — but here nothing was re-proved and + nothing stopped holding; only the invocation was tightened. Is that a new + receipt with the old one superseded, or the same grade with a re-earned + receipt? I have written it as the latter and flagged the difference. + +What I can offer: a real ledger with 47 rows in five statuses, five Grade 3 rows +with an artefact-per-row discipline and expected-rejection fixtures, a page +(`docs/theory/PROOF-GRADES.adoc`) that maps every row onto §1 and §5 and records +what is *not* graded — the seven Idris2 ABI rows, which PROOF-POLICY §1 classes +as engineering rather than theory. If any of that mapping is wrong by your +reading, say which and I will change the page rather than the grade. + +Boundary: I treat §5's sentences as the definition and §6's bullets as the +reporting rules; I have not inferred anything about Grade 2i/2ii beyond the +text, and I claim no translation work. diff --git a/docs/estate/prompts/2026-11-01-resource-algebra-homomorphism.md b/docs/estate/prompts/2026-11-01-resource-algebra-homomorphism.md new file mode 100644 index 0000000..29fa108 --- /dev/null +++ b/docs/estate/prompts/2026-11-01-resource-algebra-homomorphism.md @@ -0,0 +1,45 @@ +# Paste-ready prompt — `hyperpolymath/resource-algebra` + +Scope: **this repo only.** Do not edit `januskey`. Latest stable Agda (2.8.0.2 +at the time of writing) unless you have a pin you would rather keep. + +--- + +Context: I am working in `hyperpolymath/januskey`, which consumes this repo as +its one proof dependency, pinned at `cf9235c532712a783a404c359a1055f40134794a` +(`scripts/fetch-siblings.sh`, one commit per re-pin). The Agda gate imports +`ResourceAlgebra.Prelude`, `.Core` and `.Instances.Loss` and proves over them; +the modules are `verification/proofs/agda/{Reversibility,TransactionAtomicity}.agda` +and they type-check against that pin today (Agda 2.6.4.3, `--safe --without-K`). + +Two things, both small, both measurably *your* side of the boundary: + +1. **The homomorphism obligation is the one blocking my ledger.** Your tree + lists homomorphisms as OPEN; my row G-3 is exactly that statement for the FFI + bridge — that wrapping a grade-𝟙 operation preserves grade 𝟙 across the + Zig/Rust boundary. I am not asking you to prove my bridge. I am asking + whether you will state the obligation in your vocabulary so that I can + consume it by pin, the way I consume `Loss`, instead of restating a + homomorphism-shaped claim in my own tree, which would be the failure mode + your own docs warn about (a dependent re-declaring what its sibling owns). + +2. **`--cubical-compatible` in your module pragmas.** Every module here opens + with `{-# OPTIONS --safe --without-K #-}`. The estate's PROOF-POLICY §2.1 + canonical invocation is `agda --safe --without-K --cubical-compatible`, and I + now run it on my side. It works — Agda accepts a `--without-K` import and + warns instead of failing — but 14 of my warnings come from this repo, the + first being `≤-trans` in `ResourceAlgebra.Prelude` (indexed match on `suc`, + so it will not compute under transports). If you adopt `--cubical-compatible` + in your own pragmas, those warnings go away for every dependent, not just me. + If you would rather not, say so and I will keep the warnings recorded in my + receipt instead of treating them as a defect of yours. + +Evidence you can check without trusting me: my pinned clone is your `cf9235c`; +the warning text and counts are in `docs/theory/PROOF-GRADES.adoc` and +`docs/estate/environment-toolchains.md` in `januskey`, and the gate is +`scripts/check-agda.sh`. + +Boundary: I have read only `src/ResourceAlgebra/{Prelude,Core,Instances/Loss}`, +`docs/AFFIRMATION.adoc` and `PROOF-STATUS.adoc`, and only as a consumer. If the +homomorphism item is already stated somewhere I did not read, point at it and +ignore item 1. diff --git a/docs/estate/prompts/2026-11-01-standards-proof-policy.md b/docs/estate/prompts/2026-11-01-standards-proof-policy.md new file mode 100644 index 0000000..9184d84 --- /dev/null +++ b/docs/estate/prompts/2026-11-01-standards-proof-policy.md @@ -0,0 +1,61 @@ +# Paste-ready prompt — `hyperpolymath/standards` (`3-practice/PROOF-POLICY.adoc`) + +Scope: **this repo only.** Do not edit `januskey`. Pin everything to latest +stable (Agda 2.8.0.2, Idris2 v0.8.0, Zig 0.15.1, Rust latest stable via rustup). + +--- + +Context: I am working in `hyperpolymath/januskey` (branch off `main` @ +`4afb710`). I implemented PROOF-POLICY §2.1 in a real CI gate and hit four +places where the policy does not say what to do. I am not asking for a +relaxation; I am asking for the rule, because I had to invent one and I would +rather cite yours. + +What I measured, with Agda 2.6.4.3 (the version the gate pins), so you can +check each claim rather than take it: + +1. **The canonical invocation runs into the "infectious flag" case.** §2.1 says + `agda --safe --without-K --cubical-compatible `. `--cubical-compatible` + is documented as requiring every directly imported module to use it too. My + modules import a pinned sibling (`resource-algebra@cf9235c`) whose every + module declares `{-# OPTIONS --safe --without-K #-}`. Empirically Agda + *accepts* this: exit 0, with 14 and 16 `-W[no]UnsupportedIndexedMatch` + warnings respectively, naming clauses (the sibling's `≤-trans`, my + `obliterate-absorbs`) that will not compute under transports. So the policy's + canonical form is achievable against a `--without-K` dependency. **Question: + is that the intended reading, and should the policy say so?** As written, a + reader like me inferred the opposite and shipped the weaker invocation for + months. + +2. **Warnings are not covered.** §2.2 lists statuses for *executions*; nothing + says whether a proof that type-checks with warnings may be `AGDA-VERIFIED`, + whether the warning classes must be recorded, or whether `-WnoUnsupportedIndexedMatch` + is an acceptable silencing. I chose: keep them visible, record the classes + and counts in the receipt, and treat them as statements about computation + under transport rather than about the proposition. **Question: keep, ban, or + require per-class justification?** + +3. **Two prover versions in one repository's CI.** One workflow pins 2.6.4.3 + (the real receipt); another installs 2.6.3 from a different base image + because it also needs Idris2. §2.1 says record the version per commit but not + which of two recorded versions is the receipt. **Question: should a repo be + required to have exactly one prover version per prover, and should a checker + run under a different version be marked as a consistency check rather than a + receipt?** + +4. **Provenance of the prover binary.** A sandbox I work in can install Agda + only as a PyPI wheel (`agda==2.6.4.3.post1`, reporting `2.6.4.3-56f5f56`), + not from a signed distro archive. §2.1 says pin and record; §2.3 says CI + receipts establish execution. **Question: is a local run with a wheel-built + prover recordable as anything, and if so under what label — `reproduction`?** + I have used "reproduction, not a receipt" and would rather use your word. + +What I can offer back: the gate itself (`scripts/check-agda.sh`), the +expected-rejection fixtures whose refusal message is asserted (four Agda files +refused with the exact text they exist for), and the recorded receipt with +commit hash, prover version, flags and sibling pin — in +`docs/theory/PROOF-GRADES.adoc`. If you change the policy, that page is a +place where the change is *used*. + +Boundary: I have implemented §1's mapping as written (Rust → Creusot, theory → +Agda, ABI → Idris2) and make no claim to know your intent beyond the text. diff --git a/docs/estate/prompts/2026-11-01-the-metadatastician.md b/docs/estate/prompts/2026-11-01-the-metadatastician.md new file mode 100644 index 0000000..8a67a92 --- /dev/null +++ b/docs/estate/prompts/2026-11-01-the-metadatastician.md @@ -0,0 +1,36 @@ +# Paste-ready prompt — `hyperpolymath/the-metadatastician` + +Scope: **this repo only.** Do not edit `januskey`. Latest stable versions only +(Rust latest stable via rustup; Node/Python whatever your tree already pins). + +--- + +Context: I work in `hyperpolymath/januskey`, a reversible-operation tool that +emits A2ML manifests (`crates/reversible-core/src/manifest.rs`) and maintains a +claims ledger (`PROOF-NEEDS.adoc`) plus a proof-grade page graded against +`mathesis` and the estate's PROOF-POLICY. + +I am writing because your README promises "auditable provenance trails", +"grounded documentation claims" and "release-time evidence checks", and januskey +now has exactly those artefacts in a machine-readable shape: 46 claim rows, five +statuses, per-row artefact and checker command, and a receipt naming commit, +prover version and flags. Two questions, no dependency claimed either way: + +1. **Do you ingest A2ML manifests today, and in what shape?** januskey's + `ManifestEmitter` has never been parsed by anything outside its own tests — + my ledger records that as `DESIGNED`, not as a working integration. If you + already read A2ML, I would like to know which fields you require, so that the + row can be restated at the strength of your parser rather than my emitter. +2. **Would a claims ledger be in scope for your evidence checks?** Concretely: + would you want (a) the ledger as data, (b) the grade page as a narrative, or + (c) nothing until the manifest path is settled? I would rather record "not in + scope" than a designed-but-unbuilt integration. + +Evidence: januskey's `PROOF-NEEDS.adoc`, `docs/theory/PROOF-GRADES.adoc`, +`crates/reversible-core/src/manifest.rs`, and ledger rows V-1..V-3 which record +downstream consumption as `DESIGNED` with the change condition (a dependency +edge in the consumer's manifest plus a green test there). + +Boundary: I have read only your `README.adoc` and file listing; I have not read +your implementation, so I make no claim about what it does. If any of the above +misreads your scope, correct it — that is more useful to me than a yes. diff --git a/docs/security/KEY_LIFECYCLE.adoc b/docs/security/KEY_LIFECYCLE.adoc index f3558c2..ff6690f 100644 --- a/docs/security/KEY_LIFECYCLE.adoc +++ b/docs/security/KEY_LIFECYCLE.adoc @@ -7,11 +7,29 @@ :sectnums: :icons: font +== Scope — read this first + +This document describes the key store in `crates/januskey-cli/src/keys.rs`, built as +the `jk-keys` binary. **It is not part of JanusKey's identity and is not on the `jk` +reversibility path.** There is no call edge in either direction between the two, the +binary is behind the opt-in `key-lifecycle` feature so a default build produces `jk` +only, and the module is scheduled to move out of this repository +(`link:../../docs/adr/0001-identity-and-scope.md[ADR-0001]`). + +**Accuracy note.** Everything below is a *specification*. The implemented `jk-keys` +subcommands are `init, list, generate, show, rotate, revoke, backup, status, audit, +export, verify, history`. Examples that use `restore`, `recover`, +`obliterate` or `verify-obliteration` describe behaviour that does not exist in the +CLI yet; they are marked where they appear. + == Overview -This document specifies the complete lifecycle for cryptographic keys managed by JanusKey, -from generation through destruction. Following MPR principles, key lifecycle transitions -are enforced through type-state patterns, making invalid state transitions impossible. +This document specifies the lifecycle for the keys held in that store, from generation +through destruction. The type-state discipline it describes is the design intent: the +implemented state machine is the `KeyState` sum +(`Generated, Active, Rotating, Suspended, Revoked, Obliterated`), which makes an +unenumerated state unrepresentable but does not by itself forbid every invalid +transition. == Key Hierarchy @@ -461,18 +479,30 @@ fn obliterate_key(key_id: Uuid) -> Result { === Destruction CLI +Implemented: + [source,bash] ---- # Revoke a key (retain for audit) jk-keys revoke --key-id --reason "scheduled rotation" -# Obliterate a key (GDPR erasure) -jk-keys obliterate --key-id --confirm -# Output: Obliteration proof (for compliance records) +# Inspect the audit log +jk-keys audit +jk-keys verify +---- + +Specified but **not implemented** in the CLI (the library has +`KeyManager::retrieve`, and `KeyState::Obliterated` exists, but no command reaches +either): -# Verify obliteration proof -jk-keys verify-obliteration --proof +[source,bash] ---- +jk-keys obliterate --key-id --confirm # not implemented +jk-keys verify-obliteration --proof # not implemented +---- + +Note that key destruction is not an erasure claim about anything outside the store: +the same caveat as `jk obliterate` applies (`../wiki/theory/rmo-primitive.md`). == Audit Trail diff --git a/docs/security/THREAT_MODEL.adoc b/docs/security/THREAT_MODEL.adoc index bcd7079..bd6dd26 100644 --- a/docs/security/THREAT_MODEL.adoc +++ b/docs/security/THREAT_MODEL.adoc @@ -10,8 +10,10 @@ == Executive Summary This document defines the threat model for JanusKey's cryptographic key management subsystem. -Following the **Maximal Principle Reduction (MPR)** methodology, security guarantees are achieved -through architectural design rather than operational procedures. +It is written under the **Maximal Principle Reduction (MPR)** design philosophy — eliminate a +vulnerability by removing the code path that would create it, rather than by procedure. MPR is +design vocabulary in this repository, not a formal method, and no security guarantee below has +been mechanically proved (`PROOF-NEEDS.adoc` §Claims ledger). == Scope @@ -235,6 +237,10 @@ Residual Risk:: LOW - Reversibility enables recovery == Cryptographic Primitives +What is in the tree, as opposed to what is planned. Two rows here were +previously written as if the planned algorithm were present; both are now +marked. + [cols="2,2,2"] |=== | Purpose | Algorithm | Rationale @@ -248,12 +254,12 @@ Residual Risk:: LOW - Reversibility enables recovery | Memory-hard, resistant to GPU/ASIC attacks | Asymmetric Keys -| Ed25519 / X25519 -| Modern elliptic curves, constant-time, compact +| **Not implemented** (Ed25519 / X25519 exist as enum variants only) +| `KeyAlgorithm::Ed25519` / `X25519` are retained so historical serialized metadata deserializes; `jk-keys generate --type ed25519` and `--type x25519` are refused (no dalek dependency, no keypair is produced) | Hashing -| SHA-256, BLAKE3 -| SHA-256 for compatibility, BLAKE3 for performance +| SHA-256 +| The only hash in the tree. BLAKE3 is **not** a dependency; it is mentioned in `ARCHITECTURE.adoc` only as what ochrance is believed to use, which is unresolved | Random Generation | OS CSPRNG @@ -278,27 +284,37 @@ Residual Risk:: LOW - Reversibility enables recovery == Compliance Mapping -[cols="1,2,2"] +This table maps *design intent* to published requirements. It is not a +certification, an attestation, or a statement of compliance: no assessment has +been performed by anyone, and several rows describe mechanisms that cover only +part of the requirement named. Read the third column as "what exists", not as +"what is satisfied". + +[cols="1,2,3"] |=== -| Standard | Requirement | JanusKey Implementation +| Standard | Requirement | What exists in this repository | NIST SP 800-57 | Key lengths appropriate for security strength -| 256-bit symmetric, 256-bit ECC +| 256-bit symmetric only (AES-256). No asymmetric algorithm is implemented: Ed25519 and X25519 are enum variants that the CLI refuses to generate | NIST SP 800-132 | Password-based key derivation -| Argon2id with recommended parameters +| Argon2id, 64 MiB / 3 iterations / 4 lanes / 16-byte salt, as literals in `keys.rs`. OWASP-recommended values; not a maintained policy and not checked against a published revision | GDPR Article 32 | Appropriate technical measures -| Encryption at rest, access controls +| Key *material* wrapped with AES-256-GCM (per-key nonce, key UUID as AAD); key store protected by file permissions. The content store itself is **not** encrypted. Whether these measures are "appropriate" is a controller-level determination, not one this repository can make | SOC 2 | Logical access controls -| File permissions, key encryption +| File permissions and key-store encryption. No SOC 2 audit has been performed, and no control has been mapped to a TSC criterion |=== +Related: `docs/wiki/theory/rmo-primitive.md` records that obliteration is an +engineering primitive, not an erasure guarantee, and that no GDPR Article 17 +determination follows from it. + == References * NIST SP 800-57: Recommendation for Key Management diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc new file mode 100644 index 0000000..6fed117 --- /dev/null +++ b/docs/theory/PROOF-GRADES.adoc @@ -0,0 +1,347 @@ += Proof grades under mathesis and PROOF-POLICY +:toc: preamble +:icons: font + +This page grades januskey's proof claims in the vocabulary its owner's estate +mathematics architecture uses, and records the receipt for every grade. It is +the answer to a single question a reader of `PROOF-NEEDS.adoc` should not have +to reconstruct: *which of these claims is a proof, and how good a proof is it?* + +It grades nothing by confidence. There is no percentage anywhere in this +repository, and none is introduced here. + +== What governs the grades + +Two owner documents, both read at HEAD on 2026-11-01: + +[cols="1,2,3",options="header"] +|=== +| Source | Section | Rule taken from it + +| `hyperpolymath/mathesis`, + file `estate-mathematical-architecture` +| §5 grades +| **Grade 3** — "a proof is Grade 3 if it type-checks locally in Agda but has + not been translated to an independent foundational system". Grade 2i adds one + translation, Grade 2ii two *foundationally distinct* ones (Agda, Rocq and + Lean are all dependent type theory, so 2ii needs Isabelle/HOL), Grade 1 is a + check served to headless CI tooling (AXLE, isabelle server, coq-lsp REST). + +| mathesis, same file +| §6 reporting +| No percentage; every axiom the development relies on is tracked; a grade + receipt records the **commit hash** it was produced at; a grade that stops + applying is marked `Superseded` or `Regressed`, never quietly deleted. + +| `hyperpolymath/standards`, + `3-practice/PROOF-POLICY.adoc` +| §1 mapping +| Theory is proved in **Agda** and rechecked in Rocq and Lean; the behaviour of + first-party Rust is **Creusot** on that code; API, ABI and wire-format + contracts are **Idris2**. The earlier "Rust always means Rust/SPARK" note is + withdrawn (owner ruling 2026-04-10): Rust is Creusot. + +| PROOF-POLICY +| §2.1 invocation +| `agda --safe --without-K --cubical-compatible `; pin and record + the Agda version and the library set per commit; a missing tool is an open + obligation, never a silent skip. + +| PROOF-POLICY +| §2.3 execution +| The policy text records policy; CI receipts establish the executions. §2.2's + statuses (`AGDA-PENDING`, `AGDA-VERIFIED`, `COQ-CHECKED`, `LEAN-CHECKED`, + `BRIDGE-PENDING`, `RECONCILED`, `COUNTEREXAMPLE`, `QUARANTINED`) name what + happened to one proposition. +|=== + +januskey's own five-status ledger vocabulary (`PROVEN`, `TESTED`, `ASSUMED`, +`DESIGNED`, `OPEN`) is the estate's claim vocabulary and is unchanged by any of +this. A grade is a second axis laid over it, not a replacement: a row is +`PROVEN` *because* a named artefact checks it, and separately has (or has not) a +mathesis grade. + +== The Grade 3 receipt + +The theory artefacts are two Agda modules: + +* `verification/proofs/agda/Reversibility.agda` — the Loss grade algebra: + lossless traces have only lossless steps, obliteration absorbs, and a + wrap/unwrap pair with a cancellation premise is a grade-𝟙 two-step trace. +* `verification/proofs/agda/TransactionAtomicity.agda` — rollback restores the + state the transaction began in; the `TransactionManager` lifecycle keeps its + log invariant under begin, add_operation, commit and mark_rolled_back, and at + most one transaction is Active. + +Both are checked by `scripts/check-agda.sh` (`just test-agda`), which is also +the ledger's recorded checker for rows G-1, T-1, T-2 and T-3. The receipt: + +[cols="1,3",options="header"] +|=== +| Field | Value + +| Workflow, run | `agda-proofs.yml`, run + https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509], + branch `main`, conclusion **success** +| Commit | `4afb710e86646658f667f10bd6274ee47416bfc7` (started 2026-10-29T11:40:36Z) +| Prover | `agda-bin=2.6.4.3-1+b2` on Debian trixie-slim + (`@sha256:a29215f6…`), asserted by a passing step: + `test "$(agda --version)" = 'Agda version 2.6.4.3'` +| Flags | `--safe --without-K --no-libraries --ignore-interfaces --double-check` + at the receipt commit; the gate now runs PROOF-POLICY §2.1's canonical form + with `--cubical-compatible` added (see §The §2.1 invocation below) +| Sibling | `resource-algebra` at + `cf9235c532712a783a404c359a1055f40134794a`, fetched by + `scripts/fetch-siblings.sh`; consumed by pin, not re-declared here +| Result | The two modules in this receipt type-check; the fixtures under + `tests/reject-agda/` are refused *with the message each fixture names*, so a + fixture that starts passing, or starts failing for the wrong reason, fails the + gate +| Transfer | `Reversibility.agda`, `TransactionAtomicity.agda`, + `scripts/fetch-siblings.sh` and `agda-proofs.yml` are byte-identical at that + commit and at this branch's HEAD (blobs `0d30206…`, `38c9b06…`, `9b66a48…`, + `7c7e653…`), so the receipt covers those two rows as they stand. It does + **not** cover `Epistemic.agda` (new) or the changed `check-agda.sh`: their + first CI evidence is the run on this branch's pull request +|=== + +That is a Grade 3 receipt in mathesis terms: the propositions type-check in +Agda, in CI, at a named commit, with the prover version pinned and recorded. +mathesis §5 illustrates "strict solver flags" with `--safe --erasure`; +januskey's strictness is `--safe --without-K` plus `--double-check`, which is +the same family and stricter than bare `--safe` (no K, no trusted compiled +interfaces, a second checking pass). +Nothing here has been translated to Rocq, Lean or Isabelle, so it is not +Grade 2i, and no headless proof service is involved, so it is not Grade 1. + +=== Why it stops at Grade 3 + +Grade 2i and above would require an Agda → Dedukti → Rocq/Lean transport or a +re-proof, with the outcome recorded as `transported`, `re-proved` or +`unavailable` (PROOF-POLICY §2). That work has not been done, is not claimed, +and would not change what these modules prove: §2.2 is explicit that compiling +in a second prover does not establish the same proposition unless the +correspondence is checked too. + +== The §2.1 invocation: adopted, and measured (2026-11-01) + +PROOF-POLICY §2.1's canonical form is +`agda --safe --without-K --cubical-compatible `. Until this branch +the gate ran `--safe --without-K --no-libraries --ignore-interfaces +--double-check` without the cubical flag, and an earlier revision of this page +predicted that adding it would fail, because the flag is *infectious* (direct +imports must use it too) and every module of the pinned sibling opens with +`{-# OPTIONS --safe --without-K #-}`. + +**That prediction was wrong and is withdrawn.** With Agda 2.6.4.3 installed in +the sandbox (PyPI wheel `agda==2.6.4.3.post1`, reporting +`Agda version 2.6.4.3-56f5f56`, the same version CI pins), the canonical +invocation type-checks both modules: + +[source,text] +---- +$ agda --safe --without-K --cubical-compatible --no-libraries \ + --ignore-interfaces --double-check \ + -i verification/proofs/agda -i _build/dependencies/resource-algebra/src \ + verification/proofs/agda/Reversibility.agda + → exit 0, 14 × warning: -W[no]UnsupportedIndexedMatch + +$ … verification/proofs/agda/TransactionAtomicity.agda + → exit 0, 16 × warning: -W[no]UnsupportedIndexedMatch + +$ AGDA=/tmp/tc/bin/agda bash scripts/check-agda.sh + → [PASS] refused as expected: tests/reject-agda/{CommitWhenIdle,ForwardRollback,HiddenLoss,ReviveAfterObliterate} + → [check-agda] OK +---- + +Agda warns where the earlier reading expected it to refuse: a `--without-K` +import is accepted, and what it reports is that particular clauses — the +sibling's `≤-trans`, and `obliterate-absorbs` here — will not compute when +applied to cubical transports. That is a statement about computation under +transport, not about the propositions these modules prove, so the gate keeps the +warnings visible rather than silencing them with `-WnoUnsupportedIndexedMatch`. + +`scripts/check-agda.sh` now runs the canonical invocation, so januskey matches +§2.1 exactly and is still stricter in two other respects (`--ignore-interfaces` +re-checks the sibling from source instead of trusting compiled interfaces; +`--double-check` re-verifies the type-checker's own work). + +=== Receipt bookkeeping for that change + +The CI receipt in the table above was produced **before** the flag changed. +Changing a graded artefact's checker invalidates its receipt's exactness, so: + +* the local run above is recorded as **reproduction** — same prover version, + PyPI provenance instead of Debian, and no CI provenance at all (PROOF-POLICY + §2.3: receipts of execution come from CI); +* the next `agda-proofs.yml` run on `main` is the new receipt, and this page + must cite it in place of the local run once it exists. Until then the rows + stay `AGDA-VERIFIED` on the strength of the four artefacts being unchanged + plus a matching local run, and that is the strongest claim available. + +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. + +=== Upgrade path, measured + +`agda==2.7.0.1` runs in the sandbox once its wheel's missing `data/lib` is +supplied (bare install dies with "The lib directory … does not exist"), and +under 2.7.0.1 **both modules also type-check, exit 0**. The latest upstream +release is 2.8.0.2 (2026-09-13), which has not been tried. None of this is a +recommendation to move: the CI pin is Debian trixie's 2.6.4.3, and an upgrade +means a new container, a new pin and a new receipt. + +The sandbox's installable set, and the exact hosts that block Rust, Creusot and +Idris2, are recorded in `docs/estate/environment-toolchains.md`. + +== Grades, ledger row by ledger row + +The 47 ledger rows fall into three classes under PROOF-POLICY §1. Counts are +from `PROOF-NEEDS.adoc` at this commit and are `PROVEN` 12, `TESTED` 23, +`ASSUMED` 4, `DESIGNED` 3, `OPEN` 5. + +=== Grade 3 — theory, proved in Agda + +[cols="1,3,2",options="header"] +|=== +| Row | Proposition | Theorem + +| G-1 | A lossless trace has only lossless steps; an obliterating step absorbs; + wrap/unwrap is grade 𝟙 given cancellation | `Reversibility.agda::lossless-trace-all`, + `obliterate-absorbs`, `wrap-unwrap-id` +| T-1 | Undoing a fully executed transaction in reverse order restores the state + it began in, given each step's undo restores its execute | + `TransactionAtomicity.agda::rollback-restores` +| T-2 | The four lifecycle transitions preserve the log invariant and rewrite + only the Active transaction | `TransactionAtomicity.agda::lifecycle-preserves-good` +| T-3 | At most one transaction is Active, exactly one when the pointer is set | + `TransactionAtomicity.agda::at-most-one-active` +| 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 + leaves no agent — the system included — able to use the old key | + `Epistemic.agda::adversary-ignorant`, `obliterate-cuts-recovery`, + `obliterate-ignorance`, `rotate-forgets-old` +|=== + +These five are the only rows in this repository with a mathesis grade. Each +rests on a premise it names rather than assumes silently — the per-step +cancellation law (`undoes`, TESTED as `execute_then_undo_is_identity`), the +freshness of the transaction id (T-7, `ASSUMED`, probabilistic), the absence of +I/O, and, for E-1m, that the modelled channels are the only ones an attacker +has (X-1). §6 asks for the axioms to be tracked; they are, in the modules' +own "What is NOT claimed" blocks and in the ledger's T-6, T-7, G-2, X-1 rows. + +=== Engineering contracts — no mathesis grade applies + +Seven `PROVEN` rows are Idris2 theorems about this ABI: A-1, A-2, C-1, C-2, +C-3, C-4, C-5, checked by +`idris2 --typecheck src/abi/januskey-abi.ipkg`. Under PROOF-POLICY §1 these +are interface and wire-format contracts, so the theory ladder does not grade +them — they are `PROVEN` in the ledger's own vocabulary and that is the whole +of the claim. The `Rust/SPARK` shorthand is withdrawn; the mapping that +replaces it is Rust → **Creusot**, Ada → SPARK, API/ABI → Idris2, theory → +Agda. + +The same heading covers every `TESTED` row (23): a test proves behaviour was +observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) is +`ASSUMED` by transcription and would have to become mechanical before any +"every operation is reversible" theorem could cite both halves. + +=== Not graded, and what would grade them + +[cols="1,2,3",options="header"] +|=== +| Rows | Today | What moves them + +| E-1 (`OPEN`) — the cryptographic claim that an attacker cannot recover + obliterated content or use a revoked key +| Its model-level shadow is proved as E-1m, and the row stays OPEN because a + model of channels is not a statement about cryptography. +| Nothing in Agda: recovering from ciphertext is the assumption X-1. Only a + different kind of evidence (a cryptanalysis, or a reduction) would move it, and + this repository would record that as an external assumption with its source. + +| `TESTED` rows describing Rust behaviour (T-4, T-5, the property tests) +| Claimed, tested. No Creusot annotation exists and Creusot is not installed in + the session that wrote this file. +| Creusot contracts on the Rust functions, run in CI: PROOF-POLICY §1 sends + first-party Rust behaviour to Creusot, not to Idris2 and not to Agda. + +| T-6, T-7, X-1, G-2, E-1, G-3 (`ASSUMED` / `OPEN`) +| Premises, external assumptions, or filed obligations. +| Each names its own gap in `PROOF-NEEDS.adoc`; none may be counted as proved + by the grade of a neighbouring row (README-EXPLAINME: "a row is only as + strong as its weakest step"). + +| V-1, V-2, V-3 (`DESIGNED`) +| Downstream consumption designed, never exercised. +| A dependency edge in the consumer's manifest and a green test there. + +| T-8 (`OPEN`) +| The metadata log now saves through the same write → sync → rename path as the + transaction log, but the crate has not been built since that change. +| The new test `metadata::tests::save_replaces_the_log_atomically` green in CI. + Its half of the row — retry after a failed `mark_undone` — is untouched. +|=== + +== The epistemic rewrite: E-1 becomes E-1m + +The one claim with an inheritance, rather than an invention, behind it. januskey's +Idris2 ABI carries `Knows : Agent → Type → Type` (`Types.idr` §Level 12), a +discrete epistemic modality inherited from the estate's epistemic-types work. It +could not state the security claims the ledger attributed to it: + +* `Knows Adversary a` is uninhabited **by construction** — there is no Adversary + constructor — so "an attacker cannot recover …" (E-1) was a property of a + datatype. The repository's own comment says as much: "a property of this + model, not a security proof". +* "The system forgets the old key" was **unstateable**, because `Knows` has no + negative form. The lemma was deleted rather than repaired, and the ledger + records the deletion. + +`verification/proofs/agda/Epistemic.agda` replaces the modality with one whose +ignorance is a proposition. Knowledge is indiscriminability over an observation +— an agent knows φ in *x* when φ holds in every world it cannot tell apart from +*x* — so: + +* ignorance is `¬ Knows`, proved by exhibiting a world that looks the same and is + not (`adversary-ignorant`, over two worlds that differ only in the store); +* obliteration is a change to the store channel, and recovery is a `Σ` that + becomes empty (`obliterate-cuts-recovery`), with the adversary's ignorance + surviving the operation because its observation did not change + (`obliterate-ignorance`); +* rotation is an update to a `usable` predicate, so "no agent can use the old + key" is a theorem with a Bool on the right (`rotate-forgets-old`), and the + deleted Idris lemma now has a proved counterpart. + +Two fixtures pin the refusals: `AdversaryKnows.agda` (asserting the two stores +are identical — refused, `2 != 1`) and `OldKeyStillUsable.agda` (asserting the +old key survives rotation — refused, `!= true`). + +What this does **not** do is move E-1. A model of channels is not a model of +cryptography: that the store channel is the only one an attacker has, and that a +key which is not `usable` cannot decrypt, are assumptions (X-1), and E-1 stays +`OPEN`. The Idris module is unchanged — its typecheck status, its deleted lemma +and its comments now pointing here — because the theory belongs in Agda under +PROOF-POLICY §1 and the ABI belongs in Idris2. + +== Reporting rules this repository follows + +* No percentage, ever. Where a "completion" figure exists elsewhere in the + tree it is a project-plan measure, not a proof measure, and it is not a grade. +* Every grade names its receipt: commit, prover, prover version, flags, + sibling pin. The receipt above is the only one of its kind here. +* A receipt is invalidated by a change to a graded artefact, to its checker or + to its pin, and is then re-earned by the next run, not carried forward. The + blob comparison in §The Grade 3 receipt exists precisely to show which + changes do and do not invalidate it. +* When a graded artefact is replaced, the grade is marked `Superseded`; when a + green receipt goes red and is not immediately fixed, `Regressed`. Neither is + deleted from the history. +* `AGDA-PENDING` is the correct status for a module committed but not yet + checked. No row in this repository is in that state today: the four graded + rows are `AGDA-VERIFIED` at the commit above. diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md index 88dadde..244bcd0 100644 --- a/docs/wiki/Home.md +++ b/docs/wiki/Home.md @@ -5,7 +5,7 @@ ## Welcome to JanusKey -JanusKey is a reversible file operations utility (formal proofs pending) that pursues complete reversibility through architectural design rather than logging or backups. Unlike traditional backup systems that restore from external state, JanusKey operations carry sufficient information for inversion — the goal is to make data loss architecturally impossible. 30 Idris2 ABI proofs are landed; the reversibility theorems themselves are a target, not yet complete. +JanusKey is a reversible file operations utility (formal proofs pending) that pursues complete reversibility through architectural design rather than logging or backups. Unlike traditional backup systems that restore from external state, JanusKey operations carry sufficient information for inversion — the goal is to make data loss architecturally impossible. The Idris2 ABI typechecks and 11 ledger rows are PROVEN — ABI, grade and transaction-model lemmas, not the security obligations; the reversibility theorem itself is an OPEN row (`PROOF-NEEDS.adoc`). ### Project Status (2026-06-12) diff --git a/docs/wiki/architecture/index.md b/docs/wiki/architecture/index.md index 733ed9f..87f70ca 100644 --- a/docs/wiki/architecture/index.md +++ b/docs/wiki/architecture/index.md @@ -45,7 +45,7 @@ The CLI provides the user interface for JanusKey operations: ``` rust #[derive(Parser)] #[command(name = "jk")] -#[command(about = "JanusKey: Provably Reversible File Operations")] +#[command(about = "JanusKey: reversible file operations with inversion metadata")] struct Cli { #[command(subcommand)] command: Commands, diff --git a/docs/wiki/theory/formal-model.md b/docs/wiki/theory/formal-model.md index 27c1a3a..615accf 100644 --- a/docs/wiki/theory/formal-model.md +++ b/docs/wiki/theory/formal-model.md @@ -5,7 +5,12 @@ ## Introduction -This document defines the formal model underlying JanusKey’s reversibility guarantees. We establish mathematical definitions for file system state, operations, and the conditions for reversibility. +This document defines the formal model that JanusKey's reversibility claims are +stated over: file-system state, operations, and the conditions under which a +composition of them is reversible. Writing a model down is not proving anything +about the implementation; where a lemma in it is checked, the corresponding +ledger row in `PROOF-NEEDS.adoc` says so, and where the model and the Rust are +only related by reading, the row is marked ASSUMED (G-2). ## Definitions diff --git a/docs/wiki/theory/index.md b/docs/wiki/theory/index.md index 6054a36..464c228 100644 --- a/docs/wiki/theory/index.md +++ b/docs/wiki/theory/index.md @@ -5,7 +5,13 @@ ## Overview -JanusKey’s design is grounded in rigorous theoretical foundations that provide mathematical guarantees for reversibility. This section covers the core concepts that make JanusKey’s guarantees possible. +JanusKey's design is stated over a formal model — file-system states, operations +and their inverses — and part of that model is checked by machine. The pages here +describe the intended theory and, in each case, how much of it is actually +discharged: three transaction lemmas are proved in Agda, the ABI lemmas are proved +in Idris2, and the claims that would matter most (that every operation is +reversible, that the model corresponds to the Rust) are OPEN and ASSUMED +respectively. `PROOF-NEEDS.adoc` is the authority. ### Contents @@ -29,12 +35,16 @@ The foundational principle underlying JanusKey is **Maximal Principle Reduction ### Traditional vs MPR Approach -| Aspect | Traditional | MPR | -|--------------|-----------------------------|------------------------------| -| Data safety | Achieved through backups | Impossible to lose by design | -| Verification | Post-hoc testing | Compile-time guarantees | -| Trust model | Trust operational processes | Trust mathematical proofs | -| Failure mode | Graceful degradation | No degradation possible | +| Aspect | Traditional | MPR (as intended) | +|--------------|-----------------------------|--------------------------------------| +| Data safety | Achieved through backups | No code path destroys the inverse | +| Verification | Post-hoc testing | Design review; proofs where they exist | +| Trust model | Trust operational processes | Trust the record, and the proof where one is discharged | +| Failure mode | Graceful degradation | Not applicable — this is a CLI, and it can lose the store | + +Read MPR as a design philosophy, not a method with tooling: the repository says so +itself (`README.adoc` §Known scope boundaries) and no proof in this tree is linked +to the Rust by machine (ledger row G-2 is ASSUMED). ## The MAA Framework diff --git a/docs/wiki/theory/maa-framework.md b/docs/wiki/theory/maa-framework.md index 0e20a9b..d0b2332 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -11,7 +11,15 @@ The MAA Framework is an ethical and engineering paradigm that structurally balan 2. **User Autonomy/Privacy**: Users must have verifiable control over their data, including deletion -These requirements are often in tension. MAA resolves this through formal primitives that provide mathematical guarantees for both. +These requirements are often in tension. MAA proposes a pair of primitives that +address both sides — one reversible, one obliterative. + +> **Status.** MAA is a design framework, not a verified theory. RMR and RMO are +> described below at the strength the code supports: RMR's transactional model +> has three proved lemmas and an open obligation for "every operation is +> reversible"; RMO is an engineering primitive that destroys data and records +> that it did, with no proof that the data is unrecoverable. The claims ledger in +> `PROOF-NEEDS.adoc` is the authority for both. ## The Problem Statement @@ -62,7 +70,7 @@ MAA introduces two formally verified primitives that satisfy both requirements: ### RMR (Reversible Transaction) -> A primitive for state transitions that guarantees instant, mathematically certain rollback to a prior safe state via Algorithmic Reversibility. +> A primitive for state transitions that records, before each change, what is needed to undo it — so that undo is a metadata lookup rather than a restore from backup. Whether every operation is *in fact* reversible is an open obligation, not a guarantee; see the claims ledger. RMR provides: @@ -78,17 +86,23 @@ See: [RMR Primitive Specification](rmr-primitive.md) ### RMO (Obliterative Wipe) -> A primitive for data erasure that achieves Formal Obliteration, proving the non-existence of specified data traces. +> A primitive for data erasure: best-effort overwrite, removal, store scrub, and a tamper-evident record of what was destroyed. RMO provides: -- Cryptographically verifiable deletion +- An overwrite-then-unlink operation, plus scrubbing of the unshared + content-store blobs and operation-log entries for the path -- Proof of non-existence +- A timestamped commitment (`H(content_hash ‖ nonce ‖ timestamp)`) recording + what was claimed destroyed — reviewable, not independently verifiable from + outside the store -- Compliance with right-to-erasure +- A deletion path with no inverse: after RMO there is nothing for undo to restore -- User autonomy with mathematical guarantees +- An honest boundary: no proof of non-existence, no physical-erasure guarantee + on SSD/CoW/journaled media, and no compliance determination. See + [RMO Primitive Specification](rmo-primitive.md) §"Status, in the + claims-ledger vocabulary". See: [RMO Primitive Specification](rmo-primitive.md) @@ -190,16 +204,21 @@ pub fn obliterate(content_hash: &ContentHash) -> Result { } ``` -## Compliance Mapping +## Requirements Mapping (not a compliance claim) + +This table says which primitive is *relevant* to each requirement. It is not a +statement that any of them is satisfied: compliance is a determination for the +controller, on the facts of a deployment, and no assessment of JanusKey has been +performed. -| Regulation | Requirement | MAA Component | -|-------------------|-----------------------|-----------------------------| -| GDPR Art. 17 | Right to erasure | RMO primitive | -| GDPR Art. 5(1)(e) | Storage limitation | RMO with retention policies | -| GDPR Art. 30 | Records of processing | RMR audit trail | -| SOX Section 802 | Record retention | RMR full history | -| HIPAA | Audit controls | RMR operation logging | -| CCPA | Right to delete | RMO primitive | +| Regulation | Requirement | Relevant primitive | What that does **not** establish | +|-------------------|-----------------------|--------------------|----------------------------------| +| GDPR Art. 17 | Right to erasure | RMO (`jk obliterate`), for files the tool can reach | That the data is gone from backups, replicas, journals or the media | +| GDPR Art. 5(1)(e) | Storage limitation | RMR history + `jk gc` pruning | Any retention policy; none is implemented or enforced | +| GDPR Art. 30 | Records of processing | RMR operation log, `obliterations.json` | That the record is complete or that the ledger is trustworthy on its own (the obliteration ledger is unkeyed) | +| SOX Section 802 | Record retention | RMR history, while the store is intact | Immutability against an attacker with write access | +| HIPAA | Audit controls | Attestation chain (HMAC-SHA256) over covered operations | That every relevant action is covered; obliteration records are not yet chained into the keyed audit log | +| CCPA | Right to delete | RMO, as above | Any of the above | ## Security Considerations @@ -234,13 +253,24 @@ Charles Bennett proved that all computation can be made reversible without signi Rolf Landauer established that erasing information has a minimum thermodynamic cost. RMO acknowledges that true erasure is an irreversible physical process. -### Epistemological Certainty +### What is proved, and what is not -Traditional logging provides *evidence* of state changes. MAA provides *proof*: +Traditional logging provides *evidence* of state changes. JanusKey provides +smaller, differently-shaped things, and the difference matters: -- RMR: Mathematical proof of reversibility +- **RMR:** three proved lemmas over a transaction *model* — a rollback restores + the state it began in given each step's undo restores its execute; the + lifecycle preserves the log invariant; at most one transaction is active + (`verification/proofs/agda/TransactionAtomicity.agda`, ledger rows T-1..T-3). + The claim "every operation is reversible" is **OPEN**, as is the mechanical + correspondence between that model and the Rust. +- **RMO:** nothing is proved. Overwriting is best effort; the record is + tamper-evident, not a certificate of absence. There is no mathematical proof + of non-existence, and there cannot be one from inside this process: the tool + cannot observe the media, the journal, or the backups. -- RMO: Mathematical proof of non-existence +The claims ledger in `PROOF-NEEDS.adoc` is the authority for both, and +`dashboard-check` fails the build when a dashboard's counts disagree with it. ## Further Reading @@ -248,6 +278,6 @@ Traditional logging provides *evidence* of state changes. MAA provides *proof*: - [RMO Primitive Specification](rmo-primitive.md) -- [Formal Proofs of Reversibility](../formal-proofs/reversibility.md) +- [Formal Proofs](../formal-proofs/index.md) - [Maximal Principle Reduction](mpr.md) diff --git a/docs/wiki/theory/mpr.md b/docs/wiki/theory/mpr.md index b2adbc7..16335c1 100644 --- a/docs/wiki/theory/mpr.md +++ b/docs/wiki/theory/mpr.md @@ -5,7 +5,11 @@ ## Definition -**Maximal Principle Reduction (MPR)** is a design philosophy and engineering methodology that achieves security and correctness guarantees through structural constraints rather than runtime verification. +**Maximal Principle Reduction (MPR)** is a design philosophy: prefer removing a +code path over defending it, and prefer a structural constraint over a runtime +check. It is vocabulary in this repository, not a formal method with tooling — +`README.adoc` says so explicitly, and no claim below is linked to the Rust by a +machine-checked proof (ledger row G-2 is ASSUMED). > If a vulnerability cannot exist in the design space, it cannot exist in the implementation. Reduce the design space to exclude vulnerabilities entirely. > @@ -135,7 +139,9 @@ pub fn execute_delete(&mut self, path: &Path) -> Result { .with_content_hash(content_hash) .with_original_metadata(file_metadata); - // NOW safe to delete - reversal is guaranteed possible + // The inverse now exists in memory; it does not yet exist on disk. + // If the append below fails, or the process dies before it runs, this + // delete cannot be undone (ledger rows T-6, T-8). fs::remove_file(path)?; self.metadata_store.append(metadata)?; @@ -192,11 +198,15 @@ This ensures that any reachable state has complete reversal information by const ### Storage Overhead -Content must be stored before deletion. This trades: \* Storage space (more) for reversibility (guaranteed) \* Mitigated by: compression, deduplication, garbage collection +Content must be stored before deletion. This trades storage space for the +*possibility* of reversal — not for a guarantee: the reversal also needs the +metadata append to succeed and the store to survive (rows T-6, T-8). Mitigated +by compression, deduplication and `jk gc`. ### Performance Overhead -Additional I/O for metadata capture. This trades: \* Latency (higher) for safety (guaranteed) \* Mitigated by: async operations, batching, transactions +Additional I/O for metadata capture: latency for recoverability, again subject +to the same two open rows. Mitigated by batching and transactions. ### Complexity Shift diff --git a/docs/wiki/theory/rmo-primitive.md b/docs/wiki/theory/rmo-primitive.md index 18a79c3..ea823fc 100644 --- a/docs/wiki/theory/rmo-primitive.md +++ b/docs/wiki/theory/rmo-primitive.md @@ -3,296 +3,171 @@ # RMO: Obliterative Wipe Primitive -## Definition - -**RMO (Obliterative Wipe)** is a data primitive that guarantees, via formal proof, the non-existence (unrecoverability) of specific data after invocation. This implements GDPR Article 17 "Right to Erasure" with mathematical certainty. - -> For data $d$ after $\text{RMO}(d)$, there exists no algorithm $A$ such that $A(\text{system\_state}) = d$. - -## Core Properties - -### Property 1: Irrecoverability - -After obliteration, the data cannot be recovered through any algorithmic means: - -$$\nexists A: A(\Sigma', M') \to d$$ +> **Status: engineering primitive, not a compliance mechanism and not a theorem.** +> RMO describes what `jk obliterate` does. It overwrites a file's bytes and +> removes it, and — when a JanusKey store exists — shreds the unshared +> content-store blobs and purges the operation-log entries for that path. +> It does **not** establish that the data is unrecoverable, and it is not a +> GDPR Article 17 determination. This page previously claimed both; the +> correction is recorded in `PROOF-NEEDS.adoc` (rows C-3, X-1) and in the +> audit at `docs/estate/2026-11-01-handoff-and-consistency-audit.md` (D1). -where $\Sigma'$ and $M'$ are the post-obliteration content and metadata stores. - -### Property 2: Verifiable Deletion - -Obliteration generates a cryptographic proof that can be independently verified: +## Definition -``` rust +**RMO (Obliterative Wipe)** is the deliberate, documented exception to +JanusKey's reversibility. Everything else in the tool stores the information +needed to invert itself; `jk obliterate` destroys that information instead. + +It is best-effort by construction: + +- Overwrite-in-place cannot reach physical media through wear levelling + (SSD), copy-on-write (ZFS, Btrfs), journaling, or a hypervisor's snapshot. +- The threat model for overwriting assumes rotating magnetic media. +- On modern media, physical destruction of the device is the only + guaranteed obliteration. + +The same caveat appears in `README.adoc` §"The secure obliteration exception" +and `GLOSSARY.adoc` §"Secure obliteration". If this page and those disagree, +they win. + +## What the operation actually does + +1. **Overwrite.** Three passes over the file's current length — `0x00`, then + `0xFF`, then random bytes — with `sync_all()` after each pass + (`crates/januskey-cli/src/obliteration.rs`, `secure_overwrite`, `OVERWRITE_PASSES = 3`). + The pattern set has the shape of DoD 5220.22-M. That is a description of + the passes, **not** a claim of conformance to that standard. +2. **Unlink.** `fs::remove_file` on the path. +3. **Scrub the store** (only when a `.januskey/` store exists, + `obliterate_path`): shred every content-store blob referenced by an + operation-log entry whose primary or secondary path is this one — **except** + a blob that a surviving entry for another path still references, which is + kept so the other path's history stays undoable. +4. **Purge the log entries.** `MetadataStore::purge_path`, so `jk undo` and + `jk history` no longer mention the path. Blobs are shredded *before* the + log is purged: if a shred fails, the entries survive and the command can be + re-run. +5. **Record.** Each shred appends a record to `obliterations.json` + (`OBLITERATION_LOG_FILE`), including the working file's proof. + +## The obliteration record + +```rust pub struct ObliterationProof { pub id: String, - pub content_hash: ContentHash, + pub content_hash: ContentHash, // what was destroyed pub timestamp: DateTime, + pub user: String, pub nonce: String, - pub commitment: String, // H(content_hash || nonce || timestamp) + pub commitment: String, // H(content_hash ‖ nonce ‖ timestamp) pub overwrite_passes: usize, + pub storage_cleared: bool, // set by the tool; not independently verified } ``` -### Property 3: Audit Trail Without Content - -The fact of obliteration is logged for compliance, but the content itself is never stored in the audit log: - -``` rust -pub struct ObliterationRecord { - pub timestamp: DateTime, - pub user: String, - pub content_hash: ContentHash, // Hash only, not content - pub reason: Option, - pub legal_basis: Option, - pub proof: ObliterationProof, -} -``` - -## Secure Overwrite Protocol - -RMO implements a multi-pass secure overwrite based on DoD 5220.22-M standards: - -### Phase 1: Pattern Overwrite - -``` rust -const OVERWRITE_PASSES: usize = 3; -const PATTERNS: [u8; 3] = [0x00, 0xFF, 0x00]; - -// Pass 1: Write all zeros -// Pass 2: Write all ones -// Pass 3: Random data -``` - -### Phase 2: File Removal - -After secure overwrite, the file is deleted from the filesystem. - -### Phase 3: Proof Generation - -A cryptographic commitment is generated: - -$$\text{commitment} = H(\text{content\_hash} \| \text{nonce} \| \text{timestamp})$$ - -This allows verification that: - -1. The specific content (identified by hash) was obliterated - -2. Obliteration occurred at a specific time - -3. The proof has not been tampered with - -## CLI Commands - -### Obliterate Content - -``` bash -# Obliterate by content hash -jk obliterate --hash sha256:abc123... --reason "User request" --legal-basis "GDPR Article 17" - -# Obliterate content from a specific operation -jk obliterate --operation --reason "Data breach cleanup" -``` - -### View Obliteration History - -``` bash -jk obliteration-history --limit 20 -``` - -Output: - - Obliteration History (RMO Audit Trail) - ════════════════════════════════════════════════════════════════════════════════ - - 2025-12-17 10:30:00 UTC | OBLITERATED | sha256:abc123... - Proof: 12345678 | User: jonathan - Reason: User request - Legal basis: GDPR Article 17 - - ════════════════════════════════════════════════════════════════════════════════ - Total obliterations: 1 - -### Verify Obliteration Proof - -``` bash -jk verify-obliteration -``` - -Output: - - Obliteration Proof Verification - ────────────────────────────────────────────────── - - Proof ID: abc123-def456... - Content Hash: sha256:abc123... - Timestamp: 2025-12-17 10:30:00 UTC - User: jonathan - Overwrite Passes: 3 - - Commitment: 9f86d081884c7d659a2feaa0c55ad015... - Nonce: a3f2b8c9d0e1f2a3... - - ✓ Cryptographic commitment VERIFIED - The proof cryptographically confirms that: - • Content with hash sha256:abc123... was obliterated - • Obliteration occurred at 2025-12-17 10:30:00 - • 3 overwrite passes were performed - - ✓ Content confirmed absent from store +What the commitment is: a SHA-256 binding of *the claim being made* — which +content hash, at what time, with which nonce. It detects accidental changes +to the record. It does not resist a writer who edits the record, because the +commitment has no secret key. It is **not** a proof that the content +is gone, and `storage_cleared` is an assertion written by the same code path +that performed the overwrite, not an independent check. + +What can be checked in-process today: `ObliterationProof::verify_commitment` +(recompute the hash from the record), `ObliterationManager::verify_proof(id)`, +and `verify_obliteration(path, original_hash)` (the path no longer holds that +content). There is **no** `jk verify-obliteration` and no +`jk obliteration-history` subcommand; the CLI surface is `jk obliterate …` +with the global `--dry-run` and `--yes` flags, and it asks for confirmation +when non-interactive without `--yes`. + +## Status, in the claims-ledger vocabulary + +| Statement | Status | Where | +|---|---|---| +| A transaction containing an obliteration is not all-reversible | **PROVEN** (model) | `Layout.idr::obliterateNotReversible` (ledger C-3) | +| Obliterating a path shreds its unshared blobs and log entries, and undo then has nothing | **TESTED** | `obliteration_cas_test::obliterate_scrubs_blobs_log_and_undo` | +| A blob another path still references is kept | **TESTED** | `obliteration_cas_test::obliterate_keeps_blob_shared_with_another_path` | +| `jk obliterate` scrubs the store end to end | **TESTED** | `obliteration_cas_test::cli_obliterate_scrubs_store_and_undo_has_nothing` | +| Data erasure is complete and irreversible (obliteration correctness) | **OPEN** | `PROOF-NEEDS.adoc` §What Needs Proving | +| Physical erasure; hash one-wayness | **ASSUMED** (external) | ledger X-1 | +| The obliteration record is chained into the keyed, tamper-evident audit log | **DESIGNED, not built** | `obliterations.json` is an unkeyed JSON ledger; chaining deferred (J2-3) | + +Nothing in RMO is proved. The one PROVEN row above is a *model* statement +(C-3) about the operation log, not about bytes on a device. + +## Erasure requests: what this does and does not establish + +RMO is useful to a controller handling an erasure request. It is not a +compliance determination, and this repository makes none. + +| Requirement (e.g. GDPR Art. 17) | What JanusKey supplies | What it does not supply | +|---|---|---| +| Erase without undue delay | Overwrite + unlink in one command; store scrub where a store exists | Any guarantee against media-level retention, journaling, snapshots, or backups | +| Evidence that erasure was carried out | A timestamped commitment record with the content hash, user, pass count — logged without the content | Proof of non-existence; independent verification | +| Records of the request | `obliterations.json`, plus the audit chain for other operations | Retention policy, legal-basis handling, controller/processor analysis | +| No retention of erased content | Proof records hold the hash, not the bytes | Erased copies outside JanusKey's reach (backups, replicas, caches) | + +Whether a given deployment is compliant is a determination for the +controller, on the facts of that deployment — including media type, backups, +replicas, and retention policy. A local file tool cannot make it. ## Relationship with RMR -RMR and RMO are complementary primitives in the MAA Framework: +RMR (reversible transactions) and RMO (obliterative wipe) are complementary, +and the composition is intentional: +``` +---------------+ +---------------+ | RMR | | RMO | | Reversibility | | Obliteration | +-------+-------+ +-------+-------+ - | | - | Normal operation | - +------------------------------------> - | | - | Can undo via RMR | + | normal operation | + +------------------------------------>| + | can undo via RMR | <------------------------------------+ - | | - | GDPR erasure request | - +------------------------------------> - | | - | After RMO: NO undo | - | Content unrecoverable | - | | - +-------+-------+ +-------+-------+ - | Accountability| | Autonomy | - +---------------+ +---------------+ - -### Key Differences - -| Aspect | RMR | RMO | -|-----------------|----------------------------|---------------------------| -| Purpose | Track and reverse changes | Permanently erase data | -| Reversibility | Always reversible | Never reversible | -| Content storage | Preserves original content | Destroys original content | -| Audit | Full operation details | Fact of deletion only | -| Legal basis | Accountability | Right to Erasure | - -## GDPR Compliance - -RMO directly supports GDPR Article 17 "Right to Erasure": - -### Article 17 Requirements - -> The data subject shall have the right to obtain from the controller the erasure of personal data concerning him or her without undue delay. -> -> — GDPR Article 17 - -### How RMO Complies - -| GDPR Requirement | RMO Implementation | -|-----------------------------|---------------------------------------------| -| Erasure without undue delay | Immediate secure overwrite | -| Verification of erasure | Cryptographic obliteration proof | -| Record of erasure | Audit log with timestamp, user, legal basis | -| No retention of erased data | Proof contains only hash, not content | - -## Formal Verification - -### Theorem: Formal Obliteration - -After $\text{RMO}(h)$ for content hash $h$: - -$$\Sigma(h) = \bot \land \text{proof\_valid}(h)$$ - -The content is removed from the store and a valid proof exists. - -### Proof - -1. **Secure Overwrite**: Content at path derived from $h$ is overwritten with patterns - -2. **File Removal**: Path is deleted from filesystem - -3. **Proof Generation**: Commitment $H(h \| n \| t)$ is computed - -4. **Store Update**: $\Sigma(h) := \bot$ - -By the irreversibility of secure overwrite and the collision resistance of SHA256, the content is unrecoverable. ∎ - -## Implementation - -``` rust -impl ObliterationManager { - pub fn obliterate( - &mut self, - content_store: &ContentStore, - content_hash: &ContentHash, - reason: Option, - legal_basis: Option, - ) -> Result { - // Get content path - let content_path = content_store.content_path(content_hash); - - // Perform secure overwrite - let passes = secure_overwrite(&content_path)?; - - // Remove file - fs::remove_file(&content_path)?; - - // Generate proof - let proof = ObliterationProof::generate(content_hash, passes); - - // Create audit record - let record = ObliterationRecord { - id: Uuid::new_v4().to_string(), - timestamp: Utc::now(), - user: whoami::username(), - content_hash: content_hash.clone(), - reason, - legal_basis, - proof, - cleaned_operation_ids: Vec::new(), - }; - - // Log for audit - self.log.records.push(record.clone()); - self.save()?; - - Ok(record) - } -} + | erasure request | + +------------------------------------>| + | after RMO: no undo path | ``` -## Security Considerations - -### Secure Overwrite Limitations - -- Does not guarantee erasure from SSDs with wear leveling - -- May not erase data from filesystem journal - -- Cloud storage may retain backups - -For maximum security: - -1. Use encrypted storage where possible - -2. Consider physical destruction for highly sensitive data - -3. Verify with specialized forensic tools - -### Proof Tamper Resistance - -The cryptographic commitment prevents: - -- Backdating obliteration claims - -- Claiming obliteration of different content - -- Modifying the proof after generation - -## Further Reading +The difference that matters for design, not marketing: + +| Aspect | RMR | RMO | +|---|---|---| +| Purpose | Track and reverse changes | Destroy the record of one path | +| Reversibility | Reversible by metadata lookup | No inverse exists; undo has nothing to restore | +| Content storage | Preserved in the content store | Shredded, unless another path shares the blob | +| Audit | Operation log entries | Fact of deletion only, in an unkeyed ledger | +| Failure mode | Store loss makes undo impossible | Shared blobs and media-level retention leave traces | + +## Security considerations + +- **Media.** See the caveat at the top. A successful `jk obliterate` on an + SSD does not mean the bytes are gone. +- **Shared blobs.** Deduplication means one blob can back several paths. + Obliterating one path keeps a blob another path still references — correct + for reversibility, but it means "obliterated" is not "gone from the store". + `--dry-run` lists only the target paths. It does not report the shared + blobs that will be kept or the history entries that will be purged. +- **The ledger is unkeyed.** `obliterations.json` is not HMAC-chained. An + attacker with write access to the store can edit it. The keyed `AuditLog` + covers other operations and requires an unlocked key; joining the two is + J2-3, not done. +- **Interruption.** Blobs are shredded before the log is purged, so a + partially completed obliteration can be re-run. It cannot be *undone*. + +## Formal status + +There is no theorem here, and there should not be a `∎` on this page until +one exists. The nearest statement in the kernel is G-1 +(`verification/proofs/agda/Reversibility.agda`): reversibility is a `Loss` +grade over traces, with an obliterating step absorbing — a statement about the +grade algebra, not about storage media. `X-1` keeps physical erasure and hash +one-wayness explicitly outside the theorem set. + +## Further reading - [RMR: Reversible Transaction Primitive](rmr-primitive.md) - - [MAA Framework Overview](maa-framework.md) - -- [CLI Commands Guide](../guides/cli.md) +- `../../../PROOF-NEEDS.adoc` — the claims ledger this page reconciles against +- `../../security/THREAT_MODEL.adoc` — limitations and the compliance mapping diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 18130a8..2d425e6 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -3,86 +3,119 @@ # RMR: Reversible Transaction Primitive -## Definition - -**RMR (Reversible Transaction)** is a data primitive that guarantees the existence of a mathematically sound inverse function for every state change. - -> For every operation $F$ applied to state $S$, there exists an inverse $F^{-1}$ such that $F^{-1}(F(S)) = S$. - -## Core Properties +> **Status: an engineering mechanism with a partially proved model.** +> JanusKey records the inverse of each operation and can replay it. Three +> lemmas about the transaction *model* are proved in Agda; the step-level +> premise, two failure-path premises and the atomicity of the metadata log are +> not, and the headline claim "every operation is reversible" is an OPEN row in +> `PROOF-NEEDS.adoc`. This page previously stated the property as a theorem +> with a proof sketch and a `∎`; the correction is recorded in +> `../../../docs/estate/2026-11-01-handoff-and-consistency-audit.md` (D1). -### Property 1: Deterministic Reversal - -Given an operation and its metadata, the reversal is uniquely determined: - -$$\text{undo}: (\text{Operation}, \text{Metadata}) \to \text{Operation}^{-1}$$ +## Definition -There is no ambiguity in how to reverse an operation. +**RMR (Reversible Transaction)** is the property JanusKey aims at: for every +operation `F` it applies to state `S`, it records enough to apply an inverse +`F⁻¹` with `F⁻¹(F(S)) = S`. -### Property 2: State Preservation +Whether that holds in general is **open**. What holds today, concretely: -The reversal restores *complete* original state, including: +- each operation type has a named inverse (`OperationType::inverse`: + `Delete↔Create`, `Modify↔Modify`, `Move↔Move`, `Copy→Delete`, `Chmod`, + `Chown` self-inverse); +- the information needed for that inverse is captured *before* the mutation + (content into the store, file metadata into the log); +- `execute` then `undo` restores the prior state under property testing + (`property_tests::execute_then_undo_is_identity`); +- rolling back a whole transaction in reverse order restores the state it + began in, **given** that each step's undo restores its execute. That + conditional is a proved Agda lemma (T-1); the premise itself is tested, not + proved (T-6). -- File content (byte-for-byte identical) +## Core properties, at the strength the code supports -- File metadata (permissions, ownership, timestamps) +### 1. Reversal is determined, not searched -- Directory structure +The inverse is a function of the recorded metadata, not of a filesystem scan: +undo is a lookup in the append-only log followed by the operation-specific +inverse in `delta.rs` / `operations.rs`. "Determined" is the honest word — the +metadata is the sole input, and if it is lost the reversal is not merely +ambiguous, it is unavailable. -- Symbolic link targets +### 2. What a reversal restores -### Property 3: Sequential Composition +Capture and restore are **not** the same set, and the difference matters: -For a sequence of operations, reversals compose correctly: +| Aspect | Captured? | Restored on undo? | +|---|---|---| +| File content | yes — content store, SHA-256 | yes, verified against the hash on read | +| Permissions | yes (`FileMetadata.permissions`) | yes — `FileMetadata::apply` sets the mode | +| Owner / group | yes (`owner`, `group`) | **no** — no `chown` call exists; values are recorded for the record's sake | +| Modification time | yes (`modified`) | **no** — no `utimensat`/`set_times` call exists | +| Symlink target | yes (`is_symlink`, `symlink_target` via `read_link`) | **no** — no `symlink()` call exists, so a deleted symlink is not recreated as a symlink | +| Directory structure | per-file: a recursive delete logs one operation per entry | recreated only as far as the individual file undos recreate their parents | -$$(O_2 \circ O_1)^{-1} = O_1^{-1} \circ O_2^{-1}$$ +So "complete original state, byte-for-byte" is not true of this +implementation. It is true of content and permissions on Unix; the rest is +recorded but not applied. -Operations are undone in reverse order. +### 3. Sequential composition -### Property 4: Transaction Atomicity +Undo runs in reverse order, and composition is the proved model statement: -Operations grouped in a transaction satisfy: +``` +undo(Oₙ) ∘ ⋯ ∘ undo(O₁) ∘ O₁ ∘ ⋯ ∘ Oₙ(S₀) = S₀ +``` -- All-or-nothing execution +This is ledger row **T-1** (`TransactionAtomicity.rollback-restores`, PROVEN in +Agda over the log model) plus the rejected fixture +`tests/reject-agda/ForwardRollback.agda`. It is conditional on T-6; it is not a +statement about bytes on a device. -- All-or-nothing reversal +### 4. Transaction semantics: recorded and resumable, not isolated -- Intermediate states are not externally visible +| Claim | Reality | +|---|---| +| Commit/rollback settle a group of operations | yes — `TransactionManager`, states `Active`/`Committed`/`RolledBack`; at most one active (T-3, PROVEN) | +| A rollback that fails part-way can be retried | yes (T-4, TESTED — `rollback_resume_test`, driving the real `jk`) | +| A failed save leaves memory and disk agreeing | yes for the transaction log (T-5, TESTED, write→fsync→rename with permission preservation) | +| The **operation metadata** log has the same guarantee | **unverified** — `MetadataStore::save` now calls `crate::transaction::write_atomic` (write → sync → rename), but that edit has not been built or run (T-8, **OPEN**); an undo whose `mark_undone` fails to persist still leaves the file undone and the log unchanged | +| A failed execute leaves the filesystem unchanged | assumed, not checked (T-6) | +| Intermediate states are invisible to other processes | **false** — operations are applied to the filesystem one at a time as they are executed. A transaction gives you a recorded, resumable rollback, not isolation. Nothing in this tool locks, stages, or hides the working tree | -## RMR Protocol +## Protocol, as a sketch -### Phase 1: Pre-Capture +The phases below are the intended shape, not the call surface: `PreCaptureData` +and `StorageReceipt` are illustrative types, and the real API is +`ReversibleExecutor` in `crates/reversible-core/src/lib.rs` plus +`OperationExecutor` in `crates/januskey-cli/src/operations.rs`. Read them as +prose with braces. -Before any modification, capture everything needed for reversal: +### Phase 1: Pre-capture -``` rust +```rust // For a DELETE operation fn pre_capture_delete(path: &Path) -> PreCaptureData { PreCaptureData { - content: fs::read(path), // Full file content - metadata: FileMetadata::from_path(path), // All metadata - content_hash: sha256(content), // For verification + content: fs::read(path), + metadata: FileMetadata::from_path(path), + content_hash: sha256(content), } } ``` -### Phase 2: Secure Storage - -Store captured data in content-addressed storage: +### Phase 2: Content-addressed storage -``` rust +```rust fn secure_store(data: PreCaptureData) -> StorageReceipt { let hash = content_store.store(data.content)?; - // Content is now safely stored with deduplication StorageReceipt { hash, verified: true } } ``` -### Phase 3: Metadata Recording +### Phase 3: Metadata recording -Create complete operation metadata: - -``` rust +```rust fn record_metadata(op: Operation, receipt: StorageReceipt) -> OperationMetadata { OperationMetadata { id: uuid::new_v4(), @@ -92,221 +125,159 @@ fn record_metadata(op: Operation, receipt: StorageReceipt) -> OperationMetadata path: op.path(), content_hash: Some(receipt.hash), original_metadata: Some(op.original_metadata()), - // Everything needed for reversal } } ``` ### Phase 4: Execute -Only after all safety measures are in place: - -``` rust +```rust fn execute(op: Operation) -> Result<()> { - // At this point, reversal is guaranteed possible + // The recorded metadata is now the only thing between this operation + // and unrecoverability. If the append below fails, the inverse is lost. op.perform()?; metadata_store.append(metadata)?; Ok(()) } ``` -### Phase 5: Reversal +Ordering note, because this is where the guarantee is thinnest: in +`execute_delete` the content is stored **before** the unlink and the metadata is +appended **after** it (`operations.rs`). A crash between the unlink and the +append loses the ability to undo that delete. T-6 and T-8 are the ledger rows +that would have to close to remove that window. -When undo is requested: +### Phase 5: Reversal -``` rust +```rust fn undo(operation_id: &str) -> Result<()> { let metadata = metadata_store.get(operation_id)?; - - // Retrieve original content let content = content_store.retrieve(&metadata.content_hash)?; - - // Reconstruct inverse operation let inverse = construct_inverse(&metadata, content); - - // Execute reversal inverse.perform()?; - - // Record the undo - metadata_store.mark_undone(operation_id)?; + metadata_store.mark_undone(operation_id)?; // T-8: save atomic since 2026-11-01, unbuilt Ok(()) } ``` -## Operation-Specific RMR - -### DELETE → CREATE - -| Forward (Delete) | Reverse (Create) | -|-----------------------|-----------------------------| -| Read content → Store | Retrieve content from store | -| Read metadata → Store | Apply stored metadata | -| Remove file | Write file with content | -| Log operation | Log undo operation | - -### MODIFY → MODIFY - -| Forward (Modify) | Reverse (Modify back) | -|-------------------------------|-----------------------------| -| Read original content → Store | Retrieve original content | -| Write new content | Write original content back | -| Log with both hashes | Log undo | - -### MOVE → MOVE - -| Forward (Move A→B) | Reverse (Move B→A) | -|-------------------------|----------------------------------| -| Record source path | Use stored source as destination | -| Record destination path | Use stored destination as source | -| Perform rename | Perform rename back | -| Log operation | Log undo | - -### MKDIR → RMDIR - -| Forward (Mkdir) | Reverse (Rmdir) | -|-----------------------|-------------------------| -| Create directory | Remove directory | -| Log path | Use logged path | -| (No content to store) | (No content to restore) | +## Operation-specific inverses -### RMDIR (recursive) → Restore +Taken from `OperationType::inverse` (`crates/reversible-core/src/metadata.rs`). +There is no `Mkdir`/`Rmdir` operation type: a directory is deleted by walking it +and logging one `Delete` per entry. -| Forward (Rmdir -r) | Reverse (Full restore) | -|-------------------------|------------------------| -| Walk directory tree | Read manifest | -| Store each file content | Restore each file | -| Store manifest | Recreate directories | -| Remove directory tree | Apply metadata | +| Forward | Inverse | What is stored for the inverse | +|---|---|---| +| `Delete` | `Create` | content hash + original metadata | +| `Create` | `Delete` | nothing (the file did not exist) | +| `Modify` | `Modify` | original hash + new hash; `delta.rs` stores a full copy or a line/block delta | +| `Move` | `Move` | source and destination paths; the inverse swaps them | +| `Copy` | `Delete` | destination path; the inverse removes the copy | +| `Chmod` | `Chmod` | original mode | +| `Chown` | `Chown` | original owner/group | -## Formal Verification +`Chmod` and `Chown` exist in the model and the operation layer but are **not** +exposed as `jk` subcommands; the CLI surface is `init, delete, modify, move, +copy, rename, obliterate, undo, begin, commit, rollback, preview, history, +status, gc`. -### Theorem: RMR Correctness +## Formal status -For all operations $O$ and states $S$: +There is no single "RMR correctness" theorem here, and this page should not +present one until it exists. What exists, by ledger row: -$$\text{undo}(\text{execute}(O, S)) = S$$ +| Row | Statement | Status | +|---|---|---| +| T-1 | Undoing a fully executed transaction in reverse order restores the state it began in, given each step's undo restores its execute | **PROVEN** (Agda, model) | +| T-2 | The lifecycle preserves the log invariant and rewrites only the Active transaction | **PROVEN** (Agda, model) | +| T-3 | At most one transaction is Active | **PROVEN** (Agda, model) | +| T-4 | A partially failed rollback can be retried to completion | **TESTED** | +| T-5 | The transaction log is replaced atomically, with permissions preserved | **TESTED** | +| T-6 | A failed execute leaves the filesystem unchanged; each undo restores its execute's pre-state | **ASSUMED** | +| T-7 | Transaction ids never collide | **ASSUMED** | +| T-8 | The operation metadata log is saved atomically | **OPEN** — saves by rename since 2026-11-01, not yet built or run | +| — | "Every operation is reversible" as a theorem linked to the Rust | **OPEN** | +| G-2 | The Idris2 and Agda presentations correspond | **ASSUMED** — "by transcription, no mechanical link claimed" | -#### Proof Sketch +## Implementation details -1. **Pre-capture completeness**: By construction, pre-capture stores all information needed to reconstruct original state. +### Content store -2. **Storage integrity**: Content-addressed storage with SHA256 verification ensures stored content is retrieved exactly. - -3. **Metadata sufficiency**: Operation metadata contains path, original metadata, and content hash—sufficient for reconstruction. - -4. **Inverse construction**: Each operation type has a defined inverse that uses stored information. - -5. **Composition**: Undo operations are themselves operations that can be tracked. ∎ - -### Theorem: Sequential Reversibility (Theorem 3.4) - -For operations $O_1, O_2, \ldots, O_n$: - -$$\text{undo}(O_n) \circ \cdots \circ \text{undo}(O_1) \circ O_1 \circ \cdots \circ O_n(S) = S$$ - -#### Proof - -By induction on $n$: - -**Base case** ($n=1$): Direct application of RMR correctness. - -**Inductive step**: Assume true for $n-1$. Then: - -$$\text{undo}(O_n)(O_n(O_{n-1}(\cdots O_1(S)))) = O_{n-1}(\cdots O_1(S))$$ - -By inductive hypothesis, the remaining undos restore $S$. ∎ - -## Implementation Details - -### Content Store - -``` rust -pub struct ContentStore { - root: PathBuf, - compression: bool, -} +```rust +pub struct ContentStore { root: PathBuf, compression: bool } impl ContentStore { - // Store content, return hash pub fn store(&self, content: &[u8]) -> Result { - let hash = ContentHash::from_bytes(content); + let hash = ContentHash::from_bytes(content); // sha256: let path = self.content_path(&hash); - - // Deduplication: skip if already stored - if path.exists() { - return Ok(hash); - } - - // Write (optionally compressed) + if path.exists() { return Ok(hash); } // dedup self.write_content(&path, content)?; Ok(hash) } - // Retrieve with integrity verification pub fn retrieve(&self, hash: &ContentHash) -> Result> { let content = self.read_content(&self.content_path(hash))?; - - // Verify integrity - if !hash.verify(&content) { - return Err(JanusError::ContentIntegrityError); - } - + if !hash.verify(&content) { return Err(JanusError::ContentIntegrityError); } Ok(content) } } ``` -### Metadata Store +Deduplication has a consequence worth knowing: a blob can back several paths, so +"delete the blob" is not the same as "delete this file's history" — see the +shared-blob rule in [RMO](rmo-primitive.md). -``` rust -pub struct MetadataStore { - path: PathBuf, - log: OperationLog, -} +### Metadata store +```rust impl MetadataStore { - // Append-only operation logging pub fn append(&mut self, metadata: OperationMetadata) -> Result<()> { self.log.operations.push(metadata); - self.save()?; + self.save()?; // T-8: write→sync→rename, unbuilt Ok(()) } - // Mark operation as undone - pub fn mark_undone(&mut self, id: &str, undo_id: &str) -> Result<()> { - if let Some(op) = self.get_mut(id) { - op.undone = true; - op.undo_operation_id = Some(undo_id.to_string()); - self.save()?; - } + pub fn mark_undone(&mut self, id: &str) -> Result<()> { + if let Some(op) = self.get_mut(id) { op.undone = true; self.save()?; } Ok(()) } } ``` -## Performance Characteristics - -| Metric | Value | Notes | -|-------------------|----------------------|------------------------| -| Storage overhead | O(content size) | With deduplication | -| Capture latency | O(file size) | Single read operation | -| Undo latency | O(file size) | Single write operation | -| Metadata overhead | ~500 bytes/operation | JSON serialized | +The transaction log (`TransactionLog::save`) uses the atomic path in +`transaction.rs`: a per-save temporary file, mode preservation, fsync and +rename. The operation metadata log now calls the same helper, so the asymmetry +is closed in source and still open in evidence — nothing has built or run the +change, which is why row T-8 stays OPEN. -## Limitations +## Performance -1. **Requires disk space**: Original content must be stored +The table below is *expected* cost derived from the algorithm, not a +measurement. No baseline has been recorded; the five Criterion groups exist but +their results are unbaselined (`READINESS.adoc` §Benchmark Classification). -2. **Not instantaneous**: Pre-capture adds latency to operations +| Metric | Expected | Notes | +|---|---|---| +| Storage overhead | O(content size) | with deduplication | +| Capture latency | O(file size) | one read | +| Undo latency | O(file size) | one write | +| Metadata overhead | ~500 bytes/operation | JSON serialized | -3. **Single-system**: RMR operates on local file system only +## Limitations -4. **No external side effects**: Cannot reverse network operations, etc. +1. **The store is the whole guarantee.** Lose `.januskey/` and undo is gone. +2. **Metadata consistency is weaker than it looks** — T-8 is open; the + metadata log now saves by rename, but that change is unverified. +3. **Not everything captured is restored** — ownership, mtime and symlink + identity are recorded but not applied (§2). +4. **No isolation.** Operations touch the live filesystem as they execute. +5. **Local filesystem only.** No network or external side effects are reversed. +6. **Not proved against the Rust** — G-2 is ASSUMED, so the Agda model and the + implementation are linked by review, not by machine. -## Further Reading +## Further reading - [RMO: Obliterative Wipe Primitive](rmo-primitive.md) - - [Formal Model of File System State](formal-model.md) - -- [Content Store Implementation](../architecture/content-store.md) +- `../../../PROOF-NEEDS.adoc` — the claims ledger, rows T-1..T-8 +- [Architecture](../architecture/index.md) diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 98b9f0d..27862c0 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -9,9 +9,18 @@ export LC_ALL="${LC_ALL:-C.UTF-8}" prover="${AGDA:-agda}" "$prover" --version bash scripts/fetch-siblings.sh -flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check +# PROOF-POLICY §2.1 canonical invocation: --safe --without-K --cubical-compatible +# (standards/3-practice/PROOF-POLICY.adoc). The cubical-compatible flag is +# infectious in principle — direct imports must use it too — but Agda 2.6.4.3 +# accepts a --without-K sibling on the include path and reports the pattern +# matches that will not compute under transports as UnsupportedIndexedMatch +# warnings (14 in Reversibility, 16 in TransactionAtomicity, 2 in Epistemic; the +# sibling's ≤-trans, obliterate-absorbs and just-inj). Those are warnings about +# computation under transport, not about the propositions, so the gate keeps +# them visible rather than silencing them with -WnoUnsupportedIndexedMatch. +flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -i verification/proofs/agda -i _build/dependencies/resource-algebra/src) -for module in Reversibility TransactionAtomicity; do +for module in Reversibility TransactionAtomicity Epistemic; do "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda" done mkdir -p _build/check-logs diff --git a/src/abi/JanusKey/ABI/Proofs.idr b/src/abi/JanusKey/ABI/Proofs.idr index 1a4af99..597c8cc 100644 --- a/src/abi/JanusKey/ABI/Proofs.idr +++ b/src/abi/JanusKey/ABI/Proofs.idr @@ -217,6 +217,13 @@ data AuditorView : Type where ||| Knows has no negative form, so the former `systemForgetsOldKey` (which ||| returned knowledge of the new key and said nothing about the old) is gone. ||| Types.systemKnowsNewKey remains as the positive statement. +||| +||| It *is* expressible once knowledge is indiscriminability over an observation +||| and "usable" is a predicate that can be false: see +||| verification/proofs/agda/Epistemic.agda, lemma rotate-forgets-old (no agent, +||| the system included, can use the old key after rotation) and row E-1m in the +||| claims ledger. The deleted lemma stays deleted here — this module's model has +||| not changed. -- ============================================================ -- 10. Error Code Proofs diff --git a/src/abi/JanusKey/ABI/Types.idr b/src/abi/JanusKey/ABI/Types.idr index 5037c5f..bcc4f6b 100644 --- a/src/abi/JanusKey/ABI/Types.idr +++ b/src/abi/JanusKey/ABI/Types.idr @@ -402,7 +402,15 @@ data PostObliteration : ContentHash -> Type where ||| `Knows Adversary a` is uninhabited because `Knows` has no Adversary ||| constructor: a property of this model, not a security proof. What a real ||| attacker can recover after obliteration is OPEN in the claims ledger -||| (PROOF-NEEDS.adoc). +||| (PROOF-NEEDS.adoc, row E-1). +||| +||| The *model-level* statements this constructor family cannot make — that an +||| adversary whose observation excludes the store does not know its contents, +||| that obliteration leaves nothing to recover, and that rotation makes the old +||| key unusable for every agent — are proved in Agda over a world model with an +||| observation channel: verification/proofs/agda/Epistemic.agda (ledger row +||| E-1m). This module is unchanged by that; the epistemic theory lives there, +||| under the kernel gate, and the cryptographic claim stays OPEN here. public export adversaryCannotKnow : Knows Adversary a -> Void adversaryCannotKnow _ impossible diff --git a/tests/reject-agda/AdversaryKnows.agda b/tests/reject-agda/AdversaryKnows.agda new file mode 100644 index 0000000..170dc2c --- /dev/null +++ b/tests/reject-agda/AdversaryKnows.agda @@ -0,0 +1,15 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- expect: 2 != 1 +-- +-- Ledger row E-1m: "the two worlds hold the same thing". Epistemic.x₁ and +-- Epistemic.x₂ differ only in what the store holds, and the epistemic model is +-- built so the adversary cannot tell them apart — which is exactly why the +-- stores cannot be identified. This fixture pins that the checker refuses it. +module AdversaryKnows where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Epistemic + +wrong : World.content x₂ ≡ World.content x₁ +wrong = refl diff --git a/tests/reject-agda/OldKeyStillUsable.agda b/tests/reject-agda/OldKeyStillUsable.agda new file mode 100644 index 0000000..bfdc0d7 --- /dev/null +++ b/tests/reject-agda/OldKeyStillUsable.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- expect: != true of type Agda.Builtin.Bool.Bool +-- +-- Ledger row E-1m, the rotation half: "after rotating old -> new the old key is +-- still usable". Epistemic.rotate-forgets-old says it is not. This fixture pins +-- that the checker refuses the claim. +module OldKeyStillUsable where + +open import Agda.Builtin.Bool using (true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Epistemic + +wrong : ∀ a old new x → (old == new) ≡ false → + World.usable (rotate old new x) a old ≡ true +wrong a old new x neq = refl diff --git a/verification/proofs/agda/Epistemic.agda b/verification/proofs/agda/Epistemic.agda new file mode 100644 index 0000000..807a5e4 --- /dev/null +++ b/verification/proofs/agda/Epistemic.agda @@ -0,0 +1,253 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- The epistemic fragment, rewritten. +-- +-- januskey's Idris2 ABI carries a `Knows : Agent -> Type -> Type` modality +-- (src/abi/JanusKey/ABI/Types.idr §Level 12) inherited from the estate's +-- epistemic work. It cannot state what the security claims need: +-- +-- * `Knows Adversary a` is uninhabited *by construction* — there is no +-- Adversary constructor — so "an attacker cannot recover ..." (ledger row +-- E-1) reduces to an absence in a datatype, which the repository's own +-- comment calls "a property of this model, not a security proof". +-- * "The system forgets the old key" is not expressible at all: `Knows` has +-- no negative form, so the lemma was deleted rather than repaired. +-- +-- This module replaces the modality with one whose ignorance is a proposition. +-- Knowledge is indiscriminability over an observation: an agent knows φ in x +-- when φ holds in every world it cannot distinguish from x. Ignorance is then +-- ¬ Knows, which is provable by exhibiting a world that looks the same and is +-- not; and forgetting is a statement about what an agent can use, which can be +-- false. +-- +-- What this does and does not buy is stated at the foot of the file. + +module Epistemic where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Maybe using (Maybe; nothing; just) +open import Agda.Builtin.Nat using (Nat; zero; suc) +open import Agda.Builtin.Sigma using (Σ; _,_) + +---------------------------------------------------------------------- +-- A kernel-sized prelude: nothing is imported beyond the builtins +---------------------------------------------------------------------- + +data ⊥ : Set where + +_×_ : (A B : Set) → Set +A × B = Σ A (λ _ → B) + +⊥-elim : ∀ {A : Set} → ⊥ → A +⊥-elim () + +¬_ : Set → Set +¬ A = A → ⊥ + +infix 3 ¬_ + +_≢_ : ∀ {A : Set} → A → A → Set +x ≢ y = ¬ (x ≡ y) + +infix 4 _≢_ + +trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z +trans refl q = q + +sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x +sym refl = refl + +cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y +cong f refl = refl + +just-inj : ∀ {a b : Nat} → just a ≡ just b → a ≡ b +just-inj refl = refl + +nothing≢just : ∀ {a : Nat} → nothing ≡ just a → ⊥ +nothing≢just () + +just≢nothing : ∀ {a : Nat} → just a ≡ nothing → ⊥ +just≢nothing () + +false≢true : false ≡ true → ⊥ +false≢true () + +subst : ∀ {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y +subst P refl p = p + +if_then_else_ : ∀ {A : Set} → Bool → A → A → A +if true then a else b = a +if false then a else b = b + +-- Decidable equality on Nat, and the only fact about it the proofs need: +-- a number equals itself. +_==_ : Nat → Nat → Bool +zero == zero = true +zero == suc _ = false +suc _ == zero = false +suc m == suc n = m == n + +==-refl : ∀ n → (n == n) ≡ true +==-refl zero = refl +==-refl (suc n) = ==-refl n + +---------------------------------------------------------------------- +-- The model +---------------------------------------------------------------------- + +ContentHash = Nat +Content = Nat +KeyId = Nat + +data Agent : Set where + owner system auditor adversary : Agent + +-- A world: what the store holds, which keys each agent can use, and what each +-- agent can see. `see` is the observation channel; the Store channel is +-- `content`. They are separate fields on purpose: the interesting theorems are +-- about how they come apart. +record World : Set where + constructor w + field + content : ContentHash → Maybe Content + usable : Agent → KeyId → Bool + see : Agent → List (ContentHash × Content) + +open World public + +observe : Agent → World → List (ContentHash × Content) +observe a x = see x a + +-- Knowledge as indiscriminability: φ holds in every world the agent cannot +-- tell apart from this one. This is the replacement for the uninhabited `Knows` +-- constructor family — it can be false, which is the point. +Knows : Agent → (World → Set) → World → Set +Knows a φ x = ∀ x' → observe a x' ≡ observe a x → φ x' + +CanUse : World → Agent → KeyId → Set +CanUse x a k = usable x a k ≡ true + +-- The store holds a recoverable value for this hash. +Recovers : World → ContentHash → Set +Recovers x h = Σ Content (λ c → content x h ≡ just c) + +---------------------------------------------------------------------- +-- Theorem 1. Knowledge is inhabited: an agent knows its own observation. +-- (The positive control — without it, "the adversary does not know" would be +-- uninteresting. Note what is *not* claimed: knowing that φ holds does not give +-- knowledge of φ; only what the observation fixes is known.) +---------------------------------------------------------------------- + +knows-observation : ∀ a x → Knows a (λ y → observe a y ≡ observe a x) x +knows-observation a x y eq = eq + +---------------------------------------------------------------------- +-- Theorem 2. Ignorance is a proposition: if a world looks the same to an agent +-- but its store differs, that agent does not know what the store holds. +---------------------------------------------------------------------- + +different-store-unknown : + ∀ a x x' → observe a x' ≡ observe a x → content x' ≢ content x → + ¬ Knows a (λ y → content y ≡ content x) x +different-store-unknown a x x' eq neq k = neq (k x' eq) + +---------------------------------------------------------------------- +-- Theorem 3. Two worlds, same observation, different content: the adversary +-- does not know the stored value. This is the shape ledger row E-1 could not +-- take in the Idris model, where `Knows Adversary a` had no constructor. +---------------------------------------------------------------------- + +private + one≢two : suc zero ≡ suc (suc zero) → ⊥ + one≢two () + +-- Two worlds that differ only in what the store holds, and in nothing the +-- adversary can observe: its channel is empty in both. +x₁ : World +x₁ = w (λ _ → just (suc zero)) (λ _ _ → true) (λ _ → []) + +x₂ : World +x₂ = w (λ _ → just (suc (suc zero))) (λ _ _ → true) (λ _ → []) + +adversary-ignorant : ¬ Knows adversary (λ y → content y ≡ content x₁) x₁ +adversary-ignorant k = + one≢two (just-inj (sym (cong (λ f → f zero) (k x₂ refl)))) + +---------------------------------------------------------------------- +-- Theorem 4. Obliteration cuts recovery: after obliterating h the store holds +-- nothing at h, so there is nothing for any agent to recover. +---------------------------------------------------------------------- + +obliterate : ContentHash → World → World +obliterate h x = + record x { content = λ k → if k == h then nothing else content x k } + +obliterate-cuts-recovery : ∀ h x → ¬ Recovers (obliterate h x) h +obliterate-cuts-recovery h x (c , p) = + nothing≢just (subst (λ b → (if b then nothing else content x h) ≡ just c) + (==-refl h) p) + +---------------------------------------------------------------------- +-- Theorem 5. Obliteration does not make the adversary any wiser: the store +-- changes and its observation does not, so the ignorance of Theorem 3 survives +-- the obliteration. Stated at h = 0 for a closed proof. +---------------------------------------------------------------------- + +obliterate-ignorance : + ¬ Knows adversary (λ y → content y ≡ content (obliterate zero x₁)) + (obliterate zero x₁) +obliterate-ignorance k = + adversary-so-blind (cong (λ f → f zero) (k x₂ refl)) + where + -- `content x₂ zero` is `just 2`; after obliterating 0 the store's entry is + -- `nothing`. Congruence gives an equation between them, which is absurd. + adversary-so-blind : just (suc (suc zero)) ≡ nothing → ⊥ + adversary-so-blind = just≢nothing + +---------------------------------------------------------------------- +-- Theorem 6. Rotation forgets: after rotating old -> new with old ≠ new, no agent can use the +-- old key, including the system. This is the statement the Idris model could +-- not make at all, because `Knows` had no negative form. +---------------------------------------------------------------------- + +rotate : KeyId → KeyId → World → World +rotate old new x = + record x { usable = λ a k → + if k == new then true + else (if k == old then false else usable x a k) } + +rotate-keeps-new : ∀ a old new x → usable (rotate old new x) a new ≡ true +rotate-keeps-new a old new x rewrite ==-refl new = refl + +rotate-forgets-old : + ∀ a old new x → (old == new) ≡ false → + usable (rotate old new x) a old ≡ false +rotate-forgets-old a old new x neq rewrite neq | ==-refl old = refl + +rotate-forgets-canUse : + ∀ a old new x → (old == new) ≡ false → ¬ CanUse (rotate old new x) a old +rotate-forgets-canUse a old new x neq p = + false≢true (trans (sym (rotate-forgets-old a old new x neq)) p) + +---------------------------------------------------------------------- +-- What is NOT claimed. +-- +-- * This is a model of *channels*, not of cryptography. That the store's +-- `content` channel is the only one an attacker has, that a hash does not +-- leak its content, and that a key that is not `usable` cannot be used to +-- decrypt are assumptions about the implementation, not theorems here. +-- Ledger row X-1 carries them. +-- * The adversary's observation `see` is modelled but not yet *filtered* by +-- obliteration: obliterate changes the store channel and leaves the +-- observation channel alone, which is exactly why Theorem 5 is available +-- and also its limit. Removing the entry from every agent's observation is +-- the next increment, and it needs a list-filtering lemma that this module +-- does not have. +-- * Key ids are Nat and `usable` is a Bool. Nothing here says a usable key +-- actually decrypts anything. +-- * Time, partial knowledge, and probabilistic leakage are out of scope. +----------------------------------------------------------------------