nx_chatmsg_gate.nx source

1// nx_chatmsg_gate.nx -- proves the sovereign chat receipt ladder (nx_chatmsg). Native, fast. 2import "nx_syscalls.nx" 3import "nx_chatmsg.nx" 4import "nx_gate_verdict.nx" 5 6func g_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 7func g_pn(v: i64) -> i64 { 8 let b: *u8 = sys_mmap(28); var x: i64 = v 9 if x == 0 { b[0]=48; sys_write(1,b,1); return 0 } 10 var d: i64=0; var y: i64=x 11 while y>0 { d=d+1; y=y/10 } 12 var i: i64=d-1; y=x 13 while i>=0 { b[i]=(48+(y%10)) as u8; y=y/10; i=i-1 } 14 sys_write(1,b,d); return 0 15} 16func g_check(name: *u8, cond: i64) -> i64 { 17 if cond==1 { g_puts(" PASS " as *u8) } else { g_puts(" FAIL " as *u8) } 18 g_puts(name); g_puts("\n" as *u8); return cond 19} 20 21func main() -> i64 { 22 g_puts("nx_chatmsg gate (delivery/read-receipt ladder)\n" as *u8) 23 var pass: i64 = 0; var total: i64 = 0 24 25 // normal progression queued -> sent -> delivered -> read 26 var s: i64 = MS_QUEUED 27 s = cm_advance(s, MS_SENT) 28 s = cm_advance(s, MS_DELIVERED) 29 s = cm_advance(s, MS_READ) 30 pass = pass + g_check("progresses queued->sent->delivered->read" as *u8, (s == MS_READ) & (cm_is_read(s) == 1)); total=total+1 31 32 // MONOTONIC: a late DELIVERED receipt after READ does not regress 33 pass = pass + g_check("monotonic: late delivered receipt can't un-read" as *u8, cm_advance(MS_READ, MS_DELIVERED) == MS_READ); total=total+1 34 35 // duplicate receipt -> no change 36 pass = pass + g_check("duplicate receipt is idempotent" as *u8, cm_advance(MS_DELIVERED, MS_DELIVERED) == MS_DELIVERED); total=total+1 37 38 // a READ receipt may skip straight from SENT (read implies delivered) 39 pass = pass + g_check("read receipt implies delivered (skip ok)" as *u8, cm_advance(MS_SENT, MS_READ) == MS_READ); total=total+1 40 41 // offline message stays QUEUED until actually sent (never lost) 42 pass = pass + g_check("offline stays queued (cm_advance with no send keeps QUEUED)" as *u8, cm_advance(MS_QUEUED, MS_QUEUED) == MS_QUEUED); total=total+1 43 44 // unread badge counts delivered-but-not-read 45 let inbox: *i64 = sys_mmap(5*8) as *i64 46 inbox[0]=MS_READ; inbox[1]=MS_DELIVERED; inbox[2]=MS_DELIVERED; inbox[3]=MS_READ; inbox[4]=MS_SENT 47 let badge: i64 = cm_badge(inbox, 5) 48 g_puts(" [measure] inbox unread badge = " as *u8); g_pn(badge); g_puts("\n" as *u8) 49 pass = pass + g_check("unread badge counts delivered-not-read (=2)" as *u8, badge == 2); total=total+1 50 51 g_puts("---- chatmsg gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 52 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 53 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 54 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 55 let ctr__dry: *i64 = gv_ctr() 56 ctr__dry[0] = pass 57 ctr__dry[1] = total 58 let rc__dry: i64 = gv_verdict("CHATMSG-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 59 sys_exit(rc__dry) 60 return rc__dry 61}