diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml
new file mode 100644
index 0000000..32457ed
--- /dev/null
+++ b/.github/workflows/bar.yml
@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2
diff --git a/.gitignore b/.gitignore
index 01f8cdb..a2759c4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,4 @@
 .lake/
+__pycache__/
+venv/
+scratch/
diff --git a/ClientHello.lean b/ClientHello.lean
new file mode 100644
index 0000000..cd42942
--- /dev/null
+++ b/ClientHello.lean
@@ -0,0 +1,2 @@
+import ClientHello.Value
+import ClientHello.Parse
diff --git a/ClientHello/Parse.lean b/ClientHello/Parse.lean
new file mode 100644
index 0000000..6f8e10c
--- /dev/null
+++ b/ClientHello/Parse.lean
@@ -0,0 +1,312 @@
+/-
+  The TLS ClientHello parser. It reads one record holding
+  one ClientHello and returns the message, or `none` when the
+  bytes break any of the rules in SPEC.md. Every read is
+  length checked: a field read from input too short for it
+  gives `none`. The rules:
+
+  - The record header is five bytes: content type 22, a
+    legacy record version carried unchecked, and a two byte
+    length of at most 2^14 = 16384 (RFC 8446 section 5.1).
+    The body is exactly that many bytes, and no bytes may
+    follow the record. A body of length 0 cannot hold a
+    handshake header, so it is turned away by the body read.
+  - The handshake header is a type byte, which must be 1,
+    and a three byte length that must cover the rest of the
+    record body exactly.
+  - The body fields follow their length rules: session id at
+    most 32 bytes; cipher suites an even byte count of at
+    least 2; compression methods at least one byte and the
+    null method 0 among them, and exactly the one byte 0
+    when supported_versions lists TLS 1.3 (0x0304). A body
+    that ends before the extensions length is turned away:
+    the extensions block must be present, though it may be
+    empty.
+  - The extensions block is consumed exactly. Each extension
+    is a type, a length, and that many value bytes; a length
+    running past the block turns the message away, and a
+    type standing twice turns it away. pre_shared_key (41)
+    may only stand last.
+  - Four extension values are decoded. In each, the inner
+    length must cover the rest of the value exactly. Server
+    name entries may not repeat a name type, and a host_name
+    entry must be nonempty. ALPN names must be nonempty.
+    supported_versions in a hello is a list of two byte
+    versions of even, nonzero byte length. Key share entries
+    may not repeat a group, and key exchange bytes must be
+    nonempty. Every other type is carried opaque.
+
+  The variable length lists are read with a fuel count, one
+  more than the length of the input at the top level, which
+  is always enough, since every step takes bytes. A hostile
+  input is rejected, never looped on.
+-/
+
+import ClientHello.Value
+
+namespace ClientHello
+
+/-- Read two bytes as a big endian value, with the rest of
+    the input. Fewer than two bytes gives `none`. -/
+def getU16 : List UInt8 → Option (Nat × List UInt8)
+  | a :: b :: rest => some (u16 a b, rest)
+  | _ => none
+
+/-! The record, the handshake header and the body fields are
+read with the four readers below. Each one reads a field off
+the front of the input and goes on with the field's value
+and the rest of the input, or gives `none` when the input is
+too short. Writing the top of the parser this way keeps each
+proof step a rewrite with one of the reader lemmas, which
+every kernel bundled with Lean checks quickly. -/
+
+/-- Read one byte, then go on with its value and the rest of
+    the input. No byte gives `none`. -/
+def withU8 {α : Type} (bs : List UInt8)
+    (k : Nat → List UInt8 → Option α) : Option α :=
+  match bs with
+  | b :: rest => k b.toNat rest
+  | [] => none
+
+/-- Read two bytes as a big endian value, then go on with the
+    value and the rest of the input. Fewer than two bytes give
+    `none`. -/
+def withU16 {α : Type} (bs : List UInt8)
+    (k : Nat → List UInt8 → Option α) : Option α :=
+  match bs with
+  | a :: b :: rest => k (u16 a b) rest
+  | _ => none
+
+/-- Read three bytes as a big endian value, then go on with
+    the value and the rest of the input. Fewer than three bytes
+    give `none`. -/
+def withU24 {α : Type} (bs : List UInt8)
+    (k : Nat → List UInt8 → Option α) : Option α :=
+  match bs with
+  | a :: b :: c :: rest => k (u24 a b c) rest
+  | _ => none
+
+/-- Read `n` bytes as a block, then go on with the block and
+    the rest of the input. Fewer than `n` bytes give `none`. -/
+def withBytes {α : Type} (n : Nat) (bs : List UInt8)
+    (k : List UInt8 → List UInt8 → Option α) : Option α :=
+  if (bs.take n).length = n then k (bs.take n) (bs.drop n)
+  else none
+
+/-- Read a list of two byte values from bytes that must be
+    consumed exactly. An odd trailing byte gives `none`. -/
+def parsePairs : List UInt8 → Option (List Nat)
+  | [] => some []
+  | a :: b :: rest =>
+    (parsePairs rest).map (fun vs => u16 a b :: vs)
+  | _ => none
+
+/-- Read server name entries with a fuel count. A name type
+    standing twice in the list gives `none`; the repeat
+    check is made against the entries that follow. -/
+def parseNameEntriesGo :
+    Nat → List UInt8 → Option (List (Nat × List UInt8))
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, t :: rest =>
+    getU16 rest >>= fun (n, r1) =>
+    if (r1.take n).length = n then
+      parseNameEntriesGo f (r1.drop n) >>= fun es =>
+      if t.toNat ∈ es.map Prod.fst then none
+      else some ((t.toNat, r1.take n) :: es)
+    else none
+
+/-- Read server name entries, with enough fuel for the whole
+    input. -/
+def parseNameEntries (bs : List UInt8) :
+    Option (List (Nat × List UInt8)) :=
+  parseNameEntriesGo (bs.length + 1) bs
+
+/-- The server name value check that stands outside the
+    entry grammar: the list is nonempty, and every host_name
+    entry (type 0) carries at least one byte. -/
+def validNames (es : List (Nat × List UInt8)) : Bool :=
+  !es.isEmpty &&
+  es.all (fun e => decide (e.1 ≠ 0 ∨ e.2 ≠ []))
+
+/-- Read the server_name value: a two byte list length that
+    covers the rest of the value, then the entries, then
+    the value check. -/
+def parseSNI (v : List UInt8) : Option Extension :=
+  getU16 v >>= fun (n, rest) =>
+  if rest.length = n then
+    parseNameEntries rest >>= fun es =>
+    if validNames es then some (.serverName es) else none
+  else none
+
+/-- Read ALPN protocol names with a fuel count. An empty
+    name gives `none`. -/
+def parseAlpnGo : Nat → List UInt8 → Option (List (List UInt8))
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, len :: rest =>
+    if len.toNat = 0 then none
+    else if (rest.take len.toNat).length = len.toNat then
+      (parseAlpnGo f (rest.drop len.toNat)).map
+        (fun ns => (rest.take len.toNat) :: ns)
+    else none
+
+/-- Read ALPN protocol names, with enough fuel for the whole
+    input. -/
+def parseAlpnNames (bs : List UInt8) :
+    Option (List (List UInt8)) :=
+  parseAlpnGo (bs.length + 1) bs
+
+/-- Read the ALPN value: a two byte list length that covers
+    the rest of the value, then at least one name. -/
+def parseALPN (v : List UInt8) : Option Extension :=
+  getU16 v >>= fun (n, rest) =>
+  if rest.length = n then
+    parseAlpnNames rest >>= fun ns =>
+    if ns.isEmpty then none else some (.alpn ns)
+  else none
+
+/-- Read the supported_versions value, in the ClientHello
+    form: a one byte length, even and at least 2, then that
+    many bytes as two byte versions. -/
+def parseSV (v : List UInt8) : Option Extension :=
+  match v with
+  | n :: rest =>
+    if rest.length = n.toNat ∧ n.toNat % 2 = 0 ∧ 2 ≤ n.toNat
+      then parsePairs rest >>= fun vs =>
+        some (.supportedVersions vs)
+    else none
+  | [] => none
+
+/-- Read key share entries with a fuel count. Empty key
+    exchange bytes give `none`, and a group standing twice
+    in the list gives `none`. -/
+def parseSharesGo :
+    Nat → List UInt8 → Option (List (Nat × List UInt8))
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, bs =>
+    getU16 bs >>= fun (g, r1) =>
+    getU16 r1 >>= fun (n, r2) =>
+    if n = 0 then none
+    else if (r2.take n).length = n then
+      parseSharesGo f (r2.drop n) >>= fun ss =>
+      if g ∈ ss.map Prod.fst then none
+      else some ((g, r2.take n) :: ss)
+    else none
+
+/-- Read key share entries, with enough fuel for the whole
+    input. -/
+def parseShares (bs : List UInt8) :
+    Option (List (Nat × List UInt8)) :=
+  parseSharesGo (bs.length + 1) bs
+
+/-- Read the key_share value, in the client form: a two
+    byte list length that covers the rest of the value, then
+    the entries. The list may be empty: RFC 8446 section
+    4.2.8 lets a client send no shares, to ask for a
+    HelloRetryRequest. -/
+def parseKS (v : List UInt8) : Option Extension :=
+  getU16 v >>= fun (n, rest) =>
+  if rest.length = n then
+    parseShares rest >>= fun ss => some (.keyShare ss)
+  else none
+
+/-- Read one extension value, by its type. The four decoded
+    types go to their readers; every other type is carried
+    opaque, as the type and the value bytes as they stood. -/
+def parseExtValue (t : Nat) (v : List UInt8) :
+    Option Extension :=
+  if t = 0 then parseSNI v
+  else if t = 16 then parseALPN v
+  else if t = 43 then parseSV v
+  else if t = 51 then parseKS v
+  else some (.opaque t v)
+
+/-- Read the extensions of a block that must be consumed
+    exactly, with a fuel count. An extension length running
+    past the block gives `none`, and a type standing twice
+    gives `none`. -/
+def parseExtsGo : Nat → List UInt8 → Option (List Extension)
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, bs =>
+    getU16 bs >>= fun (t, r1) =>
+    getU16 r1 >>= fun (n, r2) =>
+    if (r2.take n).length = n then
+      parseExtValue t (r2.take n) >>= fun e =>
+      parseExtsGo f (r2.drop n) >>= fun es =>
+      if extType e ∈ es.map extType then none
+      else some (e :: es)
+    else none
+
+/-- Read an extensions block, with enough fuel for the
+    whole block. -/
+def parseExts (bs : List UInt8) : Option (List Extension) :=
+  parseExtsGo (bs.length + 1) bs
+
+/-- Read the body fields from bytes that are exactly the
+    fields: legacy version, random, session id, cipher
+    suites, compression methods, and the extensions block,
+    which must be present and must run to the end. -/
+def parseBodyFields (bs : List UInt8) : Option Hello :=
+  withU16 bs fun ver r1 =>
+  withBytes 32 r1 fun rand r2 =>
+  withU8 r2 fun slen r3 =>
+  if slen ≤ 32 then
+    withBytes slen r3 fun sess r4 =>
+    withU16 r4 fun clen r5 =>
+    if clen % 2 = 0 ∧ 2 ≤ clen then
+      withBytes clen r5 fun cbytes r6 =>
+      (parsePairs cbytes).bind fun suites =>
+      withU8 r6 fun mlen r7 =>
+      if 1 ≤ mlen then
+        withBytes mlen r7 fun comps r8 =>
+        if (0 : UInt8) ∈ comps then
+          withU16 r8 fun elen r9 =>
+          withBytes elen r9 fun ebytes r10 =>
+          if r10 = [] then
+            (parseExts ebytes).bind fun exts =>
+            -- RFC 8446 section 4.2.11: pre_shared_key (41)
+            -- must be the last extension.
+            if 41 ∉ (exts.dropLast).map extType then
+              -- RFC 8446 section 4.1.2: a TLS 1.3 ClientHello
+              -- carries exactly one compression method, null.
+              if offersTls13 exts = true → comps = [0] then
+                some ⟨ver, rand, sess, suites, comps, exts⟩
+              else none
+            else none
+          else none
+        else none
+      else none
+    else none
+  else none
+
+/-- Read the handshake message from a record body: the type
+    byte must be 1, and the three byte length must cover the
+    rest of the body exactly. -/
+def parseBody (body : List UInt8) : Option Hello :=
+  withU8 body fun htype r1 =>
+  if htype = 1 then
+    withU24 r1 fun hlen r2 =>
+    withBytes hlen r2 fun fbs r3 =>
+    if r3 = [] then parseBodyFields fbs else none
+  else none
+
+/-- Parse a whole message: one record, holding one
+    ClientHello, with no bytes after the record. The record
+    length may not exceed 2^14 = 16384 bytes (RFC 8446
+    section 5.1). -/
+def parse (bs : List UInt8) : Option Message :=
+  withU8 bs fun ct r1 =>
+  if ct = 22 then
+    withU16 r1 fun rv r2 =>
+    withU16 r2 fun rlen r3 =>
+    if rlen ≤ 16384 then
+      withBytes rlen r3 fun body r4 =>
+      if r4 = [] then (parseBody body).map fun h => ⟨rv, h⟩
+      else none
+    else none
+  else none
+
+end ClientHello
diff --git a/ClientHello/Value.lean b/ClientHello/Value.lean
new file mode 100644
index 0000000..28a26db
--- /dev/null
+++ b/ClientHello/Value.lean
@@ -0,0 +1,188 @@
+/-
+  The TLS ClientHello data model and the canonical printer.
+
+  A message is one TLS record holding one ClientHello, in the
+  shape of RFC 8446 section 4.1.2 with the legacy fields of
+  RFC 5246. The record header carries a content type, which
+  must be 22 (handshake), a legacy record version, which is
+  carried unchecked, and a length. Inside it, a handshake
+  header carries the message type, which must be 1
+  (client_hello), and a three byte length. The body holds the
+  legacy version, the 32 byte random, the legacy session id,
+  the cipher suites, the legacy compression methods, and the
+  extensions.
+
+  Four extensions are decoded: server_name (0, RFC 6066
+  section 3), ALPN (16, RFC 7301), supported_versions (43),
+  and key_share (51). Every other extension is carried as its
+  type and its raw value bytes, length checked and not read.
+
+  Numbers are held as plain natural numbers. Byte blocks are
+  held as byte lists. Printing recomputes every length from
+  the value it prints, so a printed message is the canonical
+  form of the value.
+-/
+
+namespace ClientHello
+
+/-- A value as two bytes, big endian. The value is taken
+    modulo 2^16; callers only pass values below that. -/
+def be16 (n : Nat) : List UInt8 :=
+  [ (n / 256).toUInt8, n.toUInt8 ]
+
+/-- The value of two bytes read big endian. -/
+def u16 (a b : UInt8) : Nat :=
+  a.toNat * 256 + b.toNat
+
+/-- A value as three bytes, big endian. The value is taken
+    modulo 2^24; callers only pass values below that. -/
+def be24 (n : Nat) : List UInt8 :=
+  [ (n / 65536).toUInt8, (n / 256).toUInt8, n.toUInt8 ]
+
+/-- The value of three bytes read big endian. -/
+def u24 (a b c : UInt8) : Nat :=
+  a.toNat * 65536 + b.toNat * 256 + c.toNat
+
+/-- One extension. The four decoded forms are distinct from
+    the opaque form, which carries a type the slice does not
+    decode and the value bytes as they stood. A server name
+    entry is a name type and its bytes; a key share entry is
+    a group and its key exchange bytes. -/
+inductive Extension where
+  | serverName (entries : List (Nat × List UInt8)) : Extension
+  | alpn (names : List (List UInt8)) : Extension
+  | supportedVersions (versions : List Nat) : Extension
+  | keyShare (shares : List (Nat × List UInt8)) : Extension
+  | opaque (extType : Nat) (value : List UInt8) : Extension
+  deriving DecidableEq, Repr
+
+/-- The wire type of an extension. -/
+def extType : Extension → Nat
+  | .serverName _ => 0
+  | .alpn _ => 16
+  | .supportedVersions _ => 43
+  | .keyShare _ => 51
+  | .opaque t _ => t
+
+/-- Two byte values in printed form, one after another. -/
+def printPairs : List Nat → List UInt8
+  | [] => []
+  | v :: vs => be16 v ++ printPairs vs
+
+/-- Server name entries in printed form: a name type byte, a
+    two byte length, and the name bytes. -/
+def printNameEntries : List (Nat × List UInt8) → List UInt8
+  | [] => []
+  | (t, bs) :: es =>
+    (t.toUInt8 :: (be16 bs.length ++ bs)) ++ printNameEntries es
+
+/-- ALPN protocol names in printed form: a one byte length
+    and the name bytes. -/
+def printAlpnNames : List (List UInt8) → List UInt8
+  | [] => []
+  | n :: ns => (n.length.toUInt8 :: n) ++ printAlpnNames ns
+
+/-- Key share entries in printed form: a two byte group, a
+    two byte length, and the key exchange bytes. -/
+def printShares : List (Nat × List UInt8) → List UInt8
+  | [] => []
+  | (g, k) :: ss =>
+    (be16 g ++ (be16 k.length ++ k)) ++ printShares ss
+
+/-- The value bytes of an extension, as the printer writes
+    them. Three of the decoded forms open with a length that
+    covers the rest of the value: two bytes for server_name
+    and key_share, one byte for supported_versions in a
+    ClientHello. -/
+def printExtValue : Extension → List UInt8
+  | .serverName es =>
+    be16 (printNameEntries es).length ++ printNameEntries es
+  | .alpn ns =>
+    be16 (printAlpnNames ns).length ++ printAlpnNames ns
+  | .supportedVersions vs =>
+    (printPairs vs).length.toUInt8 :: printPairs vs
+  | .keyShare ss =>
+    be16 (printShares ss).length ++ printShares ss
+  | .opaque _ v => v
+
+/-- One extension in printed form: type, length, value. -/
+def printExt (e : Extension) : List UInt8 :=
+  be16 (extType e) ++ be16 (printExtValue e).length ++
+    printExtValue e
+
+/-- The extension list in printed form. -/
+def printExts : List Extension → List UInt8
+  | [] => []
+  | e :: es => printExt e ++ printExts es
+
+/-- The ClientHello body fields, in wire order. -/
+structure Hello where
+  /-- The legacy version, two bytes. Carried unchecked. -/
+  legacyVersion : Nat
+  /-- The random: 32 bytes in a well formed message. -/
+  random : List UInt8
+  /-- The legacy session id: at most 32 bytes in a well
+      formed message. -/
+  sessionId : List UInt8
+  /-- The cipher suites, as two byte codes. A well formed
+      message holds at least one. -/
+  cipherSuites : List Nat
+  /-- The legacy compression methods. A well formed message
+      holds at least one, and the null method 0 is among
+      them. -/
+  compressionMethods : List UInt8
+  /-- The extensions, in wire order. No type stands twice in
+      a well formed message. -/
+  extensions : List Extension
+  deriving DecidableEq, Repr
+
+/-- One record holding one ClientHello. -/
+structure Message where
+  /-- The legacy record version, two bytes. Carried
+      unchecked. -/
+  recordVersion : Nat
+  /-- The ClientHello the record holds. -/
+  hello : Hello
+  deriving DecidableEq, Repr
+
+/-- The body fields in printed form, without the handshake
+    header: legacy version, random, session id with its one
+    byte length, cipher suites with their two byte length,
+    compression methods with their one byte length, and the
+    extensions with their two byte length. -/
+def printBodyFields (h : Hello) : List UInt8 :=
+  be16 h.legacyVersion ++ h.random ++
+  (h.sessionId.length.toUInt8 :: h.sessionId) ++
+  (be16 (printPairs h.cipherSuites).length ++
+    printPairs h.cipherSuites) ++
+  (h.compressionMethods.length.toUInt8 ::
+    h.compressionMethods) ++
+  (be16 (printExts h.extensions).length ++
+    printExts h.extensions)
+
+/-- The handshake message in printed form: type 1, a three
+    byte length, and the body fields. -/
+def printBody (h : Hello) : List UInt8 :=
+  (1 : UInt8) :: (be24 (printBodyFields h).length ++
+    printBodyFields h)
+
+/-- The whole message in printed form: content type 22, the
+    legacy record version, a two byte length, and the
+    handshake message. -/
+def print (m : Message) : List UInt8 :=
+  (22 : UInt8) :: (be16 m.recordVersion ++
+    (be16 (printBody m.hello).length ++ printBody m.hello))
+
+/-- Whether an extension list offers TLS 1.3: it holds a
+    supported_versions extension that lists 0x0304 (772). Such
+    a hello is a TLS 1.3 ClientHello in the sense of RFC 8446
+    section 4.1.2, whatever older versions it also lists. The
+    parser uses this test. The specification does not: it
+    states the same condition on the extension itself, in
+    `Spec.WF` and `Spec.tls13_compression_null`. -/
+def offersTls13 : List Extension → Bool
+  | [] => false
+  | .supportedVersions vs :: es => vs.contains 772 || offersTls13 es
+  | _ :: es => offersTls13 es
+
+end ClientHello
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..642c584
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,87 @@
+/-
+  Command line front end, used by the tests.
+
+  Reads one request per line and prints one answer per line. A
+  request is an operation and its input as comma-separated
+  decimal byte codes.
+
+    parse 22,3,3,...   prints  ok:22,3,3,... or none
+
+  The one operation is `parse`. Its input is the byte codes of
+  a TLS record holding a ClientHello. Its answer is `ok:` and
+  the byte codes of the canonical reprint of the parsed
+  message, or `none` when the message is rejected.
+
+  A request is an operation, then optionally one space and its
+  numbers; with no numbers after the space, the input is empty.
+  A malformed request prints `error`: any other line, an unknown
+  operation, a number that is not plain decimal digits, or a
+  code above 255, which no byte holds. A line may end in LF or
+  CR LF; nothing else around a request is ignored.
+
+  The parsing and printing here call `ClientHello.parse` and
+  `ClientHello.print` directly. The line handling is covered by
+  the tests, not by a proof.
+-/
+
+import ClientHello
+
+open ClientHello
+
+/-- A number in plain decimal digits. Longer numbers than any
+    byte code are refused before they are converted, since
+    that takes time quadratic in their length. -/
+def number (t : String) : Option Nat :=
+  let ds := t.toList
+  if ds.isEmpty || !ds.all Char.isDigit || (ds.dropWhile (· = '0')).length > 7 then none
+  else t.toNat?
+
+/-- The comma-separated numbers in `s`. -/
+def numbers (s : String) : Option (List Nat) :=
+  if s.isEmpty then some [] else (s.splitOn ",").mapM number
+
+/-- The numbers as bytes. A number above 255 is not a byte, and
+    makes the request malformed. -/
+def toBytes (ns : List Nat) : Option (List UInt8) :=
+  ns.mapM fun n => if n < 256 then some n.toUInt8 else none
+
+def showCodes (bs : List UInt8) : String :=
+  ",".intercalate (bs.map fun b => toString b.toNat)
+
+/-- The answer to one request, or `none` when the request is
+    malformed. -/
+def answer (op : String) (ns : List Nat) : Option String :=
+  match op with
+  | "parse" =>
+    match toBytes ns with
+    | none => none
+    | some bs =>
+      match parse bs with
+      | some v => some ("ok:" ++ showCodes (print v))
+      | none => some "none"
+  | _ => none
+
+/-- The answer to one line: an operation, then optionally one
+    space and its numbers. -/
+def request (line : String) : Option String :=
+  match line.splitOn " " with
+  | [op] => answer op []
+  | [op, arg] => numbers arg >>= answer op
+  | _ => none
+
+/-- The line without its line ending: LF, or CR LF. -/
+def chomp (line : String) : String :=
+  let cs := line.toList
+  if cs.getLast? = some '\n' then
+    let cs := cs.dropLast
+    String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+  else line
+
+def main : IO Unit := do
+  let stdin ← IO.getStdin
+  let stdout ← IO.getStdout
+  repeat
+    let line ← stdin.getLine
+    if line.isEmpty then break
+    let line := chomp line
+    stdout.putStrLn ((request line).getD "error")
diff --git a/Proofs.lean b/Proofs.lean
new file mode 100644
index 0000000..36165f5
--- /dev/null
+++ b/Proofs.lean
@@ -0,0 +1,3 @@
+import Proofs.RoundTrip
+import Proofs.SpecProofs
+import Proofs.Verify
diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean
new file mode 100644
index 0000000..fde11e2
--- /dev/null
+++ b/Proofs/RoundTrip.lean
@@ -0,0 +1,2007 @@
+/-
+  The round trip proofs.
+
+  Two claims are proved here, matching the plan's main claim
+  and its mirror:
+
+  - `parse_print`: for every well formed message, parsing its
+    printed form gives the message back.
+  - `print_parse`: for every byte list the parser takes,
+    printing the parsed message gives the same bytes back.
+    The printer is canonical and the parser takes exactly the
+    canonical forms: every length is recomputed from the
+    value, and the value holds every byte the message
+    carried, so nothing is lost or added.
+
+  No theorem here says the parser never reads past the end
+  of its input. In this list model every reader is a total
+  function, so there is no out of bounds read to rule out: a
+  read from input too short for its field gives `none`. The
+  statement about the bytes is `print_parse`: every byte of
+  an accepted input is accounted for in the message.
+-/
+
+import ClientHello
+import Spec.Defs
+
+namespace ClientHello.Proofs
+
+open ClientHello
+-- `WF` and `ExtWF` below are `Spec.WF` and `Spec.ExtWF`, the
+-- well formedness predicate of the specification (`Spec/Defs.lean`).
+open Spec (WF ExtWF)
+
+/-! ## Byte and number basics -/
+
+/-- A byte printed from a number reads back as the number
+    modulo 256. -/
+theorem toUInt8_toNat (n : Nat) : (n.toUInt8).toNat = n % 256 := rfl
+
+/-- A byte's value fits in 256. -/
+theorem toNat_lt (b : UInt8) : b.toNat < 256 := UInt8.toNat_lt_size b
+
+/-- A byte rebuilt from its value is the byte. -/
+theorem toNat_toUInt8 (b : UInt8) : b.toNat.toUInt8 = b := by
+  apply UInt8.toNat_inj.mp
+  show (b.toNat.toUInt8).toNat = b.toNat
+  rw [toUInt8_toNat]
+  exact Nat.mod_eq_of_lt (toNat_lt b)
+
+/-- Two bytes printed from a value below 2^16 read back as
+    the value. -/
+theorem u16_be16 (n : Nat) (h : n < 65536) :
+    u16 (n / 256).toUInt8 n.toUInt8 = n := by
+  simp only [u16, toUInt8_toNat]
+  omega
+
+/-- The bytes read as a two byte value print back to those
+    bytes. -/
+theorem be16_u16 (a b : UInt8) : be16 (u16 a b) = [a, b] := by
+  have ha := toNat_lt a
+  have hb := toNat_lt b
+  have e1 : u16 a b / 256 = a.toNat := by
+    simp only [u16]; omega
+  have e2 : (u16 a b).toUInt8 = b := by
+    apply UInt8.toNat_inj.mp
+    show ((u16 a b).toUInt8).toNat = b.toNat
+    rw [toUInt8_toNat]; simp only [u16]; omega
+  simp only [be16, e1, e2, toNat_toUInt8]
+
+/-- Three bytes printed from a value below 2^24 read back as
+    the value. -/
+theorem u24_be24 (n : Nat) (h : n < 16777216) :
+    u24 (n / 65536).toUInt8 (n / 256).toUInt8 n.toUInt8 = n := by
+  simp only [u24, toUInt8_toNat]
+  omega
+
+/-- The bytes read as a three byte value print back to those
+    bytes. -/
+theorem be24_u24 (a b c : UInt8) :
+    be24 (u24 a b c) = [a, b, c] := by
+  have ha := toNat_lt a
+  have hb := toNat_lt b
+  have hc := toNat_lt c
+  have e1 : u24 a b c / 65536 = a.toNat := by
+    simp only [u24]; omega
+  have e2 : (u24 a b c / 256).toUInt8 = b := by
+    apply UInt8.toNat_inj.mp
+    show ((u24 a b c / 256).toUInt8).toNat = b.toNat
+    rw [toUInt8_toNat]; simp only [u24]; omega
+  have e3 : (u24 a b c).toUInt8 = c := by
+    apply UInt8.toNat_inj.mp
+    show ((u24 a b c).toUInt8).toNat = c.toNat
+    rw [toUInt8_toNat]; simp only [u24]; omega
+  simp only [be24, e1, e2, e3, toNat_toUInt8]
+
+/-! ## The readers, on printed forms and on read forms -/
+
+/-- Reading two bytes off the front of a printed value and
+    what follows it. -/
+theorem getU16_be16 (n : Nat) (h : n < 65536) (r : List UInt8) :
+    getU16 (be16 n ++ r) = some (n, r) := by
+  show getU16 ((n / 256).toUInt8 :: n.toUInt8 :: r) = some (n, r)
+  show some (u16 (n / 256).toUInt8 n.toUInt8, r) = some (n, r)
+  rw [u16_be16 n h]
+
+/-- Bytes read by the two byte reader print back as those
+    bytes, and the value fits two bytes. -/
+theorem getU16_inv {bs : List UInt8} {n : Nat} {r : List UInt8}
+    (h : getU16 bs = some (n, r)) :
+    bs = be16 n ++ r ∧ n < 65536 := by
+  cases bs with
+  | nil => simp [getU16] at h
+  | cons a bs' =>
+    cases bs' with
+    | nil => simp [getU16] at h
+    | cons b r' =>
+      have hstep : getU16 (a :: b :: r') = some (u16 a b, r') := rfl
+      rw [hstep] at h
+      simp only [Option.some.injEq, Prod.mk.injEq] at h
+      obtain ⟨rfl, rfl⟩ := h
+      refine ⟨?_, ?_⟩
+      · simp only [be16_u16, List.cons_append, List.nil_append]
+      · have ha := toNat_lt a
+        have hb := toNat_lt b
+        simp only [u16]; omega
+
+/-! The continuation readers. Each lemma below is stated for
+any continuation `k`, so a proof uses it by rewriting: the
+continuation in the goal is matched as it stands, and what is
+left is its body, applied to the field read. -/
+
+/-- A printed two byte value, as its two bytes in front of
+    what follows it. -/
+theorem be16_append (n : Nat) (r : List UInt8) :
+    be16 n ++ r = (n / 256).toUInt8 :: n.toUInt8 :: r := rfl
+
+/-- A printed three byte value, as its three bytes in front
+    of what follows it. -/
+theorem be24_append (n : Nat) (r : List UInt8) :
+    be24 n ++ r =
+      (n / 65536).toUInt8 :: (n / 256).toUInt8 :: n.toUInt8 :: r :=
+  rfl
+
+/-- One step of the one byte reader. -/
+theorem withU8_cons {α : Type} (b : UInt8) (r : List UInt8)
+    (k : Nat → List UInt8 → Option α) :
+    withU8 (b :: r) k = k b.toNat r := rfl
+
+/-- One step of the two byte reader. -/
+theorem withU16_cons {α : Type} (a b : UInt8) (r : List UInt8)
+    (k : Nat → List UInt8 → Option α) :
+    withU16 (a :: b :: r) k = k (u16 a b) r := rfl
+
+/-- One step of the three byte reader. -/
+theorem withU24_cons {α : Type} (a b c : UInt8) (r : List UInt8)
+    (k : Nat → List UInt8 → Option α) :
+    withU24 (a :: b :: c :: r) k = k (u24 a b c) r := rfl
+
+/-- The two byte reader on a printed value reads the value. -/
+theorem withU16_be16 {α : Type} {n : Nat} (h : n < 65536)
+    (r : List UInt8) (k : Nat → List UInt8 → Option α) :
+    withU16 (be16 n ++ r) k = k n r := by
+  rw [be16_append, withU16_cons, u16_be16 n h]
+
+/-- The three byte reader on a printed value reads the
+    value. -/
+theorem withU24_be24 {α : Type} {n : Nat} (h : n < 16777216)
+    (r : List UInt8) (k : Nat → List UInt8 → Option α) :
+    withU24 (be24 n ++ r) k = k n r := by
+  rw [be24_append, withU24_cons, u24_be24 n h]
+
+/-- The block reader on a block of the length it asks for
+    reads the block. -/
+theorem withBytes_app {α : Type} {n : Nat} {v : List UInt8}
+    (hv : v.length = n) (r : List UInt8)
+    (k : List UInt8 → List UInt8 → Option α) :
+    withBytes n (v ++ r) k = k v r := by
+  unfold withBytes
+  have ht : (v ++ r).take n = v := by
+    rw [← hv]; exact List.take_left
+  have hd : (v ++ r).drop n = r := by
+    rw [← hv]; exact List.drop_left
+  rw [ht, hd, ite_eq_left hv]
+
+/-- A block read at exactly its own length gives the block
+    and nothing after it. -/
+theorem withBytes_self {α : Type} (bs : List UInt8)
+    (k : List UInt8 → List UInt8 → Option α) :
+    withBytes bs.length bs k = k bs [] := by
+  have h := withBytes_app (v := bs) rfl [] k
+  rw [List.append_nil] at h
+  exact h
+
+/-- A successful one byte read: the input was the byte and
+    the rest, and the value fits a byte. -/
+theorem withU8_inv {α : Type} {bs : List UInt8}
+    {k : Nat → List UInt8 → Option α} {x : α}
+    (h : withU8 bs k = some x) :
+    ∃ n r, bs = n.toUInt8 :: r ∧ n < 256 ∧ k n r = some x := by
+  cases bs with
+  | nil =>
+    have h0 : withU8 ([] : List UInt8) k = none := rfl
+    rw [h0] at h
+    cases h
+  | cons b r =>
+    rw [withU8_cons] at h
+    exact ⟨b.toNat, r, by rw [toNat_toUInt8], toNat_lt b, h⟩
+
+/-- A successful two byte read: the input was the printed
+    value and the rest, and the value fits two bytes. -/
+theorem withU16_inv {α : Type} {bs : List UInt8}
+    {k : Nat → List UInt8 → Option α} {x : α}
+    (h : withU16 bs k = some x) :
+    ∃ n r, bs = be16 n ++ r ∧ n < 65536 ∧ k n r = some x := by
+  cases bs with
+  | nil =>
+    have h0 : withU16 ([] : List UInt8) k = none := rfl
+    rw [h0] at h
+    cases h
+  | cons a bs' =>
+    cases bs' with
+    | nil =>
+      have h0 : withU16 [a] k = none := rfl
+      rw [h0] at h
+      cases h
+    | cons b r =>
+      rw [withU16_cons] at h
+      refine ⟨u16 a b, r, ?_, ?_, h⟩
+      · rw [be16_u16]
+        rfl
+      · have ha := toNat_lt a
+        have hb := toNat_lt b
+        simp only [u16]; omega
+
+/-- A successful three byte read: the input was the printed
+    value and the rest, and the value fits three bytes. -/
+theorem withU24_inv {α : Type} {bs : List UInt8}
+    {k : Nat → List UInt8 → Option α} {x : α}
+    (h : withU24 bs k = some x) :
+    ∃ n r, bs = be24 n ++ r ∧ n < 16777216 ∧ k n r = some x := by
+  cases bs with
+  | nil =>
+    have h0 : withU24 ([] : List UInt8) k = none := rfl
+    rw [h0] at h
+    cases h
+  | cons a bs' =>
+    cases bs' with
+    | nil =>
+      have h0 : withU24 [a] k = none := rfl
+      rw [h0] at h
+      cases h
+    | cons b bs'' =>
+      cases bs'' with
+      | nil =>
+        have h0 : withU24 [a, b] k = none := rfl
+        rw [h0] at h
+        cases h
+      | cons c r =>
+        rw [withU24_cons] at h
+        refine ⟨u24 a b c, r, ?_, ?_, h⟩
+        · rw [be24_u24]
+          rfl
+        · have ha := toNat_lt a
+          have hb := toNat_lt b
+          have hc := toNat_lt c
+          simp only [u24]; omega
+
+/-- A successful block read: the block holds `n` bytes, and
+    the input was the block and the rest. -/
+theorem withBytes_inv {α : Type} {n : Nat} {bs : List UInt8}
+    {k : List UInt8 → List UInt8 → Option α} {x : α}
+    (h : withBytes n bs k = some x) :
+    ∃ v r, v.length = n ∧ bs = v ++ r ∧ k v r = some x := by
+  unfold withBytes at h
+  by_cases hc : (bs.take n).length = n
+  · rw [ite_eq_left hc] at h
+    exact ⟨bs.take n, bs.drop n, hc,
+      (List.take_append_drop n bs).symm, h⟩
+  · rw [ite_eq_right hc] at h
+    cases h
+
+/-! ## Two byte value lists: the cipher suites and the
+       supported versions -/
+
+/-- The printed length of a two byte value list. -/
+theorem printPairs_length (vs : List Nat) :
+    (printPairs vs).length = 2 * vs.length := by
+  induction vs with
+  | nil => rfl
+  | cons v vs ih =>
+    simp only [printPairs, be16, List.length_append,
+      List.length_cons, List.length_nil, ih]
+    omega
+
+/-- Printed two byte values read back as the values. -/
+theorem parsePairs_printPairs :
+    ∀ {vs : List Nat}, (∀ v ∈ vs, v < 65536) →
+    parsePairs (printPairs vs) = some vs := by
+  intro vs
+  induction vs with
+  | nil => intro _; rfl
+  | cons v vs ih =>
+    intro hw
+    have hv : v < 65536 := hw v (by simp)
+    have htail : ∀ x ∈ vs, x < 65536 :=
+      fun x hx => hw x (List.mem_cons_of_mem v hx)
+    show parsePairs (be16 v ++ printPairs vs) = some (v :: vs)
+    show parsePairs ((v / 256).toUInt8 :: v.toUInt8 ::
+      printPairs vs) = some (v :: vs)
+    show (parsePairs (printPairs vs)).map
+        (fun vs' => u16 (v / 256).toUInt8 v.toUInt8 :: vs')
+      = some (v :: vs)
+    rw [ih htail, u16_be16 v hv]
+    rfl
+
+/-- Two byte values a successful read gives print back to
+    the bytes they were read from, and each fits two bytes.
+    The induction is on the byte count, two at a time, since
+    the reader takes two bytes per value. -/
+theorem parsePairs_inv_aux : ∀ (n : Nat) (bs : List UInt8)
+    (vs : List Nat), bs.length = n → parsePairs bs = some vs →
+    printPairs vs = bs ∧ ∀ v ∈ vs, v < 65536
+  | 0, bs, vs, hlen, h => by
+    cases bs with
+    | nil =>
+      have h1 : parsePairs ([] : List UInt8) = some [] := rfl
+      rw [h1] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      exact ⟨rfl, by simp⟩
+    | cons a bs' => simp at hlen
+  | 1, bs, vs, hlen, h => by
+    cases bs with
+    | nil => simp at hlen
+    | cons a bs' =>
+      cases bs' with
+      | nil => simp [parsePairs] at h
+      | cons b rest => simp at hlen
+  | n + 2, bs, vs, hlen, h => by
+    cases bs with
+    | nil => simp at hlen
+    | cons a bs' =>
+      cases bs' with
+      | nil => simp at hlen
+      | cons b rest =>
+        have hrest : rest.length = n := by
+          simp only [List.length_cons] at hlen
+          omega
+        have hstep : parsePairs (a :: b :: rest)
+            = (parsePairs rest).map
+              (fun vs' => u16 a b :: vs') := rfl
+        rw [hstep] at h
+        obtain ⟨vs', hrec, hvs⟩ := Option.map_eq_some_iff.mp h
+        obtain ⟨hprint, hlt⟩ :=
+          parsePairs_inv_aux n rest vs' hrest hrec
+        refine ⟨?_, ?_⟩
+        · show printPairs vs = a :: b :: rest
+          rw [← hvs]
+          show printPairs (u16 a b :: vs') = a :: b :: rest
+          simp only [printPairs, be16_u16, List.cons_append,
+            List.nil_append, hprint]
+        · rw [← hvs]
+          intro x hx
+          simp only [List.mem_cons] at hx
+          rcases hx with rfl | hx
+          · have ha := toNat_lt a
+            have hb := toNat_lt b
+            simp only [u16]; omega
+          · exact hlt x hx
+
+/-- Two byte values a successful read gives print back to
+    the bytes they were read from, and each fits two
+    bytes. -/
+theorem parsePairs_inv {bs : List UInt8} {vs : List Nat}
+    (h : parsePairs bs = some vs) :
+    printPairs vs = bs ∧ ∀ v ∈ vs, v < 65536 :=
+  parsePairs_inv_aux bs.length bs vs rfl h
+
+/-- The count of values a successful two byte read gives,
+    from the byte count it read. -/
+theorem parsePairs_length {bs : List UInt8} {vs : List Nat}
+    (h : parsePairs bs = some vs) :
+    bs.length = 2 * vs.length := by
+  have h1 := (parsePairs_inv h).1
+  rw [← h1, printPairs_length]
+
+/-! ## Server name entries -/
+
+/-- The printed length of a server name entry list, one entry
+    at a time. -/
+theorem printNameEntries_length_cons (t : Nat)
+    (bs : List UInt8) (es : List (Nat × List UInt8)) :
+    (printNameEntries ((t, bs) :: es)).length
+      = bs.length + 3 + (printNameEntries es).length := by
+  simp only [printNameEntries, be16, List.length_append,
+    List.length_cons, List.length_nil]
+  omega
+
+/-- One step of the server name entry reader, stated for
+    rewriting. -/
+theorem parseNameEntriesGo_step (f : Nat) (t : UInt8)
+    (rest : List UInt8) :
+    parseNameEntriesGo (f + 1) (t :: rest) =
+      getU16 rest >>= fun (n, r1) =>
+      if (r1.take n).length = n then
+        parseNameEntriesGo f (r1.drop n) >>= fun es =>
+        if t.toNat ∈ es.map Prod.fst then none
+        else some ((t.toNat, r1.take n) :: es)
+      else none := rfl
+
+/-- Printed server name entries read back as the entries. -/
+theorem parseNameEntriesGo_print :
+    ∀ (es : List (Nat × List UInt8)) (fuel : Nat),
+    (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) →
+    List.Nodup (es.map Prod.fst) →
+    (printNameEntries es).length < fuel →
+    parseNameEntriesGo fuel (printNameEntries es) = some es := by
+  intro es
+  induction es with
+  | nil =>
+    intro fuel _ _ hf
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    rfl
+  | cons e es ih =>
+    intro fuel hw hnodup hf
+    obtain ⟨t, bs⟩ := e
+    have hhead : t < 256 ∧ bs.length ≤ 65535 :=
+      hw (t, bs) (by simp)
+    have htail : ∀ x ∈ es, x.1 < 256 ∧ x.2.length ≤ 65535 :=
+      fun x hx => hw x (List.mem_cons_of_mem (t, bs) hx)
+    have hnodup' : List.Nodup (es.map Prod.fst) := by
+      have h2 : ((t, bs) :: es).map Prod.fst
+          = t :: es.map Prod.fst := rfl
+      rw [h2] at hnodup
+      exact (List.nodup_cons.mp hnodup).2
+    have hnotin : t ∉ es.map Prod.fst := by
+      have h2 : ((t, bs) :: es).map Prod.fst
+          = t :: es.map Prod.fst := rfl
+      rw [h2] at hnodup
+      exact (List.nodup_cons.mp hnodup).1
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    have hf' : (printNameEntries es).length < f := by
+      have hflen : (printNameEntries ((t, bs) :: es)).length
+          = bs.length + 3 + (printNameEntries es).length :=
+        printNameEntries_length_cons t bs es
+      omega
+    have ht : (t.toUInt8).toNat = t := by
+      rw [toUInt8_toNat]
+      exact Nat.mod_eq_of_lt hhead.1
+    show parseNameEntriesGo (f + 1)
+        ((t.toUInt8 :: (be16 bs.length ++ bs)) ++
+          printNameEntries es)
+      = some ((t, bs) :: es)
+    have hform : (t.toUInt8 :: (be16 bs.length ++ bs)) ++
+          printNameEntries es
+        = t.toUInt8 :: (bs.length / 256).toUInt8 ::
+          bs.length.toUInt8 :: (bs ++ printNameEntries es) := by
+      simp only [be16, List.cons_append, List.nil_append]
+    rw [hform, parseNameEntriesGo_step]
+    show (getU16 ((bs.length / 256).toUInt8 ::
+        bs.length.toUInt8 :: (bs ++ printNameEntries es)) >>=
+      fun (n, r1) =>
+      if (r1.take n).length = n then
+        parseNameEntriesGo f (r1.drop n) >>= fun es' =>
+        if (t.toUInt8).toNat ∈ es'.map Prod.fst then none
+        else some (((t.toUInt8).toNat, r1.take n) :: es')
+      else none) = some ((t, bs) :: es)
+    have hg : getU16 ((bs.length / 256).toUInt8 ::
+        bs.length.toUInt8 :: (bs ++ printNameEntries es))
+        = some (bs.length, bs ++ printNameEntries es) := by
+      show some (u16 (bs.length / 256).toUInt8
+        bs.length.toUInt8, bs ++ printNameEntries es) = _
+      rw [u16_be16 bs.length (by omega)]
+    rw [hg]
+    simp only []
+    show (if ((bs ++ printNameEntries es).take bs.length).length
+        = bs.length then
+      parseNameEntriesGo f ((bs ++ printNameEntries es).drop
+        bs.length) >>= fun es' =>
+      if (t.toUInt8).toNat ∈ es'.map Prod.fst then none
+      else some (((t.toUInt8).toNat,
+        (bs ++ printNameEntries es).take bs.length) :: es')
+      else none) = some ((t, bs) :: es)
+    rw [List.take_left, List.drop_left, ite_eq_left rfl,
+      ih f htail hnodup' hf']
+    show (if (t.toUInt8).toNat ∈ es.map Prod.fst then none
+      else some (((t.toUInt8).toNat, bs) :: es))
+      = some ((t, bs) :: es)
+    rw [ite_eq_right (by rw [ht]; exact hnotin), ht]
+
+/-- Printed server name entries read back, at the top
+    level. -/
+theorem parseNameEntries_print {es : List (Nat × List UInt8)}
+    (hw : ∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535)
+    (hn : List.Nodup (es.map Prod.fst)) :
+    parseNameEntries (printNameEntries es) = some es := by
+  show parseNameEntriesGo ((printNameEntries es).length + 1)
+    (printNameEntries es) = some es
+  exact parseNameEntriesGo_print es _ hw hn (Nat.lt_succ_self _)
+
+/-- Server name entries a successful read gives print back
+    to the bytes they were read from, each name type fits
+    one byte, each name fits two length bytes, and no name
+    type stands twice. -/
+theorem parseNameEntriesGo_inv :
+    ∀ (f : Nat) (bs : List UInt8)
+      (es : List (Nat × List UInt8)),
+    parseNameEntriesGo f bs = some es →
+    printNameEntries es = bs ∧
+    (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) ∧
+    List.Nodup (es.map Prod.fst) := by
+  intro f
+  induction f with
+  | zero =>
+    intro bs es h
+    simp [parseNameEntriesGo] at h
+  | succ f ih =>
+    intro bs es h
+    cases bs with
+    | nil =>
+      have h1 : parseNameEntriesGo (f + 1) ([] : List UInt8)
+          = some [] := rfl
+      rw [h1] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      exact ⟨rfl, by simp, by simp⟩
+    | cons t rest =>
+      rw [parseNameEntriesGo_step] at h
+      obtain ⟨⟨n, r1⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h
+      change (if (r1.take n).length = n then
+          parseNameEntriesGo f (r1.drop n) >>= fun es' =>
+          if t.toNat ∈ es'.map Prod.fst then none
+          else some ((t.toNat, r1.take n) :: es')
+        else none) = some es at h
+      obtain ⟨hrest, hnlt⟩ := getU16_inv hn
+      by_cases hc : (r1.take n).length = n
+      · rw [ite_eq_left hc] at h
+        obtain ⟨es', hrec, h⟩ :=
+          Option.bind_eq_some_iff.mp h
+        obtain ⟨hprint, hprops, hnodup⟩ := ih _ _ hrec
+        by_cases hd : t.toNat ∈ es'.map Prod.fst
+        · rw [ite_eq_left hd] at h
+          simp at h
+        · rw [ite_eq_right hd] at h
+          simp only [Option.some.injEq] at h
+          obtain ⟨rfl, rfl⟩ := h
+          refine ⟨?_, ?_, ?_⟩
+          · show printNameEntries ((t.toNat, r1.take n) :: es')
+              = t :: rest
+            have htake : (r1.take n).length = n := hc
+            show ((t.toNat.toUInt8 ::
+                (be16 (r1.take n).length ++ r1.take n)) ++
+              printNameEntries es') = t :: rest
+            rw [htake, hprint, toNat_toUInt8, hrest]
+            show (t :: ((be16 n ++ r1.take n) ++ r1.drop n))
+              = t :: (be16 n ++ r1)
+            rw [List.append_assoc, List.take_append_drop]
+          · intro x hx
+            simp only [List.mem_cons] at hx
+            rcases hx with rfl | hx
+            · exact ⟨toNat_lt t, by rw [hc]; omega⟩
+            · exact hprops x hx
+          · have h2 : ((t.toNat, r1.take n) :: es').map Prod.fst
+                = t.toNat :: es'.map Prod.fst := rfl
+            rw [h2]
+            exact List.nodup_cons.mpr ⟨hd, hnodup⟩
+      · rw [ite_eq_right hc] at h
+        simp at h
+
+/-- Server name entries a successful read gives print back,
+    at the top level. -/
+theorem parseNameEntries_inv {bs : List UInt8}
+    {es : List (Nat × List UInt8)}
+    (h : parseNameEntries bs = some es) :
+    printNameEntries es = bs ∧
+    (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) ∧
+    List.Nodup (es.map Prod.fst) :=
+  parseNameEntriesGo_inv _ _ _ h
+
+/-- The server name value check holds for a list the printer
+    can write: nonempty, and every host_name entry
+    nonempty. -/
+theorem validNames_of {es : List (Nat × List UInt8)}
+    (hne : es ≠ [])
+    (hhost : ∀ e ∈ es, e.1 = 0 → e.2 ≠ []) :
+    validNames es = true := by
+  unfold validNames
+  rw [Bool.and_eq_true]
+  constructor
+  · cases es with
+    | nil => exact absurd rfl hne
+    | cons e es' => rfl
+  · rw [List.all_eq_true]
+    intro e he
+    simp only [decide_eq_true_eq]
+    by_cases h0 : e.1 = 0
+    · exact Or.inr (hhost e he h0)
+    · exact Or.inl h0
+
+/-- A server name list that passes the value check is
+    nonempty, and its host_name entries are nonempty. -/
+theorem validNames_true {es : List (Nat × List UInt8)}
+    (h : validNames es = true) :
+    es ≠ [] ∧ ∀ e ∈ es, e.1 = 0 → e.2 ≠ [] := by
+  have hne : es ≠ [] := by
+    cases es with
+    | nil => simp [validNames] at h
+    | cons e es' => simp
+  have hall : ∀ e ∈ es, e.1 ≠ 0 ∨ e.2 ≠ [] := by
+    have h2 : es.all
+        (fun e => decide (e.1 ≠ 0 ∨ e.2 ≠ [])) = true := by
+      have h' : (!es.isEmpty &&
+          es.all (fun e => decide (e.1 ≠ 0 ∨ e.2 ≠ [])))
+          = true := h
+      rw [Bool.and_eq_true] at h'
+      exact h'.2
+    rw [List.all_eq_true] at h2
+    intro e he
+    have h3 := h2 e he
+    simpa only [decide_eq_true_eq] using h3
+  exact ⟨hne, fun e he h0 =>
+    (hall e he).elim (fun hn => absurd h0 hn) id⟩
+
+/-! ## The server_name value -/
+
+/-- A printed server_name value reads back as the
+    extension. -/
+theorem parseSNI_print {es : List (Nat × List UInt8)}
+    (hne : es ≠ [])
+    (hw : ∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧
+      (e.1 = 0 → e.2 ≠ []))
+    (hnodup : List.Nodup (es.map Prod.fst))
+    (hlen : (printNameEntries es).length ≤ 65533) :
+    parseSNI (printExtValue (.serverName es))
+      = some (.serverName es) := by
+  have hw' : ∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 :=
+    fun e he => ⟨(hw e he).1, (hw e he).2.1⟩
+  show parseSNI (be16 (printNameEntries es).length ++
+      printNameEntries es) = some (Extension.serverName es)
+  unfold parseSNI
+  rw [getU16_be16 _ (by omega)]
+  simp only []
+  show (if (printNameEntries es).length
+        = (printNameEntries es).length then
+      parseNameEntries (printNameEntries es) >>= fun es' =>
+      if validNames es' then some (Extension.serverName es') else none
+    else none) = some (Extension.serverName es)
+  rw [ite_eq_left rfl, parseNameEntries_print hw' hnodup]
+  show (if validNames es then some (Extension.serverName es)
+    else none) = some (Extension.serverName es)
+  rw [ite_eq_left (validNames_of hne (fun e he => (hw e he).2.2))]
+
+/-- A server_name value a successful read gives is the
+    printed form of the extension it gives, and the
+    extension is well formed. The value length bound comes
+    from the caller: an extension value fits two length
+    bytes. -/
+theorem parseSNI_inv {v : List UInt8} {e : Extension}
+    (hv : v.length ≤ 65535) (h : parseSNI v = some e) :
+    ∃ es, e = .serverName es ∧
+      printExtValue (.serverName es) = v ∧
+      ExtWF (.serverName es) := by
+  unfold parseSNI at h
+  obtain ⟨⟨n, rest⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h
+  change (if rest.length = n then
+      parseNameEntries rest >>= fun es =>
+      if validNames es then some (.serverName es) else none
+    else none) = some e at h
+  obtain ⟨hrest, hnlt⟩ := getU16_inv hn
+  by_cases hc : rest.length = n
+  · rw [ite_eq_left hc] at h
+    obtain ⟨es, hrec, h⟩ := Option.bind_eq_some_iff.mp h
+    by_cases hval : validNames es = true
+    · rw [ite_eq_left hval] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      obtain ⟨hprint, hprops, hnodup⟩ := parseNameEntries_inv hrec
+      obtain ⟨hne, hhost⟩ := validNames_true hval
+      refine ⟨es, rfl, ?_, ?_⟩
+      · show be16 (printNameEntries es).length ++
+          printNameEntries es = v
+        rw [hprint, hc, hrest]
+      · exact ⟨hne, fun x hx =>
+          ⟨(hprops x hx).1, (hprops x hx).2, hhost x hx⟩,
+          hnodup, by
+          have h2 : (printNameEntries es).length = rest.length := by
+            rw [hprint]
+          have hvlen : v.length = rest.length + 2 := by
+            rw [hrest]; simp [be16]
+          omega⟩
+    · rw [ite_eq_right hval] at h
+      simp at h
+  · rw [ite_eq_right hc] at h
+    simp at h
+
+/-! ## ALPN protocol names -/
+
+/-- The printed length of an ALPN name list, one name at a
+    time. -/
+theorem printAlpnNames_length_cons (n : List UInt8)
+    (ns : List (List UInt8)) :
+    (printAlpnNames (n :: ns)).length
+      = n.length + 1 + (printAlpnNames ns).length := by
+  simp only [printAlpnNames, List.length_append,
+    List.length_cons]
+
+/-- One step of the ALPN name reader, stated for
+    rewriting. -/
+theorem parseAlpnGo_step (f : Nat) (len : UInt8)
+    (rest : List UInt8) :
+    parseAlpnGo (f + 1) (len :: rest) =
+      if len.toNat = 0 then none
+      else if (rest.take len.toNat).length = len.toNat then
+        (parseAlpnGo f (rest.drop len.toNat)).map
+          (fun ns => (rest.take len.toNat) :: ns)
+      else none := rfl
+
+/-- Printed ALPN names read back as the names. -/
+theorem parseAlpnGo_print :
+    ∀ (ns : List (List UInt8)) (fuel : Nat),
+    (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) →
+    (printAlpnNames ns).length < fuel →
+    parseAlpnGo fuel (printAlpnNames ns) = some ns := by
+  intro ns
+  induction ns with
+  | nil =>
+    intro fuel _ hf
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    rfl
+  | cons n ns ih =>
+    intro fuel hw hf
+    have hhead : n ≠ [] ∧ n.length ≤ 255 := hw n (by simp)
+    have htail : ∀ x ∈ ns, x ≠ [] ∧ x.length ≤ 255 :=
+      fun x hx => hw x (List.mem_cons_of_mem n hx)
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    have hf' : (printAlpnNames ns).length < f := by
+      have hflen : (printAlpnNames (n :: ns)).length
+          = n.length + 1 + (printAlpnNames ns).length :=
+        printAlpnNames_length_cons n ns
+      omega
+    have hlen : (n.length.toUInt8).toNat = n.length := by
+      rw [toUInt8_toNat]
+      exact Nat.mod_eq_of_lt (by omega)
+    show parseAlpnGo (f + 1)
+        ((n.length.toUInt8 :: n) ++ printAlpnNames ns)
+      = some (n :: ns)
+    have hform : (n.length.toUInt8 :: n) ++ printAlpnNames ns
+        = n.length.toUInt8 :: (n ++ printAlpnNames ns) := by
+      simp only [List.cons_append]
+    rw [hform, parseAlpnGo_step, hlen,
+      ite_eq_right (by
+        intro hcon
+        cases n with
+        | nil => exact hhead.1 rfl
+        | cons b bs => simp at hcon),
+      List.take_left, List.drop_left, ite_eq_left rfl, ih f htail hf']
+    rfl
+
+/-- Printed ALPN names read back, at the top level. -/
+theorem parseAlpnNames_print {ns : List (List UInt8)}
+    (hw : ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) :
+    parseAlpnNames (printAlpnNames ns) = some ns := by
+  show parseAlpnGo ((printAlpnNames ns).length + 1)
+    (printAlpnNames ns) = some ns
+  exact parseAlpnGo_print ns _ hw (Nat.lt_succ_self _)
+
+/-- ALPN names a successful read gives print back to the
+    bytes they were read from, and each name is nonempty
+    and fits one length byte. -/
+theorem parseAlpnGo_inv :
+    ∀ (f : Nat) (bs : List UInt8) (ns : List (List UInt8)),
+    parseAlpnGo f bs = some ns →
+    printAlpnNames ns = bs ∧
+    ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255 := by
+  intro f
+  induction f with
+  | zero =>
+    intro bs ns h
+    simp [parseAlpnGo] at h
+  | succ f ih =>
+    intro bs ns h
+    cases bs with
+    | nil =>
+      have h1 : parseAlpnGo (f + 1) ([] : List UInt8)
+          = some [] := rfl
+      rw [h1] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      exact ⟨rfl, by simp⟩
+    | cons len rest =>
+      rw [parseAlpnGo_step] at h
+      by_cases h0 : len.toNat = 0
+      · rw [ite_eq_left h0] at h
+        simp at h
+      · rw [ite_eq_right h0] at h
+        by_cases hc : (rest.take len.toNat).length = len.toNat
+        · rw [ite_eq_left hc] at h
+          obtain ⟨ns', hrec, hns⟩ := Option.map_eq_some_iff.mp h
+          obtain ⟨hprint, hprops⟩ := ih _ _ hrec
+          refine ⟨?_, ?_⟩
+          · show printAlpnNames ns = len :: rest
+            rw [← hns]
+            show printAlpnNames ((rest.take len.toNat) :: ns')
+              = len :: rest
+            have htake : (rest.take len.toNat).length
+                = len.toNat := hc
+            show ((rest.take len.toNat).length.toUInt8 ::
+                rest.take len.toNat) ++ printAlpnNames ns'
+              = len :: rest
+            rw [htake, toNat_toUInt8, hprint]
+            show len :: (rest.take len.toNat ++ rest.drop len.toNat)
+              = len :: rest
+            rw [List.take_append_drop]
+          · intro x hx
+            rw [← hns] at hx
+            simp only [List.mem_cons] at hx
+            rcases hx with rfl | hx
+            · refine ⟨?_, by rw [hc]; have h := toNat_lt len; omega⟩
+              intro hcon
+              rw [hcon] at hc
+              simp at hc
+              omega
+            · exact hprops x hx
+        · rw [ite_eq_right hc] at h
+          simp at h
+
+/-- ALPN names a successful read gives print back, at the
+    top level. -/
+theorem parseAlpnNames_inv {bs : List UInt8}
+    {ns : List (List UInt8)}
+    (h : parseAlpnNames bs = some ns) :
+    printAlpnNames ns = bs ∧
+    ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255 :=
+  parseAlpnGo_inv _ _ _ h
+
+/-- A printed ALPN value reads back as the extension. -/
+theorem parseALPN_print {ns : List (List UInt8)}
+    (hne : ns ≠ [])
+    (hw : ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255)
+    (hlen : (printAlpnNames ns).length ≤ 65533) :
+    parseALPN (printExtValue (.alpn ns)) = some (.alpn ns) := by
+  show parseALPN (be16 (printAlpnNames ns).length ++
+      printAlpnNames ns) = some (Extension.alpn ns)
+  unfold parseALPN
+  rw [getU16_be16 _ (by omega)]
+  simp only []
+  show (if (printAlpnNames ns).length
+        = (printAlpnNames ns).length then
+      parseAlpnNames (printAlpnNames ns) >>= fun ns' =>
+      if ns'.isEmpty then none else some (Extension.alpn ns')
+    else none) = some (Extension.alpn ns)
+  rw [ite_eq_left rfl, parseAlpnNames_print hw]
+  show (if ns.isEmpty then none else some (Extension.alpn ns))
+    = some (Extension.alpn ns)
+  rw [ite_eq_right (by
+    cases ns with
+    | nil => exact absurd rfl hne
+    | cons n ns' => simp)]
+
+/-- An ALPN value a successful read gives is the printed
+    form of the extension it gives, and the extension is
+    well formed. -/
+theorem parseALPN_inv {v : List UInt8} {e : Extension}
+    (hv : v.length ≤ 65535) (h : parseALPN v = some e) :
+    ∃ ns, e = .alpn ns ∧
+      printExtValue (.alpn ns) = v ∧ ExtWF (.alpn ns) := by
+  unfold parseALPN at h
+  obtain ⟨⟨n, rest⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h
+  change (if rest.length = n then
+      parseAlpnNames rest >>= fun ns =>
+      if ns.isEmpty then none else some (.alpn ns)
+    else none) = some e at h
+  obtain ⟨hrest, hnlt⟩ := getU16_inv hn
+  by_cases hc : rest.length = n
+  · rw [ite_eq_left hc] at h
+    obtain ⟨ns, hrec, h⟩ := Option.bind_eq_some_iff.mp h
+    by_cases hemp : ns.isEmpty = false
+    · rw [ite_eq_right (by
+        intro hcon
+        rw [hcon] at hemp
+        simp at hemp)] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      obtain ⟨hprint, hprops⟩ := parseAlpnNames_inv hrec
+      have hne : ns ≠ [] := by
+        cases ns with
+        | nil => simp at hemp
+        | cons n' ns' => simp
+      refine ⟨ns, rfl, ?_, ?_⟩
+      · show be16 (printAlpnNames ns).length ++
+          printAlpnNames ns = v
+        rw [hprint, hc, hrest]
+      · exact ⟨hne, hprops, by
+          have h2 : (printAlpnNames ns).length = rest.length := by
+            rw [hprint]
+          have hvlen : v.length = rest.length + 2 := by
+            rw [hrest]; simp [be16]
+          omega⟩
+    · have hemp2 : ns.isEmpty = true := by
+        cases h' : ns.isEmpty with
+        | true => rfl
+        | false => exact absurd h' hemp
+      rw [ite_eq_left hemp2] at h
+      simp at h
+  · rw [ite_eq_right hc] at h
+    simp at h
+
+/-! ## The supported_versions value -/
+
+/-- A printed supported_versions value reads back as the
+    extension. -/
+theorem parseSV_print {vs : List Nat}
+    (hne : vs ≠ []) (hw : ∀ v ∈ vs, v < 65536)
+    (hlen : vs.length ≤ 127) :
+    parseSV (printExtValue (.supportedVersions vs))
+      = some (.supportedVersions vs) := by
+  show parseSV ((printPairs vs).length.toUInt8 ::
+      printPairs vs) = some (.supportedVersions vs)
+  have hlen2 : ((printPairs vs).length.toUInt8).toNat
+      = (printPairs vs).length := by
+    rw [toUInt8_toNat, printPairs_length]
+    have : 2 * vs.length < 256 := by omega
+    exact Nat.mod_eq_of_lt this
+  have hcond : (printPairs vs).length
+        = ((printPairs vs).length.toUInt8).toNat ∧
+      ((printPairs vs).length.toUInt8).toNat % 2 = 0 ∧
+      2 ≤ ((printPairs vs).length.toUInt8).toNat := by
+    rw [hlen2, printPairs_length]
+    refine ⟨rfl, by omega, by
+      cases vs with
+      | nil => exact absurd rfl hne
+      | cons v vs' => simp; omega⟩
+  show (if (printPairs vs).length
+        = ((printPairs vs).length.toUInt8).toNat ∧
+      ((printPairs vs).length.toUInt8).toNat % 2 = 0 ∧
+      2 ≤ ((printPairs vs).length.toUInt8).toNat then
+      parsePairs (printPairs vs) >>= fun vs' =>
+        some (Extension.supportedVersions vs')
+    else none) = some (Extension.supportedVersions vs)
+  rw [ite_eq_left hcond, parsePairs_printPairs hw]
+  rfl
+
+/-- A supported_versions value a successful read gives is
+    the printed form of the extension it gives, and the
+    extension is well formed. -/
+theorem parseSV_inv {v : List UInt8} {e : Extension}
+    (h : parseSV v = some e) :
+    ∃ vs, e = .supportedVersions vs ∧
+      printExtValue (.supportedVersions vs) = v ∧
+      ExtWF (.supportedVersions vs) := by
+  cases v with
+  | nil => simp [parseSV] at h
+  | cons n rest =>
+    have hstep : parseSV (n :: rest) =
+        if rest.length = n.toNat ∧ n.toNat % 2 = 0 ∧
+            2 ≤ n.toNat then
+          parsePairs rest >>= fun vs =>
+            some (.supportedVersions vs)
+        else none := rfl
+    rw [hstep] at h
+    by_cases hc : rest.length = n.toNat ∧ n.toNat % 2 = 0 ∧
+        2 ≤ n.toNat
+    · rw [ite_eq_left hc] at h
+      obtain ⟨vs, hrec, h⟩ := Option.bind_eq_some_iff.mp h
+      simp only [Option.some.injEq] at h
+      subst h
+      obtain ⟨hprint, hlt⟩ := parsePairs_inv hrec
+      have hlen := parsePairs_length hrec
+      refine ⟨vs, rfl, ?_, ?_⟩
+      · show (printPairs vs).length.toUInt8 :: printPairs vs
+          = n :: rest
+        rw [hprint]
+        have hbyte : (rest.length).toUInt8 = n := by
+          apply UInt8.toNat_inj.mp
+          show ((rest.length).toUInt8).toNat = n.toNat
+          rw [toUInt8_toNat, hc.1]
+          exact Nat.mod_eq_of_lt (toNat_lt n)
+        rw [hbyte]
+      · refine ⟨?_, hlt, by
+          have h1 := hc.1
+          have h2 := toNat_lt n
+          omega⟩
+        cases vs with
+        | nil =>
+          intro hcon
+          have h5 := (parsePairs_inv hrec).1
+          simp only [printPairs] at h5
+          have hz : rest.length = 0 := by
+            rw [← h5]
+            simp
+          have h1 := hc.1
+          have h3 := hc.2.2
+          omega
+        | cons v' vs' => intro hcon; cases hcon
+    · rw [ite_eq_right hc] at h
+      simp at h
+
+/-! ## Key share entries -/
+
+/-- The printed length of a key share entry list, one entry
+    at a time. -/
+theorem printShares_length_cons (g : Nat) (k : List UInt8)
+    (ss : List (Nat × List UInt8)) :
+    (printShares ((g, k) :: ss)).length
+      = k.length + 4 + (printShares ss).length := by
+  show ((be16 g ++ (be16 k.length ++ k)) ++
+    printShares ss).length = _
+  rw [List.length_append, List.length_append,
+    List.length_append]
+  simp only [be16, List.length_cons, List.length_nil]
+  omega
+
+/-- One step of the key share entry reader, stated for
+    rewriting. -/
+theorem parseSharesGo_step (f : Nat) (x y : UInt8)
+    (rest : List UInt8) :
+    parseSharesGo (f + 1) (x :: y :: rest) =
+      getU16 (x :: y :: rest) >>= fun (g, r1) =>
+      getU16 r1 >>= fun (n, r2) =>
+      if n = 0 then none
+      else if (r2.take n).length = n then
+        parseSharesGo f (r2.drop n) >>= fun ss =>
+        if g ∈ ss.map Prod.fst then none
+        else some ((g, r2.take n) :: ss)
+      else none := rfl
+
+/-- Printed key share entries read back as the entries. -/
+theorem parseSharesGo_print :
+    ∀ (ss : List (Nat × List UInt8)) (fuel : Nat),
+    (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ s.2.length ≤ 65535) →
+    List.Nodup (ss.map Prod.fst) →
+    (printShares ss).length < fuel →
+    parseSharesGo fuel (printShares ss) = some ss := by
+  intro ss
+  induction ss with
+  | nil =>
+    intro fuel _ _ hf
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    rfl
+  | cons s ss ih =>
+    intro fuel hw hnodup hf
+    obtain ⟨g, k⟩ := s
+    have hhead : g < 65536 ∧ k ≠ [] ∧ k.length ≤ 65535 :=
+      hw (g, k) (by simp)
+    have htail : ∀ x ∈ ss, x.1 < 65536 ∧ x.2 ≠ [] ∧
+        x.2.length ≤ 65535 :=
+      fun x hx => hw x (List.mem_cons_of_mem (g, k) hx)
+    have hnodup' : List.Nodup (ss.map Prod.fst) := by
+      have h2 : ((g, k) :: ss).map Prod.fst
+          = g :: ss.map Prod.fst := rfl
+      rw [h2] at hnodup
+      exact (List.nodup_cons.mp hnodup).2
+    have hnotin : g ∉ ss.map Prod.fst := by
+      have h2 : ((g, k) :: ss).map Prod.fst
+          = g :: ss.map Prod.fst := rfl
+      rw [h2] at hnodup
+      exact (List.nodup_cons.mp hnodup).1
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    have hf' : (printShares ss).length < f := by
+      have hflen : (printShares ((g, k) :: ss)).length
+          = k.length + 4 + (printShares ss).length :=
+        printShares_length_cons g k ss
+      omega
+    show parseSharesGo (f + 1)
+        ((be16 g ++ (be16 k.length ++ k)) ++ printShares ss)
+      = some ((g, k) :: ss)
+    have hform : (be16 g ++ (be16 k.length ++ k)) ++
+          printShares ss
+        = be16 g ++ (be16 k.length ++ (k ++ printShares ss)) := by
+      simp only [← List.append_assoc]
+    rw [hform]
+    show parseSharesGo (f + 1) ((g / 256).toUInt8 ::
+        g.toUInt8 :: ((k.length / 256).toUInt8 ::
+        k.length.toUInt8 :: (k ++ printShares ss)))
+      = some ((g, k) :: ss)
+    rw [parseSharesGo_step]
+    have hg : getU16 ((g / 256).toUInt8 :: g.toUInt8 ::
+        ((k.length / 256).toUInt8 :: k.length.toUInt8 ::
+          (k ++ printShares ss)))
+        = some (g, (k.length / 256).toUInt8 ::
+            k.length.toUInt8 :: (k ++ printShares ss)) := by
+      show some (u16 (g / 256).toUInt8 g.toUInt8, _) = _
+      rw [u16_be16 g hhead.1]
+    rw [hg]
+    simp only []
+    show (getU16 ((k.length / 256).toUInt8 ::
+        k.length.toUInt8 :: (k ++ printShares ss)) >>=
+        fun (n, r2) =>
+        if n = 0 then none
+        else if (r2.take n).length = n then
+          parseSharesGo f (r2.drop n) >>= fun ss' =>
+          if g ∈ ss'.map Prod.fst then none
+          else some ((g, r2.take n) :: ss')
+        else none) = some ((g, k) :: ss)
+    have hk : getU16 ((k.length / 256).toUInt8 ::
+        k.length.toUInt8 :: (k ++ printShares ss))
+        = some (k.length, k ++ printShares ss) := by
+      show some (u16 (k.length / 256).toUInt8
+        k.length.toUInt8, _) = _
+      rw [u16_be16 _ (by omega)]
+    rw [hk]
+    simp only []
+    show (if k.length = 0 then none
+        else if ((k ++ printShares ss).take k.length).length
+            = k.length then
+          parseSharesGo f ((k ++ printShares ss).drop
+            k.length) >>= fun ss' =>
+          if g ∈ ss'.map Prod.fst then none
+          else some ((g, (k ++ printShares ss).take
+            k.length) :: ss')
+        else none) = some ((g, k) :: ss)
+    rw [ite_eq_right (by
+        intro hcon
+        cases k with
+        | nil => exact hhead.2.1 rfl
+        | cons b bs => simp at hcon),
+      List.take_left, List.drop_left, ite_eq_left rfl,
+      ih f htail hnodup' hf']
+    show (if g ∈ ss.map Prod.fst then none
+      else some ((g, k) :: ss)) = some ((g, k) :: ss)
+    rw [ite_eq_right hnotin]
+
+/-- Printed key share entries read back, at the top
+    level. -/
+theorem parseShares_print {ss : List (Nat × List UInt8)}
+    (hw : ∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+      s.2.length ≤ 65535)
+    (hn : List.Nodup (ss.map Prod.fst)) :
+    parseShares (printShares ss) = some ss := by
+  show parseSharesGo ((printShares ss).length + 1)
+    (printShares ss) = some ss
+  exact parseSharesGo_print ss _ hw hn (Nat.lt_succ_self _)
+
+/-- Key share entries a successful read gives print back to
+    the bytes they were read from, each group fits two
+    bytes, each key is nonempty and fits two length bytes,
+    and no group stands twice. -/
+theorem parseSharesGo_inv :
+    ∀ (f : Nat) (bs : List UInt8)
+      (ss : List (Nat × List UInt8)),
+    parseSharesGo f bs = some ss →
+    printShares ss = bs ∧
+    (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+      s.2.length ≤ 65535) ∧
+    List.Nodup (ss.map Prod.fst) := by
+  intro f
+  induction f with
+  | zero =>
+    intro bs ss h
+    simp [parseSharesGo] at h
+  | succ f ih =>
+    intro bs ss h
+    cases bs with
+    | nil =>
+      have h1 : parseSharesGo (f + 1) ([] : List UInt8)
+          = some [] := rfl
+      rw [h1] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      exact ⟨rfl, by simp, by simp⟩
+    | cons b1 rest =>
+      cases rest with
+      | nil => simp [parseSharesGo, getU16] at h
+      | cons b2 rest =>
+        rw [parseSharesGo_step] at h
+        obtain ⟨⟨g, r1⟩, hg, h⟩ := Option.bind_eq_some_iff.mp h
+        change (getU16 r1 >>= fun (n, r2) =>
+          if n = 0 then none
+          else if (r2.take n).length = n then
+            parseSharesGo f (r2.drop n) >>= fun ss =>
+            if g ∈ ss.map Prod.fst then none
+            else some ((g, r2.take n) :: ss)
+          else none) = some ss at h
+        obtain ⟨⟨n, r2⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h
+        change (if n = 0 then none
+          else if (r2.take n).length = n then
+            parseSharesGo f (r2.drop n) >>= fun ss' =>
+            if g ∈ ss'.map Prod.fst then none
+            else some ((g, r2.take n) :: ss')
+          else none) = some ss at h
+        obtain ⟨hbs, hglt⟩ := getU16_inv hg
+        obtain ⟨hr1, hnlt⟩ := getU16_inv hn
+        by_cases h0 : n = 0
+        · rw [ite_eq_left h0] at h
+          simp at h
+        · rw [ite_eq_right h0] at h
+          by_cases hc : (r2.take n).length = n
+          · rw [ite_eq_left hc] at h
+            obtain ⟨ss', hrec, h⟩ := Option.bind_eq_some_iff.mp h
+            obtain ⟨hprint, hprops, hnodup⟩ := ih _ _ hrec
+            by_cases hd : g ∈ ss'.map Prod.fst
+            · rw [ite_eq_left hd] at h
+              simp at h
+            · rw [ite_eq_right hd] at h
+              simp only [Option.some.injEq] at h
+              obtain ⟨rfl, rfl⟩ := h
+              refine ⟨?_, ?_, ?_⟩
+              · have htake : (r2.take n).length = n := hc
+                show ((be16 g ++ (be16 (r2.take n).length ++
+                    r2.take n)) ++ printShares ss')
+                  = b1 :: b2 :: rest
+                rw [htake, hprint, hbs, hr1]
+                simp only [List.append_assoc]
+                rw [List.take_append_drop]
+              · intro x hx
+                simp only [List.mem_cons] at hx
+                rcases hx with rfl | hx
+                · exact ⟨hglt, by
+                    intro hcon
+                    change r2.take n = [] at hcon
+                    rw [hcon] at hc
+                    exact h0 hc.symm, by
+                    change (r2.take n).length ≤ 65535
+                    rw [hc]; omega⟩
+                · exact hprops x hx
+              · have h2 : ((g, r2.take n) :: ss').map Prod.fst
+                    = g :: ss'.map Prod.fst := rfl
+                rw [h2]
+                exact List.nodup_cons.mpr ⟨hd, hnodup⟩
+          · rw [ite_eq_right hc] at h
+            simp at h
+
+/-- Key share entries a successful read gives print back,
+    at the top level. -/
+theorem parseShares_inv {bs : List UInt8}
+    {ss : List (Nat × List UInt8)}
+    (h : parseShares bs = some ss) :
+    printShares ss = bs ∧
+    (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+      s.2.length ≤ 65535) ∧
+    List.Nodup (ss.map Prod.fst) :=
+  parseSharesGo_inv _ _ _ h
+
+/-- A printed key_share value reads back as the
+    extension. The list may be empty. -/
+theorem parseKS_print {ss : List (Nat × List UInt8)}
+    (hw : ∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+      s.2.length ≤ 65535)
+    (hnodup : List.Nodup (ss.map Prod.fst))
+    (hlen : (printShares ss).length ≤ 65533) :
+    parseKS (printExtValue (.keyShare ss))
+      = some (.keyShare ss) := by
+  show parseKS (be16 (printShares ss).length ++
+      printShares ss) = some (Extension.keyShare ss)
+  unfold parseKS
+  rw [getU16_be16 _ (by omega)]
+  simp only []
+  show (if (printShares ss).length
+        = (printShares ss).length then
+      parseShares (printShares ss) >>= fun ss' =>
+        some (Extension.keyShare ss')
+    else none) = some (Extension.keyShare ss)
+  rw [ite_eq_left rfl, parseShares_print hw hnodup]
+  rfl
+
+/-- A key_share value a successful read gives is the
+    printed form of the extension it gives, and the
+    extension is well formed. -/
+theorem parseKS_inv {v : List UInt8} {e : Extension}
+    (hv : v.length ≤ 65535) (h : parseKS v = some e) :
+    ∃ ss, e = .keyShare ss ∧
+      printExtValue (.keyShare ss) = v ∧
+      ExtWF (.keyShare ss) := by
+  unfold parseKS at h
+  obtain ⟨⟨n, rest⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h
+  change (if rest.length = n then
+      parseShares rest >>= fun ss => some (.keyShare ss)
+    else none) = some e at h
+  obtain ⟨hrest, hnlt⟩ := getU16_inv hn
+  by_cases hc : rest.length = n
+  · rw [ite_eq_left hc] at h
+    obtain ⟨ss, hrec, h⟩ := Option.bind_eq_some_iff.mp h
+    simp only [Option.some.injEq] at h
+    subst h
+    obtain ⟨hprint, hprops, hnodup⟩ := parseShares_inv hrec
+    refine ⟨ss, rfl, ?_, ?_⟩
+    · show be16 (printShares ss).length ++
+        printShares ss = v
+      rw [hprint, hc, hrest]
+    · exact ⟨hprops, hnodup, by
+        have h2 : (printShares ss).length = rest.length := by
+          rw [hprint]
+        have hvlen : v.length = rest.length + 2 := by
+          rw [hrest]; simp [be16]
+        omega⟩
+  · rw [ite_eq_right hc] at h
+    simp at h
+
+/-! ## Extension values, dispatched by type -/
+
+/-- The type of a well formed extension fits two bytes. -/
+theorem extType_lt {e : Extension} (h : ExtWF e) :
+    extType e < 65536 := by
+  rcases e with ⟨es⟩ | ⟨ns⟩ | ⟨vs⟩ | ⟨ss⟩ | ⟨t, v⟩
+  · show (0 : Nat) < 65536; omega
+  · show (16 : Nat) < 65536; omega
+  · show (43 : Nat) < 65536; omega
+  · show (51 : Nat) < 65536; omega
+  · have h' : ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧
+        t < 65536 ∧ v.length ≤ 65535 := h
+    exact h'.2.1
+
+/-- The printed value of a well formed extension fits two
+    length bytes. -/
+theorem printExtValue_length_le {e : Extension}
+    (h : ExtWF e) : (printExtValue e).length ≤ 65535 := by
+  rcases e with ⟨es⟩ | ⟨ns⟩ | ⟨vs⟩ | ⟨ss⟩ | ⟨t, v⟩
+  ·
+    have h' : es ≠ [] ∧
+        (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧
+          (e.1 = 0 → e.2 ≠ [])) ∧
+        List.Nodup (es.map Prod.fst) ∧
+        (printNameEntries es).length ≤ 65533 := h
+    show (be16 (printNameEntries es).length ++
+      printNameEntries es).length ≤ 65535
+    rw [List.length_append]
+    simp [be16]
+    omega
+  · have h' : ns ≠ [] ∧
+        (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) ∧
+        (printAlpnNames ns).length ≤ 65533 := h
+    show (be16 (printAlpnNames ns).length ++
+      printAlpnNames ns).length ≤ 65535
+    rw [List.length_append]
+    simp [be16]
+    omega
+  · have h' : vs ≠ [] ∧ (∀ v ∈ vs, v < 65536) ∧
+        vs.length ≤ 127 := h
+    show ((printPairs vs).length.toUInt8 ::
+      printPairs vs).length ≤ 65535
+    rw [List.length_cons, printPairs_length]
+    omega
+  · have h' : (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+          s.2.length ≤ 65535) ∧
+        List.Nodup (ss.map Prod.fst) ∧
+        (printShares ss).length ≤ 65533 := h
+    show (be16 (printShares ss).length ++
+      printShares ss).length ≤ 65535
+    rw [List.length_append]
+    simp [be16]
+    omega
+  · have h' : ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧
+        t < 65536 ∧ v.length ≤ 65535 := h
+    exact h'.2.2
+
+/-- A printed extension value reads back as the extension,
+    at its own type. -/
+theorem parseExtValue_printExtValue (e : Extension)
+    (h : ExtWF e) :
+    parseExtValue (extType e) (printExtValue e) = some e := by
+  rcases e with ⟨es⟩ | ⟨ns⟩ | ⟨vs⟩ | ⟨ss⟩ | ⟨t, v⟩
+  ·
+    have h' : es ≠ [] ∧
+        (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧
+          (e.1 = 0 → e.2 ≠ [])) ∧
+        List.Nodup (es.map Prod.fst) ∧
+        (printNameEntries es).length ≤ 65533 := h
+    show parseExtValue 0 (printExtValue
+      (Extension.serverName es)) = some (Extension.serverName es)
+    unfold parseExtValue
+    rw [ite_eq_left rfl]
+    exact parseSNI_print h'.1 h'.2.1 h'.2.2.1 h'.2.2.2
+  · have h' : ns ≠ [] ∧
+        (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) ∧
+        (printAlpnNames ns).length ≤ 65533 := h
+    show parseExtValue 16 (printExtValue
+      (Extension.alpn ns)) = some (Extension.alpn ns)
+    unfold parseExtValue
+    rw [ite_eq_right (by decide), ite_eq_left rfl]
+    exact parseALPN_print h'.1 h'.2.1 h'.2.2
+  · have h' : vs ≠ [] ∧ (∀ v ∈ vs, v < 65536) ∧
+        vs.length ≤ 127 := h
+    show parseExtValue 43 (printExtValue
+      (Extension.supportedVersions vs))
+      = some (Extension.supportedVersions vs)
+    unfold parseExtValue
+    rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left rfl]
+    exact parseSV_print h'.1 h'.2.1 h'.2.2
+  · have h' : (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+          s.2.length ≤ 65535) ∧
+        List.Nodup (ss.map Prod.fst) ∧
+        (printShares ss).length ≤ 65533 := h
+    show parseExtValue 51 (printExtValue
+      (Extension.keyShare ss)) = some (Extension.keyShare ss)
+    unfold parseExtValue
+    rw [ite_eq_right (by decide), ite_eq_right (by decide),
+      ite_eq_right (by decide), ite_eq_left rfl]
+    exact parseKS_print h'.1 h'.2.1 h'.2.2
+  · have h' : ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧
+        t < 65536 ∧ v.length ≤ 65535 := h
+    have hn := not_or.mp h'.1
+    have hn2 := not_or.mp hn.2
+    have hn3 := not_or.mp hn2.2
+    show parseExtValue t (printExtValue
+      (Extension.opaque t v)) = some (Extension.opaque t v)
+    unfold parseExtValue
+    rw [ite_eq_right hn.1, ite_eq_right hn2.1, ite_eq_right hn3.1,
+      ite_eq_right hn3.2]
+    rfl
+
+/-- An extension value a successful read gives is the
+    printed form of the extension it gives, the extension
+    carries the type it was read under, and the extension
+    is well formed. -/
+theorem parseExtValue_inv {t : Nat} {v : List UInt8}
+    {e : Extension}
+    (ht : t < 65536) (hv : v.length ≤ 65535)
+    (h : parseExtValue t v = some e) :
+    extType e = t ∧ printExtValue e = v ∧ ExtWF e := by
+  unfold parseExtValue at h
+  by_cases h0 : t = 0
+  · rw [ite_eq_left h0] at h
+    obtain ⟨es, he, hprint, hwf⟩ := parseSNI_inv hv h
+    refine ⟨?_, ?_, ?_⟩
+    · rw [he]; exact h0.symm
+    · rw [he]; exact hprint
+    · rw [he]; exact hwf
+  · rw [ite_eq_right h0] at h
+    by_cases h16 : t = 16
+    · rw [ite_eq_left h16] at h
+      obtain ⟨ns, he, hprint, hwf⟩ := parseALPN_inv hv h
+      refine ⟨?_, ?_, ?_⟩
+      · rw [he]; exact h16.symm
+      · rw [he]; exact hprint
+      · rw [he]; exact hwf
+    · rw [ite_eq_right h16] at h
+      by_cases h43 : t = 43
+      · rw [ite_eq_left h43] at h
+        obtain ⟨vs, he, hprint, hwf⟩ := parseSV_inv h
+        refine ⟨?_, ?_, ?_⟩
+        · rw [he]; exact h43.symm
+        · rw [he]; exact hprint
+        · rw [he]; exact hwf
+      · rw [ite_eq_right h43] at h
+        by_cases h51 : t = 51
+        · rw [ite_eq_left h51] at h
+          obtain ⟨ss, he, hprint, hwf⟩ := parseKS_inv hv h
+          refine ⟨?_, ?_, ?_⟩
+          · rw [he]; exact h51.symm
+          · rw [he]; exact hprint
+          · rw [he]; exact hwf
+        · rw [ite_eq_right h51] at h
+          simp only [Option.some.injEq] at h
+          subst h
+          refine ⟨rfl, rfl, ?_⟩
+          exact ⟨fun hc => by
+            rcases hc with rfl | rfl | rfl | rfl
+            · exact h0 rfl
+            · exact h16 rfl
+            · exact h43 rfl
+            · exact h51 rfl, ht, hv⟩
+
+/-! ## The extensions block -/
+
+/-- The printed length of one extension: four bytes of type
+    and length, then the value. -/
+theorem printExt_length (e : Extension) :
+    (printExt e).length = (printExtValue e).length + 4 := by
+  show (be16 (extType e) ++ be16 (printExtValue e).length ++
+    printExtValue e).length = _
+  rw [List.length_append, List.length_append]
+  have h1 : (be16 (extType e)).length = 2 := rfl
+  have h2 : (be16 (printExtValue e).length).length = 2 := rfl
+  omega
+
+/-- One step of the extension reader, stated for
+    rewriting. -/
+theorem parseExtsGo_step (f : Nat) (x y : UInt8)
+    (rest : List UInt8) :
+    parseExtsGo (f + 1) (x :: y :: rest) =
+      getU16 (x :: y :: rest) >>= fun (t, r1) =>
+      getU16 r1 >>= fun (n, r2) =>
+      if (r2.take n).length = n then
+        parseExtValue t (r2.take n) >>= fun e =>
+        parseExtsGo f (r2.drop n) >>= fun es =>
+        if extType e ∈ es.map extType then none
+        else some (e :: es)
+      else none := rfl
+
+/-- Printed extensions read back as the extensions. -/
+theorem parseExtsGo_print :
+    ∀ (es : List Extension) (fuel : Nat),
+    (∀ e ∈ es, ExtWF e) →
+    List.Nodup (es.map extType) →
+    (printExts es).length < fuel →
+    parseExtsGo fuel (printExts es) = some es := by
+  intro es
+  induction es with
+  | nil =>
+    intro fuel _ _ hf
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    rfl
+  | cons e es ih =>
+    intro fuel hw hnodup hf
+    have hwe : ExtWF e := hw e (by simp)
+    have htail : ∀ x ∈ es, ExtWF x :=
+      fun x hx => hw x (List.mem_cons_of_mem e hx)
+    have hnodup' : List.Nodup (es.map extType) := by
+      have h2 : (e :: es).map extType
+          = extType e :: es.map extType := rfl
+      rw [h2] at hnodup
+      exact (List.nodup_cons.mp hnodup).2
+    have hnotin : extType e ∉ es.map extType := by
+      have h2 : (e :: es).map extType
+          = extType e :: es.map extType := rfl
+      rw [h2] at hnodup
+      exact (List.nodup_cons.mp hnodup).1
+    obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    have hf' : (printExts es).length < f := by
+      have hflen : (printExts (e :: es)).length
+          = (printExt e).length + (printExts es).length := by
+        show ((printExt e) ++ printExts es).length = _
+        rw [List.length_append]
+      have h2 := printExt_length e
+      omega
+    show parseExtsGo (f + 1)
+        ((be16 (extType e) ++
+          (be16 (printExtValue e).length ++
+            printExtValue e)) ++ printExts es)
+      = some (e :: es)
+    have hform : (be16 (extType e) ++
+          (be16 (printExtValue e).length ++
+            printExtValue e)) ++ printExts es
+        = (extType e / 256).toUInt8 :: (extType e).toUInt8 ::
+          ((printExtValue e).length / 256).toUInt8 ::
+          (printExtValue e).length.toUInt8 ::
+          (printExtValue e ++ printExts es) := by
+      simp only [be16, List.cons_append,
+        List.nil_append]
+    rw [hform, parseExtsGo_step]
+    have hg : getU16 ((extType e / 256).toUInt8 ::
+        (extType e).toUInt8 ::
+        ((printExtValue e).length / 256).toUInt8 ::
+        (printExtValue e).length.toUInt8 ::
+        (printExtValue e ++ printExts es))
+        = some (extType e,
+          ((printExtValue e).length / 256).toUInt8 ::
+          (printExtValue e).length.toUInt8 ::
+          (printExtValue e ++ printExts es)) := by
+      show some (u16 (extType e / 256).toUInt8
+        (extType e).toUInt8, _) = _
+      rw [u16_be16 _ (extType_lt hwe)]
+    rw [hg]
+    simp only []
+    show (getU16 (((printExtValue e).length / 256).toUInt8 ::
+        (printExtValue e).length.toUInt8 ::
+        (printExtValue e ++ printExts es)) >>=
+        fun (n, r2) =>
+        if (r2.take n).length = n then
+          parseExtValue (extType e) (r2.take n) >>= fun e' =>
+          parseExtsGo f (r2.drop n) >>= fun es' =>
+          if extType e' ∈ es'.map extType then none
+          else some (e' :: es')
+        else none) = some (e :: es)
+    have hk : getU16 (((printExtValue e).length / 256).toUInt8 ::
+        (printExtValue e).length.toUInt8 ::
+        (printExtValue e ++ printExts es))
+        = some ((printExtValue e).length,
+          printExtValue e ++ printExts es) := by
+      show some (u16 ((printExtValue e).length / 256).toUInt8
+        (printExtValue e).length.toUInt8, _) = _
+      rw [u16_be16 _ (by
+        have h2 := printExtValue_length_le hwe
+        omega)]
+    rw [hk]
+    simp only []
+    show (if ((printExtValue e ++ printExts es).take
+          (printExtValue e).length).length
+        = (printExtValue e).length then
+      parseExtValue (extType e)
+        ((printExtValue e ++ printExts es).take
+          (printExtValue e).length) >>= fun e' =>
+      parseExtsGo f ((printExtValue e ++ printExts es).drop
+        (printExtValue e).length) >>= fun es' =>
+      if extType e' ∈ es'.map extType then none
+      else some (e' :: es')
+    else none) = some (e :: es)
+    rw [List.take_left, List.drop_left, ite_eq_left rfl,
+      parseExtValue_printExtValue e hwe]
+    show (parseExtsGo f (printExts es) >>= fun es' =>
+      if extType e ∈ es'.map extType then none
+      else some (e :: es')) = some (e :: es)
+    rw [ih f htail hnodup' hf']
+    show (if extType e ∈ es.map extType then none
+      else some (e :: es)) = some (e :: es)
+    rw [ite_eq_right hnotin]
+
+/-- Printed extensions read back, at the top level. -/
+theorem parseExts_print {es : List Extension}
+    (hw : ∀ e ∈ es, ExtWF e)
+    (hn : List.Nodup (es.map extType)) :
+    parseExts (printExts es) = some es := by
+  show parseExtsGo ((printExts es).length + 1)
+    (printExts es) = some es
+  exact parseExtsGo_print es _ hw hn (Nat.lt_succ_self _)
+
+/-- Extensions a successful read gives print back to the
+    bytes they were read from, each extension is well
+    formed, and no type stands twice. -/
+theorem parseExtsGo_inv :
+    ∀ (f : Nat) (bs : List UInt8) (es : List Extension),
+    parseExtsGo f bs = some es →
+    printExts es = bs ∧
+    (∀ e ∈ es, ExtWF e) ∧
+    List.Nodup (es.map extType) := by
+  intro f
+  induction f with
+  | zero =>
+    intro bs es h
+    simp [parseExtsGo] at h
+  | succ f ih =>
+    intro bs es h
+    cases bs with
+    | nil =>
+      have h1 : parseExtsGo (f + 1) ([] : List UInt8)
+          = some [] := rfl
+      rw [h1] at h
+      simp only [Option.some.injEq] at h
+      subst h
+      exact ⟨rfl, by simp, by simp⟩
+    | cons b1 rest =>
+      cases rest with
+      | nil =>
+        have h1 : parseExtsGo (f + 1) [b1] = none := rfl
+        rw [h1] at h
+        simp at h
+      | cons b2 rest =>
+        rw [parseExtsGo_step] at h
+        obtain ⟨⟨t, r1⟩, ht, h⟩ := Option.bind_eq_some_iff.mp h
+        change (getU16 r1 >>= fun (n, r2) =>
+          if (r2.take n).length = n then
+            parseExtValue t (r2.take n) >>= fun e =>
+            parseExtsGo f (r2.drop n) >>= fun es =>
+            if extType e ∈ es.map extType then none
+            else some (e :: es)
+          else none) = some es at h
+        obtain ⟨⟨n, r2⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h
+        change (if (r2.take n).length = n then
+            parseExtValue t (r2.take n) >>= fun e =>
+            parseExtsGo f (r2.drop n) >>= fun es' =>
+            if extType e ∈ es'.map extType then none
+            else some (e :: es')
+          else none) = some es at h
+        obtain ⟨hbs, htlt⟩ := getU16_inv ht
+        obtain ⟨hr1, hnlt⟩ := getU16_inv hn
+        by_cases hc : (r2.take n).length = n
+        · rw [ite_eq_left hc] at h
+          obtain ⟨e, hev, h⟩ := Option.bind_eq_some_iff.mp h
+          obtain ⟨es', hrec, h⟩ := Option.bind_eq_some_iff.mp h
+          obtain ⟨hprint, hprops, hnodup⟩ := ih _ _ hrec
+          obtain ⟨htype, hvalue, hwe⟩ := parseExtValue_inv htlt
+            (by rw [hc]; omega) hev
+          by_cases hd : extType e ∈ es'.map extType
+          · rw [ite_eq_left hd] at h
+            simp at h
+          · rw [ite_eq_right hd] at h
+            simp only [Option.some.injEq] at h
+            subst h
+            refine ⟨?_, ?_, ?_⟩
+            · show printExts (e :: es') = b1 :: b2 :: rest
+              have htake : (r2.take n).length = n := hc
+              show (printExt e ++ printExts es')
+                = b1 :: b2 :: rest
+              show ((be16 (extType e) ++
+                  be16 (printExtValue e).length ++
+                  printExtValue e) ++ printExts es')
+                = b1 :: b2 :: rest
+              rw [htype, hvalue, htake, hprint, hbs, hr1]
+              simp only [List.append_assoc]
+              rw [List.take_append_drop]
+            · intro x hx
+              simp only [List.mem_cons] at hx
+              rcases hx with rfl | hx
+              · exact hwe
+              · exact hprops x hx
+            · have h2 : (e :: es').map extType
+                  = extType e :: es'.map extType := rfl
+              rw [h2]
+              exact List.nodup_cons.mpr ⟨hd, hnodup⟩
+        · rw [ite_eq_right hc] at h
+          simp at h
+
+/-- Extensions a successful read gives print back, at the
+    top level. -/
+theorem parseExts_inv {bs : List UInt8}
+    {es : List Extension}
+    (h : parseExts bs = some es) :
+    printExts es = bs ∧
+    (∀ e ∈ es, ExtWF e) ∧
+    List.Nodup (es.map extType) :=
+  parseExtsGo_inv _ _ _ h
+
+/-! ## The body fields -/
+
+/-- The printed body fields, with each field in front of the
+    rest, in the shape the readers take them apart. -/
+theorem printBodyFields_eq (h : Hello) :
+    printBodyFields h =
+      be16 h.legacyVersion ++ (h.random ++
+      (h.sessionId.length.toUInt8 :: (h.sessionId ++
+      (be16 (printPairs h.cipherSuites).length ++
+      (printPairs h.cipherSuites ++
+      (h.compressionMethods.length.toUInt8 ::
+      (h.compressionMethods ++
+      (be16 (printExts h.extensions).length ++
+      printExts h.extensions)))))))) := by
+  simp only [printBodyFields, List.append_assoc, List.cons_append]
+
+/-- A list holding a supported_versions extension whose list holds
+    0x0304 offers TLS 1.3, wherever the extension and the version
+    stand. -/
+theorem offersTls13_of_mem {exts : List Extension} {vs : List Nat}
+    (h : Extension.supportedVersions vs ∈ exts) (h13 : 772 ∈ vs) :
+    offersTls13 exts = true := by
+  induction exts with
+  | nil => simp at h
+  | cons e es ih =>
+    rcases List.mem_cons.mp h with rfl | h'
+    · simp [offersTls13, h13]
+    · cases e <;> simp [offersTls13, ih h']
+
+/-- A list that offers TLS 1.3 holds a supported_versions
+    extension whose list holds 0x0304. -/
+theorem mem_of_offersTls13 {exts : List Extension}
+    (h : offersTls13 exts = true) :
+    ∃ vs, Extension.supportedVersions vs ∈ exts ∧ 772 ∈ vs := by
+  induction exts with
+  | nil => simp [offersTls13] at h
+  | cons e es ih =>
+    cases e with
+    | supportedVersions vs =>
+      simp only [offersTls13, Bool.or_eq_true] at h
+      rcases h with h | h
+      · exact ⟨vs, List.mem_cons_self, by simpa using h⟩
+      · obtain ⟨ws, hm, h7⟩ := ih h
+        exact ⟨ws, List.mem_cons_of_mem _ hm, h7⟩
+    | _ =>
+      obtain ⟨ws, hm, h7⟩ := ih (by simpa [offersTls13] using h)
+      exact ⟨ws, List.mem_cons_of_mem _ hm, h7⟩
+
+/-- The printed body fields read back as the hello. -/
+theorem parseBodyFields_print (m : Message) (hw : WF m) :
+    parseBodyFields (printBodyFields m.hello) = some m.hello := by
+  obtain ⟨_, hver, hrand, hsess, hsuites_ne, hsuites_lt,
+    hsuites_len, hcomp_ne, hcomp0, hcomp_len, hext_wf,
+    hnodup, hpsk, h13sv, hext_len, _⟩ := hw
+  have h13 : offersTls13 m.hello.extensions = true →
+      m.hello.compressionMethods = [0] := fun ho =>
+    let ⟨vs, hm, h7⟩ := mem_of_offersTls13 ho
+    h13sv vs hm h7
+  have hsuites_len1 : 1 ≤ m.hello.cipherSuites.length := by
+    cases hcs : m.hello.cipherSuites with
+    | nil => exact absurd hcs hsuites_ne
+    | cons v vs' => simp
+  have hcomp_len1 : 1 ≤ m.hello.compressionMethods.length := by
+    cases hcc : m.hello.compressionMethods with
+    | nil => exact absurd hcc hcomp_ne
+    | cons c cs' => simp
+  have hsb : (m.hello.sessionId.length.toUInt8).toNat
+      = m.hello.sessionId.length := by
+    rw [toUInt8_toNat]
+    exact Nat.mod_eq_of_lt (by omega)
+  have hcb : (m.hello.compressionMethods.length.toUInt8).toNat
+      = m.hello.compressionMethods.length := by
+    rw [toUInt8_toNat]
+    exact Nat.mod_eq_of_lt (by omega)
+  have hpl := printPairs_length m.hello.cipherSuites
+  have hguard : (printPairs m.hello.cipherSuites).length % 2 = 0 ∧
+      2 ≤ (printPairs m.hello.cipherSuites).length :=
+    ⟨by omega, by omega⟩
+  rw [printBodyFields_eq]
+  unfold parseBodyFields
+  rw [withU16_be16 hver, withBytes_app hrand, withU8_cons, hsb,
+    ite_eq_left hsess, withBytes_app rfl, withU16_be16 (by omega),
+    ite_eq_left hguard, withBytes_app rfl,
+    parsePairs_printPairs hsuites_lt, Option.bind_some,
+    withU8_cons, hcb, ite_eq_left hcomp_len1, withBytes_app rfl,
+    ite_eq_left hcomp0, withU16_be16 (by omega), withBytes_self,
+    ite_eq_left rfl, parseExts_print hext_wf hnodup, Option.bind_some,
+    ite_eq_left hpsk, ite_eq_left h13]
+
+/-- A parsed hello prints back to the input bytes, and every
+    field satisfies the well formedness bounds. -/
+theorem parseBodyFields_inv {bs : List UInt8} {h : Hello}
+    (hparse : parseBodyFields bs = some h) :
+    printBodyFields h = bs ∧
+    h.legacyVersion < 65536 ∧ h.random.length = 32 ∧
+    h.sessionId.length ≤ 32 ∧
+    h.cipherSuites ≠ [] ∧
+    (∀ v ∈ h.cipherSuites, v < 65536) ∧
+    h.cipherSuites.length ≤ 32767 ∧
+    h.compressionMethods ≠ [] ∧
+    (0 : UInt8) ∈ h.compressionMethods ∧
+    h.compressionMethods.length ≤ 255 ∧
+    (∀ e ∈ h.extensions, ExtWF e) ∧
+    List.Nodup (h.extensions.map extType) ∧
+    41 ∉ (h.extensions.dropLast).map extType ∧
+    (offersTls13 h.extensions = true →
+      h.compressionMethods = [0]) ∧
+    (printExts h.extensions).length ≤ 65535 := by
+  unfold parseBodyFields at hparse
+  obtain ⟨ver, r1, hbs, hver, hp⟩ := withU16_inv hparse
+  obtain ⟨rand, r2, hrand, hr1, hp⟩ := withBytes_inv hp
+  obtain ⟨slen, r3, hr2, _, hp⟩ := withU8_inv hp
+  by_cases hs : slen ≤ 32
+  case neg => rw [ite_eq_right hs] at hp; cases hp
+  rw [ite_eq_left hs] at hp
+  obtain ⟨sess, r4, hsesslen, hr3, hp⟩ := withBytes_inv hp
+  obtain ⟨clen, r5, hr4, hclen_lt, hp⟩ := withU16_inv hp
+  by_cases hg : clen % 2 = 0 ∧ 2 ≤ clen
+  case neg => rw [ite_eq_right hg] at hp; cases hp
+  rw [ite_eq_left hg] at hp
+  obtain ⟨cbytes, r6, hcbyteslen, hr5, hp⟩ := withBytes_inv hp
+  obtain ⟨suites, s7, hp⟩ := Option.bind_eq_some_iff.mp hp
+  obtain ⟨mlen, r7, hr6, hmlen_lt, hp⟩ := withU8_inv hp
+  by_cases hm : 1 ≤ mlen
+  case neg => rw [ite_eq_right hm] at hp; cases hp
+  rw [ite_eq_left hm] at hp
+  obtain ⟨comps, r8, hcomplen, hr7, hp⟩ := withBytes_inv hp
+  by_cases h0 : (0 : UInt8) ∈ comps
+  case neg => rw [ite_eq_right h0] at hp; cases hp
+  rw [ite_eq_left h0] at hp
+  obtain ⟨elen, r9, hr8, helen_lt, hp⟩ := withU16_inv hp
+  obtain ⟨ebytes, r10, hebyteslen, hr9, hp⟩ := withBytes_inv hp
+  by_cases hr : r10 = []
+  case neg => rw [ite_eq_right hr] at hp; cases hp
+  rw [ite_eq_left hr] at hp
+  obtain ⟨exts, s12, hp⟩ := Option.bind_eq_some_iff.mp hp
+  by_cases hpsk : 41 ∉ (exts.dropLast).map extType
+  case neg => rw [ite_eq_right hpsk] at hp; cases hp
+  rw [ite_eq_left hpsk] at hp
+  by_cases h13 : offersTls13 exts = true → comps = [0]
+  case neg => rw [ite_eq_right h13] at hp; cases hp
+  rw [ite_eq_left h13] at hp
+  simp only [Option.some.injEq] at hp
+  subst hp
+  have hpp : printPairs suites = cbytes := (parsePairs_inv s7).1
+  have hsuites_lt : ∀ v ∈ suites, v < 65536 :=
+    (parsePairs_inv s7).2
+  have hplen : cbytes.length = 2 * suites.length :=
+    parsePairs_length s7
+  have hpe : printExts exts = ebytes := (parseExts_inv s12).1
+  have hext_wf : ∀ e ∈ exts, ExtWF e := (parseExts_inv s12).2.1
+  have hnodup : (exts.map extType).Nodup :=
+    (parseExts_inv s12).2.2
+  have hsess_le : sess.length ≤ 32 := by omega
+  have hsuites_ne : suites ≠ [] := by
+    intro hcon
+    rw [hcon, List.length_nil] at hplen
+    omega
+  have hsuites_len : suites.length ≤ 32767 := by omega
+  have hcomp_ne : comps ≠ [] := by
+    intro hcon
+    rw [hcon] at hcomplen
+    simp at hcomplen
+    omega
+  have hcomp_len : comps.length ≤ 255 := by omega
+  have hext_len : (printExts exts).length ≤ 65535 := by
+    rw [hpe, hebyteslen]
+    omega
+  have hprint : printBodyFields
+      ⟨ver, rand, sess, suites, comps, exts⟩ = bs := by
+    rw [printBodyFields_eq]
+    show be16 ver ++ (rand ++
+      (sess.length.toUInt8 :: (sess ++
+      (be16 (printPairs suites).length ++
+      (printPairs suites ++
+      (comps.length.toUInt8 :: (comps ++
+      (be16 (printExts exts).length ++
+      printExts exts)))))))) = bs
+    rw [hsesslen, hcomplen, hpp, hcbyteslen, hpe, hebyteslen,
+      hbs, hr1, hr2, hr3, hr4, hr5, hr6, hr7, hr8, hr9, hr,
+      List.append_nil]
+  exact ⟨hprint, hver, hrand, hsess_le, hsuites_ne, hsuites_lt,
+    hsuites_len, hcomp_ne, h0, hcomp_len, hext_wf, hnodup, hpsk,
+    h13, hext_len⟩
+
+/-! ## The handshake message and the record -/
+
+/-- The printed handshake message is four bytes longer than
+    the printed body fields. -/
+theorem printBody_length (h : Hello) :
+    (printBody h).length = (printBodyFields h).length + 4 := by
+  simp [printBody, be24]
+
+/-- The printed handshake message, as its type byte in front
+    of the rest. -/
+theorem printBody_eq (h : Hello) :
+    printBody h = (1 : UInt8) ::
+      (be24 (printBodyFields h).length ++ printBodyFields h) :=
+  rfl
+
+/-- The printed handshake message reads back as the hello. -/
+theorem parseBody_print (m : Message) (hw : WF m) :
+    parseBody (printBody m.hello) = some m.hello := by
+  have hwf : WF m := hw
+  obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, _, _,
+    hflen⟩ := hw
+  rw [printBody_eq]
+  unfold parseBody
+  rw [withU8_cons, ite_eq_left (by decide : ((1 : UInt8).toNat = 1)),
+    withU24_be24 (by omega), withBytes_self, ite_eq_left rfl]
+  exact parseBodyFields_print m hwf
+
+/-- A parsed handshake message prints back to the input
+    bytes, and every field satisfies the bounds. -/
+theorem parseBody_inv {body : List UInt8} {h : Hello}
+    (hparse : parseBody body = some h) :
+    printBody h = body ∧
+    h.legacyVersion < 65536 ∧ h.random.length = 32 ∧
+    h.sessionId.length ≤ 32 ∧
+    h.cipherSuites ≠ [] ∧
+    (∀ v ∈ h.cipherSuites, v < 65536) ∧
+    h.cipherSuites.length ≤ 32767 ∧
+    h.compressionMethods ≠ [] ∧
+    (0 : UInt8) ∈ h.compressionMethods ∧
+    h.compressionMethods.length ≤ 255 ∧
+    (∀ e ∈ h.extensions, ExtWF e) ∧
+    List.Nodup (h.extensions.map extType) ∧
+    41 ∉ (h.extensions.dropLast).map extType ∧
+    (offersTls13 h.extensions = true →
+      h.compressionMethods = [0]) ∧
+    (printExts h.extensions).length ≤ 65535 := by
+  unfold parseBody at hparse
+  obtain ⟨htype, r1, hbody1, _, hp⟩ := withU8_inv hparse
+  by_cases ht : htype = 1
+  case neg => rw [ite_eq_right ht] at hp; cases hp
+  rw [ite_eq_left ht] at hp
+  obtain ⟨hlen, r2, hr1, _, hp⟩ := withU24_inv hp
+  obtain ⟨fbs, r3, hfbs, hr2, hp⟩ := withBytes_inv hp
+  by_cases hr : r3 = []
+  case neg => rw [ite_eq_right hr] at hp; cases hp
+  rw [ite_eq_left hr] at hp
+  have hfi := parseBodyFields_inv hp
+  have hbyte : htype.toUInt8 = (1 : UInt8) := by
+    rw [ht]
+    decide
+  have hprint : printBody h = body := by
+    rw [printBody_eq, hfi.1, hfbs, hbody1, hbyte, hr1, hr2, hr,
+      List.append_nil]
+  exact ⟨hprint, hfi.2⟩
+
+/-- The whole printed message, as its content type byte in
+    front of the rest. -/
+theorem print_eq (m : Message) :
+    print m = (22 : UInt8) :: (be16 m.recordVersion ++
+      (be16 (printBody m.hello).length ++ printBody m.hello)) :=
+  rfl
+
+/-- The whole printed message reads back as the message. -/
+theorem parse_print (m : Message) (hw : WF m) :
+    parse (print m) = some m := by
+  have hwf : WF m := hw
+  obtain ⟨hrv, _, _, _, _, _, _, _, _, _, _, _, _, _, _,
+    hflen⟩ := hw
+  have hblt : (printBody m.hello).length < 65536 := by
+    rw [printBody_length]
+    omega
+  have hble : (printBody m.hello).length ≤ 16384 := by
+    rw [printBody_length]
+    omega
+  rw [print_eq]
+  unfold parse
+  rw [withU8_cons, ite_eq_left (by decide : ((22 : UInt8).toNat = 22)),
+    withU16_be16 hrv, withU16_be16 hblt, ite_eq_left hble,
+    withBytes_self, ite_eq_left rfl, parseBody_print m hwf,
+    Option.map_some]
+
+/-- A parsed message prints back to the input bytes, and the
+    message is well formed. -/
+theorem print_parse {bs : List UInt8} {m : Message}
+    (hparse : parse bs = some m) :
+    print m = bs ∧ WF m := by
+  unfold parse at hparse
+  obtain ⟨ct, r1, hbs1, _, hp⟩ := withU8_inv hparse
+  by_cases hct : ct = 22
+  case neg => rw [ite_eq_right hct] at hp; cases hp
+  rw [ite_eq_left hct] at hp
+  obtain ⟨rv, r2, hr1, hrv, hp⟩ := withU16_inv hp
+  obtain ⟨rlen, r3, hr2, hrlen, hp⟩ := withU16_inv hp
+  by_cases hrl : rlen ≤ 16384
+  case neg => rw [ite_eq_right hrl] at hp; cases hp
+  rw [ite_eq_left hrl] at hp
+  obtain ⟨body, r4, hbodylen, hr3, hp⟩ := withBytes_inv hp
+  by_cases hr : r4 = []
+  case neg => rw [ite_eq_right hr] at hp; cases hp
+  rw [ite_eq_left hr] at hp
+  obtain ⟨hh, hpb, hp⟩ := Option.map_eq_some_iff.mp hp
+  subst hp
+  obtain ⟨hbody_eq, hver, hrand, hsess, hsne, hslt, hslen, hcne,
+    hc0, hclen, hewf, hnod, hpsk, h13, helen⟩ := parseBody_inv hpb
+  have hctb : ct.toUInt8 = (22 : UInt8) := by
+    rw [hct]
+    decide
+  have hflen : (printBodyFields hh).length ≤ 16380 := by
+    have h1 := printBody_length hh
+    rw [hbody_eq] at h1
+    omega
+  have hprint : print ⟨rv, hh⟩ = bs := by
+    rw [print_eq]
+    show (22 : UInt8) :: (be16 rv ++
+      (be16 (printBody hh).length ++ printBody hh)) = bs
+    rw [hbody_eq, hbodylen, hbs1, hctb, hr1, hr2, hr3, hr,
+      List.append_nil]
+  exact ⟨hprint, hrv, hver, hrand, hsess, hsne, hslt, hslen,
+    hcne, hc0, hclen, hewf, hnod, hpsk,
+    fun vs hm h7 => h13 (offersTls13_of_mem hm h7), helen, hflen⟩
diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean
new file mode 100644
index 0000000..6fafd6d
--- /dev/null
+++ b/Proofs/SpecProofs.lean
@@ -0,0 +1,247 @@
+/-
+  Proofs of the statements in `Spec.lean`, under the same names.
+
+  The two round trips are the theorems proved in
+  `Proofs/RoundTrip.lean`. The examples are single inputs, checked
+  in the kernel with `decide +kernel`: no native evaluation, which
+  the bar forbids.
+-/
+
+import ClientHello
+import Spec.Defs
+import Proofs.RoundTrip
+
+open ClientHello
+
+theorem Spec.parse_print (m : Message) (hw : Spec.WF m) :
+    parse (print m) = some m :=
+  ClientHello.Proofs.parse_print m hw
+
+theorem Spec.print_parse {bs : List UInt8} {m : Message}
+    (hparse : parse bs = some m) :
+    print m = bs ∧ Spec.WF m :=
+  ClientHello.Proofs.print_parse hparse
+
+
+theorem Spec.tls13_compression_null {bs : List UInt8} {m : Message}
+    {vs : List Nat}
+    (hparse : parse bs = some m)
+    (hsv : Extension.supportedVersions vs ∈ m.hello.extensions)
+    (h13 : 772 ∈ vs) :
+    m.hello.compressionMethods = [0] := by
+  obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, hc13, _, _⟩ :=
+    (ClientHello.Proofs.print_parse hparse).2
+  exact hc13 vs hsv h13
+
+theorem Spec.psk_last {bs : List UInt8} {m : Message}
+    (hparse : parse bs = some m) :
+    41 ∉ (m.hello.extensions.dropLast).map extType := by
+  obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, hpsk, _, _, _⟩ :=
+    (ClientHello.Proofs.print_parse hparse).2
+  exact hpsk
+
+theorem Spec.accepts_empty_extensions :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8) := by
+  decide +kernel
+
+
+theorem Spec.accepts_supported_versions :
+    (parse ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8) := by
+  decide +kernel
+
+
+theorem Spec.accepts_key_share_empty_list :
+    (parse ([22, 3, 1, 0, 78, 1, 0, 0, 74, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 31, 0, 10, 0, 6, 0, 4, 0, 29, 0, 23, 0, 43, 0, 3, 2, 3, 4, 0, 51, 0, 2, 0, 0, 0, 13, 0, 4, 0, 2, 4, 3] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 78, 1, 0, 0, 74, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 31, 0, 10, 0, 6, 0, 4, 0, 29, 0, 23, 0, 43, 0, 3, 2, 3, 4, 0, 51, 0, 2, 0, 0, 0, 13, 0, 4, 0, 2, 4, 3] : List UInt8) := by
+  decide +kernel
+
+
+theorem Spec.accepts_tls12_compression :
+    (parse ([22, 3, 1, 0, 48, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 0] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 48, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 0] : List UInt8) := by
+  decide +kernel
+
+
+theorem Spec.accepts_psk_last :
+    (parse ([22, 3, 1, 0, 62, 1, 0, 0, 58, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 15, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 41, 0, 2, 0, 0] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 62, 1, 0, 0, 58, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 15, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 41, 0, 2, 0, 0] : List UInt8) := by
+  decide +kernel
+
+
+theorem Spec.accepts_record_at_limit (v : List UInt8)
+    (hv : v.length = 16324) :
+    (parse (([22, 3, 1, 64, 0, 1, 0, 63, 252, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 63, 209, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 21, 63, 196] : List UInt8) ++ v)).map print =
+      some (([22, 3, 1, 64, 0, 1, 0, 63, 252, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 63, 209, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 21, 63, 196] : List UInt8) ++ v) := by
+  let h : Hello := ⟨771, [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
+    15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31], [],
+    [4865], [0], [.supportedVersions [772, 771], .opaque 21 v]⟩
+  let m : Message := ⟨769, h⟩
+  have hfields : (printBodyFields h).length = 16380 := by
+    simp [h, printBodyFields, printExts, printExt, printExtValue,
+      printPairs, be16, hv]
+  have hp : print m = ([22, 3, 1, 64, 0, 1, 0, 63, 252, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 63, 209, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 21, 63, 196] : List UInt8) ++ v := by
+    simp [m, h, print, printBody, printBodyFields, printExts, printExt,
+      printExtValue, printPairs, extType, be16, be24, hv]
+  have hw : Spec.WF m := by
+    refine ⟨?_, ?_, rfl, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_,
+      fun _ _ _ => rfl, ?_, Nat.le_of_eq hfields⟩
+    all_goals first
+      | (dsimp only [m, h]; decide)
+      | skip
+    · intro e he
+      simp only [m, h, List.mem_cons, List.not_mem_nil, or_false] at he
+      rcases he with rfl | rfl
+      · simp [Spec.ExtWF]
+      · simp [Spec.ExtWF, hv]
+    · simp [m, h, extType]
+    · simp [m, h, extType]
+    · simp [m, h, printExts, printExt, printExtValue, printPairs, be16, hv]
+  rw [← hp, ClientHello.Proofs.parse_print m hw]
+  rfl
+
+
+theorem Spec.rejects_empty :
+    (parse ([] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_short_header :
+    (parse ([22, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_record_length_zero :
+    (parse ([22, 3, 1, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_content_type :
+    (parse ([23, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_record_length_longer :
+    (parse ([22, 3, 1, 0, 10, 1, 0, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_record_overflow (ct v1 v2 a b : UInt8)
+    (rest : List UInt8) (h : 16384 < a.toNat * 256 + b.toNat) :
+    parse (ct :: v1 :: v2 :: a :: b :: rest) = none := by
+  have hover : ¬ (u16 a b ≤ 16384) := by
+    simp only [u16]
+    omega
+  unfold parse
+  rw [ClientHello.Proofs.withU8_cons]
+  by_cases hct : ct.toNat = 22
+  · rw [ite_eq_left hct, ClientHello.Proofs.withU16_cons,
+      ClientHello.Proofs.withU16_cons, ite_eq_right hover]
+  · rw [ite_eq_right hct]
+
+
+theorem Spec.rejects_trailing_bytes :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_handshake_type :
+    (parse ([22, 3, 1, 0, 56, 2, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_handshake_length :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_missing_extensions :
+    (parse ([22, 3, 1, 0, 45, 1, 0, 0, 41, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_session_id_33 :
+    (parse ([22, 3, 1, 0, 89, 1, 0, 0, 85, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 33, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_odd_cipher_suites :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 3, 19, 1, 19, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_empty_cipher_suites :
+    (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 0, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_compression_without_null :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 1, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_empty_compression :
+    (parse ([22, 3, 1, 0, 46, 1, 0, 0, 42, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 0, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_tls13_compression :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_tls13_compression_second :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 3, 3, 4] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_duplicate_extension :
+    (parse ([22, 3, 1, 0, 61, 1, 0, 0, 57, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 14, 0, 43, 0, 3, 2, 3, 4, 0, 43, 0, 3, 2, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_psk_not_last :
+    (parse ([22, 3, 1, 0, 62, 1, 0, 0, 58, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 15, 0, 41, 0, 2, 0, 0, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_extension_overrun :
+    (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 0, 0, 10, 2, 3, 4] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_duplicate_key_share_group :
+    (parse ([22, 3, 1, 0, 63, 1, 0, 0, 59, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 16, 0, 51, 0, 12, 0, 10, 0, 29, 0, 1, 1, 0, 29, 0, 1, 2] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_key_share_empty_key :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 10, 0, 51, 0, 6, 0, 4, 0, 29, 0, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+
+theorem Spec.rejects_supported_versions_odd :
+    (parse ([22, 3, 1, 0, 55, 1, 0, 0, 51, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 8, 0, 43, 0, 4, 3, 3, 4, 3] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_supported_versions_zero :
+    (parse ([22, 3, 1, 0, 52, 1, 0, 0, 48, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 5, 0, 43, 0, 1, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_alpn_empty_name :
+    (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 16, 0, 3, 0, 1, 0] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_sni_second_host_name :
+    (parse ([22, 3, 1, 0, 77, 1, 0, 0, 73, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 30, 0, 0, 0, 26, 0, 24, 0, 0, 9, 97, 46, 101, 120, 97, 109, 112, 108, 101, 0, 0, 9, 98, 46, 101, 120, 97, 109, 112, 108, 101] : List UInt8)).isSome = false := by
+  decide +kernel
+
+
+theorem Spec.rejects_sni_list_length :
+    (parse ([22, 3, 1, 0, 67, 1, 0, 0, 63, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 20, 0, 0, 0, 16, 0, 99, 0, 0, 11, 101, 120, 97, 109, 112, 108, 101, 46, 99, 111, 109] : List UInt8)).isSome = false := by
+  decide +kernel
diff --git a/Proofs/Verify.lean b/Proofs/Verify.lean
new file mode 100644
index 0000000..ab094b5
--- /dev/null
+++ b/Proofs/Verify.lean
@@ -0,0 +1,4 @@
+import Proofs.RoundTrip
+
+#print axioms ClientHello.Proofs.parse_print
+#print axioms ClientHello.Proofs.print_parse
diff --git a/README.md b/README.md
index 5d9891b..7f21c61 100644
--- a/README.md
+++ b/README.md
@@ -1,38 +1,218 @@
-# clienthello
+# clienthello: a TLS ClientHello parser and printer, with proved round trips
 
-A Lean parser for the TLS ClientHello message. This is a Proven Commons project: it rebuilds a widely used format in Lean and proves the new code follows its written specification.
+Status: in progress
 
-Status: not verified. No code has landed yet. Plan issue 1 holds the first slice, and it is unclaimed. The specification has not been approved by a reviewer, so do not call this verified.
+A parser and printer for the TLS ClientHello message, in
+Lean, following RFC 8446 section 4.1.2, with the legacy
+fields carried from RFC 5246, the server name indication
+from RFC 6066, and ALPN from RFC 7301. The definitions are
+in `ClientHello/Value.lean` (the data model and the
+printer) and `ClientHello/Parse.lean` (the parser). The
+proofs are in `Proofs/RoundTrip.lean`. The rules are
+written out in `SPEC.md`, and as one Lean predicate,
+`Spec.WF`, in `Spec/Defs.lean`. This slice reads one TLS
+record holding one ClientHello; it does no handshake
+crypto and parses no certificates.
 
-## First slice
+The statements a reviewer approves are in `Spec.lean`,
+with the definition of a well formed message they use in
+`Spec/Defs.lean`, and their proofs in
+`Proofs/SpecProofs.lean`. No reviewer has approved them
+yet, so this project is not called verified.
 
-- 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.
+## How to run it
 
-This is distinct from the hostname repo. ClientHello extracts the server name string. Matching that name against a certificate stays in the hostname repo.
+`lake build` builds the library, the proofs, and the
+command line tool. The tool reads one request per line:
+the word `parse`, a space, and the message as
+comma-separated decimal byte codes. It answers `ok:` and
+the byte codes of the canonical reprint when the message
+parses, `none` when it is rejected, and `error` when the
+request itself is malformed.
 
-## Main claim
+`python3 tests/run_tests.py` rebuilds, runs the fixed
+cases, the named rejections, the differential run against
+the harness oracle, and real ClientHellos built by OpenSSL
+through Python's ssl module, and writes the outcome to
+`tests/TEST-RESULTS.md`.
 
-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.
+## What is proved
 
-## Test oracles
+Each claim below names the theorem behind it. The
+theorems are stated in `Spec.lean` (the challenge file,
+where they end in `sorry`) and proved in
+`Proofs/SpecProofs.lean`, under the same names.
+`comparator.json` lists all of them.
 
-- Go crypto/tls.
-- OpenSSL captures.
-- Wireshark TLS dissectors.
+Statements about every input, or every input of one form:
 
-## Score
+| Claim | Theorem |
+|-------|---------|
+| Parsing the printed form of a well formed message gives the message back. | `Spec.parse_print` |
+| Printing a message the parser took gives the same bytes it was read from, and the message is well formed. | `Spec.print_parse` |
+| A record whose length field is above 2^14 = 16384 is refused, whatever else the input holds. | `Spec.rejects_record_overflow` |
+| A record of exactly 2^14 = 16384 bytes is accepted and writes back as the same bytes. The input is the hello of `Spec.accepts_supported_versions` with a padding extension (type 21) after its supported_versions, whose value is any 16324 bytes, and the lengths that cover it, 16389 bytes in all. | `Spec.accepts_record_at_limit` |
+| Every accepted hello with a supported_versions extension that lists 0x0304, in any position (a hello that offers TLS 1.3), has exactly the compression methods [0]. | `Spec.tls13_compression_null` |
+| In every accepted hello, no extension but the last has type 41: pre_shared_key, when present, is the last extension. | `Spec.psk_last` |
 
-15 out of 18, first pass score in mission issue 19, the round 4 sheet. Created at the org owner's direction on that sheet, on the judgement that the slice, claim, and oracles are sound and that it duplicates no existing repo.
+Together, the two round trips say that the parser accepts
+exactly the printed forms of well formed messages, so
+every rule that is part of well formedness (below) holds
+for every accepted input. The statements after them state
+the record limit from both sides and two more of those
+rules on their own, so that each has a theorem of its own.
 
-## What is not in this slice
+Single inputs. Each theorem below is about the one input
+written out in `Spec.lean`, and each claim says what that
+input is. Most refused inputs are an accepted input with
+one field changed, so that the field's rule is what refuses
+it. These theorems pin each rule to a concrete case; they
+do not state the rule for every input.
 
-- The rest of the TLS handshake.
-- Certificate parsing. That follows from the der repo.
-- Any claim about a full TLS implementation.
+| Claim | Theorem |
+|-------|---------|
+| A 52-byte hello with a present, empty extensions block is accepted and writes back as the same bytes. | `Spec.accepts_empty_extensions` |
+| A 61-byte hello whose one extension is supported_versions [0x0304, 0x0303] is accepted and writes back as the same bytes. | `Spec.accepts_supported_versions` |
+| An 83-byte TLS 1.3 hello whose key_share carries no entries, the form a client uses to ask for a HelloRetryRequest, is accepted and writes back as the same bytes. | `Spec.accepts_key_share_empty_list` |
+| The hello of `Spec.accepts_empty_extensions` with compression methods [1, 0] is accepted and writes back as the same bytes: it does not offer TLS 1.3, so methods besides null may be listed. | `Spec.accepts_tls12_compression` |
+| A hello whose extensions are supported_versions and then pre_shared_key is accepted and writes back as the same bytes. | `Spec.accepts_psk_last` |
+| Empty input is refused. | `Spec.rejects_empty` |
+| A 2-byte input, shorter than the record header, is refused. | `Spec.rejects_short_header` |
+| A record header with length 0 and nothing after it is refused. | `Spec.rejects_record_length_zero` |
+| The hello of `Spec.accepts_supported_versions` with content type 23 in place of 22 is refused. | `Spec.rejects_content_type` |
+| A record whose length field (10) is longer than the 4 bytes that follow is refused. | `Spec.rejects_record_length_longer` |
+| The hello of `Spec.accepts_empty_extensions` with one byte after the record is refused. | `Spec.rejects_trailing_bytes` |
+| The hello of `Spec.accepts_supported_versions` with handshake type 2 in place of 1 is refused. | `Spec.rejects_handshake_type` |
+| The hello of `Spec.accepts_empty_extensions` with a handshake length one more than the body holds is refused. | `Spec.rejects_handshake_length` |
+| The hello of `Spec.accepts_empty_extensions` without its extensions block, ending after the compression methods, is refused. | `Spec.rejects_missing_extensions` |
+| The hello of `Spec.accepts_supported_versions` with a 33-byte session id is refused. | `Spec.rejects_session_id_33` |
+| The hello of `Spec.accepts_supported_versions` with a 3-byte cipher suite list is refused. | `Spec.rejects_odd_cipher_suites` |
+| The hello of `Spec.accepts_supported_versions` with an empty cipher suite list is refused. | `Spec.rejects_empty_cipher_suites` |
+| The hello of `Spec.accepts_empty_extensions` with compression methods [1], without the null method, is refused. | `Spec.rejects_compression_without_null` |
+| The hello of `Spec.accepts_empty_extensions` with an empty compression method list is refused. (An empty list holds no null method, so the rule above refuses it too.) | `Spec.rejects_empty_compression` |
+| The hello of `Spec.accepts_supported_versions`, which offers TLS 1.3, with compression methods [1, 0] is refused. | `Spec.rejects_tls13_compression` |
+| The input of `Spec.rejects_tls13_compression` with its supported_versions list in the other order, [0x0303, 0x0304], is refused. | `Spec.rejects_tls13_compression_second` |
+| A hello with two supported_versions extensions is refused. | `Spec.rejects_duplicate_extension` |
+| The hello of `Spec.accepts_psk_last` with its two extensions in the other order, pre_shared_key first, is refused. | `Spec.rejects_psk_not_last` |
+| A hello whose one extension declares 10 value bytes where its block holds 3 is refused. | `Spec.rejects_extension_overrun` |
+| A hello whose key_share carries two entries for group 29 is refused. | `Spec.rejects_duplicate_key_share_group` |
+| A hello whose key_share entry has empty key exchange bytes is refused. | `Spec.rejects_key_share_empty_key` |
+| A hello whose one extension is supported_versions with the 4-byte value 3, 3, 4, 3 is refused: its list length byte is 3, which is odd, and 3 bytes follow it. | `Spec.rejects_supported_versions_odd` |
+| A hello whose one extension is supported_versions with the 1-byte value 0 is refused: its list length byte is 0, so it lists no version. | `Spec.rejects_supported_versions_zero` |
+| A hello whose ALPN value holds one protocol name of length 0 is refused. | `Spec.rejects_alpn_empty_name` |
+| A hello whose server_name value holds two host_name entries is refused. | `Spec.rejects_sni_second_host_name` |
+| A hello whose server_name list length (99) does not cover the rest of the value is refused. | `Spec.rejects_sni_list_length` |
 
-## Layout, when the first slice lands
+A message is well formed (`Spec.WF`) when the record
+version and the legacy version each fit two bytes; the
+random holds exactly 32 bytes; the session id holds at
+most 32 bytes; the cipher suites are nonempty, each fits
+two bytes, and there are at most 32767 of them; the
+compression methods are nonempty, contain the null method
+0, number at most 255, and are exactly [0] when the hello
+offers TLS 1.3 (its supported_versions lists 0x0304);
+every extension is well formed (its lengths fit their
+fields, an SNI entry list is nonempty with distinct entry
+types and a nonempty host name when present, an ALPN name
+list is nonempty and its names are nonempty, a
+supported_versions list is nonempty, key share groups are
+distinct with nonempty keys, and an opaque
+extension's type is none of the four decoded types); no
+extension type stands twice; no extension but the last has
+type 41 (pre_shared_key); the printed extensions block
+fits two bytes of length; and the printed handshake
+message, its four header bytes and the body fields, is at
+most 2^14 = 16384 bytes, the record limit of RFC 8446
+section 5.1.
 
-The layout follows the Proven Commons template in the mission repo, under bar/template. Spec.lean holds the statements a reviewer approves. Proofs.lean holds the proofs under the same names. Main.lean holds the command line tool used by the tests. The bar check runs in CI on every change.
+`Spec.WF` is in `Spec/Defs.lean`, which `bar.toml` lists
+among the spec files. The approval covers it with
+`Spec.lean`, so what the two round trips mean cannot
+change without changing the approved text.
+
+The two round trip theorems rest on the proofs in
+`Proofs/RoundTrip.lean`, where they are
+`ClientHello.Proofs.parse_print` and
+`ClientHello.Proofs.print_parse`. Both check against the
+standard axioms only (`propext`, `Classical.choice`,
+`Quot.sound`), which a reader can confirm with
+`#print axioms`; `Proofs/Verify.lean` prints them at
+build time. The single-input theorems are checked in the
+kernel with `decide +kernel`.
+
+The command line tool in `Main.lean` calls
+`ClientHello.parse` and `ClientHello.print` directly,
+the same functions the theorems are about.
+
+## What is not proved
+
+- That the well formedness predicate, `Spec.WF`, is the
+  same as the rules in `SPEC.md`. Relative to the
+  predicate, the accepted inputs are fixed exactly: the
+  parser accepts the printed forms of well formed messages
+  and nothing else. That the predicate holds every rule of
+  `SPEC.md`, and no other, is read by the reviewer and
+  checked by the differential tests in `tests/`, not
+  proved. The single-input theorems pin one input each.
+- That the printer writes the byte layout the RFCs give.
+  The round trips relate the parser and the printer to
+  each other; the accepted examples pin some whole inputs,
+  but no theorem names the bytes of each field.
+- The meaning of any extension other than the four
+  decoded ones. Every other extension is carried as its
+  type and value bytes, and no per extension content rule
+  is checked.
+- Anything about the host name bytes beyond their being
+  nonempty when present: no label rules, no case rules, no
+  matching against a certificate. Name matching belongs
+  to the hostname work.
+- Anything about the rest of the handshake, the key
+  schedule, or any other record or message type.
+
+## What you must trust
+
+- The Lean kernel (Lean 4.35.0, pinned in
+  `lean-toolchain`), which checks every proof.
+- The Lean compiler, which turns the proved definitions
+  into the program that runs.
+- The Lean runtime, which runs that program.
+- The hardware the program runs on.
+- Every dependency in `lake-manifest.json`: the manifest
+  lists no packages, so there are no library dependencies
+  to trust beyond the Lean toolchain itself.
+- That `SPEC.md` states the reading of the RFCs you
+  intend. The proofs are about the parser and printer in
+  this repo following each other exactly; the fidelity of
+  the spec to the RFCs is a reading, pinned in SPEC.md
+  where the RFCs leave a choice open.
+- The test oracle in `tests/run_tests.py` is a second
+  reading of the same rules, in Python, by the same
+  authors. It is evidence, not proof. OpenSSL, through
+  Python's ssl module, supplies real ClientHellos that must
+  be accepted, but no outside TLS stack judges the
+  malformed inputs.
+- The line handling in `Main.lean` (splitting a request
+  line, reading decimal codes). The tests drive it, and
+  no proof covers it.
+- There are no exceptions to item 4 of the bar: the
+  project uses none of the features it forbids.
+
+## Re-check it
+
+1. `lake comparator --paranoid`: builds the challenge
+   file `Spec.lean` and the proofs in a sandbox and
+   checks that each theorem named in `comparator.json`
+   proves exactly the statement in the challenge file,
+   uses no axiom but the three standard ones, and is
+   accepted by Lean's kernel and every other kernel
+   shipped with Lean.
+2. `python3 tests/run_tests.py`: the fixed cases, the
+   named rejections, the differential run against the
+   oracle, and the OpenSSL-built hellos, with the oracle,
+   seed, input count and failures written to
+   `tests/TEST-RESULTS.md`.
+3. `lake build`: the library, the proofs, and the tool
+   build clean, and the build prints the axiom list for
+   both round trip theorems.
+4. Read `SPEC.md` against RFC 8446 section 4.1.2 and
+   check the pinned readings are the ones you want.
diff --git a/SPEC.md b/SPEC.md
new file mode 100644
index 0000000..10a171a
--- /dev/null
+++ b/SPEC.md
@@ -0,0 +1,276 @@
+# Specification: clienthello
+
+A TLS ClientHello parser and printer in Lean, following
+RFC 8446 section 4.1.2 (the ClientHello message), the
+legacy fields as carried from RFC 5246, RFC 6066 section 3
+(the server name indication), and RFC 7301 (ALPN). This
+slice reads exactly one TLS record holding exactly one
+ClientHello, and prints that message back in canonical
+form: every length is recomputed from the values.
+
+## The record layer
+
+A message is one TLS record:
+
+| Bytes | Field |
+|-------|-------|
+| 0 | content type: must be 22 (handshake) |
+| 1, 2 | legacy record version: carried, value unchecked |
+| 3, 4 | length: two bytes, big endian, at most 2^14 = 16384 |
+| 5 ... | the record body, exactly that many bytes |
+
+- Input shorter than the five byte header rejects.
+- A length above 2^14 = 16384 rejects, whatever follows.
+  RFC 8446 section 5.1 says the length "MUST NOT exceed
+  2^14 bytes" and that a receiver answers a longer record
+  with a record_overflow alert. A length of exactly 16384
+  is allowed.
+- A body shorter than the declared length rejects.
+- Bytes after the record reject. The decoder takes exactly
+  one record; a stream reader is later work.
+- A record length of 0 rejects: an empty body cannot hold
+  a ClientHello. (In the code this falls out of the body
+  read failing; it is stated here because it is a rule a
+  reader of the bytes should expect.)
+
+## The handshake header
+
+Inside the record body:
+
+| Bytes | Field |
+|-------|-------|
+| 0 | message type: must be 1 (client_hello) |
+| 1, 2, 3 | length: three bytes, big endian |
+| 4 ... | the ClientHello body |
+
+The three byte length must equal the remaining body length
+exactly. A mismatch rejects.
+
+## The ClientHello body
+
+In order:
+
+| Field | Size | Rule |
+|-------|------|------|
+| legacy version | 2 bytes | carried, value unchecked |
+| random | 32 bytes | exactly 32 |
+| legacy session id | 1 byte length, then that many bytes | length at most 32; a longer length rejects |
+| cipher suites | 2 byte length, then that many bytes | length even and at least 2; the bytes read as two byte suite codes; an empty list or an odd length rejects |
+| legacy compression methods | 1 byte length, then that many bytes | length at least 1; the list must contain the byte 0 (the null method); in a hello that offers TLS 1.3 it must be exactly the one byte 0 |
+| extensions | 2 byte length, then that many bytes | the block must consume the rest of the body exactly |
+
+Compression methods. RFC 5246 section 7.4.1.2 says the
+list "MUST contain" the null method, so a list without the
+byte 0 rejects. A hello offers TLS 1.3 when it has a
+supported_versions extension that lists 0x0304. RFC 8446
+section 4.1.2 says that for every TLS 1.3 ClientHello the
+list "MUST contain exactly one byte, set to zero", and that
+a server must abort otherwise, so a hello that offers TLS
+1.3 with any other list rejects: [1, 0] and [0, 0] both
+reject. A hello that does not offer TLS 1.3 may list other
+methods besides 0.
+
+The extensions block must be present. A body that ends
+after the compression methods is the pre-TLS-1.3 shape;
+this slice rejects it, because the slice frames the
+message by its extensions and supported_versions is how a
+TLS 1.3 hello speaks. The block may be empty: a present
+block of length 0 consumes the body and carries no
+extensions, and is accepted.
+
+## Extensions
+
+Each extension is a two byte type, a two byte length, and
+that many value bytes. An extension length running past
+the end of the block rejects, and the block must be
+consumed exactly. A duplicate extension type rejects.
+
+pre_shared_key (type 41), when present, must be the last
+extension. RFC 8446 section 4.2 says it "MUST be the last
+extension in the ClientHello", and section 4.2.11 says
+servers "MUST check that it is the last extension", so a
+block in which type 41 stands anywhere but last rejects.
+Its value is carried opaque, like every type not decoded
+below.
+
+Four types are decoded. Every other type is carried as
+the pair of its type and its raw value bytes, length
+checked, not interpreted.
+
+### server_name (type 0), RFC 6066 section 3
+
+The value is a two byte list length covering the rest of
+the value, then entries. Each entry is a one byte name
+type, a two byte length, and that many bytes. Type 0 is
+host_name.
+
+- The list length must equal the value length minus two.
+- The list must be nonempty and consume the value exactly.
+- Two entries of the same type reject, so there is at
+  most one host_name entry.
+- The host_name bytes must be nonempty.
+- Host name bytes are carried as bytes. No case folding,
+  label, or character validation happens in this slice.
+  Entries of other types are carried as (type, bytes).
+
+### ALPN (type 16), RFC 7301
+
+The value is a two byte list length covering the rest of
+the value, then protocol names. Each name is a one byte
+length and that many bytes.
+
+- The list length must equal the value length minus two.
+- The list must be nonempty and consume the value exactly.
+- A name length of 0 rejects.
+
+### supported_versions (type 43), RFC 8446 section 4.2.1
+
+The client form: a one byte length, then that many bytes
+read as two byte versions.
+
+- The length must equal the value length minus one.
+- The length must be even and at least 2. An odd or zero
+  length rejects.
+
+The server form (a single version) is not this message and
+is not read here.
+
+### key_share (type 51), RFC 8446 section 4.2.8
+
+The client form: a two byte list length covering the rest
+of the value, then entries. Each entry is a two byte
+group, a two byte key exchange length, and that many
+bytes.
+
+- The list length must equal the value length minus two.
+- The entries must consume the value exactly.
+- The list may be empty. RFC 8446 section 4.2.8 says the
+  client_shares vector "MAY be empty", which a client does
+  to ask for a HelloRetryRequest, so an empty list is
+  accepted.
+- A key exchange length of 0 rejects.
+- A duplicate group rejects.
+
+## Pinned readings
+
+Where the RFCs or the plan leave a reading open, this
+slice pins it:
+
+- Trailing bytes after the record reject.
+- A missing extensions block rejects; a present block of
+  length 0 is accepted.
+- A hello offers TLS 1.3 exactly when its
+  supported_versions lists 0x0304; draft version numbers
+  such as 0x7F1C do not count. Only such a hello must have
+  the compression methods [0].
+- The session id length is at most 32.
+- The cipher suite list is nonempty, with an even byte
+  length.
+- A duplicate extension type rejects.
+- SNI carries at most one host_name entry, and duplicate
+  SNI entry types reject in general.
+- Host name bytes are unvalidated beyond being nonempty.
+- Unknown extension types are carried opaque.
+- A duplicate key share group rejects.
+
+## Properties and their theorems
+
+Each property a reader can check in the page (`README.md`)
+names its theorem. The theorems are stated in `Spec.lean`
+and proved in `Proofs/SpecProofs.lean`. The two round
+trips are stated over `Spec.WF` in `Spec/Defs.lean`, which
+writes the rules of this page as one predicate on the
+message. That file is part of this specification, and the
+approval covers it. The example theorems are single
+inputs; the tests in `tests/` cover each rule on many more
+inputs.
+
+Statements about every input, or every input of one form:
+
+| Property | Theorem |
+|-------|---------|
+| Parsing the printed form of a well formed message gives the message back. | `Spec.parse_print` |
+| Printing a message the parser took gives the same bytes it was read from, and the message is well formed. | `Spec.print_parse` |
+| A record whose length field is above 2^14 = 16384 is refused, whatever else the input holds. | `Spec.rejects_record_overflow` |
+| A record of exactly 2^14 = 16384 bytes is accepted and writes back as the same bytes. The input is the hello of `Spec.accepts_supported_versions` with a padding extension (type 21) after its supported_versions, whose value is any 16324 bytes, and the lengths that cover it, 16389 bytes in all. | `Spec.accepts_record_at_limit` |
+| Every accepted hello with a supported_versions extension that lists 0x0304, in any position (a hello that offers TLS 1.3), has exactly the compression methods [0]. | `Spec.tls13_compression_null` |
+| In every accepted hello, no extension but the last has type 41: pre_shared_key, when present, is the last extension. | `Spec.psk_last` |
+
+Single inputs, each about the one input written out in
+`Spec.lean`. Most refused inputs are an accepted input with
+one field changed, so that the field's rule is what refuses
+it:
+
+| Property | Theorem |
+|-------|---------|
+| A 52-byte hello with a present, empty extensions block is accepted and writes back as the same bytes. | `Spec.accepts_empty_extensions` |
+| A 61-byte hello whose one extension is supported_versions [0x0304, 0x0303] is accepted and writes back as the same bytes. | `Spec.accepts_supported_versions` |
+| An 83-byte TLS 1.3 hello whose key_share carries no entries, the form a client uses to ask for a HelloRetryRequest, is accepted and writes back as the same bytes. | `Spec.accepts_key_share_empty_list` |
+| The hello of `Spec.accepts_empty_extensions` with compression methods [1, 0] is accepted and writes back as the same bytes: it does not offer TLS 1.3, so methods besides null may be listed. | `Spec.accepts_tls12_compression` |
+| A hello whose extensions are supported_versions and then pre_shared_key is accepted and writes back as the same bytes. | `Spec.accepts_psk_last` |
+| Empty input is refused. | `Spec.rejects_empty` |
+| A 2-byte input, shorter than the record header, is refused. | `Spec.rejects_short_header` |
+| A record header with length 0 and nothing after it is refused. | `Spec.rejects_record_length_zero` |
+| The hello of `Spec.accepts_supported_versions` with content type 23 in place of 22 is refused. | `Spec.rejects_content_type` |
+| A record whose length field (10) is longer than the 4 bytes that follow is refused. | `Spec.rejects_record_length_longer` |
+| The hello of `Spec.accepts_empty_extensions` with one byte after the record is refused. | `Spec.rejects_trailing_bytes` |
+| The hello of `Spec.accepts_supported_versions` with handshake type 2 in place of 1 is refused. | `Spec.rejects_handshake_type` |
+| The hello of `Spec.accepts_empty_extensions` with a handshake length one more than the body holds is refused. | `Spec.rejects_handshake_length` |
+| The hello of `Spec.accepts_empty_extensions` without its extensions block, ending after the compression methods, is refused. | `Spec.rejects_missing_extensions` |
+| The hello of `Spec.accepts_supported_versions` with a 33-byte session id is refused. | `Spec.rejects_session_id_33` |
+| The hello of `Spec.accepts_supported_versions` with a 3-byte cipher suite list is refused. | `Spec.rejects_odd_cipher_suites` |
+| The hello of `Spec.accepts_supported_versions` with an empty cipher suite list is refused. | `Spec.rejects_empty_cipher_suites` |
+| The hello of `Spec.accepts_empty_extensions` with compression methods [1], without the null method, is refused. | `Spec.rejects_compression_without_null` |
+| The hello of `Spec.accepts_empty_extensions` with an empty compression method list is refused. (An empty list holds no null method, so the rule above refuses it too.) | `Spec.rejects_empty_compression` |
+| The hello of `Spec.accepts_supported_versions`, which offers TLS 1.3, with compression methods [1, 0] is refused. | `Spec.rejects_tls13_compression` |
+| The input of `Spec.rejects_tls13_compression` with its supported_versions list in the other order, [0x0303, 0x0304], is refused. | `Spec.rejects_tls13_compression_second` |
+| A hello with two supported_versions extensions is refused. | `Spec.rejects_duplicate_extension` |
+| The hello of `Spec.accepts_psk_last` with its two extensions in the other order, pre_shared_key first, is refused. | `Spec.rejects_psk_not_last` |
+| A hello whose one extension declares 10 value bytes where its block holds 3 is refused. | `Spec.rejects_extension_overrun` |
+| A hello whose key_share carries two entries for group 29 is refused. | `Spec.rejects_duplicate_key_share_group` |
+| A hello whose key_share entry has empty key exchange bytes is refused. | `Spec.rejects_key_share_empty_key` |
+| A hello whose one extension is supported_versions with the 4-byte value 3, 3, 4, 3 is refused: its list length byte is 3, which is odd, and 3 bytes follow it. | `Spec.rejects_supported_versions_odd` |
+| A hello whose one extension is supported_versions with the 1-byte value 0 is refused: its list length byte is 0, so it lists no version. | `Spec.rejects_supported_versions_zero` |
+| A hello whose ALPN value holds one protocol name of length 0 is refused. | `Spec.rejects_alpn_empty_name` |
+| A hello whose server_name value holds two host_name entries is refused. | `Spec.rejects_sni_second_host_name` |
+| A hello whose server_name list length (99) does not cover the rest of the value is refused. | `Spec.rejects_sni_list_length` |
+
+## Reading past the end
+
+No theorem says the parser never reads past the end of its
+input, and this page does not claim it as proved. In the
+Lean model the input is a list and every reader is a total
+function on lists, so there is no out of bounds read to
+rule out: a field read from input too short for it gives
+`none`, and the parser refuses. The extension parsers run
+over a value already cut to its declared length. What the
+theorems do say about the bytes is `Spec.print_parse`:
+every byte of an accepted input is accounted for, since
+the parsed message prints back to exactly that input.
+Lengths that run past the input are refused in the cases
+of `Spec.rejects_record_length_longer` and
+`Spec.rejects_extension_overrun`, and the tests cover
+more.
+
+## Slice boundaries
+
+- No server messages: no ServerHello, no EncryptedExtensions,
+  no Certificate, no Finished.
+- No handshake crypto: no key schedule, no transcript hash,
+  no signature checking.
+- No rules that tie one extension to another beyond those
+  above. For example, the slice does not check that a
+  pre_shared_key comes with psk_key_exchange_modes (RFC
+  8446 section 4.2.9), or that each key share's group is
+  offered in supported_groups (section 4.2.8).
+- No certificate work of any kind, and no matching of the
+  server name against a certificate. That matching belongs
+  to the hostname work; this slice only carries the name
+  bytes out of the message.
+- One record only: no stream reading, no record splitting
+  or joining, no alerts, no renegotiation. RFC 8446 section
+  5.1 lets a sender split a handshake message across
+  records; such a hello is refused here, since its first
+  record does not hold the whole message. A hello whose
+  handshake message is longer than 16384 bytes cannot fit
+  one record, so this slice refuses it.
diff --git a/Spec.lean b/Spec.lean
new file mode 100644
index 0000000..5953818
--- /dev/null
+++ b/Spec.lean
@@ -0,0 +1,265 @@
+/-
+  The specification as Lean statements: the challenge file.
+
+  A reviewer who did not write this file approves it, and `bar.toml`
+  records the SHA-256 it had then. The proofs live in `Proofs`
+  (`Proofs/SpecProofs.lean`); `lake comparator` checks that each one
+  proves exactly the statement written here. The `sorry` below is
+  expected in this file only.
+
+  The statements use the definitions in `ClientHello/Value.lean` and
+  `ClientHello/Parse.lean`, the code under proof named in `bar.toml`,
+  and one definition of their own: `Spec.WF`, what a well formed
+  message is, in `Spec/Defs.lean`. That file is a spec file too, so the
+  approval fixes what the round trips mean.
+-/
+
+import ClientHello
+import Spec.Defs
+
+open ClientHello
+
+/-! ## The round trips
+
+The two statements the slice stands on. Each one is the statement of
+the proved theorem of the same shape in `Proofs/RoundTrip.lean`, over
+the well formedness predicate `Spec.WF` of `Spec/Defs.lean`. -/
+
+/-- Parsing the printed form of a well formed message gives the
+    message back. -/
+theorem Spec.parse_print (m : Message) (hw : Spec.WF m) :
+    parse (print m) = some m := sorry
+
+/-- A message the parser took prints back to the bytes it was read
+    from, and the message is well formed. So a printer that wrote
+    nothing, or wrote something shorter, fails the first half. -/
+theorem Spec.print_parse {bs : List UInt8} {m : Message}
+    (hparse : parse bs = some m) :
+    print m = bs ∧ Spec.WF m := sorry
+
+/-! ## Rules every accepted message meets
+
+Each of these follows from `Spec.print_parse`, since the well formedness
+predicate includes the rule; it is stated on its own so that the claim on
+the page names a theorem that says exactly that. -/
+
+/-- An accepted hello that offers TLS 1.3, that is one with a
+    supported_versions extension whose list holds 0x0304 (772) in any
+    position, carries exactly one compression method, the null method 0
+    (RFC 8446 section 4.1.2). The hypotheses name the extension and the
+    version themselves, so what "offers TLS 1.3" means is fixed here and
+    not by a definition in the code. -/
+theorem Spec.tls13_compression_null {bs : List UInt8} {m : Message}
+    {vs : List Nat}
+    (hparse : parse bs = some m)
+    (hsv : Extension.supportedVersions vs ∈ m.hello.extensions)
+    (h13 : 772 ∈ vs) :
+    m.hello.compressionMethods = [0] := sorry
+
+/-- In an accepted hello, no extension but the last has type 41
+    (pre_shared_key): when present, pre_shared_key is the last extension
+    (RFC 8446 section 4.2.11). -/
+theorem Spec.psk_last {bs : List UInt8} {m : Message}
+    (hparse : parse bs = some m) :
+    41 ∉ (m.hello.extensions.dropLast).map extType := sorry
+
+/-! ## Accepted examples
+
+Single inputs the parser accepts. Each one is stated in the form the
+round trip gives for a single input: parsing the bytes and printing
+the result gives the same bytes back. -/
+
+/-- A hello whose extensions block is present and empty is accepted, and writes back as the same bytes. -/
+theorem Spec.accepts_empty_extensions :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8) := sorry
+
+/-- A minimal hello carrying only a supported_versions extension is accepted, and writes back as the same bytes. -/
+theorem Spec.accepts_supported_versions :
+    (parse ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8) := sorry
+
+/-- A TLS 1.3 hello whose key_share carries an empty client_shares list,
+    the form a client sends to ask for a HelloRetryRequest (RFC 8446
+    section 4.2.8), is accepted and writes back as the same bytes. Besides
+    key_share it carries supported_groups [x25519, secp256r1],
+    supported_versions [0x0304] and signature_algorithms. -/
+theorem Spec.accepts_key_share_empty_list :
+    (parse ([22, 3, 1, 0, 78, 1, 0, 0, 74, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 31, 0, 10, 0, 6, 0, 4, 0, 29, 0, 23, 0, 43, 0, 3, 2, 3, 4, 0, 51, 0, 2, 0, 0, 0, 13, 0, 4, 0, 2, 4, 3] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 78, 1, 0, 0, 74, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 31, 0, 10, 0, 6, 0, 4, 0, 29, 0, 23, 0, 43, 0, 3, 2, 3, 4, 0, 51, 0, 2, 0, 0, 0, 13, 0, 4, 0, 2, 4, 3] : List UInt8) := sorry
+
+/-- A hello that does not offer TLS 1.3 (it has no extensions) may list
+    compression methods besides null: here [1, 0]. It is accepted and writes
+    back as the same bytes. -/
+theorem Spec.accepts_tls12_compression :
+    (parse ([22, 3, 1, 0, 48, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 0] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 48, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 0] : List UInt8) := sorry
+
+/-- A hello whose last extension is pre_shared_key (type 41, its value
+    carried opaque, here two bytes) after supported_versions is accepted
+    and writes back as the same bytes. -/
+theorem Spec.accepts_psk_last :
+    (parse ([22, 3, 1, 0, 62, 1, 0, 0, 58, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 15, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 41, 0, 2, 0, 0] : List UInt8)).map print =
+      some ([22, 3, 1, 0, 62, 1, 0, 0, 58, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 15, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 41, 0, 2, 0, 0] : List UInt8) := sorry
+
+/-! ## The record limit, accept side
+
+`Spec.rejects_record_overflow` refuses every record length above 2^14.
+This is the other side of that limit: one record of exactly 2^14 bytes
+is accepted. Its first 65 bytes are fixed; the 16324 bytes of its padding
+value may be any bytes. -/
+
+/-- A record of exactly 2^14 = 16384 bytes, the most RFC 8446 section 5.1
+    allows, is accepted and writes back as the same bytes. The input is
+    the hello of `Spec.accepts_supported_versions` with a second extension
+    after its supported_versions: type 21 (padding, RFC 7685, carried
+    opaque) whose value is any 16324 bytes `v`. The lengths that cover it
+    change to match: the record length field is 16384 (64, 0), the
+    handshake length 16380, the extensions block 16337 and the padding
+    value 16324. The input is 16389 bytes long. -/
+theorem Spec.accepts_record_at_limit (v : List UInt8)
+    (hv : v.length = 16324) :
+    (parse (([22, 3, 1, 64, 0, 1, 0, 63, 252, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 63, 209, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 21, 63, 196] : List UInt8) ++ v)).map print =
+      some (([22, 3, 1, 64, 0, 1, 0, 63, 252, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 63, 209, 0, 43, 0, 5, 4, 3, 4, 3, 3, 0, 21, 63, 196] : List UInt8) ++ v) := sorry
+
+/-! ## Refused inputs
+
+Single inputs the parser refuses, one for each headline rule of
+`SPEC.md`. The differential tests cover these rules on many more
+inputs; these statements pin them so a reader of the specification
+can check each rule against one concrete case. -/
+
+/-- Empty input is refused: it is not a record with an empty body. -/
+theorem Spec.rejects_empty :
+    (parse ([] : List UInt8)).isSome = false := sorry
+
+/-- Input shorter than the five byte record header is refused. -/
+theorem Spec.rejects_short_header :
+    (parse ([22, 3] : List UInt8)).isSome = false := sorry
+
+/-- A record length of 0 is refused: an empty body cannot hold a ClientHello. -/
+theorem Spec.rejects_record_length_zero :
+    (parse ([22, 3, 1, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_supported_versions` with content type 23
+    (application_data) in place of 22 is refused. -/
+theorem Spec.rejects_content_type :
+    (parse ([23, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- A record whose length field (10) is longer than the 4 bytes that follow
+    is refused. -/
+theorem Spec.rejects_record_length_longer :
+    (parse ([22, 3, 1, 0, 10, 1, 0, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- A record whose length field, bytes 3 and 4 read big endian, is above
+    2^14 = 16384 is refused, whatever the other header bytes are and
+    whatever follows (RFC 8446 section 5.1: the length MUST NOT exceed
+    2^14 bytes). -/
+theorem Spec.rejects_record_overflow (ct v1 v2 a b : UInt8)
+    (rest : List UInt8) (h : 16384 < a.toNat * 256 + b.toNat) :
+    parse (ct :: v1 :: v2 :: a :: b :: rest) = none := sorry
+
+/-- Bytes after the record are refused rather than ignored. -/
+theorem Spec.rejects_trailing_bytes :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_supported_versions` with handshake type 2
+    (server_hello) in place of 1 is refused. -/
+theorem Spec.rejects_handshake_type :
+    (parse ([22, 3, 1, 0, 56, 2, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- A handshake length that does not equal the remaining body length is refused. -/
+theorem Spec.rejects_handshake_length :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- A body that ends after the compression methods, with no extensions block, is refused. -/
+theorem Spec.rejects_missing_extensions :
+    (parse ([22, 3, 1, 0, 45, 1, 0, 0, 41, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_supported_versions` with a 33-byte session
+    id, one over the limit of 32, is refused. Only the session id and the
+    lengths that cover it differ. -/
+theorem Spec.rejects_session_id_33 :
+    (parse ([22, 3, 1, 0, 89, 1, 0, 0, 85, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 33, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_supported_versions` with a 3-byte cipher
+    suite list (19, 1, 19), an odd length, is refused. -/
+theorem Spec.rejects_odd_cipher_suites :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 3, 19, 1, 19, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_supported_versions` with an empty cipher
+    suite list is refused. -/
+theorem Spec.rejects_empty_cipher_suites :
+    (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 0, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_empty_extensions` with compression methods
+    [1], which lack the null method 0, is refused. It offers no TLS 1.3,
+    so only the null method rule applies. -/
+theorem Spec.rejects_compression_without_null :
+    (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 1, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_empty_extensions` with an empty compression
+    method list is refused. An empty list holds no null method, so the
+    rule of `Spec.rejects_compression_without_null` refuses it as well. -/
+theorem Spec.rejects_empty_compression :
+    (parse ([22, 3, 1, 0, 46, 1, 0, 0, 42, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 0, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- A hello that offers TLS 1.3 and lists compression methods [1, 0] is
+    refused: for TLS 1.3 the list must be exactly [0]. The input is the
+    hello of `Spec.accepts_supported_versions` with that one field
+    changed. -/
+theorem Spec.rejects_tls13_compression :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.rejects_tls13_compression` with its supported_versions
+    list in the other order, [0x0303, 0x0304], is refused too: a hello
+    offers TLS 1.3 when 0x0304 is anywhere in the list, not only first. -/
+theorem Spec.rejects_tls13_compression_second :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 2, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 3, 3, 4] : List UInt8)).isSome = false := sorry
+
+/-- An extension type standing twice in one block is refused. -/
+theorem Spec.rejects_duplicate_extension :
+    (parse ([22, 3, 1, 0, 61, 1, 0, 0, 57, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 14, 0, 43, 0, 3, 2, 3, 4, 0, 43, 0, 3, 2, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- The hello of `Spec.accepts_psk_last` with its two extensions in the
+    other order, pre_shared_key first, is refused. -/
+theorem Spec.rejects_psk_not_last :
+    (parse ([22, 3, 1, 0, 62, 1, 0, 0, 58, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 15, 0, 41, 0, 2, 0, 0, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).isSome = false := sorry
+
+/-- A hello whose one extension declares 10 value bytes where its block
+    holds 3 is refused. -/
+theorem Spec.rejects_extension_overrun :
+    (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 0, 0, 10, 2, 3, 4] : List UInt8)).isSome = false := sorry
+
+/-- A key share group standing twice in one key_share value is refused. -/
+theorem Spec.rejects_duplicate_key_share_group :
+    (parse ([22, 3, 1, 0, 63, 1, 0, 0, 59, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 16, 0, 51, 0, 12, 0, 10, 0, 29, 0, 1, 1, 0, 29, 0, 1, 2] : List UInt8)).isSome = false := sorry
+
+/-- A key share entry with empty key exchange bytes is refused. -/
+theorem Spec.rejects_key_share_empty_key :
+    (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 10, 0, 51, 0, 6, 0, 4, 0, 29, 0, 0] : List UInt8)).isSome = false := sorry
+
+/-- A hello whose one extension is supported_versions with the 4-byte
+    value [3, 3, 4, 3] is refused. Its list length byte is 3, which is odd,
+    and the 3 bytes after it match that length, so the odd length
+    is what refuses it. -/
+theorem Spec.rejects_supported_versions_odd :
+    (parse ([22, 3, 1, 0, 55, 1, 0, 0, 51, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 8, 0, 43, 0, 4, 3, 3, 4, 3] : List UInt8)).isSome = false := sorry
+
+/-- A hello whose one extension is supported_versions with the 1-byte
+    value [0] is refused. Its list length byte is 0, so it lists no
+    version. -/
+theorem Spec.rejects_supported_versions_zero :
+    (parse ([22, 3, 1, 0, 52, 1, 0, 0, 48, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 5, 0, 43, 0, 1, 0] : List UInt8)).isSome = false := sorry
+
+/-- An ALPN value holding an empty protocol name is refused. -/
+theorem Spec.rejects_alpn_empty_name :
+    (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 16, 0, 3, 0, 1, 0] : List UInt8)).isSome = false := sorry
+
+/-- A server_name value with two host_name entries is refused. -/
+theorem Spec.rejects_sni_second_host_name :
+    (parse ([22, 3, 1, 0, 77, 1, 0, 0, 73, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 30, 0, 0, 0, 26, 0, 24, 0, 0, 9, 97, 46, 101, 120, 97, 109, 112, 108, 101, 0, 0, 9, 98, 46, 101, 120, 97, 109, 112, 108, 101] : List UInt8)).isSome = false := sorry
+
+/-- A server_name value whose list length does not cover the rest of the value is refused. -/
+theorem Spec.rejects_sni_list_length :
+    (parse ([22, 3, 1, 0, 67, 1, 0, 0, 63, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 20, 0, 0, 0, 16, 0, 99, 0, 0, 11, 101, 120, 97, 109, 112, 108, 101, 46, 99, 111, 109] : List UInt8)).isSome = false := sorry
diff --git a/Spec/Defs.lean b/Spec/Defs.lean
new file mode 100644
index 0000000..5b89f33
--- /dev/null
+++ b/Spec/Defs.lean
@@ -0,0 +1,82 @@
+/-
+  What a well formed message is: the one definition the statements in
+  `Spec.lean` use besides the code under proof.
+
+  This file is part of the specification. `bar.toml` lists it among the
+  spec files, so a reviewer approves it with `Spec.lean` and `SPEC.md`,
+  and the approval hash pins it. `Spec.parse_print` and
+  `Spec.print_parse` take their meaning from `Spec.WF`: together they
+  say the parser accepts exactly the printed forms of the messages
+  `Spec.WF` describes. If the predicate sat in the code, a change to the
+  parser together with the same change to the predicate would leave
+  every statement true and the hash unchanged.
+
+  It reads the data model and the printer of `ClientHello/Value.lean`
+  (the types, `extType`, and the lengths of printed blocks), which are
+  code under proof, and nothing of the parser.
+-/
+
+import ClientHello.Value
+
+namespace Spec
+
+open ClientHello
+
+/-- Well formedness of one extension, at the level the
+    printer needs: every length it writes fits the field that
+    holds it, and the rules `SPEC.md` gives for the value
+    hold. -/
+def ExtWF : Extension → Prop
+  | .serverName es =>
+    es ≠ [] ∧
+    (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧
+      (e.1 = 0 → e.2 ≠ [])) ∧
+    List.Nodup (es.map Prod.fst) ∧
+    (printNameEntries es).length ≤ 65533
+  | .alpn ns =>
+    ns ≠ [] ∧
+    (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) ∧
+    (printAlpnNames ns).length ≤ 65533
+  | .supportedVersions vs =>
+    vs ≠ [] ∧ (∀ v ∈ vs, v < 65536) ∧ vs.length ≤ 127
+  | .keyShare ss =>
+    (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧
+      s.2.length ≤ 65535) ∧
+    List.Nodup (ss.map Prod.fst) ∧
+    (printShares ss).length ≤ 65533
+  | .opaque t v =>
+    ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧
+    t < 65536 ∧ v.length ≤ 65535
+
+/-- A well formed message: every number fits the field that
+    holds it, every byte block holds the length its field
+    demands, the cipher suites and compression methods meet
+    their rules, every extension is well formed, no
+    extension type stands twice, pre_shared_key (type 41)
+    stands last if present (RFC 8446 section 4.2.11), a
+    hello with a supported_versions extension that lists
+    0x0304 (772), that is one that offers TLS 1.3, carries
+    exactly the null compression method (RFC 8446 section
+    4.1.2), and the handshake message (four header bytes and
+    the body fields) fits a record of at most 2^14 = 16384
+    bytes (RFC 8446 section 5.1). -/
+def WF (m : Message) : Prop :=
+  m.recordVersion < 65536 ∧
+  m.hello.legacyVersion < 65536 ∧
+  m.hello.random.length = 32 ∧
+  m.hello.sessionId.length ≤ 32 ∧
+  m.hello.cipherSuites ≠ [] ∧
+  (∀ v ∈ m.hello.cipherSuites, v < 65536) ∧
+  m.hello.cipherSuites.length ≤ 32767 ∧
+  m.hello.compressionMethods ≠ [] ∧
+  (0 : UInt8) ∈ m.hello.compressionMethods ∧
+  m.hello.compressionMethods.length ≤ 255 ∧
+  (∀ e ∈ m.hello.extensions, ExtWF e) ∧
+  List.Nodup (m.hello.extensions.map extType) ∧
+  41 ∉ (m.hello.extensions.dropLast).map extType ∧
+  (∀ vs, Extension.supportedVersions vs ∈ m.hello.extensions →
+    772 ∈ vs → m.hello.compressionMethods = [0]) ∧
+  (printExts m.hello.extensions).length ≤ 65535 ∧
+  (printBodyFields m.hello).length ≤ 16380
+
+end Spec
diff --git a/bar.toml b/bar.toml
new file mode 100644
index 0000000..1c9efca
--- /dev/null
+++ b/bar.toml
@@ -0,0 +1,63 @@
+# Read by bar/check.py in Proven-Commons/mission.
+# See playbook/verified-bar.md there for what each field means.
+
+[project]
+name = "clienthello"
+# "in-progress" until every bar item passes, then "verified".
+status = "in-progress"
+page = "README.md"
+# GitHub handles of everyone who wrote the specification.
+spec_authors = ["abu-aska", "zero-aska"]
+# The program people run. A change to it voids the approval.
+entry_points = ["Main.lean"]
+
+[spec]
+# Spec/Defs.lean holds Spec.WF, the well formedness predicate the round
+# trips are stated over, so that the approval pins what they mean.
+files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean"]
+# The code under proof: the functions the statements are about.
+code = [
+  # The data types the statements are about, their constructors, and
+  # the case split on an extension that Spec.ExtWF's match compiles to.
+  "ClientHello.Message", "ClientHello.Hello", "ClientHello.Extension",
+  "ClientHello.Extension.serverName", "ClientHello.Extension.alpn",
+  "ClientHello.Extension.supportedVersions", "ClientHello.Extension.keyShare",
+  "ClientHello.Extension.opaque", "ClientHello.Extension.casesOn",
+  # The fields the statements and Spec.WF read.
+  "ClientHello.Message.recordVersion", "ClientHello.Message.hello",
+  "ClientHello.Hello.legacyVersion", "ClientHello.Hello.random",
+  "ClientHello.Hello.sessionId", "ClientHello.Hello.cipherSuites",
+  "ClientHello.Hello.compressionMethods", "ClientHello.Hello.extensions",
+  # The byte forms and the printer.
+  "ClientHello.be16", "ClientHello.u16", "ClientHello.be24", "ClientHello.u24",
+  "ClientHello.extType", "ClientHello.printPairs", "ClientHello.printNameEntries",
+  "ClientHello.printAlpnNames", "ClientHello.printShares",
+  "ClientHello.printExtValue", "ClientHello.printExt", "ClientHello.printExts",
+  "ClientHello.printBodyFields", "ClientHello.printBody", "ClientHello.print",
+  # The parser's test of whether a hello offers TLS 1.3. It is listed
+  # because parseBodyFields calls it; no statement and nothing in the
+  # spec files reads it.
+  "ClientHello.offersTls13",
+  # The length checked readers and the parser.
+  "ClientHello.getU16", "ClientHello.withU8", "ClientHello.withU16",
+  "ClientHello.withU24", "ClientHello.withBytes", "ClientHello.parsePairs",
+  "ClientHello.parseNameEntriesGo", "ClientHello.parseNameEntries",
+  "ClientHello.validNames", "ClientHello.parseSNI",
+  "ClientHello.parseAlpnGo", "ClientHello.parseAlpnNames", "ClientHello.parseALPN",
+  "ClientHello.parseSV", "ClientHello.parseSharesGo", "ClientHello.parseShares",
+  "ClientHello.parseKS", "ClientHello.parseExtValue",
+  "ClientHello.parseExtsGo", "ClientHello.parseExts",
+  "ClientHello.parseBodyFields", "ClientHello.parseBody", "ClientHello.parse",
+]
+
+# One entry per approval, added in a pull request the reviewer approves.
+# [[spec.approval]]
+# reviewer = "github-handle"
+# date = "2026-11-02"
+# sha256 = "..."
+# record = "https://github.com/Proven-Commons/clienthello/pull/<n>"
+
+[tests]
+results = "tests/TEST-RESULTS.md"
+command = "python3 tests/run_tests.py"
+files = ["tests/run_tests.py"]
diff --git a/comparator.json b/comparator.json
new file mode 100644
index 0000000..ee70f03
--- /dev/null
+++ b/comparator.json
@@ -0,0 +1,48 @@
+{
+  "challenge_module": "Spec",
+  "solution_module": "Proofs",
+  "theorem_names": [
+    "Spec.parse_print",
+    "Spec.print_parse",
+    "Spec.tls13_compression_null",
+    "Spec.psk_last",
+    "Spec.accepts_empty_extensions",
+    "Spec.accepts_supported_versions",
+    "Spec.accepts_key_share_empty_list",
+    "Spec.accepts_tls12_compression",
+    "Spec.accepts_psk_last",
+    "Spec.accepts_record_at_limit",
+    "Spec.rejects_empty",
+    "Spec.rejects_short_header",
+    "Spec.rejects_record_length_zero",
+    "Spec.rejects_content_type",
+    "Spec.rejects_record_length_longer",
+    "Spec.rejects_record_overflow",
+    "Spec.rejects_trailing_bytes",
+    "Spec.rejects_handshake_type",
+    "Spec.rejects_handshake_length",
+    "Spec.rejects_missing_extensions",
+    "Spec.rejects_session_id_33",
+    "Spec.rejects_odd_cipher_suites",
+    "Spec.rejects_empty_cipher_suites",
+    "Spec.rejects_compression_without_null",
+    "Spec.rejects_empty_compression",
+    "Spec.rejects_tls13_compression",
+    "Spec.rejects_tls13_compression_second",
+    "Spec.rejects_duplicate_extension",
+    "Spec.rejects_psk_not_last",
+    "Spec.rejects_extension_overrun",
+    "Spec.rejects_duplicate_key_share_group",
+    "Spec.rejects_key_share_empty_key",
+    "Spec.rejects_supported_versions_odd",
+    "Spec.rejects_supported_versions_zero",
+    "Spec.rejects_alpn_empty_name",
+    "Spec.rejects_sni_second_host_name",
+    "Spec.rejects_sni_list_length"
+  ],
+  "permitted_axioms": [
+    "propext",
+    "Classical.choice",
+    "Quot.sound"
+  ]
+}
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..e965eb3
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "clienthello",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..f719108
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,17 @@
+name = "clienthello"
+version = "0.1.0"
+license = "Apache-2.0"
+defaultTargets = ["ClientHello", "Proofs", "clienthello"]
+
+[[lean_lib]]
+name = "ClientHello"
+
+[[lean_lib]]
+name = "Proofs"
+
+[[lean_lib]]
+name = "Spec"
+
+[[lean_exe]]
+name = "clienthello"
+root = "Main"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..a6aff06
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.35.0
diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md
new file mode 100644
index 0000000..e913f5d
--- /dev/null
+++ b/tests/TEST-RESULTS.md
@@ -0,0 +1,75 @@
+# ClientHello slice: test results
+
+- Oracle: the harness oracle in tests/run_tests.py, a second reading of SPEC.md in Python 3.13.17, for every input; and OpenSSL 3.0.13 30 Jan 2024 through Python's ssl module, which built 24 of the inputs as real ClientHellos that must be accepted and printed back byte for byte
+- Seed: 20261026
+- Inputs: 4939
+- Failures: 0
+- Command: python3 tests/run_tests.py --seed 20261026 --count 3200
+
+## Oracles
+
+Every verdict is settled by the harness oracle, a Python implementation of the rules in SPEC.md written for these tests. It is a second reading by the same authors, not an independent implementation. The tool must agree with it on every input, and an accepted message must print back to the oracle's canonical form byte for byte.
+
+Python's ssl module builds real ClientHellos in memory: a client SSLObject over two MemoryBIOs writes its hello on the first do_handshake(). The run makes 24 of them with OpenSSL 3.0.13 30 Jan 2024, two under each of 12 settings (TLS 1.2 only, TLS 1.3 only, both; with and without SNI and ALPN; a cipher list, a single group, post-handshake auth). Each must be accepted and printed back unchanged. Their random bytes and key shares differ from run to run; their count and settings do not. OpenSSL is a source of real accepted inputs here, not a verdict oracle: no TLS stack is asked to judge the malformed inputs, so the verdicts on those rest on the harness oracle alone. The other fixed cases are built by hand from the RFCs.
+
+## Counts
+
+| part | run | agreed |
+| --- | --- | --- |
+| named cases | 40 | 40 |
+| generated messages | 3200 | 3200 |
+| mutations of the full hello | 1308 | 1308 |
+| random raw byte strings | 300 | 300 |
+| hellos near the 2^14 record limit | 60 | 60 |
+| ClientHellos built by OpenSSL | 24 | 24 |
+| malformed request lines | 7 | 7 |
+| total | 4939 | 4939 |
+
+Of the 3200 generated messages, the oracle accepts 1266 and rejects 1934.
+
+## Named cases
+
+- full TLS 1.3 style hello: accept (252 bytes)
+- minimal hello, supported versions only: accept (61 bytes)
+- duplicate extension type: reject (66 bytes)
+- duplicate key share group: reject (130 bytes)
+- extension length overrunning the block: reject (59 bytes)
+- record length longer than the input: reject (52 bytes)
+- handshake length not matching the body: reject (52 bytes)
+- content type 23: reject (61 bytes)
+- handshake type 2: reject (61 bytes)
+- session id length 33: reject (85 bytes)
+- odd cipher suite length: reject (53 bytes)
+- empty cipher suites: reject (50 bytes)
+- compression methods without 0: reject (53 bytes)
+- TLS 1.3 hello with compression methods 01 00: reject (60 bytes)
+- TLS 1.3 hello with compression methods 00 00: reject (62 bytes)
+- TLS 1.3 hello listing 0x0304 second, supported_versions [0x0303, 0x0304], with compression methods 01 00: reject (62 bytes)
+- TLS 1.2 hello (supported_versions 0x0303 only) with compression methods 01 00, accepted: accept (60 bytes)
+- hello without extensions, compression methods 01 00, accepted: accept (53 bytes)
+- pre_shared_key last, after key_share, accepted: accept (157 bytes)
+- pre_shared_key before key_share: reject (157 bytes)
+- pre_shared_key first of two: reject (109 bytes)
+- missing extensions block: reject (50 bytes)
+- supported versions value 03 03 04 03: list length byte 3, odd: reject (60 bytes)
+- supported versions value 00: list length byte 0: reject (57 bytes)
+- ALPN empty name: reject (59 bytes)
+- ALPN list length mismatch: reject (61 bytes)
+- ALPN empty list: reject (58 bytes)
+- SNI second host_name entry: reject (82 bytes)
+- SNI list length mismatch: reject (72 bytes)
+- SNI empty list: reject (58 bytes)
+- key share empty key bytes: reject (62 bytes)
+- key share empty list, accepted: accept (58 bytes)
+- TLS 1.3 hello asking for a HelloRetryRequest (supported_groups, supported_versions 0x0304, empty key_share), accepted: accept (83 bytes)
+- trailing garbage after the record: reject (53 bytes)
+- empty extensions block, length 0, accepted: accept (52 bytes)
+- record length 16384, the 2^14 limit, accepted: accept (16389 bytes)
+- record length 16385, over the 2^14 limit: reject (16390 bytes)
+- record length zero: reject (5 bytes)
+- input shorter than the record header: reject (2 bytes)
+- empty input: reject (0 bytes)
+
+## Differences
+
+No disagreements between the tool and the oracle, and every named case matched its stated expectation.
diff --git a/tests/run_tests.py b/tests/run_tests.py
new file mode 100644
index 0000000..46f020c
--- /dev/null
+++ b/tests/run_tests.py
@@ -0,0 +1,1068 @@
+#!/usr/bin/env python3
+"""Tests for the Lean TLS ClientHello parser and printer.
+
+Three parts.
+
+1. Fixed cases built by hand from RFC 8446 section 4.1.2,
+   RFC 5246 and RFC 6066: one full TLS 1.3 style hello (SNI
+   for a named host, ALPN h2 and http/1.1, supported versions
+   0x0304 and 0x0303, key shares for x25519 and secp256r1
+   with fixed key bytes, and one opaque extension), one
+   minimal hello (supported versions only), and the named
+   rejection shapes listed in SPEC.md, plus the pinned
+   reading that a present but empty extensions block (length
+   0) is accepted.
+
+2. A differential run against a strict Python oracle written
+   in this harness from the rules in SPEC.md: at least 3,000
+   generated messages (varied record and legacy versions,
+   session ids, cipher suite lists, compression lists,
+   extension sets and orders, with defects injected from a
+   menu), plus raw mutations of the full fixed hello (every
+   truncation, single byte flips, random multi-byte changes)
+   and fully random byte strings. The oracle settles every
+   verdict; the tool must agree with it on each input.
+
+3. Real ClientHellos built by OpenSSL through Python's ssl
+   module, under a fixed list of settings. A client SSLObject
+   over two MemoryBIOs writes its hello on the first
+   do_handshake(), with no network. Each must be accepted and
+   printed back byte for byte. OpenSSL is used here only as a
+   source of real hellos; its verdicts on malformed input are
+   not compared.
+
+4. Malformed request lines must be answered `error`.
+
+The harness oracle is a second reading of SPEC.md, written
+for these tests by the same authors. It is not an
+independent implementation, and the results record says so.
+
+    python3 tests/run_tests.py [--seed N] [--count N]
+
+The tool is driven one batch process per chunk of requests,
+input written and closed, output drained until the process
+exits. It builds the executable first, writes
+tests/TEST-RESULTS.md, and exits non-zero if any check
+fails. It needs Python 3.11 or later.
+"""
+
+import argparse
+import os
+import platform
+import random
+import subprocess
+import sys
+import threading
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent.parent
+EXE = ROOT / ".lake" / "build" / "bin" / "clienthello"
+RESULTS = ROOT / "tests" / "TEST-RESULTS.md"
+
+
+# ----------------------------------------------------------------
+# The oracle: a second implementation of the SPEC rules, written
+# for these tests. It parses bytes into a model and reprints the
+# model; the reprint of an accepted message is the expected tool
+# answer.
+# ----------------------------------------------------------------
+
+class Reject(Exception):
+    pass
+
+
+def take(bs, i, n):
+    if i + n > len(bs):
+        raise Reject()
+    return bs[i:i + n], i + n
+
+
+def u8(bs, i):
+    bs2, i = take(bs, i, 1)
+    return bs2[0], i
+
+
+def u16(bs, i):
+    bs2, i = take(bs, i, 2)
+    return (bs2[0] << 8) | bs2[1], i
+
+
+def u24(bs, i):
+    bs2, i = take(bs, i, 3)
+    return (bs2[0] << 16) | (bs2[1] << 8) | bs2[2], i
+
+
+def be16(n):
+    return bytes([(n >> 8) & 0xFF, n & 0xFF])
+
+
+def be24(n):
+    return bytes([(n >> 16) & 0xFF, (n >> 8) & 0xFF, n & 0xFF])
+
+
+def oracle_sni(v):
+    listlen, i = u16(v, 0)
+    if listlen != len(v) - 2:
+        raise Reject()
+    entries = []
+    seen = set()
+    while i < len(v):
+        t, i = u8(v, i)
+        ln, i = u16(v, i)
+        name, i = take(v, i, ln)
+        if t in seen:
+            raise Reject()
+        seen.add(t)
+        if t == 0 and len(name) == 0:
+            raise Reject()
+        entries.append((t, bytes(name)))
+    if not entries:
+        raise Reject()
+    out = be16(listlen)
+    for t, name in entries:
+        out += bytes([t]) + be16(len(name)) + name
+    return ("sni", entries), out
+
+
+def oracle_alpn(v):
+    listlen, i = u16(v, 0)
+    if listlen != len(v) - 2:
+        raise Reject()
+    names = []
+    while i < len(v):
+        ln, i = u8(v, i)
+        if ln < 1:
+            raise Reject()
+        name, i = take(v, i, ln)
+        names.append(bytes(name))
+    if not names:
+        raise Reject()
+    out = be16(listlen)
+    for name in names:
+        out += bytes([len(name)]) + name
+    return ("alpn", names), out
+
+
+def oracle_sv(v):
+    ln, i = u8(v, 0)
+    if ln != len(v) - 1 or ln % 2 != 0 or ln < 2:
+        raise Reject()
+    versions = []
+    while i < len(v):
+        ver, i = u16(v, i)
+        versions.append(ver)
+    out = bytes([ln])
+    for ver in versions:
+        out += be16(ver)
+    return ("sv", versions), out
+
+
+def oracle_ks(v):
+    listlen, i = u16(v, 0)
+    if listlen != len(v) - 2:
+        raise Reject()
+    shares = []
+    seen = set()
+    while i < len(v):
+        group, i = u16(v, i)
+        klen, i = u16(v, i)
+        if klen < 1:
+            raise Reject()
+        key, i = take(v, i, klen)
+        if group in seen:
+            raise Reject()
+        seen.add(group)
+        shares.append((group, bytes(key)))
+    # An empty list is allowed: RFC 8446 section 4.2.8, a
+    # client asking for a HelloRetryRequest sends no shares.
+    out = be16(listlen)
+    for group, key in shares:
+        out += be16(group) + be16(len(key)) + key
+    return ("ks", shares), out
+
+
+def oracle_ext_value(t, v):
+    if t == 0:
+        return oracle_sni(v)
+    if t == 16:
+        return oracle_alpn(v)
+    if t == 43:
+        return oracle_sv(v)
+    if t == 51:
+        return oracle_ks(v)
+    return ("opaque", t, bytes(v)), bytes(v)
+
+
+def oracle_exts(block):
+    exts = []
+    seen = set()
+    i = 0
+    while i < len(block):
+        t, i = u16(block, i)
+        ln, i = u16(block, i)
+        v, i = take(block, i, ln)
+        if t in seen:
+            raise Reject()
+        seen.add(t)
+        ext, _ = oracle_ext_value(t, bytes(v))
+        exts.append((t, ext))
+    # RFC 8446 section 4.2.11: pre_shared_key (41) must be the
+    # last extension in the ClientHello.
+    if 41 in [t for t, _ in exts[:-1]]:
+        raise Reject()
+    return exts
+
+
+def print_ext(ext):
+    kind = ext[0]
+    if kind == "sni":
+        body = b""
+        for t, name in ext[1]:
+            body += bytes([t]) + be16(len(name)) + name
+        return be16(0) + be16(len(body) + 2) + be16(len(body)) + body
+    if kind == "alpn":
+        body = b""
+        for name in ext[1]:
+            body += bytes([len(name)]) + name
+        return be16(16) + be16(len(body) + 2) + be16(len(body)) + body
+    if kind == "sv":
+        body = bytes([2 * len(ext[1])])
+        for ver in ext[1]:
+            body += be16(ver)
+        return be16(43) + be16(len(body)) + body
+    if kind == "ks":
+        body = b""
+        for group, key in ext[1]:
+            body += be16(group) + be16(len(key)) + key
+        return be16(51) + be16(len(body) + 2) + be16(len(body)) + body
+    _, t, v = ext
+    return be16(t) + be16(len(v)) + v
+
+
+def oracle_parse(bs):
+    """The canonical reprint of the message, or None."""
+    try:
+        return oracle_parse_go(bs)
+    except Reject:
+        return None
+
+
+def oracle_parse_go(bs):
+    ct, i = u8(bs, 0)
+    if ct != 22:
+        raise Reject()
+    rv, i = take(bs, i, 2)
+    rlen, i = u16(bs, i)
+    # RFC 8446 section 5.1: the record length MUST NOT exceed
+    # 2^14 bytes.
+    if rlen > 16384:
+        raise Reject()
+    body, i = take(bs, i, rlen)
+    if i != len(bs):
+        raise Reject()
+    htype, j = u8(body, 0)
+    if htype != 1:
+        raise Reject()
+    hlen, j = u24(body, j)
+    fields, j = take(body, j, hlen)
+    if j != len(body):
+        raise Reject()
+    ver, k = take(fields, 0, 2)
+    rand, k = take(fields, k, 32)
+    slen, k = u8(fields, k)
+    if slen > 32:
+        raise Reject()
+    sess, k = take(fields, k, slen)
+    clen, k = u16(fields, k)
+    if clen % 2 != 0 or clen < 2:
+        raise Reject()
+    cbytes, k = take(fields, k, clen)
+    suites = []
+    for off in range(0, clen, 2):
+        suites.append((cbytes[off] << 8) | cbytes[off + 1])
+    mlen, k = u8(fields, k)
+    if mlen < 1:
+        raise Reject()
+    comps, k = take(fields, k, mlen)
+    if 0 not in comps:
+        raise Reject()
+    elen, k = u16(fields, k)
+    block, k = take(fields, k, elen)
+    if k != len(fields):
+        raise Reject()
+    exts = oracle_exts(bytes(block))
+    # RFC 8446 section 4.1.2: a hello that offers TLS 1.3 (its
+    # supported_versions lists 0x0304) carries exactly one
+    # compression method, null.
+    offers13 = any(e[0] == "sv" and 0x0304 in e[1] for _, e in exts)
+    if offers13 and bytes(comps) != b"\x00":
+        raise Reject()
+    out_fields = bytes(ver) + bytes(rand)
+    out_fields += bytes([len(sess)]) + bytes(sess)
+    pairs = b""
+    for s in suites:
+        pairs += be16(s)
+    out_fields += be16(len(pairs)) + pairs
+    out_fields += bytes([len(comps)]) + bytes(comps)
+    block_out = b""
+    for _, ext in exts:
+        block_out += print_ext(ext)
+    out_fields += be16(len(block_out)) + block_out
+    out_body = bytes([1]) + be24(len(out_fields)) + out_fields
+    return bytes([22]) + bytes(rv) + be16(len(out_body)) + out_body
+
+
+# ----------------------------------------------------------------
+# Builders: byte level construction of test messages, with
+# knobs for the defect cases. The builders are not the oracle;
+# every built message is judged by the oracle and the tool.
+# ----------------------------------------------------------------
+
+def sni_value(entries):
+    body = b""
+    for t, name in entries:
+        body += bytes([t]) + be16(len(name)) + name
+    return be16(len(body)) + body
+
+
+def alpn_value(names):
+    body = b""
+    for name in names:
+        body += bytes([len(name)]) + name
+    return be16(len(body)) + body
+
+
+def sv_value(versions):
+    body = bytes([2 * len(versions)])
+    for ver in versions:
+        body += be16(ver)
+    return body
+
+
+def ks_value(shares):
+    body = b""
+    for group, key in shares:
+        body += be16(group) + be16(len(key)) + key
+    return be16(len(body)) + body
+
+
+def psk_value(identity=b"abc", binder=bytes(range(32))):
+    """A pre_shared_key value: one identity with a ticket age,
+    and one binder. The parser carries it opaque."""
+    ident = be16(len(identity)) + identity + b"\x00\x00\x00\x07"
+    binders = bytes([len(binder)]) + binder
+    return be16(len(ident)) + ident + be16(len(binders)) + binders
+
+
+def ext_bytes(t, v):
+    return be16(t) + be16(len(v)) + v
+
+
+def build_hello(record_version=b"\x03\x01", legacy_version=b"\x03\x03",
+                random_bytes=None, session_id=b"", suites=(0x1301,),
+                comps=(0,), exts=(), ext_block=True,
+                record_len_delta=0, hs_len_delta=0, trailing=b""):
+    if random_bytes is None:
+        random_bytes = bytes(range(32))
+    fields = legacy_version + random_bytes
+    fields += bytes([len(session_id)]) + session_id
+    pairs = b""
+    for s in suites:
+        pairs += be16(s)
+    fields += be16(len(pairs)) + pairs
+    fields += bytes([len(comps)]) + bytes(comps)
+    if ext_block:
+        block = b""
+        for t, v in exts:
+            block += ext_bytes(t, v)
+        fields += be16(len(block)) + block
+    body = bytes([1]) + be24(len(fields) + hs_len_delta) + fields
+    rec = bytes([22]) + record_version
+    rec += be16(len(body) + record_len_delta) + body
+    return rec + trailing
+
+
+FULL_EXTS = [
+    (0, sni_value([(0, b"example.com")])),
+    (16, alpn_value([b"h2", b"http/1.1"])),
+    (43, sv_value([0x0304, 0x0303])),
+    (51, ks_value([(29, bytes(range(32))),
+                   (23, b"\x04" + bytes(range(64)))])),
+    (23, b""),
+]
+FULL_HELLO = build_hello(
+    session_id=bytes(range(32)),
+    suites=(0x1301, 0x1302, 0x1303, 0xC02F),
+    exts=FULL_EXTS)
+MIN_HELLO = build_hello(exts=[(43, sv_value([0x0304, 0x0303]))])
+EMPTY_EXT_HELLO = build_hello(exts=[])
+
+
+def raw_fields(suites_bytes, comps=(0,), exts=(), ext_block=True):
+    fields = b"\x03\x03" + bytes(range(32)) + b"\x00"
+    fields += be16(len(suites_bytes)) + suites_bytes
+    fields += bytes([len(comps)]) + bytes(comps)
+    if ext_block:
+        block = b""
+        for t, v in exts:
+            block += ext_bytes(t, v)
+        fields += be16(len(block)) + block
+    body = bytes([1]) + be24(len(fields)) + fields
+    return bytes([22, 3, 1]) + be16(len(body)) + body
+
+
+def padded_hello(record_len, rng=None, base_exts=None):
+    """A TLS 1.3 style hello whose record body is exactly
+    record_len bytes, padded with a padding extension (21)."""
+    exts = list(base_exts if base_exts is not None
+                else [(43, sv_value([0x0304, 0x0303]))])
+    probe = build_hello(exts=exts + [(21, b"")])
+    pad = record_len - (len(probe) - 5)
+    fill = (bytes(rng.randrange(256) for _ in range(pad))
+            if rng else bytes(pad))
+    out = build_hello(exts=exts + [(21, fill)])
+    assert len(out) - 5 == record_len
+    return out
+
+
+def gen_near_limit(rng):
+    """Hellos whose record length is within a few bytes of the
+    2^14 limit, on both sides of it."""
+    out = []
+    for _ in range(60):
+        n = rng.randrange(16376, 16393)
+        exts = [(43, sv_value([0x0304]))]
+        if rng.random() < 0.5:
+            exts.append((51, ks_value([(29, bytes(32))])))
+        out.append(padded_hello(n, rng, exts))
+    return out
+
+
+def named_cases():
+    """(name, bytes, expected: True accept / False reject)."""
+    cases = []
+    cases.append(("full TLS 1.3 style hello", FULL_HELLO, True))
+    cases.append(("minimal hello, supported versions only",
+                  MIN_HELLO, True))
+    cases.append(("duplicate extension type",
+                  build_hello(exts=[(43, sv_value([0x0304])),
+                                    (43, sv_value([0x0303]))]),
+                  False))
+    cases.append(("duplicate key share group",
+                  build_hello(exts=[(51, ks_value(
+                      [(29, b"\x01" * 32), (29, b"\x02" * 32)]))]),
+                  False))
+    overrun_block = be16(0) + be16(10) + b"\x02\x03\x04"
+    fields = b"\x03\x03" + bytes(range(32)) + b"\x00"
+    fields += be16(2) + b"\x13\x01" + b"\x01\x00"
+    fields += be16(len(overrun_block)) + overrun_block
+    body = bytes([1]) + be24(len(fields)) + fields
+    cases.append(("extension length overrunning the block",
+                  bytes([22, 3, 1]) + be16(len(body)) + body,
+                  False))
+    cases.append(("record length longer than the input",
+                  build_hello(record_len_delta=5), False))
+    cases.append(("handshake length not matching the body",
+                  build_hello(hs_len_delta=1), False))
+    bad = bytearray(MIN_HELLO)
+    bad[0] = 23
+    cases.append(("content type 23", bytes(bad), False))
+    bad = bytearray(MIN_HELLO)
+    bad[5] = 2
+    cases.append(("handshake type 2", bytes(bad), False))
+    cases.append(("session id length 33",
+                  build_hello(session_id=b"\x07" * 33), False))
+    cases.append(("odd cipher suite length",
+                  raw_fields(b"\x13\x01\x13"), False))
+    cases.append(("empty cipher suites",
+                  build_hello(suites=()), False))
+    cases.append(("compression methods without 0",
+                  build_hello(comps=(1, 2)), False))
+    cases.append(("TLS 1.3 hello with compression methods 01 00",
+                  build_hello(comps=(1, 0),
+                              exts=[(43, sv_value([0x0304]))]),
+                  False))
+    cases.append(("TLS 1.3 hello with compression methods 00 00",
+                  build_hello(comps=(0, 0),
+                              exts=[(43, sv_value([0x0304, 0x0303]))]),
+                  False))
+    cases.append(("TLS 1.3 hello listing 0x0304 second, supported_versions "
+                  "[0x0303, 0x0304], with compression methods 01 00",
+                  build_hello(comps=(1, 0),
+                              exts=[(43, sv_value([0x0303, 0x0304]))]),
+                  False))
+    cases.append(("TLS 1.2 hello (supported_versions 0x0303 only) "
+                  "with compression methods 01 00, accepted",
+                  build_hello(comps=(1, 0),
+                              exts=[(43, sv_value([0x0303]))]),
+                  True))
+    cases.append(("hello without extensions, compression methods "
+                  "01 00, accepted",
+                  build_hello(comps=(1, 0)), True))
+    cases.append(("pre_shared_key last, after key_share, accepted",
+                  build_hello(exts=[
+                      (43, sv_value([0x0304])),
+                      (51, ks_value([(29, bytes(32))])),
+                      (45, b"\x01\x01"),
+                      (41, psk_value())]),
+                  True))
+    cases.append(("pre_shared_key before key_share",
+                  build_hello(exts=[
+                      (43, sv_value([0x0304])),
+                      (41, psk_value()),
+                      (51, ks_value([(29, bytes(32))])),
+                      (45, b"\x01\x01")]),
+                  False))
+    cases.append(("pre_shared_key first of two",
+                  build_hello(exts=[(41, psk_value()),
+                                    (43, sv_value([0x0304]))]),
+                  False))
+    cases.append(("missing extensions block",
+                  build_hello(ext_block=False), False))
+    cases.append(("supported versions value 03 03 04 03: list length "
+                  "byte 3, odd",
+                  build_hello(exts=[(43, bytes([3, 3, 4, 3]))]),
+                  False))
+    cases.append(("supported versions value 00: list length byte 0",
+                  build_hello(exts=[(43, bytes([0]))]), False))
+    cases.append(("ALPN empty name",
+                  build_hello(exts=[(16, be16(1) + b"\x00")]),
+                  False))
+    alpn_bad = be16(9) + alpn_value([b"h2"])[2:]
+    cases.append(("ALPN list length mismatch",
+                  build_hello(exts=[(16, alpn_bad)]), False))
+    cases.append(("ALPN empty list",
+                  build_hello(exts=[(16, alpn_value([]))]),
+                  False))
+    cases.append(("SNI second host_name entry",
+                  build_hello(exts=[(0, sni_value(
+                      [(0, b"a.example"), (0, b"b.example")]))]),
+                  False))
+    sni_bad = be16(99) + sni_value([(0, b"example.com")])[2:]
+    cases.append(("SNI list length mismatch",
+                  build_hello(exts=[(0, sni_bad)]), False))
+    cases.append(("SNI empty list",
+                  build_hello(exts=[(0, sni_value([]))]),
+                  False))
+    cases.append(("key share empty key bytes",
+                  build_hello(exts=[(51, ks_value([(29, b"")]))]),
+                  False))
+    cases.append(("key share empty list, accepted",
+                  build_hello(exts=[(51, ks_value([]))]),
+                  True))
+    cases.append(("TLS 1.3 hello asking for a HelloRetryRequest "
+                  "(supported_groups, supported_versions 0x0304, "
+                  "empty key_share), accepted",
+                  build_hello(exts=[
+                      (10, be16(4) + be16(29) + be16(23)),
+                      (43, sv_value([0x0304])),
+                      (51, ks_value([])),
+                      (13, be16(2) + b"\x04\x03")]),
+                  True))
+    cases.append(("trailing garbage after the record",
+                  build_hello(trailing=b"\x00"), False))
+    cases.append(("empty extensions block, length 0, accepted",
+                  EMPTY_EXT_HELLO, True))
+    cases.append(("record length 16384, the 2^14 limit, accepted",
+                  padded_hello(16384), True))
+    cases.append(("record length 16385, over the 2^14 limit",
+                  padded_hello(16385), False))
+    cases.append(("record length zero",
+                  bytes([22, 3, 1, 0, 0]), False))
+    cases.append(("input shorter than the record header",
+                  bytes([22, 3]), False))
+    cases.append(("empty input", b"", False))
+    return cases
+
+
+# ----------------------------------------------------------------
+# The generated differential cases.
+# ----------------------------------------------------------------
+
+HOSTS = [b"example.com", b"a.b.example.org", b"x", b"host-name.example"]
+
+
+def gen_sni(rng, defect):
+    entries = [(0, rng.choice(HOSTS))]
+    if rng.random() < 0.3:
+        entries.append((rng.choice([1, 2, 3, 17]),
+                        bytes(rng.randrange(256)
+                              for _ in range(rng.randrange(1, 6)))))
+    if defect == "sni-second-host":
+        entries.append((0, b"other.example"))
+    if defect == "sni-dup-type":
+        entries.append((entries[-1][0], b"zz"))
+    if defect == "sni-empty-host":
+        entries[0] = (0, b"")
+    v = sni_value(entries)
+    if defect == "sni-list-len":
+        v = be16(len(v)) + v[2:]
+    return (0, v)
+
+
+def gen_alpn(rng, defect):
+    names = [bytes(rng.choice(b"abcdefg0123456789/.-")
+                   for _ in range(rng.randrange(1, 9)))
+             for _ in range(rng.randrange(1, 4))]
+    if defect == "alpn-empty-name":
+        names.insert(0, b"")
+    v = alpn_value(names)
+    if defect == "alpn-list-len":
+        v = be16(len(v) + 2) + v[2:]
+    return (16, v)
+
+
+def gen_sv(rng, defect):
+    versions = [rng.choice([0x0300, 0x0301, 0x0302, 0x0303,
+                            0x0304, 0x7F1C])
+                for _ in range(rng.randrange(1, 5))]
+    if defect == "sv-odd":
+        return (43, bytes([3, 3, 4, 3]))
+    if defect == "sv-zero":
+        return (43, bytes([0]))
+    if defect == "sv-len-lie":
+        v = sv_value(versions)
+        return (43, bytes([v[0] + 2]) + v[1:])
+    return (43, sv_value(versions))
+
+
+def gen_ks(rng, defect):
+    groups = rng.sample([29, 23, 24, 25, 256, 257],
+                        rng.randrange(1, 4))
+    shares = [(g, bytes(rng.randrange(256)
+                        for _ in range(rng.choice([1, 32, 65]))))
+              for g in groups]
+    if defect == "ks-empty-list":
+        shares = []
+    if defect == "ks-dup-group":
+        shares.append((shares[0][0], b"\x09" * 8))
+    if defect == "ks-empty-key":
+        shares[0] = (shares[0][0], b"")
+    v = ks_value(shares)
+    if defect == "ks-list-len":
+        v = be16(len(v)) + v[2:]
+    return (51, v)
+
+
+def gen_opaque(rng, taken):
+    choices = [t for t in [5, 10, 11, 13, 21, 23, 35, 41, 42,
+                           44, 45, 49, 50, 300, 1000, 65281]
+               if t not in taken]
+    t = rng.choice(choices)
+    if t == 41 and rng.random() < 0.5:
+        return (t, psk_value(bytes(rng.randrange(256)
+                                   for _ in range(rng.randrange(1, 9)))))
+    v = bytes(rng.randrange(256)
+              for _ in range(rng.choice([0, 1, 4, 17, 40])))
+    return (t, v)
+
+
+DEFECTS = [None, None, None, "dup-ext", "no-ext-block",
+           "trailing", "rec-len", "hs-len", "sess33",
+           "suites-empty", "comps-no-null", "comps-empty",
+           "sni-second-host", "sni-dup-type", "sni-empty-host",
+           "sni-list-len", "alpn-empty-name", "alpn-list-len",
+           "sv-odd", "sv-zero", "sv-len-lie", "ks-dup-group",
+           "ks-empty-key", "ks-list-len", "ks-empty-list"]
+
+
+def gen_message(rng):
+    defect = rng.choice(DEFECTS)
+    session_id = bytes(rng.randrange(256)
+                       for _ in range(rng.choice([0, 0, 1, 8, 32])))
+    if defect == "sess33":
+        session_id = bytes(33)
+    nsuites = rng.choice([1, 1, 2, 3, 4, 6])
+    if defect == "suites-empty":
+        nsuites = 0
+    suites = [rng.randrange(65536) for _ in range(nsuites)]
+    comps = [0]
+    if rng.random() < 0.3:
+        comps = [0, 1]
+    if defect == "comps-no-null":
+        comps = [1, 2]
+    if defect == "comps-empty":
+        comps = []
+    builders = [gen_sni, gen_alpn, gen_sv, gen_ks]
+    rng.shuffle(builders)
+    nexts = rng.randrange(0, 5)
+    chosen = builders[:nexts]
+    exts = []
+    taken = set()
+    for b in chosen:
+        e = b(rng, defect)
+        exts.append(e)
+        taken.add(e[0])
+    if rng.random() < 0.5:
+        e = gen_opaque(rng, taken)
+        exts.insert(rng.randrange(len(exts) + 1), e)
+        taken.add(e[0])
+    if defect == "dup-ext" and exts:
+        exts.append(exts[0])
+    rng.shuffle(exts)
+    return build_hello(
+        record_version=bytes([rng.randrange(256),
+                              rng.randrange(256)]),
+        legacy_version=bytes([rng.randrange(256),
+                              rng.randrange(256)]),
+        random_bytes=bytes(rng.randrange(256) for _ in range(32)),
+        session_id=session_id, suites=suites, comps=comps,
+        exts=exts, ext_block=(defect != "no-ext-block"),
+        record_len_delta=(5 if defect == "rec-len" else 0),
+        hs_len_delta=(1 if defect == "hs-len" else 0),
+        trailing=(b"\xaa" if defect == "trailing" else b""))
+
+
+def gen_mutations(rng):
+    out = []
+    for i in range(len(FULL_HELLO)):
+        out.append(FULL_HELLO[:i])
+    for i in range(len(FULL_HELLO)):
+        for d in (0x01, 0x80, 0xFF):
+            b = bytearray(FULL_HELLO)
+            b[i] ^= d
+            out.append(bytes(b))
+    for _ in range(300):
+        b = bytearray(FULL_HELLO)
+        for _ in range(rng.randrange(1, 9)):
+            op = rng.randrange(3)
+            pos = rng.randrange(len(b) + (1 if op == 1 else 0))
+            if op == 0 and b:
+                b[pos % len(b)] = rng.randrange(256)
+            elif op == 1:
+                b.insert(pos, rng.randrange(256))
+            elif op == 2 and b:
+                del b[pos % len(b)]
+        out.append(bytes(b))
+    return out
+
+
+def gen_random_raw(rng):
+    out = []
+    for _ in range(300):
+        n = rng.randrange(0, 320)
+        b = bytes(rng.randrange(256) for _ in range(n))
+        if n > 0 and rng.random() < 0.5:
+            b = bytes([22]) + b[1:]
+        out.append(b)
+    return out
+
+
+# ----------------------------------------------------------------
+# Real ClientHellos, built by OpenSSL through Python's ssl module.
+# ----------------------------------------------------------------
+
+OPENSSL_SETTINGS = [
+    ("TLS 1.2 and 1.3, SNI example.com, ALPN h2 and http/1.1",
+     dict(sni="example.com", alpn=["h2", "http/1.1"])),
+    ("TLS 1.2 and 1.3, SNI example.com", dict(sni="example.com")),
+    ("TLS 1.2 and 1.3, no SNI", dict()),
+    ("TLS 1.3 only, SNI example.com",
+     dict(sni="example.com", min="TLSv1_3")),
+    ("TLS 1.3 only, SNI a.b.example.org, ALPN h2",
+     dict(sni="a.b.example.org", min="TLSv1_3", alpn=["h2"])),
+    ("TLS 1.2 only, SNI example.com",
+     dict(sni="example.com", min="TLSv1_2", max="TLSv1_2")),
+    ("TLS 1.2 only, no SNI, ALPN http/1.1",
+     dict(min="TLSv1_2", max="TLSv1_2", alpn=["http/1.1"])),
+    ("TLS 1.2 and 1.3, SNI xn--bcher-kva.example",
+     dict(sni="xn--bcher-kva.example")),
+    ("TLS 1.2 and 1.3, SNI with a 63-byte label",
+     dict(sni="a" * 63 + ".example")),
+    ("TLS 1.2 and 1.3, cipher list ECDHE+AESGCM",
+     dict(sni="example.com", ciphers="ECDHE+AESGCM")),
+    ("TLS 1.2 and 1.3, group P-256 only",
+     dict(sni="example.com", curve="prime256v1")),
+    ("TLS 1.3 only, post-handshake auth",
+     dict(sni="example.com", min="TLSv1_3", pha=True)),
+]
+
+
+def openssl_hello(kw):
+    """The ClientHello record OpenSSL writes for these settings.
+    Its random and key shares are new on every call."""
+    import ssl
+    ctx = ssl.SSLContext(ssl.PROTOCOL_TLS_CLIENT)
+    ctx.check_hostname = False
+    ctx.verify_mode = ssl.CERT_NONE
+    if "min" in kw:
+        ctx.minimum_version = getattr(ssl.TLSVersion, kw["min"])
+    if "max" in kw:
+        ctx.maximum_version = getattr(ssl.TLSVersion, kw["max"])
+    if "alpn" in kw:
+        ctx.set_alpn_protocols(kw["alpn"])
+    if "ciphers" in kw:
+        ctx.set_ciphers(kw["ciphers"])
+    if "curve" in kw:
+        ctx.set_ecdh_curve(kw["curve"])
+    if kw.get("pha"):
+        ctx.post_handshake_auth = True
+    inc, out = ssl.MemoryBIO(), ssl.MemoryBIO()
+    obj = ctx.wrap_bio(inc, out, server_hostname=kw.get("sni"))
+    try:
+        obj.do_handshake()
+    except ssl.SSLWantReadError:
+        pass
+    return out.read()
+
+
+def openssl_hellos():
+    """Two hellos for each setting: (label, bytes) pairs."""
+    return [(label, openssl_hello(kw))
+            for label, kw in OPENSSL_SETTINGS for _ in range(2)]
+
+
+def openssl_version():
+    import ssl
+    return ssl.OPENSSL_VERSION
+
+
+# ----------------------------------------------------------------
+# The runner.
+# ----------------------------------------------------------------
+
+def run_batch(lines, timeout=120):
+    """Run the tool on request lines; return answer lines."""
+    proc = subprocess.Popen(
+        [str(EXE)], stdin=subprocess.PIPE, stdout=subprocess.PIPE,
+        stderr=subprocess.PIPE)
+    out_lines = []
+    err = []
+
+    def drain():
+        try:
+            data = proc.stdout.read()
+            out_lines.extend(data.decode().splitlines())
+        except Exception:
+            pass
+
+    t = threading.Thread(target=drain, daemon=True)
+    t.start()
+    try:
+        proc.stdin.write(("\n".join(lines) + "\n").encode())
+        proc.stdin.close()
+    except BrokenPipeError:
+        pass
+    t.join(timeout)
+    if t.is_alive():
+        proc.kill()
+        raise TimeoutError("tool did not finish in time")
+    err = proc.stderr.read().decode()
+    if err.strip():
+        raise RuntimeError(f"tool wrote to stderr: {err[:400]}")
+    return out_lines
+
+
+def codes(bs):
+    return ",".join(str(b) for b in bs)
+
+
+def expected_answer(bs):
+    rep = oracle_parse(bs)
+    if rep is None:
+        return "none"
+    return "ok:" + codes(rep)
+
+
+def check_batch(cases, label, failures):
+    """cases: list of byte strings. Returns (run, agreed)."""
+    lines = []
+    for bs in cases:
+        if bs:
+            lines.append("parse " + codes(bs))
+        else:
+            lines.append("parse")
+    answers = []
+    chunk = 400
+    for i in range(0, len(lines), chunk):
+        answers.extend(run_batch(lines[i:i + chunk]))
+    if len(answers) != len(cases):
+        failures.append(
+            f"{label}: got {len(answers)} answers for "
+            f"{len(cases)} cases")
+        return len(cases), 0
+    agreed = 0
+    for bs, got in zip(cases, answers):
+        want = expected_answer(bs)
+        if got == want:
+            agreed += 1
+        elif len(failures) < 25:
+            failures.append(
+                f"{label}: input {codes(bs)[:120]}... "
+                f"tool said {got[:80]}, oracle said {want[:80]}")
+    return len(cases), agreed
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--seed", type=int, default=20261026)
+    ap.add_argument("--count", type=int, default=3200)
+    args = ap.parse_args()
+    rng = random.Random(args.seed)
+
+    env = dict(os.environ)
+    if not any(Path(p, "lake").exists()
+               for p in env.get("PATH", "").split(":")):
+        env["PATH"] = (str(Path.home() / ".elan" / "bin")
+                       + ":" + env.get("PATH", ""))
+    build = subprocess.run(
+        ["lake", "build"], cwd=ROOT, capture_output=True,
+        text=True, timeout=1200, env=env)
+    if build.returncode != 0:
+        print(build.stdout[-2000:])
+        print(build.stderr[-2000:])
+        print("lake build failed", file=sys.stderr)
+        return 1
+
+    failures = []
+    tally = {}
+
+    named = named_cases()
+    agreed_named = 0
+    named_lines = []
+    named_want = []
+    for name, bs, want_ok in named:
+        rep = oracle_parse(bs)
+        oracle_ok = rep is not None
+        if oracle_ok != want_ok:
+            failures.append(
+                f"named case {name}: oracle "
+                f"{'accepts' if oracle_ok else 'rejects'}, "
+                f"the case expects "
+                f"{'accept' if want_ok else 'reject'}")
+        named_lines.append(bs)
+        named_want.append(name)
+    n, a = check_batch(named_lines, "named", failures)
+    tally["named cases"] = (n, a)
+
+    gen = [gen_message(rng) for _ in range(args.count)]
+    n, a = check_batch(gen, "generated", failures)
+    tally["generated messages"] = (n, a)
+    gen_accepted = sum(1 for bs in gen
+                        if oracle_parse(bs) is not None)
+
+    mut = gen_mutations(rng)
+    n, a = check_batch(mut, "mutations", failures)
+    tally["mutations of the full hello"] = (n, a)
+
+    raw = gen_random_raw(rng)
+    n, a = check_batch(raw, "random raw", failures)
+    tally["random raw byte strings"] = (n, a)
+
+    near = gen_near_limit(rng)
+    n, a = check_batch(near, "near the record limit", failures)
+    tally["hellos near the 2^14 record limit"] = (n, a)
+
+    real = openssl_hellos()
+    for label, bs in real:
+        if oracle_parse(bs) != bs:
+            failures.append(f"OpenSSL hello ({label}): the oracle does "
+                            f"not accept it and print it back unchanged")
+    n, a = check_batch([bs for _, bs in real], "OpenSSL hellos",
+                       failures)
+    tally["ClientHellos built by OpenSSL"] = (n, a)
+
+    malformed = ["parse 256", "parse 1,x", "parse 1,,2",
+                 "peek 1,2", "parse -1", "parse 1 2",
+                 "parse 999999999999"]
+    bad_agreed = 0
+    for line in malformed:
+        got = run_batch([line])
+        if got == ["error"]:
+            bad_agreed += 1
+        else:
+            failures.append(
+                f"malformed line {line!r}: got {got}")
+    tally["malformed request lines"] = (len(malformed),
+                                         bad_agreed)
+
+    total = sum(n for n, _ in tally.values())
+    agreed = sum(a for _, a in tally.values())
+
+    lines = []
+    lines.append("# ClientHello slice: test results")
+    lines.append("")
+    lines.append(f"- Oracle: the harness oracle in tests/run_tests.py, "
+                 f"a second reading of SPEC.md in Python "
+                 f"{platform.python_version()}, for every input; and "
+                 f"{openssl_version()} through Python's ssl module, "
+                 f"which built {len(real)} of the inputs as real "
+                 f"ClientHellos that must be accepted and printed "
+                 f"back byte for byte")
+    lines.append(f"- Seed: {args.seed}")
+    lines.append(f"- Inputs: {total}")
+    lines.append(f"- Failures: {len(failures)}")
+    lines.append(f"- Command: python3 tests/run_tests.py "
+                 f"--seed {args.seed} --count {args.count}")
+    lines.append("")
+    lines.append("## Oracles")
+    lines.append("")
+    lines.append("Every verdict is settled by the harness oracle, a "
+                 "Python implementation of the rules in SPEC.md "
+                 "written for these tests. It is a second reading "
+                 "by the same authors, not an independent "
+                 "implementation. The tool must agree with it on "
+                 "every input, and an accepted message must print "
+                 "back to the oracle's canonical form byte for "
+                 "byte.")
+    lines.append("")
+    lines.append("Python's ssl module builds real ClientHellos in "
+                 "memory: a client SSLObject over two MemoryBIOs "
+                 "writes its hello on the first do_handshake(). The "
+                 f"run makes {len(real)} of them with "
+                 f"{openssl_version()}, two under each of "
+                 f"{len(OPENSSL_SETTINGS)} settings (TLS 1.2 only, "
+                 "TLS 1.3 only, both; with and without SNI and "
+                 "ALPN; a cipher list, a single group, "
+                 "post-handshake auth). Each must be accepted and "
+                 "printed back unchanged. Their random bytes and "
+                 "key shares differ from run to run; their count "
+                 "and settings do not. OpenSSL is a source of real "
+                 "accepted inputs here, not a verdict oracle: no "
+                 "TLS stack is asked to judge the malformed inputs, "
+                 "so the verdicts on those rest on the harness "
+                 "oracle alone. The other fixed cases are built by "
+                 "hand from the RFCs.")
+    lines.append("")
+    lines.append("## Counts")
+    lines.append("")
+    lines.append("| part | run | agreed |")
+    lines.append("| --- | --- | --- |")
+    for label, (n, a) in tally.items():
+        lines.append(f"| {label} | {n} | {a} |")
+    lines.append(f"| total | {total} | {agreed} |")
+    lines.append("")
+    lines.append(f"Of the {tally['generated messages'][0]} "
+                 f"generated messages, the oracle accepts "
+                 f"{gen_accepted} and rejects "
+                 f"{tally['generated messages'][0] - gen_accepted}.")
+    lines.append("")
+    lines.append("## Named cases")
+    lines.append("")
+    for name, bs, want_ok in named:
+        lines.append(f"- {name}: "
+                     f"{'accept' if want_ok else 'reject'} "
+                     f"({len(bs)} bytes)")
+    lines.append("")
+    lines.append("## Differences")
+    lines.append("")
+    if failures:
+        lines.append(f"{len(failures)} failure(s):")
+        lines.append("")
+        for f in failures:
+            lines.append(f"- {f}")
+    else:
+        lines.append("No disagreements between the tool and "
+                     "the oracle, and every named case matched "
+                     "its stated expectation.")
+    lines.append("")
+    RESULTS.write_text("\n".join(lines))
+    print(f"run {total}, agreed {agreed}, "
+          f"failures {len(failures)}")
+    for f in failures:
+        print("FAIL:", f)
+    return 0 if not failures else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())