[saeta-eth]

Add TLS 1.3 handshake message encoding and decoding, plus SHA-256 transcript handling.
A transcript is the sequence of handshake messages that TLS hashes for authentication.
Part of #2163.

The problem

EthLib derives traffic secrets from encoded transcripts, but callers lack shared message framing and transcript construction.
Handshake headers and extension order are part of the hashed input and must be preserved.

The idea

Decode one complete message within its declared length and return any following bytes.
Keep unrecognized algorithm identifiers and opaque extensions for the caller to interpret.
The round-trip and injectivity theorems cover every successfully encoded message.

A transcript stores received bytes, preserving their headers and extension order.
ClientHello is the client's initial offer of handshake parameters.
HelloRetryRequest is the server's request for a revised offer.
On a retry, the transcript replaces the first ClientHello with a synthetic message containing its SHA-256 hash.
It also builds the content signed by CertificateVerify, the message that proves possession of the certificate key.

Example

An empty EncryptedExtensions, the TLS server's extension-block message, has these six bytes:

08 | 00 00 02 | 00 00

The first byte selects the message; the next three give a two-byte body.
The body declares an empty extension list.
Decoding preserves any following message, and the transcript retains all six bytes, including the header.

For reviewers

• Decoding validates wire format; required extensions, negotiation, authentication and client/server steps remain in specs: the TLS 1.3 handshake of a libp2p QUIC connection #2163.
• Extension payload interpretation is explicit and depends on the enclosing message.
• Finished uses the caller's hash length; transcript handling here is SHA-256.
• Tests cover the RFC 8448 trace, truncated input, nested length errors, duplicate extension types with different data, unknown extensions and retry rejection.
• Maintainer choices of cipher suites, groups and signature schemes remain open.

Checks

Python checks use the project's .venv; Lean uses the pinned 4.35.0 toolchain.

• lake build --wfail: passed, 7,681 jobs.
• uv sync --frozen --extra test --group lint: passed.
• .venv/bin/python -m pytest -n auto: 71,058 passed, 608 skipped, 13 expected failures.
• lake exe check-decls --scope EthLib.Networking.Quic: zero findings.
• lake exe check-accessors: zero sites in 535 modules.
• lake exe check-decls: fails on 28 opaque-dependency findings in untouched modules; all 28 also occur with the TLS modules excluded.

Binding, source, fixture and prose checks

• lake exe gen-bindings --check: passed.
• .venv/bin/ruff check: passed.
• .venv/bin/ruff format --check: 582 files formatted.
• .venv/bin/ty check: passed.
• .venv/bin/python scripts/check_layers.py: passed.
• .venv/bin/python scripts/check_lean_layout.py --base origin/master: no findings.
• .venv/bin/python scripts/check_fixture_pins.py: all pins match.
• .venv/bin/python tests/cryptography/check_vectors.py: 2,310 pinned vectors match.
• .venv/bin/python scripts/soundness_facts.py --check: passed.
• .venv/bin/python -m unittest scripts/test_soundness_facts.py: 18 tests passed.
• .venv/bin/python scripts/release_manifest.py --check: passed.
• .venv/bin/python -m unittest scripts/test_release_manifest.py: 9 tests passed.
• .venv/bin/python scripts/check_python_boundary.py --base origin/master: passed.
• .venv/bin/python scripts/check_python_comments.py --base origin/master: no wrapped comments.
• .venv/bin/python scripts/check_raises.py: passed.
• .venv/bin/python scripts/check_docstrings.py: passed.
• .venv/bin/codespell on the four changed Python files: passed.
• .venv/bin/python scripts/check_writing.py --base origin/master: no suggestions.
• .venv/bin/python scripts/check_writing.py on the eight added Lean files: no suggestions.
• .venv/bin/python scripts/check_writing.py --stdin description: no suggestions.
• .venv/bin/python scripts/check_writing.py --stdin commits: no suggestions.
• git diff --check: passed.

The unchanged-root audit imports EthLib.Consensus, EthLib.Execution.Rpc and EthLib.Engine.BeaconApiEvents.
It reports the same 28 findings and contains zero declarations under EthLib.Networking.Quic.Tls.
Archive tests use the suite's default skips; no archive suite was run.