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

↩ module page · 172 lines · 7977 B
1// nx_legal_portal_post_gate.nx -- GATE for the interactive POST routes (lp_handle_post), ENGINEER verify.
2//
3// Proves the portal's MUTATING actions over HTTP (the markup/checklist interactivity),
4// composing D4 (annotate) + D8 (persist), each with a control:
5//   T1 POST annotate     : POST /portal/annotate adds a note -> 200, store grows
6//   T2 POST check         : add a required checklist item then POST /portal/check?ann= ->
7//                           the item is DONE (GET /portal/checklist -> remaining 0 READY)
8//   T3 MUTATION PERSISTS  : after the POSTs, save + reload into FRESH arrays -> the
9//                           checklist done-state + the note survive (durable interactivity)
10//   T4 AUTHZ              : POST to /staff at level 1 -> 403 ; unknown path -> 404
11//   T5 NEG                : POST /portal/annotate with no doc -> 400 (not silent)
12//
13// lp_handle (GET) is UNCHANGED -- the POST router is a new function, so the existing
14// portal GET gates are not regressed (re-verified separately).
15//
16// Evidence -> knowledge/status/legal_portal_post.log
17// license_tier: ORIGINAL
18import "nx_legal_portal.nx"
19import "nx_legal_portal_boot.nx"
20import "nx_doc_annotate.nx"
21import "nx_doc_envelope.nx"
22import "nx_doc_vault.nx"
23import "nx_legal_compliance.nx"
24import "nx_syscalls.nx"
25import "nx_gate_verdict.nx"
26
27const LPP_LOG: *u8 = "knowledge/status/legal_portal_post.log"
28const LPP_BASE: *u8 = "/tmp/nx_lpp_"
29
30func 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 }
31func 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
39}
40func slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
41func g_cat(d: *u8, o: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != (0 as u8) { d[o + i] = s[i]; i = i + 1 } return o + i }
42func g_starts(buf: *u8, n: i64, s: *u8) -> i64 {
  let sn: i64 = slen(s)
  if n < sn { return 0 }
  var i: i64 = 0
  while i < sn { if buf[i] != s[i] { return 0 } i = i + 1 }
  return 1
48}
49func g_contains(hay: *u8, n: i64, needle: *u8) -> i64 {
  let nn: i64 = slen(needle)
  if nn == 0 { return 1 }
  var i: i64 = 0
  while i + nn <= n {
      var m: i64 = 1
      var j: i64 = 0
      while j < nn { if hay[i + j] != needle[j] { m = 0; break } j = j + 1 }
      if m == 1 { return 1 }
      i = i + 1
  }
  return 0
61}
62
63func main() -> i64 {
  var ok: i64 = 1
  let ncap: i64 = 16
  let vcap: i64 = 8
  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
  let anflat: *i64 = sys_mmap(ncap * NF_STRIDE * 8) as *i64
  let vflat: *i64 = sys_mmap(vcap * VF_STRIDE * 8) as *i64
  let eidbuf: *i64 = sys_mmap(32) as *i64
  var vc: i64 = nx_vault_add(vflat, 0, vcap, 8601, 5001, 64, 1000)
75
  let ctx: *NxPortalCtx = sys_mmap(256) as *NxPortalCtx
  ctx.user_level = 1
  ctx.eflat = eflat; ctx.ne = 0
  ctx.rflat = rflat; ctx.nr = 0
  ctx.anflat = anflat; ctx.na = 0
  ctx.vflat = vflat; ctx.vc = vc
  ctx.env_ids = eidbuf; ctx.env_count = 0
83
  let req: *u8 = sys_mmap(4096)
  let out: *u8 = sys_mmap(16384)
86
  // ---- T1: POST annotate adds a note ----
  var t1: i64 = 1
  var rn: i64 = g_cat(req, 0, "POST /portal/annotate?doc=8601&ann=50&author=700&typ=0 HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  var on: i64 = lp_handle_post(ctx, ncap, req, rn, out)
  if g_starts(out, on, "HTTP/1.1 200" as *u8) != 1 { t1 = 0 }
  if g_contains(out, on, "ANNOTATED doc 8601 ann 50" as *u8) != 1 { t1 = 0 }
  if nx_ann_count(anflat, ctx.na, 8601, 1) != 1 { t1 = 0 }
  if t1 != 1 { ok = 0 }
95
  // ---- T2: POST add a required checklist item, then POST check it done ----
  var t2: i64 = 1
  rn = g_cat(req, 0, "POST /portal/annotate?doc=8601&ann=60&author=700&typ=4&req=1 HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle_post(ctx, ncap, req, rn, out)
  if g_starts(out, on, "HTTP/1.1 200" as *u8) != 1 { t2 = 0 }
  if nx_ann_checklist_remaining(anflat, ctx.na, 8601, 1) != 1 { t2 = 0 }   // pending
  rn = g_cat(req, 0, "POST /portal/check?ann=60 HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle_post(ctx, ncap, req, rn, out)
  if g_starts(out, on, "HTTP/1.1 200" as *u8) != 1 { t2 = 0 }
  if g_contains(out, on, "CHECKED ann 60" as *u8) != 1 { t2 = 0 }
  // GET the checklist via lp_handle -> now READY
  rn = g_cat(req, 0, "GET /portal/checklist?doc=8601 HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle(ctx, req, rn, out)
  if g_contains(out, on, "remaining 0 READY" as *u8) != 1 { t2 = 0 }
  if t2 != 1 { ok = 0 }
111
  // ---- T3: the mutations PERSIST across a reboot ----
  var t3: i64 = 1
  lp_boot_save(ctx, LPP_BASE, "clientA" as *u8)
  let anflat2: *i64 = sys_mmap(ncap * NF_STRIDE * 8) as *i64
  let eflat2: *i64 = sys_mmap(ecap * EF_STRIDE * 8) as *i64
  let rflat2: *i64 = sys_mmap(rcap * RF_STRIDE * 8) as *i64
  let vflat2: *i64 = sys_mmap(vcap * VF_STRIDE * 8) as *i64
  let eidbuf2: *i64 = sys_mmap(32) as *i64
  let ctx2: *NxPortalCtx = sys_mmap(256) as *NxPortalCtx
  ctx2.user_level = 1
  lp_boot_load(ctx2, LPP_BASE, "clientA" as *u8, eflat2, ecap, rflat2, rcap, anflat2, ncap, vflat2, vcap, eidbuf2)
  if nx_ann_count(anflat2, ctx2.na, 8601, 1) != 2 { t3 = 0 }              // note + check persisted
  rn = g_cat(req, 0, "GET /portal/checklist?doc=8601 HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle(ctx2, req, rn, out)
  if g_contains(out, on, "remaining 0 READY" as *u8) != 1 { t3 = 0 }       // done-state persisted
  if t3 != 1 { ok = 0 }
128
  // ---- T4: authz ----
  var t4: i64 = 1
  rn = g_cat(req, 0, "POST /staff/x HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle_post(ctx, ncap, req, rn, out)
  if g_starts(out, on, "HTTP/1.1 403" as *u8) != 1 { t4 = 0 }
  rn = g_cat(req, 0, "POST /portal/bogus HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle_post(ctx, ncap, req, rn, out)
  if g_starts(out, on, "HTTP/1.1 404" as *u8) != 1 { t4 = 0 }
  if t4 != 1 { ok = 0 }
138
  // ---- T5: NEG -- missing doc -> 400 ----
  var t5: i64 = 1
  rn = g_cat(req, 0, "POST /portal/annotate?ann=99 HTTP/1.1\r\nHost: x\r\n\r\n" as *u8)
  on = lp_handle_post(ctx, ncap, req, rn, out)
  if g_starts(out, on, "HTTP/1.1 400" as *u8) != 1 { t5 = 0 }
  if t5 != 1 { ok = 0 }
145
  // ---- evidence ----
  var fd: i64 = 1
  while fd >= 1 {
      ew(fd, "LEGALPORTALPOSTGATE authored=organ composes=D4+D8 post_annotate=" as *u8); ewn(fd, t1)
      ew(fd, " post_check_done=" as *u8); ewn(fd, t2)
      ew(fd, " mutation_persists=" as *u8); ewn(fd, t3)
      ew(fd, " authz=" as *u8); ewn(fd, t4)
      ew(fd, " neg_missing_doc=" as *u8); ewn(fd, t5)
      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(LPP_LOG, 420)
          if lf >= 1 { fd = lf } else { fd = 0 }
      } else {
          sys_close(fd); fd = 0
      }
  }
162
  // 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("LEGAL-PORTAL-POST-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
172}
nx_legal_portal_post_gate.nx source

`nx_legal_portal_post_gate.nx` source
