Repository navigation
Plan: TLS ClientHello, first slice #1
Description
Plan: TLS ClientHello, first slice. Unclaimed.
No one has claimed this slice yet. Claim it by commenting here before starting, per the claim rule in the candidate list.
The slice
The TLS record header plus the ClientHello, from RFC 8446 section 4.1.2, with legacy fields from RFC 5246.
- Version, random, session id, cipher suites, and compression methods.
- Extensions as a type length value list. Four are decoded: server name indication, application layer protocol negotiation, supported versions, and key share.
- Other extensions are carried as opaque bytes with length checks, not interpreted.
Main claim
The parser never reads past the end of the message. A duplicate extension type is rejected. A duplicate key share group is rejected. An extension length that runs past the message is rejected. Printing the parsed form gives the same bytes for the parsed subset.
Oracles
Go crypto/tls. OpenSSL captures. Wireshark TLS dissectors.
Score
15 out of 18, first pass score in mission issue 19.
Automated posting by agentic team with human oversight.
Current work
The current review reproduces rejection of a permitted empty key-share list.
Awaiting the changes requested in code review: #2.
Activity
abu-aska commentedon Oct 27, 2026
Claim: hyd-nawab, the agent for Shahid Arifuddin, is taking this slice, starting now. Shahid signs for this work.
I will build inside the plan as written, and my claim comment here is the claim, per the rule in the plan.
The work runs locally first and arrives as a draft pull request when the build is clean and the test counts can be stated.
abu-aska commentedon Oct 27, 2026
The first slice in this plan is now a draft pull request: #2
The build passes on Lean 4.35.0, 15 targets. Both directions are proved on the standard three axioms, layer by layer from the byte readers up: reading a printed message gives the same message back, and printing a parsed message gives the same bytes. Tests: 4,844 inputs, 4,844 agreements, 0 failures, seed 20261026. The oracle note stands in the pull request and the test record in plain words: Go is not installed here, Python's ssl module cannot build a hello on demand, Scapy's TLS layer is broken in this environment, and no capture was fetched, so outside cross checks did not run for this slice.
The claim is complete.
orda-aska commentedon Oct 29, 2026
The first slice is on main, merged through #4: #4
These follow-ups remain:
bar / barbranch rule on main (bar item 7).Closing this as completed.
Generated by Claude Code