security: 2 ProofDrift findings need DRAFT-PR remediation (Track D)

[hyperpolymath]

panic-attack estate sweep — Track D (proof-aware) tracking issue

panic-attack assail flagged the following PA021 ProofDrift findings in this repo on 2026-05-26.

Unlike Track C findings (judgement calls in non-proof code), these touch proof modules. The campaign convention is to remediate them via DRAFT PRs with a local proof-rebuild check (agda / lake build / coqc / idris2 --check / isabelle build) before flipping to ready-for-review. Each finding falls into one of these buckets:

• legitimate-upstream-postulate: language-binding primitives that are postulated by design (FFI to Haskell, IO base, primitive types) — classify in audits/assail-classifications.a2ml, do NOT 'fix'.
• unfinished-proof: Admitted / sorry / oops / believe_me / trustMe in finishable proofs — discharge in a DRAFT PR, rebuild, then mark ready.
• parked-debt: tracked separately (e.g. ephapax preservation, boj-server class-J primitives) — do NOT refile here.

Estate tracker: hyperpolymath/panic-attack#32.

Findings

Medium  proofs/agda/Basic.agda:?  1 postulate block(s) (unproven axiom — verify these hold) in proofs/agda/Basic.agda
Medium  proofs/agda/SoundnessPreservation.agda:?  1 postulate block(s) (unproven axiom — verify these hold) in proofs/agda/SoundnessPreservation.agda

---

🤖 Discovered during the panic-attack estate sweep (2026-05-26). See hyperpolymath/panic-attack#32 for campaign tracker.

[hyperpolymath]

Closed by classification PR #107. Both findings are legitimate axioms with inline source justification (funext = HoTT-standard function extensionality; Conflicts = intentional parameter, not debt).