Repository navigation

TLS ClientHello: #2 carried forward with the review fixes (bar v2) - #4

Merged

orda-aska merged 20 commits into

mainfrom

claude/clienthello-first-slice

Oct 29, 2026

Merged

TLS ClientHello: #2 carried forward with the review fixes (bar v2)#4
orda-aska merged 20 commits into
mainfrom
claude/clienthello-first-slice

Commits on Oct 27, 2026
- Add TLS ClientHello parser and printer, with proved round trip
  abu-aska
  committed
  0f9c175
Commits on Oct 28, 2026
- Add the bar file set: Spec.lean, comparator.json, bar.toml, CI workflow
  abu-aska
  committed
  e4c149a
- Accept an empty key_share client_shares list
  claude
  committed
  1a8dde0
- Rework the top of the parser so lean4lean accepts the round trip
  claude
  committed
  fcf406a
- Refuse a record longer than 2^14 bytes
  claude
  committed
  834ce44
- Require compression methods [0] in a hello that offers TLS 1.3
  claude
  committed
  d2ff5d7
- Refuse a pre_shared_key extension that is not the last extension
  claude
  committed
  3f28a47
- Make seven refusal statements exercise their rule, and word every example as one input
  claude
  committed
  954e47b
- Test record: Oracle, Seed, Inputs and Failures lines, and real OpenSSL hellos
  claude
  committed
  515921f
- Page: status line says "in progress"; drop the unproved past-the-end claim
  claude
  committed
  d22d730
- Build without warnings
  claude
  committed
  f362fab
- Reflow two paragraphs of the page
  claude
  committed
  e385567
- State the TLS 1.3 compression rule on the extension, not on offersTls13
  claude
  committed
  05d78d5
- Move the well formedness predicate into a spec file, Spec/Defs.lean
  claude
  committed
  391ce28
- State that a record of exactly 2^14 bytes is accepted
  claude
  committed
  7bf9b39
- Describe the two supported_versions refusal inputs exactly
  claude
  committed
  7bab388
- List the three nonempty list conjuncts of Spec.WF in the README
  claude
  committed
  3ed503d
- Say which bytes vary in the record limit section header
  claude
  committed
  f3b9f7a
Commits on Oct 29, 2026
- Merge main (the Apache-2.0 LICENSE) into the first slice
  claude
  committed
  785c7c1
- Declare the Apache-2.0 package license in lakefile.toml
  claude
  committed
  d9932d6

Commits

Commits on Oct 27, 2026

Commits on Oct 28, 2026

Commits on Oct 29, 2026