feat(formal): mechanize the four Wave-0 siblings (P-2, P-3, F-3, F-4)

[hyperpolymath]

What

Turns the four stated Wave-0 siblings in Siblings_Stated.v into mechanized proofs. Each new file builds a concrete model, proves the property, and ends in a *_discharged : Siblings_Stated.<name> … := <proof> line that type-checks the concrete proof against the stated obligation. All Coq/Rocq 8.18, axiom-free (Print Assumptions → "Closed under the global context"), no Admitted.

File	Obligation	Proven
P2_Progress.v	P-2	progress + preservation for a simply-typed first-order calculus (nat/bool/add/if), small-step CBV, with canonical forms
P3_BorrowSound.v	P-3	a one-resource borrow checker is sound and rejects the #554 witness [OBorrow; OMove; OUseRef]
F3_PragmaDecidable.v	F-3	the alias table is a function; detection factors through the scanned region (independent of bytes past the pragma)
F4_ErrorFaithful.v	F-4	the face renderer preserves an error's class + referent, changing only vocabulary

P3_BorrowSound.v matches lib/borrow.ml's post-#554-fix behaviour (per the new SOUNDNESS.adoc): the sound checker is exactly the one that now rejects use-after-move through a callee-returned borrow.

Scope (honest)

These are small fragments — enough to discharge the obligation and pin its meaning, not the full language. Growing them is Wave 1: functions/binders/QTT for P-2, the real borrow graph + Polonius (#553) for P-3.

Wiring & docs

• justfile check + _CoqProject compile all eight files in dependency order and assert no axioms — 11 closure reports.
• .hypatia-ignore extends the Coq-.v-isn't-V-lang carve-out to the four new files.
• PROOF-NEEDS.adoc: P-2/P-3/F-3/F-4 → partial (mechanized model); Wave-0 row marked done. README.adoc + the Siblings_Stated header point at the discharge files.

Check

just -f formal/justfile check

Verified locally: 8 files, 11 closure reports, zero axioms.

🤖 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