nx_handoff_gate.nx source
↩ module page · 244 lines · 8009 B
1// nx_handoff_gate.nx -- SHARED deep-gate primitives (the DRY keystone of the sensor-gap program).
2//
3// Per [[feedback-handoff-chain-sota-gate-doctrine]] step 1: makes deepening ANY gate cheap (rule 15 DRY)
4// instead of hand-rolling ~3000 liar-killers. Three sensor families, one import:
5// LIAR-KILLERS -- hg_neg_control (a wrong-input score must stay under a floor, else the metric is
6// GAMED/broken), hg_monotonic_* (physics: drift accumulates, counts don't jump back),
7// hg_invariant_le/ge (bounds: drifted can never beat its clean floor),
8// hg_evidence_file (a claim's artifact must OPEN on disk -- never asserted).
9// REGRESSION -- hg_baseline_load (absent baseline => -1, NEVER fabricated) + hg_no_backslide /
10// hg_no_worsen (stored SOTA-track guard: a change that worsens any tracked value = RED)
11// + hg_baseline_print (the canonical capture line).
12// TELEMETRY -- HgStage per-handoff records (quality/bytes/time/fail) + hg_chain_report (per-stage
13// table, not just a final number) + LOCALIZERS hg_chain_worst_drop (WHICH handoff lost
14// the most quality) and hg_chain_max_time (WHERE the time goes).
15// Pure logic + read-only I/O; deterministic; no writes (never-brick by construction). Library (no main);
16// proven by runtime/_hdl_build/nx_handoff_gate_proof.nx. First consumer: nx_sensor_gap_census.
17// license_tier: ORIGINAL
18import "syscalls.nx"
19import "runtime.nx"
20
21// ===== liar-killer primitives =========================================
22
23// A metric fed WRONG input must score <= floor. Returns 1 = honest, 0 = GAMED (the number can lie).
24func hg_neg_control(wrong_score: i64, floor: i64) -> i64 {
25 if wrong_score <= floor { return 1 }
26 return 0
27}
28
29// 1 iff vals[0..n) is non-decreasing (physics: accumulation never reverses). n<=1 is trivially monotone.
30func hg_monotonic_nondec(vals: *i64, n: i64) -> i64 {
31 var i: i64 = 1
32 while i < n {
33 if vals[i] < vals[i-1] { return 0 }
34 i = i + 1
35 }
36 return 1
37}
38
39// 1 iff vals[0..n) is non-increasing.
40func hg_monotonic_noninc(vals: *i64, n: i64) -> i64 {
41 var i: i64 = 1
42 while i < n {
43 if vals[i] > vals[i-1] { return 0 }
44 i = i + 1
45 }
46 return 1
47}
48
49// physical bound: a must not exceed b (e.g. drifted-ref quality <= clean-ref floor).
50func hg_invariant_le(a: i64, b: i64) -> i64 {
51 if a <= b { return 1 }
52 return 0
53}
54
55func hg_invariant_ge(a: i64, b: i64) -> i64 {
56 if a >= b { return 1 }
57 return 0
58}
59
60// evidence-grounding: the artifact a claim rests on must OPEN on disk. 1 = present, 0 = absent.
61func hg_evidence_file(path: *u8) -> i64 {
62 let fd: i64 = sys_openat_rd(path)
63 if fd < 0 { return 0 }
64 sys_close(fd)
65 return 1
66}
67
68// ===== regression-baseline machinery ==================================
69
70// parse up to maxn base-10 ints from buf[0..len); returns count found. Go-flag scan (no frozen-index trap).
71func hg_parse_ints(buf: *u8, len: i64, out: *i64, maxn: i64) -> i64 {
72 var i: i64 = 0
73 var count: i64 = 0
74 while i < len {
75 let c: i64 = buf[i] as i64
76 var isdig: i64 = 0
77 if c >= 48 { if c <= 57 { isdig = 1 } }
78 if isdig == 0 { i = i + 1 }
79 if isdig == 1 {
80 var val: i64 = 0
81 var go: i64 = 1
82 while go == 1 {
83 go = 0
84 if i < len {
85 let d: i64 = buf[i] as i64
86 if d >= 48 { if d <= 57 { val = val * 10 + (d - 48); i = i + 1; go = 1 } }
87 }
88 }
89 if count < maxn { out[count] = val }
90 count = count + 1
91 }
92 }
93 return count
94}
95
96// load a baseline file of ints; returns count parsed, or -1 if the file is ABSENT/unreadable
97// (an absent baseline is reported, never fabricated -- evidence-grounding).
98func hg_baseline_load(path: *u8, out: *i64, maxn: i64) -> i64 {
99 let fd: i64 = sys_openat_rd(path)
100 if fd < 0 { return 0 - 1 }
101 let cap: i64 = 4096
102 let buf: *u8 = sys_mmap(cap)
103 var total: i64 = 0
104 var go: i64 = 1
105 while go == 1 {
106 go = 0
107 let tail: *u8 = ((buf as i64) + total) as *u8
108 let n: i64 = sys_read(fd, tail, cap - total)
109 if n > 0 { total = total + n; if total < cap { go = 1 } }
110 }
111 sys_close(fd)
112 return hg_parse_ints(buf, total, out, maxn)
113}
114
115// higher-is-better guard: 1 iff EVERY cur[i] >= base[i] (no backslide). 0 = REGRESSION.
116func hg_no_backslide(cur: *i64, base: *i64, n: i64) -> i64 {
117 var i: i64 = 0
118 while i < n {
119 if cur[i] < base[i] { return 0 }
120 i = i + 1
121 }
122 return 1
123}
124
125// lower-is-better guard (latency, bytes, error counts): 1 iff EVERY cur[i] <= base[i].
126func hg_no_worsen(cur: *i64, base: *i64, n: i64) -> i64 {
127 var i: i64 = 0
128 while i < n {
129 if cur[i] > base[i] { return 0 }
130 i = i + 1
131 }
132 return 1
133}
134
135// print the canonical tab-separated baseline capture line: TAG\tv0\tv1...\n
136func hg_baseline_print(tag: *u8, vals: *i64, n: i64) -> i64 {
137 print(tag)
138 var i: i64 = 0
139 while i < n {
140 print("\t" as *u8)
141 print_i64(vals[i])
142 i = i + 1
143 }
144 print("\n" as *u8)
145 return 0
146}
147
148// ===== handoff telemetry ==============================================
149// One record per handoff stage; report PER-STAGE so a micro-change shows WHICH handoff moved on WHICH axis.
150
151struct HgStage {
152 name: *u8,
153 quality: i64,
154 bytes: i64,
155 time_us: i64,
156 fail: i64,
157}
158
159const HG_STAGE_BYTES: i64 = 40
160
161func hg_stage_at(stages: *HgStage, i: i64) -> *HgStage {
162 return ((stages as i64) + i * HG_STAGE_BYTES) as *HgStage
163}
164
165func hg_stage_set(stages: *HgStage, i: i64, name: *u8, quality: i64, bytes: i64, time_us: i64, fail: i64) -> i64 {
166 let s: *HgStage = hg_stage_at(stages, i)
167 s.name = name
168 s.quality = quality
169 s.bytes = bytes
170 s.time_us = time_us
171 s.fail = fail
172 return 0
173}
174
175// count of failed stages in the chain
176func hg_chain_fails(stages: *HgStage, n: i64) -> i64 {
177 var f: i64 = 0
178 var i: i64 = 0
179 while i < n {
180 let s: *HgStage = hg_stage_at(stages, i)
181 if s.fail != 0 { f = f + 1 }
182 i = i + 1
183 }
184 return f
185}
186
187// LOCALIZER: index (1..n-1) of the handoff with the LARGEST quality drop vs its predecessor; -1 if n<2.
188func hg_chain_worst_drop(stages: *HgStage, n: i64) -> i64 {
189 if n < 2 { return 0 - 1 }
190 var worst: i64 = 1
191 var wdrop: i64 = 0
192 let s0: *HgStage = hg_stage_at(stages, 0)
193 var prevq: i64 = s0.quality
194 var i: i64 = 1
195 while i < n {
196 let s: *HgStage = hg_stage_at(stages, i)
197 let drop: i64 = prevq - s.quality
198 if drop > wdrop { wdrop = drop; worst = i }
199 prevq = s.quality
200 i = i + 1
201 }
202 return worst
203}
204
205// LOCALIZER: index of the slowest stage; -1 if n<1.
206func hg_chain_max_time(stages: *HgStage, n: i64) -> i64 {
207 if n < 1 { return 0 - 1 }
208 var best: i64 = 0
209 let s0: *HgStage = hg_stage_at(stages, 0)
210 var bt: i64 = s0.time_us
211 var i: i64 = 1
212 while i < n {
213 let s: *HgStage = hg_stage_at(stages, i)
214 if s.time_us > bt { bt = s.time_us; best = i }
215 i = i + 1
216 }
217 return best
218}
219
220// per-stage table (quality / bytes / time_us / fail per handoff); returns the fail count.
221func hg_chain_report(tag: *u8, stages: *HgStage, n: i64) -> i64 {
222 print(" [chain " as *u8)
223 print(tag)
224 print("] stage : quality bytes time_us fail\n" as *u8)
225 var i: i64 = 0
226 while i < n {
227 let s: *HgStage = hg_stage_at(stages, i)
228 print(" " as *u8)
229 print_i64(i)
230 print(" " as *u8)
231 print(s.name)
232 print(" : " as *u8)
233 print_i64(s.quality)
234 print(" " as *u8)
235 print_i64(s.bytes)
236 print(" " as *u8)
237 print_i64(s.time_us)
238 print(" " as *u8)
239 print_i64(s.fail)
240 print("\n" as *u8)
241 i = i + 1
242 }
243 return hg_chain_fails(stages, n)
244}