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}