sketch_types_gate.nx source
↩ module page · 93 lines · 5041 B
1// sketch_types_gate.nx -- the gate for the typed loss-envelope 139 modules import.
2// WHY: nx_gensota's gen-3 worklist rank 1 after the first three closures. This module is the
3// substrate's honesty contract for approximate primitives -- every sketch ships its loss NAMED,
4// BOUNDED and QUERYABLE -- so a defect here silently un-bounds every approximate answer.
5// THE TWO TEETH THAT ACTUALLY MATTER:
6// (a) DISCRIMINATOR DISTINCTNESS. envelope_kind, maturity and adv_safety are enums whose whole
7// job is to be TOLD APART at a composition boundary ("refuse Theoretical in production",
8// "never substitute Honest-only where Adversarial is required"). If two constants collide,
9// every such refusal silently passes the wrong thing and NOTHING else would notice.
10// ★A DISCRIMINATOR WHOSE VALUES CAN COLLIDE IS NOT A DISCRIMINATOR.
11// (b) 6-FIELD STRUCT ROUND-TRIP with SIX DISTINCT values. This ecosystem has a banked compiler
12// defect class where struct field offsets mis-resolve; a constructor test using repeated
13// values would pass straight through a swapped pair. Every field here gets a unique
14// witness, so any offset error surfaces as a specific mismatch.
15// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26).
16import "nx_syscalls.nx"
17import "nx_gate_verdict.nx"
18import "sketch_types.nx"
19
20// distinct witnesses -- no two equal, so a field swap cannot pass
21const STG_W_VALUE: i64 = 111
22const STG_W_PARAM: i64 = 16200000
23const STG_W_CONF: i64 = 682700000
24
25func main() -> i64 {
26 let ctr: *i64 = gv_ctr()
27 gv_head("SKETCH-TYPES-GATE -- the loss-envelope contract 139 modules import" as *u8)
28
29 // (a) discriminator distinctness -- the property the composition refusals rest on
30 var t1: i64 = 1
31 if NX_ENV_REL_STDDEV == NX_ENV_RANK_ERROR { t1 = 0 }
32 if NX_ENV_REL_STDDEV == NX_ENV_ABS { t1 = 0 }
33 if NX_ENV_REL_STDDEV == NX_ENV_REL_RANK_ERROR { t1 = 0 }
34 if NX_ENV_RANK_ERROR == NX_ENV_ABS { t1 = 0 }
35 if NX_ENV_RANK_ERROR == NX_ENV_REL_RANK_ERROR { t1 = 0 }
36 if NX_ENV_ABS == NX_ENV_REL_RANK_ERROR { t1 = 0 }
37 gv_check("T1 all FOUR envelope kinds are pairwise DISTINCT" as *u8, t1, ctr)
38
39 var t2: i64 = 1
40 if NX_MATURITY_THEORETICAL == NX_MATURITY_REFERENCE_IMPL { t2 = 0 }
41 if NX_MATURITY_THEORETICAL == NX_MATURITY_PRODUCTION { t2 = 0 }
42 if NX_MATURITY_REFERENCE_IMPL == NX_MATURITY_PRODUCTION { t2 = 0 }
43 gv_check("T2 maturity classes distinct (refuse-Theoretical-in-production can bite)" as *u8, t2, ctr)
44
45 var t3: i64 = 1
46 if NX_ADV_HONEST == NX_ADV_ADVERSARIAL { t3 = 0 }
47 gv_check("T3 Honest and Adversarial distinct (no silent substitution)" as *u8, t3, ctr)
48
49 // maturity is ORDERED by design (Theoretical < Reference < Production) so a
50 // >= comparison is a legitimate production admission test
51 var t4: i64 = 0
52 if NX_MATURITY_THEORETICAL < NX_MATURITY_REFERENCE_IMPL {
53 if NX_MATURITY_REFERENCE_IMPL < NX_MATURITY_PRODUCTION { t4 = 1 }
54 }
55 gv_check("T4 maturity is ORDERED, so a >= admission test is meaningful" as *u8, t4, ctr)
56
57 // (b) 6-field round-trip, every field a distinct witness
58 let a: *ApproxI64 = nx_approx_new(STG_W_VALUE, NX_ENV_RANK_ERROR, STG_W_PARAM,
59 STG_W_CONF, NX_MATURITY_PRODUCTION, NX_ADV_ADVERSARIAL)
60 var t5: i64 = 0
61 if (a as i64) != 0 { t5 = 1 }
62 gv_check("T5 constructor returns a non-null envelope" as *u8, t5, ctr)
63
64 var t6: i64 = 1
65 if a.value != STG_W_VALUE { t6 = 0 }
66 if a.envelope_kind != NX_ENV_RANK_ERROR { t6 = 0 }
67 if a.param_a != STG_W_PARAM { t6 = 0 }
68 if a.conf_ppb != STG_W_CONF { t6 = 0 }
69 if a.maturity != NX_MATURITY_PRODUCTION { t6 = 0 }
70 if a.adv_safety != NX_ADV_ADVERSARIAL { t6 = 0 }
71 gv_check("T6 all SIX fields round-trip with DISTINCT witnesses (offset-swap proof)" as *u8, t6, ctr)
72
73 // the ppb convention the header documents: conf 0.6827 -> 682_700_000
74 var t7: i64 = 0
75 if a.conf_ppb / 1000000 == 682 { if a.param_a / 1000000 == 16 { t7 = 1 } }
76 gv_check("T7 ppb fixed-point convention holds (conf .6827, stddev_rel .0162)" as *u8, t7, ctr)
77
78 // independence: a second envelope must not disturb the first (fresh allocation per call)
79 let b: *ApproxI64 = nx_approx_new(0 - 5, NX_ENV_ABS, 7, 950000000,
80 NX_MATURITY_THEORETICAL, NX_ADV_HONEST)
81 var t8: i64 = 0
82 if b.value == (0 - 5) { if a.value == STG_W_VALUE { if (b as i64) != (a as i64) { t8 = 1 } } }
83 gv_check("T8 envelopes are INDEPENDENT allocations; negatives survive" as *u8, t8, ctr)
84
85 // NEGATIVE CONTROL: the field comparator must be able to say NO.
86 var t9: i64 = 0
87 if a.value != STG_W_PARAM { if b.maturity != NX_MATURITY_PRODUCTION { t9 = 1 } }
88 gv_check("T9 NEG-CONTROL: wrong-field and wrong-value comparisons REJECT" as *u8, t9, ctr)
89
90 let rc: i64 = gv_verdict("SKETCH-TYPES-GATE" as *u8, ctr, "discriminators distinct, 6-field round-trip proven" as *u8)
91 sys_exit(rc)
92 return rc
93}