{"name":"std/tls.nu","source":"// stdlib/std/tls.nu — a pure-NURL TLS 1.3 client (RFC 8446).\n//\n// No OpenSSL, no FFI beyond the libc TCP socket: the handshake crypto\n// (X25519, ChaCha20-Poly1305, HKDF, SHA-256) is all pure NURL, so a\n// program can open an authenticated, encrypted TLS 1.3 connection on a\n// host with nothing installed — Linux, macOS, the BSDs, Windows.\n//\n// Cipher suites: TLS_AES_128_GCM_SHA256 and TLS_CHACHA20_POLY1305_SHA256\n// with the X25519 group — between them accepted by essentially every\n// modern TLS 1.3 server (OpenSSL, BoringSSL, nginx, the big CDNs).\n//\n// Surface:\n//   ( tls_connect host port server_name )          → !TlsConn TlsErr  (verify-full)\n//   ( tls_connect_insecure host port server_name ) → !TlsConn TlsErr  (no cert check)\n//   ( tls_write conn bytes )                       → !v TlsErr\n//   ( tls_read conn max )                          → !( Vec u ) TlsErr  ([] at EOF)\n//   ( tls_read_into conn dst max )                 → !i TlsErr  (appended to dst; 0 at EOF)\n//   ( tls_key_update conn request_peer )           → !v TlsErr  KeyUpdate (RFC 8446 §4.6.3)\n//   ( tls_ktls conn )                              → i  record protection to the kernel\n//                                                     (1 write, 2 read, 3 both; Linux 6.14+)\n//   ( tls_ktls_default on )                        → v  every connection after its handshake\n//                                                     (or NURL_KTLS=1)\n//   ( tls_close conn )                             → v  close_notify + close the socket\n//\n// A TlsConn is a handle: every copy is the same connection, and its last\n// owner releases it (closing the socket if tls_close has not).\n//\n// `tls_connect` is secure by default: it completes the handshake and then\n// verifies the server certificate chain (see verify.nu) against the system\n// trust store, failing with TlsBadCert otherwise. `tls_connect_insecure`\n// is the encrypted-but-unauthenticated escape hatch.\n\n$ `stdlib/core/marker.nu`\n$ `stdlib/core/string.nu`\n$ `stdlib/core/vec.nu`\n$ `stdlib/std/bytes.nu`\n$ `stdlib/std/hash_sha256.nu`\n$ `stdlib/std/hkdf.nu`\n$ `stdlib/std/x25519.nu`\n$ `stdlib/std/ecdsa_p256.nu`\n$ `stdlib/std/chacha20poly1305.nu`\n$ `stdlib/std/aes_gcm.nu`\n$ `stdlib/std/mlkem.nu`\n$ `stdlib/std/time.nu`\n$ `stdlib/std/tls_verify.nu`\n\n& `libc` @ nurl_tcp_connect s host i port → i\n\n& `c` @ nurl_monotonic_ns → i\n\n// Fiber/reactor primitives (nurl_fiber_current, nurl_reactor_wait_*,\n// nurl_tcp_get_fd / _timeout_ms / _set_nonblock). FFI-only module, so\n// this import keeps tls.nu free of any stdlib/std/net.nu dependency —\n// net.nu imports THIS module and dispatches its polymorphic TcpConn\n// reads/writes to the pure TLS stack without an import cycle.\n$ `stdlib/std/async_ffi.nu`\n$ `stdlib/core/rcbox.nu`\n$ `stdlib/core/slice.nu`\n\n// Park the current fiber until `raw`'s socket is readable (want = 0)\n// or writable (want = 1), honouring the handle's configured timeout\n// (0 = wait for ever, matching the blocking path's SO_RCVTIMEO\n// semantics). Returns T when the socket is ready, F on timeout or a\n// missing fiber context.\n@ __tls_io_wait i raw i want → b {\n    : i fd ( nurl_tcp_get_fd raw )\n    : i ms ( nurl_tcp_timeout_ms raw )\n    : i deadline ? != want 0 ( nurl_tcp_write_wait_ms raw ) ? > ms 0 ms - 0 1\n    ? == deadline 0 { ^ F } {}\n    : i rc ? != want 0 ( nurl_reactor_wait_write fd deadline ) ( nurl_reactor_wait_read fd deadline )\n    ^ > rc 0\n}\n\n// Write all of `data` to the raw socket fd. Returns F on any error.\n//\n// Context-aware: on a fiber the socket is flipped non-blocking and an\n// EAGAIN parks on the reactor until writable (the worker pthread stays\n// free for other fibers); off a fiber the write blocks in the kernel,\n// which is what a synchronous client wants.\n@ _tls_sock_write i fd ( Vec u ) data → b {\n    : *u dp ( vec_data [u] data )\n    : i n ( vec_len [u] data )\n    : b on_fiber != ( nurl_fiber_current ) 0\n    ? on_fiber { ( nurl_tcp_set_nonblock fd 1 ) } {}\n    : ~ i off 0\n    ~ < off n {\n        : i wn ( nurl_tcp_write fd # s + # i dp off - n off )\n        ? <= wn 0 {\n            : ~ b retry F\n            ? & on_fiber == ( nurl_tcp_err_kind fd ) 7 {\n                = retry ( __tls_io_wait fd 1 )\n            } {}\n            ? retry {} { ^ F }\n        } {\n            = off + off wn\n        }\n    }\n    ^ T\n}\n\n& `c` @ nurl_rand_fill *u buf i n → i\n\n// `head` then `body` to the socket in one sendmsg per attempt\n// (nurl_tcp_write2), parking a fiber while the socket is full.\n@ _tls_sock_write2 i fd ( Vec u ) head ( Vec u ) body → b {\n    : *u hp ( vec_data [u] head )\n    : *u bp ( vec_data [u] body )\n    : i hn ( vec_len [u] head )\n    : i bn ( vec_len [u] body )\n    : i n + hn bn\n    : b on_fiber != ( nurl_fiber_current ) 0\n    ? on_fiber { ( nurl_tcp_set_nonblock fd 1 ) } {}\n    : ~ i off 0\n    ~ < off n {\n        : i wn ? < off hn ( nurl_tcp_write2 fd # *u + # i hp off - hn off bp bn ) ( nurl_tcp_write fd # s + # i bp - off hn - n off )\n        ? <= wn 0 {\n            : ~ b retry F\n            ? & on_fiber == ( nurl_tcp_err_kind fd ) 7 { = retry ( __tls_io_wait fd 1 ) } {}\n            ? retry {} { ^ F }\n        } { = off + off wn }\n    }\n    ^ T\n}\n\n& `c` @ nurl_ktls_supported → i\n\n& `c` @ nurl_ktls_set i conn i dir i cipher *u key *u iv i seq → i\n\n& `c` @ nurl_ktls_send i conn i rtype *u buf i n → i\n\n& `c` @ nurl_ktls_recv i conn *u buf i n i nowait → i\n\n& `c` @ nurl_ktls_rtype i conn → i\n\nunsafe & `c` @ nurl_tcp_write2 i conn *u b1 i n1 *u b2 i n2 → i\n\n: | TlsErr {\n    TlsConnect\n    TlsHandshake\n    TlsDecrypt\n    TlsRead\n    TlsWrite\n    TlsClosed\n    TlsAlert\n    TlsProtocol\n    TlsBadCipher\n    TlsHRR\n    TlsBadCert\n}\n\n@ tls_err_name TlsErr e → s {\n    ^ ?? e {\n        TlsConnect → `TlsConnect`\n        TlsHandshake → `TlsHandshake`\n        TlsDecrypt → `TlsDecrypt`\n        TlsRead → `TlsRead`\n        TlsWrite → `TlsWrite`\n        TlsClosed → `TlsClosed`\n        TlsAlert → `TlsAlert`\n        TlsProtocol → `TlsProtocol`\n        TlsBadCipher → `TlsBadCipher`\n        TlsHRR → `TlsHRR`\n        TlsBadCert → `TlsBadCert`\n    }\n}\n\n// Live connection state. Vec fields are reassigned as keys rotate\n// (handshake → application) and as buffers are consumed.\n: TlsConnImpl {\n    i fd\n    i owns_fd  // 1 until tls_close closes the socket\n    i read_nowait  // one try-read call must not park on partial records\n    ( Vec u ) rxbuf  // raw socket bytes not yet split into records\n    ( Vec u ) hsbuf  // decrypted handshake bytes not yet a full message\n    ( Vec u ) appbuf  // decrypted application bytes for the caller\n    ( Vec u ) s_key\n    ( Vec u ) s_iv\n    ( Vec u ) c_key\n    ( Vec u ) c_iv\n    // The AES-GCM keys of s_key / c_key, prepared once per traffic secret\n    // (round keys, GHASH powers) — null unless the suite is AES-GCM.\n    AesGcmKey s_gk\n    AesGcmKey c_gk\n    // Outgoing records are built and sealed in place here, one write's\n    // worth at a time; it keeps its capacity across writes.\n    ( Vec u ) txbuf\n    // kTLS (opt-in, Linux): where each key direction's records are\n    // protected — 0 here, 1 by the kernel as TX, 2 by the kernel as RX —\n    // for the server's write keys (s_*) and the client's (c_*).\n    i ktls_s\n    i ktls_c\n    i ktls_want  // 1 once a handover was asked for: a read side that\n    // could not go yet (rxbuf held a record) goes when rxbuf drains\n    i server  // 1 on the accepting side\n    ( Vec u ) s_secret  // retained TLS 1.3 traffic secrets for KeyUpdate\n    ( Vec u ) c_secret\n    i update_pending  // peer requested our next write-key generation\n    i fatal_alert  // queued protocol failure, emitted before closing\n    i s_seq\n    i c_seq\n    i enc_read  // 1 once server records are encrypted\n    i established\n    i closed\n    ( Vec u ) cert_msg  // raw Certificate handshake message (full chain)\n    ( Vec u ) cv_sig  // CertificateVerify signature\n    ( Vec u ) th_cert  // transcript hash through Certificate (for CertVerify)\n    i cv_scheme  // CertificateVerify SignatureScheme\n    i cipher  // 0 = ChaCha20-Poly1305, 1 = AES-128-GCM\n    i version  // 13 = TLS 1.3, 12 = TLS 1.2\n    ( Vec u ) kx_p256  // P-256 ephemeral private key (empty if X25519 chosen)\n    ( Vec u ) kx_mlkem  // ML-KEM-768 decapsulation key (empty unless the\n    // hybrid group is chosen)\n    i kx_group  // negotiated group: 4588 X25519MLKEM768, 29 x25519,\n    // 23 secp256r1, 0 before the handshake reaches it\n    ( Vec u ) alpn_sel  // ALPN protocol the server selected (empty if none)\n    // ── session resumption (RFC 8446 §4.6.1 / §4.2.11) ──\n    i resumed  // 1 when this connection came up from a PSK ticket\n    ( Vec u ) res_master  // resumption_master_secret, set when the handshake\n    // completes; the PSK of every ticket on this connection derives from it\n    ( Vec u ) res_early  // client scratch: early_secret(PSK) while offering\n    ( Vec u ) tk_ticket  // newest ticket (to offer next time / being offered)\n    ( Vec u ) tk_psk  // its PSK\n    i tk_age_add  // its ticket_age_add\n    i tk_lifetime  // its ticket_lifetime, seconds\n    i tk_received_ms  // wall clock (ms) when it arrived\n    i hs_deadline_ns  // absolute monotonic ns bounding the handshake's\n    // reads and writes (tls_attach_full_until); 0 = none\n}\n\n// The socket is the one raw part: a connection nobody tls_close'd is\n// closed by its last owner (without a close_notify — that alert is\n// tls_close's, said at a point of the caller's choosing).\n% Drop TlsConnImpl {\n    @ drop TlsConnImpl c → v {\n        ? != . c owns_fd 0 { ( nurl_tcp_close . c fd ) } {}\n    }\n}\n\n// A TlsConn is a handle on its state in an rcbox (stdlib/core/rcbox.nu):\n// every copy is the same connection, and the last owner releases it.\n: TlsConn { ( Shared TlsConnImpl ) ctl }\n\n// Its drop closes something the outside world sees (stdlib/core/marker.nu).\n% Resource TlsConn {}\n\n@ TlsConn_share TlsConn h → TlsConn { ^ @ TlsConn { ( shared_clone [TlsConnImpl] . h ctl ) } }\n\n@ TlsConn_drop sink TlsConn h → v {}\n\n@ __TlsConn_ptr TlsConn h → *TlsConnImpl { ^ ( shared_ptr [TlsConnImpl] . h ctl ) }\n\n// The state in place, for the stdlib's own transport layer (std/net.nu).\n@ _tls_ptr TlsConn h → *TlsConnImpl { ^ ( shared_ptr [TlsConnImpl] . h ctl ) }\n\n// The connection as a word, for a holder that is not a handle itself\n// (std/net.nu's TcpConn keeps one): one more owner, which\n// `_tls_word_release` gives back.\n@ _tls_word TlsConn h → i { ^ ( shared_into_word [TlsConnImpl] ( shared_clone [TlsConnImpl] . h ctl ) ) }\n\n@ _tls_word_release i w → v { : ( Shared TlsConnImpl ) _back ( shared_from_word [TlsConnImpl] w ) }\n\n// A connection over socket `raw`. The connection owns the socket from\n// here: tls_close closes it, or else the last owner does. A `raw` of 0 is\n// no socket (a connection state built for a test).\n@ _tls_conn_new i raw → TlsConn {\n    : ( Shared TlsConnImpl ) c__box ( shared_zero [TlsConnImpl] )\n    : *TlsConnImpl c ( shared_ptr [TlsConnImpl] c__box )\n    = . c fd raw\n    = . c read_nowait 0\n    = . c s_secret ( vec_new [u] )\n    = . c c_secret ( vec_new [u] )\n    = . c update_pending 0\n    = . c fatal_alert 0\n    = . c rxbuf ( vec_new [u] )\n    = . c hsbuf ( vec_new [u] )\n    = . c appbuf ( vec_new [u] )\n    = . c s_key ( vec_new [u] )\n    = . c s_iv ( vec_new [u] )\n    = . c c_key ( vec_new [u] )\n    = . c c_iv ( vec_new [u] )\n    = . c txbuf ( vec_new [u] )\n    = . c s_seq 0\n    = . c c_seq 0\n    = . c enc_read 0\n    = . c established 0\n    = . c closed 0\n    = . c cert_msg ( vec_new [u] )\n    = . c cv_sig ( vec_new [u] )\n    = . c th_cert ( vec_new [u] )\n    = . c cv_scheme 0\n    = . c cipher 0\n    = . c version 13\n    = . c kx_p256 ( vec_new [u] )\n    = . c kx_mlkem ( vec_new [u] )\n    = . c kx_group 0\n    = . c alpn_sel ( vec_new [u] )\n    = . c resumed 0\n    = . c res_master ( vec_new [u] )\n    = . c res_early ( vec_new [u] )\n    = . c tk_ticket ( vec_new [u] )\n    = . c tk_psk ( vec_new [u] )\n    = . c tk_age_add 0\n    = . c tk_lifetime 0\n    = . c tk_received_ms 0\n    = . c owns_fd ? > raw 0 1 0\n    ^ @ TlsConn { c__box }\n}\n\n// ── small helpers ─────────────────────────────────────────────────\n@ _t_bget ( Vec u ) v i k → i {\n    ?? ( vec_get [u] v k ) { T x → ^ # i x F _ → ^ 0 }\n}\n\n@ _tls_u16 ( Vec u ) v i n → v {\n    ( vec_push [u] v # u & >> n 8 255 )\n    ( vec_push [u] v # u & n 255 )\n}\n\n@ _tls_u32 ( Vec u ) v i n → v {\n    ( vec_push [u] v # u & >> n 24 255 )\n    ( vec_push [u] v # u & >> n 16 255 )\n    ( vec_push [u] v # u & >> n 8 255 )\n    ( vec_push [u] v # u & n 255 )\n}\n\n@ _tls_u64 ( Vec u ) v i n → v {\n    ( _tls_u32 v & >> n 32 4294967295 )\n    ( _tls_u32 v & n 4294967295 )\n}\n\n@ _u24 ( Vec u ) v i n → v {\n    ( vec_push [u] v # u & >> n 16 255 )\n    ( vec_push [u] v # u & >> n 8 255 )\n    ( vec_push [u] v # u & n 255 )\n}\n\n// Bulk append — memcpy via bytes_extend_bytes rather than a per-byte\n// push loop; this runs over every received record (socket → rxbuf,\n// plaintext → appbuf) on the download hot path.\n@ _tls_cat ( Vec u ) dst ( Vec u ) src → v {\n    ( bytes_extend_bytes dst src )\n}\n\n// Append a 2-byte length prefix + the block bytes.\n@ _blk16 ( Vec u ) dst ( Vec u ) sub → v {\n    ( _tls_u16 dst ( vec_len [u] sub ) )\n    ( _tls_cat dst sub )\n}\n\n// Read a big-endian integer of `n` bytes from `v` at `off`.\n@ _rdint ( Vec u ) v i off i n → i {\n    : ~ i acc 0\n    : ~ i k 0\n    ~ < k n { = acc | << acc 8 ( _t_bget v + off k ) = k + k 1 }\n    ^ acc\n}\n\n@ _rand_bytes i n → ( Vec u ) {\n    : ( Vec u ) v ( vec_with_cap [u] ? > n 0 n 1 )\n    : ~ i k 0\n    ~ < k n { ( vec_push [u] v # u 0 ) = k + k 1 }\n    : i r ( nurl_rand_fill # *u ( vec_data [u] v ) n )\n    // L4: never proceed with non-CSPRNG bytes. nurl_rand_fill returns 0 only on\n    // total entropy failure; these bytes seed ephemeral keys and nonces, so\n    // fail closed rather than emit predictable key material.\n    ? & > n 0 == r 0 { ( nurl_panic `tls: CSPRNG (nurl_rand_fill) failed` ) } {}\n    ^ v\n}\n\n// Constant-time all-zero test (OR-accumulate every byte; no early exit). An\n// empty vector counts as zero. Used to reject a degenerate ECDHE secret.\n@ _all_zero ( Vec u ) v → b {\n    : i n ( vec_len [u] v )\n    ? == n 0 { ^ T } {}\n    : ~ i acc 0\n    : ~ i k 0\n    ~ < k n { = acc | acc ( _t_bget v k ) = k + k 1 }\n    ^ == acc 0\n}\n\n// X25519MLKEM768 (RFC 9370 group 0x11ec): turn the server's 1120-byte\n// key_share into the 64-byte secret the key schedule consumes.\n//\n// The server share is `ML-KEM-768 ciphertext (1088) ‖ X25519 public key\n// (32)`, and the result is `ML-KEM shared secret ‖ X25519 shared secret`\n// in the same order.\n//\n// Decapsulation cannot report failure — that is the point of ML-KEM's\n// implicit rejection, which returns an unpredictable key rather than an\n// error so an attacker learns nothing from probing. A wrong ciphertext\n// therefore surfaces here as a handshake that fails at Finished, which\n// is exactly the intended behaviour.\n//\n// The X25519 half still gets RFC 8446 §7.4.2's all-zero check on its\n// own. Checking only the concatenation would not do: a low-order peer\n// point makes the X25519 half all-zero while the ML-KEM half stays\n// random, so the pair looks fine and the classical half is silently\n// worthless. Returning an empty vector here makes the caller's\n// `_all_zero` test fail closed.\n@ __hybrid_shared ( Vec u ) dk ( Vec u ) priv ( Vec u ) spub → ( Vec u ) {\n    : ( Vec u ) ct ( bytes_slice spub 0 1088 )\n    : ( Vec u ) xpub ( bytes_slice spub 1088 1120 )\n    : ( Vec u ) xs ( x25519 priv xpub )\n    ? ( _all_zero xs ) {\n        ^ ( vec_new [u] )\n    } {}\n    : ( Vec u ) out ( mlkem_decaps 768 dk ct )\n    ( bytes_extend_bytes out xs )\n    ^ out\n}\n\n// RFC 8446 §4.1.3 downgrade sentinel: a TLS 1.3-capable client that ends up\n// on TLS 1.2 must abort if the last 8 bytes of the 32-byte server random are\n// \"DOWNGRD\" + 0x01 (1.2) or + 0x00 (1.1/below) — the server is signalling a\n// forced downgrade by an active attacker.\n@ __downgrade_sentinel ( Vec u ) srand → b {\n    ? < ( vec_len [u] srand ) 32 { ^ F } {}\n    : ~ b m T\n    ? != ( _t_bget srand 24 ) 68 { = m F } {}  // 'D'\n    ? != ( _t_bget srand 25 ) 79 { = m F } {}  // 'O'\n    ? != ( _t_bget srand 26 ) 87 { = m F } {}  // 'W'\n    ? != ( _t_bget srand 27 ) 78 { = m F } {}  // 'N'\n    ? != ( _t_bget srand 28 ) 71 { = m F } {}  // 'G'\n    ? != ( _t_bget srand 29 ) 82 { = m F } {}  // 'R'\n    ? != ( _t_bget srand 30 ) 68 { = m F } {}  // 'D'\n    : i last ( _t_bget srand 31 )\n    ? & != last 0 != last 1 { = m F } {}\n    ^ m\n}\n\n// ── socket record I/O ─────────────────────────────────────────────\n// Ensure rxbuf holds at least `n` bytes, reading from the socket.\n//\n// Context-aware: on a fiber the socket is non-blocking and an EAGAIN\n// parks on the reactor until readable — the worker pthread stays free,\n// so a fiber HTTP-over-TLS server multiplexes its connections instead\n// of pinning one worker per idle keep-alive conn. Off a fiber the raw\n// blocking read is what a synchronous client wants (SO_RCVTIMEO still\n// bounds it; the reactor deadline mirrors that via __tls_io_wait).\n@ __fill inout TlsConnImpl c i n → !i TlsErr {\n    : i raw . c fd\n    : b on_fiber != ( nurl_fiber_current ) 0\n    // A handshake under a deadline: every read gets what is left of it\n    // as its timeout — SO_RCVTIMEO on a thread, the reactor deadline on\n    // a fiber (both read nurl_tcp_set_timeout) — so the handshake as a\n    // whole, not each read, is bounded.\n    // Rounded UP, plus the 1 ms the reactor's millisecond clock can\n    // fire early by: a read that times out has really reached the\n    // deadline, which is how the caller tells a timeout from a failure.\n    ? > . c hs_deadline_ns 0 {\n        : i left_ns - . c hs_deadline_ns ( nurl_monotonic_ns )\n        ? <= left_ns 0 { ^ @ !i TlsErr { F # TlsErr TlsRead } } {}\n        ( nurl_tcp_set_timeout raw + / + left_ns 999999 1000000 1 )\n    } {}\n    ? & on_fiber == . c read_nowait 0 { ( nurl_tcp_set_nonblock raw 1 ) } {}\n    ~ < ( vec_len [u] . c rxbuf ) n {\n        // Read straight into rxbuf's spare capacity — the previous\n        // per-fill 16 KB scratch Vec + copy-append + free was pure\n        // overhead on the record hot path (once per record read, i.e.\n        // once per keep-alive HTTPS request). Capacity settles at\n        // ~len+16 K and is reused for the connection's lifetime.\n        ( vec_reserve [u] . c rxbuf 16384 )\n        : i len ( vec_len [u] . c rxbuf )\n        : *u p ( vec_data [u] . c rxbuf )\n        : s pbuf # s + # i p len\n        : ~ i got ? != . c read_nowait 0 ( nurl_tcp_read_nowait raw pbuf 16384 ) ( nurl_tcp_read raw pbuf 16384 )\n        : ~ b timed_out F\n        : ~ i at len\n        ~ & == . c read_nowait 0 & ! timed_out & on_fiber & < got 0 == ( nurl_tcp_err_kind raw ) 7 {\n            ? ( __tls_io_wait raw 0 ) {\n                // Parked: another fiber holding this connection may have\n                // read into rxbuf meanwhile and moved it, so the place to\n                // read into is taken again, not the one from before.\n                ( vec_reserve [u] . c rxbuf 16384 )\n                = at ( vec_len [u] . c rxbuf )\n                = got ( nurl_tcp_read raw # s + # i ( vec_data [u] . c rxbuf ) at 16384 )\n            } { = timed_out T }\n        }\n        ? < got 0 { ^ @ !i TlsErr { F # TlsErr TlsRead } } {}\n        ? == got 0 { ^ @ !i TlsErr { F # TlsErr TlsClosed } } {}\n        : b _ok ( vec_set_len [u] . c rxbuf + at got )\n    }\n    ^ @ !i TlsErr { T 1 }\n}\n\n// Drop the first `n` bytes of rxbuf (consume them). In place: shift the\n// tail down and shrink len — the old slice-copy allocated (and freed) a\n// fresh Vec per consumed record. The tail is empty in the common case\n// (one record per read), so the memmove is usually zero bytes.\n@ __consume inout TlsConnImpl c i n → v {\n    : ( Vec u ) buf . c rxbuf\n    : i total ( vec_len [u] buf )\n    ? >= n total { ( vec_clear [u] buf ) ^ v } {}\n    : i remaining - total n\n    : *u p ( vec_data [u] buf )\n    ( nurl_memmove # s p # s # *u + # i p n remaining )\n    : b _ok ( vec_set_len [u] buf remaining )\n}\n\n// Record = type(1) ver(2) length(2) body. Returns (type, body); body is\n// an owned slice.\n: TlsRecord { i rtype ( Vec u ) body }\n\n@ _read_record inout TlsConnImpl c → !TlsRecord TlsErr {\n    : !i TlsErr h ( __fill c 5 )\n    ?? h { T _ → {} F e → { ^ @ !TlsRecord TlsErr { F e } } }\n    : i rtype ( _t_bget . c rxbuf 0 )\n    : i len ( _rdint . c rxbuf 3 2 )\n    : !i TlsErr b ( __fill c + 5 len )\n    ?? b { T _ → {} F e → { ^ @ !TlsRecord TlsErr { F e } } }\n    : ( Vec u ) body ( bytes_slice . c rxbuf 5 + 5 len )\n    ( __consume c + 5 len )\n    ^ @ !TlsRecord TlsErr { T @ TlsRecord { rtype body } }\n}\n\n// Build the per-record nonce: static IV with the 64-bit sequence number\n// XORed into the low 8 bytes.\n@ _nonce ( Vec u ) iv i seq → ( Vec u ) {\n    : ( Vec u ) n ( vec_with_cap [u] 12 )\n    : ~ i k 0\n    ~ < k 12 { ( vec_push [u] n # u ( _t_bget iv k ) ) = k + k 1 }\n    : ~ i b 0\n    ~ < b 8 {\n        : i sb & >> seq * 8 - 7 b 255\n        ( vec_set [u] n + 4 b # u ^^ ( _t_bget n + 4 b ) sb )\n        = b + b 1\n    }\n    ^ n\n}\n\n// AEAD-open one record body (ct‖tag) — already a copy, on the\n// handshake's path — under the keys the peer writes with (`peer` 0: the\n// server's, a client connection's read side; 1: the client's) → the\n// inner plaintext. The application-data path opens in place instead\n// (__open_front).\n@ _tls_open_body inout TlsConnImpl c i peer ( Vec u ) body → ?( Vec u ) {\n    : ( Vec u ) aad ( vec_with_cap [u] 5 )\n    ( vec_push [u] aad # u 23 )\n    ( vec_push [u] aad # u 3 )\n    ( vec_push [u] aad # u 3 )\n    ( _tls_u16 aad ( vec_len [u] body ) )\n    ? == peer 0 {\n        : ( Vec u ) nonce ( _nonce . c s_iv . c s_seq )\n        = . c s_seq + . c s_seq 1\n        ? == . c cipher 1 { ^ ( aes_gcm_open . c s_gk nonce aad body ) } {}\n        ^ ( aead_decrypt . c s_key nonce aad body )\n    } {}\n    : ( Vec u ) nonce ( _nonce . c c_iv . c c_seq )\n    = . c c_seq + . c c_seq 1\n    ? == . c cipher 1 { ^ ( aes_gcm_open . c c_gk nonce aad body ) } {}\n    ^ ( aead_decrypt . c c_key nonce aad body )\n}\n\n// AEAD-decrypt one record body under the server's keys → inner plaintext.\n@ __decrypt_record inout TlsConnImpl c ( Vec u ) body → ?( Vec u ) {\n    ^ ( _tls_open_body c 0 body )\n}\n\n// The next whole record in rxbuf, left at its front: Ok(its length on\n// the wire, header included). Nothing is copied out of it.\n@ __rec_front inout TlsConnImpl c → !i TlsErr {\n    : !i TlsErr h ( __fill c 5 )\n    ?? h { T _ → {} F e → { ^ @ !i TlsErr { F e } } }\n    : i len ( _rdint . c rxbuf 3 2 )\n    : !i TlsErr b ( __fill c + 5 len )\n    ?? b { T _ → {} F e → { ^ @ !i TlsErr { F e } } }\n    ^ @ !i TlsErr { T + 5 len }\n}\n\n// Open the TLS 1.3 record at the front of rxbuf (`rlen` bytes) in place,\n// under the keys `peer` writes with: its inner plaintext is then\n// rxbuf[5, 5 + plen), padding and type byte stripped (RFC 8446 §5.4).\n// Returns plen · 256 + the content type — type 0 for a record that is\n// all padding — or -1 for one that does not authenticate.\n@ __open_front inout TlsConnImpl c i peer i rlen → i {\n    : ~ b ok F\n    ? == peer 0 {\n        = ok ? == . c cipher 1 ( aes_gcm_open_in . c s_gk . c s_iv . c s_seq . c rxbuf 0 5 rlen ) ( chacha20poly1305_open_in . c s_key . c s_iv . c s_seq . c rxbuf 0 5 rlen )\n        = . c s_seq + . c s_seq 1\n    } {\n        = ok ? == . c cipher 1 ( aes_gcm_open_in . c c_gk . c c_iv . c c_seq . c rxbuf 0 5 rlen ) ( chacha20poly1305_open_in . c c_key . c c_iv . c c_seq . c rxbuf 0 5 rlen )\n        = . c c_seq + . c c_seq 1\n    }\n    ? ! ok { ^ -1 } {}\n    : *u p ( vec_data [u] . c rxbuf )\n    : ~ i k - rlen 17\n    ~ & >= k 5 == # i . p k 0 { = k - k 1 }\n    ? < k 5 { ^ 0 } {}\n    ^ + * - k 5 256 # i . p k\n}\n\n// `n` plaintext bytes at rxbuf[5 ..]: up to `room` of them appended to\n// `dst`, the rest to appbuf. Returns how many went to `dst`.\n@ __deliver inout TlsConnImpl c ( Vec u ) dst i n i room → i {\n    : i take ? < n room n room\n    : *u p ( vec_data [u] . c rxbuf )\n    ( bytes_extend_raw dst # s + # i p 5 take )\n    ? > n take { ( bytes_extend_raw . c appbuf # s + # i p + 5 take - n take ) } {}\n    ^ take\n}\n\n// Up to `max` decrypted application bytes appended to `dst`: Ok(how\n// many), 0 on clean EOF (close_notify). `peer` is who writes the records\n// read here (0 the server: a client connection; 1 the client). Records\n// are opened in place in rxbuf and the plaintext copied once, into\n// `dst`; only what does not fit waits in appbuf. Post-handshake messages\n// (tickets, key updates) are consumed transparently.\n@ _tls_read_into_in inout TlsConnImpl c i peer ( Vec u ) dst i max → !i TlsErr {\n    ? <= max 0 { ^ @ !i TlsErr { T 0 } } {}\n    : i have ( vec_len [u] . c appbuf )\n    ? > have 0 {\n        : i take ? < have max have max\n        : *u ap ( vec_data [u] . c appbuf )\n        ( bytes_extend_raw dst # s ap take )\n        ( nurl_memmove # s ap # s + # i ap take - have take )\n        : b _al ( vec_set_len [u] . c appbuf - have take )\n        ^ @ !i TlsErr { T take }\n    } {}\n    ? != 0 ( _tls_ktls_of c peer ) { ^ ( _tls_ktls_read_into c peer dst max ) } {}\n    ~ == . c closed 0 {\n        ? != . c fatal_alert 0 { ^ @ !i TlsErr { F TlsProtocol } } {}\n        ? != . c update_pending 0 {\n            ? != . c read_nowait 0 { ^ @ !i TlsErr { F TlsRead } } {}\n            ?? ( _tls_flush_control c - 1 peer ) { T _ → {} F error → { ^ @ !i TlsErr { F error } } }\n        } {}\n        : !i TlsErr fr ( __rec_front c )\n        ?? fr {\n            F e → {\n                ?? e {\n                    TlsClosed → { = . c closed 1 ^ @ !i TlsErr { T 0 } }\n                    _ → { ^ @ !i TlsErr { F e } }\n                }\n            }\n            T rlen → {\n                : i rtype ( _t_bget . c rxbuf 0 )\n                ? == rtype 20 { ( __consume c rlen ) } {\n                    ? == . c version 12 {\n                        // TLS 1.2: the record type is the real content\n                        // type, and the explicit nonce rides in the body.\n                        : ( Vec u ) body ( bytes_slice . c rxbuf 5 rlen )\n                        ( __consume c rlen )\n                        ?? ( __decrypt_record_12 c rtype body ) {\n                            T inner → {\n                                ? == rtype 23 {\n                                    : i n ( vec_len [u] inner )\n                                    : i take ? < n max n max\n                                    ( bytes_extend_raw dst # s ( vec_data [u] inner ) take )\n                                    ? > n take { ( bytes_extend_raw . c appbuf # s + # i ( vec_data [u] inner ) take - n take ) } {}\n                                    ? > take 0 { ^ @ !i TlsErr { T take } } {}\n                                } {\n                                    // 21 alert: closed; 22 (post-handshake, e.g. tickets): ignored\n                                    ? == rtype 21 { = . c closed 1 } {}\n                                }\n                            }\n                            F _ → { ^ @ !i TlsErr { F # TlsErr TlsDecrypt } }\n                        }\n                    } {\n                        : i r ( __open_front c peer rlen )\n                        ? < r 0 {\n                            ( __consume c rlen )\n                            ^ @ !i TlsErr { F # TlsErr TlsDecrypt }\n                        } {}\n                        : i ct & r 255\n                        : i plen >> r 8\n                        ? == ct 23 {\n                            ? != ( vec_len [u] . c hsbuf ) 0 {\n                                ( __consume c rlen )\n                                : !v TlsErr failed ( _tls_post_fail c peer 10 )\n                                ?? failed { T _ → {} F _ → {} }\n                                ^ @ !i TlsErr { F TlsProtocol }\n                            } {}\n                            : i got ( __deliver c dst plen max )\n                            ( __consume c rlen )\n                            ? & != . c ktls_want 0 == ( vec_len [u] . c rxbuf ) 0 { : i _m ( _tls_ktls_in c ) } {}\n                            ? > got 0 { ^ @ !i TlsErr { T got } } {}\n                        } {\n                            : ( Vec u ) inner ( bytes_slice . c rxbuf 5 + 5 plen )\n                            ( __consume c rlen )\n                            ? == ct 21 { = . c closed 1 } {}\n                            ? == ct 22 {\n                                ?? ( _tls_post_hs c inner peer ) {\n                                    T _ → {}\n                                    F error → { ^ @ !i TlsErr { F error } }\n                                }\n                            } {}\n                        }\n                    }\n                }\n            }\n        }\n    }\n    ^ @ !i TlsErr { T 0 }\n}\n\n// Up to `max` decrypted application bytes appended to `dst`: Ok(n), 0 on\n// clean EOF — the zero-copy form of tls_read: the plaintext is copied\n// once, from the record buffer into `dst`.\n@ tls_read_into TlsConn c__h ( Vec u ) dst i max → !i TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_read_into_in . c 0 0 dst max )\n}\n\n// Strip TLS 1.3 inner padding: trailing zeros then the real content type.\n// Returns the content type; truncates `inner` to the real content length.\n@ _inner_type ( Vec u ) inner → i {\n    : ~ i i - ( vec_len [u] inner ) 1\n    ~ & >= i 0 == ( _t_bget inner i ) 0 { = i - i 1 }\n    ? < i 0 { ^ 0 } {}\n    : i ct ( _t_bget inner i )\n    : b _ok ( vec_set_len [u] inner i )\n    ^ ct\n}\n\n// Encrypt + send one record of `content` under the client keys.\n@ __send_encrypted inout TlsConnImpl c i content_type ( Vec u ) content → !v TlsErr {\n    : ( Vec u ) buf ( _tls_tx_take c )\n    ( _tls_rec_range_to c buf 1 content_type content 0 ( vec_len [u] content ) )\n    : !v TlsErr r ( _tls_tx_flush c buf )\n    ( _tls_tx_put c buf )\n    ^ r\n}\n\n@ _tls_seal_direction_to inout TlsConnImpl c ( Vec u ) out i dir i content_type ( Vec u ) inner → v {\n    ? != 0 ( _tls_ktls_of c dir ) {\n        ( _tls_rec_range_to c out dir content_type inner 0 ( vec_len [u] inner ) )\n        ^ v\n    } {}\n    : i at ( _tls_rec_open out ( vec_len [u] inner ) )\n    ( _tls_cat out inner )\n    ( _tls_rec_close c out dir at content_type )\n}\n\n// ── records built in place ─────────────────────────────────────────\n// A TLS 1.3 record is sealed where it is written: the header, then the\n// plaintext appended straight from wherever it lies, then the content\n// type byte, then the AEAD runs over that range of `out` and appends the\n// tag. No inner-plaintext Vec, no sealed copy, no nonce or AAD Vec — the\n// nonce is the direction's iv and sequence number, the AAD the header\n// itself (RFC 8446 §5.2) — and the AES-GCM key is the connection's\n// prepared one, not a key schedule per record.\n\n// Room past a record for the AEAD's scratch (aes_gcm.nu's __gcm_scratch,\n// chacha20poly1305.nu's __ccp_scratch) and its 16-byte alignment.\n@ _tls_rec_slack → i { ^ 400 }\n\n// Start a record at the end of `out` — its header, the length still 0 —\n// with room reserved for `n` plaintext bytes, the type byte, the tag and\n// the sealer's scratch: one growth at most. Returns where it starts.\n@ _tls_rec_open ( Vec u ) out i n → i {\n    : i at ( vec_len [u] out )\n    ( vec_reserve [u] out + + n 22 ( _tls_rec_slack ) )\n    ( vec_push [u] out # u 23 )\n    ( vec_push [u] out # u 3 )\n    ( vec_push [u] out # u 3 )\n    ( vec_push [u] out # u 0 )\n    ( vec_push [u] out # u 0 )\n    ^ at\n}\n\n// Finish the record started at `at`: the content type byte, the header's\n// length, and the seal under direction `dir`'s keys (0 = server write,\n// 1 = client write), which appends the tag.\n@ _tls_rec_close inout TlsConnImpl c ( Vec u ) out i dir i at i content_type → v {\n    ( vec_push [u] out # u content_type )\n    : i total + - ( vec_len [u] out ) + at 5 16\n    ( vec_put [u] out + at 3 # u >> total 8 )\n    ( vec_put [u] out + at 4 # u & total 255 )\n    ? == dir 0 {\n        : b _s ? == . c cipher 1 ( aes_gcm_seal_in . c s_gk . c s_iv . c s_seq out at + at 5 ) ( chacha20poly1305_seal_in . c s_key . c s_iv . c s_seq out at + at 5 )\n        = . c s_seq + . c s_seq 1\n    } {\n        : b _s ? == . c cipher 1 ( aes_gcm_seal_in . c c_gk . c c_iv . c c_seq out at + at 5 ) ( chacha20poly1305_seal_in . c c_key . c c_iv . c c_seq out at + at 5 )\n        = . c c_seq + . c c_seq 1\n    }\n}\n\n// Bytes [lo, hi) of the logical concatenation `head`‖`body` appended to\n// `out` — a record's plaintext cut from two buffers without joining them.\n@ _tls_pair_into ( Vec u ) out ( Vec u ) head ( Vec u ) body i lo i hi → v {\n    : i hn ( vec_len [u] head )\n    : i bn ( vec_len [u] body )\n    : ~ i a lo\n    : ~ i z hi\n    ? < a 0 { = a 0 } {}\n    ? > z + hn bn { = z + hn bn } {}\n    ? < z a { = z a } {}\n    ? < a hn {\n        : i h_hi ? < z hn z hn\n        ( bytes_extend_raw out # s + # i ( vec_data [u] head ) a - h_hi a )\n    } {}\n    ? > z hn {\n        : i b_lo ? > a hn - a hn 0\n        ( bytes_extend_raw out # s + # i ( vec_data [u] body ) b_lo - - z hn b_lo )\n    } {}\n}\n\n// One record of `data[lo, hi)` (content type `ct`) appended to `out`\n// under direction `dir`'s keys. With that direction in the kernel the\n// plaintext of application data is appended instead (the kernel seals\n// it on the way out), and any other content type is sent at once as a\n// record of its own (_tls_ktls_send).\n@ _tls_rec_range_to inout TlsConnImpl c ( Vec u ) out i dir i ct ( Vec u ) data i lo i hi → v {\n    ? != 0 ( _tls_ktls_of c dir ) {\n        ? == ct 23 { ( bytes_extend_raw out # s + # i ( vec_data [u] data ) lo - hi lo ) } { : b _k ( _tls_ktls_send c ct # *u + # i ( vec_data [u] data ) lo - hi lo ) }\n        ^ v\n    } {}\n    : i at ( _tls_rec_open out - hi lo )\n    ( bytes_extend_raw out # s + # i ( vec_data [u] data ) lo - hi lo )\n    ( _tls_rec_close c out dir at ct )\n}\n\n// One record of `head`‖`body`[lo, hi) appended to `out`.\n@ _tls_rec_pair_to inout TlsConnImpl c ( Vec u ) out i dir i ct ( Vec u ) head ( Vec u ) body i lo i hi → v {\n    ? != 0 ( _tls_ktls_of c dir ) {\n        ? == ct 23 { ( _tls_pair_into out head body lo hi ) } {\n            : ( Vec u ) part ( vec_new [u] )\n            ( _tls_pair_into part head body lo hi )\n            : b _k ( _tls_ktls_send c ct ( vec_data [u] part ) ( vec_len [u] part ) )\n        }\n        ^ v\n    } {}\n    : i at ( _tls_rec_open out - hi lo )\n    ( _tls_pair_into out head body lo hi )\n    ( _tls_rec_close c out dir at ct )\n}\n\n// ── kTLS (opt-in, Linux 6.14+) ─────────────────────────────────────\n// After the handshake the connection can hand its record protection to\n// the kernel (runtime: nurl_ktls_*): application data is then plain\n// write / recv on the socket — the kernel seals and opens the records,\n// and sendfile produces records too — while alerts and post-handshake\n// messages travel as records of their own type. It pays for bulk and\n// sendfile traffic; for small API responses the userspace record layer\n// is as fast (docs/NETWORKING.md), hence opt-in: NURL_KTLS=1 in the\n// environment, tls_ktls_default T, or tls_ktls on one connection.\n\n// Is key direction `dir` (0 the server's write keys, 1 the client's)\n// protected by the kernel? 0, or 1 (as TX) / 2 (as RX).\n@ _tls_ktls_of inout TlsConnImpl c i dir → i { ^ ? == dir 0 . c ktls_s . c ktls_c }\n\n// One record of content type `ct` through kernel TX, parking a fiber\n// while the socket is full; a short send continues as further records of\n// the same type (handshake messages may span records; an alert is two\n// bytes). F — and the connection closed — on a send that fails.\nunsafe @ _tls_ktls_send inout TlsConnImpl c i ct * u p i n → b {\n    : b on_fiber != ( nurl_fiber_current ) 0\n    : ~ i off 0\n    ~ < off n {\n        : i wn ( nurl_ktls_send . c fd ct # *u + # i p off - n off )\n        ? <= wn 0 {\n            : ~ b retry F\n            ? & on_fiber == ( nurl_tcp_err_kind . c fd ) 7 { = retry ( __tls_io_wait . c fd 1 ) } {}\n            ? retry {} { = . c closed 1 ^ F }\n        } { = off + off wn }\n    }\n    ^ T\n}\n\n// Process-wide default: -1 not read yet, 0 off, 1 on.\n: ~ i g_tls_ktls -1\n\n// Hand every TLS 1.3 connection to the kernel after its handshake (where\n// the kernel can take it), or stop doing so. Overrides NURL_KTLS.\n@ tls_ktls_default b on → v { = g_tls_ktls ? on 1 0 }\n\n@ __tls_ktls_wanted → b {\n    ? < g_tls_ktls 0 {\n        : s v ( getenv `NURL_KTLS` )\n        = g_tls_ktls 0\n        // `&` evaluates both sides: the null check guards on its own.\n        ? != # i v 0 { ? != 0 ( nurl_str_eq v `1` ) { = g_tls_ktls 1 } {} } {}\n    } {}\n    ^ == g_tls_ktls 1\n}\n\n// Give the connection's record protection to the kernel, each direction\n// that can go: its write side always, its read side only while rxbuf\n// holds nothing undecrypted (bytes of a record already read out of the\n// socket cannot be handed back). Returns what the kernel now protects:\n// 1 the write side, 2 the read side, 3 both, 0 neither (no ULP, an older\n// kernel, TLS 1.2, a closed connection — the record layer here stays).\n@ _tls_ktls_in inout TlsConnImpl c → i {\n    ? | | != . c version 13 != . c established 1 != . c closed 0 { ^ 0 } {}\n    = . c ktls_want 1\n    : i wdir ? == . c server 1 0 1\n    : i rdir - 1 wdir\n    : ~ i mask 0\n    ? == 0 ( _tls_ktls_of c wdir ) {\n        : i rc ? == wdir 0 ( nurl_ktls_set . c fd 1 . c cipher ( vec_data [u] . c s_key ) ( vec_data [u] . c s_iv ) . c s_seq ) ( nurl_ktls_set . c fd 1 . c cipher ( vec_data [u] . c c_key ) ( vec_data [u] . c c_iv ) . c c_seq )\n        ? == rc 0 { ? == wdir 0 { = . c ktls_s 1 } { = . c ktls_c 1 } } {}\n    } {}\n    ? & == 0 ( _tls_ktls_of c rdir ) == ( vec_len [u] . c rxbuf ) 0 {\n        : i rc ? == rdir 0 ( nurl_ktls_set . c fd 2 . c cipher ( vec_data [u] . c s_key ) ( vec_data [u] . c s_iv ) . c s_seq ) ( nurl_ktls_set . c fd 2 . c cipher ( vec_data [u] . c c_key ) ( vec_data [u] . c c_iv ) . c c_seq )\n        ? == rc 0 { ? == rdir 0 { = . c ktls_s 2 } { = . c ktls_c 2 } } {}\n    } {}\n    ? != 0 ( _tls_ktls_of c wdir ) { = mask | mask 1 } {}\n    ? != 0 ( _tls_ktls_of c rdir ) { = mask | mask 2 } {}\n    ^ mask\n}\n\n// Send a KeyUpdate (RFC 8446 §4.6.3) and move this end's writes to the\n// next key generation; with `request_peer` the peer is asked to do the\n// same for its writes (it answers on its next write). Under kTLS the\n// message goes out as a handshake record through the kernel and the\n// kernel takes the new key. TLS 1.3 only.\n@ tls_key_update TlsConn c__h b request_peer → !v TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_key_update_in . c 0 request_peer )\n}\n\n@ _tls_key_update_in inout TlsConnImpl c b request_peer → !v TlsErr {\n    ? | | != . c version 13 != . c established 1 != . c closed 0 { ^ @ !v TlsErr { F TlsClosed } } {}\n    : i wdir ? == . c server 1 0 1\n    : ( Vec u ) msg ( vec_new [u] )\n    ( vec_push [u] msg # u 24 ) ( _u24 msg 1 )\n    ( vec_push [u] msg # u ? request_peer 1 0 )\n    : ( Vec u ) buf ( _tls_tx_take c )\n    ( _tls_seal_direction_to c buf wdir 22 msg )\n    : !v TlsErr r ( _tls_tx_flush c buf )\n    ( _tls_tx_put c buf )\n    ?? r { T _ → {} F e → { ^ @ !v TlsErr { F e } } }\n    ( _tls_rotate_keys c wdir )\n    ? != . c closed 0 { ^ @ !v TlsErr { F TlsClosed } } {}\n    ^ @ !v TlsErr { T 0 }\n}\n\n// Is this connection's write side sealed by the kernel — so that a\n// sendfile on its socket produces TLS records? Pending control records\n// (a KeyUpdate answer, an alert) go out first, since bytes written past\n// the record layer would otherwise overtake them. F for a connection\n// that seals its own records, or one that has failed.\n@ tls_ktls_tx_ready TlsConn c__h → b {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_ktls_tx_ready_in . c 0 )\n}\n\n@ _tls_ktls_tx_ready_in inout TlsConnImpl c → b {\n    : i wdir ? == . c server 1 0 1\n    ? | != 1 ( _tls_ktls_of c wdir ) != . c closed 0 { ^ F } {}\n    ?? ( _tls_flush_control c wdir ) { T _ → {} F _ → { ^ F } }\n    ^ == . c closed 0\n}\n\n// tls_ktls for one connection: 1 write side, 2 read side, 3 both, 0\n// neither — see _tls_ktls_in.\n@ tls_ktls TlsConn c__h → i {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_ktls_in . c 0 )\n}\n\n// The handshake's last step: the opt-in handover.\n@ _tls_ktls_auto inout TlsConnImpl c → v {\n    ? ( __tls_ktls_wanted ) { : i _m ( _tls_ktls_in c ) } {}\n}\n\n// _tls_read_into_in with the read side in the kernel: application data\n// straight from the socket into `dst`; an alert or a post-handshake\n// message arrives as a read of its own type and is handled as the\n// record layer handles it.\nunsafe @ _tls_ktls_read_into inout TlsConnImpl c i peer ( Vec u ) dst i max → !i TlsErr {\n    : i raw . c fd\n    : b on_fiber != ( nurl_fiber_current ) 0\n    ? & on_fiber == . c read_nowait 0 { ( nurl_tcp_set_nonblock raw 1 ) } {}\n    ~ == . c closed 0 {\n        ? != . c fatal_alert 0 { ^ @ !i TlsErr { F TlsProtocol } } {}\n        ? != . c update_pending 0 {\n            ? != . c read_nowait 0 { ^ @ !i TlsErr { F TlsRead } } {}\n            ?? ( _tls_flush_control c - 1 peer ) { T _ → {} F error → { ^ @ !i TlsErr { F error } } }\n        } {}\n        ( vec_reserve [u] dst max )\n        : i len ( vec_len [u] dst )\n        : i got ( nurl_ktls_recv raw # *u + # i ( vec_data [u] dst ) len max . c read_nowait )\n        ? > got 0 {\n            : i rt ( nurl_ktls_rtype raw )\n            ? == rt 23 {\n                : b _l ( vec_set_len [u] dst + len got )\n                ^ @ !i TlsErr { T got }\n            } {}\n            : ( Vec u ) inner ( vec_with_cap [u] got )\n            ( bytes_extend_raw inner # s + # i ( vec_data [u] dst ) len got )\n            ? == rt 21 { = . c closed 1 } {\n                ? == rt 22 {\n                    ?? ( _tls_post_hs c inner peer ) { T _ → {} F error → { ^ @ !i TlsErr { F error } } }\n                } {\n                    : !v TlsErr _f ( _tls_post_fail c peer 10 )\n                    ^ @ !i TlsErr { F TlsProtocol }\n                }\n            }\n        } {\n            ? == got 0 { = . c closed 1 ^ @ !i TlsErr { T 0 } } {}\n            ? | != . c read_nowait 0 | ! on_fiber != ( nurl_tcp_err_kind raw ) 7 { ^ @ !i TlsErr { F TlsRead } } {}\n            ? ! ( __tls_io_wait raw 0 ) { ^ @ !i TlsErr { F TlsRead } } {}\n        }\n    }\n    ^ @ !i TlsErr { T 0 }\n}\n\n// The connection's write buffer, TAKEN for one write — an empty one left\n// in its place — and put back after it (_tls_tx_put). A write may park\n// on the socket with a pointer into the buffer; a second writer on the\n// same connection (two fibers holding copies of it) then builds into a\n// buffer of its own instead of growing the one being written. Their\n// records would still interleave — one connection takes one writer at a\n// time — but no write reads memory another has moved. In steady state the\n// same buffer goes round and nothing is allocated.\n@ _tls_tx_take inout TlsConnImpl c → ( Vec u ) {\n    : ( Vec u ) buf ( mem_replace [( Vec u )] . c txbuf ( vec_new [u] ) )\n    ( vec_clear [u] buf )\n    ^ buf\n}\n\n@ _tls_tx_put inout TlsConnImpl c sink ( Vec u ) buf → v {\n    ( vec_clear [u] buf )\n    = . c txbuf buf\n}\n\n// Write `buf` to the socket and empty it; a failure closes the\n// connection.\n@ _tls_tx_flush inout TlsConnImpl c ( Vec u ) buf → !v TlsErr {\n    : b written ( _tls_sock_write . c fd buf )\n    ( vec_clear [u] buf )\n    ? ! written { = . c closed 1 } {}\n    ^ ? written @ !v TlsErr { T 0 } @ !v TlsErr { F TlsWrite }\n}\n\n// Write a plaintext record straight to the socket.\n@ _send_plain inout TlsConnImpl c i rtype ( Vec u ) body → !v TlsErr {\n    : ( Vec u ) rec ( vec_with_cap [u] + ( vec_len [u] body ) 5 )\n    ( vec_push [u] rec # u rtype )\n    // legacy_record_version 0x0303 (RFC 8446 §5.1: required for every\n    // record except the initial ClientHello, where 0x0303 is also valid).\n    ( vec_push [u] rec # u 3 )\n    ( vec_push [u] rec # u 3 )\n    ( _tls_u16 rec ( vec_len [u] body ) )\n    ( _tls_cat rec body )\n    : b w ( _tls_sock_write . c fd rec )\n    ^ ? w @ !v TlsErr { T 0 } @ !v TlsErr { F # TlsErr TlsWrite }\n}\n\n// ── handshake-message reader ──────────────────────────────────────\n// Pull the next complete handshake message (header + body) from hsbuf,\n// decrypting more records as needed. CCS records are skipped.\n@ __next_hs inout TlsConnImpl c → !( Vec u ) TlsErr {\n    : ~ i need 1\n    ~ == need 1 {\n        : i have ( vec_len [u] . c hsbuf )\n        ? >= have 4 {\n            : i mlen ( _rdint . c hsbuf 1 3 )\n            ? >= have + 4 mlen {\n                : ( Vec u ) msg ( bytes_slice . c hsbuf 0 + 4 mlen )\n                : ( Vec u ) rest ( bytes_slice . c hsbuf + 4 mlen have )\n                = . c hsbuf rest\n                ^ @ !( Vec u ) TlsErr { T msg }\n            } {}\n        } {}\n        // Need more bytes: read another record.\n        : !TlsRecord TlsErr rr ( _read_record c )\n        ?? rr {\n            F e → { ^ @ !( Vec u ) TlsErr { F e } }\n            T rec → {\n                ? == . rec rtype 20 {\n                    // change_cipher_spec — ignore.\n                } {\n                    ? == . rec rtype 23 {\n                        ?? ( __decrypt_record c . rec body ) {\n                            T inner → {\n                                : i ct ( _inner_type inner )\n                                ? == ct 22 {\n                                    ( _tls_cat . c hsbuf inner )\n                                } {\n                                    ? == ct 21 { ^ @ !( Vec u ) TlsErr { F # TlsErr TlsAlert } } {}\n                                    ^ @ !( Vec u ) TlsErr { F # TlsErr TlsProtocol }\n                                }\n                            }\n                            F _ → {\n                                ^ @ !( Vec u ) TlsErr { F # TlsErr TlsDecrypt }\n                            }\n                        }\n                    } {\n                        // plaintext handshake (ServerHello stage) or alert\n                        ? == . rec rtype 22 {\n                            ( _tls_cat . c hsbuf . rec body )\n                        } {\n                            ^ @ !( Vec u ) TlsErr { F # TlsErr TlsProtocol }\n                        }\n                    }\n                }\n            }\n        }\n    }\n    ^ @ !( Vec u ) TlsErr { F # TlsErr TlsProtocol }\n}\n\n// ── ClientHello ───────────────────────────────────────────────────\n@ __build_client_hello ( Vec u ) host ( Vec u ) pubkey ( Vec u ) p256pub ( Vec u ) pqpub ( Vec u ) random ( Vec u ) sessid ( Vec u ) alp_list ( Vec u ) ext_extra ( Vec u ) psk_id i obf_age → ( Vec u ) {\n    : ( Vec u ) body ( vec_new [u] )\n    ( _tls_u16 body 771 )  // legacy_version 0x0303\n    ( _tls_cat body random )  // 32-byte random\n    ( vec_push [u] body # u ( vec_len [u] sessid ) )  // legacy_session_id (empty for QUIC)\n    ( _tls_cat body sessid )\n    // cipher_suites: TLS_AES_128_GCM_SHA256 (0x1301) and\n    // TLS_CHACHA20_POLY1305_SHA256 (0x1303) — both use the SHA-256 key\n    // schedule, so either keeps the rest of the handshake unchanged —\n    // the faster one for THIS CPU first: AES-GCM where it has the\n    // hardware crypto tier — AES-NI and PCLMULQDQ, or AES and PMULL on\n    // AArch64 (nurl_cpu_has_aes; std/aes_gcm.nu's hardware path, ~3 GB/s\n    // over 16 KB records on a Haswell and ~9–12 on VAES, against\n    // ChaCha's ~1.1–1.4) — ChaCha where it does not (the bitsliced AES\n    // runs at ~113 MB/s). Servers\n    // honouring client preference (Cloudflare et al.) pick the first;\n    // AES-only peers get 0x1301 from the same list either way.\n    // 1.3 suites first, then the TLS 1.2 ECDHE suites in the same order.\n    : b hw_aes ( nurl_cpu_has_aes )\n    ( _tls_u16 body 12 )\n    ? hw_aes {\n        ( _tls_u16 body 4865 )  // 0x1301 TLS_AES_128_GCM_SHA256\n        ( _tls_u16 body 4867 )  // 0x1303 TLS_CHACHA20_POLY1305_SHA256\n        ( _tls_u16 body 49195 )  // 0xc02b ECDHE-ECDSA-AES128-GCM-SHA256\n        ( _tls_u16 body 49199 )  // 0xc02f ECDHE-RSA-AES128-GCM-SHA256\n        ( _tls_u16 body 52393 )  // 0xcca9 ECDHE-ECDSA-CHACHA20-POLY1305\n        ( _tls_u16 body 52392 )  // 0xcca8 ECDHE-RSA-CHACHA20-POLY1305\n    } {\n        ( _tls_u16 body 4867 )  // 0x1303 TLS_CHACHA20_POLY1305_SHA256\n        ( _tls_u16 body 4865 )  // 0x1301 TLS_AES_128_GCM_SHA256\n        ( _tls_u16 body 52393 )  // 0xcca9 ECDHE-ECDSA-CHACHA20-POLY1305\n        ( _tls_u16 body 52392 )  // 0xcca8 ECDHE-RSA-CHACHA20-POLY1305\n        ( _tls_u16 body 49195 )  // 0xc02b ECDHE-ECDSA-AES128-GCM-SHA256\n        ( _tls_u16 body 49199 )  // 0xc02f ECDHE-RSA-AES128-GCM-SHA256\n    }\n    // compression methods\n    ( vec_push [u] body # u 1 )\n    ( vec_push [u] body # u 0 )\n\n    // extensions\n    : ( Vec u ) ext ( vec_new [u] )\n\n    // server_name (0x0000)\n    : ( Vec u ) sni ( vec_new [u] )\n    : i hl ( vec_len [u] host )\n    ( _tls_u16 sni + hl 3 )  // ServerNameList length\n    ( vec_push [u] sni # u 0 )  // name_type host_name\n    ( _tls_u16 sni hl )\n    : ~ i k 0\n    ~ < k hl { ( vec_push [u] sni # u ( _t_bget host k ) ) = k + k 1 }\n    ( _tls_u16 ext 0 )\n    ( _blk16 ext sni )\n\n    // supported_groups (0x000a): X25519MLKEM768 (0x11ec) first, then\n    // x25519 (0x001d) and secp256r1 (0x0017).\n    //\n    // The hybrid group leads because it is the only one here that\n    // survives a quantum adversary, and because it is what current\n    // browsers put first — servers that know it will take it. The two\n    // classical groups stay for everything else; PostgreSQL/OpenSSL\n    // servers commonly default to P-256. Order is a preference, not a\n    // demand: the server picks, and we sent a key share for all three.\n    : ( Vec u ) grp ( vec_new [u] )\n    ( _tls_u16 grp 6 )\n    ( _tls_u16 grp 4588 )  // X25519MLKEM768 0x11ec\n    ( _tls_u16 grp 29 )  // x25519\n    ( _tls_u16 grp 23 )  // secp256r1\n    ( _tls_u16 ext 10 )\n    ( _blk16 ext grp )\n\n    // signature_algorithms (0x000d)\n    // ML-DSA leads: it is the only family here a quantum adversary\n    // cannot forge, and a server that has an ML-DSA certificate should\n    // use it. The classical schemes follow for everything else — which\n    // today is everything with a publicly-issued certificate, since no\n    // CA issues ML-DSA yet.\n    : ( Vec u ) sa ( vec_new [u] )\n    ( _tls_u16 sa 22 )  // list length (11 algs × 2)\n    ( _tls_u16 sa 2309 )  // mldsa65                0x0905\n    ( _tls_u16 sa 2310 )  // mldsa87                0x0906\n    ( _tls_u16 sa 2308 )  // mldsa44                0x0904\n    ( _tls_u16 sa 1027 )  // ecdsa_secp256r1_sha256 0x0403\n    ( _tls_u16 sa 2052 )  // rsa_pss_rsae_sha256    0x0804\n    ( _tls_u16 sa 1025 )  // rsa_pkcs1_sha256       0x0401\n    ( _tls_u16 sa 1283 )  // ecdsa_secp384r1_sha384 0x0503\n    ( _tls_u16 sa 2053 )  // rsa_pss_rsae_sha384    0x0805\n    ( _tls_u16 sa 2054 )  // rsa_pss_rsae_sha512    0x0806\n    ( _tls_u16 sa 2055 )  // ed25519                0x0807\n    ( _tls_u16 sa 1281 )  // rsa_pkcs1_sha384       0x0501\n    ( _tls_u16 ext 13 )\n    ( _blk16 ext sa )\n\n    // supported_versions (0x002b): TLS 1.3 (0x0304) then TLS 1.2 (0x0303)\n    : ( Vec u ) sv ( vec_new [u] )\n    ( vec_push [u] sv # u 4 )\n    ( _tls_u16 sv 772 )\n    ( _tls_u16 sv 771 )\n    ( _tls_u16 ext 43 )\n    ( _blk16 ext sv )\n\n    // ec_point_formats (0x000b): uncompressed — some TLS 1.2 servers require it\n    : ( Vec u ) epf ( vec_new [u] )\n    ( vec_push [u] epf # u 1 )\n    ( vec_push [u] epf # u 0 )\n    ( _tls_u16 ext 11 )\n    ( _blk16 ext epf )\n\n    // key_share (0x0033): a share for each group we offered, so whichever\n    // one the server selects we already supplied a matching public key —\n    // no HelloRetryRequest round trip.\n    //\n    // The X25519MLKEM768 share is the concatenation\n    // `ML-KEM-768 encapsulation key ‖ X25519 public key` — 1184 + 32 =\n    // 1216 bytes, ML-KEM first. That order is specific to this group\n    // (SecP256r1MLKEM768 puts the classical part first) and getting it\n    // backwards produces a handshake that fails only at Finished.\n    //\n    // It also makes the ClientHello roughly 1.5 kB, so it no longer fits\n    // in one TCP segment. That is ordinary — every browser sending this\n    // group has the same shape — but it does mean a path that silently\n    // drops large handshake packets will now fail where it used to work.\n    : ( Vec u ) ks ( vec_new [u] )\n    : ( Vec u ) entry ( vec_new [u] )\n    ? > ( vec_len [u] pqpub ) 0 {\n        ( _tls_u16 entry 4588 )  // group X25519MLKEM768\n        ( _tls_u16 entry + ( vec_len [u] pqpub ) 32 )  // 1216\n        ( _tls_cat entry pqpub )\n        ( _tls_cat entry pubkey )\n    } {}\n    ( _tls_u16 entry 29 )  // group x25519\n    ( _tls_u16 entry 32 )  // key_exchange length\n    ( _tls_cat entry pubkey )\n    ( _tls_u16 entry 23 )  // group secp256r1\n    ( _tls_u16 entry ( vec_len [u] p256pub ) )  // 65\n    ( _tls_cat entry p256pub )\n    ( _tls_u16 ks ( vec_len [u] entry ) )\n    ( _tls_cat ks entry )\n    ( _tls_u16 ext 51 )\n    ( _blk16 ext ks )\n\n    // application_layer_protocol_negotiation (0x0010), RFC 7301: the\n    // protocols we speak, most preferred first — `alp_list` is the wire\n    // form tls_alpn_pack makes of \"h2 http/1.1\", the same list the\n    // server's listener takes. Only emitted when at least one protocol\n    // was requested; otherwise the extension is omitted and the connect\n    // behaves exactly as before.\n    ? > ( vec_len [u] alp_list ) 0 {\n        : ( Vec u ) alp ( vec_new [u] )\n        ( _tls_u16 alp ( vec_len [u] alp_list ) )  // ProtocolNameList length\n        ( _tls_cat alp alp_list )\n        ( _tls_u16 ext 16 )\n        ( _blk16 ext alp )\n    } {}\n\n    // ── resumption (RFC 8446 §4.2.9 + §4.2.11) ──\n    // psk_key_exchange_modes goes in EVERY hello, offer or not: it is\n    // how a client says it can resume, and §4.2.9 forbids a server from\n    // sending a NewSessionTicket to a client that did not send it —\n    // rustls obeys, so without this the client never received a ticket\n    // from the Rust peer (openssl and our own server were lenient, which\n    // hid it). psk_dhe_ke only — a resumed handshake still runs a fresh\n    // (EC)DHE, so a ticket that leaks later never decrypts a recording of\n    // this connection.\n    : ( Vec u ) modes ( vec_new [u] )\n    ( vec_push [u] modes # u 1 )  // list length\n    ( vec_push [u] modes # u 1 )  // psk_dhe_ke\n    ( _tls_u16 ext 45 )\n    ( _blk16 ext modes )\n    // Whatever the driver asked for (QUIC: quic_transport_parameters),\n    // already wire-framed.\n    ( _tls_cat ext ext_extra )\n    // pre_shared_key MUST be the last extension: its binder is an HMAC\n    // over the ClientHello up to (not including) the binders list, so\n    // everything else has to be in place first. The binder bytes here\n    // are a placeholder the caller overwrites once it has hashed the\n    // truncated hello (see _psk_binder_over).\n    ? > ( vec_len [u] psk_id ) 0 {\n        : ( Vec u ) psk ( vec_new [u] )\n        ( _tls_u16 psk + ( vec_len [u] psk_id ) 6 )  // identities: u16 len + id + u32 age\n        ( _blk16 psk psk_id )\n        ( _tls_u32 psk obf_age )\n        ( _tls_u16 psk 33 )  // binders: u8 len + 32 bytes\n        ( vec_push [u] psk # u 32 )\n        : ~ i bk 0\n        ~ < bk 32 { ( vec_push [u] psk # u 0 ) = bk + bk 1 }\n        ( _tls_u16 ext 41 )\n        ( _blk16 ext psk )\n    } {}\n\n    ( _blk16 body ext )\n\n    // wrap as handshake message: type=1 (client_hello) + 3-byte length\n    : ( Vec u ) hs ( vec_with_cap [u] + ( vec_len [u] body ) 4 )\n    ( vec_push [u] hs # u 1 )\n    ( _u24 hs ( vec_len [u] body ) )\n    ( _tls_cat hs body )\n    ^ hs\n}\n\n// Parse ServerHello (full handshake message bytes) → server x25519 pubkey.\n@ __parse_server_hello ( Vec u ) msg → !( Vec u ) TlsErr {\n    // [0]=type(2) [1..4]=len ; body starts at 4\n    // body: ver(2) random(32) sid_len(1) sid cipher(2) comp(1) ext_len(2) ext...\n    : ~ i p 4\n    // HelloRetryRequest detection: random == special constant.\n    ? ( __is_hrr msg ) { ^ @ !( Vec u ) TlsErr { F # TlsErr TlsHRR } } {}\n    = p + p 2  // skip legacy_version\n    = p + p 32  // skip random\n    : i sidlen ( _t_bget msg p )\n    = p + + p 1 sidlen\n    : i cipher ( _rdint msg p 2 )\n    = p + p 2\n    ? & != cipher 4867 != cipher 4865 { ^ @ !( Vec u ) TlsErr { F # TlsErr TlsBadCipher } } {}\n    = p + p 1  // skip compression method\n    : i extlen ( _rdint msg p 2 )\n    = p + p 2\n    : i extend + p extlen\n    : ~ ( Vec u ) found ( vec_new [u] )\n    : ~ i got 0\n    ~ < p extend {\n        : i etype ( _rdint msg p 2 )\n        : i elen ( _rdint msg + p 2 2 )\n        : i edata + p 4\n        ? == etype 51 {\n            // key_share: group(2) ke_len(2) key_exchange\n            : i klen ( _rdint msg + edata 2 2 )\n            : ( Vec u ) key ( bytes_slice msg + edata 4 + + edata 4 klen )\n            = found key\n            = got 1\n        } {}\n        = p + + p 4 elen\n    }\n    ? == got 0 { ^ @ !( Vec u ) TlsErr { F # TlsErr TlsHandshake } } {}\n    ^ @ !( Vec u ) TlsErr { T found }\n}\n\n// The ALPN protocol a TLS 1.2 ServerHello selects (the 1.3 ServerHello\n// carries none: there it travels in EncryptedExtensions, __ee_alpn), or\n// an empty Vec. Same walk as __parse_server_hello, stopping at extension\n// 0x0010; the data is [list_len:2][name_len:1][name…].\n@ __sh_alpn ( Vec u ) msg → ( Vec u ) {\n    : ( Vec u ) out ( vec_new [u] )\n    : i n ( vec_len [u] msg )\n    ? < n 42 { ^ out } {}\n    : ~ i p 38  // past type, len, version, random\n    : i sidlen ( _t_bget msg p )\n    = p + + p 1 sidlen\n    = p + p 3  // cipher, compression\n    ? > + p 2 n { ^ out } {}\n    : i extlen ( _rdint msg p 2 )\n    = p + p 2\n    : i extend ? > + p extlen n n + p extlen\n    ~ < p extend {\n        ? > + p 4 extend { ^ out } {}\n        : i etype ( _rdint msg p 2 )\n        : i elen ( _rdint msg + p 2 2 )\n        : i edata + p 4\n        ? == etype 16 {\n            ? & >= elen 3 <= + edata elen extend {\n                : i nl ( _t_bget msg + edata 2 )\n                : ~ i j 0\n                ~ & < j nl < + + edata 3 j extend {\n                    ( vec_push [u] out # u ( _t_bget msg + + edata 3 j ) )\n                    = j + j 1\n                }\n            } {}\n            ^ out\n        } {}\n        = p + + p 4 elen\n    }\n    ^ out\n}\n\n// The raw cipher suite the server selected (2-byte value).\n@ __sh_suite ( Vec u ) msg → i {\n    : i sidlen ( _t_bget msg 38 )\n    ^ ( _rdint msg + 39 sidlen 2 )\n}\n\n// Negotiated TLS version (13/12) from the selected suite: the TLS 1.3\n// suites (0x1301/0x1303) imply 1.3, the ECDHE suites imply 1.2.\n@ __suite_version i suite → i {\n    ^ ? | == suite 4865 == suite 4867 13 12\n}\n\n// Our AEAD code (0 ChaCha20 / 1 AES-128-GCM) for a selected suite.\n@ __suite_cipher i suite → i {\n    ^ ? | | == suite 4865 == suite 49195 == suite 49199 1 0\n}\n\n@ __is_hrr ( Vec u ) msg → b {\n    // SHA-256(\"HelloRetryRequest\") in the ServerHello random field.\n    : i a ( _t_bget msg 6 )\n    : i b ( _t_bget msg 7 )\n    : i c2 ( _t_bget msg 8 )\n    : i d ( _t_bget msg 9 )\n    ^ & & & == a 207 == b 33 == c2 173 == d 116\n}\n\n// ── traffic-key derivation ────────────────────────────────────────\n// From a traffic secret, derive (key, iv) and store on the conn for the\n// given direction. dir 0 = server-read, 1 = client-write.\n@ _set_keys inout TlsConnImpl c i dir ( Vec u ) secret → v {\n    : ( Vec u ) retained ( bytes_slice secret 0 ( vec_len [u] secret ) )\n    : ( Vec u ) emptyc ( vec_new [u] )\n    : i klen ? == . c cipher 1 16 32\n    // One prepared secret for both derivations (stdlib/std/hkdf.nu).\n    : HmacSha256 sk ( hmac_sha256_key secret )\n    : ( Vec u ) key ( hkdf_expand_label_prk sk `key` emptyc klen )\n    : ( Vec u ) iv ( hkdf_expand_label_prk sk `iv` emptyc 12 )\n    ? == dir 0 {\n        = . c s_secret retained\n        = . c s_gk ( __tls_gk . c cipher key )\n        = . c s_key key\n        = . c s_iv iv\n        = . c s_seq 0\n    } {\n        = . c c_secret retained\n        = . c c_gk ( __tls_gk . c cipher key )\n        = . c c_key key\n        = . c c_iv iv\n        = . c c_seq 0\n    }\n    // A direction the kernel protects takes the new generation too (a\n    // KeyUpdate): the socket cannot fall back to this record layer, so a\n    // key the kernel refuses ends the connection.\n    : i kd ? == dir 0 . c ktls_s . c ktls_c\n    ? != kd 0 {\n        ? != 0 ( nurl_ktls_set . c fd kd . c cipher ( vec_data [u] ? == dir 0 . c s_key . c c_key ) ( vec_data [u] ? == dir 0 . c s_iv . c c_iv ) 0 ) {\n            = . c closed 1\n        } {}\n    } {}\n}\n\n// The prepared AES-GCM key for a traffic key — null for ChaCha20, whose\n// key needs no schedule.\n@ __tls_gk i cipher ( Vec u ) key → AesGcmKey {\n    ? == cipher 1 { ^ ( aes_gcm_key_new key ) } {}\n    ^ ( aes_gcm_key_new ( vec_new [u] ) )\n}\n\n// ── PSK key schedule pieces (shared by client and server) ─────────\n\n// early_secret for a PSK: HKDF-Extract(salt = \"\", IKM = PSK).\n@ _psk_early ( Vec u ) psk → ( Vec u ) {\n    : ( Vec u ) empty ( vec_new [u] )\n    : ( Vec u ) early ( hkdf_extract empty psk )\n    ^ early\n}\n\n// The binder for a pre_shared_key offer (RFC 8446 §4.2.11.2): the\n// Finished-style MAC under early_secret → \"res binder\" → \"finished\", over\n// the transcript hash of the ClientHello TRUNCATED to `trunc_len` bytes —\n// everything before the binders list. With the extension last that is\n// `len - 35` (u16 binders length + u8 binder length + 32 bytes).\n@ _psk_binder_over ( Vec u ) early ( Vec u ) ch i trunc_len → ( Vec u ) {\n    : ( Vec u ) empty ( vec_new [u] )\n    : ( Vec u ) ehash ( sha256_pure empty )\n    : ( Vec u ) bkey ( derive_secret early `res binder` ehash )\n    : ( Vec u ) fkey ( hkdf_expand_label bkey `finished` empty 32 )\n    : ( Vec u ) trunc ( bytes_slice ch 0 trunc_len )\n    : ( Vec u ) th ( sha256_pure trunc )\n    : ( Vec u ) mac ( hmac_sha256_pure fkey th )\n    ^ mac\n}\n\n// Constant-time compare of two 32-byte values (binders, Finished MACs).\n@ _ct_eq32 ( Vec u ) a i aoff ( Vec u ) b → b {\n    ? | < ( vec_len [u] a ) + aoff 32 < ( vec_len [u] b ) 32 { ^ F } {}\n    : ~ i diff 0\n    : ~ i k 0\n    ~ < k 32 { = diff | diff ^^ ( _t_bget a + aoff k ) ( _t_bget b k ) = k + k 1 }\n    ^ == diff 0\n}\n\n// Overwrite the last 32 bytes of `ch` (the binder placeholder) with `b`.\n@ __ch_patch_binder ( Vec u ) ch ( Vec u ) b → v {\n    : i off - ( vec_len [u] ch ) 32\n    : *u d ( vec_data [u] ch )\n    : ~ i k 0\n    ~ < k 32 { = . d + off k # u ( _t_bget b k ) = k + k 1 }\n}\n\n// ── session state (client) ────────────────────────────────────────\n\n// Opaque resumption state for a later connection: what the newest\n// NewSessionTicket said plus the PSK derived from it. Empty when no\n// ticket has arrived — the server sends it right after the handshake,\n// inside the application-data stream, so it lands during the first\n// tls_read. Hand the bytes to tls_connect_resume / tls_attach_resume;\n// they are secret (they hold the PSK) and single-purpose.\n@ tls_session_export TlsConn c__h → ( Vec u ) {\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    : ( Vec u ) out ( vec_new [u] )\n    ? == ( vec_len [u] . c tk_ticket ) 0 { ^ out } {}\n    ( vec_push [u] out # u 1 )  // format version\n    ( _tls_u32 out . c tk_age_add )\n    ( _tls_u32 out . c tk_lifetime )\n    ( _tls_u64 out . c tk_received_ms )\n    ( _blk16 out . c tk_psk )\n    ( _blk16 out . c tk_ticket )\n    ^ out\n}\n\n// The runtime socket handle under the connection — for timeouts and\n// readiness polling (nurl_tcp_set_timeout, nurl_tcp_err_kind, …).\n@ tls_socket TlsConn c__h → i { ^ . ( __TlsConn_ptr c__h ) fd }\n\n// T when the handshake used a ticket (no certificate was sent; the PSK\n// authenticates the server as the one that issued it).\n@ tls_is_resumed TlsConn c__h → b {\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ == . c resumed 1\n}\n\n// RFC 8446 §§4.6.3, 7.2: rotate the indicated sender's keys and\n// reset that direction's record sequence without retaining old generations.\n@ _tls_rotate_keys inout TlsConnImpl c i dir → v {\n    : ( Vec u ) empty ( vec_new [u] )\n    : ( Vec u ) next ( hkdf_expand_label ? == dir 0 . c s_secret . c c_secret `traffic upd` empty 32 )\n    ( _set_keys c dir next )\n}\n\n// Encoding joins the same FIFO as already prepared ciphertext. The KU\n// itself uses the old write keys; all subsequent records use the new ones.\n@ _tls_control_to inout TlsConnImpl c ( Vec u ) out i dir → v {\n    ? != . c fatal_alert 0 {\n        : ( Vec u ) alert ( vec_new [u] )\n        ( vec_push [u] alert # u 2 ) ( vec_push [u] alert # u . c fatal_alert )\n        ( _tls_seal_direction_to c out dir 21 alert )\n        = . c fatal_alert 0 = . c update_pending 0 = . c closed 1\n        ^\n    } {}\n    ? | != . c version 13 == . c update_pending 0 { ^ } {}\n    : ( Vec u ) update ( vec_new [u] )\n    ( vec_push [u] update # u 24 ) ( _u24 update 1 )\n    ( vec_push [u] update # u 0 )\n    ( _tls_seal_direction_to c out dir 22 update )\n    ( _tls_rotate_keys c dir )\n    = . c update_pending 0\n}\n\n@ _tls_flush_control inout TlsConnImpl c i dir → !v TlsErr {\n    ? & == . c update_pending 0 == . c fatal_alert 0 { ^ @ !v TlsErr { T 0 } } {}\n    : ( Vec u ) wire ( vec_new [u] )\n    ( _tls_control_to c wire dir )\n    : b sent ( _tls_sock_write . c fd wire )\n    ? ! sent { = . c closed 1 ^ @ !v TlsErr { F TlsWrite } } {}\n    ^ @ !v TlsErr { T 0 }\n}\n\n// Blocking readers send the fatal alert before returning the error.\n// Try-read leaves it for the existing ordered writer; once encoded, reads\n// report closed. Neither path emits further application data after failure.\n@ _tls_post_fail inout TlsConnImpl c i peer i alert → !v TlsErr {\n    = . c fatal_alert alert\n    ? == . c read_nowait 0 {\n        : !v TlsErr sent ( _tls_flush_control c - 1 peer )\n        ?? sent { T _ → {} F _ → {} }\n    } {}\n    ^ @ !v TlsErr { F TlsProtocol }\n}\n\n// Post-handshake fragments are bounded and cannot cross content-type or\n// key-generation boundaries. dir identifies the peer (0 server,1 client).\n@ _tls_post_hs inout TlsConnImpl c ( Vec u ) inner i dir → !v TlsErr {\n    ? | == ( vec_len [u] inner ) 0 > + ( vec_len [u] . c hsbuf ) ( vec_len [u] inner ) 262144 {\n        ^ ( _tls_post_fail c dir 50 )\n    } {}\n    ( _tls_cat . c hsbuf inner )\n    ~ >= ( vec_len [u] . c hsbuf ) 4 {\n        : i have ( vec_len [u] . c hsbuf )\n        : i kind ( _t_bget . c hsbuf 0 )\n        : i mlen ( _rdint . c hsbuf 1 3 )\n        ? | > mlen 262140 & != kind 24 | != dir 0 != kind 4 {\n            ^ ( _tls_post_fail c dir 10 )\n        } {}\n        ? & == kind 24 != mlen 1 { ^ ( _tls_post_fail c dir 50 ) } {}\n        ? < have + 4 mlen { ^ @ !v TlsErr { T 0 } } {}\n        ? == kind 24 {\n            // KU must end its record, so no bytes may follow it under old keys.\n            : i request ( _t_bget . c hsbuf 4 )\n            ? != have 5 { ^ ( _tls_post_fail c dir 10 ) } {}\n            ? > request 1 { ^ ( _tls_post_fail c dir 47 ) } {}\n            ( vec_clear [u] . c hsbuf )\n            ( _tls_rotate_keys c dir )\n            ? == request 1 { = . c update_pending 1 } {}\n        } {\n            : ( Vec u ) msg ( bytes_slice . c hsbuf 0 + 4 mlen )\n            : ( Vec u ) rest ( bytes_slice . c hsbuf + 4 mlen have )\n            = . c hsbuf rest\n            ( __client_take_ticket c msg )\n        }\n    }\n    ^ @ !v TlsErr { T 0 }\n}\n\n// NewSessionTicket body: u32 lifetime, u32 age_add, nonce<u8>, ticket<u16>,\n// extensions<u16>. PSK = HKDF-Expand-Label(res_master, \"resumption\", nonce, 32).\n@ __client_take_ticket inout TlsConnImpl c ( Vec u ) msg → v {\n    ? == ( vec_len [u] . c res_master ) 0 { ^ } {}\n    : i n ( vec_len [u] msg )\n    ? < n 17 { ^ } {}\n    : i lifetime ( _rdint msg 4 4 )\n    : i age_add ( _rdint msg 8 4 )\n    : i nlen ( _t_bget msg 12 )\n    : i tp + 13 nlen\n    ? > + tp 2 n { ^ } {}\n    : i tlen ( _rdint msg tp 2 )\n    ? | == tlen 0 > + + tp 2 tlen n { ^ } {}\n    : ( Vec u ) nonce ( bytes_slice msg 13 tp )\n    : ( Vec u ) psk ( hkdf_expand_label . c res_master `resumption` nonce 32 )\n    = . c tk_ticket ( bytes_slice msg + tp 2 + + tp 2 tlen )\n    = . c tk_psk psk\n    = . c tk_age_add age_add\n    = . c tk_lifetime lifetime\n    = . c tk_received_ms ( now_ms )\n}\n\n// Does a ServerHello carry pre_shared_key (41) — i.e. did the server take\n// our ticket? Layout after the 4-byte header: ver(2) random(32) sid<u8>\n// cipher(2) compression(1) extensions<u16>.\n@ __sh_has_psk ( Vec u ) msg → b {\n    : ~ i p 38\n    : i sidlen ( _t_bget msg p )\n    = p + + p 1 sidlen\n    = p + p 3\n    : i extlen ( _rdint msg p 2 )\n    = p + p 2\n    : i extend + p extlen\n    ~ < + p 4 + extend 1 {\n        : i etype ( _rdint msg p 2 )\n        : i elen ( _rdint msg + p 2 2 )\n        ? == etype 41 { ^ T } {}\n        = p + + p 4 elen\n    }\n    ^ F\n}\n\n// HMAC-based Finished verify_data over a traffic secret + transcript hash.\n@ _finished_mac ( Vec u ) secret ( Vec u ) thash → ( Vec u ) {\n    : ( Vec u ) emptyc ( vec_new [u] )\n    : ( Vec u ) fkey ( hkdf_expand_label secret `finished` emptyc 32 )\n    : ( Vec u ) mac ( hmac_sha256_pure fkey thash )\n    ^ mac\n}\n\n// Establish a TLS 1.3 connection WITHOUT verifying the server\n// certificate — encrypted but not authenticated (MITM-able). Use only\n// for pinned/self-signed/testing cases. `tls_connect` (below) is the\n// secure, verifying entry point. The presented chain, CertificateVerify\n// signature and transcript hash are captured on the conn for the\n// verifier.\n@ tls_connect_insecure s host i port s server_name → !TlsConn TlsErr {\n    : i raw ( nurl_tcp_connect host port )\n    ^ ( tls_attach raw server_name )\n}\n\n// Run the TLS handshake over a socket that is ALREADY connected (a raw\n// libc fd handle as returned by `nurl_tcp_connect`). This is what\n// STARTTLS-style protocols need — PostgreSQL's SSLRequest, SMTP STARTTLS,\n// IMAP/FTP — where the plaintext leg must exchange a few bytes before the\n// channel is upgraded to TLS on the same socket. No certificate\n// verification (see `tls_attach_verify` for the secure variant).\n// Extract the server-selected ALPN protocol from an EncryptedExtensions\n// handshake message (type 8). Returns the protocol bytes (e.g. \"h2\"), or\n// an empty Vec if the server sent no ALPN extension. Message layout:\n// [type:1][len:3][exts_len:2] then exts; ALPN ext (0x0010) data is\n// [list_len:2][name_len:1][name…].\n// Pack a space-separated protocol list (\"h2 http/1.1\") into ALPN wire\n// form: [len:1][name] per entry, in the given order — the ProtocolNameList\n// body of RFC 7301 §3.1, used by both the client's offer and the server's\n// listener preference. Names longer than 255 bytes cannot be encoded and\n// are dropped; empty tokens are skipped.\n@ tls_alpn_pack s list → ( Vec u ) {\n    : ( Vec u ) out ( vec_new [u] )\n    : i n ( nurl_str_len list )\n    : ~ i p 0\n    ~ < p n {\n        ~ & < p n == ( nurl_str_at list n p ) 32 { = p + p 1 }\n        : i start p\n        ~ & < p n != ( nurl_str_at list n p ) 32 { = p + p 1 }\n        : i tl - p start\n        ? & > tl 0 <= tl 255 {\n            ( vec_push [u] out # u tl )\n            : ~ i k start\n            ~ < k p { ( vec_push [u] out # u ( nurl_str_at list n k ) ) = k + k 1 }\n        } {}\n    }\n    ^ out\n}\n\n// T iff `sel` (a bare protocol name) is one of the entries of the\n// space-separated offer `list`.\n@ _alpn_offered s list ( Vec u ) sel → b {\n    : ( Vec u ) packed ( tls_alpn_pack list )\n    : b r ( _alpn_offered_packed packed sel )\n    ^ r\n}\n\n// The same over an offer already in wire form.\n@ _alpn_offered_packed ( Vec u ) packed ( Vec u ) sel → b {\n    : i n ( vec_len [u] packed )\n    : i sl ( vec_len [u] sel )\n    : ~ i p 0\n    : ~ b found F\n    ~ & ! found < p n {\n        : i tl ( _t_bget packed p )\n        ? == tl sl {\n            : ~ i k 0\n            : ~ b same T\n            ~ & same < k tl {\n                ? != ( _t_bget packed + + p 1 k ) ( _t_bget sel k ) { = same F } {}\n                = k + k 1\n            }\n            = found same\n        } {}\n        = p + + p 1 tl\n    }\n    ^ found\n}\n\n// Send a fatal alert (RFC 8446 §6) under the current write keys — during\n// the server flight those are the handshake keys, so the peer can read\n// it. Best effort: the connection is being torn down either way.\n@ __send_alert inout TlsConnImpl c i desc → v {\n    : ( Vec u ) alert ( vec_with_cap [u] 2 )\n    ( vec_push [u] alert # u 2 )\n    ( vec_push [u] alert # u desc )\n    : !v TlsErr _w ( __send_encrypted c 21 alert )\n}\n\n@ __ee_alpn ( Vec u ) msg → ( Vec u ) {\n    : ( Vec u ) out ( vec_new [u] )\n    : i n ( vec_len [u] msg )\n    ? < n 6 { ^ out } {}\n    : i extlen ( _rdint msg 4 2 )\n    : i end ? > + 6 extlen n n + 6 extlen\n    : ~ i p 6\n    ~ < p end {\n        ? > + p 4 end { ^ out } {}\n        : i et ( _rdint msg p 2 )\n        : i elen ( _rdint msg + p 2 2 )\n        : i edata + p 4\n        ? == et 16 {\n            ? >= elen 3 {\n                : i nl ( _t_bget msg + edata 2 )\n                : ~ i j 0\n                ~ < j nl {\n                    ( vec_push [u] out # u ( _t_bget msg + + edata 3 j ) )\n                    = j + j 1\n                }\n            } {}\n            ^ out\n        } {}\n        = p + + p 4 elen\n    }\n    ^ out\n}\n\n// ── the client handshake machine ──────────────────────────────────\n//\n// `CliHs` is the TLS 1.3 client handshake with no socket in it — the\n// same split `std/tls_server.nu` gives the server in `SrvHs`: whole\n// handshake messages go in, the messages to send come out, and the\n// traffic secrets are read straight off the machine. Two drivers:\n//\n//   * `__tls_handshake` below (TCP): sends `out_ch` as a plaintext\n//     record, feeds the ServerHello and then the encrypted server\n//     flight message by message, installs the secrets as record keys,\n//     sends `out_fin` under the handshake keys.\n//   * `std/quic_tls.nu` (QUIC, RFC 9001, client role): CRYPTO frame\n//     bytes per encryption level, packet keys from the same secrets,\n//     the quic_transport_parameters extension carried through\n//     `ext_out` / `ext_want` / `ext_in`.\n//\n//   ( _cli_hs_new server_name alpn sess ) → CliHs    `alpn` = \"h2 http/1.1\" (empty: no ALPN);\n//                                                    `sess` = a tls_session_export blob (empty: none) —\n//                                                    a usable one becomes the pre_shared_key offer\n//   ( _cli_hs_set_ext h ext_out want )    → v        append `ext_out` (wire-framed extension(s)) to the\n//                                                    ClientHello; require EE extension `want` (0 = none)\n//   ( _cli_hs_set_compat h on )           → v        0 = no middlebox compatibility: an empty\n//                                                    legacy_session_id (QUIC, RFC 9001 §8.4); default 1\n//   ( _cli_hs_start h )                   → v        key shares + ClientHello into `out_ch`\n//   ( _cli_hs_server_hello h sh )         → i        0 ok · alert description otherwise. With TLS 1.2\n//                                                    chosen `version` is 12, nothing is derived, `sh`\n//                                                    is kept, and the caller decides what to do\n//   ( _cli_hs_message h m )               → i        EncryptedExtensions / Certificate /\n//                                                    CertificateVerify / Finished; 0 ok · alert\n//                                                    description. After the Finished `state` is 3 and\n//                                                    out_fin, c_ap / s_ap, res_master are set\n//   ( _cli_hs_err h )                     → TlsErr   what a failure was, in the record layer's terms\n//   ( _cli_hs_out_ch h ) … ( _cli_hs_s_ap h )         the machine's fields, read (Vecs lent)\n//\n// `state`: 0 new · 1 ClientHello built (awaiting ServerHello) · 2\n// handshake secrets derived (awaiting the server flight) · 3 done ·\n// 4 failed. A CliHs is a library handle (docs/MEMORY.md §7.6): its last\n// owner releases it, so a handshake abandoned at any step leaks nothing.\n// Every `( Vec u )` field is owned by the machine; a caller that wants to\n// keep one copies (or, in this file, moves) it.\n//\n// The certificate is NOT verified here: `cert_msg`, `cv_scheme`,\n// `cv_sig` and `th_cert` are captured for `tls_cert_verify`, exactly as\n// the record layer has always done (`__verify_conn`). A resumed\n// handshake captures nothing — the PSK authenticates the server.\n\n// The machine's state, behind the CliHs handle below.\n: CliHsImpl {\n    ( Vec u ) sni  // host bytes for server_name\n    ( Vec u ) alpn  // ALPN offer, wire form (tls_alpn_pack)\n    ( Vec u ) ext_out  // extra ClientHello extension(s), wire-framed\n    i ext_want  // EncryptedExtensions extension type required (0 = none)\n    ( Vec u ) ext_in  // its body once seen\n    i ext_in_present\n    i compat  // 1: TLS-over-TCP middlebox compatibility (a 32-byte legacy_session_id, RFC 8446 D.4);\n    // 0: QUIC, where the session id MUST be empty (RFC 9001 §8.4)\n    i state\n    i err  // failure kind: 1 TlsHandshake 2 TlsProtocol 3 TlsBadCipher 4 TlsHRR\n    Sha256 trh  // incremental transcript hash\n    i cipher  // 0 ChaCha20-Poly1305 · 1 AES-128-GCM\n    i version  // 13 / 12, known from the ServerHello on\n    i kx_group  // 4588 X25519MLKEM768 · 29 x25519 · 23 secp256r1\n    i resumed  // 1 when the server took the offered ticket\n    i offer  // 1 when a ticket was offered\n    ( Vec u ) x_priv  // X25519 ephemeral\n    ( Vec u ) x_pub\n    ( Vec u ) p256_priv  // P-256 ephemeral scalar\n    ( Vec u ) pq_dk  // ML-KEM-768 decapsulation key\n    ( Vec u ) random\n    ( Vec u ) sessid\n    ( Vec u ) tk_ticket  // the offered ticket and its PSK\n    ( Vec u ) tk_psk\n    i tk_age_add\n    i tk_lifetime\n    i tk_received_ms\n    ( Vec u ) res_early  // early_secret(PSK) while offering\n    ( Vec u ) alpn_sel  // what the server selected (checked against `alpn`)\n    ( Vec u ) c_hs\n    ( Vec u ) s_hs\n    ( Vec u ) master\n    ( Vec u ) c_ap\n    ( Vec u ) s_ap\n    ( Vec u ) res_master\n    ( Vec u ) cert_msg  // raw Certificate message, for the verifier\n    ( Vec u ) cv_sig  // CertificateVerify signature\n    ( Vec u ) th_cert  // transcript hash through Certificate\n    i cv_scheme  // CertificateVerify SignatureScheme\n    ( Vec u ) out_ch  // the ClientHello, to send in the clear\n    ( Vec u ) out_fin  // the client Finished, to send under c_hs\n    ( Vec u ) sh  // the ServerHello, kept only for a TLS 1.2 fallback\n}\n\n// A CliHs is a handle on its state in an rcbox (stdlib/core/rcbox.nu):\n// every copy is the same state, and the last owner releases it.\n: CliHs { ( Shared CliHsImpl ) ctl }\n\n@ CliHs_share CliHs h → CliHs { ^ @ CliHs { ( shared_clone [CliHsImpl] . h ctl ) } }\n\n@ CliHs_drop sink CliHs h → v {}\n\n@ __CliHs_ptr CliHs h → *CliHsImpl { ^ ( shared_ptr [CliHsImpl] . h ctl ) }\n\n@ _cli_hs_new s server_name s alpn ( Vec u ) sess → CliHs {\n    : ( Shared CliHsImpl ) h__box ( shared_zero [CliHsImpl] )\n    : ~ * CliHsImpl h ( shared_ptr [CliHsImpl] h__box )\n    = . h sni ( bytes_from_str server_name )\n    = . h alpn ( tls_alpn_pack alpn )\n    = . h ext_out ( vec_new [u] )\n    = . h ext_want 0\n    = . h ext_in ( vec_new [u] )\n    = . h ext_in_present 0\n    = . h compat 1\n    = . h state 0\n    = . h err 0\n    // Incremental transcript hash, snapshotted at the checkpoints —\n    // the server's machine hashes the same way.\n    = . h trh ( sha256_init )\n    = . h cipher 0\n    = . h version 13\n    = . h kx_group 0\n    = . h resumed 0\n    = . h offer 0\n    = . h x_priv ( vec_new [u] )\n    = . h x_pub ( vec_new [u] )\n    = . h p256_priv ( vec_new [u] )\n    = . h pq_dk ( vec_new [u] )\n    = . h random ( vec_new [u] )\n    = . h sessid ( vec_new [u] )\n    = . h tk_ticket ( vec_new [u] )\n    = . h tk_psk ( vec_new [u] )\n    = . h tk_age_add 0\n    = . h tk_lifetime 0\n    = . h tk_received_ms 0\n    = . h alpn_sel ( vec_new [u] )\n    = . h c_hs ( vec_new [u] )\n    = . h s_hs ( vec_new [u] )\n    = . h master ( vec_new [u] )\n    = . h c_ap ( vec_new [u] )\n    = . h s_ap ( vec_new [u] )\n    = . h res_master ( vec_new [u] )\n    = . h cert_msg ( vec_new [u] )\n    = . h cv_sig ( vec_new [u] )\n    = . h th_cert ( vec_new [u] )\n    = . h cv_scheme 0\n    = . h out_ch ( vec_new [u] )\n    = . h out_fin ( vec_new [u] )\n    = . h sh ( vec_new [u] )\n    // A usable exported session becomes the pre_shared_key offer; the\n    // server may still decline it (rotated ticket key, expired, or no\n    // resumption at all), in which case the handshake is simply the\n    // full one — nothing here is trusted until the ServerHello says\n    // the ticket was taken.\n    ? ( __cli_sess_load . h 0 sess ) {\n        = . h offer 1\n        = . h res_early ( _psk_early . h tk_psk )\n    } { = . h res_early ( vec_new [u] ) }\n    ^ @ CliHs { h__box }\n}\n\n@ _cli_hs_set_ext CliHs h__h ( Vec u ) ext_out i want → v {\n    : *CliHsImpl h ( __CliHs_ptr h__h )\n    ( vec_clear [u] . h ext_out )\n    ( bytes_extend_bytes . h ext_out ext_out )\n    = . h ext_want want\n}\n\n@ _cli_hs_set_compat CliHs h__h i on → v {\n    : *CliHsImpl h ( __CliHs_ptr h__h )\n    = . h compat on\n}\n\n// What the QUIC driver (std/quic_tls.nu) reads off the machine. Vecs are\n// the machine's own, lent.\n@ _cli_hs_state CliHs h → i { ^ . ( __CliHs_ptr h ) state }\n\n@ _cli_hs_version CliHs h → i { ^ . ( __CliHs_ptr h ) version }\n\n@ _cli_hs_cipher CliHs h → i { ^ . ( __CliHs_ptr h ) cipher }\n\n@ _cli_hs_kx_group CliHs h → i { ^ . ( __CliHs_ptr h ) kx_group }\n\n@ _cli_hs_resumed CliHs h → i { ^ . ( __CliHs_ptr h ) resumed }\n\n@ _cli_hs_cv_scheme CliHs h → i { ^ . ( __CliHs_ptr h ) cv_scheme }\n\n@ _cli_hs_out_ch CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) out_ch }\n\n@ _cli_hs_out_fin CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) out_fin }\n\n@ _cli_hs_ext_in CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) ext_in }\n\n@ _cli_hs_alpn_sel CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) alpn_sel }\n\n@ _cli_hs_cert_msg CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) cert_msg }\n\n@ _cli_hs_cv_sig CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) cv_sig }\n\n@ _cli_hs_th_cert CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) th_cert }\n\n@ _cli_hs_c_hs CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) c_hs }\n\n@ _cli_hs_s_hs CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) s_hs }\n\n@ _cli_hs_c_ap CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) c_ap }\n\n@ _cli_hs_s_ap CliHs h → ( Vec u ) { ^ . ( __CliHs_ptr h ) s_ap }\n\n@ __cli_hs_fail inout CliHsImpl h i err i alert → i {\n    = . h state 4\n    = . h err err\n    ^ alert\n}\n\n@ _cli_hs_err CliHs h__h → TlsErr {\n    : ~ * CliHsImpl h ( __CliHs_ptr h__h )\n    ^ ( __cli_hs_errk . h 0 )\n}\n\n@ __cli_hs_errk inout CliHsImpl h → TlsErr {\n    ? == . h err 2 { ^ # TlsErr TlsProtocol } {}\n    ? == . h err 3 { ^ # TlsErr TlsBadCipher } {}\n    ? == . h err 4 { ^ # TlsErr TlsHRR } {}\n    ^ # TlsErr TlsHandshake\n}\n\n// Load an exported session onto the machine as the offer for its\n// handshake. F (and nothing loaded) for an empty, malformed or expired\n// blob — the caller then simply does a full handshake.\n@ __cli_sess_load inout CliHsImpl h ( Vec u ) sess → b {\n    : i n ( vec_len [u] sess )\n    ? | < n 21 != ( _t_bget sess 0 ) 1 { ^ F } {}\n    : i age_add ( _rdint sess 1 4 )\n    : i lifetime ( _rdint sess 5 4 )\n    : i received ( _rdint sess 9 8 )\n    : i plen ( _rdint sess 17 2 )\n    : i tp + 19 plen\n    ? > + tp 2 n { ^ F } {}\n    : i tlen ( _rdint sess tp 2 )\n    ? | == tlen 0 != + + tp 2 tlen n { ^ F } {}\n    // RFC 8446 §4.6.1: a ticket is usable for ticket_lifetime seconds\n    // (never more than 7 days); past that the server will decline it, so\n    // do not offer it.\n    : i age_ms - ( now_ms ) received\n    ? | < age_ms 0 > age_ms * lifetime 1000 { ^ F } {}\n    = . h tk_psk ( bytes_slice sess 19 tp )\n    = . h tk_ticket ( bytes_slice sess + tp 2 n )\n    = . h tk_age_add age_add\n    = . h tk_lifetime lifetime\n    = . h tk_received_ms received\n    ^ T\n}\n\n// Fresh key shares for every group we offer and the ClientHello that\n// carries them, into `out_ch`.\n@ _cli_hs_start CliHs h__h → v {\n    : ~ * CliHsImpl h ( __CliHs_ptr h__h )\n    ( _cli_hs_start_in . h 0 )\n}\n\n@ _cli_hs_start_in inout CliHsImpl h → v {\n    ? != . h state 0 { ^ } {}\n    = . h x_priv ( _rand_bytes 32 )\n    = . h x_pub ( x25519_base . h x_priv )\n    = . h p256_priv ( _rand_bytes 32 )\n    : ( Vec u ) p256pub ( p256_ecdh_keygen . h p256_priv )\n    // ML-KEM-768 for the hybrid group. The decapsulation key stays on\n    // the machine until the server's share arrives; the encapsulation\n    // key travels in the ClientHello.\n    : MlkemKeys pqkeys ( mlkem_keygen 768 )\n    : ( Vec u ) pqpub ( bytes_slice ( mlkem_ek pqkeys ) 0 ( vec_len [u] ( mlkem_ek pqkeys ) ) )\n    = . h pq_dk ( bytes_slice ( mlkem_dk pqkeys ) 0 ( vec_len [u] ( mlkem_dk pqkeys ) ) )\n    = . h random ( _rand_bytes 32 )\n    = . h sessid ( _rand_bytes ? != . h compat 0 32 0 )\n    : ~ i obf_age 0\n    ? == . h offer 1 {\n        : i age - ( now_ms ) . h tk_received_ms\n        = obf_age & + age . h tk_age_add 4294967295\n    } {}\n    : ( Vec u ) noid ( vec_new [u] )\n    : ( Vec u ) ch ( __build_client_hello . h sni . h x_pub p256pub pqpub . h random . h sessid . h alpn . h ext_out ? == . h offer 1 . h tk_ticket noid obf_age )\n    ? == . h offer 1 {\n        : ( Vec u ) binder ( _psk_binder_over . h res_early ch - ( vec_len [u] ch ) 35 )\n        ( __ch_patch_binder ch binder )\n    } {}\n    ( sha256_update . h trh ch )\n    = . h out_ch ch\n    = . h state 1\n}\n\n// The ServerHello: cipher and version, the server's key share, and the\n// whole handshake key schedule. On success `state` is 2 and c_hs / s_hs\n// are the handshake traffic secrets.\n@ _cli_hs_server_hello CliHs h__h ( Vec u ) sh → i {\n    : ~ * CliHsImpl h ( __CliHs_ptr h__h )\n    ^ ( _cli_hs_server_hello_in . h 0 sh )\n}\n\n@ _cli_hs_server_hello_in inout CliHsImpl h ( Vec u ) sh → i {\n    ? != . h state 1 { ^ ( __cli_hs_fail h 1 10 ) } {}\n    // handshake type 2, and at least the fixed part of the body\n    ? | < ( vec_len [u] sh ) 42 != ( _t_bget sh 0 ) 2 { ^ ( __cli_hs_fail h 1 50 ) } {}\n    : i suite ( __sh_suite sh )\n    = . h version ( __suite_version suite )\n    = . h cipher ( __suite_cipher suite )\n    ? == . h version 12 {\n        // TLS 1.2: none of the 1.3 schedule applies. The hello is kept\n        // for a caller that speaks 1.2 (the TCP record layer does);\n        // QUIC refuses it.\n        = . h sh ( bytes_slice sh 0 ( vec_len [u] sh ) )\n        ^ 0\n    } {}\n    : ~ ( Vec u ) spub ( vec_new [u] )\n    : ~ i bad 0\n    : !( Vec u ) TlsErr spkr ( __parse_server_hello sh )\n    ?? spkr {\n        T k → { = spub k }\n        F e → { = bad ?? e { TlsHRR → 4 TlsBadCipher → 3 _ → 1 } }\n    }\n    // A HelloRetryRequest is not taken up (every share is in the first\n    // hello, so a server has no reason to send one): handshake_failure.\n    // A suite or key_share we cannot use is illegal_parameter.\n    ? != bad 0 { ^ ( __cli_hs_fail h bad ? == bad 4 40 47 ) } {}\n    ( sha256_update . h trh sh )\n\n    // The negotiated group is told by the server key-exchange length:\n    // X25519 is 32 bytes, an uncompressed secp256r1 point is 65, and\n    // the X25519MLKEM768 share is 1088 + 32 = 1120.\n    //\n    // For the hybrid group the shared secret handed to the key schedule\n    // is `ML-KEM shared secret ‖ X25519 shared secret` — 64 bytes,\n    // ML-KEM first, matching the order of the shares. Concatenation is\n    // what makes it a hybrid worth having: HKDF-Extract over the pair\n    // is at least as strong as either half, so the handshake survives\n    // ML-KEM being broken *and* survives X25519 being broken.\n    : i sl ( vec_len [u] spub )\n    ? & & != sl 1120 != sl 65 != sl 32 { ^ ( __cli_hs_fail h 2 47 ) } {}\n    = . h kx_group ? == sl 1120 4588 ? == sl 65 23 29\n    : ( Vec u ) ecdhe ? == sl 1120\n    ( __hybrid_shared . h pq_dk . h x_priv spub )\n    ? == sl 65 ( p256_ecdh_shared . h p256_priv spub ) ( x25519 . h x_priv spub )\n    // RFC 8446 §7.4.2 — abort if the ECDHE output is all-zero (peer sent\n    // a low-order / small-subgroup point forcing a known shared secret).\n    ? ( _all_zero ecdhe ) { ^ ( __cli_hs_fail h 2 47 ) } {}\n\n    : ( Vec u ) z32 ( vec_with_cap [u] 32 )\n    : ~ i zk 0\n    ~ < zk 32 { ( vec_push [u] z32 # u 0 ) = zk + zk 1 }\n    : ( Vec u ) empty ( vec_new [u] )\n    : ( Vec u ) ehash ( sha256_pure empty )\n    // The server took our ticket iff its ServerHello carries\n    // pre_shared_key; then the early secret is the PSK's and no\n    // Certificate / CertificateVerify will follow — the PSK is the proof\n    // of identity (only the issuer of the ticket knows it).\n    ? & == . h offer 1 ( __sh_has_psk sh ) { = . h resumed 1 } {}\n    : ( Vec u ) early ? == . h resumed 1 ( bytes_slice . h res_early 0 32 ) ( hkdf_extract empty z32 )\n    : ( Vec u ) derived1 ( derive_secret early `derived` ehash )\n    // handshake_secret derives three secrets: prepared once.\n    : ( Vec u ) hs_secret ( hkdf_extract derived1 ecdhe )\n    : HmacSha256 hsk ( hmac_sha256_key hs_secret )\n    : ( Vec u ) th_sh ( sha256_snapshot . h trh )\n    = . h c_hs ( derive_secret_prk hsk `c hs traffic` th_sh )\n    = . h s_hs ( derive_secret_prk hsk `s hs traffic` th_sh )\n    : ( Vec u ) derived2 ( derive_secret_prk hsk `derived` ehash )\n    = . h master ( hkdf_extract derived2 z32 )\n    = . h state 2\n    ^ 0\n}\n\n// Offset of the data of extension `want` within msg[es..ee), or -1.\n@ __cli_find_ext ( Vec u ) msg i es i ee i want → i {\n    : ~ i p es\n    : ~ i found -1\n    ~ & < + p 4 + ee 1 == found -1 {\n        : i et ( _rdint msg p 2 )\n        : i el ( _rdint msg + p 2 2 )\n        ? == et want { = found + p 4 } { = p + + p 4 el }\n    }\n    ^ found\n}\n\n// One message of the server's flight, under the handshake keys.\n@ _cli_hs_message CliHs h__h ( Vec u ) m → i {\n    : ~ * CliHsImpl h ( __CliHs_ptr h__h )\n    ^ ( _cli_hs_message_in . h 0 m )\n}\n\n@ _cli_hs_message_in inout CliHsImpl h ( Vec u ) m → i {\n    ? != . h state 2 { ^ ( __cli_hs_fail h 1 10 ) } {}\n    ? < ( vec_len [u] m ) 4 { ^ ( __cli_hs_fail h 1 50 ) } {}\n    : i t ( _t_bget m 0 )\n    // Nothing but the flight belongs here: a hello, EndOfEarlyData, a\n    // ticket or a KeyUpdate before the Finished is unexpected_message.\n    ? | | | | == t 1 == t 2 == t 4 == t 5 == t 24 { ^ ( __cli_hs_fail h 1 10 ) } {}\n\n    ? == t 20 {\n        // Finished: the MAC is over the transcript BEFORE this message.\n        : ( Vec u ) th_cv ( sha256_snapshot . h trh )\n        : ( Vec u ) expect ( _finished_mac . h s_hs th_cv )\n        : b okfin ( _cmp_finished m expect )\n        ? okfin {} { ^ ( __cli_hs_fail h 1 51 ) }\n        ( sha256_update . h trh m )\n        // application traffic secrets: transcript through the server\n        // Finished — also what our own Finished is computed over\n        : ( Vec u ) th_sf ( sha256_snapshot . h trh )\n        // master_secret derives three secrets: prepared once.\n        : HmacSha256 mk ( hmac_sha256_key . h master )\n        = . h c_ap ( derive_secret_prk mk `c ap traffic` th_sf )\n        = . h s_ap ( derive_secret_prk mk `s ap traffic` th_sf )\n        : ( Vec u ) cfin ( _finished_mac . h c_hs th_sf )\n        : ( Vec u ) finmsg ( vec_with_cap [u] 36 )\n        ( vec_push [u] finmsg # u 20 )\n        ( _u24 finmsg 32 )\n        ( _tls_cat finmsg cfin )\n        // resumption_master_secret: transcript through our own Finished.\n        // Every NewSessionTicket the server sends from here on derives\n        // its PSK from this (see __client_take_ticket).\n        ( sha256_update . h trh finmsg )\n        : ( Vec u ) th_cf ( sha256_final . h trh )\n        = . h res_master ( derive_secret_prk mk `res master` th_cf )\n        = . h out_fin finmsg\n        = . h state 3\n        ^ 0\n    } {}\n\n    ? == t 8 {\n        // EncryptedExtensions — the negotiated ALPN. The server must\n        // pick from OUR list (RFC 7301 §3.2); anything else is a\n        // protocol violation answered with no_application_protocol.\n        : ( Vec u ) sel ( __ee_alpn m )\n        ? > ( vec_len [u] sel ) 0 {\n            ? ( _alpn_offered_packed . h alpn sel ) {\n                = . h alpn_sel sel\n            } {\n                ^ ( __cli_hs_fail h 1 120 )\n            }\n        } {}\n        // The extension a driver requires (QUIC: transport parameters).\n        ? != . h ext_want 0 {\n            : i n ( vec_len [u] m )\n            : i extlen ( _rdint m 4 2 )\n            : i ee ? > + 6 extlen n n + 6 extlen\n            : i xo ( __cli_find_ext m 6 ee . h ext_want )\n            ? < xo 0 { ^ ( __cli_hs_fail h 1 109 ) } {}\n            : i xl ( _rdint m - xo 2 2 )\n            ? > + xo xl ee { ^ ( __cli_hs_fail h 1 50 ) } {}\n            = . h ext_in_present 1\n            ( vec_clear [u] . h ext_in )\n            : ( Vec u ) xb ( bytes_slice m xo + xo xl )\n            ( bytes_extend_bytes . h ext_in xb )\n        } {}\n    } {}\n    ? == t 11 {\n        = . h cert_msg ( bytes_slice m 0 ( vec_len [u] m ) )\n    } {}\n    ? == t 15 {\n        // CertificateVerify: the transcript through Certificate (before\n        // this message), the scheme and the signature — for the verifier.\n        ? < ( vec_len [u] m ) 8 { ^ ( __cli_hs_fail h 1 50 ) } {}\n        = . h th_cert ( sha256_snapshot . h trh )\n        = . h cv_scheme ( _rdint m 4 2 )\n        : i siglen ( _rdint m 6 2 )\n        ? > + 8 siglen ( vec_len [u] m ) { ^ ( __cli_hs_fail h 1 50 ) } {}\n        = . h cv_sig ( bytes_slice m 8 + 8 siglen )\n    } {}\n    ( sha256_update . h trh m )\n    ^ 0\n}\n\n// Send an alert record (RFC 8446 §6) the way the peer can read it right\n// now: under the current write keys once there are any, in the clear\n// before that. Best effort — the connection is being torn down.\n@ __cli_say_alert inout TlsConnImpl c i desc → v {\n    ? > ( vec_len [u] . c c_key ) 0 { ( __send_alert c desc ) ^ } {}\n    : ( Vec u ) alert ( vec_with_cap [u] 2 )\n    ( vec_push [u] alert # u 2 )\n    ( vec_push [u] alert # u desc )\n    : !v TlsErr _w ( _send_plain c 21 alert )\n}\n\n// The handshake machine is the caller's binding: it goes with that scope.\n@ __cli_abort inout TlsConnImpl c TlsErr e → !v TlsErr {\n    ( _tls_close_in c )\n    ^ @ !v TlsErr { F e }\n}\n\n// Core client handshake over a socket: the record layer around `CliHs`.\n// `alpn` is the space-separated list of ALPN protocols to offer, most\n// preferred first (e.g. \"h2 http/1.1\"); empty means no ALPN extension\n// is sent. The negotiated protocol (from the server's\n// EncryptedExtensions, checked to be one we offered) is stored in\n// `c.alpn_sel`.\n@ __tls_handshake i raw s server_name s alpn ( Vec u ) sess → !TlsConn TlsErr {\n    ^ ( __tls_handshake_until raw server_name alpn sess 0 )\n}\n\n// __tls_handshake bounded by `deadline_ns` (absolute nurl_monotonic_ns;\n// 0 = none). Without one, each read waits up to 20 s — an unresponsive\n// peer fails the handshake instead of blocking the client for ever.\n// With one, the reads and writes share it: each read's timeout is what\n// is left, the writes carry it as their write deadline, and a passed\n// deadline fails the handshake (TlsRead / TlsWrite; the caller, who\n// knows the deadline, reports it as a timeout). The 20 s read timeout\n// is what the established connection keeps either way.\n@ __tls_handshake_until i raw s server_name s alpn ( Vec u ) sess i deadline_ns → !TlsConn TlsErr {\n    // The connection owns the socket from here, on every path: a connect\n    // that failed is closed with it (it used to be left open).\n    : TlsConn c__h ( _tls_conn_new raw )\n    ? != ( nurl_tcp_err_kind raw ) 0 { ^ @ !TlsConn TlsErr { F # TlsErr TlsConnect } } {}\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ? > deadline_ns 0 {\n        = . c hs_deadline_ns deadline_ns\n        ( nurl_tcp_set_write_deadline raw deadline_ns )\n    } {\n        ( nurl_tcp_set_timeout raw 20000 )\n    }\n    // The handshake machine goes with this scope, on every path out of it.\n    : CliHs hs__h ( _cli_hs_new server_name alpn sess )\n    : ~ * CliHsImpl hs ( __CliHs_ptr hs__h )\n    : !v TlsErr r ( __cli_connect . c 0 . hs 0 )\n    ?? r {\n        T _ → {\n            // The established connection keeps no handshake deadline. (A\n            // failed handshake has already closed the socket — touching\n            // `raw` then would be a use after free.)\n            ? > deadline_ns 0 {\n                = . c hs_deadline_ns 0\n                ( nurl_tcp_set_write_deadline raw 0 )\n                ( nurl_tcp_set_timeout raw 20000 )\n            } {}\n            ^ @ !TlsConn TlsErr { T c__h }\n        }\n        F e → ^ @ !TlsConn TlsErr { F e }\n    }\n}\n\n// The record layer around the machine: ClientHello out, the server's\n// flight in, Finished out, keys installed on `c`.\n@ __cli_connect inout TlsConnImpl c inout CliHsImpl hs → !v TlsErr {\n    // ── ClientHello ──\n    ( _cli_hs_start_in hs )\n    // The offered ticket stays on the connection: a resumed handshake\n    // brings no certificate and need not bring a new ticket, and\n    // tls_session_export still has to hand this one on.\n    ? == . hs offer 1 {\n        = . c tk_ticket ( bytes_slice . hs tk_ticket 0 ( vec_len [u] . hs tk_ticket ) )\n        = . c tk_psk ( bytes_slice . hs tk_psk 0 ( vec_len [u] . hs tk_psk ) )\n        = . c tk_age_add . hs tk_age_add\n        = . c tk_lifetime . hs tk_lifetime\n        = . c tk_received_ms . hs tk_received_ms\n    } {}\n    : !v TlsErr sw ( _send_plain c 22 . hs out_ch )\n    ?? sw { T _ → {} F e → { ^ ( __cli_abort c e ) } }\n\n    // ── ServerHello ──\n    : !( Vec u ) TlsErr shr ( __next_hs c )\n    : ( Vec u ) sh ?? shr { T m → m F e → { ^ ( __cli_abort c e ) } }\n    : i shrc ( _cli_hs_server_hello_in hs sh )\n    ? != shrc 0 {\n        ( __cli_say_alert c shrc )\n        ^ ( __cli_abort c ( __cli_hs_errk hs ) )\n    } {}\n    = . c version . hs version\n    = . c cipher . hs cipher\n\n    // ── TLS 1.2 fallback ──\n    // The 1.2 path owns what it is handed, so it gets copies of the\n    // machine's ephemerals and the hellos, and the machine goes.\n    ? == . c version 12 {\n        : ( Vec u ) priv ( bytes_slice . hs x_priv 0 ( vec_len [u] . hs x_priv ) )\n        : ( Vec u ) cpub ( bytes_slice . hs x_pub 0 ( vec_len [u] . hs x_pub ) )\n        : ( Vec u ) random ( bytes_slice . hs random 0 ( vec_len [u] . hs random ) )\n        : ( Vec u ) sessid ( bytes_slice . hs sessid 0 ( vec_len [u] . hs sessid ) )\n        : ( Vec u ) ch ( bytes_slice . hs out_ch 0 ( vec_len [u] . hs out_ch ) )\n        : ( Vec u ) tr ( bytes_slice . hs out_ch 0 ( vec_len [u] . hs out_ch ) )\n        ( _tls_cat tr sh )\n        = . c kx_p256 ( bytes_slice . hs p256_priv 0 ( vec_len [u] . hs p256_priv ) )\n        // ALPN under 1.2 is answered in the ServerHello itself. Without\n        // this a load balancer that picked h2 there was spoken to in\n        // HTTP/1.1 — and every request to it failed.\n        : ( Vec u ) sel12 ( __sh_alpn sh )\n        ? & > ( vec_len [u] sel12 ) 0 ( _alpn_offered_packed . hs alpn sel12 ) {\n            = . c alpn_sel sel12\n        } {}\n        ^ ( __tls12_handshake c sh priv cpub random sessid ch tr )\n    } {}\n    = . c kx_group . hs kx_group\n    = . c resumed . hs resumed\n\n    // handshake keys: the client writes under c_hs, reads the server\n    // under s_hs\n    ( _set_keys c 0 . hs s_hs )\n    ( _set_keys c 1 . hs c_hs )\n    = . c enc_read 1\n\n    // ── server flight: EE, Certificate, CertVerify, Finished ──\n    : ~ i rc 0\n    ~ & == rc 0 != . hs state 3 {\n        : !( Vec u ) TlsErr mr ( __next_hs c )\n        ?? mr {\n            F e → { ^ ( __cli_abort c e ) }\n            T msg → {\n                = rc ( _cli_hs_message_in hs msg )\n            }\n        }\n    }\n    ? != rc 0 {\n        ( __cli_say_alert c rc )\n        ^ ( __cli_abort c ( __cli_hs_errk hs ) )\n    } {}\n    // what the verifier and the callers read off the connection\n    = . c cert_msg . hs cert_msg\n    = . hs cert_msg ( vec_new [u] )\n    = . c cv_sig . hs cv_sig\n    = . hs cv_sig ( vec_new [u] )\n    = . c th_cert . hs th_cert\n    = . hs th_cert ( vec_new [u] )\n    = . c cv_scheme . hs cv_scheme\n    = . c alpn_sel . hs alpn_sel\n    = . hs alpn_sel ( vec_new [u] )\n\n    // ── client Finished (under handshake keys) ──\n    // change_cipher_spec for middlebox compatibility\n    : ( Vec u ) ccs ( vec_with_cap [u] 1 )\n    ( vec_push [u] ccs # u 1 )\n    : !v TlsErr cw ( _send_plain c 20 ccs )\n    ?? cw { T _ → {} F _ → {} }\n    : !v TlsErr fw ( __send_encrypted c 22 . hs out_fin )\n    ?? fw { T _ → {} F _ → {} }\n\n    // switch to application traffic keys\n    ( _set_keys c 0 . hs s_ap )\n    ( _set_keys c 1 . hs c_ap )\n    = . c established 1\n    = . c res_master . hs res_master\n    = . hs res_master ( vec_new [u] )\n    ( _tls_ktls_auto c )\n    ^ @ !v TlsErr { T 0 }\n}\n\n// Upgrade an already-connected fd to TLS (no ALPN). Insecure: does not\n// verify the certificate (see tls_attach_verify).\n@ tls_attach i raw s server_name → !TlsConn TlsErr {\n    : ( Vec u ) nosess ( vec_new [u] )\n    : !TlsConn TlsErr r ( __tls_handshake raw server_name `` nosess )\n    ^ r\n}\n\n// Like tls_attach but offers ALPN protocols (\"h2\" or a preference list\n// \"h2 http/1.1\"). After a successful handshake the negotiated protocol is\n// readable via tls_alpn_selected (empty if the server declined ALPN).\n// Insecure variant.\n@ tls_attach_alpn i raw s server_name s alpn → !TlsConn TlsErr {\n    : ( Vec u ) nosess ( vec_new [u] )\n    : !TlsConn TlsErr r ( __tls_handshake raw server_name alpn nosess )\n    ^ r\n}\n\n// tls_attach with a resumption offer: `sess` is what tls_session_export\n// returned from an earlier connection to the same server. If the server\n// takes it the handshake is the abbreviated PSK one (no certificate, one\n// round trip, no signature to verify) and tls_is_resumed answers T;\n// otherwise this is exactly tls_attach. Insecure variant — see\n// tls_connect_resume for the verifying one.\n@ tls_attach_resume i raw s server_name ( Vec u ) sess → !TlsConn TlsErr {\n    ^ ( __tls_handshake raw server_name `` sess )\n}\n\n// Unverified connect with a resumption offer (the tls_connect_insecure\n// of resumption — pinned / self-signed / test servers).\n@ tls_connect_insecure_resume s host i port s server_name ( Vec u ) sess → !TlsConn TlsErr {\n    : i raw ( nurl_tcp_connect host port )\n    ^ ( tls_attach_resume raw server_name sess )\n}\n\n// Verifying connect with a resumption offer. A resumed connection is\n// authenticated by the PSK (the ticket's issuer is the server verified\n// when the session was made); a declined offer falls back to the full\n// handshake and the usual chain / hostname verification.\n@ tls_connect_resume s host i port s server_name ( Vec u ) sess → !TlsConn TlsErr {\n    : i raw ( nurl_tcp_connect host port )\n    : !TlsConn TlsErr r ( tls_attach_resume raw server_name sess )\n    ^ ( __verify_conn r server_name )\n}\n\n// The ALPN protocol the server selected, as an owned String (\"\" if none).\n// The key-exchange group the server selected, as its IANA number:\n//\n//   4588  X25519MLKEM768   hybrid, post-quantum + X25519\n//     29  x25519\n//     23  secp256r1\n//      0  not negotiated yet, or a TLS 1.2 handshake\n//\n// Worth checking rather than assuming: offering the hybrid group does\n// not mean getting it, and the difference is the whole point. A server\n// that has not deployed ML-KEM silently falls back to X25519, and the\n// handshake looks identical from every other angle.\n@ tls_group TlsConn c__h → i {\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ . c kx_group\n}\n\n// The SignatureScheme of this connection's CertificateVerify: on a client,\n// what the server signed with; on a server, what it chose to sign with\n// (ecdsa_secp256r1_sha256 0x0403, rsa_pss_rsae_sha256 0x0804, mldsa44/65/87\n// 0x0904–0x0906). 0 on a resumed handshake, which carries no certificate.\n@ tls_cv_scheme TlsConn c__h → i {\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ . c cv_scheme\n}\n\n// What a client captured for the verifier (lent; empty on a resumed\n// handshake): the raw Certificate message, the CertificateVerify\n// signature, and the transcript hash through the Certificate —\n// `tls_cv_verify ( tls_cert_msg c ) ( tls_cv_scheme c ) ( tls_cv_sig c )\n// ( tls_th_cert c )` re-checks the server's proof of key possession.\n@ tls_cert_msg TlsConn c__h → ( Vec u ) { ^ . ( __TlsConn_ptr c__h ) cert_msg }\n\n@ tls_cv_sig TlsConn c__h → ( Vec u ) { ^ . ( __TlsConn_ptr c__h ) cv_sig }\n\n@ tls_th_cert TlsConn c__h → ( Vec u ) { ^ . ( __TlsConn_ptr c__h ) th_cert }\n\n// T when the negotiated group carries a post-quantum component, so the\n// session's forward secrecy survives a future quantum adversary\n// recording it today.\n@ tls_is_post_quantum TlsConn c__h → b {\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ == . c kx_group 4588\n}\n\n// True iff the negotiated ALPN protocol is exactly `proto` — the\n// allocation-free form of tls_alpn_selected for the per-connection\n// dispatch question (\"is this h2?\").\n@ tls_alpn_is TlsConn c__h s proto → b {\n    : ( Slice u ) proto_v ( slice_of_str proto )\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    : i n ( vec_len [u] . c alpn_sel )\n    ? != n ( nurl_str_len proto ) { ^ F } {}\n    : *u p ( vec_data [u] . c alpn_sel )\n    : ~ i k 0\n    ~ < k n {\n        ? != # i . p k ( slice_byte proto_v k ) { ^ F } {}\n        = k + k 1\n    }\n    ^ T\n}\n\n@ tls_alpn_selected TlsConn c__h → String {\n    : *TlsConnImpl c ( __TlsConn_ptr c__h )\n    : String s ( string_new )\n    : i n ( vec_len [u] . c alpn_sel )\n    : ~ i k 0\n    ~ < k n {\n        ?? ( vec_get [u] . c alpn_sel k ) { T b → ( string_push_char s # i b ) F _ → {} }\n        = k + k 1\n    }\n    ^ s\n}\n\n// Establish a verified TLS 1.3 connection (the secure default): complete\n// the handshake, then verify the server's CertificateVerify signature,\n// the certificate chain up to the system trust store, the validity\n// window, and that `server_name` matches the leaf SANs. On any failure\n// the connection is closed and TlsBadCert is returned.\n// TLS 1.2 verification: the ServerKeyExchange signature (authenticating\n// the ephemeral key to the leaf cert) + the certificate chain.\n@ __verify12 inout TlsConnImpl c s hostname → i {\n    : X509 leaf ( tls_leaf_cert . c cert_msg 1 )\n    ? ! . leaf ok { ^ 2 } {}\n    : i sk ( tls12_ske_verify leaf . c cv_scheme . c cv_sig . c th_cert )\n    ? != sk 0 { ^ sk } {}\n    ^ ( tls_chain_verify . c cert_msg 1 hostname )\n}\n\n@ tls_connect s host i port s server_name → !TlsConn TlsErr {\n    : !TlsConn TlsErr r ( tls_connect_insecure host port server_name )\n    ^ ( __verify_conn r server_name )\n}\n\n// Verifying counterpart of `tls_attach`: upgrade an already-connected\n// socket to TLS and verify the chain / hostname against the system trust\n// store (the secure default for STARTTLS-style upgrades).\n@ tls_attach_verify i raw s server_name → !TlsConn TlsErr {\n    : !TlsConn TlsErr r ( tls_attach raw server_name )\n    ^ ( __verify_conn r server_name )\n}\n\n// Verifying counterpart of tls_attach_alpn: offer an ALPN protocol AND\n// verify the chain / hostname. The negotiated protocol is then readable\n// with tls_alpn_selected.\n@ tls_attach_alpn_verify i raw s server_name s alpn → !TlsConn TlsErr {\n    : !TlsConn TlsErr r ( tls_attach_alpn raw server_name alpn )\n    ^ ( __verify_conn r server_name )\n}\n\n// Every client knob in one call: upgrade an already-connected socket to\n// TLS offering the ALPN list `alpn` (\"\" = none) AND the resumption\n// session `sess` (empty = none), verifying the chain / hostname when\n// `verify` is non-zero. The one-knob variants above are this with a\n// blank somewhere; an HTTP client that wants to resume a session on the\n// same connection it negotiates HTTP/2 over needs all of them at once.\n@ tls_attach_full i raw s server_name s alpn ( Vec u ) sess i verify → !TlsConn TlsErr {\n    ^ ( tls_attach_full_until raw server_name alpn sess verify 0 )\n}\n\n// tls_attach_full with the whole handshake bounded by `deadline_ns`, an\n// absolute nurl_monotonic_ns (std/time.nu's monotonic_ns); 0 = none,\n// which is tls_attach_full. A deadline that passes fails the handshake.\n@ tls_attach_full_until i raw s server_name s alpn ( Vec u ) sess i verify i deadline_ns → !TlsConn TlsErr {\n    : !TlsConn TlsErr r ( __tls_handshake_until raw server_name alpn sess deadline_ns )\n    ? != verify 0 { ^ ( __verify_conn r server_name ) } {}\n    ^ r\n}\n\n// tls_attach_full over a fresh TCP connection to host:port.\n@ tls_connect_full s host i port s server_name s alpn ( Vec u ) sess i verify → !TlsConn TlsErr {\n    : i raw ( nurl_tcp_connect host port )\n    ^ ( tls_attach_full raw server_name alpn sess verify )\n}\n\n// Shared post-handshake verification used by both tls_connect and\n// tls_attach_verify: check the certificate (TLS 1.3 CertificateVerify or\n// TLS 1.2 ServerKeyExchange sig + chain + hostname) and close on failure.\n@ __verify_conn sink ! TlsConn TlsErr r s server_name → !TlsConn TlsErr {\n    ?? r {\n        F e → { ^ @ !TlsConn TlsErr { F e } }\n        T h → {\n            : ~ * TlsConnImpl c ( __TlsConn_ptr h )\n            // A resumed connection carries no certificate: the PSK it was\n            // established from authenticates the server as the issuer of\n            // the ticket, which was verified when that session was made.\n            : i rc ? == . c resumed 1 0 ? == . c version 12 ( __verify12 . c 0 server_name ) ( tls_cert_verify . c cert_msg . c cv_scheme . c cv_sig . c th_cert server_name )\n            ? == rc 0 {\n                ^ @ !TlsConn TlsErr { T h }\n            } {\n                ( _tls_close_in . c 0 )\n                ^ @ !TlsConn TlsErr { F # TlsErr TlsBadCert }\n            }\n        }\n    }\n}\n\n// Compare a Finished message's verify_data (bytes 4..36) against expected.\n@ _cmp_finished ( Vec u ) msg ( Vec u ) expect → b {\n    ? < ( vec_len [u] msg ) 36 { ^ F } {}\n    : ~ i diff 0\n    : ~ i k 0\n    ~ < k 32 { = diff | diff ^^ ( _t_bget msg + 4 k ) ( _t_bget expect k ) = k + k 1 }\n    ^ == diff 0\n}\n\n// Cleanup paths on early/late handshake failure.\n@ __fail inout TlsConnImpl c TlsErr e → !v TlsErr {\n    ( _tls_close_in c )\n    ^ @ !v TlsErr { F e }\n}\n\n// ── application data ──────────────────────────────────────────────\n//\n// A TLS record carries at most 2^14 bytes of plaintext (RFC 8446 §5.1,\n// same limit in 1.2): peers MUST reject anything larger, and past 65535\n// the record header's u16 length field wraps outright. Split\n// application data into ≤16384-byte records.\n@ tls_write TlsConn c__h ( Vec u ) data → !v TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_write_in . c 0 data )\n}\n\n@ _tls_write_in inout TlsConnImpl c ( Vec u ) data → !v TlsErr {\n    ?? ( _tls_flush_control c 1 ) { T _ → {} F error → { ^ @ !v TlsErr { F error } } }\n    ? != . c closed 0 { ^ @ !v TlsErr { F TlsClosed } } {}\n    : i n ( vec_len [u] data )\n    ? == . c version 12 {\n        ? <= n 16384 { ^ ( __send_record_12 c 23 data ) } {}\n        : ~ i off 0\n        ~ < off n {\n            : ~ i hi + off 16384\n            ? > hi n { = hi n } {}\n            : ( Vec u ) part ( bytes_slice data off hi )\n            ?? ( __send_record_12 c 23 part ) { T _ → {} F e → { ^ @ !v TlsErr { F e } } }\n            = off hi\n        }\n        ^ @ !v TlsErr { T 0 }\n    } {}\n    ^ ( _tls_write_records c 1 data data n T )\n}\n\n// `head`‖`body`[0, n) (or `data` alone when `single`) as ≤16384-byte\n// application records under direction `dir`'s keys, sealed in place in\n// txbuf and written out every 64 KB — so a large write is a few\n// syscalls, and txbuf never holds more than one such batch.\n@ _tls_write_records inout TlsConnImpl c i dir ( Vec u ) head ( Vec u ) body i n b single → !v TlsErr {\n    ? != 0 ( _tls_ktls_of c dir ) {\n        // The kernel cuts and seals the records: the plaintext goes to\n        // the socket as it is, both buffers in one sendmsg.\n        : b written ? single ( _tls_sock_write . c fd head ) ( _tls_sock_write2 . c fd head body )\n        ? ! written { = . c closed 1 ^ @ !v TlsErr { F TlsWrite } } {}\n        ^ @ !v TlsErr { T 0 }\n    } {}\n    : ( Vec u ) buf ( _tls_tx_take c )\n    : ~ i off 0\n    ~ < off n {\n        : ~ i hi + off 16384\n        ? > hi n { = hi n } {}\n        ? single { ( _tls_rec_range_to c buf dir 23 head off hi ) } { ( _tls_rec_pair_to c buf dir 23 head body off hi ) }\n        = off hi\n        ? | >= off n >= ( vec_len [u] buf ) 65536 {\n            : !v TlsErr r ( _tls_tx_flush c buf )\n            ?? r { T _ → {} F e → { ( _tls_tx_put c buf ) ^ @ !v TlsErr { F e } } }\n        } {}\n    }\n    ( _tls_tx_put c buf )\n    ^ @ !v TlsErr { T 0 }\n}\n\n// Bytes [lo, hi) of the logical concatenation `head`‖`body`, as a fresh\n// Vec — the record cutter behind tls_write2 / tls_server_write2. One\n// memcpy per source touched; a range inside a single source is one.\n// One spare byte of capacity: the sealers push the inner content-type\n// byte onto this same Vec, and that must not be a reallocation.\n@ _tls_pair_slice ( Vec u ) head ( Vec u ) body i lo i hi → ( Vec u ) {\n    : i hn ( vec_len [u] head )\n    : i bn ( vec_len [u] body )\n    : ~ i a lo\n    : ~ i z hi\n    ? < a 0 { = a 0 } {}\n    ? > z + hn bn { = z + hn bn } {}\n    ? < z a { = z a } {}\n    : ( Vec u ) out ( vec_with_cap [u] + 1 - z a )\n    ? < a hn {\n        : i h_hi ? < z hn z hn\n        : *u hp ( vec_data [u] head )\n        ( bytes_extend_raw out # s + # i hp a - h_hi a )\n    } {}\n    ? > z hn {\n        : i b_lo ? > a hn - a hn 0\n        : *u bp ( vec_data [u] body )\n        ( bytes_extend_raw out # s + # i bp b_lo - - z hn b_lo )\n    } {}\n    ^ out\n}\n\n// Encode application records once for a nonblocking FIFO writer. The\n// returned bytes own their storage; advancing the sequence belongs here,\n// never in a retry of a partial socket write. No socket I/O occurs.\n@ tls_prepare_write TlsConn c__h ( Vec u ) data → !( Vec u ) TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_prepare_write_in . c 0 data )\n}\n\n@ _tls_prepare_write_in inout TlsConnImpl c ( Vec u ) data → !( Vec u ) TlsErr {\n    ? | != . c closed 0 != . c established 1 {\n        ^ @ !( Vec u ) TlsErr { F TlsClosed }\n    } {}\n    ? & != . c fatal_alert 0 > ( vec_len [u] data ) 0 { ^ @ !( Vec u ) TlsErr { F TlsProtocol } } {}\n    : ( Vec u ) wire ( vec_new [u] )\n    ( _tls_control_to c wire 1 )\n    : ~ i offset 0\n    : i size ( vec_len [u] data )\n    ~ < offset size {\n        : i end ? < - size offset 16384 size + offset 16384\n        ? == . c version 12 {\n            : ( Vec u ) part ( bytes_slice data offset end )\n            ( _tls_record12_to c wire 23 part )\n        } { ( _tls_rec_range_to c wire 1 23 data offset end ) }\n        = offset end\n    }\n    ^ @ !( Vec u ) TlsErr { T wire }\n}\n\n// Pair variant of tls_prepare_write: records cut from `head`‖`body` are\n// sealed straight into `out`, the caller's ciphertext FIFO. No socket I/O.\n@ tls_prepare_write2_to TlsConn c__h ( Vec u ) out ( Vec u ) head ( Vec u ) body → !v TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_prepare_write2_to_in . c 0 out head body )\n}\n\n@ _tls_prepare_write2_to_in inout TlsConnImpl c ( Vec u ) out ( Vec u ) head ( Vec u ) body → !v TlsErr {\n    ? | != . c closed 0 != . c established 1 { ^ @ !v TlsErr { F TlsClosed } } {}\n    : i n + ( vec_len [u] head ) ( vec_len [u] body )\n    ? & != . c fatal_alert 0 > n 0 { ^ @ !v TlsErr { F TlsProtocol } } {}\n    ( _tls_control_to c out 1 )\n    : ~ i off 0\n    ~ < off n {\n        : ~ i hi + off 16384\n        ? > hi n { = hi n } {}\n        ? == . c version 12 {\n            : ( Vec u ) part ( _tls_pair_slice head body off hi )\n            ( _tls_record12_to c out 23 part )\n        } { ( _tls_rec_pair_to c out 1 23 head body off hi ) }\n        = off hi\n    }\n    ^ @ !v TlsErr { T 0 }\n}\n\n// Two-buffer variant of tls_write (client side of tcp_write_all2):\n// records are cut from `head`‖`body` without joining the two first.\n// TLS 1.3 assembles each record's plaintext straight from the pair;\n// TLS 1.2 hands the AEAD a plaintext Vec, so it cuts one per record\n// (the same one bytes_slice cut before).\n@ tls_write2 TlsConn c__h ( Vec u ) head ( Vec u ) body → !v TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_write2_in . c 0 head body )\n}\n\n@ _tls_write2_in inout TlsConnImpl c ( Vec u ) head ( Vec u ) body → !v TlsErr {\n    ?? ( _tls_flush_control c 1 ) { T _ → {} F error → { ^ @ !v TlsErr { F error } } }\n    ? != . c closed 0 { ^ @ !v TlsErr { F TlsClosed } } {}\n    : i n + ( vec_len [u] head ) ( vec_len [u] body )\n    ? == . c version 12 {\n        : ~ i off 0\n        ~ < off n {\n            : ~ i hi + off 16384\n            ? > hi n { = hi n } {}\n            : ( Vec u ) part ( _tls_pair_slice head body off hi )\n            ?? ( __send_record_12 c 23 part ) { T _ → {} F e → { ^ @ !v TlsErr { F e } } }\n            = off hi\n        }\n        ^ @ !v TlsErr { T 0 }\n    } {}\n    ^ ( _tls_write_records c 1 head body n F )\n}\n\n// Read up to `max` decrypted application bytes. Returns [] on clean EOF\n// (close_notify). Post-handshake messages (tickets, key updates) are\n// consumed transparently.\n@ tls_read TlsConn c__h i max → !( Vec u ) TlsErr {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ^ ( _tls_read_in . c 0 max )\n}\n\n@ _tls_read_in inout TlsConnImpl c i max → !( Vec u ) TlsErr {\n    : ( Vec u ) out ( vec_new [u] )\n    : !i TlsErr r ( _tls_read_into_in c 0 out max )\n    ?? r { T _ → ^ @ !( Vec u ) TlsErr { T out } F e → ^ @ !( Vec u ) TlsErr { F e } }\n}\n\n// Say close_notify (best effort) and close the socket. Safe to repeat;\n// the connection's memory goes with its last owner.\n@ tls_close TlsConn c__h → v {\n    : ~ * TlsConnImpl c ( __TlsConn_ptr c__h )\n    ( _tls_close_in . c 0 )\n}\n\n@ _tls_close_in inout TlsConnImpl c → v {\n    ? != . c fatal_alert 0 {\n        : !v TlsErr sent ( _tls_flush_control c 1 )\n        ?? sent { T _ → {} F _ → {} }\n    } {}\n    ? == . c closed 0 {\n        // best-effort close_notify alert (encrypted if established)\n        ? == . c established 1 {\n            : ( Vec u ) alert ( vec_with_cap [u] 2 )\n            ( vec_push [u] alert # u 1 )\n            ( vec_push [u] alert # u 0 )\n            : !v TlsErr _w ? == . c version 12 ( __send_record_12 c 21 alert ) ( __send_encrypted c 21 alert )\n        } {}\n        = . c closed 1\n    } {}\n    // The socket goes now; the state goes with the handle's last owner.\n    ? != . c owns_fd 0 { ( nurl_tcp_close . c fd ) = . c owns_fd 0 } {}\n}\n\n// ══════════════════════════════════════════════════════════════════\n//  TLS 1.2 fallback (RFC 5246 + RFC 5288 GCM + RFC 7905 ChaCha20)\n// ══════════════════════════════════════════════════════════════════\n\n// TLS 1.2 PRF (P_SHA256): PRF(secret, label, seed) over HMAC-SHA-256.\n@ __prf12 ( Vec u ) secret s label ( Vec u ) seed i outlen → ( Vec u ) {\n    : ( Vec u ) fs ( vec_new [u] )\n    ( bytes_extend_str fs label )\n    ( bytes_extend_bytes fs seed )\n    : ( Vec u ) out ( vec_with_cap [u] ? > outlen 0 outlen 1 )\n    : ~ ( Vec u ) a ( bytes_slice fs 0 ( vec_len [u] fs ) )\n    ~ < ( vec_len [u] out ) outlen {\n        : ( Vec u ) anew ( hmac_sha256_pure secret a )\n        = a anew\n        : ( Vec u ) cat ( bytes_slice a 0 ( vec_len [u] a ) )\n        ( bytes_extend_bytes cat fs )\n        : ( Vec u ) chunk ( hmac_sha256_pure secret cat )\n        : ~ i j 0\n        ~ & < j 32 < ( vec_len [u] out ) outlen { ( vec_push [u] out # u ( _t_bget chunk j ) ) = j + j 1 }\n    }\n    ^ out\n}\n\n// TLS 1.2 record AAD: seq(8) || type(1) || 0x0303 || plaintext_len(2).\n@ __aad12 i seq i rtype i ptlen → ( Vec u ) {\n    : ( Vec u ) a ( vec_with_cap [u] 13 )\n    : ~ i k 0\n    ~ < k 8 { ( vec_push [u] a # u & >> seq * 8 - 7 k 255 ) = k + k 1 }\n    ( vec_push [u] a # u rtype )\n    ( vec_push [u] a # u 3 )\n    ( vec_push [u] a # u 3 )\n    ( _tls_u16 a ptlen )\n    ^ a\n}\n\n// AES-GCM nonce: 4-byte salt || 8-byte explicit (= seq).\n@ __nonce12_aes ( Vec u ) iv4 i seq → ( Vec u ) {\n    : ( Vec u ) n ( vec_with_cap [u] 12 )\n    : ~ i k 0\n    ~ < k 4 { ( vec_push [u] n # u ( _t_bget iv4 k ) ) = k + k 1 }\n    : ~ i b 0\n    ~ < b 8 { ( vec_push [u] n # u & >> seq * 8 - 7 b 255 ) = b + b 1 }\n    ^ n\n}\n\n// ChaCha20 nonce (RFC 7905): 12-byte IV XOR (0^4 || seq).\n@ __nonce12_chacha ( Vec u ) iv12 i seq → ( Vec u ) {\n    : ( Vec u ) n ( vec_with_cap [u] 12 )\n    : ~ i k 0\n    ~ < k 12 { ( vec_push [u] n # u ( _t_bget iv12 k ) ) = k + k 1 }\n    : ~ i b 0\n    ~ < b 8 {\n        : i sb & >> seq * 8 - 7 b 255\n        ( vec_set [u] n + 4 b # u ^^ ( _t_bget n + 4 b ) sb )\n        = b + b 1\n    }\n    ^ n\n}\n\n// Send one TLS 1.2 record of `content` (real content type `rtype`).\n@ _tls_record12_to inout TlsConnImpl c ( Vec u ) out i rtype ( Vec u ) content → v {\n    : i ptlen ( vec_len [u] content )\n    : ( Vec u ) aad ( __aad12 . c c_seq rtype ptlen )\n    : ( Vec u ) body ( vec_new [u] )\n    ? == . c cipher 1 {\n        : ( Vec u ) nonce ( __nonce12_aes . c c_iv . c c_seq )\n        : ( Vec u ) sealed ( aes_gcm_seal . c c_gk nonce aad content )\n        // explicit nonce (= seq) is prepended on the wire\n        : ~ i b 0\n        ~ < b 8 { ( vec_push [u] body # u & >> . c c_seq * 8 - 7 b 255 ) = b + b 1 }\n        ( _tls_cat body sealed )\n    } {\n        : ( Vec u ) nonce ( __nonce12_chacha . c c_iv . c c_seq )\n        : ( Vec u ) sealed ( aead_encrypt . c c_key nonce aad content )\n        ( _tls_cat body sealed )\n    }\n    ( vec_push [u] out # u rtype )\n    ( vec_push [u] out # u 3 )\n    ( vec_push [u] out # u 3 )\n    ( _tls_u16 out ( vec_len [u] body ) )\n    ( _tls_cat out body )\n    = . c c_seq + . c c_seq 1\n}\n\n@ __send_record_12 inout TlsConnImpl c i rtype ( Vec u ) content → !v TlsErr {\n    : ( Vec u ) record ( vec_new [u] )\n    ( _tls_record12_to c record rtype content )\n    : b written ( _tls_sock_write . c fd record )\n    ? ! written { = . c closed 1 } {}\n    ^ ? written @ !v TlsErr { T 0 } @ !v TlsErr { F TlsWrite }\n}\n\n// Decrypt a TLS 1.2 record body (real type `rtype`) → plaintext.\n@ __decrypt_record_12 inout TlsConnImpl c i rtype ( Vec u ) body → ?( Vec u ) {\n    : ?( Vec u ) pt ? == . c cipher 1 {\n        : i explen 8\n        : ( Vec u ) nonce ( vec_with_cap [u] 12 )\n        : ~ i k 0\n        ~ < k 4 { ( vec_push [u] nonce # u ( _t_bget . c s_iv k ) ) = k + k 1 }\n        : ~ i e 0\n        ~ < e 8 { ( vec_push [u] nonce # u ( _t_bget body e ) ) = e + e 1 }\n        : ( Vec u ) ct ( bytes_slice body 8 ( vec_len [u] body ) )\n        : i ptlen - ( vec_len [u] ct ) 16\n        : ( Vec u ) aad ( __aad12 . c s_seq rtype ptlen )\n        : ?( Vec u ) r ( aes_gcm_open . c s_gk nonce aad ct )\n        r\n    } {\n        : ( Vec u ) nonce ( __nonce12_chacha . c s_iv . c s_seq )\n        : i ptlen - ( vec_len [u] body ) 16\n        : ( Vec u ) aad ( __aad12 . c s_seq rtype ptlen )\n        : ?( Vec u ) r ( aead_decrypt . c s_key nonce aad body )\n        r\n    }\n    = . c s_seq + . c s_seq 1\n    ^ pt\n}\n\n// Derive the TLS 1.2 key block and install client/server write keys.\n@ __tls12_setkeys inout TlsConnImpl c ( Vec u ) master ( Vec u ) crand ( Vec u ) srand → v {\n    : ( Vec u ) seed ( vec_new [u] )\n    ( bytes_extend_bytes seed srand )\n    ( bytes_extend_bytes seed crand )\n    : i klen ? == . c cipher 1 16 32\n    : i ivlen ? == . c cipher 1 4 12\n    : i need + * 2 klen * 2 ivlen\n    : ( Vec u ) kb ( __prf12 master `key expansion` seed need )\n    : ( Vec u ) ck ( bytes_slice kb 0 klen )\n    : ( Vec u ) sk ( bytes_slice kb klen * 2 klen )\n    : ( Vec u ) civ ( bytes_slice kb * 2 klen + * 2 klen ivlen )\n    : ( Vec u ) siv ( bytes_slice kb + * 2 klen ivlen + * 2 klen * 2 ivlen )\n    = . c c_gk ( __tls_gk . c cipher ck )\n    = . c s_gk ( __tls_gk . c cipher sk )\n    = . c c_key ck\n    = . c s_key sk\n    = . c c_iv civ\n    = . c s_iv siv\n    = . c c_seq 0\n    = . c s_seq 0\n}\n\n// Drive the TLS 1.2 handshake after ServerHello. Consumes all the passed\n// buffers. On success returns the established (encrypted) connection;\n// the certificate chain + ServerKeyExchange signature material are\n// captured on `c` for the verifier (cv_sig / cv_scheme / th_cert).\n@ __tls12_handshake inout TlsConnImpl c ( Vec u ) sh ( Vec u ) priv ( Vec u ) cpub ( Vec u ) random ( Vec u ) sessid ( Vec u ) ch ( Vec u ) tr → !v TlsErr {\n    : ( Vec u ) srand ( bytes_slice sh 6 38 )\n    // M1: we always offer TLS 1.3 in supported_versions, so negotiating 1.2\n    // here means a possible forced downgrade — abort on the RFC 8446 sentinel.\n    ? ( __downgrade_sentinel srand ) {\n        ^ ( __fail c # TlsErr TlsProtocol )\n    } {}\n\n    // ── server flight 1: Certificate, ServerKeyExchange, ServerHelloDone ──\n    : ~ ( Vec u ) spub ( vec_new [u] )\n    : ~ i kx_curve 29  // named_curve from ServerKeyExchange: 29 x25519, 23 secp256r1\n    : ~ i err 0\n    : ~ i done 0\n    ~ & == done 0 == err 0 {\n        : !( Vec u ) TlsErr mr ( __next_hs c )\n        ?? mr {\n            F _ → { = err 1 }\n            T msg → {\n                : i t ( _t_bget msg 0 )\n                ? == t 11 {\n                    = . c cert_msg ( bytes_slice msg 0 ( vec_len [u] msg ) )\n                } {}\n                ? == t 12 {\n                    // ServerKeyExchange: curve_type(1) curve(2) pklen(1) pk sig_scheme(2) siglen(2) sig\n                    = kx_curve ( _rdint msg 5 2 )\n                    : i pklen ( _t_bget msg 7 )\n                    = spub ( bytes_slice msg 8 + 8 pklen )\n                    : i sp + 8 pklen\n                    = . c cv_scheme ( _rdint msg sp 2 )\n                    : i siglen ( _rdint msg + sp 2 2 )\n                    = . c cv_sig ( bytes_slice msg + sp 4 + + sp 4 siglen )\n                    // signed data = client_random || server_random || ecdhe_params\n                    : ( Vec u ) signed ( vec_new [u] )\n                    ( bytes_extend_bytes signed random )\n                    ( bytes_extend_bytes signed srand )\n                    : ( Vec u ) eparams ( bytes_slice msg 4 + 8 pklen )\n                    ( _tls_cat signed eparams )\n                    = . c th_cert signed\n                } {}\n                ? == t 14 { = done 1 } {}\n                ( _tls_cat tr msg )\n            }\n        }\n    }\n    ? | == err 1 == ( vec_len [u] spub ) 0 {\n        ^ ( __fail c # TlsErr TlsHandshake )\n    } {}\n\n    // ── ECDHE + master secret ──\n    // Curve chosen by the server's ServerKeyExchange: secp256r1 (P-256,\n    // 23) or x25519 (29). Stock TLS-1.2 servers (e.g. OpenSSL with the\n    // default ssl_ecdh_curve=prime256v1) pick P-256, so both are handled.\n    : i is_p256 == kx_curve 23\n    : ( Vec u ) ckpub ? is_p256 ( p256_ecdh_keygen . c kx_p256 ) cpub\n    : ( Vec u ) pms ? is_p256 ( p256_ecdh_shared . c kx_p256 spub ) ( x25519 priv spub )\n    : ( Vec u ) cs_seed ( vec_new [u] )\n    ( bytes_extend_bytes cs_seed random )\n    ( bytes_extend_bytes cs_seed srand )\n    : ( Vec u ) master ( __prf12 pms `master secret` cs_seed 48 )\n    ( __tls12_setkeys c master random srand )\n\n    // ── ClientKeyExchange (plaintext handshake) ──\n    // body = pubkey_len(1) || pubkey ; handshake length = 1 + len(pubkey)\n    : i cklen ( vec_len [u] ckpub )\n    : ( Vec u ) cke ( vec_with_cap [u] + cklen 5 )\n    ( vec_push [u] cke # u 16 )\n    ( _u24 cke + cklen 1 )\n    ( vec_push [u] cke # u cklen )\n    ( _tls_cat cke ckpub )\n    : !v TlsErr ckw ( _send_plain c 22 cke )\n    ?? ckw { T _ → {} F _ → {} }\n    ( _tls_cat tr cke )\n\n    // ── ChangeCipherSpec + client Finished (encrypted) ──\n    : ( Vec u ) ccs ( vec_with_cap [u] 1 )\n    ( vec_push [u] ccs # u 1 )\n    : !v TlsErr cw ( _send_plain c 20 ccs )\n    ?? cw { T _ → {} F _ → {} }\n\n    : ( Vec u ) th_c ( sha256_pure tr )\n    : ( Vec u ) cfin_vd ( __prf12 master `client finished` th_c 12 )\n    : ( Vec u ) finmsg ( vec_with_cap [u] 16 )\n    ( vec_push [u] finmsg # u 20 )\n    ( _u24 finmsg 12 )\n    ( _tls_cat finmsg cfin_vd )\n    : !v TlsErr fw ( __send_record_12 c 22 finmsg )\n    ?? fw { T _ → {} F _ → {} }\n    ( _tls_cat tr finmsg )\n\n    // ── server ChangeCipherSpec + Finished ──\n    : ( Vec u ) th_s ( sha256_pure tr )\n    : ( Vec u ) sfin_exp ( __prf12 master `server finished` th_s 12 )\n    : ~ i serr 0\n    : ~ i sdone 0\n    ~ & == sdone 0 == serr 0 {\n        : !TlsRecord TlsErr rr ( _read_record c )\n        ?? rr {\n            F _ → { = serr 1 }\n            T rec → {\n                ? == . rec rtype 20 {\n                } {\n                    ?? ( __decrypt_record_12 c . rec rtype . rec body ) {\n                        T inner → {\n                            // inner = Finished handshake msg: [20][len3][verify_data]\n                            // L5: compare the 12-byte verify_data in constant\n                            // time (OR-accumulate XOR diffs, no early exit).\n                            : ~ i diff ? >= ( vec_len [u] inner ) 16 0 1\n                            : ~ i vi 0\n                            ~ < vi 12 { = diff | diff ^^ ( _t_bget inner + 4 vi ) ( _t_bget sfin_exp vi ) = vi + vi 1 }\n                            ? == diff 0 { = sdone 1 } { = serr 1 }\n                        }\n                        F _ → { = serr 1 }\n                    }\n                }\n            }\n        }\n    }\n\n    ? == serr 1 { ( _tls_close_in c ) ^ @ !v TlsErr { F # TlsErr TlsHandshake } } {}\n    = . c established 1\n    ^ @ !v TlsErr { T 0 }\n}\n","bytes":130808}