|
| 1 | +-- SPDX-License-Identifier: MPL-2.0 |
| 2 | +-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +-- ===================================================================== |
| 5 | +-- KitchenSpeak — Echo Bridge to the echo-types library |
| 6 | +-- ===================================================================== |
| 7 | +-- |
| 8 | +-- KitchenSpeak's Echo (@) type is a *postulated-oracle witness*: a |
| 9 | +-- dependent pair of a sensor sample time and a proof the sensor met its |
| 10 | +-- threshold there (Dough.agda's `Witness`, PoachedEgg.agda's |
| 11 | +-- `ShimmerWitness` / `WhiteWitness`). |
| 12 | +-- |
| 13 | +-- The hyperpolymath/echo-types library (module `Echo`) gives the |
| 14 | +-- canonical, mechanised form of exactly this structure — the *fiber*: |
| 15 | +-- |
| 16 | +-- Echo : (f : A → B) → B → Set |
| 17 | +-- Echo f y = Σ A (λ x → f x ≡ y) |
| 18 | +-- |
| 19 | +-- i.e. "which inputs map to y", the proof-relevant record of structured |
| 20 | +-- loss (a non-injective classifier forgets *which* sample fired, but the |
| 21 | +-- Echo retains that one did). This module wires KitchenSpeak's Echo type |
| 22 | +-- onto that library type so the planned type checker (ROADMAP Phase 3) |
| 23 | +-- and the proofs share a single, mechanised notion of Echo rather than |
| 24 | +-- an ad-hoc Σ. See decisions/0003-echo-types-dependency.adoc. |
| 25 | +-- |
| 26 | +-- The reconciliation. KitchenSpeak's witness is a fiber over a |
| 27 | +-- *predicate* (`sensor t ≥ thr`); echo-types' Echo is a fiber over an |
| 28 | +-- *equality* (`f x ≡ y`). We bridge by viewing each threshold oracle as |
| 29 | +-- a Boolean *classifier* `fired s thr t = ⌊ s t ≥? thr ⌋`, whose Echo |
| 30 | +-- over `true` is the KitchenSpeak witness. The classifier is the lossy |
| 31 | +-- function; the Echo is its structured-loss witness. |
| 32 | +-- |
| 33 | +-- --------------------------------------------------------------------- |
| 34 | +-- NOTE (hand-verified, not machine-checked here). Agda is not installed |
| 35 | +-- in the authoring environment, and echo-types (plus its own |
| 36 | +-- `depend: absolute-zero`) is not registered here, so the cross-library |
| 37 | +-- import below is verified by careful reading against the echo-types |
| 38 | +-- source (module `Echo`, definition quoted above, confirmed verbatim). |
| 39 | +-- When echo-types + absolute-zero + agda-stdlib 2.3+ are registered, |
| 40 | +-- `make -C proofs echobridge` should be the first check. The flag stance |
| 41 | +-- (this module is left at Agda's default discipline, importing the |
| 42 | +-- `--safe --without-K` `Echo`) is also to be confirmed there. |
| 43 | +-- --------------------------------------------------------------------- |
| 44 | + |
| 45 | +module EchoBridge where |
| 46 | + |
| 47 | +open import Data.Bool using (Bool; true; false) |
| 48 | +open import Data.Nat using (ℕ; _≥_; _≥?_) |
| 49 | +open import Data.Product using (Σ; _,_; Σ-syntax) |
| 50 | +open import Data.Empty using (⊥-elim) |
| 51 | +open import Relation.Nullary using (yes; no) |
| 52 | +open import Relation.Nullary.Decidable using (⌊_⌋) |
| 53 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 54 | + |
| 55 | +-- The Echo (fiber) type from hyperpolymath/echo-types (module `Echo`): |
| 56 | +-- Echo f y = Σ A (λ x → f x ≡ y) |
| 57 | +open import Echo using (Echo) |
| 58 | + |
| 59 | + |
| 60 | +-- ===================================================================== |
| 61 | +-- § 1. The threshold oracle as a Boolean classifier. |
| 62 | +-- ===================================================================== |
| 63 | +-- |
| 64 | +-- A KitchenSpeak echo-oracle samples a sensor `s : ℕ → ℕ` (reading per |
| 65 | +-- minute) and asks whether it has met a threshold `thr`. As a function |
| 66 | +-- into Bool this is the (generally non-injective) classifier whose Echo |
| 67 | +-- carries the structured loss: many minutes map to `true`, and the Echo |
| 68 | +-- records that *some* qualifying minute exists without pinning which. |
| 69 | + |
| 70 | +fired : (ℕ → ℕ) → ℕ → ℕ → Bool |
| 71 | +fired s thr t = ⌊ s t ≥? thr ⌋ |
| 72 | + |
| 73 | + |
| 74 | +-- ===================================================================== |
| 75 | +-- § 2. The two presentations of a KitchenSpeak Echo witness. |
| 76 | +-- ===================================================================== |
| 77 | +-- |
| 78 | +-- ThresholdWitness — the form used inline in Dough.agda / PoachedEgg.agda |
| 79 | +-- (`Σ[ t ] sensor t ≥ thr`). |
| 80 | +-- SensorEcho — the echo-types form: the fiber `Echo (fired …) true`. |
| 81 | + |
| 82 | +ThresholdWitness : (ℕ → ℕ) → ℕ → Set |
| 83 | +ThresholdWitness s thr = Σ[ t ∈ ℕ ] s t ≥ thr |
| 84 | + |
| 85 | +SensorEcho : (ℕ → ℕ) → ℕ → Set |
| 86 | +SensorEcho s thr = Echo (fired s thr) true |
| 87 | + |
| 88 | + |
| 89 | +-- ===================================================================== |
| 90 | +-- § 3. The bridge: KitchenSpeak's @-witness IS an echo-types Echo. |
| 91 | +-- ===================================================================== |
| 92 | +-- |
| 93 | +-- The two lemmas establish `s t ≥ thr ⟺ fired s thr t ≡ true`, lifted |
| 94 | +-- to the Σ/Echo level. Stating the goal with `⌊ s t ≥? thr ⌋` (which is |
| 95 | +-- `fired s thr t` by definition) keeps the `with`-abstraction robust. |
| 96 | + |
| 97 | +≥⇒fired : ∀ (s : ℕ → ℕ) (thr t : ℕ) → s t ≥ thr → ⌊ s t ≥? thr ⌋ ≡ true |
| 98 | +≥⇒fired s thr t pf with s t ≥? thr |
| 99 | +... | yes _ = refl |
| 100 | +... | no ¬p = ⊥-elim (¬p pf) |
| 101 | + |
| 102 | +fired⇒≥ : ∀ (s : ℕ → ℕ) (thr t : ℕ) → ⌊ s t ≥? thr ⌋ ≡ true → s t ≥ thr |
| 103 | +fired⇒≥ s thr t eq with s t ≥? thr |
| 104 | +... | yes p = p |
| 105 | +... | no _ with eq |
| 106 | +... | () |
| 107 | + |
| 108 | +-- KitchenSpeak threshold witness → echo-types Echo. |
| 109 | +witness⇒echo : ∀ {s thr} → ThresholdWitness s thr → SensorEcho s thr |
| 110 | +witness⇒echo {s} {thr} (t , pf) = t , ≥⇒fired s thr t pf |
| 111 | + |
| 112 | +-- echo-types Echo → KitchenSpeak threshold witness. |
| 113 | +echo⇒witness : ∀ {s thr} → SensorEcho s thr → ThresholdWitness s thr |
| 114 | +echo⇒witness {s} {thr} (t , eq) = t , fired⇒≥ s thr t eq |
| 115 | + |
| 116 | + |
| 117 | +-- ===================================================================== |
| 118 | +-- § 4. Usage from the recipe proofs. |
| 119 | +-- ===================================================================== |
| 120 | +-- |
| 121 | +-- Dough.agda and PoachedEgg.agda keep their inline `Σ[ t ] sensor t ≥ |
| 122 | +-- thr` witnesses (so their structural-recursion proofs are unchanged), |
| 123 | +-- and may present them as echo-types Echoes through `witness⇒echo`: |
| 124 | +-- |
| 125 | +-- viscosity-echo : Witness → SensorEcho viscosity-at kneaded-threshold |
| 126 | +-- viscosity-echo = witness⇒echo |
| 127 | +-- |
| 128 | +-- The planned KitchenSpeak type checker (ROADMAP Phase 3) takes |
| 129 | +-- `Echo (fired sensor thr) true` as the canonical typing of an `@` |
| 130 | +-- witness, with EchoTypes.jl as the finite-domain runtime/HAL model. |
0 commit comments