feat(formal): Wave 2 — the affine/QTT quantity semiring + affine usage

[hyperpolymath]

What

Wave 2: the affine/QTT layer — the algebraic core that makes AffineScript actually affine. Advances P-4 from prose to mechanized. Axiom-free (Print Assumptions closed; lia introduces no axioms), no Admitted.

QttSemiring.v — the quantity semiring {0,1,ω}

• qplus (context addition, with the crux 1 + 1 = ω) and qmult (scaling)
• All semiring laws (assoc/comm/identity/distributivity) + the usage order 0 ≤ 1 ≤ ω, by exhaustive case analysis
• The bridge qof (m + n) = qplus (qof m) (qof n) — occurrence counts add under QTT addition
• The affine fact: qplus One One = Omega and ~ qle (qplus One One) One

AffineUsage.v — affine usage over the semiring

• usage x t := qof (count x t); proves usage composes through application: usage x (app f a) = qplus (usage x f) (usage x a) (from qof_plus)
• Defines affine well-formedness (every binder consumes its variable at most once)
• Payoff: λx.x is affine; λx. x x is not — its variable totals ω, exceeding the affine bound. The mechanized statement of "a linear value may not be duplicated."

Scope (honest)

The full typed QTT calculus — context splitting Γ = Γ₁ + Γ₂, progress + preservation tracking quantities, on top of P2_Stlc.v — is the next increment. This PR lands the algebra + usage reading it rests on.

Track status

12 files, 18 closure reports, zero axioms. justfile/_CoqProject build both new files; .hypatia-ignore extends the Coq-.v-isn't-V-lang carve-out; README gains a "Wave 2" section; PROOF-NEEDS.adoc P-4 → partial.

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