diff --git a/03_PROTO/crates/riina-codegen/src/emit.rs b/03_PROTO/crates/riina-codegen/src/emit.rs index a56e3fb2..966566af 100644 --- a/03_PROTO/crates/riina-codegen/src/emit.rs +++ b/03_PROTO/crates/riina-codegen/src/emit.rs @@ -3267,9 +3267,143 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln("#include "); self.writeln(""); + // ═══════════════════════════════════════════════════════════════════ + // VERIFIED FILE GATE + // ═══════════════════════════════════════════════════════════════════ + // + // The interpreter never touches the host filesystem directly: every + // `fail_*` builtin first calls gate_read/gate_write/gate_delete, which + // evaluate the Coq `can_read`/`can_write` predicates. Emitted C used to + // have none of that — bare fopen/fwrite — so compiling a program was a + // way around a verified security check (REQ-70/REQ-27). This is the + // gate, mirrored. + // + // ONE SPECIFICATION, TWO IMPLEMENTATIONS. The spec is Coq + // `domains/VerifiedFileSystem.v` (Inode / Ownership / Permission / + // is_owner / get_permission); `riina-os/src/vfs.rs` is the Rust + // implementation and this is the C one. They cannot share code — the + // compile pipeline is `cc -o out one.c` with nothing linked, so a + // single implementation callable from both would mean shipping a + // per-target Rust staticlib. The same shape as the `masa` civil + // calendar (REQ-70) and the GF128/AES Coq⇄Rust equivalences: two + // implementations of one model, held together by a differential — + // here `file_gate_parity.rs` plus `file_differential.rs`. + // + // Deliberately NOT the host OS's own permission bits. The gate is + // RIINA's model, so it must deny where the model denies even when the + // host would allow (the process typically owns these files); letting + // the kernel decide would silently make the check a no-op. + self.writeln("typedef struct { bool read; bool write; bool execute; } riina_perm_t;"); + self.writeln("typedef struct riina_inode_s {"); + self.writeln(" char* path;"); + self.writeln(" uint64_t owner_uid;"); + self.writeln(" uint64_t owner_gid;"); + self.writeln(" riina_perm_t perm_owner;"); + self.writeln(" riina_perm_t perm_group;"); + self.writeln(" riina_perm_t perm_other;"); + self.writeln(" struct riina_inode_s* next;"); + self.writeln("} riina_inode_t;"); + self.writeln(""); + // `ctx_for(uid)` in builtins/vfs.rs yields { uid, gid: uid, + // groups: [uid], is_root: false }, and DEFAULT_UID is 1000. Supplementary + // groups are therefore always exactly [gid] today; `in_group` below is + // written in the general form anyway so it still matches the model if + // that changes. + self.writeln("static uint64_t riina_ctx_uid = 1000;"); + self.writeln("static uint64_t riina_ctx_gid = 1000;"); + self.writeln("static bool riina_ctx_is_root = false;"); + self.writeln("static riina_inode_t* riina_inodes = NULL;"); + self.writeln(""); + // First touch registers the path owned by the CURRENT uid at mode 0644, + // matching the interpreter's HostGate::gate and the modes vfs_tulis + // creates with (owner rw, group/other r). + self.writeln("static riina_inode_t* riina_gate_touch(const char* path) {"); + self.writeln(" for (riina_inode_t* i = riina_inodes; i; i = i->next) {"); + self.writeln(" if (strcmp(i->path, path) == 0) return i;"); + self.writeln(" }"); + self.writeln(" riina_inode_t* ino = (riina_inode_t*)malloc(sizeof(riina_inode_t));"); + self.writeln(" if (!ino) abort();"); + self.writeln(" ino->path = strdup(path);"); + self.writeln(" if (!ino->path) abort();"); + self.writeln(" ino->owner_uid = riina_ctx_uid;"); + self.writeln(" ino->owner_gid = riina_ctx_gid;"); + self.writeln(" ino->perm_owner = (riina_perm_t){ true, true, false };"); + self.writeln(" ino->perm_group = (riina_perm_t){ true, false, false };"); + self.writeln(" ino->perm_other = (riina_perm_t){ true, false, false };"); + self.writeln(" ino->next = riina_inodes;"); + self.writeln(" riina_inodes = ino;"); + self.writeln(" return ino;"); + self.writeln("}"); + self.writeln(""); + // Coq `get_permission` — owner > group > other resolution order. + self.writeln("static riina_perm_t riina_permission_for(const riina_inode_t* ino) {"); + self.writeln(" if (ino->owner_uid == riina_ctx_uid) return ino->perm_owner;"); + self.writeln(" if (ino->owner_gid == riina_ctx_gid) return ino->perm_group;"); + self.writeln(" return ino->perm_other;"); + self.writeln("}"); + self.writeln(""); + // Coq `can_read` / `can_write` — root always, else the applicable bit. + // Denial exits non-zero with the interpreter's wording; it must not be + // possible for a denied op to fall through and touch the filesystem. + self.writeln("static void riina_gate(const char* op, const char* path, bool want_write) {"); + self.writeln(" riina_inode_t* ino = riina_gate_touch(path);"); + self.writeln(" riina_perm_t p = riina_permission_for(ino);"); + self.writeln(" bool ok = riina_ctx_is_root || (want_write ? p.write : p.read);"); + self.writeln(" if (!ok) {"); + self.writeln(" fprintf(stderr, \"RIINA: %s: '%s': permission denied (verified %s is false for the current uid)\\n\","); + self.writeln(" op, path, want_write ? \"can_write\" : \"can_read\");"); + self.writeln(" exit(1);"); + self.writeln(" }"); + self.writeln("}"); + self.writeln(""); + // gate_delete: gate_write, then drop the mapping so a re-created file is + // owned by whoever re-creates it (VFS delete-then-create semantics). + self.writeln("static void riina_gate_delete(const char* op, const char* path) {"); + self.writeln(" riina_gate(op, path, true);"); + self.writeln(" riina_inode_t** slot = &riina_inodes;"); + self.writeln(" while (*slot) {"); + self.writeln(" if (strcmp((*slot)->path, path) == 0) {"); + self.writeln(" riina_inode_t* dead = *slot;"); + self.writeln(" *slot = dead->next;"); + self.writeln(" free(dead->path);"); + self.writeln(" free(dead);"); + self.writeln(" return;"); + self.writeln(" }"); + self.writeln(" slot = &(*slot)->next;"); + self.writeln(" }"); + self.writeln("}"); + self.writeln(""); + // vfs_mula (vfs_init): resets the gate. The quota argument is accepted + // and ignored here — quota accounting belongs to the in-memory + // VirtualFs, which is not routed to C (vfs_tulis/baca/padam stay + // interpreter-only), so honouring it would be a claim this backend + // cannot make. + self.writeln("static riina_value_t* riina_builtin_vfs_mula(riina_value_t* arg) {"); + self.writeln(" (void)arg;"); + self.writeln(" while (riina_inodes) {"); + self.writeln(" riina_inode_t* dead = riina_inodes;"); + self.writeln(" riina_inodes = dead->next;"); + self.writeln(" free(dead->path);"); + self.writeln(" free(dead);"); + self.writeln(" }"); + self.writeln(" riina_ctx_uid = 1000; riina_ctx_gid = 1000; riina_ctx_is_root = false;"); + self.writeln(" return riina_unit();"); + self.writeln("}"); + self.writeln(""); + // vfs_jadi_pengguna (vfs_become_user): mirrors ctx_for(uid). + self.writeln("static riina_value_t* riina_builtin_vfs_jadi_pengguna(riina_value_t* arg) {"); + self.writeln(" if (arg->tag != RIINA_TAG_INT) abort();"); + self.writeln(" riina_ctx_uid = arg->data.int_val;"); + self.writeln(" riina_ctx_gid = arg->data.int_val;"); + self.writeln(" riina_ctx_is_root = false;"); + self.writeln(" return riina_unit();"); + self.writeln("}"); + self.writeln(""); + // fail_baca (file_read): Teks -> Teks self.writeln("static riina_value_t* riina_builtin_fail_baca(riina_value_t* arg) {"); self.writeln(" if (arg->tag != RIINA_TAG_STRING) abort();"); + self.writeln(" riina_gate(\"fail_baca\", arg->data.string_val.data, false);"); self.writeln(" FILE* f = fopen(arg->data.string_val.data, \"r\");"); self.writeln(" if (!f) { fprintf(stderr, \"RIINA: cannot open file '%s'\\n\", arg->data.string_val.data); abort(); }"); self.writeln(" fseek(f, 0, SEEK_END);"); @@ -3291,6 +3425,8 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln(" if (arg->tag != RIINA_TAG_PAIR) abort();"); self.writeln(" riina_value_t* path = arg->data.pair_val.fst;"); self.writeln(" riina_value_t* content = arg->data.pair_val.snd;"); + self.writeln(" if (path->tag != RIINA_TAG_STRING) abort();"); + self.writeln(" riina_gate(\"fail_tulis\", path->data.string_val.data, true);"); self.writeln( " if (path->tag != RIINA_TAG_STRING || content->tag != RIINA_TAG_STRING) abort();", ); @@ -3309,6 +3445,8 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln(" if (arg->tag != RIINA_TAG_PAIR) abort();"); self.writeln(" riina_value_t* path = arg->data.pair_val.fst;"); self.writeln(" riina_value_t* content = arg->data.pair_val.snd;"); + self.writeln(" if (path->tag != RIINA_TAG_STRING) abort();"); + self.writeln(" riina_gate(\"fail_tambah\", path->data.string_val.data, true);"); self.writeln( " if (path->tag != RIINA_TAG_STRING || content->tag != RIINA_TAG_STRING) abort();", ); @@ -3332,6 +3470,7 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { // fail_buang (file_delete): Teks -> Bool self.writeln("static riina_value_t* riina_builtin_fail_buang(riina_value_t* arg) {"); self.writeln(" if (arg->tag != RIINA_TAG_STRING) abort();"); + self.writeln(" riina_gate_delete(\"fail_buang\", arg->data.string_val.data);"); self.writeln(" return riina_bool(remove(arg->data.string_val.data) == 0);"); self.writeln("}"); self.writeln(""); @@ -3339,6 +3478,7 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { // fail_panjang (file_size): Teks -> Int self.writeln("static riina_value_t* riina_builtin_fail_panjang(riina_value_t* arg) {"); self.writeln(" if (arg->tag != RIINA_TAG_STRING) abort();"); + self.writeln(" riina_gate(\"fail_panjang\", arg->data.string_val.data, false);"); self.writeln(" struct stat st;"); self.writeln(" if (stat(arg->data.string_val.data, &st) != 0) { fprintf(stderr, \"RIINA: cannot stat '%s'\\n\", arg->data.string_val.data); abort(); }"); self.writeln(" return riina_int((uint64_t)st.st_size);"); @@ -3364,6 +3504,7 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { // fail_baca_baris (file_read_lines): Teks -> List self.writeln("static riina_value_t* riina_builtin_fail_baca_baris(riina_value_t* arg) {"); self.writeln(" if (arg->tag != RIINA_TAG_STRING) abort();"); + self.writeln(" riina_gate(\"fail_baca_baris\", arg->data.string_val.data, false);"); self.writeln(" FILE* f = fopen(arg->data.string_val.data, \"r\");"); self.writeln(" if (!f) { fprintf(stderr, \"RIINA: cannot open '%s'\\n\", arg->data.string_val.data); abort(); }"); self.writeln(" riina_list_t nl = riina_list_new();"); diff --git a/03_PROTO/crates/riina-codegen/src/lower.rs b/03_PROTO/crates/riina-codegen/src/lower.rs index 59bca93f..5088274e 100644 --- a/03_PROTO/crates/riina-codegen/src/lower.rs +++ b/03_PROTO/crates/riina-codegen/src/lower.rs @@ -151,6 +151,32 @@ pub(crate) fn builtin_canonical(name: &str) -> Option<&'static str> { return Some(canonical); } } + // File builtins (REQ-70 family routing) — routed ONLY because the emitted + // C now carries the verified gate. + // + // These were held back deliberately: the interpreter runs every `fail_*` + // through gate_read/gate_write/gate_delete (the Coq can_read/can_write + // predicates), and the C helpers were bare fopen/fwrite, so routing them + // would have made `riinac build` a way around a security check that + // `riinac run` enforces. `emit.rs` now mirrors the gate — inode table, + // first-touch ownership at mode 0644, owner > group > other resolution — + // and `file_gate_parity.rs` fails if a compiled binary ever performs an + // access the interpreter refuses. + for &(bm, en, canonical) in builtins::fail::BUILTINS { + if name == bm || name == en { + return Some(canonical); + } + } + // Only the two VFS context setters route: they are what makes the gate + // meaningful (`vfs_jadi_pengguna` switches uid). `vfs_tulis`/`vfs_baca`/ + // `vfs_padam` operate on the in-memory VirtualFs with quota accounting, + // which has no C implementation, so they stay interpreter-only rather than + // being stubbed into something that silently ignores the quota. + match name { + "vfs_mula" | "vfs_init" => return Some("vfs_mula"), + "vfs_jadi_pengguna" | "vfs_become_user" => return Some("vfs_jadi_pengguna"), + _ => {} + } // JSON builtins (REQ-70 family routing). Pure value transformations — no // syscalls — so the C backend can implement them outright. The C helpers // (`riina_builtin_json_*`) already existed in `emit.rs` but were diff --git a/03_PROTO/crates/riinac/tests/file_differential.rs b/03_PROTO/crates/riinac/tests/file_differential.rs new file mode 100644 index 00000000..d075b3e3 --- /dev/null +++ b/03_PROTO/crates/riinac/tests/file_differential.rs @@ -0,0 +1,267 @@ +// Copyright (c) 2026 The RIINA Authors. All rights reserved. + +//! Interpreter/C differential for the file (`fail`) family — master plan +//! REQ-70 family routing. +//! +//! # What makes this family different from the others +//! +//! `json`, `masa`, `simpan` and `net` were routed to fix *correctness* +//! divergences. This family was held back because its divergence was a +//! **security** one: every `fail_*` builtin runs through +//! `gate_read`/`gate_write`/`gate_delete` in the interpreter — the Coq +//! `can_read`/`can_write` predicates over an inode model — and the emitted C +//! had none of it. Routing it before the gate existed would have made +//! `riinac build` a way around a check `riinac run` enforces. +//! +//! `file_gate_parity.rs` holds the invariant (a compiled binary must not +//! perform an access the interpreter refuses). This file checks that the two +//! implementations of the gate *agree in detail*, which is the discipline that +//! keeps them from drifting: the C gate mirrors +//! `domains/VerifiedFileSystem.v` / `riina-os/src/vfs.rs`, and they cannot +//! share code because the compile pipeline is `cc -o out one.c` with nothing +//! linked. +//! +//! # Cases chosen to pin the resolution order +//! +//! First touch registers a path owned by the current uid at mode 0644 — owner +//! `rw`, group and other `r`. So the interesting boundaries are: the owner may +//! write, a non-owner may read but NOT write, and a delete drops the mapping +//! so whoever re-creates the file owns it. Each is a different arm of +//! `get_permission`'s owner ▷ group ▷ other resolution, and a C gate that +//! collapsed them (say, by always consulting `perm_owner`) would pass a +//! naive same-uid test and fail these. + +use std::path::PathBuf; +use std::process::Command; + +fn tool_available(tool: &str) -> bool { + Command::new(tool) + .arg("--version") + .output() + .map(|o| o.status.success()) + .unwrap_or(false) +} + +/// A missing `cc` PANICS by default — a test that cannot run must never report +/// `ok`. Opt out deliberately with `RIINA_ALLOW_MISSING_BACKEND_TOOLS=1`. +fn require_cc() -> bool { + if tool_available("cc") { + return true; + } + if std::env::var("RIINA_ALLOW_MISSING_BACKEND_TOOLS").is_ok() { + eprintln!("!!! SKIPPED (cc missing) — file differential NOT exercised."); + return false; + } + panic!( + "cc is required: this test cannot compare the backends without it, so it \ + fails rather than reporting a false pass. Set \ + RIINA_ALLOW_MISSING_BACKEND_TOOLS=1 to skip deliberately." + ); +} + +struct Sandbox { + dir: PathBuf, + stem: String, +} + +impl Sandbox { + fn new(tag: &str) -> Self { + let stem = format!("req70_file_{tag}"); + let dir = std::env::temp_dir().join(format!("riina_{stem}_{}", std::process::id())); + let _ = std::fs::remove_dir_all(&dir); + std::fs::create_dir_all(&dir).expect("create sandbox"); + Self { dir, stem } + } +} + +impl Drop for Sandbox { + fn drop(&mut self) { + let _ = std::fs::remove_dir_all(&self.dir); + } +} + +/// Build the program with `{}` replaced by a backend-private target path, run +/// it under both backends, and return (interpreter stdout, native stdout). +/// +/// Each backend gets its OWN target file: they run as separate processes and a +/// shared path would let one backend's writes be read by the other, which would +/// make an agreement look real when it was just leftover state. +fn run_both(tag: &str, body_tmpl: &str) -> (String, String) { + let sb = Sandbox::new(tag); + + let interp_target = sb.dir.join("t_interp.txt"); + let interp_src = sb.dir.join(format!("{}_i.rii", sb.stem)); + std::fs::write( + &interp_src, + format!( + "fungsi utama() -> Nombor kesan SistemFail {{\n{}\n 0\n}}\n", + body_tmpl.replace("{}", &interp_target.display().to_string()) + ), + ) + .expect("write interp program"); + + let out = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("run") + .arg(&interp_src) + .output() + .expect("riinac run"); + // A denial is an expected outcome here, so a non-zero exit is not asserted + // against — what is compared is the observable output up to that point. + let s = String::from_utf8_lossy(&out.stdout).into_owned(); + let mut lines: Vec<&str> = s.lines().collect(); + // `riinac run` appends the program's final value only on success. + if out.status.success() { + lines.pop(); + } + let interp = if lines.is_empty() { + String::new() + } else { + format!("{}\n", lines.join("\n")) + }; + + let native_target = sb.dir.join("t_native.txt"); + let native_src = sb.dir.join(format!("{}.rii", sb.stem)); + std::fs::write( + &native_src, + format!( + "fungsi utama() -> Nombor kesan SistemFail {{\n{}\n 0\n}}\n", + body_tmpl.replace("{}", &native_target.display().to_string()) + ), + ) + .expect("write native program"); + + let build = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("build") + .arg(&native_src) + .output() + .expect("riinac build"); + assert!( + build.status.success(), + "native build failed for {tag} — the fail family must route to codegen: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + let run = Command::new(sb.dir.join(&sb.stem)) + .output() + .expect("run native binary"); + let native = String::from_utf8_lossy(&run.stdout).into_owned(); + + (interp, native) +} + +fn assert_agree(tag: &str, body_tmpl: &str) { + if !require_cc() { + return; + } + let (interp, native) = run_both(tag, body_tmpl); + assert_eq!( + interp, native, + "interp/C divergence for {tag}\n interp: {interp:?}\n C: {native:?}" + ); +} + +/// The owner may read back what it wrote. The baseline round trip. +#[test] +fn owner_round_trip_agrees() { + assert_agree( + "owner", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"hello\"));\n\ + \x20 cetakln(fail_baca(\"{}\"));", + ); +} + +/// A NON-owner may read a 0644 file — the `perm_other.read` arm. If the C gate +/// consulted `perm_owner` for everyone this would still pass; the write case +/// below is what separates them. +#[test] +fn non_owner_read_is_allowed_and_agrees() { + assert_agree( + "otherread", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"owned-by-7\"));\n\ + \x20 biar d = vfs_jadi_pengguna(9);\n\ + \x20 cetakln(fail_baca(\"{}\"));", + ); +} + +/// A non-owner may NOT write — `perm_other.write` is false at 0644. Both +/// backends must stop here, so neither prints the line after the write. +#[test] +fn non_owner_write_is_denied_by_both() { + assert_agree( + "otherwrite", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"owned-by-7\"));\n\ + \x20 cetakln(\"before\");\n\ + \x20 biar d = vfs_jadi_pengguna(9);\n\ + \x20 biar e = fail_tulis((\"{}\", \"intruder\"));\n\ + \x20 cetakln(\"after\");", + ); +} + +/// Append is gated as a write, so a non-owner is refused there too. Pinned +/// separately because `fail_tambah` is a different call site from `fail_tulis` +/// and an unwired one would go unnoticed. +#[test] +fn non_owner_append_is_denied_by_both() { + assert_agree( + "otherappend", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"base\"));\n\ + \x20 cetakln(\"before\");\n\ + \x20 biar d = vfs_jadi_pengguna(9);\n\ + \x20 biar e = fail_tambah((\"{}\", \"-more\"));\n\ + \x20 cetakln(\"after\");", + ); +} + +/// `fail_panjang` and `fail_baca_baris` are gated as reads; the owner passes. +#[test] +fn size_and_lines_agree_for_the_owner() { + assert_agree( + "sizelines", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"ab\\ncd\"));\n\ + \x20 cetakln(ke_teks(fail_panjang(\"{}\")));\n\ + \x20 cetakln(ke_teks(senarai_panjang(fail_baca_baris(\"{}\"))));", + ); +} + +/// Delete drops the inode mapping, so the file may be re-created by a +/// DIFFERENT uid, which then owns it and may write again. This is the +/// `gate_delete` half — a C gate that merely checked the write bit without +/// clearing the mapping would deny the re-write and diverge here. +#[test] +fn delete_clears_ownership_and_agrees() { + assert_agree( + "delete", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"first\"));\n\ + \x20 biar d = fail_buang(\"{}\");\n\ + \x20 biar e = vfs_jadi_pengguna(9);\n\ + \x20 biar f = fail_tulis((\"{}\", \"second\"));\n\ + \x20 cetakln(fail_baca(\"{}\"));", + ); +} + +/// `fail_ada` is UNGATED in the interpreter — an existence check is not an +/// access. The C side must be ungated too: adding a gate there would be a +/// divergence in the opposite direction, denying what the interpreter allows. +#[test] +fn existence_check_is_ungated_in_both() { + assert_agree( + "exists", + " biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis((\"{}\", \"x\"));\n\ + \x20 biar d = vfs_jadi_pengguna(9);\n\ + \x20 cetakln(ke_teks(fail_ada(\"{}\")));", + ); +} diff --git a/03_PROTO/crates/riinac/tests/pkg_build.rs b/03_PROTO/crates/riinac/tests/pkg_build.rs index 029fa38b..598a79a4 100644 --- a/03_PROTO/crates/riinac/tests/pkg_build.rs +++ b/03_PROTO/crates/riinac/tests/pkg_build.rs @@ -130,19 +130,23 @@ fn package_with_wrong_return_type_fails_to_build() { /// A package using an interpreter-only builtin (REQ-70) fails at lowering /// rather than emitting a binary that cannot exist. /// -/// The example used to be `jaring_dengar`. It is not any more, because that -/// builtin now compiles — `fail_baca` is one of the families still unrouted, so -/// it is what still exercises the boundary. Update this again when `fail_*` -/// lands; the test is about the boundary existing, not about which side any -/// particular builtin is on. +/// The example has moved twice as REQ-70 routed families: first +/// `jaring_dengar`, then `fail_baca`, and now `vfs_baca`. `fail_baca` compiles +/// as of the verified-gate work, so it no longer sits on the boundary. +/// +/// `vfs_baca` is a deliberate choice rather than the next arbitrary one: it +/// reads the in-memory VirtualFs, whose quota accounting has no C +/// implementation, so it is expected to stay interpreter-only for as long as +/// that remains true. Update this again when it lands; the test is about the +/// boundary existing, not about which side any particular builtin is on. #[test] fn package_using_interpreter_only_builtin_fails_at_codegen() { let pkg = Pkg::new("interponly"); pkg.rm_src("lib.rii"); pkg.src( "utama.rii", - "fungsi utama() -> Nombor kesan (SistemFail | Tulis) {\n\ - \x20 cetakln(fail_baca(\"nota.txt\"));\n\ + "fungsi utama() -> Nombor kesan (Baca | Tulis) {\n\ + \x20 cetakln(vfs_baca(\"nota.txt\"));\n\ \x20 0\n\ }\n", ); diff --git a/RIINA_MASTER_PLAN.md b/RIINA_MASTER_PLAN.md index 8e9d5750..fb3787b0 100644 --- a/RIINA_MASTER_PLAN.md +++ b/RIINA_MASTER_PLAN.md @@ -431,7 +431,7 @@ research source, and detailed description. | REQ-67 | **Multi-prover honest-mechanization program (owner approved 2026-08-06, incl. both retirements).** Goal: every non-Coq lane either MECHANIZED AT AN HONESTLY-STATED SCOPE (prover passes in CI, 0 sorry/admit/axiom at that scope, claim level flipped only by `generate-metrics.sh` from fresh checker output) or RETIRED visibly — no lane left in the generated middle. REQ-29's retraction stands: no transpiler tricks, no axiom-backed compiles. Per-lane targets and DONE-whens: **(a) SMT (first, cheapest)** — redefine the lane as the Z3-VERIFIED set (today: 25 security-lattice properties in `SecurityLatticeVerification`), grow it with effect-join/policy algebra, retire the ~12,380 generated asserts from the headline; DONE when `z3` runs in CI on the scoped set and `claimLevels.smt` flips from the fresh report. **(b) Lean 4 (the credibility jewel)** — an INDEPENDENT hand-written re-proof of the core metatheory spine (Progress, Preservation, TypeSafety, Declassification), NOT the generated port; satisfies the maturity pillar's "≥1 independently re-proven theorem"; DONE per capstone when `lake build` elaborates it with 0 sorry/axiom in CI. **(c) TLA+** — one real spec where model checking beats Coq (JALINAN choreography deadlock-freedom, TLC-checked in CI); retire the generated corpus number. **(d) Alloy** — bounded capability/access-control model, same pattern. **(e) Verus/Kani** — REDIRECTED to verify the Rust implementation (which Coq does not cover): Kani harnesses on lexer/parser invariants, Verus on riina-core primitives; toolchain spike first (both fight the 1.94.1 pin as cargo-fuzz did). **(f) TV** — carried by REQ-59. **(g) Isabelle: RETIRED** (owner decision 2026-08-06 — Lean is the independence witness; a second redundant port adds no claim value). **(h) F*: RETIRED** (owner decision 2026-08-06 — 11,935 admits unsalvageable; the crypto story is carried by the nine Coq⇄Rust equivalences + the REQ-47 boundary). Retirement mechanics: `.RETIRED` marker in the lane root (rationale inside), `claimLevels.` = "retired" (legend extended; claim-integrity gate ranks retired at 0 so it can never overclaim), corpora stay in-tree for the record, website renders the badge from metrics as always. Sequencing: SMT → Lean capstone 1 → TLA+/Alloy → Verus/Kani spike; F*/Isabelle retirements EXECUTED 2026-08-06 (this session, verified by gates: metrics flip from the `.RETIRED` markers, all ten public-quality gates pass, claim-integrity ranks retired at 0). **SMT first step EXECUTED same session: z3 4.8.12 installed in-container via apt and the scoped set re-verified BY COMMAND — 25/25 unsat on `02_FORMAL/smt/RIINA/Active/SecurityLatticeVerification.smt2`, matching the 2026-06-01 record.** **SMT gate LANDED same session:** `scripts/verify-smt.sh` verifies exactly the files in `02_FORMAL/smt/SCOPED_SET.txt` against recorded verdicts (never self-skips — missing z3 is a FAILURE); validated by positive run (25/25 unsat, z3 4.8.12) and TWO negative controls (corrupted expected count FAILS; satisfiable check injected before `(exit)` FAILS — first control attempt exposed that content after `(exit)` is dead to Z3, and the gate is truncation-safe both directions); CI thin-wrapper job `smt-scoped` added to verify.yml. **Scoped set GROWN 2026-08-06 (same session): `EffectJoinVerification.smt2` — 12 properties of the 17-level effect-join algebra (Pure identity ×2, upper bounds ×2, commutativity, associativity, idempotence, LEAST-upper-bound, monotonicity, level-soundness, purity-preservation — the law that makes `kesan Bersih` compose — and closure), all UNSAT under z3 4.8.12; scoped set now 2 files / 37 properties.** **`claimLevels.smt` FLIPPED TO MECHANIZED 2026-08-07** — automatically, from the fresh strict checker report (the REQ-67a design working as intended): once the `escape_json` fix made the noncoq report valid JSON at the current head, `generate-metrics.sh` read the report's smt lane (mechanized_ready via the verify-smt scoped-set gate, 2 files / 37 properties UNSAT) and flipped the published level; the claim-integrity gate verifies it against the same report. Publishing consequence handled in the same increment: the report is now INCLUDED in the public tree (exclusion removed in sync-public.sh) because the public-side claim gate requires the evidence file the moment any lane claims above generated — its container-absolute paths are relativized by escape_json so it is publishable. Next SMT increments: policy-acceptance algebra (AlgorithmPolicy mirror) | P1 | IN PROGRESS (retirements + SMT flip done) | Gate D / Part 12 | | REQ-68 | **Zero-parameter function semantics defect in the interpreter's `LetRecGroup` (found 2026-08-06 by the C/WASM differential + a minimal repro, exactly the gate working as designed).** `build_lambda` (riina-types lib.rs) with an EMPTY params list emits the BARE BODY, not a lambda — so a zero-param `fungsi` desugars to a non-lambda group member whose declared type is the bare return type (not `Fn(Unit, …)`, inconsistent with the surface `Fn() -> T` annotation type). Consequences, all verified by minimal repro (22-line t22): (1) the interp's `LetRecGroup` arm evaluates non-lambda members EAGERLY at group-bind time — a zero-param function's body (including any side effects) runs ONCE at program startup, not per call; (2) such members are excluded from the sibling-closure rebind set, so a zero-param function whose body calls ANY group sibling dies at startup with `unbound variable` even when the function is never called — while `riinac check` and BOTH native backends accept and run the same program (C/WASM handle zero-param functions by their own convention). Trigger shape: `fungsi a() { … }` + `fungsi b(x) { a() }` + `fungsi c() { b(5) }` — `c` eagerly evaluates, enters `b`, whose rebind set lacks `a`. Found when the REQ-55 repair of effect_inference.rii made it the first dual-backend corpus file exercising the shape; the differential failed loudly rather than letting the divergence land (contrast the 2026-08-04 silent-skip lesson). ALSO surfaced en route: list values are UNPRINTABLE outside the interpreter — reference interp prints `[1, 2, 3]`/`[]`, the C backend prints ``/`()` (and ABORTS on `senarai_panjang` of a generic-Any empty list), WASM prints blank/`Benar` — a backend parity gap for the REQ-59 lane. FIX (focused increment, NOT rushed into the example batch): desugar zero-param `fungsi` to a unit-lambda `Lam(_, Unit, body)` with type `Fn(Unit, ret, eff)`, make zero-arg call sites apply `Unit`, align the driver's `utama` invocation and the typechecker's two-pass signature pre-bind, and add the t22 shape as a regression test in program.rs + an interp e2e; then remove the workaround note from effect_inference.rii. Until then the corpus discipline is: zero-param functions must not call group siblings (one file annotated). **2026-08-07 backend-parity increment (CI caught what the local suite could not — then the local gate was fixed so it can):** (1) **WASM `cetak`-of-Bool FIXED** — a bool argument fell into the string-pointer branch, dereferencing the 0/1 VALUE as a length-prefixed string address; CI's wasmtime produced wrong bytes (differential FAILED on security_levels.rii, the first dual-backend file printing a bool) while the local wasmtime CRASHED, which the old harness treated as a silent skip. The fix emits "betul"/"salah" byte-identical to the C backend's `riina_format`; verified by 7-line minimal repro + security_levels byte-equality. (2) **The differential's silent-skip gap CLOSED**: `run_c`/`run_wasm` now return `NoBuild | RunFail | Ran` — a build failure remains out-of-scope, BOTH-fail-at-runtime is a shared feature gap (skip), but exactly-one-side-fails is reported as a DIVERGENCE. This is the local-vs-CI asymmetry that hid (1). (3) The tightened gate immediately surfaced **four tracked asymmetric divergences** (KNOWN_DIVERGENT with reasons, all four run correctly on the reference interpreter): builder/command/state_machine (C runtime aborts — "le/mul on non-int", "load on non-ref": C lowering of padan enum-payload arithmetic and record loads through sum values) and test_driven (WASM translation error: closures stored in records). These are the backend feature gaps the REQ-55 pattern rewrites now exercise; clearing them is the same increment class as the zero-param fix. **FIXED 2026-08-12 — exactly the prescribed fix.** `desugar_function` (renamed from `build_lambda`) now gives a zero-parameter `fungsi` a SYNTHESISED `()` parameter, so it is `Unit -> T ! E` like any other function; `f()` is a real application; and the desugared program CALLS `utama` rather than running it as a side effect of binding it (the call is sequenced so the program value stays `Unit` — returning it made every compiled binary print its own exit code as a trailing line). **The prescription said "align the typechecker's two-pass signature pre-bind", and that was load-bearing:** the typechecker's `declared_function_type` and the parser's NESTED-function path each hand-rolled the same params→type fold, so each kept the old thunk shape after desugaring moved — the first made every zero-arg call fail with "Expected function type, found Int", the second left nested zero-arg functions broken. All three now route through `riina_types::declared_fn_ty` / `desugar_function`. **Consequence (2) is closed too:** the t22 trigger shape (`fungsi a()` + `fungsi b(x) { a() }` + `fungsi c() { b(5) }`) now yields 12 byte-identically on interpreter, C and WASM, where it previously died at startup with `unbound variable`. **It also closed an effect-system BYPASS not noted in the original row:** a zero-arg call incurred NO effect, because there was no application — so `baca_garisan()` read input and `masa_unix()` read the clock without `Sistem`/`Masa` ever reaching a signature. Five examples relied on it and now fail closed; their declarations were corrected rather than the check weakened. `baca_garisan` was typed at its RESULT type for the same reason and is now `Fn((), Teks, Sistem)` with a real stdin read. Verified: 9 three-way interp/C/WASM behavioural tests in `riinac/tests/zero_arg_function.rs` (6 fail without the change, confirmed by reverting; they assert EXPECTED output, not just agreement, because the old behaviour was a wrong answer both backends agreed on) + 2 IR-level tests in `backend_agreement.rs`; the whole `07_EXAMPLES` tree re-measured check+run before and after — **84 fully working, up from 78, zero regressions**. Remaining REQ-68 sub-item, tracked separately as part of the collections surface: list values print `[1, 2, 3]` under the interpreter, `` under C and blank under WASM | P1 | DONE | Phase 2 / Gate C | | REQ-69 | **Actor keyword corrected: `pelakon` → `pelaku` (owner decision 2026-08-08, hard rename — DONE same day).** `pelakon` is a stage/film actor — a mistranslation for the actor-model computation unit; `pelaku` (doer/agent) is correct. Hard mode: no deprecated alias — `pelakon` now lexes as a plain identifier (guard test: `pelaku`/`actor` → KwActor, `pelakon` → Identifier). The language surface was ONE lexer line; the sweep covered parser tests, the fuzz keyword list, the 6 Jalinan examples, docs (README/AGENTS/JALINAN_GUIDE/BIJAK_SPEC/session-types paper/2 Jalinan specs), llms.txt, the AI training corpus, and the website source. Historical CHANGELOG entries deliberately left as written. Zero Coq impact (the actor calculus uses English identifiers). Landed with the 2026-08-08 Gate C batch (see Part 11 entry) | P1 | DONE | Gate C | -| REQ-70 | **Deployability gap: effectful builtins are interpreter-only, so no effectful program can be compiled (found 2026-08-09 by codebase review; VERIFIED, not inferred).** `lower.rs::builtin_canonical` routes only the pure core (print, conversion, numeric tower, `teks`/`senarai`/`peta`/`set`, math, assertions). Every effectful family — `jaring_*` (net), `fail_*`/`file_*` (filesystem), `vfs_*`, `json_*`, `masa_*`, and the 84 `keselamatan` security builtins — is registered in the interpreter env ONLY, so C/WASM fail closed with `Codegen Error: unbound variable`. Reproduced end-to-end: a `jaring_dengar`-based HTTP server **typechecks, interprets, and serves a real `HTTP/1.1 200`**, but `riinac build` on the identical file fails. Consequence: RIINA can today compile console/pure programs only — **no networked or persistent program has a native or WASM deployment path.** Scope: route each effectful family through `builtin_canonical` + emit C/WASM implementations (or an explicit, documented runtime-shim ABI), family by family, each landed with an interp/C/WASM byte-equal differential. Sub-item (doc, do first — cheap and prevents agent breakage): **DONE 2026-08-09.** `docs/api/STDLIB.md` and `07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md` documented these builtins with full signatures and **no interpreter-only marker**, so any AI agent wrote a service, saw `Success!`, then hit an unexplained codegen error. Closed by making the boundary a *generated* fact rather than prose: `builtin_canonical` (the lowering gate that produces the error) is now exposed as `riina_codegen::codegen_supports_builtin`, and the STDLIB.md generator (`riina-typechecker/tests/stdlib_doc.rs`, already a byte-equality drift guard) consumes it to emit a per-builtin **Backend** column plus a section-level verdict — so the marker cannot drift from the compiler, and a future codegen fix updates the doc by regeneration. Required a deliberate dev-dependency cycle (riina-typechecker dev-deps riina-codegen; Cargo permits this) because the doc needs both halves of the truth. **Measured: 148 of 329 builtins compile, 181 are interpreter-only** — teks 16/16, senarai 18/18, peta 8/8, set 7/7 all compile; matematik 7/10 (`baki`/`log2`/`rawak` not), ujian 5/6 (`jangkakan` not); masa, fail, json, net, vfs and all 42 `keselamatan` sinks compile **none**. Boundary spot-verified empirically in both directions (`riinac build` on compiled-marked vs interp-only-marked builtins) — no contradiction. Also added COMMON_MISTAKES.md #21 with a verified wrong/fixed pair, and corrected that file's stale "Top 20" header and RIINA_FOR_AI.md's stale per-module counts (teks 18→16, senarai 17→18, peta 6→8, set 5→7, ujian 5→6, masa 6→7; net/vfs/keselamatan were **missing entirely**). Remaining REQ-70 work is the codegen implementation itself. **2026-08-11 update:** starting that work immediately surfaced REQ-78 — the WASM backend was emitting silent stubs, so the Backend column's `compiled` = "C **and** WASM" was FALSE for ~128 builtins. That is fixed and the column is now three-state. Re-derived from the regenerated `docs/api/STDLIB.md` after merging main 2026-08-12 (which added the `riina-tls` builtins): **373 registered, 148 compile — `compiled` 20 / `native-only` 128 / `interp-only` 225**. Fixing the honesty of the existing boundary had to come before adding families to it: routing more builtins into a backend that silently miscompiles would have multiplied the wrong answers. **Family routing STARTED 2026-08-11.** First finding: the families already marked `native-only` were not all usable — the **collections** family was counted as compiled while aborting on contact (REQ-79, fixed: `senarai_*`/`peta_*`/`set_*` now verified interp==C by 7 differential tests). Second finding: three `00_basics` examples diverged under C (REQ-80). The suspected cause — closures — was **disproved**; the real causes were a `#define`d collection tag colliding with the `riina_tag_t` enum, a missing list case in `+`, builtins that could not be shadowed by user functions, and an unresolvable field access that silently lowered to its base. All four are fixed (2026-08-12), as is early return — whose recorded blocker (the WASM relooper) turned out to be a misdiagnosis; the real causes were zero-parameter functions not being IR functions at all, and an `if` whose arms both return leaving its result on the WASM operand stack. A zero-arg `pulang` and boolean rendering remain open under REQ-80. **Order corrected as a result:** making the families ALREADY claimed as compiled actually work comes before routing new ones, because the Backend column's `native-only` was measuring lowering rather than behaviour. **JSON family ROUTED 2026-08-15 (first family under the corrected order).** Chosen first because it is pure value transformation — no syscalls — so interp/C byte-equality is actually reachable. The five `riina_builtin_json_*` helpers already existed in `emit.rs` but `builtin_canonical` had no `json` arm, so they were **unreachable dead code that had never executed**; adding the arm ran them for the first time and three disagreements fell out, all now fixed and pinned by `crates/riinac/tests/json_differential.rs` (9 tests): (1) **map iteration order** — the interpreter backs `Value::Map` with a `BTreeMap` (sorted) while the C runtime appended new keys at the tail (insertion order), so `json_ke_teks` serialised one object two ways. This was ALSO a live bug in `peta_*`, a family REQ-79 recorded as verified interp==C: `peta_kunci` on keys inserted zebra/apple/mango returned `apple,mango,zebra` interpreted and `zebra,apple,mango` compiled. REQ-79's differential never inserted out of order, so nothing caught it. All map-producing C builtins now funnel through one `riina_map_put_sorted`; (2) **`\uXXXX` escapes were silently dropped** — the C string parser's `default:` arm emitted the escape char literally, so `"ab"` parsed as the six characters `au0001b` (data corruption, not an error); (3) the C stringifier passed control chars `< 0x20` through raw where the interpreter escapes `\u00xx`, and rendered a `Pair` as `null` where the interpreter renders `[a,b]`. WASM still refuses the family through its fail-closed arm (no JSON parser in linear memory), so the Backend column reads **native-only**, not `compiled` — regenerated from the compiler, not hand-edited. **The REQ-79 lesson repeats and should now be assumed: a family marked as lowering is not thereby a family that agrees.** **Family routing (1.0) — `masa`/time DONE 2026-08-13, the first of the six.** Routed through `builtin_canonical`; **148 -> 162 builtins compile, interpreter-only 225 -> 211**. Two findings make this family worth having gone first. **(a) The C emitter already contained all six `masa` functions** — the family was interpreter-only purely because the routing gate did not list it, and the same is true of `fail` (8 C functions) and `json` (5). The remaining work for those three is smaller than the row implied. **(b) Routing it REVEALED three live divergences rather than introducing them**, all measured: `masa_format` **ignored its format string** in the interpreter (`1700000000`) while C ran a real `strftime` (`2023-11-14`); `masa_urai` parsed a bare decimal against C's `strptime`; and `masa_jam` returned **wall-clock nanos since the epoch** (~1.79e18) against C's `CLOCK_MONOTONIC` (~1.9e11) — a different clock, not a different reading. The first two are the silent-wrong-answer class. **Fix:** stop letting libc define the contract, since the interpreter can never match it under Law 8. Both backends now implement the SAME documented specifier subset (`%Y %m %d %H %M %S %s %%`, unsupported specifiers emitted literally so they are visible rather than dropped) over the same proleptic-Gregorian civil calendar, and `masa_jam` is monotonic on both. **Verification shape, which generalises to the rest of REQ-70: an effectful builtin is often not byte-comparable.** Two processes read a clock at different instants, so only the pure functions of their inputs (`masa_format`/`masa_urai`) are compared byte-for-byte; the clocks are checked as PROPERTIES — wall clocks agree within tolerance, the monotonic clock is not the wall clock and never goes backwards, milliseconds have millisecond magnitude, and `masa_tidur` actually sleeps. 9 differential tests (`riinac/tests/masa_differential.rs`), **all 9 fail at the pre-routing commit** (checked in an isolated worktree), plus 8 new unit tests over the calendar (era boundaries, the 1900/2000 century rules, pre-epoch flooring, format/parse round-trip). **WASM stays fail-closed for this family** — deliberately: a third hand-written calendar in raw WASM bytecode would reintroduce exactly the drift just removed, so `masa` is `native-only` and the Backend column says so. WASI's `clock_time_get` would allow the clocks alone later. **Family routing — `simpan`/store DONE 2026-08-13, the second family. 162 -> 178 builtins compile, interpreter-only 211 -> 195.** Unlike `masa`, this family had NO C implementation, so `riina-os::store`'s log-structured journal is now implemented twice — once in Rust, once in ~400 lines of emitted C (handle table, byte-sorted live map, replay, fsync-per-record, compaction). That is only safe because **the on-disk format is the contract**: a store written by an interpreted program must be readable by a compiled one and vice versa, or "durable" means "durable until you rebuild", which is worse than no persistence. Verified in BOTH directions plus a stronger check — the two backends emit **byte-identical journals** (same SHA-256), which catches the case where two implementations agree on how to parse but disagree on what to write. Also pinned on both backends: keys come back sorted (Rust gets it from `BTreeMap`, C from a sorted array, so it is a real invariant not a container accident); compaction shrinks the journal, preserves the live set, and produces byte-identical output; a **foreign file is refused, not overwritten**; and a **torn tail is discarded while every committed record before it survives** — the `VerifiedFileSystem.v` pending-transaction rule, now enforced by two independent implementations. 8 differential tests (`riinac/tests/simpan_differential.rs`), all 8 failing at the pre-routing commit. **Three families are now routed by two sessions working in parallel — `json` on `main` (PR #69), `masa` and `simpan` on the Gate C branch — and they converged on the same lesson independently: a family marked as LOWERING is not thereby a family that AGREES.** **Family routing — `jaring`+`http`/net DONE 2026-08-15, the third family on this branch and the one that makes a shipping service possible. 188 -> 218 builtins compile, interpreter-only 155.** Routed **in halves, deliberately**: the 8 plain-TCP `jaring_*` builtins, `tls_dasar_ok` and all 6 `http_*` builtins now lower to C; the 8 `jaring_tls_*` builtins do **not**, and that split is the finding, not a shortcut. A C TLS that is not really `riina-tls` (X25519, HKDF-SHA384, AES-256-GCM, the RFC 8446 §7.1 key schedule, raw-public-key auth) would compile programs that *appear* to negotiate while being weaker than the interpreter they were tested against, with nothing in the type signature to say so — strictly worse than a build error, so those names stay unbound and `riinac build` fails closed (REQ-78 rule). Two things were ported rather than approximated: the **verified RFC 793 machine** (`next_state`'s 15 edges, so the C backend gates send/recv on ESTABLISHED for the same reason the interpreter does — a backend that skipped the model would be weaker than the language it compiles) and the **strict RFC 9112 parser** in full. **Verification shape, new for this family: a protocol has a second party, so the load-bearing tests run TWO PROCESSES** — an interpreted client against a compiled server *and* a compiled client against an interpreted server, both compared to a literal expected wire message so the pair cannot pass by being wrong together. Eleven hostile messages (CL+TE, conflicting duplicate `Content-Length`, `Content-Length: 5, 6`, `Foo : bar`, missing `Host`, `HTTP/2.0`, chunked, truncated body, `0x10` length) are required to be refused by **both** backends: a C parser that accepted any of them would reintroduce request smuggling into compiled programs while the happy-path differential stayed green. 10 differential tests (`riinac/tests/net_differential.rs`), **8 of 10 failing at the pre-routing commit** (checked in an isolated worktree; the other 2 are the fail-closed guards, which must pass before and after), plus 3 routing tests in `riina-codegen/tests/backend_agreement.rs`. **Three divergences fell out, all pre-existing and all invisible until the second backend existed:** (a) **`cetak`/`cetakln` did not flush** in emitted C — Rust's stdout is line-buffered even when piped, C's switches to block buffering off a tty, so a compiled service that announces its address and then blocks on `jaring_terima_sambungan` (exactly `07_EXAMPLES/11_servis/pelayan.rii`) emitted **nothing until exit**; (b) `http_minta` stripped whatever port followed the last colon when building `Host`, sending `Host: x.test` for `http://x.test:8080/` — an RFC 9110 §7.2 violation that breaks port-keyed virtual hosts; now only `:80` is stripped, on both backends; (c) the earlier family differentials' `run_interp` helper split stdout into `lines()` and rejoined with `\n`, **silently deleting every CR** — harmless for `masa`/`simpan`, fatal for a family whose whole contract is CRLF framing, so this one strips only the final value line. **Gate C criterion 6 verified by command:** `07_EXAMPLES/11_servis/pelayan.rii` — multi-file (`guna kedai`), networked and persistent — now compiles with `riinac build`, serves real `HTTP/1.1 200` responses, and its visit counter **survives restarts across three separate compiled processes** (1, 2, 3). Pinning that as a test is REQ-75's remaining work. **Fourth divergence, found by the pre-commit gate rather than by a differential, and worth recording because it is a whole new failure MODE:** the corpus C⇄WASM differential ran every example with `Command::output()`, which has no timeout. That was safe only while nothing effectful compiled — every compiled example was pure computation that terminated or crashed. Once `pelayan.rii` compiled, the corpus harness built it and ran it with no client, so it parked in `jaring_terima_sambungan` and **hung the entire test suite forever** instead of failing. It was intermittent in the worst way: the first full run after routing went green because port 8140 was still held by the manual three-process persistence check, so the bind failed, the example was skipped, and the hang only appeared after a container restart freed the port. Fixed structurally — `run_c`/`run_wasm` now spawn with stdout/stderr to files (pipes would deadlock before the deadline could be checked), poll `try_wait` against a 20s deadline, and report `did not terminate within 20s` as a `RunFail`, which is an outcome the differential can reason about. **The general rule this establishes for the remaining REQ-70 families: routing an effectful family means the example corpus can now BLOCK, and every harness that runs a corpus example needs a deadline.** **FILE family: DO NOT ROUTE AS-IS — the gap is a security bypass, not a divergence (found 2026-08-17, VERIFIED).** The `json` prediction held (the 8 `riina_builtin_fail_*` C functions exist and have never executed), but the reason they must not simply be wired up is worse than the correctness bugs the other families produced. `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` — **12 gate call sites**. The emitted C helpers contain **0** gating constructs of any kind: `fail_baca` is a bare `fopen`, `fail_tulis` a bare `fwrite`. Adding a `fail`/`vfs` arm to `builtin_canonical` would therefore mean **`riinac run` denies an access that `riinac build` permits** — the compiler becomes the way around a verified security check, which is REQ-27 enforcement parity failing in the direction that matters. Measured on the interpreter: uid 1 writes a file, uid 2 is refused with `permission denied (verified can_write is false for the current uid)` and the file on disk is unchanged. **Prerequisite for routing: port the inode model + the uid/gid context + 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). Guarded by `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* — so it passes now (vacuously, no binary), passes after a correct port, and fails only if someone routes without porting. Honest limitation recorded in the test: its active arm is reviewed but **unexecuted**, because no `vfs_*` C helper exists to build the bypass with; both vacuous controls were run. Still NOT routed: file (`fail`/`vfs`, blocked on the gate port above), security (`keselamatan` — same question applies, its 42 sinks are the security surface), and the `jaring_tls_*` half above | P0 | IN PROGRESS (json + masa + simpan + net DONE; file/security + `jaring_tls_*` remain) | Gate C | +| REQ-70 | **Deployability gap: effectful builtins are interpreter-only, so no effectful program can be compiled (found 2026-08-09 by codebase review; VERIFIED, not inferred).** `lower.rs::builtin_canonical` routes only the pure core (print, conversion, numeric tower, `teks`/`senarai`/`peta`/`set`, math, assertions). Every effectful family — `jaring_*` (net), `fail_*`/`file_*` (filesystem), `vfs_*`, `json_*`, `masa_*`, and the 84 `keselamatan` security builtins — is registered in the interpreter env ONLY, so C/WASM fail closed with `Codegen Error: unbound variable`. Reproduced end-to-end: a `jaring_dengar`-based HTTP server **typechecks, interprets, and serves a real `HTTP/1.1 200`**, but `riinac build` on the identical file fails. Consequence: RIINA can today compile console/pure programs only — **no networked or persistent program has a native or WASM deployment path.** Scope: route each effectful family through `builtin_canonical` + emit C/WASM implementations (or an explicit, documented runtime-shim ABI), family by family, each landed with an interp/C/WASM byte-equal differential. Sub-item (doc, do first — cheap and prevents agent breakage): **DONE 2026-08-09.** `docs/api/STDLIB.md` and `07_EXAMPLES/06_ai_context/RIINA_FOR_AI.md` documented these builtins with full signatures and **no interpreter-only marker**, so any AI agent wrote a service, saw `Success!`, then hit an unexplained codegen error. Closed by making the boundary a *generated* fact rather than prose: `builtin_canonical` (the lowering gate that produces the error) is now exposed as `riina_codegen::codegen_supports_builtin`, and the STDLIB.md generator (`riina-typechecker/tests/stdlib_doc.rs`, already a byte-equality drift guard) consumes it to emit a per-builtin **Backend** column plus a section-level verdict — so the marker cannot drift from the compiler, and a future codegen fix updates the doc by regeneration. Required a deliberate dev-dependency cycle (riina-typechecker dev-deps riina-codegen; Cargo permits this) because the doc needs both halves of the truth. **Measured: 148 of 329 builtins compile, 181 are interpreter-only** — teks 16/16, senarai 18/18, peta 8/8, set 7/7 all compile; matematik 7/10 (`baki`/`log2`/`rawak` not), ujian 5/6 (`jangkakan` not); masa, fail, json, net, vfs and all 42 `keselamatan` sinks compile **none**. Boundary spot-verified empirically in both directions (`riinac build` on compiled-marked vs interp-only-marked builtins) — no contradiction. Also added COMMON_MISTAKES.md #21 with a verified wrong/fixed pair, and corrected that file's stale "Top 20" header and RIINA_FOR_AI.md's stale per-module counts (teks 18→16, senarai 17→18, peta 6→8, set 5→7, ujian 5→6, masa 6→7; net/vfs/keselamatan were **missing entirely**). Remaining REQ-70 work is the codegen implementation itself. **2026-08-11 update:** starting that work immediately surfaced REQ-78 — the WASM backend was emitting silent stubs, so the Backend column's `compiled` = "C **and** WASM" was FALSE for ~128 builtins. That is fixed and the column is now three-state. Re-derived from the regenerated `docs/api/STDLIB.md` after merging main 2026-08-12 (which added the `riina-tls` builtins): **373 registered, 148 compile — `compiled` 20 / `native-only` 128 / `interp-only` 225**. Fixing the honesty of the existing boundary had to come before adding families to it: routing more builtins into a backend that silently miscompiles would have multiplied the wrong answers. **Family routing STARTED 2026-08-11.** First finding: the families already marked `native-only` were not all usable — the **collections** family was counted as compiled while aborting on contact (REQ-79, fixed: `senarai_*`/`peta_*`/`set_*` now verified interp==C by 7 differential tests). Second finding: three `00_basics` examples diverged under C (REQ-80). The suspected cause — closures — was **disproved**; the real causes were a `#define`d collection tag colliding with the `riina_tag_t` enum, a missing list case in `+`, builtins that could not be shadowed by user functions, and an unresolvable field access that silently lowered to its base. All four are fixed (2026-08-12), as is early return — whose recorded blocker (the WASM relooper) turned out to be a misdiagnosis; the real causes were zero-parameter functions not being IR functions at all, and an `if` whose arms both return leaving its result on the WASM operand stack. A zero-arg `pulang` and boolean rendering remain open under REQ-80. **Order corrected as a result:** making the families ALREADY claimed as compiled actually work comes before routing new ones, because the Backend column's `native-only` was measuring lowering rather than behaviour. **JSON family ROUTED 2026-08-15 (first family under the corrected order).** Chosen first because it is pure value transformation — no syscalls — so interp/C byte-equality is actually reachable. The five `riina_builtin_json_*` helpers already existed in `emit.rs` but `builtin_canonical` had no `json` arm, so they were **unreachable dead code that had never executed**; adding the arm ran them for the first time and three disagreements fell out, all now fixed and pinned by `crates/riinac/tests/json_differential.rs` (9 tests): (1) **map iteration order** — the interpreter backs `Value::Map` with a `BTreeMap` (sorted) while the C runtime appended new keys at the tail (insertion order), so `json_ke_teks` serialised one object two ways. This was ALSO a live bug in `peta_*`, a family REQ-79 recorded as verified interp==C: `peta_kunci` on keys inserted zebra/apple/mango returned `apple,mango,zebra` interpreted and `zebra,apple,mango` compiled. REQ-79's differential never inserted out of order, so nothing caught it. All map-producing C builtins now funnel through one `riina_map_put_sorted`; (2) **`\uXXXX` escapes were silently dropped** — the C string parser's `default:` arm emitted the escape char literally, so `"ab"` parsed as the six characters `au0001b` (data corruption, not an error); (3) the C stringifier passed control chars `< 0x20` through raw where the interpreter escapes `\u00xx`, and rendered a `Pair` as `null` where the interpreter renders `[a,b]`. WASM still refuses the family through its fail-closed arm (no JSON parser in linear memory), so the Backend column reads **native-only**, not `compiled` — regenerated from the compiler, not hand-edited. **The REQ-79 lesson repeats and should now be assumed: a family marked as lowering is not thereby a family that agrees.** **Family routing (1.0) — `masa`/time DONE 2026-08-13, the first of the six.** Routed through `builtin_canonical`; **148 -> 162 builtins compile, interpreter-only 225 -> 211**. Two findings make this family worth having gone first. **(a) The C emitter already contained all six `masa` functions** — the family was interpreter-only purely because the routing gate did not list it, and the same is true of `fail` (8 C functions) and `json` (5). The remaining work for those three is smaller than the row implied. **(b) Routing it REVEALED three live divergences rather than introducing them**, all measured: `masa_format` **ignored its format string** in the interpreter (`1700000000`) while C ran a real `strftime` (`2023-11-14`); `masa_urai` parsed a bare decimal against C's `strptime`; and `masa_jam` returned **wall-clock nanos since the epoch** (~1.79e18) against C's `CLOCK_MONOTONIC` (~1.9e11) — a different clock, not a different reading. The first two are the silent-wrong-answer class. **Fix:** stop letting libc define the contract, since the interpreter can never match it under Law 8. Both backends now implement the SAME documented specifier subset (`%Y %m %d %H %M %S %s %%`, unsupported specifiers emitted literally so they are visible rather than dropped) over the same proleptic-Gregorian civil calendar, and `masa_jam` is monotonic on both. **Verification shape, which generalises to the rest of REQ-70: an effectful builtin is often not byte-comparable.** Two processes read a clock at different instants, so only the pure functions of their inputs (`masa_format`/`masa_urai`) are compared byte-for-byte; the clocks are checked as PROPERTIES — wall clocks agree within tolerance, the monotonic clock is not the wall clock and never goes backwards, milliseconds have millisecond magnitude, and `masa_tidur` actually sleeps. 9 differential tests (`riinac/tests/masa_differential.rs`), **all 9 fail at the pre-routing commit** (checked in an isolated worktree), plus 8 new unit tests over the calendar (era boundaries, the 1900/2000 century rules, pre-epoch flooring, format/parse round-trip). **WASM stays fail-closed for this family** — deliberately: a third hand-written calendar in raw WASM bytecode would reintroduce exactly the drift just removed, so `masa` is `native-only` and the Backend column says so. WASI's `clock_time_get` would allow the clocks alone later. **Family routing — `simpan`/store DONE 2026-08-13, the second family. 162 -> 178 builtins compile, interpreter-only 211 -> 195.** Unlike `masa`, this family had NO C implementation, so `riina-os::store`'s log-structured journal is now implemented twice — once in Rust, once in ~400 lines of emitted C (handle table, byte-sorted live map, replay, fsync-per-record, compaction). That is only safe because **the on-disk format is the contract**: a store written by an interpreted program must be readable by a compiled one and vice versa, or "durable" means "durable until you rebuild", which is worse than no persistence. Verified in BOTH directions plus a stronger check — the two backends emit **byte-identical journals** (same SHA-256), which catches the case where two implementations agree on how to parse but disagree on what to write. Also pinned on both backends: keys come back sorted (Rust gets it from `BTreeMap`, C from a sorted array, so it is a real invariant not a container accident); compaction shrinks the journal, preserves the live set, and produces byte-identical output; a **foreign file is refused, not overwritten**; and a **torn tail is discarded while every committed record before it survives** — the `VerifiedFileSystem.v` pending-transaction rule, now enforced by two independent implementations. 8 differential tests (`riinac/tests/simpan_differential.rs`), all 8 failing at the pre-routing commit. **Three families are now routed by two sessions working in parallel — `json` on `main` (PR #69), `masa` and `simpan` on the Gate C branch — and they converged on the same lesson independently: a family marked as LOWERING is not thereby a family that AGREES.** **Family routing — `jaring`+`http`/net DONE 2026-08-15, the third family on this branch and the one that makes a shipping service possible. 188 -> 218 builtins compile, interpreter-only 155.** Routed **in halves, deliberately**: the 8 plain-TCP `jaring_*` builtins, `tls_dasar_ok` and all 6 `http_*` builtins now lower to C; the 8 `jaring_tls_*` builtins do **not**, and that split is the finding, not a shortcut. A C TLS that is not really `riina-tls` (X25519, HKDF-SHA384, AES-256-GCM, the RFC 8446 §7.1 key schedule, raw-public-key auth) would compile programs that *appear* to negotiate while being weaker than the interpreter they were tested against, with nothing in the type signature to say so — strictly worse than a build error, so those names stay unbound and `riinac build` fails closed (REQ-78 rule). Two things were ported rather than approximated: the **verified RFC 793 machine** (`next_state`'s 15 edges, so the C backend gates send/recv on ESTABLISHED for the same reason the interpreter does — a backend that skipped the model would be weaker than the language it compiles) and the **strict RFC 9112 parser** in full. **Verification shape, new for this family: a protocol has a second party, so the load-bearing tests run TWO PROCESSES** — an interpreted client against a compiled server *and* a compiled client against an interpreted server, both compared to a literal expected wire message so the pair cannot pass by being wrong together. Eleven hostile messages (CL+TE, conflicting duplicate `Content-Length`, `Content-Length: 5, 6`, `Foo : bar`, missing `Host`, `HTTP/2.0`, chunked, truncated body, `0x10` length) are required to be refused by **both** backends: a C parser that accepted any of them would reintroduce request smuggling into compiled programs while the happy-path differential stayed green. 10 differential tests (`riinac/tests/net_differential.rs`), **8 of 10 failing at the pre-routing commit** (checked in an isolated worktree; the other 2 are the fail-closed guards, which must pass before and after), plus 3 routing tests in `riina-codegen/tests/backend_agreement.rs`. **Three divergences fell out, all pre-existing and all invisible until the second backend existed:** (a) **`cetak`/`cetakln` did not flush** in emitted C — Rust's stdout is line-buffered even when piped, C's switches to block buffering off a tty, so a compiled service that announces its address and then blocks on `jaring_terima_sambungan` (exactly `07_EXAMPLES/11_servis/pelayan.rii`) emitted **nothing until exit**; (b) `http_minta` stripped whatever port followed the last colon when building `Host`, sending `Host: x.test` for `http://x.test:8080/` — an RFC 9110 §7.2 violation that breaks port-keyed virtual hosts; now only `:80` is stripped, on both backends; (c) the earlier family differentials' `run_interp` helper split stdout into `lines()` and rejoined with `\n`, **silently deleting every CR** — harmless for `masa`/`simpan`, fatal for a family whose whole contract is CRLF framing, so this one strips only the final value line. **Gate C criterion 6 verified by command:** `07_EXAMPLES/11_servis/pelayan.rii` — multi-file (`guna kedai`), networked and persistent — now compiles with `riinac build`, serves real `HTTP/1.1 200` responses, and its visit counter **survives restarts across three separate compiled processes** (1, 2, 3). Pinning that as a test is REQ-75's remaining work. **Fourth divergence, found by the pre-commit gate rather than by a differential, and worth recording because it is a whole new failure MODE:** the corpus C⇄WASM differential ran every example with `Command::output()`, which has no timeout. That was safe only while nothing effectful compiled — every compiled example was pure computation that terminated or crashed. Once `pelayan.rii` compiled, the corpus harness built it and ran it with no client, so it parked in `jaring_terima_sambungan` and **hung the entire test suite forever** instead of failing. It was intermittent in the worst way: the first full run after routing went green because port 8140 was still held by the manual three-process persistence check, so the bind failed, the example was skipped, and the hang only appeared after a container restart freed the port. Fixed structurally — `run_c`/`run_wasm` now spawn with stdout/stderr to files (pipes would deadlock before the deadline could be checked), poll `try_wait` against a 20s deadline, and report `did not terminate within 20s` as a `RunFail`, which is an outcome the differential can reason about. **The general rule this establishes for the remaining REQ-70 families: routing an effectful family means the example corpus can now BLOCK, and every harness that runs a corpus example needs a deadline.** **FILE family: ROUTED 2026-08-18, behind a mirrored verified gate — the prerequisite below is now MET.** The 8 `fail_*` builtins plus the two VFS context setters (`vfs_mula`, `vfs_jadi_pengguna`) compile; a compiled binary now refuses a non-owner write exactly as `riinac run` does, with the file left unchanged. Design decision worth recording, because the obvious approach is impossible: **emitted C cannot call into Rust.** The pipeline is `cc -o out one.c` with nothing linked, so a single shared implementation of the predicate would have required shipping per-target Rust staticlibs (native/wasm32/android/ios) and rebuilding the compile pipeline. Instead the **Coq model is the single source of truth** — `domains/VerifiedFileSystem.v` (`Inode`/`Ownership`/`Permission`/`is_owner`/`get_permission`) — with `riina-os/src/vfs.rs` and the emitted C as two implementations of it, held together by a differential. Same shape as the `masa` civil calendar and the GF128/AES Coq⇄Rust equivalences. The C mirrors the inode table, first-touch ownership at mode 0644, and owner▷group▷other resolution; `fail_ada` and `fail_senarai` are left **ungated on both sides**, matching the interpreter (an existence check is not an access, and gating them in C would be a divergence in the opposite direction). `vfs_tulis`/`vfs_baca`/`vfs_padam` stay interpreter-only — they operate on the in-memory VirtualFs with quota accounting, which has no C implementation, and stubbing them would claim an enforcement this backend cannot make. **The `file_gate_parity.rs` limitation recorded on 2026-08-17 is now CLOSED**: its active `SECURITY REGRESSION` arm was previously unexecutable and is now negative-controlled — deleting a single `riina_gate` call from the emitted `fail_tulis` makes the compiled binary perform the write (exit 0) and the test fails with the intended message. Behaviour pinned by `file_differential.rs` (7 cases chosen to separate the resolution arms: owner write, non-owner read ALLOWED at 0644, non-owner write and append DENIED, delete clears ownership so a re-creator owns it, ungated existence check). Historical finding, retained: **FILE family: DO NOT ROUTE AS-IS — the gap is a security bypass, not a divergence (found 2026-08-17, VERIFIED).** The `json` prediction held (the 8 `riina_builtin_fail_*` C functions exist and have never executed), but the reason they must not simply be wired up is worse than the correctness bugs the other families produced. `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` — **12 gate call sites**. The emitted C helpers contain **0** gating constructs of any kind: `fail_baca` is a bare `fopen`, `fail_tulis` a bare `fwrite`. Adding a `fail`/`vfs` arm to `builtin_canonical` would therefore mean **`riinac run` denies an access that `riinac build` permits** — the compiler becomes the way around a verified security check, which is REQ-27 enforcement parity failing in the direction that matters. Measured on the interpreter: uid 1 writes a file, uid 2 is refused with `permission denied (verified can_write is false for the current uid)` and the file on disk is unchanged. **Prerequisite for routing: port the inode model + the uid/gid context + 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). Guarded by `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* — so it passes now (vacuously, no binary), passes after a correct port, and fails only if someone routes without porting. Honest limitation recorded in the test: its active arm is reviewed but **unexecuted**, because no `vfs_*` C helper exists to build the bypass with; both vacuous controls were run. **`keselamatan` INSPECTED 2026-08-18 (read-only) — it is NOT a second file family.** Its taint/sink discipline is enforced at COMPILE time by the type system, not at runtime: `sql_laksana : Fn(Disanitasi, …)`, `sanitasi_html : Fn(Tercemar, Disanitasi)`. Verified by running it — feeding raw input to a sink fails at `riinac check` with `expected Sanitized(String, SqlParam), found String`, before a backend is chosen, so a compiled program cannot bypass it. Only 3 of the 42 carry a RUNTIME security property — `fail_baca_selamat`/`fail_tulis_selamat`/`fail_buang_selamat`, which call the SAME gate as `fail_*` and are therefore covered by the mirrored C gate. `emit.rs` contains **zero** C helpers for any `keselamatan` builtin, so unlike `fail_*` there is no pre-written ungated code to route by accident. Consequence: routing the remaining 39 is ordinary work, not security-critical. **Incidental finding:** `csrf_jana` derives tokens from `SystemTime` nanos + a counter through `DefaultHasher` — predictable, not a CSPRNG. This is honestly disclaimed in the source ("a *reference* token … production deployments should source it from `riina-core`'s CSPRNG") but the caveat does NOT reach `docs/api/STDLIB.md`, where a caller sees only `Fn((), Teks, Rawak)` — the REQ-47 boundary-disclosure pattern again, and cheap to fix with a generated caveat column. Still NOT routed: `keselamatan` (39 of 42 — ordinary work per the inspection above), the VirtualFs trio `vfs_tulis`/`vfs_baca`/`vfs_padam` (need an in-memory FS + quota in C), and the `jaring_tls_*` half above | P0 | IN PROGRESS (json + masa + simpan + net DONE; file/security + `jaring_tls_*` remain) | Gate C | | REQ-71 | **No module system: every RIINA program must be a single file (found 2026-08-09; VERIFIED).** `guna ;` parses but is a no-op — a two-file program fails with `Variable not found`. There is also **no `.rii` standard library anywhere in the repo** (`find -name '*.rii' -path '*std*'` is empty); "stdlib" today means Rust-side builtins only, and the `guna std::rangkaian`-style imports used across `07_EXAMPLES/03_applications/` refer to modules that do not exist. Consequence: no application above single-file scale — an OS, ERP, or web app is structurally impossible regardless of builtin coverage. Scope: implement `guna` resolution (path→file, visibility via `awam`, cycle detection), a multi-file compilation unit in `riinac`, and a real `.rii` stdlib layered over the builtins. **MODULE SYSTEM DONE 2026-08-09** (`riina-parser/src/modules.rs`, 11 end-to-end tests in `riinac/tests/module_system.rs` + 6 traversal unit tests). A two-file program now **checks, runs, AND compiles** — verified native (`build --run` prints the right answer) and `wasm32` (the linked `.wasm` executes under wasmtime). Design: linking reuses the flat-name convention the surface already had (`kira::tambah` → `kira_tambah` via `parse_module_path`; `modul k { fungsi f }` → `k_f`) rather than inventing a second one — every top-level name of an imported module is renamed `_` and every FREE reference inside that module is renamed with it, so module-internal calls keep working while a shadowing local (`biar tambah = 100`) is correctly left alone. The root module is never renamed, so `utama` stays `utama`. Renaming and reference-collection share ONE binder-aware traversal (`walk_free_idents`) whose `match` is exhaustive over all 54 `Expr` variants with **no wildcard arm**, so a future AST variant fails the build instead of silently escaping renaming and mis-linking. Enforced, each with a test: import **cycles** (reports the chain `main -> a -> b -> a`, not a stack overflow), **visibility** (non-`awam` is module-private despite the flat namespace), **direct imports** (a transitively-loaded module is present but not silently in scope), **name collisions** (hard error, never silent shadowing), and **no top-level code in an imported module**. Back-compat: `guna std::teks;` is multi-segment, names the builtin namespace, has no file, and is deliberately NOT a file import — corpus sweep unchanged at 92/167 passing. **Remaining: the `.rii` stdlib**, which is deliberately deferred — the resolver currently searches only the importing file's directory, so a stdlib needs a search-path/prelude design decision (where it ships, how `guna` finds it, whether `std::` stops meaning "builtin"), and it is worth far more once REQ-70 lets stdlib code be compiled | P0 | TODO (module system DONE; `.rii` stdlib remains) | Gate C | | REQ-72 | **`riinac pkg build` is a placeholder that copies source and reports success (found 2026-08-09; VERIFIED — violates Prime Directive 2 "No Shortcuts").** `riina-pkg/src/build.rs::execute_build` contains `// Copy source to output (placeholder for actual compilation)` and `std::fs::copy`s `src/*.rii` into `sasaran/`. It printed `Built: ujian / Build complete.` for a package whose only source called an **undefined function** — no parse, no typecheck, no codegen, no artifact. The manifest/resolver/lockfile/registry layers around it are real; only the compile step is a stub. Scope: make `execute_build` invoke the actual pipeline, fail non-zero on any error, emit real artifacts, and add a negative test pinning that a package with a type error cannot "build". **DONE 2026-08-09.** `execute_build` now takes an injected `CompileFn` and has no path that reports success without the compiler agreeing; `riinac` supplies `pkg_compile::compile_package`. **Dependency injection was chosen over adding the compiler crates to `riina-pkg`** precisely so a SECOND compile path cannot grow there and silently diverge from `riinac build` — both now call the same four entry points (`riina_parser::modules::resolve_program` → `check_program` → `riina_codegen::compile` → `backend.emit`). Verified end-to-end: the exact source that used to print `Built: ujian / Build complete.` and exit 0 (`INI_TIDAK_WUJUD()`) now exits **1** with the compiler's own diagnostic; a valid multi-file package emits a real native binary at `sasaran//` that runs and prints the right answer (so `pkg build` goes through the REQ-71 resolver); `sasaran/` no longer contains copied `.rii` source; a `lib.rii` library entry is type-checked and emits no binary (never a silent pass — a broken library still fails); a `src/` with no entry module errors naming both candidates; REQ-70's boundary is enforced here too (a package using `jaring_dengar` fails with `unbound variable` instead of emitting a binary that cannot exist); and REQ-71 visibility holds inside a package. 12 new tests (8 end-to-end in `riinac/tests/pkg_build.rs` incl. the required negative test, 4 unit in `riina-pkg`). **Not in scope, and still open:** cross-package linking — a dependency's modules are not importable, because `guna` resolves only within the importing file's directory (the REQ-71 search-path item). Dependencies therefore remain decorative until that lands | P0 | DONE | Gate C | | REQ-73 | **No TLS record layer and no real HTTP — the web/network surface above raw TCP is modelled (found 2026-08-09; VERIFIED).** `jaring_*` performs real TCP gated by the Coq RFC 793 machine, but `tls_dasar_ok` is the **acceptance policy only** (no handshake, no record layer — `net.rs` states this outright: no dep-free TLS stack exists under Law 8), and the `keselamatan` web sinks are explicitly modelled: `http_get`/`http_post` return a canned constant **with no socket opened**, `sql_execute`/`ldap_search`/`xml_query`/`js_eval` echo their (sanitized) input with **no database or engine contacted**, `email_send` returns `true` with no SMTP, `shell_exec` returns `0` without spawning. These are sound demonstrations of the taint→sink type discipline, not working I/O. Consequence: no transport security and no data tier — disqualifying for banking, healthcare, and defense. Scope (three parts, only one of which was ever blocked): **(a) HTTP/1.1 client+server over the verified TCP machine — DONE 2026-08-11.** `riina-os/src/http.rs` is a dependency-free RFC 9112 codec (28 unit tests) exposed as the REAL builtins `http_hurai_kaedah/laluan/jasad/kepala`, `http_balas`, `http_minta` (6 builtin tests, 6 end-to-end tests). A RIINA program now parses a request off a socket and serves a correctly framed response that `curl` accepts, and `http_minta` performs a real request driving the same verified RFC 793 machine (CLOSED→SYN_SENT→ESTABLISHED, gated send, verified active close). **The parser is deliberately strict, because HTTP's real vulnerabilities are framing disagreements:** `Content-Length` + `Transfer-Encoding` (CL.TE/TE.CL smuggling), conflicting duplicate/comma-list `Content-Length`, whitespace before the colon (`Foo : bar`), chunked (rejected, never mis-framed), missing `Host` on 1.1, non-1.x versions, oversized head/body, too many headers — each is an ERROR surfaced into the RIINA program, not a repaired message. Encoding computes `Content-Length`/`Connection` itself and refuses CR/LF/NUL in any field, so a program cannot emit a split response even passing attacker data straight through; caller-supplied framing headers are ignored. These are DISTINCT from the modelled `http_get`/`http_post` sinks in `keselamatan`, which are deliberately left alone because they carry the taint→sink TYPE discipline the Coq `*_injection_impossible` family is about. **(b) TLS 1.3 — STILL BLOCKED on the owner decision, but the decision is now much better informed:** the claim "no dep-free TLS stack exists under Law 8" was about the PROTOCOL layer, not the crypto. `05_TOOLING/crates/riina-core` is already zero-dependency (Law 8 clean) and already ships the entire TLS 1.3 cipher suite, KAT-verified: X25519 (RFC 7748), AES-256-GCM, HKDF-SHA256 (RFC 5869), SHA-2/SHA-3, Ed25519, plus `constant_time` and `zeroize`. What is missing is the handshake state machine, the record layer, and X.509 parsing/validation — NOT the primitives. `http_minta` therefore REFUSES `https://` loudly (pointing at this REQ) rather than silently downgrading to cleartext. Remaining sub-decision for the owner: (i) in-tree TLS 1.3 over the existing KAT'd primitives, or (ii) vendor an audited stack (breaks Law 8 as written), plus who owns X.509. **UNBLOCKED — the owner chose (i) and it landed on `main` (PRs #61–#64), merged into this branch 2026-08-12.** Re-derived from the merged code rather than the PR prose: `03_PROTO/crates/riina-tls` (the 20th proto crate) implements a real ephemeral-X25519 TLS 1.3 handshake with the RFC 8446 §7.1 key schedule, transcript binding and Finished verification, with per-direction traffic keys (a shared key with both peers at sequence 0 would be catastrophic AES-GCM nonce reuse), peer authentication via RFC 7250 raw-public-key Certificate + §4.4.3 CertificateVerify, and a schedule parameterised over the hash so `HashAlg::Sha384` names the registered IANA suite `TLS_AES_256_GCM_SHA384`. `jaring_tls_jabat_sah`/`jaring_tls_identiti`/`jaring_tls_percaya`/`jaring_tls_disahkan` expose it to `.rii`, and `jaring_tls_disahkan` reports whether the FULL Coq `tls_connected` conjunction holds. Stated limits carried forward, not closed by this: trust is **pinning**, not PKI — no chains, no CA, no revocation, no X.509 — and the anonymous `jaring_tls_jabat` path still resists only a passive eavesdropper. The whole `jaring_tls_*` surface is **interpreter-only** (not in `builtin_canonical`), so it inherits REQ-70's compile gap; `http_minta` still refuses `https://` loudly. **(c) durable persistence — DONE 2026-08-11.** `riina-os/src/store.rs` is a dependency-free log-structured key-value store (12 unit tests) exposed as `simpan_buka/letak/dapat/ada/padam/kunci/padat/tutup` (9 builtin tests, 6 end-to-end tests). **Its on-disk journal is the `VerifiedFileSystem.v` model made real:** the model says a transaction counts only when `TxnCommitted` (`txn_complete`) and a journal is consistent only when every transaction is complete (`journal_consistent`), so a record is committed iff its length prefix AND CRC-32 both validate, and a torn tail (a crash mid-append = `TxnPending`) is truncated on recovery — after `Store::open` the file is consistent by construction. Verified: data written by one process is read by a different process; a delete is durable too; a torn tail is discarded while every committed record before it survives and the store stays writable; a single flipped byte fails CRC and is never returned as data; a non-store file is REFUSED, not overwritten; compaction preserves the live set and post-compaction writes persist. `fsi_atomic_writes` is realised by fsyncing every committed record before the call returns (survives power loss, not just process death); compaction is atomic via temp-file → fsync → `rename` → **fsync of the parent directory** (the usually-forgotten step, without which the rename is not durable). CRC-32/IEEE is pinned by its standard check value (`crc32("123456789") == 0xCBF43926`). **Reference service landed:** `07_EXAMPLES/11_servis/` is multi-file (REQ-71) + networked (REQ-73 HTTP) + durable (REQ-73 store) — a guest book whose visit counter continues across process restarts (verified #1→#2→#3 over three separate runs). It runs on the interpreter; COMPILING it still needs REQ-70's codegen half, which is what keeps Gate C exit criterion 6 open. **2026-08-15: it now COMPILES and runs compiled** — `simpan_*`, `jaring_*` and `http_*` are all routed, and the compiled binary keeps its counter across three separate process restarts. The `http_*` codec exists twice as a result (Rust and emitted C) and the strict refusals above are pinned as agreeing on both backends — see the REQ-70 row. The `jaring_tls_*` surface stays interpreter-only on purpose: its C half would have to be `riina-tls` itself, and anything less would compile programs that look negotiated while being weaker than the interpreter | P0 | TODO (HTTP + persistence DONE and now COMPILED; TLS 1.3 handshake DONE via riina-tls, merged from main 2026-08-12 — X.509/PKI and `jaring_tls_*` codegen routing still open) | Gate C | diff --git a/VERIFICATION_MANIFEST.md b/VERIFICATION_MANIFEST.md index 4f93ec2c..0a983f0d 100644 --- a/VERIFICATION_MANIFEST.md +++ b/VERIFICATION_MANIFEST.md @@ -1,6 +1,6 @@ # RIINA Verification Manifest -**Generated:** 2026-08-17T22:04:25Z -**Git SHA:** 2536f0bf6 +**Generated:** 2026-08-18T22:01:33Z +**Git SHA:** 512c6baf4 **Mode:** full **Status:** PASS @@ -8,10 +8,10 @@ | Check | Status | Details | |-------|--------|---------| -| Rust Tests | PASS | 3323 tests | +| Rust Tests | PASS | 3330 tests | | Clippy | PASS | 0 warnings | | _CoqProject Completeness | PASS | all 331 .v files listed in _CoqProject | -| Coq Compilation | PASS | 331 .vo files compiled in 235s | +| Coq Compilation | PASS | 331 .vo files compiled in 159s | | Coq Kernel Assumptions | PASS | 5 capstones attested; axioms within reviewed whitelist (1 allowed: funext) | | Coq Admits | PASS | 0 (target: 1) | | Coq Axioms | PASS | 0 (informational; explicit assumptions tracked separately) | @@ -22,9 +22,9 @@ | Isabelle sorry/oops | PASS | 0 sorry + 0 oops in 368 files (12925 lemmas) | | F* Compilation | WARN | pinned local F* not found (run: bash scripts/provision-smoke-toolchains.sh or bash scripts/provision-fstar.sh) | | F* admit Scan | WARN | 12010 admit in 315 files (19 lemmas) | -| TLA+ Compilation | PASS | Active spec TelusProcurementProtocol parsed and model checked in 2s (5 theorems, local_active) | +| TLA+ Compilation | PASS | Active spec TelusProcurementProtocol parsed and model checked in 1s (5 theorems, local_active) | | TLA+ Scan | PASS | 317 files (12282 theorems) | -| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 11s (6 checked assertions, local_active) | +| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 6s (6 checked assertions, local_active) | | Alloy Scan | PASS | 306 files (11627 assertions) | | SMT Scan | PASS | 318 files (12431 assertions) | | Verus admit Scan | PASS | 0 admit in 323 files (6395 proof fns) | diff --git a/docs/api/STDLIB.md b/docs/api/STDLIB.md index b9323ea5..e23f23d0 100644 --- a/docs/api/STDLIB.md +++ b/docs/api/STDLIB.md @@ -6,13 +6,13 @@ Total registered builtins: **373**. Grouped by the effect each performs (`kesan` ## ⚠ Read first: type-checking does not imply compiling -Every builtin below type-checks and runs under `riinac run` (the interpreter). Only **218** of the 373 also compile, and they do NOT all reach the same backends: +Every builtin below type-checks and runs under `riinac run` (the interpreter). Only **238** of the 373 also compile, and they do NOT all reach the same backends: | Backend value | Meaning | |---|---| | `compiled` | Lowers to C **and** WASM (20 builtins). | -| `native-only` | Lowers to C. The WASM backend **refuses** it (198 builtins). | -| `interp-only` | `riinac run` only (155 builtins). `riinac build` fails with `unbound variable`. | +| `native-only` | Lowers to C. The WASM backend **refuses** it (218 builtins). | +| `interp-only` | `riinac run` only (135 builtins). `riinac build` fails with `unbound variable`. | ``` $ riinac check baca.rii # Success! Effect: FileSystem @@ -297,26 +297,24 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## SistemFail (FileSystem) -> **Mixed:** 16 of 36 compile; the rest are interpreter-only (REQ-70). - | Builtin | Type | Backend | |---|---|---| -| `fail_ada` | `Fn(Teks, Benar, SistemFail)` | **interp-only** | -| `fail_baca` | `Fn(Teks, Tercemar, SistemFail)` | **interp-only** | -| `fail_baca_baris` | `Fn(Teks, Tercemar, SistemFail)` | **interp-only** | -| `fail_buang` | `Fn(Teks, (), SistemFail)` | **interp-only** | -| `fail_panjang` | `Fn(Teks, Nombor, SistemFail)` | **interp-only** | -| `fail_senarai` | `Fn(Teks, Any, SistemFail)` | **interp-only** | -| `fail_tambah` | `Fn((Teks, Teks), (), SistemFail)` | **interp-only** | -| `fail_tulis` | `Fn((Teks, Teks), (), SistemFail)` | **interp-only** | -| `file_append` | `Fn((Teks, Teks), (), SistemFail)` | **interp-only** | -| `file_delete` | `Fn(Teks, (), SistemFail)` | **interp-only** | -| `file_exists` | `Fn(Teks, Benar, SistemFail)` | **interp-only** | -| `file_list_dir` | `Fn(Teks, Any, SistemFail)` | **interp-only** | -| `file_read` | `Fn(Teks, Tercemar, SistemFail)` | **interp-only** | -| `file_read_lines` | `Fn(Teks, Tercemar, SistemFail)` | **interp-only** | -| `file_size` | `Fn(Teks, Nombor, SistemFail)` | **interp-only** | -| `file_write` | `Fn((Teks, Teks), (), SistemFail)` | **interp-only** | +| `fail_ada` | `Fn(Teks, Benar, SistemFail)` | **native-only** | +| `fail_baca` | `Fn(Teks, Tercemar, SistemFail)` | **native-only** | +| `fail_baca_baris` | `Fn(Teks, Tercemar, SistemFail)` | **native-only** | +| `fail_buang` | `Fn(Teks, (), SistemFail)` | **native-only** | +| `fail_panjang` | `Fn(Teks, Nombor, SistemFail)` | **native-only** | +| `fail_senarai` | `Fn(Teks, Any, SistemFail)` | **native-only** | +| `fail_tambah` | `Fn((Teks, Teks), (), SistemFail)` | **native-only** | +| `fail_tulis` | `Fn((Teks, Teks), (), SistemFail)` | **native-only** | +| `file_append` | `Fn((Teks, Teks), (), SistemFail)` | **native-only** | +| `file_delete` | `Fn(Teks, (), SistemFail)` | **native-only** | +| `file_exists` | `Fn(Teks, Benar, SistemFail)` | **native-only** | +| `file_list_dir` | `Fn(Teks, Any, SistemFail)` | **native-only** | +| `file_read` | `Fn(Teks, Tercemar, SistemFail)` | **native-only** | +| `file_read_lines` | `Fn(Teks, Tercemar, SistemFail)` | **native-only** | +| `file_size` | `Fn(Teks, Nombor, SistemFail)` | **native-only** | +| `file_write` | `Fn((Teks, Teks), (), SistemFail)` | **native-only** | | `simpan_ada` | `Fn((Nombor, Teks), Benar, SistemFail)` | **native-only** | | `simpan_buka` | `Fn(Teks, Nombor, SistemFail)` | **native-only** | | `simpan_dapat` | `Fn((Nombor, Teks), Teks, SistemFail)` | **native-only** | @@ -333,10 +331,10 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `store_keys` | `Fn(Nombor, Senarai, SistemFail)` | **native-only** | | `store_open` | `Fn(Teks, Nombor, SistemFail)` | **native-only** | | `store_put` | `Fn((Nombor, (Teks, Teks)), Benar, SistemFail)` | **native-only** | -| `vfs_become_user` | `Fn(Nombor, (), SistemFail)` | **interp-only** | -| `vfs_init` | `Fn(Nombor, (), SistemFail)` | **interp-only** | -| `vfs_jadi_pengguna` | `Fn(Nombor, (), SistemFail)` | **interp-only** | -| `vfs_mula` | `Fn(Nombor, (), SistemFail)` | **interp-only** | +| `vfs_become_user` | `Fn(Nombor, (), SistemFail)` | **native-only** | +| `vfs_init` | `Fn(Nombor, (), SistemFail)` | **native-only** | +| `vfs_jadi_pengguna` | `Fn(Nombor, (), SistemFail)` | **native-only** | +| `vfs_mula` | `Fn(Nombor, (), SistemFail)` | **native-only** | ## Rangkaian (Network) diff --git a/website/public/metrics.json b/website/public/metrics.json index 4757cd4c..0b7b591f 100644 --- a/website/public/metrics.json +++ b/website/public/metrics.json @@ -1,11 +1,11 @@ { - "generated": "2026-08-18T21:24:55Z", - "generatedHuman": "August 18, 2026 at 21:24 UTC", + "generated": "2026-08-18T21:51:53Z", + "generatedHuman": "August 18, 2026 at 21:51 UTC", "version": "0.4.0", "session": 0, "git": { - "commit": "796aea405", - "branch": "main" + "commit": "73dc579c2", + "branch": "claude/continue-solution-4gn31y" }, "proofs": { "qedActive": 12678, @@ -196,8 +196,8 @@ "rust": { "tests": 3323, "testsVerified": 3323, - "testsEstimated": 0, - "testsSource": "full_cargo_test", + "testsEstimated": 3326, + "testsSource": "cached_verified", "crates": 20 }, "examples": 169,