code wiki / _hdl_build / nx_lane_attest.nx
nx_lane_attest.nx source
↩ module page · 162 lines · 6503 B
1// nx_lane_attest.nx -- LANE-CLOSURE ATTESTOR (operator 2026-07-20: "this needs evidence and a
2// feedback loop keeping it honest"). Replaces the trusting substring-count lane gate: a seat-lane
3// closure is attested ONLY if the evidence ledger is COMPLETE (every manifest episode has a row --
4// silent drops refused), FRESH (every row ts within maxage of now -- a stale ledger from an old
5// run can NEVER pass), and OVER THRESHOLD (>= min property-verified greens). All parameters are
6// config DATA. exit 0 = attested; 1 = refused (any tooth); 2 = config.
7// argv: <attestconf> conf keys: ledger= manifest= min= maxage=
8// KNOWN LIMIT (filed, not hidden): greens are still only as good as the ledger row -- the loop
9// reverts fixes post-judge, so post-hoc re-judging needs the patch-persistence rung (debt filed).
10// license_tier: ORIGINAL No hw writes (Rule 26).
11import "nx_seat_drive_lib.nx"
12import "nx_deploy_lib.nx"
13import "nx_syscalls.nx"
14
15const LA_CAP: i64 = 1048576
16const LA_CONF_CAP: i64 = 65536
17
18func la_atoi(s: *u8) -> i64 {
19 var v: i64 = 0
20 var i: i64 = 0
21 while s[i] != (0 as u8) {
22 let c: i64 = s[i] as i64
23 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48) } }
24 i = i + 1
25 }
26 return v
27}
28
29// parse the integer right after needle at line-start scans of buf; fills vals[0..cap); returns count
30func la_ts_all(buf: *u8, n: i64, vals: *i64, cap: i64) -> i64 {
31 var cnt: i64 = 0
32 var i: i64 = 0
33 while i < n {
34 // line start at i: find " ts=" within the line, parse digits after it
35 var le: i64 = i
36 var s: i64 = 1
37 while s == 1 { if le >= n { s = 0 } else { if buf[le] == (10 as u8) { s = 0 } else { le = le + 1 } } }
38 var p: i64 = i
39 var found: i64 = 0 - 1
40 while p + 4 < le {
41 if buf[p] == (32 as u8) { if buf[p+1] == (116 as u8) { if buf[p+2] == (115 as u8) { if buf[p+3] == (61 as u8) { found = p + 4; p = le } } } }
42 p = p + 1
43 }
44 if found >= 0 {
45 var v: i64 = 0
46 var q: i64 = found
47 var d: i64 = 1
48 while d == 1 {
49 if q >= le { d = 0 } else {
50 let c: i64 = buf[q] as i64
51 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); q = q + 1 } else { d = 0 } } else { d = 0 }
52 }
53 }
54 if cnt < cap { vals[cnt] = v; cnt = cnt + 1 }
55 }
56 i = le + 1
57 }
58 return cnt
59}
60
61func main(argc: i64, argv: *i64) -> i64 {
62 if argc < 2 { sd_w("usage: nx_lane_attest <attestconf>\n" as *u8); sys_exit(2); return 2 }
63 let confp: *u8 = argv[1] as *u8
64 let conf: *u8 = sys_mmap(LA_CONF_CAP)
65 let cn: i64 = dp_read(confp, conf, LA_CONF_CAP)
66 if cn <= 0 { sd_w("LANE-ATTEST-CONF-MISSING\n" as *u8); sys_exit(2); return 2 }
67 let ledp: *u8 = sd_val(conf, cn, "ledger=" as *u8)
68 let manp: *u8 = sd_val(conf, cn, "manifest=" as *u8)
69 let mins: *u8 = sd_val(conf, cn, "min=" as *u8)
70 let ages: *u8 = sd_val(conf, cn, "maxage=" as *u8)
71 if (ledp as i64) == 0 { sd_w("LANE-ATTEST-CONF-BAD missing=ledger\n" as *u8); sys_exit(2); return 2 }
72 if (manp as i64) == 0 { sd_w("LANE-ATTEST-CONF-BAD missing=manifest\n" as *u8); sys_exit(2); return 2 }
73 if (mins as i64) == 0 { sd_w("LANE-ATTEST-CONF-BAD missing=min\n" as *u8); sys_exit(2); return 2 }
74 if (ages as i64) == 0 { sd_w("LANE-ATTEST-CONF-BAD missing=maxage\n" as *u8); sys_exit(2); return 2 }
75 let minv: i64 = la_atoi(mins)
76 let maxage: i64 = la_atoi(ages)
77
78 let led: *u8 = sys_mmap(LA_CAP)
79 let ln: i64 = dp_read(ledp, led, LA_CAP)
80 let man: *u8 = sys_mmap(LA_CAP)
81 let mn: i64 = dp_read(manp, man, LA_CAP)
82 if mn <= 0 { sd_w("LANE-ATTEST-REFUSED manifest-unreadable\n" as *u8); sys_exit(1); return 1 }
83
84 var fail: i64 = 0
85
86 // tooth 1: threshold -- >= min property-verified greens
87 let greens: i64 = sd_count(led, ln, "maker=GREEN" as *u8)
88 sd_w("ATTEST greens=" as *u8)
89 let nb: *u8 = sys_mmap(64)
90 var no: i64 = sd_num(nb, 0, greens)
91 sd_w(nb)
92 sd_w(" min=" as *u8)
93 no = sd_num(nb, 0, minv)
94 sd_w(nb)
95 if greens < minv { sd_w(" THRESHOLD-FAIL" as *u8); fail = 1 }
96 sd_w("\n" as *u8)
97
98 // tooth 2: completeness -- every manifest episode name has a ledger row (no silent drops)
99 var miss: i64 = 0
100 var total: i64 = 0
101 var mi: i64 = 0
102 while mi < mn {
103 var mle: i64 = mi
104 var s2: i64 = 1
105 while s2 == 1 { if mle >= mn { s2 = 0 } else { if man[mle] == (10 as u8) { s2 = 0 } else { mle = mle + 1 } } }
106 // name = chars up to '|'
107 var pe: i64 = mi
108 var s3: i64 = 1
109 while s3 == 1 { if pe >= mle { s3 = 0 } else { if man[pe] == (124 as u8) { s3 = 0 } else { pe = pe + 1 } } }
110 if pe > mi { if pe < mle {
111 total = total + 1
112 let needle: *u8 = sys_mmap(256)
113 var o2: i64 = sd_cat(needle, 0, "cand=" as *u8)
114 var k: i64 = mi
115 while k < pe { needle[o2] = man[k]; o2 = o2 + 1; k = k + 1 }
116 needle[o2] = 32 as u8
117 needle[o2 + 1] = 0 as u8
118 if sd_count(led, ln, needle) == 0 {
119 miss = miss + 1
120 sd_w("ATTEST MISSING-EPISODE " as *u8)
121 sd_w(needle)
122 sd_w("\n" as *u8)
123 }
124 } }
125 mi = mle + 1
126 }
127 sd_w("ATTEST episodes=" as *u8)
128 no = sd_num(nb, 0, total)
129 sd_w(nb)
130 sd_w(" missing=" as *u8)
131 no = sd_num(nb, 0, miss)
132 sd_w(nb)
133 if miss > 0 { sd_w(" COMPLETENESS-FAIL" as *u8); fail = 1 }
134 if total == 0 { sd_w(" EMPTY-MANIFEST-FAIL" as *u8); fail = 1 }
135 sd_w("\n" as *u8)
136
137 // tooth 3: freshness -- EVERY ledger row ts within maxage of now (stale ledgers refused)
138 let now: i64 = sys_now_realtime_sec()
139 let tsv: *i64 = sys_mmap(8 * 256) as *i64
140 let ntts: i64 = la_ts_all(led, ln, tsv, 256)
141 var stale: i64 = 0
142 var ti: i64 = 0
143 while ti < ntts { if now - tsv[ti] > maxage { stale = stale + 1 } ti = ti + 1 }
144 sd_w("ATTEST ts_rows=" as *u8)
145 no = sd_num(nb, 0, ntts)
146 sd_w(nb)
147 sd_w(" stale=" as *u8)
148 no = sd_num(nb, 0, stale)
149 sd_w(nb)
150 if stale > 0 { sd_w(" FRESHNESS-FAIL" as *u8); fail = 1 }
151 if ntts == 0 { sd_w(" NO-TS-ROWS-FAIL" as *u8); fail = 1 }
152 sd_w("\n" as *u8)
153
154 if fail == 0 {
155 sd_w("NX-LANE-ATTEST verdict=ATTESTED\n" as *u8)
156 sys_exit(0)
157 return 0
158 }
159 sd_w("NX-LANE-ATTEST verdict=REFUSED\n" as *u8)
160 sys_exit(1)
161 return 1
162}