From bf7837ebee4e577843d35f233ef03ebb8c9ffcc2 Mon Sep 17 00:00:00 2001 From: shah Date: Sun, 25 Oct 2026 10:42:28 -0500 Subject: [PATCH 1/2] Add Protobuf wire format codec, with proved round trips --- .gitignore | 2 + Main.lean | 176 +++++++++++++ Proofs.lean | 2 + Proofs/Examples.lean | 98 ++++++++ Proofs/RoundTrip.lean | 259 +++++++++++++++++++ Protobuf.lean | 1 + Protobuf/Verify.lean | 22 ++ Protobuf/Wire.lean | 202 +++++++++++++++ README.md | 139 +++++++++- SPEC.md | 173 +++++++++++++ lake-manifest.json | 5 + lakefile.toml | 13 + lean-toolchain | 1 + tests/TEST-RESULTS.md | 35 +++ tests/run_tests.py | 574 ++++++++++++++++++++++++++++++++++++++++++ 15 files changed, 1701 insertions(+), 1 deletion(-) create mode 100644 .gitignore create mode 100644 Main.lean create mode 100644 Proofs.lean create mode 100644 Proofs/Examples.lean create mode 100644 Proofs/RoundTrip.lean create mode 100644 Protobuf.lean create mode 100644 Protobuf/Verify.lean create mode 100644 Protobuf/Wire.lean create mode 100644 SPEC.md 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/.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..15f22da --- /dev/null +++ b/Main.lean @@ -0,0 +1,176 @@ +/- + Command line front end for the Protobuf wire format codec. + + One request per line, in the shape `op numbers`, where the op + and the numbers are parted by one space, and the numbers are + decimal numbers parted by commas, with no spaces inside the + number list. A line holds a number in plain decimal: no sign, + no leading zeros (the number 0 itself is written `0`), and at + most twenty digits. An empty line is passed over with no + answer. A request that breaks the line shape prints `error`. + + The operations: + + - `venc` takes one number, the value to encode, below 2^64, + and prints its varint bytes as comma parted decimal numbers. + - `vdec` takes comma parted byte numbers and prints `ok:` and + the value when the bytes are exactly one varint that this + slice reads, and `none` when they are not. + - `enc` takes a field list in the field list format below and + prints the message bytes as comma parted decimal numbers. + - `dec` takes comma parted byte numbers and prints `ok:` and + the field list in the same format when the bytes are a + message this slice reads, and `none` when they are not. + + The field list format reads the numbers as groups, one group + per field, in field order. A group is: the field number, the + wire type, then the payload. The payload is one number, the + varint value, for wire type 0. It is eight byte numbers for + wire type 1. It is a length number and then that many byte + numbers for wire type 2. It is four byte numbers for wire type + 5. The empty field list is the empty number list. A group that + breaks these rules (a field number of 0 or above 536870911, a + wire type outside 0, 1, 2, 5, a byte number above 255, a varint + value or a length at or above 2^64, or numbers that run out in + the middle of a group) makes the whole request malformed, and + `enc` prints `error`. The full rules are in SPEC.md. +-/ + +import Protobuf + +open Protobuf + +/-- Read one number token: plain decimal digits, no sign, no + leading zeros but for the number 0 itself, at most twenty + digits. -/ +def parseNat (s : String) : Option Nat := + let cs := s.toList + if cs.isEmpty ∨ 20 < cs.length then none + else if 1 < cs.length ∧ cs.head! = '0' then none + else if cs.all Char.isDigit then + some (cs.foldl (fun n c => n * 10 + (c.toNat - 48)) 0) + else none + +/-- Read the number list of a payload. The empty payload is the + empty list. -/ +def numsOf (payload : String) : Option (List Nat) := + if payload.isEmpty then some [] + else (payload.splitOn ",").mapM parseNat + +/-- Read the byte list of a payload: every number at most 255. -/ +def bytesOf (payload : String) : Option (List UInt8) := + (numsOf payload).bind fun ns => + if ns.all (· ≤ 255) then some (ns.map Nat.toUInt8) else none + +/-- Take `n` byte values off the front of a number list. -/ +def takeBytes : Nat → List Nat → Option (List UInt8 × List Nat) + | 0, ts => some ([], ts) + | _ + 1, [] => none + | n + 1, t :: ts => + if t ≤ 255 then + (takeBytes n ts).map fun (bs, rest) => (t.toUInt8 :: bs, rest) + else none + +/-- Read a field list off a number list, group by group, in the + field list format of the header comment. The fuel count is + the number count: each group eats at least two numbers. -/ +def parseFieldTokens : Nat → List Nat → Option (List Field) + | _, [] => some [] + | 0, _ :: _ => none + | fuel + 1, num :: wt :: rest => + if num = 0 ∨ 536870912 ≤ num then none + else if wt = 0 then + match rest with + | v :: rest' => + if v < 18446744073709551616 then + (parseFieldTokens fuel rest').map (⟨num, .varint v⟩ :: ·) + else none + | [] => none + else if wt = 1 then + (takeBytes 8 rest).bind fun (bs, rest') => + (parseFieldTokens fuel rest').map (⟨num, .fixed64 bs⟩ :: ·) + else if wt = 2 then + match rest with + | len :: rest' => + if len < 18446744073709551616 then + (takeBytes len rest').bind fun (bs, rest'') => + (parseFieldTokens fuel rest'').map (⟨num, .bytes bs⟩ :: ·) + else none + | [] => none + else if wt = 5 then + (takeBytes 4 rest).bind fun (bs, rest') => + (parseFieldTokens fuel rest').map (⟨num, .fixed32 bs⟩ :: ·) + else none + | _, _ => none + +/-- The numbers of one field, in the field list format. -/ +def fieldTokens (f : Field) : List Nat := + f.num :: wireType f.value :: match f.value with + | .varint v => [v] + | .fixed64 bs => bs.map UInt8.toNat + | .bytes bs => bs.length :: bs.map UInt8.toNat + | .fixed32 bs => bs.map UInt8.toNat + +/-- Print a number list as comma parted decimal numbers. -/ +def joinNums (ns : List Nat) : String := + ns.foldl (fun acc n => if acc.isEmpty then toString n else acc ++ "," ++ toString n) "" + +/-- Run one operation on one payload. The answer is `error` for a + malformed request, and `none` (as an answer, for the decoders) + for well formed bytes that this slice rejects. -/ +def run (op payload : String) : String := + match op with + | "venc" => + match numsOf payload with + | some [v] => + if v < 18446744073709551616 then + joinNums (List.map UInt8.toNat (encodeVarint v)) + else "error" + | _ => "error" + | "vdec" => + match bytesOf payload with + | none => "error" + | some bs => + match decodeVarint bs with + | some (v, []) => s!"ok:{v}" + | _ => "none" + | "enc" => + match (numsOf payload).bind fun ns => parseFieldTokens ns.length ns with + | some fs => joinNums (List.map UInt8.toNat (encodeMessage fs)) + | none => "error" + | "dec" => + match bytesOf payload with + | none => "error" + | some bs => + match decodeMessage bs with + | some fs => + let ts := fs.flatMap fieldTokens + if ts.isEmpty then "ok:" else "ok:" ++ joinNums ts + | none => "none" + | _ => "error" + +/-- Answer one request line. An empty line gets no answer. -/ +def processLine (line : String) : Option String := + if line.isEmpty then none + else + match line.splitOn " " with + | [op] => some (run op "") + | [op, payload] => some (run op payload) + | _ => some "error" + +/-- The line without its line ending: LF, or CR LF. -/ +def chomp (line : String) : String := + let cs := line.toList + if cs.getLast? = some '\n' then + let cs := cs.dropLast + String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) + else line + +def main : IO Unit := do + let stdin ← IO.getStdin + repeat + let line ← stdin.getLine + if line.isEmpty then break + match processLine (chomp line) with + | some out => IO.println out + | none => pure () diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..447e07d --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,2 @@ +import Proofs.RoundTrip +import Proofs.Examples diff --git a/Proofs/Examples.lean b/Proofs/Examples.lean new file mode 100644 index 0000000..ab08146 --- /dev/null +++ b/Proofs/Examples.lean @@ -0,0 +1,98 @@ +/- + The worked examples from the Protobuf encoding documentation, + proved. The same examples run through the command line tool in + the test harness, where they are checked byte by byte a second + time. + + From the docs: the number 1 encodes as the single byte 1, and + 300 as the two bytes 172 and 2, since 300 is 44 plus two times + 128. The message with field 1 holding the varint 150 encodes as + the bytes 8, 150, 1. The message with field 2 holding the text + "testing" encodes as the tag byte 18, the length 7, and the + seven text bytes. +-/ + +import Protobuf + +namespace Protobuf.Examples + +open Protobuf + +/-- The byte list of the text "testing". -/ +def testingBytes : List UInt8 := [116, 101, 115, 116, 105, 110, 103] + +theorem encodeVarint_one : encodeVarint 1 = [1] := by + rw [encodeVarint_def] + decide + +theorem encodeVarint_300 : encodeVarint 300 = [172, 2] := by + rw [encodeVarint_def, encodeVarint_def] + decide + +theorem decodeVarint_300 : decodeVarint [172, 2] = some (300, []) := by decide + +theorem encodeVarint_150 : encodeVarint 150 = [150, 1] := by + rw [encodeVarint_def, encodeVarint_def] + decide + +/-- A varint of ten bytes with every value bit set is the largest + 64 bit number, and is accepted. -/ +theorem decodeVarint_max : + decodeVarint [255, 255, 255, 255, 255, 255, 255, 255, 255, 1] = + some (18446744073709551615, []) := by decide + +/-- The same ten bytes with 2 in the last byte carry a bit past + 64, and are rejected. -/ +theorem decodeVarint_past64 : + decodeVarint [255, 255, 255, 255, 255, 255, 255, 255, 255, 2] = none := by + decide + +/-- An eleven byte varint is rejected, however it ends. -/ +theorem decodeVarint_eleven : + decodeVarint [128, 128, 128, 128, 128, 128, 128, 128, 128, 128, 1] = + none := by decide + +/-- A varint cut short by the end of the input is rejected. -/ +theorem decodeVarint_cut : decodeVarint [172] = none := by decide + +/-- The docs message example, on the encode side: field 1 with + the varint 150. -/ +theorem encode_test1 : + encodeMessage [⟨1, .varint 150⟩] = [8, 150, 1] := by + have h8 : encodeVarint 8 = [8] := by + rw [encodeVarint_def] + decide + simp [encodeMessage, encodeField, encodeValue, wireType, h8, encodeVarint_150] + +/-- The docs message example, on the decode side. -/ +theorem decode_test1 : + decodeMessage [8, 150, 1] = some [⟨1, .varint 150⟩] := by decide + +/-- The docs string example, on the encode side: field 2 with + the text "testing". -/ +theorem encode_test2 : + encodeMessage [⟨2, .bytes testingBytes⟩] = + [18, 7, 116, 101, 115, 116, 105, 110, 103] := by + have h18 : encodeVarint 18 = [18] := by + rw [encodeVarint_def] + decide + have h7 : encodeVarint 7 = [7] := by + rw [encodeVarint_def] + decide + simp [encodeMessage, encodeField, encodeValue, wireType, testingBytes, h18, h7] + +/-- The docs string example, on the decode side. -/ +theorem decode_test2 : + decodeMessage [18, 7, 116, 101, 115, 116, 105, 110, 103] = + some [⟨2, .bytes testingBytes⟩] := by decide + +/-- A tag with field number zero is rejected. -/ +theorem decode_field_zero : decodeMessage [0, 1] = none := by decide + +/-- A group start tag, wire type 3, is rejected. -/ +theorem decode_group_tag : decodeMessage [27, 1] = none := by decide + +/-- A length that runs past the bytes left is rejected. -/ +theorem decode_length_past : decodeMessage [18, 7, 116, 101] = none := by decide + +end Protobuf.Examples diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..885ed13 --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,259 @@ +/- + The round trip proofs: decoding an encoding gives back what was + encoded, first for one varint, then for one field, then for a + whole message of well formed fields. + + The statements proved here are `decodeVarint_encode` and + `decodeMessage_encode`. A matching statement in a spec file + still has to be added by a reviewer, so this file builds on its + own, in the same shape as the codec and json proofs. + + Helper lemmas live in `Protobuf.Proofs`. +-/ + +import Protobuf + +namespace Protobuf.Proofs + +open Protobuf + +/-- An encoding of a varint always has at least one byte. -/ +theorem encodeVarint_length_pos (n : Nat) : 0 < (encodeVarint n).length := by + rw [encodeVarint_def] + split <;> simp + +/-- A number below `128 ^ (k + 1)` encodes in at most `k + 1` + bytes. -/ +theorem encodeVarint_length_le (k n : Nat) (hn : n < 128 ^ (k + 1)) : + (encodeVarint n).length ≤ k + 1 := by + induction k generalizing n with + | zero => + have h : n < 128 := by simpa using hn + rw [encodeVarint_def, if_pos h] + simp + | succ k ih => + rw [encodeVarint_def] + by_cases h : n < 128 + · rw [if_pos h] + simp + · rw [if_neg h] + simp only [List.length_cons] + have hpow : 128 ^ (k + 1 + 1) = 128 ^ (k + 1) * 128 := by rw [Nat.pow_succ] + rw [hpow] at hn + have hdiv : n / 128 < 128 ^ (k + 1) := by omega + have hle := ih (n / 128) hdiv + omega + +/-- The varint reader, run with fuel at least the length of an + encoding, reads that encoding whole and leaves the rest of the + list alone. Induction on the fuel: each step eats one byte of + the encoding and one unit of fuel. -/ +theorem go_encode (fuel n : Nat) (rest : List UInt8) + (h : (encodeVarint n).length ≤ fuel) : + decodeVarintGo fuel (encodeVarint n ++ rest) = some (n, rest) := by + induction fuel generalizing n rest with + | zero => + have hpos := encodeVarint_length_pos n + omega + | succ fuel ih => + by_cases hn : n < 128 + · have henc : encodeVarint n = [n.toUInt8] := by + rw [encodeVarint_def, if_pos hn] + have h1 : (n.toUInt8).toNat = n := + UInt8.toNat_ofNat_of_lt (show n < 256 by omega) + have hb : n.toUInt8 < 128 := by + rw [UInt8.lt_iff_toNat_lt, h1] + show n < 128 + exact hn + rw [henc] + show decodeVarintGo (fuel + 1) (n.toUInt8 :: rest) = some (n, rest) + rw [decodeVarintGo_cons, if_pos hb, h1] + · have henc : encodeVarint n = + (n % 128 + 128).toUInt8 :: encodeVarint (n / 128) := by + rw [encodeVarint_def, if_neg hn] + have hlen : (encodeVarint (n / 128)).length ≤ fuel := by + rw [henc] at h + simp only [List.length_cons] at h + omega + have hc : ((n % 128 + 128).toUInt8).toNat = n % 128 + 128 := + UInt8.toNat_ofNat_of_lt + (show n % 128 + 128 < 256 by + have := Nat.mod_lt n (show 0 < 128 by decide); omega) + have hnb : ¬ (n % 128 + 128).toUInt8 < 128 := by + rw [UInt8.lt_iff_toNat_lt, hc] + show ¬ (n % 128 + 128 < 128) + have hmod := Nat.mod_lt n (show 0 < 128 by decide) + omega + rw [henc] + show decodeVarintGo (fuel + 1) + ((n % 128 + 128).toUInt8 :: (encodeVarint (n / 128) ++ rest)) = + some (n, rest) + rw [decodeVarintGo_cons, if_neg hnb, ih (n / 128) rest hlen, hc] + simp [Nat.mod_add_div] + +/-- Decoding an encoded varint, with more bytes after it, gives + the number back and leaves the other bytes alone. -/ +theorem decodeVarint_encode_append {n : Nat} (hn : n < 18446744073709551616) + (rest : List UInt8) : + decodeVarint (encodeVarint n ++ rest) = some (n, rest) := by + have h70 : (128 : Nat) ^ (9 + 1) = 1180591620717411303424 := by decide + have hlen : (encodeVarint n).length ≤ 10 := by + have h1 : n < 128 ^ (9 + 1) := by omega + exact encodeVarint_length_le 9 n h1 + unfold decodeVarint + rw [go_encode 10 n rest hlen] + simp [hn] + +/-- Decoding an encoded varint gives the number back. -/ +theorem decodeVarint_encode {n : Nat} (hn : n < 18446744073709551616) : + decodeVarint (encodeVarint n) = some (n, []) := by + have h := decodeVarint_encode_append hn ([] : List UInt8) + simpa using h + +/-- A wire type number is below eight, so a tag's low three bits + hold the wire type and the rest holds the field number. -/ +theorem wireType_lt (v : Value) : wireType v < 8 := by + cases v <;> simp [wireType] + +/-- Reading the encoding of a well formed field, with more bytes + after it, gives the field back and leaves the other bytes + alone. The tag decodes first: its value splits into the field + number and the wire type, the number is not zero, and each + value case then follows the varint and take and drop rules. -/ +theorem parseField_encode {f : Field} (hf : WFField f) (rest : List UInt8) : + parseField (encodeField f ++ rest) = some (f, rest) := by + obtain ⟨num, value⟩ := f + obtain ⟨hnum0, hnum29, hv⟩ := hf + have hnum0' : 0 < num := hnum0 + have hnum29' : num < 536870912 := hnum29 + have hwt : wireType value < 8 := wireType_lt value + have htag : num * 8 + wireType value < 18446744073709551616 := by omega + have hdiv : (num * 8 + wireType value) / 8 = num := by omega + have hmod : (num * 8 + wireType value) % 8 = wireType value := by omega + have happ : encodeField ⟨num, value⟩ ++ rest = + encodeVarint (num * 8 + wireType value) ++ (encodeValue value ++ rest) := by + simp only [encodeField, List.append_assoc] + have hdec := decodeVarint_encode_append htag (encodeValue value ++ rest) + have hne : ¬ num = 0 := by omega + cases value with + | varint n => + cases hv with + | varint hv64 => + rw [happ] + unfold parseField + rw [hdec] + dsimp only + have hwv : wireType (.varint n) = 0 := rfl + rw [hdiv, hmod, if_neg hne, if_pos hwv] + have hEv : encodeValue (.varint n) = encodeVarint n := rfl + rw [hEv, decodeVarint_encode_append hv64 rest] + rfl + | fixed64 bs => + cases hv with + | fixed64 hlen => + rw [happ] + unfold parseField + rw [hdec] + dsimp only + have hwv : wireType (.fixed64 bs) = 1 := rfl + rw [hdiv, hmod, if_neg hne, if_neg (by omega : ¬ wireType (.fixed64 bs) = 0), + if_pos hwv] + have hEv : encodeValue (.fixed64 bs) = bs := rfl + rw [hEv, if_pos (by simp [List.length_append, hlen] : 8 ≤ (bs ++ rest).length), + List.take_left' hlen, List.drop_left' hlen] + | bytes bs => + cases hv with + | bytes hvlen => + rw [happ] + unfold parseField + rw [hdec] + dsimp only + have hwv : wireType (.bytes bs) = 2 := rfl + rw [hdiv, hmod, if_neg hne, if_neg (by omega : ¬ wireType (.bytes bs) = 0), + if_neg (by omega : ¬ wireType (.bytes bs) = 1), if_pos hwv] + have hEv : encodeValue (.bytes bs) = encodeVarint bs.length ++ bs := rfl + rw [hEv, List.append_assoc, decodeVarint_encode_append hvlen (bs ++ rest)] + dsimp only + rw [if_pos (by simp [List.length_append] : bs.length ≤ (bs ++ rest).length), + List.take_left, List.drop_left] + | fixed32 bs => + cases hv with + | fixed32 hlen => + rw [happ] + unfold parseField + rw [hdec] + dsimp only + have hwv : wireType (.fixed32 bs) = 5 := rfl + rw [hdiv, hmod, if_neg hne, if_neg (by omega : ¬ wireType (.fixed32 bs) = 0), + if_neg (by omega : ¬ wireType (.fixed32 bs) = 1), + if_neg (by omega : ¬ wireType (.fixed32 bs) = 2), if_pos hwv] + have hEv : encodeValue (.fixed32 bs) = bs := rfl + rw [hEv, if_pos (by simp [List.length_append, hlen] : 4 ≤ (bs ++ rest).length), + List.take_left' hlen, List.drop_left' hlen] + +/-- A field always encodes to at least one byte: its tag. -/ +theorem encodeField_length_pos (f : Field) : 0 < (encodeField f).length := by + have h := encodeVarint_length_pos (f.num * 8 + wireType f.value) + simp only [encodeField, List.length_append] + omega + +/-- A message encoding is at least as long as its field count. -/ +theorem encodeMessage_length : ∀ (fs : List Field), + fs.length ≤ (encodeMessage fs).length := by + intro fs + induction fs with + | nil => simp [encodeMessage] + | cons f fs ih => + have h1 := encodeField_length_pos f + have h2 : encodeMessage (f :: fs) = encodeField f ++ encodeMessage fs := rfl + rw [h2, List.length_append, List.length_cons] + omega + +/-- One step of the field reader: on a byte list with a head byte, + the reader reads one field and goes on with the rest. -/ +theorem parseFields_step (fuel : Nat) (bs : List UInt8) (h : bs ≠ []) : + parseFields (fuel + 1) bs = + match parseField bs with + | some (f, rest) => (parseFields fuel rest).map (f :: ·) + | none => none := by + cases bs with + | nil => exact absurd rfl h + | cons b rest => rfl + +/-- Reading the encoding of a well formed message, with fuel at + least the field count, gives the message back. Induction on + the field list: the head field reads by `parseField_encode`, + and the tail is shorter than the bytes it came from, so the + fuel lasts. -/ +theorem parseFields_encode : ∀ (fs : List Field), WFMessage fs → + ∀ (fuel : Nat), fs.length ≤ fuel → + parseFields fuel (encodeMessage fs) = some fs := by + intro fs + induction fs with + | nil => + intro _ fuel _ + exact parseFields_nil fuel + | cons f fs ih => + intro hwf fuel hf + have hf' : WFField f := hwf f (by simp) + have hfs : WFMessage fs := fun x hx => hwf x (List.mem_cons_of_mem f hx) + cases fuel with + | zero => simp at hf + | succ fuel => + have hne : encodeMessage (f :: fs) ≠ [] := by + have hlen := encodeMessage_length (f :: fs) + simp only [List.length_cons] at hlen + exact List.ne_nil_of_length_pos (by omega) + have hcons : encodeMessage (f :: fs) = encodeField f ++ encodeMessage fs := rfl + rw [parseFields_step fuel _ hne, hcons, parseField_encode hf' (encodeMessage fs)] + dsimp only + rw [ih hfs fuel (by simp at hf; omega)] + rfl + +/-- Decoding the encoding of a well formed message gives the + message back. -/ +theorem decodeMessage_encode {fs : List Field} (h : WFMessage fs) : + decodeMessage (encodeMessage fs) = some fs := + parseFields_encode fs h _ (encodeMessage_length fs) + +end Protobuf.Proofs diff --git a/Protobuf.lean b/Protobuf.lean new file mode 100644 index 0000000..e5a5365 --- /dev/null +++ b/Protobuf.lean @@ -0,0 +1 @@ +import Protobuf.Wire diff --git a/Protobuf/Verify.lean b/Protobuf/Verify.lean new file mode 100644 index 0000000..e17b9b8 --- /dev/null +++ b/Protobuf/Verify.lean @@ -0,0 +1,22 @@ +/- + Axiom check for the claims this package makes. Run with: + + lake env lean Protobuf/Verify.lean + + Every claim should list only the standard axioms (propext, + Classical.choice, Quot.sound). A line naming sorryAx would mean + a proof rests on an admitted gap, and the claim is not proved. +-/ + +import Proofs +import Proofs.Examples + +open Protobuf.Proofs Protobuf.Examples + +#print axioms decodeVarint_encode +#print axioms decodeVarint_encode_append +#print axioms parseField_encode +#print axioms decodeMessage_encode +#print axioms encodeVarint_300 +#print axioms decode_test1 +#print axioms decode_test2 diff --git a/Protobuf/Wire.lean b/Protobuf/Wire.lean new file mode 100644 index 0000000..0631367 --- /dev/null +++ b/Protobuf/Wire.lean @@ -0,0 +1,202 @@ +/- + The Protobuf wire format, at the level of bytes: varints, field + tags, and the four wire types this slice carries. + + A message is a list of fields. Each field holds a field number + and a raw value: a varint number, eight bytes, a length delimited + byte string, or four bytes. No meaning is attached to a field + here. Meanings live in `.proto` schema files, which sit outside + this slice. + + Rules the decoder follows: + + - A varint is at most ten bytes. A varint cut short by the end of + the input is rejected, a varint that runs past ten bytes is + rejected, and a varint whose value does not fit in 64 bits is + rejected. + - A field tag is a varint that holds the field number times + eight, plus the wire type. A field number of zero is rejected. + - Wire types 0, 1, 2, and 5 are read. Wire types 3 and 4 are + group markers, which the format has set aside, and 6 and 7 are + not wire types at all. All four are rejected. + - A length delimited value whose length runs past the bytes left + is rejected, and so is a fixed width value cut short. The + decoder returns an error in place of reading past the end of + its input. + + The encoding of a value never depends on a schema, so a packed + repeated field is simply a length delimited byte string at this + level, like any other. +-/ + +namespace Protobuf + +/-- A raw field value, as the wire carries it. A `fixed64` value + holds its eight bytes in wire order, low byte first, and a + `fixed32` value holds its four bytes the same way. -/ +inductive Value where + | varint (n : Nat) + | fixed64 (bs : List UInt8) + | bytes (bs : List UInt8) + | fixed32 (bs : List UInt8) + deriving DecidableEq, Repr + +/-- One field: a field number and a raw value. -/ +structure Field where + num : Nat + value : Value + deriving DecidableEq, Repr + +/-- The wire type number of a value: 0 for a varint, 1 for 64 bit, + 2 for length delimited, 5 for 32 bit. -/ +def wireType : Value → Nat + | .varint _ => 0 + | .fixed64 _ => 1 + | .bytes _ => 2 + | .fixed32 _ => 5 + +/-! ## Varints -/ + +/-- Encode a natural number as a base 128 varint: seven bits at a + time, low group first, with the high bit of each byte set on + every byte but the last. The encoding is the short one: no + leading zero groups. -/ +def encodeVarint (n : Nat) : List UInt8 := + if n < 128 then [n.toUInt8] + else (n % 128 + 128).toUInt8 :: encodeVarint (n / 128) +termination_by n +decreasing_by exact Nat.div_lt_self (by omega) (by omega) + +/-- The unfolding rule for `encodeVarint`. -/ +theorem encodeVarint_def (n : Nat) : + encodeVarint n = + if n < 128 then [n.toUInt8] + else (n % 128 + 128).toUInt8 :: encodeVarint (n / 128) := by + rw [encodeVarint] + +/-- Read a varint from the front of a byte list, with at most + `fuel` bytes. Returns the value and the bytes after it. A list + that ends while a byte still asks for one more gives `none`, + and so does a list whose varint needs more than `fuel` bytes. -/ +def decodeVarintGo : Nat → List UInt8 → Option (Nat × List UInt8) + | 0, _ => none + | _ + 1, [] => none + | fuel + 1, b :: rest => + if b < 128 then some (b.toNat, rest) + else (decodeVarintGo fuel rest).map fun (v, r) => (b.toNat - 128 + 128 * v, r) + +/-- The unfolding rule for `decodeVarintGo` on a list with a head + byte. -/ +theorem decodeVarintGo_cons (fuel : Nat) (b : UInt8) (rest : List UInt8) : + decodeVarintGo (fuel + 1) (b :: rest) = + if b < 128 then some (b.toNat, rest) + else (decodeVarintGo fuel rest).map fun (v, r) => (b.toNat - 128 + 128 * v, r) := by + rw [decodeVarintGo] + +/-- Read one varint from the front of a byte list: at most ten + bytes, and a value that fits in 64 bits. Returns the value and + the bytes after it, or `none` when the bytes hold no such + varint at the front. -/ +def decodeVarint (bs : List UInt8) : Option (Nat × List UInt8) := + (decodeVarintGo 10 bs).bind fun (v, rest) => + if v < 18446744073709551616 then some (v, rest) else none + +/-! ## Fields and messages -/ + +/-- Encode one field value, without its tag. A length delimited + value writes its length as a varint, then its bytes. -/ +def encodeValue : Value → List UInt8 + | .varint n => encodeVarint n + | .fixed64 bs => bs + | .bytes bs => encodeVarint bs.length ++ bs + | .fixed32 bs => bs + +/-- Encode one field: its tag as a varint, then its value. The tag + holds the field number times eight, plus the wire type. -/ +def encodeField (f : Field) : List UInt8 := + encodeVarint (f.num * 8 + wireType f.value) ++ encodeValue f.value + +/-- Encode a message: the fields in list order, one after the + other, with nothing between them. -/ +def encodeMessage (fs : List Field) : List UInt8 := + fs.flatMap encodeField + +/-- Read one field from the front of a byte list. Returns the field + and the bytes after it, or `none` when the front of the list + holds no field this slice reads. -/ +def parseField (bs : List UInt8) : Option (Field × List UInt8) := + match decodeVarint bs with + | none => none + | some (tag, rest1) => + let num := tag / 8 + let wt := tag % 8 + if num = 0 then none + else if wt = 0 then + (decodeVarint rest1).map fun (v, r) => (⟨num, .varint v⟩, r) + else if wt = 1 then + if 8 ≤ rest1.length then + some (⟨num, .fixed64 (rest1.take 8)⟩, rest1.drop 8) + else none + else if wt = 2 then + match decodeVarint rest1 with + | none => none + | some (len, rest2) => + if len ≤ rest2.length then + some (⟨num, .bytes (rest2.take len)⟩, rest2.drop len) + else none + else if wt = 5 then + if 4 ≤ rest1.length then + some (⟨num, .fixed32 (rest1.take 4)⟩, rest1.drop 4) + else none + else none + +/-- Read fields until the byte list ends. The fuel count bounds + the fields read: each field takes at least one byte, so the + length of the input is always fuel enough. A byte list that + ends in the middle of a field gives `none`. -/ +def parseFields : Nat → List UInt8 → Option (List Field) + | _, [] => some [] + | 0, _ :: _ => none + | fuel + 1, bs => + match parseField bs with + | some (f, rest) => (parseFields fuel rest).map (f :: ·) + | none => none + +/-- The unfolding rule for `parseFields` on an empty byte list. -/ +theorem parseFields_nil (fuel : Nat) : parseFields fuel [] = some [] := by + cases fuel with + | zero => rfl + | succ fuel => rfl + +/-- Read a whole message: fields until the input ends, with + nothing left over. -/ +def decodeMessage (bs : List UInt8) : Option (List Field) := + parseFields bs.length bs + +/-! ## Well formed fields + + The round trip claims in `Proofs` hold for well formed fields. + A varint value fits in 64 bits, a fixed width value holds the + right count of bytes, and a field number sits in the range the + Protobuf format allows, from 1 to 536870911. A length delimited + value asks only that its length fits in 64 bits, which any list + a program can hold does in practice, but the proof needs the + bound stated. -/ + +/-- A value in the shape the encoder and the round trip proofs + rely on. -/ +inductive WFValue : Value → Prop + | varint {n : Nat} (h : n < 18446744073709551616) : WFValue (.varint n) + | fixed64 {bs : List UInt8} (h : bs.length = 8) : WFValue (.fixed64 bs) + | bytes {bs : List UInt8} (h : bs.length < 18446744073709551616) : WFValue (.bytes bs) + | fixed32 {bs : List UInt8} (h : bs.length = 4) : WFValue (.fixed32 bs) + +/-- A field with a number in range and a well formed value. -/ +def WFField (f : Field) : Prop := + 0 < f.num ∧ f.num < 536870912 ∧ WFValue f.value + +/-- A message whose fields are all well formed. -/ +def WFMessage (fs : List Field) : Prop := + ∀ f ∈ fs, WFField f + +end Protobuf diff --git a/README.md b/README.md index 09395a9..a9d76d6 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,139 @@ # protobuf -lean Protobuf wire format codec + +A Lean Protobuf wire format codec: varints, field tags, and +messages of raw fields, with the round trips proved. + +The package works at the level of bytes only. A message is a +list of fields; each field holds a field number and a raw value: +a varint number, eight bytes, a length delimited byte string, +or four bytes. There are no `.proto` schemas and no field +meanings here: what a field means lives in a schema, and a +schema sits outside this slice. A packed repeated field is +simply a length delimited byte string at this level. + +Files: + +- `Protobuf/Wire.lean` holds the value and field types, the + varint encoder and decoder, the field and message encoder and + decoder, and the well formedness rules the proofs use. +- `Proofs/RoundTrip.lean` proves the round trips. +- `Proofs/Examples.lean` proves the worked examples from the + Protobuf encoding documentation. +- `Protobuf/Verify.lean` prints the axioms the claims rest on. +- `Main.lean` is a command line front end over the codec. +- `SPEC.md` is the specification in prose. +- `tests/run_tests.py` runs the worked examples and a + differential run against a Python oracle, and writes + `tests/TEST-RESULTS.md`. + +## Using the codec + +Build once: + +```sh +lake build +``` + +The tool reads one request per line. A request is an operation, +one space, and a list of decimal numbers parted by commas. The +operations are `venc` and `vdec` for one varint, and `enc` and +`dec` for a message. A field list is read as groups: field +number, wire type, then the payload (one number for wire type +0, eight byte numbers for type 1, a length and that many byte +numbers for type 2, four byte numbers for type 5). The full +format rules are in `SPEC.md`. + +```console +$ printf 'venc 300\nenc 1,0,150\nenc 2,2,7,116,101,115,116,105,110,103\ndec 8,150,1\n' | .lake/build/bin/protobuf +172,2 +8,150,1 +18,7,116,101,115,116,105,110,103 +ok:1,0,150 +``` + +The first line is 300 as a varint. The second is the docs +message: field 1 holding the varint 150. The third is field 2 +holding the text "testing". The fourth decodes the second +line's bytes back to their field list. + +`dec` prints `none` for well formed bytes this slice rejects +(a group tag, a length past the end, a field cut short), and +any malformed request line prints `error`. + +## Tests + +```sh +python3 tests/run_tests.py +``` + +The harness checks the worked examples byte by byte (the same +examples are also proved in `Proofs/Examples.lean`), then runs +a differential comparison against a Python oracle written with +plain byte code in the harness: random field lists are encoded +by both sides and decoded by both sides, mutated byte strings +must be read alike, and varints are run both ways on their own. +Run of 2026-10-25: 26 fixed cases passed, 52440 differential +inputs, 52440 agreements, 0 failures, seed 20261025. The full +record is in `tests/TEST-RESULTS.md`. + +## What is proved + +With the build passing and no `sorry` anywhere: + +- **Varint round trip** (`Protobuf.Proofs.decodeVarint_encode`): + for any natural number below 2^64, decoding its encoding + gives the number back with no leftover. The appended form + (`decodeVarint_encode_append`) shows that bytes after the + encoding are left alone. +- **Message round trip** (`Protobuf.Proofs.decodeMessage_encode`, + by way of `parseField_encode`): decoding the encoding of a + well formed field list gives the same list back. Well formed + means field numbers from 1 to 536870911, varint values and + lengths below 2^64, and fixed width values of the right byte + count. +- **Worked examples** (`Protobuf.Examples`): the byte examples + from the Protobuf encoding documentation, proved, including + the largest 64 bit varint and the rejections for a bit past + 64 and for eleven byte varints. + +## What is not proved + +- Which byte strings are accepted is covered by tests, not + proof. The proofs cover the round trips. +- There is no decode then encode claim for arbitrary bytes: a + varint written long reads fine but writes back short, and a + field number above 536870911 can be read off the wire but is + outside the field list format, so it cannot be written back. +- No schemas or meanings: no `.proto` files, no field types, no + signed or zigzag readings, no packed field contents. +- Groups are rejected, not read. Wire types 3, 4, 6, and 7 all + reject the message. +- Soundness of the readings rests on the code matching + `SPEC.md`; the differential run is the check for that. + +## What you must trust + +- The Lean kernel and the way `#print axioms` reports proof + dependencies. +- That `SPEC.md` states the wire rules you care about. The code + is written to it and the oracle mirrors it, so a rule stated + wrong in the same way in both would not be caught by the + differential run. The worked examples, taken from the + Protobuf documentation itself, are the outside anchor. +- The Python oracle in the harness is a reading check only; the + proofs do not depend on it. + +## How to re-check + +```sh +lake build # the package and the proofs +grep -rn sorry Protobuf Proofs Main.lean # only the sorryAx comment in Verify.lean +lake env lean Protobuf/Verify.lean # axioms: only the standard ones +python3 tests/run_tests.py # the worked examples and the differential run +``` + +`Verify.lean` is not part of the build; run it by hand as +above. Each claim should list only standard axioms (the +recorded run shows propext and Quot.sound, a subset of the +usual three). A line naming `sorryAx` would mean a proof rests +on an admitted gap. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..cd82b53 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,173 @@ +# Protobuf wire format codec: specification + +This is the specification of the first slice for the `protobuf` +package: the Protobuf wire format at the level of bytes, in Lean, +with the round trips proved. + +What the slice is: a varint codec, field tags, and messages made +of fields with raw values, for the four wire types the format +uses today (0, 1, 2, 5). What it is not: anything about `.proto` +schema files, message meanings, or the types a schema assigns to +a field. A field here is a number and raw bytes or a raw number, +and nothing more. + +## Varints + +A varint encodes a natural number in base 128: seven bits at a +time, low group first, with the high bit of each byte set on +every byte but the last. The encoder writes the short form: no +leading zero groups, and the number 0 is the single byte 0. + +The decoder reads one varint from the front of a byte list and +returns the value and the bytes after it. It rejects: + +- a varint cut short by the end of the input (a byte with its + high bit set and nothing after it), +- a varint longer than ten bytes, +- a varint whose value does not fit in 64 bits. Ten bytes carry + seventy bit places; a ten byte varint whose last byte is 2 or + more sets a bit past 64 and is rejected. The largest varint + read is 18446744073709551615, ten bytes ending in the byte 1. + +Longer than needed encodings are read, up to those limits: a +value written with leading zero groups (the byte pairs 128, 0 +for the number 0, say) decodes to the same value. Only the +encoder is held to the short form. + +## Tags and wire types + +Every field starts with a tag: a varint holding the field number +times eight plus the wire type. Field number zero is rejected. +The wire types: + +| Type | Meaning | Value held here | +| --- | --- | --- | +| 0 | varint | a natural number below 2^64 | +| 1 | 64 bit | eight bytes, in wire order | +| 2 | length delimited | a length varint, then that many bytes | +| 5 | 32 bit | four bytes, in wire order | + +Wire types 3 and 4 are group start and end markers. The format +has set them aside, and this slice rejects them. Wire types 6 +and 7 are not wire types at all, and are rejected too. + +The decoder puts no upper bound on the field number beyond what +the tag varint itself allows: a tag is a varint below 2^64, so +any field number the tag holds is read. The field list format +of the command line (below) binds a field number to the range +the Protobuf format allows for schemas, 1 to 536870911, because +that is the range the round trip claim covers. A number read off +the wire above that range is reported as read; the command line +will not write it back. That gap is stated again under "not +claimed". + +## Messages + +A message is a list of fields, written in list order, one field +after another with nothing between them. The decoder reads +fields until the input ends. It returns an error in place of +reading past the end of its input: + +- a length that runs past the bytes left, +- a 64 bit or 32 bit value cut short, +- a tag or a value varint cut short, +- a field with number zero, or a wire type of 3, 4, 6, or 7, + anywhere in the message. One bad field rejects the whole + message; there is no partial reading. + +Fixed width values are held as their wire bytes, low byte +first, and written back as they were read. Length delimited +values are held as byte strings; a packed repeated field is one +of those, and its contents are not looked inside at this level. + +## The command line format + +One request per line: an operation, one space, and a number +list. The empty line is passed over. A line of any other shape +prints `error`. A number in the list is plain decimal: no sign, +no leading zeros (0 itself is written `0`), at most twenty +digits, numbers parted by commas with no spaces. + +- `venc` takes one number, below 2^64, and prints its varint + bytes as a comma parted number list. +- `vdec` takes byte numbers (each at most 255) and prints `ok:` + and the value when the bytes are exactly one varint this + slice reads, and `none` when they are not. +- `enc` takes a field list (below) and prints the message bytes + as a comma parted number list. +- `dec` takes byte numbers and prints `ok:` and the field list + when the bytes are a message this slice reads, and `none` + when they are not. + +`none` and `error` mean different things: `none` is a well +formed request whose bytes are rejected; `error` is a request +that breaks the line rules or the field list rules. + +The field list format reads the numbers as groups, one group +per field, in field order. A group is: the field number, the +wire type, then the payload. + +- Wire type 0: one number, the varint value, below 2^64. +- Wire type 1: eight byte numbers. +- Wire type 2: a length number, below 2^64, then that many byte + numbers. +- Wire type 5: four byte numbers. + +The empty field list is the empty number list, so `enc ` with an +empty list prints an empty line (the empty message), and `dec ` +of no bytes prints `ok:` with nothing after it. Field numbers +run from 1 to 536870911. A group that breaks any rule (a field +number of 0 or above the range, a wire type outside 0, 1, 2, 5, +a byte number above 255, a value or length at or above 2^64, or +numbers that run out in the middle of a group) makes the whole +request malformed, and the answer is `error`. + +## The claims + +A field is *well formed* when its number is between 1 and +536870911 and its value is in shape: a varint value below 2^64, +a 64 bit value of eight bytes, a 32 bit value of four bytes, or +a length delimited value whose length is below 2^64. A message +is well formed when all of its fields are. + +Over well formed input, the following are proved (in +`Proofs/RoundTrip.lean`, names in the `Protobuf.Proofs` +namespace): + +1. **Varint round trip** (`decodeVarint_encode`, with the + appended form `decodeVarint_encode_append`): for `n` below + 2^64, decoding the encoding of `n` gives `n` back, with no + leftover, and bytes after the encoding are left alone. +2. **Message round trip** (`decodeMessage_encode`, by way of + `parseField_encode`): decoding the encoding of a well formed + field list gives the same field list back. +3. **Worked examples** (`Proofs/Examples.lean`): the byte + examples from the Protobuf encoding documentation (varint 1, + varint 300, varint 150, field 1 holding varint 150, field 2 + holding the text "testing"), the largest 64 bit varint, and + the rejections at this level (a bit past 64, eleven bytes, + field number zero, a group tag, a length past the end), each + proved. + +The printed spec file of the verified bar (a `Spec.lean` whose +statements a checker compares against these) is a reviewer step +that has not been taken yet, so the statements above are the +claims as proved in `Proofs`, in prose form here. + +## Not claimed + +- No round trip for arbitrary byte strings. A message read off + the wire and written back need not give the same bytes: a + varint may have been written long, and a field number above + 536870911, which the decoder reads, cannot be written by the + command line format at all. +- No claim about which byte strings are accepted, beyond the + tests. The accept and reject rules above are what the code + does; the proofs cover the round trips, and the differential + tests cover the readings. +- Nothing about schemas or meanings: no `.proto` files, no field + names or types, no signed or zigzag readings of a varint, no + packed field contents, no maps, no unknown field policy. +- Groups are rejected, not read. +- No streaming: a message is read from a whole byte list in + memory, and nothing here writes to disk. diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..0e8904d --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "protobuf", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..8aa6f4b --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,13 @@ +name = "protobuf" +version = "0.1.0" +defaultTargets = ["Protobuf", "Proofs", "protobuf"] + +[[lean_lib]] +name = "Protobuf" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "protobuf" +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..5d2166c --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,35 @@ +# Test results + +Run with `python3 tests/run_tests.py` from the package root (it runs `lake build` first; pass `--skip-build` to skip that step). Date of the recorded run: 2026-10-25. Seed: 20261025. + +Oracle: a Python oracle written with plain byte code in tests/run_tests.py. No protobuf library is used. The oracle follows the same rules as the Lean decoder, as SPEC.md states them. + +## Worked examples from the encoding documentation + +26 of 26 fixed cases passed: varint 1 and 300, varint 150, the largest 64 bit varint, cut short and eleven byte and past 64 bit rejections, field 1 varint 150 (bytes 8, 150, 1), field 2 with the text "testing" (bytes 18, 7, then the text), a four field message across all four wire types, and rejections for field number zero, wire types 3, 4, 6, 7, a length past the end, fixed width values cut short, and a tag cut short. + +## Differential run against the Python oracle + +Varint encodings and decodings: 6000 cases (3000 random values, each encoded by the Lean tool and decoded back from the oracle encoding), 6000 agreements, 0 failures. + +Whole input varint readings: 600 mutated and random byte strings, 600 agreements, 0 failures. + +Messages: 6000 cases (3000 random field lists of 1 to 6 fields, each encoded by the Lean tool and checked byte by byte against the oracle, and the oracle encoding decoded by the Lean tool and checked field by field), 6000 agreements, 0 failures. + +Mutated messages: 39840 byte strings (every truncation and single byte change of 400 random messages, plus appended bytes), read by both sides, 39840 agreements, 0 failures. + +Differential total: 52440 inputs, 52440 agreements, 0 failures, seed 20261025. + +Named differences: none. Every byte string the two sides read, they read the same way, and every one they reject, they both reject. + +## Malformed requests + +18 of 18 malformed lines printed `error`: field number zero or too big, bad wire types, groups that run out of numbers, values and lengths at 2^64, byte numbers above 255, empty tokens, leading zeros, spaces in the number list, signs, twenty one digit numbers, and an unknown op. One near miss is well formed and checked apart: `enc 1,0,256` encodes the varint value 256 and answers 8,128,2. + +## The empty message + +Checked in its own run, since its encoding is an empty line: `enc ` prints an empty line, `dec ` prints `ok:`, and the bytes of the docs example still decode after them. + +## Failures + +None. diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..64584ef --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,574 @@ +#!/usr/bin/env python3 +"""Test harness for the Lean Protobuf wire format codec. + +Runs the worked byte examples from the Protobuf encoding +documentation, then differential runs against a Python oracle +written with plain byte code here in the harness (no protobuf +library is used). Random field lists are encoded by both sides +and decoded by both sides. Mutated byte strings must be read +alike by both sides. Results are written to tests/TEST-RESULTS.md +in the same shape as the codec, zip, and json records. + +The oracle follows the same rules as the Lean decoder, on +purpose: a varint is at most ten bytes and its value fits in 64 +bits, field number zero is rejected, wire types 3, 4, 6, and 7 +are rejected, and nothing is read past the end of the input. The +decoder puts no upper bound on the field number: a tag is a +varint below 2^64, so any field number the tag holds is read. +The encoder side of the field list format does bound the field +number, at 536870911, as SPEC.md states. + +Usage: python3 tests/run_tests.py [--skip-build] +""" + +import os +import random +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(HERE) +EXE = os.path.join(ROOT, ".lake", "build", "bin", "protobuf") +SEED = 20261025 +MAX64 = 1 << 64 + +failures = [] + + +def check(cond, label, detail=""): + if not cond: + failures.append(f"{label}: {detail}") + print(f"FAIL {label}: {detail}") + + +# --------------------------------------------------------------------------- +# Batch runner: one process for many requests. +# --------------------------------------------------------------------------- + +class Tool: + def __init__(self): + self.lines = [] + self.expected = 0 + + def ask(self, line, skip=0): + """Queue a request. Its answer is line (index - skip) among the + answers: every request answers exactly one line, except the + empty field list encoding, which answers with an empty line + that splitlines drops. Such requests are marked with skip.""" + self.lines.append(line) + self.expected += 1 + return self.expected - 1 - skip + + def run(self): + proc = subprocess.run([EXE], input="\n".join(self.lines) + "\n", + capture_output=True, text=True, timeout=1200) + if proc.returncode != 0: + raise RuntimeError(f"tool exited {proc.returncode}: {proc.stderr[:500]}") + self.answers = proc.stdout.splitlines() + return self.answers + + +# --------------------------------------------------------------------------- +# Python oracle: plain byte code, the rules of the slice. +# --------------------------------------------------------------------------- + +def o_enc_varint(n): + out = bytearray() + while True: + b = n % 128 + n //= 128 + if n: + out.append(b + 128) + else: + out.append(b) + return bytes(out) + + +def o_dec_varint(bs, i=0): + """(value, next index) or None.""" + val = 0 + shift = 0 + count = 0 + while True: + if i >= len(bs): + return None + b = bs[i] + i += 1 + count += 1 + if count > 10: + return None + val |= (b & 127) << shift + shift += 7 + if b < 128: + break + if val >= MAX64: + return None + return val, i + + +def o_dec_varint_whole(bs): + r = o_dec_varint(bs, 0) + if r is None or r[1] != len(bs): + return None + return r[0] + + +def o_enc_field(f): + num, wt, payload = f + tag = o_enc_varint(num * 8 + wt) + if wt == 0: + body = o_enc_varint(payload) + elif wt in (1, 5): + body = bytes(payload) + else: + body = o_enc_varint(len(payload)) + bytes(payload) + return tag + body + + +def o_enc_msg(fs): + return b"".join(o_enc_field(f) for f in fs) + + +def o_dec_msg(bs): + """A field list: (num, wt, payload) with payload an int for + wire type 0 and a list of bytes otherwise. None on rejection.""" + i = 0 + out = [] + while i < len(bs): + r = o_dec_varint(bs, i) + if r is None: + return None + tag, i = r + num, wt = tag // 8, tag % 8 + if num == 0: + return None + if wt == 0: + r = o_dec_varint(bs, i) + if r is None: + return None + v, i = r + out.append((num, 0, v)) + elif wt == 1: + if i + 8 > len(bs): + return None + out.append((num, 1, list(bs[i:i + 8]))) + i += 8 + elif wt == 2: + r = o_dec_varint(bs, i) + if r is None: + return None + ln, i = r + if i + ln > len(bs): + return None + out.append((num, 2, list(bs[i:i + ln]))) + i += ln + elif wt == 5: + if i + 4 > len(bs): + return None + out.append((num, 5, list(bs[i:i + 4]))) + i += 4 + else: + return None + return out + + +def tokens_of(fs): + toks = [] + for num, wt, payload in fs: + toks.append(num) + toks.append(wt) + if wt == 0: + toks.append(payload) + elif wt == 2: + toks.append(len(payload)) + toks.extend(payload) + else: + toks.extend(payload) + return toks + + +def csv(bs): + return ",".join(str(b) for b in bs) + + +def parse_dec(answer): + """A `dec` answer to a field list, or None for `none`.""" + if answer == "none": + return None + assert answer.startswith("ok:"), answer + rest = answer[3:] + if rest == "": + return [] + toks = [int(t) for t in rest.split(",")] + out = [] + i = 0 + while i < len(toks): + num, wt = toks[i], toks[i + 1] + i += 2 + if wt == 0: + out.append((num, 0, toks[i])) + i += 1 + elif wt == 1: + out.append((num, 1, toks[i:i + 8])) + i += 8 + elif wt == 2: + ln = toks[i] + i += 1 + out.append((num, 2, toks[i:i + ln])) + i += ln + else: + out.append((num, 5, toks[i:i + 4])) + i += 4 + return out + + +# --------------------------------------------------------------------------- +# Worked examples from the Protobuf encoding documentation. +# --------------------------------------------------------------------------- + +def worked_examples(tool): + cases = [] + def venc(v, want): + idx = tool.ask(f"venc {v}") + cases.append((idx, want, f"venc {v}")) + def vdec(bs, want): + idx = tool.ask(f"vdec {csv(bs)}") + cases.append((idx, want, f"vdec {csv(bs)}")) + def enc(fs, want): + idx = tool.ask("enc " + ",".join(str(t) for t in tokens_of(fs))) + cases.append((idx, want, f"enc {tokens_of(fs)}")) + def dec(bs, want): + idx = tool.ask(f"dec {csv(bs)}") + cases.append((idx, want, f"dec {csv(bs)}")) + + testing = [116, 101, 115, 116, 105, 110, 103] + venc(1, "1") + venc(300, "172,2") + venc(150, "150,1") + venc(0, "0") + venc(18446744073709551615, + "255,255,255,255,255,255,255,255,255,1") + vdec([1], "ok:1") + vdec([172, 2], "ok:300") + vdec([172], "none") # cut short + vdec([128, 128, 128, 128, 128, 128, 128, 128, 128, 128, 1], + "none") # eleven bytes + vdec([255, 255, 255, 255, 255, 255, 255, 255, 255, 2], + "none") # a bit past 64 + vdec([1, 1], "none") # trailing byte + enc([(1, 0, 150)], "8,150,1") # the docs message + dec([8, 150, 1], "ok:1,0,150") + enc([(2, 2, testing)], "18,7,116,101,115,116,105,110,103") + dec([18, 7, 116, 101, 115, 116, 105, 110, 103], + "ok:2,2,7,116,101,115,116,105,110,103") + enc([(1, 0, 1), (2, 2, testing), (3, 5, [1, 2, 3, 4]), + (4, 1, [8, 7, 6, 5, 4, 3, 2, 1])], + "8,1,18,7,116,101,115,116,105,110,103,29,1,2,3,4," + "33,8,7,6,5,4,3,2,1") + dec([8, 1, 18, 7, 116, 101, 115, 116, 105, 110, 103, + 29, 1, 2, 3, 4, 33, 8, 7, 6, 5, 4, 3, 2, 1], + "ok:1,0,1,2,2,7,116,101,115,116,105,110,103,3,5,1,2,3,4," + "4,1,8,7,6,5,4,3,2,1") + dec([0, 1], "none") # field number zero + dec([27, 1], "none") # wire type 3, a group + dec([28, 1], "none") # wire type 4, a group + dec([30, 1], "none") # wire type 6 + dec([31, 1], "none") # wire type 7 + dec([18, 7, 116, 101], "none") # length past the end + dec([9, 1, 2, 3], "none") # fixed64 cut short + dec([13, 1, 2], "none") # fixed32 cut short + dec([136], "none") # tag varint cut short + return cases + + +def verify_cases(tool, cases, label): + ok = 0 + for idx, want, name in cases: + got = tool.answers[idx] if idx < len(tool.answers) else "" + if got == want: + ok += 1 + else: + check(False, label, f"{name}: want {want!r}, got {got!r}") + return ok, len(cases) + + +# --------------------------------------------------------------------------- +# Random generation. +# --------------------------------------------------------------------------- + +def rand_varint(rng): + return rng.choice([ + lambda: rng.randrange(0, 128), + lambda: rng.randrange(0, 300), + lambda: rng.randrange(0, 1 << 16), + lambda: rng.randrange(0, 1 << 32), + lambda: rng.randrange(0, MAX64), + lambda: rng.choice([0, 1, 127, 128, 300, (1 << 32) - 1, + 1 << 63, MAX64 - 1]), + ])() + + +def rand_field(rng): + num = rng.choice([1, 2, 3, 4, 5, 16, 100, 2047, + rng.randrange(1, 536870912)]) + wt = rng.choice([0, 0, 1, 2, 2, 5]) + if wt == 0: + return (num, 0, rand_varint(rng)) + if wt == 1: + return (num, 1, [rng.randrange(256) for _ in range(8)]) + if wt == 5: + return (num, 5, [rng.randrange(256) for _ in range(4)]) + ln = rng.choice([0, 1, 3, 7, 16, rng.randrange(0, 40)]) + return (num, 2, [rng.randrange(256) for _ in range(ln)]) + + +# --------------------------------------------------------------------------- + +def main(): + if "--skip-build" not in sys.argv: + env = dict(os.environ) + env["PATH"] = os.path.expanduser("~/.elan/bin") + ":" + env["PATH"] + r = subprocess.run(["lake", "build"], cwd=ROOT, env=env, + capture_output=True, text=True, timeout=1800) + if r.returncode != 0: + print(r.stdout[-2000:], r.stderr[-2000:]) + print("BUILD FAILED") + return 1 + + tool = Tool() + cases = worked_examples(tool) + + rng = random.Random(SEED) + + # Varint differential. + varint_inputs = [] + varint_idx = [] + for _ in range(3000): + v = rand_varint(rng) + varint_inputs.append(v) + varint_idx.append((tool.ask(f"venc {v}"), + tool.ask(f"vdec {csv(o_enc_varint(v))}"))) + # Whole input varint rejections and readings, both sides. + neg_inputs = [] + neg_idx = [] + for _ in range(600): + bs = bytearray(o_enc_varint(rand_varint(rng))) + kind = rng.randrange(3) + if kind == 0 and bs: + bs = bs[:rng.randrange(len(bs))] # truncate + elif kind == 1: + bs = bs + bytearray([rng.randrange(256)]) # trailing byte + else: + bs = bytearray(rng.randrange(256) + for _ in range(rng.randrange(0, 13))) + neg_inputs.append(bytes(bs)) + neg_idx.append(tool.ask(f"vdec {csv(bs)}")) + + # Message differential. + msg_inputs = [] + msg_idx = [] + for _ in range(3000): + fs = [rand_field(rng) for _ in range(rng.randrange(1, 7))] + msg_inputs.append(fs) + msg_idx.append((tool.ask("enc " + ",".join(str(t) for t in tokens_of(fs))), + tool.ask(f"dec {csv(o_enc_msg(fs))}"))) + + # Mutations of valid messages, read by both sides. + mut_inputs = [] + mut_idx = [] + for _ in range(400): + fs = [rand_field(rng) for _ in range(rng.randrange(1, 5))] + bs = bytearray(o_enc_msg(fs)) + muts = [] + for cut in range(0, len(bs)): + muts.append(bytes(bs[:cut])) + for pos in range(len(bs)): + for val in (0, 255, bs[pos] ^ 128, (bs[pos] + 1) % 256): + m = bytearray(bs) + m[pos] = val + muts.append(bytes(m)) + muts.append(bytes(bs) + bytes([0])) + muts.append(bytes(bs) + bytes([128])) + muts.append(bytes(bs) + bytes([8, 1])) + for m in muts: + mut_inputs.append(m) + mut_idx.append(tool.ask(f"dec {csv(m)}")) + + # Malformed requests. + malformed = [ + "enc 0,0,1", # field number zero + "enc 536870912,0,1", # field number too big + "enc 1,3,1", # wire type outside the slice + "enc 1,0", # group runs out of numbers + "enc 1,0,18446744073709551616", # varint value at 2^64 + "enc 1,1,1,2,3", # fixed64 payload short + "enc 1,2,3,9,9", # length says 3, 2 bytes follow + "enc 1,2,18446744073709551616,9", # length at 2^64 + "enc 1,0,256", # fine as a value, but... + "dec 256", # byte number above 255 + "dec 1,,2", # empty token + "venc 18446744073709551616", # at 2^64 + "venc 1,2", # two numbers + "vdec 300", # byte number above 255 + "dec 08,1", # leading zero + "enc 1, 0,1", # space inside the number list + "foo 1", # unknown op + "enc 1,0,-1", # a sign + "dec 999999999999999999999", # twenty one digits + ] + # `enc 1,0,256` is well formed (256 is a varint value): drop it + # from the malformed list and check it on its own below. + malformed.remove("enc 1,0,256") + mal_idx = [(tool.ask(m), m) for m in malformed] + value256_idx = tool.ask("enc 1,0,256") + + answers = tool.run() + check(len(answers) == tool.expected, "answer-count", + f"{len(answers)} answers for {tool.expected} requests") + + lines = [] + lines.append("# Test results\n") + lines.append("Run with `python3 tests/run_tests.py` from the " + "package root (it runs `lake build` first; pass " + "`--skip-build` to skip that step). Date of the " + "recorded run: 2026-10-25. Seed: 20261025.\n") + lines.append("Oracle: a Python oracle written with plain byte " + "code in tests/run_tests.py. No protobuf library " + "is used. The oracle follows the same rules as " + "the Lean decoder, as SPEC.md states them.\n") + + ok, total = verify_cases(tool, cases, "worked") + lines.append("## Worked examples from the encoding documentation\n") + lines.append(f"{ok} of {total} fixed cases passed: varint 1 " + "and 300, varint 150, the largest 64 bit varint, " + "cut short and eleven byte and past 64 bit " + "rejections, field 1 varint 150 (bytes 8, 150, 1), " + "field 2 with the text \"testing\" (bytes 18, 7, " + "then the text), a four field message across all " + "four wire types, and rejections for field number " + "zero, wire types 3, 4, 6, 7, a length past the " + "end, fixed width values cut short, and a tag " + "cut short.\n") + + # Varint differential scoring. + v_agree = v_total = 0 + for v, (ie, idc) in zip(varint_inputs, varint_idx): + v_total += 2 + if answers[ie] == csv(o_enc_varint(v)): + v_agree += 1 + else: + check(False, "varint-enc", f"{v}: got {answers[ie]!r}") + want = f"ok:{v}" + if answers[idc] == want: + v_agree += 1 + else: + check(False, "varint-dec", f"{v}: got {answers[idc]!r}") + n_agree = n_total = 0 + for bs, idx in zip(neg_inputs, neg_idx): + n_total += 1 + ov = o_dec_varint_whole(bs) + want = "none" if ov is None else f"ok:{ov}" + if answers[idx] == want: + n_agree += 1 + else: + check(False, "varint-neg", f"{csv(bs)}: want {want}, got {answers[idx]!r}") + + m_agree = m_total = 0 + for fs, (ie, idc) in zip(msg_inputs, msg_idx): + m_total += 2 + if answers[ie] == csv(o_enc_msg(fs)): + m_agree += 1 + else: + check(False, "msg-enc", f"{tokens_of(fs)}: got {answers[ie]!r}") + got = parse_dec(answers[idc]) if idc < len(answers) else None + if got == fs: + m_agree += 1 + else: + check(False, "msg-dec", f"{tokens_of(fs)}: got {answers[idc]!r}") + + u_agree = u_total = 0 + for bs, idx in zip(mut_inputs, mut_idx): + u_total += 1 + ov = o_dec_msg(bs) + want = "none" if ov is None else "ok:" + ",".join(str(t) for t in tokens_of(ov)) + if answers[idx] == want: + u_agree += 1 + else: + check(False, "mut", f"{csv(bs)}: want {want!r}, got {answers[idx]!r}") + + lines.append("## Differential run against the Python oracle\n") + lines.append(f"Varint encodings and decodings: {v_total} cases " + f"(3000 random values, each encoded by the Lean " + f"tool and decoded back from the oracle encoding), " + f"{v_agree} agreements, {v_total - v_agree} failures.\n") + lines.append(f"Whole input varint readings: {n_total} mutated " + f"and random byte strings, {n_agree} agreements, " + f"{n_total - n_agree} failures.\n") + lines.append(f"Messages: {m_total} cases (3000 random field " + f"lists of 1 to 6 fields, each encoded by the Lean " + f"tool and checked byte by byte against the oracle, " + f"and the oracle encoding decoded by the Lean tool " + f"and checked field by field), {m_agree} agreements, " + f"{m_total - m_agree} failures.\n") + lines.append(f"Mutated messages: {u_total} byte strings (every " + f"truncation and single byte change of 400 random " + f"messages, plus appended bytes), read by both " + f"sides, {u_agree} agreements, " + f"{u_total - u_agree} failures.\n") + total_in = v_total + n_total + m_total + u_total + total_ag = v_agree + n_agree + m_agree + u_agree + lines.append(f"Differential total: {total_in} inputs, {total_ag} " + f"agreements, {total_in - total_ag} failures, " + f"seed 20261025.\n") + lines.append("Named differences: none. Every byte string the " + "two sides read, they read the same way, and every " + "one they reject, they both reject.\n") + + mal_ok = 0 + for idx, m in mal_idx: + if answers[idx] == "error": + mal_ok += 1 + else: + check(False, "malformed", f"{m!r}: got {answers[idx]!r}") + check(answers[value256_idx] == "8,128,2", "value-256", + f"got {answers[value256_idx]!r}") + lines.append("## Malformed requests\n") + lines.append(f"{mal_ok} of {len(mal_idx)} malformed lines " + "printed `error`: field number zero or too big, " + "bad wire types, groups that run out of numbers, " + "values and lengths at 2^64, byte numbers above " + "255, empty tokens, leading zeros, spaces in the " + "number list, signs, twenty one digit numbers, " + "and an unknown op. One near miss is well formed " + "and checked apart: `enc 1,0,256` encodes the " + "varint value 256 and answers 8,128,2.\n") + + # The empty message, in its own run: its encoding is an empty + # line, which the batch runner cannot count. + proc = subprocess.run([EXE], input="enc \ndec \ndec 8,150,1\n", + capture_output=True, text=True, timeout=60) + got_empty = proc.stdout.splitlines() + check(got_empty == ["", "ok:", "ok:1,0,150"], "empty-message", + f"got {got_empty!r}") + lines.append("## The empty message\n") + lines.append("Checked in its own run, since its encoding is " + "an empty line: `enc ` prints an empty line, " + "`dec ` prints `ok:`, and the bytes of the docs " + "example still decode after them.\n") + + lines.append("## Failures\n") + if failures: + for f in failures[:50]: + lines.append(f"- {f}") + else: + lines.append("None.\n") + + with open(os.path.join(HERE, "TEST-RESULTS.md"), "w") as fh: + fh.write("\n".join(lines)) + print("\n".join(lines)) + print(f"failures: {len(failures)}") + return 0 if not failures else 1 + + +if __name__ == "__main__": + sys.exit(main()) From f25bbec321320eccfbccb18c808c477d5531fa88 Mon Sep 17 00:00:00 2001 From: shah Date: Mon, 26 Oct 2026 09:06:54 -0500 Subject: [PATCH 2/2] Record the axiom check output in the test results --- tests/TEST-RESULTS.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 5d2166c..12c1125 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -33,3 +33,19 @@ Checked in its own run, since its encoding is an empty line: `enc ` prints an em ## Failures None. + +## Axiom check + +Recorded on 2026-10-26 against the head of this pull request, on Lean 4.35.0. The lines below are the output of the `#print axioms` commands in `Protobuf/Verify.lean`, run with `lake env lean Protobuf/Verify.lean` after a clean `lake build` (13 jobs). + +```text +'Protobuf.Proofs.decodeVarint_encode' depends on axioms: [propext, Quot.sound] +'Protobuf.Proofs.decodeVarint_encode_append' depends on axioms: [propext, Quot.sound] +'Protobuf.Proofs.parseField_encode' depends on axioms: [propext, Quot.sound] +'Protobuf.Proofs.decodeMessage_encode' depends on axioms: [propext, Quot.sound] +'Protobuf.Examples.encodeVarint_300' depends on axioms: [propext, Quot.sound] +'Protobuf.Examples.decode_test1' does not depend on any axioms +'Protobuf.Examples.decode_test2' does not depend on any axioms +``` + +No line names sorryAx. No line names Classical.choice.