From dbfedef0c6ab0bfd9813bf8eac189fe9a2ba071f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 21 Aug 2026 02:03:47 +0000 Subject: [PATCH 1/4] [TRACK_B] FIX: route 12 of the last pure builtins, and fix three defects they hid REQ-70. I described the remaining interpreter-only set as a backlog of builtins nobody had examined. Examining them found that most were not missing implementations at all -- they were defects that the Backend column happened to render as "interp-only". 1. A LANGUAGE FEATURE DID NOT COMPILE. adalah_kiri/adalah_kanan/nilai_kiri/ nilai_kanan are not stdlib functions a user calls; they are COMPILER INTERNALS. The parser's if-chain pattern compiler emits them for a constructor pattern nested where a `Case` cannot go -- `(Ada(a), Tiada)` inside a tuple pattern. Unrouted, that entire class of pattern ran under `riinac run` and failed `riinac build` with `Codegen Error: unbound variable: nilai_kiri`. Four obscure interp-only rows were in fact one missing feature in the compiled backend. 2. baki/rem WERE UNCALLABLE FROM ANY WELL-TYPED PROGRAM. They are binary and take a pair -- the interpreter's extract_pair_ints and the emitted C's RIINA_TAG_PAIR check both say so -- but the typechecker declared them `Nombor -> Nombor`, because they shared a registration loop with the genuinely unary log2. So `baki(10, 3)` failed with "Expected function type, found Int" and `baki((10, 3))` failed with "expected Int, found Prod(Int, Int)". Two of three components agreed; the type was the outlier, so the type is what changed. 3. cetak_baris WAS A PURE ALIASING GAP. The interpreter binds cetakln, println AND cetak_baris to one Value::Builtin("cetakln"). Only builtin_canonical knew two of the three, so a program using the third ran and then failed to build. baki, log2 and rawak already HAD C implementations sitting unreferenced in emit.rs, exactly like the json helpers before them. Only the gate was missing. ROUTED (12 names): the four sum helpers, baki/rem, log2, julat/julat_inklusif, rawak/random, cetak_baris. New C for the ranges and the sum helpers; the ranges mirror the interpreter's SATURATING inclusive increment, and the sum payload projections are deliberately lenient on a non-sum argument as the interpreter is. rawak/random is routed despite the two backends being uncomparable by output -- both are time-seeded. The differential pins the range invariant instead and says plainly that equality is not being checked. Routing is still right: without it a compiled RIINA program has no source of randomness at all. Neither implementation is a CSPRNG and neither claims to be. THE BACKEND COLUMN WAS MAKING A FALSE PROMISE, now fixed. Its `interp-only` cell reads "`riinac run` only". For the eight crypto-agility builtins (guna_kripto/use_crypto, pilih_algo/select_algorithm, cipher/sifer, hash_dengan/hash_with) that was FALSE: they are in the typechecker registry with `Fn(Teks, Any, Kripto)` and carry the REQ-48 deprecation check at their call sites, but NO runtime binds them, so `riinac run` fails with `unbound variable` exactly as `riinac build` does. Verified by command for all eight. A three-state column had no way to say "typed but unimplemented", so it said the nearest thing, which was wrong. Added a fourth state `typed-only`, derived from a new `riina_codegen::interpreter_supports_builtin` that builds the real interpreter environment and looks the name up -- not from a list, which would drift the moment a runtime is added. Counts re-derived from the regenerated doc: 373 registered -- compiled 21 / native-only 314 / interp-only 30 / typed-only 8. The remaining 30 are the TLS half (16), the VirtualFs trio (6), csrf_generate (2) and the Unicode NFC and confusables builtins (6); the first three are excluded for stated reasons, and the Unicode six are the next increment. Tests: pure_builtin_differential.rs (6 cases). The load-bearing one is the nested constructor pattern, ordered so a failing tag test precedes a succeeding one, plus a separate case asserting the BOUND PAYLOAD matches -- a nilai_kiri returning the sum rather than its contents would still pick the right arm and print the wrong number. Verified: 03_PROTO 3366/0 (+6), clippy clean on both workspaces, audit-docs.sh 0 discrepancies. --- 03_PROTO/crates/riina-codegen/src/emit.rs | 65 +++++ 03_PROTO/crates/riina-codegen/src/lib.rs | 23 ++ 03_PROTO/crates/riina-codegen/src/lower.rs | 36 ++- 03_PROTO/crates/riina-typechecker/src/lib.rs | 29 +- .../riina-typechecker/tests/stdlib_doc.rs | 38 ++- .../riinac/tests/pure_builtin_differential.rs | 255 ++++++++++++++++++ docs/api/STDLIB.md | 57 ++-- website/public/metrics.json | 12 +- 8 files changed, 464 insertions(+), 51 deletions(-) create mode 100644 03_PROTO/crates/riinac/tests/pure_builtin_differential.rs diff --git a/03_PROTO/crates/riina-codegen/src/emit.rs b/03_PROTO/crates/riina-codegen/src/emit.rs index dc49d56d..e23cfd6e 100644 --- a/03_PROTO/crates/riina-codegen/src/emit.rs +++ b/03_PROTO/crates/riina-codegen/src/emit.rs @@ -4805,6 +4805,71 @@ static riina_value_t* riina_builtin_deserialize_safe(riina_value_t* arg) { self.writeln("}"); self.writeln(""); + // Range constructors and sum introspection. + // + // The four sum helpers are NOT a stdlib convenience — they are compiler + // internals. `parse_module_path`'s if-chain pattern compiler emits them + // for a constructor pattern nested where a `Case` cannot go, e.g. + // `(Ada(a), Tiada)` inside a tuple pattern. Until they were routed, that + // whole class of pattern ran under `riinac run` and failed `riinac build` + // with `Codegen Error: unbound variable: nilai_kiri` — a LANGUAGE feature + // that did not compile, surfacing as a missing builtin. + // + // `nilai_kiri`/`nilai_kanan` are deliberately LENIENT, matching the + // interpreter: a non-matching or non-sum argument yields the value + // itself rather than aborting. The generated code only projects a + // payload after the corresponding `adalah_*` tag test has passed, so the + // lenient arms are unreachable from generated code — but a hand-written + // call must behave the same in both backends. + self.writeln( + r####" +static riina_value_t* riina_builtin_julat(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* a = arg->data.pair_val.fst; + riina_value_t* b = arg->data.pair_val.snd; + if (a->tag != RIINA_TAG_INT || b->tag != RIINA_TAG_INT) abort(); + riina_list_t l = riina_list_new(); + for (uint64_t i = a->data.int_val; i < b->data.int_val; i++) { + riina_list_push(&l, riina_int(i)); + } + return riina_make_list(l); +} + +/* Inclusive of the upper bound. The interpreter uses a SATURATING increment, so + an upper bound of UINT64_MAX yields the same list as the exclusive form + rather than wrapping to an empty one. */ +static riina_value_t* riina_builtin_julat_inklusif(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* a = arg->data.pair_val.fst; + riina_value_t* b = arg->data.pair_val.snd; + if (a->tag != RIINA_TAG_INT || b->tag != RIINA_TAG_INT) abort(); + uint64_t hi = b->data.int_val; + uint64_t end = (hi == 0xFFFFFFFFFFFFFFFFULL) ? hi : hi + 1; + riina_list_t l = riina_list_new(); + for (uint64_t i = a->data.int_val; i < end; i++) { + riina_list_push(&l, riina_int(i)); + } + return riina_make_list(l); +} + +static riina_value_t* riina_builtin_adalah_kiri(riina_value_t* arg) { + return riina_bool(arg->tag == RIINA_TAG_SUM_LEFT); +} +static riina_value_t* riina_builtin_adalah_kanan(riina_value_t* arg) { + return riina_bool(arg->tag == RIINA_TAG_SUM_RIGHT); +} +static riina_value_t* riina_builtin_nilai_kiri(riina_value_t* arg) { + if (arg->tag == RIINA_TAG_SUM_LEFT || arg->tag == RIINA_TAG_SUM_RIGHT) { + return arg->data.sum_val; + } + return arg; +} +static riina_value_t* riina_builtin_nilai_kanan(riina_value_t* arg) { + return riina_builtin_nilai_kiri(arg); +} +"####, + ); + // log2: Int -> Int self.writeln("static riina_value_t* riina_builtin_log2(riina_value_t* arg) {"); self.writeln(" if (arg->tag != RIINA_TAG_INT) abort();"); diff --git a/03_PROTO/crates/riina-codegen/src/lib.rs b/03_PROTO/crates/riina-codegen/src/lib.rs index adaca4a5..1b3f234d 100644 --- a/03_PROTO/crates/riina-codegen/src/lib.rs +++ b/03_PROTO/crates/riina-codegen/src/lib.rs @@ -150,6 +150,29 @@ pub fn wasm_supports_builtin(name: &str) -> bool { pub fn codegen_supports_builtin(name: &str) -> bool { lower::builtin_canonical(name).is_some() } + +/// Whether the reference INTERPRETER binds `name` — i.e. whether `riinac run` +/// can execute a call to it. +/// +/// This exists because "the typechecker accepts it" and "something can run it" +/// are different questions, and the Backend column in `docs/api/STDLIB.md` was +/// silently conflating them. Its `interp-only` cell promised "`riinac run` +/// only", which for the eight crypto-agility builtins +/// (`guna_kripto`/`use_crypto`, `pilih_algo`/`select_algorithm`, +/// `cipher`/`sifer`, `hash_dengan`/`hash_with`) was FALSE: they are registered +/// in the typechecker with `Fn(Teks, Any, Kripto)` and carry the REQ-48 +/// deprecation check at their call sites, but no runtime binds them, so +/// `riinac run` fails with `unbound variable` exactly as `riinac build` does. +/// A doc that says a builtin runs somewhere it does not is worse than one that +/// says nothing, so the column now distinguishes the two. +/// +/// Derived by building the real interpreter environment and looking the name +/// up, not from a list — a list would drift the moment a runtime is added. +pub fn interpreter_supports_builtin(name: &str) -> bool { + builtins::register_builtins(&value::Env::new()) + .lookup(name) + .is_some() +} pub use value::Value; /// Result type for code generation operations diff --git a/03_PROTO/crates/riina-codegen/src/lower.rs b/03_PROTO/crates/riina-codegen/src/lower.rs index 480ebed2..65793e06 100644 --- a/03_PROTO/crates/riina-codegen/src/lower.rs +++ b/03_PROTO/crates/riina-codegen/src/lower.rs @@ -79,7 +79,11 @@ pub(crate) fn builtin_canonical(name: &str) -> Option<&'static str> { // I/O match name { "cetak" | "print" => return Some("cetak"), - "cetakln" | "println" => return Some("cetakln"), + // `cetak_baris` is a third spelling of `cetakln` — the interpreter binds + // all three to the same `Value::Builtin("cetakln")`. Only this gate did + // not know it, so a program using that spelling ran and then failed to + // build. A pure aliasing gap, not a missing implementation. + "cetakln" | "println" | "cetak_baris" => return Some("cetakln"), // String "gabung_teks" | "concat" => return Some("gabung_teks"), "panjang" | "length" => return Some("panjang"), @@ -105,6 +109,36 @@ pub(crate) fn builtin_canonical(name: &str) -> Option<&'static str> { "punca" | "sqrt" => return Some("punca"), "gcd" => return Some("gcd"), "lcm" => return Some("lcm"), + // `baki`/`rem` and `log2` had C implementations in emit.rs all along; + // only this gate was missing, so they were unreachable from a compiled + // program. `baki` additionally needed its TYPE corrected — it was + // declared unary and so could not be called from any well-typed program + // at all (see the note in riina-typechecker's math section). + "baki" | "rem" => return Some("baki"), + "log2" => return Some("log2"), + // `rawak`/`random`. Routed even though the two backends CANNOT be held + // to byte equality — both are time-seeded, so a differential can only + // pin the range invariant, and `pure_builtin_differential` says so + // rather than pretending otherwise. Routing is still right: without it + // a compiled RIINA program has no source of randomness at all, and + // neither implementation claims to be a CSPRNG (the interpreter hashes + // the clock, the emitted C runs an LCG). Anything needing cryptographic + // randomness must come from `riina-core`, not from here. + "rawak" | "random" => return Some("rawak"), + // Range constructors behind the `a..b` / `a..=b` surface syntax. + "julat" => return Some("julat"), + "julat_inklusif" => return Some("julat_inklusif"), + // Sum introspection. COMPILER INTERNALS, not stdlib: the parser's + // if-chain pattern compiler emits these for a constructor pattern nested + // where a `Case` cannot go, such as `(Ada(a), Tiada)` inside a tuple + // pattern. Leaving them unrouted meant that whole class of pattern ran + // under `riinac run` and failed `riinac build` with + // `unbound variable: nilai_kiri` — a language feature that did not + // compile, wearing the costume of a missing builtin. + "adalah_kiri" => return Some("adalah_kiri"), + "adalah_kanan" => return Some("adalah_kanan"), + "nilai_kiri" => return Some("nilai_kiri"), + "nilai_kanan" => return Some("nilai_kanan"), // Test "tegaskan" | "assert" => return Some("tegaskan"), "tegaskan_sama" | "assert_eq" => return Some("tegaskan_sama"), diff --git a/03_PROTO/crates/riina-typechecker/src/lib.rs b/03_PROTO/crates/riina-typechecker/src/lib.rs index 7717cb29..0411385e 100644 --- a/03_PROTO/crates/riina-typechecker/src/lib.rs +++ b/03_PROTO/crates/riina-typechecker/src/lib.rs @@ -1486,16 +1486,31 @@ pub fn register_builtin_types(ctx: &Context) -> Context { } // ── Extra math builtins ── - for (bm, en) in &[("baki", "rem"), ("log2", "log2")] { + // + // `baki`/`rem` are BINARY and take a pair, like `minimum`/`maksimum`/`kuasa`. + // They were previously typed `Nombor -> Nombor` because they shared this + // loop with the genuinely unary `log2`, which made them **uncallable from + // any well-typed program**: `baki(10, 3)` is `App(App(baki, 10), 3)` and + // failed with "Expected function type, found Int", while `baki((10, 3))` + // failed with "expected Int, found Prod(Int, Int)". Both the interpreter + // (`matematik.rs`, `extract_pair_ints`) and the emitted C + // (`riina_builtin_baki`, which requires `RIINA_TAG_PAIR`) have always taken + // a pair, so the type was the single odd one out. + for nm in ["baki", "rem"] { c = c.extend( - bm.to_string(), - Ty::Fn(Box::new(Ty::Int), Box::new(Ty::Int), Effect::Pure), - ); - c = c.extend( - en.to_string(), - Ty::Fn(Box::new(Ty::Int), Box::new(Ty::Int), Effect::Pure), + nm.to_string(), + Ty::Fn( + Box::new(Ty::Prod(Box::new(Ty::Int), Box::new(Ty::Int))), + Box::new(Ty::Int), + Effect::Pure, + ), ); } + // `log2` really is unary — it is what the loop above was written for. + c = c.extend( + "log2".to_string(), + Ty::Fn(Box::new(Ty::Int), Box::new(Ty::Int), Effect::Pure), + ); // Random — Effect::Random c = c.extend( "rawak".to_string(), diff --git a/03_PROTO/crates/riina-typechecker/tests/stdlib_doc.rs b/03_PROTO/crates/riina-typechecker/tests/stdlib_doc.rs index 702be654..3ecf09c8 100644 --- a/03_PROTO/crates/riina-typechecker/tests/stdlib_doc.rs +++ b/03_PROTO/crates/riina-typechecker/tests/stdlib_doc.rs @@ -11,7 +11,9 @@ //! Regenerate after changing the builtin table: //! REGEN_STDLIB_DOC=1 cargo test -p riina-typechecker --test stdlib_doc -use riina_codegen::{codegen_supports_builtin, wasm_supports_builtin}; +use riina_codegen::{ + codegen_supports_builtin, interpreter_supports_builtin, wasm_supports_builtin, +}; use riina_fmt::format_ty; use riina_typechecker::{register_builtin_types, Context}; use riina_types::{Effect, Ty}; @@ -29,8 +31,19 @@ enum Backend { Wasm, /// Compiles to C; the WASM backend refuses it (fails closed). Native, - /// Neither: `riinac run` only. + /// Neither compiles, but the interpreter binds it: `riinac run` only. Interp, + /// NOTHING runs it. The typechecker accepts the call — the name is in the + /// builtin type registry — but no interpreter or backend binds it, so every + /// path fails with `unbound variable`. + /// + /// This state was added because `interp-only` was making a FALSE promise for + /// the eight crypto-agility builtins: its cell reads "`riinac run` only", + /// and `riinac run` cannot run them either. A three-state column had no way + /// to say "typed but unimplemented", so it said the nearest thing, which was + /// wrong. A doc claiming a builtin runs somewhere it does not is worse than + /// one that says nothing. + TypedOnly, } impl Backend { @@ -39,8 +52,10 @@ impl Backend { Self::Wasm } else if codegen_supports_builtin(name) { Self::Native - } else { + } else if interpreter_supports_builtin(name) { Self::Interp + } else { + Self::TypedOnly } } @@ -49,6 +64,7 @@ impl Backend { Self::Wasm => "compiled", Self::Native => "**native-only**", Self::Interp => "**interp-only**", + Self::TypedOnly => "**typed-only**", } } } @@ -112,7 +128,11 @@ fn generate() -> String { let wasm_count = rows.iter().filter(|(_, _, _, b)| *b == Backend::Wasm).count(); let native_count = rows.iter().filter(|(_, _, _, b)| *b == Backend::Native).count(); let compiled_count = wasm_count + native_count; - let interp_only_count = rows.len() - compiled_count; + let interp_only_count = rows.iter().filter(|(_, _, _, b)| *b == Backend::Interp).count(); + let typed_only_count = rows + .iter() + .filter(|(_, _, _, b)| *b == Backend::TypedOnly) + .count(); // Group by effect; render an effect section ordered by the effect enum. let effect_order = [ @@ -163,13 +183,14 @@ fn generate() -> String { // then cannot be built. State it before the tables, not after. out.push_str(&format!( "## ⚠ Read first: type-checking does not imply compiling\n\n\ - Every builtin below type-checks and runs under `riinac run` (the \ - interpreter). Only **{compiled}** of the {total} also compile, and they \ - do NOT all reach the same backends:\n\n\ + Every builtin below type-checks. That is ALL it means: type-checking \ + does not imply compiling, and it does not even imply running. \ + **{compiled}** of the {total} compile:\n\n\ | Backend value | Meaning |\n|---|---|\n\ | `compiled` | Lowers to C **and** WASM ({wasm} builtins). |\n\ | `native-only` | Lowers to C. The WASM backend **refuses** it ({native} builtins). |\n\ - | `interp-only` | `riinac run` only ({interp} builtins). `riinac build` fails with `unbound variable`. |\n\n\ + | `interp-only` | `riinac run` only ({interp} builtins). `riinac build` fails with `unbound variable`. |\n\ + | `typed-only` | **Nothing runs it** ({typed} builtins). The name is in the type registry, but neither the interpreter nor any backend binds it, so `riinac run` fails with `unbound variable` too. |\n\n\ ```\n\ $ riinac check baca.rii # Success! Effect: FileSystem\n\ $ riinac run baca.rii # works — reads the file\n\ @@ -198,6 +219,7 @@ fn generate() -> String { native = native_count, total = rows.len(), interp = interp_only_count, + typed = typed_only_count, )); out.push_str( "*Scope note:* this lists the language builtins the typechecker installs. \ diff --git a/03_PROTO/crates/riinac/tests/pure_builtin_differential.rs b/03_PROTO/crates/riinac/tests/pure_builtin_differential.rs new file mode 100644 index 00000000..bfeec5cf --- /dev/null +++ b/03_PROTO/crates/riinac/tests/pure_builtin_differential.rs @@ -0,0 +1,255 @@ +// Copyright (c) 2026 The RIINA Authors. All rights reserved. + +//! Interpreter/C differential for the last unrouted PURE builtins — master plan +//! REQ-70 family routing. +//! +//! # These were not a family, they were three defects wearing a family's clothes +//! +//! REQ-70's remaining interpreter-only set was described as a backlog of +//! builtins nobody had looked at yet. Looking at them found that most were not +//! missing implementations at all: +//! +//! 1. **`cetak_baris` was a pure aliasing gap.** The interpreter binds +//! `cetakln`, `println` AND `cetak_baris` to the same +//! `Value::Builtin("cetakln")`. Only `lower::builtin_canonical` knew two of +//! the three, so a program using the third ran and then failed to build. +//! +//! 2. **`baki`/`rem` were UNCALLABLE from any well-typed program.** They are +//! binary and take a pair — the interpreter's `extract_pair_ints` and the +//! emitted C's `RIINA_TAG_PAIR` check agree on that — but the typechecker +//! declared them `Nombor -> Nombor`, because they shared a registration loop +//! with the genuinely unary `log2`. So `baki(10, 3)` failed with "Expected +//! function type, found Int" and `baki((10, 3))` failed with "expected Int, +//! found Prod(Int, Int)". Two of the three components agreed and the type was +//! the outlier, which is why the fix is to the type. +//! +//! 3. **`baki` and `log2` already had C.** `riina_builtin_baki` and +//! `riina_builtin_log2` sat in `emit.rs` unreferenced, like the `json` +//! helpers before them. Only the routing gate was missing. +//! +//! # The load-bearing case is [`nested_constructor_pattern_compiles`] +//! +//! `adalah_kiri`/`adalah_kanan`/`nilai_kiri`/`nilai_kanan` are not stdlib +//! functions a user calls. They are COMPILER INTERNALS: the parser's if-chain +//! pattern compiler emits them for a constructor pattern nested somewhere a +//! `Case` cannot go, such as `(Ada(a), Tiada)` inside a tuple pattern. Leaving +//! them unrouted meant that entire class of pattern ran under `riinac run` and +//! failed `riinac build` with `Codegen Error: unbound variable: nilai_kiri`. +//! +//! That is a LANGUAGE FEATURE that did not compile, surfacing in the Backend +//! column as four obscure `interp-only` builtins. It is the reason this file +//! exists, and the reason "unexamined builtins" was the wrong description. + +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) — pure-builtin 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." + ); +} + +/// Run `src_body` under both backends and assert the program's own output +/// matches byte for byte. +fn assert_backends_agree(tag: &str, program: &str) { + if !require_cc() { + return; + } + let dir = std::env::temp_dir().join(format!("riina_req70_pure_{tag}_{}", std::process::id())); + let _ = std::fs::remove_dir_all(&dir); + std::fs::create_dir_all(&dir).expect("create dir"); + let stem = format!("req70_pure_{tag}"); + let src: PathBuf = dir.join(format!("{stem}.rii")); + std::fs::write(&src, program).expect("write program"); + + let interp = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("run") + .arg(&src) + .output() + .expect("riinac run"); + assert!( + interp.status.success(), + "interpreter failed for {tag}: {}{}", + String::from_utf8_lossy(&interp.stdout), + String::from_utf8_lossy(&interp.stderr) + ); + // `riinac run` appends the program's final value as a trailing LINE. + let raw = String::from_utf8_lossy(&interp.stdout).into_owned(); + let mut lines: Vec<&str> = raw.lines().collect(); + lines.pop(); + let interp_out = if lines.is_empty() { + String::new() + } else { + format!("{}\n", lines.join("\n")) + }; + + let build = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("build") + .arg(&src) + .output() + .expect("riinac build"); + assert!( + build.status.success(), + "compile failed for {tag}: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + let run = Command::new(dir.join(&stem)).output().expect("run binary"); + assert!( + run.status.success(), + "compiled binary failed for {tag} (exit {:?}): {}{}", + run.status.code(), + String::from_utf8_lossy(&run.stdout), + String::from_utf8_lossy(&run.stderr) + ); + let c_out = String::from_utf8_lossy(&run.stdout).into_owned(); + + assert_eq!( + interp_out, c_out, + "interp/C divergence for {tag}\n interp: {interp_out:?}\n C: {c_out:?}" + ); + + let _ = std::fs::remove_dir_all(&dir); +} + +/// THE regression this increment exists for: a constructor pattern nested inside +/// a tuple pattern. Before the four sum helpers were routed this program ran +/// under `riinac run` and `riinac build` failed with +/// `Codegen Error: unbound variable: nilai_kiri`. +/// +/// The arms are ordered so the SECOND one matches, which forces the generated +/// code to evaluate a failing `adalah_kanan` tag test and then a succeeding one +/// — exercising both tag helpers and the payload projection, not just the arm +/// that happens to win. +#[test] +fn nested_constructor_pattern_compiles() { + assert_backends_agree( + "nestedctor", + "fungsi bungkus(n: Nombor) -> Mungkin kesan Bersih {\n\ + \x20 kalau n > 0 { Ada(n) } lain { Tiada }\n\ + }\n\ + fungsi utama() -> Nombor kesan Tulis {\n\ + \x20 biar pab = (bungkus(1), bungkus(2));\n\ + \x20 biar pa = (bungkus(1), bungkus(0));\n\ + \x20 biar pnone = (bungkus(0), bungkus(0));\n\ + \x20 cetakln(padan pab { (Ada(a), Ada(b)) => \"kedua\", (Ada(a), Tiada) => \"pertama\", _ => \"tiada\" });\n\ + \x20 cetakln(padan pa { (Ada(a), Ada(b)) => \"kedua\", (Ada(a), Tiada) => \"pertama\", _ => \"tiada\" });\n\ + \x20 cetakln(padan pnone { (Ada(a), Ada(b)) => \"kedua\", (Ada(a), Tiada) => \"pertama\", _ => \"tiada\" });\n\ + \x20 0\n\ + }\n", + ); +} + +/// The payload BOUND by a nested pattern must be the same value in both +/// backends, not merely the same arm. A `nilai_kiri` that returned the sum +/// rather than its contents would still pick the right arm and print the wrong +/// number. +#[test] +fn nested_constructor_pattern_binds_the_same_payload() { + assert_backends_agree( + "nestedbind", + "fungsi bungkus(n: Nombor) -> Mungkin kesan Bersih {\n\ + \x20 kalau n > 0 { Ada(n) } lain { Tiada }\n\ + }\n\ + fungsi utama() -> Nombor kesan Tulis {\n\ + \x20 biar p = (bungkus(7), bungkus(35));\n\ + \x20 cetakln(ke_teks(padan p { (Ada(a), Ada(b)) => b / a, _ => 0 }));\n\ + \x20 0\n\ + }\n", + ); +} + +/// `baki`/`rem` after the type correction. The zero case is left out +/// deliberately: both backends abort on modulo-by-zero, which is agreement of a +/// different kind and belongs in a both-must-fail test, not here. +#[test] +fn modulo_and_log2_agree() { + assert_backends_agree( + "math", + "fungsi utama() -> Nombor kesan Tulis {\n\ + \x20 cetakln(ke_teks(baki((10, 3))));\n\ + \x20 cetakln(ke_teks(baki((9, 3))));\n\ + \x20 cetakln(ke_teks(rem((255, 16))));\n\ + \x20 cetakln(ke_teks(log2(1)));\n\ + \x20 cetakln(ke_teks(log2(1024)));\n\ + \x20 cetakln(ke_teks(log2(1023)));\n\ + \x20 0\n\ + }\n", + ); +} + +/// Ranges, including the two boundaries a naive C loop gets wrong: an EMPTY +/// range (`lo >= hi`) and the inclusive form's extra element. +#[test] +fn ranges_agree_including_the_empty_case() { + assert_backends_agree( + "range", + "fungsi utama() -> Nombor kesan Tulis {\n\ + \x20 cetakln(ke_teks(julat((1, 5))));\n\ + \x20 cetakln(ke_teks(julat_inklusif((1, 5))));\n\ + \x20 cetakln(ke_teks(julat((5, 5))));\n\ + \x20 cetakln(ke_teks(julat_inklusif((5, 5))));\n\ + \x20 cetakln(ke_teks(julat((7, 3))));\n\ + \x20 cetakln(ke_teks(senarai_panjang(julat((0, 10)))));\n\ + \x20 0\n\ + }\n", + ); +} + +/// `cetak_baris` is the third spelling of `cetakln`, and must be the same +/// function — including the newline — in both backends. +#[test] +fn cetak_baris_is_cetakln_in_both() { + assert_backends_agree( + "alias", + "fungsi utama() -> Nombor kesan Tulis {\n\ + \x20 cetakln(\"satu\");\n\ + \x20 cetak_baris(\"dua\");\n\ + \x20 println(\"tiga\");\n\ + \x20 0\n\ + }\n", + ); +} + +/// `rawak`/`random` is the one routed member whose backends CANNOT be compared +/// by output: both are time-seeded, so equality would be a coin flip dressed as +/// a test. What is pinned instead is the invariant each must satisfy — every +/// draw lands in `[0, n)` — checked inside the program so both backends assert +/// it themselves, plus the fact that a compiled program can obtain randomness at +/// all, which before routing it could not. +/// +/// Neither implementation is a CSPRNG and neither claims to be (the interpreter +/// hashes the clock; the emitted C runs an LCG). Anything needing cryptographic +/// randomness must come from `riina-core`. +#[test] +fn random_stays_in_range_in_both_backends() { + assert_backends_agree( + "rawak", + "fungsi utama() -> Nombor kesan (Rawak | Tulis) {\n\ + \x20 biar a = rawak(10);\n\ + \x20 biar b = rawak(1);\n\ + \x20 cetakln(ke_teks(a < 10));\n\ + \x20 cetakln(ke_teks(b));\n\ + \x20 0\n\ + }\n", + ); +} diff --git a/docs/api/STDLIB.md b/docs/api/STDLIB.md index 1d241d7b..3c90a6df 100644 --- a/docs/api/STDLIB.md +++ b/docs/api/STDLIB.md @@ -6,13 +6,14 @@ 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 **323** of the 373 also compile, and they do NOT all reach the same backends: +Every builtin below type-checks. That is ALL it means: type-checking does not imply compiling, and it does not even imply running. **335** of the 373 compile: | Backend value | Meaning | |---|---| -| `compiled` | Lowers to C **and** WASM (20 builtins). | -| `native-only` | Lowers to C. The WASM backend **refuses** it (303 builtins). | -| `interp-only` | `riinac run` only (50 builtins). `riinac build` fails with `unbound variable`. | +| `compiled` | Lowers to C **and** WASM (21 builtins). | +| `native-only` | Lowers to C. The WASM backend **refuses** it (314 builtins). | +| `interp-only` | `riinac run` only (30 builtins). `riinac build` fails with `unbound variable`. | +| `typed-only` | **Nothing runs it** (8 builtins). The name is in the type registry, but neither the interpreter nor any backend binds it, so `riinac run` fails with `unbound variable` too. | ``` $ riinac check baca.rii # Success! Effect: FileSystem @@ -30,20 +31,20 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Bersih (Pure) -> **Mixed:** 214 of 229 compile; the rest are interpreter-only (REQ-70). +> **Mixed:** 223 of 229 compile; the rest are interpreter-only (REQ-70). | Builtin | Type | Backend | |---|---|---| | `abs` | `Fn(Nombor, Nombor)` | **native-only** | -| `adalah_kanan` | `Fn(Any, Benar)` | **interp-only** | +| `adalah_kanan` | `Fn(Any, Benar)` | **native-only** | | `adalah_keliru` | `Fn((Teks, Teks), Benar)` | **interp-only** | -| `adalah_kiri` | `Fn(Any, Benar)` | **interp-only** | +| `adalah_kiri` | `Fn(Any, Benar)` | **native-only** | | `assert` | `Fn(Benar, ())` | **native-only** | | `assert_eq` | `Fn((Any, Any), ())` | **native-only** | | `assert_false` | `Fn(Benar, ())` | **native-only** | | `assert_ne` | `Fn((Any, Any), ())` | **native-only** | | `assert_true` | `Fn(Benar, ())` | **native-only** | -| `baki` | `Fn(Nombor, Nombor)` | **interp-only** | +| `baki` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | | `besar` | `Fn(Teks, Besar)` | compiled | | `bigint` | `Fn(Teks, Besar)` | compiled | | `binary_fixed` | `Fn((Teks, Nombor), Qmn)` | compiled | @@ -90,8 +91,8 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `json_stringify` | `Fn(Any, Any)` | **native-only** | | `json_urai` | `Fn(Any, Any)` | **native-only** | | `json_urai_selamat` | `Fn(Disanitasi, Any)` | **native-only** | -| `julat` | `Fn((Nombor, Nombor), Senarai)` | **interp-only** | -| `julat_inklusif` | `Fn((Nombor, Nombor), Senarai)` | **interp-only** | +| `julat` | `Fn((Nombor, Nombor), Senarai)` | **native-only** | +| `julat_inklusif` | `Fn((Nombor, Nombor), Senarai)` | **native-only** | | `ke_bool` | `Fn(Any, Benar)` | **native-only** | | `ke_nfc` | `Fn(Teks, Teks)` | **interp-only** | | `ke_nombor` | `Fn(Teks, Nombor)` | **native-only** | @@ -117,7 +118,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `list_tail` | `Fn(Any, Any)` | **native-only** | | `list_unique` | `Fn(Any, Any)` | **native-only** | | `list_zip` | `Fn(Any, Any)` | **native-only** | -| `log2` | `Fn(Nombor, Nombor)` | **interp-only** | +| `log2` | `Fn(Nombor, Nombor)` | **native-only** | | `maksimum` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | | `map_contains` | `Fn(Any, Any)` | **native-only** | | `map_get` | `Fn(Any, Any)` | **native-only** | @@ -133,8 +134,8 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `money` | `Fn(Teks, Wang)` | compiled | | `mutlak` | `Fn(Nombor, Nombor)` | **native-only** | | `nfc` | `Fn(Teks, Teks)` | **interp-only** | -| `nilai_kanan` | `Fn(Any, Any)` | **interp-only** | -| `nilai_kiri` | `Fn(Any, Any)` | **interp-only** | +| `nilai_kanan` | `Fn(Any, Any)` | **native-only** | +| `nilai_kiri` | `Fn(Any, Any)` | **native-only** | | `nombor_ke_teks` | `Fn(Nombor, Teks)` | compiled | | `normal_unicode` | `Fn(Tercemar, Tercemar)` | **native-only** | | `normalize_unicode` | `Fn(Tercemar, Tercemar)` | **native-only** | @@ -154,7 +155,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `punca` | `Fn(Nombor, Nombor)` | **native-only** | | `qmn` | `Fn((Teks, Nombor), Qmn)` | compiled | | `rangka` | `Fn(Teks, Teks)` | **interp-only** | -| `rem` | `Fn(Nombor, Nombor)` | **interp-only** | +| `rem` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | | `sahkan_panjang` | `Fn((Tercemar, Nombor), Mungkin>)` | **native-only** | | `sahkan_url` | `Fn(Tercemar, Disanitasi)` | **native-only** | | `sanitasi_css` | `Fn(Tercemar, Disanitasi)` | **native-only** | @@ -277,12 +278,12 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Tulis (Write) -> **Mixed:** 8 of 13 compile; the rest are interpreter-only (REQ-70). +> **Mixed:** 9 of 13 compile; the rest are interpreter-only (REQ-70). | Builtin | Type | Backend | |---|---|---| | `cetak` | `Fn(Any, (), Tulis)` | compiled | -| `cetak_baris` | `Fn(Any, (), Tulis)` | **interp-only** | +| `cetak_baris` | `Fn(Any, (), Tulis)` | compiled | | `cetakln` | `Fn(Any, (), Tulis)` | compiled | | `fail_buang_selamat` | `Fn(Disanitasi, Benar, Tulis)` | **native-only** | | `fail_tulis_selamat` | `Fn((Disanitasi, Any), (), Tulis)` | **native-only** | @@ -400,29 +401,27 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Kripto (Crypto) -> **Entirely interpreter-only.** No builtin in this section compiles — a program using any of them runs under `riinac run` but cannot be built for native or WASM (REQ-70). - | Builtin | Type | Backend | |---|---|---| -| `cipher` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `guna_kripto` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `hash_dengan` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `hash_with` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `pilih_algo` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `select_algorithm` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `sifer` | `Fn(Teks, Any, Kripto)` | **interp-only** | -| `use_crypto` | `Fn(Teks, Any, Kripto)` | **interp-only** | +| `cipher` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `guna_kripto` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `hash_dengan` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `hash_with` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `pilih_algo` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `select_algorithm` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `sifer` | `Fn(Teks, Any, Kripto)` | **typed-only** | +| `use_crypto` | `Fn(Teks, Any, Kripto)` | **typed-only** | ## Rawak (Random) -> **Entirely interpreter-only.** No builtin in this section compiles — a program using any of them runs under `riinac run` but cannot be built for native or WASM (REQ-70). +> **Mixed:** 2 of 4 compile; the rest are interpreter-only (REQ-70). | Builtin | Type | Backend | |---|---|---| | `csrf_generate` | `Fn((), Teks, Rawak)` | **interp-only** | | `csrf_jana` | `Fn((), Teks, Rawak)` | **interp-only** | -| `random` | `Fn(Nombor, Nombor, Rawak)` | **interp-only** | -| `rawak` | `Fn(Nombor, Nombor, Rawak)` | **interp-only** | +| `random` | `Fn(Nombor, Nombor, Rawak)` | **native-only** | +| `rawak` | `Fn(Nombor, Nombor, Rawak)` | **native-only** | ## Sistem (System) diff --git a/website/public/metrics.json b/website/public/metrics.json index a0402a0c..a75145c5 100644 --- a/website/public/metrics.json +++ b/website/public/metrics.json @@ -1,11 +1,11 @@ { - "generated": "2026-08-20T10:14:37Z", - "generatedHuman": "August 20, 2026 at 10:14 UTC", + "generated": "2026-08-21T02:03:50Z", + "generatedHuman": "August 21, 2026 at 02:03 UTC", "version": "0.4.0", "session": 0, "git": { - "commit": "ec793e0a8", - "branch": "main" + "commit": "cd76403d4", + "branch": "claude/continue-solution-4gn31y" }, "proofs": { "qedActive": 12678, @@ -196,8 +196,8 @@ "rust": { "tests": 3360, "testsVerified": 3360, - "testsEstimated": 0, - "testsSource": "full_cargo_test", + "testsEstimated": 3362, + "testsSource": "cached_verified", "crates": 20 }, "examples": 169, From 286a2a3d26fe27079bba35855fe36de593a57c00 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 21 Aug 2026 02:21:11 +0000 Subject: [PATCH 2/4] [TRACK_B] FEAT: route the Unicode builtins behind the emitter's first conditional prelude REQ-70. Routes nfc/ke_nfc (UAX #15), skeleton/rangka and adalah_keliru/is_confusable (UTS #39) -- the last group with no stated reason to stay interpreter-only. 341 of 373 builtins now compile. The Gate C sample app 07_EXAMPLES/03_applications/keselamatan_nama.rii NOW COMPILES. It was one of four apps the gate cites as shipping evidence and the only one that would not build; verified by command, and its compiled output is byte-identical to `riinac run`. WHY THIS NEEDED A CONDITIONAL BLOCK. Every other builtin's C is a few dozen lines. These need ~250 KB of vendored UCD tables. The emitted prelude is already ~228 KB for a hello-world and is otherwise entirely unconditional, so emitting the tables always would MORE THAN DOUBLE every compiled binary to serve three builtins most programs never call. emit() now scans the IR for a call to one of the three and emits the block only then. Measured: hello-world stays 229,600 bytes with zero tables; a program calling nfc gets 492,515. THE TABLES ARE GENERATED, NOT TRANSCRIBED. The C arrays are written out from the same unicode_nfc_data / unicode_confusables_data statics the interpreter reads. A hand-copied 250 KB table is a drift source no differential could realistically cover; generating it means the two backends cannot disagree about the DATA at all -- only about the ALGORITHM, which is ~150 lines and is what the tests actually exercise. A NEGATIVE CONTROL CAUGHT A TEST THAT PASSED FOR THE WRONG REASON. The blocking case was first written as `a` + dot-below + acute, on the reasoning that the acute cannot reach the starter past a lower-class mark. Deleting the blocking condition from the emitted C did NOT make that test fail: there both marks compose into the starter in turn, so blocking never applies. Rewritten as `a` + U+0305 overline + U+0301 acute -- equal combining classes, and the overline does not compose -- where removing the check composes `a`+acute across the overline and shortens the result from five bytes to four. Re-ran the control: the test now fails as intended. Recorded in the test's own comment so the input is not "simplified" back later. Cases chosen where the ALGORITHM decides rather than the data: Hangul (composed and decomposed arithmetically, so it appears in no table -- a lookup-only port leaves it decomposed); stable canonical ordering; the blocking rule above; and that skeleton ends in NFD, not NFC, because it is a comparison key rather than a display form. Plus hello_world_carries_no_ucd_tables, which keeps the conditional-emission promise honest -- without it the block would silently become unconditional again and nothing else would notice, the binaries would just get bigger. Every remaining interp-only builtin now has a stated reason: the TLS half (16, awaiting the Law 8 decision), the VirtualFs trio (6, needs an in-memory FS and quota in C), and csrf_generate (2, non-deterministic). Counts re-derived from the regenerated doc: compiled 21 / native-only 320 / interp-only 24 / typed-only 8. Verified: 03_PROTO 3373/0 (+7), 05_TOOLING 323/0, clippy clean on both, audit-docs.sh 0 discrepancies. --- 03_PROTO/crates/riina-codegen/src/emit.rs | 357 ++++++++++++++++++ 03_PROTO/crates/riina-codegen/src/lower.rs | 7 + .../riinac/tests/unicode_differential.rs | 294 +++++++++++++++ docs/api/STDLIB.md | 20 +- website/public/metrics.json | 8 +- 5 files changed, 671 insertions(+), 15 deletions(-) create mode 100644 03_PROTO/crates/riinac/tests/unicode_differential.rs diff --git a/03_PROTO/crates/riina-codegen/src/emit.rs b/03_PROTO/crates/riina-codegen/src/emit.rs index e23cfd6e..e909119e 100644 --- a/03_PROTO/crates/riina-codegen/src/emit.rs +++ b/03_PROTO/crates/riina-codegen/src/emit.rs @@ -122,6 +122,23 @@ impl CEmitter { // Emit runtime support self.emit_runtime_prelude(); + // The Unicode runtime is the ONE part of the prelude emitted + // conditionally. Everything else is unconditional and already costs a + // hello-world ~228 KB of C; the vendored UCD tables would add ~250 KB + // MORE — more than doubling every binary — to serve three builtins most + // programs never call. So they are emitted only when the program + // actually calls one. + // + // The tables are written out FROM the same Rust statics the interpreter + // reads (`unicode_nfc_data`, `unicode_confusables_data`), not + // transcribed. A hand-copied 250 KB table is a drift source no + // differential could realistically cover; generating it means the two + // backends cannot disagree about the DATA, only about the algorithm, + // which is small enough to test properly. + if Self::program_uses_unicode(program) { + self.emit_unicode_runtime(); + } + // Collect forward declarations for func_id in program.functions.keys() { self.forward_decls.push(*func_id); @@ -141,6 +158,346 @@ impl CEmitter { Ok(self.output.clone()) } + + /// Canonical names of the builtins that need the Unicode runtime. + const UNICODE_BUILTINS: &'static [&'static str] = &["nfc", "skeleton", "adalah_keliru"]; + + /// Whether `program` calls any builtin that needs the UCD tables. + fn program_uses_unicode(program: &Program) -> bool { + program.functions.values().any(|f| { + f.blocks.iter().any(|b| { + b.instrs.iter().any(|i| { + matches!(&i.instr, crate::ir::Instruction::BuiltinCall { name, .. } + if Self::UNICODE_BUILTINS.contains(&name.as_str())) + }) + }) + }) + } + + /// Emit the UCD tables and the NFC / UTS-39 skeleton implementation. + /// + /// The TABLES are generated from the very statics the interpreter uses, so + /// the two backends read identical data by construction. Only the ALGORITHM + /// is written twice, and it is short: canonical decomposition (with the + /// algorithmic Hangul case), canonical ordering by combining class, + /// canonical composition, and the confusable prototype mapping. + fn emit_unicode_runtime(&mut self) { + use crate::unicode_confusables_data::{CONFUSABLE_DATA, CONFUSABLE_INDEX}; + use crate::unicode_nfc_data::{COMBINING_CLASS, COMPOSE, DECOMP_DATA, DECOMP_INDEX}; + + self.writeln("/* ══════════════════════════════════════════════════════════════════ */"); + self.writeln("/* UNICODE RUNTIME (UAX #15 NFC + UTS #39 skeleton) */"); + self.writeln("/* Emitted only for programs that call nfc/skeleton/adalah_keliru. */"); + self.writeln("/* Tables generated from riina-codegen's own UCD statics — the */"); + self.writeln("/* interpreter and this backend read the SAME data by construction. */"); + self.writeln("/* ══════════════════════════════════════════════════════════════════ */"); + self.writeln(""); + + // ── Tables ── + self.writeln(&format!( + "static const uint32_t riina_ucd_ccc[][2] = {{ /* {} */", + COMBINING_CLASS.len() + )); + for chunk in COMBINING_CLASS.chunks(8) { + let row: Vec = chunk + .iter() + .map(|(cp, cc)| format!("{{{cp:#x},{cc}}}")) + .collect(); + self.writeln(&format!("{},", row.join(","))); + } + self.writeln("};"); + self.writeln(&format!( + "#define RIINA_UCD_CCC_N {}", + COMBINING_CLASS.len() + )); + self.writeln(""); + + self.writeln(&format!( + "static const uint32_t riina_ucd_decomp_index[][3] = {{ /* {} */", + DECOMP_INDEX.len() + )); + for chunk in DECOMP_INDEX.chunks(6) { + let row: Vec = chunk + .iter() + .map(|(cp, off, len)| format!("{{{cp:#x},{off},{len}}}")) + .collect(); + self.writeln(&format!("{},", row.join(","))); + } + self.writeln("};"); + self.writeln(&format!( + "#define RIINA_UCD_DECOMP_INDEX_N {}", + DECOMP_INDEX.len() + )); + self.writeln(""); + + self.writeln(&format!( + "static const uint32_t riina_ucd_decomp_data[] = {{ /* {} */", + DECOMP_DATA.len() + )); + for chunk in DECOMP_DATA.chunks(12) { + let row: Vec = chunk.iter().map(|cp| format!("{cp:#x}")).collect(); + self.writeln(&format!("{},", row.join(","))); + } + self.writeln("};"); + self.writeln(""); + + self.writeln(&format!( + "static const uint32_t riina_ucd_compose[][3] = {{ /* {} */", + COMPOSE.len() + )); + for chunk in COMPOSE.chunks(6) { + let row: Vec = chunk + .iter() + .map(|(a, b, c)| format!("{{{a:#x},{b:#x},{c:#x}}}")) + .collect(); + self.writeln(&format!("{},", row.join(","))); + } + self.writeln("};"); + self.writeln(&format!("#define RIINA_UCD_COMPOSE_N {}", COMPOSE.len())); + self.writeln(""); + + self.writeln(&format!( + "static const uint32_t riina_ucd_conf_index[][3] = {{ /* {} */", + CONFUSABLE_INDEX.len() + )); + for chunk in CONFUSABLE_INDEX.chunks(6) { + let row: Vec = chunk + .iter() + .map(|(cp, off, len)| format!("{{{cp:#x},{off},{len}}}")) + .collect(); + self.writeln(&format!("{},", row.join(","))); + } + self.writeln("};"); + self.writeln(&format!( + "#define RIINA_UCD_CONF_INDEX_N {}", + CONFUSABLE_INDEX.len() + )); + self.writeln(""); + + self.writeln(&format!( + "static const uint32_t riina_ucd_conf_data[] = {{ /* {} */", + CONFUSABLE_DATA.len() + )); + for chunk in CONFUSABLE_DATA.chunks(12) { + let row: Vec = chunk.iter().map(|cp| format!("{cp:#x}")).collect(); + self.writeln(&format!("{},", row.join(","))); + } + self.writeln("};"); + self.writeln(""); + + // ── Algorithm ── + // + // Mirrors unicode_nfc.rs and unicode_confusables.rs. The parts a C + // author would get wrong on their own are called out inline. + self.writeln( + r####" +/* Hangul composes and decomposes arithmetically (UAX #15 §16) rather than by + table, so these 11172 syllables never appear in the decomposition data. */ +#define RIINA_HANGUL_S_BASE 0xAC00u +#define RIINA_HANGUL_L_BASE 0x1100u +#define RIINA_HANGUL_V_BASE 0x1161u +#define RIINA_HANGUL_T_BASE 0x11A7u +#define RIINA_HANGUL_L_COUNT 19u +#define RIINA_HANGUL_V_COUNT 21u +#define RIINA_HANGUL_T_COUNT 28u +#define RIINA_HANGUL_N_COUNT (RIINA_HANGUL_V_COUNT * RIINA_HANGUL_T_COUNT) +#define RIINA_HANGUL_S_COUNT (RIINA_HANGUL_L_COUNT * RIINA_HANGUL_N_COUNT) + +typedef struct { uint32_t* cps; size_t len; size_t cap; } riina_cpbuf_t; + +static void riina_cpbuf_push(riina_cpbuf_t* b, uint32_t cp) { + if (b->len >= b->cap) { + b->cap = b->cap ? b->cap * 2 : 32; + b->cps = (uint32_t*)realloc(b->cps, b->cap * sizeof(uint32_t)); + if (!b->cps) abort(); + } + b->cps[b->len++] = cp; +} + +static uint8_t riina_ucd_ccc_of(uint32_t cp) { + size_t lo = 0, hi = RIINA_UCD_CCC_N; + while (lo < hi) { + size_t mid = lo + (hi - lo) / 2; + if (riina_ucd_ccc[mid][0] == cp) return (uint8_t)riina_ucd_ccc[mid][1]; + if (riina_ucd_ccc[mid][0] < cp) lo = mid + 1; else hi = mid; + } + return 0; +} + +/* Full (recursive) canonical decomposition of one code point. */ +static void riina_ucd_decompose_cp(uint32_t cp, riina_cpbuf_t* out) { + if (cp >= RIINA_HANGUL_S_BASE && cp < RIINA_HANGUL_S_BASE + RIINA_HANGUL_S_COUNT) { + uint32_t si = cp - RIINA_HANGUL_S_BASE; + riina_cpbuf_push(out, RIINA_HANGUL_L_BASE + si / RIINA_HANGUL_N_COUNT); + riina_cpbuf_push(out, RIINA_HANGUL_V_BASE + + (si % RIINA_HANGUL_N_COUNT) / RIINA_HANGUL_T_COUNT); + uint32_t t = si % RIINA_HANGUL_T_COUNT; + if (t != 0) riina_cpbuf_push(out, RIINA_HANGUL_T_BASE + t); + return; + } + size_t lo = 0, hi = RIINA_UCD_DECOMP_INDEX_N, found = (size_t)-1; + while (lo < hi) { + size_t mid = lo + (hi - lo) / 2; + if (riina_ucd_decomp_index[mid][0] == cp) { found = mid; break; } + if (riina_ucd_decomp_index[mid][0] < cp) lo = mid + 1; else hi = mid; + } + if (found == (size_t)-1) { riina_cpbuf_push(out, cp); return; } + uint32_t off = riina_ucd_decomp_index[found][1]; + uint32_t len = riina_ucd_decomp_index[found][2]; + for (uint32_t i = 0; i < len; i++) { + riina_ucd_decompose_cp(riina_ucd_decomp_data[off + i], out); + } +} + +/* Canonical ordering: a STABLE insertion sort over runs of non-zero combining + class. Stability is required by UAX #15 — an unstable sort reorders equal + classes and changes the result. */ +static void riina_ucd_canonical_order(riina_cpbuf_t* b) { + for (size_t i = 1; i < b->len; i++) { + uint8_t cc = riina_ucd_ccc_of(b->cps[i]); + if (cc == 0) continue; + size_t j = i; + while (j > 0) { + uint8_t prev = riina_ucd_ccc_of(b->cps[j - 1]); + if (prev == 0 || prev <= cc) break; + uint32_t t = b->cps[j]; b->cps[j] = b->cps[j - 1]; b->cps[j - 1] = t; + j--; + } + } +} + +static int riina_ucd_compose_pair(uint32_t a, uint32_t b, uint32_t* out) { + /* Hangul first, arithmetically. */ + if (a >= RIINA_HANGUL_L_BASE && a < RIINA_HANGUL_L_BASE + RIINA_HANGUL_L_COUNT + && b >= RIINA_HANGUL_V_BASE && b < RIINA_HANGUL_V_BASE + RIINA_HANGUL_V_COUNT) { + *out = RIINA_HANGUL_S_BASE + + ((a - RIINA_HANGUL_L_BASE) * RIINA_HANGUL_V_COUNT + (b - RIINA_HANGUL_V_BASE)) + * RIINA_HANGUL_T_COUNT; + return 1; + } + if (a >= RIINA_HANGUL_S_BASE && a < RIINA_HANGUL_S_BASE + RIINA_HANGUL_S_COUNT + && ((a - RIINA_HANGUL_S_BASE) % RIINA_HANGUL_T_COUNT) == 0 + && b > RIINA_HANGUL_T_BASE && b < RIINA_HANGUL_T_BASE + RIINA_HANGUL_T_COUNT) { + *out = a + (b - RIINA_HANGUL_T_BASE); + return 1; + } + /* COMPOSE is sorted by (first, second). */ + size_t lo = 0, hi = RIINA_UCD_COMPOSE_N; + while (lo < hi) { + size_t mid = lo + (hi - lo) / 2; + uint32_t ma = riina_ucd_compose[mid][0], mb = riina_ucd_compose[mid][1]; + if (ma == a && mb == b) { *out = riina_ucd_compose[mid][2]; return 1; } + if (ma < a || (ma == a && mb < b)) lo = mid + 1; else hi = mid; + } + return 0; +} + +/* Canonical composition (UAX #15 §X3). The BLOCKED check is the subtle part: a + starter may only combine with a following mark if no intervening character + has a combining class >= that mark's. Dropping it composes across a blocker + and gives a different string. */ +static void riina_ucd_compose_buf(riina_cpbuf_t* b) { + if (b->len == 0) return; + size_t starter = 0; + uint8_t last_cc = 0; + size_t out = 1; + if (riina_ucd_ccc_of(b->cps[0]) != 0) last_cc = 0xFF; /* not a starter */ + for (size_t i = 1; i < b->len; i++) { + uint32_t cp = b->cps[i]; + uint8_t cc = riina_ucd_ccc_of(cp); + uint32_t composed; + if (last_cc != 0xFF && (last_cc == 0 ? 1 : last_cc < cc) + && riina_ucd_compose_pair(b->cps[starter], cp, &composed)) { + b->cps[starter] = composed; + continue; + } + if (cc == 0) { starter = out; last_cc = 0; } + else { last_cc = cc; } + b->cps[out++] = cp; + } + b->len = out; +} + +static riina_cpbuf_t riina_ucd_decode(const char* s, size_t slen) { + riina_cpbuf_t b = { NULL, 0, 0 }; + size_t i = 0; + while (i < slen) riina_cpbuf_push(&b, riina_sec_utf8_next(s, slen, &i)); + return b; +} + +static riina_value_t* riina_ucd_encode(riina_cpbuf_t* b) { + size_t cap = b->len * 4 + 1, n = 0; + char* out = (char*)malloc(cap); + if (!out) abort(); + for (size_t i = 0; i < b->len; i++) riina_sec_put_utf8(&out, &n, &cap, b->cps[i]); + out[n] = '\0'; + riina_value_t* v = riina_string(out); + free(out); + return v; +} + +/* NFD: decompose then canonically order. */ +static void riina_ucd_nfd_buf(riina_cpbuf_t* in, riina_cpbuf_t* out) { + for (size_t i = 0; i < in->len; i++) riina_ucd_decompose_cp(in->cps[i], out); + riina_ucd_canonical_order(out); +} + +static riina_value_t* riina_builtin_nfc(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + riina_cpbuf_t in = riina_ucd_decode(arg->data.string_val.data, arg->data.string_val.len); + riina_cpbuf_t d = { NULL, 0, 0 }; + riina_ucd_nfd_buf(&in, &d); + riina_ucd_compose_buf(&d); + riina_value_t* r = riina_ucd_encode(&d); + free(in.cps); free(d.cps); + return r; +} + +/* skeleton(X) = NFD( map(NFD(X)) ) — UTS #39 §4. Note it ends in NFD, NOT NFC: + the skeleton is a comparison key, not a display form. */ +static riina_value_t* riina_builtin_skeleton(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + riina_cpbuf_t in = riina_ucd_decode(arg->data.string_val.data, arg->data.string_val.len); + riina_cpbuf_t d1 = { NULL, 0, 0 }; + riina_ucd_nfd_buf(&in, &d1); + + riina_cpbuf_t mapped = { NULL, 0, 0 }; + for (size_t i = 0; i < d1.len; i++) { + uint32_t cp = d1.cps[i]; + size_t lo = 0, hi = RIINA_UCD_CONF_INDEX_N, found = (size_t)-1; + while (lo < hi) { + size_t mid = lo + (hi - lo) / 2; + if (riina_ucd_conf_index[mid][0] == cp) { found = mid; break; } + if (riina_ucd_conf_index[mid][0] < cp) lo = mid + 1; else hi = mid; + } + if (found == (size_t)-1) { riina_cpbuf_push(&mapped, cp); continue; } + uint32_t off = riina_ucd_conf_index[found][1]; + uint32_t len = riina_ucd_conf_index[found][2]; + for (uint32_t k = 0; k < len; k++) { + riina_cpbuf_push(&mapped, riina_ucd_conf_data[off + k]); + } + } + + riina_cpbuf_t d2 = { NULL, 0, 0 }; + riina_ucd_nfd_buf(&mapped, &d2); + riina_value_t* r = riina_ucd_encode(&d2); + free(in.cps); free(d1.cps); free(mapped.cps); free(d2.cps); + return r; +} + +static riina_value_t* riina_builtin_adalah_keliru(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* a = riina_builtin_skeleton(arg->data.pair_val.fst); + riina_value_t* b = riina_builtin_skeleton(arg->data.pair_val.snd); + int same = a->data.string_val.len == b->data.string_val.len + && memcmp(a->data.string_val.data, b->data.string_val.data, + a->data.string_val.len) == 0; + return riina_bool(same != 0); +} +"####, + ); + } + /// Write a line with current indentation fn writeln(&mut self, s: &str) { for _ in 0..self.indent { diff --git a/03_PROTO/crates/riina-codegen/src/lower.rs b/03_PROTO/crates/riina-codegen/src/lower.rs index 65793e06..e443f05d 100644 --- a/03_PROTO/crates/riina-codegen/src/lower.rs +++ b/03_PROTO/crates/riina-codegen/src/lower.rs @@ -135,6 +135,13 @@ pub(crate) fn builtin_canonical(name: &str) -> Option<&'static str> { // under `riinac run` and failed `riinac build` with // `unbound variable: nilai_kiri` — a language feature that did not // compile, wearing the costume of a missing builtin. + // Unicode. These three are why `emit.rs` gained its ONE conditional + // prelude block: they need ~250 KB of vendored UCD tables, which would + // otherwise more than double every compiled binary to serve builtins + // most programs never call. See `emit_unicode_runtime`. + "nfc" | "ke_nfc" => return Some("nfc"), + "skeleton" | "rangka" => return Some("skeleton"), + "adalah_keliru" | "is_confusable" => return Some("adalah_keliru"), "adalah_kiri" => return Some("adalah_kiri"), "adalah_kanan" => return Some("adalah_kanan"), "nilai_kiri" => return Some("nilai_kiri"), diff --git a/03_PROTO/crates/riinac/tests/unicode_differential.rs b/03_PROTO/crates/riinac/tests/unicode_differential.rs new file mode 100644 index 00000000..63044a89 --- /dev/null +++ b/03_PROTO/crates/riinac/tests/unicode_differential.rs @@ -0,0 +1,294 @@ +// Copyright (c) 2026 The RIINA Authors. All rights reserved. + +//! Interpreter/C differential for the Unicode builtins — `nfc`/`ke_nfc` +//! (UAX #15), `skeleton`/`rangka` and `adalah_keliru`/`is_confusable` (UTS #39). +//! Master plan REQ-70, the last routed group. +//! +//! # Why these needed the emitter's first conditional prelude block +//! +//! Every other builtin's C is a few dozen lines. These need ~250 KB of vendored +//! UCD tables — canonical combining classes, decompositions, composition pairs, +//! and the confusable prototype map. The emitted prelude is already ~228 KB for +//! a hello-world and is otherwise entirely unconditional, so emitting the tables +//! always would MORE THAN DOUBLE every compiled binary to serve three builtins +//! most programs never call. `emit.rs` therefore scans the program for a call to +//! one of them and emits the block only then; [`hello_world_carries_no_ucd_tables`] +//! is what keeps that promise honest. +//! +//! # The tables are generated, not transcribed +//! +//! The C arrays are written out from the same `unicode_nfc_data` / +//! `unicode_confusables_data` statics the interpreter reads. That is deliberate: +//! a hand-copied 250 KB table is a drift source no differential could +//! realistically cover, whereas generating it means the two backends cannot +//! disagree about the DATA at all — only about the ALGORITHM, which is ~150 +//! lines and is what the cases below actually test. +//! +//! # Cases chosen where the algorithm, not the data, decides +//! +//! - **Hangul** composes and decomposes ARITHMETICALLY (UAX #15 §16) and so +//! appears in no table. A C port that only did table lookups would leave +//! Hangul decomposed. +//! - **Canonical ordering must be STABLE.** Two combining marks of equal class +//! must keep their relative order; an unstable sort silently reorders them. +//! - **Composition must respect BLOCKING.** A starter may only combine with a +//! following mark when no intervening character has a combining class at +//! least as high. Dropping that check composes across a blocker. +//! - **`skeleton` ends in NFD, not NFC** — it is a comparison key, not a display +//! form. Ending it in NFC would still make the homograph cases below pass +//! while producing the wrong string. + +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) — Unicode 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_uni_{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); + } +} + +fn assert_backends_agree(tag: &str, body: &str) { + if !require_cc() { + return; + } + let sb = Sandbox::new(tag); + let src = sb.dir.join(format!("{}.rii", sb.stem)); + std::fs::write( + &src, + format!("fungsi utama() -> Nombor kesan Tulis {{\n{body}\n 0\n}}\n"), + ) + .expect("write program"); + + let interp = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("run") + .arg(&src) + .output() + .expect("riinac run"); + assert!( + interp.status.success(), + "interpreter failed for {tag}: {}{}", + String::from_utf8_lossy(&interp.stdout), + String::from_utf8_lossy(&interp.stderr) + ); + let raw = String::from_utf8_lossy(&interp.stdout).into_owned(); + let mut lines: Vec<&str> = raw.lines().collect(); + lines.pop(); // `riinac run` appends the program's final value + let interp_out = if lines.is_empty() { + String::new() + } else { + format!("{}\n", lines.join("\n")) + }; + + let build = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("build") + .arg(&src) + .output() + .expect("riinac build"); + assert!( + build.status.success(), + "compile failed for {tag}: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + let run = Command::new(sb.dir.join(&sb.stem)) + .output() + .expect("run binary"); + assert!( + run.status.success(), + "compiled binary failed for {tag} (exit {:?}): {}{}", + run.status.code(), + String::from_utf8_lossy(&run.stdout), + String::from_utf8_lossy(&run.stderr) + ); + let c_out = String::from_utf8_lossy(&run.stdout).into_owned(); + + assert_eq!( + interp_out, c_out, + "interp/C divergence for {tag}\n interp: {interp_out:?}\n C: {c_out:?}" + ); +} + +/// Precomposed and decomposed spellings must normalise to the same bytes, and +/// the LENGTH is asserted alongside the text so a backend that silently returned +/// its input unchanged is caught (both spellings print identically otherwise). +#[test] +fn nfc_composes_combining_marks() { + assert_backends_agree( + "compose", + " cetakln(nfc(\"e\u{0301}\"));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"e\u{0301}\"))));\n\ + \x20 cetakln(ke_teks(panjang(\"e\u{0301}\")));\n\ + \x20 cetakln(ke_nfc(\"A\u{030A}\"));\n\ + \x20 cetakln(ke_teks(panjang(ke_nfc(\"A\u{030A}\"))));", + ); +} + +/// Hangul is composed and decomposed by ARITHMETIC, not by table, so a C port +/// that only consulted the decomposition data would leave these apart. +#[test] +fn hangul_composes_arithmetically() { + assert_backends_agree( + "hangul", + " cetakln(nfc(\"\u{1100}\u{1161}\"));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"\u{1100}\u{1161}\"))));\n\ + \x20 cetakln(nfc(\"\u{1100}\u{1161}\u{11A8}\"));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"각\"))));", + ); +} + +/// Canonical ordering sorts combining marks by class and must be STABLE. The +/// first string has marks OUT of class order (dot-below 220 after acute 230), so +/// NFC must reorder them; the second already has them in order, and both must +/// normalise to the same bytes. +#[test] +fn canonical_ordering_is_stable_and_agrees() { + assert_backends_agree( + "order", + " cetakln(ke_teks(nfc(\"q\u{0301}\u{0323}\") == nfc(\"q\u{0323}\u{0301}\")));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"q\u{0301}\u{0323}\"))));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"q\u{0323}\u{0301}\"))));", + ); +} + +/// A BLOCKED starter must not compose. +/// +/// `a` + U+0305 overline + U+0301 acute. Both marks have combining class 230, +/// and the overline does not compose with `a`, so the acute is BLOCKED — equal +/// classes do not let it reach the starter. The result stays five bytes +/// (a + overline + acute); dropping the blocking check composes `a`+acute into +/// `á` across the overline and gives FOUR. +/// +/// The obvious case — `a` + dot-below + acute — does NOT test this, which a +/// negative control caught: there both marks compose into the starter in turn, +/// so blocking never applies and removing the check changes nothing. This input +/// was chosen after verifying by experiment that deleting the blocking +/// condition from the emitted C actually makes this test fail. +#[test] +fn blocked_composition_is_refused_by_both() { + assert_backends_agree( + "blocked", + " cetakln(ke_teks(panjang(nfc(\"a\u{0305}\u{0301}\"))));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"a\u{0301}\"))));\n\ + \x20 cetakln(nfc(\"a\u{0305}\u{0301}\"));\n\ + \x20 cetakln(ke_teks(nfc(\"a\u{0305}\u{0301}\") == nfc(\"a\u{0301}\")));", + ); +} + +/// The homograph defence itself: Cyrillic look-alikes must collapse to the same +/// skeleton, and genuinely different names must not. +#[test] +fn confusable_detection_agrees() { + assert_backends_agree( + "confuse", + " cetakln(skeleton(\"paypal\"));\n\ + \x20 cetakln(ke_teks(adalah_keliru((\"a\", \"\u{0430}\"))));\n\ + \x20 cetakln(ke_teks(adalah_keliru((\"paypal\", \"pa\u{0443}pal\"))));\n\ + \x20 cetakln(ke_teks(is_confusable((\"case\", \"\u{0441}\u{0430}\u{0455}\u{0435}\"))));\n\ + \x20 cetakln(ke_teks(adalah_keliru((\"microsoft\", \"paypal\"))));\n\ + \x20 cetakln(rangka(\"\u{0430}\"));", + ); +} + +/// Empty and ASCII-only inputs take the early-exit paths on both sides. +#[test] +fn degenerate_inputs_agree() { + assert_backends_agree( + "degen", + " cetakln(nfc(\"\"));\n\ + \x20 cetakln(nfc(\"plain ascii\"));\n\ + \x20 cetakln(skeleton(\"\"));\n\ + \x20 cetakln(ke_teks(adalah_keliru((\"\", \"\"))));\n\ + \x20 cetakln(ke_teks(panjang(nfc(\"\"))));", + ); +} + +/// The conditional-emission promise: a program that does NOT call a Unicode +/// builtin must not carry the ~250 KB of UCD tables. Without this the block +/// would silently become unconditional again the first time someone moved the +/// call, and nothing else would notice — the binaries would just get bigger. +#[test] +fn hello_world_carries_no_ucd_tables() { + let sb = Sandbox::new("nogate"); + let plain = sb.dir.join("plain.rii"); + std::fs::write( + &plain, + "fungsi utama() -> Nombor kesan Tulis { cetakln(\"hai\"); 0 }\n", + ) + .expect("write plain"); + let uni = sb.dir.join("uni.rii"); + std::fs::write( + &uni, + "fungsi utama() -> Nombor kesan Tulis { cetakln(nfc(\"hai\")); 0 }\n", + ) + .expect("write uni"); + + let emit = |p: &PathBuf| -> String { + let out = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("emit-c") + .arg(p) + .output() + .expect("riinac emit-c"); + assert!(out.status.success(), "emit-c failed for {}", p.display()); + String::from_utf8_lossy(&out.stdout).into_owned() + }; + + let plain_c = emit(&plain); + let uni_c = emit(&uni); + + assert!( + !plain_c.contains("riina_ucd_ccc"), + "a program with no Unicode call carried the UCD tables ({} bytes of C)", + plain_c.len() + ); + assert!( + uni_c.contains("riina_ucd_ccc"), + "a program that calls nfc did NOT get the UCD tables — the gate is \ + inverted, and every Unicode program would abort on contact" + ); + assert!( + uni_c.len() > plain_c.len() + 100_000, + "the tables look absent from the Unicode build: plain={} uni={}", + plain_c.len(), + uni_c.len() + ); +} diff --git a/docs/api/STDLIB.md b/docs/api/STDLIB.md index 3c90a6df..8a8e1bd4 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. That is ALL it means: type-checking does not imply compiling, and it does not even imply running. **335** of the 373 compile: +Every builtin below type-checks. That is ALL it means: type-checking does not imply compiling, and it does not even imply running. **341** of the 373 compile: | Backend value | Meaning | |---|---| | `compiled` | Lowers to C **and** WASM (21 builtins). | -| `native-only` | Lowers to C. The WASM backend **refuses** it (314 builtins). | -| `interp-only` | `riinac run` only (30 builtins). `riinac build` fails with `unbound variable`. | +| `native-only` | Lowers to C. The WASM backend **refuses** it (320 builtins). | +| `interp-only` | `riinac run` only (24 builtins). `riinac build` fails with `unbound variable`. | | `typed-only` | **Nothing runs it** (8 builtins). The name is in the type registry, but neither the interpreter nor any backend binds it, so `riinac run` fails with `unbound variable` too. | ``` @@ -31,13 +31,11 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Bersih (Pure) -> **Mixed:** 223 of 229 compile; the rest are interpreter-only (REQ-70). - | Builtin | Type | Backend | |---|---|---| | `abs` | `Fn(Nombor, Nombor)` | **native-only** | | `adalah_kanan` | `Fn(Any, Benar)` | **native-only** | -| `adalah_keliru` | `Fn((Teks, Teks), Benar)` | **interp-only** | +| `adalah_keliru` | `Fn((Teks, Teks), Benar)` | **native-only** | | `adalah_kiri` | `Fn(Any, Benar)` | **native-only** | | `assert` | `Fn(Benar, ())` | **native-only** | | `assert_eq` | `Fn((Any, Any), ())` | **native-only** | @@ -78,7 +76,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `http_parse_method` | `Fn(Teks, Teks)` | **native-only** | | `http_parse_target` | `Fn(Teks, Teks)` | **native-only** | | `int_to_string` | `Fn(Nombor, Teks)` | compiled | -| `is_confusable` | `Fn((Teks, Teks), Benar)` | **interp-only** | +| `is_confusable` | `Fn((Teks, Teks), Benar)` | **native-only** | | `json_ada` | `Fn(Any, Any)` | **native-only** | | `json_dapat` | `Fn(Any, Any)` | **native-only** | | `json_get` | `Fn(Any, Any)` | **native-only** | @@ -94,7 +92,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `julat` | `Fn((Nombor, Nombor), Senarai)` | **native-only** | | `julat_inklusif` | `Fn((Nombor, Nombor), Senarai)` | **native-only** | | `ke_bool` | `Fn(Any, Benar)` | **native-only** | -| `ke_nfc` | `Fn(Teks, Teks)` | **interp-only** | +| `ke_nfc` | `Fn(Teks, Teks)` | **native-only** | | `ke_nombor` | `Fn(Teks, Nombor)` | **native-only** | | `ke_teks` | `Fn(Any, Teks)` | compiled | | `kuasa` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | @@ -133,7 +131,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `minimum` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | | `money` | `Fn(Teks, Wang)` | compiled | | `mutlak` | `Fn(Nombor, Nombor)` | **native-only** | -| `nfc` | `Fn(Teks, Teks)` | **interp-only** | +| `nfc` | `Fn(Teks, Teks)` | **native-only** | | `nilai_kanan` | `Fn(Any, Any)` | **native-only** | | `nilai_kiri` | `Fn(Any, Any)` | **native-only** | | `nombor_ke_teks` | `Fn(Nombor, Teks)` | compiled | @@ -154,7 +152,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `pow` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | | `punca` | `Fn(Nombor, Nombor)` | **native-only** | | `qmn` | `Fn((Teks, Nombor), Qmn)` | compiled | -| `rangka` | `Fn(Teks, Teks)` | **interp-only** | +| `rangka` | `Fn(Teks, Teks)` | **native-only** | | `rem` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | | `sahkan_panjang` | `Fn((Tercemar, Nombor), Mungkin>)` | **native-only** | | `sahkan_url` | `Fn(Tercemar, Disanitasi)` | **native-only** | @@ -212,7 +210,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `set_persilangan` | `Fn(Any, Any)` | **native-only** | | `set_remove` | `Fn(Any, Any)` | **native-only** | | `set_union` | `Fn(Any, Any)` | **native-only** | -| `skeleton` | `Fn(Teks, Teks)` | **interp-only** | +| `skeleton` | `Fn(Teks, Teks)` | **native-only** | | `sqrt` | `Fn(Nombor, Nombor)` | **native-only** | | `str_char_at` | `Fn(Any, Any)` | **native-only** | | `str_contains` | `Fn(Any, Any)` | **native-only** | diff --git a/website/public/metrics.json b/website/public/metrics.json index a75145c5..a4408a7c 100644 --- a/website/public/metrics.json +++ b/website/public/metrics.json @@ -1,10 +1,10 @@ { - "generated": "2026-08-21T02:03:50Z", - "generatedHuman": "August 21, 2026 at 02:03 UTC", + "generated": "2026-08-21T02:21:11Z", + "generatedHuman": "August 21, 2026 at 02:21 UTC", "version": "0.4.0", "session": 0, "git": { - "commit": "cd76403d4", + "commit": "dbfedef0c", "branch": "claude/continue-solution-4gn31y" }, "proofs": { @@ -196,7 +196,7 @@ "rust": { "tests": 3360, "testsVerified": 3360, - "testsEstimated": 3362, + "testsEstimated": 3369, "testsSource": "cached_verified", "crates": 20 }, From 495bae56419032d663ade716799f8aa8a351f3e9 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 21 Aug 2026 02:28:34 +0000 Subject: [PATCH 3/4] [ALL] DOCS: record the last pure-builtin group and what examining it found Updates the REQ-70 row and the Part 12 Wave 1.0 status. Counts re-derived from the regenerated docs/api/STDLIB.md: 373 registered, 341 compile -- compiled 21 / native-only 320 / interp-only 24 / typed-only 8. Corrects my own framing. I listed these 26 as unexamined backlog and told the owner the remaining interpreter-only set each had a stated reason. Both were wrong: only 24 of the 50 did, and examining the other 26 found three defects rather than missing implementations -- a language feature (nested constructor patterns) that did not compile, a pair-taking builtin declared unary and so uncallable from any well-typed program, and an aliasing gap. Also records that the Backend column was making a false promise for eight crypto-agility builtins, now fixed with a fourth `typed-only` state derived from the real interpreter environment; that the Unicode three needed the emitter's first conditional prelude block, with the measured sizes; and that keselamatan_nama.rii -- one of four Gate C sample apps, and the only one that would not build -- now compiles. Generalises the wave's recurring finding one step further. It already said a family marked as lowering is not a family that agrees. Two cases in this wave went further: they PASSED while the property they named was absent from the code. json's nine differential cases all fed well-formed input to a parser that could not fail, and the Unicode composition-blocking case chose an input where blocking never applies. Both were found by deliberately breaking the implementation and checking whether the test noticed. A green differential is evidence only about the inputs it actually runs. --- RIINA_MASTER_PLAN.md | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/RIINA_MASTER_PLAN.md b/RIINA_MASTER_PLAN.md index 613aae59..0a6aa5f2 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: 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. **`keselamatan` FAMILY CLOSED 2026-08-20 — 41 of 42, and the deferral that held back the last 17 was wrong.** The 2026-08-19 increment routed only the single-argument subset, reasoning that eleven members take a pair and `split_pair` returns a `Value::BuiltinPartial` for a non-pair argument, which the C backend has no equivalent of. Checking that instead of repeating it is what unblocked the rest: every one of those signatures is typed `Ty::Prod(..) -> _` in `riina-typechecker`, so the curried form `f(a, b)` is REJECTED AT TYPE-CHECK — identically under `riinac run` and `riinac build` — and only `f((a, b))` ever reaches a runtime. The interpreter's partial arm is unreachable from well-typed source, so C needing no partial-application machinery costs nothing; a test now pins that assumption, since eleven C implementations rest on it. **Two prerequisites had to be fixed first, both in families this row already recorded as closed, and both invisible to the differentials those families shipped with.** (a) **The emitted C JSON parser could not fail at all** — `riina_json_parse_value` had no error path, so unknown input fell through to `strtoll` and became a value: `"xyz"` and `""` became `0`, `"12abc"` became `12`, `"nul"` became `()`, `"[1,2"` closed itself. The interpreter rejects all five. A compiled program parsing attacker-controlled JSON therefore saw a FABRICATED value where `riinac run` refuses, and `json_parse_safe`/`nyahsiri_selamat` — whose whole contract is "malformed input yields Unit" — could not be routed to a backend where "malformed" had no meaning. `json_differential` missed it because all nine of its cases fed WELL-FORMED input. The parser now mirrors `builtins/json.rs` production-for-production, including Unicode (not ASCII) whitespace, lone surrogates decoding to nothing, and `u64`-then-saturating-`f64` number parsing (so `-5` is `0`, not `18446744073709551611`). (b) **Composite values rendered as the literal text ``** — `riina_format` defaulted PAIR, LIST, MAP and both SUM arms, and `ke_teks` carried a second copy of the scalar arms. A compiled program printing a list showed `` where `riinac run` shows `[1, 2, 3]`, which also made `sahkan_panjang` unroutable in practice: it returns an `Option`, so its answer was unobservable in compiled code — the REQ-79 trap in a new costume. Both of the interpreter's rendering modes are now mirrored (`format_value` prints strings bare and bools as `betul`/`salah`; `Display`, the only path a sum takes, quotes strings and prints English `true`/`false`), pinned so that reconciling them is a language decision rather than codegen drift. **NOT routed: `csrf_generate`/`csrf_jana`, deliberately** — its result is not a function of its input (a token seeded from the clock and a process-local counter), so the backends can be held only to a shape, not to agreement; mirroring it would mean transcribing Rust's `DefaultHasher` into C to reproduce a generator its own doc comment marks as "a *reference* token, not a certified CSPRNG". Nothing is cut off — `csrf_validate` takes plain `Teks`, so compiled programs can carry tokens minted elsewhere. **Recorded, not fixed — a stdlib defect the differential surfaced:** `sanitasi_json` is the only producer of `Disanitasi` and so the only way to reach `json_urai_selamat`, but it is a string-EMBEDDING escaper — it turns `{"a":1}` into `{\"a\":1}`. Every JSON object arrives malformed and parses to `Unit` because object keys are quoted; only quote-free documents survive. Both backends agree, so it is a type-signature defect in the security stdlib (the gate on a safe PARSER should be a validation, not an escape), not a divergence. Counts re-derived from the compiler after the merge: **373 registered, 323 compile — `compiled` 20 / `native-only` 303 / `interp-only` 50.** Still NOT routed: `csrf_generate` (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 + file + security DONE; `jaring_tls_*` and the VirtualFs trio 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. **`keselamatan` FAMILY CLOSED 2026-08-20 — 41 of 42, and the deferral that held back the last 17 was wrong.** The 2026-08-19 increment routed only the single-argument subset, reasoning that eleven members take a pair and `split_pair` returns a `Value::BuiltinPartial` for a non-pair argument, which the C backend has no equivalent of. Checking that instead of repeating it is what unblocked the rest: every one of those signatures is typed `Ty::Prod(..) -> _` in `riina-typechecker`, so the curried form `f(a, b)` is REJECTED AT TYPE-CHECK — identically under `riinac run` and `riinac build` — and only `f((a, b))` ever reaches a runtime. The interpreter's partial arm is unreachable from well-typed source, so C needing no partial-application machinery costs nothing; a test now pins that assumption, since eleven C implementations rest on it. **Two prerequisites had to be fixed first, both in families this row already recorded as closed, and both invisible to the differentials those families shipped with.** (a) **The emitted C JSON parser could not fail at all** — `riina_json_parse_value` had no error path, so unknown input fell through to `strtoll` and became a value: `"xyz"` and `""` became `0`, `"12abc"` became `12`, `"nul"` became `()`, `"[1,2"` closed itself. The interpreter rejects all five. A compiled program parsing attacker-controlled JSON therefore saw a FABRICATED value where `riinac run` refuses, and `json_parse_safe`/`nyahsiri_selamat` — whose whole contract is "malformed input yields Unit" — could not be routed to a backend where "malformed" had no meaning. `json_differential` missed it because all nine of its cases fed WELL-FORMED input. The parser now mirrors `builtins/json.rs` production-for-production, including Unicode (not ASCII) whitespace, lone surrogates decoding to nothing, and `u64`-then-saturating-`f64` number parsing (so `-5` is `0`, not `18446744073709551611`). (b) **Composite values rendered as the literal text ``** — `riina_format` defaulted PAIR, LIST, MAP and both SUM arms, and `ke_teks` carried a second copy of the scalar arms. A compiled program printing a list showed `` where `riinac run` shows `[1, 2, 3]`, which also made `sahkan_panjang` unroutable in practice: it returns an `Option`, so its answer was unobservable in compiled code — the REQ-79 trap in a new costume. Both of the interpreter's rendering modes are now mirrored (`format_value` prints strings bare and bools as `betul`/`salah`; `Display`, the only path a sum takes, quotes strings and prints English `true`/`false`), pinned so that reconciling them is a language decision rather than codegen drift. **NOT routed: `csrf_generate`/`csrf_jana`, deliberately** — its result is not a function of its input (a token seeded from the clock and a process-local counter), so the backends can be held only to a shape, not to agreement; mirroring it would mean transcribing Rust's `DefaultHasher` into C to reproduce a generator its own doc comment marks as "a *reference* token, not a certified CSPRNG". Nothing is cut off — `csrf_validate` takes plain `Teks`, so compiled programs can carry tokens minted elsewhere. **Recorded, not fixed — a stdlib defect the differential surfaced:** `sanitasi_json` is the only producer of `Disanitasi` and so the only way to reach `json_urai_selamat`, but it is a string-EMBEDDING escaper — it turns `{"a":1}` into `{\"a\":1}`. Every JSON object arrives malformed and parses to `Unit` because object keys are quoted; only quote-free documents survive. Both backends agree, so it is a type-signature defect in the security stdlib (the gate on a safe PARSER should be a validation, not an escape), not a divergence. **THE LAST PURE GROUP: 2026-08-21. What I called 26 unexamined builtins was three DEFECTS plus a design question, and describing them as backlog was wrong.** (i) `adalah_kiri`/`adalah_kanan`/`nilai_kiri`/`nilai_kanan` are COMPILER INTERNALS, not stdlib: the parser's if-chain pattern compiler emits them for a constructor pattern nested where a `Case` cannot go, e.g. `(Ada(a), Tiada)` inside a tuple pattern. Unrouted, that whole class of pattern ran under `riinac run` and failed `riinac build` with `unbound variable: nilai_kiri` — a LANGUAGE FEATURE that did not compile, showing up in the Backend column as four obscure builtins. (ii) `baki`/`rem` were UNCALLABLE from any well-typed program: binary and pair-taking in both the interpreter and the emitted C, but declared `Nombor -> Nombor` in the typechecker because they shared a registration loop with the genuinely unary `log2`, so `baki(10, 3)` and `baki((10, 3))` both failed. Two of three components agreed and the TYPE was the outlier. (iii) `cetak_baris` was a pure aliasing gap — the interpreter binds it to `cetakln` and only this gate did not know. `baki`, `log2` and `rawak` already HAD C sitting unreferenced in emit.rs, like the json helpers before them. **The Backend column was making a FALSE PROMISE, now fixed.** Its `interp-only` cell reads "`riinac run` only". For the eight crypto-agility builtins (`guna_kripto`/`use_crypto`, `pilih_algo`/`select_algorithm`, `cipher`/`sifer`, `hash_dengan`/`hash_with`) that was FALSE: they sit in the typechecker registry with `Fn(Teks, Any, Kripto)` and carry the REQ-48 deprecation check at their call sites, but NO runtime binds them — verified by command for all eight, `riinac run` fails with `unbound variable` exactly as `riinac build` does. A three-state column had no way to say "typed but unimplemented", so it said the nearest thing, which was wrong. Added a fourth state **`typed-only`**, derived from a new `riina_codegen::interpreter_supports_builtin` that builds the real interpreter environment and looks the name up rather than consulting a list. **The Unicode three needed the emitter's FIRST conditional prelude block.** `nfc`, `skeleton` and `adalah_keliru` need ~250 KB of vendored UCD tables, and the prelude is already ~228 KB for a hello-world and otherwise entirely unconditional — emitting them always would more than double every binary to serve three builtins most programs never call. `emit()` scans the IR and emits the block only on a call; measured 229,600 bytes for a hello-world with zero tables against 492,515 for a program calling `nfc`. The C tables are GENERATED from the same Rust statics the interpreter reads, so the backends cannot disagree about the data at all — only about the ~150-line algorithm. **A NEGATIVE CONTROL CAUGHT A TEST PASSING FOR THE WRONG REASON**: the composition-blocking case was first written as `a`+dot-below+acute, and deleting the blocking condition from the emitted C did not make it fail, because there both marks compose into the starter in turn and blocking never applies. Rewritten as `a`+U+0305+U+0301 (equal combining classes, overline does not compose), where removing the check shortens the result from five bytes to four; the control then failed as intended. **`keselamatan_nama.rii` NOW COMPILES** — one of the four Gate C sample apps, and the only one that would not build. Counts re-derived from the regenerated doc: **373 registered, 341 compile — `compiled` 21 / `native-only` 320 / `interp-only` 24 / `typed-only` 8.** Every remaining `interp-only` builtin now has a stated reason: the `jaring_tls_*`/`net_tls_*` half (16, awaiting the Law 8 decision), the VirtualFs trio (6, needs an in-memory FS + quota in C), and `csrf_generate` (2, non-deterministic). The 8 `typed-only` crypto-agility builtins need a RUNTIME, not routing — a separate piece of work, and not one REQ-70 can close | P0 | IN PROGRESS (all families routed; `jaring_tls_*`, the VirtualFs trio and the crypto-agility runtime 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 | @@ -4535,23 +4535,31 @@ calling `riina-os`, and emitted C cannot call Rust, so that question must be ans something small — then `simpan`, then `jaring`+`http` (at which point criterion 6 becomes closable), then `fail`+`vfs`, `json`, and `keselamatan` last as the largest and the one whose scope depends on criterion 5's unresolved "no sink may be modelled" clause. **Status -2026-08-20: `json`, `masa`, `simpan`, `jaring`+`http`, `fail`+`vfs` and `keselamatan` are all -DONE — 323 of 373 builtins compile, 50 interpreter-only** (re-derived from the compiler via -`docs/api/STDLIB.md`, not carried forward). Criterion 6 is now verified by command (the +2026-08-21: every family is routed — 341 of 373 builtins compile, 24 interpreter-only and 8 +typed-only** (re-derived from the compiler via `docs/api/STDLIB.md`, not carried forward). +Each of the 24 has a stated reason (TLS 16, VirtualFs 6, `csrf_generate` 2); the 8 +`typed-only` crypto-agility builtins have no runtime anywhere and need one written, which is +not routing work and is not REQ-70's to close. Criterion 6 is now verified by command (the reference service compiles, serves, and persists across restarts); pinning it as a test is REQ-75. Remaining under 1.0: the `jaring_tls_*` half held back on purpose — see the REQ-70 row for why a C TLS that is not really `riina-tls` would be worse than a build error — plus the VirtualFs trio and `csrf_generate`, each excluded for a stated reason rather than left undone. -**The finding this wave keeps producing, now six families deep: a family marked as lowering is -not thereby a family that agrees, and neither is a family with a differential.** Every routed +**The finding this wave keeps producing, now seven groups deep: a family marked as lowering is +not thereby a family that agrees, neither is a family with a differential, and a builtin marked +interpreter-only is not thereby a builtin anyone has looked at.** Every routed family exposed a defect its own Backend column had already called `native-only`; `json` then exposed a SECOND one after being marked closed, because its nine differential cases all fed well-formed input and so never asked the C parser to fail. Two of the defects were security- shaped (the file gate; the fabricated JSON value on attacker-controlled input). The lesson for the families still queued is that the differential must include the inputs the implementation -is supposed to REJECT, not only the ones it is supposed to transform. (1.1) REQ-68 +is supposed to REJECT, not only the ones it is supposed to transform — and that a differential +case should be negative-controlled before it is trusted. Two cases in this wave passed while the +property they named was absent from the code: `json`'s nine cases all fed well-formed input to a +parser that could not fail, and the Unicode composition-blocking case chose an input where +blocking never applies. Both were found by deliberately breaking the implementation and checking +the test noticed. A green differential is evidence only about the inputs it actually runs. (1.1) REQ-68 zero-param `LetRecGroup` + the four tracked backend divergences — **REQ-68 DONE 2026-08-12** (the zero-param half; see its row) — blocks 1.4, REQ-59, and Gate E's differential criterion; (1.2) interpreter frame cost, *then* a recursion-depth guard (at ~350 KiB of native stack per From 5b6983e4078209cf7fdd8313069fefb9deb14632 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 21 Aug 2026 02:48:36 +0000 Subject: [PATCH 4/4] [ALL] CHORE: full-mode verification manifest at the pure-builtin routing (3360 -> 3373 tests) --- VERIFICATION_MANIFEST.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/VERIFICATION_MANIFEST.md b/VERIFICATION_MANIFEST.md index 7172ebfe..356aa218 100644 --- a/VERIFICATION_MANIFEST.md +++ b/VERIFICATION_MANIFEST.md @@ -1,6 +1,6 @@ # RIINA Verification Manifest -**Generated:** 2026-08-20T01:51:06Z -**Git SHA:** 623391e91 +**Generated:** 2026-08-21T02:47:16Z +**Git SHA:** 495bae564 **Mode:** full **Status:** PASS @@ -8,10 +8,10 @@ | Check | Status | Details | |-------|--------|---------| -| Rust Tests | PASS | 3360 tests | +| Rust Tests | PASS | 3373 tests | | Clippy | PASS | 0 warnings | | _CoqProject Completeness | PASS | all 331 .v files listed in _CoqProject | -| Coq Compilation | PASS | 331 .vo files compiled in 179s | +| Coq Compilation | PASS | 331 .vo files compiled in 225s | | 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 1s (5 theorems, local_active) | +| TLA+ Compilation | PASS | Active spec TelusProcurementProtocol parsed and model checked in 2s (5 theorems, local_active) | | TLA+ Scan | PASS | 317 files (12282 theorems) | -| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 7s (6 checked assertions, local_active) | +| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 11s (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) |