Identity from code, proof grades under mathesis, and the epistemic proof rewritten in Agda

.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

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
 

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)

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)