You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hypatia code_scanning_alertsCSA004 (medium, review), surfaced on the #266 scan.
Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' at proofs/agda/EchoImageFactorizationPropPostulated.agda — ensure dismissal is documented and justified.
Assessment (verified): appears ALREADY satisfied. The dismissal is documented in three places:
commit ae7f8fb self-documents the CSA004 agda_postulate dismissal inline in the module;
docs/proof-debt.md §(c) justifies the four propositional-truncation postulates as the --safe --without-K-profile shadow of the --cubical-constructed ∥_∥ in EchoImageFactorizationPropCubical.agda (which realises them with zero postulates);
the module carries an inline hypatia: allow pragma and is allow-listed in tools/check-guardrails.sh. It is outside the wired All.agda/Smoke.agda cone, so the --safe kernel depends on it not at all.
Disposition: confirmation only — verify the above satisfies the "documented + justified" bar, then close. Likely immediately closeable.
Verified 2026-09-30 against HEAD, closing as satisfied:
proofs/agda/EchoImageFactorizationPropPostulated.agda:3: inline hypatia: allow code_safety/agda_postulate with justification (commit ae7f8fb)
docs/proof-debt.adoc:41: the postulate site is documented, with the zero-postulate --cubical discharge in EchoImageFactorizationPropCubical.agda
tools/check-guardrails.sh:43: the module is guardrail-exempted
The CSA004 dismissal is documented and justified in all three places the issue asked for.
Activity
hyperpolymath commentedon Sep 30, 2026
Verified 2026-09-30 against HEAD, closing as satisfied:
proofs/agda/EchoImageFactorizationPropPostulated.agda:3: inlinehypatia: allow code_safety/agda_postulatewith justification (commit ae7f8fb)docs/proof-debt.adoc:41: the postulate site is documented, with the zero-postulate--cubicaldischarge inEchoImageFactorizationPropCubical.agdatools/check-guardrails.sh:43: the module is guardrail-exemptedThe CSA004 dismissal is documented and justified in all three places the issue asked for.