code wiki / _hdl_build / nx_wardrobe_state_gate.nx
nx_wardrobe_state_gate.nx source
↩ module page · 150 lines · 7748 B
1// nx_wardrobe_state_gate.nx -- certifies the wardrobe/exposure/transformation part.
2// Method (the proven one): every equality tooth carries a NON-VACUITY guard; the flagship tooth is the
3// ADULT GATE (a minor can never be placed in an exposed state, and the mutation test drives THAT tooth RED
4// while anti-vacuity holds). On full pass it writes the evidence artifacts the board's liar-kill stats.
5// license_tier: ORIGINAL expect_exit: 0
6import "nx_syscalls.nx"
7import "nx_gamesave.nx"
8import "nx_wardrobe_state.nx"
9
10func pw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
11func pn(v: i64) -> i64 {
12 if v==0 { sys_write(1,"0" as *u8,1); return 0 }
13 var m: i64=v; if m<0 { sys_write(1,"-" as *u8,1); m=0-m }
14 let t: *u8=sys_mmap(32); var k: i64=0
15 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 }
16 let o: *u8=sys_mmap(32); var q: i64=k-1; var i: i64=0
17 while q>=0 { o[i]=t[q]; i=i+1; q=q-1 }
18 sys_write(1,o,i); return 0
19}
20func line_g(nm: *u8) -> i64 { pw(" " as *u8); pw(nm as *u8); pw(" GREEN\n" as *u8); return 0 }
21func line_r(nm: *u8) -> i64 { pw(" " as *u8); pw(nm as *u8); pw(" RED\n" as *u8); return 0 }
22
23// write a small proof stamp file (adult-gate refusal witnessed on disk)
24func stamp(path: *u8, s: *u8) -> i64 {
25 let fd: i64 = sys_openat_wr(path, 0x1a4)
26 if fd < 0 { return 0-1 }
27 var n: i64=0; while s[n]!=(0 as u8){n=n+1}
28 sys_write(fd, s, n)
29 sys_fsync(fd); sys_close(fd)
30 return 0
31}
32
33func main() -> i64 {
34 let L: i64 = ws_len()
35 let a: *i64 = sys_mmap(L*8) as *i64
36 let b: *i64 = sys_mmap(L*8) as *i64
37 var pass: i64 = 0
38 let NT: i64 = 8
39
40 // ---- T1: init adult = fully dressed + coherent + zero exposure ----
41 ws_init(a, 25, 0)
42 var t1: i64 = 1
43 if ws_coherent(a) != 1 { t1 = 0 }
44 if ws_exposure(a) != 0 { t1 = 0 }
45 if a[2] != WS_MAXCOV { t1 = 0 }
46 if t1==1 { pass=pass+1; line_g("T1 init-adult dressed+coherent" as *u8) }
47 if t1==0 { line_r("T1 init-adult dressed+coherent" as *u8) }
48
49 // ---- T2: adult may expose; exposure rises; still coherent ----
50 var t2: i64 = 1
51 let r2: i64 = ws_set(a, 2, 0) // adult bares chest
52 if r2 != 0 { t2 = 0 }
53 if ws_exposure(a) <= 0 { t2 = 0 }
54 if ws_coherent(a) != 1 { t2 = 0 }
55 if t2==1 { pass=pass+1; line_g("T2 adult-expose allowed" as *u8) }
56 if t2==0 { line_r("T2 adult-expose allowed" as *u8) }
57
58 // ---- T3 FLAGSHIP: adult gate -- a minor can NEVER be exposed on a gated zone, state untouched ----
59 ws_init(b, 16, 0) // a minor, fully dressed
60 let ck_before: i64 = ws_ck(b)
61 var t3: i64 = 1
62 let rm: i64 = ws_set(b, 2, 0) // attempt to bare chest (gated) on a minor
63 if rm != WS_E_MINOR { t3 = 0 } // must be REFUSED with the specific code
64 if ws_ck(b) != ck_before { t3 = 0 } // and state BIT-IDENTICAL (no partial mutation)
65 let rh: i64 = ws_set(b, 4, 1) // hips below modest on a minor -> also refused
66 if rh != WS_E_MINOR { t3 = 0 }
67 // targeted, not a blanket lock: a minor MAY change a non-gated zone, and MAY stay modest
68 let rf: i64 = ws_set(b, 6, 1) // feet (non-gated) coverage change -> allowed
69 if rf != 0 { t3 = 0 }
70 let rmod: i64 = ws_set(b, 2, WS_MODEST) // chest to modest (not exposed) -> allowed
71 if rmod != 0 { t3 = 0 }
72 if ws_coherent(b) != 1 { t3 = 0 }
73 if t3==1 { pass=pass+1; line_g("T3 ADULT-GATE minor-refused+state-intact" as *u8) }
74 if t3==0 { line_r("T3 ADULT-GATE minor-refused+state-intact" as *u8) }
75
76 // ---- T4: coherence check BITES on an out-of-range zone AND on an illegally-exposed minor ----
77 ws_init(a, 25, 0)
78 var t4: i64 = 1
79 a[3] = WS_MAXCOV + 5 // corrupt a zone out of range
80 if ws_coherent(a) != 0 { t4 = 0 }
81 ws_init(a, 25, 0) // restore -> coherent again (proves the check isn't stuck at 0)
82 if ws_coherent(a) != 1 { t4 = 0 }
83 // a minor whose gated zone got exposed by tampering (direct write, bypassing ws_set) is INCOHERENT.
84 // chest is zone 2, whose coverage slot is w[2+2]=w[4]; baring it (0) on a 15-yr-old must read incoherent.
85 ws_init(a, 15, 0); a[4] = 0
86 if ws_coherent(a) != 0 { t4 = 0 }
87 if t4==1 { pass=pass+1; line_g("T4 coherence-bites (range+minor-tamper)" as *u8) }
88 if t4==0 { line_r("T4 coherence-bites (range+minor-tamper)" as *u8) }
89
90 // ---- T5: save/load round-trip bit-exact through the certified save part ----
91 ws_init(a, 25, 3); ws_set(a, 2, 0); ws_set(a, 4, 1) // a real, non-trivial adult state
92 let ck_saved: i64 = ws_ck(a)
93 let exp_saved: i64 = ws_exposure(a)
94 var t5: i64 = 1
95 let wrote: i64 = ws_save(a, "knowledge/nx_wardrobe_state.sav" as *u8, 424242)
96 if wrote <= 0 { t5 = 0 }
97 var z: i64 = 0
98 while z < L { b[z] = 0; z = z+1 } // zero the target so a stale value cannot pass
99 let got: i64 = ws_load(b, "knowledge/nx_wardrobe_state.sav" as *u8)
100 if got < 0 { t5 = 0 }
101 if ws_ck(b) != ck_saved { t5 = 0 } // checksum-identical after a round-trip through zero
102 var diff: i64 = 0
103 z = 0
104 while z < L { if b[z] != a[z] { diff = diff+1 } z = z+1 }
105 if diff != 0 { t5 = 0 }
106 if exp_saved <= 0 { t5 = 0 } // NON-VACUITY: the saved state was actually non-trivial
107 if t5==1 { pass=pass+1; line_g("T5 save/load bit-exact" as *u8) }
108 if t5==0 { line_r("T5 save/load bit-exact" as *u8) }
109
110 // ---- T6: LOAD REFUSES an incoherent persisted state (coherence holds across persistence) ----
111 // persist an ILLEGAL state directly via the raw save part (bypassing ws_set's gate), then ws_load it.
112 ws_init(a, 15, 0); a[4] = 0 // minor with a bared gated zone (chest=zone2 -> slot w[4]) = illegal on disk
113 var t6: i64 = 1
114 let wr2: i64 = gs_save("knowledge/nx_wardrobe_bad.sav" as *u8, WS_SCHEMA, a, L, 111)
115 if wr2 <= 0 { t6 = 0 }
116 let bad: i64 = ws_load(b, "knowledge/nx_wardrobe_bad.sav" as *u8)
117 if bad != WS_E_INCOHERENT { t6 = 0 } // load must REFUSE it
118 if t6==1 { pass=pass+1; line_g("T6 load-refuses-incoherent" as *u8) }
119 if t6==0 { line_r("T6 load-refuses-incoherent" as *u8) }
120
121 // ---- T7: determinism -- identical op sequence -> identical checksum ----
122 ws_init(a, 21, 2); ws_set(a, 2, 1); ws_morph(a, 5); ws_set(a, 5, 0)
123 ws_init(b, 21, 2); ws_set(b, 2, 1); ws_morph(b, 5); ws_set(b, 5, 0)
124 var t7: i64 = 1
125 if ws_ck(a) != ws_ck(b) { t7 = 0 }
126 if t7==1 { pass=pass+1; line_g("T7 determinism" as *u8) }
127 if t7==0 { line_r("T7 determinism" as *u8) }
128
129 // ---- T8 ANTI-VACUITY: dressed vs exposed differ in BOTH exposure and checksum ----
130 ws_init(a, 30, 0) // fully dressed
131 ws_init(b, 30, 0); ws_set(b, 2, 0); ws_set(b, 4, 0); ws_set(b, 1, 0) // exposed
132 var t8: i64 = 1
133 if ws_exposure(a) == ws_exposure(b) { t8 = 0 }
134 if ws_ck(a) == ws_ck(b) { t8 = 0 }
135 if ws_exposure(b) <= ws_exposure(a) { t8 = 0 }
136 if t8==1 { pass=pass+1; line_g("T8 anti-vacuity distinct-states" as *u8) }
137 if t8==0 { line_r("T8 anti-vacuity distinct-states" as *u8) }
138
139 pw("=== nx_wardrobe_state_gate " as *u8); pn(pass); pw("/" as *u8); pn(NT)
140 if pass==NT { pw(" GREEN ===\n" as *u8) }
141 if pass!=NT { pw(" RED ===\n" as *u8) }
142
143 // on full pass, bank the adult-gate refusal proof for the board liar-kill
144 if pass==NT {
145 stamp("knowledge/nx_wardrobe_adultgate.txt" as *u8,
146 "ADULT-GATE PROVEN: ws_set refuses gated-zone exposure on age<18 (rc=WS_E_MINOR), state bit-identical; ws_load refuses incoherent persisted state (rc=WS_E_INCOHERENT). nx_wardrobe_state_gate 8/8, mutation-proven.\n" as *u8)
147 }
148 if pass != NT { return 1 }
149 return 0
150}