diff --git a/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc new file mode 100644 index 00000000..e187a453 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc @@ -0,0 +1,1657 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Owner: Jonathan D.A. Jewell +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Ephapax v2 — system architecture and ultracode completion plan +:toc: left +:toclevels: 2 +:sectnums: + +[abstract] +This plan synthesises three candidate routes (proof-first, dogfood-first and seam-contract) and the adversarial critiques of each. The evidence base is a read-only survey of `/home/user/ephapax` and its sibling repositories carried out between 2026-10-27 and 2026-11-04. + +The survey ran the following toolchains: + +* coqc 8.18.0 on a scratch copy of `formal/`; +* `cargo test` across the ephapax and typed-wasm workspaces; +* Agda 2.6.3 against agda-stdlib v2.3 for the Agda siblings. + +Idris2, Lean, Isabelle, zig, julia, z3 and the wasmtime CLI are not installed. Every claim that depends on them is marked *UNVERIFIED*. + +Nothing in this document proposes closing or extending `formal/Semantics.v` or `formal/Typing.v`. The legacy `Theorem preservation` is false (`formal/Counterexample.v`). It stayed `Admitted.` by owner directive until the owner ratified D0b (2026-11-05): P0 now retires it to a `Prop` statement, which the owner applies, rather than closing it. Because an `Admitted` statement is an axiom, the legacy theorem together with `Counterexample.v` also derives `False` (`evidence/SurveyCounterexamples.v`, F0). It therefore must never appear in the `Print Assumptions` of any headline theorem; see P0/P1 and D0b. + +Throughout, *ephapax-affine* means the internal sublanguage. It is not AffineScript. The two projects share only the compile target, typed-wasm. + +[IMPORTANT] +.Evidence preserved with this document (re-checked 2026-11-04) +==== +The survey ran in an ephemeral container, so its scratch files do not survive. The load-bearing witnesses were re-checked by hand and committed beside this plan: + +* `evidence/SurveyCounterexamples.v` (Coq 8.18, not part of `formal/_CoqProject`). It proves `False` from each of the two `Admitted.` v2 lemmas (F1), and from the legacy `Admitted` `Semantics.preservation` together with `Counterexample.v` (F0). It also proves the closed-context preservation failure (ClosedCex, F2), the echo cross-path failure (EchoCex part 1, F3), the stuck `EObserve` (EchoCex part 2, F4), PairDup (F5) and EchoCopy (F6). Apart from F0 and F1, every lemma prints "Closed under the global context". +* `evidence/probes/*.eph.txt`, with verdicts tabulated in `evidence/README.adoc`. These are the Rust-checker probes: `ephapax check` accepts dup2, dup4, pairdup and lamcap, and rec1 aborts with a stack overflow (exit 134). + +*Not re-checked:* the EscapeCex, L2Comp and LetCheck families were produced by a survey agent whose scratch files were lost to a container restart. Their statements in this plan are as that agent reported them. Rung P2 must re-create and land them before they are relied on. +==== + +[NOTE] +.Size scale and oracle shorthands used below +==== +*Size scale:* S is at most 1 session; M is 2–3 sessions; L is 4–8 sessions; XL is more than 8 sessions or open research. + +*ORACLE-COQ* means `cd formal && coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq -j4`, then `bash scripts/assumptions-gate.sh`. The gate script does not exist yet; it is created at rung P1. + +*CLOSED* means `Print Assumptions ` reports "Closed under the global context". +==== + +== Executive answer + +=== Fastest proof route + +. *Restore consistency (P0/P1, size S).* Today the build can derive `False`. +** `preservation_l1` (`formal/Semantics_L1.v:3323`, `Admitted.` at :3336) and `step_pop_disjoint_from_type_l1` (:3280, `Admitted.` at :3317) are both refuted by Qed files built in the same `_CoqProject`: `Counterexample_PreservationL1.v:154` and `Counterexample_StepPop.v:145`. +** `env_inconsistent_preservation_l1 : False` and `env_inconsistent_step_pop : False` compile (`evidence/SurveyCounterexamples.v`, F1). +** The owner ratifies retiring both lemmas to `Definition …_stmt : Prop`. +** `preservation_l2_via_l1` and `preservation_l2_lift_case` (`formal/TypingL2.v:334-357`) are made conditional. +** CI must *assert* `Print Assumptions` for every headline theorem against an *empty* allowlist. Today it only prints the output. No refuted `Admitted` may be allowlisted. That includes the legacy `Semantics.preservation`, because with `Counterexample.v` it derives `False` too. Under the ratified D0b (2026-11-05), P0 retires `Semantics.preservation` to `preservation_stmt : Prop`, refuted by `Counterexample.preservation_false`, so no import-closure quarantine is needed (hyperpolymath/ephapax#422). +. *Land the falsifiers in the repo before any design work (P2, size S).* The scratch counterexamples become in-repo Qed regression files against the *current* judgment: +** ClosedCex, EchoCex, EscapeCex, L2Comp, LetCheck; +** PairDup (`has_type_l1` lets a `TProd` variable duplicate a linear `TString` in Linear mode, CLOSED); +** EchoCopy (`TEcho` can be `ECopy`'d in Linear mode). +. *One owner decision packet (P3).* It covers: +** a v2-owned fork of the syntax, typing *and* step relation under `formal/v2/`; +** runtime frames; +** locally nameless region binders; +** latent region effects with prenex region polymorphism; +** per-binder usage grades with the modality as the preorder; +** syntactically distinct echo forms plus `S_Observe`; +** a global function environment for top-level recursion. +. *Build `formal/v2` and test it before proving (P4–P6).* +** Write the skeleton and `Regress.v`, re-encoding every counterexample. +** Write an executable `step_v2_fn` and a naive `check_v2`. +** Write a *typed-by-construction* term generator with a measured acceptance floor, and only then run the property falsifier. +. *Prove L1 with L2 folded in (P7–P10).* +** Prove the opening, renaming and substitution lemmas and the canonical forms. +** Then prove `progress_v2` and `preservation_v2`. +. *Then L3, L4, the meta plane and the certified checker (P11–P15).* + +=== Fastest engineering route + +. *Close the Rust holes and fail loudly (E0/E1, size S–M).* No owner decision is needed: compound linearity is conservatively rejected, independently of D5 (which may relax it in W1). +** Make `let!` contraction honour `demands_consumption` (`src/ephapax-typing/src/lib.rs:191-201`). +** Reject closures that consume a captured linear value (`lib.rs:1109`). +** Reject pairs that contain a linear value. +** Turn the recursive-`data` stack overflow into an error. +** Make perform/handle a `CodegenError` (`src/ephapax-wasm/src/lib.rs:1991-2000`). +** Make `@total`, `@pure` and `@comptime` errors until they are enforced. +. *One front end and a wasm runner (E3/E4).* `ephapax-driver::load_program` serves every tool, and `ephapax run` executes the compiled wasm through the wasmtime 36 crate. +. *A typed side table from the *existing* checker feeds codegen (E5).* This fixes I64/F32/F64 binops, `String.len` and n-tuples. It is *not* gated on the certified checker. +. *An aLib conformer today (E6).* `stdlib/ALib.eph` plus a wasmtime-based Rust test over pinned vectors. The measured baseline is 89 pass / 1 fail / 13 skip / 51 unimplemented. +. *Then the upstream fix to the typed-wasm access-site convention*, after which the full gate is on by default (E8). +. *Then grammar reconciliation*, generics, `M.Ctor(x)`, recursive types and closures behind `--unstable-core`, the stdlib port, and the LSP. + +=== Where the two routes meet + +* *The core interchange.* The `ephapax-ir` S-expression codec, plus a new Rust-core→Coq-`SyntaxV2` translator, is the single exchange format for differential testing. +* *The soundness-direction gate.* "Rust accepts ⇒ oracle accepts" is asserted at zero tolerance from the moment `check_v2` exists. The completeness direction is report-only until the Rust checker is rewritten as an image of `CheckV2.v`. +* *One ADR for compound linearity and grades.* The hole exists in *both* Coq (PairDup) and Rust (`pairdup`), so the decision is made once for both. +* *Translation validation at the target.* Every module emitted by the default `compile` path must pass `typed_wasm_gate::gate_module`. Output of `compile --no-verify` is outside this claim, and the flag says so when used. This is how E5a (carrier soundness) is discharged, rather than proving full compiler correctness. + +== Ground truth as of this survey + +Sources: the scratch builds and probes recorded in the dossier, plus spot checks in this session. `_CoqProject` lists 18 `.v` files, and `Counterexample.v` appears once. There are 8 `canonical_*` lemmas in `Semantics_L1.v`. No region-renaming function exists in `formal/`. At the survey base, `scripts/status-gate.sh` still read `PROOF-NEEDS.md`. #418 fixed this, and it was re-run after `main` was merged into this branch (`10339b3`): `status-gate[proofs]: OK — admitted proofs: 3`. `Counterexample.v:186` imports `TypingL1`. `ocaml`, `ocamlfind` and `coqtop` are installed. + +[cols="2,3,3,3",options="header"] +|=== +|Area |Claimed |Verified |Mismatch + +|Coq build +|green +|18 files, exit 0, about 1m42s +|none + +|Outer `Admitted.` count (comments stripped) +|PROOF-NEEDS: 3; PROOF-STATUS.a2ml: 4 admits + 1 axiom; Semantics_L1.v banner: 3; CLAUDE.md: "6 regressed" +|3: Semantics.v 1, Semantics_L1.v 2 (+2 `admit.`); 0 `Axiom`. A raw grep finds 21 matches in Semantics_L1.v, all in comments. +|PROOF-STATUS.a2ml, the banner and CLAUDE.md are stale + +|Consistency of the global environment +|implicitly consistent +|*Inconsistent*: `False` is derivable from `preservation_l1` + `preservation_l1_FALSE`, and likewise for step_pop. The legacy `Semantics.preservation` (`Admitted`, kept by directive) together with `Counterexample.v` also derives `False` (F0). +|critical; not recorded in any doc + +|`preservation_l1` partial progress +|"29–30 of 33 cases Qed" (header :3194-3233, PROOF-STATUS) +|body is `intros …; admit.` (:3323-3336); the theorem is Qed-false +|header overclaims + +|L1 counterexample families +|2 in repo +|in repo: Counterexample_PreservationL1 and _StepPop. Committed in `evidence/SurveyCounterexamples.v` (outside `_CoqProject`), Qed and CLOSED: ClosedCex (G=[]), EchoCex (echo crosspath and stuck `EObserve`), PairDup, EchoCopy. Reported by a survey agent but lost with its scratch files: EscapeCex (region escape through a TFun closure), L2Comp, LetCheck (a completeness gap, not a soundness one) +|4 are in `evidence/` (outside `_CoqProject`); 3 are lost and must be re-created + +|Compound linearity in Coq +|not discussed +|`is_linear_ty TProd = false` (Syntax.v:468-474), and `T_Var_Unr_L1` with `T_Fst_L1` duplicates a linear `TString` (`evidence/SurveyCounterexamples.v` `pair_dup_linear_string`, F5, CLOSED) +|a hole in the v2 judgment itself + +|`preservation_l3` +|"conditional on an L1 admit" (pre-#418 CLAUDE.md, V1-TO-V2, STATUS.adoc) +|CLOSED, but it is only a conjunction of two case lemmas (:3450-3468) with a weak/strict freedom mismatch +|docs are stale and the scope is overstated + +|L2 +|`linear_to_affine` Qed; L2 landed +|`linear_to_affine` and `weaken_modality` CLOSED; the beta lemmas are CLOSED with P1/P2 side conditions; `has_type_l2` does not compose (L2Comp) +|`preservation_l2_via_l1` rests on a false axiom + +|L4 +|"Phase A scaffold landed" +|`L4.v`: 2 `eq_refl` definitions, no theorem, imported by nothing +|scaffold only + +|Qed counts per file +|PROOF-NEEDS §4: Semantics_L1 54, Echo 12, TypingL2 10, Modality 1 +|52 / 19 / 14 / 2; RegionEnvL1 18 is omitted from that table +|stale + +|Canonical forms +|"7" +|8 (`canonical_string_l1` plus 7 `*_l1_m`) +|minor + +|CI Print Assumptions +|"build truth is the Print Assumptions CI gate" (Semantics_L1.v:4) +|`coq-build.yml` only pipes the output to `tail` +|gate not enforced + +|`status-gate.sh --proofs` +|working +|exit 1 at the survey base: it read `PROOF-NEEDS.md`, but the file had been renamed to `.adoc` +|fixed on `main` by #418 (exit 0 at `10339b3`) + +|Rust workspace tests +|488 (TEST-NEEDS.adoc:24) +|507 pass, 0 fail, 0 ignored; v2 phase tests 17 + stdlib import 3 +|count stale + +|v2 grammar coverage +|"ACTIVE, phases pass" +|traits, impl, effect/handler decls, comptime, contracts, capabilities, where-clauses, `with` effect types, annotation args and `import … from` are all parse errors; EBNF and pest disagree on `` vs `[a]` and on the import syntax +|large spec/implementation gap + +|Rust checker soundness +|"memory-safe" +|accepts: `let!` reuse (dup2 returns 10), pair duplication, re-calling a capturing closure; all three pass `--verify-ownership` clean +|soundness holes + +|Recursive `data` +|supported in specs +|compiler stack overflow (rec1) +|crash + +|Codegen typing +|typed +|all binops lower to i32 (`lib.rs:3019-3039`); I64/F64, `String.len` and 3-tuples produce invalid wasm; function-typed parameters produce "unknown table 0" +|untyped codegen + +|Front end +|one language +|run/repl/lsp/query use the v1 `parse_module`; `check` has no import resolver +|split language + +|Corpus +|— +|120 `.eph` files; 14 compile, 12 check, 104 parse failures; the 5 `conformance/invalid` files all fail at *parse*, not for their intended reason +|negative corpus is vacuous + +|stdlib +|"partial implementation" +|compile: 1/9 (Argv). Check: 2/9 (Argv, Coproc). `src/ephapax-stdlib` crate: no consumer +|overclaim + +|typed-wasm seam +|seam tests green +|seam tests 6/6 and 3/3 pass; `gate_module` accepts *0/17* ephapax modules; after a byte-offset→operator-index translation, 17/17 are clean +|a typed-wasm-internal contradiction with ADR-0003 + +|typed-wasm L10 +|linearity enforced on bytes +|a `local.set` copy bypasses it (aliasprobe); a payload with count 0xFFFFFFFF aborts with a 137 GB allocation +|soundness hole and DoS + +|typed-wasm tests +|— +|197 default / 209 with `--all-features` +|none + +|`--mode affine` vs `--mode linear` +|distinct sublanguages +|byte-identical output +|ephapax-affine is invisible on the wire + +|aLib (aggregate-library 48b7694) +|"29 / 22 / 20 ops" across its docs; `just validate` works +|29 specs, 154 vectors; `just validate` / `just test` fail (`.md` globs); `not.adoc` has contradictory vectors +|several + +|aLib against ephapax (scratch) +|no conformer +|89 pass / 1 fail (spec defect) / 13 out of the I32 domain (10 decimal + 3 string-valued `if_then_else`) / 51 unimplemented +|n/a + +|Idris2 (ephapax `src/abi`, `idris2/`; typed-wasm `src/abi` incl. VerifierSpec, Layout.*; januskey A-/C-rows; anytype) +|"Qed", "22/22 modules" +|*UNVERIFIED* (no idris2). Read-only finding: the typed-wasm VerifierSpec agreement is true by construction, and Idris E1 is stated in the legacy shape and cites the false Semantics.v +|cannot check here + +|Lean / Isabelle (tropical-types, occupancy stackcert) +|various +|*UNVERIFIED* +|— + +|zig / julia / z3 / wasmtime CLI / Creusot +|various +|*UNVERIFIED* +|— + +|Agda siblings +|green on the pinned 2.6.4.3 +|green on *2.6.3*: echo-types All/Smoke, secret, epistemic, occupancy (with resource-algebra 0b338c9), choreographic (with resource-algebra b2c9f1f and the working-tree epistemic, not pin 495db9c), residual, absolute-zero (4 modules), januskey (with resource-algebra cf9235c) +|version mismatch recorded + +|absolute-zero +|CNO terminates and is thermodynamically reversible; Coq/Lean/Isabelle "VERIFIED" +|both Agda fields are vacuous by definition (CNO.agda:165-170, 201-206); the Coq/Lean/Isabelle trees are archived +|overclaim + +|jtv-halting-islands-ct +|"grammar membership = termination", 45 tests +|Rust binary ignores its input, has 0 tests, and does not reject `violation.jtv` +|not citable + +|januskey +|135 tests +|135 pass +|none + +|typell-ephapax +|ephapax bridge +|9 pass; models pre-v2 ephapax (`mut` affinity, no regions, no echo) +|lags v2 +|=== + +=== Corrections applied to the input routes + +* `_CoqProject` does *not* list `Counterexample.v` twice. There is no de-duplication task. +* There are 6 in-repo `Counterexample*.v` files, not 18. Of the other families, 4 are in `evidence/SurveyCounterexamples.v` (outside `_CoqProject`) and 3 were lost and must be re-created; all are landed first (P2). +* LetCheck is a *completeness* gap: v2 must make `let_unit` typable. It is not a term to prove untypable. +* PairDup settles the open X4 question: compound linearity is a hole in the *Coq judgment*, not only in Rust. It therefore moves into the first judgment revision, under the doctrine "holes before anything". +* Editing `TypingL1.v` in place ripples into the fenced `Counterexample.v` (`:186` imports it, and `:192-254` inverts over its constructors). The v2 typing must therefore be forked as well, not only the step relation. +* A configuration-level frame stack alone cannot tell an entered `ERegion` from an unentered one (`Syntax.v:122`). A runtime-only frame form in `SyntaxV2.v` is the main path, not a fallback. +* The EFrame-at-Enter design needs region renaming or opening, and there is none in `formal/`. Latent effects need region polymorphism. Both are added as rungs. +* A falsifier over random terms is vacuous. The typed generator moves into the same wave, with an acceptance floor. +* aLib "≥102 after decimals" is unreachable. With an F64 binding the ceiling is 99 unless string-valued `if_then_else` is also implemented. +* OCaml *is* installed, so extraction is not blocked by the toolchain. Whether OCaml is acceptable for the naive W2 oracle is a policy question (D9a, ratified in W1); the certified-checker form is D9 (W4). +* The Rust↔Coq differential needs a translator that does not exist yet. The Coq core has no recursion and no top-level declarations, so the v2 core gets a global function environment. +* W0 exit gates must not depend on another repository's owner. The typed-wasm gate criteria move to the wave after the upstream fix lands. + +== Target architecture + +=== System diagram + +---- + .eph v2 source (spec/ephapax-v2-grammar.ebnf == ephapax.pest : ONE normative grammar) + | S1 parse [O1: grammar-conformance fixtures; each EBNF production parses or is marked UNIMPLEMENTED + | and is rejected loudly] + v + ephapax-parser (pest) --> ephapax-surface AST (type params, mode decls, echo/observe/drop!, @comptime island) + | S2 desugar [O2: golden + metamorphic desugar tests; formal/v2/Desugar.v match_desugar_correct + | (data/match -> right-nested sums); surface sugar (traits, contracts) = pure desugar] + v + ephapax-desugar --> CORE v2 AST (src/ephapax-syntax mirrors formal/v2/SyntaxV2.v constructor-for-constructor) + | \______ ephapax-ir S-expr codec --> core->SyntaxV2 translator --> tools/ephapax-oracle + | (extracted check_v2 + step_v2_fn) + ephapax-driver::load_program (import resolver + package tier + surface + desugar) + used by check | compile | run | repl | lsp | query | fmt [O-D: driver_agreement.rs, check == compile] + | S3 check [O3: check_v2_sound Qed+CLOSED; CI: Rust-accept => oracle-accept, zero tolerance; + | verdict + Ty + R' + G' agreement report] + v + ephapax-check-v2 (Rust I/O-context algorithm: grades {0,1,w}, mode = preorder, R -> R', latent effects, + EFrame never surface-writable) ==> TYPED CORE (expr-id -> Ty, grades, regions) + | S4 semantics [O4: progress_v2, preservation_v2 (L1+L2), linear_echo_discharged (L3), + | mode_coherence / handoff_sound (L4), over StepV2 + ConfigWF] + v + meta plane (comptime halting island; ephapax-meta evaluator restricted to it) + | S4' meta [O4': comptime_normalises, comptime_ignores_runtime; spliced output re-checked by S3] + v + ephapax-wasm (typed dispatch; funcref table + closure ABI per typed-wasm ADR-005; boxed iso-recursive ADTs) + carriers: typedwasm.ownership (per-param kind from grade + mode, ret_kind, module mode record), + typedwasm.regions + typedwasm.access-sites (ADR-0003 BYTE offsets), + later: L9 lifetime-intervals for L1 region scopes (typed-wasm proposal 0006) + | S5 target [O5: E5a translation validation: typed_wasm_gate::gate_module == Ok on every module from + | the default path (--no-verify output excluded); formal/v2/CarrierSpec.v ownership_kind_sound; negative mutants + | rejected; Idris E5a restatement UNVERIFIED] + v + typed-wasm verify + gate (locals taint for L7/L10, bounded counts) --> wasmtime host (`ephapax run`) + | S6 library [O6: alib_conformance.rs ratchet over pinned vectors; eph_corpus_gate ratchet] + v + stdlib/*.eph: ALib, Prelude, Aggregate, Allen, Argv, Coproc, IO, Region, Stream, Transactions; later Reversible (RMR), Erasure (RMO) + + S7 cross-kernel [O7: formal/v2/CORRESPONDENCE.adoc: one row per mirrored theorem with Agda module@pin, + Coq lemma, both checker invocations + exit codes + checker versions] + S8 status [O8: generated PROOF-STATUS from coqc; Print-Assumptions allowlist; Admitted-vs-*_FALSE tripwire] +---- + +=== Formal stack (`formal/v2/`, Coq 8.18; oracle = ORACLE-COQ) + +---- + L4 L4Boundary.v module judgment has_type_mod with a declared mode; adjoint shifts EUp (Linear->Affine) + / EDown (Affine->Linear, only for obligation-free values); mode_coherence, handoff_sound, + program_safety_mod + L3 (folded) distinct echo forms (EDropE / ERegionE); EObserve + S_Observe; residue shape + {full, commitment, trivial} kept separate from obligation grade; TEcho has grade 1 in + Linear mode. Echo.v is bridged by mode_iso : Echo.Mode ~= the modality preorder. + L2 (folded) per-binder usage grades {0,1,w}; the modality m picks the preorder (Affine adds 1 <= 0); + compound types take the join of component grades; effect-typed application is a + rule of the one judgment (fixes L2Comp) + L1 TypingV2.v has_type_v2 m Sigma R G e T R' G'; locally nameless region binders; runtime-only EFrame typed + only by T_Frame; arrows TArr Rin Rout T1 T2 with prenex region abstraction for top-level fns + StepV2.v deterministic step_v2; Enter opens the binder with the canonical fresh name next_r carried + in the configuration (then increments it), so plain equality, not alpha, suffices; Exit removes the frame + ConfigWF.v R =_multiset frames(e) /\ store_typed mu /\ every ELoc tagged r occurs only while r is + framed /\ closed e /\ sigma_wf Sigma (every definition in Sigma + has its declared type, checked against the whole recursive Sigma) /\ next_r is above every + region name that is framed, free in e, or tags a store location + ProgressV2.v / PreservationV2.v / SafetyV2.v + meta MetaPlane.v first-order comptime calculus; structural Fixpoint as the termination certificate + tool CheckV2.v check_v2 + check_v2_sound (+ complete on the annotated fragment) + Extraction + Exec.v step_v2_fn + step_v2_fn_correct; typed term generator spec + Regress.v every counterexample family re-stated (untypable / not WF / preserved; LetCheck now typable) + LEGACY (frozen): Syntax.v, Typing.v, TypingL1.v; Semantics.v and Semantics_L1.v frozen except the D0/D0b retirement + (refuted statements now Prop: preservation_stmt, preservation_l1_stmt, step_pop_..._stmt) + (P0 retirement edits only), TypingL2.v (P0 only), Counterexample*.v (regression) +---- + +=== Components + +*Surface and grammar.* There is one normative grammar. The plan's default is to regenerate the EBNF from `ephapax.pest` and back it with a conformance fixture test, keeping every current EBNF production that the parser lacks as UNIMPLEMENTED rather than deleting it. Productions that are not implemented must fail with a named error, and E7's "0 productions unaccounted for" counts them; the specification never shrinks to make that number. + +*Desugar.* It stays the only place where sugar lives: `data`/`match` become right-nested sums, records become products, traits become dictionary passing, and contracts become asserts. Each lowering either has a `Desugar.v` lemma or is a pure syntactic macro that has a test. + +*Core.* `ephapax-syntax` is a Rust mirror of `SyntaxV2.v`. The additions over today's core are: + +* a global function table Σ, giving top-level recursion; +* iso-recursive `TMu` (after D7); +* `TArr` with Rin/Rout; +* region abstraction; +* grades on binders; +* distinct echo forms; +* `EObserve`. + +`EFrame` is runtime-only: the parser cannot produce it, and only `Enter` creates it. + +*Checker (L1–L4).* `ephapax-check-v2` is an input/output-context algorithm in the Hodas–Miller style. It has one function per `has_type_v2` constructor, named after that constructor. It returns `(Ty, R', G')` and emits the typed core. + +`ephapax-typing` remains as a façade until switch-over. `ephapax-linear` either becomes a thin linter over the grades or is deprecated, according to the D5 ADR. + +*Meta plane.* `@comptime` is a halting island: + +* no free recursive `comptime_call`; +* built-in bounded folds over finite type descriptors, with a cut-off at recursive types; +* no comptime inside `@emit_decl`; +* spliced output is re-checked by S3. + +`ephapax-meta`'s reflective `quote`/`eval` is fenced to that island. This needs a decision against ADR-016. + +*IR.* The typed core is the IR. `ephapax-ir` is the exchange format between the driver and the oracle; it is not a new optimisation layer. + +*typed-wasm backend.* Linear memory with a bump allocator and region stack, which is today's design. On top of that: + +* typed instruction selection; +* a funcref table using the ADR-005 closure ABI `[fnId@0, envPtr@4]`; +* carriers as listed in the diagram; +* `ret_kind` populated; +* an Affine ownership kind and a module mode record, once typed-wasm ratifies them. + +The *interop representation* question (linear-memory layout profile vs WasmGC) is D10. + +*Runtime.* There is one embedded runtime, generated by `ephapax-wasm`. `ephapax-runtime` and `ephapax-analysis` are either wired in or explicitly retired. Scrub-on-exit (`memory.fill` over the freed bump range) applies to regions marked sensitive. + +*stdlib via aLib.* `stdlib/ALib.eph` is scored against vendored, pinned aLib vectors. `Aggregate.eph` follows the echo-types `EchoAggregation` monoid-homomorphism shape. `Transactions.eph` and `Reversible.eph` are RMR; `Erasure.eph` is RMO. + +*Tooling.* LSP, REPL, query, fmt/lint and the package manager all run on the driver. The package manager's lockfile tier feeds the import resolver. + +=== How sibling repositories plug in + +All cross-kernel use is *port plus ledger*; nothing is imported across kernels. Per D-2026-10-12, Agda is the family proof kernel and Idris2 is used for ABI/runtime only. + +[cols="2,2,3,3",options="header"] +|=== +|Sibling |Plugs into |How |Obligation at the seam + +|echo-types (Agda) +|L3, `Echo.v`, residue taxonomy, RMR +|Coq ports of `weaken`, `degradeMode-comp`, no-section, DecorationStructure laws, `reversibility-via-totality`, EchoResidueCell once-only. The variance verdict (graded monad of accumulation, *not* a comonad) constrains residue composition. +|CORRESPONDENCE rows (coqc exit 0 + agda exit 0, versions recorded); no comonadic "recover from residue" rule + +|resource-algebra / tropical-types +|L1 region-count carrier (`RegionEnvL1.v`); optional cost/HWM effect layer +|The count-map carrier is already adopted. The Agda `ResourceAlgebra` requires idempotent ⊕, so it *cannot* host {0,1,ω} usage grades; keep separate sorts. +|instance laws Qed in Coq plus ledger rows; Lean UNVERIFIED + +|occupancy-types +|optional HWM peak analysis over linear memory +|separate graded-effect layer (P20), orthogonal to L2 +|`peak_sound`: dynamic live bytes ≤ static HWM; stackcert (Lean) and occ (Idris) UNVERIFIED + +|secret-types +|optional IFC layer +|three-law Lattice census; TINI holds only for a two-variable while-language +|new relational proof over the v2 core (XL); never folded into L2 + +|choreographic-types +|research route for D2 option (iii) and for L4 handoff +|K-CUT proven only for a finite, binary-choice, plain-merge fragment +|no claim outside that fragment + +|epistemic-types +|contracts and audit receipts (warrant ≠ proof) +|conceptual only +|none until contracts land + +|residual-evidence-types +|diagnostics +|candidate-world explanations in `ephapax-analysis` +|none (non-semantic) + +|anytype (Idris2) +|design reference only +|"pick the algebra, get the discipline"; no branching (no join), no soundness proof, UNVERIFIED +|must not become a dependency (kernel ruling) + +|absolute-zero +|shape of the RMO statement +|`is-OND` observation model; OND-5 non-composition +|cite only after the vacuous CNO fields (`terminates`, `energy-dissipated`) are documented as definitional + +|januskey + MAA draft +|RMR/RMO reference semantics; `Transactions.eph` +|`TransactionAtomicity.rollback-restores`; Loss grade {fin 0, ∞} ⊇ Linear≤Affine quotient +|MAA draft expired (2026-04-13) and attributes enforcement to Oblíbený; do not assimilate across the boundary; Idris rows UNVERIFIED + +|jtv-halting-islands-ct +|meta-plane totality by grammar +|the *principle* only; the current jtv artefact has no parser and 0 tests +|`MetaPlane.v` stands on its own Coq certificate, not on jtv + +|typell +|downstream consumer +|update typell-ephapax after D5 +|bridge tests green against v2 fixtures + +|typed-wasm +|compile target, VerifierSpec of record +|upstream fixes first (offsets, taint, bounds), then Affine kind and mode record +|S5 obligations above + +|aggregate-library +|stdlib semantics +|pinned vendored vectors +|ratchet; upstream fixes for spec defects +|=== + +== What needs creating + +Items marked "*(external)*" in the Home column live outside `hyperpolymath/ephapax`. + +[cols="3,2,4,1",options="header"] +|=== +|Component |Home |Why |Size + +|`formal/AssumptionsAudit.v` + `scripts/assumptions-gate.sh` + `formal/ASSUMPTIONS-ALLOWLIST` + Admitted-vs-`*_FALSE` tripwire +|ephapax +|CI prints but never asserts, which let an inconsistent environment stay green +|S + +|`formal/regress/` (ClosedCex, EchoCex, EscapeCex, L2Comp, LetCheck, PairDup, EchoCopy), as Qed against the *current* judgment +|ephapax +|makes every later judgment revision falsifiable by machine +|S + +|`formal/v2/{SyntaxV2,TypingV2,StepV2,ConfigWF}.v` +|ephapax +|the v2-owned core; forking syntax *and* typing keeps `Counterexample.v` (which imports TypingL1) untouched +|L + +|`formal/v2/Regions.v` (locally nameless region binders, open/close, renaming equivariance) +|ephapax +|needed for fresh names at Enter; no renaming exists in `formal/` +|M–L + +|`formal/v2/Regress.v` +|ephapax +|each counterexample family re-stated against v2 +|M + +|`formal/v2/Exec.v` + extraction prototype + `tests/differential` (crate `ephapax-differential`: typed-by-construction generator, mutation operator, acceptance and coverage metrics, and the `preservation_property` / `progress_property` / `determinism_property` tests) +|ephapax +|cheap falsifier before XL proofs; prevents vacuous property tests +|M + +|`formal/v2/{ProgressV2,PreservationV2,SafetyV2}.v` +|ephapax +|L1+L2 soundness +|L–XL + +|`formal/v2/L4Boundary.v` +|ephapax +|L4 has no theorem today +|L + +|`formal/v2/MetaPlane.v` +|ephapax +|backs "total and pure" (currently false) +|M + +|`tools/ephapax-oracle` + hand-written S-expr reader (trusted, labelled), first wrapping the naive `check_v2` (W2); later `formal/v2/CheckV2.v` (W5) +|ephapax +|certified reference for the Rust checker +|M–L + +|core→SyntaxV2 translator (named vars → locally nameless, multi-arg → curried, Σ for top-level fns, ADTs → sums) +|ephapax +|the differential cannot run without it; measures fragment coverage +|M + +|`formal/v2/Desugar.v` +|ephapax +|S2 contract for match/data +|M + +|`formal/v2/CarrierSpec.v` +|ephapax +|E5a checkable in Coq (the Idris side is UNVERIFIED) +|M + +|`formal/v2/CORRESPONDENCE.adoc` + `EchoBridge.v` +|ephapax (mirror in echo-types) +|`Echo.v` claims to mirror upstream but has no checked correspondence +|S–M + +|`scripts/gen-proof-status.sh` (generated PROOF-STATUS) +|ephapax +|every status doc disagrees with coqc +|S + +|`src/ephapax-driver` +|ephapax +|one language for every tool +|M + +|typed side table → `TypedModule` from the current checker (stopgap), later emitted by `ephapax-check-v2` +|ephapax +|untyped codegen produces invalid wasm +|M–L + +|`ephapax run` on wasm (wasmtime crate, host bindings) +|ephapax +|no runner exists; the interpreter fails on 2-parameter functions +|S + +|`src/ephapax-check-v2` +|ephapax +|the current checker is v1-shaped (cites Typing.v) and has 3 holes +|L + +|v2 conformance corpus with `// expect-error: ` headers +|ephapax +|the negative corpus fails at parse today +|S + +|`conformance/alib/{vectors.json,binding.ephapax.json,PINNED-COMMIT}` + `stdlib/ALib.eph` + `tests/alib_conformance.rs` +|ephapax +|stdlib semantic seam; no JS toolchain needed +|S + +|`examples/proving-ground/eph-agg` + `tests/proving_ground.rs` +|ephapax +|real program covering I64/F64, ADTs, closures, regions, `let!`, imports, package, runner, LSP +|M + +|`stdlib/{Erasure,Reversible}.eph` + scrub-on-exit codegen +|ephapax +|RMO/RMR primitives; physical scrub absent today +|M + +|ADRs: dyadic split / grades; compound linearity; region binders and polymorphism; echo determinism; recursive types; interop representation; comptime vs ADR-016; normative grammar source (syntax ADR); naive-oracle extraction target (D9a); checker oracle form (D9); certified-erasure statement (D12) +|ephapax (`docs/decisions`, `PRESERVATION-DESIGN.adoc` decision record) +|owner-gated design calls +|S each + +|Access typing honours ADR-0003 byte offsets (verify.rs:1235, codegen lib.rs:578); bounded wire counts; locals-taint L10/L7 +|typed-wasm *(external)* +|0/17 gate acceptance; `local.set` bypass; DoS abort +|M + +|Proposal: Affine OwnershipKind + module mode record; borrow axis kept separate from usage grade +|typed-wasm *(external)* +|ephapax-affine is invisible on the wire +|M + +|Linear-memory stdlib layout profile + aLib wasm-ABI binding profile + shared aLib runner crate +|typed-wasm *(external)* +|Layout.* is WasmGC-only and has no emitter +|M + +|`vectors/*.json` export, fn-string mini-grammar, `not.adoc` fix, Justfile `.adoc` globs, substring semantics +|aggregate-library *(external)* +|fix at source +|S + +|Ledger rows + RMR/RMO/OND correspondence note +|echo-types *(external)* +|cross-kernel honesty +|S + +|Grade-interface reconciliation note + TYPE-CONNECTIONS rows for ephapax and anytype; fix stale secret-types text +|nextgen-typing *(external)* +|five incompatible grade interfaces +|M + +|Restored parser + diode-negative tests +|jtv-halting-islands-ct *(external)* +|makes the principle citable again +|M + +|Linear-token undo API +|januskey *(external)* +|`undo(&str)` allows double-undo +|S–M + +|Document vacuous CNO fields; fix the archived-prover PROOF-STATUS rows +|absolute-zero *(external)* +|citation hygiene +|S + +|typell-ephapax v2 bridge +|typell *(external)* +|consumer lag +|S +|=== + +== Proof, theory and solver ladder + +=== On-trajectory rungs + +[cols="1,4,3,2,1",options="header"] +|=== +|Rung |Deliverable |Oracle |Depends |Size + +|P0 Consistency restore +|Owner-ratified retirement: `preservation_l1` and `step_pop_disjoint_from_type_l1` become `Definition …_stmt : Prop`. `preservation_l2_via_l1` and `lift_case` take `preservation_l1_stmt` as a hypothesis, or are deleted. The `*_FALSE` files still compile. The PR is framed as *retirement*, not closure (CLAUDE.md DO NOT #3 adjacency). #418 already corrected CLAUDE.md, V1-TO-V2.adoc and PROOF-NEEDS so they mark the L1 pair as refuted rather than residual debt. The same PR still has to record that these `Admitted` lemmas, and the legacy theorem, make the environment able to derive `False`. No document on `main` states that yet. Docs are applied by the owner, GPG-signed. +|ORACLE-COQ; `env_inconsistent_preservation_l1` and `env_inconsistent_step_pop` fail to compile (expected-failure targets); allowlist = `{}` for every headline. Under the ratified D0b (retire), `Semantics.preservation` becomes `Definition preservation_stmt : Prop` and `Counterexample.v` proves `~ preservation_stmt`, so `legacy_inconsistent` (F0) also fails to compile (expected-failure target) and the environment no longer derives `False`. +|owner ratification +|S + +|P1 Gate integrity +|`assumptions-gate.sh` covers every headline and is required in `coq-build.yml`. The tripwire keeps two lists. It fails on any *new* refuted `Admitted`: an Admitted `X` coexisting with a Qed `X_FALSE`, or a refutation registered without D0b approval. Entries on the owner-approved *quarantine* list are reported but do not fail CI, provided no headline depends on them. Under the recommended D0b option that list holds `Semantics.preservation` ↦ `Counterexample.bad_step`/`bad_typable`/`bad_post_untypable`, plus the L1 pair until P0 merges. Adding to the quarantine list needs an owner-ratified D0b amendment. `status-gate.sh`/`.yml` read `PROOF-NEEDS.adoc`. `gen-proof-status.sh` generates PROOF-STATUS. +|CI red when a dummy `Admitted.` is injected; `bash scripts/status-gate.sh --proofs` exits 0; generated file diff-clean +|none. Until P0 lands, the gate runs report-only for the two refuted L1 names and never allowlists them. +|S + +|P2 Land falsifiers +|ClosedCex, EchoCex, PairDup and EchoCopy are ported from `evidence/SurveyCounterexamples.v`; EscapeCex, L2Comp and LetCheck are re-created from their reported statements. All become `formal/regress/*.v`, Qed against the *current* judgment, with `Print Assumptions` CLOSED. +|ORACLE-COQ +|P0 +|S + +|P3 Decision record +|`PRESERVATION-DESIGN.adoc` "Experiment 3 decision record" covering D1–D8 and the syntax ADR (normative grammar source) (section 9), each with the default labelled and the X3 prototype table attached. +|merged and signed off by the owner +|X3, X4, X9, X11 (D8), X13 (D7) +|S (plus owner time) + +|P4 v2 core skeleton +|`SyntaxV2` / `Regions` / `TypingV2` / `StepV2` / `ConfigWF` with: + +* region binders in the D3 representation: locally nameless with cofinite quantification under the recommended option (P7 then proves open/close lemmas); concrete names with fresh renaming at `Enter` under the concrete option (P7 proves the equivariance lemma instead); de Bruijn indices under that option (P7 proves the shifting lemmas instead); +* runtime-only `EFrame`; +* a fresh-region counter `next_r` in the configuration that `Enter` uses and increments, so `step_v2_deterministic` holds up to plain equality rather than modulo alpha-renaming; `config_wf` requires `next_r` to exceed every framed, free or store-tagged region name, and P7 proves that `step_v2` preserves this (it is what `frames_fresh_at_enter` rests on); +* `TArr Rin Rout` with prenex region abstraction; +* signed integer literals and the I64/F32/F64 literal forms with their primitive step rules (today `Syntax.v` declares `TI64`/`TF32`/`TF64` but has only `EI32 : nat`); +* grades {0,1,ω} with modality = preorder; +* compound join; +* `TEcho` grade 1 in Linear mode; +* distinct echo forms; +* `S_Observe`; +* a typed foreign-signature environment Φ for `extern` declarations (stdlib `Argv.eph` and others), with a host-call step rule over a host *function* (total and deterministic by construction, so `step_v2_deterministic` survives). The host function also receives an immutable host input fixed for the whole run, which carries the argument vector: the program path as element 0 followed by `Run.args`, matching `stdlib/Argv.eph`'s contract that `argv_count()` includes `argv[0]` (a finite list of byte strings, well-formed when every entry is valid UTF-8 and the list length fits in I32), so `env::argv_count`, `argv_arg_len` and `argv_arg_get` are deterministic functions of it and are covered by P9 and P10. The metatheory takes `host_wf` as a *hypothesis*, never as an `Axiom`: a host call returns a value of the declared type, touches only the buffers passed to it, and preserves `store_typed`, region tags and ownership, and the rest of `config_wf`: it never frees or retags a passed location, and its result refers to no freed region. Each signature in Φ carries its own instance of these conditions. P9 and P10 are stated for every `host_wf` host; +* an explicit trap configuration: integer division or remainder by zero, and `MIN / -1`, step to `Trap`, while `MIN % -1` evaluates to 0 as Wasm `rem_s` does (matching the interpreter's `DivisionByZero` and the Wasm trap), and `progress_v2` reads "a value, a step, or `Trap`"; +* a global Σ for recursion, with a `sigma_wf` judgment (every definition checked against its declared type under the whole recursive Σ) that `config_wf` requires and that P9 and P10 take as a hypothesis; +* the recursive-type form D7 selected (ratified in W1, before P4), so P7–P13 are proved against the full core: iso-recursive `TMu` with fold/unfold under the recommended option; nominal named types with unfold at `match` under the nominal option; no recursive type former under the no-core-recursion option, in which case P8 drops `mu`, P17 becomes the encoding-alignment rung, and E9/E10 use the bounded encodings; +* store coherence in `config_wf`. + +Includes `step_v2_deterministic`. +|ORACLE-COQ; `step_v2_deterministic` CLOSED +|P3 +|L + +|P5 Regress.v +|Each family re-stated against v2: PreservationL1, StepPop, ClosedCex, EscapeCex, EchoCex, L2Comp, PairDup and EchoCopy each become untypable, not-WF or preserved. LetCheck becomes `let_unit_typable_v2`. `Counterexample.v` `bad_input_untypable_l1` is untouched and still Qed. +|ORACLE-COQ; all CLOSED +|P4 +|M + +|P6 Executable falsifier +|`Exec.v` with `step_v2_fn_correct`; a naive `check_v2`; its executable form per D9a (extraction to OCaml or Guile, or in-Coq `vm_compute` evaluation, with the 100k-term budget re-sized by X10 for the latter); a typed generator; a proptest for preservation, progress and determinism. +|ORACLE-COQ with `step_v2_fn_correct` CLOSED; `cargo test -p ephapax-differential --test preservation_property --test progress_property --test determinism_property`: 0 counterexamples over 100k *well-typed* terms; acceptance rate ≥ 20%; every `has_type_v2` constructor and every `step_v2` constructor (region exit, observe and the echo drop rules included) hit ≥ 100 times, because `step_v2_fn_correct` only relates the two steppers and cannot catch a rule both get wrong +|P4 +|M + +|P7 Structural lemmas +|Open/close/rename for region binders (or the D3 branch's equivalent: equivariance under concrete names, shifting under de Bruijn) and typing equivariance; substitution (port `subst_typing_gen_l1_m`); `value_R_G_preserving_v2`; weakening and strengthening; `frames_unique`, `frames_fresh_at_enter`, store coherence preserved. Includes a porting report on how many of the 52 Semantics_L1 Qed lemmas carry over. Step-shaped lemmas must be re-proved against `step_v2`. +|ORACLE-COQ CLOSED; `formal/v2/PORT-REPORT.adoc` with measured numbers +|P4, X4 +|L + +|P8 Canonical forms +|For every type former present at P4: unit, bool, i32, i64, f32, f64, string, arr, sum, prod, ref, borrow, region, echo, and the D7 recursive former (`mu`, or named types; none under the no-core-recursion option). Lists and n-ary tuples are not core formers: E12 lowers them to the D7 recursive sum and to nested pairs before translation. +|CLOSED +|P4 +|S–M + +|P9 `progress_v2` +|For closed well-formed configurations: every one is a value, steps, or is `Trap` (P4's trap configuration for integer division and remainder). EscapeCex and the stuck `EObserve` are already ruled out at P5. +|CLOSED +|P7, P8 +|M + +|P10 `preservation_v2` (L1 + L2 folded) +|All step cases, including an unconditional effect-typed beta. This discharges what #240–#242 were working toward. Corollary `type_safety_v2`. Sub-agents work by case family: region, drop, app/beta, let/case/pair, ref/borrow, echo/observe. +|CLOSED; allowlist unchanged +|P7, P8, P9 +|L–XL + +|P11 L2 metatheory +|`linear_to_affine_v2` as transport along the preorder inclusion; `weaken_modality_v2`; join plus 3 laws in the `Modality` pattern (`Echo.v:543-573`). +|CLOSED +|P10 (the join laws can start in W1) +|S–M + +|P12 L3 obligation +|`linear_echo_discharged` (no unobserved echo at a Linear value); a single freedom predicate replaces the weak/strict pair; `mode_iso`; residue-shape parameter. EchoCopy is untypable. +|CLOSED +|P10 +|M + +|P13 L4 boundary +|`has_type_mod`, `EUp`/`EDown`, `mode_coherence`, `handoff_sound`, `program_safety_mod`. +|CLOSED; a boundary-leak counterexample (`EDown` of an obligation-carrying value), added to `Regress.v` as part of this rung, is Qed-untypable +|P11, P12 +|L + +|P14 Meta plane +|`MetaPlane.v`: `comptime_normalises` (structural Fixpoint) and `comptime_ignores_runtime`. +|CLOSED +|E15 grammar (parallel) +|M + +|P15 Certified checker +|`check_v2_sound`; `check_v2_complete` on the annotated fragment; `check_mod`, covering `extern` signatures in Φ; extraction (target per D9). If D9 picks derivation certificates (the recommended option): `check_v2_cert` and `check_v2_cert_sound` (an accepted certificate implies `has_type_v2`), extracted or run under Coq. +|CLOSED; extracted oracle builds in CI and checks the corpus +|P10, P13, D9 ratified (with the X10 prototype attached) before W5 starts +|M–L + +|P16 Desugar seam +|`match_desugar_correct`. +|CLOSED +|P4 +|M + +|P17 Recursive types +|Alignment of the P4 recursive-type core (the D7 branch; described here for the recommended `TMu` option, with the nominal branch inserting no fold/unfold and the no-core-recursion branch aligning the encodings instead) with its producers and target: desugar inserts fold/unfold for recursive `data`, and the boxed codegen matches typed-wasm `listHeapType` WHT_Rec. No core syntax changes here, so P7–P13 are not invalidated. +|`progress_v2` / `preservation_v2` still CLOSED; desugar fold/unfold insertion covered by tests (re-checked by `Desugar.v` at P16) +|P10, D7 (P16 optional; until it lands, coverage is by tests) +|M + +|P18 Carrier seam E5a +|`CarrierSpec.v` `ownership_kind_sound` (grade + mode → kind). Restate Idris E1/E5a against `has_type_v2` (*UNVERIFIED*). +|CLOSED; gate acceptance from E8 +|P15, typed-wasm fixes, E8 completed (re-scheduled after any W2 delay), T5h merged +|M + +|P19 Ledger + RMR +|`EchoBridge.v`, CORRESPONDENCE rows, `rmr_restores`, `residue_once_only`. +|CLOSED; each row records coqc and agda exit 0 with versions +|P12 +|M–L +|=== + +=== Detours and optional rungs + +These are kept off the critical path. + +* *P20 graded-effect layer* (cost = MaxPlus, occupancy = HWM): a Coq port of resource-algebra Core. It is orthogonal to L2. Size L. +* *P21 `erase_noninterference`* (RMO): a binary logical relation with an `is-OND` observation model. Physical scrub is a *tagged METAL-BOUNDARY axiom*. That needs explicit owner sign-off, must be allowlisted by name, and must never appear in the `Print Assumptions` of any L1/L2 theorem. Size XL. +* *IFC layer* over secret-types TINI. Size XL; deferred. +* *Generalising L2 into an anytype-style single algebra.* This is a detour. No existing interface hosts usage grades, cost, HWM and labels together (idempotent ⊕ vs 1+1=ω), and doing so would break four-layer orthogonality. +* *Full E5b* semantic compiler correctness. XL; deferred behind translation validation. +* *Explicitly out of scope:* anything touching `Semantics.v`, `Typing.v`, `Syntax.v` or the legacy preservation statement, except the owner-ratified D0/D0b retirement under P0/T0g (an agent prepares it; the owner reviews and signs it). + +=== Theory hooks that could give a more final solution + +* *Semantic soundness* via a unary step-indexed or Iris-style logical relation with region liveness as a world or resource. It gives safety without syntactic preservation. The *same* relation, made binary, delivers `erase_noninterference` (P21) and an IFC result. This is the fallback if K1 fires (section 10), and arguably the more final architecture once L1 is stable. +* *Proof-producing checker.* `ephapax-check-v2` emits a typing derivation, and Coq checks it, or an extracted certificate checker does. This removes Rust from the trusted base per program, without extracting the whole checker (D9 option D). +* *RichWasm* (Coq-mechanised typed Wasm with linear/unrestricted qualifiers and regions) as a target-IR model. It turns E5 into a typed translation. +* *QTT grades with a mode preorder.* Linear vs Affine is exactly whether `1 ≤ 0` holds. This unifies L2 placement (D5), the Rust `let`/`let!` split and the wire ownership kinds. +* *Adjoint/LNL shifts* for L4 (Pruiksma–Pfenning mode preorders). +* *Calcagno–Helsen–Thiemann* syntactic region soundness (runtime frames). *Tofte–Talpin* latent effects and region polymorphism. *Aydemir et al.* cofinite quantification for region binders. +* *2LTT / staged calculi* for the meta plane: a total meta level generating a partial object level. +* *Abstract interpretation over Wasm locals* (must/may use-count lattice) for the typed-wasm L10 fix. + +== Engineering ladder + +[cols="1,4,3,2,1",options="header"] +|=== +|Rung |Deliverable |Gate |Depends |Size + +|E0 Holes first +|`mark_used` routes through `demands_consumption` (lib.rs:191). `check_lambda` rejects consuming a captured linear value. `Ty::is_linear` takes the join over Prod/Sum/Tuple/List (conservative *reject*, D5-independent; D5 in W1 may relax it). Recursive `data` gives a `DesugarError`, not an overflow. Dereferencing a borrow of a linear value may not consume ownership (today `check_deref` returns the owned inner type, `ephapax-typing/src/lib.rs:1739`, and borrows are not loan-tracked). A pattern may not discard a linear payload: a wildcard over a linear component, or a duplicate binder, is rejected (today a wildcard binds nothing, `lib.rs:1592`). +|`tests/linearity_holes.rs`: dup2, dup4, pairdup, lamcap, sum-, tuple- and list-of-linear duplication probes, a double-borrow-then-drop probe, and a `(_, y)` match over a linear pair are each rejected with a named `TypeError` kind; rec1 fails with the named `DesugarError` and the compiler's normal error exit, never a crash or abort; `cargo test --workspace` green (≥ 507) +|none (escalation note for pairdup) +|S–M + +|E1 Fail loudly +|Perform/Handle give a `CodegenError`. `@total`, `@pure` and `@comptime` give an "annotation not enforced" error. Raw variadic `__ffi` (probe g5) is rejected with a named error; typed `extern` declarations are the only FFI path, since only they have a formal-core representation (Φ). The import-index bug (lib.rs:478, 579) is fixed for `extern`. `-O`, `--debug` and `check --mode` take effect or are rejected. +|`tests/fail_loud.rs`: the perform/handle probes return `CodegenError` without producing a module. g5 fails with the named raw-FFI error; an `extern`-based rewrite of g5 compiles to a module whose imports are contiguous and which passes structural validation. The `@total` loop, an `@pure` function with an effect and an `@comptime` declaration are each rejected with the "annotation not enforced" error. `-O`, `--debug` and `check --mode` each have a test showing they either take effect or are rejected. (`compile_match` legitimately emits an `unreachable` fallback, so the gate does not ban `unreachable` globally.) +|none +|S + +|E2 Real negative corpus +|`conformance/{valid,invalid}` rewritten in v2 syntax with `expect-error` headers; `examples/v2/hello.eph` fixed. +|`eph_corpus_gate` asserts the error kind; reverting E0 turns it red (CI mutation job); `examples/v2/hello.eph` compiles and runs +|E0 +|S + +|E3 Driver +|`src/ephapax-driver` used by every tool; `src/ephapax-tools` either joins the workspace or is excluded. +|`driver_agreement.rs`: every entry point (check, compile, run, repl, lsp, query, fmt) loads each corpus file through `ephapax-driver` and agrees on parse/desugar success; check == compile on all corpus files, which holds because `check` runs the same unsupported-feature validation as codegen (so the E1 fail-loud forms, such as the `perform` probe, are rejected by both with the same named diagnostic until E17); an integer literal above `i64::MAX` is a named `ParseError` on every entry point (today the core-parser fallback turns it into 0 via `unwrap_or(0)`, `ephapax-parser/src/lib.rs:965`), with a corpus-gate fixture; `qualified-import/app.eph` and `bridge.eph` check +|none +|M + +|E4 Runner +|`ephapax run` executes wasm and forwards `Run.args` (today discarded as `args: _`, `src/ephapax-cli/src/main.rs:193`) through the wasmtime host imports `env::argv_count`, `argv_arg_len` and `argv_arg_get` that `stdlib/Argv.eph` needs, with the program path synthesised as `argv[0]` (clap's trailing `args` holds only what follows the file); the interpreter becomes `run --interp` and is fixed or marked. +|`ephapax run p1.eph` prints 162; an argv fixture prints its arguments correctly for at least three argument vectors (none, one, several), and `argv_count()` is 1 when no arguments follow the file; interpreter and wasm agree on the compiling corpus, except files listed in a checked-in `interp-known-failures` list when the interpreter is marked +|E3 +|S–M + +|E5 Typed codegen (stopgap) +|Expr-id → Ty side table from the current checker; typed binop/literal/string/tuple; F32 and F64 rem lowering to an exact `fmod` helper emitted into the module (Wasm has no float remainder instruction, and the naive `x - trunc(x / y) * y` is wrong under rounding, quotient overflow and signed zero, so it must match the interpreter, which uses Rust `%`, i.e. IEEE `fmod`); an F32 source literal form (an `f32` suffix such as `1.5f32` in `ephapax.pest`, producing `Literal::F32`, recorded in the syntax ADR with a conformance fixture), since today every float literal parses as `Literal::F64`; I64 literals (probe `i64`, which as stored exercises only an I64 parameter). Typed unary lowering (`i64.sub` from 0 for I64 negation, `f32.neg`/`f64.neg` for floats; today `compile_unaryop` always emits `I32Const(0)`/`I32Sub`, `ephapax-wasm/src/lib.rs:3047`). Wrapping integer overflow as the defined semantics, matching Wasm, with the interpreter switched to `wrapping_*` operations. Element-width-aware list storage and retrieval (today `list_append`/`list_get` are `(i32, i32) -> i32`), so I64, F32 and F64 elements are stored in full. Beyond these named cases, E5 is driven by a generated *type × operation conformance matrix*: every operand type the checker accepts, for every binary operator, unary operator and comparison, and every value type in every container position (pair field via `Pair`/`fst`/`snd`, which `compile_pair` lowers separately from n-ary tuples, tuple field, list element, sum payload, extern parameter and result), every control-flow result position (`if`, `case`/`match` and block results; today `compile_if` fixes the block result to I32, `ephapax-wasm/src/lib.rs:2963`), and the `copy` and `drop` forms (today `compile_copy` stores through an I32 temporary). Closure parameter and result positions join the matrix in E9, where type-indexed closure lowering lands. List indexing is bounds-checked in Wasm (today `gen_list_get` computes the address and loads unchecked, `ephapax-wasm/src/lib.rs:1859`) and traps on a negative or oversized index, matching the interpreter's `IndexOutOfBounds`, which E5 treats as a trap. Today sums use `I32Store`/`I32Load` regardless of payload, and comparisons emit I32 instructions for every type. String equality compares contents, as the interpreter does, not pointers. +|`wasm_e2e`: i64, f32, f64, s1, s6, t3 return correct values (i64 evaluates an I64 literal outside the I32 range, such as `5000000000`, inside the returned expression with a checked result; f32 = a literal plus arithmetic case and a `%` remainder expression, each with a checked result; f64 includes a `%` remainder expression with a checked result, so the integer-only `I32RemS` path cannot pass); an interpreter-vs-wasm remainder table for both float types covers `1.0 % 0.1` (rounding), `-0.0 % 1.0` (signed zero), `1e308 % 3.0` (extreme ratio), `x % inf` and NaN operands, with bit-identical results (NaN results need only both be NaN); a negative I64 result (`-5000000000`) and negated F32/F64 values are checked; interpreter-vs-wasm boundary cases for I32 and I64 add, subtract, multiply and negation at the type limits agree under wrapping; integer `/` and `%` by zero, and `MIN / -1`, trap in both, and `MIN % -1` yields 0 in both (the interpreter reports `DivisionByZero` or overflow as a trap, never a wrapped value, matching P4's `Trap`); lists of I64 and F64 values round-trip a value outside the I32 range; negative and oversized list indices trap in both interpreter and Wasm; the full type × operation matrix runs interpreter-vs-wasm with 0 disagreements and 0 invalid modules, including I64 and F64 sum payloads, I64/F32/F64 comparisons and equal-content strings allocated separately; corpus compile count > 14 +|E3 +|M–L + +|E6 aLib conformer +|`ALib.eph` (20 scalar ops), vectors, binding with reasoned skips, `alib_conformance.rs` ratchet. +|pass ≥ 89, 0 unexpected FAIL, every skip has a reason; after E5 with an F64 binding: pass ≥ 99 +|none (widens after E5) +|S + +|E7 Grammar + generics +|One normative grammar plus a conformance fixture test. `SurfaceDecl::Fn` type params (desugar lib.rs:323). Until E13 brings grades, unconstrained type parameters are treated as linear (today `Ty::is_linear` makes `Ty::Var`/`Ty::Unif` non-linear, `ephapax-syntax/src/lib.rs:154`), so a generic body cannot duplicate a value that is later instantiated at a linear type. Desugar monomorphises type parameters before the core, so the core, the translator and `CheckV2` only see monomorphic terms; polymorphic recursion is rejected with a named error. `M.Ctor(x)` lowers to `Construct`. Match guards are honoured by desugar (today `build_arm_body_inner` never consults `arm.guard`, `ephapax-desugar/src/lib.rs:1169`, so `Some(x) if false` is taken unconditionally), or guarded constructor arms are rejected with a named error until they are; P16 proves the lowering later. Import and extern syntax reconciled. +|`gen_angle.eph` and `qa/app2.eph` compile and run; a guarded constructor match whose guard is false falls through to the next arm in both interpreter and wasm (or is rejected with the named error); `fn dup(x: a) = (x, x)` is rejected with a named `TypeError` (and so cannot be instantiated at a region-owned `String`); `id` instantiated at two types desugars to two monomorphic core functions that translate to `SyntaxV2`; 0 EBNF productions unaccounted for +|E3, the syntax ADR (normative grammar source) ratified in the W1 T1a packet +|M + +|E8 Gate on by default +|Pin bump to a typed-wasm rev with the fixes; add the `typed-wasm-gate` dependency; `compile` runs `gate_module` by default (`--no-verify` escape; also on the sexpr path); `ret_kind`; fix the seam-test comment overclaim; negative mutants. +|`typed_wasm_full_gate.rs`: accepted == compiled corpus count, 0 rejected; `local.set` alias and count-0xFFFFFFFF mutants rejected with `Err`; a fixture with a linear return type decodes to the matching non-Unrestricted `ret_kind`, and a mutant that flips it is rejected by the gate; the sexpr compile path is gated; `--no-verify` skips the gate and says so +|typed-wasm upstream fixes from T1b/X7 (byte offsets, bounded counts, locals taint) merged; D11 +|S–M + +|E9 Recursive types + closures +|Iso-recursive `TMu` with boxed codegen; funcref table with the ADR-005 ABI; behind `--unstable-core` until P17 is CLOSED. +|IntList sum and `apply(f: I32 -> I32, x)` run and pass the gate; closures with I64, F32 and F64 parameters and results run through type-indexed `call_indirect` signatures (today every closure call uses the single `TYPE_CLOSURE_CALL` `(i32, i32) -> i32`); the E5 conformance matrix gains its closure parameter and result columns, with 0 disagreements +|E5, D7; E8 for completing the gate (implementation behind `--unstable-core` can proceed earlier) +|L + +|E10 stdlib port +|Prelude, IO, Region, Aggregate, Stream, Allen, Transactions, Argv and Coproc (the nine current `stdlib/` modules) in v2; Coproc migrates from its five raw variadic `__ffi` calls to typed `extern` declarations, so it enters Φ like Argv; `CoprocBuf` (today `data CoprocBuf = CoprocBuf(I64)`, which D5's compound-grade join would classify as unrestricted) gets a linearity annotation on its declaration, with the syntax fixed by the syntax ADR, so the handle is linear; raw `__ffi` is otherwise rejected (E1); `src/ephapax-stdlib` retired (default); package import tier. +|`ephapax check stdlib/*.eph` 10/10 (the nine current modules plus `ALib.eph`); a duplicate `download`, a duplicate `release` and a dropped `CoprocBuf` are each rejected with a named `TypeError`; and `ephapax compile` 10/10 with each module accepted by `typed_wasm_gate`; a runner test per module exercises its exported operations; a corpus file importing a stdlib module through the package tier checks and runs; corpus ≥ 22; aLib collection group attempted +|E7, E9 promoted out of `--unstable-core` (T4i), E8 +|L + +|E11 LSP +|On the driver plus query: diagnostics, hover from the typed table, go-to-definition, format. +|`lsp_e2e.rs`: 0 diagnostics on `bridge.eph`/`p1.eph`; hover on `fact` = `I32 -> I32`; go-to-definition on `fact` resolves to its declaration; formatting `bridge.eph` is idempotent +|E3, E5 +|M + +|E12 Differential harness +|core→SyntaxV2 translator (extern blocks map to Φ) with a checked-in *core coverage table*: every Rust core constructor maps to a `SyntaxV2` form or to a tested lowering (n-ary tuples to nested pairs; `List` to the D7 recursive sum), and any unmapped constructor is an `EXCLUSIONS.adoc` entry naming the rung that removes it; oracle runner, generator, mutation, corpus mode; report of fragment coverage. +|soundness direction (Rust-accept ⇒ oracle-accept) at 0 tolerance from the first oracle, counted over *every* Rust-accepted input: an input the translator cannot translate counts as a soundness failure unless it matches a named entry in `tools/ephapax-oracle/EXCLUSIONS.adoc` (each entry gives the fragment, the reason and the rung that removes it; the list may not grow after W2 without owner sign-off); completeness reported; for jointly accepted terms, normalized `(Ty, R', G')` tuples are compared and mismatches reported +|P6 (naive oracle) for the initial harness. P15 is only a later upgrade, re-pointing it to `CheckV2` in W5. +|M–L + +|E13 Rust v2 checker +|`ephapax-check-v2` as an image of `CheckV2.v`; emits the typed core and, under the D9 certificate option, a derivation certificate that `check_v2_cert` checks per program; `ephapax-typing` delegates to it. +|0 disagreements (both directions, and on normalized `(Ty, R', G')` output tuples for jointly accepted terms) over corpus + 100k generated + 10k mutated terms, in CI on every PR. `EXCLUSIONS.adoc` is empty before `ephapax-typing` delegates to it; any fragment still excluded at that point is rejected by the delegated checker with a named diagnostic until its rung lands, so no accepted fragment goes unchecked by the oracle. Under the D9 certificate option: `check_v2_cert` accepts the certificate emitted for every Rust-accepted input, and a corrupted-certificate test case is rejected. +|P15, D5 +|L + +|E14 Proving ground +|`eph-agg` region-scoped CLI. +|`ephapax run eph-agg -- 3 4 5` prints `sum=12 count=3 max=5`; gate Ok; LSP 0 diagnostics; within the X12 budget +|E4, E8, E9, E10, X12 baseline (T5i) +|M + +|E15 Comptime island +|Restricted grammar, `@comptime` parses, wired to `ephapax-meta`. +|Branches on D8. Recommended option or 2LTT: a self-recursive `comptime_fn` fails to parse; a fold over `@fields_of` compiles and is re-checked. Fuel-bounded option: the same fold compiles, and a non-terminating `comptime_fn` fails with a named fuel-exhausted diagnostic. Drop option: `@comptime` and `@fields_of` fail with a named UNIMPLEMENTED diagnostic, and P14 is not scheduled. +|E3, D8 +|L + +|E16 L3/L4 surface + RMR/RMO +|echo/observe/`drop!`/`region!`, mode declarations, `Erasure.eph`, `Reversible.eph`, scrub-on-exit; docs: full-fiber Linear echo = RMR (retention), never "erasure". +|unobserved Linear echo rejected; `drop!`/`region!` phase tests run; `Erasure.eph` and `Reversible.eph` check, compile, pass the gate and have runner tests; affine and linear outputs differ in ownership; freed sensitive cells read 0 both in the interpreter and in a wasmtime runner test (E4) that inspects the freed linear-memory range after region exit. That scrub test is for the recommended D12 option. Under crypto-shredding, E16 instead encrypts each sensitive region under a per-region key, erases the key at exit, and tests that the key cell reads 0 and that the receipt check accepts. Under "claim nothing", E16 ships no erasure claim and its docs label the rows designed-not-mechanised +|P12, P13, T5h (upstream Affine kind merged and pinned), D12, X12 baseline (T5i), E8 +|L + +|E17 Effects / traits / contracts / capabilities +|Annotation args and capabilities → contracts as asserts → traits by dictionary passing → one-shot handlers via evidence passing. +|one phase test per feature that *runs* wasm through gate and runner; differential still 0 +|E13, E8 +|XL + +|E18 Ecosystem +|typell-ephapax v2; shared aLib runner in typed-wasm; linear-memory layout profile. +|typell tests green on v2 fixtures; shared runner reproduces ephapax's pass count; the layout profile is merged upstream and `typed_wasm_gate` validates the stdlib against it +|E6, D10, E8, E10 (the completed v2 stdlib port) +|M +|=== + +== Experiments and benches before bigger commitments + +[cols="1,4,3",options="header"] +|=== +|# |Experiment |Decides + +|X1 +|Check in `scripts/probe-battery.sh` plus its inputs under `tests/probes/`, emitting a TSV of verdicts for dup2, dup4, pairdup, lamcap, rec1, i64, s1, s6, t3, perform, g5, gen_angle, qa/app2, p1, the `@total` loop and the five `conformance/invalid` files. Nine inputs are in `docs/reports/2026-11-04-v2-survey/evidence/probes/`. s1, s6, t3, qa/app2, p1 and the `@total` loop are not in the evidence directory (most were lost with the survey scratch files), so X1 writes them and commits each with its expected result before any later gate cites them. +|the E0–E2 baseline; every wave diffs against it + +|X2 +|P0 dry run in scratch: apply the retirement edits, confirm `env_inconsistent_preservation_l1` and `env_inconsistent_step_pop` fail, confirm the `*_FALSE` files still compile, run the gate script. +|the evidence package for owner ratification + +|X3 +|Frames prototype (time-boxed to 3 days): a scratch `SyntaxV2`/`StepV2`/`ConfigWF`, plus a scratch L1-only `TypingV2` (rule statements, no metatheory) for X4 to retarget against, with option (i); re-check all 8 families. +|whether D2(i) kills every known class (input to K1) + +|X4 +|Porting rate: retarget the 52 Semantics_L1 Qed lemmas against the X3 scratch `TypingV2`/`StepV2`, and count verbatim / small edit / dead, with step-shaped lemmas counted separately. The count is provisional and is re-measured against the real P4 core when P7 starts. +|real sizes for P7 and P10 + +|X5 +|Typed generator acceptance and constructor coverage on the naive `check_v2`. +|whether the P6 falsifier counts (K2) + +|X6 +|Translator fragment coverage: what fraction of the 14 compiling corpus files and of 1k proptest terms reaches SyntaxV2. +|whether the differential gate is meaningful; sizes E12 + +|X7 +|typed-wasm replay: port the scratch `xlate` mapping into `probe_op_at`; typed-wasm tests stay at 209; aliasprobe variants (`local.set`, `local.tee`, store) against a taint prototype; the count-0xFFFFFFFF payload; one-byte ownership flip mutation over the corpus. +|the upstream PR content; the E8 baseline (0/17 → 17/17 expected) + +|X8 +|Reproduce aLib in Rust/wasmtime at exactly 89/1/13/51. +|runner validity before it becomes a gate + +|X9 +|A-prime / grade impact: classify corpus files by bare-TFun region capture, compound-linear use and non-linear `let!`. +|how many programs D4/D5 reject (K8) + +|X10 +|Extraction feasibility: a toy `check_v2` extracted to OCaml and to Guile Scheme, and also run in-Coq under `vm_compute`, reading `ephapax-ir` S-expressions and timed on the corpus and on 1k generated terms; plus a 100-line derivation-certificate prototype (the recommended D9 option). +|the D9a choice (W1) and the D9 choice (W4) + +|X11 +|Halting-island grammar on a scratch pest copy: fraction of intended EBNF comptime uses that survive. +|D8 (K9) + +|X12 +|Bench: corpus compile time cold and warm; `p1.wasm` size (959 B baseline); wasmtime time for a 1e6-iteration fold with and without scrub; LSP incremental latency on `bridge.eph` (target < 100 ms). +|budgets before E14 and E16 (baseline in W5 via T5i with a scrub prototype; re-measured as validation in W6) + +|X13 +|Recursive-type probe: monomorphic IntList, iso-recursive vs nominal, termination of desugar, diagnostic quality. +|D7 + +|X14 +|Agda re-pin to 2.6.4.3 if obtainable; otherwise ledger rows record 2.6.3. +|ledger honesty +|=== + +== Ultracode session plan + +=== Global fences (all waves) + +* Never edit `formal/Semantics.v`, `formal/Typing.v`, `formal/Syntax.v` or the in-repo `formal/Counterexample*.v`, except the owner-ratified D0/D0b retirement under P0/T0g: replacing the three refuted `Admitted` statements by `Prop` definitions and restating their refutations against them. The owner reviews and signs that change; nothing else in those files may change. +* `formal/TypingL1.v` is frozen once the fork exists. `formal/Semantics_L1.v` and `formal/TypingL2.v` receive only the P0 retirement edits. +* Never propose closing `Theorem preservation`. Never add an `Axiom` or `Admitted` outside the allowlist. +* Any cross-layer side condition triggers escalation under the CLAUDE.md anti-pattern detector. +* No Idris2, Lean, Isabelle, zig or wasmtime-CLI result is ever reported as passing. +* ephapax-affine ≠ AffineScript. typed-wasm "region" (a memory schema) ≠ ephapax L1 region. L1 maps to typed-wasm L9, not L2. +* typed-wasm, aggregate-library and other external changes go only through upstream PRs. Never work around them in ephapax; in particular, never emit operator indices while D11 stands at its recommended option. If the typed-wasm owner instead ratifies the operator-index amendment, the fence lifts for that one change: ephapax migrates in a scheduled rung (E8 re-scoped to emit operator indices and pin the bumped `ACCESS_SITES_VERSION`) in the wave after ratification, through the normal carry-over rule. +* No admin-merge before CI is green ("squabble, don't bypass"). Commits are GPG-signed with key `4A03639C…2867091E`. No licence edits. + +=== Waves + +[cols="1,4,1,3,3",options="header"] +|=== +|Wave |Parallel tracks |Agents |Exit gate |Must not touch + +|*W0 Honesty and holes* (1 week; ephapax only) +a|* T0a P0 dry run, then one ratification request covering D0 and D0b (X2) +* T0h after ratification, apply the P0 retirement from the X2 dry-run diff (an agent prepares the PR; the owner reviews and signs it) +* T0g implement the ratified D0b retirement inside P0: `Semantics.preservation` becomes `preservation_stmt : Prop`, `Counterexample.v` is restated as `preservation_false : ~ preservation_stmt` (Qed), and a CI gate checks the enumerated conditions: no `Admitted`/`Axiom`/`Parameter` in any `_CoqProject` file, and the named refutations and L2 results closed under the global context. Consistency of the whole build then follows from Coq's own consistency, since no axiom remains; the gate does not claim more than that. The fenced-file edit and the CLAUDE.md fence revision are applied by the owner, GPG-signed. +* T0b P1 gate, tripwire (runs before the X2 step of T0a), `gen-proof-status` (the `status-gate` path fix landed in #418) +* T0c P2 land the 7 scratch falsifiers +* T0d E0 + E1 Rust holes and fail-loud +* T0e X1 probe battery + X8 aLib harness + E6 conformer +* T0f doc-correction PR draft (owner applies) +|6 +|`assumptions-gate.sh` exits 0 with an empty allowlist for every headline (on the P0 branch; temporarily the two L1 names on main are reported, not allowlisted). After P0 merges, the tripwire finds no refuted `Admitted` at all and its quarantine list is empty (before then it reports the L1 pair and the legacy theorem). Dummy `Admitted` turns CI red. `status-gate.sh --proofs` exits 0. `formal/regress/*` CLOSED. `linearity_holes.rs` and `fail_loud.rs` green. `alib_conformance` at 89/0 unexpected. D0 and D0b ratified (2026-11-05), and the no-`False` gate present (0 `Admitted`/`Axiom`/`Parameter`; named results closed). *No cross-repo criterion.* +|typed-wasm; any judgment design; `formal/v2` + +|*W1 Decisions and infrastructure* (1–2 weeks) +a|* T1a P3 decision packet: D1–D8, D9a, D10 (interop representation; it fixes the backend that E5, E9, E8 and E10 build on, so it cannot wait for W5) (extraction target / OCaml policy for the naive oracle) and the syntax ADR (normative grammar source; default: regenerate the EBNF from `ephapax.pest` for implemented productions while keeping every current EBNF production that `ephapax.pest` lacks, such as traits, handlers, contracts, capabilities and comptime, in the conformance inventory as UNIMPLEMENTED; removing one needs an explicit owner decision recorded in the ADR), with X3 + X4 + X9 + X11 + X13 attached; D9a is ratified separately, after T1f, with X10 attached, and the W1 exit requires it +* T1b X7 typed-wasm upstream PRs (offsets, bounds, taint) and the D11 request to the typed-wasm owner +* T1c E3 driver + E4 runner +* T1d E2 corpus + E7 grammar reconciliation draft +* T1e `Modality` join laws (P11 part 1) +* T1f X10 extraction / certificate prototype; it must finish before the D9a part of T1a is ratified +|6 +|Decision record merged and signed off, including D9a ratified with the X10 results attached. Driver agreement passes; `ephapax run p1.eph` prints 162 and the argv fixture passes. Corpus gate asserts error kinds. typed-wasm PRs open with green tests (≥ 209). Join laws CLOSED. +|`formal/v2` beyond prototypes; Rust checker rewrite + +|*W2 v2 core and falsifier* (2–3 weeks) +a|* T2a P4 skeleton +* T2b P5 Regress +* T2c P6 `Exec.v` + typed generator (X5) +* T2d E12 translator + harness. The soundness direction (Rust-accept ⇒ oracle-accept) is asserted at zero tolerance against the naive `check_v2` over every Rust-accepted input, with an untranslatable input outside `EXCLUSIONS.adoc` counted as a failure; only completeness is report-only (X6). +* T2e E5 typed side-table codegen + aLib F64 re-binding (E6 widening) +* T2f E8 if typed-wasm has merged; otherwise it carries over to each later wave until it does +* T2g E7 completion (generics, `M.Ctor(x)` lowering, reconciled import/extern syntax) on top of the W1 draft +|6 +|ORACLE-COQ green on `formal/v2`. All Regress CLOSED; `let_unit_typable_v2` CLOSED. Falsifier: 0 counterexamples over 100k well-typed terms at ≥ 20% acceptance with every `has_type_v2` and every `step_v2` constructor hit ≥ 100 times. `alib_conformance` pass ≥ 99, 0 unexpected FAIL. `wasm_e2e` i64/f32/f64/s1/s6/t3 green. Differential soundness direction: 0 disagreements and 0 non-excluded translation failures over all Rust-accepted corpus files and generated terms; the `EXCLUSIONS.adoc` entry count is recorded as the baseline that later waves may only shrink. E7 gate green (`gen_angle.eph` and `qa/app2.eph` compile and run; 0 EBNF productions unaccounted for). +|`PreservationV2` main proof (no proving before the falsifier is green) + +|*W3 L1 metatheory* (3–5 weeks) +a|* T3a P7 structural lemmas (2 agents: regions/renaming, substitution/weakening) +* T3b P8 canonical forms +* T3c P9 progress +* T3d P10 preservation, split by case family (4 agents) +* T3e E9 recursive types and closures behind a flag +* T3f E11 LSP +|10 +|`progress_v2`, `preservation_v2` and `type_safety_v2` CLOSED; allowlist unchanged. `formal/v2/PORT-REPORT.adoc` (P7) committed. Translator coverage reported. LSP e2e green. E9: IntList sum and `apply` run under `--unstable-core` (the gate part carries over with E8). +|L3/L4 surface; Rust checker rewrite + +|*W4 L2/L3/L4 and meta* (3–4 weeks) +a|* T4a P11 rest +* T4b P12 L3 obligation +* T4c P13 L4 boundary +* T4d P14 + E15 comptime island +* T4e P17 `TMu` desugar/target alignment (closes on tests per its acceptance row; it does not wait for P16, whose `Desugar.v` re-checks the fold/unfold insertion as T5d in W5) +* T4f X14 (Agda re-pin), then P19 ledger + `EchoBridge` (both checkers) +* T4g typed-wasm Affine kind + mode-record proposal +* T4h D9 decision record (checker oracle form) with the X10 results attached, ratified by the owner before W5 +* T4i E9 promotion: once P17 is CLOSED (T4e), remove `--unstable-core` from recursive `data` and closures so plain `ephapax check`/`compile` accept them; the gate part still follows E8 under the carry-over rule. T5f (E10) waits on T4i. +|7 +|All CLOSED; EchoCopy untypable; `preservation_v2` CLOSED with TMu; every ledger row records both exit codes and versions; E15 and P14 exit on the branch D8 selected (see the E15 row); D9 ratified. +|stdlib bulk port; effects + +|*W5 Certified checker and Rust as its image* (3–4 weeks) +a|* T5a P15 `CheckV2` + extraction +* T5b E13 `ephapax-check-v2` +* T5c E12 soundness direction re-pointed from the naive `check_v2` to the proved `CheckV2` (asserted since W2) +* T5d P16 `Desugar.v` +* T5i X12 budget baseline: compile time, `p1.wasm` size and LSP latency, plus the fold benchmark with and without a `memory.fill` scrub prototype, so E14 and E16 start in W6 with known budgets +* T5h typed-wasm Affine OwnershipKind and mode record implemented upstream, merged, and the ephapax pin bumped (follows the T4g proposal) +* T5e P18 `CarrierSpec` + Affine emission (completes after T5h) +* T5f E10 stdlib port +* T5g D12 (certified-erasure statement) decision record, ratified by the owner before W6 starts T6b, T6d and T6e (D10 was ratified in W1); also file the absolute-zero CNO-documentation and januskey MAA-restatement upstream PRs, and D12 plus the RMR/RMO citations wait on their merge (carry-over rule applies) +|6 +|`check_v2_sound` CLOSED. Differential: 0 disagreements in both directions over corpus + 100k generated + 10k mutated, on every PR. `ephapax-typing` delegates. Gate accepts 100% of compiled modules. Affine and linear outputs differ. stdlib 10/10 check, compile, pass the gate and pass their runner tests. `match_desugar_correct`, `ownership_kind_sound`, `check_v2_complete` and `check_mod` CLOSED; under the D9 certificate option `check_v2_cert_sound` CLOSED and the corrupted-certificate test rejected. D12 ratified. +|L3/L4 surface beyond phase tests; effects + +|*W6 Growth* (open-ended) +a|* T6a E14 proving ground + X12 budgets +* T6b E16 L3/L4 surface, RMR/RMO stdlib, scrub +* T6c E17 effects / traits / contracts +* T6d E18 ecosystem +* T6e optional P20 / P21 research +|5–6 +|Each feature lands with (a) a CLOSED rule or desugar lemma, (b) a phase test that runs wasm through gate and runner, (c) differential still 0. The allowlist grows only by named, owner-signed METAL-BOUNDARY entries. +|any core change without its formal rule +|=== + +*Order.* Run W0, then W1, then W2, then W3, then W4, then W5, then W6. + +Engineering tracks inside each wave run in parallel with the proof tracks. The only hard cross-dependencies are: + +* E8 waits on the typed-wasm upstream fix; +* E13 waits on P15; +* E9's promotion out of `--unstable-core` waits on P17; +* E16 waits on P12 and P13, and on T5h; +* E12 waits on P6; +* P14 and E15 run together; +* P18 waits on E8 and T5h. + +*Owner-decision schedule.* Every decision is ratified before the first rung that depends on it: + +[cols="1,2,3",options="header"] +|=== +|Decision |Ratified in |Evidence attached / first dependent + +|D0, D0b |W0 (T0a) |X2 dry run / P0, P1, T0g +|D1–D8 + syntax ADR |W1 (T1a) |X3, X4, X9, X11, X13 / P4, E7 (W2) +|D9a (naive-oracle extraction target) |W1 (T1a) |X10 / P6, E12 (W2) +|D11 (typed-wasm owner) |W1, with the T1b upstream PRs |X7 / E8 +|D9 |W4 (T4h) |X10 / P15, E13 (W5) +|D10 |W1 (T1a) |layout-profile note / E5 (W2), then E9, E8, E10, E18 +|D12 |W5 (T5g) |erasure notes / E16, P21 (W6) +|=== + +A rung whose dependency has not completed (for example E8 while the typed-wasm fix is unmerged) carries over to the next wave together with every rung that depends on it (E9 completion, E10, E14, P18, the W5 gate-acceptance exit). It is never declared done against a missing dependency. + +*Decision-branch rule.* Rung deliverables and gates are written against each decision's recommended option. Ratifying any other listed option is valid, but that decision record must then carry a branch table. The table restates the deliverable and acceptance of every dependent rung (the "first dependent" column above and everything downstream of it) before those rungs start. Where the option invalidates completed work, the table lists what is redone and in which wave. A rung whose branch has not been written does not start. Options marked *not eligible* (for example D9a's Rust hand-port) cannot be ratified without first rewriting the gate they would break. D3, D7, D8, D9a and D12 already carry inline branches; the rule covers the rest. + +== Options requiring owner decision + +Ratings run from 1 to 5. Column (a) is elegance and correctness; column (b) is dependability and security/privacy. The *recommended* option in each table is labelled. Where it is not the most elegant option, the departure is stated, per doctrine 15. + +=== D0 — Form of the P0 retirement + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* `Definition …_stmt : Prop`; refutations kept; L2 corollaries take the statement as a hypothesis +|5 |5 +|Maintainability: keeps the history readable. Security: removes `False` from the environment. Precedent: the 2026-06-26 removal of `region_liveness`. + +|Delete both lemmas outright +|4 |5 +|Loses the statement that the `*_FALSE` files reference; those must be restated. + +|Move them to an unbuilt `formal/attic/` +|3 |4 +|Not checked by coqc, so they can rot silently. + +|Unconventional: keep them Admitted but sealed in a `Module Type` (never instantiated) +|3 |3 +|Consistent, but confusing for agents; the tripwire still fires. +|=== + +=== D0b — Isolating the legacy refutation + +The legacy `Semantics.preservation` is `Admitted` by directive and is refuted by `Counterexample.v`, so any environment that loads both can derive `False` (F0). Every option keeps both files unchanged unless it says otherwise. + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* import-closure quarantine. Nothing in `formal/v2` imports `Semantics.v` or `Counterexample.v`, directly *or transitively* (CI checks the `coqdep` closure). Every headline's allowlist is empty, and the tripwire reports the legacy `Semantics.preservation` as a known refuted `Admitted` through the registered refutation list. +|5 |4 +|No fenced file changes. Soundness is per theorem, read off `Print Assumptions`. This isolates the v2 environment but does *not* make the legacy environment consistent: `legacy_inconsistent` (F0) stays as positive evidence. Residual risk: an agent that imports both modules can still prove `False`, which is why the gate is per headline. + +|Split `_CoqProject` into a default `v2` target and a separate `legacy` target that builds `Semantics.v` + `Counterexample*.v` +|4 |5 +|The default build becomes consistent. It touches only the project file, not the fenced `.v` files. It still needs owner sign-off because it changes what "the build" means. + +|Retire `Semantics.preservation` to `Definition preservation_stmt : Prop` and restate `Counterexample.v` against it +|5 |5 +|Fully consistent and honest. It edits two fenced files, so it requires the owner to revise the 2026-05-27 fence. + +|Unconventional: keep everything and make `Counterexample.v` state the negation of `preservation_stmt` in a separate `Module Type` sandbox +|3 |3 +|Consistent, but harder to read, and it changes the fenced counterexample's shape. +|=== + +=== Ratified: D0 and D0b (owner, 2026-11-05) + +* *D0:* the recommended option. `preservation_l1` and `step_pop_disjoint_from_type_l1` become `Definition …_stmt : Prop`; the `*_FALSE` refutations are kept; the L2 corollaries take the statement as a hypothesis. +* *D0b:* *retire `Semantics.preservation` to `preservation_stmt`*. This is not the recommended option, so the decision-branch rule applies. Its branch table: + +[cols="1,4",options="header"] +|=== +|Rung |Branch under the ratified D0b + +|P0 +|Also retires the legacy theorem: `Definition preservation_stmt : Prop`, and `Counterexample.v` restated as `preservation_false : ~ preservation_stmt` (Qed). The acceptance gains: `legacy_inconsistent` (F0) fails to compile, and the build has no `Admitted`, `Axiom` or `Parameter`, so a derivation of `False` would contradict Coq's own consistency. +|P1 +|The tripwire's quarantine list starts empty after P0. Any refuted `Admitted` fails CI. +|T0g +|Replaced: instead of the import-closure job, a CI gate checks that no `_CoqProject` file contains `Admitted`, `Axiom` or `Parameter`, and that the named refutations and L2 results print "Closed under the global context". With no axioms in the build, a closed proof of `False` would contradict the consistency of Coq's own theory; that meta-level argument, not the enumerated checks, is what rules out every other derivation. +|T0f +|The doc-correction PR also revises the 2026-05-27 fence in CLAUDE.md (DO NOT items 1, 2 and 5), PROOF-NEEDS, EXPLAINME and V1-TO-V2, and records that the legacy theorem is retired, not closed. Applied by the owner, GPG-signed. +|Evidence +|`evidence/SurveyCounterexamples.v` F0 becomes an expected-failure target, like F1. +|=== + +Beyond this repo: the memory entry `feedback_ephapax_no_patching_legacy_preservation.md` needs the same revision. + +=== D1 — Where the v2 core lives + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* fork `formal/v2/` (syntax + typing + step); legacy frozen +|5 |5 +|The only option that leaves the fenced files untouched (`Counterexample.v:186` imports TypingL1). Cost: duplicated step machinery, sized by X4. + +|Edit `TypingL1.v` / `Syntax.v` in place +|2 |2 +|Breaks `Counterexample.v` inversions and touches fenced artefacts. *Rejected.* + +|Configuration-level frame stack, no new constructors +|2 |3 +|Cannot distinguish an entered from an unentered `ERegion` (`Syntax.v:122`). + +|Unconventional: semantic soundness (logical relations / Iris-style) over the current syntax, with no syntactic preservation +|4 |4 +|Most robust against hidden invariants and doubles as the P21 machinery. Heavier infrastructure; kept as the K1 fallback. +|=== + +=== D2 — Region-frame invariant + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* (i) runtime `EFrame` + binder freshness + `config_wf` (Calcagno–Helsen–Thiemann) +|5 |5 +|Targets the root cause; standard; validated cheaply by X3 / Regress. + +|(ii) capability well-formedness of Γ and the result type +|4 |4 +|Principled (Walker–Morrisett), but heavier typing rules. + +|(iii) choreographic trace coherence as a judgment input +|3 |3 +|Research; proven only for a finite fragment. + +|Unconventional: region liveness as an Iris resource +|4 |4 +|See D1, last option. +|=== + +=== D3 — Region naming + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* locally nameless with cofinite quantification +|5 |5 +|Freshness and shadowing are solved by construction; region weakening becomes provable. + +|Concrete names + fresh renaming at Enter + equivariance lemma +|3 |4 +|Closest to today's code; the equivariance lemma is an L-sized tax. + +|de Bruijn region indices +|3 |4 +|Shifting lemmas everywhere; hard to read when mirrored in Rust. +|=== + +=== D4 — Closure region visibility (A-prime) + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* latent effects on every arrow (`TArr Rin Rout`) plus prenex region polymorphism on top-level functions +|5 |5 +|Kills EscapeCex; region polymorphism keeps stdlib functions reusable; decidable. Performance: none at runtime. + +|Effect-typed lambdas only (retire bare TFun) +|3 |4 +|Simpler, but rejects more programs (X9) and has no answer for reuse across regions. + +|Unconventional: capture checking (CC<:□-style capture sets) +|4 |4 +|Elegant and expressive, but new theory to mechanise; inference cost is higher. +|=== + +=== D5 — Placement of the dyadic split and compound linearity + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|Judgment-level `m` only (current formal design) +|3 |3 +|Does not match the Rust `let`/`let!` or the v2 grammar; does not fix PairDup by itself. + +|Per-binder grades only (Rust today) +|3 |3 +|Loses the program-level L4 mode. + +|*Recommended (elegant default):* per-binder grades {0,1,ω}, with the modality as the *preorder* (Affine adds `1 ≤ 0`); compound types take the join; `TEcho` has grade 1 in Linear mode; borrows on a separate axis +|5 |5 +|Unifies Coq, Rust and the wire ownership kinds. `linear_to_affine` becomes order inclusion. Fixes PairDup and EchoCopy. Interop: maps to typed-wasm Linear / Affine / Unrestricted, with ExclBorrow and SharedBorrow kept separate. + +|Unconventional: LNL / adjoint two-sorted contexts with up/down shifts in the core +|4 |4 +|Very principled for L4; heavier surface; adopted only at L4 boundaries (P13). +|=== + +=== D6 — Echo determinism + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* syntactically distinct echo forms (`EDropE`, `ERegionE`), chosen by the elaborator from the declared obligation +|5 |5 +|Deterministic step; obligation visible in source. + +|Modality-indexed step relation +|3 |4 +|Couples the operational semantics to typing. + +|Unconventional: an echo as an algebraic effect discharged by a residue handler +|4 |3 +|Elegant and unifies with effects (E17), but delays L3 until effects exist. +|=== + +=== D7 — Recursive types + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* iso-recursive `TMu` with fold/unfold inserted by desugar +|5 |5 +|Aligns with typed-wasm WHT_Rec; small core. + +|Nominal named types +|4 |4 +|Better diagnostics (X13); a larger core. + +|Unconventional: no core recursion; Church / bounded encodings only (*not eligible*) +|2 |4 +|Total, but unusable for the stdlib, and E12 would have no translation for `List`. Listed only to record why it is excluded; ratifying it would first need a bounded `List` encoding with stated limits. +|=== + +=== D8 — Comptime / reflection vs ADR-016 (meta plane) + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* halting-island grammar plus `MetaPlane.v`; `ephapax-meta` reflection fenced to the island +|5 |5 +|Total by construction; Harvard separation provable. Security: no runtime data reaches comptime. + +|Fuel-bounded evaluator +|3 |4 +|Termination by fuel, not by construction; nondeterministic failures. + +|Drop comptime from v2.0 +|3 |5 +|Most dependable; loses `@derive`. + +|Unconventional: full 2LTT staging (typed quotes) +|4 |4 +|The most final theory; XL effort. +|=== + +=== D9a — Naive-oracle extraction target (ratified in W1, after X10) + +The naive `check_v2` and `step_v2_fn` from P6 need an executable form for the W2 falsifier and the E12 differential. This is a test-only oracle that never ships in the compiler. D9 later decides the form of the certified checker, and that choice may reuse or replace this one. + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* Coq extraction to OCaml, confined to `tools/ephapax-oracle` as a test-only binary, with a policy exception recorded in the ADR +|5 |4 +|Mature extractor, and OCaml is installed. The trusted base is the extractor, the OCaml runtime and the S-expression reader. The policy exception is narrow because nothing ships. + +|Extraction to Scheme (Guile, estate-allowed) +|3 |4 +|Policy-clean, but extraction is less mature and slower on 100k terms. X10 measures both. + +|Unconventional: no extraction; evaluate inside Coq (`vm_compute` over serialised terms) +|3 |5 +|No extra trusted runtime and no policy question, but likely too slow for 100k terms per run. X10 measures the throughput. + +|Hand-port to Rust (*not eligible*) +|1 |2 +|Loses the link to the Coq definition, so the differential would compare Rust with Rust and could not serve as the E12 zero-tolerance soundness gate. Listed only to record why it is excluded. +|=== + +=== D9 — Checker oracle form + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|Coq extraction to OCaml (installed; estate policy lists OCaml for the AffineScript compiler only) +|4 |4 +|Mature extractor. The trusted base is the extractor, the OCaml runtime and a hand-written S-expression reader. Needs policy sign-off. + +|Extraction to Scheme (Guile, estate-allowed) +|3 |4 +|Policy-clean; less mature extraction. + +|Hand-port to Rust +|2 |2 +|Loses the soundness link; only a stopgap. + +|*Recommended:* derivation certificates. Rust emits a typing derivation; `check_v2_cert` (proved sound, then extracted, or run under Coq) checks it per program. OCaml extraction is used for the bulk differential. +|5 |5 +|Per-program verified acceptance without trusting the Rust checker. Performance: a certificate-size overhead, measured by X10. This option is both the most elegant and the recommendation. +|=== + +=== D10 — Interop representation + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* typed-wasm adds a linear-memory layout profile (String `(ptr,len)`, Bool i32, closure per ADR-005) beside WasmGC Layout.* +|4 |5 +|Matches what both ephapax and typed-wasm-codegen emit today; size M. + +|A WasmGC backend for ephapax +|4 |3 +|Interop with Layout.* contracts that have no emitter and whose proofs are UNVERIFIED; size XL. + +|Unconventional: dual codegen behind one typed core +|3 |3 +|Maximal interop; double maintenance. +|=== + +=== D11 — Access-site convention (typed-wasm owner) + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* honour ADR-0003 byte offsets in the verifier and codegen +|5 |5 +|Fix at source; ephapax is already correct (17/17 after translation). + +|Amend to operator indices + `ACCESS_SITES_VERSION` bump +|3 |3 +|Breaks other producers; re-pins all fixtures. If ratified, ephapax follows it through the re-scoped E8 rung (see Global fences), not a workaround. +|=== + +=== D12 — Certified erasure (RMO) statement + +[cols="3,1,1,4",options="header"] +|=== +|Option |(a) |(b) |Comment + +|*Recommended (elegant default):* OND-shaped non-interference over a declared observation model, plus a tagged METAL-BOUNDARY scrub assumption, plus scrub-on-exit codegen +|5 |4 +|The only honest type-level statement. Privacy: physical remanence is stated as an assumption. + +|Crypto-shredding receipts (erase one key) +|4 |4 +|Reduces the assumption to one key; adds key management. + +|Claim nothing; label the README rows as designed-not-mechanised +|3 |5 +|Mandatory *now* regardless of which option is chosen later. The full-fiber Linear drop echo is RMR (retention), never erasure. +|=== + +== Risks and kill criteria + +[cols="3,3,3",options="header"] +|=== +|Risk |Mitigation |Kill criterion + +|Owner bottleneck on P0, D1–D12 and typed-wasm +|Pre-packaged prototypes with labelled defaults; engineering waves continue on sugar-only work +|If a decision is open for more than 2 weeks, the dependent track pauses; no workaround patches + +|Option (i) misses a counterexample class +|X3 and Regress before P10 +|*K1:* if any family remains typable-and-failing after 2 design iterations, stop the syntactic route and switch to D1's semantic-soundness option + +|Vacuous falsifier +|Typed generator, acceptance floor, coverage +|*K2:* below 20% well-typed acceptance or any `has_type_v2` or `step_v2` constructor hit fewer than 100 times, the falsifier result does not count toward the W2 exit + +|Fork cost underestimated +|X4 porting report +|*K3:* if fewer than 30% of lemmas port verbatim, re-size P7/P10 to XL and re-run the D1 comparison + +|Preservation grind (CLAUDE.md anti-pattern) +|Case-family split; escalate on any new side condition +|*K4:* if P10 is open after 8 sessions with no new case closed in 2, escalate; never add a side condition or Axiom + +|Inconsistency or axiom regression +|P1 gate and tripwire +|*K5:* any axiom in a headline's `Print Assumptions` that is not on the owner-signed allowlist reverts the PR automatically. The allowlist starts empty and stays empty for every L1/L2 headline. Only named METAL-BOUNDARY entries for P21 may be added to it. + +|Rust/Coq drift; trusted oracle +|Soundness direction at 0 tolerance; derivation certificates; report as "tested agreement", never "verified Rust checker" +|*K6:* an unresolved soundness-direction disagreement for one wave blocks making `ephapax-check-v2` the default + +|typed-wasm upstream delay +|Gate remains report-only and is labelled as such +|*K7:* never switch ephapax to operator indices unilaterally (only via a ratified D11 amendment and the re-scoped E8); never report the gate as passing + +|Language shrinkage from D4/D5 +|X9; region and grade inference; LetCheck completeness fix in the same revision +|*K8:* if corpus acceptance drops more than 40%, revisit inference before shipping + +|Comptime restriction too tight +|X11 +|*K9:* if more than 50% of intended uses are blocked, defer comptime (D8 option 3); do not re-allow recursion + +|Overclaims (erasure, totality, Idris, jtv, CNO) +|W0 doc PR; generated status +|Any doc claim without a matching oracle run is removed or labelled + +|Prover fragmentation (Coq / Agda / Idris / Lean) +|Port plus ledger with versions +|A ledger row without both exit codes is marked ASSUMED + +|Name collisions ("aggregate library" ×5, Linear/Affine ×4, "region" ×2) +|Qualified names at every seam +|— + +|Toolchain gaps (Idris2, Lean, Agda 2.6.4.3, wasmtime CLI) +|Every dependent claim marked UNVERIFIED +|No wave exit may depend on them +|=== + +== Cross-repo action list + +*hyperpolymath/typed-wasm* + +* Make `verify_access_typing_from_module` read ADR-0003 byte offsets (`crates/typed-wasm-verify/src/verify.rs:1235`). Emit byte offsets in `typed-wasm-codegen` (`lib.rs:578`). Update fixtures. +* Bound wire counts in `section.rs:47` and the `with_capacity` sites (`:441`, `:762`, `:768`). +* Add a locals-taint L10/L7 analysis (`local.set`, `local.tee`, stores). +* Proposal: Affine OwnershipKind, module mode record, and a separate borrow axis. Extend VerifierSpec `OwnershipIntent` accordingly. The Idris parts are UNVERIFIED. +* Write the linear-memory stdlib layout profile, the aLib wasm-ABI binding profile, and a shared aLib runner crate. +* Docs: +** `LEVEL-STATUS.adoc:576-577` says ownership is emitted "on every compile"; it is emitted only when some parameter is non-Unrestricted. +** ephapax#251 is listed as pending; ephapax already emits access sites. +** `verify_regions_from_module` is cited but does not exist. +** "Ephapax compiles to WasmGC" is wrong; ephapax emits linear memory. +** String is documented as `(array i8)` but modelled as `(array i32)`. +** Missing `stdlib/` and `generated/` directories. +** VerifierSpec agreement is described as proven; it is tautological. + +*hyperpolymath/aggregate-library* + +* Fix `specs/logical/not.adoc` vector 3, the substring start/end semantics and the AffineScript conformer drift (`src/affinescript/ALib.affine:106-108`). +* Fix the Justfile `.md` → `.adoc` globs. +* Export `vectors/*.json` and a grammar for the fn/condition mini-language. +* Reconcile the operation counts (29 / 22 / 20). +* The owner decides Deno vs Bun for aLib's own runner. Both CLAUDE.md files conflict, and `mise.toml` violates both. + +*hyperpolymath/echo-types* + +* Add CORRESPONDENCE rows: `weaken`, `degradeMode-comp`, no-section, DecorationStructure laws, `reversibility-via-totality`, EchoResidueCell. +* Add an RMR/RMO/OND correspondence note in `docs/bridges/cross-repo-bridge-status.md`. + +*hyperpolymath/nextgen-typing* + +* Grade-interface reconciliation note declaring distinct sorts. +* TYPE-CONNECTIONS rows for ephapax and anytype. +* Fix the self-contradictory secret-types "specification-stage" text. + +*hyperpolymath/jtv-halting-islands-ct* + +* Restore the parser and the diode-negative tests. +* The binary must read its input file. +* Update README/GRAMMAR, which still describe the deleted Python, and the DATA semantics (now i64, documented as rationals). +* Replace the `ensures(true)` "verification" claim. + +*hyperpolymath/januskey* + +* Linear-token undo API (T-8). +* Keep X-1 and E-1 labelled ASSUMED/OPEN. +* The MAA draft has expired (2026-04-13). Restate RMR two-sided and state-equality-relative, and drop the Oblíbený and Isabelle attributions before ephapax cites it. + +*hyperpolymath/absolute-zero* + +* Document that `terminates` and `energy-dissipated` are definitional or vacuous. +* Fix the PROOF-STATUS rows that point to the archived `proofs/coq` and `verify-all-provers.sh`. +* Make the Agda stdlib registration reproducible. + +*hyperpolymath/typell* + +* typell-ephapax v2 bridge (regions, TEcho, grades) after the D5 ADR. + +*hyperpolymath/resource-algebra, tropical-types, occupancy-types* + +* No change is required for v2.0. +* Before the optional P20 layer: Lean checks for tropical and stackcert in an environment that has Lean (UNVERIFIED here), and an Agda re-run on 2.6.4.3. + +*hyperpolymath/anytype* + +* Record that ephapax uses anytype as a *design reference only*: no dependency, per the kernel ruling, and no soundness proof exists. + +*hyperpolymath/secret-types, choreographic-types, epistemic-types, residual-evidence-types* + +* No action until W6. +* choreographic-types should re-check against its pinned epistemic-types 495db9c. Here it was checked against the working tree. + +*hyperpolymath/ephapax* (tracked here for completeness; all owner-applied): + +* The W0 doc-truth PR: record the derivable-`False` finding in CLAUDE.md, V1-TO-V2.adoc, STATUS.adoc and PROOF-NEEDS §4 (#418 already marks the L1 pair refuted); fix PROOF-STATUS.a2ml, the `Echo.v` and `Semantics_L1.v` banners, README.adoc:265-273 (erasure), `docs/wikis/Home.md:55-56` (six L2 admits, conditional L3), `docs/testing-and-bench-strategy.adoc:34` (four outer L1 admits) and `spec/FRG-PROFILE.adoc:29-30` (obsolete `.md` links). +* Stale typed-wasm pin comment in `Cargo.toml:60-64`. +* Rust "Coq bridge" test equating `Ty::Effectful` with `TFunEff` (`src/ephapax-syntax/src/lib.rs:880-888`). + +*Evidence for this survey:* see `evidence/README.adoc` beside this document. Scratch paths quoted by the survey agents no longer exist. diff --git a/docs/reports/2026-11-04-v2-survey/evidence/README.adoc b/docs/reports/2026-11-04-v2-survey/evidence/README.adoc new file mode 100644 index 00000000..61f3a813 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/README.adoc @@ -0,0 +1,53 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Evidence for the 2026-11-04 v2 survey + +These files back the findings in `../EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc`. They are deliberately *outside* `formal/_CoqProject` and the Cargo workspace, so they change no build. + +== Coq witnesses + +`SurveyCounterexamples.v` is checked against the current `formal/` build: + +[source,sh] +---- +cd formal +coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq -j4 +coqc -R . Ephapax ../docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v +---- + +Expected `Print Assumptions` output with coqc 8.18.0. This was first checked at `800030f`, then re-checked after `main` (including #418) was merged into the branch at `10339b3`, with identical results: + +[cols="2,3",options="header"] +|=== +|Lemma |Assumptions +|`legacy_inconsistent` |axiom `Semantics.preservation` (legacy, `Admitted` by directive) +|`env_inconsistent_preservation_l1` |axiom `preservation_l1` (the `Admitted.` lemma) +|`env_inconsistent_step_pop` |axiom `step_pop_disjoint_from_type_l1` (the `Admitted.` lemma) +|`preservation_l1_FALSE_closed` |Closed under the global context +|`preservation_l1_FALSE_echo_crosspath` |Closed under the global context +|`observe_stuck` |Closed under the global context +|`pair_dup_linear_string` |Closed under the global context +|`echo_copyable_linear_mode` |Closed under the global context +|=== + +NOTE: These results describe `main` before the D0/D0b retirement in hyperpolymath/ephapax#422 (owner-ratified 2026-11-05). After #422 merges, the three refuted statements are `Prop` definitions rather than `Admitted` lemmas. `legacy_inconsistent`, `env_inconsistent_preservation_l1` and `env_inconsistent_step_pop` then fail to compile, which is the intended result: the environment no longer derives `False`. The other five lemmas compile unchanged on top of #422 and stay "Closed under the global context" (checked with coqc 8.18.0 after removing F0/F1); P2 moves them into `formal/regress/`. + +The first three rows mean the global environment can derive `False`. The L1 pair needs the P0 retirement in the plan. The legacy row needs decision D0b in the plan, because the legacy theorem is fenced. Both are owner decisions. The `Admitted.` must not be closed, and no side-condition may be added. + +== Rust checker probes + +`probes/*.eph.txt` (stored with a `.txt` suffix so the repo-wide `eph_corpus_gate` ignores them; copy to `.eph` to re-run) were run with `target/debug/ephapax check` from a `cargo build --workspace` of the same commit. The table below records each exit code and the last output line. For dup2, dup4, pairdup and lamcap, exit 0 is a *soundness hole*, because each one reuses a linear value. For rec1, exit 134 is a crash. + +[cols="1,1,4",options="header"] +|=== +|Probe |`check` exit |Last output line +|`dup2` |0 |✓ 1 file(s) checked successfully +|`dup4` |0 |✓ 1 file(s) checked successfully +|`pairdup` |0 |✓ 1 file(s) checked successfully +|`lamcap` |0 |✓ 1 file(s) checked successfully +|`rec1` |134 |fatal runtime error: stack overflow, aborting +|`i64` |0 |✓ 1 file(s) checked successfully +|`perform` |0 |✓ 1 file(s) checked successfully +|`g5` |0 |✓ 1 file(s) checked successfully +|`gen_angle` |1 |Error: 1 file(s) checked, 1 error(s) +|=== diff --git a/docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v b/docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v new file mode 100644 index 00000000..9aa0e2dc --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v @@ -0,0 +1,185 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(** * Survey evidence, 2026-11-04 — NOT part of formal/_CoqProject. + + Re-checkable witnesses for the findings in + docs/reports/2026-11-04-v2-survey/EPHAPAX-V2-ARCHITECTURE-AND-PLAN.adoc. + Apart from F0, every lemma here is against the CURRENT v2 judgment + ([has_type_l1], [step]). F0 is the single exception: it *uses* the + legacy [Semantics.preservation] (Admitted by owner directive) together + with [Counterexample.v] to witness the legacy inconsistency. Nothing + here closes, edits or extends the legacy theorem or Semantics.v. + + Check (from repo root, after building formal/): + cd formal && coq_makefile -f _CoqProject -o Makefile.coq \ + && make -f Makefile.coq -j4 \ + && coqc -R . Ephapax ../docs/reports/2026-11-04-v2-survey/evidence/SurveyCounterexamples.v +*) + +From Ephapax Require Import Syntax Typing TypingL1 Semantics Semantics_L1 + Modality Counterexample Counterexample_PreservationL1 Counterexample_StepPop. +Require Import Coq.Lists.List Coq.Strings.String. Import ListNotations. +Open Scope string_scope. + +(** ** F0. The legacy [Semantics.preservation] is [Admitted] (kept by + owner directive) and refuted by [Counterexample.v], so loading both + also derives [False]. This does not ask for the legacy theorem to + be closed or edited. It records that it must never appear in a + headline theorem's assumptions. *) +Lemma legacy_inconsistent : False. +Proof. + destruct (Semantics.preservation _ _ _ _ _ _ (Counterexample.bad_step nil) + _ _ _ Counterexample.bad_typable) as [G_out H]. + exact (Counterexample.bad_post_untypable _ _ H). +Qed. + +(** ** F1. The global environment is inconsistent. + [preservation_l1] and [step_pop_disjoint_from_type_l1] are + [Admitted] (hence axioms) and are refuted by Qed, axiom-free + files that are built in the same project. *) +Lemma env_inconsistent_preservation_l1 : False. +Proof. exact (preservation_l1_FALSE preservation_l1). Qed. + +Lemma env_inconsistent_step_pop : False. +Proof. exact (step_pop_disjoint_from_type_l1_FALSE step_pop_disjoint_from_type_l1). Qed. + +(** ** F2. preservation_l1 is false with a closed context ([G = []]). + An un-entered same-name [ERegion] exits immediately and pops the + ambient occurrence of [rv] that the sibling [ELoc 0 rv] needs. *) +Definition rv : region_name := "rv". + +Definition closed_pre : expr := + EStringConcat (ELoc 0 rv) (EFst (EPair (ELoc 1 rv) (ERegion rv (EI32 0)))). +Definition closed_post : expr := + EStringConcat (ELoc 0 rv) (EFst (EPair (ELoc 1 rv) (EI32 0))). + +Lemma closed_pre_typed : + has_type_l1 Linear [rv] [] closed_pre (TString rv) [] []. +Proof. + unfold closed_pre. + eapply T_StringConcat_L1. + - apply T_Loc_L1. simpl; auto. + - apply (T_Fst_L1 Linear [rv] [] [] [] _ (TString rv) (TBase TI32)); [| reflexivity]. + eapply T_Pair_L1. + + apply T_Loc_L1. simpl; auto. + + change (@nil region_name) with (remove_first_L1 rv [rv]). + eapply T_Region_Active_L1. + * simpl; auto. + * simpl; intros []. + * simpl; auto. + * apply T_I32_L1. +Qed. + +Lemma closed_step : + step ([], [rv], closed_pre) ([], [], closed_post). +Proof. + unfold closed_pre, closed_post. + apply S_StringConcat_Step2; [constructor |]. + apply S_Fst_Step. + apply S_Pair_Step2; [constructor |]. + change (@nil region_name) with (remove_first rv [rv]). + change (@nil mem_cell) with (mem_free_region [] rv). + apply S_Region_Exit; [constructor | simpl; auto | simpl; auto]. +Qed. + +Lemma closed_post_untypable : + forall T Rf G', ~ has_type_l1 Linear [] [] closed_post T Rf G'. +Proof. + intros T Rf G' H. unfold closed_post in H. + inversion H; subst. + match goal with + | Hl : has_type_l1 _ [] [] (ELoc 0 rv) _ _ _ |- _ => inversion Hl; subst + end. + match goal with Hin : In _ [] |- _ => inversion Hin end. +Qed. + +Theorem preservation_l1_FALSE_closed : + ~ (forall m mu R e mu' R' e', + step (mu, R, e) (mu', R', e') -> + forall G T R_final G', + has_type_l1 m R G e T R_final G' -> + has_type_l1 m R' G e' T R_final G'). +Proof. + intro Hp. + eapply closed_post_untypable. + eapply (Hp Linear [] [rv] closed_pre [] [] closed_post closed_step); + exact closed_pre_typed. +Qed. + +(** ** F3. preservation_l1 is false for a reason unrelated to regions: + [S_Drop] and [S_Drop_Echo] both fire on the same term, so [step] + is nondeterministic, and the echo path leaves a [T_Drop_L1] + derivation untypable. *) +Lemma drop_typed : + has_type_l1 Linear [rv] [] (EDrop (ELoc 0 rv)) (TBase TUnit) [rv] []. +Proof. apply (T_Drop_L1 Linear [rv] [rv] [] [] (ELoc 0 rv) (TString rv)); [reflexivity | apply T_Loc_L1; simpl; auto]. Qed. + +Lemma drop_echo_step : + step ([], [rv], EDrop (ELoc 0 rv)) ([], [rv], EEcho (TString rv) (ELoc 0 rv)). +Proof. + change (@nil mem_cell) with (mem_write [] 0 CFree) at 2. + apply S_Drop_Echo. +Qed. + +Lemma echo_not_unit : + forall R G Rf G' T, ~ has_type_l1 Linear R G (EEcho T (ELoc 0 rv)) (TBase TUnit) Rf G'. +Proof. intros R G Rf G' T H. inversion H. Qed. + +Theorem preservation_l1_FALSE_echo_crosspath : + ~ (forall m mu R e mu' R' e', + step (mu, R, e) (mu', R', e') -> + forall G T R_final G', + has_type_l1 m R G e T R_final G' -> + has_type_l1 m R' G e' T R_final G'). +Proof. + intro Hp. + eapply echo_not_unit. + eapply (Hp Linear [] [rv] _ [] [rv] _ drop_echo_step); exact drop_typed. +Qed. + +(** ** F4. progress fails: [EObserve] has a typing rule but no step rule. *) +Lemma observe_typed : + has_type_l1 Linear [] [] (EObserve (EEcho (TBase TUnit) EUnit)) (TBase TUnit) [] []. +Proof. apply (T_Observe_L1 Linear [] [] [] [] _ (TBase TUnit)). apply T_Echo_L1; [constructor | apply T_Unit_L1]. Qed. + +Lemma observe_not_value : ~ is_value (EObserve (EEcho (TBase TUnit) EUnit)). +Proof. intro H; inversion H. Qed. + +Lemma observe_stuck : + forall mu c', ~ step (mu, [], EObserve (EEcho (TBase TUnit) EUnit)) c'. +Proof. intros mu c' H. inversion H. Qed. + +(** ** F5. Compound linearity hole: a pair variable whose first + component is a linear [TString] is treated as unrestricted + ([is_linear_ty (TProd _ _) = false]), so Linear mode duplicates + the string. *) +Lemma pair_dup_linear_string : forall r, + has_type_l1 Linear [r] [(TProd (TString r) (TBase TI32), false)] + (EPair (EFst (EVar 0)) (EFst (EVar 0))) + (TProd (TString r) (TString r)) [r] [(TProd (TString r) (TBase TI32), false)]. +Proof. + intros r. eapply T_Pair_L1; + (eapply T_Fst_L1; [eapply T_Var_Unr_L1; reflexivity | reflexivity]). +Qed. + +(** ** F6. A drop-echo residue of a linear String can be copied in + Linear mode ([is_linear_ty (TEcho _) = false]). *) +Lemma echo_copyable_linear_mode : + forall l r R G, In r R -> + has_type_l1 Linear R G (ECopy (EEcho (TString r) (ELoc l r))) + (TProd (TEcho (TString r)) (TEcho (TString r))) R G. +Proof. + intros l r R G Hin. apply T_Copy_L1; [reflexivity|]. + apply T_Echo_L1; [constructor | now apply T_Loc_L1]. +Qed. + +(** Assumption audit. Expected: F0/F1 lemmas list the refuted axiom; + every other lemma is "Closed under the global context". *) +Print Assumptions legacy_inconsistent. +Print Assumptions env_inconsistent_preservation_l1. +Print Assumptions env_inconsistent_step_pop. +Print Assumptions preservation_l1_FALSE_closed. +Print Assumptions preservation_l1_FALSE_echo_crosspath. +Print Assumptions observe_stuck. +Print Assumptions pair_dup_linear_string. +Print Assumptions echo_copyable_linear_mode. diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/dup2.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/dup2.eph.txt new file mode 100644 index 00000000..f409edf0 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/dup2.eph.txt @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn main(): I32 = + let! x = 5 + let a = x + let b = x + a + b diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/dup4.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/dup4.eph.txt new file mode 100644 index 00000000..3e612349 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/dup4.eph.txt @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn use2(x: I32, y: I32): I32 = x + y +fn main(): I32 = + let! x = 5 in use2(x, x) diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/g5.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/g5.eph.txt new file mode 100644 index 00000000..3d98b0d3 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/g5.eph.txt @@ -0,0 +1,4 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn t(): I64 = + __ffi("foo", 1) diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/gen_angle.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/gen_angle.eph.txt new file mode 100644 index 00000000..eadee71f --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/gen_angle.eph.txt @@ -0,0 +1,4 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn id(x: a): a = x +fn main(): I32 = id(3) diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/i64.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/i64.eph.txt new file mode 100644 index 00000000..a3df9c5e --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/i64.eph.txt @@ -0,0 +1,4 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn f(x: I64): I64 = x + x +fn main(): I32 = 0 diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/lamcap.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/lamcap.eph.txt new file mode 100644 index 00000000..b72c69a6 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/lamcap.eph.txt @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn main(): I32 = + region r { + let! s = String.new@r("hi") in + let f = fn(u: ()) -> s in + let a = f(()) in + let b = f(()) in + drop(a); + drop(b); + 0 + } diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/pairdup.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/pairdup.eph.txt new file mode 100644 index 00000000..f3883df6 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/pairdup.eph.txt @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn main(): I32 = + region r { + let! s = String.new@r("hi") in + let p = (s, 1) in + let a = fst(p) in + let b = fst(p) in + drop(a); + drop(b); + 0 + } diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/perform.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/perform.eph.txt new file mode 100644 index 00000000..b58a6f07 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/perform.eph.txt @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +fn main(): I32 = + handle perform ask() with + | return(x) => x + | ask(resume) => 42 + end diff --git a/docs/reports/2026-11-04-v2-survey/evidence/probes/rec1.eph.txt b/docs/reports/2026-11-04-v2-survey/evidence/probes/rec1.eph.txt new file mode 100644 index 00000000..bb19d3a9 --- /dev/null +++ b/docs/reports/2026-11-04-v2-survey/evidence/probes/rec1.eph.txt @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: MPL-2.0 +// Survey probe (2026-11-04). Stored as .eph.txt so the repo-wide .eph corpus gate ignores it. +data L = Nil | Cons(I32, L) +fn f(l: L): I32 = 0 +fn main(): I32 = 0