code wiki / _hdl_build / nx_sketch_types_kat.nx
nx_sketch_types_kat.nx source
↩ module page · 45 lines · 3063 B
1// nx_sketch_types_kat.nx -- KAT for nx_sketch_types (ApproxI64 typed-envelope scaffold; 53 children).
2// HONESTY [W] weak point (reach=85). Constructor field roundtrip + sealed-enum distinctness.
3// license_tier: ORIGINAL expect_exit:0
4import "nx_syscalls.nx"
5import "nx_sketch_types.nx"
6
7func w(s: *u8) -> i64 { var k:i64=0; while s[k]!=(0 as u8){k=k+1} sys_write(1,s,k); return 0 }
8func n(v: i64) -> i64 { let b:*u8=sys_mmap(24); var m:i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} let t:*u8=sys_mmap(24); var k:i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} var j:i64=0; while j<k{b[j]=t[k-1-j];j=j+1} sys_write(1,b,k); return 0 }
9
10func main() -> i64 {
11 var pass: i64 = 0
12
13 // T1: constructor field roundtrip -- all 6 fields readback exactly
14 let a: *ApproxI64 = nx_approx_new(123456, NX_ENV_REL_STDDEV, 50000000, 682700000, NX_MATURITY_PRODUCTION, NX_ADV_ADVERSARIAL)
15 var ok1: i64 = 1
16 if a.value != 123456 { ok1 = 0 }
17 if a.envelope_kind != NX_ENV_REL_STDDEV { ok1 = 0 }
18 if a.param_a != 50000000 { ok1 = 0 }
19 if a.conf_ppb != 682700000 { ok1 = 0 }
20 if a.maturity != NX_MATURITY_PRODUCTION { ok1 = 0 }
21 if a.adv_safety != NX_ADV_ADVERSARIAL { ok1 = 0 }
22 if ok1 == 1 { pass = pass + 1; w("T1 field-roundtrip PASS\n" as *u8) } else { w("T1 FAIL\n" as *u8) }
23
24 // T2: a second, distinct instance doesn't alias the first
25 let b: *ApproxI64 = nx_approx_new(999, NX_ENV_ABS, 1, 500000000, NX_MATURITY_THEORETICAL, NX_ADV_HONEST)
26 if b.value == 999 { if a.value == 123456 { pass = pass + 1; w("T2 no-alias PASS\n" as *u8) } else { w("T2 FAIL a clobbered\n" as *u8) } } else { w("T2 FAIL b\n" as *u8) }
27
28 // T3: envelope-kind sealed enum distinct + ordered
29 if NX_ENV_REL_STDDEV == 0 { if NX_ENV_RANK_ERROR == 1 { if NX_ENV_ABS == 2 { pass = pass + 1; w("T3 env-enum PASS\n" as *u8) } else { w("T3 FAIL abs\n" as *u8) } } else { w("T3 FAIL rank\n" as *u8) } } else { w("T3 FAIL rel\n" as *u8) }
30
31 // T4: maturity ladder distinct + ordered
32 if NX_MATURITY_THEORETICAL == 0 { if NX_MATURITY_REFERENCE_IMPL == 1 { if NX_MATURITY_PRODUCTION == 2 { pass = pass + 1; w("T4 maturity-ladder PASS\n" as *u8) } else { w("T4 FAIL prod\n" as *u8) } } else { w("T4 FAIL ref\n" as *u8) } } else { w("T4 FAIL theo\n" as *u8) }
33
34 // T5: adversarial-safety enum distinct
35 if NX_ADV_HONEST != NX_ADV_ADVERSARIAL { if NX_ADV_HONEST == 0 { pass = pass + 1; w("T5 adv-enum PASS\n" as *u8) } else { w("T5 FAIL honest!=0\n" as *u8) } } else { w("T5 FAIL adv==honest\n" as *u8) }
36
37 // T6: negative + zero values survive the envelope (no unsigned coercion)
38 let c: *ApproxI64 = nx_approx_new(0 - 5, NX_ENV_ABS, 0, 0, NX_MATURITY_THEORETICAL, NX_ADV_HONEST)
39 if c.value == (0 - 5) { if c.param_a == 0 { pass = pass + 1; w("T6 negative/zero PASS\n" as *u8) } else { w("T6 FAIL param\n" as *u8) } } else { w("T6 FAIL neg\n" as *u8) }
40
41 w("NX-SKETCH-TYPES-KAT " as *u8); n(pass); w("/6" as *u8)
42 if pass == 6 { w(" GREEN\n" as *u8); return 0 }
43 w(" RED\n" as *u8)
44 return 1
45}