Merge main into feat/solo-core-metatheory-proofs (un-block #614) by hyperpolymath · Pull Request #615 · hyperpolymath/affinescript

hyperpolymath · 2026-06-21T01:08:25Z

What

Merges current main into feat/solo-core-metatheory-proofs and resolves all conflicts, so that #614 stops being mergeable_state: dirty. While #614 is dirty, GitHub cannot build the merge commit, so its entire CI suite is suppressed (only lint-workflows runs). Merging this PR into the feature branch un-blocks #614's CI.

Why it was needed

#614 branched off an old main (merge-base 61 commits back) and conflicts with the standalone-CI + codegen work that has since landed (#602, #603, #604, #606, #609, #610, #611, #612, #613).

Conflict resolutions (5 files)

File(s)	Resolution
`governance.yml`, `scorecard.yml`, `scorecard-enforcer.yml`, `hypatia-scan.yml`	Take `main`'s standalone versions. The branch re-adopted the estate `standards` reusables that `main` deliberately dropped (#603/#604) to stop run-creation `startup_failure`s. `main`'s `hypatia-scan.yml` also restores the permissions Hypatia needs (`security-events: write`, `pull-requests: write`, `secrets: inherit`) and the `MPL-2.0` SPDX id the Palimpsest license doc mandates for tooling.
`docs/PROOF-NEEDS.md`	Drop the branch's stale 103-line `.md`; keep `main`'s canonical 359-line `.adoc` (#609). Also satisfies DOC-FORMAT.
`docs/history/MODULE-SYSTEM-PROGRESS`	Keep the branch's `.md`→`.adoc` migration; port `main`'s additive #138 codegen-follow-up note + status-table row into the `.adoc` so `main`'s work is preserved.

spark-theatre-gate.yml and mirror.yml were identical to main.

Verification (merged tree)

dune build — clean
dune test — 534/534 pass (incl. cross-module constructor linking, Wasm (#138), Wasm nested tuple patterns, Deno-ESM / JS no duplicate Option/Result constructor)
wasm-runtime harness (tools/run_codegen_wasm_tests.sh) — all pass
workflow scan — no startup_failure risk introduced

How to use

Merge this into feat/solo-core-metatheory-proofs. #614 then becomes mergeable and its full CI runs.

Routed via this branch because the environment only permits pushes to claude/inspiring-newton-dg5wov, not directly to the feature branch.

Un-blocks #614.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8

Generated by Claude Code

## What Docs-only. Fixes staleness in `docs/specs/faces.adoc` surfaced while grounding the faces work, and records the grounded same-cube finding. ## Changes - **Active Faces table** now includes **LucidScript** (PureScript/Haskell) and **CafeScripto** (CoffeeScript) — both ship as established faces (`lib/lucid_face.ml`, `lib/cafe_face.ml`; see `examples/faces/README.adoc` and the brand repos), but the table previously listed only Canonical/Python/JS/Pseudocode. - **CoffeeScript-face** retitled from "Roadmap (strategic priority)" to **SHIPPED as CafeScripto** (design notes kept as history); only **ActionScript-face** remains on the roadmap. - New **Brand-surface repos** table (face → brand repo → transformer). - New **Same-cube grounding** section recording `invariant-path`'s `verify-same-cube.sh` + the grounded result. ## The grounded finding (worth a transformer-consistency issue) Built the compiler and ran the verifier (457-test suite green, per-face snapshot net 6/6 green). On the `greet` corpus the six faces compile to **two** wasm modules — `{canonical, jaffa, cafe}` vs `{rattle, pseudo, lucid}` — because the transformers disagree on **trailing-statement lowering** (statement `{ println(x); }` vs tail-expression `{ println(x) }`). Observationally identical, **not byte-identical wasm**. Making the transformers agree would give byte-level same-cube. (Informational: the verifier upgrade lives in `hyperpolymath/invariant-path#33`.) 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- _Generated by [Claude Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_

Closes #138 > Note: #138 itself was joint-closed (2026-05-18) when the front-end > seeded-builtins band-aid was removed. That removal correctly routed > `Some/None/Ok/Err` through the module path so `check` passes — but it > exposed a **codegen** regression that this PR fixes. Verified at HEAD > `58dc2a0`. ## Symptom A module that imports prelude's `Option`/`Result` and applies their constructors type-checks but fails to compile — the WASM backend raises `UnboundVariable "...Some"`. This blocked the stdlib `option`/`result` layer (and downstream consumers) from producing a runnable artifact. ## Root cause Codegen learns constructor tags **only** from `TopType` decls. Two import paths dropped imported types before they reached that registration: * **Core-Wasm `Codegen.gen_imports`** — the path the default `compile` uses. It feeds the *original* (un-flattened) `prog` to `generate_module` and resolved imports natively, but wired up only `TopFn` (→ wasm import) and `TopConst` (→ global); imported **types** were silently dropped, so `variant_tags` had no `Some` → `UnboundVariable`. **This is the path the reported failure hits.** * **`Module_loader.flatten_imports`** — used by the `prog_decls`-iterating backends (Deno / JS / Julia / C / Rust / …). It carried only `TopFn`/ `TopConst`. (The task brief pointed at `flatten_imports`; in practice the reported `compile` failure flows through `gen_imports` — empirically, before this PR the Deno/JS/Julia/C/Rust backends already compiled the consumer; only the WASM backend was broken. Both sites are fixed for completeness.) ## Fix 1. **`Codegen.gen_imports`** now registers the constructor tags / struct layouts of imported **public** types, reusing `gen_decl`'s local-type registration so imported and local types share exactly one code path. 2. **`Module_loader.flatten_imports`** now inlines imported public `TopType` decls — a **separate namespace** from fn/const (own dedup table, so a local `fn Foo` can't suppress an imported `type Foo`), **local-wins**, **deduped** across paths, and **ordered before** consumers so the single-pass codegen sees a type before any function that uses it. Selection: `use M::{..}` carries a type when the list names the type **or any of its constructors** (so `use prelude::{Some}` works without naming `Option`); `use M` / `use M::*` carry all public types. **Scope:** directly-imported constructors lower on **every** backend. **Transitive re-export** (a module re-exposing names it itself imported) stays unimplemented — noted in `docs/history/MODULE-SYSTEM-PROGRESS.md`. ## Verify — before / after Minimal `consumer.affine` (`use prelude::{Option, Some, None}` + `Some(x)`/`None`): ``` # BEFORE (HEAD 58dc2a0) $ affinescript check consumer.affine # Type checking passed $ affinescript compile consumer.affine # Code generation error: # (Codegen.UnboundVariable # "Function or variable not found: Some") # AFTER $ affinescript check consumer.affine # Type checking passed $ affinescript compile -o consumer.wasm c.affine # Compiled -> consumer.wasm (WASM) ``` Emitted WASM is valid and **runtime-correct** (via node `WebAssembly`): `wrap(5)` → boxed `Some` (tag 0, payload 5); `empty()` → `None` (tag 1); `Ok`/`Err` tags 0/1. Module imports only `wasi_snapshot_preview1.fd_write` — constructors are compiled inline, no spurious imports. All-backend matrix on the consumer (before → after): | backend | before | after | |---|---|---| | wasm (default) | **FAIL** `UnboundVariable "Some"` | **OK** | | deno.js / jl / c / rs / js / cjs | OK | OK | ## Tests * New Wasm-path regression test `cross-module constructor linking, Wasm (#138)` in `test/test_stdlib_aot.ml` — the counterpart to the #137 Deno-path integration. Feeds the imported-constructor decl shape to all three `variant_tags` consumers (with-arg construction, zero-arg, constructor patterns). * `dune test`: **458 tests, all green** (incl. #136 AOT smoke over 34 stdlib files and #137 integration — no regression). * `dune runtest conformance`: green. ## Out of scope (do not conflate with #138) Pre-existing core-Wasm gaps that reproduce with **purely local** enums and are independent of cross-module linking: * `stdlib/option.affine` / `result.affine` → `UnsupportedFeature "Only variable and wildcard patterns supported in tuple patterns"`. With this PR they get *past* the #138 `UnboundVariable` and reach this separate tuple-pattern codegen gap. * Mixed-representation `match` of a zero-arg variant (`None`) against a constructor-with-args arm returns the wrong value at runtime — reproduces with a local `Opt = Som(Int) | Non`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ Co-authored-by: Claude <noreply@anthropic.com>

…setup action) (#603) ## Make CI standalone (no external-repo reusable workflows on the gating path) Follow-up to the #602 investigation: the PR-gating `build`/`lint`/`test` never ran because several workflows were in `startup_failure`. This makes the **gating** CI self-contained — no dependency on the external `hyperpolymath/standards` reusable workflows and no third-party toolchain action — so it runs regardless of that repo's state or an org "allowed actions" policy. ### Root cause found The estate **`spark-theatre-gate.yml`** carries a documented note (BP008): **a `concurrency:` block in a reusable-workflow *caller*, when the reusable also declares concurrency on the same key, is rejected at run-creation → `startup_failure`** (no check-run is ever emitted). `governance.yml` and `secret-scanner.yml` both still had caller-level `concurrency:` blocks calling estate reusables → that is why they startup-failed, while `hypatia`/`spark` (no stacking) passed. The standalone replacements here are **normal** workflows, so their concurrency blocks are safe. ### Changes | Workflow | Before | After | |---|---|---| | **ci.yml** | `ocaml/setup-ocaml` (third-party) + first-party pins with **fictional** version comments (`checkout # v6.0.3`, `upload-artifact # v7.0.1`) | Self-hosted OCaml via `apt + opam` (`ocaml-system`, base-compiler fallback; dune-project needs ≥4.14); only first-party `actions/*` at real major tags | | **governance.yml** | calls `hyperpolymath/standards/.../governance-reusable.yml@main` | local `tools/ci/governance-standalone.sh` (Jekyll ban, MPL-1.0 SPDX-header ban, **PR-delta** DOC-FORMAT) | | **secret-scanner.yml** | calls `hyperpolymath/standards/.../secret-scanner-reusable.yml` + `secrets: inherit` | local `tools/ci/secret-scan-standalone.sh` (pure-shell, high-confidence patterns, no secrets) | | **scorecard.yml** | calls `hyperpolymath/standards/.../scorecard-reusable.yml` | direct `ossf/scorecard-action` (mirrors the already-direct `scorecard-enforcer.yml`) | New: `tools/ci/governance-standalone.sh`, `tools/ci/secret-scan-standalone.sh` (both `chmod +x`). ### Verification (local) ``` tools/ci/governance-standalone.sh → PASS (Jekyll: none; MPL-1.0 headers: none) tools/ci/governance-standalone.sh main → PASS (no newly-added docs/ .md) tools/ci/secret-scan-standalone.sh → PASS (no high-confidence secrets in tracked files) python3 -c yaml.safe_load on all 4 workflows → valid bash -n on both scripts → ok ``` The gates were calibrated against the tree first: a naïve gate would false-fail (59 pre-existing `docs/*.md`, 14 `MPL-1.0` *mentions* in policy/docs), so the checks are header-aware (0 actual `SPDX: MPL-1.0` headers) and DOC-FORMAT is **delta-only** (matches the canonical "PR that adds a docs/ .md" semantics; pre-existing files are never retro-flagged). ### Left intentionally (not "fully" standalone — by design) - **hypatia-scan.yml**, **spark-theatre-gate.yml** — estate-proprietary scanners (neurosymbolic / SPARK), **currently passing**. No public standalone equivalent exists; stubbing them would *lose* real coverage. Left calling the estate reusable. - **mirror.yml** — cross-forge mirroring is inherently external; not a CI gate. - **release.yml** — its `ocaml/setup-ocaml` runs on a **cross-platform matrix (Linux + macOS)**; a Linux-only `apt` inline setup would break the macOS release builds, and the publish path isn't testable here. Not PR-gating. - Standard community actions elsewhere (`github/codeql-action`, `denoland/setup-deno`, `dtolnay/rust-toolchain`, `haskell-actions/setup`, `peter-evans/repository-dispatch`) — normal, non-estate; inlining toolchain setups (esp. cross-platform) is a larger follow-up. Happy to do these if you want. ### Notes / trade-offs for review - First-party `actions/*` are pinned to **major tags** (`@v4`) rather than SHAs, because the prior SHA pins were labelled with nonexistent versions. `scorecard-enforcer.yml`'s `check-critical` job warns (non-blocking) on `@vN` pins. Re-pin to verified upstream SHAs if you prefer; first-party actions are always allowed under any allowlist. - The self-hosted OCaml step bumps the affected jobs' `timeout-minutes` 10 → 25 to cover the toolchain install. - I can't exercise GitHub runner behaviour from here; CI on this PR is the real test. If `ci.yml` still startup-fails after this, the remaining cause is isolated to first-party actions and points at an org Actions-policy/platform issue (owner-side). - Alternative considered: the **minimal** fix for governance/secret-scanner is simply removing the stacked `concurrency:` block (keeps the canonical estate checks). This PR goes standalone per request, but that option remains if you'd rather keep estate coverage. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ Co-authored-by: Claude <noreply@anthropic.com>

…er (#604) Follow-up to #603 (merged). #603 went in via admin bypass with **red CI**, so `main` is currently not green — this PR fixes that and completes "ensure standalone CI makes it through CI/CD." ## What was still wrong after #603 1. **`startup_failure` persisted** on `CI` / `Governance` / `Secret Scanner` — even though Governance/Secret-Scanner became trivial (`checkout` + `run:`). Identical failure across totally different file content ⇒ not the content. The one structural difference vs the **passing** simple workflows (`stdlib-naming`, `workflow-linter`, `scorecard-enforcer`): they pin `actions/checkout@<SHA>`; #603 used `@v4` **tags**. The repo's "allowed actions" policy appears to **reject tag refs at run-creation**. 2. **Hypatia check FAILED** — "Private Key" detected in `tools/ci/secret-scan-standalone.sh`: the scanner's literal PEM markers tripped the code-scanner against itself. 3. **Hypatia `unpinned_action` findings** (+15) — the `@v4` tags violate the repo's SHA-pinning policy (`workflow_audit`). ## Fix - **Re-pin all first-party `actions/*` to SHAs** (revert `@v4` → the repo's existing SHAs; only the fictional version *comments* `v6.0.3`/`v7.0.1` were corrected to `v4`). This clears the `unpinned_action` findings **and** is the fix for the tag-ref `startup_failure` (SHA-only policy). - **De-trip the secret scanner**: the PEM marker is now assembled from fragments, so no full marker literal appears in the file (clears the failing Hypatia "Private Key" alert). - **Fix a latent scanner bug**: patterns starting with `-` need `grep -e`, else grep parsed them as options and silently matched nothing. Verified: planted PEM **and** AWS keys are now detected; the tree stays clean. ## Verified locally ``` tools/ci/secret-scan-standalone.sh → PASS (clean tree) planted -----BEGIN RSA PRIVATE KEY----- file → FAIL (detected) ✅ planted AKIA… file → FAIL (detected) ✅ no literal 'BEGIN' marker remains in the script all 4 workflows: valid YAML; zero `actions/*@vN` tag pins (all SHA) ``` ## Honest caveat The SHA-only-policy theory is evidence-based but I can't observe GitHub's run-creation from here. **This PR's own CI run is the test:** if `CI`/`Governance`/`Secret Scanner` now *start* (and `build`/`lint`/`test` run), the theory holds. If `startup_failure` persists despite SHA pins, the remaining cause is an owner-side **Settings → Actions → Allowed actions** policy I can't change — I'll report that. Unchanged from #603 and still intentional: `hypatia-scan` / `spark-theatre-gate` (estate-proprietary, passing), `mirror` (cross-forge), `release.yml` (cross-platform macOS matrix needs `ocaml/setup-ocaml`). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ --------- Co-authored-by: Claude <noreply@anthropic.com>

…rs (#606) ## Deno-ESM: stop re-declaring the preamble's Option/Result constructors The locally-declared sibling of the duplicate-constructor bug fixed in #604. ### Bug The Deno-ESM runtime preamble always declares `Some`/`None`/`Ok`/`Err`. `gen_type_decl` *also* emits them for any program that **declares** `type Option`/`type Result` — including `stdlib/prelude.affine` — so the emitted module crashes under node: ``` $ affinescript compile --deno-esm -o prelude.deno.js stdlib/prelude.affine $ node prelude.deno.js SyntaxError: Identifier 'Some' has already been declared ``` It stayed latent because the #136 AOT smoke only checks the emitted module is **non-empty** — it never runs it. ### Fix Skip the variants the preamble already provides (`Some`/`None`/`Ok`/`Err`) when lowering a `TyEnum` in `codegen_deno.ml`. User-defined enums are unaffected. ### Verified ``` stdlib/prelude.affine -> deno : `const Some` ×1, runs under node ✅ (was ×2, crashed) user enum (Color=Red|Green|Blue): still emitted, runs ✅ tools/run_codegen_deno_tests.sh : all harnesses pass under node ✅ dune test : 459 green (+1 new regression test) ``` New test `Deno-ESM no duplicate Option/Result constructor` asserts `const Some` is declared exactly once — the run-under-node guard the AOT smoke lacked. ### Scope / follow-ups - This + #604 close the duplicate-constructor class on the **Deno** backend (the one executed in CI). - The **JS and C** backends show the same latent preamble/declaration duplication (2 `Some` decls) but their output isn't executed in CI — tracked as a follow-up, not fixed here. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ Co-authored-by: Claude <noreply@anthropic.com>

Optional housekeeping from the #138 / standalone-CI thread. Docs + regenerated test fixtures only — no source change. ### 1. `.claude/CLAUDE.md` — refresh the stale "known-failing baseline checks" Now that CI is standalone + green on `main` (#604), several entries were out of date: - `vscode-smoke` → **now passes** (self-contained; skips cleanly without the optional npm package). - `migration-assistant` → **passes on current `main`** (only red on pre-#342 bases). - `governance` → replaced by the self-contained local gate (`tools/ci/governance-standalone.sh`); the old estate `Language / package anti-pattern policy` sub-check no longer runs. - Hypatia comment counts refreshed (~43–71); clarified it's a *delta in your changed files* that matters, and the Hypatia *check* gates separately (green). - Recorded the two `startup_failure` classes that bit the repo for days so they aren't reintroduced: **(1)** the Actions "allowed actions" policy rejects **tag-pinned** refs at run-creation → pin every `uses:` to a full SHA; **(2)** BP008 reusable-caller `concurrency:` stacking. ### 2. `tests/codegen-deno/*.deno.js` — sync 3 drifted snapshots 3 of 30 committed Deno-ESM snapshots had drifted from current codegen output (runtime-preamble evolution — WASI `fd_write` import, pixi/ipc bindings); regenerated. All deno harnesses still pass under node. ### Verified `dune test` green · `tools/run_codegen_deno_tests.sh` all harnesses pass. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ Co-authored-by: Claude <noreply@anthropic.com>

…des #605) (#610) Supersedes **#605** with the cosmetic defect from my `/review` resolved. (I couldn't push the fix onto #605's branch — GitHub returns `403` on `dependabot/*` branches — so this carries Dependabot's exact bump commit plus the correction.) ### What's here 1. **Dependabot's commit** (`69f7fcc`) — `actions/checkout` v6.0.3 → v7.0.0 (`df4cb1c…` → `9c091bb…`), unchanged. 2. **Comment normalization** (`0df4a5e`) — every `actions/checkout` line now reads `# v7.0.0`. #605 left 14 lines tagged `# v4` (they'd been mislabeled `# v4` in #604/#606, where that SHA was actually **v6.0.3**), so the v7 SHA was carrying a `# v4` comment. Also adds the missing comment on `publish-jsr.yml`'s bare line and refreshes the `ci.yml` pin note. `setup-node` / `upload-artifact` remain genuinely **v4** and are untouched. **Comments only** beyond Dependabot's commit — no SHA or logic change. ### Why it's safe - SHA-pinned (`9c091bb…`), so compatible with the repo's "allowed actions" policy (tag refs would `startup_fail`). - v7's only breaking change (blocking fork-PR checkout for `pull_request_target` / `workflow_run`) **does not apply** — the repo uses neither trigger. - YAML validated on all 14 workflows; the genuine-v4 actions verified untouched. ### Action for you Merge this and **close #605** (this is its corrected equivalent). If you'd rather keep #605, close this instead and I'll land the comment fix as a follow-up once #605 merges. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ --------- Signed-off-by: dependabot[bot] <support@github.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>

…609) ## What Replaces the near-empty `docs/PROOF-NEEDS.md` (which held only the 2026-03-29 template-ABI cleanup note) with a real, structured inventory of **what AffineScript must prove, at what rigour, with honest status** — and renames it to `.adoc` per DOC-FORMAT. This is the deliverable for a fresh proof-needs review of the repo: *what we may have missed before*, *what's sharpened by outstanding work*, and *what's newly arisen from the **faces** work*. ## The review, in three partitions **`P-1…P-10` — pre-faces obligations that existed but were never catalogued.** The mechanized core is thinner than the prose corpus suggests: - `solo-core/Soundness.idr` is **statements-only** — `data Step` has no constructors, `progress`/`preservation` are `?todo` holes. It proves nothing yet, and covers only the Solo fragment (no traits/effects/rows/refinements/ownership/dependent types). - The seven `docs/academic/proofs/*.md` are **prose**; `docs/academic/mechanized/{agda,coq,lean}/` are explicit **stubs**; the `affinescript-vite/verification/proofs/` files are RSR **templates**; and `formal/` (the dir #513 names) **does not exist**. - The open soundness holes (#554/#555/#556/#558/#559) were tracked as defects but had **no proof obligations** linking them to the soundness arguments they falsify. **`K-1…K-4` — needs sharpened by outstanding work.** Codegen semantic-preservation (#513 must-have 7) is the **keystone** every face rests on; effect-soundness is **blocked** (not merely unproven) by the #555 handler mis-lowering; borrow soundness must be *stated to reject* the #554 counterexample. **`F-1…F-7` — NEW obligations from the faces work, entirely absent from the #513 programme:** - **F-1** transformer semantics-preservation (the *real* same-cube theorem — front-end analogue of K-1) - **F-2** same-cube cross-face agreement — *partially mechanized* in `invariant-path/proofs/SameCube.agda` (unit-tail case); the value-returning divergence is the concrete instance #601 - **F-3** pragma-detection determinism/totality/confluence (`lib/face_pragma.ml`) - **F-4** error-vocabulary faithfulness (`lib/face.ml` — a simulation, beyond OCaml's exhaustiveness check) - **F-5** `render_ty` injectivity / non-collision - **F-6** preview round-trip totality - **F-7** face confluence with canonicalisation Also catalogues the **aggregate-library** law-conformance obligation (cross-*cube*, vs faces' cross-*face*) and points the same-cube track at invariant-path's `SameCube.agda` + `verify-same-cube.sh`. ## Also in this PR - Rename `docs/PROOF-NEEDS.md` → `docs/PROOF-NEEDS.adoc` (DOC-FORMAT). - Update the three referrers: `docs/NAVIGATION.adoc`, `.machine_readable/integrations/verisimdb.a2ml`, and `spec/FRG-PROFILE.adoc` — the FRG "no PROOF-NEEDS" honest gap is now **met** (path-to-D step 6 done; grade unchanged, still no `formal/` prover encoding). ## Scope / non-goals This is a **catalogue of obligations only** — no proof is asserted discharged, no code changes, no relicensing. Every `Status` column entry of `stated`/`prose`/`absent` means **not proven**. Cross-referenced to #513 (it *adds* the faces + aLib obligations #513 omits) and #563. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr --- _Generated by [Claude Code](https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr)_ Co-authored-by: hyperpolymath <paraordinate@yahoo.co.uk> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Mirror of the Deno-ESM fix (#606) for the JS backend, which shares the same Some/None/Ok/Err runtime preamble. A program that declares `type Option` / `type Result` (e.g. stdlib/prelude.affine) re-emitted those consts from the TyEnum lowering, redeclaring them (SyntaxError under node). Skip the preamble-provided constructors; user-defined enums are unaffected. The C backend does NOT share this bug — it emits a tag-enum plus distinct constructor functions (TAG_Some / Some()), with no Some/None preamble — so #607's "JS/C" item is JS-only. Adds a JS-path regression guard alongside the existing Deno one. Verified: stdlib/prelude.affine -> JS has a single `const Some` and loads under node; dune test 460 green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8

The core-Wasm backend rejected any tuple sub-pattern that wasn't a plain variable or wildcard (UnsupportedFeature "Only variable and wildcard patterns supported in tuple patterns") — which stdlib/option.affine and result.affine hit. gen_pattern now recurses per tuple element: each element is loaded into a temp local and matched against its sub-pattern, with the per-element test bools ANDed together. Every gen_pattern result is one-bool-net with net-zero binds, so the combination is stack-safe; binds register via the threaded ctx (the same mechanism constructor-argument patterns use). Verified under node: `match (a,b) { (0,y)=>y, (x,0)=>x+100, (x,y)=>x+y }` selects the right arm and binds correctly — (0,5)->5, (7,0)->107, (3,4)->7. option.affine / result.affine now get PAST this gap (they next hit a separate `panic`-builtin gap in the Wasm backend, tracked in #607). dune test 461 green; adds a Wasm nested-tuple regression test. Part of #607. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8

…rep match Zero-argument variants (None, plain enum cases) were emitted as raw i32 tags while argument-carrying variants (Some(x), Ok/Err) were heap pointers to [tag][fields]. A `match` over a value that can be either form (Option/Result) mis-read one as the other: `match None { Some(v) => v, None => d }` dereferenced the raw tag as a pointer in the Some(v) arm and returned garbage instead of d (#607). Box zero-arg variants as a heap [tag] too, so EVERY variant value is uniformly a pointer; the zero-arg match arm now dereferences [ptr+0] for the tag, symmetric with construction and with the args path. Touches the construction sites (bare-ident ExprVar, ExprVariant) and the zero-arg PatCon match. Verified under node: unwrap_or(None,99)=99 and unwrap_or(Some 7,99)=7 (the None case was 0 before); Result Ok/Err and plain multi-constructor enums unchanged. dune test 461 green; adds tests/codegen/mixed_variant_match — a runtime regression (main()==9907) executed by run_codegen_wasm_tests.sh. Closes the mixed-representation match item in #607. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8

Reconcile the metatheory-proofs branch (61 commits off an old base) with the standalone-CI + codegen work that has since landed on main. Conflict resolutions: - CI workflows (governance.yml, scorecard.yml, scorecard-enforcer.yml, hypatia-scan.yml): take main's versions. main migrated these off the estate "standards" reusables to self-contained standalone gates (#603/ #604) precisely to stop the run-creation startup_failures; the branch's re-adoption of the reusables predates that work. main's hypatia-scan.yml also restores the permissions Hypatia needs (security-events: write, pull-requests: write, secrets: inherit) and the MPL-2.0 SPDX id that the Palimpsest license doc itself mandates for tooling. - docs/PROOF-NEEDS: drop the branch's stale 103-line .md; keep main's canonical 359-line .adoc authored in #609 (also satisfies DOC-FORMAT). - docs/history/MODULE-SYSTEM-PROGRESS: keep the branch's .md -> .adoc migration; port main's additive #138 codegen-follow-up note + status- table row into the .adoc so main's work is not lost. spark-theatre-gate.yml and mirror.yml were identical to main. Tree builds clean (dune build). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8

…ict (#616) ## What Clears the **last** merge conflict blocking #614. After #615 was **squash-merged**, the feature branch gained `main`'s content but not its ancestry, so #614's 3-way merge re-derived one conflict: `docs/history/MODULE-SYSTEM-PROGRESS` (modified on `main` in #602 / migrated to `.adoc` + deleted on this branch). ## Fix Match `main` exactly for that one file — restore `main`'s `.md`, drop the `.adoc`. **No content is lost**: `main`'s `.md` already carries the #138 codegen-follow-up note. The `.md`→`.adoc` migration can be redone later as a standalone DOC-FORMAT change. This resolution is **squash-robust** — it makes the file modify/modify-identical rather than modify/delete, so #614 stays conflict-free regardless of how this PR is merged. ## Verified - Trial merge of the fixed feature branch into `main`: **0 conflicts** ("Automatic merge went well"). - `dune build` clean (docs-only delta from the already-green #615 tree — `dune test` 534/534 there). Merging this into `feat/solo-core-metatheory-proofs` makes **#614 mergeable** and triggers its full CI. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8 --- _Generated by [Claude Code](https://claude.ai/code/session_01Lz7pRcec2Z3tVtaAhvB3M8)_ Co-authored-by: Claude <noreply@anthropic.com>

hyperpolymath and others added 12 commits June 18, 2026 14:52

hyperpolymath marked this pull request as ready for review June 21, 2026 01:09

hyperpolymath merged commit 51a00c6 into feat/solo-core-metatheory-proofs Jun 21, 2026
4 of 5 checks passed

hyperpolymath deleted the claude/inspiring-newton-dg5wov branch June 21, 2026 01:09

hyperpolymath mentioned this pull request Jun 21, 2026

fix(docs): align MODULE-SYSTEM-PROGRESS with main — clears #614 conflict #616

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Merge main into feat/solo-core-metatheory-proofs (un-block #614)#615

Merge main into feat/solo-core-metatheory-proofs (un-block #614)#615
hyperpolymath merged 12 commits into
feat/solo-core-metatheory-proofsfrom
claude/inspiring-newton-dg5wov

hyperpolymath commented Jun 21, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 21, 2026

What

Why it was needed

Conflict resolutions (5 files)

Verification (merged tree)

How to use

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants