code wiki / _hdl_build / nx_tls13_app_send_fd_gate.nx
nx_tls13_app_send_fd_gate.nx
buildroot/runtime/_hdl_build/nx_tls13_app_send_fd_gate.nx
about
nx_tls13_app_send_fd_gate.nx -- ENGINEER gate for the chunked TLS app-data
sender. Evidence-driven, re-runnable, no network: fabricates a CONNECTED
Tls13ServerSession with fixed ChaCha20-Poly1305 keys, sends a 40000-byte
payload to a real file fd, then plays the CLIENT side -- walks the wire
bytes record by record, asserts every record plaintext <= 16384 (the RFC
8446 ยง5.1 cap the old single-record path violated), decrypts each record
with the KAT'd nx_tls13_record_decrypt_v2 under the same keys, reassembles,
and byte-compares against the original payload. Also gates the empty-
payload path (one empty record) and the partner invariant: exactly
ceil(40000/16000) = 3 records, seq increments 0,1,2.
license_tier: ORIGINAL
dependencies 2 imports · 0 importers
imports: nx_tls13_app_send_fd.nxnx_gate_verdict.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| 30 | const TFG_CASES: *u8="send returns payload_len (40000)\nsession seq advanced to 3 (3 records)\nwire length = 40000 + 3*22\nrecord count = 3 (chunked, not one giant record)\nevery record plaintext <= 16384 (RFC 8446 5.1)\nevery record decrypts OK under app keys\nreassembled length = 40000\nreassembled plaintext byte-identical\nempty payload -> rc 0, one record\nempty payload advanced seq by 1\nfile range completes with closed reader\nfile range decrypts to exact header and selected bytes\nfailed header closes reader without reading body\npremature EOF retains read cause and closes reader\nempty region sends header and closes\ninvalid scratch closes owned reader\nclosed socket peer retains EPIPE and closes reader\n" |
functions
| 17 | func g_equal(a: *u8,b: *u8) -> i64 { var i: i64=0;while a[i]==b[i] { if a[i]==(0 as u8) { return 1 };i=i+1 };return 0 } called by 1: main |
| 19 | func g_slen(s: *u8) -> i64 { var n: i64=0;while s[n]!=(0 as u8) { n=n+1 };return n } called by 1: main |
| 20 | func 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 } |
| 21 | func g_pn(v: i64) -> i64 called by 1: main |
| 31 | func g_check(name: *u8, cond: i64) -> i64 |
| 37 | func main(argc: i64, argv: *i64) -> i64 |