code wiki / _hdl_build / nx_doc_annotate_gate.nx
`nx_doc_annotate_gate.nx` source

↩ module page · 243 lines · 12908 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"
37import "nx_gate_verdict.nx"
38
39const DA_LOG: *u8 = "knowledge/status/doc_annotate.log"
40
41func 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 }
42func ewn(fd: i64, v: i64) -> i64 {
  let bb: *u8 = sys_mmap(28); var m: i64 = v
  if m < 0 { m = 0 - m; sys_write(fd, "-" as *u8, 1) }
  let t: *u8 = sys_mmap(28); var k: i64 = 0
  if m == 0 { t[0] = 48; 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 { bb[i] = t[k - 1 - i]; i = i + 1 }
  sys_write(fd, bb, k); return 0
50}
51func slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
52
53func mk_seal(s: *NxSeal, dt: i64, ewills: i64, signer: *u8, ts: i64,
           intent: i64, consent: i64, attribution: i64, retainable: i64,
           witnesses: i64, notarized: i64) -> i64 {
  s.doc_type = dt
  s.e_wills_allowed = ewills
  s.intent = intent
  s.consent = consent
  s.attribution = attribution
  s.retainable = retainable
  s.witnesses = witnesses
  s.notarized = notarized
  s.signer_id = signer
  s.signer_id_len = slen(signer)
  s.ts = ts
  return nx_seal_create(s)
68}
69
70func main() -> i64 {
  var ok: i64 = 1
72
  // ---- annotation overlay store ----
  let ncap: i64 = 64
  let anflat: *i64 = sys_mmap(ncap * NF_STRIDE * 8) as *i64
  var na: i64 = 0
77
  // ======== T1: add + count + type filter ========
  var t1: i64 = 1
  let D1: i64 = 8101
  na = nx_ann_add(anflat, na, ncap, 0, 1, D1, 1, AN_NOTE, 700, 1, 0, 100)
  na = nx_ann_add(anflat, na, ncap, 0, 2, D1, 1, AN_COMMENT, 700, 1, 0, 101)
  na = nx_ann_add(anflat, na, ncap, 0, 3, D1, 1, AN_HIGHLIGHT, 701, 2, 0, 102)
  na = nx_ann_add(anflat, na, ncap, 0, 4, D1, 1, AN_REDLINE, 701, 1, 0, 103)
  na = nx_ann_add(anflat, na, ncap, 0, 5, D1, 1, AN_SIGFIELD, 702, 501, 0, 104)
  na = nx_ann_add(anflat, na, ncap, 0, 6, D1, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 105)
  na = nx_ann_add(anflat, na, ncap, 0, 7, D1, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 106)
  na = nx_ann_add(anflat, na, ncap, 0, 8, D1, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 107)
  if nx_ann_count(anflat, na, D1, 1) != 8 { t1 = 0 }
  if nx_ann_count_type(anflat, na, D1, 1, AN_NOTE) != 1 { t1 = 0 }
  if nx_ann_count_type(anflat, na, D1, 1, AN_REDLINE) != 1 { t1 = 0 }
  if nx_ann_count_type(anflat, na, D1, 1, AN_SIGFIELD) != 1 { t1 = 0 }
  if nx_ann_count_type(anflat, na, D1, 1, AN_CHECK) != 3 { t1 = 0 }
  if t1 != 1 { ok = 0 }
95
  // ======== T2: redline accept/reject is additive ========
  var t2: i64 = 1
  let D2D: i64 = 8102
  na = nx_ann_add(anflat, na, ncap, 0, 20, D2D, 1, AN_REDLINE, 1, 800, 0, 200)
  na = nx_ann_add(anflat, na, ncap, 0, 21, D2D, 1, AN_REDLINE, 1, 800, 0, 201)
  let pre2: i64 = nx_ann_count(anflat, na, D2D, 1)
  if pre2 != 2 { t2 = 0 }
  // accept redline 20
  if nx_ann_resolve(anflat, na, 0, 20, AS_ACCEPTED, 900, 210) != ANR_OK { t2 = 0 }
  if nx_ann_status(anflat, na, 20) != AS_ACCEPTED { t2 = 0 }
  // reject redline 21 -> retained (not deleted)
  if nx_ann_resolve(anflat, na, 0, 21, AS_REJECTED, 900, 211) != ANR_OK { t2 = 0 }
  if nx_ann_status(anflat, na, 21) != AS_REJECTED { t2 = 0 }
  if nx_ann_count(anflat, na, D2D, 1) != pre2 { t2 = 0 }   // additive: count unchanged
  if t2 != 1 { ok = 0 }
111
  // ======== T3: threaded comments ========
  var t3: i64 = 1
  let D3D: i64 = 8103
  na = nx_ann_add(anflat, na, ncap, 0, 30, D3D, 1, AN_COMMENT, 1, 800, 0, 300)
  na = nx_ann_add_reply(anflat, na, ncap, 0, 31, D3D, 1, 801, 30, 301)
  na = nx_ann_add_reply(anflat, na, ncap, 0, 32, D3D, 1, 802, 30, 302)
  if nx_ann_thread_replies(anflat, na, 30) != 2 { t3 = 0 }
  if t3 != 1 { ok = 0 }
120
  // ======== T4: a required checklist gates the envelope send (compose D2) ========
  var t4: i64 = 1
  let ecap: i64 = 8
  let rcap: i64 = 8
  let eflat: *i64 = sys_mmap(ecap * EF_STRIDE * 8) as *i64
  let rflat: *i64 = sys_mmap(rcap * RF_STRIDE * 8) as *i64
  var ne: i64 = 0
  var nr: i64 = 0
  let D4D: i64 = 8104
  na = nx_ann_add(anflat, na, ncap, 0, 40, D4D, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 400)
  na = nx_ann_add(anflat, na, ncap, 0, 41, D4D, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 401)
  na = nx_ann_add(anflat, na, ncap, 0, 42, D4D, 1, AN_CHECK, 0, 700, ANF_REQUIRED, 402)
  ne = nx_env_create(eflat, ne, ecap, 9401, D4D, "Services Agreement" as *u8, 1, 400)
  nr = nx_env_add_recipient(rflat, nr, rcap, 9401, 401, ROLE_SIGNER, 1)
  // 2 of 3 done -> incomplete -> a portal would NOT send
  if nx_ann_resolve(anflat, na, 0, 40, AS_DONE, 700, 410) != ANR_OK { t4 = 0 }
  if nx_ann_resolve(anflat, na, 0, 41, AS_DONE, 700, 411) != ANR_OK { t4 = 0 }
  if nx_ann_checklist_remaining(anflat, na, D4D, 1) != 1 { t4 = 0 }
  if nx_ann_checklist_complete(anflat, na, D4D, 1) != 0 { t4 = 0 }
  if nx_env_status(eflat, ne, 9401) != ENV_DRAFT { t4 = 0 }   // not yet sent
  // complete the checklist -> may send
  if nx_ann_resolve(anflat, na, 0, 42, AS_DONE, 700, 412) != ANR_OK { t4 = 0 }
  if nx_ann_checklist_complete(anflat, na, D4D, 1) != 1 { t4 = 0 }
  if nx_env_send(eflat, ne, rflat, nr, 9401) != ENV_SEND_OK { t4 = 0 }
  if t4 != 1 { ok = 0 }
146
  // ======== T5: immutable-after-complete ========
  var t5: i64 = 1
  // (a) organ contract: frozen=1 refuses add + resolve
  let D5D: i64 = 8105
  let r_frozen_add: i64 = nx_ann_add(anflat, na, ncap, 1, 50, D5D, 1, AN_NOTE, 1, 0, 0, 500)
  if r_frozen_add != (0 - ANR_FROZEN) { t5 = 0 }
  // pre-completion annotation (frozen=0) lands
  na = nx_ann_add(anflat, na, ncap, 0, 51, D5D, 1, AN_NOTE, 1, 0, 0, 501)
  if nx_ann_resolve(anflat, na, 1, 51, AS_RESOLVED, 900, 510) != ANR_FROZEN { t5 = 0 }
  // (b) drive a REAL envelope on D5D to COMPLETED, derive frozen from its status
  let priv: *u8 = sys_mmap(64)
  priv[0]=0x9d; priv[1]=0x61; priv[2]=0xb1; priv[3]=0x9d; priv[4]=0xef; priv[5]=0xfd; priv[6]=0x5a; priv[7]=0x60
  priv[8]=0xba; priv[9]=0x84; priv[10]=0x4a; priv[11]=0xf4; priv[12]=0x92; priv[13]=0xec; priv[14]=0x2c; priv[15]=0xc4
  priv[16]=0x44; priv[17]=0x49; priv[18]=0xc5; priv[19]=0x69; priv[20]=0x7b; priv[21]=0x32; priv[22]=0x69; priv[23]=0x19
  priv[24]=0x70; priv[25]=0x3b; priv[26]=0xac; priv[27]=0x03; priv[28]=0x1c; priv[29]=0xae; priv[30]=0x7f; priv[31]=0x60
  let pub: *u8 = sys_mmap(64)
  pub[0]=0xd7; pub[1]=0x5a; pub[2]=0x98; pub[3]=0x01; pub[4]=0x82; pub[5]=0xb1; pub[6]=0x0a; pub[7]=0xb7
  pub[8]=0xd5; pub[9]=0x4b; pub[10]=0xfe; pub[11]=0xd3; pub[12]=0xc9; pub[13]=0x64; pub[14]=0x07; pub[15]=0x3a
  pub[16]=0x0e; pub[17]=0xe1; pub[18]=0x72; pub[19]=0xf3; pub[20]=0xda; pub[21]=0xa6; pub[22]=0x23; pub[23]=0x25
  pub[24]=0xaf; pub[25]=0x02; pub[26]=0x1a; pub[27]=0x68; pub[28]=0xf7; pub[29]=0x07; pub[30]=0x51; pub[31]=0x1a
  let dh: *u8 = sys_mmap(64)
  var di: i64 = 0
  while di < 32 { dh[di] = ((di * 7 + 3) & 0xff) as u8; di = di + 1 }
  let s: *NxSeal = sys_mmap(256) as *NxSeal
  s.doc_hash = dh; s.doc_hash_len = 32
  s.priv = priv; s.canon = sys_mmap(512); s.sig = sys_mmap(128)
  ne = nx_env_create(eflat, ne, ecap, 9501, D5D, "Services Agreement" as *u8, 1, 520)
  nr = nx_env_add_recipient(rflat, nr, rcap, 9501, 501, ROLE_SIGNER, 1)
  if nx_env_send(eflat, ne, rflat, nr, 9501) != ENV_SEND_OK { t5 = 0 }
  // control: still SENT -> not frozen -> add succeeds
  var frozen_sent: i64 = 0
  if nx_env_status(eflat, ne, 9501) == ENV_COMPLETED { frozen_sent = 1 }
  if frozen_sent != 0 { t5 = 0 }
  na = nx_ann_add(anflat, na, ncap, frozen_sent, 52, D5D, 1, AN_COMMENT, 1, 0, 0, 521)
  // complete it
  let a5: i64 = mk_seal(s, DT_CONTRACT, 1, "client@x.com" as *u8, 530, 1, 1, 1, 1, 0, 0)
  if a5 != SEAL_OK { t5 = 0 }
  if nx_env_sign(eflat, ne, rflat, nr, 9501, 501, s, pub) != ENV_SIGN_OK { t5 = 0 }
  if nx_env_try_complete(eflat, ne, rflat, nr, 9501) != ENV_COMPLETE_OK { t5 = 0 }
  // now frozen derives from a real signed envelope -> add REFUSED
  var frozen_done: i64 = 0
  if nx_env_status(eflat, ne, 9501) == ENV_COMPLETED { frozen_done = 1 }
  if frozen_done != 1 { t5 = 0 }
  let r_after: i64 = nx_ann_add(anflat, na, ncap, frozen_done, 53, D5D, 1, AN_NOTE, 1, 0, 0, 540)
  if r_after != (0 - ANR_FROZEN) { t5 = 0 }
  if t5 != 1 { ok = 0 }
193
  // ======== T6: per-version anchoring ========
  var t6: i64 = 1
  let vcap: i64 = 8
  let vflat: *i64 = sys_mmap(vcap * VF_STRIDE * 8) as *i64
  var vc: i64 = 0
  let D6D: i64 = 8106
  vc = nx_vault_add(vflat, vc, vcap, D6D, 6001, 100, 600)   // v1
  na = nx_ann_add(anflat, na, ncap, 0, 60, D6D, 1, AN_NOTE, 1, 0, 0, 600)
  vc = nx_vault_add(vflat, vc, vcap, D6D, 6002, 110, 601)   // v2 (bump)
  if nx_ann_count(anflat, na, D6D, 1) != 1 { t6 = 0 }       // pinned to v1
  if nx_ann_count(anflat, na, D6D, 2) != 0 { t6 = 0 }       // did NOT move to v2
  if t6 != 1 { ok = 0 }
206
  // ======== T7: a completed doc's prior annotations remain readable ========
  var t7: i64 = 1
  // D5D had pre-completion annotations 51 (note) + 52 (comment) before freeze
  if nx_ann_count(anflat, na, D5D, 1) != 2 { t7 = 0 }
  if nx_ann_status(anflat, na, 51) != AS_OPEN { t7 = 0 }
  if nx_ann_author(anflat, na, 52) < 0 { t7 = 0 }           // still findable
  if t7 != 1 { ok = 0 }
214
  // ---- evidence ----
  var fd: i64 = 1
  while fd >= 1 {
      ew(fd, "DOCANNOTATEGATE authored=organ composes=D1+D2+D5 add_count_type=" as *u8); ewn(fd, t1)
      ew(fd, " redline_additive=" as *u8); ewn(fd, t2)
      ew(fd, " threaded_comments=" as *u8); ewn(fd, t3)
      ew(fd, " checklist_gates_send=" as *u8); ewn(fd, t4)
      ew(fd, " immutable_after_complete=" as *u8); ewn(fd, t5)
      ew(fd, " per_version_anchored=" as *u8); ewn(fd, t6)
      ew(fd, " history_readable_frozen=" as *u8); ewn(fd, t7)
      if ok == 1 { ew(fd, " verdict=GREEN\n" as *u8) } else { ew(fd, " verdict=RED\n" as *u8) }
      if fd == 1 {
          let lf: i64 = sys_openat_append(DA_LOG, 420)
          if lf >= 1 { fd = lf } else { fd = 0 }
      } else {
          sys_close(fd); fd = 0
      }
  }
233
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = ok
  ctr__dry[1] = 1
  let rc__dry: i64 = gv_verdict("DOC-ANNOTATE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
243}
nx_doc_annotate_gate.nx source

`nx_doc_annotate_gate.nx` source
