feat(formal): P-4 dynamic half — β-reduction preserves the QTT usage profile

[hyperpolymath]

What

Completes the static/dynamic pair for P-4 (QTT affine usage). QttTyping.v (Wave 3) proved the static side — usage_soundness: the typing context records exactly the usage. This adds formal/QttDynamic.v, the dynamic side: a small-step β-reduction on the QTT term language (AffineUsage.tm) that carries the whole usage profile forward unchanged.

Headline

Theorem step_preserves_usage : forall t t',
  step t t' -> forall z, usage z t' = usage z t.

The quantity accounting is a dynamic invariant. Composed with the Wave-3 static capstone it yields:

Corollary qtt_context_preserved : forall G t A t',
  qtt G t A -> step t t' -> forall x, usage x t' = G x.

— a well-typed term's QTT context stays valid across a reduction step (static + dynamic ⇒ the quantity discipline is sound under evaluation).

Also

• QTT scaling law usage z (subst x v b) = usage z b + usage x b · usage z v on the binder-free fragment, via a new qof_mult ×-homomorphism (qof (m*n) = qmult (qof m) (qof n)) — the analogue of QttSemiring.qof_plus. This is the multiplicity scaling that makes substructurality bite.
• affine_no_increase — an affine redex (usage x b ≤ 1) never increases any variable's usage: the dynamic face of the affine bound.
• linear_exact — a linear redex preserves usage exactly.

β substitutes a closed value (the call-by-value, closed-program convention P2_Stlc.v also uses), so capture cannot arise and the development is axiom-free — all three Print Assumptions report Closed under the global context.

Honest scope

This is the dynamic half on the same small QTT model as Wave 2/3, not the full language. The remaining lift is the quantity-preserving substitution lemma generalised past the binder-free / closed-value fragment onto the real AST (tracked in PROOF-NEEDS.adoc §6 Wave 3 — the "real lift").

Wiring / docs

• formal/_CoqProject, formal/justfile (dep-order compile + axiom gate), .hypatia-ignore (.v is Coq, not V-lang — both rule names), formal/README.adoc (Contents row + Wave-2/3 prose).
• docs/PROOF-NEEDS.adoc: P-4 row + §6 Wave 2 updated (dynamic half no longer pending). formal/ is now 14 files, 23 axiom-free closure reports.

Verified locally: all 14 proofs recompile in dependency order with coqc -Q . ASFormal; no Axioms: in any Print Assumptions.

🤖 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