// SPDX-License-Identifier: CC-BY-SA-4.0
= echo-boundary
:toc: macro
:icons: font

A runnable tool that turns the AffineScript `@boundary` *encoding-faithfulness
obligation* into a *machine-checked* check.

toc::[]

== What it is

When a host-side enumerated / stringly-typed value (a 4-element security rank
`Open/Weak/Medium/Strong`, a device-port name, ...) is encoded to an integer
and a pure integer kernel (e.g. a wasm kernel) computes on that integer, the
migration slogan is *"the integer IS the host value."* That slogan is exactly
an encode-faithfulness question on the encoder `enc : Source -> Code`:

* *Lossless* iff the codes are pairwise distinct (the encoder is injective).
  Then the integer faithfully names the host value -- every code determines its
  source uniquely.
* *Controlled loss* iff two distinct names map to the same code (a collision /
  clamp). Then *no section* exists: there is no pure `decode : Code -> Source`
  recovering the host value from the integer. The lost distinction is named and
  localised at the colliding code -- the classic "default a bad input to 0 /
  `Open`" clamp bug.

`echo-boundary` reads an *encoding table* (`{name: integer-code}`), decides the
verdict, then *generates a self-contained Agda module that proves that verdict*
by reusing the existing `EchoEncodingFaithfulness` framework, and *typechecks
it*. `agda` exit 0 means the verdict is certified, not merely asserted.

The generated modules copy the SHAPE of the framework's worked
`Rank`/`rankCode`/`rankCode-injective` instance:

* *Lossless* -> `data Host`, `code : Host -> ℕ`, a diagonal `refl`-per-constructor
  `code-injective` (Agda's coverage discharges the off-diagonal absurd numeral
  cases), an `Encoding` record, and the re-exported `encoding-lossless` headline.
* *Controlled loss* -> the enum + code fn, the two colliding constructors
  exhibited as data, and `encoding-collision⇒no-section` invoked to obtain the
  certified no-section (controlled-loss) witness.

== Requirements

* `deno` on PATH (the tool is plain JavaScript -- TypeScript is banned
  estate-wide).
* `agda` (2.6.3 here) with `standard-library` on the library path.
* The echo *mirror* repo at `/tmp/mirror-boundary` (override with `--mirror`),
  containing `proofs/agda/EchoEncodingFaithfulness.agda` and its dependencies.
  The generated module is written into `proofs/agda/<Name>.agda` and typechecked
  from there so it can `open import` the framework.

== Usage

[source,sh]
----
# Table on argv:
deno run --allow-read --allow-write --allow-run --allow-env \
  boundary.mjs '{"Open":0,"Weak":1,"Medium":2,"Strong":3}'

# Table (with a clamp spec) on stdin:
echo '{"table":{"Open":0,"Weak":1,"Medium":2,"Strong":3},"clamp":{"OOB":0}}' \
  | deno run --allow-read --allow-write --allow-run --allow-env boundary.mjs
----

Input forms:

* *Bare table*: `{"Open":0,"Weak":1,"Medium":2,"Strong":3}`.
* *With clamp*: `{"table":{...},"clamp":{"OOB":0}}`. The `clamp` entries are
  merged into the table; an out-of-band name (`OOB`) that shares a code with a
  valid name is the canonical clamp bug. (Clamp vs. table is purely a
  presentation distinction -- the faithfulness logic treats every entry
  uniformly, so a collision between two ordinary table names is detected too.)

Flags:

[cols="1,3"]
|===
| `--name <Mod>`   | generated Agda module name (default `BoundaryLossless` /
                     `BoundaryControlledLoss`)
| `--mirror <dir>` | echo mirror repo (default `/tmp/mirror-boundary`)
| `--out <file>`   | also write the generated `.agda` to this path
| `--no-check`     | generate only; do not invoke `agda`
| `--help`         | usage
|===

Exit code: `0` if the verdict's proof typechecks, `1` if `agda` rejects the
generated module, `2` on bad input, `3` if `agda` could not be run.

== Trial runs (captured)

Both trials were run on 2026-06-04 against the mirror at `/tmp/mirror-boundary`
(Agda 2.6.3, stdlib 2.3). The generated, verified modules are saved under
`samples/`.

=== Trial 1 -- SecurityRank table -> LOSSLESS

Command:

[source,sh]
----
deno run --allow-read --allow-write --allow-run --allow-env \
  boundary.mjs '{"Open":0,"Weak":1,"Medium":2,"Strong":3}' --name BoundaryLossless
----

Output:

----
verdict: LOSSLESS
  names:  4
  codes:  0, 1, 2, 3
  module: BoundaryLossless
  agda:   exit 0 (wrote /tmp/mirror-boundary/proofs/agda/BoundaryLossless.agda)
  PROOF HOLDS: encoder injective -> boundary is lossless (the integer IS the host value).
----

Independent re-typecheck of the generated module:

[source,sh]
----
cd /tmp/mirror-boundary && LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/BoundaryLossless.agda
# AGDA_EXIT=0
----

Generated module: `samples/BoundaryLossless.agda`. The headline proved is
`boundary-lossless : (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂`
(every integer code determines its host value uniquely), via the framework's
`encoding-lossless` and a diagonal `code-injective`.

=== Trial 2 -- clamping table that collides -> CONTROLLED LOSS

Command (input on stdin):

[source,sh]
----
echo '{"table":{"Open":0,"Weak":1,"Medium":2,"Strong":3},"clamp":{"OOB":0}}' \
  | deno run --allow-read --allow-write --allow-run --allow-env \
    boundary.mjs --name BoundaryControlledLoss
----

Output:

----
verdict: CONTROLLED LOSS
  names:  5
  codes:  0, 1, 2, 3
  collision at code 0: "Open" and "OOB"
  module: BoundaryControlledLoss
  agda:   exit 0 (wrote /tmp/mirror-boundary/proofs/agda/BoundaryControlledLoss.agda)
  PROOF HOLDS: code collision -> no section -> controlled loss is certified.
----

Independent re-typecheck of the generated module:

[source,sh]
----
cd /tmp/mirror-boundary && LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/BoundaryControlledLoss.agda
# AGDA_EXIT=0
----

Generated module: `samples/BoundaryControlledLoss.agda`. The clamp value `OOB`
collides with `Open` on the sentinel code `0`; the headline proved is
`boundary-controlled-loss : ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x)`
(no integer-to-host recovery type-checks), via the framework's
`encoding-collision⇒no-section`.

== Files

[cols="1,3"]
|===
| `boundary.mjs`                     | the tool (Deno / plain JavaScript)
| `README.adoc`                      | this file
| `samples/BoundaryLossless.agda`    | generated + verified lossless proof (Trial 1)
| `samples/BoundaryControlledLoss.agda` | generated + verified controlled-loss proof (Trial 2)
|===

== Scope / honest bounds

This is a *type-level* faithfulness check, inheriting the
`EchoEncodingFaithfulness` `NotProved-*` discipline:

* It certifies the encoder *table* is injective (lossless) or has a localised
  collision (controlled loss). It says *nothing* about whether the deployed
  runtime bit-for-bit implements that encoder -- that is the differential-parity
  harness's job.
* `Code` is modelled as Agda `ℕ`. A real fixed-width integer type could
  re-introduce collisions (overflow / truncation) that a `ℕ` model never sees,
  so a lossless verdict is about the *table as given*, not about any particular
  integer width.

== Implementation note (Agda generation)

The lossless injectivity proof uses the *finite-enum diagonal form* -- one
`code-injective {cN} {cN} _ = refl` clause per constructor, exactly as the
framework's `rankCode-injective` does. This is sound *because* every `code`
clause maps its constructor to a literal `ℕ` numeral, so Agda's coverage checker
discharges every off-diagonal pair as an absurd numeral equality (e.g. `0 ≡ 1`)
without the generator having to enumerate them. A fully general
`Injective`-for-arbitrary-codomain proof is *not* attempted; the diagonal form
is both what the framework uses and what is robust to generate for any finite
table. No generation obstruction was hit -- both verdict shapes typecheck
straight off the framework's worked instances, including non-clamp collisions
(two ordinary table names sharing a code) and clamp collisions alike.
