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

## 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](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/codeql.yml

@@ -33,6 +33,8 @@ jobs:
         include:
           - language: javascript-typescript
             build-mode: none
+          - language: actions
+            build-mode: none
 
     steps:
       - name: Checkout

.github/workflows/instant-sync.yml

@@ -21,6 +21,7 @@ jobs:
     timeout-minutes: 5
     steps:
       - name: Trigger Propagation
+        if: ${{ secrets.FARM_DISPATCH_TOKEN != '' }}
         uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3
         with:
           token: ${{ secrets.FARM_DISPATCH_TOKEN }}

.github/workflows/push-email-notify.yml

@@ -13,6 +13,7 @@ jobs:
     name: Email on push
     if: ${{ vars.PUSH_EMAIL_ENABLED == 'true' }}
     runs-on: ubuntu-latest
+    timeout-minutes: 5
     steps:
       - name: Send push notification email
         uses: dawidd6/action-send-mail@6e502825a508b867ab2954ad6343b68787624c01 # pinned

.github/workflows/scorecard.yml

@@ -13,4 +13,8 @@ permissions:
 
 jobs:
   scorecard:
+    permissions:
+      contents: read
+      security-events: write
+      id-token: write
     uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236

.github/workflows/status-gate.yml

@@ -38,6 +38,7 @@ jobs:
   status-gate-core:
     name: status-gate-core
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - name: Checkout repository
         uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
@@ -49,6 +50,7 @@ jobs:
   status-gate-tests:
     name: status-gate-tests (slow · cancellable)
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - name: Notice — this is the slow, skippable job
         run: |

.hypatia-ignore

@@ -30,3 +30,47 @@
 cicd_rules/banned_language_file:formal/Makefile.coq
 cicd_rules/banned_language_file:formal/Makefile.coq.conf
 cicd_rules/banned_language_file:formal/Makefile.conf
+
+# ─── Coq proof archaeology — legacy preservation admit (2026-06-24 triage) ─────
+#
+# formal/Semantics.v carries the LEGACY `preservation` Theorem (declared :8556),
+# closed with a DELIBERATE `Admitted.` (:9258). The theorem is provably FALSE —
+# formal/Counterexample.v discharges its falsity with 5 Qed lemmas — so the admit
+# is owner-mandated (CLAUDE.md 2026-05-27 fence + in-file ARCHAEOLOGY/DO-NOT-EXTEND
+# banner). It must never be "fixed"; the principled work is the four-layer redesign
+# in formal/PRESERVATION-DESIGN.md (preservation re-derived per layer). File-scoped:
+# the whole file is fenced legacy archaeology where any admit re-detection is the
+# same accepted non-defect. (Semantics_L1.v / Counterexample_L2_nested.v admits are
+# handled by in-file `hypatia: allow` directives, not here.)
+code_safety/admitted:formal/Semantics.v
+
+# ─── Stale duplicate linter (lib/linter.rs) ────────────────────────────────────
+#
+# lib/linter.rs (178 lines) is a stale/legacy sibling of the live
+# src/ephapax-tools/src/linter.rs (920 lines). Its two `line.find(..).unwrap_or(0)+1`
+# sites compute 1-based diagnostic columns; 0 is a benign "column 1" default, not a
+# masked fault. Exempted pending an owner decision on whether to remove the duplicate.
+code_safety/unwrap_dangerous_default:lib/linter.rs
+
+# ─── SD009: legacy OCaml files without SPDX headers (src/*.ml) ──────────────────
+#
+# src/{lexer,parser,ast,typecheck}.ml are legacy OCaml artefacts in a Rust/Coq/Idris
+# project (the live type checker is Rust). Adding licence headers is an SPDX edit,
+# which estate policy reserves for the owner (no-automated-licence-edits). Flag-only:
+# exempted here and surfaced to the owner — these are also candidates for removal.
+structural_drift/SD009:src/lexer.ml
+structural_drift/SD009:src/parser.ml
+structural_drift/SD009:src/ast.ml
+structural_drift/SD009:src/typecheck.ml
+
+# ─── SD022: doc references to pre-restructure directories (deferred doc refresh) ─
+#
+# EXPLAINME/README/ROADMAP.adoc + tests/fuzz/FUZZING_GUIDE.md reference dirs
+# (src/core, src/Burble, src/Ephapax, src/parse_fuzzer, src/typecheck_fuzzer) that
+# predate the move to the `src/ephapax-*` cargo workspace. This is real (deferred)
+# doc-drift, not a false positive; exempted pending an owner doc-refresh
+# (prose = CC-BY-SA-4.0, not auto-edited in this security-triage PR).
+structural_drift/SD022:EXPLAINME.adoc
+structural_drift/SD022:README.adoc
+structural_drift/SD022:ROADMAP.adoc
+structural_drift/SD022:tests/fuzz/FUZZING_GUIDE.md

formal/Counterexample_L2_nested.v

@@ -1,6 +1,8 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
 (* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
+(* hypatia: allow code_safety/admitted -- FALSE POSITIVE: this file has no Coq admit/Admitted/Axiom; all proofs are Qed-closed. The scanner substring-matched prose in the doc comment that NEGATES their presence ("No new [Axiom] or [Admitted] markers"). *)
+(* hypatia: allow coq_admit_tactic -- same false positive: substring match on documentation prose, not a Coq tactic. *)
 
 (** * Soundness gap (L2): preservation_l2 fails for nested-TFunEff
       substituends — the gap Phase 3b Stage 1's [tfuneff_lambda_free]

formal/Semantics_L1.v

@@ -1,6 +1,9 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
+(* hypatia: allow code_safety/admitted -- TRACKED v2 proof-debt, not an honest-completion gap. The 3 Admitted lemmas (region_liveness_at_split_l1_gen, step_pop_disjoint_from_type_l1, preservation_l1) and their internal `admit.` tactics are documented in PROOF-NEEDS.md and owner-fenced by CLAUDE.md (directive 2026-05-27): closing or extending them is a banned anti-pattern. region_liveness is provably FALSE as stated; step_pop is open eliminator-fork research; preservation_l1 is the capstone gated on the others. Build truth is the `Print Assumptions` CI gate, not this comment. *)
+(* hypatia: allow coq_admit_tactic -- see preceding directive; same tracked admits. *)
+
 (**
 
   *********************************************************************

idris2/ffi/zig/tokbuf.zig

@@ -1,3 +1,7 @@
+// SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
 const std = @import("std");
 
 const Tok = struct {
@@ -85,6 +89,13 @@ export fn eph_tokbuf_str_ptr(buf: *TokBuf, idx: i32) [*:0]const u8 {
     const i = @as(usize, @intCast(idx));
     const t = buf.items[i];
     if (t.str_ptr) |p| {
+        // SAFETY: p is [*]u8 (align 1); cast to the [*:0]const u8 return
+        // type is alignment- and provenance-preserving and only narrows
+        // mutability (adds const). The :0 sentinel is upheld by the
+        // producer copyStr (allocates len+1 and writes a trailing NUL) and
+        // required by the consumer (Idris FFI binds this to `String`, which
+        // reads a NUL-terminated C string). The cast asserts, not checks,
+        // the sentinel; the invariant is guaranteed at the copyStr seam.
         return @ptrCast(p);
     }
     return "";

src/ephapax-interp/src/lib.rs

@@ -357,6 +357,10 @@ impl Interpreter {
     /// Loading shared libraries is inherently unsafe. The caller must
     /// ensure the library is trustworthy.
     pub fn load_ffi_library(&mut self, path: &str) -> Result<(), RuntimeError> {
+        // SAFETY: Loading a shared library is unsafe because the loaded code
+        // is unverified; caller trust is documented in this fn's `# Safety`
+        // section. The handle is stored in `self.ffi_libraries` and kept alive
+        // until the interpreter is dropped, so no symbol outlives its library.
         let lib = unsafe {
             libloading::Library::new(path).map_err(|e| {
                 RuntimeError::Unimplemented(format!("Failed to load FFI library '{}': {}", path, e))
@@ -373,6 +377,9 @@ impl Interpreter {
     ) -> Option<libloading::Symbol<'a, unsafe extern "C" fn(i64, i64, i64, i64, i64, i64) -> i64>>
     {
         for lib in &self.ffi_libraries {
+            // SAFETY: `lib` is a live, owned library handle borrowed from
+            // `self.ffi_libraries` for `'a`; the returned Symbol is tied to that
+            // borrow, so it cannot outlive the library it was resolved from.
             if let Ok(sym) = unsafe { lib.get(name.as_bytes()) } {
                 return Some(sym);
             }
@@ -533,6 +540,11 @@ impl Interpreter {
                 if let Some(func) = self.find_ffi_symbol(symbol) {
                     // Pad args to 6 (max C ABI args we support)
                     let a = |i: usize| *c_args.get(i).unwrap_or(&0);
+                    // SAFETY: `func` was resolved via find_ffi_symbol from a
+                    // loaded library to the 6-arg i64 C-ABI signature it is
+                    // called with here; args are padded to 6 so all params are
+                    // supplied. Soundness ultimately rests on the caller having
+                    // loaded a trustworthy library (see load_ffi_library).
                     let result = unsafe { func(a(0), a(1), a(2), a(3), a(4), a(5)) };
                     Ok(Value::I64(result))
                 } else {
@@ -1233,6 +1245,10 @@ impl Interpreter {
                 // until the FFI call completes.
                 match std::ffi::CString::new(data.as_str()) {
                     Ok(cstr) => {
+                        // SAFETY: the raw pointer stays valid because `cstr` is
+                        // immediately moved into `cstrings` (kept alive until the
+                        // FFI call completes) on the next line, so `ptr` never
+                        // dangles for the duration of its use.
                         let ptr = cstr.as_ptr() as i64;
                         cstrings.push(cstr);
                         ptr