diff --git a/.machine_readable/descriptiles/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml index 26858c2..b1540ae 100644 --- a/.machine_readable/descriptiles/AGENTIC.a2ml +++ b/.machine_readable/descriptiles/AGENTIC.a2ml @@ -7,7 +7,7 @@ repository = "hyperpolymath/epistemic-types" author = "Jonathan D.A. Jewell (hyperpolymath) " version = "0.1.0" status = "prototype" -last-updated = "2026-11-01" +last-updated = "2026-11-07" [agent-permissions] can-edit-source = true # Agda modules under src/EpistemicTypes/ @@ -57,10 +57,10 @@ release-claim-requires-hard-pass = true [verification] # The single source of truth for "does it hold". command = "just check" -underlying = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh" +underlying = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh && bash tests/check-approval-seal-mutations.sh" agda-version = "2.6.4.3" entrypoint = "scripts/check.sh (recursive source gate; All.agda is the aggregate module)" -expected = "22 source modules accepted, 13 intended rejections, strict profile/import/escape-hatch policy and planted-postulate control pass" +expected = "25 source modules accepted, 19 intended rejections, strict profile/import/escape-hatch policy and planted-postulate control pass" [automation-hooks] # on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml. diff --git a/.machine_readable/descriptiles/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml index 10af825..89bb8e9 100644 --- a/.machine_readable/descriptiles/ECOSYSTEM.a2ml +++ b/.machine_readable/descriptiles/ECOSYSTEM.a2ml @@ -5,7 +5,7 @@ project = "epistemic-types" ecosystem = "hyperpolymath" version = "0.1.0" status = "prototype" -last-updated = "2026-11-01" +last-updated = "2026-11-07" [position] type = "formal-methods-library" @@ -17,7 +17,7 @@ options = "--safe --without-K --cubical-compatible; source also declares --exact libraries = "core: none — --no-libraries against Agda.Builtin.*, Agda.Primitive and local modules; optional CanonicalEcho integration has pinned external source/stdlib" machine-readable = "a2ml + Nickel/k9" docs = "AsciiDoc" -check = "just check == policy inventory/negative control + all 22 source modules + all 13 expected rejections" +check = "just check == policy inventory/negative control + all 25 source modules + all 19 expected rejections" notes = "Single-tool Agda library. The core has no runtime dependencies; CI uses a pinned Debian verification container." [core] @@ -28,6 +28,7 @@ modules = [ "EpistemicTypes.Warrant — Warrant / Epi / SoundWarrant", "EpistemicTypes.Access — Preorder + AccessibleModality transport 'increase'", "EpistemicTypes.EchoBridge — certified residue and separately measured bounds 'Echo C y', kept distinct from E κ A", + "EpistemicTypes.PartialRecovery / PartialRecoveryExamples — pair-only partial recovery, separate success soundness, explicit image decision, fallback totalization and finite boundary controls", "EpistemicTypes.SurrealBridge — SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower", "EpistemicTypes.Examples", "EpistemicTypes.ProofTransport — standpoint-indexed proof transport across trust boundaries", diff --git a/.machine_readable/descriptiles/PLAYBOOK.a2ml b/.machine_readable/descriptiles/PLAYBOOK.a2ml index 52b2847..140df34 100644 --- a/.machine_readable/descriptiles/PLAYBOOK.a2ml +++ b/.machine_readable/descriptiles/PLAYBOOK.a2ml @@ -5,7 +5,7 @@ [metadata] version = "0.1.0" status = "prototype" -last-updated = "2026-11-01" +last-updated = "2026-11-07" repo = "hyperpolymath/epistemic-types" single-tool = "agda" @@ -18,7 +18,7 @@ ci = "Proof and security CI enabled; see docs/ci-safety.adoc" [gate] # The single source of truth for 'is the library healthy?'. command = "just check" -expands-to = "tests/check-policy.sh; tests/check-proofs.sh over all 22 source modules; tests/check-rejections.sh over all 13 fixtures" +expands-to = "tests/check-policy.sh; tests/check-proofs.sh over all 25 source modules; tests/check-rejections.sh over all 19 fixtures; tests/check-approval-seal-mutations.sh over four fixed mutants" agda-version = "2.6.4.3" options = "--safe --without-K --cubical-compatible; source hardening --exact-split --no-sized-types --no-guardedness" dependencies = "core: Agda builtins/primitive and local modules only; optional canonical integration pins Echo source and stdlib" diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index cbcdfa8..7fa411b 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -1,7 +1,7 @@ [metadata] project = "epistemic-types" version = "0.1.0" -last-updated = "2026-11-01" +last-updated = "2026-11-07" status = "prototype" # prototype | active | paused | archived [project-context] @@ -26,17 +26,18 @@ secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the sta checker = "Agda 2.6.4.3 (CI-matched)" command = "just check" entry-point = "scripts/check.sh — local agda when present, else 'guix shell -D -f build/guix.scm -- bash scripts/check.sh'" -expands-to = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh" +expands-to = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh && bash tests/check-approval-seal-mutations.sh" dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'" ci-entry-point = ".github/workflows/agda.yml asserts 'Agda version 2.6.4.3', then runs 'bash scripts/check.sh'" warning-policy = "-W error with only noUnsupportedIndexedMatch disabled: locally for Kripke.Belief's indexed relation elimination and at the pinned external integration boundary. No Cubical transport computation is claimed for those functions." -proof-status = "AGDA-VERIFIED; Mathesis Grade 3. Proof Safety run 41326349568 passed both core/rejection/policy and pinned integration jobs at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Rocq/Lean/bridge legs remain open." +proof-status = "AGDA-VERIFIED; historical hosted receipt below, new local partial-recovery receipt in docs/partial-recovery.adoc. Proof Safety run 41326349568 passed both core/rejection/policy and pinned integration jobs at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Rocq/Lean/bridge legs remain open." aggregator = "src/EpistemicTypes/All.agda imports the full source graph; the recursive gate separately checks every source file, including modules not publicly re-exported." [modules] # Agda modules under src/EpistemicTypes/. list = [ "EpistemicTypes.Access", + "EpistemicTypes.Applications.ApprovalSeal", "EpistemicTypes.Applications.IntegerModel", "EpistemicTypes.Applications.OrderedGroup", "EpistemicTypes.Applications.QCriterion", @@ -53,6 +54,8 @@ list = [ "EpistemicTypes.Kripke.Frame", "EpistemicTypes.Kripke.Indexed", "EpistemicTypes.Kripke.Residual", + "EpistemicTypes.PartialRecovery", + "EpistemicTypes.PartialRecoveryExamples", "EpistemicTypes.ProofTransport", "EpistemicTypes.ProofTransportExample", "EpistemicTypes.ReadConsistency", @@ -65,6 +68,7 @@ base = "Modality / LawfulModality / FactiveModality / BeliefModality / ReturnMod warrant = "Warrant / Epi / SoundWarrant." access = "Preorder + AccessibleModality transport 'increase'." echo-bridge = "Certified residue Echo C y, explicit source compatibility, recovery/migration laws and measured resource bounds; distinct from E κ A." +partial-recovery = "Pair-only partial recovery; success soundness is separate. Sound partial recovery and separation plus explicit image decision construct each other. A chosen source fallback totalizes partial recovery; empty/collision/off-image controls and actual canonical Echo-fibre adapter are checked. See docs/partial-recovery.adoc for local receipt and sibling proposals." surreal-bridge = "SurrealAccess carrier + GradedSurrealModality + daySurrealAccess finite birthday tower." examples = "Worked instances exercising the interfaces." proof-transport = "proofSound derives Meaning holder artifact claim from an accepted sound checker. Receipts alone do not certify; transfer requires the target-holder meaning." @@ -106,7 +110,7 @@ items = [ ] [progress-summary] -note = "Prototype. Authoritative inventory: 22 source modules and 13 expected-rejection fixtures. The map-only core, explicit warrant/factivity boundary, proof transport, store consistency, certified Echo residue with separate measured bounds, finite-day surreal adapter, RapidNJ integer certificate, and scoped constructive Kripke semantics are implemented. The 2026-11-01 canonical profile is --safe --without-K --cubical-compatible; hosted receipt status and Mathesis grade are in PROOF-STATUS.adoc. Open work includes data-dependent warrant soundness, residual owning-record correspondence, lawful instances, rational/rescaling and update obligations, independent Rocq/Lean legs, and runtime refinement." +note = "Prototype. Authoritative inventory: 25 source modules and 19 expected-rejection fixtures. The map-only core, explicit warrant/factivity boundary, proof transport, store consistency, certified Echo residue with separate measured bounds, finite-day surreal adapter, RapidNJ integer certificate, and scoped constructive Kripke semantics are implemented. The 2026-11-01 canonical profile is --safe --without-K --cubical-compatible; hosted/local receipts and the proof-weight grading boundary are in PROOF-STATUS.adoc. Open work includes data-dependent warrant soundness, residual owning-record correspondence, lawful instances, rational/rescaling and update obligations, independent Rocq/Lean legs, and runtime refinement." [blockers-and-issues] # No active blockers. diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index ecc7ace..15f1824 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -4,7 +4,7 @@ title = "epistemic-types — universal AI agent entry point" version = "0.1.0" format = "a2ml" status = "prototype" -last-updated = "2026-11-01" +last-updated = "2026-11-07" [project] name = "epistemic-types" @@ -36,12 +36,12 @@ format = "AsciiDoc (.adoc) is the default. README.adoc is the overview, explainm machine-readable-location = "Project specifications live under .machine_readable/. The root 0-AI-MANIFEST.a2ml universal pointer and coordination.k9 session entry point are the explicit operational exceptions." license = "MPL-2.0" build = "just check" -build-expansion = "bash scripts/check.sh → policy gate + all 22 source modules + all 13 expected rejections" +build-expansion = "bash scripts/check.sh → policy gate + all 25 source modules + all 19 expected rejections + four approval-seal mutation controls" agda-options = "--safe --without-K --cubical-compatible plus source hardening --exact-split --no-sized-types --no-guardedness; -W error with UnsupportedIndexedMatch disabled only alongside an exact 23-source-span audit; no postulates; core imports only builtins/primitive/local modules" agda-version = "2.6.4.3" echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality." ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc" -proof-status = "AGDA-VERIFIED; Mathesis Grade 3. Canonical Proof Safety receipt 41326349568 at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Independent Rocq/Lean/bridge legs remain open." +proof-status = "AGDA-VERIFIED; historical hosted receipt below, new local partial-recovery receipt in docs/partial-recovery.adoc. Canonical Proof Safety receipt 41326349568 at checked revision bf9c75a38794d744ce466574e6323062e7d22533. Independent Rocq/Lean/bridge legs remain open." secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone production home (D153/D154). Do not add a Secret API, IFC implementation or confidentiality theorem here. #29 stays closed; #32 closed on 2026-10-05 with no transfer and must not be reopened/duplicated (guard #39). Source-reviewed at standalone f581f8295bdee854f76291ab884a16cc8114dc6f on 2026-11-01: generic TINI and its two-point instance are PROVEN; termination-sensitive noninterference and declassification remain OPEN. No theorem is imported here." [first-run] @@ -55,6 +55,7 @@ aggregator = "src/EpistemicTypes/All.agda" modules = [ "EpistemicTypes.Access", "EpistemicTypes.All", + "EpistemicTypes.Applications.ApprovalSeal", "EpistemicTypes.Applications.IntegerModel", "EpistemicTypes.Applications.OrderedGroup", "EpistemicTypes.Applications.QCriterion", @@ -70,6 +71,8 @@ modules = [ "EpistemicTypes.Kripke.Frame", "EpistemicTypes.Kripke.Indexed", "EpistemicTypes.Kripke.Residual", + "EpistemicTypes.PartialRecovery", + "EpistemicTypes.PartialRecoveryExamples", "EpistemicTypes.ProofTransport", "EpistemicTypes.ProofTransportExample", "EpistemicTypes.ReadConsistency", @@ -82,6 +85,7 @@ Base = "Modality / LawfulModality / FactiveModality / BeliefModality / ReturnMod Warrant = "Warrant / Epi / SoundWarrant — explicit warrant objects." Access = "Preorder plus AccessibleModality transport ('increase') across the access preorder." EchoBridge = "Certified Echo C y residues, explicit migration/recovery and separately measured resource bounds." +PartialRecovery = "Pair-only Maybe decoder, separate success soundness, constructive image-decision characterization, explicit fallback totalization and finite boundary controls; see docs/partial-recovery.adoc." SurrealBridge = "SurrealAccess carrier plus GradedSurrealModality plus daySurrealAccess finite-birthday tower." Examples = "Worked instances of the abstract interfaces." ProofTransport = "Standpoint-indexed proof transport across trust boundaries." @@ -112,7 +116,7 @@ step-3 = "Read .machine_readable/descriptiles/META.a2ml for architecture and des step-4 = "Read .machine_readable/descriptiles/ECOSYSTEM.a2ml for ecosystem position and sibling repos." step-5 = "Read .machine_readable/descriptiles/AGENTIC.a2ml, NEUROSYM.a2ml, and PLAYBOOK.a2ml for agent guidance." step-6 = "Read README.adoc and explainme.adoc for the human-facing overview." -step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or Guix/dev container) to enforce policy, check all 22 source modules and validate all 13 expected rejections before and after changes." +step-7 = "Run 'just check' (→ scripts/check.sh: local Agda or Guix/dev container) to enforce policy, check all 25 source modules and validate all 19 expected rejections plus four mutation controls before and after changes." [policy] rules = [ diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9398fd7..b5bfa25 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = epistemic-types — proof needs -:revdate: 2026-11-04 +:revdate: 2026-11-07 :toc: This queue records only obligations that remain relevant to this repository. @@ -27,8 +27,11 @@ planted-postulate negative control | CLOSED — run `41326349568` | CLOSED — run `41326349568` |=== -Closing P0 establishes Mathesis Grade 3 for the checked Agda revision. It does -not establish independent cross-prover agreement. +The P0 receipts establish `AGDA-VERIFIED` for their checked revisions, not +independent cross-prover agreement. The earlier "Mathesis Grade 3" label is +distinct from the canonical PWG vocabulary; see the policy clarification in +link:PROOF-STATUS.adoc[]. The new partial-recovery local receipt is separate +from these historical hosted runs. == P1 — theorem-level independent rechecks @@ -50,8 +53,14 @@ modality, totality, and assumption translations | BRIDGE-PENDING than weakening the Agda statement | OPEN |=== -No Grade 2i, Grade 2ii, Grade 1, or `RECONCILED` claim is made until the -applicable rows close. +No independent prover or `RECONCILED` claim is made until the applicable rows +close. For a bounded next translation, PR-1/PR-2/C-4 in the proof ledger now +identify the partial-recovery statements: `Set` carriers, builtin intensional +equality, untruncated Sigma fibres, pair-only Maybe decoding, separate success +soundness, an explicit image decision and an explicit fallback source where +used. The checked source and full assumptions are in +link:docs/partial-recovery.adoc[]. Translating those exact statements and +comparing their propositions in Rocq/Lean remains OPEN. == P2 — local mathematical obligations diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index d13809f..025df4b 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -6,10 +6,10 @@ [abstract] This is the current, source-anchored verification record for the Agda -formalisation. The authoritative positive tree contains *23 source modules* and -the negative-control manifest contains *17 expected-rejection fixtures*. The -2026-11-03 extension adds one module and four fixtures to the previous verified -22-module/13-fixture baseline, plus four isolated mutation controls. The +formalisation. The authoritative positive tree contains *25 source modules* and +the negative-control manifest contains *19 expected-rejection fixtures*. The +partial-recovery extension adds two modules and two fixtures to the preceding +23-module/17-fixture corpus, retaining four isolated mutation controls. The source is constructive, builtins-only, map-only at its base interface, and has no postulates or proof escape hatches. Exact theorem scope and trust boundaries are recorded below; historical snapshots remain in `AFFIRMATION.adoc` and are @@ -17,6 +17,19 @@ not current inventory. == Status vocabulary +The partial-recovery extension is locally *AGDA-VERIFIED* by the complete +Agda 2.6.4.3 core gate: 25 source modules, 19 intended rejections and four +mutation controls, with the existing exact 23-span warning manifest unchanged. +`PartialRecovery` and separate `SuccessSound` construct separation and an +image decision; conversely those two obligations construct sound partial +recovery. An explicit fallback totalizes it. No new warning exemption, +independent-review credit or cross-prover result is claimed. The canonical +fibre integration passed under Agda 2.6.4.3/stdlib 2.1 and separately under +Agda 2.7.0.1/stdlib 2.3. Its detailed local receipt is recorded in +link:docs/partial-recovery.adoc[]. + +The following paragraphs are historical receipts for the preceding corpus. + The 2026-11-07 optional recovery integration adds `tests/integration/CanonicalRecovery.agda` and `RecoveryExamples.agda`. It is locally *AGDA-VERIFIED* under the native Agda 2.6.4.3 / stdlib 2.1 @@ -79,7 +92,7 @@ its 23 existing warning spans are checked separately against the exact manifest in `tests/check-proofs.sh`. A new, moved, or stale location fails the gate. The safe proofs check, but no Cubical transport-computation claim is made for those indexed eliminations, including `Kripke.Belief.believed`. The policy gate also -compares all 23 source modules, 17 rejection fixtures, and three integration +compares all 25 source modules, 19 rejection fixtures, and four integration witnesses with exact path manifests; rejects additional `OPTIONS` pragmas, proof escape hatches, and non-core imports; and verifies a generated negative control: `--safe` must reject a planted postulate with Agda's expected @@ -110,11 +123,10 @@ passed with Agda 2.6.4.3. The core job ran the policy preflight, all 22 source modules, and all 13 intended rejections; the separate integration job checked the pinned Echo witness. -Current profile status: `AGDA-VERIFIED`; the checked revision is *Mathesis -Grade 3*. The immediately following status/metadata receipt update changes no -Agda source, fixture, gate, option, or dependency pin and is itself rerun by the -same PR workflow. No missing tool, import failure, or unexpected rejection -counts as a pass. +That hosted revision is `AGDA-VERIFIED`; the earlier ledger called it +"Mathesis Grade 3". The canonical policy uses PWG labels, as clarified below, +and the receipt covers its exact revision. No missing tool, import failure, +or unexpected rejection counts as a pass. == Approval-seal hosted receipt @@ -242,7 +254,7 @@ external runtime or an unlisted mathematical correspondence. | Documentary comparison only; no imported owning definition | C-1 -| Every one of the 17 intended-invalid constructions is rejected for its +| Every one of the 19 intended-invalid constructions is rejected for its enumerated semantic type mismatch. This is negative-control evidence, not a positive theorem. | TESTED @@ -266,6 +278,28 @@ external runtime or an unlisted mathematical correspondence. | PROVEN — local receipt 2026-11-07 | `tests/integration/CanonicalRecovery.agda`, `RecoveryExamples.agda`; link:docs/echo-recovery-adapter.adoc[assumptions and verification scope] + +| PR-1 +| Pair-only partial recovery implies source separation; total recovery + constructs partial recovery; an explicit source fallback totalizes it. + Empty-source and collision counterexamples delimit those constructions. +| PROVEN — local receipt 2026-11-07 +| `PartialRecovery.agda`, `PartialRecoveryExamples.agda` + +| PR-2 +| Partial recovery plus separate success soundness constructs separation and + an image decision. Conversely, these two obligations construct sound + partial recovery. These are mutual existence implications, not inverse + record equalities; all carriers are Set and fibres are untruncated. +| PROVEN — local receipt 2026-11-07 +| `PartialRecovery.agda`; link:docs/partial-recovery.adoc[exact assumptions] + +| C-4 +| The local retained-pair image is definitionally canonical `Echo` of the + retained-pair function. Conversions preserve the source and equality path; + the canonical image decision constructs the checked finite partial decoder. +| PROVEN — local receipt 2026-11-07 +| `tests/integration/CanonicalPartialRecovery.agda`, `RecoveryExamples.agda` |=== == External pinned evidence, not local closure @@ -283,12 +317,16 @@ The current cross-repository status statements in `docs/what-epistemic-is.adoc` are documentary pointers. They are not imports, build dependencies, or independent proof legs for this repository. -== Mathesis grade and independent proof legs +== Proof-weight grading and independent proof legs -Mathesis Grade 3 means that the Agda source checks under the strict profile at a -recorded revision, without an independent foundational translation. Hosted run -`41326349568` closes that requirement for checked revision `bf9c75a`; this -proof corpus is *Mathesis Grade 3*. +Earlier receipts used "Mathesis Grade 3" for one Agda verification leg. +The https://github.com/metadatastician/standards/blob/b8f60511e76c9015d86990317162dce653c92fe1/3-practice/PROOF-POLICY.adoc[owning standards proof policy, section 8] +uses the canonical labels `PWG-3`, +`PWG-2i`, `PWG-2ii` and `PWG-1`. Mathesis is a discovery index; its separate +architecture proposal does not override the standards policy. This extension +records `AGDA-VERIFIED` for the explicitly checked source and profile, without +claiming a new PWG assessment, policy completion, independent review or +cross-prover reconciliation. No theorem in this repository currently has a theorem-by-theorem Rocq or Lean leg with an exact statement comparison: @@ -296,9 +334,9 @@ leg with an exact statement comparison: [cols="2,1,3",options="header"] |=== | Leg | Status | Consequence -| Agda canonical profile | AGDA-VERIFIED | Grade 3 receipt: run `41326349568`, revision `bf9c75a` -| Rocq/Coq | OPEN / NOT-INVENTORIED | No Grade 2i/2ii credit -| Lean | OPEN / NOT-INVENTORIED | No Grade 2i/2ii credit +| Agda canonical profile | AGDA-VERIFIED | Exact hosted and local receipts above; no automatic coverage of later edits +| Rocq/Coq | OPEN / NOT-INVENTORIED | No independent prover credit +| Lean | OPEN / NOT-INVENTORIED | No independent prover credit | Proposition/semantics bridge | BRIDGE-PENDING | No claim of reconciliation | Runtime refinement | OPEN | Model theorems do not verify an implementation |=== @@ -322,6 +360,6 @@ not inferred from the Mathesis grade. * Full Conway-surreal semantics, full graded-loss/comonad semantics, external store/scheduler/attestation/runtime refinement, and physical guarantees. * The theorem-level Rocq and Lean inventory, independent checks, and explicit - proposition bridges needed for Mathesis Grade 2 or stronger. + proposition bridges needed for an independently reconciled result. See `PROOF-NEEDS.adoc` for the executable next-proof queue. diff --git a/README.adoc b/README.adoc index d06a261..4442495 100644 --- a/README.adoc +++ b/README.adoc @@ -228,7 +228,7 @@ This is a prototype, not a complete epistemic logic. The following are **intenti [source,bash] ---- -just check # policy guard + 22 positive modules + 13 expected rejections +just check # policy guard + 25 positive modules + 19 expected rejections + 4 mutation controls ---- `just check` calls `scripts/check.sh`: it uses a local `agda` when one is on diff --git a/docs/README.adoc b/docs/README.adoc index f0e71e2..f8d7841 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -65,6 +65,12 @@ authority. == Continuity foundations +link:partial-recovery.adoc[] defines recovery from the visible/residue pair +with possible failure, the separate success-soundness law, the constructive +image-decision boundary, explicit fallback totalization and canonical fibre +correspondence. It includes finite counterexamples and a pinned sibling +source review with proposed follow-ups kept separate from checked adapters. + link:continuity-foundations.adoc[] documents store-coherent reads, certified residues, source compatibility, migration sufficiency, resource bounds, and the optional canonical Echo integration gate. @@ -112,8 +118,8 @@ link:applications/rapidnj-q-criterion.adoc[]. == Notes * `Echo C y`, `BoundedEcho C measure budget y`, and `E κ A` have separate roles. -* `just check` enforces the policy profile, checks all 22 source modules - (including applications and Kripke), and validates 13 semantic rejection - fixtures. +* `just check` enforces the policy profile, checks all 25 source modules + (including applications and Kripke), validates 19 semantic rejection + fixtures, and runs four mutation controls. * `just check-canonical` separately checks correspondence against actual sibling Echo sources; it requires an explicit standard-library source path. diff --git a/docs/partial-recovery.adoc b/docs/partial-recovery.adoc new file mode 100644 index 0000000..54c89b3 --- /dev/null +++ b/docs/partial-recovery.adoc @@ -0,0 +1,246 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Partial recovery from the retained pair +:revdate: 2026-11-07 + +== Problem and exact contract + +`EchoBridge.Recovery C` requires a total decoder on every visible/residue +pair, including pairs that no source produces. The optional canonical +adapter identifies that existing contract with Echo's `ExactRecovery`. +The new `EpistemicTypes.PartialRecovery` module adds a separate contract: + +[source,agda] +---- +decode : B -> R -> Maybe A +roundtrip : (x : A) -> decode (observe x) (retain x) ≡ just x +---- + +The decoder receives only the visible value and residue. It receives no +source, certificate or inhabitant of a fibre. All carriers are `Set`; the +existing `Retention A B R`, including its arbitrary certificate family, +stays fixed. The new theorem does not infer recovery from certificate +validity and does not turn a standpoint into an access-control label. + +`PartialRecovery` alone says nothing about successful decoding at an +unreachable pair. `SuccessSound rec` is the separate law that every +successful output reproduces the input pair. Keeping these laws separate +is necessary: converting an arbitrary total recovery to `just` preserves +the source round trip but can succeed on an unreachable input. + +This is standard constructive mathematics about left inverses and +decidable images. The contribution is a checked API boundary and its +correspondence with the owning Echo definition, not a new fibre theorem, +a novel type primitive or a claim of minimum information cost. + +== Constructive characterization + +Write `pair x = (observe x, retain x)`. The module defines: + +* `Image C y r = Σ A (λ x -> pair x ≡ (y , r))`, an ordinary + proof-relevant fibre containing an actual source and an equality path. +* `Separates C`: equal retained pairs imply equal sources. +* `ImageDecision C`: for each pair, return either a concrete inhabitant of + its fibre or a function refuting every inhabitant. + +The following constructive maps prove both existence implications between +a partial recovery with `SuccessSound` and the pair of obligations +`Separates C` and `ImageDecision C`: + +[cols="2,4",options="header"] +|=== +|Declaration |Proved obligation +|`partialSeparates` +|Every partial recovery separates sources. The proof uses the decoder's +two round trips and injectivity of `just`. +|`soundPartialDecidesImage` +|Partial recovery plus success soundness decides the fibre: `just x` +supplies the source and matching path; `nothing` contradicts the round trip +of any proposed source witness. +|`fromImageDecision` +|Separation plus an explicit image decision constructs partial recovery. +A positive decision chooses a source internally; separation proves that +the chosen source equals the original on every generated pair. +|`imageDecisionSound`, `imageDecisionComplete` +|For this construction, successful output exactly corresponds to a +matching source. Completeness recovers every supplied inhabitant of the +fibre; soundness returns the matching equality for each successful output. +|=== + +These are existence constructions, not inverse equalities between records, +decision procedures or proof fields. No equality of all certificates or +equality paths, proof irrelevance, function extensionality, choice axiom, +propositional truncation or quotient is assumed. Image decidability does +not follow from separation, a certificate, or the name of the retention +contract. A concrete decision procedure is an explicit input. + +The proof-relevant image is useful as a specification, but its projection +is not a decoder from the pair alone. Even a constant map on two sources +has witnesses containing either source. `witnessProjectionRoundtrip` +checks this trivial projection; `witnessProjectionDependsOnWitness` and +`noCollidingPartial` show why it cannot establish the pair-only contract. + +== Totality and its boundary + +`totalToPartial` wraps the existing total decoder in `just`. +`partialToTotal` fills failed outputs with a caller-supplied source +`fallback : A`. The source round trip ensures that the fallback is never +used on a generated pair. `totalPartialDecoder` proves that converting an +existing total decoder to partial and back preserves all its outputs, +pointwise, including off-image outputs. + +The opposite composition may replace `nothing` with `just fallback`; +no two-sided isomorphism is claimed. A fallback is sufficient, not asserted +to be necessary for every possible carrier. In particular, an empty source +with inhabited visible/residue space admits an always-failing partial +recovery but no total recovery. This refutes unconditional totalization. + +== Executable finite controls + +`PartialRecoveryExamples.agda` checks the complete two-Boolean visible +space with source `Bool` and a singleton residue. Observation sends `b` +to `(b, false)`. An explicit image decision succeeds on the two generated +pairs and rejects the two unreachable pairs. The decoder and reconstructed +image decision reduce on both branches. Two fallback choices agree on all +generated pairs and differ off-image. + +The same module also proves: + +* Empty-source partial recovery exists while total recovery is impossible. +* Constant observation and residue on `Bool` forbid every partial recovery, + even though every generated residue is certified and witness projection + has a trivial round trip. +* A valid total decoder wrapped in `just` succeeds on an unreachable input + whose returned source is incompatible with that input. + +The expected-rejection gate includes `CollidingPartialRecovery` and +`PartialSuccessProvesImage`. They must reach their intended Boolean type +mismatch with Agda exit 42; a tool, import or parse failure does not count. +These finite controls supplement the generic proofs. They do not claim +runtime refinement or performance bounds. + +== Canonical ownership and sibling boundaries + +`tests/integration/CanonicalPartialRecovery.agda` imports the actual +`Echo.Echo` and identifies `Image C y r` with +`Echo (retainedPair C) (y , r)` by definitional equality. The two conversions +and their record-free inverse laws preserve the particular source and path. +`fromCanonicalDecision` uses a decision over that owning fibre. The existing +`RecoveryExamples` root executes its finite generated and unreachable cases. +Echo acquires no Epistemic dependency; the builtins-only core imports no +standard library or sibling module. + +The following source review guides bounded future work. Only the Echo and +Epistemic imports above are compiled by this bridge's checks. These sibling +observations are not imported theorem claims or completed adapters. + +[cols="1,2,3",options="header"] +|=== +|Owning source |Observed boundary |Possible next operation +|https://github.com/hyperpolymath/Mathesis/blob/1a582f2e860bb395207b4b181f9fdfb2fa313fa8/README.adoc[Mathesis README] +|Discovery index; textual census candidates are not kernel verdicts. +|Index exact theorem, assumption and checker receipts after validation. +|https://github.com/hyperpolymath/residual-evidence-types/blob/14c93f4e19aaacbcfeca91bf5f2368d3e7b5a4bc/src/ResidualEvidence/Core.agda[Residual Evidence Core] +|Candidates refine an observation fibre by evidence; `Case` carries a +consistency witness, and `Identified` requires agreement of all candidates. +|An adapter from pair separation to source identification for an inhabited +Case over that pair observation. A Case witness is not a recovery algorithm. +|https://github.com/hyperpolymath/choreographic-types/blob/5a2a6cf1c657d7819558bf38b85ed11e2170ad1b/src/Choreographic/AsyncKnowledge.agda[Choreographic AsyncKnowledge] +|Delivered and in-flight worlds can have the same sender view. +|With an explicitly identical residue, instantiate a collision obstruction +for whole-world recovery. A target-relative query needs its own statement. +|https://github.com/hyperpolymath/secret-types/blob/42ac315bc8ec1f8d9ce30e4b8d97c02830645bd9/src/SecretTypes/Witness.agda[Secret Types Witness] +|Termination-insensitive noninterference does not identify the observable +`nothing`/`just` behaviour of a secret-dependent loop. +|A security adapter must state two-run observations, including whether +decoding success is visible. Partial recovery is no confidentiality theorem. +|https://github.com/hyperpolymath/tropical-types/blob/168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5/Resource/EchoBridge.lean[Tropical EchoBridge] +|Resource measurement has separate `measure_empty`/`measure_combine` laws. +Its residue carrier has no associativity/identity fields despite monoid wording. +|Review that wording or supply carrier laws separately. Equal measured cost +does not imply recoverability; no Tropical code is changed here. +|=== + +Confidentiality, declassification, historical provenance, source ownership, +linear consumption and independent Rocq/Lean correspondences remain separate +obligations. Ordinal research is outside this cycle. + +== Reproduction + +Epistemic base: `b2ebe09832814cdb6330742f9a5fccad97651c8d`. +Canonical Echo pin: `ebde9ac4e1a9f115b441c642c82aced1316c5983`. +The integration workflow's pin and toolchain remain unchanged. + +[source,shell] +---- +bash scripts/check.sh +bash scripts/check-canonical.sh /path/to/echo-types /path/to/stdlib/src +---- + +The core gate checks every source root with interfaces ignored, all expected +semantic rejections, policy controls and four existing mutation controls. +The canonical command cold-checks the complete four-module integration +closure. Each first-party source retains all six strict local options. +The existing indexed-match warning boundary is not a warning-free Cubical +transport-computation claim. + +== Local verification receipt — 2026-11-07 + +The base core gate was reproduced before editing: 23 source modules, +17 intended semantic rejections, the exact 23-span warning audit and all +four approval-seal mutants passed. The candidate core gate passed with +25 source modules, 19 intended semantic rejections and the same four mutants. +The exact 23-span warning manifest is unchanged. The policy gate covers +all four integration modules; no proof option or warning exception was added. + +The complete `RecoveryExamples` integration closure passed natively with: + +* Debian `agda-bin=2.6.4.3-1+b2` and `agda-stdlib=2.1-4`. +* Agda `2.7.0.1` and standard library `2.3` at + `8326c7475af1fa456ca04a0203c168d5d7ff842b`. + +Both runs used the canonical Echo pin above, `--no-libraries --safe +--without-K --cubical-compatible --double-check --ignore-interfaces +-W error -W noUnsupportedIndexedMatch`, the explicit `src` and +`tests/integration` include roots, and the pinned Echo and standard-library +source roots. First-party files retain their strict local options. These +are native WSL Debian executions, not executions of the pinned CI container. +The private writable standard-library 2.1 copy has an Agda-source manifest +identical to the installed Debian package. + +A separate unsuppressed cold run of that complete closure under Agda +2.6.4.3 also passed. It reported 776 `UnsupportedIndexedMatch` occurrences +at 161 unique spans; none is in either new core module or the new canonical +adapter. This matches the preceding integration receipt's counts; repeated +occurrences are not independent defects. The compiler's observed `Checking` +cone contains 148 distinct modules; the retained manifest records each path +and source digest, with compiler builtins belonging to the recorded toolchain. +These diagnostics are not a claim of warning-free Cubical computation. + +The checked native sources, secondary-profile sources and working sources +were compared byte-for-byte after LF normalization. Key SHA256 values: + +[cols="2,3",options="header"] +|=== +|Source |SHA256, LF-normalized +|`src/EpistemicTypes/PartialRecovery.agda` +|`a42d6f7a58c808b9cb12f8d455faa309997f887a70739429f1c5c8f90d542995` +|`src/EpistemicTypes/PartialRecoveryExamples.agda` +|`ca21fad6366459fdffaed8558fecda8fdecdad57a5130b0b2ed2dd06cb7ad862` +|`tests/integration/CanonicalPartialRecovery.agda` +|`ee893ff0793112f8938c5ab08f7a03df533a63a3864c4bcf395b91c59c414754` +|`tests/integration/RecoveryExamples.agda` +|`6272ae42fe347cc10e33900c894f33c36b3440fb0ba0ae84addcf91297019f99` +|=== + +The candidate core log SHA256 is +`d223de07eecdf0549d7d93f9443eb49db7b9570dcec6f837f9831328510df0d9`; +the complete unsuppressed integration log SHA256 is +`4fd07b2d2757a9dbc30fecdc9e25be99176061391b7c8be783cf2bd23a849a03`. +Logs, the import cone, the source manifests, the warning spans and command +records are retained in the coordinating workspace's +`bridge-cycle-20261107/foundation-receipt/`. Those are local artifacts, not +remotely accessible links. The commands, pins, hashes and scope above are +the distributable receipt. Hosted checks of the published candidate, +independent review, Rocq and Lean rechecks and proposition reconciliation +remain separate obligations; this local receipt does not imply their success. diff --git a/scripts/check-canonical.sh b/scripts/check-canonical.sh index bea198d..a1bb777 100644 --- a/scripts/check-canonical.sh +++ b/scripts/check-canonical.sh @@ -22,9 +22,9 @@ done # Success does not assert Cubical transport computation for indexed matches. # Each first-party module also declares exact-split/no-sized-types/no-guardedness. # Do not impose those local options on the independently maintained stdlib. -# RecoveryExamples imports both CanonicalEcho and CanonicalRecovery: one cold -# closure checks all three policy-manifest modules without rechecking the -# same standard library three times. +# RecoveryExamples imports CanonicalEcho, CanonicalRecovery and +# CanonicalPartialRecovery: one cold closure checks all four policy-manifest +# modules without rechecking the same standard library four times. "$prover" --no-libraries --safe --without-K --cubical-compatible \ --double-check --ignore-interfaces \ -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \ diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda index bce43d0..332fc5c 100644 --- a/src/EpistemicTypes/All.agda +++ b/src/EpistemicTypes/All.agda @@ -11,6 +11,8 @@ import EpistemicTypes.Kripke.Belief import EpistemicTypes.Kripke.Residual import EpistemicTypes.Kripke.Dependence open import EpistemicTypes.EchoBridge public +import EpistemicTypes.PartialRecovery +import EpistemicTypes.PartialRecoveryExamples -- Imported (checked) but NOT re-exported publicly: ReadConsistency keeps -- its own self-contained ⊥/¬_ (matching the Examples.agda convention), -- which would clash with Examples' identically-named helpers if both were diff --git a/src/EpistemicTypes/PartialRecovery.agda b/src/EpistemicTypes/PartialRecovery.agda new file mode 100644 index 0000000..b529737 --- /dev/null +++ b/src/EpistemicTypes/PartialRecovery.agda @@ -0,0 +1,154 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +module EpistemicTypes.PartialRecovery where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Maybe using (Maybe; just; nothing) +open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd) +open import EpistemicTypes.EchoBridge using (Retention; Recovery; Impossible) + +withDefault : {A : Set} -> A -> Maybe A -> A +withDefault fallback nothing = fallback +withDefault fallback (just x) = x + +private + sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x + sym refl = refl + + trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z + trans refl q = q + + cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y + cong f refl = refl + + eliminate : {A : Set} -> Impossible -> A + eliminate () + + justInjective : {A : Set} {x y : A} -> just x ≡ just y -> x ≡ y + justInjective {x = x} = cong (withDefault x) + + nothingNotJust : {A : Set} {x : A} -> nothing ≡ just x -> Impossible + nothingNotJust () + +retainedPair : {A B R : Set} -> Retention A B R -> A -> Σ B (λ _ -> R) +retainedPair C x = Retention.observe C x , Retention.retain C x + +-- This is the standard proof-relevant fibre of the retained-pair function. +-- Its witness CONTAINS a source; projecting that source is not recovery +-- from the visible/residue pair alone. The optional canonical adapter +-- identifies this definition with the owning Echo.Echo, without truncation. +Image : {A B R : Set} -> Retention A B R -> B -> R -> Set +Image {A} C y r = Σ A (λ x -> retainedPair C x ≡ (y , r)) + +Separates : {A B R : Set} -> Retention A B R -> Set +Separates {A} C = {x z : A} -> retainedPair C x ≡ retainedPair C z -> x ≡ z + +-- A decoder is a function of the retained pair ONLY. It receives neither +-- a source witness nor a certificate. Failure is allowed off the image. +-- Roundtrip does NOT require failure off the image: a successful result +-- there need not reproduce its input pair. Soundness is a separate property. +record PartialRecovery {A B R : Set} (C : Retention A B R) : Set where + field + decode : B -> R -> Maybe A + roundtrip : (x : A) -> + decode (Retention.observe C x) (Retention.retain C x) ≡ just x + +totalToPartial : {A B R : Set} {C : Retention A B R} -> + Recovery C -> PartialRecovery C +PartialRecovery.decode (totalToPartial rec) y r = just (Recovery.recover rec y r) +PartialRecovery.roundtrip (totalToPartial rec) x = cong just (Recovery.roundtrip rec x) + +-- The fallback is explicit data, not an assumed inhabitant or a choice +-- principle. It is irrelevant on generated pairs by the roundtrip law. +partialToTotal : {A B R : Set} {C : Retention A B R} -> + A -> PartialRecovery C -> Recovery C +Recovery.recover (partialToTotal fallback rec) y r = + withDefault fallback (PartialRecovery.decode rec y r) +Recovery.roundtrip (partialToTotal fallback rec) x = + cong (withDefault fallback) (PartialRecovery.roundtrip rec x) + +totalPartialDecoder : {A B R : Set} {C : Retention A B R} + (fallback : A) (rec : Recovery C) (y : B) (r : R) -> + Recovery.recover (partialToTotal fallback (totalToPartial rec)) y r ≡ + Recovery.recover rec y r +totalPartialDecoder fallback rec y r = refl + +partialSeparates : {A B R : Set} {C : Retention A B R} -> + PartialRecovery C -> Separates C +partialSeparates rec {x} {z} same = justInjective + (trans (sym (PartialRecovery.roundtrip rec x)) + (trans (cong (λ pair -> PartialRecovery.decode rec (fst pair) + (snd pair)) same) (PartialRecovery.roundtrip rec z))) + +partialComplete : {A B R : Set} {C : Retention A B R} + (rec : PartialRecovery C) {y : B} {r : R} (witness : Image C y r) -> + PartialRecovery.decode rec y r ≡ just (fst witness) +partialComplete rec (x , same) = + trans (sym (cong (λ pair -> PartialRecovery.decode rec (fst pair) (snd pair)) same)) + (PartialRecovery.roundtrip rec x) + +-- Independent of roundtrip: every successful output must reproduce the +-- requested pair. Plain PartialRecovery does not promise this property. +SuccessSound : {A B R : Set} {C : Retention A B R} -> PartialRecovery C -> Set +SuccessSound {A} {B} {R} {C} rec = (y : B) (r : R) (x : A) -> + PartialRecovery.decode rec y r ≡ just x -> retainedPair C x ≡ (y , r) + +data Decision (P : Set) : Set where + yes : P -> Decision P + no : (P -> Impossible) -> Decision P + +-- A positive answer must provide an actual source and an equality proof. +-- No general decision procedure follows from Separates, Cert or sound. +ImageDecision : {A B R : Set} -> Retention A B R -> Set +ImageDecision {B = B} {R = R} C = (y : B) (r : R) -> Decision (Image C y r) + +-- Sound success supplies an image witness; failure refutes all witnesses +-- because roundtrip recovers every member of the image. This is the exact +-- additional premise needed here to obtain a decision from a partial decoder. +soundPartialDecidesImage : {A B R : Set} {C : Retention A B R} + (rec : PartialRecovery C) -> SuccessSound rec -> ImageDecision C +soundPartialDecidesImage rec sound y r with PartialRecovery.decode rec y r in result +... | just x = yes (x , sound y r x result) +... | nothing = no + (λ witness -> nothingNotJust (trans (sym result) (partialComplete rec witness))) + +private + imageValue : {A B R : Set} {C : Retention A B R} {y : B} {r : R} -> + Decision (Image C y r) -> Maybe A + imageValue (yes (x , _)) = just x + imageValue (no _) = nothing + +-- The decision procedure chooses a witness internally from y and r. +-- Separation proves that every possible positive answer at a generated +-- pair returns the original source. A bare fibre projection lacks this law. +fromImageDecision : {A B R : Set} {C : Retention A B R} -> + Separates C -> ImageDecision C -> PartialRecovery C +PartialRecovery.decode (fromImageDecision {C = C} separates decide) y r = + imageValue {C = C} (decide y r) +PartialRecovery.roundtrip (fromImageDecision {C = C} separates decide) x + with decide (Retention.observe C x) (Retention.retain C x) +... | yes (z , same) = cong just (separates same) +... | no absent = eliminate (absent (x , refl)) + +-- This stronger property holds for the image-decision construction, but +-- is deliberately not a field of PartialRecovery (totalToPartial would +-- otherwise require an extra right-inverse law on unreachable inputs). +imageDecisionSound : {A B R : Set} {C : Retention A B R} + (separates : Separates C) (decide : ImageDecision C) -> + SuccessSound (fromImageDecision {C = C} separates decide) +imageDecisionSound {C = C} separates decide y r x success with decide y r +... | yes (z , same) = + trans (cong (retainedPair C) (sym (justInjective success))) same +... | no absent = eliminate (nothingNotJust success) + +-- Any concrete inhabitant of the fibre is recovered; combined with +-- imageDecisionSound this is a constructive, untruncated characterization +-- of successful decoding by this construction. No equality of proofs is used. +imageDecisionComplete : {A B R : Set} {C : Retention A B R} + (separates : Separates C) (decide : ImageDecision C) + {y : B} {r : R} (witness : Image C y r) -> + PartialRecovery.decode (fromImageDecision {C = C} separates decide) y r ≡ just (fst witness) +imageDecisionComplete {C = C} separates decide = + partialComplete (fromImageDecision {C = C} separates decide) diff --git a/src/EpistemicTypes/PartialRecoveryExamples.agda b/src/EpistemicTypes/PartialRecoveryExamples.agda new file mode 100644 index 0000000..38b3806 --- /dev/null +++ b/src/EpistemicTypes/PartialRecoveryExamples.agda @@ -0,0 +1,134 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +module EpistemicTypes.PartialRecoveryExamples where + +open import Agda.Builtin.Bool using (Bool; false; true) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Maybe using (just; nothing) +open import Agda.Builtin.Sigma using (Σ; _,_; fst; snd) +open import Agda.Builtin.Unit using (⊤; tt) +open import EpistemicTypes.EchoBridge using (Retention; Recovery; Impossible) +open import EpistemicTypes.PartialRecovery + +private + cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y + cong f refl = refl + + falseNotTrue : false ≡ true -> Impossible + falseNotTrue () + +-- Two generated pairs and two unreachable visible values: the image +-- decision is a finite, explicit computation, with both branches checked. +Visible : Set +Visible = Σ Bool (λ _ -> Bool) + +finiteRetention : Retention Bool Visible ⊤ +Retention.observe finiteRetention b = b , false +Retention.retain finiteRetention _ = tt +Retention.Cert finiteRetention _ _ = ⊤ +Retention.sound finiteRetention _ = tt + +finiteSeparates : Separates finiteRetention +finiteSeparates same = cong (λ pair -> fst (fst pair)) same + +finiteImageDecision : ImageDecision finiteRetention +finiteImageDecision (b , false) tt = yes (b , refl) +finiteImageDecision (b , true) tt = no + (λ witness -> falseNotTrue (cong (λ pair -> snd (fst pair)) (snd witness))) + +finitePartial : PartialRecovery finiteRetention +finitePartial = fromImageDecision {C = finiteRetention} finiteSeparates finiteImageDecision + +finiteGenerated : (b : Bool) -> + PartialRecovery.decode finitePartial (b , false) tt ≡ just b +finiteGenerated b = refl + +finiteUnreachable : (b : Bool) -> + PartialRecovery.decode finitePartial (b , true) tt ≡ nothing +finiteUnreachable b = refl + +finiteSound : SuccessSound finitePartial +finiteSound = imageDecisionSound {C = finiteRetention} finiteSeparates finiteImageDecision + +reconstructedDecision : ImageDecision finiteRetention +reconstructedDecision = soundPartialDecidesImage finitePartial finiteSound + +private + positive : {P : Set} -> Decision P -> Bool + positive (yes _) = true + positive (no _) = false + +reconstructedGenerated : (b : Bool) -> + positive (reconstructedDecision (b , false) tt) ≡ true +reconstructedGenerated b = refl + +reconstructedUnreachable : (b : Bool) -> + positive (reconstructedDecision (b , true) tt) ≡ false +reconstructedUnreachable b = refl + +falseDefault : Recovery finiteRetention +falseDefault = partialToTotal false finitePartial + +trueDefault : Recovery finiteRetention +trueDefault = partialToTotal true finitePartial + +defaultsAgreeOnImage : (b : Bool) -> + Recovery.recover falseDefault (b , false) tt ≡ Recovery.recover trueDefault (b , false) tt +defaultsAgreeOnImage b = refl + +defaultsDifferOffImage : + Recovery.recover falseDefault (false , true) tt ≡ + Recovery.recover trueDefault (false , true) tt -> Impossible +defaultsDifferOffImage = falseNotTrue + +-- General PartialRecovery deliberately allows success off the image. +-- The chosen total decoder satisfies roundtrip but not a global right inverse. +projectionRecovery : Recovery finiteRetention +Recovery.recover projectionRecovery y _ = fst y +Recovery.roundtrip projectionRecovery _ = refl + +offImageSuccess : + PartialRecovery.decode (totalToPartial projectionRecovery) (false , true) tt ≡ just false +offImageSuccess = refl + +offImageIncompatible : retainedPair finiteRetention false ≡ ((false , true) , tt) -> Impossible +offImageIncompatible same = falseNotTrue (cong (λ pair -> snd (fst pair)) same) + +-- Empty source makes the partial law vacuous, while the total signature +-- would have to produce an impossible source at the singleton input pair. +emptyRetention : Retention Impossible ⊤ ⊤ +Retention.observe emptyRetention () +Retention.retain emptyRetention () +Retention.Cert emptyRetention _ _ = Impossible +Retention.sound emptyRetention () + +emptyPartial : PartialRecovery emptyRetention +PartialRecovery.decode emptyPartial _ _ = nothing +PartialRecovery.roundtrip emptyPartial () + +noEmptyTotal : Recovery emptyRetention -> Impossible +noEmptyTotal rec = Recovery.recover rec tt tt + +-- Dropping the residue loses the Boolean distinction. A proof-relevant +-- fibre still carries either source, so projection trivially "roundtrips". +-- Its dependence on that supplied witness prevents pair-only recovery. +collisionRetention : Retention Bool ⊤ ⊤ +Retention.observe collisionRetention _ = tt +Retention.retain collisionRetention _ = tt +Retention.Cert collisionRetention _ _ = ⊤ +Retention.sound collisionRetention _ = tt + +witnessProjection : Image collisionRetention tt tt -> Bool +witnessProjection = fst + +witnessProjectionRoundtrip : (b : Bool) -> witnessProjection (b , refl) ≡ b +witnessProjectionRoundtrip b = refl + +witnessProjectionDependsOnWitness : + witnessProjection (false , refl) ≡ witnessProjection (true , refl) -> Impossible +witnessProjectionDependsOnWitness = falseNotTrue + +noCollidingPartial : PartialRecovery collisionRetention -> Impossible +noCollidingPartial rec = falseNotTrue (partialSeparates rec {false} {true} refl) diff --git a/tests/check-policy.sh b/tests/check-policy.sh index a9af153..27f28f0 100755 --- a/tests/check-policy.sh +++ b/tests/check-policy.sh @@ -25,6 +25,8 @@ expected_source_modules=( src/EpistemicTypes/Kripke/Frame.agda src/EpistemicTypes/Kripke/Indexed.agda src/EpistemicTypes/Kripke/Residual.agda + src/EpistemicTypes/PartialRecovery.agda + src/EpistemicTypes/PartialRecoveryExamples.agda src/EpistemicTypes/ProofTransport.agda src/EpistemicTypes/ProofTransportExample.agda src/EpistemicTypes/ReadConsistency.agda @@ -35,6 +37,7 @@ expected_source_modules=( expected_rejection_fixtures=( tests/reject/AgentChangesAnchor.agda tests/reject/BeliefIsKnowledge.agda + tests/reject/CollidingPartialRecovery.agda tests/reject/FakeFreshness.agda tests/reject/FinalStateProvesNoTouch.agda tests/reject/ForgedAcceptance.agda @@ -43,6 +46,7 @@ expected_rejection_fixtures=( tests/reject/InventedMigration.agda tests/reject/LyingVerifier.agda tests/reject/MismatchedSource.agda + tests/reject/PartialSuccessProvesImage.agda tests/reject/ReplayedArtifact.agda tests/reject/ReplayedHolder.agda tests/reject/ResealApprovesChange.agda @@ -54,6 +58,7 @@ expected_rejection_fixtures=( # shellcheck disable=SC2034 # consumed through require_exact_inventory namerefs expected_integration_modules=( tests/integration/CanonicalEcho.agda + tests/integration/CanonicalPartialRecovery.agda tests/integration/CanonicalRecovery.agda tests/integration/RecoveryExamples.agda ) diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index 565e893..984014b 100644 --- a/tests/check-rejections.sh +++ b/tests/check-rejections.sh @@ -7,7 +7,8 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." fixtures=(LyingVerifier ForgedAcceptance ReplayedArtifact ReplayedHolder \ StaleSample FakeFreshness ForkedHistory ForgedResidue MismatchedSource \ UnderstatedBound InventedMigration UncheckedSkip BeliefIsKnowledge \ - AgentChangesAnchor FinalStateProvesNoTouch ResealApprovesChange RestoreErasesHistory) + AgentChangesAnchor FinalStateProvesNoTouch ResealApprovesChange RestoreErasesHistory \ + CollidingPartialRecovery PartialSuccessProvesImage) expected_files=$(printf 'tests/reject/%s.agda\n' "${fixtures[@]}" | sort) actual_files=$(rg --files tests/reject -g '*.agda' | sort) [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; } @@ -37,6 +38,7 @@ for fixture in "${fixtures[@]}"; do AgentChangesAnchor) expected='0 != 1' ;; FinalStateProvesNoTouch) expected='true != .*false' ;; ResealApprovesChange|RestoreErasesHistory) expected='sealBroken != .*accepted' ;; + CollidingPartialRecovery|PartialSuccessProvesImage) expected='false != .*true' ;; esac if [[ "$status" -ne 42 ]] || ! rg -q "$expected" <<< "$diagnostic" || \ ! rg -q 'when checking' <<< "$diagnostic"; then diff --git a/tests/integration/CanonicalPartialRecovery.agda b/tests/integration/CanonicalPartialRecovery.agda new file mode 100644 index 0000000..386e2c2 --- /dev/null +++ b/tests/integration/CanonicalPartialRecovery.agda @@ -0,0 +1,39 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +module CanonicalPartialRecovery where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Sigma using (_,_) +import Echo as Canonical +open import EpistemicTypes.EchoBridge using (Retention) +open import EpistemicTypes.PartialRecovery + +-- The builtin Sigma and equality used by Image are the exact types used by +-- canonical Echo. Both maps preserve the source AND the original path. +-- This is a definitional identification of a standard fibre, not a claim +-- that its source can be recovered from a pair without further evidence. +toCanonicalImage : {A B R : Set} {C : Retention A B R} {y : B} {r : R} -> + Image C y r -> Canonical.Echo (retainedPair C) (y , r) +toCanonicalImage witness = witness + +fromCanonicalImage : {A B R : Set} {C : Retention A B R} {y : B} {r : R} -> + Canonical.Echo (retainedPair C) (y , r) -> Image C y r +fromCanonicalImage witness = witness + +imageRoundtrip : {A B R : Set} {C : Retention A B R} {y : B} {r : R} + (witness : Image C y r) -> + fromCanonicalImage {C = C} (toCanonicalImage {C = C} witness) ≡ witness +imageRoundtrip witness = refl + +canonicalRoundtrip : {A B R : Set} {C : Retention A B R} {y : B} {r : R} + (witness : Canonical.Echo (retainedPair C) (y , r)) -> + toCanonicalImage {C = C} (fromCanonicalImage {C = C} witness) ≡ witness +canonicalRoundtrip witness = refl + +fromCanonicalDecision : {A B R : Set} {C : Retention A B R} -> + Separates C -> + ((y : B) (r : R) -> Decision (Canonical.Echo (retainedPair C) (y , r))) -> + PartialRecovery C +fromCanonicalDecision {C = C} = fromImageDecision {C = C} diff --git a/tests/integration/RecoveryExamples.agda b/tests/integration/RecoveryExamples.agda index 070c246..9584ee3 100644 --- a/tests/integration/RecoveryExamples.agda +++ b/tests/integration/RecoveryExamples.agda @@ -5,6 +5,7 @@ module RecoveryExamples where open import Data.Bool.Base using (Bool; false; true) +open import Agda.Builtin.Maybe using (just; nothing) open import Data.Empty using (⊥) open import Data.Fin.Base using (Fin; zero; suc) open import Data.Nat.Base using (_≤_) @@ -13,8 +14,11 @@ open import Data.Unit.Base using (⊤; tt) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) import CanonicalEcho as Residues import CanonicalRecovery as Adapter +import CanonicalPartialRecovery as PartialAdapter import EchoFiniteResidue as Exact import EpistemicTypes.EchoBridge as Epistemic +import EpistemicTypes.PartialRecovery as Partial +import EpistemicTypes.PartialRecoveryExamples as PartialExamples -- Two distinct sources occupy one visible fibre. Identity retention supplies -- enough residue; the certificate restricts the visible index to that fibre. @@ -135,3 +139,18 @@ adapterPreservesOffImage : (Adapter.fromExactRecovery {C = offImageRetention} (Adapter.toExactRecovery flipOffImageRecovery)) (false , true) tt ≡ true adapterPreservesOffImage = refl + +-- This decision returns actual canonical Echo fibres of the joint pair +-- function. The adapter checks the owning definition at the reviewed pin. +canonicalPartial : Partial.PartialRecovery PartialExamples.finiteRetention +canonicalPartial = PartialAdapter.fromCanonicalDecision + {C = PartialExamples.finiteRetention} + PartialExamples.finiteSeparates PartialExamples.finiteImageDecision + +canonicalPartialGenerated : (b : Bool) -> + Partial.PartialRecovery.decode canonicalPartial (b , false) tt ≡ just b +canonicalPartialGenerated b = refl + +canonicalPartialUnreachable : (b : Bool) -> + Partial.PartialRecovery.decode canonicalPartial (b , true) tt ≡ nothing +canonicalPartialUnreachable b = refl diff --git a/tests/reject/CollidingPartialRecovery.agda b/tests/reject/CollidingPartialRecovery.agda new file mode 100644 index 0000000..ca08843 --- /dev/null +++ b/tests/reject/CollidingPartialRecovery.agda @@ -0,0 +1,16 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +module CollidingPartialRecovery where + +open import Agda.Builtin.Bool using (Bool; false; true) +open import Agda.Builtin.Equality using (refl) +open import Agda.Builtin.Maybe using (just) +open import EpistemicTypes.PartialRecovery using (PartialRecovery) +open import EpistemicTypes.PartialRecoveryExamples using (collisionRetention) + +forged : PartialRecovery collisionRetention +PartialRecovery.decode forged _ _ = just false +PartialRecovery.roundtrip forged false = refl +PartialRecovery.roundtrip forged true = refl diff --git a/tests/reject/PartialSuccessProvesImage.agda b/tests/reject/PartialSuccessProvesImage.agda new file mode 100644 index 0000000..252496b --- /dev/null +++ b/tests/reject/PartialSuccessProvesImage.agda @@ -0,0 +1,17 @@ +{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +module PartialSuccessProvesImage where + +open import Agda.Builtin.Bool using (false; true) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Sigma using (_,_) +open import Agda.Builtin.Unit using (tt) +open import EpistemicTypes.PartialRecovery using (retainedPair) +open import EpistemicTypes.PartialRecoveryExamples using (finiteRetention; offImageSuccess) + +-- offImageSuccess is checked, yet the successful source does not reproduce +-- this unreachable pair. Success alone cannot establish the stronger law. +forgedCompatibility : retainedPair finiteRetention false ≡ ((false , true) , tt) +forgedCompatibility = refl