code wiki / _hdl_build / nx_coe_consistency.nx
nx_coe_consistency.nx source
↩ module page · 182 lines · 7618 B
1// nx_coe_consistency.nx -- CHAIN-OF-EVIDENCE CONSISTENCY PROOF (F713 consistency clause, seq135)
2// Proves the transparency log only APPENDED, never rewrote: for every published signed-tree-head
3// (root, leaves=m) in coe_witness.log, recompute the Merkle root over the FIRST m leaves of the
4// CURRENT signed chain and require it equals the recorded root, and require m is non-decreasing.
5// A match across all STHs => the log is append-only (no prefix was ever altered). Any mismatch =>
6// RED (rewrite/tamper detected). This is the RFC-6962 consistency property, sovereign.
7// Composes proven libs only: nx_str/nx_syscalls/nx_sha256. x86-lane. license_tier: ORIGINAL
8import "nx_str.nx"
9import "nx_syscalls.nx"
10import "nx_estate_path.nx" // ep_anchor: the CWD must not decide this organ's verdict
11import "nx_sha256.nx"
12
13const CC_CAP: i64 = 1048576
14const CC_MAXLEAF: i64 = 4096
15
16func cc_puts(s: *u8) -> i64 { sys_write(1, s, nx_str_len(s)); return 0 }
17func cc_pi(v: i64) -> i64 {
18 let t: *u8 = sys_mmap(32)
19 var m: i64 = v
20 var k: i64 = 0
21 if m == 0 { t[0] = 48 as u8; k = 1 }
22 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
23 let o: *u8 = sys_mmap(32)
24 var i: i64 = 0
25 while i < k { o[i] = t[k-1-i]; i = i + 1 }
26 sys_write(1, o, k)
27 return 0
28}
29func cc_nib(c: i64) -> i64 { if c >= 97 { return c - 87 } return c - 48 }
30func cc_line_end(b: *u8, i0: i64, n: i64) -> i64 { var e: i64 = i0; while e < n { if b[e] == (10 as u8) { return e } e = e + 1 } return n }
31func cc_find_tab(b: *u8, i0: i64, e: i64) -> i64 { var j: i64 = i0; while j < e { if b[j] == (9 as u8) { return j } j = j + 1 } return e }
32func cc_cp32(dst: *u8, src: *u8) -> i64 { var i: i64 = 0; while i < 32 { dst[i] = src[i]; i = i + 1 } return 0 }
33func cc_eq32(a: *u8, b: *u8) -> i64 { var i: i64 = 0; while i < 32 { if a[i] != b[i] { return 0 } i = i + 1 } return 1 }
34func cc_pair(l: *u8, r: *u8, out: *u8) -> i64 {
35 let b: *u8 = sys_mmap(64)
36 var i: i64 = 0
37 while i < 32 { b[i] = l[i]; i = i + 1 }
38 i = 0
39 while i < 32 { b[32+i] = r[i]; i = i + 1 }
40 sha256_digest(b, 64, out)
41 return 0
42}
43func cc_unhex32(src: *u8, off: i64, out: *u8) -> i64 {
44 var i: i64 = 0
45 while i < 32 {
46 let hi: i64 = cc_nib(src[off + i*2] as i64)
47 let lo: i64 = cc_nib(src[off + i*2 + 1] as i64)
48 out[i] = ((hi * 16) + lo) as u8
49 i = i + 1
50 }
51 return 0
52}
53// integer from ascii digits in [off,end); non-digits ignored
54func cc_atoi(b: *u8, off: i64, end: i64) -> i64 {
55 var v: i64 = 0
56 var i: i64 = off
57 while i < end {
58 let c: i64 = b[i] as i64
59 if (c >= 48) && (c <= 57) { v = v * 10 + (c - 48) }
60 i = i + 1
61 }
62 return v
63}
64// Merkle root over the first k leaves (flat 32-byte array) -> out; uses lvl/nxt scratch. -1 if k<1.
65func cc_root(leaves: *u8, k: i64, lvl: *u8, nxt: *u8, out: *u8) -> i64 {
66 if k < 1 { return 0 - 1 }
67 var c: i64 = 0
68 while c < k*32 { lvl[c] = leaves[c]; c = c + 1 }
69 var curn: i64 = k
70 while curn > 1 {
71 var nn: i64 = 0
72 var j: i64 = 0
73 while j < curn {
74 let leftp: *u8 = ((lvl as i64) + j*32) as *u8
75 var rightp: *u8 = ((lvl as i64) + j*32) as *u8
76 if (j + 1) < curn { rightp = ((lvl as i64) + (j+1)*32) as *u8 }
77 cc_pair(leftp, rightp, ((nxt as i64) + nn*32) as *u8)
78 nn = nn + 1
79 j = j + 2
80 }
81 c = 0
82 while c < nn*32 { lvl[c] = nxt[c]; c = c + 1 }
83 curn = nn
84 }
85 cc_cp32(out, lvl)
86 return 0
87}
88
89func cc_cats(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != (0 as u8) { dst[off+i] = s[i]; i = i + 1 } return off + i }
90func cc_catn(dst: *u8, off: i64, v: i64) -> i64 { let t: *u8 = sys_mmap(32); var m: i64 = v; 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 i: i64 = 0; while i < k { dst[off+i] = t[k-1-i]; i = i + 1 } return off + k }
91
92func main() -> i64 {
93 // ANCHOR FIRST (2026-08-04): run from buildroot this organ read an EMPTY/absent estate
94 // and fail-closed RED (or, worse, appended to a SECOND store). Its subject is the
95 // estate, so the caller's working directory must not decide its verdict.
96 ep_anchor()
97 cc_puts("=== COE-CONSISTENCY (F713/seq135): append-only proof across STH roots ===\n" as *u8)
98
99 // parse current leaves from the signed chain
100 let lp: *i64 = sys_mmap(16) as *i64
101 lp[0] = 0
102 let vb: *u8 = sys_read_file("knowledge/status/coe_signed.log" as *u8, lp)
103 var vn: i64 = lp[0]
104 if vn < 0 { vn = 0 }
105 if vn > CC_CAP { vn = CC_CAP }
106 let leaves: *u8 = sys_mmap(CC_MAXLEAF * 32 + 16)
107 var n: i64 = 0
108 var i: i64 = 0
109 while i < vn {
110 let e: i64 = cc_line_end(vb, i, vn)
111 if e > i {
112 if n < CC_MAXLEAF {
113 let t: i64 = cc_find_tab(vb, i, e)
114 if (t - i) >= 64 { cc_unhex32(vb, i, ((leaves as i64) + n*32) as *u8); n = n + 1 }
115 }
116 }
117 i = e + 1
118 }
119 if n == 0 { cc_puts("COE-CONSISTENCY RED reason=no-leaves\n" as *u8); sys_exit(1); return 1 }
120
121 // parse STH sequence from the witness log: field0 = root hex(64), field1 = leaves=<m>
122 lp[0] = 0
123 let wb: *u8 = sys_read_file("knowledge/status/coe_witness.log" as *u8, lp)
124 var wn: i64 = lp[0]
125 if wn < 0 { wn = 0 }
126 if wn > CC_CAP { wn = CC_CAP }
127 if wn == 0 { cc_puts("COE-CONSISTENCY RED reason=no-sth\n" as *u8); sys_exit(1); return 1 }
128
129 let lvl: *u8 = sys_mmap(CC_MAXLEAF * 32 + 16)
130 let nxt: *u8 = sys_mmap(CC_MAXLEAF * 32 + 16)
131 let rootbuf: *u8 = sys_mmap(32)
132 let sthroot: *u8 = sys_mmap(32)
133 var sths: i64 = 0
134 var ok: i64 = 1
135 var prevm: i64 = 0
136 i = 0
137 while i < wn {
138 let e: i64 = cc_line_end(wb, i, wn)
139 if e > i {
140 let t1: i64 = cc_find_tab(wb, i, e)
141 if (t1 - i) >= 64 {
142 let t2: i64 = cc_find_tab(wb, t1 + 1, e)
143 let mval: i64 = cc_atoi(wb, t1 + 1, t2)
144 cc_unhex32(wb, i, sthroot)
145 if mval > n { ok = 0 }
146 if mval < prevm { ok = 0 }
147 if mval >= 1 {
148 if mval <= n {
149 cc_root(leaves, mval, lvl, nxt, rootbuf)
150 if cc_eq32(rootbuf, sthroot) == 0 { ok = 0 }
151 }
152 }
153 prevm = mval
154 sths = sths + 1
155 }
156 }
157 i = e + 1
158 }
159
160 let gl: *u8 = sys_mmap(256)
161 var go: i64 = 0
162 if ok == 1 { go = cc_cats(gl, 0, "verdict=GREEN coe-attest append-only=OK sths=" as *u8) }
163 if ok == 0 { go = cc_cats(gl, 0, "verdict=RED coe-attest sths=" as *u8) }
164 go = cc_catn(gl, go, sths)
165 go = cc_cats(gl, go, " leaves=" as *u8)
166 go = cc_catn(gl, go, n)
167 gl[go] = 10 as u8
168 go = go + 1
169 let gfd: i64 = sys_openat_append("knowledge/status/coe_gate.log" as *u8, 0x1a4)
170 if gfd >= 0 { sys_write(gfd, gl, go); sys_close(gfd) }
171 cc_puts(" current-leaves=" as *u8); cc_pi(n)
172 cc_puts(" sths-checked=" as *u8); cc_pi(sths); cc_puts("\n" as *u8)
173 if ok == 1 {
174 cc_puts("COE-CONSISTENCY GREEN append-only=OK every-published-root-is-a-prefix sths=" as *u8); cc_pi(sths)
175 cc_puts(" leaves=" as *u8); cc_pi(n)
176 cc_puts(" envelope=cap:" as *u8); cc_pi(CC_CAP); cc_puts("/maxleaf:" as *u8); cc_pi(CC_MAXLEAF); cc_puts("\n" as *u8)
177 return 0
178 }
179 cc_puts("COE-CONSISTENCY RED reason=rewrite-or-truncation-detected sths=" as *u8); cc_pi(sths); cc_puts("\n" as *u8)
180 sys_exit(1)
181 return 1
182}