feat(formal): verify + wire Rows.v (P-11 record-row soundness)

.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

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 <<status>>).
 
@@ -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 <<outstanding>>, <<faces>>.
+  (R1: the first real `⟦compile p⟧ = ⟦p⟧`). Record rows: `Rows.v` (P-11 —
+  progress + preservation for extensible records). See <<outstanding>>, <<faces>>.
 * **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]

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

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.<name> … := <proof>` 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.

formal/_CoqProject

@@ -16,3 +16,4 @@ QttDynamic.v
 F5_RenderFaithful.v
 RealWasm.v
 RealCompile.v
+Rows.v

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"