proofs(agda): preserve the bit-narrowing exhibits from unpushed commi…

proofs/agda/EchoBitNarrowingNumeric.agda

@@ -0,0 +1,89 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Numeric specification for the typed-wasm-echo receipt. This proves the
+-- natural-number equation and bounds, not a refinement of compiled Rust.
+-- Prepared with Codex (GPT-6) assistance, 2026-09-07.
+module EchoBitNarrowingNumeric where
+
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _^_; _<_; _≤_; z≤n; s≤s)
+open import Data.Nat.Properties using (+-suc; +-identityʳ; *-assoc; ≤-step)
+open import Data.Vec.Base using (Vec; []; _∷_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; cong; sym; trans; subst; module ≡-Reasoning)
+open import EchoExampleTruncation using (double)
+open import EchoExampleBitNarrowing
+  using (Bit; O; I; joinBit; restore; keepBits; dropBits; reconstruct-original)
+
+open ≡-Reasoning
+
+radix : ℕ → ℕ
+radix width = 2 ^ width
+
+value : ∀ {width} → Vec Bit width → ℕ
+value = restore 0
+
+private
+  double-sum : ∀ n → double n ≡ n + n
+  double-sum zero = refl
+  double-sum (suc n) = trans
+    (cong (λ k → suc (suc k)) (double-sum n))
+    (sym (cong suc (+-suc n n)))
+
+  double-times-two : ∀ n → double n ≡ 2 * n
+  double-times-two n = trans (double-sum n)
+    (sym (cong (n +_) (+-identityʳ n)))
+
+  double-plus : ∀ m n → double (m + n) ≡ double m + double n
+  double-plus zero n = refl
+  double-plus (suc m) n = cong (λ k → suc (suc k)) (double-plus m n)
+
+  join-plus : ∀ m n b → joinBit (m + n) b ≡ double m + joinBit n b
+  join-plus m n O = double-plus m n
+  join-plus m n I = trans (cong suc (double-plus m n))
+    (sym (+-suc (double m) (double n)))
+
+  double-mono : ∀ {m n} → m ≤ n → double m ≤ double n
+  double-mono z≤n = z≤n
+  double-mono (s≤s p) = s≤s (s≤s (double-mono p))
+
+  join-bound : ∀ {m n} → m < n → ∀ b → joinBit m b < double n
+  join-bound (s≤s p) O = s≤s (≤-step (double-mono p))
+  join-bound (s≤s p) I = s≤s (s≤s (double-mono p))
+
+-- The bit-vector reconstruction has the exact arithmetic shape of the API.
+restore-numeric : ∀ {width} high (bits : Vec Bit width) →
+  restore high bits ≡ radix width * high + value bits
+restore-numeric high [] = sym
+  (trans (+-identityʳ (high + 0)) (+-identityʳ high))
+restore-numeric {suc width} high (bit ∷ rest) = begin
+  joinBit (restore high rest) bit
+    ≡⟨ cong (λ k → joinBit k bit) (restore-numeric high rest) ⟩
+  joinBit (radix width * high + value rest) bit
+    ≡⟨ join-plus (radix width * high) (value rest) bit ⟩
+  double (radix width * high) + joinBit (value rest) bit
+    ≡⟨ cong (_+ joinBit (value rest) bit) (double-times-two (radix width * high)) ⟩
+  2 * (radix width * high) + joinBit (value rest) bit
+    ≡⟨ cong (_+ joinBit (value rest) bit) (sym (*-assoc 2 (radix width) high)) ⟩
+  radix (suc width) * high + value (bit ∷ rest) ∎
+
+-- A width-indexed output is always below its radix, including width zero.
+value-bounded : ∀ {width} (bits : Vec Bit width) → value bits < radix width
+value-bounded [] = s≤s z≤n
+value-bounded {suc width} (bit ∷ rest) = subst
+  (joinBit (value rest) bit <_)
+  (double-times-two (radix width))
+  (join-bound (value-bounded rest) bit)
+
+numeric-decomposition : ∀ width n →
+  n ≡ radix width * dropBits width n + value (keepBits width n)
+numeric-decomposition width n = trans
+  (sym (reconstruct-original width n))
+  (restore-numeric (dropBits width n) (keepBits width n))
+
+-- Under any declared word bound, reconstruction stays within that bound.
+-- In particular wordBits = 32 expresses the mathematical u32 obligation.
+reconstruction-bounded : ∀ wordBits width n → n < radix wordBits →
+  radix width * dropBits width n + value (keepBits width n) < radix wordBits
+reconstruction-bounded wordBits width n input-bound = subst
+  (_< radix wordBits) (numeric-decomposition width n) input-bound

proofs/agda/EchoExampleBitNarrowing.agda

@@ -0,0 +1,99 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+-- An exact echo for unsigned bit narrowing. The visible output is a
+-- little-endian vector of retained bits; the residue is the discarded
+-- quotient. Reconstruction is proved for every width and natural input.
+-- This is a mathematical specification, not a refinement proof of a Rust
+-- shift/mask implementation or of a Wasm compiler/runtime.
+module EchoExampleBitNarrowing where
+
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Vec.Base using (Vec; []; _∷_)
+open import Data.Product.Base using (_,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans)
+open import Echo using (Echo)
+open import EchoExampleTruncation
+  using (halve; double; halve-double; halve-suc-double)
+
+data Bit : Set where
+  O I : Bit
+
+lowBit : ℕ → Bit
+lowBit zero = O
+lowBit (suc zero) = I
+lowBit (suc (suc n)) = lowBit n
+
+joinBit : ℕ → Bit → ℕ
+joinBit n O = double n
+joinBit n I = suc (double n)
+
+private
+  low-double : ∀ n → lowBit (double n) ≡ O
+  low-double zero = refl
+  low-double (suc n) = low-double n
+
+  low-suc-double : ∀ n → lowBit (suc (double n)) ≡ I
+  low-suc-double zero = refl
+  low-suc-double (suc n) = low-suc-double n
+
+  halve-join : ∀ n b → halve (joinBit n b) ≡ n
+  halve-join n O = halve-double n
+  halve-join n I = halve-suc-double n
+
+  low-join : ∀ n b → lowBit (joinBit n b) ≡ b
+  low-join n O = low-double n
+  low-join n I = low-suc-double n
+
+  join-suc : ∀ n b → joinBit (suc n) b ≡ suc (suc (joinBit n b))
+  join-suc n O = refl
+  join-suc n I = refl
+
+join-split : ∀ n → joinBit (halve n) (lowBit n) ≡ n
+join-split zero = refl
+join-split (suc zero) = refl
+join-split (suc (suc n)) = trans
+  (join-suc (halve n) (lowBit n))
+  (cong (λ k → suc (suc k)) (join-split n))
+
+-- Drop the retained low bits, leaving the upper quotient as residue.
+dropBits : ℕ → ℕ → ℕ
+dropBits zero n = n
+dropBits (suc width) n = dropBits width (halve n)
+
+keepBits : (width : ℕ) → ℕ → Vec Bit width
+keepBits zero n = []
+keepBits (suc width) n = lowBit n ∷ keepBits width (halve n)
+
+restore : ∀ {width} → ℕ → Vec Bit width → ℕ
+restore high [] = high
+restore high (bit ∷ rest) = joinBit (restore high rest) bit
+
+-- Every input is recovered, including width zero and widths above its size.
+reconstruct-original : ∀ width n →
+  restore (dropBits width n) (keepBits width n) ≡ n
+reconstruct-original zero n = refl
+reconstruct-original (suc width) n = trans
+  (cong (λ high → joinBit high (lowBit n))
+    (reconstruct-original width (halve n)))
+  (join-split n)
+
+-- Any high residue reconstructs an origin in the fibre over these low bits.
+keep-restored : ∀ {width} high (bits : Vec Bit width) →
+  keepBits width (restore high bits) ≡ bits
+keep-restored high [] = refl
+keep-restored high (bit ∷ rest)
+  rewrite low-join (restore high rest) bit
+        | halve-join (restore high rest) bit
+        | keep-restored high rest = refl
+
+restored-echo : ∀ {width} high (bits : Vec Bit width) → Echo (keepBits width) bits
+restored-echo high bits = restore high bits , keep-restored high bits
+
+-- Reassembly also preserves the specified high residue, not just the output.
+drop-restored : ∀ {width} high (bits : Vec Bit width) →
+  dropBits width (restore high bits) ≡ high
+drop-restored high [] = refl
+drop-restored high (bit ∷ rest)
+  rewrite halve-join (restore high rest) bit = drop-restored high rest

proofs/agda/EchoExampleTruncation.agda

@@ -6,11 +6,10 @@
 -- truncation.
 --
 -- An Agda exhibit demonstrating compiler-analysis-style residue
--- in a numerical setting.  The original example takes `truncate :
--- ℝ → ℤ` with floor; ℝ isn't in stdlib v2.3, so this exhibit
--- adapts to an analogous `halve : ℕ → ℕ` (integer division by 2)
--- which exhibits the same structural shape: each output has
--- exactly two preimages, both equally valid concrete witnesses.
+-- in a numerical setting. This uses `halve : ℕ → ℕ` (integer division
+-- by 2), whose small structural definitions expose both preimages
+-- of each output. It is an analogue of lossy real-valued floor,
+-- which has an interval of preimages rather than just two.
 --
 -- The applications-chapter axis-2 widening discussion
 -- (`applications-compiler-analysis.adoc` § Example 2) uses the
@@ -19,14 +18,17 @@
 -- a follow-on could pair it with `EchoApprox` for the tolerance
 -- accumulation.
 --
--- Headline lemmas (pinned in `Smoke.agda`):
+-- Headline lemmas:
 --
 --   * halve                       -- the truncation function
 --   * halve-non-injective         -- 6 and 7 both halve to 3
 --   * echo-6-halve3               -- 6 is a witness at 3
 --   * echo-7-halve3               -- 7 is a witness at 3
 --   * echo-6≢echo-7              -- the residue is not propositional
---   * echo-halve-classification   -- every echo at n is in {2n, 2n+1}
+--   * echo-halve-even / odd       -- witnesses over every output n
+--   * echo-halve-witnesses-distinct -- their origins remain distinct
+--   * echo-halve-classification-general -- origins at n are {2n, 2n+1}
+--   * echo-halve-classification   -- the original n = 3 specialisation
 
 module EchoExampleTruncation where
 
@@ -50,6 +52,38 @@ halve zero          = zero
 halve (suc zero)    = zero
 halve (suc (suc n)) = suc (halve n)
 
+-- A structural doubling operation keeps the arithmetic specification
+-- aligned with halve's successor-pair recursion.
+double : ℕ → ℕ
+double zero    = zero
+double (suc n) = suc (suc (double n))
+
+halve-double : ∀ n → halve (double n) ≡ n
+halve-double zero    = refl
+halve-double (suc n) = cong suc (halve-double n)
+
+halve-suc-double : ∀ n → halve (suc (double n)) ≡ n
+halve-suc-double zero    = refl
+halve-suc-double (suc n) = cong suc (halve-suc-double n)
+
+-- Both possible origins are inhabited at every output, including zero.
+echo-halve-even : ∀ n → Echo halve n
+echo-halve-even n = double n , halve-double n
+
+echo-halve-odd : ∀ n → Echo halve n
+echo-halve-odd n = suc (double n) , halve-suc-double n
+
+private
+  suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
+  suc-injective refl = refl
+
+  distinct-successor : ∀ n → n ≢ suc n
+  distinct-successor zero ()
+  distinct-successor (suc n) p = distinct-successor n (suc-injective p)
+
+echo-halve-witnesses-distinct : ∀ n → echo-halve-even n ≢ echo-halve-odd n
+echo-halve-witnesses-distinct n p = distinct-successor (double n) (cong proj₁ p)
+
 ----------------------------------------------------------------------
 -- Headline 1 — non-injectivity at every output
 --
@@ -65,10 +99,9 @@ halve-non-injective = 6 , 7 , refl , λ ()
 ----------------------------------------------------------------------
 -- Headline 2 — concrete witnesses at halve = 3
 --
--- `Echo halve 3 = Σ ℕ (λ n → halve n ≡ 3)`.  Both 6 and 7 witness
--- the residue at 3.  These are the two preimages of `truncate(x) =
--- 3` in the original `truncate : ℝ → ℤ` formulation (the integer-
--- pair analogue of the half-unit fractional spread).
+-- `Echo halve 3 = Σ ℕ (λ n → halve n ≡ 3)`. Both 6 and 7 witness
+-- the residue at 3 in this integer-halving model. The corresponding
+-- real-valued floor fibre over 3 is the interval [3, 4).
 ----------------------------------------------------------------------
 
 echo-6-halve3 : Echo halve 3
@@ -95,16 +128,27 @@ echo-6≢echo-7 p with cong proj₁ p
 ----------------------------------------------------------------------
 -- Headline 4 — classification: every preimage of n is 2n or 2n+1
 --
--- The residue at any `n` is exactly the pair `{2n, 2n+1}` (using
--- ℕ-arithmetic that does not name `2n` explicitly).  Proved by
--- structural recursion: `halve m ≡ n` forces `m` to be of one of
--- two shapes by inspection.
+-- Every possible source natural at output n is double n or its
+-- successor. Together with the distinct witnesses above this gives
+-- both directions of the classification of source values. This
+-- statement does not compare the equality-proof components of echoes.
+-- Recursion reduces n and removes a successor pair from the source.
 ----------------------------------------------------------------------
 
+echo-halve-classification-general :
+  ∀ n (e : Echo halve n) →
+  (proj₁ e ≡ double n) ⊎ (proj₁ e ≡ suc (double n))
+echo-halve-classification-general zero (zero , _) = inj₁ refl
+echo-halve-classification-general zero (suc zero , _) = inj₂ refl
+echo-halve-classification-general zero (suc (suc m) , ())
+echo-halve-classification-general (suc n) (zero , ())
+echo-halve-classification-general (suc n) (suc zero , ())
+echo-halve-classification-general (suc n) (suc (suc m) , p)
+  with echo-halve-classification-general n (m , suc-injective p)
+... | inj₁ q = inj₁ (cong (λ k → suc (suc k)) q)
+... | inj₂ q = inj₂ (cong (λ k → suc (suc k)) q)
+
+-- Retain the original public statement for existing callers.
 echo-halve-classification :
   ∀ (e : Echo halve 3) → (proj₁ e ≡ 6) ⊎ (proj₁ e ≡ 7)
-echo-halve-classification (6                , refl) = inj₁ refl
-echo-halve-classification (7                , refl) = inj₂ refl
-echo-halve-classification (zero             , ())
-echo-halve-classification (suc zero         , ())
-echo-halve-classification (suc (suc (suc (suc (suc (suc (suc (suc m))))))) , ())
+echo-halve-classification = echo-halve-classification-general 3

proofs/agda/NarrowingSmoke.agda

@@ -0,0 +1,31 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- Focused entrypoint for the Wasm narrowing model and numeric contract.
+-- Prepared with Codex (GPT-6) assistance, 2026-09-07.
+module NarrowingSmoke where
+
+open import Data.Nat.Base using (_+_; _*_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import EchoExampleTruncation using
+  (echo-halve-even; echo-halve-odd; echo-halve-witnesses-distinct;
+   echo-halve-classification-general)
+open import EchoExampleBitNarrowing using
+  (dropBits; keepBits; restore; reconstruct-original;
+   keep-restored; drop-restored; restored-echo)
+open import EchoBitNarrowingNumeric using
+  (radix; value; restore-numeric; value-bounded;
+   numeric-decomposition; reconstruction-bounded)
+
+u8-radix : radix 8 ≡ 256
+u8-radix = refl
+
+u8-retained : value (keepBits 8 263) ≡ 7
+u8-retained = refl
+
+u8-discarded : dropBits 8 263 ≡ 1
+u8-discarded = refl
+
+u8-numeric-reconstruction :
+  263 ≡ radix 8 * dropBits 8 263 + value (keepBits 8 263)
+u8-numeric-reconstruction = numeric-decomposition 8 263