Port full TLS handshake state machine to CakeML (J3/L4 complete)

Ports extensions, certificate verification, and the client/server state
machine (TlsExtensions, TlsCertVerify, TlsClient/TlsServer/Tls) onto the
CakeML tower. The self-contained tls_handshake_test.cml runs a full
in-process client<->server 1-RTT handshake under the pinned v3400 cake
compiler: both sides reach CONNECTED, the coalesced-flight path works, and
the client verifies the server's RSA-PSS CertificateVerify and Finished.
17/17 handshake checks PASS, independently re-verified (compiled to native
arm8 and run). Completes the CakeML port of the entire stack (L0-L4).

Co-authored-by: Cursor <cursoragent@cursor.com>

Author: sjqtentacles

cakeml/tls_PORT_NOTES.md

@@ -17,9 +17,15 @@ verified previously in `cakeml/`.
 one file because, as a single CakeML compilation unit, `TlsRecordProtect` must
 follow `Aead` and `TlsRecord` in concatenation order.
 
-**Harness:** `cakeml/tls_test.cml` — a SELF-CONTAINED single-compilation-unit
-harness that inlines the full dependency-ordered tower + the ported TLS code + a
-driver, and checks real TLS vectors. It PASSes only on byte/value match.
+The handshake state machine (`TlsExtensions`, `TlsCertVerify`, `TlsClient`,
+`TlsServer`, from `extensions.sml`/`certverify.sml`/`tlsstate.sml`) is also
+ported, in `cakeml/tls_state.sml` — see the "Handshake state machine" section
+below.
+
+**Harnesses:** two SELF-CONTAINED single-compilation-unit harnesses that inline
+the full dependency-ordered tower + the ported TLS code + a driver, PASSing only
+on byte/value match: `cakeml/tls_test.cml` (52/52 core vectors) and
+`cakeml/tls_handshake_test.cml` (17/17 in-process handshake).
 
 ### Result (real run on the cached `cake`)
 
@@ -157,10 +163,66 @@ syntax / basis gaps. The notable ones for the TLS layer:
 - PSK-resumption helpers (`resumptionMasterSecret`, `resumptionPsk`,
   `binderKey`, `binderFinishedKey`, `pskBinder`) are ported for completeness.
 
+## Handshake state machine (the capstone — also ported & verified)
+
+On top of the core, the handshake state machine was ported and verified with a
+real in-process client↔server 1-RTT handshake:
+
+**Ported source** — `cakeml/tls_state.sml`:
+
+| Upstream | Ported structure | Notes |
+|---|---|---|
+| `extensions.sml` | `TlsExtensions` | All extension codecs (key_share CH/SH/HRR, supported_versions, supported_groups, signature_algorithms, SNI, ALPN, cookie, psk_key_exchange_modes, early_data, pre_shared_key) + `negotiateVersion/Group/SigAlg` + downgrade sentinels. Word16/32/8 → `int`; records → tuples. |
+| `certverify.sml` | `TlsCertVerify` | Full RFC 5280 path validation (chain build, validity window, BasicConstraints CA + pathLen, KeyUsage `keyCertSign`, EKU `serverAuth`, sig-alg enforcement, X509 signature verification, RFC 6125 wildcard hostnames). X509 record patterns (`{notBefore,notAfter}`, `{pathLen,…}`, `RsaPss {hash,…}`) → the ported tower's tuple/accessor + curried-constructor forms. ECDSA/Ed25519 unsupported (matches upstream). |
+| `tlsstate.sml` | `TlsClient`, `TlsServer` | ~22-field records → positional tuples (15-tuple client / 12-tuple server). Covers `startHandshake`, `processServerHello`, server-flight decrypt/`processFlight`, client `step` (incl. the J2 coalesced ServerHello+CCS+flight in one step), and server `receiveClientHello`/`produceServerHello`/`produceServerFlight`/`step`, plus the real CV sign+verify. |
+
+**Harness** — `cakeml/tls_handshake_test.cml` (self-contained: tower +
+`x25519.sml` + `tls.sml` + `tls_state.sml` + driver). Compiled with `cake`
+v3400, linked, ran:
+
+```
+HANDSHAKE RESULT: 17 passed, 0 failed
+ALL HANDSHAKE CHECKS PASS
+```
+
+The PASSes are real: client and server opaque states are driven directly
+in-process (handshake records passed as byte strings between them, no sockets),
+reaching **CONNECTED**; "agree on app key" is tuple equality of independently
+derived `(key,iv)` pairs on each side; the coalesced ServerHello+CCS+flight is
+processed in a single `step`; and "CertificateVerify verified" is a genuine
+`Rsa.verifyPss` over the transcript hash against the fixture leaf's public key.
+
+### Handshake concatenation order
+
+`cakeml/kdf.sml` + `bigint.sml` + `asn1.sml` + `pem.sml` + `aead.sml` +
+`rsa.sml` + `x509.sml` + **`x25519.sml`** (inserted here for the ECDHE key
+exchange; `pow2` is structure-local so it introduces no top-level clash) +
+`tls.sml` + `tls_state.sml` + driver.
+
+### Handshake-layer dialect notes / scope limits
+
+- **P256 is not ported.** Upstream `tlsstate` references P256 only for the
+  optional P-256 key-exchange path; the tests use X25519 with
+  `p256PrivateKey = None`, so every P256 branch is stubbed (unsupported/raise).
+- **The `Tls` re-export bundle is not expressible.** CakeML's grammar forbids
+  nested `structure` declarations and structure abbreviations, so the upstream
+  `structure Tls` that re-exports the others has no equivalent — the six
+  structures are simply top-level instead. (Confirmed with a 3-line probe.)
+- **Out of scope** for the handshake harness (focused on the 1-RTT path):
+  HelloRetryRequest, KeyUpdate, `sendApplicationData`, NewSessionTicket
+  issuance, and post-handshake `stepConnected`. The encode/decode codecs for
+  these messages are present in the ported `TlsHandshake` (and round-trip
+  in `tls_test.cml`); only the state-machine driving of them is omitted.
+
 ## Files
 
 - `cakeml/tls.sml` — ported TLS core (TlsRecord/TlsAlert/TlsHandshake/
   TlsKeySchedule + TlsRecordProtect)
-- `cakeml/tls_test.cml` — self-contained harness (tower + TLS + driver),
-  52/52 PASS on `cake` v3400
+- `cakeml/tls_state.sml` — ported handshake state machine (TlsExtensions/
+  TlsCertVerify/TlsClient/TlsServer)
+- `cakeml/tls_test.cml` — self-contained core-vector harness (tower + TLS +
+  driver), **52/52 PASS** on `cake` v3400
+- `cakeml/tls_handshake_test.cml` — self-contained in-process client↔server
+  handshake harness (tower + x25519 + TLS + tls_state + driver),
+  **17/17 PASS** on `cake` v3400
 - `cakeml/tls_PORT_NOTES.md` — this file