From 1fac093f71e576442bcafb3cb35a37886c0b1858 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 19:04:02 +0000 Subject: [PATCH] feat(formal): verify + wire Rows.v (P-11 record-row soundness) Rows.v landed in #639 as an explicitly-UNVERIFIED scaffold because the authoring container had no Coq toolchain. Installed Coq 8.18.0 (OCaml 4.14.1, the repo's pinned toolchain) and verified it: coqc -Q . ASFormal Rows.v -> clean Print Assumptions progress / preservation -> "Closed under the global context" (axiom-free, no Admitted) The hand-written proofs compiled first try. So promote the scaffold to a real, wired obligation: * formal/_CoqProject + formal/justfile `check`: add Rows (the recipe fails on any axiom/Admitted, so this now gates Rows too). * formal/Rows.v: replace the UNVERIFIED banner with the verified/wired note; drop the stale "Target:"/"lift into Siblings_Stated" wording. * formal/README.adoc: contents-table row + a "Record rows (P-11)" section. * docs/PROOF-NEEDS.adoc: new P-11 obligation row (mechanized); refresh the Coq-core counts to 18 files / 31 Print-Assumptions reports (also corrects the long-stale "13 files" intro line). * .hypatia-ignore: de-stale the Rows.v comment (now mechanized + wired). Full track re-verified end to end: 18 files, 31 closure reports, zero axioms. dune build clean; soundness-ledger gate green (SOUNDNESS.adoc untouched). Scope unchanged: Wave W0 (monomorphic extensible records); row-*variable* polymorphism is the W1 increment (P-11 row notes it). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01BbxKhXQwTvVgkYDgBMLJoa --- .hypatia-ignore | 9 ++++----- docs/PROOF-NEEDS.adoc | 17 ++++++++++++++--- formal/README.adoc | 21 +++++++++++++++++++++ formal/Rows.v | 35 ++++++++++++++--------------------- formal/_CoqProject | 1 + formal/justfile | 2 +- 6 files changed, 55 insertions(+), 30 deletions(-) diff --git a/.hypatia-ignore b/.hypatia-ignore index 31bf50c1..b07071be 100644 --- a/.hypatia-ignore +++ b/.hypatia-ignore @@ -75,11 +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). +# Rows.v — record-row soundness (P-11, Wave-W0). Coq proof script, mechanized +# and wired into formal/_CoqProject like its siblings; exempt from the V-lang +# ban (the ignore matcher is fixed-string per-file, not a glob, so each new .v +# needs its own lines). cicd_rules/vlang_detected:formal/Rows.v cicd_rules/banned_language_file:formal/Rows.v cicd_rules/vlang_detected:formal/RealCompile.v diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc index a1e7e693..b424dd77 100644 --- a/docs/PROOF-NEEDS.adoc +++ b/docs/PROOF-NEEDS.adoc @@ -12,7 +12,7 @@ This is the single document that enumerates *what AffineScript must prove*, at gap between the soundness *arguments* the project relies on (prose in `docs/academic/proofs/`, the borrow-checker comments in `lib/borrow.ml`, `docs/CAPABILITY-MATRIX.adoc`) and the soundness *proofs* that are actually -mechanized today: a growing axiom-free Coq core (13 files) that pins each +mechanized today: a growing axiom-free Coq core (18 files) that pins each obligation on a deliberately *small model* — no full-language theorem is discharged yet (see <>). @@ -70,7 +70,7 @@ than the prose corpus suggests: `TypeSafety.v` is example lemmas about list length, not AffineScript. Not core-metatheory. * **`formal/`** — the directory #513 names as the mechanized-proof target now - **exists** (Coq/Rocq 8.18), axiom-free throughout — **17 files, 29 `Print + **exists** (Coq/Rocq 8.18), axiom-free throughout — **18 files, 31 `Print Assumptions` closure reports**, all "Closed under the global context". Codegen keystone: `K1_CodegenPreservation.v` (K-1 minimal) + `K1Let_CodegenPreservation.v` (K-1 grown with variables/`let`/environment). @@ -85,7 +85,8 @@ than the prose corpus suggests: typing, `usage x t = Γ x` sound) + `QttDynamic.v` (the dynamic half: β-reduction preserves the usage profile). Real lift (`REAL-LIFT.adoc`): `RealWasm.v` (real `lib/wasm.ml` IR — i32 core + locals) + `RealCompile.v` - (R1: the first real `⟦compile p⟧ = ⟦p⟧`). See <>, <>. + (R1: the first real `⟦compile p⟧ = ⟦p⟧`). Record rows: `Rows.v` (P-11 — + progress + preservation for extensible records). See <>, <>. * **Research tracks** (not core soundness): `docs/academic/tropical-session-types/` (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`, `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue, @@ -207,6 +208,16 @@ obligations. They are the "we might have missed" half of the brief. follow-up. The *proof* that resolution is unique remains unwritten. | L | `absent` | #559; #513 high-priority + +| P-11 +| **Record-row soundness.** Well-typed record operations never get stuck: a + selection of a present label always reduces, and extension/restriction + preserve typing over a `lacks`-checked row (no duplicate labels). Distinct + from P-6 *effect*-row soundness. +| M | `mechanized` +| `formal/Rows.v` — progress + preservation for STLC + extensible records + (empty/extend/select/restrict), funext-free, axiom-free. Wave W0 + (monomorphic rows); row-*variable* polymorphism is the W1 increment |=== [#outstanding] diff --git a/formal/README.adoc b/formal/README.adoc index 2c1473b6..ccd7446d 100644 --- a/formal/README.adoc +++ b/formal/README.adoc @@ -105,6 +105,11 @@ cannot mistake it. Coq has no `v.mod` manifest, so `vmod_detected` never fires. source, reference `eval`, `compile` to real wasm, `compile_correct` (retires K1/K1Let on real objects) | **mechanized**, axiom-free + +| `Rows.v` +| **P-11** — record-row soundness: progress + preservation for STLC + extensible + records (empty/extend/select/restrict over a `lacks`-checked row), funext-free +| **mechanized**, axiom-free |=== All mechanized theorems report *Closed under the global context* under `Print @@ -249,6 +254,22 @@ R-wrap → R-eff), the Coq module structure, and the strategy for each hard part (loops/termination via fuel, linear memory, floats, the elaboration nodes, effects) — is `formal/REAL-LIFT.adoc`. +== Record rows (P-11) + +`Rows.v` is the seed for AffineScript's *row-polymorphic records*. It extends the +`P2_Stlc.v` STLC with **extensible records** — `{}` (empty), `{ l = e | e' }` +(extension), `e.l` (selection), and `e \ l` (restriction) — typed over a row +carrying a `lacks` side-condition (no duplicate labels), and proves full +**progress + preservation**. The soundness payload is canonical-forms for +records: a well-typed selection of a present label never gets stuck. Record +*terms* use explicit `rempty`/`rext` constructors (so the standard term +induction covers fields) while record *types* are `list (id * ty)` (so the row +helpers are ordinary list fixpoints — no mutual-induction scheme); this is the +Software-Foundations `Records.v` idiom, kept funext-free like `P2_Stlc.v`. This +is **Wave W0** (monomorphic rows); row *variables* + the `lacks` judgment (true +row *polymorphism*, e.g. `{name : String | ρ} → String`) are the **W1** +increment, deferred exactly as `P2_Stlc.v` defers the QTT/affine layer. + == Scope (honest) These are Wave-0/1 seeds, not the discharged obligations. The fragments are diff --git a/formal/Rows.v b/formal/Rows.v index 6f574d23..12465f7e 100644 --- a/formal/Rows.v +++ b/formal/Rows.v @@ -4,22 +4,13 @@ (* 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. │ - └────────────────────────────────────────────────────────────────────────┘ + P-11 — record-row soundness, Wave-W0. **Mechanized, axiom-free.** + + Verified with Coq 8.18.0 (OCaml 4.14.1): `coqc -Q . ASFormal Rows.v` is + clean, and the `Print Assumptions` reports at the foot of this file both + say "Closed under the global context" — no axioms, no `Admitted`. Wired + into `formal/_CoqProject` and the `formal/justfile` `check` recipe (which + fails if any proof gains an axiom/`Admitted`), exactly like its siblings. WHAT THIS PROVES (the soundness content of rows): Progress + preservation for the simply-typed lambda calculus extended with @@ -48,7 +39,7 @@ 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". + is used — hence `Print Assumptions` = "Closed under the global context". `.v` is Coq, not V-lang — see formal/README.adoc and .hypatia-ignore. *) @@ -438,10 +429,12 @@ Proof. 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. *) +(* The obligation shape is progress + preservation over the record calculus — + structurally the same parametric Prop as `Siblings_Stated.P2_progress` / + `P2_preservation`, restated here with record-specific naming so P-11's + identity is self-documenting. Kept local (not lifted into + Siblings_Stated.v) precisely to avoid a near-duplicate of the P-2 section; + the discharges below type-check the concrete record model against it. *) Section Rows_Stated. Variable Tm Ty Ctx : Type. diff --git a/formal/_CoqProject b/formal/_CoqProject index 6b332769..7326d052 100644 --- a/formal/_CoqProject +++ b/formal/_CoqProject @@ -16,3 +16,4 @@ QttDynamic.v F5_RenderFaithful.v RealWasm.v RealCompile.v +Rows.v diff --git a/formal/justfile b/formal/justfile index 4d78562b..4aa4f01f 100644 --- a/formal/justfile +++ b/formal/justfile @@ -13,7 +13,7 @@ check: F1_TransformerPreservation F3_PragmaDecidable F4_ErrorFaithful \ P3_BorrowSound P3_BorrowGraph P2_Progress P2_Stlc \ QttSemiring AffineUsage QttTyping QttDynamic \ - F5_RenderFaithful RealWasm RealCompile; do + F5_RenderFaithful RealWasm RealCompile Rows; do echo "== coqc $f.v ==" o="$(coqc -Q . ASFormal "$f.v")" printf '%s\n' "$o"