docs(audits): FFI boundary §§9-11 (FLINT + Zig bridges + Zig overlay) — closes #177

[hyperpolymath]

Summary

Closes #177 (post-#104 panic-attack re-sweep — 6 new legitimate-FFI High findings need audit + classification).

Extends reports/audits/audit-ffi-boundary.md with three new sections and adds 6 matching entries to reports/audits/assail-classifications.a2ml.

audits/audit-ffi-boundary.md

• §9 — src/rust/coprocessor/flint.rs (UnsafeCode × 17): FLINT C bigint library FFI (feature-gated --features flint). Documents the 4 unsafe-block patterns (RAII init/clear, string round-trip via fmpz_set_str/get_str + flint_free, fmpz_poly arithmetic, integer root/binomial), the #[repr(C)] layout invariants for FmpzPolyStruct, and the blocking-thread-only ownership model.
• §10 — Zig FFI bridges:
  • §10.1 src/zig/ffi/axiom_spark_bridge.zig (Ada/SPARK → Zig shim → Rust extern "C" in spark_axiom.rs, §2)
  • §10.2 src/zig_ffi/chapel_bridge.zig (Chapel C API → Zig @cImport → Rust safe-call layer in proof_search.rs, §3)
  • Documents the @cImport intent + enum-from-int bounds check + owned-string-copy invariants.
• §11 — ffi/zig/src/ overlay (UnsafeCode × 3): three identical echidna_<subsystem>_last_error() functions in boj.zig, overlay.zig, typell.zig that @ptrCast a module-static error_buf [N]u8 to [*:0]const u8. Documents the static-lifetime + nul-terminator + null-fast-path + read-only contract invariants.

reports/audits/assail-classifications.a2ml

Adds 6 classification entries cross-referencing §§9-11:

File	Category	Audit ref
src/rust/coprocessor/flint.rs	UnsafeCode	§9
src/zig/ffi/axiom_spark_bridge.zig	UnsafeFFI	§10.1
src/zig_ffi/chapel_bridge.zig	UnsafeFFI	§10.2
ffi/zig/src/boj.zig	UnsafeCode	§11
ffi/zig/src/overlay.zig	UnsafeCode	§11
ffi/zig/src/typell.zig	UnsafeCode	§11

Brings the total classification count from 16 → 22, covering all 6 new High-tier FFI findings reported by panic-attack v2.5.0 on 2026-06-01.

Out-of-scope observation (meander)

The panic-attack registry loader (load_user_classifications in panic-attack/src/assail/mod.rs:220) reads from <project>/audits/assail-classifications.a2ml or <project>/.panic-attack-classifications.a2ml, but this repo keeps the registry at reports/audits/. This means the registry entries (both pre-existing and these new ones) do not currently flip findings to suppressed = true in panic-attack output — the kanren structural-suppression pass is what suppresses today. Out-of-scope for this PR; can be addressed by either a one-line symlink (audits → reports/audits) or moving the file. Filing separately if desired.

Test plan

• audits/audit-ffi-boundary.md §§9-11 follow the established §1-§8 format (header + boundary description + invariants list + classification verdict).
• All 6 new classification entries are syntactically consistent with the existing 16 (s-expr form, (file …) + (category …) + (audit …) + (rationale …)).
• GPG-signed commit (key 4A03639C…).
• Auto-merge SQUASH armed post-CI.

🤖 Discovered + audited during the post-#104 panic-attack estate sweep (2026-06-01). See hyperpolymath/panic-attack#32 for campaign tracker.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 246 issues detected

Severity	Count
🔴 Critical	12
🟠 High	75
🟡 Medium	159

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in agda-meta-checker.yml",
    "type": "missing_timeout_minutes",
    "file": "agda-meta-checker.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cargo-audit.yml",
    "type": "missing_timeout_minutes",
    "file": "cargo-audit.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in chapel-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "chapel-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence