[TRACK_B] Close the keselamatan family (41/42), and fix two divergences it exposed

[ib823]

REQ-70. Routes the remaining 17 security builtins, taking the family from 24/42 to 41/42. Getting there required fixing two divergences in families the plan had already marked closed — both invisible to the differentials those families shipped with, and both prerequisites rather than side quests.

The deferral was wrong, and checking it is what unblocked this

The previous increment routed only the single-argument subset, 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 does not hold. 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 pins that, because it is the assumption eleven C implementations rest on.

Prerequisite 1 — the C JSON parser could not fail

riina_json_parse_value had no error path at all: unknown input fell through to strtoll and became a value. Five classes, each silent:

input	riinac run	compiled binary
xyz	unexpected char 'x'	0
(empty)	unexpected end of input	0
12abc	unexpected trailing content	12
nul	expected 'null'	()
[1,2	expected ',' or ']' in array	[1,2]

A compiled program parsing attacker-controlled JSON saw a fabricated value where the interpreter refuses. json_differential missed it because all nine of its cases fed well-formed input, so a parser that cannot fail was never asked to. And json_parse_safe/nyahsiri_selamat could not be routed at all: their whole contract is "malformed input yields Unit", and "malformed" had no meaning on the C side.

The parser now mirrors builtins/json.rs production-for-production, including the parts that are not obviously deliberate: whitespace is Unicode (str::trim), not the ASCII four; a lone surrogate in a \uXXXX escape decodes to nothing (char::from_u32 is None and the interpreter pushes no character); and a number is read as u64 first, then as f64 with Rust's saturating as u64 cast — so -5 is 0, where strtoll plus a C cast gave 18446744073709551611.

Prerequisite 2 — composite values rendered as the literal text <value>

riina_format handled the scalar tags and defaulted every composite one — PAIR, LIST, MAP and both SUM arms — to "<value>". cetakln and ke_teks both go through it, so a compiled program printing a list showed <value> where riinac run shows [1, 2, 3].

That also made sahkan_panjang unroutable in practice: it returns an Option, so its answer was unobservable in compiled code — the REQ-79 "compiles but you cannot see the result" trap in a new costume. ke_teks additionally carried its own copy of the scalar arms, which is how the two came to disagree; it now delegates, so there is one switch rather than two.

The interpreter has two rendering modes that spell values differently: builtins::format_value prints a string bare and a bool as betul/salah, while 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 is betul in a list and true in a sum. That is an inconsistency in the reference, not a design, but the reference is what a compiled program must match; both modes are mirrored rather than tidied, and pinned so that changing it is a language decision and not codegen drift.

Routed

Seven pair-taking modelled sinks (dom_set_html/attr, email_send/set_header, http_post/put/delete), validate_length, the three CSRF predicates, the safe-file trio, and the three safe parsers.

The safe-file trio share the verified gate with fail_* — the interpreter calls the same fail::gate_read/gate_write/gate_delete — so the emitted C reaches the same riina_gate. A "safe" file op that skipped the access check would be the REQ-72 bypass wearing the word selamat. They were routable only because the gate landed in #73.

Not routed, deliberately

csrf_generate/csrf_jana, the single remaining member. 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 already marks as "a reference token, not a certified CSPRNG" — spreading that to a second implementation makes the eventual fix twice the work. Nothing is cut off: csrf_validate takes plain Teks, so a compiled program can carry tokens minted elsewhere, unlike the sanitizers which would have been unreachable without baca_baris.

Recorded, not fixed — a stdlib defect the differential surfaced

sanitasi_json is the only producer of Disanitasi<Teks, JsonValidation> 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 survive. 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 — and not a divergence. Pinned in both directions so a fix has to update the test deliberately.

Tests

keselamatan_differential 14 → 24, json_differential 9 → 13, collection_differential 7 → 9.

The keselamatan additions cover the empty allowed-origin arms (a C author reaching for strncmp alone would accept every origin), character-vs-byte length counting, gate parity for the safe-file trio including a denied non-owner write, and the safe parsers on each malformed class.

Verification

• 03_PROTO: 3360 passing, 0 failed (+30)
• 05_TOOLING: 323 passing, 0 failed
• cargo clippy -- -D warnings: clean on both workspaces
• scripts/audit-docs.sh: 0 discrepancies (2 pre-existing warnings, unrelated: Lean sorry syntactic-only, Coq warning-budget freshness)
• scripts/update-proof-ledger.sh --check: up to date
• docs/api/STDLIB.md regenerated from the compiler — counts re-derived, not carried forward: 376 registered, 323 compile (compiled 20 / native-only 303 / interp-only 50)

🤖 Generated with Claude Code

https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth

---

Generated by Claude Code