diff --git a/03_PROTO/crates/riina-codegen/src/emit.rs b/03_PROTO/crates/riina-codegen/src/emit.rs index 966566af..dc49d56d 100644 --- a/03_PROTO/crates/riina-codegen/src/emit.rs +++ b/03_PROTO/crates/riina-codegen/src/emit.rs @@ -2016,27 +2016,18 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln(""); // Helper: format a value as a string for printing - self.writeln("static const char* riina_format(riina_value_t* v) {"); - self.writeln(" static char buf[256];"); - self.writeln(" switch (v->tag) {"); - self.writeln(" case RIINA_TAG_UNIT: return \"()\";"); - self.writeln( - " case RIINA_TAG_BOOL: return v->data.bool_val ? \"betul\" : \"salah\";", - ); - self.writeln(" case RIINA_TAG_INT:"); - self.writeln(" if (v->int_signed_bits)"); - self.writeln(" snprintf(buf, sizeof(buf), \"%lld\", (long long)riina_sext(v->data.int_val, v->int_signed_bits));"); - self.writeln(" else"); - self.writeln(" snprintf(buf, sizeof(buf), \"%llu\", (unsigned long long)v->data.int_val);"); - self.writeln(" return buf;"); - self.writeln(" case RIINA_TAG_STRING: return v->data.string_val.data;"); - self.writeln(" case RIINA_TAG_BIGINT: return riina_bigint_to_str(v);"); - self.writeln(" case RIINA_TAG_DECIMAL: return riina_decimal_to_str(v);"); - self.writeln(" case RIINA_TAG_FIXED: return riina_fixed_to_str(v);"); - self.writeln(" case RIINA_TAG_FIXEDBIN: return riina_fixedbin_to_str(v);"); - self.writeln(" default: return \"\";"); - self.writeln(" }"); - self.writeln("}"); + // Value rendering. Only DECLARED here: the definition needs + // `riina_list_t` / `riina_map_t`, which are emitted with the collection + // runtime further down, and `cetak`/`cetakln` below call it immediately. + // + // Until REQ-70's keselamatan increment this function handled the scalar + // tags and answered the literal text `` for every composite one — + // PAIR, LIST, MAP and both SUM arms. `cetakln` and `ke_teks` both go + // through it, so a compiled program printing a list, a map, or the + // `Option` that `sahkan_panjang` returns showed `` where + // `riinac run` shows the contents. See the definition for the two + // rendering modes it has to mirror. + self.writeln("static const char* riina_format(riina_value_t* v);"); self.writeln(""); // cetak (print without newline) @@ -2065,27 +2056,14 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln(""); // ke_teks (to_string) + // `ke_teks` IS `builtins::format_value` in the interpreter, so it is + // that one function here too rather than a parallel switch. It used to + // carry its own copy of the scalar arms plus a `default:` returning the + // literal text ``, which is how the composite tags came to render + // differently from `cetakln` — two switches, one of them updated. self.writeln("static riina_value_t* riina_builtin_ke_teks(riina_value_t* arg) {"); - self.writeln(" char buf[256];"); - self.writeln(" switch (arg->tag) {"); - self.writeln(" case RIINA_TAG_UNIT: return riina_string(\"()\");"); - self.writeln(" case RIINA_TAG_BOOL: return riina_string(arg->data.bool_val ? \"betul\" : \"salah\");"); - self.writeln(" case RIINA_TAG_INT:"); - // A signed sized int renders as its signed value (the interpreter is the - // reference: `ke_teks(0i8 - 3i8)` is "-3", not the masked "253"). Same - // tag-driven branch as riina_format — this one had been left unsigned-only. - self.writeln(" if (arg->int_signed_bits)"); - self.writeln(" snprintf(buf, sizeof(buf), \"%lld\", (long long)riina_sext(arg->data.int_val, arg->int_signed_bits));"); - self.writeln(" else"); - self.writeln(" snprintf(buf, sizeof(buf), \"%llu\", (unsigned long long)arg->data.int_val);"); - self.writeln(" return riina_string(buf);"); - self.writeln(" case RIINA_TAG_STRING: return arg;"); - self.writeln(" case RIINA_TAG_BIGINT: return riina_string(riina_bigint_to_str(arg));"); - self.writeln(" case RIINA_TAG_DECIMAL: return riina_string(riina_decimal_to_str(arg));"); - self.writeln(" case RIINA_TAG_FIXED: return riina_string(riina_fixed_to_str(arg));"); - self.writeln(" case RIINA_TAG_FIXEDBIN: return riina_string(riina_fixedbin_to_str(arg));"); - self.writeln(" default: return riina_string(\"\");"); - self.writeln(" }"); + self.writeln(" if (arg->tag == RIINA_TAG_STRING) return arg;"); + self.writeln(" return riina_string(riina_format(arg));"); self.writeln("}"); self.writeln(""); @@ -2398,6 +2376,117 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln("#define RIINA_MAP_DATA(v) ((riina_map_t*)(v)->data.wrapped_val)"); self.writeln(""); + // Value rendering, definition (declared above, next to `cetak`). + // Emitted as one raw string because it is recursive and carries two + // mutually-reachable modes, which the per-line `writeln` form makes + // unreadable. + // + // WHY TWO MODES. The interpreter's `builtins::format_value` handles the + // common tags itself and falls through to `Value`'s `Display` for the + // rest — and the two spell the same value differently. `format_value` + // prints a string BARE and a bool in RIINA's own `betul`/`salah`; + // `Display` QUOTES the string and prints Rust's English `true`/`false`. + // So `cetakln("x")` is `x` while `cetakln(inl "x")` is `inl "x"`, and a + // bool inside a sum comes out English. That is an inconsistency in the + // reference rather than a design, but the reference is what a compiled + // program must match, so both modes are mirrored here rather than + // tidied — changing it is a language decision, not a codegen one. + self.writeln( + r####" +static void riina_fmt_put(char** b, size_t* n, size_t* cap, const char* s) { + size_t l = strlen(s); + while (*n + l + 1 > *cap) { + *cap = *cap ? *cap * 2 : 128; + *b = (char*)realloc(*b, *cap); + if (!*b) abort(); + } + memcpy(*b + *n, s, l); + *n += l; + (*b)[*n] = '\0'; +} + +/* `display` selects Value::Display (quoted strings, English booleans) over + builtins::format_value (bare strings, betul/salah). See the note above. */ +static void riina_fmt_impl(riina_value_t* v, char** b, size_t* n, size_t* cap, bool display) { + char tmp[64]; + switch (v->tag) { + case RIINA_TAG_UNIT: riina_fmt_put(b, n, cap, "()"); return; + case RIINA_TAG_BOOL: + if (display) riina_fmt_put(b, n, cap, v->data.bool_val ? "true" : "false"); + else riina_fmt_put(b, n, cap, v->data.bool_val ? "betul" : "salah"); + return; + case RIINA_TAG_INT: + if (v->int_signed_bits) { + snprintf(tmp, sizeof(tmp), "%lld", + (long long)riina_sext(v->data.int_val, v->int_signed_bits)); + } else { + snprintf(tmp, sizeof(tmp), "%llu", (unsigned long long)v->data.int_val); + } + riina_fmt_put(b, n, cap, tmp); + return; + case RIINA_TAG_STRING: + if (display) riina_fmt_put(b, n, cap, "\""); + riina_fmt_put(b, n, cap, v->data.string_val.data); + if (display) riina_fmt_put(b, n, cap, "\""); + return; + case RIINA_TAG_BIGINT: riina_fmt_put(b, n, cap, riina_bigint_to_str(v)); return; + case RIINA_TAG_DECIMAL: riina_fmt_put(b, n, cap, riina_decimal_to_str(v)); return; + case RIINA_TAG_FIXED: riina_fmt_put(b, n, cap, riina_fixed_to_str(v)); return; + case RIINA_TAG_FIXEDBIN: riina_fmt_put(b, n, cap, riina_fixedbin_to_str(v)); return; + case RIINA_TAG_PAIR: + riina_fmt_put(b, n, cap, "("); + riina_fmt_impl(v->data.pair_val.fst, b, n, cap, display); + riina_fmt_put(b, n, cap, ", "); + riina_fmt_impl(v->data.pair_val.snd, b, n, cap, display); + riina_fmt_put(b, n, cap, ")"); + return; + /* A sum has no `format_value` arm at all: it reaches Display, and so + does everything nested inside it, however deep. Hence the hard `true` + rather than passing `display` down. */ + case RIINA_TAG_SUM_LEFT: + riina_fmt_put(b, n, cap, "inl "); + riina_fmt_impl(v->data.sum_val, b, n, cap, true); + return; + case RIINA_TAG_SUM_RIGHT: + riina_fmt_put(b, n, cap, "inr "); + riina_fmt_impl(v->data.sum_val, b, n, cap, true); + return; + case RIINA_TAG_LIST: { + riina_list_t* l = RIINA_LIST_DATA(v); + riina_fmt_put(b, n, cap, "["); + for (size_t i = 0; i < l->len; i++) { + if (i) riina_fmt_put(b, n, cap, ", "); + riina_fmt_impl(l->items[i], b, n, cap, display); + } + riina_fmt_put(b, n, cap, "]"); + return; + } + case RIINA_TAG_MAP: { + riina_map_t* m = RIINA_MAP_DATA(v); + riina_fmt_put(b, n, cap, "{"); + size_t i = 0; + for (riina_map_entry_t* e = m->head; e; e = e->next, i++) { + if (i) riina_fmt_put(b, n, cap, ", "); + riina_fmt_put(b, n, cap, "\""); + riina_fmt_put(b, n, cap, e->key); + riina_fmt_put(b, n, cap, "\": "); + riina_fmt_impl(e->value, b, n, cap, display); + } + riina_fmt_put(b, n, cap, "}"); + return; + } + default: riina_fmt_put(b, n, cap, ""); return; + } +} + +static const char* riina_format(riina_value_t* v) { + char* b = NULL; size_t n = 0, cap = 0; + riina_fmt_impl(v, &b, &n, &cap, false); + return b ? b : ""; +} +"####, + ); + // ═══════════════════════════════════════════════════════════════════ // STRING BUILTINS (teks) // ═══════════════════════════════════════════════════════════════════ @@ -3259,6 +3348,528 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.emit_net_builtins(); // ═══════════════════════════════════════════════════════════════════ + // ═══════════════════════════════════════════════════════════════════ + // SECURITY BUILTINS (keselamatan) — sanitizers, validators, and the + // modelled sinks. REQ-70 family routing. + // ═══════════════════════════════════════════════════════════════════ + // + // Emitted as ONE raw-string block rather than ~200 `writeln` calls. + // The rest of this file uses per-line `writeln`; at this volume that + // is more transcription error than it is house style, and the block is + // self-contained C with no interpolation. `writeln` indents only the + // first line, which is cosmetic in C. + // + // These mirror `builtins::keselamatan` exactly, including the parts + // that look like bugs and are not: `url_encode` iterates BYTES while + // every other transform iterates CODEPOINTS, and `css_escape` emits a + // trailing space after the hex escape (which CSS requires as a + // terminator). Matching the interpreter matters more than matching + // one's expectations of what the function ought to do. + // + // `constant_time_eq` is security-relevant and is transcribed as a + // non-short-circuiting compare: a C version that returned early on the + // first differing byte would leak by timing where the interpreter does + // not — the same class of gap as the file gate, in a function whose + // entire purpose is to not leak. + self.writeln(r####" +/* ---- UTF-8 decode: one codepoint, advancing *i. Invalid bytes are passed + through as U+FFFD-free single units so behaviour matches Rust's &str + guarantee that the input was already valid UTF-8. ---- */ +static uint32_t riina_sec_utf8_next(const char* s, size_t len, size_t* i) { + unsigned char c = (unsigned char)s[*i]; + if (c < 0x80) { (*i) += 1; return c; } + if ((c & 0xE0) == 0xC0 && *i + 1 < len) { + uint32_t cp = ((uint32_t)(c & 0x1F) << 6) | (uint32_t)(s[*i+1] & 0x3F); + (*i) += 2; return cp; + } + if ((c & 0xF0) == 0xE0 && *i + 2 < len) { + uint32_t cp = ((uint32_t)(c & 0x0F) << 12) | ((uint32_t)(s[*i+1] & 0x3F) << 6) + | (uint32_t)(s[*i+2] & 0x3F); + (*i) += 3; return cp; + } + if ((c & 0xF8) == 0xF0 && *i + 3 < len) { + uint32_t cp = ((uint32_t)(c & 0x07) << 18) | ((uint32_t)(s[*i+1] & 0x3F) << 12) + | ((uint32_t)(s[*i+2] & 0x3F) << 6) | (uint32_t)(s[*i+3] & 0x3F); + (*i) += 4; return cp; + } + (*i) += 1; return c; +} + +static void riina_sec_put_utf8(char** b, size_t* n, size_t* cap, uint32_t cp); + +static void riina_sec_reserve(char** b, size_t* n, size_t* cap, size_t extra) { + while (*n + extra + 1 >= *cap) { + *cap *= 2; + *b = (char*)realloc(*b, *cap); + if (!*b) abort(); + } +} + +static void riina_sec_puts(char** b, size_t* n, size_t* cap, const char* s) { + size_t l = strlen(s); + riina_sec_reserve(b, n, cap, l); + memcpy(*b + *n, s, l); + *n += l; +} + +static void riina_sec_putc(char** b, size_t* n, size_t* cap, char c) { + riina_sec_reserve(b, n, cap, 1); + (*b)[(*n)++] = c; +} + +static void riina_sec_put_utf8(char** b, size_t* n, size_t* cap, uint32_t cp) { + riina_sec_reserve(b, n, cap, 4); + if (cp < 0x80) { (*b)[(*n)++] = (char)cp; } + else if (cp < 0x800) { + (*b)[(*n)++] = (char)(0xC0 | (cp >> 6)); + (*b)[(*n)++] = (char)(0x80 | (cp & 0x3F)); + } else if (cp < 0x10000) { + (*b)[(*n)++] = (char)(0xE0 | (cp >> 12)); + (*b)[(*n)++] = (char)(0x80 | ((cp >> 6) & 0x3F)); + (*b)[(*n)++] = (char)(0x80 | (cp & 0x3F)); + } else { + (*b)[(*n)++] = (char)(0xF0 | (cp >> 18)); + (*b)[(*n)++] = (char)(0x80 | ((cp >> 12) & 0x3F)); + (*b)[(*n)++] = (char)(0x80 | ((cp >> 6) & 0x3F)); + (*b)[(*n)++] = (char)(0x80 | (cp & 0x3F)); + } +} + +/* Rust's char::is_whitespace, which str::trim uses. Enumerated because an + ASCII-only trim would diverge on NBSP and the U+2000 block. */ +static bool riina_sec_is_ws(uint32_t c) { + return c == 0x20 || (c >= 0x09 && c <= 0x0D) || c == 0x85 || c == 0xA0 + || c == 0x1680 || (c >= 0x2000 && c <= 0x200A) || c == 0x2028 + || c == 0x2029 || c == 0x202F || c == 0x205F || c == 0x3000; +} + +static bool riina_sec_ascii_alnum(uint32_t c) { + return (c >= '0' && c <= '9') || (c >= 'A' && c <= 'Z') || (c >= 'a' && c <= 'z'); +} + +#define RIINA_SEC_BEGIN(argv) \ + if ((argv)->tag != RIINA_TAG_STRING) abort(); \ + const char* _s = (argv)->data.string_val.data; \ + size_t _slen = (argv)->data.string_val.len; \ + size_t _cap = _slen * 2 + 16, _n = 0; \ + char* _b = (char*)malloc(_cap); \ + if (!_b) abort(); + +#define RIINA_SEC_END() \ + _b[_n] = 0; \ + riina_value_t* _r = riina_string(_b); \ + free(_b); \ + return _r; + +/* ---- Taint source. Routed alongside the sanitizers deliberately: it is the + ONLY producer of `Tainted`, so without it every sanitizer + would be marked `native-only` while being unreachable from any compiled + program — the REQ-79 "lowers but aborts on contact" trap in a new costume. + Taint is type-level, so the runtime value is just the line. ---- */ +static riina_value_t* riina_builtin_baca_baris(riina_value_t* arg) { + (void)arg; + size_t cap = 256, n = 0; + char* buf = (char*)malloc(cap); + if (!buf) abort(); + int ch; + while ((ch = fgetc(stdin)) != EOF) { + if (n + 2 >= cap) { cap *= 2; buf = (char*)realloc(buf, cap); if (!buf) abort(); } + buf[n++] = (char)ch; + if (ch == '\n') break; + } + buf[n] = 0; + /* Mirrors the interpreter: strip ALL trailing \n and \r, not just one. */ + while (n > 0 && (buf[n-1] == '\n' || buf[n-1] == '\r')) { buf[--n] = 0; } + riina_value_t* r = riina_string(buf); + free(buf); + return r; +} + +static riina_value_t* riina_builtin_sanitize_html(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c == '&') riina_sec_puts(&_b, &_n, &_cap, "&"); + else if (c == '<') riina_sec_puts(&_b, &_n, &_cap, "<"); + else if (c == '>') riina_sec_puts(&_b, &_n, &_cap, ">"); + else if (c == '"') riina_sec_puts(&_b, &_n, &_cap, """); + else if (c == '\'') riina_sec_puts(&_b, &_n, &_cap, "'"); + else if (c == '/') riina_sec_puts(&_b, &_n, &_cap, "/"); + else riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_xml(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c == '&') riina_sec_puts(&_b, &_n, &_cap, "&"); + else if (c == '<') riina_sec_puts(&_b, &_n, &_cap, "<"); + else if (c == '>') riina_sec_puts(&_b, &_n, &_cap, ">"); + else if (c == '"') riina_sec_puts(&_b, &_n, &_cap, """); + else if (c == '\'') riina_sec_puts(&_b, &_n, &_cap, "'"); + else riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_sql(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c == 0) { /* strip NUL */ } + else if (c == '\\') riina_sec_puts(&_b, &_n, &_cap, "\\\\"); + else if (c == '\'') riina_sec_puts(&_b, &_n, &_cap, "''"); + else riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_js(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + char tmp[16]; + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (riina_sec_ascii_alnum(c)) { + riina_sec_putc(&_b, &_n, &_cap, (char)c); + } else if (c < 0x100) { + snprintf(tmp, sizeof(tmp), "\\x%02X", (unsigned)c); + riina_sec_puts(&_b, &_n, &_cap, tmp); + } else if (c < 0x10000) { + snprintf(tmp, sizeof(tmp), "\\u%04X", (unsigned)c); + riina_sec_puts(&_b, &_n, &_cap, tmp); + } else { + /* Rust encode_utf16 yields a surrogate PAIR above the BMP. */ + uint32_t v = c - 0x10000; + snprintf(tmp, sizeof(tmp), "\\u%04X", (unsigned)(0xD800 + (v >> 10))); + riina_sec_puts(&_b, &_n, &_cap, tmp); + snprintf(tmp, sizeof(tmp), "\\u%04X", (unsigned)(0xDC00 + (v & 0x3FF))); + riina_sec_puts(&_b, &_n, &_cap, tmp); + } + } + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_css(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + char tmp[16]; + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (riina_sec_ascii_alnum(c)) { + riina_sec_putc(&_b, &_n, &_cap, (char)c); + } else { + snprintf(tmp, sizeof(tmp), "\\%x ", (unsigned)c); + riina_sec_puts(&_b, &_n, &_cap, tmp); + } + } + RIINA_SEC_END() +} + +/* NOTE: bytes, not codepoints — the interpreter iterates s.bytes() here. */ +static riina_value_t* riina_builtin_sanitize_url(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + char tmp[8]; + for (size_t i = 0; i < _slen; i++) { + unsigned char b = (unsigned char)_s[i]; + if ((b >= 'A' && b <= 'Z') || (b >= 'a' && b <= 'z') || (b >= '0' && b <= '9') + || b == '-' || b == '.' || b == '_' || b == '~') { + riina_sec_putc(&_b, &_n, &_cap, (char)b); + } else { + snprintf(tmp, sizeof(tmp), "%%%02X", b); + riina_sec_puts(&_b, &_n, &_cap, tmp); + } + } + RIINA_SEC_END() +} + +/* Drop NULs, then split on '/' and '\\', dropping empty, "." and ".." + segments, and rejoin with '/'. */ +static riina_value_t* riina_builtin_sanitize_path(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + size_t seg_start = 0; + bool first_out = true; + char* seg = (char*)malloc(_slen + 1); + if (!seg) abort(); + for (size_t i = 0; i <= _slen; i++) { + char ch = (i < _slen) ? _s[i] : '/'; + if (ch == '/' || ch == '\\' || i == _slen) { + size_t sl = 0; + for (size_t k = seg_start; k < i; k++) { + if (_s[k] != 0) seg[sl++] = _s[k]; + } + seg[sl] = 0; + bool skip = (sl == 0) || (strcmp(seg, ".") == 0) || (strcmp(seg, "..") == 0); + if (!skip) { + if (!first_out) riina_sec_putc(&_b, &_n, &_cap, '/'); + riina_sec_puts(&_b, &_n, &_cap, seg); + first_out = false; + } + seg_start = i + 1; + } + } + free(seg); + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_command(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + riina_sec_putc(&_b, &_n, &_cap, '\''); + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c == '\'') riina_sec_puts(&_b, &_n, &_cap, "'\\''"); + else riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + riina_sec_putc(&_b, &_n, &_cap, '\''); + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_ldap(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c == '\\') riina_sec_puts(&_b, &_n, &_cap, "\\5c"); + else if (c == '*') riina_sec_puts(&_b, &_n, &_cap, "\\2a"); + else if (c == '(') riina_sec_puts(&_b, &_n, &_cap, "\\28"); + else if (c == ')') riina_sec_puts(&_b, &_n, &_cap, "\\29"); + else if (c == 0) riina_sec_puts(&_b, &_n, &_cap, "\\00"); + else riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_sanitize_json(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + char tmp[16]; + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c == '"') riina_sec_puts(&_b, &_n, &_cap, "\\\""); + else if (c == '\\') riina_sec_puts(&_b, &_n, &_cap, "\\\\"); + else if (c == 0x08) riina_sec_puts(&_b, &_n, &_cap, "\\b"); + else if (c == 0x0C) riina_sec_puts(&_b, &_n, &_cap, "\\f"); + else if (c == '\n') riina_sec_puts(&_b, &_n, &_cap, "\\n"); + else if (c == '\r') riina_sec_puts(&_b, &_n, &_cap, "\\r"); + else if (c == '\t') riina_sec_puts(&_b, &_n, &_cap, "\\t"); + else if (c == 0x2028) riina_sec_puts(&_b, &_n, &_cap, "\\u2028"); + else if (c == 0x2029) riina_sec_puts(&_b, &_n, &_cap, "\\u2029"); + else if (c < 0x20) { + snprintf(tmp, sizeof(tmp), "\\u%04x", (unsigned)c); + riina_sec_puts(&_b, &_n, &_cap, tmp); + } + else riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +/* Filter CR/LF/NUL, then trim (Rust str::trim = Unicode whitespace). */ +static riina_value_t* riina_builtin_sanitize_email(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + uint32_t* cps = (uint32_t*)malloc((_slen + 1) * sizeof(uint32_t)); + if (!cps) abort(); + size_t ncp = 0; + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c != '\r' && c != '\n' && c != 0) cps[ncp++] = c; + } + size_t lo = 0, hi = ncp; + while (lo < hi && riina_sec_is_ws(cps[lo])) lo++; + while (hi > lo && riina_sec_is_ws(cps[hi-1])) hi--; + for (size_t k = lo; k < hi; k++) riina_sec_put_utf8(&_b, &_n, &_cap, cps[k]); + free(cps); + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_validate_url(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + size_t lo = 0, hi = _slen; + while (lo < hi && (unsigned char)_s[lo] <= 0x20) lo++; + while (hi > lo && (unsigned char)_s[hi-1] <= 0x20) hi--; + size_t tl = hi - lo; + char* t = (char*)malloc(tl + 1); + if (!t) abort(); + memcpy(t, _s + lo, tl); t[tl] = 0; + char* low = (char*)malloc(tl + 1); + if (!low) abort(); + for (size_t k = 0; k < tl; k++) { + char c = t[k]; + low[k] = (c >= 'A' && c <= 'Z') ? (char)(c - 'A' + 'a') : c; + } + low[tl] = 0; + bool ok = strncmp(low, "http://", 7) == 0 || strncmp(low, "https://", 8) == 0 + || strncmp(low, "mailto:", 7) == 0 + || (tl > 0 && t[0] == '/' && !(tl > 1 && t[1] == '/')); + riina_sec_puts(&_b, &_n, &_cap, ok ? t : "about:blank"); + free(t); free(low); + RIINA_SEC_END() +} + +static bool riina_sec_dangerous_format(uint32_t c) { + return (c >= 0x200B && c <= 0x200F) || (c >= 0x202A && c <= 0x202E) + || (c >= 0x2066 && c <= 0x2069) || c == 0x2060 || c == 0x00AD || c == 0xFEFF; +} + +static riina_value_t* riina_builtin_normalize_unicode(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (!riina_sec_dangerous_format(c)) riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +static riina_value_t* riina_builtin_strip_nulls(riina_value_t* arg) { + RIINA_SEC_BEGIN(arg) + for (size_t i = 0; i < _slen; ) { + uint32_t c = riina_sec_utf8_next(_s, _slen, &i); + if (c != 0) riina_sec_put_utf8(&_b, &_n, &_cap, c); + } + RIINA_SEC_END() +} + +/* ---- Modelled sinks. These do NOT perform the dangerous operation; the + interpreter models them and so does this. Their value is that the type + system forces a Disanitasi<_> argument to reach them at all. ---- */ +static riina_value_t* riina_builtin_sql_execute(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + return riina_string(arg->data.string_val.data); +} +static riina_value_t* riina_builtin_ldap_search(riina_value_t* arg) { + return riina_builtin_sql_execute(arg); +} +static riina_value_t* riina_builtin_xml_query(riina_value_t* arg) { + return riina_builtin_sql_execute(arg); +} +static riina_value_t* riina_builtin_js_eval(riina_value_t* arg) { + return riina_builtin_sql_execute(arg); +} +static riina_value_t* riina_builtin_html_render(riina_value_t* arg) { + return riina_builtin_sql_execute(arg); +} +static riina_value_t* riina_builtin_shell_exec(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + return riina_int(0); +} +static riina_value_t* riina_builtin_http_redirect_safe(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + return riina_unit(); +} +/* Mirrors `MODELLED_HTTP_RESPONSE` in builtins/keselamatan.rs. No socket is + opened on either side; the two must agree on the string they invent. */ +#define RIINA_MODELLED_HTTP_RESPONSE "200 OK" +static riina_value_t* riina_builtin_http_get(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + return riina_string(RIINA_MODELLED_HTTP_RESPONSE); +} +static riina_value_t* riina_builtin_http_fetch_safe(riina_value_t* arg) { + return riina_builtin_http_get(arg); +} +static riina_value_t* riina_builtin_http_body(riina_value_t* arg) { + if (arg->tag == RIINA_TAG_STRING) return riina_string(arg->data.string_val.data); + return riina_builtin_ke_teks(arg); +} + +/* ---- Pair-taking members of the family. + + These take ONE argument that is a pair, never two curried arguments: every + signature in riina-typechecker types them `Ty::Prod(..) -> _`, so the surface + form `f(a, b)` is REJECTED AT TYPE-CHECK in both backends and only `f((a, b))` + reaches a runtime. That is why no partial-application machinery is needed + here — the interpreter's `BuiltinPartial` arm is unreachable from well-typed + source, and a C backend that only understands pairs loses nothing. ---- */ + +/* (Tainted, Nombor) -> Option>. Length is counted in + UNICODE SCALAR VALUES, not bytes, so a multi-byte character costs one. */ +static riina_value_t* riina_builtin_validate_length(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* sv = arg->data.pair_val.fst; + riina_value_t* nv = arg->data.pair_val.snd; + if (sv->tag != RIINA_TAG_STRING || nv->tag != RIINA_TAG_INT) abort(); + const char* s = sv->data.string_val.data; + size_t slen = sv->data.string_val.len, i = 0, chars = 0; + while (i < slen) { (void)riina_sec_utf8_next(s, slen, &i); chars++; } + if ((uint64_t)chars <= nv->data.int_val) return riina_inl(riina_string(s)); + return riina_inr(riina_unit()); +} + +static riina_value_t* riina_builtin_dom_set_html(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + return riina_unit(); +} +static riina_value_t* riina_builtin_dom_set_attr(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + return riina_unit(); +} +/* Modelled send: no SMTP is spoken, and the interpreter reports success. */ +static riina_value_t* riina_builtin_email_send(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + return riina_bool(true); +} +static riina_value_t* riina_builtin_email_set_header(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + return riina_unit(); +} + +/* POST/PUT carry (url, (body, csrf_token)); DELETE carries (url, token). All + three answer with the same modelled status line as GET. */ +static riina_value_t* riina_builtin_http_post(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + return riina_string(RIINA_MODELLED_HTTP_RESPONSE); +} +static riina_value_t* riina_builtin_http_put(riina_value_t* arg) { + return riina_builtin_http_post(arg); +} +static riina_value_t* riina_builtin_http_delete(riina_value_t* arg) { + return riina_builtin_http_post(arg); +} + +/* Non-short-circuiting compare: the loop must not stop at the first differing + byte, or the time taken leaks the length of the matching prefix. Length is + compared first, exactly as the interpreter does — that much is already + observable from the token's size. */ +static riina_value_t* riina_builtin_csrf_validate(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_STRING || b->tag != RIINA_TAG_STRING) abort(); + if (a->data.string_val.len != b->data.string_val.len) return riina_bool(false); + unsigned char diff = 0; + for (size_t i = 0; i < a->data.string_val.len; i++) { + diff |= (unsigned char)(a->data.string_val.data[i] ^ b->data.string_val.data[i]); + } + return riina_bool(diff == 0); +} + +/* An EMPTY allowed-origin never matches. Without that guard a program that + forgot to configure one would accept every origin. */ +static riina_value_t* riina_builtin_csrf_check_origin(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* o = arg->data.pair_val.fst; + riina_value_t* w = arg->data.pair_val.snd; + if (o->tag != RIINA_TAG_STRING || w->tag != RIINA_TAG_STRING) abort(); + if (w->data.string_val.len == 0) return riina_bool(false); + if (o->data.string_val.len != w->data.string_val.len) return riina_bool(false); + return riina_bool(memcmp(o->data.string_val.data, w->data.string_val.data, + w->data.string_val.len) == 0); +} +static riina_value_t* riina_builtin_csrf_check_referer(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* r = arg->data.pair_val.fst; + riina_value_t* w = arg->data.pair_val.snd; + if (r->tag != RIINA_TAG_STRING || w->tag != RIINA_TAG_STRING) abort(); + if (w->data.string_val.len == 0) return riina_bool(false); + if (r->data.string_val.len < w->data.string_val.len) return riina_bool(false); + return riina_bool(memcmp(r->data.string_val.data, w->data.string_val.data, + w->data.string_val.len) == 0); +} + +/* No XML tree exists in-tree, so the interpreter models the parse as identity + on the document text and deliberately does NOT resolve entities (no XXE + surface). Identity here too — inventing a tree would be the overclaim. */ +static riina_value_t* riina_builtin_xml_parse_safe(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + return riina_string(arg->data.string_val.data); +} +"####); // FILE I/O BUILTINS (fail) // ═══════════════════════════════════════════════════════════════════ @@ -3475,6 +4086,63 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { self.writeln("}"); self.writeln(""); + // The keselamatan safe-file trio. They live HERE rather than with the + // rest of their family because they go through the SAME verified gate as + // `fail_*` — `riina_gate` is defined above and the security family is + // emitted before it. The interpreter shares `fail::gate_read` / + // `gate_write` / `gate_delete` for exactly this reason; a "safe" file op + // that skipped the access check would be the REQ-72 bypass wearing the + // word `selamat`. The gate is passed the SAFE builtin's own name so a + // denial says which call site was refused. + self.writeln( + r####" +static riina_value_t* riina_builtin_file_read_safe(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + riina_gate("file_read_safe", arg->data.string_val.data, false); + FILE* f = fopen(arg->data.string_val.data, "r"); + if (!f) { + fprintf(stderr, "RIINA: file_read_safe: cannot read '%s'\n", arg->data.string_val.data); + exit(1); + } + fseek(f, 0, SEEK_END); + long sz = ftell(f); + fseek(f, 0, SEEK_SET); + char* buf = (char*)malloc((size_t)sz + 1); + if (!buf) abort(); + size_t rd = fread(buf, 1, (size_t)sz, f); + buf[rd] = '\0'; + fclose(f); + riina_value_t* r = riina_string(buf); + free(buf); + return r; +} + +static riina_value_t* riina_builtin_file_write_safe(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_PAIR) abort(); + riina_value_t* path = arg->data.pair_val.fst; + riina_value_t* content = arg->data.pair_val.snd; + if (path->tag != RIINA_TAG_STRING || content->tag != RIINA_TAG_STRING) abort(); + riina_gate("file_write_safe", path->data.string_val.data, true); + FILE* f = fopen(path->data.string_val.data, "w"); + if (!f) { + fprintf(stderr, "RIINA: file_write_safe: cannot write '%s'\n", path->data.string_val.data); + exit(1); + } + fwrite(content->data.string_val.data, 1, content->data.string_val.len, f); + fclose(f); + return riina_unit(); +} + +/* Returns whether the removal succeeded rather than stopping the program — the + interpreter's `remove_file(..).is_ok()`. The GATE still stops it. */ +static riina_value_t* riina_builtin_file_delete_safe(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + riina_gate_delete("file_delete_safe", arg->data.string_val.data); + return riina_bool(remove(arg->data.string_val.data) == 0); +} +"####, + ); + // fail_panjang (file_size): Teks -> Int self.writeln("static riina_value_t* riina_builtin_fail_panjang(riina_value_t* arg) {"); self.writeln(" if (arg->tag != RIINA_TAG_STRING) abort();"); @@ -3524,157 +4192,333 @@ static riina_value_t* riina_builtin_qmn(riina_value_t* arg) { // JSON BUILTINS // ═══════════════════════════════════════════════════════════════════ - // Forward-declare the recursive parser - self.writeln("static riina_value_t* riina_json_parse_value(const char** p);"); - self.writeln(""); - - // Skip whitespace helper - self.writeln("static void riina_json_skip_ws(const char** p) {"); + // The parser is emitted as one raw string rather than per-line + // `writeln` calls (the house style elsewhere in this file). At this + // volume of C the escaping noise of the per-line form actively hides + // bugs — which is how the LENIENT parser this replaces went unnoticed. + // + // STRICTNESS IS THE POINT. The previous emitter never failed: garbage + // fell through to `strtoll` and became `0`, `nul` became `()`, `12abc` + // became `12`, and an unterminated array closed itself. The interpreter + // (`builtins/json.rs`) rejects all four. 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", cannot be routed to a + // backend that has no notion of malformed. + // + // So this mirrors `builtins/json.rs` production-for-production, + // including the parts that are not obviously deliberate: + // * whitespace is UNICODE (`str::trim`), not the ASCII four; + // * `\uD800`-`\uDFFF` decode to nothing at all (`char::from_u32` + // returns None and the interpreter pushes no character); + // * a number is read as `u64` first and only then as `f64` with a + // SATURATING cast, so `-5` is `0` and not a huge unsigned value; + // * trailing content after the top-level value is an error. + // Failure is recorded rather than raised in place, because `json_urai` + // must report it and `json_parse_safe` must swallow it. self.writeln( - " while (**p == ' ' || **p == '\\t' || **p == '\\n' || **p == '\\r') (*p)++;", - ); - self.writeln("}"); - self.writeln(""); + r####" +static bool riina_json_has_err = false; +static char riina_json_errbuf[192]; + +static void riina_json_fail(const char* msg) { + if (riina_json_has_err) return; + riina_json_has_err = true; + snprintf(riina_json_errbuf, sizeof(riina_json_errbuf), "%s", msg); +} + +/* Decode one codepoint from a NUL-terminated buffer. A truncated or invalid + sequence advances one byte and reports U+FFFD, which is never whitespace and + never a structural character, so the caller treats it as ordinary text. */ +static uint32_t riina_json_cp(const char* p, size_t* adv) { + unsigned char c0 = (unsigned char)p[0]; + unsigned char c1 = (unsigned char)p[1]; + if (c0 < 0x80) { *adv = 1; return c0; } + if ((c0 & 0xE0) == 0xC0 && (c1 & 0xC0) == 0x80) { + *adv = 2; return ((uint32_t)(c0 & 0x1F) << 6) | (uint32_t)(c1 & 0x3F); + } + unsigned char c2 = c1 ? (unsigned char)p[2] : 0; + if ((c0 & 0xF0) == 0xE0 && (c1 & 0xC0) == 0x80 && (c2 & 0xC0) == 0x80) { + *adv = 3; + return ((uint32_t)(c0 & 0x0F) << 12) | ((uint32_t)(c1 & 0x3F) << 6) + | (uint32_t)(c2 & 0x3F); + } + unsigned char c3 = c2 ? (unsigned char)p[3] : 0; + if ((c0 & 0xF8) == 0xF0 && (c1 & 0xC0) == 0x80 && (c2 & 0xC0) == 0x80 + && (c3 & 0xC0) == 0x80) { + *adv = 4; + return ((uint32_t)(c0 & 0x07) << 18) | ((uint32_t)(c1 & 0x3F) << 12) + | ((uint32_t)(c2 & 0x3F) << 6) | (uint32_t)(c3 & 0x3F); + } + *adv = 1; return 0xFFFD; +} + +/* `str::trim_start`. Unicode, because the interpreter's is: an NBSP-indented + document parses there and must parse here. */ +static void riina_json_skip_ws(const char** p) { + while (**p) { + size_t adv; uint32_t c = riina_json_cp(*p, &adv); + if (!riina_sec_is_ws(c)) return; + *p += adv; + } +} + +static riina_value_t* riina_json_parse_value(const char** p); + +static riina_value_t* riina_json_parse_string(const char** p) { + (*p)++; /* opening quote; the caller has already matched it */ + size_t cap = 64, len = 0; + char* buf = (char*)malloc(cap); + if (!buf) abort(); + for (;;) { + if (len + 8 >= cap) { + cap *= 2; buf = (char*)realloc(buf, cap); if (!buf) abort(); + } + if (**p == '\0') { + free(buf); riina_json_fail("unterminated string"); return NULL; + } + if (**p == '"') { + (*p)++; buf[len] = '\0'; + riina_value_t* r = riina_string(buf); + free(buf); + return r; + } + if (**p != '\\') { + size_t adv; (void)riina_json_cp(*p, &adv); + for (size_t k = 0; k < adv; k++) buf[len++] = (*p)[k]; + *p += adv; + continue; + } + (*p)++; + char e = **p; + if (e == '"') { buf[len++] = '"'; (*p)++; continue; } + if (e == '\\') { buf[len++] = '\\'; (*p)++; continue; } + if (e == '/') { buf[len++] = '/'; (*p)++; continue; } + if (e == 'n') { buf[len++] = '\n'; (*p)++; continue; } + if (e == 'r') { buf[len++] = '\r'; (*p)++; continue; } + if (e == 't') { buf[len++] = '\t'; (*p)++; continue; } + if (e == 'b') { buf[len++] = '\b'; (*p)++; continue; } + if (e == 'f') { buf[len++] = '\f'; (*p)++; continue; } + if (e != 'u') { + /* Covers end-of-input too: the interpreter's `_ => invalid escape` + arm matches `None` as well as an unknown character. */ + free(buf); riina_json_fail("invalid escape"); return NULL; + } + (*p)++; + /* The interpreter takes FOUR CHARS and then checks the BYTE length, so + a multi-byte char inside the escape is not "incomplete" — it reaches + `from_str_radix` and fails as "invalid" instead. Mirror both arms. */ + const char* hex = *p; + int nchars = 0; + while (nchars < 4 && **p) { + size_t adv; (void)riina_json_cp(*p, &adv); + *p += adv; nchars++; + } + size_t nbytes = (size_t)(*p - hex); + if (nbytes < 4) { + free(buf); riina_json_fail("incomplete unicode escape"); return NULL; + } + /* `u32::from_str_radix` accepts an optional leading '+' and nothing + else outside the digits. Anything wider than 4 bytes contains a + non-ASCII char and so cannot be radix-16 digits. */ + bool ok = (nbytes == 4); + size_t i = (ok && hex[0] == '+') ? 1 : 0; + if (ok && i == nbytes) ok = false; + uint32_t cp = 0; + for (; ok && i < nbytes; i++) { + char h = hex[i]; int d; + if (h >= '0' && h <= '9') d = h - '0'; + else if (h >= 'a' && h <= 'f') d = h - 'a' + 10; + else if (h >= 'A' && h <= 'F') d = h - 'A' + 10; + else { ok = false; break; } + cp = (cp << 4) | (uint32_t)d; + } + if (!ok) { + free(buf); riina_json_fail("invalid unicode escape"); return NULL; + } + /* A lone surrogate is `char::from_u32(cp) == None`, and the interpreter + pushes NOTHING in that case rather than erroring. */ + if (cp >= 0xD800 && cp <= 0xDFFF) continue; + if (cp < 0x80) { + buf[len++] = (char)cp; + } else if (cp < 0x800) { + buf[len++] = (char)(0xC0 | (cp >> 6)); + buf[len++] = (char)(0x80 | (cp & 0x3F)); + } else { + buf[len++] = (char)(0xE0 | (cp >> 12)); + buf[len++] = (char)(0x80 | ((cp >> 6) & 0x3F)); + buf[len++] = (char)(0x80 | (cp & 0x3F)); + } + } +} - // Parse string (returns riina_value_t* STRING) - self.writeln("static riina_value_t* riina_json_parse_string(const char** p) {"); - self.writeln(" if (**p != '\"') abort();"); - self.writeln(" (*p)++;"); - self.writeln(" size_t cap = 64, len = 0;"); - self.writeln(" char* buf = (char*)malloc(cap);"); - self.writeln(" if (!buf) abort();"); - self.writeln(" while (**p && **p != '\"') {"); - self.writeln(" if (len + 4 >= cap) { cap *= 2; buf = (char*)realloc(buf, cap); if (!buf) abort(); }"); - self.writeln(" if (**p == '\\\\') {"); - self.writeln(" (*p)++;"); - self.writeln(" switch (**p) {"); - self.writeln(" case '\"': buf[len++] = '\"'; break;"); - self.writeln(" case '\\\\': buf[len++] = '\\\\'; break;"); - self.writeln(" case '/': buf[len++] = '/'; break;"); - self.writeln(" case 'n': buf[len++] = '\\n'; break;"); - self.writeln(" case 'r': buf[len++] = '\\r'; break;"); - self.writeln(" case 't': buf[len++] = '\\t'; break;"); - self.writeln(" case 'b': buf[len++] = '\\b'; break;"); - self.writeln(" case 'f': buf[len++] = '\\f'; break;"); - self.writeln(" case 'u': {"); - self.writeln(" /* \\uXXXX -> UTF-8. The interpreter does"); - self.writeln(" char::from_u32(cp) and pushes on Some, so an"); - self.writeln(" unpaired surrogate is dropped; match that. Without"); - self.writeln(" this case the default arm emitted a literal 'u' and"); - self.writeln(" the four hex digits fell through as ordinary text. */"); - self.writeln(" unsigned int cp = 0; int nhex = 0;"); - self.writeln(" for (int i = 0; i < 4; i++) {"); - self.writeln(" char h = (*p)[1]; int d;"); - self.writeln(" if (h >= '0' && h <= '9') d = h - '0';"); - self.writeln(" else if (h >= 'a' && h <= 'f') d = h - 'a' + 10;"); - self.writeln(" else if (h >= 'A' && h <= 'F') d = h - 'A' + 10;"); - self.writeln(" else break;"); - self.writeln(" cp = (cp << 4) | (unsigned int)d; (*p)++; nhex++;"); - self.writeln(" }"); - self.writeln(" if (nhex == 4 && !(cp >= 0xD800 && cp <= 0xDFFF)) {"); - self.writeln(" if (cp < 0x80) {"); - self.writeln(" buf[len++] = (char)cp;"); - self.writeln(" } else if (cp < 0x800) {"); - self.writeln(" buf[len++] = (char)(0xC0 | (cp >> 6));"); - self.writeln(" buf[len++] = (char)(0x80 | (cp & 0x3F));"); - self.writeln(" } else {"); - self.writeln(" buf[len++] = (char)(0xE0 | (cp >> 12));"); - self.writeln(" buf[len++] = (char)(0x80 | ((cp >> 6) & 0x3F));"); - self.writeln(" buf[len++] = (char)(0x80 | (cp & 0x3F));"); - self.writeln(" }"); - self.writeln(" }"); - self.writeln(" break;"); - self.writeln(" }"); - self.writeln(" default: buf[len++] = **p; break;"); - self.writeln(" }"); - self.writeln(" } else {"); - self.writeln(" buf[len++] = **p;"); - self.writeln(" }"); - self.writeln(" (*p)++;"); - self.writeln(" }"); - self.writeln(" if (**p == '\"') (*p)++;"); - self.writeln(" buf[len] = '\\0';"); - self.writeln(" riina_value_t* r = riina_string(buf);"); - self.writeln(" free(buf);"); - self.writeln(" return r;"); - self.writeln("}"); - self.writeln(""); +/* `u64` first, then `f64` with Rust's SATURATING `as u64`. The old emitter used + `strtoll` and a C cast, so `-5` became 18446744073709551611 where the + interpreter gives 0. */ +static riina_value_t* riina_json_parse_number(const char** p) { + const char* s = *p; + size_t end = 0; + while (s[end]) { + char c = s[end]; + bool allowed = (c >= '0' && c <= '9') || c == '-' || c == '.' + || c == 'e' || c == 'E' || c == '+'; + if (!allowed) break; + end++; + } + char nbuf[128]; + if (end >= sizeof(nbuf)) { + riina_json_fail("cannot parse number"); return NULL; + } + memcpy(nbuf, s, end); + nbuf[end] = '\0'; + *p = s + end; + + bool u_ok = true; + size_t i = (nbuf[0] == '+') ? 1 : 0; + if (nbuf[i] == '\0') u_ok = false; + unsigned long long uv = 0; + for (size_t k = i; u_ok && nbuf[k]; k++) { + if (nbuf[k] < '0' || nbuf[k] > '9') { u_ok = false; break; } + unsigned long long d = (unsigned long long)(nbuf[k] - '0'); + if (uv > (0xFFFFFFFFFFFFFFFFULL - d) / 10ULL) { u_ok = false; break; } + uv = uv * 10ULL + d; + } + if (u_ok) return riina_int((uint64_t)uv); + + char* fend = NULL; + double d = strtod(nbuf, &fend); + if (fend == nbuf || *fend != '\0') { + char msg[160]; + snprintf(msg, sizeof(msg), "cannot parse number: '%s'", nbuf); + riina_json_fail(msg); + return NULL; + } + if (!(d == d) || d <= 0.0) return riina_int(0); /* NaN, negatives */ + if (d >= 18446744073709551616.0) return riina_int(0xFFFFFFFFFFFFFFFFULL); + return riina_int((uint64_t)d); +} + +static riina_value_t* riina_json_parse_object(const char** p) { + (*p)++; /* '{' */ + riina_map_t m = { NULL, 0 }; + riina_json_skip_ws(p); + if (**p == '}') { (*p)++; return riina_make_map(m); } + for (;;) { + riina_json_skip_ws(p); + if (**p != '"') { riina_json_fail("expected string key in object"); return NULL; } + riina_value_t* key = riina_json_parse_string(p); + if (!key) return NULL; + riina_json_skip_ws(p); + if (**p != ':') { riina_json_fail("expected ':' in object"); return NULL; } + (*p)++; + riina_value_t* val = riina_json_parse_value(p); + if (!val) return NULL; + /* Sorted insert: the interpreter parses into a BTreeMap, so a duplicate + key keeps the LAST value and iteration is by key. */ + riina_map_put_sorted(&m, key->data.string_val.data, val); + riina_json_skip_ws(p); + if (**p == '}') { (*p)++; return riina_make_map(m); } + if (**p == ',') { (*p)++; continue; } + riina_json_fail("expected ',' or '}' in object"); + return NULL; + } +} - // Parse number - self.writeln("static riina_value_t* riina_json_parse_number(const char** p) {"); - self.writeln(" char* end;"); - self.writeln(" long long val = strtoll(*p, &end, 10);"); - self.writeln(" *p = end;"); - self.writeln(" /* Skip fractional/exponent parts */"); - self.writeln(" if (**p == '.') { strtod(*p - (end - *p), &end); *p = end; }"); - self.writeln(" return riina_int((uint64_t)val);"); - self.writeln("}"); - self.writeln(""); +static riina_value_t* riina_json_parse_array(const char** p) { + (*p)++; /* '[' */ + riina_list_t l = riina_list_new(); + riina_json_skip_ws(p); + if (**p == ']') { (*p)++; return riina_make_list(l); } + for (;;) { + riina_value_t* val = riina_json_parse_value(p); + if (!val) return NULL; + riina_list_push(&l, val); + riina_json_skip_ws(p); + if (**p == ']') { (*p)++; return riina_make_list(l); } + if (**p == ',') { (*p)++; continue; } + riina_json_fail("expected ',' or ']' in array"); + return NULL; + } +} - // Parse object - self.writeln("static riina_value_t* riina_json_parse_object(const char** p) {"); - self.writeln(" (*p)++; /* skip '{' */"); - self.writeln(" riina_map_t m = { NULL, 0 };"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" if (**p == '}') { (*p)++; return riina_make_map(m); }"); - self.writeln(" for (;;) {"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" riina_value_t* key = riina_json_parse_string(p);"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" if (**p == ':') (*p)++;"); - self.writeln(" riina_value_t* val = riina_json_parse_value(p);"); - self.writeln(" /* Sorted insert: the interpreter parses into a BTreeMap, so a"); - self.writeln(" duplicate key keeps the LAST value and iteration is by key. */"); - self.writeln(" riina_map_put_sorted(&m, key->data.string_val.data, val);"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" if (**p == ',') { (*p)++; continue; }"); - self.writeln(" if (**p == '}') { (*p)++; break; }"); - self.writeln(" break;"); - self.writeln(" }"); - self.writeln(" return riina_make_map(m);"); - self.writeln("}"); - self.writeln(""); +static bool riina_json_eat(const char** p, const char* lit) { + size_t n = strlen(lit); + if (strncmp(*p, lit, n) != 0) return false; + *p += n; + return true; +} - // Parse array - self.writeln("static riina_value_t* riina_json_parse_array(const char** p) {"); - self.writeln(" (*p)++; /* skip '[' */"); - self.writeln(" riina_list_t l = riina_list_new();"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" if (**p == ']') { (*p)++; return riina_make_list(l); }"); - self.writeln(" for (;;) {"); - self.writeln(" riina_value_t* val = riina_json_parse_value(p);"); - self.writeln(" riina_list_push(&l, val);"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" if (**p == ',') { (*p)++; continue; }"); - self.writeln(" if (**p == ']') { (*p)++; break; }"); - self.writeln(" break;"); - self.writeln(" }"); - self.writeln(" return riina_make_list(l);"); - self.writeln("}"); - self.writeln(""); +static riina_value_t* riina_json_parse_value(const char** p) { + riina_json_skip_ws(p); + if (**p == '\0') { riina_json_fail("unexpected end of input"); return NULL; } + char c = **p; + if (c == '"') return riina_json_parse_string(p); + if (c == '{') return riina_json_parse_object(p); + if (c == '[') return riina_json_parse_array(p); + if (c == 't' || c == 'f') { + if (riina_json_eat(p, "true")) return riina_bool(true); + if (riina_json_eat(p, "false")) return riina_bool(false); + riina_json_fail("expected 'true' or 'false'"); + return NULL; + } + if (c == 'n') { + if (riina_json_eat(p, "null")) return riina_unit(); + riina_json_fail("expected 'null'"); + return NULL; + } + if (c == '-' || (c >= '0' && c <= '9')) return riina_json_parse_number(p); + char msg[64]; + snprintf(msg, sizeof(msg), "unexpected char '%c'", c); + riina_json_fail(msg); + return NULL; +} - // Parse value (recursive dispatch) - self.writeln("static riina_value_t* riina_json_parse_value(const char** p) {"); - self.writeln(" riina_json_skip_ws(p);"); - self.writeln(" switch (**p) {"); - self.writeln(" case '\"': return riina_json_parse_string(p);"); - self.writeln(" case '{': return riina_json_parse_object(p);"); - self.writeln(" case '[': return riina_json_parse_array(p);"); - self.writeln(" case 't': (*p) += 4; return riina_bool(true);"); - self.writeln(" case 'f': (*p) += 5; return riina_bool(false);"); - self.writeln(" case 'n': (*p) += 4; return riina_unit();"); - self.writeln(" default: return riina_json_parse_number(p);"); - self.writeln(" }"); - self.writeln("}"); - self.writeln(""); +/* Whole document: a value, then nothing but whitespace. NULL ⇒ malformed, with + the reason in riina_json_errbuf. */ +static riina_value_t* riina_json_parse_document(const char* s) { + riina_json_has_err = false; + riina_json_errbuf[0] = '\0'; + const char* p = s; + riina_value_t* v = riina_json_parse_value(&p); + if (!v) return NULL; + riina_json_skip_ws(&p); + if (*p != '\0') { + char msg[160]; + snprintf(msg, sizeof(msg), "unexpected trailing content: '%.20s'", p); + riina_json_fail(msg); + return NULL; + } + return v; +} - // json_urai (json_parse): Teks -> Value - self.writeln("static riina_value_t* riina_builtin_json_urai(riina_value_t* arg) {"); - self.writeln(" if (arg->tag != RIINA_TAG_STRING) abort();"); - self.writeln(" const char* p = arg->data.string_val.data;"); - self.writeln(" return riina_json_parse_value(&p);"); - self.writeln("}"); - self.writeln(""); +/* json_urai (json_parse): Teks -> Value. Malformed input is a runtime error, as + in the interpreter — not a fabricated value. */ +static riina_value_t* riina_builtin_json_urai(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + riina_value_t* v = riina_json_parse_document(arg->data.string_val.data); + if (!v) { + fprintf(stderr, "RIINA: invalid operation: json_urai: %s\n", riina_json_errbuf); + exit(1); + } + return v; +} + +/* json_parse_safe / deserialize_safe: the SAME parser, with malformed input + yielding Unit instead of stopping the program. That contract is the reason + the strict parser above had to exist first. */ +static riina_value_t* riina_builtin_json_parse_safe(riina_value_t* arg) { + if (arg->tag != RIINA_TAG_STRING) abort(); + riina_value_t* v = riina_json_parse_document(arg->data.string_val.data); + return v ? v : riina_unit(); +} + +/* nyahsiri_selamat. The interpreter dispatches it to the same JSON parser, so + this is an alias and not a second format. */ +static riina_value_t* riina_builtin_deserialize_safe(riina_value_t* arg) { + return riina_builtin_json_parse_safe(arg); +} +"####, + ); // JSON stringify helper (forward declare for recursion) self.writeln("static void riina_json_stringify_impl(riina_value_t* v, char** buf, size_t* len, size_t* cap);"); diff --git a/03_PROTO/crates/riina-codegen/src/lower.rs b/03_PROTO/crates/riina-codegen/src/lower.rs index 5088274e..480ebed2 100644 --- a/03_PROTO/crates/riina-codegen/src/lower.rs +++ b/03_PROTO/crates/riina-codegen/src/lower.rs @@ -151,6 +151,95 @@ pub(crate) fn builtin_canonical(name: &str) -> Option<&'static str> { return Some(canonical); } } + // Security builtins (keselamatan) — REQ-70 family routing. 41 of the 42 are + // here; `csrf_generate` is the single exclusion and is justified below. + // + // ON THE PAIR-TAKING MEMBERS. An earlier increment routed only the + // single-argument subset, on the reasoning that eleven members take a pair + // and `split_pair` hands back a `Value::BuiltinPartial` for a non-pair + // argument, which the C backend has no equivalent of. That reasoning was + // WRONG, and checking it rather than repeating it is what unblocked the + // rest of the family: every one of those signatures is typed + // `Ty::Prod(..) -> _` in riina-typechecker, so the curried surface 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. + // + // NOT ROUTED: `csrf_generate` / `csrf_jana`. It is the one member whose + // result is not a function of its input — a token seeded from the clock and + // a process-local counter — so the two backends cannot be held to agreement + // by a differential, only to a shape. Mirroring it would mean transcribing + // Rust's `DefaultHasher` into C to reproduce a generator its own doc comment + // already marks as "a *reference* token, not a certified CSPRNG". Spreading + // that to a second implementation makes the eventual fix twice the work and + // buys nothing: `csrf_validate` takes plain `Teks`, so a compiled program + // can still carry tokens minted elsewhere and is not cut off from the + // family the way the sanitizers would have been without `baca_baris`. + match name { + // The taint SOURCE. Routed with the sanitizers because it is their only + // input: `Tainted` has exactly one producer, so + // routing the sanitizers alone would mark them native-only while + // leaving them unreachable from compiled code. + "baca_baris" | "read_line" | "baca_garisan" => return Some("baca_baris"), + // Sanitizers — pure transforms, mirrored byte-for-byte in emit.rs. + "sanitasi_html" | "sanitize_html" => return Some("sanitize_html"), + "sanitasi_xml" | "sanitize_xml" => return Some("sanitize_xml"), + "sanitasi_sql" | "sanitize_sql" => return Some("sanitize_sql"), + "sanitasi_js" | "sanitize_js" => return Some("sanitize_js"), + "sanitasi_css" | "sanitize_css" => return Some("sanitize_css"), + "sanitasi_url" | "sanitize_url" => return Some("sanitize_url"), + "sanitasi_laluan" | "sanitize_path" => return Some("sanitize_path"), + "sanitasi_perintah" | "sanitize_command" => return Some("sanitize_command"), + "sanitasi_ldap" | "sanitize_ldap" => return Some("sanitize_ldap"), + "sanitasi_json" | "sanitize_json" => return Some("sanitize_json"), + "sanitasi_emel" | "sanitize_email" => return Some("sanitize_email"), + // Validators / normalizers. + "sahkan_url" | "validate_url" => return Some("validate_url"), + "normal_unicode" | "normalize_unicode" => return Some("normalize_unicode"), + "buang_null" | "strip_nulls" => return Some("strip_nulls"), + // Modelled sinks. These do NOT perform the dangerous operation in + // either backend — their value is that the type system forces a + // `Disanitasi<_>` argument to reach them at all, which is a + // compile-time property and so already holds for both backends. + "sql_laksana" | "sql_execute" => return Some("sql_execute"), + "ldap_cari" | "ldap_search" => return Some("ldap_search"), + "xml_cari" | "xml_query" => return Some("xml_query"), + "js_nilai" | "js_eval" => return Some("js_eval"), + "html_papar" | "html_render" => return Some("html_render"), + "shell_laksana" | "shell_exec" => return Some("shell_exec"), + "http_arah_selamat" | "http_redirect_safe" => return Some("http_redirect_safe"), + "http_dapat" | "http_get" => return Some("http_get"), + "http_ambil_selamat" | "http_fetch_safe" => return Some("http_fetch_safe"), + "badan_http" | "http_body" => return Some("http_body"), + // Pair-taking sinks. Modelled the same way, and reached only through an + // explicit tuple (see the note above). + "dom_tetap_html" | "dom_set_html" => return Some("dom_set_html"), + "dom_tetap_atribut" | "dom_set_attr" => return Some("dom_set_attr"), + "emel_hantar" | "email_send" => return Some("email_send"), + "emel_tetap_kepala" | "email_set_header" => return Some("email_set_header"), + "http_hantar" | "http_post" => return Some("http_post"), + "http_kemaskini" | "http_put" => return Some("http_put"), + "http_padam" | "http_delete" => return Some("http_delete"), + // Input validation. Counts UNICODE SCALAR VALUES, not bytes. + "sahkan_panjang" | "validate_length" => return Some("validate_length"), + // CSRF checks — pure predicates over their two arguments. + "csrf_sahkan" | "csrf_validate" => return Some("csrf_validate"), + "csrf_semak_origin" | "csrf_check_origin" => return Some("csrf_check_origin"), + "csrf_semak_referer" | "csrf_check_referer" => return Some("csrf_check_referer"), + // Safe file I/O. Routable only because these share the verified gate + // with `fail_*`, which the emitted C now carries. + "fail_baca_selamat" | "file_read_safe" => return Some("file_read_safe"), + "fail_tulis_selamat" | "file_write_safe" => return Some("file_write_safe"), + "fail_buang_selamat" | "file_delete_safe" => return Some("file_delete_safe"), + // Safe parsers. Routable only because the emitted JSON parser is now + // STRICT: "malformed input yields Unit" is not a contract a lenient + // parser can honour, and the old one never failed on anything. + "json_urai_selamat" | "json_parse_safe" => return Some("json_parse_safe"), + "nyahsiri_selamat" | "deserialize_safe" => return Some("deserialize_safe"), + "xml_urai_selamat" | "xml_parse_safe" => return Some("xml_parse_safe"), + _ => {} + } // File builtins (REQ-70 family routing) — routed ONLY because the emitted // C now carries the verified gate. // diff --git a/03_PROTO/crates/riinac/tests/collection_differential.rs b/03_PROTO/crates/riinac/tests/collection_differential.rs index ccdd8781..0f468805 100644 --- a/03_PROTO/crates/riinac/tests/collection_differential.rs +++ b/03_PROTO/crates/riinac/tests/collection_differential.rs @@ -189,3 +189,42 @@ fn map_and_set_agree() { \x20 cetakln(ke_teks(set_panjang(s)));", ); } + +// ── Rendering composite values ───────────────────────────────────────────── + +/// `cetakln` and `ke_teks` both render through one function, and until REQ-70's +/// keselamatan increment the C one answered the literal text `` for every +/// composite tag: PAIR, LIST, MAP and both SUM arms. A compiled program printing +/// a list showed `` where `riinac run` shows `[1, 2, 3]`. +/// +/// The cases here separate the two rendering modes the interpreter actually has, +/// because a C author mirroring only the obvious one would still pass a +/// list-of-ints test: +/// +/// * `builtins::format_value` prints a string BARE and a bool as `betul`/`salah`; +/// * `Value`'s `Display` — which `format_value` falls through to, and which is +/// the ONLY path a sum takes — QUOTES the string and prints Rust's English +/// `true`/`false`. +/// +/// So the same bool renders `betul` inside a list and `true` inside a sum. That +/// is an inconsistency in the reference rather than a design; it is pinned here +/// so that changing it is a deliberate language decision and not codegen drift. +#[test] +fn composite_values_render_identically() { + assert_backends_agree("fmt_list", " cetakln(ke_teks([1, 2, 3]));"); + assert_backends_agree("fmt_pair", " cetakln(ke_teks((1, \"dua\")));"); + assert_backends_agree("fmt_nested", " cetakln(ke_teks(([1, 2], (betul, ()))));"); +} + +/// The mode split, isolated: a bool and a string each rendered directly, inside +/// a list, and inside a sum. +#[test] +fn sum_rendering_uses_display_not_format_value() { + assert_backends_agree( + "fmt_modes", + " cetakln(ke_teks(betul));\n\ + \x20 cetakln(ke_teks([betul, salah]));\n\ + \x20 cetakln(ke_teks(\"teks\"));\n\ + \x20 cetakln(ke_teks([\"teks\"]));", + ); +} diff --git a/03_PROTO/crates/riinac/tests/json_differential.rs b/03_PROTO/crates/riinac/tests/json_differential.rs index 5eb2ff75..ea271a4c 100644 --- a/03_PROTO/crates/riinac/tests/json_differential.rs +++ b/03_PROTO/crates/riinac/tests/json_differential.rs @@ -213,3 +213,120 @@ fn accessors_agree() { " cetakln(json_ke_teks(json_letak((json_urai(\"{\\\"z\\\":1}\"), (\"a\", 9)))));", ); } + +// ── Malformed input ──────────────────────────────────────────────────────── + +/// Run one program under both backends and require BOTH to fail, having printed +/// the same output up to the point of failure. +/// +/// The success-only helper above cannot express this, which is precisely how the +/// divergence these cases pin survived: every existing case fed WELL-FORMED +/// JSON, so a C parser that could not fail was never asked to. +fn assert_backends_both_reject(tag: &str, body: &str) { + let dir = std::env::temp_dir().join(format!("riina_req70_jsonbad_{tag}_{}", std::process::id())); + let _ = std::fs::remove_dir_all(&dir); + std::fs::create_dir_all(&dir).expect("create dir"); + let stem = format!("ujian_jsonbad_{tag}"); + let src: PathBuf = dir.join(format!("{stem}.rii")); + 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(), + "the interpreter ACCEPTED malformed JSON for {tag} — this test's premise \ + is that it rejects it: {}", + String::from_utf8_lossy(&interp.stdout) + ); + let interp_out = String::from_utf8_lossy(&interp.stdout).into_owned(); + + 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"); + let c_out = String::from_utf8_lossy(&run.stdout).into_owned(); + assert!( + !run.status.success(), + "THE REGRESSION: the compiled binary accepted malformed JSON for {tag} \ + and printed {c_out:?} where `riinac run` refuses. A backend that \ + invents a value for input the interpreter rejects is a silent \ + correctness hole on attacker-controlled data." + ); + assert_eq!( + interp_out, c_out, + "backends printed different output before failing for {tag}" + ); + + let _ = std::fs::remove_dir_all(&dir); +} + +/// Each case is one arm the old lenient emitter took SILENTLY, with the value it +/// invented: `xyz` and `""` became `0` (everything fell through to `strtoll`), +/// `12abc` became `12` (no trailing-content check), `nul` became `()` (the +/// literal arms advanced a fixed width without comparing), and `[1,2` closed +/// itself into `[1,2]`. +#[test] +fn malformed_documents_are_rejected_by_both() { + assert_backends_both_reject("mal_word", " cetakln(ke_teks(json_urai(\"xyz\")));"); + assert_backends_both_reject("mal_empty", " cetakln(ke_teks(json_urai(\"\")));"); + assert_backends_both_reject("mal_trail", " cetakln(ke_teks(json_urai(\"12abc\")));"); + assert_backends_both_reject("mal_nul", " cetakln(ke_teks(json_urai(\"nul\")));"); + assert_backends_both_reject("mal_arr", " cetakln(ke_teks(json_urai(\"[1,2\")));"); + assert_backends_both_reject( + "mal_obj", + " cetakln(ke_teks(json_urai(\"{\\\"a\\\" 1}\")));", + ); + assert_backends_both_reject( + "mal_str", + " cetakln(ke_teks(json_urai(\"\\\"unterminated\")));", + ); +} + +/// Output printed BEFORE the malformed parse must survive in both backends, so +/// the failure is a stop and not a silent difference in flush behaviour. +#[test] +fn output_before_a_rejected_parse_is_identical() { + assert_backends_both_reject( + "mal_prefix", + " cetakln(\"before\");\n\ + \x20 cetakln(ke_teks(json_urai(\"nope\")));\n\ + \x20 cetakln(\"after\");", + ); +} + +/// A NEGATIVE number is the case where the old emitter produced a plausible +/// wrong answer rather than an obvious one: `strtoll` gave -5 and the cast to +/// `uint64_t` made it 18446744073709551611, where the interpreter parses `-5` as +/// `u64` (fails), then as `f64`, then applies Rust's SATURATING `as u64` — 0. +#[test] +fn negative_numbers_saturate_to_zero_in_both() { + assert_backends_agree("neg", " cetakln(ke_teks(json_urai(\"-5\")));"); + assert_backends_agree("negfrac", " cetakln(ke_teks(json_urai(\"-0.5\")));"); + assert_backends_agree("frac", " cetakln(ke_teks(json_urai(\"3.9\")));"); + assert_backends_agree("exp", " cetakln(ke_teks(json_urai(\"1e3\")));"); +} + +/// Unicode whitespace around a document is accepted by `str::trim`, so the C +/// side may not use the ASCII four. The old `riina_json_skip_ws` did. +#[test] +fn unicode_whitespace_around_a_document_agrees() { + assert_backends_agree( + "ws_nbsp", + " cetakln(json_ke_teks(json_urai(\"\u{00A0}[1,2]\u{2007}\")));", + ); +} diff --git a/03_PROTO/crates/riinac/tests/keselamatan_differential.rs b/03_PROTO/crates/riinac/tests/keselamatan_differential.rs new file mode 100644 index 00000000..ac4748aa --- /dev/null +++ b/03_PROTO/crates/riinac/tests/keselamatan_differential.rs @@ -0,0 +1,670 @@ +// Copyright (c) 2026 The RIINA Authors. All rights reserved. + +//! Interpreter/C differential for the security (`keselamatan`) family — master +//! plan REQ-70 family routing. +//! +//! # What this family needed that the others did not +//! +//! Every previous family had its C helpers already written and merely +//! unrouted. This one had **none** — all 25 routed here are new C. So unlike +//! `json` or `masa`, routing could not *reveal* a pre-existing divergence; it +//! could only introduce one. That inverts the job: the differential is not +//! archaeology, it is the thing keeping a fresh transcription honest. +//! +//! # The taint source is routed with them, deliberately +//! +//! The sanitizers take `Tercemar`, and that type has exactly +//! ONE producer: `baca_baris`. Routing the sanitizers alone would have marked +//! them `native-only` in the Backend column while leaving them unreachable +//! from any compiled program — the REQ-79 "lowers to C but aborts on contact" +//! trap wearing a new costume. `baca_baris` is therefore routed too, and every +//! case below feeds input through it, which is also what makes the compiled +//! side genuinely exercised rather than constant-folded. +//! +//! # Cases chosen where a transcription would plausibly drift +//! +//! Not the happy path. The interpreter has two deliberate inconsistencies that +//! a C author would "fix" by accident, and both are pinned here: +//! +//! - `sanitize_url` iterates **bytes** while every other transform iterates +//! **codepoints**, so a non-ASCII input percent-encodes each UTF-8 byte +//! separately. Writing the C the obvious way (decode codepoints) gives a +//! different answer. +//! - `sanitize_css` emits a **trailing space** after each hex escape. It looks +//! like a bug; it is the CSS escape terminator, and dropping it changes the +//! output. +//! +//! Plus the cases where C and Rust genuinely differ in machinery: UTF-16 +//! surrogate pairs above the BMP (`sanitize_js`), and Unicode-aware trimming +//! (`sanitize_email` uses Rust's `str::trim`, which is *not* ASCII-only). + +use std::io::Write; +use std::path::PathBuf; +use std::process::{Command, Stdio}; + +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) — keselamatan 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_ks_{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 feed(cmd: &mut Command, stdin_text: &str) -> String { + let mut child = cmd + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .expect("spawn"); + child + .stdin + .as_mut() + .expect("stdin") + .write_all(format!("{stdin_text}\n").as_bytes()) + .expect("write stdin"); + let out = child.wait_with_output().expect("wait"); + assert!( + out.status.success(), + "process failed (exit {:?}): {}{}", + out.status.code(), + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + String::from_utf8_lossy(&out.stdout).into_owned() +} + +/// Feed `input` on stdin to a program that reads one tainted line, applies +/// `expr` to it, and prints the result. Assert both backends agree. +fn assert_agree(tag: &str, expr: &str, input: &str) { + assert_agree_eff(tag, expr, input, "(Sistem | Tulis)"); +} + +/// As `assert_agree`, with an explicit effect annotation. The HTTP sinks carry +/// `Rangkaian`, and RIINA's capability discipline rejects the program outright +/// without it — a useful reminder that the effect system gates these before +/// either backend runs. +fn assert_agree_eff(tag: &str, expr: &str, input: &str, eff: &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 {eff} {{\n\ + \x20 biar mentah = baca_baris(());\n\ + \x20 cetakln({expr});\n\ + \x20 0\n\ + }}\n" + ), + ) + .expect("write program"); + + let mut interp_cmd = Command::new(env!("CARGO_BIN_EXE_riinac")); + interp_cmd.arg("run").arg(&src); + let interp_raw = feed(&mut interp_cmd, input); + // `riinac run` appends the program's final value as a trailing line. + let mut lines: Vec<&str> = interp_raw.lines().collect(); + lines.pop(); + let interp = 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(), + "native build failed for {tag} — keselamatan must route, and so must its \ + taint source `baca_baris`: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + + let mut native_cmd = Command::new(sb.dir.join(&sb.stem)); + let native = feed(&mut native_cmd, input); + + assert_eq!( + interp, native, + "interp/C divergence for {tag}\n input: {input:?}\n interp: {interp:?}\n C: {native:?}" + ); +} + +// ── Sanitizers ───────────────────────────────────────────────────────────── + +#[test] +fn html_and_xml_escapes_agree() { + assert_agree("html", "sanitasi_html(mentah)", "&/"); + // XML differs from HTML on the apostrophe (' vs ') and does not + // escape '/', so the same input separates the two. + assert_agree("xml", "sanitasi_xml(mentah)", "&/"); +} + +#[test] +fn sql_escape_doubles_quotes_and_strips_nul() { + assert_agree("sql", "sanitasi_sql(mentah)", "O'Brien \\ end"); +} + +/// Above the BMP, Rust's `encode_utf16` yields a SURROGATE PAIR, so one +/// codepoint becomes two `\uXXXX` escapes. C has no UTF-16 in sight and must +/// compute the pair explicitly. +#[test] +fn js_escape_emits_surrogate_pairs_above_the_bmp() { + assert_agree("js_ascii", "sanitasi_js(mentah)", "a-b_c"); + assert_agree("js_latin", "sanitasi_js(mentah)", "café"); + assert_agree("js_astral", "sanitasi_js(mentah)", "x🔒y"); +} + +/// The trailing space after the hex escape is the CSS terminator, not a typo. +#[test] +fn css_escape_keeps_the_terminating_space() { + assert_agree("css", "sanitasi_css(mentah)", "a b;c{}"); +} + +/// `url_encode` iterates BYTES, so a multi-byte codepoint becomes several +/// percent escapes. Writing the C over codepoints would diverge here and only +/// here. +#[test] +fn url_encode_is_byte_wise_not_codepoint_wise() { + assert_agree("url_ascii", "sanitasi_url(mentah)", "a b/c~d-e._f"); + assert_agree("url_utf8", "sanitasi_url(mentah)", "café ☂"); +} + +#[test] +fn path_sanitize_drops_traversal_segments() { + assert_agree("path", "sanitasi_laluan(mentah)", "/a/../b//c/./d"); + assert_agree("path_win", "sanitasi_laluan(mentah)", "..\\..\\etc\\passwd"); +} + +#[test] +fn shell_quote_wraps_and_escapes_single_quotes() { + assert_agree("shell", "sanitasi_perintah(mentah)", "it's; rm -rf /"); +} + +#[test] +fn ldap_and_json_escapes_agree() { + assert_agree("ldap", "sanitasi_ldap(mentah)", "a*b(c)d\\e"); + assert_agree("json", "sanitasi_json(mentah)", "a\"b\\c"); +} + +/// `str::trim` is Unicode-aware, so a NBSP-padded address must trim in both +/// backends. An ASCII-only trim in C would leave the NBSP behind. +#[test] +fn email_sanitize_trims_unicode_whitespace() { + assert_agree("email", "sanitasi_emel(mentah)", " user@example.test "); + assert_agree("email_nbsp", "sanitasi_emel(mentah)", "\u{00A0}user@x.test\u{2007}"); +} + +// ── Validators / normalizers ─────────────────────────────────────────────── + +#[test] +fn url_validate_allows_only_the_safe_schemes() { + assert_agree("u_https", "sahkan_url(mentah)", " HTTPS://x.test/p "); + assert_agree("u_js", "sahkan_url(mentah)", "javascript:alert(1)"); + assert_agree("u_rel", "sahkan_url(mentah)", "/relative/ok"); + // Protocol-relative `//evil` must NOT be treated as a safe relative path. + assert_agree("u_proto_rel", "sahkan_url(mentah)", "//evil.test/x"); +} + +#[test] +fn normalize_unicode_strips_bidi_and_zero_width() { + // RLO is the classic filename-spoofing character; ZWSP hides token breaks. + assert_agree("norm", "normal_unicode(mentah)", "a\u{202E}b\u{200B}c\u{FEFF}d"); +} + +#[test] +fn strip_nulls_removes_nul_only() { + assert_agree("nul", "buang_null(mentah)", "a b c"); +} + +// ── Modelled sinks ───────────────────────────────────────────────────────── + +/// The sinks do not perform the dangerous operation in either backend. What is +/// pinned is that they agree on what they return, so a compiled program sees +/// the same values. +#[test] +fn modelled_sinks_agree() { + assert_agree("sink_sql", "sql_laksana(sanitasi_sql(mentah))", "O'Brien"); + assert_agree("sink_html", "html_papar(sanitasi_html(mentah))", "x"); + assert_agree( + "sink_shell", + "ke_teks(shell_laksana(sanitasi_perintah(mentah)))", + "ls -la", + ); + assert_agree_eff( + "sink_http", + "http_dapat(sahkan_url(mentah))", + "https://x.test", + "(Sistem | Tulis | Rangkaian)", + ); + // `badan_http` extracts the body of a modelled response, so it too is a + // Network operation as far as the effect system is concerned. + assert_agree_eff( + "sink_body", + "badan_http(sanitasi_html(mentah))", + "y", + "(Sistem | Tulis | Rangkaian)", + ); +} + +/// The taint source itself: both backends must read the same line and strip +/// the trailing newline identically. +#[test] +fn taint_source_reads_the_same_line() { + assert_agree("taint", "mentah", "plain line of input"); +} + +// ── Pair-taking members ──────────────────────────────────────────────────── + +/// Feed `input` on stdin to a program whose body is `body`, and assert both +/// backends agree. Unlike [`assert_agree_eff`] the caller writes the whole body, +/// which the pair-taking cases need because a single expression cannot show a +/// predicate answering differently on two inputs. +fn assert_body_agrees(tag: &str, body: &str, input: &str, eff: &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 {eff} {{\n{body}\n 0\n}}\n"), + ) + .expect("write program"); + + let mut interp_cmd = Command::new(env!("CARGO_BIN_EXE_riinac")); + interp_cmd.arg("run").arg(&src); + let interp_raw = feed(&mut interp_cmd, input); + let mut lines: Vec<&str> = interp_raw.lines().collect(); + lines.pop(); + let interp = 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(), + "native build failed for {tag}: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + + let mut native_cmd = Command::new(sb.dir.join(&sb.stem)); + let native = feed(&mut native_cmd, input); + + assert_eq!( + interp, native, + "interp/C divergence for {tag}\n interp: {interp:?}\n C: {native:?}" + ); +} + +/// The pair-taking members are reached through an EXPLICIT tuple, never a +/// curried call. That is not a convention this test relies on — the typechecker +/// enforces it: each signature is `Ty::Prod(..) -> _`, so `f(a, b)` is a type +/// error in both backends and the interpreter's `BuiltinPartial` path is +/// unreachable from well-typed source. +/// +/// This case exists because the previous increment deferred all eleven of them +/// on the belief that C would need partial-application machinery to match. It +/// does not, and the deferral was the wrong call. +#[test] +fn the_curried_form_is_a_type_error_not_a_divergence() { + if !require_cc() { + return; + } + let sb = Sandbox::new("curry"); + let src = sb.dir.join(format!("{}.rii", sb.stem)); + std::fs::write( + &src, + "fungsi utama() -> Nombor kesan Bersih {\n\ + \x20 biar x = csrf_sahkan(\"a\", \"a\");\n\ + \x20 0\n\ + }\n", + ) + .expect("write program"); + + for verb in ["run", "build"] { + let out = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg(verb) + .arg(&src) + .output() + .expect("riinac"); + let text = format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + assert!( + !out.status.success() && text.contains("Type mismatch"), + "`riinac {verb}` accepted the curried form; the pair-only \ + assumption the C implementations rest on does not hold: {text}" + ); + } +} + +/// CSRF predicates. The EMPTY allowed-origin arms are the load-bearing ones: a +/// C implementation that reached for `strcmp`/`strncmp` alone would accept every +/// origin (and every referer) when the program forgot to configure one. +#[test] +fn csrf_predicates_agree_including_the_empty_allowed_origin() { + assert_body_agrees( + "csrf", + " cetakln(ke_teks(csrf_sahkan((\"tok\", \"tok\"))));\n\ + \x20 cetakln(ke_teks(csrf_sahkan((\"tok\", \"tox\"))));\n\ + \x20 cetakln(ke_teks(csrf_sahkan((\"tok\", \"tokk\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_origin((\"https://a.test\", \"https://a.test\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_origin((\"https://b.test\", \"https://a.test\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_origin((\"https://a.test\", \"\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_origin((\"\", \"\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_referer((\"https://a.test/p\", \"https://a.test\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_referer((\"https://b.test/p\", \"https://a.test\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_referer((\"https://a\", \"https://a.test\"))));\n\ + \x20 cetakln(ke_teks(csrf_semak_referer((\"anything\", \"\"))));", + "unused", + "(Sistem | Tulis)", + ); +} + +/// `validate_length` counts UNICODE SCALAR VALUES, not bytes, so a multi-byte +/// input sits on the boundary differently in the two counting schemes. `café` is +/// 4 chars and 5 bytes: at a bound of 4 the interpreter admits it and a +/// byte-counting C would reject it. +#[test] +fn validate_length_counts_characters_not_bytes() { + assert_body_agrees( + "vlen", + " biar mentah = baca_baris(());\n\ + \x20 cetakln(ke_teks(sahkan_panjang((mentah, 4))));\n\ + \x20 cetakln(ke_teks(sahkan_panjang((mentah, 3))));", + "café", + "(Sistem | Tulis)", + ); + assert_body_agrees( + "vlen_astral", + " biar mentah = baca_baris(());\n\ + \x20 cetakln(ke_teks(sahkan_panjang((mentah, 3))));\n\ + \x20 cetakln(ke_teks(sahkan_panjang((mentah, 2))));", + "a🔒b", + "(Sistem | Tulis)", + ); +} + +/// The remaining modelled sinks: DOM mutation, email, and the state-changing +/// HTTP methods. All carry a CSRF token in their type, which is the point of +/// their shape; what is pinned here is only that both backends return the same +/// value for it. +#[test] +fn pair_taking_modelled_sinks_agree() { + assert_body_agrees( + "pairsinks", + " biar mentah = baca_baris(());\n\ + \x20 cetakln(ke_teks(dom_tetap_html((\"#el\", sanitasi_html(mentah)))));\n\ + \x20 cetakln(ke_teks(emel_hantar((sanitasi_emel(mentah), \"subjek\"))));\n\ + \x20 cetakln(ke_teks(emel_tetap_kepala((\"X-H\", sanitasi_emel(mentah)))));\n\ + \x20 cetakln(ke_teks(http_hantar((\"https://x.test\", (\"body\", \"tok\")))));\n\ + \x20 cetakln(ke_teks(http_kemaskini((\"https://x.test\", (\"body\", \"tok\")))));\n\ + \x20 cetakln(ke_teks(http_padam((\"https://x.test\", \"tok\"))));", + "user@example.test", + "(Sistem | Tulis | Rangkaian)", + ); +} + +// ── Safe file I/O ────────────────────────────────────────────────────────── + +/// The `*_selamat` file ops share the verified gate with `fail_*` — the +/// interpreter calls the same `fail::gate_read`/`gate_write`/`gate_delete`, so +/// the emitted C must reach the same `riina_gate`. A "safe" file op that skipped +/// the access check would be the REQ-72 bypass wearing the word `selamat`. +/// +/// The paths are relative because `sanitasi_laluan` — the only producer of a +/// `Disanitasi`, and so the only way to call these at all — +/// drops leading separators along with `..` segments. Each backend therefore +/// runs in its own working directory. +fn assert_safe_file_agrees(tag: &str, body: &str, filename: &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 (Sistem | SistemFail | Tulis) {{\n{body}\n 0\n}}\n" + ), + ) + .expect("write program"); + + let build = Command::new(env!("CARGO_BIN_EXE_riinac")) + .arg("build") + .arg(&src) + .output() + .expect("riinac build"); + assert!( + build.status.success(), + "native build failed for {tag}: {}{}", + String::from_utf8_lossy(&build.stdout), + String::from_utf8_lossy(&build.stderr) + ); + + // Separate working directories: a shared one would let one backend read the + // file the other wrote and make an agreement look real when it was leftover + // state. + let idir = sb.dir.join("wd_interp"); + let ndir = sb.dir.join("wd_native"); + std::fs::create_dir_all(&idir).expect("interp wd"); + std::fs::create_dir_all(&ndir).expect("native wd"); + + // `drop_value_line` is true ONLY for the interpreter: `riinac run` appends + // the program's final value as an extra line, and only when the program + // completes. A compiled binary never prints it, so applying the same trim to + // both would silently discard a real line of the native output. + let run = |dir: &PathBuf, cmd: &mut Command, drop_value_line: bool| -> String { + let mut child = cmd + .current_dir(dir) + .stdin(Stdio::piped()) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn() + .expect("spawn"); + child + .stdin + .as_mut() + .expect("stdin") + .write_all(format!("{filename}\n").as_bytes()) + .expect("write stdin"); + let out = child.wait_with_output().expect("wait"); + let s = String::from_utf8_lossy(&out.stdout).into_owned(); + let mut lines: Vec<&str> = s.lines().collect(); + // A denial is an expected outcome here, so a non-zero exit is not + // asserted against; what is compared is the output up to that point. + if drop_value_line && out.status.success() { + lines.pop(); + } + if lines.is_empty() { + String::new() + } else { + format!("{}\n", lines.join("\n")) + } + }; + + let mut interp_cmd = Command::new(env!("CARGO_BIN_EXE_riinac")); + interp_cmd.arg("run").arg(&src); + let interp = run(&idir, &mut interp_cmd, true); + let mut native_cmd = Command::new(sb.dir.join(&sb.stem)); + let native = run(&ndir, &mut native_cmd, false); + + assert_eq!( + interp, native, + "interp/C divergence for {tag}\n interp: {interp:?}\n C: {native:?}" + ); +} + +#[test] +fn safe_file_round_trip_agrees_for_the_owner() { + assert_safe_file_agrees( + "sf_owner", + " biar p = sanitasi_laluan(baca_baris(()));\n\ + \x20 biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis_selamat((p, \"safe-content\"));\n\ + \x20 cetakln(fail_baca_selamat(p));\n\ + \x20 cetakln(ke_teks(fail_buang_selamat(p)));", + "nota.txt", + ); +} + +/// THE reason these could not be routed before the gate existed: a non-owner +/// write must be refused by the compiled binary exactly as `riinac run` refuses +/// it. Both stop before printing `after`. +#[test] +fn safe_file_write_is_denied_to_a_non_owner_in_both() { + assert_safe_file_agrees( + "sf_other", + " biar p = sanitasi_laluan(baca_baris(()));\n\ + \x20 biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis_selamat((p, \"owned-by-7\"));\n\ + \x20 cetakln(fail_baca_selamat(p));\n\ + \x20 biar d = vfs_jadi_pengguna(9);\n\ + \x20 cetakln(\"before\");\n\ + \x20 biar e = fail_tulis_selamat((p, \"intruder\"));\n\ + \x20 cetakln(\"after\");", + "nota.txt", + ); +} + +/// A non-owner may READ a 0644 file, so the safe read resolves through the same +/// owner ▷ group ▷ other arms as `fail_baca` rather than a blanket owner check. +#[test] +fn safe_file_read_is_allowed_to_a_non_owner_in_both() { + assert_safe_file_agrees( + "sf_otherread", + " biar p = sanitasi_laluan(baca_baris(()));\n\ + \x20 biar a = vfs_mula(100000);\n\ + \x20 biar b = vfs_jadi_pengguna(7);\n\ + \x20 biar c = fail_tulis_selamat((p, \"owned-by-7\"));\n\ + \x20 biar d = vfs_jadi_pengguna(9);\n\ + \x20 cetakln(fail_baca_selamat(p));", + "nota.txt", + ); +} + +// ── Safe parsers ─────────────────────────────────────────────────────────── + +/// `json_parse_safe`'s contract is that malformed input yields Unit rather than +/// stopping the program — which is why it could not be routed until the emitted +/// JSON parser could FAIL at all. The old one never did: it fell through to +/// `strtoll` and invented a value, so "malformed" had no meaning on the C side +/// and every one of these would have printed a number instead of `null`. +#[test] +fn safe_parsers_yield_unit_on_malformed_input_in_both() { + for (tag, input) in [ + ("sp_word", "xyz"), + ("sp_trail", "12abc"), + ("sp_nul", "nul"), + ("sp_arr", "[1,2"), + ] { + assert_body_agrees( + tag, + " biar mentah = baca_baris(());\n\ + \x20 cetakln(json_ke_teks(json_urai_selamat(sanitasi_json(mentah))));\n\ + \x20 cetakln(json_ke_teks(nyahsiri_selamat(sanitasi_json(mentah))));", + input, + "(Sistem | Tulis)", + ); + } +} + +/// Well-formed input parses identically — and pins a STDLIB WART rather than a +/// codegen one, so that a future fix has to update this case deliberately. +/// +/// `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 therefore arrives malformed and parses to Unit, because object keys +/// are quoted. Only quote-free documents — numbers, booleans, `null`, arrays of +/// those — survive the round trip, which is what the array case below shows. +/// Both backends agree on this, 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 between them. +#[test] +fn safe_parsers_agree_on_what_survives_the_sanitizer() { + assert_body_agrees( + "sp_arr_ok", + " biar mentah = baca_baris(());\n\ + \x20 cetakln(json_ke_teks(json_urai_selamat(sanitasi_json(mentah))));", + "[1,2,3]", + "(Sistem | Tulis)", + ); + assert_body_agrees( + "sp_obj_lost", + " biar mentah = baca_baris(());\n\ + \x20 cetakln(json_ke_teks(json_urai_selamat(sanitasi_json(mentah))));", + "{\"a\":1}", + "(Sistem | Tulis)", + ); +} + +/// `xml_parse_safe` is identity on the document text in the interpreter — there +/// is no XML tree in-tree, and it deliberately does not resolve entities (no XXE +/// surface). Identity in C too; inventing a tree would be the overclaim. +#[test] +fn xml_parse_safe_is_identity_in_both() { + assert_body_agrees( + "xps", + " biar mentah = baca_baris(());\n\ + \x20 cetakln(xml_urai_selamat(sanitasi_xml(mentah)));", + "&", + "(Sistem | Tulis)", + ); +} diff --git a/RIINA_MASTER_PLAN.md b/RIINA_MASTER_PLAN.md index fb3787b0..f6a3c690 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. Still NOT routed: `keselamatan` (39 of 42 — ordinary work per the inspection above), the VirtualFs trio `vfs_tulis`/`vfs_baca`/`vfs_padam` (need an in-memory FS + quota in C), and the `jaring_tls_*` half above | P0 | IN PROGRESS (json + masa + simpan + net DONE; file/security + `jaring_tls_*` remain) | Gate C | +| REQ-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: **376 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-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,12 +4535,23 @@ 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-15: `json` (on main, PR #69), `masa`, `simpan` and `jaring`+`http` are DONE — 218 of -373 builtins compile, 155 interpreter-only.** Criterion 6 is now verified by command (the +2026-08-20: `json`, `masa`, `simpan`, `jaring`+`http`, `fail`+`vfs` and `keselamatan` are all +DONE — 323 of 376 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 reference service compiles, serves, and persists across restarts); pinning it as a test is -REQ-75. Remaining under 1.0: `fail`+`vfs`, `keselamatan`, and 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. (1.1) REQ-68 +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 +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 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 diff --git a/VERIFICATION_MANIFEST.md b/VERIFICATION_MANIFEST.md index 0a983f0d..7172ebfe 100644 --- a/VERIFICATION_MANIFEST.md +++ b/VERIFICATION_MANIFEST.md @@ -1,6 +1,6 @@ # RIINA Verification Manifest -**Generated:** 2026-08-18T22:01:33Z -**Git SHA:** 512c6baf4 +**Generated:** 2026-08-20T01:51:06Z +**Git SHA:** 623391e91 **Mode:** full **Status:** PASS @@ -8,10 +8,10 @@ | Check | Status | Details | |-------|--------|---------| -| Rust Tests | PASS | 3330 tests | +| Rust Tests | PASS | 3360 tests | | Clippy | PASS | 0 warnings | | _CoqProject Completeness | PASS | all 331 .v files listed in _CoqProject | -| Coq Compilation | PASS | 331 .vo files compiled in 159s | +| Coq Compilation | PASS | 331 .vo files compiled in 179s | | 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) | @@ -24,7 +24,7 @@ | 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+ Scan | PASS | 317 files (12282 theorems) | -| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 6s (6 checked assertions, local_active) | +| Alloy Compilation | PASS | Active model TelusProcurementAccessControl executed in 7s (6 checked assertions, local_active) | | Alloy Scan | PASS | 306 files (11627 assertions) | | SMT Scan | PASS | 318 files (12431 assertions) | | Verus admit Scan | PASS | 0 admit in 323 files (6395 proof fns) | diff --git a/docs/api/STDLIB.md b/docs/api/STDLIB.md index e23f23d0..1d241d7b 100644 --- a/docs/api/STDLIB.md +++ b/docs/api/STDLIB.md @@ -6,13 +6,13 @@ Total registered builtins: **373**. Grouped by the effect each performs (`kesan` ## ⚠ Read first: type-checking does not imply compiling -Every builtin below type-checks and runs under `riinac run` (the interpreter). Only **238** of the 373 also compile, and they do NOT all reach the same backends: +Every builtin below type-checks and runs under `riinac run` (the interpreter). Only **323** of the 373 also compile, and they do NOT all reach the same backends: | Backend value | Meaning | |---|---| | `compiled` | Lowers to C **and** WASM (20 builtins). | -| `native-only` | Lowers to C. The WASM backend **refuses** it (218 builtins). | -| `interp-only` | `riinac run` only (135 builtins). `riinac build` fails with `unbound variable`. | +| `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`. | ``` $ riinac check baca.rii # Success! Effect: FileSystem @@ -30,7 +30,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Bersih (Pure) -> **Mixed:** 166 of 229 compile; the rest are interpreter-only (REQ-70). +> **Mixed:** 214 of 229 compile; the rest are interpreter-only (REQ-70). | Builtin | Type | Backend | |---|---|---| @@ -49,23 +49,23 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `binary_fixed` | `Fn((Teks, Nombor), Qmn)` | compiled | | `bool_ke_nombor` | `Fn(Benar, Nombor)` | **native-only** | | `bool_to_int` | `Fn(Benar, Nombor)` | **native-only** | -| `buang_null` | `Fn(Tercemar, Tercemar)` | **interp-only** | +| `buang_null` | `Fn(Tercemar, Tercemar)` | **native-only** | | `concat` | `Fn((Teks, Teks), Teks)` | compiled | -| `csrf_check_origin` | `Fn((Teks, Teks), Benar)` | **interp-only** | -| `csrf_check_referer` | `Fn((Teks, Teks), Benar)` | **interp-only** | -| `csrf_sahkan` | `Fn((Teks, Teks), Benar)` | **interp-only** | -| `csrf_semak_origin` | `Fn((Teks, Teks), Benar)` | **interp-only** | -| `csrf_semak_referer` | `Fn((Teks, Teks), Benar)` | **interp-only** | -| `csrf_validate` | `Fn((Teks, Teks), Benar)` | **interp-only** | +| `csrf_check_origin` | `Fn((Teks, Teks), Benar)` | **native-only** | +| `csrf_check_referer` | `Fn((Teks, Teks), Benar)` | **native-only** | +| `csrf_sahkan` | `Fn((Teks, Teks), Benar)` | **native-only** | +| `csrf_semak_origin` | `Fn((Teks, Teks), Benar)` | **native-only** | +| `csrf_semak_referer` | `Fn((Teks, Teks), Benar)` | **native-only** | +| `csrf_validate` | `Fn((Teks, Teks), Benar)` | **native-only** | | `decimal` | `Fn(Teks, Perpuluhan)` | compiled | -| `deserialize_safe` | `Fn(Disanitasi, Any)` | **interp-only** | -| `email_set_header` | `Fn((Teks, Disanitasi), ())` | **interp-only** | -| `emel_tetap_kepala` | `Fn((Teks, Disanitasi), ())` | **interp-only** | +| `deserialize_safe` | `Fn(Disanitasi, Any)` | **native-only** | +| `email_set_header` | `Fn((Teks, Disanitasi), ())` | **native-only** | +| `emel_tetap_kepala` | `Fn((Teks, Disanitasi), ())` | **native-only** | | `fixed` | `Fn((Teks, Nombor), Wang)` | compiled | | `gabung_teks` | `Fn((Teks, Teks), Teks)` | compiled | | `gcd` | `Fn((Nombor, Nombor), Nombor)` | **native-only** | -| `html_papar` | `Fn(Disanitasi, Teks)` | **interp-only** | -| `html_render` | `Fn(Disanitasi, Teks)` | **interp-only** | +| `html_papar` | `Fn(Disanitasi, Teks)` | **native-only** | +| `html_render` | `Fn(Disanitasi, Teks)` | **native-only** | | `http_balas` | `Fn((Nombor, Teks), Teks)` | **native-only** | | `http_build_response` | `Fn((Nombor, Teks), Teks)` | **native-only** | | `http_hurai_jasad` | `Fn(Teks, Teks)` | **native-only** | @@ -85,11 +85,11 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `json_ke_teks` | `Fn(Any, Any)` | **native-only** | | `json_letak` | `Fn(Any, Any)` | **native-only** | | `json_parse` | `Fn(Any, Any)` | **native-only** | -| `json_parse_safe` | `Fn(Disanitasi, Any)` | **interp-only** | +| `json_parse_safe` | `Fn(Disanitasi, Any)` | **native-only** | | `json_set` | `Fn(Any, Any)` | **native-only** | | `json_stringify` | `Fn(Any, Any)` | **native-only** | | `json_urai` | `Fn(Any, Any)` | **native-only** | -| `json_urai_selamat` | `Fn(Disanitasi, Any)` | **interp-only** | +| `json_urai_selamat` | `Fn(Disanitasi, Any)` | **native-only** | | `julat` | `Fn((Nombor, Nombor), Senarai)` | **interp-only** | | `julat_inklusif` | `Fn((Nombor, Nombor), Senarai)` | **interp-only** | | `ke_bool` | `Fn(Any, Benar)` | **native-only** | @@ -136,9 +136,9 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `nilai_kanan` | `Fn(Any, Any)` | **interp-only** | | `nilai_kiri` | `Fn(Any, Any)` | **interp-only** | | `nombor_ke_teks` | `Fn(Nombor, Teks)` | compiled | -| `normal_unicode` | `Fn(Tercemar, Tercemar)` | **interp-only** | -| `normalize_unicode` | `Fn(Tercemar, Tercemar)` | **interp-only** | -| `nyahsiri_selamat` | `Fn(Disanitasi, Any)` | **interp-only** | +| `normal_unicode` | `Fn(Tercemar, Tercemar)` | **native-only** | +| `normalize_unicode` | `Fn(Tercemar, Tercemar)` | **native-only** | +| `nyahsiri_selamat` | `Fn(Disanitasi, Any)` | **native-only** | | `panjang` | `Fn(Teks, Nombor)` | **native-only** | | `parse_int` | `Fn(Teks, Nombor)` | **native-only** | | `perpuluhan` | `Fn(Teks, Perpuluhan)` | compiled | @@ -155,30 +155,30 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `qmn` | `Fn((Teks, Nombor), Qmn)` | compiled | | `rangka` | `Fn(Teks, Teks)` | **interp-only** | | `rem` | `Fn(Nombor, Nombor)` | **interp-only** | -| `sahkan_panjang` | `Fn((Tercemar, Nombor), Mungkin>)` | **interp-only** | -| `sahkan_url` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_css` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_emel` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_html` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_js` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_json` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_laluan` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_ldap` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_perintah` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_sql` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_url` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitasi_xml` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_command` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_css` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_email` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_html` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_js` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_json` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_ldap` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_path` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_sql` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_url` | `Fn(Tercemar, Disanitasi)` | **interp-only** | -| `sanitize_xml` | `Fn(Tercemar, Disanitasi)` | **interp-only** | +| `sahkan_panjang` | `Fn((Tercemar, Nombor), Mungkin>)` | **native-only** | +| `sahkan_url` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_css` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_emel` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_html` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_js` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_json` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_laluan` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_ldap` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_perintah` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_sql` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_url` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitasi_xml` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_command` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_css` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_email` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_html` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_js` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_json` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_ldap` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_path` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_sql` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_url` | `Fn(Tercemar, Disanitasi)` | **native-only** | +| `sanitize_xml` | `Fn(Tercemar, Disanitasi)` | **native-only** | | `senarai_balik` | `Fn(Any, Any)` | **native-only** | | `senarai_baru` | `Fn(Any, Any)` | **native-only** | | `senarai_dapat` | `Fn(Any, Any)` | **native-only** | @@ -229,7 +229,7 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `str_to_lower` | `Fn(Any, Any)` | **native-only** | | `str_to_upper` | `Fn(Any, Any)` | **native-only** | | `str_trim` | `Fn(Any, Any)` | **native-only** | -| `strip_nulls` | `Fn(Tercemar, Tercemar)` | **interp-only** | +| `strip_nulls` | `Fn(Tercemar, Tercemar)` | **native-only** | | `tegaskan` | `Fn(Benar, ())` | **native-only** | | `tegaskan_betul` | `Fn(Benar, ())` | **native-only** | | `tegaskan_beza` | `Fn((Any, Any), ())` | **native-only** | @@ -256,38 +256,38 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t | `tls_policy_ok` | `Fn((Teks, Teks), Benar)` | **native-only** | | `to_bool` | `Fn(Any, Benar)` | **native-only** | | `to_string` | `Fn(Any, Teks)` | compiled | -| `validate_length` | `Fn((Tercemar, Nombor), Mungkin>)` | **interp-only** | -| `validate_url` | `Fn(Tercemar, Disanitasi)` | **interp-only** | +| `validate_length` | `Fn((Tercemar, Nombor), Mungkin>)` | **native-only** | +| `validate_url` | `Fn(Tercemar, Disanitasi)` | **native-only** | | `wang` | `Fn(Teks, Wang)` | compiled | -| `xml_cari` | `Fn(Disanitasi, Any)` | **interp-only** | -| `xml_parse_safe` | `Fn(Disanitasi, Any)` | **interp-only** | -| `xml_query` | `Fn(Disanitasi, Any)` | **interp-only** | -| `xml_urai_selamat` | `Fn(Disanitasi, Any)` | **interp-only** | +| `xml_cari` | `Fn(Disanitasi, Any)` | **native-only** | +| `xml_parse_safe` | `Fn(Disanitasi, Any)` | **native-only** | +| `xml_query` | `Fn(Disanitasi, Any)` | **native-only** | +| `xml_urai_selamat` | `Fn(Disanitasi, Any)` | **native-only** | ## Baca (Read) -> **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 | |---|---|---| -| `fail_baca_selamat` | `Fn(Disanitasi, Any, Baca)` | **interp-only** | -| `file_read_safe` | `Fn(Disanitasi, Any, Baca)` | **interp-only** | +| `fail_baca_selamat` | `Fn(Disanitasi, Any, Baca)` | **native-only** | +| `file_read_safe` | `Fn(Disanitasi, Any, Baca)` | **native-only** | | `vfs_baca` | `Fn(Teks, Teks, Baca)` | **interp-only** | | `vfs_read` | `Fn(Teks, Teks, Baca)` | **interp-only** | ## Tulis (Write) -> **Mixed:** 4 of 13 compile; the rest are interpreter-only (REQ-70). +> **Mixed:** 8 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** | | `cetakln` | `Fn(Any, (), Tulis)` | compiled | -| `fail_buang_selamat` | `Fn(Disanitasi, Benar, Tulis)` | **interp-only** | -| `fail_tulis_selamat` | `Fn((Disanitasi, Any), (), Tulis)` | **interp-only** | -| `file_delete_safe` | `Fn(Disanitasi, Benar, Tulis)` | **interp-only** | -| `file_write_safe` | `Fn((Disanitasi, Any), (), Tulis)` | **interp-only** | +| `fail_buang_selamat` | `Fn(Disanitasi, Benar, Tulis)` | **native-only** | +| `fail_tulis_selamat` | `Fn((Disanitasi, Any), (), Tulis)` | **native-only** | +| `file_delete_safe` | `Fn(Disanitasi, Benar, Tulis)` | **native-only** | +| `file_write_safe` | `Fn((Disanitasi, Any), (), Tulis)` | **native-only** | | `print` | `Fn(Any, (), Tulis)` | compiled | | `println` | `Fn(Any, (), Tulis)` | compiled | | `vfs_delete` | `Fn(Teks, Benar, Tulis)` | **interp-only** | @@ -338,27 +338,25 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Rangkaian (Network) -> **Mixed:** 18 of 34 compile; the rest are interpreter-only (REQ-70). - | Builtin | Type | Backend | |---|---|---| -| `badan_http` | `Fn(Any, Tercemar, Rangkaian)` | **interp-only** | -| `email_send` | `Fn((Disanitasi, Teks), Benar, Rangkaian)` | **interp-only** | -| `emel_hantar` | `Fn((Disanitasi, Teks), Benar, Rangkaian)` | **interp-only** | -| `http_ambil_selamat` | `Fn(Disanitasi, Any, Rangkaian)` | **interp-only** | -| `http_arah_selamat` | `Fn(Disanitasi, (), Rangkaian)` | **interp-only** | -| `http_body` | `Fn(Any, Tercemar, Rangkaian)` | **interp-only** | -| `http_dapat` | `Fn(Teks, Any, Rangkaian)` | **interp-only** | -| `http_delete` | `Fn((Teks, Teks), Any, Rangkaian)` | **interp-only** | -| `http_fetch_safe` | `Fn(Disanitasi, Any, Rangkaian)` | **interp-only** | -| `http_get` | `Fn(Teks, Any, Rangkaian)` | **interp-only** | -| `http_hantar` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **interp-only** | -| `http_kemaskini` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **interp-only** | +| `badan_http` | `Fn(Any, Tercemar, Rangkaian)` | **native-only** | +| `email_send` | `Fn((Disanitasi, Teks), Benar, Rangkaian)` | **native-only** | +| `emel_hantar` | `Fn((Disanitasi, Teks), Benar, Rangkaian)` | **native-only** | +| `http_ambil_selamat` | `Fn(Disanitasi, Any, Rangkaian)` | **native-only** | +| `http_arah_selamat` | `Fn(Disanitasi, (), Rangkaian)` | **native-only** | +| `http_body` | `Fn(Any, Tercemar, Rangkaian)` | **native-only** | +| `http_dapat` | `Fn(Teks, Any, Rangkaian)` | **native-only** | +| `http_delete` | `Fn((Teks, Teks), Any, Rangkaian)` | **native-only** | +| `http_fetch_safe` | `Fn(Disanitasi, Any, Rangkaian)` | **native-only** | +| `http_get` | `Fn(Teks, Any, Rangkaian)` | **native-only** | +| `http_hantar` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **native-only** | +| `http_kemaskini` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **native-only** | | `http_minta` | `Fn((Teks, Teks), Teks, Rangkaian)` | **native-only** | -| `http_padam` | `Fn((Teks, Teks), Any, Rangkaian)` | **interp-only** | -| `http_post` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **interp-only** | -| `http_put` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **interp-only** | -| `http_redirect_safe` | `Fn(Disanitasi, (), Rangkaian)` | **interp-only** | +| `http_padam` | `Fn((Teks, Teks), Any, Rangkaian)` | **native-only** | +| `http_post` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **native-only** | +| `http_put` | `Fn((Teks, (Any, Teks)), Any, Rangkaian)` | **native-only** | +| `http_redirect_safe` | `Fn(Disanitasi, (), Rangkaian)` | **native-only** | | `http_request` | `Fn((Teks, Teks), Teks, Rangkaian)` | **native-only** | | `jaring_alamat` | `Fn(Nombor, Teks, Rangkaian)` | **native-only** | | `jaring_dengar` | `Fn(Teks, Nombor, Rangkaian)` | **native-only** | @@ -428,25 +426,23 @@ In practice: the WASM surface is printing, string concatenation, `ke_teks` and t ## Sistem (System) -> **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 | |---|---|---| -| `baca_baris` | `Fn((), Tercemar, Sistem)` | **interp-only** | -| `baca_garisan` | `Fn((), Teks, Sistem)` | **interp-only** | -| `dom_set_attr` | `Fn((Any, (Teks, Disanitasi)), (), Sistem)` | **interp-only** | -| `dom_set_html` | `Fn((Any, Disanitasi), (), Sistem)` | **interp-only** | -| `dom_tetap_atribut` | `Fn((Any, (Teks, Disanitasi)), (), Sistem)` | **interp-only** | -| `dom_tetap_html` | `Fn((Any, Disanitasi), (), Sistem)` | **interp-only** | -| `js_eval` | `Fn(Disanitasi, Any, Sistem)` | **interp-only** | -| `js_nilai` | `Fn(Disanitasi, Any, Sistem)` | **interp-only** | -| `ldap_cari` | `Fn(Disanitasi, Any, Sistem)` | **interp-only** | -| `ldap_search` | `Fn(Disanitasi, Any, Sistem)` | **interp-only** | -| `read_line` | `Fn((), Tercemar, Sistem)` | **interp-only** | -| `shell_exec` | `Fn(Disanitasi, Nombor, Sistem)` | **interp-only** | -| `shell_laksana` | `Fn(Disanitasi, Nombor, Sistem)` | **interp-only** | -| `sql_execute` | `Fn(Disanitasi, Any, Sistem)` | **interp-only** | -| `sql_laksana` | `Fn(Disanitasi, Any, Sistem)` | **interp-only** | +| `baca_baris` | `Fn((), Tercemar, Sistem)` | **native-only** | +| `baca_garisan` | `Fn((), Teks, Sistem)` | **native-only** | +| `dom_set_attr` | `Fn((Any, (Teks, Disanitasi)), (), Sistem)` | **native-only** | +| `dom_set_html` | `Fn((Any, Disanitasi), (), Sistem)` | **native-only** | +| `dom_tetap_atribut` | `Fn((Any, (Teks, Disanitasi)), (), Sistem)` | **native-only** | +| `dom_tetap_html` | `Fn((Any, Disanitasi), (), Sistem)` | **native-only** | +| `js_eval` | `Fn(Disanitasi, Any, Sistem)` | **native-only** | +| `js_nilai` | `Fn(Disanitasi, Any, Sistem)` | **native-only** | +| `ldap_cari` | `Fn(Disanitasi, Any, Sistem)` | **native-only** | +| `ldap_search` | `Fn(Disanitasi, Any, Sistem)` | **native-only** | +| `read_line` | `Fn((), Tercemar, Sistem)` | **native-only** | +| `shell_exec` | `Fn(Disanitasi, Nombor, Sistem)` | **native-only** | +| `shell_laksana` | `Fn(Disanitasi, Nombor, Sistem)` | **native-only** | +| `sql_execute` | `Fn(Disanitasi, Any, Sistem)` | **native-only** | +| `sql_laksana` | `Fn(Disanitasi, Any, Sistem)` | **native-only** | ## Masa (Time) diff --git a/website/public/metrics.json b/website/public/metrics.json index a00cbdbb..90ae24fe 100644 --- a/website/public/metrics.json +++ b/website/public/metrics.json @@ -1,11 +1,11 @@ { - "generated": "2026-08-20T00:37:44Z", - "generatedHuman": "August 20, 2026 at 00:37 UTC", + "generated": "2026-08-20T01:33:24Z", + "generatedHuman": "August 20, 2026 at 01:33 UTC", "version": "0.4.0", "session": 0, "git": { - "commit": "fd32601ec", - "branch": "main" + "commit": "38479de48", + "branch": "claude/continue-solution-4gn31y" }, "proofs": { "qedActive": 12678, @@ -196,8 +196,8 @@ "rust": { "tests": 3330, "testsVerified": 3330, - "testsEstimated": 0, - "testsSource": "full_cargo_test", + "testsEstimated": 3356, + "testsSource": "cached_verified", "crates": 20 }, "examples": 169,