nx_tls13_server_session_emit_ee_test.nx
buildroot/runtime/nx_tls13_server_session_emit_ee_test.nx
about
nx_tls13_server_session_emit_ee_test.nx -- verify emit_ee
produces a well-formed AEAD-encrypted record.
Closed-form invariants:
(a) Wrong state (INIT) -> negative verdict
(b) After recv_ch + emit_sh + derive_hs + derive_traffic:
emit_ee returns positive byte count
(c) Output buffer starts with type=0x17 (app_data record)
(d) Output is at least header(5) + inner(7) + tag(16) = 28 bytes
(e) State advances to CERT_SENT
(f) server_seq increments from 0 to 1
(g) Calling emit_ee again -> BAD_STATE
expect_exit: 0
license_tier: ORIGINAL
dependencies 11 imports · 0 importers
diagram shows first 10 each side; +1 more imports, +0 more importers in the complete lists below.
imports: nx_syscalls.nxnx_x25519.nxnx_x25519_ephemeral.nxnx_tls13.nxnx_tls13_hello.nxnx_tls13_server_session.nxnx_tls13_server_session_recv_ch.nxnx_tls13_server_session_emit_sh.nxnx_tls13_server_session_derive_hs.nxnx_tls13_server_session_derive_traffic.nxnx_tls13_server_session_emit_ee.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| none |
functions
| 29 | func main() -> i64 |