nx_catn_kat_gate.nx source
↩ module page · 79 lines · 3852 B
1// nx_catn_kat_gate.nx -- THE NUMBER FORMATTER RENDERS NEGATIVES. PROVEN, NOT EDITED-AND-ASSUMED.
2//
3// ta_catn had `while m > 0` with no negative branch, so a negative emitted ZERO CHARACTERS and the
4// MCP transport produced malformed JSON: `"exit_code":,"bytes":0`. A timed-out exec returns a
5// negative rc, so the one value it could not print was the one that appears only when something has
6// already gone wrong -- and the caller could not tell "timed out" from "dead tool".
7//
8// This KAT calls the REAL ta_catn from nx_tools_api.nx (a lib, no main, so it is importable) and
9// pins its output. It proves the SOURCE is correct independently of whether the daemon carrying it
10// has been deployed -- two different claims that were being conflated.
11//
12// ★ THE DECISIVE TOOTH IS THE LENGTH ONE: the defect produced exactly ZERO bytes, so asserting that
13// -1 renders as TWO characters is the direct regression assertion. A tooth that only checked the
14// digits would pass on an empty buffer left over from a previous test.
15// license_tier: ORIGINAL expect_exit: 0
16import "syscalls.nx"
17import "nx_tools_api.nx"
18import "nx_gate_verdict.nx"
19
20func kat_eq(b: *u8, n: i64, want: *u8) -> i64 {
21 var m: i64 = 0
22 while want[m] != (0 as u8) { m = m + 1 }
23 if m != n { return 0 }
24 var i: i64 = 0
25 while i < n { if b[i] != want[i] { return 0 } i = i + 1 }
26 return 1
27}
28
29func main() -> i64 {
30 let ctr: *i64 = gv_ctr()
31 gv_head("=== NX-CATN-KAT -- ta_catn renders negatives (the malformed-JSON root cause) ===" as *u8)
32
33 let b: *u8 = sys_mmap(256)
34
35 // POSITIVE PATH UNCHANGED (rule 19): every existing caller must be byte-identical.
36 var i: i64 = 0
37 while i < 256 { b[i] = 0 as u8; i = i + 1 }
38 let n0: i64 = ta_catn(b, 0, 0)
39 gv_check("zero-renders-0" as *u8, ((n0 == 1) & (kat_eq(b, n0, "0" as *u8) == 1)) as i64, ctr)
40
41 i = 0
42 while i < 256 { b[i] = 0 as u8; i = i + 1 }
43 let n1: i64 = ta_catn(b, 0, 42)
44 gv_check("positive-renders-42" as *u8, ((n1 == 2) & (kat_eq(b, n1, "42" as *u8) == 1)) as i64, ctr)
45
46 i = 0
47 while i < 256 { b[i] = 0 as u8; i = i + 1 }
48 let n2: i64 = ta_catn(b, 0, 358726)
49 gv_check("large-positive-renders" as *u8, ((n2 == 6) & (kat_eq(b, n2, "358726" as *u8) == 1)) as i64, ctr)
50
51 // THE REGRESSION. Before the fix this returned the SAME offset it was given -- zero bytes written.
52 i = 0
53 while i < 256 { b[i] = 0 as u8; i = i + 1 }
54 let n3: i64 = ta_catn(b, 0, 0 - 1)
55 gv_check("neg-control-minus-one-writes-TWO-bytes-not-zero" as *u8, (n3 == 2) as i64, ctr)
56 gv_check("minus-one-renders--1" as *u8, (kat_eq(b, n3, "-1" as *u8) == 1) as i64, ctr)
57
58 i = 0
59 while i < 256 { b[i] = 0 as u8; i = i + 1 }
60 let n4: i64 = ta_catn(b, 0, 0 - 12345)
61 gv_check("multi-digit-negative-renders" as *u8, ((n4 == 6) & (kat_eq(b, n4, "-12345" as *u8) == 1)) as i64, ctr)
62
63 // OFFSET DISCIPLINE: the return value must be the END offset, so a caller appending after a
64 // negative does not overwrite the sign. A formatter that returns the wrong end corrupts the
65 // NEXT field rather than its own, which is far harder to attribute.
66 i = 0
67 while i < 256 { b[i] = 0 as u8; i = i + 1 }
68 let e1: i64 = ta_catn(b, 3, 0 - 7)
69 gv_check("respects-start-offset-and-returns-end" as *u8, ((e1 == 5) & (b[3] == (45 as u8)) & (b[4] == (55 as u8))) as i64, ctr)
70
71 gv_puts("\n --- measured ---\n" as *u8)
72 gv_puts(" len(0)=" as *u8); gv_num(n0)
73 gv_puts(" len(42)=" as *u8); gv_num(n1)
74 gv_puts(" len(-1)=" as *u8); gv_num(n3)
75 gv_puts(" len(-12345)=" as *u8); gv_num(n4)
76 gv_puts(" (len(-1) was 0 before the fix)\n" as *u8)
77
78 return gv_verdict("nx_catn_kat_gate" as *u8, ctr,
79 "calls the real ta_catn from nx_tools_api.nx; proves the SOURCE regardless of daemon deployment state" as *u8)
80}