From af89f4b1aa2d3ce0c3b2191d24c3ac1c6ea8ce50 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 18:16:49 +0100 Subject: [PATCH 1/3] =?UTF-8?q?examples:=20Example=2010=20=E2=80=94=20abst?= =?UTF-8?q?ract=20interpretation=20(Sign=20lattice)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `proofs/agda/EchoExampleAbsInt.agda` — Example 10 from the presentation-dependence cluster identified by PR #76 (abstract interpretation via a three-element Sign lattice over a hand-rolled five-element integer carrier). Headlines: - concretization-collapses, α-non-injective-on-pos - echo-pos-p1, echo-pos-p2, echo-zero-witness - distinct-echoes-same-sign - absint-classification Wired into `All.agda` (alphabetical) and `Smoke.agda` (per-lemma pins). EchoExamples.agda not modified (separate lanes also work on examples). Invariants: `--safe --without-K`; no postulates, no funext, no escape pragmas. Clean-worktree Agda build green (EchoExampleAbsInt.agda + All.agda + Smoke.agda all exit 0 on Agda 2.8.0 + stdlib). Refs #76 Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + proofs/agda/EchoExampleAbsInt.agda | 173 +++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 17 +++ 3 files changed, 191 insertions(+) create mode 100644 proofs/agda/EchoExampleAbsInt.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 0d21186..1fd0637 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -7,6 +7,7 @@ open import AntiEcho open import EchoKernel open import EchoCharacteristic open import EchoResidue +open import EchoExampleAbsInt open import EchoExamples open import EchoChoreo diff --git a/proofs/agda/EchoExampleAbsInt.agda b/proofs/agda/EchoExampleAbsInt.agda new file mode 100644 index 0000000..4fcf6f2 --- /dev/null +++ b/proofs/agda/EchoExampleAbsInt.agda @@ -0,0 +1,173 @@ +{-# OPTIONS --safe --without-K #-} + +-- EchoExampleAbsInt: Example 10 from `docs/echo-types/examples.md` +-- (abstract interpretation via Sign lattice), realised as the +-- canonical "abstraction map collapses many concretes to one +-- abstract value" instance of Echo. +-- +-- The carrier is a hand-rolled five-element integer toy +-- `{m2, m1, z, p1, p2}` (i.e. -2, -1, 0, +1, +2). This keeps the +-- example honest (a real `α : ℤ → Sign` would behave identically +-- on each non-zero strict sign region) while avoiding the weight +-- of `Data.Integer` for what is meant to be a small worked +-- example in the examples cluster. +-- +-- Abstraction: `α : Carrier → Sign` sends m1, m2 ↦ neg; z ↦ zero; +-- p1, p2 ↦ pos. The non-injectivity of α on the `pos` (and `neg`) +-- regions IS the lost concretion; `Echo α pos` is the carrier of +-- the recovered concrete-class information. +-- +-- Cluster relationship: presentation-dependence (PR #76). The +-- abstract-interpretation example is the canonical compiler-analysis +-- lens on Echo — the structured loss is the abstraction, and the +-- intensional core distinguishes which concrete value in a Sign +-- region was the actual program value. The "widening" / approximate +-- variant (Example 6 + axis 2) is NOT addressed here; this module +-- handles only the exact-Galois-abstraction half. Approximate +-- widening would land in `EchoApprox`'s tolerance-graded family. +-- +-- Headline lemmas (pinned in Smoke.agda): +-- +-- * concretization-collapses -- Σ-witness of non-injectivity +-- * α-non-injective-on-pos -- explicit p1 ≠ p2, α p1 ≡ α p2 +-- * echo-pos-p1, echo-pos-p2 -- two concretes for the pos region +-- * echo-zero-witness -- the singleton echo at zero +-- * distinct-echoes-same-sign -- the headline: two distinct +-- Echo α pos witnesses share +-- the same abstract value +-- * absint-classification -- every Echo α pos has carrier +-- p1 or p2 (i.e. the concrete +-- class over pos is exactly +-- the strictly-positive cell +-- of the carrier) + +module EchoExampleAbsInt where + +open import Echo using (Echo; echo-intro) + +open import Data.Product.Base using (Σ; _×_; _,_; proj₁) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong) + +---------------------------------------------------------------------- +-- Sign lattice (no ⊥/⊤ — keep the abstract domain minimal; the +-- ⊥/⊤ extension is the Galois-closure refinement and adds nothing +-- to the "many concretes ↦ one abstract" headline). +---------------------------------------------------------------------- + +data Sign : Set where + neg : Sign + zero : Sign + pos : Sign + +---------------------------------------------------------------------- +-- Hand-rolled five-element integer carrier. Standing for ℤ but +-- finite, decidable-equality-free (no _≟_ needed for this example), +-- and `--safe --without-K` friendly out of the box. +---------------------------------------------------------------------- + +data Carrier : Set where + m2 : Carrier -- -2 + m1 : Carrier -- -1 + z : Carrier -- 0 + p1 : Carrier -- +1 + p2 : Carrier -- +2 + +---------------------------------------------------------------------- +-- The abstraction. Galois-style: collapse the strict-sign regions +-- to their representative element of the Sign lattice. +---------------------------------------------------------------------- + +α : Carrier → Sign +α m2 = neg +α m1 = neg +α z = zero +α p1 = pos +α p2 = pos + +---------------------------------------------------------------------- +-- Constructor disjointness (definitional; no postulates). +---------------------------------------------------------------------- + +p1≢p2 : p1 ≢ p2 +p1≢p2 () + +m1≢m2 : m1 ≢ m2 +m1≢m2 () + +---------------------------------------------------------------------- +-- Headline 1 — `concretization-collapses`. +-- +-- The Σ-witness of non-injectivity: two distinct concretes that +-- α identifies. This is the bare information-loss statement, the +-- "shadow collapse" half of the example. +---------------------------------------------------------------------- + +concretization-collapses : + Σ Carrier (λ x₁ → Σ Carrier (λ x₂ → x₁ ≢ x₂ × α x₁ ≡ α x₂)) +concretization-collapses = p1 , p2 , p1≢p2 , refl + +---------------------------------------------------------------------- +-- Headline 2 — `α-non-injective-on-pos`. +-- +-- The explicit named variant of the above, pinned to the `pos` +-- region. Used downstream to keep proofs about the `pos` Echo +-- carrier readable. +---------------------------------------------------------------------- + +α-non-injective-on-pos : p1 ≢ p2 × α p1 ≡ α p2 +α-non-injective-on-pos = p1≢p2 , refl + +---------------------------------------------------------------------- +-- Headline 3 — concrete echoes. +-- +-- One per representative of the `pos` cell, plus the canonical +-- `zero` witness. The `Echo α pos` carrier is `Σ Carrier (λ x → α x ≡ pos)`; +-- both p1 and p2 inhabit it. +---------------------------------------------------------------------- + +echo-pos-p1 : Echo α pos +echo-pos-p1 = echo-intro α p1 + +echo-pos-p2 : Echo α pos +echo-pos-p2 = echo-intro α p2 + +echo-zero-witness : Echo α zero +echo-zero-witness = echo-intro α z + +---------------------------------------------------------------------- +-- Headline 4 — `distinct-echoes-same-sign`. +-- +-- The example's headline: two distinct echoes that share the same +-- abstract value. The intensional core carries the concrete (p1 vs +-- p2) while the extensional shadow has been quotiented to `pos`. +---------------------------------------------------------------------- + +echo-pos-p1≢echo-pos-p2 : echo-pos-p1 ≢ echo-pos-p2 +echo-pos-p1≢echo-pos-p2 q = p1≢p2 (cong proj₁ q) + +distinct-echoes-same-sign : + Σ (Echo α pos) (λ e₁ → Σ (Echo α pos) (λ e₂ → e₁ ≢ e₂)) +distinct-echoes-same-sign = echo-pos-p1 , echo-pos-p2 , echo-pos-p1≢echo-pos-p2 + +---------------------------------------------------------------------- +-- Headline 5 — `absint-classification`. +-- +-- The Sign-region classification: every `Echo α pos` has its +-- carrier-projection inhabiting the strictly-positive cell `{p1, p2}`. +-- This is the abstract-interpretation analogue of +-- `EchoCharacteristic.collapse-classification` and the standard +-- "preimage class is the cell of the partition" statement. +-- +-- The proof case-splits on the carrier; the impossible cases +-- (m2, m1, z) are ruled out by the proof `α x ≡ pos` reducing to +-- a clash of distinct Sign constructors (Agda's empty-clause `()`). +---------------------------------------------------------------------- + +absint-classification : + ∀ (e : Echo α pos) → proj₁ e ≡ p1 ⊎ proj₁ e ≡ p2 +absint-classification (m2 , ()) +absint-classification (m1 , ()) +absint-classification (z , ()) +absint-classification (p1 , _) = inj₁ refl +absint-classification (p2 , _) = inj₂ refl diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index f99e2ba..2b3d344 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -67,6 +67,23 @@ open import EchoFiberTriangulation using open import EchoCharacteristic using (collapse; echo-true; echo-false; echo-true≢echo-false) open import EchoResidue using (EchoR; collapse-to-residue; strict-weakening-collapse; no-section-collapse-to-residue) open import EchoExamples using (square9; visible; quot; collapse-residue-identifies) + +-- Example 10 from `docs/echo-types/examples.md` (abstract +-- interpretation via Sign lattice). Headlines pinned so a rename +-- or a slide back to an unanchored claim fails CI fast. See +-- PR #76 (presentation-dependence cluster). +open import EchoExampleAbsInt using + ( Sign + ; Carrier + ; α + ; concretization-collapses + ; α-non-injective-on-pos + ; echo-pos-p1 + ; echo-pos-p2 + ; echo-zero-witness + ; distinct-echoes-same-sign + ; absint-classification + ) open import VecRotation using (rotL-alternating; rotR-alternating; map-alternating) open import EchoApprox using From 89508555eb34f547f08af81f8976a397b0aca5ca Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 18:36:29 +0100 Subject: [PATCH 2/3] fix: restore EchoExampleParser additions lost in merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `3227b15` merge of `main` into `examples/absint-sign` silently dropped PR #83's additive changes (Example 9 parser residue, landed on main as commit `0f37f12`). This recovers them: * `proofs/agda/EchoExampleParser.agda` — restored from `main:proofs/agda/EchoExampleParser.agda` (227 lines, byte-identical to the file PR #83 added). * `proofs/agda/All.agda` — re-add `open import EchoExampleParser` alongside the AbsInt import. * `proofs/agda/Smoke.agda` — re-add the 23-line `using` block from #83 alongside this PR's AbsInt headline pins; both examples now pinned. Build invariant restored: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K` with both Example 9 (parser) and Example 10 (AbsInt) wired in. No postulates, no escape pragmas. Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + proofs/agda/EchoExampleParser.agda | 227 +++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 24 +++ 3 files changed, 252 insertions(+) create mode 100644 proofs/agda/EchoExampleParser.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index ff61fc9..d4a7fae 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -8,6 +8,7 @@ open import EchoKernel open import EchoCharacteristic open import EchoResidue open import EchoExampleAbsInt +open import EchoExampleParser open import EchoExamples open import EchoChoreo diff --git a/proofs/agda/EchoExampleParser.agda b/proofs/agda/EchoExampleParser.agda new file mode 100644 index 0000000..06b4cb9 --- /dev/null +++ b/proofs/agda/EchoExampleParser.agda @@ -0,0 +1,227 @@ +{-# OPTIONS --safe --without-K #-} + +-- Example 9 (presentation-dependence cluster, docs/echo-types/examples.md §9): +-- parser residue — balanced parentheses. +-- +-- Pragmatic toy parser: `parses` returns `Bool`, deciding "is this token +-- stream a balanced-parens word?" via a left-to-right depth counter that +-- (a) starts at zero, (b) increments on LP, (c) decrements on RP unless +-- already at zero (in which case it aborts to `false`), (d) accepts iff +-- the final depth is zero. This avoids the full `Balanced` grammar +-- definition; the point of Example 9 is the *echo*, not the grammar. +-- +-- Per `docs/echo-types/examples.md` §9: +-- "Echo parse tree = Σ (List Token) (λ ts → parse ts ≡ tree) ... +-- the same tree can be reached from different token streams, and the +-- echo distinguishes them." +-- +-- Concretely: `(())` and `()()` are two *distinct* `List Token` values +-- whose `parses` invocation collapses to the same Boolean `true`. They +-- are therefore distinct elements of `Echo parses true` — the +-- presentation-dependent axis (axis 4 in `docs/echo-types/taxonomy.md`). +-- +-- A *concrete* `Balanced`-grammar witness is also pinned (`bal-empty`, +-- `bal-paren-empty`) so downstream consumers who want the derivation +-- tree rather than the Boolean shadow have something to plug in. The +-- "parser residue" framing (cf. `EchoResidue`) is the observation that +-- the Boolean shadow forgets *which* derivation produced the parse; +-- that is exactly the same `strict-weakening` shape as `collapse`, with +-- the residue here being the token stream itself. + +module EchoExampleParser where + +open import Echo + +open import Data.Bool.Base using (Bool; true; false; if_then_else_) +open import Data.List.Base using (List; []; _∷_) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Product.Base using (Σ; _×_; _,_; proj₁; proj₂) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl; sym; cong) + +------------------------------------------------------------------------ +-- Token alphabet and concrete streams. + +data Token : Set where + LP : Token -- '(' + RP : Token -- ')' + +LP≢RP : LP ≢ RP +LP≢RP () + +-- Concrete examples. +[]ₜ : List Token +[]ₜ = [] + +-- "()" +paren-empty : List Token +paren-empty = LP ∷ RP ∷ [] + +-- "(())" +paren-nested : List Token +paren-nested = LP ∷ LP ∷ RP ∷ RP ∷ [] + +-- "()()" +paren-pair : List Token +paren-pair = LP ∷ RP ∷ LP ∷ RP ∷ [] + +------------------------------------------------------------------------ +-- Decision procedure: parses ≡ "is balanced?". +-- +-- A left-to-right depth counter. `parses-aux d ts = true` iff the +-- prefix has never gone negative and the final depth equals `d`. The +-- top-level `parses` calls `parses-aux 0`. +-- +-- The auxiliary's signature `ℕ → List Token → Bool` mirrors a state +-- machine. We pattern-match on the token first (Agda-friendly recursion +-- shape) and on the depth only in the RP case (the abort condition). + +parses-aux : ℕ → List Token → Bool +parses-aux zero [] = true +parses-aux (suc _) [] = false +parses-aux d (LP ∷ ts) = parses-aux (suc d) ts +parses-aux zero (RP ∷ _) = false +parses-aux (suc d) (RP ∷ ts) = parses-aux d ts + +parses : List Token → Bool +parses = parses-aux 0 + +------------------------------------------------------------------------ +-- Echo carriers: distinct token streams collapsing to `parses ≡ true`. + +echo-parse-empty : Echo parses true +echo-parse-empty = echo-intro parses []ₜ + +echo-parse-pair : Echo parses true +echo-parse-pair = echo-intro parses paren-pair + +echo-parse-nested : Echo parses true +echo-parse-nested = echo-intro parses paren-nested + +-- Disequality of the underlying token streams (the presentation). + +paren-nested≢paren-pair : paren-nested ≢ paren-pair +paren-nested≢paren-pair p = + -- Both streams have head LP; the second token distinguishes them: + -- paren-nested = LP ∷ LP ∷ _, paren-pair = LP ∷ RP ∷ _. + LP≢RP (cong second-token p) + where + second-token : List Token → Token + second-token (_ ∷ t ∷ _) = t + second-token _ = LP -- default; never reached for these inputs + +paren-empty≢paren-nested : paren-empty ≢ paren-nested +paren-empty≢paren-nested p = + -- Distinguish by length: `[]ₜ` after stripping the head LP differs. + empty≢pair (cong tail p) + where + tail : List Token → List Token + tail [] = [] + tail (_ ∷ xs) = xs + + -- `tail paren-empty = RP ∷ []`, `tail paren-nested = LP ∷ RP ∷ RP ∷ []`. + -- They differ at the head of the tail: RP vs LP. + empty≢pair : (RP ∷ []) ≢ (LP ∷ RP ∷ RP ∷ []) + empty≢pair q = LP≢RP (sym (cong head q)) + where + head : List Token → Token + head [] = LP -- default; never reached + head (t ∷ _) = t + +------------------------------------------------------------------------ +-- The headline: distinct presentations collapsing to the same parse +-- shadow. This is the "presentation-dependent" axis 4 obligation: the +-- Boolean shadow loses the token stream, but the Echo retains it. + +echo-parse-nested≢echo-parse-pair : echo-parse-nested ≢ echo-parse-pair +echo-parse-nested≢echo-parse-pair p = + paren-nested≢paren-pair (cong proj₁ p) + +parses-non-injective : + Σ (List Token) + (λ xs → Σ (List Token) (λ ys → xs ≢ ys × parses xs ≡ parses ys)) +parses-non-injective = + paren-nested , paren-pair , paren-nested≢paren-pair , refl + +------------------------------------------------------------------------ +-- Concrete derivation-tree witnesses (the `Balanced` grammar). +-- +-- A simple `Balanced` inductive predicate: the empty stream is +-- balanced, and wrapping any balanced stream in matching parens is +-- balanced. This is the *positive* fragment — concatenation +-- (`bal-cat`) is omitted because it requires `_++_` reasoning that the +-- single-paren-wrap shape doesn't need, and Example 9's headline only +-- needs concrete witnesses for `[]ₜ`, `paren-empty`, `paren-nested`. + +data Balanced : List Token → Set where + bal-empty : Balanced [] + bal-paren : ∀ {xs} → Balanced xs → Balanced (LP ∷ xs) + -- Reads "if `xs` is balanced, then `LP ∷ xs` is balanced + -- *modulo* a matching `RP`". Cf. `bal-paren-with-rp` below for + -- the closed-form constructor used by the concrete witnesses. + +-- Closed-form: wrap a balanced stream in `LP ∷ ... ∷ RP ∷ []` rather +-- than passing through `_++_`. This is a separate constructor-shape so +-- that the concrete witnesses (`bal-paren-empty`, `bal-paren-nested`) +-- can be built by case-and-pattern, not by induction on `_++_`. + +data BalancedClosed : List Token → Set where + bc-empty : BalancedClosed [] + bc-paren-empty : + BalancedClosed (LP ∷ RP ∷ []) + bc-paren-nested : + BalancedClosed (LP ∷ LP ∷ RP ∷ RP ∷ []) + bc-paren-pair : + BalancedClosed (LP ∷ RP ∷ LP ∷ RP ∷ []) + +-- The four concrete grammar witnesses. + +empty-balanced : BalancedClosed []ₜ +empty-balanced = bc-empty + +paren-empty-balanced : BalancedClosed paren-empty +paren-empty-balanced = bc-paren-empty + +paren-nested-balanced : BalancedClosed paren-nested +paren-nested-balanced = bc-paren-nested + +paren-pair-balanced : BalancedClosed paren-pair +paren-pair-balanced = bc-paren-pair + +------------------------------------------------------------------------ +-- Classification of `Echo parses true` for *our* concrete streams. +-- +-- We do NOT claim a full classification of the fibre (that would +-- require an exhaustive `parses ts ≡ true → Balanced ts` style +-- decoder). Instead, we pin the three concrete witnesses we +-- constructed above and observe that each has a distinct `proj₁`. + +echo-parse-empty-proj : proj₁ echo-parse-empty ≡ []ₜ +echo-parse-empty-proj = refl + +echo-parse-pair-proj : proj₁ echo-parse-pair ≡ paren-pair +echo-parse-pair-proj = refl + +echo-parse-nested-proj : proj₁ echo-parse-nested ≡ paren-nested +echo-parse-nested-proj = refl + +------------------------------------------------------------------------ +-- Parser residue (optional tie to `EchoResidue` framing). +-- +-- The Boolean shadow is the "lossy" projection; the residue is the +-- token stream itself. `parser-residue` exhibits the Σ-pair of +-- (Boolean shadow, lossy projection witness) for the headline pair of +-- distinct streams. The full `EchoResidue` lowering apparatus (with a +-- `Cert` relation + sound section) is overkill for Example 9 — the +-- point is *that* the shadow is non-injective on Echo, witnessed +-- concretely. Cf. `EchoResidue.collapse-residue-same` for the analogous +-- shape on the Boolean-collapse example. + +parser-residue : + Σ Bool + (λ b → Σ (List Token) (λ xs → Σ (List Token) (λ ys → + xs ≢ ys × parses xs ≡ b × parses ys ≡ b))) +parser-residue = + true , paren-nested , paren-pair , + paren-nested≢paren-pair , refl , refl diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index f8b0e79..9b19cf7 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -68,6 +68,30 @@ open import EchoCharacteristic using (collapse; echo-true; echo-false; echo-true open import EchoResidue using (EchoR; collapse-to-residue; strict-weakening-collapse; no-section-collapse-to-residue) open import EchoExamples using (square9; visible; quot; collapse-residue-identifies) +-- Example 9 (docs/echo-types/examples.md §9): parser residue — +-- balanced parentheses. The Boolean shadow `parses : List Token → +-- Bool` is non-injective on distinct presentations (`(())` vs `()()`), +-- and the Echo retains the token stream. Pinned headlines: the +-- non-injectivity Σ-witness, the three concrete `Echo parses true` +-- carriers (empty / pair / nested), and the residue Σ-pair. +open import EchoExampleParser using + ( Token + ; LP + ; RP + ; parses + ; echo-parse-empty + ; echo-parse-pair + ; echo-parse-nested + ; echo-parse-nested≢echo-parse-pair + ; parses-non-injective + ; parser-residue + ; BalancedClosed + ; empty-balanced + ; paren-empty-balanced + ; paren-nested-balanced + ; paren-pair-balanced + ) + -- Example 10 from `docs/echo-types/examples.md` (abstract -- interpretation via Sign lattice). Headlines pinned so a rename -- or a slide back to an unanchored claim fails CI fast. See From 549f219db7c9dcb59c173d1484049cad71a50f91 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 18:38:57 +0100 Subject: [PATCH 3/3] fix: restore EchoSearch additions also lost in the merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second wave of the same merge regression: the `3227b15` merge of `main` into `examples/absint-sign` also dropped PR #80's additive changes (Axis 8(4) witness-search machine, landed on main as commit `a1e9cbc`). This recovers them on top of the previous parser recovery commit `8950855`: * `proofs/agda/EchoSearch.agda` — restored from `main:proofs/agda/EchoSearch.agda` (156 lines, byte-identical to PR #80). * `proofs/agda/EchoSearchInstance.agda` — restored similarly (86 lines). * `proofs/agda/All.agda` — re-add `open import EchoSearch` + `EchoSearchInstance` (in the post-`EchoDecidable` slot per #80). * `proofs/agda/Smoke.agda` — re-add the 30-line headline-pin block for both modules, slotted between `EchoDecidable` and `EchoAccess`. Build invariant restored: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`. All four parallel-session additions (PRs #80 EchoSearch, #83 EchoExampleParser, plus this PR #82's EchoExampleAbsInt) are now wired in together. Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 2 + proofs/agda/EchoSearch.agda | 156 ++++++++++++++++++++++++++++ proofs/agda/EchoSearchInstance.agda | 86 +++++++++++++++ proofs/agda/Smoke.agda | 30 ++++++ 4 files changed, 274 insertions(+) create mode 100644 proofs/agda/EchoSearch.agda create mode 100644 proofs/agda/EchoSearchInstance.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index d4a7fae..a90c6bd 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -26,6 +26,8 @@ open import EchoCost open import EchoCostInstance open import EchoIndexed open import EchoDecidable +open import EchoSearch +open import EchoSearchInstance open import EchoAccess open import EchoFiberCount open import EchoEpistemicResidue diff --git a/proofs/agda/EchoSearch.agda b/proofs/agda/EchoSearch.agda new file mode 100644 index 0000000..e28b7bc --- /dev/null +++ b/proofs/agda/EchoSearch.agda @@ -0,0 +1,156 @@ +{-# OPTIONS --safe --without-K #-} + +-- EchoSearch — Axis 8 witness-search abstract machine (thin slice). +-- +-- Axis 8 of `docs/echo-types/taxonomy.md` distinguishes +-- information-theoretic inhabitation of `Echo f y` from a +-- *computational* witness extracted by an algorithm. Refinement (4) +-- in that section names the heaviest reading: +-- +-- "Witness-search abstract machine. Model the extractor as a +-- term in a bounded-step abstract machine and pair it with +-- the echo." +-- +-- A faithful "abstract machine" with steps, configurations, and a +-- semantics would be a sizeable separate development; the *honest* +-- thin slice of that idea is the enumerator-bounded witness: +-- +-- a search strategy = an enumerator `enum : ℕ → A` +-- a bound-`n` echo = a witness `enum k ≡ x` with `k < n` +-- together with the usual `f x ≡ y` +-- +-- The `ℕ`-bound is the "step budget" of the would-be machine. Every +-- machine of the heavier refinement (e.g. a Turing-bounded extractor, +-- a polynomial-time enumeration) projects onto this thin slice by +-- forgetting everything except the index it queried and the bound it +-- queried under. So this module sits at the *bottom* of the +-- axis-8(4) lattice in the same sense that `EchoDecidable` sits at +-- the bottom of the axis-8(3) lattice (`docs/echo-types/taxonomy.md` +-- §"Open question / lattice"), and a heavier machine model lands on +-- top later without renaming or invalidating these lemmas. +-- +-- Design choices, in line with `EchoApprox` / `EchoFiberCount`: +-- +-- * `SearchStrategy A := ℕ → A`. A total function. Partiality is +-- not modelled here — that is a separate refinement (axis 8(2)). +-- A total enumerator is exactly the right shape for a +-- bound-respecting machine: at step `k` it produces the element +-- `enum k`; nothing else. +-- +-- * `EchoS enum f y n := Σ ℕ λ k → (k < n) × (f (enum k) ≡ y)`. +-- Crucially `_<_` is stdlib's `Data.Nat.Base._<_`, i.e. +-- `suc m ≤ n` — the strict form. This is the form `≤-<-trans` / +-- `<-≤-trans` from `Data.Nat.Properties` operate on without any +-- conversion glue. +-- +-- * Composition: we ship `echo-search-postcompose`, the +-- "post-compose with `g`" rule. This is the search analogue of +-- "f x ≡ y ⇒ (g ∘ f) x ≡ g y" — it preserves the bound exactly +-- (the same k, the same enumerator step, the same `< n` proof). +-- This is the genuinely-honest compositional content available +-- without further machinery; a product/sequential composition +-- under two strategies needs more (a `ℕ × ℕ` index, a paired +-- bound, and a choice of pairing function on the index set), +-- which is a separate slice. See "where next" below. +-- +-- Where next: +-- +-- * Sequential composition `EchoS enum f b n₁ → EchoS enum' g y n₂ +-- → EchoS (paired-enum) (g ∘ f) y (n₁ * n₂)` under a pairing +-- enumerator on `ℕ × ℕ`. Honest but needs a bijection +-- `ℕ × ℕ ↔ ℕ`; defer to the slice that wants it. +-- +-- * A real abstract-machine refinement: configurations + a step +-- relation, with `EchoS` recovered as `∃ trace . trace.length < n +-- ∧ trace.last ≡ x ∧ f x ≡ y`. The current `EchoS` projects from +-- that by collapsing the trace to its terminal index. +-- +-- * A *bounded-search-is-decidable* lemma in the presence of +-- decidable equality on `B`: search up to `n` either yields an +-- `EchoS enum f y n` or proves `¬ EchoS enum f y n`. This is the +-- concrete bridge to `EchoDecidable`, kept as a separate slice +-- because it needs a `_≟_` on `B` and a finite-walk recursion. + +module EchoSearch where + +open import Function.Base using (_∘_; id) +open import Data.Nat.Base using (ℕ; zero; suc; _≤_; _<_; z≤n; s≤s) +open import Data.Nat.Properties using (≤-<-trans; <-≤-trans) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) +open import Relation.Nullary using (¬_) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; trans; cong) + +open import Echo using (Echo) + +---------------------------------------------------------------------- +-- Search strategies and bound-indexed echoes +---------------------------------------------------------------------- + +-- A search strategy on `A` is a total enumeration of its elements +-- indexed by ℕ. Total, by design — partiality is a separate axis 8(2) +-- refinement and would obscure the bound semantics here. +SearchStrategy : ∀ {a} → Set a → Set a +SearchStrategy A = ℕ → A + +-- The witness-search echo at bound `n`: a step index `k < n` at +-- which the enumerator produced a preimage of `y` under `f`. +EchoS : + ∀ {a b} {A : Set a} {B : Set b} + (enum : SearchStrategy A) (f : A → B) (y : B) (n : ℕ) → Set b +EchoS enum f y n = Σ ℕ (λ k → (k < n) × (f (enum k) ≡ y)) + +---------------------------------------------------------------------- +-- Headlines +---------------------------------------------------------------------- + +-- Introduction. If at step `k < n` the enumerator returns an element +-- whose image is `y`, we have a bound-`n` search echo. +echo-search-intro : + ∀ {a b} {A : Set a} {B : Set b} + (enum : SearchStrategy A) (f : A → B) {y : B} + (k : ℕ) (n : ℕ) (k