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

[hyperpolymath]

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

[github-actions]

🔍 Hypatia Security Scan

Findings: 89 issues detected

Severity	Count
🔴 Critical	2
🟠 High	17
🟡 Medium	70

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action ons/checkout@v6\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action land/setup-deno@v2\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in affine-vscode-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "affine-vscode-publish.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence