Skip to content

Move proof modules under Protobuf #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
zero-aska merged 2 commits into from
Oct 30, 2026
Merged

Move proof modules under Protobuf #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e55d412
Move proof modules and spec names under Protobuf
ahrazzle Oct 28, 2026
c61f11f
Point the remaining Spec/Defs.lean references at Protobuf/Spec/Defs.lean
orda-aska Oct 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 0 additions & 7 deletions Proofs.lean
View file
Open in desktop

This file was deleted.

7 changes: 7 additions & 0 deletions Protobuf/Proofs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
/-
The proofs, under the names the challenge file gives them. The
theorems themselves are in `Protobuf/Proofs/Main.lean`, from the lemmas in the
other files.
-/

import Protobuf.Proofs.Main
34 changes: 17 additions & 17 deletions Proofs/Fixed.lean → Protobuf/Proofs/Fixed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
/-
Fixed-width values: `leValue` and `leBytes` in `Protobuf/Wire.lean`
are `Spec.leValue` and `Spec.leBytes`, `Spec.leBytes k n` has `k`
are `Protobuf.Spec.leValue` and `Protobuf.Spec.leBytes`, `Protobuf.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
import Protobuf.Spec.Defs

namespace Protobuf.Proofs.Fixed

Expand All @@ -21,11 +21,11 @@ theorem sum_map_mul_left (l : List Nat) (g : Nat → Nat) (c : Nat) :
| 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_nil : Protobuf.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
Protobuf.Spec.leValue (b :: bs) = b.toNat + 256 * Protobuf.Spec.leValue bs := by
unfold Protobuf.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
Expand All @@ -34,11 +34,11 @@ theorem spec_leValue_cons (b : UInt8) (bs : List UInt8) :
rw [this, sum_map_mul_left]
simp

theorem spec_leBytes_zero (n : Nat) : Spec.leBytes 0 n = [] := rfl
theorem spec_leBytes_zero (n : Nat) : Protobuf.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
Protobuf.Spec.leBytes (k + 1) n = (n % 256).toUInt8 :: Protobuf.Spec.leBytes k (n / 256) := by
unfold Protobuf.Spec.leBytes
rw [List.range_succ_eq_map, List.map_cons, List.map_map]
congr 1
· simp
Expand All @@ -51,24 +51,24 @@ theorem spec_leBytes_succ (k n : Nat) :
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
theorem leValue_eq (bs : List UInt8) : leValue bs = Protobuf.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
theorem leBytes_eq (k n : Nat) : leBytes k n = Protobuf.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 leBytes_length (k n : Nat) : (Protobuf.Spec.leBytes k n).length = k := by
simp [Protobuf.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
theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Protobuf.Spec.leValue (Protobuf.Spec.leBytes k n) = n := by
induction k generalizing n with
| zero =>
simp at h
Expand All @@ -83,22 +83,22 @@ theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Spec.leValue (Spec.leByt
rw [this]
exact Nat.mod_add_div n 256

theorem leValue_lt (bs : List UInt8) : Spec.leValue bs < 256 ^ bs.length := by
theorem leValue_lt (bs : List UInt8) : Protobuf.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
theorem leBytes_leValue (bs : List UInt8) : Protobuf.Spec.leBytes bs.length (Protobuf.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
have hm : (b.toNat + 256 * Protobuf.Spec.leValue bs) % 256 = b.toNat := by omega
have hd : (b.toNat + 256 * Protobuf.Spec.leValue bs) / 256 = Protobuf.Spec.leValue bs := by omega
rw [hm, hd, ih]
simp

Expand Down
40 changes: 20 additions & 20 deletions Proofs/Main.lean → Protobuf/Proofs/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,48 +1,48 @@
/-
The statements of `Spec.lean`, under the same names, from the lemmas
in the other files of `Proofs/`. The test vectors are checked by
The statements of `Protobuf/Spec.lean`, under the same names, from the lemmas
in the other files of `Protobuf/Proofs/`. The test vectors are checked by
evaluation.
-/

import Protobuf
import Spec.Defs
import Proofs.Varint
import Proofs.Message
import Protobuf.Spec.Defs
import Protobuf.Proofs.Varint
import Protobuf.Proofs.Message

open Protobuf
open Protobuf.Proofs

theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n :=
theorem Protobuf.Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Protobuf.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 :=
theorem Protobuf.Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Protobuf.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) :
theorem Protobuf.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 :=
theorem Protobuf.Spec.isValid_iff (f : Field) : f.isValid = true ↔ Protobuf.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 :=
theorem Protobuf.Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
Protobuf.encode fs = Protobuf.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 :=
theorem Protobuf.Spec.decode_iff (bs : List UInt8) (fs : List Field) :
decode bs = some fs ↔ Protobuf.Spec.Message bs fs :=
Protobuf.Proofs.Message.decode_iff bs fs

theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
theorem Protobuf.Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Protobuf.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 :=
theorem Protobuf.Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
∀ f ∈ fs, Protobuf.Spec.ValidField f :=
Protobuf.Proofs.Message.decode_valid bs fs h

theorem Spec.guide_vectors :
theorem Protobuf.Spec.guide_vectors :
Varint.encode 1 = [0x01] ∧
Varint.encode 150 = [0x96, 0x01] ∧
Varint.encode (2 ^ 64 - 2) = [0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
Expand All @@ -56,7 +56,7 @@ theorem Spec.guide_vectors :
[0x08, 0x96, 0x01, 0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by
decide

theorem Spec.edge_vectors :
theorem Protobuf.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] =
Expand All @@ -68,7 +68,7 @@ theorem Spec.edge_vectors :
decode [] = some [] := by
decide

theorem Spec.reject_vectors :
theorem Protobuf.Spec.reject_vectors :
decode [0x08] = none ∧
decode [0x08, 0x80] = none ∧
decode [0x08, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x00] = none ∧
Expand Down
Loading