From 2eeb2ea949339af9335b5f201d5c5e83a6bf8f75 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 09:23:50 +0000 Subject: [PATCH 1/4] Add the Protobuf wire format codec, with proofs The first slice of the plan in issue #1: varints, field tags and the four wire types VARINT, I64, LEN and I32, with messages as lists of raw fields. Eleven statements in Spec.lean are proved in Proofs/ and pass lake comparator --paranoid: the decoder accepts exactly the byte strings the encoding guide's rules allow, the encoder writes what the guide describes, and decoding an encoding gives the fields back. Differential tests against upb and the C++ parser behind protoc --decode_raw agree on 200,000 inputs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- .github/workflows/bar.yml | 21 ++ .gitignore | 2 + Main.lean | 109 +++++++ Proofs.lean | 7 + Proofs/Fixed.lean | 105 +++++++ Proofs/Main.lean | 84 ++++++ Proofs/Message.lean | 340 ++++++++++++++++++++++ Proofs/Varint.lean | 288 +++++++++++++++++++ Protobuf.lean | 8 + Protobuf/Types.lean | 32 +++ Protobuf/Varint.lean | 38 +++ Protobuf/Wire.lean | 97 +++++++ README.md | 95 ++++++- SPEC.md | 96 +++++++ Spec.lean | 113 ++++++++ Spec/Defs.lean | 148 ++++++++++ bar.toml | 35 +++ comparator.json | 10 + lake-manifest.json | 6 + lakefile.toml | 16 ++ lean-toolchain | 1 + tests/TEST-RESULTS.md | 15 + tests/run_tests.py | 577 ++++++++++++++++++++++++++++++++++++++ 23 files changed, 2241 insertions(+), 2 deletions(-) create mode 100644 .github/workflows/bar.yml create mode 100644 .gitignore create mode 100644 Main.lean create mode 100644 Proofs.lean create mode 100644 Proofs/Fixed.lean create mode 100644 Proofs/Main.lean create mode 100644 Proofs/Message.lean create mode 100644 Proofs/Varint.lean create mode 100644 Protobuf.lean create mode 100644 Protobuf/Types.lean create mode 100644 Protobuf/Varint.lean create mode 100644 Protobuf/Wire.lean create mode 100644 SPEC.md create mode 100644 Spec.lean create mode 100644 Spec/Defs.lean create mode 100644 bar.toml create mode 100644 comparator.json create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain create mode 100644 tests/TEST-RESULTS.md create mode 100644 tests/run_tests.py 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 new file mode 100644 index 0000000..ae73679 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.lake/ +__pycache__/ diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..737b356 --- /dev/null +++ b/Main.lean @@ -0,0 +1,109 @@ +/- + 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, + 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. + + A malformed request prints `error`: an unknown operation, hex digits + that are not in pairs, or a field item that does not parse. A request + line may end in LF or CR LF. + + 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") + return 0 + | _ => + IO.eprintln "usage: protowire serve" + return 2 diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..a0c5328 --- /dev/null +++ b/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 diff --git a/Proofs/Fixed.lean b/Proofs/Fixed.lean new file mode 100644 index 0000000..6a186d8 --- /dev/null +++ b/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 diff --git a/Proofs/Main.lean b/Proofs/Main.lean new file mode 100644 index 0000000..ab34a20 --- /dev/null +++ b/Proofs/Main.lean @@ -0,0 +1,84 @@ +/- + 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 - 1) = [0xff, 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, 0x06, 0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05] = + some [⟨4, .len [0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05]⟩] ∧ + 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 : + 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 [0x0e, 0x00] = none ∧ + decode [0x0f, 0x00] = none ∧ + decode [0xf8, 0xff, 0xff, 0xff, 0x1f, 0x01] = none ∧ + decode [0x88, 0x80, 0x80, 0x80, 0x80, 0x00, 0x01] = none ∧ + decode [0x0a, 0x81, 0x80, 0x80, 0x80, 0x80, 0x00, 0x61] = none := by + decide diff --git a/Proofs/Message.lean b/Proofs/Message.lean new file mode 100644 index 0000000..3b5aea3 --- /dev/null +++ b/Proofs/Message.lean @@ -0,0 +1,340 @@ +/- + Fields and messages against the spec: `Field.isValid` decides + `Spec.ValidField`, the encoder writes `Spec.encode`, `decodeField` + reads exactly one record (`Spec.FieldBytes`) from the front of its + input, `decode` reads exactly a `Spec.Message`, decoding what the + encoder wrote gives the fields back, and every field the decoder + returns is valid. +-/ + +import Protobuf +import Spec.Defs +import Proofs.Varint +import Proofs.Fixed + +namespace Protobuf.Proofs.Message + +open Protobuf + +/-! ## Validity -/ + +theorem isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f := by + obtain ⟨n, v⟩ := f + cases v <;> simp [Field.isValid, Spec.ValidField, and_assoc] + +/-! ## The encoder -/ + +theorem field_encode_eq (f : Field) (h : Spec.ValidField f) : f.encode = Spec.fieldBytes f := by + obtain ⟨n, v⟩ := f + obtain ⟨h1, h2, h3⟩ := h + have h2 : n < 2 ^ 29 := h2 + have hn : ∀ w, w < 8 → n * 8 + w < 2 ^ 64 := by intro w hw; omega + cases v with + | varint v => + have h3 : v < 2 ^ 64 := h3 + show Varint.encode (n * 8 + 0) ++ Varint.encode v = Spec.varint (n * 8 + 0) ++ Spec.varint v + rw [Proofs.Varint.encode_eq _ (hn 0 (by decide)), Proofs.Varint.encode_eq _ h3] + | i64 v => + show Varint.encode (n * 8 + 1) ++ leBytes 8 v = Spec.varint (n * 8 + 1) ++ Spec.leBytes 8 v + rw [Proofs.Varint.encode_eq _ (hn 1 (by decide)), Proofs.Fixed.leBytes_eq] + | len d => + have h3 : d.length < 2 ^ 31 := h3 + show Varint.encode (n * 8 + 2) ++ (Varint.encode d.length ++ d) = + Spec.varint (n * 8 + 2) ++ Spec.varint d.length ++ d + rw [Proofs.Varint.encode_eq _ (hn 2 (by decide)), Proofs.Varint.encode_eq _ (by omega), + List.append_assoc] + | i32 v => + show Varint.encode (n * 8 + 5) ++ leBytes 4 v = Spec.varint (n * 8 + 5) ++ Spec.leBytes 4 v + rw [Proofs.Varint.encode_eq _ (hn 5 (by decide)), Proofs.Fixed.leBytes_eq] + +theorem encode_cons (f : Field) (fs : List Field) : encode (f :: fs) = f.encode ++ encode fs := by + simp [encode] + +theorem spec_encode_cons (f : Field) (fs : List Field) : + Spec.encode (f :: fs) = Spec.fieldBytes f ++ Spec.encode fs := by + simp [Spec.encode] + +theorem encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : encode fs = Spec.encode fs := by + induction fs with + | nil => rfl + | cons f fs ih => + rw [encode_cons, spec_encode_cons, field_encode_eq f (h f (by simp)), + ih (fun g hg => h g (by simp [hg]))] + +/-! ## One record -/ + +theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) : + decodeField bs = some (f, rest) ↔ + ∃ tag payload, bs = tag ++ payload ++ rest ∧ Spec.FieldBytes tag payload f := by + constructor + · intro h + unfold decodeField at h + cases ht : Varint.decodeAux 5 bs with + | none => rw [ht] at h; exact absurd h (by simp) + | some p => + obtain ⟨t, r⟩ := p + obtain ⟨tag, hbs, hshape, hg⟩ := (Proofs.Varint.decodeAux_iff 5 bs t r).mp ht + rw [ht] at h + simp only at h + by_cases hc : 2 ^ 32 ≤ t ∨ t / 8 = 0 + · simp only [hc, ↓reduceIte] at h + exact absurd h (by simp) + · simp only [hc, ↓reduceIte] at h + have ht32 : t < 2 ^ 32 := by omega + have hn : 1 ≤ t / 8 := by omega + subst hbs + subst hg + split at h + · rename_i hw + split at h + · rename_i v r' hv + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + obtain ⟨pre, hr, hiv⟩ := (Proofs.Varint.decode_iff r v r').mp hv + refine ⟨tag, pre, by rw [hr, List.append_assoc], hshape, ht32, rfl, hn, ?_⟩ + rw [hw] + exact hiv + · exact absurd h (by simp) + · rename_i hw + by_cases hl : r.length < 8 + · simp only [hl, ↓reduceIte] at h + exact absurd h (by simp) + · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨tag, r.take 8, by rw [List.append_assoc, List.take_append_drop], hshape, ht32, + rfl, hn, ?_⟩ + rw [hw] + exact ⟨by simp; omega, Proofs.Fixed.leValue_eq _⟩ + · rename_i hw + split at h + · rename_i len r2 hv + obtain ⟨pre, hr, hps, hpv⟩ := (Proofs.Varint.decodeAux_iff 5 r len r2).mp hv + by_cases hl : 2 ^ 31 ≤ len ∨ r2.length < len + · simp only [hl, ↓reduceIte] at h + exact absurd h (by simp) + · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + have hlen : (r2.take len).length = len := by simp; omega + refine ⟨tag, pre ++ r2.take len, ?_, hshape, ht32, rfl, hn, ?_⟩ + · rw [hr, List.append_assoc, List.append_assoc, List.take_append_drop] + · rw [hw] + exact ⟨pre, rfl, hps, by rw [hlen, hpv], by rw [hlen]; omega⟩ + · exact absurd h (by simp) + · rename_i hw + by_cases hl : r.length < 4 + · simp only [hl, ↓reduceIte] at h + exact absurd h (by simp) + · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨tag, r.take 4, by rw [List.append_assoc, List.take_append_drop], hshape, ht32, + rfl, hn, ?_⟩ + rw [hw] + exact ⟨by simp; omega, Proofs.Fixed.leValue_eq _⟩ + · exact absurd h (by simp) + · rintro ⟨tag, payload, rfl, hshape, ht32, hnum, hn, hm⟩ + obtain ⟨num, val⟩ := f + have hd : Varint.decodeAux 5 (tag ++ payload ++ rest) = + some (Spec.groupsValue tag, payload ++ rest) := + (Proofs.Varint.decodeAux_iff 5 _ _ _).mpr ⟨tag, List.append_assoc _ _ _, hshape, rfl⟩ + have hc : ¬(2 ^ 32 ≤ Spec.groupsValue tag ∨ Spec.groupsValue tag / 8 = 0) := by + simp only at hnum hn + omega + have hnum' : num = Spec.groupsValue tag / 8 := hnum + unfold decodeField + rw [hd] + simp only [hc, ↓reduceIte] + simp only at hm + split at hm + · rename_i v hw + rw [hw] + simp only + rw [(Proofs.Varint.decode_iff _ v rest).mpr ⟨payload, rfl, hm⟩, hnum'] + · rename_i v hw + obtain ⟨hl, rfl⟩ := hm + have hl' : ¬(payload ++ rest).length < 8 := by simp; omega + rw [hw] + simp only [hl', ↓reduceIte] + rw [List.take_left' hl, List.drop_left' hl, Proofs.Fixed.leValue_eq, hnum'] + · rename_i d hw + obtain ⟨pre, rfl, hps, hpv, hdl⟩ := hm + have hd2 : Varint.decodeAux 5 (pre ++ d ++ rest) = some (d.length, d ++ rest) := + (Proofs.Varint.decodeAux_iff 5 _ _ _).mpr ⟨pre, List.append_assoc _ _ _, hps, hpv.symm⟩ + have hl' : ¬(2 ^ 31 ≤ d.length ∨ (d ++ rest).length < d.length) := by simp; omega + rw [hw] + simp only + rw [hd2] + simp only [hl', ↓reduceIte] + rw [List.take_left' rfl, List.drop_left' rfl, hnum'] + · rename_i v hw + obtain ⟨hl, rfl⟩ := hm + have hl' : ¬(payload ++ rest).length < 4 := by simp; omega + rw [hw] + simp only [hl', ↓reduceIte] + rw [List.take_left' hl, List.drop_left' hl, Proofs.Fixed.leValue_eq, hnum'] + · exact hm.elim + +/-! ## Messages -/ + +/-- Whatever `decodeAux` returns, with any fuel, is a message. -/ +theorem decodeAux_sound (fuel : Nat) : + ∀ bs fs, decodeAux fuel bs = some fs → Spec.Message bs fs := by + induction fuel with + | zero => + intro bs fs h + cases bs with + | nil => + simp only [decodeAux, Option.some.injEq] at h + subst h + exact .nil + | cons b bs => simp [decodeAux] at h + | succ fuel ih => + intro bs fs h + cases bs with + | nil => + simp only [decodeAux, Option.some.injEq] at h + subst h + exact .nil + | cons b bs => + simp only [decodeAux] at h + split at h + · rename_i f rest hf + split at h + · rename_i fs' hfs + simp only [Option.some.injEq] at h + subst h + obtain ⟨tag, payload, hbs, hfb⟩ := (decodeField_iff _ f rest).mp hf + rw [hbs] + exact .cons hfb (ih rest fs' hfs) + · exact absurd h (by simp) + · exact absurd h (by simp) + +/-- A message is read whole by `decodeAux` with fuel at least its length: + each record takes at least one byte, since its tag does. -/ +theorem decodeAux_complete {bs : List UInt8} {fs : List Field} (h : Spec.Message bs fs) : + ∀ fuel, bs.length ≤ fuel → decodeAux fuel bs = some fs := by + induction h with + | nil => intro fuel _; cases fuel <;> rfl + | @cons tag payload rest f fs hfb _ ih => + intro fuel hlen + obtain ⟨c, tag', rfl⟩ : ∃ c tag', tag = c :: tag' := by + cases tag with + | nil => exact absurd rfl hfb.1.1 + | cons c tag' => exact ⟨c, tag', rfl⟩ + simp only [List.cons_append, List.length_cons, List.length_append] at hlen ⊢ + obtain ⟨fuel', rfl⟩ : ∃ k, fuel = k + 1 := ⟨fuel - 1, by omega⟩ + have hd : decodeField (c :: (tag' ++ payload ++ rest)) = some (f, rest) := + (decodeField_iff _ f rest).mpr ⟨c :: tag', payload, rfl, hfb⟩ + simp only [decodeAux, hd] + rw [ih fuel' (by omega)] + +theorem decode_iff (bs : List UInt8) (fs : List Field) : decode bs = some fs ↔ Spec.Message bs fs := + ⟨decodeAux_sound bs.length bs fs, fun h => decodeAux_complete h bs.length (Nat.le_refl _)⟩ + +/-! ## Decoded fields are valid -/ + +theorem fieldBytes_valid {tag payload : List UInt8} {f : Field} (h : Spec.FieldBytes tag payload f) : + Spec.ValidField f := by + obtain ⟨num, val⟩ := f + obtain ⟨_, ht, hnum, hn, hm⟩ := h + simp only at hnum hn hm + refine ⟨hn, show num < 2 ^ 29 by omega, ?_⟩ + simp only + split at hm + · obtain ⟨_, rfl⟩ := hm + exact Nat.mod_lt _ (by decide) + · obtain ⟨hl, rfl⟩ := hm + have := Proofs.Fixed.leValue_lt payload + rw [hl] at this + exact this + · obtain ⟨_, _, _, _, hdl⟩ := hm + exact hdl + · obtain ⟨hl, rfl⟩ := hm + have := Proofs.Fixed.leValue_lt payload + rw [hl] at this + exact this + · exact hm.elim + +theorem message_valid {bs : List UInt8} {fs : List Field} (h : Spec.Message bs fs) : + ∀ f ∈ fs, Spec.ValidField f := by + induction h with + | nil => simp + | cons hfb _ ih => + intro g hg + rcases List.mem_cons.mp hg with rfl | hg + · exact fieldBytes_valid hfb + · exact ih g hg + +theorem decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) : + ∀ f ∈ fs, Spec.ValidField f := + message_valid ((decode_iff bs fs).mp h) + +/-! ## Round trip -/ + +/-- The shortest varint of a valid tag has at most five bytes. -/ +theorem tag_bytes (n w : Nat) (hn : n < 2 ^ 29) (hw : w < 8) : + Spec.VarintShape 5 (Spec.varint (n * 8 + w)) ∧ Spec.groupsValue (Spec.varint (n * 8 + w)) = n * 8 + w := by + have hs := Proofs.Varint.varint_shape (n * 8 + w) + have h5 : (2 : Nat) ^ 32 ≤ 128 ^ 5 := by decide + exact ⟨Proofs.Varint.shape_mono hs.1 (Proofs.Varint.varint_length _ 5 (by decide) (by omega)), hs.2⟩ + +/-- The bytes the encoder writes for a valid field are one record. -/ +theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) : + ∃ tag payload, Spec.fieldBytes f = tag ++ payload ∧ Spec.FieldBytes tag payload f := by + obtain ⟨n, val⟩ := f + obtain ⟨h1, h2, h3⟩ := h + have h1 : 1 ≤ n := h1 + have h2 : n < 2 ^ 29 := h2 + cases val with + | varint v => + have h3 : v < 2 ^ 64 := h3 + obtain ⟨hs, hg⟩ := tag_bytes n 0 h2 (by decide) + refine ⟨Spec.varint (n * 8 + 0), Spec.varint v, rfl, hs, by rw [hg]; omega, + show n = _ by rw [hg]; omega, h1, ?_⟩ + rw [hg, show (n * 8 + 0) % 8 = 0 by omega] + have hv := Proofs.Varint.varint_shape v + exact ⟨Proofs.Varint.shape_mono hv.1 + (Proofs.Varint.varint_length v 10 (by decide) (Nat.lt_of_lt_of_le h3 Proofs.Varint.two_pow_le)), + by rw [hv.2, Nat.mod_eq_of_lt h3]⟩ + | i64 v => + have h3 : v < 2 ^ 64 := h3 + obtain ⟨hs, hg⟩ := tag_bytes n 1 h2 (by decide) + refine ⟨Spec.varint (n * 8 + 1), Spec.leBytes 8 v, rfl, hs, by rw [hg]; omega, + show n = _ by rw [hg]; omega, h1, ?_⟩ + rw [hg, show (n * 8 + 1) % 8 = 1 by omega] + exact ⟨Proofs.Fixed.leBytes_length 8 v, + (Proofs.Fixed.leValue_leBytes 8 v (by simpa using h3)).symm⟩ + | len d => + have h3 : d.length < 2 ^ 31 := h3 + obtain ⟨hs, hg⟩ := tag_bytes n 2 h2 (by decide) + refine ⟨Spec.varint (n * 8 + 2), Spec.varint d.length ++ d, List.append_assoc _ _ _, hs, + by rw [hg]; omega, show n = _ by rw [hg]; omega, h1, ?_⟩ + rw [hg, show (n * 8 + 2) % 8 = 2 by omega] + have hv := Proofs.Varint.varint_shape d.length + have h5 : (2 : Nat) ^ 31 ≤ 128 ^ 5 := by decide + exact ⟨Spec.varint d.length, rfl, + Proofs.Varint.shape_mono hv.1 (Proofs.Varint.varint_length _ 5 (by decide) (by omega)), + hv.2, h3⟩ + | i32 v => + have h3 : v < 2 ^ 32 := h3 + obtain ⟨hs, hg⟩ := tag_bytes n 5 h2 (by decide) + refine ⟨Spec.varint (n * 8 + 5), Spec.leBytes 4 v, rfl, hs, by rw [hg]; omega, + show n = _ by rw [hg]; omega, h1, ?_⟩ + rw [hg, show (n * 8 + 5) % 8 = 5 by omega] + exact ⟨Proofs.Fixed.leBytes_length 4 v, + (Proofs.Fixed.leValue_leBytes 4 v (by simpa using h3)).symm⟩ + +theorem encode_message (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : + Spec.Message (Spec.encode fs) fs := by + induction fs with + | nil => exact .nil + | cons f fs ih => + obtain ⟨tag, payload, he, hfb⟩ := fieldBytes_split f (h f (by simp)) + rw [spec_encode_cons, he] + exact .cons hfb (ih fun g hg => h g (by simp [hg])) + +theorem decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : + decode (encode fs) = some fs := by + rw [encode_eq fs h] + exact (decode_iff _ _).mpr (encode_message fs h) + +end Protobuf.Proofs.Message diff --git a/Proofs/Varint.lean b/Proofs/Varint.lean new file mode 100644 index 0000000..19655d5 --- /dev/null +++ b/Proofs/Varint.lean @@ -0,0 +1,288 @@ +/- + The varint encoder and decoder of `Protobuf/Varint.lean` against the + spec: `encode` writes `Spec.varint`, `decodeAux k` reads exactly one + varint of at most `k` bytes (shape `Spec.VarintShape k`, value + `Spec.groupsValue`), `decode` reads exactly a `Spec.IsVarint`, and + decoding what the encoder wrote gives the number back. +-/ + +import Protobuf +import Spec.Defs + +namespace Protobuf.Proofs.Varint + +open Protobuf + +/-! ## Groups and shapes, one byte at a time -/ + +theorem sum_map_mul (c : Nat) (g : Nat → Nat) (l : List Nat) : + (l.map fun i => c * g i).sum = c * (l.map g).sum := by + induction l with + | nil => simp + | cons a l ih => simp [List.sum_cons, ih, Nat.mul_add] + +theorem groupsValue_nil : Spec.groupsValue [] = 0 := rfl + +theorem groupsValue_cons (b : UInt8) (bs : List UInt8) : + Spec.groupsValue (b :: bs) = b.toNat % 128 + 128 * Spec.groupsValue bs := by + unfold Spec.groupsValue + rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.sum_cons, List.map_map, + ← sum_map_mul] + congr 1 + · simp + · congr 1 + apply List.map_congr_left + intro i _ + simp only [Function.comp, Nat.succ_eq_add_one, List.getD_cons_succ, Nat.pow_succ] + rw [Nat.mul_comm (128 ^ i) 128, Nat.mul_left_comm] + +theorem shape_zero (bs : List UInt8) : ¬ Spec.VarintShape 0 bs := by + intro ⟨h1, h2, _⟩ + exact h1 (List.eq_nil_of_length_eq_zero (Nat.le_zero.mp h2)) + +theorem shape_nil (k : Nat) : ¬ Spec.VarintShape k [] := fun h => h.1 rfl + +theorem shape_cons (k : Nat) (b : UInt8) (bs : List UInt8) : + Spec.VarintShape (k + 1) (b :: bs) ↔ + (b.toNat < 128 ∧ bs = []) ∨ (128 ≤ b.toNat ∧ Spec.VarintShape k bs) := by + cases bs with + | nil => + simp [Spec.VarintShape] + | cons c cs => + simp [Spec.VarintShape, List.dropLast_cons_cons, List.getLast?_cons_cons] + exact ⟨fun ⟨h1, ⟨h2, h3⟩, h4⟩ => ⟨h2, h1, h3, h4⟩, fun ⟨h2, h1, h3, h4⟩ => ⟨h1, ⟨h2, h3⟩, h4⟩⟩ + + +/-! ## The decoder -/ + +/-- The right-hand side of `decodeAux_iff` at `k + 1`, one byte at a time. -/ +theorem split_cons (k : Nat) (b : UInt8) (bs : List UInt8) (v : Nat) (rest : List UInt8) : + (∃ pre, b :: bs = pre ++ rest ∧ Spec.VarintShape (k + 1) pre ∧ v = Spec.groupsValue pre) ↔ + (b.toNat < 128 ∧ bs = rest ∧ v = b.toNat) ∨ + (128 ≤ b.toNat ∧ ∃ v', (∃ pre, bs = pre ++ rest ∧ Spec.VarintShape k pre ∧ + v' = Spec.groupsValue pre) ∧ v = b.toNat % 128 + 128 * v') := by + constructor + · rintro ⟨pre, h, hs, hv⟩ + cases pre with + | nil => exact absurd hs (shape_nil _) + | cons c pre => + simp only [List.cons_append, List.cons.injEq] at h + obtain ⟨hbc, rfl⟩ := h + rw [← hbc] at hs hv + rcases (shape_cons k b pre).mp hs with ⟨hc, rfl⟩ | ⟨hc, hs'⟩ + · left + refine ⟨hc, by simp, ?_⟩ + rw [hv, groupsValue_cons, groupsValue_nil] + omega + · right + exact ⟨hc, _, ⟨pre, rfl, hs', rfl⟩, by rw [hv, groupsValue_cons]⟩ + · rintro (⟨hc, rfl, rfl⟩ | ⟨hc, v', ⟨pre, rfl, hs, rfl⟩, rfl⟩) + · refine ⟨[b], rfl, (shape_cons k b []).mpr (Or.inl ⟨hc, rfl⟩), ?_⟩ + rw [groupsValue_cons, groupsValue_nil] + omega + · exact ⟨b :: pre, rfl, (shape_cons k b pre).mpr (Or.inr ⟨hc, hs⟩), by rw [groupsValue_cons]⟩ + +theorem decodeAux_iff (k : Nat) (bs : List UInt8) (v : Nat) (rest : List UInt8) : + Varint.decodeAux k bs = some (v, rest) ↔ + ∃ pre, bs = pre ++ rest ∧ Spec.VarintShape k pre ∧ v = Spec.groupsValue pre := by + induction k generalizing bs v with + | zero => + simp only [Varint.decodeAux, reduceCtorEq, false_iff, not_exists, not_and] + intro pre _ h + exact absurd h (shape_zero pre) + | succ k ih => + cases bs with + | nil => + simp only [Varint.decodeAux, reduceCtorEq, false_iff, not_exists, not_and] + intro pre h hs _ + have : pre = [] := (List.append_eq_nil_iff.mp h.symm).1 + subst this + exact shape_nil _ hs + | cons b bs => + have hb := UInt8.toNat_lt b + rw [split_cons] + simp only [← ih] + simp only [Varint.decodeAux] + by_cases hc : b.toNat < 128 + · have hc' : ¬ 128 ≤ b.toNat := by omega + simp only [hc, hc', ite_true, false_and, or_false, Option.some.injEq, Prod.mk.injEq, + true_and] + exact ⟨fun ⟨h1, h2⟩ => ⟨h2, h1.symm⟩, fun ⟨h1, h2⟩ => ⟨h2.symm, h1⟩⟩ + · cases h : Varint.decodeAux k bs with + | none => simp [hc] + | some p => + obtain ⟨v0, r0⟩ := p + have hc' : 128 ≤ b.toNat := by omega + simp only [hc, hc', ite_false, Option.some.injEq, Prod.mk.injEq, true_and, false_and, + false_or] + constructor + · rintro ⟨h1, h2⟩ + exact ⟨v0, ⟨rfl, h2⟩, by omega⟩ + · rintro ⟨v', ⟨rfl, h2⟩, h3⟩ + exact ⟨by omega, h2⟩ + + +theorem decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) : + Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v := by + unfold Varint.decode + cases h : Varint.decodeAux 10 bs with + | none => + simp only [reduceCtorEq, false_iff, not_exists, not_and] + intro pre hbs ⟨hs, _⟩ + have h2 := (decodeAux_iff 10 bs _ rest).mpr ⟨pre, hbs, hs, rfl⟩ + rw [h] at h2 + exact absurd h2 (by simp) + | some p => + obtain ⟨v0, r0⟩ := p + obtain ⟨pre0, hbs0, hs0, hv0⟩ := (decodeAux_iff 10 bs v0 r0).mp h + simp only [Option.some.injEq, Prod.mk.injEq] + constructor + · rintro ⟨rfl, rfl⟩ + exact ⟨pre0, hbs0, hs0, by rw [hv0]⟩ + · rintro ⟨pre, hbs, hs, hv⟩ + have h2 := (decodeAux_iff 10 bs _ rest).mpr ⟨pre, hbs, hs, rfl⟩ + rw [h] at h2 + simp only [Option.some.injEq, Prod.mk.injEq] at h2 + exact ⟨by rw [hv, h2.1], h2.2⟩ + +/-! ## The shortest varint -/ + +theorem toUInt8_toNat_of_lt (n : Nat) (h : n < 256) : n.toUInt8.toNat = n := by + simp + omega + +theorem varintAux_succ (f n : Nat) : + Spec.varintAux (f + 1) n = + if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Spec.varintAux f (n / 128) := + rfl + +theorem div_lt (n f : Nat) (h : n < 128 ^ (f + 1)) : n / 128 < 128 ^ f := + (Nat.div_lt_iff_lt_mul (by decide)).mpr (by rw [← Nat.pow_succ]; exact h) + +theorem lt_pow (n : Nat) : n < 128 ^ (n + 1) := + Nat.lt_of_lt_of_le (Nat.lt_pow_self (by decide)) (Nat.pow_le_pow_right (by decide) (by omega)) + +theorem single_shape (n : Nat) (h : n < 128) : + Spec.VarintShape [n.toUInt8].length [n.toUInt8] ∧ Spec.groupsValue [n.toUInt8] = n := by + have h1 : n.toUInt8.toNat = n := toUInt8_toNat_of_lt n (by omega) + refine ⟨(shape_cons 0 _ []).mpr (Or.inl ⟨by omega, rfl⟩), ?_⟩ + rw [groupsValue_cons, groupsValue_nil, h1] + omega + +theorem cons_shape (n : Nat) (rest : List UInt8) + (hr : Spec.VarintShape rest.length rest ∧ Spec.groupsValue rest = n / 128) : + Spec.VarintShape ((n % 128 + 128).toUInt8 :: rest).length ((n % 128 + 128).toUInt8 :: rest) ∧ + Spec.groupsValue ((n % 128 + 128).toUInt8 :: rest) = n := by + have h1 : (n % 128 + 128).toUInt8.toNat = n % 128 + 128 := toUInt8_toNat_of_lt _ (by omega) + refine ⟨(shape_cons rest.length _ rest).mpr (Or.inr ⟨by omega, hr.1⟩), ?_⟩ + rw [groupsValue_cons, hr.2, h1] + omega + +theorem varintAux_shape (f : Nat) : ∀ n, n < 128 ^ (f + 1) → + Spec.VarintShape (Spec.varintAux (f + 1) n).length (Spec.varintAux (f + 1) n) ∧ + Spec.groupsValue (Spec.varintAux (f + 1) n) = n := by + induction f with + | zero => + intro n hn + have h : n < 128 := by simpa using hn + rw [varintAux_succ] + simp only [h, ite_true] + exact single_shape n h + | succ f ih => + intro n hn + rw [varintAux_succ] + by_cases h : n < 128 + · simp only [h, ite_true] + exact single_shape n h + · simp only [h, ite_false] + exact cons_shape n _ (ih (n / 128) (div_lt n (f + 1) hn)) + +theorem varint_shape (n : Nat) : + Spec.VarintShape (Spec.varint n).length (Spec.varint n) ∧ Spec.groupsValue (Spec.varint n) = n := + varintAux_shape n n (lt_pow n) + +theorem varintAux_length (f : Nat) : + ∀ n k, 1 ≤ k → n < 128 ^ k → (Spec.varintAux f n).length ≤ k := by + induction f with + | zero => + intro n k _ _ + simp [Spec.varintAux] + | succ f ih => + intro n k hk hn + rw [varintAux_succ] + by_cases h : n < 128 + · simp only [h, ite_true, List.length_singleton] + exact hk + · simp only [h, ite_false, List.length_cons] + obtain ⟨j, rfl⟩ : ∃ j, k = j + 1 := ⟨k - 1, by omega⟩ + have hj : 1 ≤ j := by + rcases Nat.eq_zero_or_pos j with rfl | hj + · simp at hn + omega + · exact hj + have := ih (n / 128) j hj (div_lt n j hn) + omega + +theorem varint_length (n k : Nat) (hk : 1 ≤ k) (h : n < 128 ^ k) : (Spec.varint n).length ≤ k := + varintAux_length (n + 1) n k hk h + +theorem shape_mono {k k' : Nat} {bs : List UInt8} (h : Spec.VarintShape k bs) (hk : k ≤ k') : + Spec.VarintShape k' bs := + ⟨h.1, Nat.le_trans h.2.1 hk, h.2.2⟩ + +theorem decodeAux_varint (n k : Nat) (rest : List UInt8) (hk : 1 ≤ k) (h : n < 128 ^ k) : + Varint.decodeAux k (Spec.varint n ++ rest) = some (n, rest) := by + have hs := varint_shape n + exact (decodeAux_iff k _ n rest).mpr + ⟨Spec.varint n, rfl, shape_mono hs.1 (varint_length n k hk h), hs.2.symm⟩ + +/-! ## The encoder -/ + +theorem encodeAux_eq (f n : Nat) : Varint.encodeAux f n = Spec.varintAux f n := by + induction f generalizing n with + | zero => rfl + | succ f ih => simp only [Varint.encodeAux, Spec.varintAux, ih] + +/-- More fuel than the digits need changes nothing. -/ +theorem varintAux_add (f g : Nat) : + ∀ n, n < 128 ^ (f + 1) → Spec.varintAux (f + g + 1) n = Spec.varintAux (f + 1) n := by + induction f with + | zero => + intro n hn + have h : n < 128 := by simpa using hn + rw [varintAux_succ, varintAux_succ] + simp only [h, ite_true] + | succ f ih => + intro n hn + rw [varintAux_succ, varintAux_succ] + by_cases h : n < 128 + · simp only [h, ite_true] + · simp only [h, ite_false] + rw [Nat.add_right_comm f 1 g, ih (n / 128) (div_lt n (f + 1) hn)] + +theorem varintAux_eq_varint (f n : Nat) (hf : 1 ≤ f) (h : n < 128 ^ f) : + Spec.varintAux f n = Spec.varint n := by + unfold Spec.varint + obtain ⟨f, rfl⟩ : ∃ j, f = j + 1 := ⟨f - 1, by omega⟩ + rcases Nat.le_total f n with hle | hle + · have := varintAux_add f (n - f) n h + rw [show f + (n - f) + 1 = n + 1 by omega] at this + exact this.symm + · have := varintAux_add n (f - n) n (lt_pow n) + rw [show n + (f - n) + 1 = f + 1 by omega] at this + exact this + +theorem two_pow_le : 2 ^ 64 ≤ 128 ^ 10 := by decide + +theorem encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n := by + unfold Varint.encode + rw [encodeAux_eq] + exact varintAux_eq_varint 10 n (by decide) (Nat.lt_of_lt_of_le h two_pow_le) + +theorem decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) : + Varint.decode (Varint.encode n ++ rest) = some (n, rest) := by + unfold Varint.decode + rw [encode_eq n h, decodeAux_varint n 10 rest (by decide) (Nat.lt_of_lt_of_le h two_pow_le)] + simp [Nat.mod_eq_of_lt h] + +end Protobuf.Proofs.Varint diff --git a/Protobuf.lean b/Protobuf.lean new file mode 100644 index 0000000..e4cf139 --- /dev/null +++ b/Protobuf.lean @@ -0,0 +1,8 @@ +/- + The Protobuf wire format: varints, fields, and messages as lists of + raw fields. +-/ + +import Protobuf.Types +import Protobuf.Varint +import Protobuf.Wire diff --git a/Protobuf/Types.lean b/Protobuf/Types.lean new file mode 100644 index 0000000..dd42d06 --- /dev/null +++ b/Protobuf/Types.lean @@ -0,0 +1,32 @@ +/- + What a message is on the wire: a list of fields, each a field number + and a raw value of one of four wire types. Part of the approved + specification, with `Spec.lean` and `Spec/Defs.lean`, since every + statement is about these types. + + Which values are in range is `Spec.ValidField`, in `Spec/Defs.lean`. +-/ + +namespace Protobuf + +/-- A field's value as the wire carries it, before any schema gives it + a meaning. Groups (wire types 3 and 4) are outside this library. -/ +inductive Value where + /-- Wire type 0, `VARINT`: an unsigned value below 2^64. -/ + | varint (v : Nat) + /-- Wire type 1, `I64`: eight bytes, read as an unsigned value. -/ + | i64 (v : Nat) + /-- Wire type 2, `LEN`: a length, then that many bytes. -/ + | len (bytes : List UInt8) + /-- Wire type 5, `I32`: four bytes, read as an unsigned value. -/ + | i32 (v : Nat) + deriving DecidableEq, Repr + +/-- One field of a message: its field number and its value. A message + may repeat a field number; the order of fields is kept. -/ +structure Field where + number : Nat + value : Value + deriving DecidableEq, Repr + +end Protobuf diff --git a/Protobuf/Varint.lean b/Protobuf/Varint.lean new file mode 100644 index 0000000..0804cd9 --- /dev/null +++ b/Protobuf/Varint.lean @@ -0,0 +1,38 @@ +/- + Varints: unsigned numbers seven bits to a byte, least significant + group first, with the high bit of each byte set when another byte + follows. +-/ + +namespace Protobuf.Varint + +/-- At most `fuel` bytes of the varint for `n`. -/ +def encodeAux : Nat → Nat → List UInt8 + | 0, _ => [] + | fuel + 1, n => + if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: encodeAux fuel (n / 128) + +/-- The shortest varint for `n`. Ten bytes hold any value below 2^64. -/ +def encode (n : Nat) : List UInt8 := encodeAux 10 n + +/-- Reads a varint of at most `k` bytes from the front of the input: the + number its groups make, and the bytes after it. Fails when the input + ends first, or when byte `k` still has its high bit set. -/ +def decodeAux : Nat → List UInt8 → Option (Nat × List UInt8) + | 0, _ => none + | _ + 1, [] => none + | k + 1, b :: bs => + if b.toNat < 128 then some (b.toNat, bs) + else + match decodeAux k bs with + | some (v, rest) => some (b.toNat - 128 + 128 * v, rest) + | none => none + +/-- Reads a varint of up to ten bytes. Bits above the 64th are dropped, + as the reference parsers drop them. -/ +def decode (bs : List UInt8) : Option (Nat × List UInt8) := + match decodeAux 10 bs with + | some (v, rest) => some (v % 2 ^ 64, rest) + | none => none + +end Protobuf.Varint diff --git a/Protobuf/Wire.lean b/Protobuf/Wire.lean new file mode 100644 index 0000000..07bfddc --- /dev/null +++ b/Protobuf/Wire.lean @@ -0,0 +1,97 @@ +/- + Fields and messages on the wire. +-/ + +import Protobuf.Types +import Protobuf.Varint + +namespace Protobuf + +/-! ## Encoding -/ + +/-- The low `k` bytes of `n`, least significant first. -/ +def leBytes : Nat → Nat → List UInt8 + | 0, _ => [] + | k + 1, n => (n % 256).toUInt8 :: leBytes k (n / 256) + +def Value.wireType : Value → Nat + | .varint _ => 0 + | .i64 _ => 1 + | .len _ => 2 + | .i32 _ => 5 + +def Value.encode : Value → List UInt8 + | .varint v => Varint.encode v + | .i64 v => leBytes 8 v + | .len d => Varint.encode d.length ++ d + | .i32 v => leBytes 4 v + +/-- The tag, a varint of the field number and the wire type, then the + value. -/ +def Field.encode (f : Field) : List UInt8 := + Varint.encode (f.number * 8 + f.value.wireType) ++ f.value.encode + +/-- A message: its fields, one after another, in order. -/ +def encode (fs : List Field) : List UInt8 := + fs.flatMap Field.encode + +/-- Whether the field can be written: a field number from 1 to + 2^29 - 1, values that fit their wire type, and bytes shorter than + 2^31. -/ +def Field.isValid (f : Field) : Bool := + 1 ≤ f.number && f.number < 2 ^ 29 && + match f.value with + | .varint v => v < 2 ^ 64 + | .i64 v => v < 2 ^ 64 + | .len d => d.length < 2 ^ 31 + | .i32 v => v < 2 ^ 32 + +/-! ## Decoding -/ + +/-- Bytes read as a number, least significant first. -/ +def leValue (bs : List UInt8) : Nat := + bs.foldr (fun b acc => b.toNat + 256 * acc) 0 + +/-- Reads one field from the front of the input: the field, and the + bytes after it. -/ +def decodeField (bs : List UInt8) : Option (Field × List UInt8) := + match Varint.decodeAux 5 bs with + | none => none + | some (t, rest) => + if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none + else + let n := t / 8 + match t % 8 with + | 0 => + match Varint.decode rest with + | some (v, rest) => some (⟨n, .varint v⟩, rest) + | none => none + | 1 => if rest.length < 8 then none else some (⟨n, .i64 (leValue (rest.take 8))⟩, rest.drop 8) + | 2 => + match Varint.decodeAux 5 rest with + | some (len, rest) => + if 2 ^ 31 ≤ len ∨ rest.length < len then none + else some (⟨n, .len (rest.take len)⟩, rest.drop len) + | none => none + | 5 => if rest.length < 4 then none else some (⟨n, .i32 (leValue (rest.take 4))⟩, rest.drop 4) + | _ => none + +/-- Reads fields until the input ends. Each field takes at least one + byte, so `fuel` equal to the input's length is enough. -/ +def decodeAux : Nat → List UInt8 → Option (List Field) + | _, [] => some [] + | 0, _ :: _ => none + | fuel + 1, b :: bs => + match decodeField (b :: bs) with + | some (f, rest) => + match decodeAux fuel rest with + | some fs => some (f :: fs) + | none => none + | none => none + +/-- Reads a whole message. Fails on anything that is not a sequence of + well-formed fields, including input that ends inside a field. -/ +def decode (bs : List UInt8) : Option (List Field) := + decodeAux bs.length bs + +end Protobuf diff --git a/README.md b/README.md index 09395a9..12d2174 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,93 @@ -# protobuf -lean Protobuf wire format codec +# protobuf: the Protobuf wire format, proved + +This library reads and writes the Protobuf wire format in Lean: varints, field tags, and messages as lists of raw fields. Machine-checked proofs show three things: + +- the decoder accepts exactly the byte strings the encoding guide's rules allow, and refuses everything else, including input cut short; +- the encoder writes what the guide describes; +- decoding what the encoder wrote gives the fields back. + +It is tested against Google's own parsers, upb and C++; `tests/TEST-RESULTS.md` has the record. + +It is a project of [Proven Commons](https://github.com/Proven-Commons/mission), built to the verified bar published there. + +Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. + +## Use it + +From Lean: + +- `Protobuf.decode` reads a whole message as a list of fields, or fails. +- `Protobuf.encode` writes a list of fields. +- `Field.isValid` says whether a field can be written. +- `Varint.encode` and `Varint.decode` work on single varints. + +`SPEC.md` says what each one does. + +## What is proved + +The statements are in `Spec.lean`. The definitions they use, written from the encoding guide, are in `Spec/Defs.lean`, and the types are in `Protobuf/Types.lean`. The proofs are in `Proofs/`. + +| Claim | Theorem | +|-------|---------| +| The encoder writes the shortest varint. | `Spec.varint_encode_eq` | +| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, leaves the rest untouched, and refuses everything else. That includes input that ends inside the varint, and an eleventh byte. | `Spec.varint_decode_iff` | +| Decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` | +| `isValid` decides exactly which fields can be written: field numbers 1 to 2^29 - 1, and values that fit their wire type. | `Spec.isValid_iff` | +| The encoder writes each field as the guide describes: the tag, then the payload, every varint in its shortest form. | `Spec.encode_eq` | +| `decode` returns a field list exactly when the bytes split into records, one per field, in order. So it reads every well-formed message and returns the fields as written. It refuses everything else: a record cut short, a length past the end, field number 0, a group, an unknown wire type, and an oversized tag or length. | `Spec.decode_iff` | +| Decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` | +| Every field the decoder returns can be written again. | `Spec.decode_valid` | +| The guide's worked examples, and the edge and refusal cases listed in `SPEC.md`. | `Spec.guide_vectors`, `Spec.edge_vectors`, `Spec.reject_vectors` | + +The command-line tool in `Main.lean` calls these functions directly. + +## What is not proved + +- Reading requests and printing answers in `Main.lean`: the hex and decimal parsing and printing, and the request format. The differential tests cover them, with malformed requests. +- Groups (wire types 3 and 4) are refused, although both reference parsers read them. They are deprecated in the encoding guide and left for a later slice. +- Where the two reference parsers disagree, this decoder takes the stricter reading: + - it refuses field number 0, which upb reads; + - it refuses a tag of 2^32 or more, which the C++ parser reads by dropping the high bits. +- What fields mean. Schemas, `.proto` files, field types such as signed or zigzag integers, floats, strings, nested messages and packed repeated fields all sit above the wire format. A `LEN` field's bytes are returned as they are. +- Limits on message size and nesting that a program may want. The decoder reads any input in memory. A `LEN` field must be shorter than 2^31 bytes, as in the reference parsers. +- Speed. The code works on lists of bytes, which suits proofs, not bulk data. + +## What you must trust + +- The Lean kernel and the five external kernels shipped with Lean, which all check the proofs. +- `lake comparator`, which builds the statements and the proofs in a sandbox, exports them, and checks that each proof proves exactly its statement. +- bubblewrap and the Linux kernel's namespaces, which keep the untrusted build from tampering with that check. +- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. +- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about (by `implemented_by` and `extern`), such as the arithmetic on natural numbers and the fixed-width byte type. +- The operating system and hardware it runs on. +- Python's `protobuf` and `grpcio-tools` packages, as the oracle in the differential tests. The record names their versions. + +This project has no dependencies beyond Lean itself. + +## Re-check it + +Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), and Python 3.11 or later with `venv`, and network access for the oracle packages. + +``` +lake build +lake comparator --paranoid +python3 tests/run_tests.py +``` + +`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. + +The test script installs the pinned oracle packages into `.lake/oracle-venv` when they are missing. It then compares the tool with upb and with the C++ parser on inputs from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. + +## Layout + +- `Protobuf/Types.lean`: the field and value types. It is part of the specification. +- `Protobuf/Varint.lean`, `Protobuf/Wire.lean`: the code under proof. +- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. +- `Spec/Defs.lean`: the definitions the statements use, written from the encoding guide, with checks against its worked bytes. +- `Proofs.lean` and `Proofs/`: the proofs, under the same names. +- `Main.lean`: the command-line tool the tests drive. +- `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else. +- `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows. +- `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. +- `SPEC.md`: the specification in plain words. +- `tests/run_tests.py`: the differential tests. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..679c8fb --- /dev/null +++ b/SPEC.md @@ -0,0 +1,96 @@ +# Specification: protobuf + +This library implements the Protobuf wire format: varints, field tags, and messages as lists of raw fields. It is the layer under every `.proto` schema. It reads and writes the bytes without knowing what the fields mean. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `Protobuf/Types.lean`, and the other files `bar.toml` lists. + +The source is the Protobuf encoding guide, . Where the guide leaves a choice, the source is the behaviour of Google's two parsers: upb, which Python's `protobuf` package uses, and the C++ parser behind `protoc --decode_raw`. + +Bytes are `List UInt8`. The command-line tool converts them at the edges. + +## Varints + +A varint carries an unsigned number seven bits to a byte, least significant group first. The high bit of each byte is set when another byte follows. + +- `Varint.encode` writes the shortest varint for a number below 2^64, from one to ten bytes. +- `Varint.decode` reads one varint from the front of its input and returns its value and the rest of the input. + - It reads up to ten bytes. + - It fails when the input ends inside the varint, or when the tenth byte still has its high bit set. + - Any bits above the 64th are dropped, as both reference parsers drop them. + - A varint need not be in its shortest form: `80 00` reads as 0, as in both reference parsers. + +## Fields + +A message is a sequence of records. Each record is a tag, then a payload. The tag is a varint of `field_number * 8 + wire_type`. + +| Wire type | Name | Payload | Value here | +|-----------|------|---------|------------| +| 0 | `VARINT` | a varint | `.varint v`, below 2^64 | +| 1 | `I64` | eight bytes | `.i64 v`, the bytes little-endian | +| 2 | `LEN` | a varint length, then that many bytes | `.len bytes` | +| 5 | `I32` | four bytes | `.i32 v`, the bytes little-endian | + +The decoder refuses everything else: + +- a tag longer than five bytes, or of 2^32 or more; +- field number 0; +- wire types 3 and 4, which are groups; +- wire types 6 and 7, which do not exist; +- a length longer than five bytes, of 2^31 or more, or running past the end of the input; +- any record cut short. + +Groups are deprecated in the guide and outside this first slice. + +The two reference parsers differ in two places, and this library takes the stricter reading in both: + +- upb reads field number 0, which the C++ parser refuses. +- The C++ parser reads a five-byte tag of 2^32 or more by dropping its high bits, which upb refuses. + +`Field.isValid` says which fields the encoder can write: + +- a field number from 1 to 2^29 - 1; +- a `VARINT` or `I64` value below 2^64; +- an `I32` value below 2^32; +- `LEN` bytes shorter than 2^31. + +## Messages + +`encode` writes each field in turn: the shortest varint for its tag, then its payload, with any varint in its shortest form. + +`decode` reads records until the input ends and returns the fields in order. A field number may repeat, and the order is kept. The empty input is the empty message. If any record is malformed, the whole input is refused. `decode` never returns part of a message. + +## The command-line tool + +`protowire serve`, in `Main.lean`, answers requests from the differential tests, one per line. Its header comment gives the protocol. Every answer comes from `decode`, `encode` and `Field.isValid`. + +## What must always hold + +Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. They are written from the encoding guide and checked against its worked bytes. + +| Property | Theorem | +|----------|---------| +| The encoder writes the shortest varint. | `Spec.varint_encode_eq` | +| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, keeps the rest untouched, and refuses everything else. | `Spec.varint_decode_iff` | +| Decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` | +| `isValid` decides exactly which fields can be written. | `Spec.isValid_iff` | +| The encoder writes each field as the guide describes. | `Spec.encode_eq` | +| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules above. | `Spec.decode_iff` | +| Decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` | +| Every field the decoder returns can be written again. | `Spec.decode_valid` | +| The guide's worked examples: 1, 150 and 2^64 - 1 as varints, and four small messages. | `Spec.guide_vectors` | +| Fixed-width values are little-endian, varints need not be in shortest form, ten-byte varints drop bits past the 64th, and the largest field number reads. | `Spec.edge_vectors` | +| The decoder refuses each kind of malformed input listed above. | `Spec.reject_vectors` | + +Together, these fix every output. + +- `decode` is fixed for every input. +- `encode` and `Varint.encode` are fixed for every valid input. +- A decoder that accepted nothing would meet `Spec.decode_valid`, but it would fail `Spec.decode_iff` and `Spec.decode_encode`. +- A decoder that accepted too much would fail `Spec.decode_iff`. + +## Oracle + +Google's Protobuf parsers, compared on every input: + +- upb, through Python's `protobuf` package, reading each message as `google.protobuf.Empty` so that every field is kept as an unknown field; +- the C++ parser behind `protoc --decode_raw`, run in-process through `grpcio-tools`. + +The encoder is compared with `google.protobuf.internal.encoder`. diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..9bbea67 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,113 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the hash it had then. The proofs live in `Proofs.lean`, under + the same names; `lake comparator` checks that each one proves exactly + the statement written here. The `sorry`s below are expected in this + file only. + + The definitions the statements use, written from the Protobuf encoding + guide, are in `Spec/Defs.lean`, and the types in `Protobuf/Types.lean`. + Both are part of the specification too. +-/ + +import Protobuf +import Spec.Defs + +open Protobuf + +/-! ## Varints -/ + +/-- The encoder writes the shortest varint. -/ +theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n := sorry + +/-- The decoder reads exactly one varint from the front of its input: + up to ten bytes, the last without its high bit, and returns its + value and the rest of the input untouched. Anything else, including + input that ends inside the varint and an eleventh byte, is + refused. -/ +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 := sorry + +/-- Round trip: decoding what the encoder wrote gives the number back, + and leaves what follows untouched. -/ +theorem Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) : + Varint.decode (Varint.encode n ++ rest) = some (n, rest) := sorry + +/-! ## Messages -/ + +/-- `isValid` decides exactly which fields can be written. -/ +theorem Spec.isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f := sorry + +/-- The encoder writes each field as the encoding guide describes, with + every varint in its shortest form. -/ +theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : + Protobuf.encode fs = Spec.encode fs := sorry + +/-- `decode` returns `fs` exactly when the bytes split into records, one + per field of `fs`, in order. So it accepts every well-formed message, + refuses everything else (a record cut short, a length past the end, + field number 0, a group, an unknown wire type), and returns the + fields as written. -/ +theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) : + decode bs = some fs ↔ Spec.Message bs fs := sorry + +/-- Round trip: decoding what the encoder wrote gives the fields back. -/ +theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : + decode (Protobuf.encode fs) = some fs := sorry + +/-- Every field the decoder returns can be written again. -/ +theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) : + ∀ f ∈ fs, Spec.ValidField f := sorry + +/-! ## Test vectors -/ + +/-- The encoding guide's examples: 1, 150, and the largest 64-bit value + as varints, and the messages with field 1 set to 150, field 2 set + to "testing", field 3 holding the first message, and the packed + field 4 holding 3, 270 and 86942. -/ +theorem Spec.guide_vectors : + Varint.encode 1 = [0x01] ∧ + Varint.encode 150 = [0x96, 0x01] ∧ + Varint.encode (2 ^ 64 - 1) = [0xff, 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, 0x06, 0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05] = + some [⟨4, .len [0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05]⟩] ∧ + 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] := sorry + +/-- Fixed-width values are little-endian, and the reference parsers' + readings of unusual varints: not in shortest form, and ten bytes + with bits past the 64th. -/ +theorem Spec.edge_vectors : + 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 [] := sorry + +/-- Input the decoder refuses: a varint cut short, an eleventh varint + byte, field number 0, a length past the end, fixed-width values cut + short, a group, wire types 6 and 7, a tag of 2^32 or more, and a tag + or length longer than five bytes. -/ +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 [0x0e, 0x00] = none ∧ + decode [0x0f, 0x00] = none ∧ + decode [0xf8, 0xff, 0xff, 0xff, 0x1f, 0x01] = none ∧ + decode [0x88, 0x80, 0x80, 0x80, 0x80, 0x00, 0x01] = none ∧ + decode [0x0a, 0x81, 0x80, 0x80, 0x80, 0x80, 0x00, 0x61] = none := sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean new file mode 100644 index 0000000..cd62d47 --- /dev/null +++ b/Spec/Defs.lean @@ -0,0 +1,148 @@ +/- + The definitions the specification uses, written from the Protobuf + encoding guide (https://protobuf.dev/programming-guides/encoding/) + independently of the code in `Protobuf/`. Part of the approved + specification, with `Spec.lean` and `Protobuf/Types.lean`. + + Both the challenge file and the proofs import this file, so each + statement means the same thing on both sides. The `example`s check the + definitions against the guide's worked bytes. +-/ + +import Protobuf + +open Protobuf + +/-! ## Varints + +"Each byte in the varint has a continuation bit that indicates if the +byte that follows it is part of the varint. This is the most significant +bit (MSB) of the byte. The lower 7 bits of each byte are used to store +the two's complement representation of the number in groups of 7 bits, +least significant group first." Varints carry unsigned 64-bit values in +one to ten bytes. -/ + +/-- The number the low seven bits of each byte make, least significant + group first. -/ +def Spec.groupsValue (bs : List UInt8) : Nat := + ((List.range bs.length).map fun i => (bs.getD i 0).toNat % 128 * 128 ^ i).sum + +/-- The shape of a varint of at most `k` bytes: at least one byte, every + byte but the last with its high bit set, the last without it. -/ +def Spec.VarintShape (k : Nat) (bs : List UInt8) : Prop := + bs ≠ [] ∧ bs.length ≤ k ∧ + (∀ b ∈ bs.dropLast, 128 ≤ b.toNat) ∧ (∀ b ∈ bs.getLast?, b.toNat < 128) + +/-- `bs` is a varint for `v`. The reference parsers read up to ten + bytes and drop any bits above the 64th, so a value is its groups + modulo 2^64. A varint need not be in its shortest form: the + reference parsers read `80 00` as 0. -/ +def Spec.IsVarint (bs : List UInt8) (v : Nat) : Prop := + Spec.VarintShape 10 bs ∧ v = Spec.groupsValue bs % 2 ^ 64 + +/-- The shortest varint for `n`, as an encoder writes it: seven bits at + a time, least significant first, with the high bit set on every + byte but the last. `fuel` bounds the number of bytes; `n + 1` is + always enough. -/ +def Spec.varintAux : Nat → Nat → List UInt8 + | 0, _ => [] + | fuel + 1, n => + if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Spec.varintAux fuel (n / 128) + +def Spec.varint (n : Nat) : List UInt8 := Spec.varintAux (n + 1) n + +-- The guide's examples: 1 is `01`, and 150 is `96 01`. +example : Spec.varint 1 = [0x01] := by decide +example : Spec.varint 150 = [0x96, 0x01] := by decide +example : Spec.groupsValue [0x96, 0x01] = 150 := by decide +example : Spec.VarintShape 10 [0x96, 0x01] := by unfold Spec.VarintShape; decide + +/-! ## Fixed-width values + +"Non-varint numeric types are simple. `double` and `fixed64` have wire +type `I64`, which tells the parser to expect a fixed eight-byte lump of +data. ... Similarly `float` and `fixed32` have wire type `I32`, which +tells it to expect four bytes instead." The bytes are little-endian. -/ + +/-- The bytes read as a number, least significant first. -/ +def Spec.leValue (bs : List UInt8) : Nat := + ((List.range bs.length).map fun i => (bs.getD i 0).toNat * 256 ^ i).sum + +/-- `n` in `k` bytes, least significant first. -/ +def Spec.leBytes (k n : Nat) : List UInt8 := + (List.range k).map fun i => (n / 256 ^ i % 256).toUInt8 + +example : Spec.leValue [0x01, 0x02, 0x03, 0x04] = 0x04030201 := by decide +example : Spec.leBytes 4 0x04030201 = [0x01, 0x02, 0x03, 0x04] := by decide + +/-! ## Fields and messages + +"A protocol buffer message is a series of key-value pairs." Each record +is a tag, then its payload. "The 'tag' of a record is encoded as a +varint formed from the field number and the wire type via the formula +`(field_number << 3) | wire_type`." The wire types are 0 `VARINT`, +1 `I64`, 2 `LEN`, 3 `SGROUP`, 4 `EGROUP` and 5 `I32`. "The `LEN` wire +type has a dynamic length, specified by a varint immediately after the +tag, which is followed by the payload as usual." + +Field numbers run from 1 to 2^29 - 1, and a message is under 2 GiB. The +reference parsers read a tag or a length as a varint of at most five +bytes, refuse a tag of 2^32 or more and a length of 2^31 or more, and +refuse field number 0. Groups, wire types 3 and 4, are deprecated and +outside this library; wire types 6 and 7 do not exist. -/ + +/-- A field the encoder can write: a field number from 1 to 2^29 - 1, + and a value that fits its wire type. -/ +def Spec.ValidField (f : Field) : Prop := + 1 ≤ f.number ∧ f.number < 2 ^ 29 ∧ + match f.value with + | .varint v => v < 2 ^ 64 + | .i64 v => v < 2 ^ 64 + | .len d => d.length < 2 ^ 31 + | .i32 v => v < 2 ^ 32 + +/-- `tag` then `payload` are the bytes of field `f`. -/ +def Spec.FieldBytes (tag payload : List UInt8) (f : Field) : Prop := + Spec.VarintShape 5 tag ∧ Spec.groupsValue tag < 2 ^ 32 ∧ + f.number = Spec.groupsValue tag / 8 ∧ 1 ≤ f.number ∧ + match Spec.groupsValue tag % 8, f.value with + | 0, .varint v => Spec.IsVarint payload v + | 1, .i64 v => payload.length = 8 ∧ v = Spec.leValue payload + | 2, .len d => + ∃ pre, payload = pre ++ d ∧ Spec.VarintShape 5 pre ∧ Spec.groupsValue pre = d.length ∧ + d.length < 2 ^ 31 + | 5, .i32 v => payload.length = 4 ∧ v = Spec.leValue payload + | _, _ => False + +/-- `bs` is a message whose fields, in order, are `fs`: the bytes split + into records, one per field. -/ +inductive Spec.Message : List UInt8 → List Field → Prop where + | nil : Spec.Message [] [] + | cons {tag payload rest : List UInt8} {f : Field} {fs : List Field} : + Spec.FieldBytes tag payload f → Spec.Message rest fs → + Spec.Message (tag ++ payload ++ rest) (f :: fs) + +/-- The bytes an encoder writes for a field: the shortest varint for + the tag, then the payload, with any varint in its shortest form. -/ +def Spec.fieldBytes (f : Field) : List UInt8 := + match f.value with + | .varint v => Spec.varint (f.number * 8 + 0) ++ Spec.varint v + | .i64 v => Spec.varint (f.number * 8 + 1) ++ Spec.leBytes 8 v + | .len d => Spec.varint (f.number * 8 + 2) ++ Spec.varint d.length ++ d + | .i32 v => Spec.varint (f.number * 8 + 5) ++ Spec.leBytes 4 v + +/-- The bytes an encoder writes for a message: its fields in order. -/ +def Spec.encode (fs : List Field) : List UInt8 := + (fs.map Spec.fieldBytes).flatten + +-- The guide's examples: field 1 set to 150 is `08 96 01`, field 2 set +-- to "testing" is `12 07 74 65 73 74 69 6e 67`, and field 3 holding the +-- first message is `1a 03 08 96 01`. +example : Spec.encode [⟨1, .varint 150⟩] = [0x08, 0x96, 0x01] := by decide +example : Spec.encode [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] = + [0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by decide +example : Spec.encode [⟨3, .len [0x08, 0x96, 0x01]⟩] = [0x1a, 0x03, 0x08, 0x96, 0x01] := by decide +example : Spec.FieldBytes [0x08] [0x96, 0x01] ⟨1, .varint 150⟩ := by + refine ⟨by unfold Spec.VarintShape; decide, by decide, by decide, by decide, ?_⟩ + show Spec.IsVarint [0x96, 0x01] 150 + exact ⟨by unfold Spec.VarintShape; decide, by decide⟩ diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..ae0c17f --- /dev/null +++ b/bar.toml @@ -0,0 +1,35 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "protobuf" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. It was drafted +# by Claude, an AI agent, for the org. +spec_authors = ["claude"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +# Protobuf/Types.lean holds the types every statement is about, so it +# is part of the specification. +files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Protobuf/Types.lean"] +# The code under proof: the functions the statements are about. +code = [ + "Protobuf.Varint.encode", "Protobuf.Varint.decode", + "Protobuf.encode", "Protobuf.decode", "Protobuf.Field.isValid", +] + +# 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/protobuf/pull/" + +[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..da878b7 --- /dev/null +++ b/comparator.json @@ -0,0 +1,10 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "Spec.varint_encode_eq", "Spec.varint_decode_iff", "Spec.varint_decode_encode", + "Spec.isValid_iff", "Spec.encode_eq", "Spec.decode_iff", "Spec.decode_encode", + "Spec.decode_valid", "Spec.guide_vectors", "Spec.edge_vectors", "Spec.reject_vectors" + ], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"] +} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..0bd7518 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "protobuf", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..f65e4dc --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,16 @@ +name = "protobuf" +version = "0.1.0" +defaultTargets = ["Protobuf", "Spec", "Proofs", "protowire"] + +[[lean_lib]] +name = "Protobuf" + +[[lean_lib]] +name = "Spec" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "protowire" +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..525e9b4 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,15 @@ +# Test results + +Written by `tests/run_tests.py`. Rerun it to check these numbers. + +- Oracle: Python 3.13.17, protobuf 7.36.2 (upb), grpcio-tools 1.84.1 (protoc --decode_raw, C++) +- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- Seed: 20261025 +- Inputs: 200000 +- Mutated: 77137 of the inputs are mutated encodings +- By kind: decode mutated 77137, decode random 18392, decode valid 46010, encode 46010, encode invalid 12436, error 15 +- Messages decoded: 141539, of which 73247 read by both reference parsers alike and 68292 refused +- Refused although a reference parser reads them: a five-byte tag of 2^32 or more, which C++ reads and upb refuses 1253, a group, which both read 1022, field number 0, which upb reads and C++ refuses 1700 +- Malformed requests answered `error`: 15 of 15 +- Last lines with no LF, sent alone, answered right: 2 of 2 +- Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..4b57a29 --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,577 @@ +#!/usr/bin/env python3 +"""Differential tests: the Lean wire format codec against the reference +Protobuf parsers. + +There are two oracles, both from Google's Protobuf releases: + +- upb, the parser behind Python's `protobuf` package. A message is read + as `google.protobuf.Empty`, so every field lands in its unknown field + set, which gives the field numbers, wire types and raw values. +- The C++ parser behind `protoc --decode_raw`, run in-process through + `grpcio-tools`. It gives whether the bytes parse, and the top-level + field numbers and numeric values. + +The encoder is compared with `google.protobuf.internal.encoder`. + +Where the two parsers disagree, the Lean decoder must take the stricter +reading and refuse the input. They differ in two known ways: upb reads +field number 0, which the C++ parser refuses, and the C++ parser reads a +five-byte tag of 2^32 or more by dropping the high bits, which upb +refuses. Groups (wire types 3 and 4) are outside this library, so a +message that both parsers read but that holds a group must be refused. +The record counts each case. + +Inputs come from a recorded seed: + +- random field lists, weighted toward boundary field numbers and + values, encoded and decoded; +- mutations of those encodings: a byte changed, dropped, added or + flipped, the message cut short or extended, a varint rewritten longer + than it needs to be (up to and past ten bytes), a tag with field + number 0, a group, wire type 6 or 7, or a tag of 2^32 or more; +- random short byte strings; +- field lists the encoder must refuse; +- malformed requests, which the tool must answer with `error`. + +For every input the Lean answer must equal the oracle's. + + python3 tests/run_tests.py [--seed N] [--count N] + +It needs `protobuf` and `grpcio-tools` at the versions below. When they +are missing it creates a virtual environment in `.lake/oracle-venv`, +installs them there, and runs itself again with it; where Python cannot +make one, it installs them into `.lake/oracle-packages` instead. It builds the +executable, writes tests/TEST-RESULTS.md, and exits non-zero if any +input disagrees. +""" + +import argparse +import itertools +import os +import platform +import random +import re +import struct +import subprocess +import sys +import tempfile +import threading +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = ROOT / ".lake" / "build" / "bin" / "protowire" +RESULTS = ROOT / "tests" / "TEST-RESULTS.md" +VENV = ROOT / ".lake" / "oracle-venv" +PKGS = ROOT / ".lake" / "oracle-packages" +PINS = ["protobuf==7.36.2", "grpcio-tools==1.84.1"] +TIMEOUT = 1800 +BUILD_TIMEOUT = 3600 + + +def ensure_oracles(): + """Import the oracles. When this Python lacks them, install the pinned + versions into a virtual environment and run again with it; where a + virtual environment cannot be made, install them into a folder + instead and import them from there.""" + try: + import google.protobuf # noqa: F401 + import grpc_tools # noqa: F401 + return + except ImportError: + pass + if os.environ.get("PROTOWIRE_ORACLE_VENV"): + sys.exit("the oracle packages did not import even in .lake/oracle-venv") + python = VENV / "bin" / "python" + made = python.exists() or subprocess.run( + [sys.executable, "-m", "venv", str(VENV)], capture_output=True).returncode == 0 + if made and not os.environ.get("PROTOWIRE_NO_VENV"): + subprocess.run([str(python), "-m", "pip", "install", "--quiet", *PINS], check=True) + env = dict(os.environ, PROTOWIRE_ORACLE_VENV="1") + os.execve(str(python), [str(python), *sys.argv], env) + subprocess.run([sys.executable, "-m", "pip", "install", "--quiet", "--break-system-packages", + "--target", str(PKGS), *PINS], check=True) + sys.path.insert(0, str(PKGS)) + + +# The oracles. + +def upb_decode(data): + """upb's reading: a list of (number, kind, value), or None.""" + from google.protobuf import empty_pb2 + from google.protobuf.message import DecodeError + from google.protobuf.unknown_fields import UnknownFieldSet + try: + msg = empty_pb2.Empty.FromString(data) + except DecodeError: + return None + fields = [] + for f in UnknownFieldSet(msg): + kind = {0: "varint", 1: "i64", 2: "len", 3: "group", 5: "i32"}[f.wire_type] + value = f.data.hex() if kind == "len" else (None if kind == "group" else f.data) + fields.append((f.field_number, kind, value)) + return fields + + +def cpp_decode_raw(data): + """The C++ parser's reading through `protoc --decode_raw`: the text it + prints, or None when it refuses the input.""" + from grpc_tools import _protoc_compiler + with tempfile.TemporaryFile() as fin, tempfile.TemporaryFile() as fout, \ + tempfile.TemporaryFile() as ferr: + fin.write(data) + fin.flush() + fin.seek(0) + saved = [os.dup(0), os.dup(1), os.dup(2)] + try: + os.dup2(fin.fileno(), 0) + os.dup2(fout.fileno(), 1) + os.dup2(ferr.fileno(), 2) + code = _protoc_compiler.run_main([b"protoc", b"--decode_raw"]) + finally: + for fd, s in zip((0, 1, 2), saved): + os.dup2(s, fd) + os.close(s) + fout.seek(0) + return fout.read().decode("utf-8", "backslashreplace") if code == 0 else None + + +TOP_VALUE = re.compile(r"(\d+): (.*)") +OPEN_LINE = re.compile(r" *\d+ \{") + + +def cpp_top_level(text): + """The top-level (number, value text) pairs of `--decode_raw` output.""" + out, depth = [], 0 + for line in text.splitlines(): + # A nested message opens with a line `N {` and closes with a + # line `}`; braces inside a quoted string are not structure. + opens = OPEN_LINE.fullmatch(line) is not None + if depth == 0: + m = TOP_VALUE.fullmatch(line) + if opens: + out.append((int(line.split(" ")[0]), "{")) + elif m: + out.append((int(m.group(1)), m.group(2))) + if opens: + depth += 1 + elif line.strip() == "}": + depth -= 1 + return out + + +def cpp_agrees(fields, text): + """Whether the C++ reading has the same field numbers, in order, and + the same numeric values.""" + top = cpp_top_level(text) + if [n for n, _ in top] != [n for n, _, _ in fields]: + return False + for (n, kind, value), (_, shown) in zip(fields, top): + if kind == "varint" and shown != str(value): + return False + if kind == "i32" and shown != f"0x{value:08x}": + return False + if kind == "i64" and shown != f"0x{value:016x}": + return False + return True + + +def oracle_encode(fields): + from google.protobuf.internal import encoder + out = b"" + for n, kind, value in fields: + wt = {"varint": 0, "i64": 1, "len": 2, "i32": 5}[kind] + out += encoder.TagBytes(n, wt) + if kind == "varint": + out += encoder._VarintBytes(value) + elif kind == "i64": + out += struct.pack(">= 7 + if n: + out.append(b | 0x80) + else: + out.append(b) + return bytes(out) + + +def long_varint(n, size): + """`n` as a varint of exactly `size` bytes, padded with zero groups.""" + groups = [] + for _ in range(size): + groups.append(n & 0x7F) + n >>= 7 + return bytes([g | 0x80 for g in groups[:-1]] + [groups[-1]]) + + +def random_number(rng): + r = rng.random() + if r < 0.6: + return rng.randint(1, 15) + if r < 0.8: + return rng.choice([1, 15, 16, 2047, 2048, 262143, 262144, 2 ** 29 - 1, 19000, 19999]) + return rng.randint(1, 2 ** 29 - 1) + + +def random_u(rng, bits): + r = rng.random() + if r < 0.3: + return rng.randint(0, 300) + if r < 0.6: + k = rng.randint(1, bits) + return rng.choice([2 ** k - 1, 2 ** (k - 1), 2 ** k - 2]) % 2 ** bits + return rng.getrandbits(bits) + + +def random_field(rng): + kind = rng.choice(["varint", "varint", "len", "len", "i64", "i32"]) + n = random_number(rng) + if kind == "varint": + return (n, kind, random_u(rng, 64)) + if kind == "i64": + return (n, kind, random_u(rng, 64)) + if kind == "i32": + return (n, kind, random_u(rng, 32)) + size = rng.choice([0, 1, 3, 7, rng.randint(0, 40), rng.randint(0, 40), rng.randint(120, 300)]) + return (n, kind, bytes(rng.getrandbits(8) for _ in range(size)).hex()) + + +def random_fields(rng): + return [random_field(rng) for _ in range(rng.choice([0, 1, 1, 2, 3, 5, 8]))] + + +def mutate(rng, data): + b = bytearray(data) + op = rng.randrange(11) + if op == 0 and b: + b[rng.randrange(len(b))] = rng.getrandbits(8) + elif op == 1 and b: + del b[rng.randrange(len(b))] + elif op == 2: + b.insert(rng.randint(0, len(b)), rng.getrandbits(8)) + elif op == 3 and b: + b[rng.randrange(len(b))] ^= 1 << rng.randrange(8) + elif op == 4 and b: + b = b[: rng.randrange(len(b))] + elif op == 5: + b += bytes(rng.getrandbits(8) for _ in range(rng.randint(1, 4))) + elif op == 6: + # A record whose tag is longer than it needs to be, up to and + # past five bytes, in front. + n, wt = random_number(rng), rng.choice([0, 0, 2, 5]) + payload = {0: varint(rng.randint(0, 300)), 2: b"\x01a", 5: b"\x00" * 4}[wt] + size = rng.randint(len(varint(n * 8 + wt)), 7) + b = bytearray(long_varint(n * 8 + wt, size) + payload) + b + elif op == 7: + # A varint value longer than it needs to be, up to and past ten bytes. + size = rng.randint(1, 12) + v = rng.getrandbits(min(64, 7 * size)) + b += varint(random_number(rng) * 8) + long_varint(v, size) + if rng.random() < 0.3: + b[-1] = rng.choice([0x01, 0x02, 0x7F, 0x80]) + elif op == 8: + # Field number 0, a group, or wire type 6 or 7. + wt = rng.choice([0, 3, 4, 6, 7]) + n = 0 if wt == 0 else random_number(rng) + rec = varint(n * 8 + wt) + (varint(1) if wt == 0 else b"") + if wt == 3 and rng.random() < 0.7: + rec += varint(random_number(rng) * 8) + varint(5) + varint(n * 8 + 4) + b = bytearray(rec) + b + elif op == 9: + # A five-byte tag of 2^32 or more. + t = rng.randint(2 ** 32, 2 ** 35 - 1) + b = bytearray(long_varint(t, 5) + varint(1)) + b + else: + # A length varint longer than it needs to be, or past the end. + data_ = bytes(rng.getrandbits(8) for _ in range(rng.randint(0, 5))) + size = rng.randint(1, 7) + claimed = len(data_) + rng.choice([0, 0, 1, -1 if data_ else 0, 2 ** 31]) + b += varint(random_number(rng) * 8 + 2) + long_varint(claimed, max(size, len(varint(claimed)))) + data_ + return bytes(b) + + +def invalid_fields(rng): + fields = random_fields(rng) or [random_field(rng)] + i = rng.randrange(len(fields)) + n, kind, value = fields[i] + which = rng.randrange(4) + if which == 0: + n = 0 + elif which == 1: + n = rng.choice([2 ** 29, 2 ** 29 + 1, 2 ** 29 + rng.randint(0, 1000), 2 ** 32]) + elif kind == "varint" or kind == "i64": + value = rng.choice([2 ** 64, 2 ** 64 + 1, 2 ** 64 + rng.randint(0, 2 ** 20)]) + elif kind == "i32": + value = rng.choice([2 ** 32, 2 ** 32 + 1, 2 ** 32 + rng.randint(0, 2 ** 20)]) + else: + n = 0 + fields[i] = (n, kind, value) + return fields + + +MALFORMED = [ + ("frob 00", "unknown operation"), + ("DECODE 00", "operations are lower case"), + ("decode", "no argument"), + ("decode 0", "an odd number of hex digits"), + ("decode 0g", "not a hex digit"), + ("decode 0A", "hex digits are lower case"), + ("decode 00 00", "two arguments"), + ("encode", "no argument"), + ("encode 1:varint", "a field item without a value"), + ("encode 1:float:1", "an unknown kind"), + ("encode 1:varint:-1", "a negative number"), + ("encode 1:varint:1,", "an empty item"), + ("encode 1:len:0", "odd hex in a len value"), + ("encode x:varint:1", "a field number that is not a number"), + (" decode 00", "a leading space"), +] + +AT_EOF = [("decode 089601", "OK\t1:varint:150"), ("encode 1:varint:150", "089601")] + + +def fields_text(fields): + return ",".join(f"{n}:{k}:{v}" for n, k, v in fields) if fields else "-" + + +def cases(seed, count, tally): + """(label, request, expected answer, mutated) for each input.""" + rng = random.Random(seed) + made = 0 + for req, _ in MALFORMED: + if made < count: + yield ("error", req, "error", False) + made += 1 + while made < count: + r = rng.random() + if r < 0.3: + fields = random_fields(rng) + data = oracle_encode(fields) + yield ("encode", f"encode {fields_text(fields)}", data.hex(), False) + want, _ = expected_decode(data, tally) + yield ("decode valid", f"decode {data.hex()}", want, False) + made += 2 + elif r < 0.8: + base = oracle_encode(random_fields(rng)) + data = mutate(rng, base) + while data == base: + data = mutate(rng, base) + want, _ = expected_decode(data, tally) + yield ("decode mutated", f"decode {data.hex()}", want, True) + made += 1 + elif r < 0.92: + data = bytes(rng.getrandbits(8) for _ in range(rng.randint(0, 12))) + want, _ = expected_decode(data, tally) + yield ("decode random", f"decode {data.hex()}", want, False) + made += 1 + else: + yield ("encode invalid", f"encode {fields_text(invalid_fields(rng))}", "INVALID", False) + made += 1 + + +def run_tool(data, timeout=TIMEOUT): + """The tool's answer lines for `data`, and a note on how the run + failed, or None.""" + raw = data.encode("utf-8") + limit = 2 * len(raw) + 64 * (data.count("\n") + 1) + try: + proc = subprocess.Popen([str(EXE), "serve"], stdin=subprocess.PIPE, + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + except OSError as e: + return [], f"could not run {EXE.relative_to(ROOT)}: {e.strerror or e}" + out, err = bytearray(), bytearray() + + def feed(): + try: + proc.stdin.write(raw) + proc.stdin.close() + except (BrokenPipeError, ValueError): + pass + + def drain(stream, buf, cap): + while chunk := stream.read1(1 << 16): + buf += chunk + if len(buf) > cap: + proc.kill() + return + + threads = [threading.Thread(target=feed), + threading.Thread(target=drain, args=(proc.stdout, out, limit)), + threading.Thread(target=drain, args=(proc.stderr, err, 1 << 20))] + for t in threads: + t.start() + problem = None + try: + proc.wait(timeout=timeout) + except subprocess.TimeoutExpired: + proc.kill() + problem = f"no end after {timeout} seconds" + for t in threads: + t.join() + proc.wait() + if len(out) > limit: + problem = problem or f"more than {limit} bytes of output, stopped" + elif proc.returncode != 0 and not problem: + tail = " / ".join(err.decode("utf-8", "backslashreplace").splitlines()[-3:]) + problem = f"exit status {proc.returncode}: {tail}" + text = bytes(out).decode("utf-8", "backslashreplace") + if text and not text.endswith("\n"): + problem = problem or "the last answer has no LF" + lines = text.split("\n") + if lines and lines[-1] == "": + lines.pop() + return lines, problem + + +def oracle(): + from importlib.metadata import version + return (f"Python {platform.python_version()}, protobuf {version('protobuf')} (upb), " + f"grpcio-tools {version('grpcio-tools')} (protoc --decode_raw, C++)") + + +def lean_version(): + try: + out = subprocess.run(["lake", "env", "lean", "--version"], cwd=ROOT, + capture_output=True, text=True, errors="backslashreplace", + timeout=300) + first = out.stdout.strip().splitlines()[:1] + return first[0] if first else "unknown" + except (OSError, subprocess.TimeoutExpired): + return "unknown" + + +def count(text): + n = int(text) + if n < 1: + raise argparse.ArgumentTypeError("the count must be at least 1") + return n + + +def write(lines): + RESULTS.write_text("\n".join(lines), encoding="utf-8") + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261025) + ap.add_argument("--count", type=count, default=200_000) + args = ap.parse_args() + ensure_oracles() + + try: + build = subprocess.run(["lake", "build", "protowire"], cwd=ROOT, capture_output=True, + text=True, errors="backslashreplace", timeout=BUILD_TIMEOUT) + built, log = build.returncode == 0, build.stdout + build.stderr + except (OSError, subprocess.TimeoutExpired) as e: + built, log = False, str(e) + if not built: + write(["# Test results", "", f"- Oracle: {oracle()}", f"- Seed: {args.seed}", + "- Inputs: 0", "- Failures: 1 (`lake build protowire` failed)", ""]) + sys.exit("lake build protowire failed:\n" + log) + + tally = {} + items = list(cases(args.seed, args.count, tally)) + out, problem = run_tool("".join(req + "\n" for _, req, _, _ in items)) + failures = [("(whole run)", "a clean run", problem)] if problem else [] + for item, got in itertools.zip_longest(items, out): + if item is None: + failures.append(("(no request)", "nothing", got)) + elif got != item[2]: + failures.append((item[1], item[2], "(no answer)" if got is None else got)) + eof_right = 0 + for req, want in AT_EOF: + got, problem = run_tool(req, timeout=60) + if got == [want] and not problem: + eof_right += 1 + else: + failures.append((req + " (at end of input)", want, f"{got} {problem or ''}".strip())) + + by_label = {} + for label, _, _, _ in items: + by_label[label] = by_label.get(label, 0) + 1 + decodes = [want for label, req, want, _ in items if label.startswith("decode")] + accepted = sum(1 for w in decodes if w.startswith("OK")) + mutated = sum(1 for item in items if item[3]) + malformed = [got for item, got in zip(items, out) if item[0] == "error"] + + lines = [ + "# Test results", + "", + "Written by `tests/run_tests.py`. Rerun it to check these numbers.", + "", + f"- Oracle: {oracle()}", + f"- Lean: {lean_version()}", + f"- Seed: {args.seed}", + f"- Inputs: {len(items)}", + f"- Mutated: {mutated} of the inputs are mutated encodings", + "- By kind: " + ", ".join(f"{k} {v}" for k, v in sorted(by_label.items())), + f"- Messages decoded: {len(decodes)}, of which {accepted} read by both reference " + f"parsers alike and {len(decodes) - accepted} refused", + "- Refused although a reference parser reads them: " + + (", ".join(f"{k} {v}" for k, v in sorted(tally.items())) or "none"), + f"- Malformed requests answered `error`: {malformed.count('error')} of " + f"{by_label.get('error', 0)}", + f"- Last lines with no LF, sent alone, answered right: {eof_right} of {len(AT_EOF)}", + f"- Failures: {len(failures)}", + "", + ] + if failures: + lines += ["## Failures", ""] + lines += [f"- `{req[:160]!r}`: expected `{want[:120]!r}`, got `{got[:120]!r}`" + for req, want, got in failures[:50]] + lines.append("") + write(lines) + agree = sum(1 for item, got in zip(items, out) if got == item[2]) + print(f"{agree}/{len(items)} inputs agree, {len(failures)} failures; results in {RESULTS}") + return 1 if failures else 0 + + +if __name__ == "__main__": + sys.exit(main()) From 8d24a862540156ff272fed8a95baaf9786eec92f Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 10:06:09 +0000 Subject: [PATCH 2/4] Take the stricter reading on long lengths, decode in linear time, and correct the page A pre-review found four things to change in the slice: - The C++ parser refuses LEN lengths of 2^31 - 16 or more, which upb reads. The decoder and Field.isValid now refuse them too, so the rule of taking the stricter reading holds in all three places where the parsers disagree. - Each length check walked the whole remaining input, so decoding many fixed-width fields took quadratic time. The checks now look at no more bytes than the field needs. - Two "guide examples" were not in the current encoding guide. The vectors now use the guide's own bytes, including -2 and Test4. A lone end-group tag and a tag of exactly 2^32 are added to the refusals. - The page and SPEC.md overstated the round trip and the headline claim. The validity conditions and the exclusion of groups are now stated. The tests now insist on the pinned upb oracle, fail on any unknown disagreement between the parsers, send CR LF and blank lines, and try the boundary tag 2^32. The tool flushes each answer. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Main.lean | 13 +++++---- Proofs/Main.lean | 9 ++++-- Proofs/Message.lean | 16 ++++++++--- Protobuf/Wire.lean | 18 ++++++++---- README.md | 37 +++++++++++++------------ SPEC.md | 28 +++++++++++-------- Spec.lean | 39 ++++++++++++++++---------- Spec/Defs.lean | 19 ++++++++----- tests/TEST-RESULTS.md | 13 +++++---- tests/run_tests.py | 64 +++++++++++++++++++++++++++++++++---------- 10 files changed, 165 insertions(+), 91 deletions(-) diff --git a/Main.lean b/Main.lean index 737b356..0cf7f43 100644 --- a/Main.lean +++ b/Main.lean @@ -10,13 +10,15 @@ 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, - 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. + 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 in pairs, or a field item that does not parse. A request - line may end in LF or CR LF. + 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 @@ -103,6 +105,7 @@ def main (args : List String) : IO UInt32 := do 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" diff --git a/Proofs/Main.lean b/Proofs/Main.lean index ab34a20..e68bf18 100644 --- a/Proofs/Main.lean +++ b/Proofs/Main.lean @@ -45,18 +45,19 @@ theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = s theorem Spec.guide_vectors : Varint.encode 1 = [0x01] ∧ Varint.encode 150 = [0x96, 0x01] ∧ - Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 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, 0x06, 0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05] = - some [⟨4, .len [0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05]⟩] ∧ + 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⟩] ∧ @@ -76,9 +77,11 @@ theorem Spec.reject_vectors : 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 diff --git a/Proofs/Message.lean b/Proofs/Message.lean index 3b5aea3..cb65b96 100644 --- a/Proofs/Message.lean +++ b/Proofs/Message.lean @@ -38,7 +38,7 @@ theorem field_encode_eq (f : Field) (h : Spec.ValidField f) : f.encode = Spec.fi show Varint.encode (n * 8 + 1) ++ leBytes 8 v = Spec.varint (n * 8 + 1) ++ Spec.leBytes 8 v rw [Proofs.Varint.encode_eq _ (hn 1 (by decide)), Proofs.Fixed.leBytes_eq] | len d => - have h3 : d.length < 2 ^ 31 := h3 + have h3 : d.length < 2 ^ 31 - 16 := h3 show Varint.encode (n * 8 + 2) ++ (Varint.encode d.length ++ d) = Spec.varint (n * 8 + 2) ++ Spec.varint d.length ++ d rw [Proofs.Varint.encode_eq _ (hn 2 (by decide)), Proofs.Varint.encode_eq _ (by omega), @@ -63,12 +63,19 @@ theorem encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : enco /-! ## One record -/ +/-- The length checks in `decodeField` look at no more than `k` bytes. -/ +theorem take_short (l : List UInt8) (k : Nat) : ((l.take k).length < k) = (l.length < k) := by + simp only [List.length_take] + apply propext + omega + theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) : decodeField bs = some (f, rest) ↔ ∃ tag payload, bs = tag ++ payload ++ rest ∧ Spec.FieldBytes tag payload f := by constructor · intro h unfold decodeField at h + simp only [take_short] at h cases ht : Varint.decodeAux 5 bs with | none => rw [ht] at h; exact absurd h (by simp) | some p => @@ -109,7 +116,7 @@ theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) : split at h · rename_i len r2 hv obtain ⟨pre, hr, hps, hpv⟩ := (Proofs.Varint.decodeAux_iff 5 r len r2).mp hv - by_cases hl : 2 ^ 31 ≤ len ∨ r2.length < len + by_cases hl : 2 ^ 31 - 16 ≤ len ∨ r2.length < len · simp only [hl, ↓reduceIte] at h exact absurd h (by simp) · simp only [hl, ↓reduceIte, Option.some.injEq, Prod.mk.injEq] at h @@ -141,6 +148,7 @@ theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) : omega have hnum' : num = Spec.groupsValue tag / 8 := hnum unfold decodeField + simp only [take_short] rw [hd] simp only [hc, ↓reduceIte] simp only at hm @@ -159,7 +167,7 @@ theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) : obtain ⟨pre, rfl, hps, hpv, hdl⟩ := hm have hd2 : Varint.decodeAux 5 (pre ++ d ++ rest) = some (d.length, d ++ rest) := (Proofs.Varint.decodeAux_iff 5 _ _ _).mpr ⟨pre, List.append_assoc _ _ _, hps, hpv.symm⟩ - have hl' : ¬(2 ^ 31 ≤ d.length ∨ (d ++ rest).length < d.length) := by simp; omega + have hl' : ¬(2 ^ 31 - 16 ≤ d.length ∨ (d ++ rest).length < d.length) := by simp; omega rw [hw] simp only rw [hd2] @@ -304,7 +312,7 @@ theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) : exact ⟨Proofs.Fixed.leBytes_length 8 v, (Proofs.Fixed.leValue_leBytes 8 v (by simpa using h3)).symm⟩ | len d => - have h3 : d.length < 2 ^ 31 := h3 + have h3 : d.length < 2 ^ 31 - 16 := h3 obtain ⟨hs, hg⟩ := tag_bytes n 2 h2 (by decide) refine ⟨Spec.varint (n * 8 + 2), Spec.varint d.length ++ d, List.append_assoc _ _ _, hs, by rw [hg]; omega, show n = _ by rw [hg]; omega, h1, ?_⟩ diff --git a/Protobuf/Wire.lean b/Protobuf/Wire.lean index 07bfddc..cac05a3 100644 --- a/Protobuf/Wire.lean +++ b/Protobuf/Wire.lean @@ -37,13 +37,13 @@ def encode (fs : List Field) : List UInt8 := /-- Whether the field can be written: a field number from 1 to 2^29 - 1, values that fit their wire type, and bytes shorter than - 2^31. -/ + 2^31 - 16, the longest the C++ parser reads. -/ def Field.isValid (f : Field) : Bool := 1 ≤ f.number && f.number < 2 ^ 29 && match f.value with | .varint v => v < 2 ^ 64 | .i64 v => v < 2 ^ 64 - | .len d => d.length < 2 ^ 31 + | .len d => d.length < 2 ^ 31 - 16 | .i32 v => v < 2 ^ 32 /-! ## Decoding -/ @@ -53,7 +53,9 @@ def leValue (bs : List UInt8) : Nat := bs.foldr (fun b acc => b.toNat + 256 * acc) 0 /-- Reads one field from the front of the input: the field, and the - bytes after it. -/ + bytes after it. Each length check looks at no more of the input than + the field needs, so reading a message takes time in proportion to + its length. -/ def decodeField (bs : List UInt8) : Option (Field × List UInt8) := match Varint.decodeAux 5 bs with | none => none @@ -66,14 +68,18 @@ def decodeField (bs : List UInt8) : Option (Field × List UInt8) := match Varint.decode rest with | some (v, rest) => some (⟨n, .varint v⟩, rest) | none => none - | 1 => if rest.length < 8 then none else some (⟨n, .i64 (leValue (rest.take 8))⟩, rest.drop 8) + | 1 => + if (rest.take 8).length < 8 then none + else some (⟨n, .i64 (leValue (rest.take 8))⟩, rest.drop 8) | 2 => match Varint.decodeAux 5 rest with | some (len, rest) => - if 2 ^ 31 ≤ len ∨ rest.length < len then none + if 2 ^ 31 - 16 ≤ len ∨ (rest.take len).length < len then none else some (⟨n, .len (rest.take len)⟩, rest.drop len) | none => none - | 5 => if rest.length < 4 then none else some (⟨n, .i32 (leValue (rest.take 4))⟩, rest.drop 4) + | 5 => + if (rest.take 4).length < 4 then none + else some (⟨n, .i32 (leValue (rest.take 4))⟩, rest.drop 4) | _ => none /-- Reads fields until the input ends. Each field takes at least one diff --git a/README.md b/README.md index 12d2174..752e664 100644 --- a/README.md +++ b/README.md @@ -2,9 +2,9 @@ This library reads and writes the Protobuf wire format in Lean: varints, field tags, and messages as lists of raw fields. Machine-checked proofs show three things: -- the decoder accepts exactly the byte strings the encoding guide's rules allow, and refuses everything else, including input cut short; -- the encoder writes what the guide describes; -- decoding what the encoder wrote gives the fields back. +- the decoder accepts exactly the messages that the rules in `SPEC.md` allow, and refuses everything else, including input cut short. Those rules are the encoding guide's, without groups, taking the stricter reading wherever Google's two parsers disagree; +- for fields that `Field.isValid` accepts, the encoder writes what the guide describes; +- for those fields, decoding what the encoder wrote gives the fields back. It is tested against Google's own parsers, upb and C++; `tests/TEST-RESULTS.md` has the record. @@ -17,9 +17,9 @@ Status: in progress. The specification has not yet been approved by a reviewer a From Lean: - `Protobuf.decode` reads a whole message as a list of fields, or fails. -- `Protobuf.encode` writes a list of fields. +- `Protobuf.encode` writes a list of fields. It is specified only for fields that `Field.isValid` accepts, so check that first, as the command-line tool does. For a field out of range, it writes bytes that do not read back as that field. - `Field.isValid` says whether a field can be written. -- `Varint.encode` and `Varint.decode` work on single varints. +- `Varint.encode` and `Varint.decode` work on single varints. `Varint.encode` is specified for numbers below 2^64. `SPEC.md` says what each one does. @@ -29,28 +29,29 @@ The statements are in `Spec.lean`. The definitions they use, written from the en | Claim | Theorem | |-------|---------| -| The encoder writes the shortest varint. | `Spec.varint_encode_eq` | +| For numbers below 2^64, the encoder writes the shortest varint. | `Spec.varint_encode_eq` | | The varint decoder reads exactly one varint of up to ten bytes from the front of its input, leaves the rest untouched, and refuses everything else. That includes input that ends inside the varint, and an eleventh byte. | `Spec.varint_decode_iff` | -| Decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` | -| `isValid` decides exactly which fields can be written: field numbers 1 to 2^29 - 1, and values that fit their wire type. | `Spec.isValid_iff` | -| The encoder writes each field as the guide describes: the tag, then the payload, every varint in its shortest form. | `Spec.encode_eq` | -| `decode` returns a field list exactly when the bytes split into records, one per field, in order. So it reads every well-formed message and returns the fields as written. It refuses everything else: a record cut short, a length past the end, field number 0, a group, an unknown wire type, and an oversized tag or length. | `Spec.decode_iff` | -| Decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` | +| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` | +| `isValid` decides exactly which fields can be written: field numbers 1 to 2^29 - 1, values that fit their wire type, and bytes shorter than 2^31 - 16. | `Spec.isValid_iff` | +| For valid fields, the encoder writes each field as the guide describes: the tag, then the payload, every varint in its shortest form. | `Spec.encode_eq` | +| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules in `SPEC.md`. So it reads every message made of `VARINT`, `I64`, `LEN` and `I32` records with field numbers from 1 to 2^29 - 1, and returns the fields as written. It refuses everything else: a record cut short, a length past the end, field number 0, a group, an unknown wire type, and an oversized tag or length. | `Spec.decode_iff` | +| For valid fields, decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` | | Every field the decoder returns can be written again. | `Spec.decode_valid` | -| The guide's worked examples, and the edge and refusal cases listed in `SPEC.md`. | `Spec.guide_vectors`, `Spec.edge_vectors`, `Spec.reject_vectors` | +| The guide's worked bytes (1, 150 and -2 as varints, and its messages `Test1` to `Test4`), and the edge and refusal cases listed in `SPEC.md`. | `Spec.guide_vectors`, `Spec.edge_vectors`, `Spec.reject_vectors` | The command-line tool in `Main.lean` calls these functions directly. ## What is not proved -- Reading requests and printing answers in `Main.lean`: the hex and decimal parsing and printing, and the request format. The differential tests cover them, with malformed requests. -- Groups (wire types 3 and 4) are refused, although both reference parsers read them. They are deprecated in the encoding guide and left for a later slice. +- Reading requests and printing answers in `Main.lean`: the hex and decimal parsing and printing, and the request format. The differential tests cover them, with malformed requests and CR LF line endings. +- Groups (wire types 3 and 4) are refused, although the encoding guide still describes them and both reference parsers read them. The guide calls them deprecated; they are left for a later slice. - Where the two reference parsers disagree, this decoder takes the stricter reading: - - it refuses field number 0, which upb reads; - - it refuses a tag of 2^32 or more, which the C++ parser reads by dropping the high bits. + - it refuses field number 0, which upb reads; the guide does not forbid it, but the language guide's field numbers start at 1; + - it refuses a tag of 2^32 or more, which the C++ parser reads by dropping the high bits; + - it refuses a `LEN` length of 2^31 - 16 or more, which upb reads. The tests cannot reach this case, since it needs an input of 2 GiB, so it rests on the proof alone. - What fields mean. Schemas, `.proto` files, field types such as signed or zigzag integers, floats, strings, nested messages and packed repeated fields all sit above the wire format. A `LEN` field's bytes are returned as they are. -- Limits on message size and nesting that a program may want. The decoder reads any input in memory. A `LEN` field must be shorter than 2^31 bytes, as in the reference parsers. -- Speed. The code works on lists of bytes, which suits proofs, not bulk data. +- Limits on message size that a program may want. The decoder reads any input in memory. +- Speed. The code works on lists of bytes, which suits proofs, not bulk data. Decoding takes time in proportion to the input's length. ## What you must trust diff --git a/SPEC.md b/SPEC.md index 679c8fb..0ed95f4 100644 --- a/SPEC.md +++ b/SPEC.md @@ -34,28 +34,31 @@ The decoder refuses everything else: - field number 0; - wire types 3 and 4, which are groups; - wire types 6 and 7, which do not exist; -- a length longer than five bytes, of 2^31 or more, or running past the end of the input; +- a length longer than five bytes, of 2^31 - 16 or more, or running past the end of the input; - any record cut short. Groups are deprecated in the guide and outside this first slice. -The two reference parsers differ in two places, and this library takes the stricter reading in both: +The two reference parsers differ in three places, and this library takes the stricter reading in each: -- upb reads field number 0, which the C++ parser refuses. +- upb reads field number 0, which the C++ parser refuses. The encoding guide does not forbid field number 0, but the language guide's field numbers start at 1. - The C++ parser reads a five-byte tag of 2^32 or more by dropping its high bits, which upb refuses. +- upb reads a `LEN` length up to 2^31 - 1, while the C++ parser refuses one of 2^31 - 16 or more. The encoding guide says a message must be smaller than 2 GiB. `Field.isValid` says which fields the encoder can write: - a field number from 1 to 2^29 - 1; - a `VARINT` or `I64` value below 2^64; - an `I32` value below 2^32; -- `LEN` bytes shorter than 2^31. +- `LEN` bytes shorter than 2^31 - 16. + +`encode` and `Varint.encode` are specified only for valid fields and for numbers below 2^64. For anything else they write bytes that do not read back as what was given, so a program checks `Field.isValid` first, as the command-line tool does. ## Messages `encode` writes each field in turn: the shortest varint for its tag, then its payload, with any varint in its shortest form. -`decode` reads records until the input ends and returns the fields in order. A field number may repeat, and the order is kept. The empty input is the empty message. If any record is malformed, the whole input is refused. `decode` never returns part of a message. +`decode` reads records until the input ends and returns the fields in order. A field number may repeat, and the order is kept. The empty input is the empty message. If any record is malformed, the whole input is refused. `decode` never returns part of a message. Each length check looks at no more of the input than the field needs, so decoding takes time in proportion to the input's length. ## The command-line tool @@ -67,23 +70,24 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | Property | Theorem | |----------|---------| -| The encoder writes the shortest varint. | `Spec.varint_encode_eq` | +| For numbers below 2^64, the encoder writes the shortest varint. | `Spec.varint_encode_eq` | | The varint decoder reads exactly one varint of up to ten bytes from the front of its input, keeps the rest untouched, and refuses everything else. | `Spec.varint_decode_iff` | -| Decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` | +| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` | | `isValid` decides exactly which fields can be written. | `Spec.isValid_iff` | -| The encoder writes each field as the guide describes. | `Spec.encode_eq` | +| For valid fields, the encoder writes each field as the guide describes. | `Spec.encode_eq` | | `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules above. | `Spec.decode_iff` | -| Decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` | +| For valid fields, decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` | | Every field the decoder returns can be written again. | `Spec.decode_valid` | -| The guide's worked examples: 1, 150 and 2^64 - 1 as varints, and four small messages. | `Spec.guide_vectors` | -| Fixed-width values are little-endian, varints need not be in shortest form, ten-byte varints drop bits past the 64th, and the largest field number reads. | `Spec.edge_vectors` | -| The decoder refuses each kind of malformed input listed above. | `Spec.reject_vectors` | +| The guide's worked bytes: 1, 150 and -2 as varints, and its messages `Test1` to `Test4`. | `Spec.guide_vectors` | +| 2^64 - 1 is ten bytes, fixed-width values are little-endian, varints need not be in shortest form, ten-byte varints drop bits past the 64th, the largest field number reads, and so does the empty message. | `Spec.edge_vectors` | +| The decoder refuses each kind of malformed input listed above, except a length of 2^31 - 16 or more, which needs a 2 GiB input; `Spec.decode_iff` covers it. | `Spec.reject_vectors` | Together, these fix every output. - `decode` is fixed for every input. - `encode` and `Varint.encode` are fixed for every valid input. - A decoder that accepted nothing would meet `Spec.decode_valid`, but it would fail `Spec.decode_iff` and `Spec.decode_encode`. +- `encode` is not fixed for fields that are not valid. - A decoder that accepted too much would fail `Spec.decode_iff`. ## Oracle diff --git a/Spec.lean b/Spec.lean index 9bbea67..135ee17 100644 --- a/Spec.lean +++ b/Spec.lean @@ -46,9 +46,11 @@ theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : Protobuf.encode fs = Spec.encode fs := sorry /-- `decode` returns `fs` exactly when the bytes split into records, one - per field of `fs`, in order. So it accepts every well-formed message, - refuses everything else (a record cut short, a length past the end, - field number 0, a group, an unknown wire type), and returns the + per field of `fs`, in order, by the rules of `Spec.FieldBytes`. So it + reads every message made of `VARINT`, `I64`, `LEN` and `I32` records + with field numbers from 1 to 2^29 - 1, refuses everything else (a + record cut short, a length past the end, field number 0, a group, an + unknown wire type, an oversized tag or length), and returns the fields as written. -/ theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) : decode bs = some fs ↔ Spec.Message bs fs := sorry @@ -63,27 +65,31 @@ theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = s /-! ## Test vectors -/ -/-- The encoding guide's examples: 1, 150, and the largest 64-bit value - as varints, and the messages with field 1 set to 150, field 2 set - to "testing", field 3 holding the first message, and the packed - field 4 holding 3, 270 and 86942. -/ +/-- The encoding guide's worked bytes: 1 and 150 as varints, -2 as a + ten-byte varint (2^64 - 2 unsigned), and the messages `Test1` with + field 1 set to 150, `Test2` with field 2 set to "testing", `Test3` + holding the first message in field 3, and `Test4` with field 4 set + to "hello" and field 5 packed with 1, 2 and 3. -/ theorem Spec.guide_vectors : Varint.encode 1 = [0x01] ∧ Varint.encode 150 = [0x96, 0x01] ∧ - Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 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, 0x06, 0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05] = - some [⟨4, .len [0x03, 0x8e, 0x02, 0x9e, 0xa7, 0x05]⟩] ∧ + 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] := sorry -/-- Fixed-width values are little-endian, and the reference parsers' - readings of unusual varints: not in shortest form, and ten bytes - with bits past the 64th. -/ +/-- Cases the guide does not work through: the largest 64-bit value is + ten bytes; fixed-width values are little-endian; the reference + parsers' readings of unusual varints, not in shortest form, and ten + bytes with bits past the 64th; the largest field number; and the + empty message. -/ 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⟩] ∧ @@ -95,8 +101,9 @@ theorem Spec.edge_vectors : /-- Input the decoder refuses: a varint cut short, an eleventh varint byte, field number 0, a length past the end, fixed-width values cut - short, a group, wire types 6 and 7, a tag of 2^32 or more, and a tag - or length longer than five bytes. -/ + short, a group start and a group end, wire types 6 and 7, a tag of + 2^32 or more (from exactly 2^32, which would be field number 2^29), + and a tag or length longer than five bytes. -/ theorem Spec.reject_vectors : decode [0x08] = none ∧ decode [0x08, 0x80] = none ∧ @@ -106,8 +113,10 @@ theorem Spec.reject_vectors : 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 := sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean index cd62d47..b7c213b 100644 --- a/Spec/Defs.lean +++ b/Spec/Defs.lean @@ -85,20 +85,25 @@ varint formed from the field number and the wire type via the formula type has a dynamic length, specified by a varint immediately after the tag, which is followed by the payload as usual." -Field numbers run from 1 to 2^29 - 1, and a message is under 2 GiB. The -reference parsers read a tag or a length as a varint of at most five -bytes, refuse a tag of 2^32 or more and a length of 2^31 or more, and -refuse field number 0. Groups, wire types 3 and 4, are deprecated and +The language guide gives field numbers from 1 to 2^29 - 1, and the +encoding guide says "Protos must be smaller than 2 GiB when serialized". +Both reference parsers read a tag or a length as a varint of at most +five bytes. Where they disagree, this specification takes the stricter +reading: upb reads field number 0 and the C++ parser refuses it; the C++ +parser reads a tag of 2^32 or more by dropping its high bits and upb +refuses it; upb reads a length up to 2^31 - 1 and the C++ parser refuses +one of 2^31 - 16 or more. Groups, wire types 3 and 4, are deprecated and outside this library; wire types 6 and 7 do not exist. -/ /-- A field the encoder can write: a field number from 1 to 2^29 - 1, - and a value that fits its wire type. -/ + and a value that fits its wire type, with bytes the C++ parser + reads. -/ def Spec.ValidField (f : Field) : Prop := 1 ≤ f.number ∧ f.number < 2 ^ 29 ∧ match f.value with | .varint v => v < 2 ^ 64 | .i64 v => v < 2 ^ 64 - | .len d => d.length < 2 ^ 31 + | .len d => d.length < 2 ^ 31 - 16 | .i32 v => v < 2 ^ 32 /-- `tag` then `payload` are the bytes of field `f`. -/ @@ -110,7 +115,7 @@ def Spec.FieldBytes (tag payload : List UInt8) (f : Field) : Prop := | 1, .i64 v => payload.length = 8 ∧ v = Spec.leValue payload | 2, .len d => ∃ pre, payload = pre ++ d ∧ Spec.VarintShape 5 pre ∧ Spec.groupsValue pre = d.length ∧ - d.length < 2 ^ 31 + d.length < 2 ^ 31 - 16 | 5, .i32 v => payload.length = 4 ∧ v = Spec.leValue payload | _, _ => False diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 525e9b4..c3ee039 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -6,10 +6,11 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261025 - Inputs: 200000 -- Mutated: 77137 of the inputs are mutated encodings -- By kind: decode mutated 77137, decode random 18392, decode valid 46010, encode 46010, encode invalid 12436, error 15 -- Messages decoded: 141539, of which 73247 read by both reference parsers alike and 68292 refused -- Refused although a reference parser reads them: a five-byte tag of 2^32 or more, which C++ reads and upb refuses 1253, a group, which both read 1022, field number 0, which upb reads and C++ refuses 1700 -- Malformed requests answered `error`: 15 of 15 -- Last lines with no LF, sent alone, answered right: 2 of 2 +- Mutated: 77017 of the inputs are mutated encodings +- By kind: decode mutated 77017, decode random 18395, decode valid 46084, encode 46084, encode invalid 12402, error 18 +- Messages decoded: 141496, of which 73280 read by both reference parsers alike and 68216 refused +- Refused although a reference parser reads them: a five-byte tag of 2^32 or more, which C++ reads and upb refuses 650, a group, which both read 981, field number 0, which upb reads and C++ refuses 1688 +- Malformed requests answered `error`: 18 of 18 +- Requests ending in CR LF: every seventh, 28571 +- Last lines sent alone, with no LF or with CR LF, answered right: 3 of 3 - Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py index 4b57a29..7e0c85d 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -33,12 +33,14 @@ - field lists the encoder must refuse; - malformed requests, which the tool must answer with `error`. -For every input the Lean answer must equal the oracle's. +Every seventh request ends in CR LF. For every input the Lean answer +must equal the oracle's, and the two parsers must disagree only in the +known ways. python3 tests/run_tests.py [--seed N] [--count N] -It needs `protobuf` and `grpcio-tools` at the versions below. When they -are missing it creates a virtual environment in `.lake/oracle-venv`, +It needs `protobuf` and `grpcio-tools` at the versions below, with +protobuf on its upb backend. When they are missing it creates a virtual environment in `.lake/oracle-venv`, installs them there, and runs itself again with it; where Python cannot make one, it installs them into `.lake/oracle-packages` instead. It builds the executable, writes tests/TEST-RESULTS.md, and exits non-zero if any @@ -73,24 +75,39 @@ def ensure_oracles(): versions into a virtual environment and run again with it; where a virtual environment cannot be made, install them into a folder instead and import them from there.""" - try: - import google.protobuf # noqa: F401 - import grpc_tools # noqa: F401 + if oracles_ready(): return - except ImportError: - pass if os.environ.get("PROTOWIRE_ORACLE_VENV"): - sys.exit("the oracle packages did not import even in .lake/oracle-venv") + sys.exit("the pinned oracle packages, with the upb backend, are not usable even in " + ".lake/oracle-venv") python = VENV / "bin" / "python" made = python.exists() or subprocess.run( [sys.executable, "-m", "venv", str(VENV)], capture_output=True).returncode == 0 if made and not os.environ.get("PROTOWIRE_NO_VENV"): subprocess.run([str(python), "-m", "pip", "install", "--quiet", *PINS], check=True) env = dict(os.environ, PROTOWIRE_ORACLE_VENV="1") + env.pop("PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION", None) os.execve(str(python), [str(python), *sys.argv], env) subprocess.run([sys.executable, "-m", "pip", "install", "--quiet", "--break-system-packages", "--target", str(PKGS), *PINS], check=True) sys.path.insert(0, str(PKGS)) + os.environ.pop("PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION", None) + for name in [m for m in sys.modules if m.startswith(("google", "grpc_tools"))]: + del sys.modules[name] + if not oracles_ready(): + sys.exit("the pinned oracle packages, with the upb backend, are not usable") + + +def oracles_ready(): + """Whether the pinned oracle versions import, with protobuf on upb.""" + from importlib.metadata import PackageNotFoundError, version + try: + import grpc_tools # noqa: F401 + from google.protobuf.internal import api_implementation + versions = [f"{p.split('==')[0]}=={version(p.split('==')[0])}" for p in PINS] + except (ImportError, PackageNotFoundError): + return False + return versions == PINS and api_implementation.Type() == "upb" # The oracles. @@ -325,8 +342,9 @@ def mutate(rng, data): rec += varint(random_number(rng) * 8) + varint(5) + varint(n * 8 + 4) b = bytearray(rec) + b elif op == 9: - # A five-byte tag of 2^32 or more. - t = rng.randint(2 ** 32, 2 ** 35 - 1) + # A five-byte tag of 2^32 or more, often exactly 2^32 plus a wire + # type: field number 2^29, one past the largest. + t = rng.choice([2 ** 32 + rng.choice([0, 1, 2, 5]), rng.randint(2 ** 32, 2 ** 35 - 1)]) b = bytearray(long_varint(t, 5) + varint(1)) + b else: # A length varint longer than it needs to be, or past the end. @@ -372,9 +390,13 @@ def invalid_fields(rng): ("encode 1:len:0", "odd hex in a len value"), ("encode x:varint:1", "a field number that is not a number"), (" decode 00", "a leading space"), + ("", "an empty line"), + ("decode 0896\r01", "a CR inside the request"), + ("encode 1:varint:" + "1" * 31, "a number of more than 30 digits"), ] -AT_EOF = [("decode 089601", "OK\t1:varint:150"), ("encode 1:varint:150", "089601")] +AT_EOF = [("decode 089601", "OK\t1:varint:150"), ("encode 1:varint:150", "089601"), + ("decode 089601\r\n", "OK\t1:varint:150")] def fields_text(fields): @@ -472,7 +494,9 @@ def drain(stream, buf, cap): def oracle(): from importlib.metadata import version - return (f"Python {platform.python_version()}, protobuf {version('protobuf')} (upb), " + from google.protobuf.internal import api_implementation + return (f"Python {platform.python_version()}, protobuf {version('protobuf')} " + f"({api_implementation.Type()}), " f"grpcio-tools {version('grpcio-tools')} (protoc --decode_raw, C++)") @@ -518,13 +542,21 @@ def main(): tally = {} items = list(cases(args.seed, args.count, tally)) - out, problem = run_tool("".join(req + "\n" for _, req, _, _ in items)) + # Every seventh request ends in CR LF, which the tool must take as LF. + out, problem = run_tool("".join(req + ("\r\n" if i % 7 == 6 else "\n") + for i, (_, req, _, _) in enumerate(items))) failures = [("(whole run)", "a clean run", problem)] if problem else [] for item, got in itertools.zip_longest(items, out): if item is None: failures.append(("(no request)", "nothing", got)) elif got != item[2]: failures.append((item[1], item[2], "(no answer)" if got is None else got)) + # The two parsers may disagree only in the ways the module comment + # names; any other disagreement means an oracle changed. + for reason, n in tally.items(): + if reason.startswith("other") or reason.startswith("C++ and upb read different"): + failures.append((f"{n} inputs", "only the known disagreements", reason)) + eof_right = 0 for req, want in AT_EOF: got, problem = run_tool(req, timeout=60) @@ -558,7 +590,9 @@ def main(): (", ".join(f"{k} {v}" for k, v in sorted(tally.items())) or "none"), f"- Malformed requests answered `error`: {malformed.count('error')} of " f"{by_label.get('error', 0)}", - f"- Last lines with no LF, sent alone, answered right: {eof_right} of {len(AT_EOF)}", + f"- Requests ending in CR LF: every seventh, {len(items) // 7}", + f"- Last lines sent alone, with no LF or with CR LF, answered right: {eof_right} of " + f"{len(AT_EOF)}", f"- Failures: {len(failures)}", "", ] From 584f02f681a163cc443ce2a7e9044dfdfb904d33 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 13:41:21 +0000 Subject: [PATCH 3/4] Record the planted bugs tests/planted_bugs.py plants ten small bugs in a copy of the code and runs the tests on 20,000 inputs against each. tests/PLANTED-BUGS.md records the result. The tests catch nine. The tenth drops the LEN length limit, which only a 2 GiB input could show, so its entry says why the tests miss it and the script does not fail on it. The limit rests on Spec.decode_iff. The script is added to the test files in bar.toml, and the README names the record. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 2 +- bar.toml | 2 +- tests/PLANTED-BUGS.md | 91 ++++++++++++++++++++++++++++ tests/planted_bugs.py | 138 ++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 231 insertions(+), 2 deletions(-) create mode 100644 tests/PLANTED-BUGS.md create mode 100644 tests/planted_bugs.py diff --git a/README.md b/README.md index 752e664..50428b2 100644 --- a/README.md +++ b/README.md @@ -77,7 +77,7 @@ python3 tests/run_tests.py `lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. -The test script installs the pinned oracle packages into `.lake/oracle-venv` when they are missing. It then compares the tool with upb and with the C++ parser on inputs from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. +The test script installs the pinned oracle packages into `.lake/oracle-venv` when they are missing. It then compares the tool with upb and with the C++ parser on inputs from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. `tests/planted_bugs.py` plants ten small bugs in a copy of the code, and `tests/PLANTED-BUGS.md` records that the tests catch nine; the tenth, a missing `LEN` length limit, needs a 2 GiB input to show, so it rests on `Spec.decode_iff`. ## Layout diff --git a/bar.toml b/bar.toml index ae0c17f..41dbccb 100644 --- a/bar.toml +++ b/bar.toml @@ -32,4 +32,4 @@ code = [ [tests] results = "tests/TEST-RESULTS.md" command = "python3 tests/run_tests.py" -files = ["tests/run_tests.py"] +files = ["tests/run_tests.py", "tests/planted_bugs.py"] diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md new file mode 100644 index 0000000..81dfae8 --- /dev/null +++ b/tests/PLANTED-BUGS.md @@ -0,0 +1,91 @@ +# Planted bugs + +Written by `python3 tests/planted_bugs.py`. Each row is one small change to the +code, made in a copy. The tests ran on 20,000 inputs from their recorded seed +against the changed tool. A bug is caught when they report failures. + +| Bug | File | Failures | +|-----|------|----------| +| Field number 0 read | `Protobuf/Wire.lean` | 170 | +| Tags of 2^32 or more read | `Protobuf/Wire.lean` | 174 | +| A tag of exactly 2^32 read | `Protobuf/Wire.lean` | 88 | +| Six-byte tags read | `Protobuf/Wire.lean` | 133 | +| Eleven-byte varints read | `Protobuf/Varint.lean` | 70 | +| Bits past the 64th kept | `Protobuf/Varint.lean` | 23 | +| No LEN length limit | `Protobuf/Wire.lean` | 0, not caught by the tests: it shows only when a length of 2^31 - 16 or more is followed by that many bytes, an input of about 2 GiB; a shorter input with such a length is refused for running out of input either way. `Spec.decode_iff` covers the limit. | +| Groups read as empty LEN fields | `Protobuf/Wire.lean` | 150 | +| isValid takes field number 2^29 | `Protobuf/Wire.lean` | 90 | +| CR kept at the end of a CR LF request | `Main.lean` | 2856 | + +## The changes + +**Field number 0 read** in `Protobuf/Wire.lean`: + +``` +- if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none ++ if 2 ^ 32 ≤ t then none +``` + +**Tags of 2^32 or more read** in `Protobuf/Wire.lean`: + +``` +- if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none ++ if t / 8 = 0 then none +``` + +**A tag of exactly 2^32 read** in `Protobuf/Wire.lean`: + +``` +- if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none ++ if 2 ^ 32 < t ∨ t / 8 = 0 then none +``` + +**Six-byte tags read** in `Protobuf/Wire.lean`: + +``` +- match Varint.decodeAux 5 bs with ++ match Varint.decodeAux 6 bs with +``` + +**Eleven-byte varints read** in `Protobuf/Varint.lean`: + +``` +- match decodeAux 10 bs with ++ match decodeAux 11 bs with +``` + +**Bits past the 64th kept** in `Protobuf/Varint.lean`: + +``` +- | some (v, rest) => some (v % 2 ^ 64, rest) ++ | some (v, rest) => some (v, rest) +``` + +**No LEN length limit** in `Protobuf/Wire.lean`: + +``` +- if 2 ^ 31 - 16 ≤ len ∨ (rest.take len).length < len then none ++ if (rest.take len).length < len then none +``` + +**Groups read as empty LEN fields** in `Protobuf/Wire.lean`: + +``` +- | _ => none ++ | 3 => some (⟨n, .len []⟩, rest) ++ | _ => none +``` + +**isValid takes field number 2^29** in `Protobuf/Wire.lean`: + +``` +- 1 ≤ f.number && f.number < 2 ^ 29 && ++ 1 ≤ f.number && f.number ≤ 2 ^ 29 && +``` + +**CR kept at the end of a CR LF request** in `Main.lean`: + +``` +- String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) ++ String.ofList cs +``` diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py new file mode 100644 index 0000000..f7f4cf5 --- /dev/null +++ b/tests/planted_bugs.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Plant each bug below in a copy of the code, and check the tests catch it. + +A planted bug is a small change to the code, of a kind a person could +make by mistake: to the code under proof, or to the request handling in +Main.lean. For each one, this script copies the project into a temporary +directory, makes the change there, builds the command-line tool, and +runs the differential tests on a given number of inputs. The tests catch +the bug when they report failures. The proofs would catch every change +to the code under proof too, since that code no longer meets its +statements; Main.lean is outside the proofs. This script checks the +tests on their own, so it builds only the tool, not the proofs. + +The project itself is never changed. The script writes the results to +tests/PLANTED-BUGS.md, and exits with 1 if a bug is not caught and its +entry gives no reason. Some bugs no test here can catch: an equivalent +change gives the same answer on every input, and some changes show only +on an input too large to send. Such an entry says why the tests miss it. + +Usage: python3 tests/planted_bugs.py [--count N] +""" + +import argparse +import re +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = "protowire" # the lake target of the command-line tool +COUNT = 20_000 + +# (name, file, text to replace, replacement, why the tests cannot catch it or None) +BUGS = [ + ("Field number 0 read", "Protobuf/Wire.lean", + "if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none", + "if 2 ^ 32 ≤ t then none", None), + ("Tags of 2^32 or more read", "Protobuf/Wire.lean", + "if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none", + "if t / 8 = 0 then none", None), + ("A tag of exactly 2^32 read", "Protobuf/Wire.lean", + "if 2 ^ 32 ≤ t ∨ t / 8 = 0 then none", + "if 2 ^ 32 < t ∨ t / 8 = 0 then none", None), + ("Six-byte tags read", "Protobuf/Wire.lean", + " match Varint.decodeAux 5 bs with", + " match Varint.decodeAux 6 bs with", None), + ("Eleven-byte varints read", "Protobuf/Varint.lean", + " match decodeAux 10 bs with", + " match decodeAux 11 bs with", None), + ("Bits past the 64th kept", "Protobuf/Varint.lean", + "| some (v, rest) => some (v % 2 ^ 64, rest)", + "| some (v, rest) => some (v, rest)", None), + ("No LEN length limit", "Protobuf/Wire.lean", + "if 2 ^ 31 - 16 ≤ len ∨ (rest.take len).length < len then none", + "if (rest.take len).length < len then none", + "it shows only when a length of 2^31 - 16 or more is followed by that many bytes, " + "an input of about 2 GiB; a shorter input with such a length is refused for running " + "out of input either way. `Spec.decode_iff` covers the limit."), + ("Groups read as empty LEN fields", "Protobuf/Wire.lean", + " | _ => none", + " | 3 => some (⟨n, .len []⟩, rest)\n | _ => none", None), + ("isValid takes field number 2^29", "Protobuf/Wire.lean", + "1 ≤ f.number && f.number < 2 ^ 29 &&", + "1 ≤ f.number && f.number ≤ 2 ^ 29 &&", None), + ("CR kept at the end of a CR LF request", "Main.lean", + " String.ofList (if cs.getLast? = some '\\r' then cs.dropLast else cs)", + " String.ofList cs", None), +] + + +def failures(out): + m = re.search(r"(\d+) failures?", out) + return int(m.group(1)) if m else None + + +def run(count): + rows = [] + with tempfile.TemporaryDirectory() as tmp: + work = Path(tmp) / "project" + shutil.copytree(ROOT, work, ignore=shutil.ignore_patterns(".git")) + for name, rel, old, new, missed in BUGS: + path = work / rel + original = (ROOT / rel).read_text() + if original.count(old) != 1: + sys.exit(f"{name}: the text to replace is not in {rel} exactly once") + path.write_text(original.replace(old, new)) + build = subprocess.run(["lake", "build", EXE], cwd=work, capture_output=True, text=True) + if build.returncode != 0: + path.write_text(original) + sys.exit(f"{name}: the tool does not build with this change\n{build.stdout[-2000:]}") + test = subprocess.run([sys.executable, "tests/run_tests.py", "--count", str(count)], + cwd=work, capture_output=True, text=True) + path.write_text(original) + n = failures(test.stdout + test.stderr) + rows.append((name, rel, old, new, missed, n)) + print(f"{name}: {n} failures", flush=True) + return rows + + +def write(rows, count): + lines = [ + "# Planted bugs", + "", + "Written by `python3 tests/planted_bugs.py`. Each row is one small change to the", + f"code, made in a copy. The tests ran on {count:,} inputs from their recorded seed", + "against the changed tool. A bug is caught when they report failures.", + "", + "| Bug | File | Failures |", + "|-----|------|----------|", + ] + for name, rel, _, _, missed, n in rows: + cell = str(n) if n else ("0, not caught by the tests: " + missed if missed + else "0, NOT CAUGHT") + lines.append(f"| {name} | `{rel}` | {cell} |") + lines += ["", "## The changes", ""] + for name, rel, old, new, _, _ in rows: + lines += [f"**{name}** in `{rel}`:", "", "```", "- " + old.replace("\n", "\n- "), + "+ " + new.replace("\n", "\n+ "), "```", ""] + (ROOT / "tests" / "PLANTED-BUGS.md").write_text("\n".join(lines)) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--count", type=int, default=COUNT) + args = ap.parse_args() + rows = run(args.count) + write(rows, args.count) + missed = [r[0] for r in rows if not r[5] and not r[4]] + caught = sum(1 for r in rows if r[5]) + print(f"{caught} of {len(rows)} planted bugs caught; results in tests/PLANTED-BUGS.md") + if missed: + sys.exit("not caught: " + ", ".join(missed)) + + +if __name__ == "__main__": + main() From 1fde088185d42131f4b715b9fd9976a8dff4094a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 13:53:45 +0000 Subject: [PATCH 4/4] Name the group bug for what it plants, and stop on a missing count The planted change reads a group's start tag as an empty LEN field; an end tag is still refused. Its name now says so. The script now stops when a test run prints no failure count, so a broken run cannot pass as a real 0. The docstring says which changes the proofs rule out, and the README's layout names the script. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- README.md | 1 + tests/PLANTED-BUGS.md | 4 ++-- tests/planted_bugs.py | 10 ++++++---- 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 50428b2..4c3886f 100644 --- a/README.md +++ b/README.md @@ -92,3 +92,4 @@ The test script installs the pinned oracle packages into `.lake/oracle-venv` whe - `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. - `SPEC.md`: the specification in plain words. - `tests/run_tests.py`: the differential tests. +- `tests/planted_bugs.py`: plants small bugs in a copy of the code, and records in `tests/PLANTED-BUGS.md` whether the tests catch each one. diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md index 81dfae8..3cdb2e0 100644 --- a/tests/PLANTED-BUGS.md +++ b/tests/PLANTED-BUGS.md @@ -13,7 +13,7 @@ against the changed tool. A bug is caught when they report failures. | Eleven-byte varints read | `Protobuf/Varint.lean` | 70 | | Bits past the 64th kept | `Protobuf/Varint.lean` | 23 | | No LEN length limit | `Protobuf/Wire.lean` | 0, not caught by the tests: it shows only when a length of 2^31 - 16 or more is followed by that many bytes, an input of about 2 GiB; a shorter input with such a length is refused for running out of input either way. `Spec.decode_iff` covers the limit. | -| Groups read as empty LEN fields | `Protobuf/Wire.lean` | 150 | +| A group start tag read as an empty LEN field | `Protobuf/Wire.lean` | 150 | | isValid takes field number 2^29 | `Protobuf/Wire.lean` | 90 | | CR kept at the end of a CR LF request | `Main.lean` | 2856 | @@ -68,7 +68,7 @@ against the changed tool. A bug is caught when they report failures. + if (rest.take len).length < len then none ``` -**Groups read as empty LEN fields** in `Protobuf/Wire.lean`: +**A group start tag read as an empty LEN field** in `Protobuf/Wire.lean`: ``` - | _ => none diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py index f7f4cf5..00431ee 100644 --- a/tests/planted_bugs.py +++ b/tests/planted_bugs.py @@ -6,9 +6,9 @@ Main.lean. For each one, this script copies the project into a temporary directory, makes the change there, builds the command-line tool, and runs the differential tests on a given number of inputs. The tests catch -the bug when they report failures. The proofs would catch every change -to the code under proof too, since that code no longer meets its -statements; Main.lean is outside the proofs. This script checks the +the bug when they report failures. A change that alters an answer of +the code under proof also breaks the proofs, since that code no longer +meets its statements; Main.lean is outside the proofs. This script checks the tests on their own, so it builds only the tool, not the proofs. The project itself is never changed. The script writes the results to @@ -58,7 +58,7 @@ "it shows only when a length of 2^31 - 16 or more is followed by that many bytes, " "an input of about 2 GiB; a shorter input with such a length is refused for running " "out of input either way. `Spec.decode_iff` covers the limit."), - ("Groups read as empty LEN fields", "Protobuf/Wire.lean", + ("A group start tag read as an empty LEN field", "Protobuf/Wire.lean", " | _ => none", " | 3 => some (⟨n, .len []⟩, rest)\n | _ => none", None), ("isValid takes field number 2^29", "Protobuf/Wire.lean", @@ -94,6 +94,8 @@ def run(count): cwd=work, capture_output=True, text=True) path.write_text(original) n = failures(test.stdout + test.stderr) + if n is None: + sys.exit(f"{name}: the tests gave no failure count\n{(test.stdout + test.stderr)[-2000:]}") rows.append((name, rel, old, new, missed, n)) print(f"{name}: {n} failures", flush=True) return rows