code wiki / _hdl_build / nx_provstmt_gate.nx
nx_provstmt_gate.nx source
↩ module page · 138 lines · 6709 B
1// nx_provstmt_gate.nx -- teeth over nx_provstmt_lib. IN-PROCESS, fixtures IN MEMORY, no filesystem.
2//
3// THE TOOTH THAT MATTERS IS T13: three DISTINCT digests must land in ORDER (subject, then srcSha256, then
4// closureSha256). A contains-only suite passes with the fields cross-wired -- artifact sha in the predicate
5// and source sha in the subject would satisfy every membership test while attesting the wrong object, which
6// is this rung's entire failure mode. Order plus distinctness is what makes the wiring falsifiable.
7
8import "nx_syscalls.nx"
9import "nx_gate_verdict.nx"
10import "nx_provstmt_lib.nx"
11
12func pg_find(hay: *u8, n: i64, needle: *u8) -> i64 {
13 var nl: i64 = 0
14 while needle[nl] != (0 as u8) { nl = nl + 1 }
15 if nl == 0 { return 0 - 1 }
16 var i: i64 = 0
17 while i + nl <= n {
18 var k: i64 = 0
19 var same: i64 = 1
20 while k < nl {
21 if hay[i + k] != needle[k] { same = 0; k = nl } else { k = k + 1 }
22 }
23 if same == 1 { return i }
24 i = i + 1
25 }
26 return 0 - 1
27}
28
29// A 64-char hex string that is valid and DISTINCT per seed: seed byte repeated. seed must be a hex char.
30func pg_mkhex(out: *u8, seedc: i64) -> i64 {
31 var i: i64 = 0
32 while i < 64 { out[i] = seedc as u8; i = i + 1 }
33 out[64] = 0 as u8
34 return 64
35}
36
37func main() -> i64 {
38 let ctr: *i64 = gv_ctr()
39 gv_head("NX-PROVSTMT-GATE -- can a statement attest the wrong object and still pass?" as *u8)
40
41 let a: *u8 = sys_mmap(80)
42 let b: *u8 = sys_mmap(80)
43 let c: *u8 = sys_mmap(80)
44 pg_mkhex(a, 97) // "aaa..."
45 pg_mkhex(b, 98) // "bbb..."
46 pg_mkhex(c, 99) // "ccc..."
47
48 gv_check("T1 HEX ACCEPT: a 64-char lowercase hex digest validates" as *u8, pv_hex_ok(a), ctr)
49
50 let short: *u8 = sys_mmap(80)
51 pg_mkhex(short, 97)
52 short[63] = 0 as u8
53 var t2: i64 = 0
54 if pv_hex_ok(short) == 0 { t2 = 1 }
55 gv_check("T2 NEG-CONTROL LENGTH: 63 chars is REFUSED -- a truncated digest matches nothing in the in-toto model and must not be serialised" as *u8, t2, ctr)
56
57 let bad: *u8 = sys_mmap(80)
58 pg_mkhex(bad, 97)
59 bad[10] = 103 as u8 // 'g'
60 var t3: i64 = 0
61 if pv_hex_ok(bad) == 0 { t3 = 1 }
62 gv_check("T3 NEG-CONTROL ALPHABET: a non-hex byte is REFUSED" as *u8, t3, ctr)
63
64 let up: *u8 = sys_mmap(80)
65 pg_mkhex(up, 97)
66 up[0] = 65 as u8 // 'A'
67 var t4: i64 = 0
68 if pv_hex_ok(up) == 0 { t4 = 1 }
69 gv_check("T4 NEG-CONTROL CASE: uppercase hex is REFUSED BY DESIGN -- every estate producer emits lowercase, so uppercase is evidence of a hand-typed or foreign digest and refusing is wrong-in-the-direction-of-refusing" as *u8, t4, ctr)
70
71 // ---- encoder round-trip, with the leading-zero case pinned ----
72 let dig: *u8 = sys_mmap(40)
73 var i: i64 = 0
74 while i < 32 { dig[i] = 0 as u8; i = i + 1 }
75 dig[0] = 0 as u8
76 dig[1] = 15 as u8
77 dig[31] = 255 as u8
78 let hx: *u8 = sys_mmap(80)
79 pv_hex_of(dig, hx)
80 gv_check("T5 ENCODER OUTPUT VALIDATES: pv_hex_of produces a string pv_hex_ok accepts -- the two halves of the lib agree on their own alphabet" as *u8, pv_hex_ok(hx), ctr)
81
82 var t6: i64 = 0
83 if hx[0] == (48 as u8) { if hx[1] == (48 as u8) { if hx[2] == (48 as u8) { if hx[3] == (102 as u8) {
84 if hx[62] == (102 as u8) { if hx[63] == (102 as u8) { t6 = 1 } } } } } }
85 gv_check("T6 LEADING ZERO PINNED: byte 0x00 encodes as 00 and 0x0f as 0f, and byte 31 lands at chars 62-63 -- the collapse-a-zero bug and any stride error both fail here" as *u8, t6, ctr)
86
87 gv_check("T7 EQ ACCEPT: identical digests compare equal" as *u8, pv_hex_eq(a, a), ctr)
88
89 let atail: *u8 = sys_mmap(80)
90 pg_mkhex(atail, 97)
91 atail[63] = 98 as u8
92 var t8: i64 = 0
93 if pv_hex_eq(a, atail) == 0 { t8 = 1 }
94 gv_check("T8 NEG-CONTROL TAIL SENSITIVITY: digests differing ONLY in the last char compare unequal -- a prefix-bounded compare passes every earlier tooth and fails exactly this one" as *u8, t8, ctr)
95
96 // ---- the statement ----
97 let J: *u8 = sys_mmap(PV_STMT_CAP)
98 let jn: i64 = pv_build(J, "nx_fixture" as *u8, a, b, c)
99 var t9: i64 = 0
100 if jn > 0 { if pg_find(J, jn, "https://in-toto.io/Statement/v1" as *u8) >= 0 { t9 = 1 } }
101 gv_check("T9 STATEMENT BUILDS and carries the ITE-6 _type URI -- and this success is also the fixture-reached proof for every refusal tooth below: the SAME inputs minus one mutation build fine, so each refusal is attributable to its mutation" as *u8, t9, ctr)
102
103 var t10: i64 = 0
104 if jn > 0 { if pg_find(J, jn, "nx_fixture.elf" as *u8) >= 0 { t10 = 1 } }
105 gv_check("T10 SUBJECT NAME: the subject is the ARTIFACT (<target>.elf), never an evidence frame -- the wrong-subject defect this rung exists to close" as *u8, t10, ctr)
106
107 let pa: i64 = pg_find(J, jn, a)
108 let pb: i64 = pg_find(J, jn, b)
109 let pc: i64 = pg_find(J, jn, c)
110 var t11: i64 = 0
111 if pa >= 0 { if pb >= 0 { if pc >= 0 { t11 = 1 } } }
112 gv_check("T11 ALL THREE DIGESTS PRESENT: artifact, source and closure each appear" as *u8, t11, ctr)
113
114 var t12: i64 = 0
115 if pg_find(J, jn, "srcSha256" as *u8) >= 0 { if pg_find(J, jn, "closureSha256" as *u8) >= 0 { t12 = 1 } }
116 gv_check("T12 PREDICATE FIELDS NAMED: srcSha256 and closureSha256 keys present" as *u8, t12, ctr)
117
118 var t13: i64 = 0
119 if pa >= 0 { if pa < pb { if pb < pc { t13 = 1 } } }
120 gv_check("T13 NEG-CONTROL WIRING ORDER: with three DISTINCT digests, artifact must precede src must precede closure in the serialised bytes (subject before predicate, src before closure). Cross-wired fields -- the artifact sha in the predicate, the source sha in the subject -- satisfy every membership tooth above and fail exactly this one" as *u8, t13, ctr)
121
122 var t14: i64 = 0
123 if pv_build(J, "nx_fixture" as *u8, bad, b, c) == 0 { t14 = 1 }
124 gv_check("T14 NEG-CONTROL BUILD REFUSES a malformed artifact digest -- returns 0 and writes nothing, so a partial statement can never be mistaken for a whole one" as *u8, t14, ctr)
125
126 var t15: i64 = 0
127 if pv_build(J, "" as *u8, a, b, c) == 0 { t15 = 1 }
128 gv_check("T15 NEG-CONTROL EMPTY TARGET refused -- a subject with no name is not a subject" as *u8, t15, ctr)
129
130 let jn2: i64 = pv_build(J, "nx_fixture" as *u8, a, b, c)
131 var t16: i64 = 0
132 if jn2 > 0 { if pg_find(J, jn2, "UNSIGNED-STATEMENT" as *u8) >= 0 { t16 = 1 } }
133 gv_check("T16 HONESTY MARKER: the statement declares IN-BAND that no DSSE envelope signs it yet -- a reader must never infer a signature that does not exist" as *u8, t16, ctr)
134
135 let rc: i64 = gv_verdict("PROVSTMT-GATE" as *u8, ctr, "every conjunct is a NAMED tooth above and this note restates none of them" as *u8)
136 sys_exit(rc)
137 return rc
138}