From d66bfabf2c6e1530ae67f32a9cda5c8bd72e7acb Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 17:37:43 +0000 Subject: [PATCH 1/2] docs(interp): CESK port plan for #623 + formal: Rows.v record-row scaffold MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two forward-looking artifacts toward the substructural-typing proof and the last silent soundness hole. 1. docs/INTERP-CESK-PORT.adoc — the staged engineering plan to port the production tree-walking interpreter (lib/interp.ml) onto a CESK abstract machine with reified, defunctionalised continuations, closing the #623 non-tail single-shot resume residual (the `5`-not-`105` shape; the one genuinely-still-silent row on the soundness ledger). Grounded in the real code: interp.ml (the Result-monad tree-walker whose `perform` discards the OCaml continuation), value.ml (the value/error domain), and the proven template lib/solo_cesk.ml (M1 Solo-core machine: deep handlers, multi-shot, non-tail resume, jsoo-compatible). Delivers ADR-0025 M2 for the real surface. Staged M2-0..M2-4 with a differential oracle so `dune runtest` stays green at every step; §5 enumerates the exact ledger flips (the xfail pin test_resume_nontail_xfail XFAIL->XPASS) that the gate couples to the fix. 2. formal/Rows.v — proof scaffold for record-row soundness (progress + preservation for STLC + extensible records: empty/extend/select/restrict over a lacks-checked row). Modeled on P2_Stlc.v conventions (funext-free, the Software-Foundations Records list-encoding), stated via a local mirror of the Siblings_Stated parametric-Prop pattern and discharged for the concrete model. Rung W0 (monomorphic records); row-variable polymorphism is the named W1 next rung. HONESTY CAVEAT: Rows.v is UNVERIFIED in this environment — no Coq toolchain (coqc/rocq) is available here, so it is NOT wired into formal/_CoqProject and NOT in formal/justfile's `check` list, and cannot affect `dune build` or the formal check. The proofs are complete attempts in the proven idiom, not a machine-checked result. The file's banner lists the owner's wire-in gate: coqc-clean, Print Assumptions closed, add to _CoqProject + README, and lift the statement into Siblings_Stated.v. Plus discoverability cross-links (ungated; SOUNDNESS.adoc deliberately untouched so its content-bound/stamped gate is unaffected): NAVIGATION.adoc and ADR-0025 now point to the port plan. Verified locally: `dune build` clean; tools/check-soundness-ledger.sh passes (all 5 properties); xfail harness reports XFAIL-OK on the #623 pin and FENCE-OK on #624 (unchanged — these are plans/scaffold, not the fix itself). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa --- docs/INTERP-CESK-PORT.adoc | 333 ++++++++++++++++++ docs/NAVIGATION.adoc | 1 + docs/decisions/0025-semantics-vm.adoc | 6 + formal/Rows.v | 474 ++++++++++++++++++++++++++ 4 files changed, 814 insertions(+) create mode 100644 docs/INTERP-CESK-PORT.adoc create mode 100644 formal/Rows.v diff --git a/docs/INTERP-CESK-PORT.adoc b/docs/INTERP-CESK-PORT.adoc new file mode 100644 index 00000000..8fa29aa0 --- /dev/null +++ b/docs/INTERP-CESK-PORT.adoc @@ -0,0 +1,333 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Interpreter CESK Port — closing the non-tail-resume residual (#623) +Jonathan D.A. Jewell +:toc: left +:toclevels: 3 +:sectnums: +:sectnumlevels: 2 + +This is the engineering plan to port the production tree-walking interpreter +`lib/interp.ml` onto a *CESK abstract machine with reified, defunctionalised +continuations*, so that `resume` re-enters the handled computation instead of +merely returning a value. It closes the one remaining *silent* soundness hole in +the language — the interpreter non-tail single-shot resume residual, #623 / +link:SOUNDNESS.adoc[SOUNDNESS.adoc] row "#555 (interp, non-tail single-shot)" — +and delivers milestone *M2* of link:decisions/0025-semantics-vm.adoc[ADR-0025] +for the *real* interpreter surface (not only the Solo core). + +It is grounded in the actual compiler: + +* the target being ported is `lib/interp.ml` — a `Result`-monad tree-walker + (`eval : env -> expr -> value result`); +* the value/error domain is `lib/value.ml` (`value`, `eval_error`, + `'a result = ('a, eval_error) Result.t`); +* the *proven template* is `lib/solo_cesk.ml` — the Solo-core CESK machine that + already implements deep handlers + multi-shot + non-tail resume, axiom-compatible + with `docs/academic/formal-verification/solo-core/Soundness.idr`; +* the governing decision is ADR-0025 (owner sign-off 2026-06-16), whose *M2* is + exactly "deep effect handlers + multi-shot `resume`… the loud-fail messages + already route here". + +[IMPORTANT] +==== +This port is *interpreter-tier* work. It does **not** touch the wasm / wasm-GC / +native backends — those cannot express reified continuations without the wasm +exception-handling / typed-continuations proposals and correctly *loud-fail* +today (ADR-0025; `docs/CAPABILITY-MATRIX.adoc`). The interpreter is the language's +*reference semantics*; closing the hole here closes it where correctness is +defined. The backends remain experimental and loud per ADR-0025. +==== + +== 1. The defect being closed + +=== 1.1 The shape + +`docs/SOUNDNESS.adoc` names it precisely: + +[source,affinescript] +---- +// handle a `get()` effect; the handler resumes with 5 +let x = get(); // perform `get` +x + 100 // continuation: "add 100 to whatever get() resumed with" +---- + +Expected: `resume(5)` re-enters the body at the bind, so `x = 5` and the `handle` +yields `105`. Actual (tree-walker): the `handle` yields `5`. The continuation +`x + 100` is silently dropped. This is the *one genuinely-still-silent* shape in +the language (interpreter path only); everything else on the soundness ledger is +`fixed` / `loud-fail` / `removed`. + +=== 1.2 Why the tree-walker structurally cannot fix it in place + +The interpreter models a performed effect as a `Result` *error* that unwinds the +OCaml call stack to the nearest handler (`lib/interp.ml`): + +[source,ocaml] +---- +(* an effect operation, when called, raises: *) +Error (PerformEffect (op_name, args)) (* interp.ml ~1218 *) + +(* ExprHandle catches it after eval of the body has already returned: *) +| ExprHandle eh -> + begin match eval env eh.eh_body with (* interp.ml ~287 *) + | Error (PerformEffect (op_name, args)) -> (* ...select arm... *) +---- + +By the time `ExprHandle` sees `PerformEffect`, `eval eh.eh_body` has *already +returned* — the OCaml frames that represented "the rest of the body after +`get()`" (`x + 100`) have been unwound and discarded. The continuation no longer +exists. The `resume` builtin can therefore only do one thing: return its argument +as the value of the whole `handle` (`interp.ml ~327`): + +[source,ocaml] +---- +let resume_fn = VBuiltin ("__resume__", fun resume_args -> + ... match resume_args with [v] -> Ok v | ...) (* returns v; cannot re-enter *) +---- + +That is correct for *tail* resume (`op() => resume(...)` as the body's tail) and +silently wrong for *non-tail* resume (a bind chain after the `perform`). The +multi-shot case is already *fenced loud* (`interp.ml ~329`, a call-counter that +errors on the second `resume`), because returning the argument twice is even more +obviously wrong. The non-tail single-shot case cannot be fenced the same way: +nothing local tells `resume` that a discarded continuation existed. + +The fix is not a patch to `ExprHandle`. It is a change of *evaluation strategy*: +the continuation must be **reified as data** so it survives the `perform` and can +be re-entered. That is a CESK machine. + +=== 1.3 Why not OCaml 5 native effect handlers + +OCaml 5's `effect`/`continuation` would express this directly. It is unavailable +to us: the interpreter must compile under `js_of_ocaml` (the in-browser / editor +playground path), and must build on OCaml 4.14. `js_of_ocaml`'s support for +native effects is partial and the estate pins 4.14 for the toolchain. A +*defunctionalised* continuation — a list of frames that is ordinary data — needs +no runtime support at all and runs identically native and under jsoo. This is +exactly why `lib/solo_cesk.ml` was built defunctionalised rather than in CPS over +host closures (ADR-0025 Q1). + +== 2. The proven template — `lib/solo_cesk.ml` + +The hard part is already built and (for the Solo fragment) proof-coupled. The +Solo-core CESK machine reifies the continuation as a `frame list` and re-installs +it on `resume`: + +[source,ocaml] +---- +(* solo_cesk.ml: perform finds the nearest handler, capturing the delimited + continuation up to AND INCLUDING that handler — so resume re-installs it. *) +| Ret v, KPerform op :: k -> + let (captured, henv, arg_q, res_q, body, krest) = find_handler op k [] in + { ctrl = Eval body; + env = bind v arg_q (bind (VCont captured) res_q henv); (* k is DATA *) + k = krest; cost } + +(* resume injects a value into the captured continuation and runs it; because + `kc` is data, the SAME VCont may be resumed again — multi-shot. *) +| Ret v, KResumeArg kc :: k -> { ctrl = Ret v; env = st.env; k = kc @ k; cost } +---- + +`VCont of kont` makes a captured continuation a first-class value; +`find_handler` walks the frame stack to the matching `KHandle`, returning the +delimited slice; `kc @ k` re-enters it. This is precisely the mechanism the +tree-walker lacks. The port's job is to bring `interp.ml`'s *full surface* up to +this machine, not to invent the machine. + +== 3. The gap from `solo_cesk.ml` to `interp.ml` + +`solo_cesk.ml` deliberately covers only the reduced Solo core (ADR-0025 M1 +scope). The production interpreter is much larger. The port must close these +gaps: + +[cols="1,3,3"] +|=== +| Concern | `solo_cesk.ml` (M1) | `interp.ml` (port target) + +| Term surface +| ~12 `term` constructors (STLC + unit + ⊗ + ⊕ + let + 3 effect nodes), de Bruijn +| ~30 `expr` constructors + `stmt` + `block`, *named* environment, literals of + 6 base types, records/rows, arrays, tuples, variants, match, try/catch, builtins + +| Value domain +| 6-constructor `value` (`VUnit`/`VClos`/`VPair`/`VInl`/`VInr`/`VCont`) +| `value.ml`: `VUnit`/`VBool`/`VInt`/`VFloat`/`VChar`/`VString`/`VTuple`/`VArray`/ + `VRecord`/`VVariant`/`VClosure`/`VBuiltin`/`VRef`/`VMut`/`VOwn` + +| Store (S) +| *elided* — "Solo is pure, so the (S)tore is trivial and elided until + effects/mutation arrive at M2" +| **required** — `VRef`/`VMut`/`VOwn`, `StmtAssign`, `while`/`for` mutation need a + real heap. This is the (S) the port must add. + +| Errors +| OCaml exceptions (`Stuck`/`Affine_violation`/`Unhandled_effect`) +| `Result` + `eval_error` (`TypeMismatch`/`RuntimeError`/`PerformEffect`/…) — the + machine's `Stuck` maps onto `Error (RuntimeError …)` + +| Effect operation surface +| `Perform (op:int, arg)` — integer-labelled, single arg +| `PerformEffect (op:string, args:value list)` — string-labelled, multi-arg, + registered as builtins; `ExprHandle` arms (`HandlerOp`/`HandlerReturn`), + `ExprResume` keyword, `ExprTry`/catch/finally +|=== + +Net: the port is `solo_cesk.ml`'s machine *grown to the real value/term surface +and given the store S*. It is M1+M2 of ADR-0025 fused onto the production +interpreter, because the production interpreter cannot ship the M2 effect +machine without simultaneously carrying its existing (stateful) M1 surface. + +== 4. The port, staged so `dune runtest` stays green at every step + +Each stage is independently shippable and CI-gated. The governing safety net is a +**differential oracle**: the new machine and the existing tree-walker are run +against the whole positive fixture corpus and must agree — until Stage M2-3, where +they are *designed* to diverge on the non-tail fixture (the machine is right, the +walker is wrong) and the oracle flips to asserting the machine. + +The new machine lands as a *new module* (`lib/cesk.ml` — the full-surface +production CESK, distinct from `solo_cesk.ml`, the Solo-core proof oracle). The +tree-walker stays the default until M2-4, exactly as ADR-0025 directs +("`interp.ml` keeps serving real programs until the machine grows to supersede +it"). + +[cols="1,4,2"] +|=== +| Stage | Deliverable | Gate + +| *M2-0* +| Scaffold `lib/cesk.ml`: `control`/`env`/`kont`/`store`/`state` types, the + `value` re-used from `value.ml`, an empty `step` covering literals + `var` + + `let`. A `run` driver and an `eval_via_cesk : env -> expr -> value result` + wrapper that maps `Stuck → Error (RuntimeError …)`. Behind `--cesk` (off by + default). Differential oracle harness comparing `eval` vs `eval_via_cesk`. +| `dune runtest` green; oracle green on the pure-literal fixtures. + +| *M2-1* +| Port the **pure fragment** by defunctionalising every `let* x = eval … in …` + in `interp.ml` into a frame: `ExprIf`/`ExprBinary`/`ExprUnary`/`ExprApp`/ + `ExprLambda`/`ExprBlock`/`ExprTuple`/`ExprRecord`/`ExprArray` + field/index/ + match. Each interpreter recursion point becomes one `frame` constructor; each + `Ok v` continuation becomes a `Ret v` refocus rule. No effects, no store yet. +| Oracle green across all *pure* fixtures (no `mut`, no `handle`). + +| *M2-2* +| Add the **store (S)**: `VRef`/`VMut`/`VOwn`, a `store` (int-keyed heap), + `StmtAssign`, `while`/`for`, `OpRef`/`OpMutRef`/`OpDeref`. The machine state + becomes the full `(C,E,K,S)`. Affine/linear runtime enforcement stays *off* in + the interpreter port (it is ADR-0025 M4, opt-in) — parity with today's + interpreter is the contract here. +| Oracle green across all *stateful* fixtures (mutation, loops, refs). + +| *M2-3* — **closes #623** +| Port effects with **reified continuations**, transcribing `solo_cesk.ml`'s + `KHandle`/`KPerform`/`KResume*` frames and `find_handler` onto the + string-labelled, multi-arg, `Result`-shaped surface. `ExprHandle` installs a + `KHandle` boundary; the effect builtins push `KPerform`; `ExprResume` re-enters + the captured `VCont`. Non-tail resume now re-enters the bind chain → `105`. + Multi-shot now genuinely supported (the `VCont` is data) — retire the + `interp.ml` multi-shot loud-fence on the CESK path. `ExprTry`/catch is the + single-shot, non-resumable specialisation (ADR-0025 M3 folds in here). +| The xfail pin `test_resume_nontail_xfail` flips **XFAIL→XPASS** (see §5). + New runtime handler fixtures (ADR-0025 notes "*zero exist today*") added and + green. Oracle *intentionally diverges* on `handle_resume_nontail.affine` — the + oracle is updated to assert the CESK value (`105`) there. + +| *M2-4* +| Make `lib/cesk.ml` the **default** evaluator; keep the tree-walker one release + behind `--legacy-interp` as an escape; then decommission `interp.ml`'s `eval` + tree (or reduce it to a thin re-export). Update `bin/` entry points and the + jsoo build. +| Full `dune runtest` green on the CESK path as default; jsoo build green. +|=== + +== 5. What flips, concretely (the ledger consequences) + +When Stage M2-3 lands, these change in lock-step — they are the *acceptance +criteria*, enforced by the soundness-ledger gate (`tools/check-soundness-ledger.sh`): + +. `test/e2e/fixtures/handle_resume_nontail.affine` evaluates to `105`, not `5`. +. `test/xfail/test_xfail_pins.ml`'s `test_resume_nontail_xfail` (which asserts the + *correct* `105` and today fails-as-expected) reports **XPASS** — the harness's + "unexpected pass" signal. Per the *Pinned-residual discipline* in + `docs/SOUNDNESS.adoc`, an XPASS is the trigger to *promote* the pin to an + ordinary positive regression test and retire the residual. +. `docs/SOUNDNESS.adoc`: the row "#555 (interp, non-tail single-shot) / #623" + moves `residual (pinned)` → `fixed`; the *Still open* section's "the one + remaining residual" sentence is removed (there is then *no* silent hole on the + interpreter path). The `:ground-truth-sha:` stamp is refreshed. +. `docs/SOUNDNESS.adoc`: the row "#555 (interp, multi-shot)" moves `loud-fail` → + `fixed`/supported on the CESK path (multi-shot is now expressible). +. ADR-0025's *M2* is delivered for the production interpreter; `docs/ROADMAP.adoc` + and `docs/EFFECTS-IMPLEMENTATION.adoc` "Not Yet Complete" items 1–3 close for + the interpreter tier. + +Because the gate is content-bound (sha256 manifest) and stamp-enforced, the +ledger edit and the test flip must be in the *same* PR — the gate fails if the +row says `fixed` while the pin still reports XFAIL, or vice-versa. That coupling +is deliberate: it is the anti-staleness property this whole subsystem exists for. + +== 6. Design notes for the capture, on the real surface + +* *Named environments, not de Bruijn.* `interp.ml` binds by name (`extend_env`, + `lookup_env`); the CESK port keeps that — frames close over the *named* `env`, + exactly as `solo_cesk.ml`'s frames close over a `qenv`. No de Bruijn conversion. +* *String-labelled, multi-arg effects.* `find_handler` matches `op_name : string` + against `HandlerOp` arm names (today's `interp.ml ~302` logic), and binds the + arm's parameter patterns to `args : value list` plus the reified continuation — + reusing the existing `match_pattern` / `__resume__` plumbing, but with + `__resume__` now bound to a `VCont` (data) instead of a return-the-arg builtin. +* *The store survives capture.* A captured `VCont` closes over the continuation + frames but **not** a snapshot of the store — the store is threaded through the + machine state, so a resumed continuation observes store writes made between + capture and resume (the standard, and correct, semantics for mutable state under + delimited control). Multi-shot resumes therefore share the heap; this matches + OCaml-5-effects semantics and is the behaviour the runtime handler tests must + pin. +* *`Stuck` ⇒ `Error (RuntimeError …)`.* The machine's "no rule applies" cases + (the analogue of `solo_cesk.ml`'s `Stuck`) are surfaced as the interpreter's + existing `eval_error`, so callers see no new error vocabulary (F-4 faithfulness + is preserved). + +== 7. Non-goals and risks + +* *Non-goal: backends.* wasm/native effect lowering stays loud-fail (ADR-0025). + This plan does not change `docs/CAPABILITY-MATRIX.adoc`'s backend rows. +* *Non-goal: runtime affine enforcement.* ADR-0025 M4 (affine/linear + tropical + cost *on by default*) is a *separate* milestone; the interpreter port keeps + today's "enforced statically, not dynamically" contract so it is a pure + semantics-preserving refactor plus the resume fix. +* *Risk: performance.* A CESK `step` loop is slower than direct tree-walk for + pure code. Mitigation: the pure fragment can keep a fast in-frame refocus; and + per ADR-0025 the VM tier is the *semantics* tier, not the performance tier + (native is). Acceptable. +* *Risk: corpus coverage.* The oracle is only as good as the fixtures. ADR-0025 + flags that *zero* runtime handler tests exist today; M2-3 must add them + (single-shot tail, single-shot non-tail, multi-shot, nested/deep handlers, + handler-over-mutation) *before* claiming the hole closed. +* *Risk: scope of the refactor.* Defunctionalising ~30 `expr` constructors is + large. It is staged (M2-0…M2-4) precisely so no single PR is unreviewable and + `dune runtest` is never red. + +== 8. Sequencing & effort + +[cols="1,3,1"] +|=== +| Phase | Stages | Size + +| Machine + pure surface | M2-0 → M2-1 | M (multi-week) +| State | M2-2 | S–M +| Effects (closes #623) | M2-3 | M — the payload milestone +| Cutover | M2-4 | S +|=== + +M2-3 is the milestone that retires the last silent soundness hole; M2-0…M2-2 are +the semantics-preserving runway that makes M2-3 a localised, oracle-checked +change rather than a big-bang rewrite. The Solo-core machine (`solo_cesk.ml`) is +the executable reference for the effect rules; the differential oracle is the +safety net for the surface growth. + +Tracked against ADR-0025 (M2), `docs/SOUNDNESS.adoc` (the #623 / non-tail row), +and `docs/PROOF-NEEDS.adoc` (P-6 effect-row soundness, whose *blocked* status is +on #555 — this port is the interpreter-tier half of unblocking it). diff --git a/docs/NAVIGATION.adoc b/docs/NAVIGATION.adoc index 0382e874..69d99032 100644 --- a/docs/NAVIGATION.adoc +++ b/docs/NAVIGATION.adoc @@ -75,6 +75,7 @@ This guide helps you navigate the AffineScript repository structure. * link:CAPABILITY-MATRIX.adoc[Capability Matrix] - **Live** per-component readiness (authoritative for feature readiness) * link:SOUNDNESS.adoc[Soundness Ledger] - **Live** test-anchored soundness-hole status (authoritative for "is it sound?"; the matrix links here). *Start here for soundness questions.* * link:PROOF-NEEDS.adoc[Proof-Needs Inventory] - what must be *proven* (mostly unmechanised); distinct from the soundness ledger above +* link:INTERP-CESK-PORT.adoc[Interpreter CESK Port Plan] - engineering plan to close the #623 non-tail-resume residual (ADR-0025 M2); the one remaining silent soundness hole the ledger names * link:guides/TESTING-REPORT.adoc[Testing Report] - *RETIRED* (redirects to standards/TESTING.adoc + CAPABILITY-MATRIX.adoc) == Build System diff --git a/docs/decisions/0025-semantics-vm.adoc b/docs/decisions/0025-semantics-vm.adoc index 73a8b5e6..0c9066d6 100644 --- a/docs/decisions/0025-semantics-vm.adoc +++ b/docs/decisions/0025-semantics-vm.adoc @@ -98,6 +98,12 @@ float-aggregate programs the wasm backend now loud-fails. | *(direction)* | Defunctionalise the CESK machine into a flat **bytecode VM** — the stated destination — when execution speed or a JIT-able instruction stream is wanted. Semantics-preserving by construction (Reynolds/Danvy). |=== +The *engineering plan* to execute *M2* against the production interpreter +(`lib/interp.ml`) — staged so `dune runtest` stays green at every step, and +closing the #623 non-tail-resume residual the soundness ledger names — is +link:../INTERP-CESK-PORT.adoc[`docs/INTERP-CESK-PORT.adoc`]. `lib/solo_cesk.ml` +is the M1 Solo-core machine that plan transcribes onto the full surface. + == Consequences * The "use the interpreter" escape hatch the compiler *already prints* for diff --git a/formal/Rows.v b/formal/Rows.v new file mode 100644 index 00000000..6f574d23 --- /dev/null +++ b/formal/Rows.v @@ -0,0 +1,474 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) *) + +(* + Rows.v + ══════ + SCAFFOLD — record-row soundness, Wave-W0 seed. + + ┌────────────────────────────────────────────────────────────────────────┐ + │ ⚠ UNVERIFIED IN THIS ENVIRONMENT. This file was authored without a Coq │ + │ toolchain available (no `coqc`/`rocq`). It is therefore **NOT wired** │ + │ into `formal/_CoqProject` and is **NOT** part of `just -f │ + │ formal/justfile check`. Before it may count toward the discharged │ + │ obligations it MUST be: (1) `coqc -Q . ASFormal Rows.v`-clean; │ + │ (2) confirmed `Print Assumptions … = Closed under the global context` │ + │ (no axioms, no `Admitted`); (3) added to `_CoqProject` and the │ + │ `formal/README.adoc` contents table; (4) its statements lifted into │ + │ `Siblings_Stated.v` as the canonical parametric obligation (matching │ + │ the P-2/P-3/F-3/F-4 sibling pattern), with a `*_discharged` line. │ + │ The proofs below are complete *attempts* in the `P2_Stlc.v` idiom, to │ + │ give the owner a real starting point — not a machine-checked result. │ + └────────────────────────────────────────────────────────────────────────┘ + + WHAT THIS PROVES (the soundness content of rows): + Progress + preservation for the simply-typed lambda calculus extended with + **extensible records** — empty record `{}`, extension `{ l = e | e' }`, + selection `e.l`, and restriction `e \ l` — over a `lacks`-checked row + (no duplicate labels). The payload is canonical-forms for records: a + well-typed selection of a present label never gets stuck. This is the + structural-typing analogue of the function canonical-forms lemma in + `P2_Stlc.v`, and the seed for AffineScript's row-polymorphic records. + + RUNG LADDER (mirrors P2_Progress → P2_Stlc, K1 → K1Let, R0 → R1): + * W0 (THIS FILE): monomorphic extensible records. Rows are concrete + lists of (label, type); the `lacks` side-condition keeps selection + deterministic. No row *variables* yet. + * W1 (next): row **variables** + the `lacks`-predicate as a real judgment + — i.e. true *row polymorphism* (`{name : String | ρ} → String`). Needs + type-level variables, a row-tail variable, and instantiation; that is + the genuinely harder development and is deliberately deferred, exactly + as `P2_Stlc.v` defers the QTT/affine context-splitting layer. + + Encoding choice: record *terms* use explicit `rempty`/`rext` constructors + (so the standard `tm` induction principle covers record fields), while + record *types* use `list (id * ty)` (so the row helpers are ordinary list + fixpoints and no mutual-induction scheme is needed). This is the + Software-Foundations `Records.v` idiom. + + Funext-free, in the `P2_Stlc.v` style: contexts are compared only on a + term's free variables (`context_invariance`), so NO `functional_extensionality` + is used. Target: `Print Assumptions` = "Closed under the global context". + + `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. +*) + +Require Import PeanoNat. +Require Import List. +Import ListNotations. + +Definition id := nat. + +(* ── Syntax ─────────────────────────────────────────────────────────────── *) + +Inductive ty : Type := +| TUnit : ty +| TArrow : ty -> ty -> ty +| TRec : list (id * ty) -> ty. (* a record type IS its row *) + +Inductive tm : Type := +| var (x : id) +| app (f a : tm) +| abs (x : id) (A : ty) (b : tm) (* A is the domain type *) +| tunit +| rempty (* {} *) +| rext (l : id) (e1 e2 : tm) (* { l = e1 | e2 } *) +| rsel (l : id) (e : tm) (* e.l *) +| rres (l : id) (e : tm). (* e \ l (restriction) *) + +(* ── Row helpers (ordinary list fixpoints) ──────────────────────────────── *) + +Fixpoint row_lookup (l : id) (r : list (id * ty)) : option ty := + match r with + | [] => None + | (l', A) :: r' => if Nat.eqb l l' then Some A else row_lookup l r' + end. + +Fixpoint row_remove (l : id) (r : list (id * ty)) : list (id * ty) := + match r with + | [] => [] + | (l', A) :: r' => if Nat.eqb l l' then row_remove l r' else (l', A) :: row_remove l r' + end. + +Lemma row_lookup_head_eq : forall l A r, row_lookup l ((l, A) :: r) = Some A. +Proof. intros. simpl. rewrite Nat.eqb_refl. reflexivity. Qed. + +Lemma row_lookup_head_neq : forall l l' A r, + l <> l' -> row_lookup l ((l', A) :: r) = row_lookup l r. +Proof. intros l l' A r H. simpl. apply Nat.eqb_neq in H. rewrite H. reflexivity. Qed. + +Lemma row_remove_head_eq : forall l A r, row_remove l ((l, A) :: r) = row_remove l r. +Proof. intros. simpl. rewrite Nat.eqb_refl. reflexivity. Qed. + +Lemma row_remove_head_neq : forall l l' A r, + l <> l' -> row_remove l ((l', A) :: r) = (l', A) :: row_remove l r. +Proof. intros l l' A r H. simpl. apply Nat.eqb_neq in H. rewrite H. reflexivity. Qed. + +(* Removing a label that is absent is the identity. *) +Lemma row_remove_absent : forall l r, row_lookup l r = None -> row_remove l r = r. +Proof. + induction r as [| [l' A] r' IH]; intros H. + - reflexivity. + - simpl in *. destruct (Nat.eqb l l') eqn:E. + + discriminate H. + + rewrite IH; [reflexivity | assumption]. +Qed. + +(* Restriction cannot introduce a label that was absent. *) +Lemma row_lookup_remove_none : forall l l' r, + row_lookup l' r = None -> row_lookup l' (row_remove l r) = None. +Proof. + induction r as [| [l0 A] r' IH]; intros H. + - reflexivity. + - simpl in H. destruct (Nat.eqb l' l0) eqn:E1. + + discriminate H. + + simpl. destruct (Nat.eqb l l0) eqn:E2. + * apply IH; assumption. + * simpl. rewrite E1. apply IH; assumption. +Qed. + +(* ── Values ─────────────────────────────────────────────────────────────── *) + +Inductive value : tm -> Prop := +| v_abs : forall x A b, value (abs x A b) +| v_unit : value tunit +| v_rempty : value rempty +| v_rext : forall l v1 v2, value v1 -> value v2 -> value (rext l v1 v2). + +(* ── Substitution (closed-value convention, as in P2_Stlc.v) ────────────── *) + +Fixpoint subst (x : id) (s t : tm) : tm := + match t with + | var y => if Nat.eqb x y then s else var y + | abs y A b => abs y A (if Nat.eqb x y then b else subst x s b) + | app f a => app (subst x s f) (subst x s a) + | tunit => tunit + | rempty => rempty + | rext l e1 e2 => rext l (subst x s e1) (subst x s e2) + | rsel l e => rsel l (subst x s e) + | rres l e => rres l (subst x s e) + end. + +(* ── Small-step, call-by-value ──────────────────────────────────────────── *) + +Inductive step : tm -> tm -> Prop := +| ST_AppAbs : forall x A b v, value v -> step (app (abs x A b) v) (subst x v b) +| ST_App1 : forall f f' a, step f f' -> step (app f a) (app f' a) +| ST_App2 : forall f a a', value f -> step a a' -> step (app f a) (app f a') +(* record construction evaluates left-to-right *) +| ST_Ext1 : forall l e1 e1' e2, step e1 e1' -> step (rext l e1 e2) (rext l e1' e2) +| ST_Ext2 : forall l v1 e2 e2', value v1 -> step e2 e2' -> step (rext l v1 e2) (rext l v1 e2') +(* selection: reduce the record, then project the chain *) +| ST_Sel : forall l e e', step e e' -> step (rsel l e) (rsel l e') +| ST_SelExt_hit : forall l v1 v2, value (rext l v1 v2) -> step (rsel l (rext l v1 v2)) v1 +| ST_SelExt_miss : forall l l' v1 v2, + l <> l' -> value (rext l' v1 v2) -> step (rsel l (rext l' v1 v2)) (rsel l v2) +(* restriction: reduce the record, then drop the label from the chain *) +| ST_Res : forall l e e', step e e' -> step (rres l e) (rres l e') +| ST_ResEmpty : forall l, step (rres l rempty) rempty +| ST_ResExt_hit : forall l v1 v2, value (rext l v1 v2) -> step (rres l (rext l v1 v2)) v2 +| ST_ResExt_miss : forall l l' v1 v2, + l <> l' -> value (rext l' v1 v2) -> + step (rres l (rext l' v1 v2)) (rext l' v1 (rres l v2)). + +(* ── Typing ─────────────────────────────────────────────────────────────── *) + +Definition context := id -> option ty. +Definition empty : context := fun _ => None. +Definition extend (G : context) (x : id) (T : ty) : context := + fun y => if Nat.eqb x y then Some T else G y. + +Inductive has_type : context -> tm -> ty -> Prop := +| T_Var : forall G x T, G x = Some T -> has_type G (var x) T +| T_Abs : forall G x A B b, has_type (extend G x A) b B -> has_type G (abs x A b) (TArrow A B) +| T_App : forall G f a A B, has_type G f (TArrow A B) -> has_type G a A -> has_type G (app f a) B +| T_Unit : forall G, has_type G tunit TUnit +| T_REmpty : forall G, has_type G rempty (TRec []) +| T_RExt : forall G l e1 e2 A r, + has_type G e1 A -> + has_type G e2 (TRec r) -> + row_lookup l r = None -> (* lacks l: no duplicate labels *) + has_type G (rext l e1 e2) (TRec ((l, A) :: r)) +| T_RSel : forall G l e r A, + has_type G e (TRec r) -> + row_lookup l r = Some A -> + has_type G (rsel l e) A +| T_RRes : forall G l e r, + has_type G e (TRec r) -> + has_type G (rres l e) (TRec (row_remove l r)). + +(* ── Free variables / free-in-context (the funext-free machinery) ───────── *) + +Inductive afi : id -> tm -> Prop := +| afi_var : forall x, afi x (var x) +| afi_app1 : forall x f a, afi x f -> afi x (app f a) +| afi_app2 : forall x f a, afi x a -> afi x (app f a) +| afi_abs : forall x y A b, y <> x -> afi x b -> afi x (abs y A b) +| afi_ext1 : forall x l e1 e2, afi x e1 -> afi x (rext l e1 e2) +| afi_ext2 : forall x l e1 e2, afi x e2 -> afi x (rext l e1 e2) +| afi_sel : forall x l e, afi x e -> afi x (rsel l e) +| afi_res : forall x l e, afi x e -> afi x (rres l e). + +#[local] Hint Constructors afi : core. + +Lemma free_in_context : forall x t S G, + afi x t -> has_type G t S -> exists U, G x = Some U. +Proof. + intros x t S G Hafi; generalize dependent S; generalize dependent G. + induction Hafi; intros G S HT; inversion HT; subst. + - eauto. + - eapply IHHafi; eauto. + - eapply IHHafi; eauto. + - edestruct IHHafi as [U HU]; eauto. + unfold extend in HU. destruct (Nat.eqb y x) eqn:E. + + apply Nat.eqb_eq in E; subst y; exfalso; apply H; reflexivity. + + eauto. + - eapply IHHafi; eauto. + - eapply IHHafi; eauto. + - eapply IHHafi; eauto. + - eapply IHHafi; eauto. +Qed. + +Corollary typable_empty_closed : forall x t S, + afi x t -> has_type empty t S -> False. +Proof. + intros x t S Hafi HT. + destruct (free_in_context x t S empty Hafi HT) as [U HU]; discriminate HU. +Qed. + +Lemma context_invariance : forall G G' t S, + has_type G t S -> + (forall x, afi x t -> G x = G' x) -> + has_type G' t S. +Proof. + intros G G' t S HT; generalize dependent G'. + induction HT; intros G' Hf. + - apply T_Var. rewrite <- (Hf x (afi_var x)). assumption. + - apply T_Abs. apply IHHT. intros z Hz. unfold extend. + destruct (Nat.eqb x z) eqn:E; auto. + apply Hf. apply Nat.eqb_neq in E. auto. + - eapply T_App; [apply IHHT1 | apply IHHT2]; intros z Hz; apply Hf; auto. + - apply T_Unit. + - apply T_REmpty. + - apply T_RExt; [ apply IHHT1; intros z Hz; apply Hf; apply afi_ext1; auto + | apply IHHT2; intros z Hz; apply Hf; apply afi_ext2; auto + | assumption ]. + - eapply T_RSel; [ apply IHHT; intros z Hz; apply Hf; apply afi_sel; auto + | eassumption ]. + - apply T_RRes. apply IHHT; intros z Hz; apply Hf; apply afi_res; auto. +Qed. + +(* ── Substitution preserves typing ──────────────────────────────────────── *) + +Lemma subst_preserves_typing : forall G x U t v S, + has_type (extend G x U) t S -> + has_type empty v U -> + has_type G (subst x v t) S. +Proof. + intros G x U t v S Ht Hv; generalize dependent S; generalize dependent G. + induction t as + [ y | f IHf a IHa | y A b IHb | | | l e1 IHe1 e2 IHe2 | l e IHe | l e IHe ]; + intros G S Ht; simpl; inversion Ht; subst. + - (* var y *) + unfold extend in H1. destruct (Nat.eqb x y) eqn:E. + + injection H1 as H1. rewrite <- H1. + apply (context_invariance empty G); [assumption |]. + intros z Hz. exfalso; apply (typable_empty_closed z v U Hz Hv). + + apply T_Var; assumption. + - (* app f a *) + eapply T_App; [apply IHf | apply IHa]; eassumption. + - (* abs y A b *) + destruct (Nat.eqb x y) eqn:E. + + apply Nat.eqb_eq in E; subst y. + apply T_Abs. + apply (context_invariance (extend (extend G x U) x A) (extend G x A)); + [assumption |]. + intros z Hz. unfold extend. destruct (Nat.eqb x z); reflexivity. + + apply T_Abs. apply IHb. + apply (context_invariance (extend (extend G x U) y A) + (extend (extend G y A) x U)); [assumption |]. + intros z Hz. unfold extend. + destruct (Nat.eqb y z) eqn:E1; destruct (Nat.eqb x z) eqn:E2; + try reflexivity. + exfalso. apply Nat.eqb_neq in E. apply E. + apply Nat.eqb_eq in E1; apply Nat.eqb_eq in E2. + rewrite E2, <- E1; reflexivity. + - (* tunit *) apply T_Unit. + - (* rempty *) apply T_REmpty. + - (* rext l e1 e2 *) + apply T_RExt; [ apply IHe1; eassumption + | apply IHe2; eassumption + | assumption ]. + - (* rsel l e *) + eapply T_RSel; [ apply IHe; eassumption | eassumption ]. + - (* rres l e *) + apply T_RRes. apply IHe; eassumption. +Qed. + +(* ── Canonical forms ────────────────────────────────────────────────────── *) + +Lemma canon_arrow : forall v A B, + value v -> has_type empty v (TArrow A B) -> exists x b, v = abs x A b. +Proof. + intros v A B Hv HT; destruct Hv. + - inversion HT; subst; eauto. + - inversion HT. + - inversion HT. + - inversion HT. +Qed. + +(* A record value is the empty record or an extension. *) +Lemma canon_rec : forall v r, + value v -> has_type empty v (TRec r) -> + v = rempty \/ (exists l v1 v2, v = rext l v1 v2). +Proof. + intros v r Hv HT; destruct Hv. + - inversion HT. + - inversion HT. + - left; reflexivity. + - right; eauto. +Qed. + +(* ── Progress ───────────────────────────────────────────────────────────── *) + +Theorem progress : forall t S, has_type empty t S -> value t \/ exists t', step t t'. +Proof. + intros t S HT; remember empty as G eqn:HG. + induction HT. + - subst G; discriminate H. + - left; apply v_abs. + - right; subst G. + destruct IHHT1 as [Hvf | [f' Hf]]; [reflexivity | |]. + + destruct (canon_arrow _ _ _ Hvf HT1) as [x [b ->]]. + destruct IHHT2 as [Hva | [a' Ha]]; [reflexivity | |]. + * eexists; apply ST_AppAbs; assumption. + * eexists; apply ST_App2; [apply v_abs | eassumption]. + + eexists; apply ST_App1; eassumption. + - left; apply v_unit. + - left; apply v_rempty. + - (* T_RExt *) + subst G. + destruct IHHT1 as [Hv1 | [e1' H1]]; [reflexivity | |]. + + destruct IHHT2 as [Hv2 | [e2' H2]]; [reflexivity | |]. + * left; apply v_rext; assumption. + * right; eexists; apply ST_Ext2; [assumption | eassumption]. + + right; eexists; apply ST_Ext1; eassumption. + - (* T_RSel: has_type G e (TRec r), row_lookup l r = Some A *) + right; subst G. + destruct IHHT as [Hve | [e' He]]; [reflexivity | |]. + + destruct (canon_rec e r Hve ltac:(eassumption)) as [Hemp | [l0 [v1 [v2 Hext]]]]. + * subst e. + match goal with Hr : has_type empty rempty (TRec _) |- _ => + inversion Hr; subst end. + match goal with Hl : row_lookup _ _ = Some _ |- _ => + simpl in Hl; discriminate Hl end. + * subst e. destruct (Nat.eqb l l0) eqn:E. + -- apply Nat.eqb_eq in E; subst l0. + eexists; apply ST_SelExt_hit; assumption. + -- apply Nat.eqb_neq in E. + eexists; apply ST_SelExt_miss; [exact E | assumption]. + + eexists; apply ST_Sel; eassumption. + - (* T_RRes: has_type G e (TRec r) *) + right; subst G. + destruct IHHT as [Hve | [e' He]]; [reflexivity | |]. + + destruct (canon_rec e r Hve ltac:(eassumption)) as [Hemp | [l0 [v1 [v2 Hext]]]]. + * subst e. eexists; apply ST_ResEmpty. + * subst e. destruct (Nat.eqb l l0) eqn:E. + -- apply Nat.eqb_eq in E; subst l0. + eexists; apply ST_ResExt_hit; assumption. + -- apply Nat.eqb_neq in E. + eexists; apply ST_ResExt_miss; [exact E | assumption]. + + eexists; apply ST_Res; eassumption. +Qed. + +(* ── Preservation ───────────────────────────────────────────────────────── *) + +Theorem preservation : forall t t' S, + has_type empty t S -> step t t' -> has_type empty t' S. +Proof. + intros t t' S HT Hstep; generalize dependent S. + induction Hstep; intros S HT; inversion HT; subst. + - (* ST_AppAbs *) + match goal with H : has_type _ (abs _ _ _) _ |- _ => inversion H; subst end. + eapply subst_preserves_typing; eassumption. + - (* ST_App1 *) eapply T_App; [ apply IHHstep; eassumption | eassumption ]. + - (* ST_App2 *) eapply T_App; [ eassumption | apply IHHstep; eassumption ]. + - (* ST_Ext1 *) + apply T_RExt; [ apply IHHstep; eassumption | eassumption | eassumption ]. + - (* ST_Ext2 *) + apply T_RExt; [ eassumption | apply IHHstep; eassumption | eassumption ]. + - (* ST_Sel (congruence) *) + eapply T_RSel; [ apply IHHstep; eassumption | eassumption ]. + - (* ST_SelExt_hit *) + match goal with H : has_type empty (rext _ _ _) (TRec _) |- _ => + inversion H; subst end. + match goal with Hl : row_lookup _ _ = Some _ |- _ => + rewrite row_lookup_head_eq in Hl; injection Hl as Hl; subst end. + assumption. + - (* ST_SelExt_miss *) + match goal with Hr : has_type empty (rext _ _ _) (TRec _) |- _ => + inversion Hr; subst end. + match goal with + | Hl : row_lookup ?l ((?l',_) :: _) = Some _, Hn : ?l <> ?l' |- _ => + rewrite (row_lookup_head_neq l l' _ _ Hn) in Hl + end. + eapply T_RSel; eassumption. + - (* ST_Res (congruence) *) + apply T_RRes. apply IHHstep; eassumption. + - (* ST_ResEmpty *) + match goal with H : has_type empty rempty _ |- _ => inversion H; subst end. + simpl. apply T_REmpty. + - (* ST_ResExt_hit *) + match goal with H : has_type empty (rext _ _ _) (TRec _) |- _ => + inversion H; subst end. + rewrite row_remove_head_eq. + match goal with Hn : row_lookup ?l ?r0 = None |- _ => + rewrite (row_remove_absent l r0 Hn) end. + assumption. + - (* ST_ResExt_miss *) + match goal with Hr : has_type empty (rext _ _ _) (TRec _) |- _ => + inversion Hr; subst end. + match goal with Hn : ?a <> ?b |- _ => + rewrite (row_remove_head_neq a b _ _ Hn) end. + apply T_RExt. + + assumption. + + apply T_RRes. assumption. + + match goal with Hlk : row_lookup _ _ = None |- _ => + apply row_lookup_remove_none; exact Hlk end. +Qed. + +(* ── Stated obligation (local mirror of the Siblings_Stated.v pattern) ───── *) +(* When this file is verified and wired, lift this Section into + Siblings_Stated.v as the canonical parametric obligation (e.g. P-11 / + "record-row soundness"), and replace the discharges below with + `*_discharged : Siblings_Stated. … := ` lines. *) + +Section Rows_Stated. + Variable Tm Ty Ctx : Type. + Variable Empty : Ctx. + Variable HasType : Ctx -> Tm -> Ty -> Prop. + Variable Value : Tm -> Prop. + Variable Step : Tm -> Tm -> Prop. + + Definition Rows_progress : Prop := + forall t a, HasType Empty t a -> Value t \/ (exists t', Step t t'). + + Definition Rows_preservation : Prop := + forall g t t' a, HasType g t a -> Step t t' -> HasType g t' a. +End Rows_Stated. + +(* Discharge for the concrete model (closed-term, ctx := unit), exactly as + P2_Stlc.v discharges P2_progress / P2_preservation. *) + +Definition Rows_progress_discharged + : Rows_progress tm ty unit tt + (fun (_ : unit) (t : tm) (T : ty) => has_type empty t T) value step + := progress. + +Definition Rows_preservation_discharged + : Rows_preservation tm ty unit + (fun (_ : unit) (t : tm) (T : ty) => has_type empty t T) step + := fun (_ : unit) t t' T HT Hs => preservation t t' T HT Hs. + +Print Assumptions progress. +Print Assumptions preservation. From be1171e4ae16e45dc63f1d49949ab5bc3846552a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 17:40:20 +0000 Subject: [PATCH 2/2] chore(hypatia): exempt formal/Rows.v from the V-lang ban (per-file matcher) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit .hypatia-ignore matches `${rule}:${path}` as fixed-string whole-line equality (grep -qxF), not a glob — so each formal/*.v needs its own two lines. The new Rows.v scaffold is a Coq proof script like its 16 siblings; add the same vlang_detected + banned_language_file exemptions so a sweep cannot mis-flag it as V-lang. (Rows.v stays un-wired from _CoqProject — the exemption is about the file in the tree, independent of the build graph.) Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa --- .hypatia-ignore | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.hypatia-ignore b/.hypatia-ignore index d0bb6e8f..f9ac6336 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -75,3 +75,10 @@ cicd_rules/vlang_detected:formal/F5_RenderFaithful.v cicd_rules/banned_language_file:formal/F5_RenderFaithful.v cicd_rules/vlang_detected:formal/RealWasm.v cicd_rules/banned_language_file:formal/RealWasm.v +# Rows.v — record-row soundness scaffold (Wave-W0). Authored without a Coq +# toolchain, so it is UNVERIFIED and deliberately NOT in formal/_CoqProject; +# it is still a Coq proof script in the tree and must be exempted from the +# V-lang ban like its siblings (the ignore matcher is fixed-string per-file, +# not a glob, so a new .v needs its own lines). +cicd_rules/vlang_detected:formal/Rows.v +cicd_rules/banned_language_file:formal/Rows.v