diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 9f63d93..f048444 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -20,6 +20,7 @@ open import EchoCNOBridge open import EchoApprox open import EchoIndexed open import EchoDecidable +open import EchoAccess open import EchoFiberCount open import EchoEpistemicResidue open import EchoRelational diff --git a/proofs/agda/EchoAccess.agda b/proofs/agda/EchoAccess.agda new file mode 100644 index 0000000..531fe7a --- /dev/null +++ b/proofs/agda/EchoAccess.agda @@ -0,0 +1,262 @@ +{-# OPTIONS --safe --without-K #-} + +-- Axis-8 second formal artifact: graded access modality. +-- +-- `EchoDecidable.agda` shipped the decidability-respecting refinement +-- of axis 8 (taxonomy.md §8): `EchoDec f y := Dec (Echo f y)`. That +-- module is the bottom of a lattice; this one builds the lattice. +-- +-- The graded access modality refines `Echo f y` with a grade +-- `c : Access` naming the *feasibility class* at which the echo's +-- witness is reachable: +-- +-- free — witness in hand, no search +-- decidable — a constructive decider exists (EchoDecidable.EchoDec) +-- enum — exhaustive Fin-search (EchoFiberCount terrain) +-- feasible — polynomial-time class (grade-only marker) +-- infeasible — super-polynomial / cryptographic; witness exists +-- only metatheoretically (grade-only marker) +-- +-- The chain `free ≤ decidable ≤ enum ≤ feasible ≤ infeasible` is +-- reflexive at every grade and one-step at the named edges; the order +-- relation `_≤a_` is enumerated by its 15 reachable pairs in +-- Hasse-diagram style, exactly mirroring `EchoGraded._≤g_` and +-- `EchoLinear._≤m_`. +-- +-- This file lands the **thin slice** of the recipe per the design in +-- `taxonomy.md` §8 / the Axis 8 study under `/tmp/echo-types-exploration`: +-- +-- 1. `Access` — enum of five feasibility classes +-- 2. `_≤a_` — Hasse-enumerated access order +-- 3. `≤a-trans` — transitivity by case-split +-- 4. `≤a-prop` — propositionality by case-split + refl +-- (load-bearing; the falsifier from the +-- design's §6) +-- 5. `EchoAccess` — Σ-shape carrier indexed by `Access` +-- 6. `access-of`, +-- `degrade-access` — projection + ≤a-indexed degrade primitive +-- +-- Deferred to follow-up (the design doc §5 obligations 5–8): +-- +-- * `degrade-access-comp`, `degrade-access-compose`, +-- `degrade-access-via-join` — per-decoration composition; the +-- "factoring-free" closer chain of `composition.md` §6. +-- * `_⊔a_` join + `≤a-⊔a-{left,right,univ}` — categorical join +-- structure. +-- * Honest carrier for `enum` (bridge to `EchoFiberCount.FiberSize-fin`) +-- so `feasible` / `infeasible` are not Potemkin labels — the +-- falsifier mode B of the design's §6. The current carriers are +-- deliberately the minimal placeholders that let the order layer +-- ship green. + +module EchoAccess where + +open import Level using (Level; _⊔_) +open import Data.Unit.Base using (⊤; tt) +open import Data.Product.Base using (Σ; _,_) +open import Relation.Nullary.Decidable.Core using (yes) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Echo using (Echo) +open import EchoDecidable using (EchoDec) + +---------------------------------------------------------------------- +-- 1. The access enum +---------------------------------------------------------------------- + +-- Five feasibility classes along a single chain. Lower = more +-- accessible. The taxonomy §8 reading: `free` is information- +-- theoretic *and* operationally trivial; `infeasible` is the +-- cryptographic-hash regime (a witness exists metatheoretically but +-- is computationally out of reach). + +data Access : Set where + free : Access + decidable : Access + enum : Access + feasible : Access + infeasible : Access + +---------------------------------------------------------------------- +-- 2. The access order +---------------------------------------------------------------------- + +-- Hasse-enumerated: every reachable (c1, c2) pair has exactly one +-- inhabitant. 5 grades give 15 constructors (5+4+3+2+1). Each +-- constructor names its source and target — the same shape as +-- `EchoGraded._≤g_` (6 constructors for 3 grades) and +-- `EchoLinear._≤m_` (3 constructors for 2 modes). This shape is what +-- makes `≤a-prop` reduce to case-split + `refl` under `--without-K`. + +data _≤a_ : Access → Access → Set where + free≤free : free ≤a free + free≤decidable : free ≤a decidable + free≤enum : free ≤a enum + free≤feasible : free ≤a feasible + free≤infeasible : free ≤a infeasible + decidable≤decidable : decidable ≤a decidable + decidable≤enum : decidable ≤a enum + decidable≤feasible : decidable ≤a feasible + decidable≤infeasible : decidable ≤a infeasible + enum≤enum : enum ≤a enum + enum≤feasible : enum ≤a feasible + enum≤infeasible : enum ≤a infeasible + feasible≤feasible : feasible ≤a feasible + feasible≤infeasible : feasible ≤a infeasible + infeasible≤infeasible : infeasible ≤a infeasible + +---------------------------------------------------------------------- +-- 3. Transitivity +---------------------------------------------------------------------- + +-- Same recipe as `EchoGraded.≤g-trans`: on a reflexive first step, +-- propagate `p23`; otherwise enumerate the reachable composites. The +-- enumerated relation has exactly one inhabitant per (c1, c3) pair so +-- there is no choice of factoring — each clause is forced. + +≤a-trans : ∀ {c1 c2 c3} → c1 ≤a c2 → c2 ≤a c3 → c1 ≤a c3 +≤a-trans free≤free p23 = p23 +≤a-trans free≤decidable decidable≤decidable = free≤decidable +≤a-trans free≤decidable decidable≤enum = free≤enum +≤a-trans free≤decidable decidable≤feasible = free≤feasible +≤a-trans free≤decidable decidable≤infeasible = free≤infeasible +≤a-trans free≤enum enum≤enum = free≤enum +≤a-trans free≤enum enum≤feasible = free≤feasible +≤a-trans free≤enum enum≤infeasible = free≤infeasible +≤a-trans free≤feasible feasible≤feasible = free≤feasible +≤a-trans free≤feasible feasible≤infeasible = free≤infeasible +≤a-trans free≤infeasible infeasible≤infeasible = free≤infeasible +≤a-trans decidable≤decidable p23 = p23 +≤a-trans decidable≤enum enum≤enum = decidable≤enum +≤a-trans decidable≤enum enum≤feasible = decidable≤feasible +≤a-trans decidable≤enum enum≤infeasible = decidable≤infeasible +≤a-trans decidable≤feasible feasible≤feasible = decidable≤feasible +≤a-trans decidable≤feasible feasible≤infeasible = decidable≤infeasible +≤a-trans decidable≤infeasible infeasible≤infeasible = decidable≤infeasible +≤a-trans enum≤enum p23 = p23 +≤a-trans enum≤feasible feasible≤feasible = enum≤feasible +≤a-trans enum≤feasible feasible≤infeasible = enum≤infeasible +≤a-trans enum≤infeasible infeasible≤infeasible = enum≤infeasible +≤a-trans feasible≤feasible p23 = p23 +≤a-trans feasible≤infeasible infeasible≤infeasible = feasible≤infeasible +≤a-trans infeasible≤infeasible infeasible≤infeasible = infeasible≤infeasible + +---------------------------------------------------------------------- +-- 4. Propositionality of the access order +---------------------------------------------------------------------- + +-- Each constructor of `_≤a_` is pinned by both source and target, so +-- the order is propositional: any two proofs of `c1 ≤a c2` are equal. +-- This is the *load-bearing* lemma of the access recipe — see +-- `composition.md` §6 and `EchoGraded.≤g-prop` (lines 79–89 of +-- `EchoGraded.agda`). The whole "factoring-free composition" closer +-- chain rests on it. +-- +-- Pattern-matches close under `--without-K` because each (c1, c2) +-- pair has exactly one inhabitant of `_≤a_`; Agda's case-split picks +-- the unique constructor on both sides and both reduce to `refl`. +-- The design doc's §6 falsifier reads: "If `≤a-prop` does not close +-- on case-split + `refl` in ≤30 minutes, the design is wrong; collapse +-- grades that case-split distinguished but propositional equality +-- does not." This module shows the chain does close. + +≤a-prop : ∀ {c1 c2} (p p' : c1 ≤a c2) → p ≡ p' +≤a-prop free≤free free≤free = refl +≤a-prop free≤decidable free≤decidable = refl +≤a-prop free≤enum free≤enum = refl +≤a-prop free≤feasible free≤feasible = refl +≤a-prop free≤infeasible free≤infeasible = refl +≤a-prop decidable≤decidable decidable≤decidable = refl +≤a-prop decidable≤enum decidable≤enum = refl +≤a-prop decidable≤feasible decidable≤feasible = refl +≤a-prop decidable≤infeasible decidable≤infeasible = refl +≤a-prop enum≤enum enum≤enum = refl +≤a-prop enum≤feasible enum≤feasible = refl +≤a-prop enum≤infeasible enum≤infeasible = refl +≤a-prop feasible≤feasible feasible≤feasible = refl +≤a-prop feasible≤infeasible feasible≤infeasible = refl +≤a-prop infeasible≤infeasible infeasible≤infeasible = refl + +---------------------------------------------------------------------- +-- 5. The graded carrier +---------------------------------------------------------------------- + +-- Per-grade carriers along the design's §4 sketch. `free` and +-- `decidable` are honest (full witness; constructive decider). The +-- `enum`, `feasible`, and `infeasible` carriers are deliberately the +-- minimal placeholder `⊤` for this slice — promoting them to honest +-- bridges (`enum` → `FiberSize-fin`, `feasible` / `infeasible` → +-- complexity-tagged variants) is the design's deferred §6 mode-B +-- mitigation and lands in the follow-up PR. +-- +-- The level lift on `⊤` is needed because `Echo f y` lives in +-- `Set (a ⊔ b)` and Agda demands a single ambient level across the +-- match. `Level.Lift` from the standard library keeps the carrier +-- universe-uniform without disturbing `≤a-prop` (which is +-- grade-indexed, not carrier-indexed). + +open import Level using (Lift; lift) + +CEcho : + ∀ {a b} {A : Set a} {B : Set b} + → Access → (A → B) → B → Set (a ⊔ b) +CEcho free f y = Echo f y +CEcho decidable f y = EchoDec f y +CEcho {a} {b} enum _ _ = Lift (a ⊔ b) ⊤ +CEcho {a} {b} feasible _ _ = Lift (a ⊔ b) ⊤ +CEcho {a} {b} infeasible _ _ = Lift (a ⊔ b) ⊤ + +-- The Σ-shape mirror of `EchoGraded.GEcho`'s implicit graded bundle: +-- pair a grade with content at that grade. Useful when callers want +-- a single hom-set to thread through the access lattice rather than +-- a grade-indexed family. + +EchoAccess : + ∀ {a b} {A : Set a} {B : Set b} + → (A → B) → B → Set (a ⊔ b) +EchoAccess f y = Σ Access (λ c → CEcho c f y) + +---------------------------------------------------------------------- +-- 6. `access-of` and `degrade-access` +---------------------------------------------------------------------- + +-- Projection: read off the access grade of a packed `EchoAccess`. + +access-of : + ∀ {a b} {A : Set a} {B : Set b} + {f : A → B} {y : B} → EchoAccess f y → Access +access-of (c , _) = c + +-- The `_≤a_`-indexed degrade primitive. Going to a *less accessible* +-- grade *forgets* content: `free → decidable` wraps the witness in +-- `yes`, every step into the placeholder block discards down to +-- `tt`, and reflexive cases are the identity. +-- +-- The cases enumerate the same 15 constructors as `_≤a_`. The chain +-- `free → decidable → enum/.../infeasible` is the only place real +-- content moves; from `enum` onward the carrier is already `⊤`-lifted +-- so every transition is `lift tt`. +-- +-- Per-decoration composition (`degrade-access-comp` + `compose` + +-- `via-join`) is deferred to the follow-up PR per the body of this +-- module. The order layer (`≤a-trans`, `≤a-prop`) is the +-- mathematical prerequisite for that follow-up, and lands here. + +degrade-access : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} + {c1 c2 : Access} → c1 ≤a c2 → CEcho c1 f y → CEcho c2 f y +degrade-access free≤free e = e +degrade-access free≤decidable e = yes e +degrade-access free≤enum _ = lift tt +degrade-access free≤feasible _ = lift tt +degrade-access free≤infeasible _ = lift tt +degrade-access decidable≤decidable d = d +degrade-access decidable≤enum _ = lift tt +degrade-access decidable≤feasible _ = lift tt +degrade-access decidable≤infeasible _ = lift tt +degrade-access enum≤enum e = e +degrade-access enum≤feasible _ = lift tt +degrade-access enum≤infeasible _ = lift tt +degrade-access feasible≤feasible e = e +degrade-access feasible≤infeasible _ = lift tt +degrade-access infeasible≤infeasible e = e diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 6315b3c..4b40ee3 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -96,6 +96,28 @@ open import EchoDecidable using ; echo-dec-compose-fin ) +-- Axis 8 second formal artifact (taxonomy.md §8): graded access +-- modality, thin slice. Mirrors `EchoGraded` and `EchoLinear`'s order +-- layer (enum, Hasse-enumerated order, transitivity, propositionality) +-- plus the Σ-shape carrier + `_≤a_`-indexed degrade primitive. +-- Per-decoration composition (`degrade-access-comp` / `compose` / +-- `via-join`) and join structure (`_⊔a_`) land in the follow-up PR. +open import EchoAccess using + ( Access + ; free + ; decidable + ; enum + ; feasible + ; infeasible + ; _≤a_ + ; ≤a-trans + ; ≤a-prop + ; CEcho + ; EchoAccess + ; access-of + ; degrade-access + ) + open import EchoFiberCount using ( FiberSize-fin ; FiberSize-fin-no-hit