WIP: AffineScript co-development — migration practice, frontier guide, verified cross-repo proofs (#531)

## What this is

A co-development branch practising the idaptik **ReScript → AffineScript
→ wasm** migration *for real*, harvesting the lessons into the
affinescript frontier-practices guide, and working out the
proofs/conflicts that surface when AffineScript meets a real game.

**Working agreement for this branch:** writes land in the **affinescript
repo only**. Anything destined for another repo (idaptik, echo-types,
standards) is staged as a reviewable, diff-able artefact under
`proposals/` — never written into its home repo without review.

## Landed so far

### `proposals/echo-types/` — verified soundness proof ✅
A machine-checked Agda module, `EchoEncodingFaithfulness.agda`, that
certifies the soundness of the **co-processor integerization** pattern
("the integer IS the X"):

- **lossless half** — an injective host-boundary encoder makes the
integer a faithful name (every fibre unique);
- **lossy half** — a code collision provably destroys the distinction
(no `decode` can type-check);
- **the clamp-to-sentinel hazard** — the canonical "default bad input to
`0`/`Open`" migration bug, exhibited as a *checked concrete instance* of
localized controlled loss.

Typechecks under `--safe --without-K` with Agda 2.6.3 + agda-stdlib 2.3,
**zero postulates, zero funext**. Independently re-verified in-session.
Reuses echo-types' existing `injective-fibres-proj-unique` /
`no-section-of-collapsing-map` — adds no new primitive, only the
migration-engineer packaging + worked `SecurityRank`-shaped instance.
See `proposals/echo-types/README.adoc` for the land-it steps.

## Incoming (in progress)

- `proposals/idaptik/` — a pure-integer coprocessor kernel migrated to
`.affine` end-to-end, with its differential-parity harness (broad sweep
→ deep verified exemplar).
- frontier-practices guide chapters — *co-processor integerization*,
*differential parity as the acceptance bar*, the *String host-boundary
ABI*, written for both human and agent readers.
- `proposals/toolchain/` — the variable-string-backend gap, `--deno-esm`
to retire the TS harnesses, compiler-emitted Echo boundary obligations,
release-cadence coupling.
- `proposals/standards/` — estate-standards implications.

## Toolchain note

Built against the **github-only network policy** (crates.io / deno.land
/ opam.ocaml.org are 403-blocked; GitHub + ubuntu-archive reachable).
Agda+stdlib, ocaml/dune, deno, and panic-attack are all installed and
verified by routing every install around the block.

Draft — will be updated as the streams land.

https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s

---
_Generated by [Claude
Code](https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

proposals/README.adoc

@@ -0,0 +1,69 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= AffineScript co-development proposals (cross-repo, staged for review)
+:toc: macro
+
+toc::[]
+
+== What this directory is
+
+This tree holds **cross-repo proposals produced during AffineScript
+co-development that target a repo *other than* affinescript**. They are
+staged here — as real, diff-able files — because the working agreement
+for this session is *writes go to the affinescript repo only*; everything
+destined for idaptik, echo-types, standards, etc. is parked here for human
+review before it is applied to its home repo.
+
+Each subdirectory is a self-contained proposal with its own `README.adoc`
+explaining what it is, where it belongs, how it was verified, and how to
+land it.
+
+== Index
+
+[cols="1,2,1,2",options="header"]
+|===
+| Subtree | Target repo | Status | What
+
+| `echo-types/`
+| `hyperpolymath/echo-types`
+| *Verified*
+| `EchoEncodingFaithfulness.agda` — a machine-checked Agda module
+  certifying the soundness of the "the integer IS the X" co-processor
+  integerization pattern (lossless = injective; lossy = collision /
+  clamp-to-sentinel). Typechecks under `--safe --without-K`, zero
+  postulates.
+
+| `idaptik/`
+| `hyperpolymath/idaptik`
+| _pending_
+| The kernel migration(s) (ReScript -> AffineScript) as a reviewable
+  case-study / patch, with their differential-parity harnesses.
+
+| `standards/`
+| `hyperpolymath/standards`
+| _pending_
+| Estate-standards implications: the co-processor integerization +
+  differential-parity convention, the String host-boundary ABI, the
+  github-only-network install recipe, the `--deno-esm` / TS-0
+  exemption-table delta.
+
+| `toolchain/`
+| `hyperpolymath/affinescript` (compiler/roadmap) + estate
+| _pending_
+| Compiler/toolchain implications harvested from dogfooding: the
+  variable-string-backend gap, `--deno-esm` to retire the TS harnesses,
+  compiler-emitted Echo boundary obligations, release-cadence coupling.
+|===
+
+== Why staged-not-applied
+
+Three reasons, all from the session's working agreement:
+
+. *Review gate.* The owner wants to review anything touching repos other
+  than affinescript before it lands.
+. *Honest provenance.* A staged proposal records exactly how it was
+  produced and verified, so the receiving repo's maintainer can re-run
+  the checks rather than trust a claim.
+. *No silent cross-repo drift.* Estate policy (see the standards repo's
+  license + no-automated-edits guardrails) is firmly against bulk
+  cross-repo sweeps; per-repo human acceptance is the rule.