code wiki / _hdl_build / nx_doc_annotate_gate.nx
nx_doc_annotate_gate.nx source
↩ module page · 235 lines · 12370 B
1// nx_doc_annotate_gate.nx -- GATE for LEGAL D4 (nx_doc_annotate).
2//
3// Drives the annotation/markup overlay composing D1 (vault versions) + D2
4// (envelope completion -> the freeze) + D5 (real Ed25519 seal to complete it)
5// and asserts every overlay invariant WITH a negative control:
6//
7// T1 ADD + COUNT + TYPE : notes/comments/highlights/redlines/checks/sigfields
8// land on a doc version; per-type counts are exact.
9// T2 REDLINE LIFECYCLE : a redline accepts (resolver recorded); another
10// rejects and is RETAINED (additive, count unchanged).
11// T3 THREADED COMMENTS : a comment + 2 replies -> thread_replies = 2.
12// T4 CHECKLIST GATES SEND : 3 required checklist items, 2 done -> complete=0
13// (a portal withholds nx_env_send); all done ->
14// complete=1 and nx_env_send = OK (compose w/ D2).
15// T5 IMMUTABLE-AFTER-COMPLETE (the crux) : (a) frozen=1 -> add/resolve REFUSED;
16// (b) a REAL envelope driven to COMPLETED yields
17// frozen := (status==COMPLETED) and a subsequent add
18// is REFUSED; control: a still-SENT envelope frozen=0
19// -> add succeeds. A signed agreement can't be re-marked.
20// T6 PER-VERSION ANCHORING : an annotation on v1 is not counted for v2 after a
21// vault version bump (it stays pinned to v1).
22// T7 HISTORY READABLE UNDER FREEZE : a completed doc's prior annotations remain
23// fully readable + counted; only NEW writes are refused.
24//
25// NOTE (honest): uses the single RFC 8032 KAT keypair for determinism (per-signer
26// keys = a PKI rung). What is proven is the overlay lifecycle + the freeze/additive
27// invariants and their composition with the real envelope + vault.
28//
29// Evidence -> knowledge/status/doc_annotate.log
30// license_tier: ORIGINAL
31import "nx_doc_annotate.nx"
32import "nx_doc_envelope.nx"
33import "nx_doc_seal.nx"
34import "nx_doc_vault.nx"
35import "nx_legal_compliance.nx"
36import "nx_syscalls.nx"
37
38const DA_LOG: *u8 = "knowledge/status/doc_annotate.log"
39
40func ew(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 }
41func ewn(fd: i64, v: i64) -> i64 {
42 let bb: *u8 = sys_mmap(28); var m: i64 = v
43 if m < 0 { m = 0 - m; sys_write(fd, "-" as *u8, 1) }
44 let t: *u8 = sys_mmap(28); var k: i64 = 0
45 if m == 0 { t[0] = 48; k = 1 }
46 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
47 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
48 sys_write(fd, bb, k); return 0
49}
50func slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
51
52func mk_seal(s: *NxSeal, dt: i64, ewills: i64, signer: *u8, ts: i64,
53 intent: i64, consent: i64, attribution: i64, retainable: i64,
54 witnesses: i64, notarized: i64) -> i64 {
55 s.doc_type = dt
56 s.e_wills_allowed = ewills
57 s.intent = intent
58 s.consent = consent
59 s.attribution = attribution
60 s.retainable = retainable
61 s.witnesses = witnesses
62 s.notarized = notarized
63 s.signer_id = signer
64 s.signer_id_len = slen(signer)
65 s.ts = ts
66 return nx_seal_create(s)
67}
68
69func main() -> i64 {
70 var ok: i64 = 1
71
72 // ---- annotation overlay store ----
73 let ncap: i64 = 64
74 let anflat: *i64 = sys_mmap(ncap * NF_STRIDE * 8) as *i64
75 var na: i64 = 0
76
77 // ======== T1: add + count + type filter ========
78 var t1: i64 = 1
79 let D1: i64 = 8101
80 na = nx_ann_add(anflat, na, ncap, 0, 1, D1, 1, AN_NOTE, 700, 1, 0, 100)
81 na = nx_ann_add(anflat, na, ncap, 0, 2, D1, 1, AN_COMMENT, 700, 1, 0, 101)
82 na = nx_ann_add(anflat, na, ncap, 0, 3, D1, 1, AN_HIGHLIGHT, 701, 2, 0, 102)
83 na = nx_ann_add(anflat, na, ncap, 0, 4, D1, 1, AN_REDLINE, 701, 1, 0, 103)
84 na = nx_ann_add(anflat, na, ncap, 0, 5, D1, 1, AN_SIGFIELD, 702, 501, 0, 104)
85 na = nx_ann_add(anflat, na, ncap, 0, 6, D1, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 105)
86 na = nx_ann_add(anflat, na, ncap, 0, 7, D1, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 106)
87 na = nx_ann_add(anflat, na, ncap, 0, 8, D1, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 107)
88 if nx_ann_count(anflat, na, D1, 1) != 8 { t1 = 0 }
89 if nx_ann_count_type(anflat, na, D1, 1, AN_NOTE) != 1 { t1 = 0 }
90 if nx_ann_count_type(anflat, na, D1, 1, AN_REDLINE) != 1 { t1 = 0 }
91 if nx_ann_count_type(anflat, na, D1, 1, AN_SIGFIELD) != 1 { t1 = 0 }
92 if nx_ann_count_type(anflat, na, D1, 1, AN_CHECK) != 3 { t1 = 0 }
93 if t1 != 1 { ok = 0 }
94
95 // ======== T2: redline accept/reject is additive ========
96 var t2: i64 = 1
97 let D2D: i64 = 8102
98 na = nx_ann_add(anflat, na, ncap, 0, 20, D2D, 1, AN_REDLINE, 1, 800, 0, 200)
99 na = nx_ann_add(anflat, na, ncap, 0, 21, D2D, 1, AN_REDLINE, 1, 800, 0, 201)
100 let pre2: i64 = nx_ann_count(anflat, na, D2D, 1)
101 if pre2 != 2 { t2 = 0 }
102 // accept redline 20
103 if nx_ann_resolve(anflat, na, 0, 20, AS_ACCEPTED, 900, 210) != ANR_OK { t2 = 0 }
104 if nx_ann_status(anflat, na, 20) != AS_ACCEPTED { t2 = 0 }
105 // reject redline 21 -> retained (not deleted)
106 if nx_ann_resolve(anflat, na, 0, 21, AS_REJECTED, 900, 211) != ANR_OK { t2 = 0 }
107 if nx_ann_status(anflat, na, 21) != AS_REJECTED { t2 = 0 }
108 if nx_ann_count(anflat, na, D2D, 1) != pre2 { t2 = 0 } // additive: count unchanged
109 if t2 != 1 { ok = 0 }
110
111 // ======== T3: threaded comments ========
112 var t3: i64 = 1
113 let D3D: i64 = 8103
114 na = nx_ann_add(anflat, na, ncap, 0, 30, D3D, 1, AN_COMMENT, 1, 800, 0, 300)
115 na = nx_ann_add_reply(anflat, na, ncap, 0, 31, D3D, 1, 801, 30, 301)
116 na = nx_ann_add_reply(anflat, na, ncap, 0, 32, D3D, 1, 802, 30, 302)
117 if nx_ann_thread_replies(anflat, na, 30) != 2 { t3 = 0 }
118 if t3 != 1 { ok = 0 }
119
120 // ======== T4: a required checklist gates the envelope send (compose D2) ========
121 var t4: i64 = 1
122 let ecap: i64 = 8
123 let rcap: i64 = 8
124 let eflat: *i64 = sys_mmap(ecap * EF_STRIDE * 8) as *i64
125 let rflat: *i64 = sys_mmap(rcap * RF_STRIDE * 8) as *i64
126 var ne: i64 = 0
127 var nr: i64 = 0
128 let D4D: i64 = 8104
129 na = nx_ann_add(anflat, na, ncap, 0, 40, D4D, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 400)
130 na = nx_ann_add(anflat, na, ncap, 0, 41, D4D, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 401)
131 na = nx_ann_add(anflat, na, ncap, 0, 42, D4D, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 402)
132 ne = nx_env_create(eflat, ne, ecap, 9401, D4D, "Services Agreement" as *u8, 1, 400)
133 nr = nx_env_add_recipient(rflat, nr, rcap, 9401, 401, ROLE_SIGNER, 1)
134 // 2 of 3 done -> incomplete -> a portal would NOT send
135 if nx_ann_resolve(anflat, na, 0, 40, AS_DONE, 700, 410) != ANR_OK { t4 = 0 }
136 if nx_ann_resolve(anflat, na, 0, 41, AS_DONE, 700, 411) != ANR_OK { t4 = 0 }
137 if nx_ann_checklist_remaining(anflat, na, D4D, 1) != 1 { t4 = 0 }
138 if nx_ann_checklist_complete(anflat, na, D4D, 1) != 0 { t4 = 0 }
139 if nx_env_status(eflat, ne, 9401) != ENV_DRAFT { t4 = 0 } // not yet sent
140 // complete the checklist -> may send
141 if nx_ann_resolve(anflat, na, 0, 42, AS_DONE, 700, 412) != ANR_OK { t4 = 0 }
142 if nx_ann_checklist_complete(anflat, na, D4D, 1) != 1 { t4 = 0 }
143 if nx_env_send(eflat, ne, rflat, nr, 9401) != ENV_SEND_OK { t4 = 0 }
144 if t4 != 1 { ok = 0 }
145
146 // ======== T5: immutable-after-complete ========
147 var t5: i64 = 1
148 // (a) organ contract: frozen=1 refuses add + resolve
149 let D5D: i64 = 8105
150 let r_frozen_add: i64 = nx_ann_add(anflat, na, ncap, 1, 50, D5D, 1, AN_NOTE, 1, 0, 0, 500)
151 if r_frozen_add != (0 - ANR_FROZEN) { t5 = 0 }
152 // pre-completion annotation (frozen=0) lands
153 na = nx_ann_add(anflat, na, ncap, 0, 51, D5D, 1, AN_NOTE, 1, 0, 0, 501)
154 if nx_ann_resolve(anflat, na, 1, 51, AS_RESOLVED, 900, 510) != ANR_FROZEN { t5 = 0 }
155 // (b) drive a REAL envelope on D5D to COMPLETED, derive frozen from its status
156 let priv: *u8 = sys_mmap(64)
157 priv[0]=0x9d; priv[1]=0x61; priv[2]=0xb1; priv[3]=0x9d; priv[4]=0xef; priv[5]=0xfd; priv[6]=0x5a; priv[7]=0x60
158 priv[8]=0xba; priv[9]=0x84; priv[10]=0x4a; priv[11]=0xf4; priv[12]=0x92; priv[13]=0xec; priv[14]=0x2c; priv[15]=0xc4
159 priv[16]=0x44; priv[17]=0x49; priv[18]=0xc5; priv[19]=0x69; priv[20]=0x7b; priv[21]=0x32; priv[22]=0x69; priv[23]=0x19
160 priv[24]=0x70; priv[25]=0x3b; priv[26]=0xac; priv[27]=0x03; priv[28]=0x1c; priv[29]=0xae; priv[30]=0x7f; priv[31]=0x60
161 let pub: *u8 = sys_mmap(64)
162 pub[0]=0xd7; pub[1]=0x5a; pub[2]=0x98; pub[3]=0x01; pub[4]=0x82; pub[5]=0xb1; pub[6]=0x0a; pub[7]=0xb7
163 pub[8]=0xd5; pub[9]=0x4b; pub[10]=0xfe; pub[11]=0xd3; pub[12]=0xc9; pub[13]=0x64; pub[14]=0x07; pub[15]=0x3a
164 pub[16]=0x0e; pub[17]=0xe1; pub[18]=0x72; pub[19]=0xf3; pub[20]=0xda; pub[21]=0xa6; pub[22]=0x23; pub[23]=0x25
165 pub[24]=0xaf; pub[25]=0x02; pub[26]=0x1a; pub[27]=0x68; pub[28]=0xf7; pub[29]=0x07; pub[30]=0x51; pub[31]=0x1a
166 let dh: *u8 = sys_mmap(64)
167 var di: i64 = 0
168 while di < 32 { dh[di] = ((di * 7 + 3) & 0xff) as u8; di = di + 1 }
169 let s: *NxSeal = sys_mmap(256) as *NxSeal
170 s.doc_hash = dh; s.doc_hash_len = 32
171 s.priv = priv; s.canon = sys_mmap(512); s.sig = sys_mmap(128)
172 ne = nx_env_create(eflat, ne, ecap, 9501, D5D, "Services Agreement" as *u8, 1, 520)
173 nr = nx_env_add_recipient(rflat, nr, rcap, 9501, 501, ROLE_SIGNER, 1)
174 if nx_env_send(eflat, ne, rflat, nr, 9501) != ENV_SEND_OK { t5 = 0 }
175 // control: still SENT -> not frozen -> add succeeds
176 var frozen_sent: i64 = 0
177 if nx_env_status(eflat, ne, 9501) == ENV_COMPLETED { frozen_sent = 1 }
178 if frozen_sent != 0 { t5 = 0 }
179 na = nx_ann_add(anflat, na, ncap, frozen_sent, 52, D5D, 1, AN_COMMENT, 1, 0, 0, 521)
180 // complete it
181 let a5: i64 = mk_seal(s, DT_CONTRACT, 1, "client@x.com" as *u8, 530, 1, 1, 1, 1, 0, 0)
182 if a5 != SEAL_OK { t5 = 0 }
183 if nx_env_sign(eflat, ne, rflat, nr, 9501, 501, s, pub) != ENV_SIGN_OK { t5 = 0 }
184 if nx_env_try_complete(eflat, ne, rflat, nr, 9501) != ENV_COMPLETE_OK { t5 = 0 }
185 // now frozen derives from a real signed envelope -> add REFUSED
186 var frozen_done: i64 = 0
187 if nx_env_status(eflat, ne, 9501) == ENV_COMPLETED { frozen_done = 1 }
188 if frozen_done != 1 { t5 = 0 }
189 let r_after: i64 = nx_ann_add(anflat, na, ncap, frozen_done, 53, D5D, 1, AN_NOTE, 1, 0, 0, 540)
190 if r_after != (0 - ANR_FROZEN) { t5 = 0 }
191 if t5 != 1 { ok = 0 }
192
193 // ======== T6: per-version anchoring ========
194 var t6: i64 = 1
195 let vcap: i64 = 8
196 let vflat: *i64 = sys_mmap(vcap * VF_STRIDE * 8) as *i64
197 var vc: i64 = 0
198 let D6D: i64 = 8106
199 vc = nx_vault_add(vflat, vc, vcap, D6D, 6001, 100, 600) // v1
200 na = nx_ann_add(anflat, na, ncap, 0, 60, D6D, 1, AN_NOTE, 1, 0, 0, 600)
201 vc = nx_vault_add(vflat, vc, vcap, D6D, 6002, 110, 601) // v2 (bump)
202 if nx_ann_count(anflat, na, D6D, 1) != 1 { t6 = 0 } // pinned to v1
203 if nx_ann_count(anflat, na, D6D, 2) != 0 { t6 = 0 } // did NOT move to v2
204 if t6 != 1 { ok = 0 }
205
206 // ======== T7: a completed doc's prior annotations remain readable ========
207 var t7: i64 = 1
208 // D5D had pre-completion annotations 51 (note) + 52 (comment) before freeze
209 if nx_ann_count(anflat, na, D5D, 1) != 2 { t7 = 0 }
210 if nx_ann_status(anflat, na, 51) != AS_OPEN { t7 = 0 }
211 if nx_ann_author(anflat, na, 52) < 0 { t7 = 0 } // still findable
212 if t7 != 1 { ok = 0 }
213
214 // ---- evidence ----
215 var fd: i64 = 1
216 while fd >= 1 {
217 ew(fd, "DOCANNOTATEGATE authored=organ composes=D1+D2+D5 add_count_type=" as *u8); ewn(fd, t1)
218 ew(fd, " redline_additive=" as *u8); ewn(fd, t2)
219 ew(fd, " threaded_comments=" as *u8); ewn(fd, t3)
220 ew(fd, " checklist_gates_send=" as *u8); ewn(fd, t4)
221 ew(fd, " immutable_after_complete=" as *u8); ewn(fd, t5)
222 ew(fd, " per_version_anchored=" as *u8); ewn(fd, t6)
223 ew(fd, " history_readable_frozen=" as *u8); ewn(fd, t7)
224 if ok == 1 { ew(fd, " verdict=GREEN\n" as *u8) } else { ew(fd, " verdict=RED\n" as *u8) }
225 if fd == 1 {
226 let lf: i64 = sys_openat_append(DA_LOG, 420)
227 if lf >= 1 { fd = lf } else { fd = 0 }
228 } else {
229 sys_close(fd); fd = 0
230 }
231 }
232
233 if ok == 1 { return 0 }
234 return 1
235}