REQ-70 file family: do not route — the gap is a security bypass

[ib823]

Summary

Investigated the file family and deliberately did not route it. The json precedent held — the 8 riina_builtin_fail_* C functions exist and have never executed — but the reason they must not simply be wired up is different in kind from the correctness divergences json, masa, simpan and net produced.

The finding

builtins::fail does not touch the host filesystem directly. All eight builtins first call gate_read / gate_write / gate_delete, which evaluate the Coq-modeled can_read / can_write predicates against an inode model (owner uid/gid, mode 0644 on first touch) and the AccessContext set by vfs_jadi_pengguna.

	gating constructs
builtins/fail.rs — gate_read/gate_write/gate_delete	12 call sites
emit.rs, all 8 helpers — gate/can_read/can_write/denied/permission/inode/owner	0

fail_baca is a bare fopen; fail_tulis a bare fwrite.

So adding a fail/vfs arm to builtin_canonical would mean riinac run denies an access that riinac build permits — the compiler becomes the way around a verified security check. That is REQ-27 enforcement parity failing in the direction that matters.

Measured on the interpreter:

uid 1 writes /tmp/owned.txt       -> ok, file contains "alice-data"
uid 2 writes the same 0644 file   -> Runtime Error: permission denied
                                     (verified can_write is false for the
                                     current uid), file unchanged

Prerequisite for routing, recorded in the REQ-70 row

Port the inode model, the uid/gid context, and the two predicates into the emitted runtime — then route fail and vfs together. vfs has no C helpers at all today, so routing it alone fails in the C compiler.

What this PR adds

crates/riinac/tests/file_gate_parity.rs, written as an invariant rather than a "stays unrouted" pin:

a compiled binary must not perform an access the interpreter refuses

• Today — unrouted, so no binary exists; holds vacuously.
• After a correct gate port — build succeeds and the binary refuses the write; still passes.
• If someone routes without porting — the binary overwrites the file and this fails, which is exactly when someone needs stopping.

It therefore never has to be deleted to make progress. That shape is deliberate: my earlier masa exclusion used a "stays unrouted" pin, and #70 had to remove it when it resolved the semantics properly. An invariant does not create that friction.

Honest limitation

The SECURITY REGRESSION branch is reviewed but UNEXECUTED. Reaching it needs a compiled binary that switches uid and then writes, which cannot be built today: emit.rs has no riina_builtin_vfs_* functions, so routing vfs emits C that does not compile.

Two controls were run, and both correctly held vacuously:

1. routing fail alone — no way to switch uid, so no bypass is expressible;
2. routing fail + vfs — fails in the C compiler.

The assertion is verified in its vacuous arm and acquires teeth exactly when someone writes the vfs C helpers, which is the moment the bypass becomes shippable. Stated in the test's own docs too, not just here.

Type

• Bug fix
• New feature
• Documentation
• Example .rii file
• Formal proof
• Refactor
• Test / guard for a known gap

Testing

• cargo test --all (03_PROTO): 3323/0 (+1)
• cargo clippy --all-targets -- -D warnings clean
• audit-docs.sh 0 discrepancies
• New test added — file_gate_parity.rs

Checklist

• No external dependencies added
• No new unsafe
• No Admitted in Coq proofs (no proof changes)
• Examples use Bahasa Melayu keywords (no example changes)

Note

Four families have now been routed (json, masa, simpan, net) and every one exposed a defect the "lowers to C" Backend column hid. This is the fifth, and the first where the hidden defect is a security property rather than a wrong answer — which suggests keselamatan (42 security sinks, still unrouted) deserves the same look before anyone routes it.

---

Generated by Claude Code