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

[hyperpolymath]

What

Rows.v (P-11, record-row soundness) landed in #639 as an explicitly-unverified scaffold — the authoring container had no Coq toolchain, so it shipped un-wired with a loud UNVERIFIED banner. This PR closes that loop: I 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"

The hand-written proofs compiled first try, axiom-free, no Admitted. So the scaffold is promoted to a real, wired obligation.

Changes

• formal/_CoqProject + formal/justfile check: add Rows (the recipe fails on any axiom/Admitted, so this now gates Rows too).
• formal/Rows.v: UNVERIFIED banner → verified/wired note; dropped the stale "Target:" / "lift into Siblings_Stated" wording.
• formal/README.adoc: contents-table row + a "Record rows (P-11)" prose section.
• docs/PROOF-NEEDS.adoc: new P-11 obligation row (mechanized); refreshed Coq-core counts to 18 files / 31 Print Assumptions reports (also fixes the long-stale "13 files" intro line).
• .hypatia-ignore: de-stale the Rows.v comment (now mechanized + wired).

Verification (run in this environment)

• Full track re-compiled end to end via the justfile check list: 18 files, 31 closure reports, zero axioms.
• Rows.v re-verified standalone after the comment edits.
• dune build clean; tools/check-soundness-ledger.sh green (SOUNDNESS.adoc untouched).

Scope

Unchanged from #639: Wave W0 (monomorphic extensible records — empty/extend/select/restrict over a lacks-checked row). Row-variable polymorphism (true row polymorphism) is the W1 increment, noted on the P-11 row as the next rung.

🤖 Generated with Claude Code

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 41 issues detected

Severity	Count
🔴 Critical	2
🟠 High	23
🟡 Medium	16

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action denoland/setup-deno@v2 needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affinescript-cli/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (2 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/packages/affine-vscode/mod.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Shell execution -- validate input before passing to shell (1 occurrences, CWE-78)",
    "type": "js_exec_sync",
    "file": "/home/runner/work/affinescript/affinescript/affinescript-vite/src/affine-plugin-improved.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (32 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/wasm_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (29 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/affinescript/affinescript/affinescriptiser/src/codegen/affine_gen.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (2 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/panic.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (1 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/alloc.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unsafe block -- requires SAFETY comment (3 occurrences, CWE-676)",
    "type": "unsafe_block",
    "file": "/home/runner/work/affinescript/affinescript/runtime/src/ffi.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence