docs(proof-needs): refresh stale §1 baseline + §6 sequencing after Wave 1–3

[hyperpolymath]

What

docs/PROOF-NEEDS.adoc's status tables were already correct (§2 P-rows, §4 F-rows track every obligation accurately), but two narrative sections went stale during the Wave 1/2/3 mechanization that landed in #632 / #634. This refresh re-grounds them against the live formal/ tree.

Ground truth at time of writing: 13 .v files, 22 Print Assumptions closure reports, all axiom-free (verified by recompiling the whole track with coqc -Q . ASFormal and auditing for Axioms:).

Changes (docs only)

• §1 formal/ baseline listed only 8 of the 13 proof files — it predated P2_Stlc, P3_BorrowGraph, and the QTT trio (QttSemiring / AffineUsage / QttTyping). Now lists all 13 with the true count.
• §6 sequencing table reframed: the doc described Waves 1–3 as future and cited "11 closure reports". Waves 1 (model growth) and 2 (static QTT) are done; Wave 3 is now correctly stated as the real lift — formalise the real AffineScript AST + real typed-WASM operational semantics, then the remaining prose/absent obligations.
• K-1 bullet now notes K1Let_CodegenPreservation.v grows the seed with de Bruijn variables / let / environment.
• K-3 bullet now notes P3_BorrowSound.v / P3_BorrowGraph.v already reject the soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554 witness in-model (was "should be written").
• Intro "almost none mechanized" → "a growing axiom-free Coq core (small models; no full-language theorem discharged yet)".

No proof content changes; no status-column downgrades. This only makes the prose match the tables and the tree.

🤖 Generated with Claude Code

https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

---

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