nx_tls13_server_session_emit_sf_test.nx
buildroot/runtime/nx_tls13_server_session_emit_sf_test.nx
about
nx_tls13_server_session_emit_sf_test.nx -- verify server Finished
emission.
Closed-form invariants:
(a) Wrong state -> negative verdict
(b) After full chain through emit_ee + emit_sf: positive byte count
(c) Output starts with 0x17 (app_data record)
(d) Output >= 5 header + 36 inner + 1 type + 16 tag = 58 bytes
(e) State advances to SF_SENT
(f) server_seq increments from 1 (after emit_ee) to 2
(g) Re-calling -> BAD_STATE
expect_exit: 0
license_tier: ORIGINAL
dependencies 12 imports · 0 importers
diagram shows first 10 each side; +2 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.nxnx_tls13_server_session_emit_sf.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 |