security(hypatia): triage 42 scanner findings — critical 9→0

[hyperpolymath]

Hypatia scanner triage — critical 9 → 0

Reproduces and triages the full Hypatia 2.0 neurosymbolic scan of ephapax
(run locally with no GITHUB_TOKEN, default severity medium) and drives
critical findings to zero, with every disposition decided from the actual
source and the four-layer proof fence respected throughout.

Ground truth note: the local scan finds 42 findings
(9 critical / 7 high / 26 medium) — more than the 37/5/7/25 in the original
handoff (the prior session scanned a different checkout). This PR triages the
real 42. Branch is based on origin/main (the handoff's
claude/compassionate-mccarthy-xvwd6r exists nowhere; only main is on origin).

Result

	critical	high	medium	total
Before	9	7	26	42
After	0	3	23	26

cargo check (query/parser/wasm/interp/runtime) passes. Semantics.v is untouched (fence respected); the only formal/*.v edits are documentation comments.

Criticals (9 → 0)

Cluster	Finding	Disposition	What & why
C1	Semantics.v legacy preservation admit	.hypatia-ignore	Theorem is provably FALSE (Counterexample.v, 5 Qed lemmas); the Admitted. is deliberate + owner-fenced (CLAUDE.md 2026-05-27). Never closed/edited — path-exempted only.
C2	Semantics_L1.v admits (3 Admitted + 14 admit)	in-file hypatia: allow	Tracked v2 proof-debt (PROOF-NEEDS.md): region_liveness (false-as-stated), step_pop (open research), preservation_l1 (capstone). Documented, not closed.
C3	Counterexample_L2_nested.v admit/coq_admit	in-file hypatia: allow	False positive — scanner substring-matched prose ("No new Axiom or Admitted markers"); file is fully Qed-closed.
C4	parser/lib.rs unwrap_or(0) ×2	file-level directive + inline notes	Grammar integer = ASCII_DIGIT+ → parse() fails only on i64 overflow; fn returns Literal (no Result). Deliberate lossy fallback + TODO. (Downgraded from a ?-refactor that would have broken 2 uncovered call sites.)
C5	wasm/lib.rs unwrap_or(0)	file-level directive	0 is a benign sentinel (None ⇒ non-data scrutinee), routed correctly by the total >= 2 check.
C6	tools/linter.rs unwrap_or(0) ×8	file-level directive	line.find(&pat).unwrap_or(0)+1 = 1-based diagnostic column; 0⇒column 1 is benign. Tooling crate.
C7	lib/linter.rs unwrap_or(0) ×2	.hypatia-ignore	Stale 178-line duplicate of the live 920-line tools/linter.rs (not a workspace member). Same benign column idiom; flagged to owner for removal.

Highs & mediums — real fixes

Cluster	Fix
H6	query/lib.rs: removed 3 .get_mut(id).unwrap() via a behavior-preserving get_mut refactor.
H1	instant-sync.yml: step-level if: secrets.FARM_DISPATCH_TOKEN != '' presence gate.
H2	scorecard.yml: job-level security-events: write + id-token: write + contents: read (the reusable's required scopes; previously capped by the workflow-level contents: read).
M1	status-gate.yml (both jobs) + push-email-notify.yml: timeout-minutes.
M2	codeql.yml: added the actions language to the matrix.
H3/H7/M4	runtime from_raw, tokbuf.zig @ptrCast, interp unsafe/as_ptr: // SAFETY: justification comments (cleared 2 of 3 unsafe_block).
incidental	tokbuf.zig: added the owner-mandated MPL-2.0 SPDX/Owner header the repo pre-commit hook requires (the file lacked it).

Residual (26 — all triaged, none critical)

• from_raw ×2 (high), zig_ptr_cast (high), unsafe/as_ptr (med): accepted FFI/unsafe, now documented with // SAFETY: comments. (See FFI-proof follow-up below.)
• expect_in_hot_path ×8 (med): accepted parser/typing grammar invariants (expect() on by-construction-unreachable cases).
• SD022 ×7 / SD009 ×4 (med): doc-drift to pre-restructure paths, and missing SPDX on legacy src/*.ml. Declared in .hypatia-ignore + flagged to owner (SPDX edits are owner-gated; no auto-licence-edit). ⚠️ These remain visible because the current scanner emits structural_drift findings without routing them through ScannerSuppression — see follow-up.
• git_state GS001/GS007 (med): environmental (unstaged-tree state, which clears on commit; remote-branch-count policy).

Two Hypatia scanner gaps found (worth upstream issues)

1. structural_drift / git_state bypass ScannerSuppression (cli.ex emits them directly), so .hypatia-ignore and inline directives can't suppress SD009/SD022/GS* — inconsistent with code_safety.
2. secret_action_without_presence_gate (WF017) only recognizes a step-level if: gate, not a functionally-equivalent job-level one.

FFI follow-up (answers a parallel question)

boj/boj-server has a reusable zig↔idris safety framework directly applicable here:
ffi/zig/src/seams.zig (32-test integration-contract harness, template-ready for tokbuf.zig),
src/abi/Boj/SafetyLemmas.idr (allRec lemma family), and the docs/proof-debt.md +
docs/backend-assurance/ axiom + external-validation methodology — the principled path to
retire the @ptrCast/from_raw findings via proof rather than suppression.

🤖 Generated with Claude Code

[github-advanced-security]

You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool.

What Enabling Code Scanning Means:

• The 'Security' tab will display more code scanning analysis results (e.g., for the default branch).
• Depending on your configuration and choice of analysis tool, future pull requests will be annotated with code scanning analysis results.
• You will be able to see the analysis results for the pull request's branch on this overview once the scans have completed and the checks have passed.

For more information about GitHub Code Scanning, check out the documentation.