ci(architecture-enforcement): safe_*.rs filename check rejects legitimate FFI wrappers #11

Problem

architecture-enforcement.yml's enforce-idris-only job bans every file named bindings/rust/src/safe_*.rs:

if ls bindings/rust/src/safe_*.rs 1> /dev/null 2>&1; then
  echo "❌ ERROR: safe_*.rs files found in Rust bindings"
  echo "These are reimplementations that bypass Idris2 verification"
  …
  exit 1
fi

There are currently 41 such files in the repo. The check has been failing on main since at least 2026-03-29 (the entire history of the workflow on main is red on this step).

Why the rule is too broad

The README convention for this repo names FFI wrapper files safe_<topic>.rs because they wrap Proven.Safe<Topic> Idris modules. The wrappers themselves are pure FFI shims — for example safe_angle.rs:

pub fn deg_to_rad(degrees: Degrees) -> Radians {
    // SAFETY: proven_angle_deg_to_rad takes a value-type f64;
    // always safe to call.
    unsafe { ffi::proven_angle_deg_to_rad(degrees) }
}

That's exactly what the workflow's own SOLUTION text says is allowed: "Bindings should ONLY contain FFI wrappers calling Zig bridge." The check is rejecting them anyway because of the filename.

Proposed fixes

Three options, listed cheapest first:

Option 1 — Drop the filename check, keep the body check

The job already has a second step that bans .unwrap() in Rust bindings (which is a body check). Extend that step instead of using the filename heuristic. Something like:

# Reject any safe_*.rs file that contains a non-FFI function body —
# i.e. anything other than a single `unsafe { ffi::… }` line or the
# trivial wrappers, modulo doc comments and use statements.

This needs a real grammar check or at least a careful regex — easy to get wrong. But it would catch real reimplementations without flagging legitimate wrappers.

Option 2 — Allowlist via repo metadata

Add an explicit list of files known to be FFI wrappers (e.g. in .github/architecture/safe-rs-allowlist.txt). The job fails only on files not on the list. New safe_*.rs files require a one-line PR addition. Forces conscious decisions but adds friction.

Option 3 — Replace the filename check with a body-shape assertion

Require every safe_*.rs file to be < N lines OR consist exclusively of unsafe { ffi::… } function bodies. Spirit of the original rule (no real logic in bindings) without the filename trap.

Recommendation

Option 1 or 3 — they don't require maintaining an allowlist.

Out of scope here

This issue is about the workflow rule, not about the binding files themselves. Deleting safe_*.rs (the workflow's own SOLUTION text) is not on the table without a separate decision because every published binding crate currently depends on them.

Background

Surfaced while triaging CI failures admin-bypassed on #9 / #10 (the 6-week CI rot). See PR #10 for the related cache / install fixes.