Skip to content

README.adoc

Latest commit

 

History

History
203 lines (169 loc) · 8.03 KB

README.adoc

File metadata and controls

203 lines (169 loc) · 8.03 KB
Raw

Proposal: EchoEncodingFaithfulness — certifying the co-processor integerization pattern

Important

Status: PROPOSAL, staged for review. This file and the accompanying EchoEncodingFaithfulness.agda are staged in the affinescript repo on purpose. Their eventual home is hyperpolymath/echo-types (proofs/agda/). Nothing here has been written into the echo-types repo — this is a reviewable, diff-able artefact so the echo-types maintainer can accept or revise it before it lands. Do not auto-merge into echo-types.
Table of Contents

One-sentence summary

The AffineScript migration slogan "the integer IS the X" is, precisely, an encoding-faithfulness theorem, and echo-types already contains every primitive needed to prove it — so this proposal packages those primitives under migration-engineer names and supplies the clamp-to-sentinel hazard as a worked, machine-checked bridge to the game.

Why this exists (the link nobody had drawn yet)

The idaptik ReScript → AffineScript → wasm migration leans on a repeatable pattern the dogfooding report calls co-processor integerization: a host-side enumerated / stringly-typed value X (a device port name, a security rank Open/Weak/Medium/Strong, a device type) is encoded to an integer, and a pure-integer AffineScript wasm kernel computes on the integer. The correctness slogan is "the integer IS the X".

That slogan is not folklore — it is a statement about the fibres of the encoder enc : X → ℤ:

Claim What it really means

"the integer IS the X" (lossless)

enc is injective — every integer determines its X uniquely; no two values share a code.

"we lost something" (lossy / controlled loss)

two distinct x₁ ≢ x₂ collide onto one integer; the lost distinction is the residue, localised at the shared code; no integer → X decoder can be written.

This is exactly the shape of echo-types: Echo f y := Σ (x : A), (f x ≡ y) is the fibre of f over y, and the library already proves "injective ⟹ fibres are unique" and "collision ⟹ no section". This proposal is the audience-facing read of that pairing for a compiler/runtime migrator — in the same mould as the existing EchoProvenance.agda and EchoSecurity.agda audience modules.

What it proves

Three headline theorems, an abstract record, two worked instances, and an honest-bounds block. All under --safe --without-K, zero postulates, zero funext.

Name Statement

encoding-lossless

If enc is injective then for every code i, any two echoes of enc over i have the same underlying source element. (K-free; via EchoImageFactorization.injective-fibres-proj-unique.) The integer faithfully names the X.

encoding-collision⇒no-section

If x₁ ≢ x₂ but enc x₁ ≡ enc x₂, there is no decode : Code → Source with decode ∘ enc ≡ id. (Via EchoNoSectionGeneric.no-section-of-collapsing-map.) The collision is the named, localised residue.

clamp-sentinel-no-section

The game-relevant one. Models the canonical migration bug: an encoder injective on the valid band that clamps out-of-band input to a sentinel integer that also names a valid value (the "default a bad input to 0 / Open`" hazard). Exhibited as a checked concrete instance: `valid0 and oob both encode to 0, so the sentinel fibre has no section. The collapse is further witnessed as a fibre-count doubling (sentinel-two-distinct-indices) against the lossless valid band (valid-band-fibre-count-1).

The abstract carrier is record Encoding (Source, Code, enc) with parametric theorems in module EncodingTheorems (E : Encoding). The worked Rank instance (open' weak medium strong → 0 1 2 3, proven injective) is the bridge to idaptik’s actual SecurityRank.

Verification (this was actually run, not asserted)

$ cd <echo-types-mirror>
$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/EchoEncodingFaithfulness.agda
Checking EchoEncodingFaithfulness (.../proofs/agda/EchoEncodingFaithfulness.agda).
  (cold elaboration of the full dependency cone)
$ echo $?
0

  • Toolchain: Agda 2.6.3 + agda-stdlib v2.3 (the exact pair echo-types CI pins).

  • Discipline: {-# OPTIONS --safe --without-K #-}; a forbidden-construct scan (postulate|TERMINATING|trustMe|primTrustMe|funext) returns nothing.

  • Independence: drafted + typechecked by a dedicated proof-engineer agent in an isolated /tmp mirror (no writes into echo-types), then re-verified independently in this session. The staged .agda file is byte-identical to the file that typechecked.

  • Size: 474 lines (most of it the dense explanatory comments that match echo-types house style).

How to land it in echo-types

Per the echo-types CLAUDE.md "Working rules" (every module wired into All.agda, every headline pinned in Smoke.agda):

  1. Drop EchoEncodingFaithfulness.agda into proofs/agda/.

  2. Register in All.agda, in the "Audience moves (Tier 3)" block, immediately after EchoSecurity (it reuses EchoSecurity’s engine, `no-section-of-collapsing-map, so it belongs in that cluster):

    open import EchoEncodingFaithfulness  -- Encode faithfulness (migration "the integer IS the X")

  3. Add the pin block to Smoke.agda (its own using block with a header comment, per house rule):

    -- EchoEncodingFaithfulness — the ReScript->AffineScript->wasm encode-
-- faithfulness theorem ("the integer IS the X").
open import EchoEncodingFaithfulness using
  ( Encoding ; encoding-injective⇒fibre-unique ; encoding-lossless
  ; encoding-collision⇒no-section ; Rank ; rankCode ; rankCode-injective
  ; rank-encoding ; rank-lossless-at ; ClampInput ; clampCode
  ; clamp-sentinel-collision ; clamp-encoding ; clamp-sentinel-no-section
  ; sentinel-two-distinct-indices ; valid-band-fibre-count-1 )

  4. agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda should both still exit 0.

Honest bounds (and the conceptual payoff)

The module ships a NotProved-* matched-negative block. The load-bearing one:

NotProved-wasm-implements-enc — proving the encoder injective says nothing about whether the deployed wasm kernel bit-for-bit implements it. That is the differential-parity harness’s job (run host-side enc and wasm-side enc on the same inputs and compare), not the proof’s.

This is the clean division of labour that the whole migration methodology turns on, now made precise:

  • the proof (EchoEncodingFaithfulness) certifies the encoding is faithful in principle — that the integer model carries no hidden collision;

  • the parity harness certifies the wasm in practice implements that model.

Neither subsumes the other. Stating the boundary as a checked NotProved-* alias is what keeps the proof honest and the harness load-bearing.

Forward pointer: the toolchain implication

If host-boundary encodings are this regular, the AffineScript compiler could emit the obligation. A boundary-annotated encoder

@boundary enc : Rank -> i32

could require discharge by either an injectivity proof (lossless — the encoding-lossless shape) or an explicit clamp-with-declared-sentinel (acknowledged controlled loss — the clamp-sentinel shape), turning "the integer IS the X" from a slogan into a checked compiler obligation. Full write-up will live in proposals/toolchain/ once the affinescript-compiler scout reports.

Provenance

Generated and verified in the 2026-06-04 co-development session on branch claude/cool-keller-gr5sl. Source of truth for the theorem statements: the existing echo-types modules Echo, EchoImageFactorization, EchoNoSectionGeneric, EchoFiberCount — this module adds no new proof primitive, only repackages and instantiates them.