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

6189 B133 linesdepth 13pulls 34 transitivereach 0 importersview sourcekind gate/prooftopic tls13
docsdependenciesstructsconstsfunctions

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 1 imports · 0 importers

nx_tls13_app_send_fd.nx nx_tls13_app_send_fd_gate.nx

imports: nx_tls13_app_send_fd.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main g_puts nx_tls13_server_session_ne sys_mmap x25519_keypair_public sys_mmap ↻ x25519_base_point x25519 nx_scratch_save nx_scratch_init sys_mmap ↻ nx_scratch nx_scratch_init ↻ nx_scratch_oom sys_write sys_exit sys_mmap ↻ fe_alloc nx_scratch ↻ fe_from_bytes fe_one fe_zero fe_zero ↻ fe_copy x25519_ladder_step fe_cswap nx_scratch_save ↻ fe_alloc ↻ fe_add fe_sq fe_mul fe_sub fe_mul ↻ fe_mul_a24 nx_scratch_save ↻ fe_alloc ↻ fe_mul ↻ nx_scratch_restore nx_scratch_restore ↻ fe_cswap ↻

structs

none

consts

none

functions

15func 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 }
called by 2: g_checkmain
16func g_pn(v: i64) -> i64
called by 1: main
25func g_check(name: *u8, cond: i64) -> i64
called by 1: main calls 1: g_puts
30func main() -> i64