docs: author the proof-needs inventory (P-/F-/K- obligation series)

[hyperpolymath]

What

Replaces the near-empty docs/PROOF-NEEDS.md (which held only the 2026-03-29 template-ABI cleanup note) with a real, structured inventory of what AffineScript must prove, at what rigour, with honest status — and renames it to .adoc per DOC-FORMAT.

This is the deliverable for a fresh proof-needs review of the repo: what we may have missed before, what's sharpened by outstanding work, and what's newly arisen from the faces work.

The review, in three partitions

P-1…P-10 — pre-faces obligations that existed but were never catalogued. The mechanized core is thinner than the prose corpus suggests:

• solo-core/Soundness.idr is statements-only — data Step has no constructors, progress/preservation are ?todo holes. It proves nothing yet, and covers only the Solo fragment (no traits/effects/rows/refinements/ownership/dependent types).
• The seven docs/academic/proofs/*.md are prose; docs/academic/mechanized/{agda,coq,lean}/ are explicit stubs; the affinescript-vite/verification/proofs/ files are RSR templates; and formal/ (the dir Umbrella: 8 must-have + 12 high-priority proof obligations for the AffineScript compiler #513 names) does not exist.
• The open soundness holes (soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554/tracking: general effect-handler dispatch (post-CORE-02 residual) — silent arm-drop on 3 backends; DECISION: back-port loud failure now? #555/codegen: Async CPS table-miss silently falls back to synchronous lowering — should fail loudly #556/soundness: refinement-type predicates parse but are silently not enforced (TRefined) #558/tracking: CORE-04 traits residual — associated-type substitution, where-clause supertraits, coherence checking #559) were tracked as defects but had no proof obligations linking them to the soundness arguments they falsify.

K-1…K-4 — needs sharpened by outstanding work. Codegen semantic-preservation (#513 must-have 7) is the keystone every face rests on; effect-soundness is blocked (not merely unproven) by the #555 handler mis-lowering; borrow soundness must be stated to reject the #554 counterexample.

F-1…F-7 — NEW obligations from the faces work, entirely absent from the #513 programme:

• F-1 transformer semantics-preservation (the real same-cube theorem — front-end analogue of K-1)
• F-2 same-cube cross-face agreement — partially mechanized in invariant-path/proofs/SameCube.agda (unit-tail case); the value-returning divergence is the concrete instance Face transformers disagree on trailing-statement lowering — greet compiles to 2 wasm classes #601
• F-3 pragma-detection determinism/totality/confluence (lib/face_pragma.ml)
• F-4 error-vocabulary faithfulness (lib/face.ml — a simulation, beyond OCaml's exhaustiveness check)
• F-5 render_ty injectivity / non-collision
• F-6 preview round-trip totality
• F-7 face confluence with canonicalisation

Also catalogues the aggregate-library law-conformance obligation (cross-cube, vs faces' cross-face) and points the same-cube track at invariant-path's SameCube.agda + verify-same-cube.sh.

Also in this PR

• Rename docs/PROOF-NEEDS.md → docs/PROOF-NEEDS.adoc (DOC-FORMAT).
• Update the three referrers: docs/NAVIGATION.adoc, .machine_readable/integrations/verisimdb.a2ml, and spec/FRG-PROFILE.adoc — the FRG "no PROOF-NEEDS" honest gap is now met (path-to-D step 6 done; grade unchanged, still no formal/ prover encoding).

Scope / non-goals

This is a catalogue of obligations only — no proof is asserted discharged, no code changes, no relicensing. Every Status column entry of stated/prose/absent means not proven. Cross-referenced to #513 (it adds the faces + aLib obligations #513 omits) and #563.

🤖 Generated with Claude Code

https://claude.ai/code/session_01KPG9mEQXFyA3k7NWAzMNMr

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 43 issues detected

Severity	Count
🔴 Critical	2
🟠 High	25
🟡 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 scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence