diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index cfcc741..1149fe2 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -47,6 +47,7 @@ open import EchoIndexed open import EchoDecidable open import EchoSearch open import EchoSearchInstance +open import EchoSearchExample open import EchoAccess open import EchoFiberCount open import EchoEpistemicResidue diff --git a/proofs/agda/EchoSearchExample.agda b/proofs/agda/EchoSearchExample.agda index a2a0a64..9653f22 100644 --- a/proofs/agda/EchoSearchExample.agda +++ b/proofs/agda/EchoSearchExample.agda @@ -2,27 +2,57 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell --- A worked axis-8 lattice exhibit: a concrete `BoundedSearch` for --- a small doubling function and its projections through the four --- axis-8 refinements. +-- A worked axis-8 lattice exhibit: a concrete bounded search +-- (`EchoSearch.EchoS`, refinement 4) for a small doubling function, +-- projected through the other axis-8 refinements. -- --- Demonstrates `EchoSearch.BoundedSearch` (refinement 4) in --- operational use, then chases the four bridges to refinements 1 --- (`EchoCost`), 2 (`EchoAccess.EchoA … feasible`), and 3 --- (`EchoDecidable.EchoDec`). The whole axis-8 lattice fires on a --- single concrete witness. +-- `EchoSearchInstance` pins the `EchoSearch` headlines at the +-- trivial-on-⊤ instance (proof-of-life only). This module is the +-- non-trivial operational counterpart: one concrete witness, found by +-- an explicit step-bounded enumeration, chased to -- --- Setting: `double : ℕ → ℕ`, `double n = n + n`. At the target --- value `6`, the witness is `3` (since `3 + 3 ≡ 6`). A bounded --- search with `bound = 4` and enumeration `λ i → toℕ i` finds the --- witness at position `Fin 4`'s third index. This is a small --- enough concrete operational substantiation that the bridges all --- fire by direct application. +-- * the base information-theoretic `Echo` (axis 1), +-- * refinement 1 (`EchoCost.Cost.EchoC`) at a real ℕ cost +-- algebra, +-- * refinement 3 (`EchoDecidable.EchoDec`) from a search hit, +-- * refinement 2 (`EchoAccess.CEcho … feasible`) via `degrade-access`. +-- +-- Setting: `double : ℕ → ℕ`, `double n = n + n` (by recursion). At +-- the target `6` the witness is `3`. The enumerator is the identity +-- on ℕ (step `k` proposes candidate `k`), so a budget of `4` admits +-- the candidates `0, 1, 2, 3` and the hit is at index `3`. The landed +-- `bounded-search-is-decidable` procedure, run on this instance, +-- computes to `yes` on exactly that witness (`search-double-6-decided`). +-- Note that procedure tests indices from the top of the budget +-- downwards (`suc n` tests `enum n` first), so here it hits index `3` +-- on its *first* comparison; it does not walk `0, 1, 2, 3`. +-- +-- Honesty notes: +-- +-- * The cost bridge is specialised to the identity enumerator: the +-- cost of a candidate is its enumeration position (inclusive), +-- `search-steps x = suc x` — the number of steps an *ascending* +-- scan of `countUp` takes to reach `x`. It is a function of `x` +-- only because the enumerator is `id`. It is a property of the +-- enumerator, NOT the executed comparison count of +-- `bounded-search-is-decidable` (which scans downwards and here +-- makes one comparison). With that choice the +-- search bound `k < n` *is* the budget receipt `suc k ≤ n` on the +-- nose (stdlib's `_<_` unfolds to `suc k ≤ n`), so no arithmetic +-- glue is needed. A general-enumerator cost bridge would need the +-- step index carried in the witness and is not attempted here. +-- +-- * The `feasible` carrier of `EchoAccess.CEcho` is the deliberate +-- `Lift ⊤` placeholder (decision doc +-- `docs/echo-types/decisions/echo-access-trivial-carrier.adoc`); +-- `search-as-feasible` therefore records the *grade* reached by +-- `degrade-access`, not extractable content. -- -- Headlines (pinned in `Smoke.agda`): -- -- * double -- the doubling function -- * search-double-6 -- the bounded search +-- * search-double-6-decided -- bounded decision computes to `yes` -- * search-as-echo -- bridge to base Echo -- * search-as-cost -- bridge to refinement 1 -- * search-as-dec -- bridge to refinement 3 @@ -30,31 +60,34 @@ module EchoSearchExample where -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Fin.Base using (Fin; zero; suc) +open import Level using (0ℓ) +open import Function.Base using (id) +open import Data.Nat.Base using (ℕ; zero; suc; _+_; s≤s; z≤n) +open import Data.Nat.Properties using (_≟_; +-mono-≤) +import Data.Nat.Base as ℕ +import Data.Nat.Properties as ℕₚ open import Data.Product.Base using (_,_) +open import Relation.Nullary using (yes) open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Echo using (Echo) -open import EchoCost using (EchoCost) +open import EchoCost using (CostAlgebra; module Cost) open import EchoDecidable using (EchoDec) -open import EchoAccess using (EchoA; feasible) +open import EchoAccess using (CEcho; feasible; free≤feasible; degrade-access) open import EchoSearch using - ( BoundedSearch - ; bounded-search - ; bounded-search-to-echo - ; bounded-search-to-cost - ; bounded-search-to-dec - ; bounded-search-to-access-feasible + ( SearchStrategy + ; EchoS + ; echo-search-forget + ; bounded-search-is-decidable ) ---------------------------------------------------------------------- -- The map: doubling ---------------------------------------------------------------------- --- A tiny lossy collapse: `double n = n + n`. Echo at `6` has a --- unique witness `3`, but the *search procedure* for finding it --- is a 4-step enumeration that explicitly tries `0, 1, 2, 3`. +-- A tiny map with a nontrivial search: `Echo double 6` has the unique +-- witness `3`, which sits at position `3` of the `countUp` enumeration, +-- inside a budget of `4`. double : ℕ → ℕ double zero = zero @@ -64,42 +97,86 @@ double (suc n) = suc (suc (double n)) -- The bounded search at target 6 ---------------------------------------------------------------------- --- A 4-position enumeration: candidate `i` (as a `Fin 4`) corresponds --- to natural-number `i`. The hit is at position `3 : Fin 4`, where --- `double 3 = 6`. +-- Step `k` of the identity enumerator proposes candidate `k`. +countUp : SearchStrategy ℕ +countUp = id + +-- The hit is at step `3 < 4`, where `double 3 ≡ 6` by computation. +search-double-6 : EchoS countUp double 6 4 +search-double-6 = 3 , s≤s (s≤s (s≤s (s≤s z≤n))) , refl + +-- The landed decision procedure, run on this instance, *finds* the +-- same search echo: the bounded decision computes to `yes` by `refl`. +-- The witness is not merely asserted, the decider produces it. (The +-- decider scans from index `3` downwards, so this is a one-comparison +-- hit; it is not evidence of an ascending four-step walk.) +search-double-6-decided : + bounded-search-is-decidable _≟_ countUp double 6 4 ≡ yes search-double-6 +search-double-6-decided = refl + +---------------------------------------------------------------------- +-- A real cost algebra: ℕ with step counts +---------------------------------------------------------------------- + +stepCostAlgebra : CostAlgebra 0ℓ +stepCostAlgebra = record + { Cost = ℕ + ; zero = 0 + ; _+_ = _+_ + ; _≤_ = ℕ._≤_ + ; ≤-refl = ℕₚ.≤-refl + ; ≤-trans = ℕₚ.≤-trans + ; +-identityˡ = λ _ → refl + ; +-mono-≤ = +-mono-≤ + } + +open Cost stepCostAlgebra using (EchoC) + +-- Enumeration position of candidate `x` under `countUp` (inclusive): +-- an ascending scan reaches `0` in one step, `x` in `suc x`. This is +-- the cost the bound `k < n` certifies, not the decider's work. +search-steps : ℕ → ℕ +search-steps = suc -search-double-6 : BoundedSearch double 6 4 -search-double-6 = bounded-search enumerate hit - where - enumerate : Fin 4 → ℕ - enumerate zero = 0 - enumerate (suc zero) = 1 - enumerate (suc (suc zero)) = 2 - enumerate (suc (suc (suc zero))) = 3 +---------------------------------------------------------------------- +-- The bridges +---------------------------------------------------------------------- - hit : _ - hit = suc (suc (suc zero)) , refl +-- Refinement 4 → refinement 1. A bound-`n` search echo under the +-- identity enumerator is a cost echo with budget `n` under the +-- step-count cost: `k < n` is definitionally `search-steps k ≤ n`. +count-up-search-to-cost : + ∀ {b} {B : Set b} {f : ℕ → B} {y : B} {n : ℕ} → + EchoS countUp f y n → EchoC search-steps n f y +count-up-search-to-cost (k , k