feat(formal): Wave 3 capstone — quantitative typing tracks usage soundly

[hyperpolymath]

What

Wave 3 (capstone): a quantitative type system. Fuses the three Wave-1/2 pieces — the term/typing structure of P2_Stlc, the multiplicity semiring of QttSemiring, and the occurrence-count usage of AffineUsage — into one judgment whose context tracks quantities.

Inductive qtt : uctx -> tm -> qty -> Prop :=   (* uctx = var -> quant *)
| Q_Var : qtt (usingle x) (var x) A                         (* one var, once *)
| Q_App : qtt G1 f (QArr q A B) -> qtt G2 a A ->
          qtt (uadd G1 G2) (app f a) B                       (* Γ₁ + Γ₂ *)
| Q_Lam : G x = Zero -> qtt (uext G x q) b B ->
          qtt G (lam x b) (QArr q A B).                      (* bind at multiplicity q *)

Capstone theorem

Theorem usage_soundness : qtt G t A -> forall x, usage x t = G x.

The typing context records exactly the QTT usage of every variable — so the static quantity bookkeeping is sound w.r.t. actual occurrence counts. Corollary linear_uses_once: a term typed in a singleton context uses that one variable exactly once — linearity, read straight off the typing.

Axiom-free, no Admitted — both Print Assumptions closed.

Scope (honest)

This is the static quantity discipline, now unified and proven sound against usage. The dynamic half — operational progress + preservation that preserves the quantity accounting under reduction (a quantitative substitution lemma over P2_Stlc.v) — is the remaining step.

Track status

13 files, 20 closure reports, zero axioms. justfile/_CoqProject build it; .hypatia-ignore extends the Coq-.v-isn't-V-lang carve-out; README gains the Wave-3 capstone; PROOF-NEEDS.adoc P-4 row updated.

just -f formal/justfile check

🤖 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