feat(formal): grow P-3 to a real borrow graph (loan edges + move-locality)

[hyperpolymath]

What

P-3, Wave 1: the real borrow graph. Replaces P3_BorrowSound.v's single validity bit with the actual shape of a borrow checker — multiple resources (each live or moved) and an explicit borrow graph of loan edges (reference ↦ the resource it borrows). A deref is valid iff its loan target is still live — the flow-sensitive, Polonius-style (#553) reading: loans are tracked, validity = target liveness at the point of use.

Proven (axiom-free, no Admitted)

• borrow_soundness — an accepted program never derefs a dangling reference.
• borrow_complete — the checker rejects exactly the use-after-move programs.
• move_locality — the genuine borrow-graph theorem: moving resource b cannot change the validity of a deref borrowing some a ≠ b (an OMove only reaches references whose loan edge points at the moved resource). This is the real, non-trivial content.
• rejects_554 — the multi-resource soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554 program [ONew 0; OBorrow 0 0; OMove 0; OUseRef 0] is rejected, matching lib/borrow.ml's post-soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554-fix behaviour.

Discharges the Siblings_Stated P3 statements for the richer model.

Scope (honest)

Still a sequential op model — no aliasing of references, no mutable borrows, no loops/CFG. Those + the real lib/borrow.ml control-flow graph are further increments. But the borrow graph (loan edges) and target-liveness validity are now real.

Track status

9 files, 14 closure reports, zero axioms. P3_BorrowSound.v stays as the single-bit seed; P3_BorrowGraph.v is the grown model (the K1/K1Let pattern). justfile/_CoqProject build it; .hypatia-ignore extends the Coq-.v-isn't-V-lang carve-out; README + PROOF-NEEDS.adoc P-3 row updated.

just -f formal/justfile check

(P-2 Wave 1 — functions/binders/substitution — is next, as a separate PR.)

🤖 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