Protobuf wire format: varints, tags and the four wire types, with proofs

.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

.gitignore

@@ -0,0 +1,2 @@
+.lake/
+__pycache__/

Main.lean

@@ -0,0 +1,112 @@
+/-
+  Command line front end, used by the differential tests.
+
+    protowire serve
+
+  answers requests on standard input, one per line:
+
+    decode HEX       prints  OK, then one tab-separated item per field,
+                     NUMBER:KIND:VALUE; or REJECT
+    encode FIELDS    prints  the hex of the encoded message, or INVALID
+                     when a field cannot be written
+
+  KIND is `varint`, `i64`, `len` or `i32`. VALUE is a decimal number of
+  at most 30 digits, or for `len` the bytes in lower case hex (empty for
+  no bytes). FIELDS is NUMBER:KIND:VALUE items separated by commas, or
+  `-` for none. HEX is lower case.
+
+  A malformed request prints `error`: an unknown operation, hex digits
+  that are not lower case or not in pairs, a number of more than 30
+  digits, or a field item that does not parse. A request line may end in
+  LF or CR LF. Each answer is flushed as soon as it is written.
+
+  Every answer comes from the proved functions in `Protobuf/`: `decode`,
+  `encode` and `Field.isValid`. The parsing and printing here are covered
+  by the tests, not by a proof.
+-/
+
+import Protobuf
+
+open Protobuf
+
+def hexValue (c : Char) : Option Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else none
+
+def hexBytes : List Char → Option (List UInt8)
+  | [] => some []
+  | a :: b :: rest => do
+    let hi ← hexValue a
+    let lo ← hexValue b
+    let bs ← hexBytes rest
+    pure ((hi * 16 + lo).toUInt8 :: bs)
+  | [_] => none
+
+def hexDigit (n : Nat) : Char := "0123456789abcdef".toList.getD n '?'
+
+def showHex (bs : List UInt8) : String :=
+  String.ofList (bs.flatMap fun b => [hexDigit (b.toNat / 16), hexDigit (b.toNat % 16)])
+
+/-- A number in plain decimal digits, refused past 30 digits so that a
+    huge request cannot make the conversion slow. -/
+def number (t : String) : Option Nat :=
+  let ds := t.toList
+  if ds.isEmpty || !ds.all Char.isDigit || ds.length > 30 then none else t.toNat?
+
+def showField (f : Field) : String :=
+  let (kind, value) := match f.value with
+    | .varint v => ("varint", toString v)
+    | .i64 v => ("i64", toString v)
+    | .len d => ("len", showHex d)
+    | .i32 v => ("i32", toString v)
+  s!"{f.number}:{kind}:{value}"
+
+def readField (item : String) : Option Field :=
+  match item.splitOn ":" with
+  | [n, kind, v] => do
+    let n ← number n
+    match kind with
+    | "varint" => pure ⟨n, .varint (← number v)⟩
+    | "i64" => pure ⟨n, .i64 (← number v)⟩
+    | "len" => pure ⟨n, .len (← hexBytes v.toList)⟩
+    | "i32" => pure ⟨n, .i32 (← number v)⟩
+    | _ => none
+  | _ => none
+
+/-- The answer to one request line, or `none` when it is malformed. -/
+def request (line : String) : Option String :=
+  match line.splitOn " " with
+  | ["decode", h] => do
+    let bs ← hexBytes h.toList
+    pure <| match decode bs with
+      | some fs => "\t".intercalate ("OK" :: fs.map showField)
+      | none => "REJECT"
+  | ["encode", "-"] => pure (showHex (encode []))
+  | ["encode", items] => do
+    let fs ← (items.splitOn ",").mapM readField
+    pure <| if fs.all Field.isValid then showHex (encode fs) else "INVALID"
+  | _ => 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 (args : List String) : IO UInt32 := do
+  match args with
+  | ["serve"] =>
+    let stdin ← IO.getStdin
+    let stdout ← IO.getStdout
+    repeat
+      let line ← stdin.getLine
+      if line.isEmpty then break
+      stdout.putStrLn ((request (chomp line)).getD "error")
+      stdout.flush
+    return 0
+  | _ =>
+    IO.eprintln "usage: protowire serve"
+    return 2

Proofs.lean

@@ -0,0 +1,7 @@
+/-
+  The proofs, under the names the challenge file gives them. The
+  theorems themselves are in `Proofs/Main.lean`, from the lemmas in the
+  other files.
+-/
+
+import Proofs.Main

Proofs/Fixed.lean

@@ -0,0 +1,105 @@
+/-
+  Fixed-width values: `leValue` and `leBytes` in `Protobuf/Wire.lean`
+  are `Spec.leValue` and `Spec.leBytes`, `Spec.leBytes k n` has `k`
+  bytes, and the two are inverse: reading back `k` bytes of a number
+  below 256^k gives the number, and writing the value of a list of bytes
+  in as many bytes gives the list.
+-/
+
+import Protobuf
+import Spec.Defs
+
+namespace Protobuf.Proofs.Fixed
+
+open Protobuf
+
+/-! ## Cons formulas for the spec -/
+
+theorem sum_map_mul_left (l : List Nat) (g : Nat → Nat) (c : Nat) :
+    (l.map fun i => c * g i).sum = c * (l.map g).sum := by
+  induction l with
+  | nil => simp
+  | cons x xs ih => simp [List.sum_cons, ih, Nat.mul_add]
+
+theorem spec_leValue_nil : Spec.leValue [] = 0 := rfl
+
+theorem spec_leValue_cons (b : UInt8) (bs : List UInt8) :
+    Spec.leValue (b :: bs) = b.toNat + 256 * Spec.leValue bs := by
+  unfold Spec.leValue
+  rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.sum_cons, List.map_map]
+  have : ((fun i => ((b :: bs).getD i 0).toNat * 256 ^ i) ∘ Nat.succ) =
+      fun i => 256 * ((bs.getD i 0).toNat * 256 ^ i) := by
+    funext i
+    simp [Nat.pow_succ', Nat.mul_left_comm]
+  rw [this, sum_map_mul_left]
+  simp
+
+theorem spec_leBytes_zero (n : Nat) : Spec.leBytes 0 n = [] := rfl
+
+theorem spec_leBytes_succ (k n : Nat) :
+    Spec.leBytes (k + 1) n = (n % 256).toUInt8 :: Spec.leBytes k (n / 256) := by
+  unfold Spec.leBytes
+  rw [List.range_succ_eq_map, List.map_cons, List.map_map]
+  congr 1
+  · simp
+  · apply List.map_congr_left
+    intro i _
+    simp [Nat.pow_succ', Nat.div_div_eq_div_mul]
+
+/-! ## The code is the spec -/
+
+theorem leValue_cons (b : UInt8) (bs : List UInt8) :
+    leValue (b :: bs) = b.toNat + 256 * leValue bs := rfl
+
+theorem leValue_eq (bs : List UInt8) : leValue bs = Spec.leValue bs := by
+  induction bs with
+  | nil => rfl
+  | cons b bs ih => rw [leValue_cons, spec_leValue_cons, ih]
+
+theorem leBytes_eq (k n : Nat) : leBytes k n = Spec.leBytes k n := by
+  induction k generalizing n with
+  | zero => rfl
+  | succ k ih => rw [spec_leBytes_succ, ← ih]; rfl
+
+/-! ## Length, bounds and inverses -/
+
+theorem leBytes_length (k n : Nat) : (Spec.leBytes k n).length = k := by
+  simp [Spec.leBytes]
+
+theorem toNat_lt (b : UInt8) : b.toNat < 256 := UInt8.toNat_lt b
+
+theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Spec.leValue (Spec.leBytes k n) = n := by
+  induction k generalizing n with
+  | zero =>
+    simp at h
+    subst h
+    rfl
+  | succ k ih =>
+    have hd : n / 256 < 256 ^ k := by
+      rw [Nat.div_lt_iff_lt_mul (by decide), ← Nat.pow_succ]
+      exact h
+    rw [spec_leBytes_succ, spec_leValue_cons, ih _ hd]
+    have : (n % 256).toUInt8.toNat = n % 256 := by simp
+    rw [this]
+    exact Nat.mod_add_div n 256
+
+theorem leValue_lt (bs : List UInt8) : Spec.leValue bs < 256 ^ bs.length := by
+  induction bs with
+  | nil => simp [spec_leValue_nil]
+  | cons b bs ih =>
+    rw [spec_leValue_cons, List.length_cons, Nat.pow_succ']
+    have := toNat_lt b
+    omega
+
+theorem leBytes_leValue (bs : List UInt8) : Spec.leBytes bs.length (Spec.leValue bs) = bs := by
+  induction bs with
+  | nil => rfl
+  | cons b bs ih =>
+    have hb := toNat_lt b
+    rw [List.length_cons, spec_leBytes_succ, spec_leValue_cons]
+    have hm : (b.toNat + 256 * Spec.leValue bs) % 256 = b.toNat := by omega
+    have hd : (b.toNat + 256 * Spec.leValue bs) / 256 = Spec.leValue bs := by omega
+    rw [hm, hd, ih]
+    simp
+
+end Protobuf.Proofs.Fixed

Proofs/Main.lean

@@ -0,0 +1,87 @@
+/-
+  The statements of `Spec.lean`, under the same names, from the lemmas
+  in the other files of `Proofs/`. The test vectors are checked by
+  evaluation.
+-/
+
+import Protobuf
+import Spec.Defs
+import Proofs.Varint
+import Proofs.Message
+
+open Protobuf
+open Protobuf.Proofs
+
+theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n :=
+  Protobuf.Proofs.Varint.encode_eq n h
+
+theorem Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v :=
+  Protobuf.Proofs.Varint.decode_iff bs v rest
+
+theorem Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
+    Varint.decode (Varint.encode n ++ rest) = some (n, rest) :=
+  Protobuf.Proofs.Varint.decode_encode n rest h
+
+theorem Spec.isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f :=
+  Protobuf.Proofs.Message.isValid_iff f
+
+theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    Protobuf.encode fs = Spec.encode fs :=
+  Protobuf.Proofs.Message.encode_eq fs h
+
+theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) :
+    decode bs = some fs ↔ Spec.Message bs fs :=
+  Protobuf.Proofs.Message.decode_iff bs fs
+
+theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+    decode (Protobuf.encode fs) = some fs :=
+  Protobuf.Proofs.Message.decode_encode fs h
+
+theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
+    ∀ f ∈ fs, Spec.ValidField f :=
+  Protobuf.Proofs.Message.decode_valid bs fs h
+
+theorem Spec.guide_vectors :
+    Varint.encode 1 = [0x01] ∧
+    Varint.encode 150 = [0x96, 0x01] ∧
+    Varint.encode (2 ^ 64 - 2) = [0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
+    decode [0x08, 0x96, 0x01] = some [⟨1, .varint 150⟩] ∧
+    decode [0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] =
+      some [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] ∧
+    decode [0x1a, 0x03, 0x08, 0x96, 0x01] = some [⟨3, .len [0x08, 0x96, 0x01]⟩] ∧
+    decode [0x22, 0x05, 0x68, 0x65, 0x6c, 0x6c, 0x6f, 0x2a, 0x03, 0x01, 0x02, 0x03] =
+      some [⟨4, .len [0x68, 0x65, 0x6c, 0x6c, 0x6f]⟩, ⟨5, .len [0x01, 0x02, 0x03]⟩] ∧
+    Protobuf.encode [⟨1, .varint 150⟩, ⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] =
+      [0x08, 0x96, 0x01, 0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by
+  decide
+
+theorem Spec.edge_vectors :
+    Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
+    decode [0x0d, 0x01, 0x02, 0x03, 0x04] = some [⟨1, .i32 0x04030201⟩] ∧
+    decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08] =
+      some [⟨1, .i64 0x0807060504030201⟩] ∧
+    decode [0x08, 0x80, 0x00] = some [⟨1, .varint 0⟩] ∧
+    decode [0x08, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x7f] =
+      some [⟨1, .varint (2 ^ 64 - 1)⟩] ∧
+    decode [0xf8, 0xff, 0xff, 0xff, 0x0f, 0x01] = some [⟨2 ^ 29 - 1, .varint 1⟩] ∧
+    decode [] = some [] := by
+  decide
+
+theorem Spec.reject_vectors :
+    decode [0x08] = none ∧
+    decode [0x08, 0x80] = none ∧
+    decode [0x08, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x00] = none ∧
+    decode [0x00, 0x00] = none ∧
+    decode [0x0a, 0x04, 0x61, 0x62] = none ∧
+    decode [0x0d, 0x01, 0x02, 0x03] = none ∧
+    decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07] = none ∧
+    decode [0x0b, 0x0c] = none ∧
+    decode [0x0c] = none ∧
+    decode [0x0e, 0x00] = none ∧
+    decode [0x0f, 0x00] = none ∧
+    decode [0xf8, 0xff, 0xff, 0xff, 0x1f, 0x01] = none ∧
+    decode [0x80, 0x80, 0x80, 0x80, 0x10, 0x01] = none ∧
+    decode [0x88, 0x80, 0x80, 0x80, 0x80, 0x00, 0x01] = none ∧
+    decode [0x0a, 0x81, 0x80, 0x80, 0x80, 0x80, 0x00, 0x61] = none := by
+  decide