|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Axis-8 second formal artifact: graded access modality. |
| 4 | +-- |
| 5 | +-- `EchoDecidable.agda` shipped the decidability-respecting refinement |
| 6 | +-- of axis 8 (taxonomy.md §8): `EchoDec f y := Dec (Echo f y)`. That |
| 7 | +-- module is the bottom of a lattice; this one builds the lattice. |
| 8 | +-- |
| 9 | +-- The graded access modality refines `Echo f y` with a grade |
| 10 | +-- `c : Access` naming the *feasibility class* at which the echo's |
| 11 | +-- witness is reachable: |
| 12 | +-- |
| 13 | +-- free — witness in hand, no search |
| 14 | +-- decidable — a constructive decider exists (EchoDecidable.EchoDec) |
| 15 | +-- enum — exhaustive Fin-search (EchoFiberCount terrain) |
| 16 | +-- feasible — polynomial-time class (grade-only marker) |
| 17 | +-- infeasible — super-polynomial / cryptographic; witness exists |
| 18 | +-- only metatheoretically (grade-only marker) |
| 19 | +-- |
| 20 | +-- The chain `free ≤ decidable ≤ enum ≤ feasible ≤ infeasible` is |
| 21 | +-- reflexive at every grade and one-step at the named edges; the order |
| 22 | +-- relation `_≤a_` is enumerated by its 15 reachable pairs in |
| 23 | +-- Hasse-diagram style, exactly mirroring `EchoGraded._≤g_` and |
| 24 | +-- `EchoLinear._≤m_`. |
| 25 | +-- |
| 26 | +-- This file lands the **thin slice** of the recipe per the design in |
| 27 | +-- `taxonomy.md` §8 / the Axis 8 study under `/tmp/echo-types-exploration`: |
| 28 | +-- |
| 29 | +-- 1. `Access` — enum of five feasibility classes |
| 30 | +-- 2. `_≤a_` — Hasse-enumerated access order |
| 31 | +-- 3. `≤a-trans` — transitivity by case-split |
| 32 | +-- 4. `≤a-prop` — propositionality by case-split + refl |
| 33 | +-- (load-bearing; the falsifier from the |
| 34 | +-- design's §6) |
| 35 | +-- 5. `EchoAccess` — Σ-shape carrier indexed by `Access` |
| 36 | +-- 6. `access-of`, |
| 37 | +-- `degrade-access` — projection + ≤a-indexed degrade primitive |
| 38 | +-- |
| 39 | +-- Deferred to follow-up (the design doc §5 obligations 5–8): |
| 40 | +-- |
| 41 | +-- * `degrade-access-comp`, `degrade-access-compose`, |
| 42 | +-- `degrade-access-via-join` — per-decoration composition; the |
| 43 | +-- "factoring-free" closer chain of `composition.md` §6. |
| 44 | +-- * `_⊔a_` join + `≤a-⊔a-{left,right,univ}` — categorical join |
| 45 | +-- structure. |
| 46 | +-- * Honest carrier for `enum` (bridge to `EchoFiberCount.FiberSize-fin`) |
| 47 | +-- so `feasible` / `infeasible` are not Potemkin labels — the |
| 48 | +-- falsifier mode B of the design's §6. The current carriers are |
| 49 | +-- deliberately the minimal placeholders that let the order layer |
| 50 | +-- ship green. |
| 51 | + |
| 52 | +module EchoAccess where |
| 53 | + |
| 54 | +open import Level using (Level; _⊔_) |
| 55 | +open import Data.Unit.Base using (⊤; tt) |
| 56 | +open import Data.Product.Base using (Σ; _,_) |
| 57 | +open import Relation.Nullary.Decidable.Core using (yes) |
| 58 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 59 | + |
| 60 | +open import Echo using (Echo) |
| 61 | +open import EchoDecidable using (EchoDec) |
| 62 | + |
| 63 | +---------------------------------------------------------------------- |
| 64 | +-- 1. The access enum |
| 65 | +---------------------------------------------------------------------- |
| 66 | + |
| 67 | +-- Five feasibility classes along a single chain. Lower = more |
| 68 | +-- accessible. The taxonomy §8 reading: `free` is information- |
| 69 | +-- theoretic *and* operationally trivial; `infeasible` is the |
| 70 | +-- cryptographic-hash regime (a witness exists metatheoretically but |
| 71 | +-- is computationally out of reach). |
| 72 | + |
| 73 | +data Access : Set where |
| 74 | + free : Access |
| 75 | + decidable : Access |
| 76 | + enum : Access |
| 77 | + feasible : Access |
| 78 | + infeasible : Access |
| 79 | + |
| 80 | +---------------------------------------------------------------------- |
| 81 | +-- 2. The access order |
| 82 | +---------------------------------------------------------------------- |
| 83 | + |
| 84 | +-- Hasse-enumerated: every reachable (c1, c2) pair has exactly one |
| 85 | +-- inhabitant. 5 grades give 15 constructors (5+4+3+2+1). Each |
| 86 | +-- constructor names its source and target — the same shape as |
| 87 | +-- `EchoGraded._≤g_` (6 constructors for 3 grades) and |
| 88 | +-- `EchoLinear._≤m_` (3 constructors for 2 modes). This shape is what |
| 89 | +-- makes `≤a-prop` reduce to case-split + `refl` under `--without-K`. |
| 90 | + |
| 91 | +data _≤a_ : Access → Access → Set where |
| 92 | + free≤free : free ≤a free |
| 93 | + free≤decidable : free ≤a decidable |
| 94 | + free≤enum : free ≤a enum |
| 95 | + free≤feasible : free ≤a feasible |
| 96 | + free≤infeasible : free ≤a infeasible |
| 97 | + decidable≤decidable : decidable ≤a decidable |
| 98 | + decidable≤enum : decidable ≤a enum |
| 99 | + decidable≤feasible : decidable ≤a feasible |
| 100 | + decidable≤infeasible : decidable ≤a infeasible |
| 101 | + enum≤enum : enum ≤a enum |
| 102 | + enum≤feasible : enum ≤a feasible |
| 103 | + enum≤infeasible : enum ≤a infeasible |
| 104 | + feasible≤feasible : feasible ≤a feasible |
| 105 | + feasible≤infeasible : feasible ≤a infeasible |
| 106 | + infeasible≤infeasible : infeasible ≤a infeasible |
| 107 | + |
| 108 | +---------------------------------------------------------------------- |
| 109 | +-- 3. Transitivity |
| 110 | +---------------------------------------------------------------------- |
| 111 | + |
| 112 | +-- Same recipe as `EchoGraded.≤g-trans`: on a reflexive first step, |
| 113 | +-- propagate `p23`; otherwise enumerate the reachable composites. The |
| 114 | +-- enumerated relation has exactly one inhabitant per (c1, c3) pair so |
| 115 | +-- there is no choice of factoring — each clause is forced. |
| 116 | + |
| 117 | +≤a-trans : ∀ {c1 c2 c3} → c1 ≤a c2 → c2 ≤a c3 → c1 ≤a c3 |
| 118 | +≤a-trans free≤free p23 = p23 |
| 119 | +≤a-trans free≤decidable decidable≤decidable = free≤decidable |
| 120 | +≤a-trans free≤decidable decidable≤enum = free≤enum |
| 121 | +≤a-trans free≤decidable decidable≤feasible = free≤feasible |
| 122 | +≤a-trans free≤decidable decidable≤infeasible = free≤infeasible |
| 123 | +≤a-trans free≤enum enum≤enum = free≤enum |
| 124 | +≤a-trans free≤enum enum≤feasible = free≤feasible |
| 125 | +≤a-trans free≤enum enum≤infeasible = free≤infeasible |
| 126 | +≤a-trans free≤feasible feasible≤feasible = free≤feasible |
| 127 | +≤a-trans free≤feasible feasible≤infeasible = free≤infeasible |
| 128 | +≤a-trans free≤infeasible infeasible≤infeasible = free≤infeasible |
| 129 | +≤a-trans decidable≤decidable p23 = p23 |
| 130 | +≤a-trans decidable≤enum enum≤enum = decidable≤enum |
| 131 | +≤a-trans decidable≤enum enum≤feasible = decidable≤feasible |
| 132 | +≤a-trans decidable≤enum enum≤infeasible = decidable≤infeasible |
| 133 | +≤a-trans decidable≤feasible feasible≤feasible = decidable≤feasible |
| 134 | +≤a-trans decidable≤feasible feasible≤infeasible = decidable≤infeasible |
| 135 | +≤a-trans decidable≤infeasible infeasible≤infeasible = decidable≤infeasible |
| 136 | +≤a-trans enum≤enum p23 = p23 |
| 137 | +≤a-trans enum≤feasible feasible≤feasible = enum≤feasible |
| 138 | +≤a-trans enum≤feasible feasible≤infeasible = enum≤infeasible |
| 139 | +≤a-trans enum≤infeasible infeasible≤infeasible = enum≤infeasible |
| 140 | +≤a-trans feasible≤feasible p23 = p23 |
| 141 | +≤a-trans feasible≤infeasible infeasible≤infeasible = feasible≤infeasible |
| 142 | +≤a-trans infeasible≤infeasible infeasible≤infeasible = infeasible≤infeasible |
| 143 | + |
| 144 | +---------------------------------------------------------------------- |
| 145 | +-- 4. Propositionality of the access order |
| 146 | +---------------------------------------------------------------------- |
| 147 | + |
| 148 | +-- Each constructor of `_≤a_` is pinned by both source and target, so |
| 149 | +-- the order is propositional: any two proofs of `c1 ≤a c2` are equal. |
| 150 | +-- This is the *load-bearing* lemma of the access recipe — see |
| 151 | +-- `composition.md` §6 and `EchoGraded.≤g-prop` (lines 79–89 of |
| 152 | +-- `EchoGraded.agda`). The whole "factoring-free composition" closer |
| 153 | +-- chain rests on it. |
| 154 | +-- |
| 155 | +-- Pattern-matches close under `--without-K` because each (c1, c2) |
| 156 | +-- pair has exactly one inhabitant of `_≤a_`; Agda's case-split picks |
| 157 | +-- the unique constructor on both sides and both reduce to `refl`. |
| 158 | +-- The design doc's §6 falsifier reads: "If `≤a-prop` does not close |
| 159 | +-- on case-split + `refl` in ≤30 minutes, the design is wrong; collapse |
| 160 | +-- grades that case-split distinguished but propositional equality |
| 161 | +-- does not." This module shows the chain does close. |
| 162 | + |
| 163 | +≤a-prop : ∀ {c1 c2} (p p' : c1 ≤a c2) → p ≡ p' |
| 164 | +≤a-prop free≤free free≤free = refl |
| 165 | +≤a-prop free≤decidable free≤decidable = refl |
| 166 | +≤a-prop free≤enum free≤enum = refl |
| 167 | +≤a-prop free≤feasible free≤feasible = refl |
| 168 | +≤a-prop free≤infeasible free≤infeasible = refl |
| 169 | +≤a-prop decidable≤decidable decidable≤decidable = refl |
| 170 | +≤a-prop decidable≤enum decidable≤enum = refl |
| 171 | +≤a-prop decidable≤feasible decidable≤feasible = refl |
| 172 | +≤a-prop decidable≤infeasible decidable≤infeasible = refl |
| 173 | +≤a-prop enum≤enum enum≤enum = refl |
| 174 | +≤a-prop enum≤feasible enum≤feasible = refl |
| 175 | +≤a-prop enum≤infeasible enum≤infeasible = refl |
| 176 | +≤a-prop feasible≤feasible feasible≤feasible = refl |
| 177 | +≤a-prop feasible≤infeasible feasible≤infeasible = refl |
| 178 | +≤a-prop infeasible≤infeasible infeasible≤infeasible = refl |
| 179 | + |
| 180 | +---------------------------------------------------------------------- |
| 181 | +-- 5. The graded carrier |
| 182 | +---------------------------------------------------------------------- |
| 183 | + |
| 184 | +-- Per-grade carriers along the design's §4 sketch. `free` and |
| 185 | +-- `decidable` are honest (full witness; constructive decider). The |
| 186 | +-- `enum`, `feasible`, and `infeasible` carriers are deliberately the |
| 187 | +-- minimal placeholder `⊤` for this slice — promoting them to honest |
| 188 | +-- bridges (`enum` → `FiberSize-fin`, `feasible` / `infeasible` → |
| 189 | +-- complexity-tagged variants) is the design's deferred §6 mode-B |
| 190 | +-- mitigation and lands in the follow-up PR. |
| 191 | +-- |
| 192 | +-- The level lift on `⊤` is needed because `Echo f y` lives in |
| 193 | +-- `Set (a ⊔ b)` and Agda demands a single ambient level across the |
| 194 | +-- match. `Level.Lift` from the standard library keeps the carrier |
| 195 | +-- universe-uniform without disturbing `≤a-prop` (which is |
| 196 | +-- grade-indexed, not carrier-indexed). |
| 197 | + |
| 198 | +open import Level using (Lift; lift) |
| 199 | + |
| 200 | +CEcho : |
| 201 | + ∀ {a b} {A : Set a} {B : Set b} |
| 202 | + → Access → (A → B) → B → Set (a ⊔ b) |
| 203 | +CEcho free f y = Echo f y |
| 204 | +CEcho decidable f y = EchoDec f y |
| 205 | +CEcho {a} {b} enum _ _ = Lift (a ⊔ b) ⊤ |
| 206 | +CEcho {a} {b} feasible _ _ = Lift (a ⊔ b) ⊤ |
| 207 | +CEcho {a} {b} infeasible _ _ = Lift (a ⊔ b) ⊤ |
| 208 | + |
| 209 | +-- The Σ-shape mirror of `EchoGraded.GEcho`'s implicit graded bundle: |
| 210 | +-- pair a grade with content at that grade. Useful when callers want |
| 211 | +-- a single hom-set to thread through the access lattice rather than |
| 212 | +-- a grade-indexed family. |
| 213 | + |
| 214 | +EchoAccess : |
| 215 | + ∀ {a b} {A : Set a} {B : Set b} |
| 216 | + → (A → B) → B → Set (a ⊔ b) |
| 217 | +EchoAccess f y = Σ Access (λ c → CEcho c f y) |
| 218 | + |
| 219 | +---------------------------------------------------------------------- |
| 220 | +-- 6. `access-of` and `degrade-access` |
| 221 | +---------------------------------------------------------------------- |
| 222 | + |
| 223 | +-- Projection: read off the access grade of a packed `EchoAccess`. |
| 224 | + |
| 225 | +access-of : |
| 226 | + ∀ {a b} {A : Set a} {B : Set b} |
| 227 | + {f : A → B} {y : B} → EchoAccess f y → Access |
| 228 | +access-of (c , _) = c |
| 229 | + |
| 230 | +-- The `_≤a_`-indexed degrade primitive. Going to a *less accessible* |
| 231 | +-- grade *forgets* content: `free → decidable` wraps the witness in |
| 232 | +-- `yes`, every step into the placeholder block discards down to |
| 233 | +-- `tt`, and reflexive cases are the identity. |
| 234 | +-- |
| 235 | +-- The cases enumerate the same 15 constructors as `_≤a_`. The chain |
| 236 | +-- `free → decidable → enum/.../infeasible` is the only place real |
| 237 | +-- content moves; from `enum` onward the carrier is already `⊤`-lifted |
| 238 | +-- so every transition is `lift tt`. |
| 239 | +-- |
| 240 | +-- Per-decoration composition (`degrade-access-comp` + `compose` + |
| 241 | +-- `via-join`) is deferred to the follow-up PR per the body of this |
| 242 | +-- module. The order layer (`≤a-trans`, `≤a-prop`) is the |
| 243 | +-- mathematical prerequisite for that follow-up, and lands here. |
| 244 | + |
| 245 | +degrade-access : |
| 246 | + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} |
| 247 | + {c1 c2 : Access} → c1 ≤a c2 → CEcho c1 f y → CEcho c2 f y |
| 248 | +degrade-access free≤free e = e |
| 249 | +degrade-access free≤decidable e = yes e |
| 250 | +degrade-access free≤enum _ = lift tt |
| 251 | +degrade-access free≤feasible _ = lift tt |
| 252 | +degrade-access free≤infeasible _ = lift tt |
| 253 | +degrade-access decidable≤decidable d = d |
| 254 | +degrade-access decidable≤enum _ = lift tt |
| 255 | +degrade-access decidable≤feasible _ = lift tt |
| 256 | +degrade-access decidable≤infeasible _ = lift tt |
| 257 | +degrade-access enum≤enum e = e |
| 258 | +degrade-access enum≤feasible _ = lift tt |
| 259 | +degrade-access enum≤infeasible _ = lift tt |
| 260 | +degrade-access feasible≤feasible e = e |
| 261 | +degrade-access feasible≤infeasible _ = lift tt |
| 262 | +degrade-access infeasible≤infeasible e = e |
0 commit comments