nx_tls_hs_order_gate.nx source

1// nx_tls_hs_order_gate.nx -- COMPOSITION GATE for the team-authored _pe_tlshs state machine: 2// the TLS 1.3 server-flight order law, proven row by row. The canonical flight CONNECTS; 3// every adjacent reorder REFUSES; truncation does NOT connect; replay-after-connect REFUSES; 4// skipping cert_verify REFUSES. Durable: TLSHS-ROW/TLSHS-GATE lines -> 5// knowledge/status/tls_hs_order_gate.log. Exit 0 iff every row passes. Owner: Engineer (verify). 6// license_tier: ORIGINAL 7import "_pe_tlshs.nx" 8import "nx_syscalls.nx" 9 10func tg_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 } 11func tg_wn(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 } 12 13// run a 6-slot event sequence (n = how many are live) 14func tg_run(e0: i64, e1: i64, e2: i64, e3: i64, e4: i64, n: i64) -> i64 { 15 let ev: *i64 = sys_mmap(64) as *i64 16 ev[0] = e0; ev[1] = e1; ev[2] = e2; ev[3] = e3; ev[4] = e4 17 return _pe_tlshs_run(ev, n, 0) 18} 19 20func tg_row(lfd: i64, name: *u8, got: i64, want: i64) -> i64 { 21 tg_w(1, " " as *u8); tg_w(1, name); tg_w(1, ": got=" as *u8); tg_wn(1, got) 22 tg_w(lfd, "TLSHS-ROW name=" as *u8); tg_w(lfd, name) 23 tg_w(lfd, " got=" as *u8); tg_wn(lfd, got); tg_w(lfd, " want=" as *u8); tg_wn(lfd, want) 24 if got == want { tg_w(1, " PASS\n" as *u8); tg_w(lfd, " verdict=PASS\n" as *u8); return 1 } 25 tg_w(1, " FAIL\n" as *u8); tg_w(lfd, " verdict=FAIL\n" as *u8) 26 return 0 27} 28 29func main() -> i64 { 30 tg_w(1, "=== TLS HS ORDER GATE: flight-order law on the team-authored machine ===\n" as *u8) 31 let lfd: i64 = sys_openat_append("knowledge/status/tls_hs_order_gate.log" as *u8, 0x1a4) 32 if lfd < 0 { tg_w(1, " gate log open FAILED -- loud fail\n" as *u8); sys_exit(1); return 1 } 33 var pass: i64 = 0 34 // [1] canonical SH EE CERT CV FIN -> CONNECTED(5) 35 pass = pass + tg_row(lfd, "canonical-connects" as *u8, tg_run(0, 1, 2, 3, 4, 5), 5) 36 // [2..5] every adjacent reorder refused 37 pass = pass + tg_row(lfd, "swap-sh-ee" as *u8, tg_run(1, 0, 2, 3, 4, 5), 0 - 1) 38 pass = pass + tg_row(lfd, "swap-ee-cert" as *u8, tg_run(0, 2, 1, 3, 4, 5), 0 - 1) 39 pass = pass + tg_row(lfd, "swap-cert-cv" as *u8, tg_run(0, 1, 3, 2, 4, 5), 0 - 1) 40 pass = pass + tg_row(lfd, "swap-cv-fin" as *u8, tg_run(0, 1, 2, 4, 3, 5), 0 - 1) 41 // [6] truncated flight does NOT connect (ends WAIT_FIN=4) 42 pass = pass + tg_row(lfd, "truncated-not-connected" as *u8, tg_run(0, 1, 2, 3, 0, 4), 4) 43 // [7] replay after connect refused (strict: no events from CONNECTED) 44 let ev6: *i64 = sys_mmap(64) as *i64 45 ev6[0] = 0; ev6[1] = 1; ev6[2] = 2; ev6[3] = 3; ev6[4] = 4; ev6[5] = 4 46 pass = pass + tg_row(lfd, "replay-fin-refused" as *u8, _pe_tlshs_run(ev6, 6, 0), 0 - 1) 47 // [8] skipping cert_verify refused 48 pass = pass + tg_row(lfd, "skip-cv-refused" as *u8, tg_run(0, 1, 2, 4, 0, 4), 0 - 1) 49 tg_w(lfd, "TLSHS-GATE rows=8 pass=" as *u8); tg_wn(lfd, pass) 50 if pass == 8 { tg_w(lfd, " verdict=GREEN\n" as *u8) } else { tg_w(lfd, " verdict=RED\n" as *u8) } 51 sys_close(lfd) 52 tg_w(1, " --- TLS HS ORDER GATE: " as *u8); tg_wn(1, pass); tg_w(1, "/8 rows ---\n" as *u8) 53 if pass == 8 { tg_w(1, " TLS HS ORDER GATE: GREEN (out-of-order handshake REFUSED, by authored machine)\n" as *u8); sys_exit(0); return 0 } 54 tg_w(1, " TLS HS ORDER GATE: RED (fix the table or the emitter, never the gate)\n" as *u8) 55 sys_exit(1) 56 return 1 57}