nx_hr_admin_gate.nx source

1// nx_hr_admin_gate.nx -- referee for NISHI HR ADMIN (the admin-operations layer). PROVES, each with a negative 2// control / leak-check: 3// owner enrolled active -> is_superadmin=1 ; member invited -> is_invited=1 but NO access (resolve 0) and 4// NOT superadmin (leak-check) ; claim invited -> active@level, then NOT invited (re-register blocked) ; 5// re-claim = no-op (idempotent) ; suspend -> 0 ; REALM ISOLATION (same handle "brad", different realm = 6// different cred_id, an invite in one realm is invisible in the other) ; provision-by-handle id == derived id ; 7// deny-by-default for unknown handles ; roster counts (active vs invited). 8// GREEN iff every row matches. Durable -> knowledge/status/hr_admin_gate.log. 9import "nx_hr_admin.nx" 10import "nx_g_puts_lib.nx" 11import "nx_syscalls.nx" 12 13func g_num(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)}; let t: *u8=sys_mmap(28); 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{bb[i]=t[k-1-i];i=i+1}; sys_write(1,bb,k); return 0 } 14func g_w(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 } 15func g_wn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m}; let t: *u8=sys_mmap(28); 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{bb[i]=t[k-1-i];i=i+1}; sys_write(fd,bb,k); return 0 } 16func g_mkpfx(base: *u8, ms: i64, out: *u8) -> i64 { var o: i64=0; while base[o]!=(0 as u8){out[o]=base[o];o=o+1} let t: *u8=sys_mmap(28); var m: i64=ms; 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 z: i64=k-1; while z>=0{out[o]=t[z];o=o+1;z=z-1} out[o]=0 as u8; return o } 17func g_streq(a: *u8, b: *u8) -> i64 { var i: i64=0; while 1==1 { let ca: i64=a[i] as i64; let cb: i64=b[i] as i64; if ca!=cb { return 0 } if ca==0 { return 1 } i=i+1 } return 1 } 18func chk(got: i64, want: i64, label: *u8) -> i64 { 19 g_puts(" "); g_puts(label); g_puts(" got="); g_num(got); g_puts(" want="); g_num(want) 20 if got == want { g_puts(" PASS\n"); return 1 } 21 g_puts(" FAIL\n"); return 0 22} 23 24func main() -> i64 { 25 g_puts("=== NISHI HR ADMIN GATE (invite/claim/suspend, superadmin-by-construction, realm isolation) ===\n" as *u8) 26 var pass: i64=0; var rows: i64=0 27 let ms: i64 = sys_now_ms() 28 let nishi: *u8 = sys_mmap(96); g_mkpfx("/tmp/nx_hra_n_" as *u8, ms, nishi) 29 let andel: *u8 = sys_mmap(96); g_mkpfx("/tmp/nx_hra_a_" as *u8, ms, andel) 30 let NR: *u8 = "nishi_site_admin" as *u8; let NRN: i64 = 16 31 let AR: *u8 = "andelinwest_admin" as *u8; let ARN: i64 = 17 32 let fam: *u8 = "andelin" as *u8 33 34 let cid_owner: *u8 = sys_mmap(96) 35 let cid_brad: *u8 = sys_mmap(96) 36 let cid_brad_a: *u8 = sys_mmap(96) 37 let cid_chk: *u8 = sys_mmap(96) 38 39 // owner = elderwesto enrolled ACTIVE at level 3 (mirrors reality: elderwesto already has an OPAQUE account) 40 rows=rows+1; pass=pass+chk(hra_enroll(nishi, NR, NRN, "elderwesto" as *u8, 10, HRA_LVL_OWNER, fam, 1000, "system" as *u8, cid_owner), 0, "enroll elderwesto owner(3) active" as *u8) 41 rows=rows+1; pass=pass+chk(hra_is_superadmin(nishi, cid_owner, 64), 1, " -> owner is_superadmin=1 (auto-everything by construction)" as *u8) 42 43 // member brad invited -> is_invited but NO access yet, NOT superadmin 44 rows=rows+1; pass=pass+chk(hra_invite(nishi, NR, NRN, "brad" as *u8, 4, HRA_LVL_MEMBER, fam, 1000, "elderwesto" as *u8, cid_brad), 0, "invite brad(member)" as *u8) 45 rows=rows+1; pass=pass+chk(hra_is_invited(nishi, NR, NRN, "brad" as *u8, 4), 1, " -> brad is_invited=1" as *u8) 46 rows=rows+1; pass=pass+chk(hra_resolve_level(nishi, cid_brad, 64), 0, " -> invited brad has NO access yet (resolve 0)" as *u8) 47 rows=rows+1; pass=pass+chk(hra_is_superadmin(nishi, cid_brad, 64), 0, " -> member brad NOT superadmin (leak-check)" as *u8) 48 49 // claim (the LAN signup completing): invited -> active@1 50 rows=rows+1; pass=pass+chk(hra_claim(nishi, NR, NRN, "brad" as *u8, 4, fam, 2000, "self" as *u8), 1, "claim brad -> level 1" as *u8) 51 rows=rows+1; pass=pass+chk(hra_resolve_level(nishi, cid_brad, 64), 1, " -> claimed brad resolves to 1 (active)" as *u8) 52 rows=rows+1; pass=pass+chk(hra_is_invited(nishi, NR, NRN, "brad" as *u8, 4), 0, " -> claimed brad NOT invited (re-register blocked)" as *u8) 53 rows=rows+1; pass=pass+chk(hra_claim(nishi, NR, NRN, "brad" as *u8, 4, fam, 2001, "self" as *u8), 0, " -> re-claim is no-op (idempotent #10)" as *u8) 54 55 // suspend 56 rows=rows+1; pass=pass+chk(hra_suspend(nishi, NR, NRN, "brad" as *u8, 4, fam, 3000, "elderwesto" as *u8), 0, "suspend brad" as *u8) 57 rows=rows+1; pass=pass+chk(hra_resolve_level(nishi, cid_brad, 64), 0, " -> suspended brad -> 0" as *u8) 58 59 // REALM ISOLATION: brad is NOT invited in the andelinwest realm (different store + different cred_id) 60 rows=rows+1; pass=pass+chk(hra_is_invited(andel, AR, ARN, "brad" as *u8, 4), 0, "brad NOT invited in andelinwest realm (isolation)" as *u8) 61 rows=rows+1; pass=pass+chk(hra_invite(andel, AR, ARN, "brad" as *u8, 4, HRA_LVL_OWNER, fam, 1000, "elderwesto" as *u8, cid_brad_a), 0, " -> invite brad as admin on andelinwest" as *u8) 62 rows=rows+1; pass=pass+chk(g_streq(cid_brad, cid_brad_a), 0, " -> SAME handle 'brad' = DIFFERENT cred_id per realm" as *u8) 63 rows=rows+1; pass=pass+chk(hra_resolve_level(nishi, cid_brad, 64), 0, " -> nishifamily brad UNAFFECTED by andelinwest invite" as *u8) 64 65 // provision-by-handle stability (the SSOT correctness property): invite's cred_id == hr_cred_id re-derived 66 hrs_cred_id(NR, NRN, "brad" as *u8, 4, cid_chk) 67 rows=rows+1; pass=pass+chk(g_streq(cid_brad, cid_chk), 1, "cred_id STABLE (provision-by-handle == re-derived)" as *u8) 68 69 // deny-by-default for unknown handles 70 rows=rows+1; pass=pass+chk(hra_is_invited(nishi, NR, NRN, "stranger" as *u8, 8), 0, "unknown handle is_invited=0 (deny-by-default)" as *u8) 71 rows=rows+1; pass=pass+chk(hra_is_superadmin(nishi, "0000000000000000000000000000000000000000000000000000000000000000" as *u8, 64), 0, "unknown cred is_superadmin=0 (deny-by-default)" as *u8) 72 73 // roster counts: invite jensen+kelli -> active=1 (owner), invited=2 (jensen,kelli; brad now suspended) 74 let cid_j: *u8 = sys_mmap(96); let cid_k: *u8 = sys_mmap(96) 75 hra_invite(nishi, NR, NRN, "jensen" as *u8, 6, HRA_LVL_MEMBER, fam, 1000, "elderwesto" as *u8, cid_j) 76 hra_invite(nishi, NR, NRN, "kelli" as *u8, 5, HRA_LVL_MEMBER, fam, 1000, "elderwesto" as *u8, cid_k) 77 rows=rows+1; pass=pass+chk(hra_roster_count(nishi, HRA_ST_ACTIVE), 1, "roster active logins = 1 (elderwesto)" as *u8) 78 rows=rows+1; pass=pass+chk(hra_roster_count(nishi, HRA_ST_INVITED), 2, "roster pending invites = 2 (jensen,kelli)" as *u8) 79 80 g_puts("----\nNISHI-HR-ADMIN-GATE rows=" as *u8); g_num(rows); g_puts(" pass=" as *u8); g_num(pass) 81 if pass==rows { g_puts(" verdict=GREEN\n" as *u8) } else { g_puts(" verdict=RED\n" as *u8) } 82 let lg: i64=sys_openat_append("knowledge/status/hr_admin_gate.log" as *u8, 0x1a4) 83 if lg>=0 { 84 g_w(lg, "NISHI-HR-ADMIN-GATE rows=" as *u8); g_wn(lg, rows); g_w(lg, " pass=" as *u8); g_wn(lg, pass) 85 if pass==rows { g_w(lg, " verdict=GREEN\n" as *u8) } else { g_w(lg, " verdict=RED\n" as *u8) } 86 sys_close(lg) 87 } 88 if pass==rows { sys_exit(0); return 0 } 89 sys_exit(1); return 1 90}