1  /-
  2    Cornell.Proofs - Verified Box Implementations
  3    
  4    This module contains Box definitions with COMPLETE proofs.
  5    No `sorry`, no `axiom`, no `partial`.
  6    
  7    The goal: real load-bearing proofs that guarantee roundtrip correctness.
  8  -/
  9  
 10  import Std.Tactic.BVDecide
 11  
 12  namespace Cornell.Proofs
 13  
 14  -- ═══════════════════════════════════════════════════════════════════════════════
 15  -- BYTES (same as Basic, but we'll use ByteArray directly for lemma access)
 16  -- ═══════════════════════════════════════════════════════════════════════════════
 17  
 18  abbrev Bytes := ByteArray
 19  
 20  -- ═══════════════════════════════════════════════════════════════════════════════
 21  -- PARSE RESULT
 22  -- ═══════════════════════════════════════════════════════════════════════════════
 23  
 24  /-- Parse result: either failure or (value, remaining bytes) -/
 25  inductive ParseResult (α : Type) where
 26    | ok : α → Bytes → ParseResult α
 27    | fail : ParseResult α
 28    deriving DecidableEq
 29  
 30  namespace ParseResult
 31  
 32  def map (f : α → β) : ParseResult α → ParseResult β
 33    | ok a rest => ok (f a) rest
 34    | fail => fail
 35  
 36  def bind (r : ParseResult α) (f : α → Bytes → ParseResult β) : ParseResult β :=
 37    match r with
 38    | ok a rest => f a rest
 39    | fail => fail
 40  
 41  -- Lemmas about ParseResult
 42  @[simp] theorem map_ok (f : α → β) (a : α) (rest : Bytes) : 
 43      map f (ok a rest) = ok (f a) rest := rfl
 44  
 45  @[simp] theorem map_fail (f : α → β) : 
 46      map f (fail : ParseResult α) = fail := rfl
 47  
 48  @[simp] theorem bind_ok (a : α) (rest : Bytes) (f : α → Bytes → ParseResult β) :
 49      bind (ok a rest) f = f a rest := rfl
 50  
 51  @[simp] theorem bind_fail (f : α → Bytes → ParseResult β) :
 52      bind (fail : ParseResult α) f = fail := rfl
 53  
 54  end ParseResult
 55  
 56  -- ═══════════════════════════════════════════════════════════════════════════════
 57  -- BOX - The verified codec structure
 58  -- ═══════════════════════════════════════════════════════════════════════════════
 59  
 60  /-- 
 61  A Box is a verified bidirectional codec.
 62  
 63  Key properties:
 64  - `roundtrip`: parsing what you serialized gives back the original value
 65  - `consumption`: parsing consumes exactly the serialized bytes, leaving extra untouched
 66  -/
 67  structure Box (α : Type) where
 68    parse : Bytes → ParseResult α
 69    serialize : α → Bytes
 70    roundtrip : ∀ a, parse (serialize a) = ParseResult.ok a ByteArray.empty
 71    consumption : ∀ a extra, parse (serialize a ++ extra) = ParseResult.ok a extra
 72  
 73  -- ═══════════════════════════════════════════════════════════════════════════════
 74  -- UNIT BOX - The trivial case (zero bytes)
 75  -- ═══════════════════════════════════════════════════════════════════════════════
 76  
 77  /-- The unit box: encodes Unit as zero bytes -/
 78  def unit : Box Unit where
 79    parse bs := .ok () bs
 80    serialize _ := ByteArray.empty
 81    roundtrip := by
 82      intro a
 83      -- parse (serialize ()) = parse ByteArray.empty = .ok () ByteArray.empty
 84      rfl
 85    consumption := by
 86      intro a extra
 87      -- parse (serialize () ++ extra) = parse (ByteArray.empty ++ extra) = parse extra = .ok () extra
 88      simp [ByteArray.empty_append]
 89  
 90  -- ═══════════════════════════════════════════════════════════════════════════════
 91  -- U8 BOX - Single byte
 92  -- ═══════════════════════════════════════════════════════════════════════════════
 93  
 94  /-- Parse a single byte -/
 95  def parseU8 (bs : Bytes) : ParseResult UInt8 :=
 96    if h : bs.size > 0 then
 97      .ok bs[0] (bs.extract 1 bs.size)
 98    else 
 99      .fail
100  
101  /-- Serialize a single byte -/
102  def serializeU8 (v : UInt8) : Bytes := 
103    [v].toByteArray
104  
105  -- Key lemma: size of a singleton ByteArray
106  theorem singleton_size (v : UInt8) : [v].toByteArray.size = 1 := by
107    simp [List.size_toByteArray]
108  
109  -- Key lemma: getting element 0 of singleton
110  theorem singleton_getElem (v : UInt8) : [v].toByteArray[0]'(by simp) = v := by
111    simp
112  
113  -- Key lemma: extracting from position 1 of a size-1 array gives empty
114  theorem singleton_extract_tail (v : UInt8) : 
115      [v].toByteArray.extract 1 [v].toByteArray.size = ByteArray.empty := by
116    simp
117  
118  /-- Single byte box with verified roundtrip -/
119  def u8 : Box UInt8 where
120    parse := parseU8
121    serialize := serializeU8
122    roundtrip := by
123      intro v
124      simp only [parseU8, serializeU8]
125      -- Need to show: if h : [v].toByteArray.size > 0 then ...
126      have hsize : [v].toByteArray.size > 0 := by simp
127      simp only [hsize, ↓reduceDIte]
128      -- Show equality by showing both components match
129      have hval : [v].toByteArray[0]'hsize = v := by simp
130      have hrest : [v].toByteArray.extract 1 [v].toByteArray.size = ByteArray.empty := by
131        simp
132      simp only [hval, hrest]
133    consumption := by
134      intro v extra
135      simp only [parseU8, serializeU8]
136      -- Size of [v].toByteArray ++ extra > 0
137      have hsize : ([v].toByteArray ++ extra).size > 0 := by
138        simp only [ByteArray.size_append, List.size_toByteArray, List.length_cons, List.length_nil]
139        omega
140      simp only [hsize, ↓reduceDIte]
141      -- Show value component: ([v].toByteArray ++ extra)[0] = v
142      have hval : ([v].toByteArray ++ extra)[0]'hsize = v := by
143        have h0 : (0 : Nat) < [v].toByteArray.size := by simp
144        rw [ByteArray.getElem_append_left h0]
145        simp
146      -- Show remaining component: extract 1 (size) = extra
147      have hrest : ([v].toByteArray ++ extra).extract 1 ([v].toByteArray ++ extra).size = extra := by
148        simp only [ByteArray.size_append]
149        -- extract 1 (1 + extra.size) from ([v].toByteArray ++ extra)
150        -- [v].toByteArray has size 1, so extract from position 1 gives us the second part
151        rw [ByteArray.extract_append_eq_right (by simp : 1 = [v].toByteArray.size)]
152        simp
153      simp only [hval, hrest]
154  
155  -- ═══════════════════════════════════════════════════════════════════════════════
156  -- SEQUENCE COMBINATOR
157  -- ═══════════════════════════════════════════════════════════════════════════════
158  
159  /-- 
160  Sequence two boxes: parse A then B, serialize A then B.
161  If both A and B have verified roundtrip, so does (A, B).
162  -/
163  def seq (boxA : Box α) (boxB : Box β) : Box (α × β) where
164    parse bs := 
165      boxA.parse bs |>.bind fun a rest =>
166        boxB.parse rest |>.map fun b => (a, b)
167    serialize ab := boxA.serialize ab.1 ++ boxB.serialize ab.2
168    roundtrip := by
169      intro ⟨a, b⟩
170      simp only [ParseResult.bind, ParseResult.map]
171      -- parse (serA a ++ serB b) 
172      -- = parseA (serA a ++ serB b) >>= ...
173      -- By consumption of A: parseA (serA a ++ serB b) = ok a (serB b)
174      rw [boxA.consumption a (boxB.serialize b)]
175      -- Simplify the match
176      simp only []
177      -- Now: parseB (serB b) = ok b empty
178      rw [boxB.roundtrip b]
179    consumption := by
180      intro ⟨a, b⟩ extra
181      simp only [ParseResult.bind, ParseResult.map]
182      -- parse ((serA a ++ serB b) ++ extra)
183      -- = parseA ((serA a ++ serB b) ++ extra) >>= ...
184      -- Rewrite: (serA a ++ serB b) ++ extra = serA a ++ (serB b ++ extra)
185      rw [ByteArray.append_assoc]
186      -- By consumption of A: parseA (serA a ++ (serB b ++ extra)) = ok a (serB b ++ extra)
187      rw [boxA.consumption a (boxB.serialize b ++ extra)]
188      -- Simplify the match
189      simp only []
190      -- By consumption of B: parseB (serB b ++ extra) = ok b extra
191      rw [boxB.consumption b extra]
192  
193  -- ═══════════════════════════════════════════════════════════════════════════════
194  -- ISO COMBINATOR (mapping through isomorphism)
195  -- ═══════════════════════════════════════════════════════════════════════════════
196  
197  /-- 
198  Map a box through an isomorphism.
199  Given Box α and bijection f : α ↔ β, get Box β.
200  -/
201  def isoBox (box : Box α) (f : α → β) (g : β → α) 
202      (fg : ∀ b, f (g b) = b) (_gf : ∀ a, g (f a) = a) : Box β where
203    parse bs := box.parse bs |>.map f
204    serialize b := box.serialize (g b)
205    roundtrip := by
206      intro b
207      simp only [ParseResult.map]
208      -- parse (serialize (g b)) = ok (g b) empty  by box.roundtrip
209      rw [box.roundtrip (g b)]
210      -- Simplify the match, then f (g b) = b by fg
211      simp only [fg]
212    consumption := by
213      intro b extra
214      simp only [ParseResult.map]
215      rw [box.consumption (g b) extra]
216      simp only [fg]
217  
218  -- ═══════════════════════════════════════════════════════════════════════════════
219  -- U64LE BOX - 64-bit little-endian using BitVec
220  -- ═══════════════════════════════════════════════════════════════════════════════
221  
222  /-- Extract byte i (0-indexed from LSB) from a 64-bit value using setWidth and shift -/
223  def extractByte (v : BitVec 64) (i : Nat) (_hi : i < 8 := by omega) : BitVec 8 :=
224    (v >>> (i * 8)).setWidth 8
225  
226  /-- Combine 8 bytes into a 64-bit value (little-endian) -/
227  def combineBytes (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) : BitVec 64 :=
228    -- Little-endian: b0 is LSB, b7 is MSB
229    -- We build from MSB to LSB using append
230    let v7 : BitVec 64 := b7.setWidth 64 <<< 56
231    let v6 : BitVec 64 := b6.setWidth 64 <<< 48
232    let v5 : BitVec 64 := b5.setWidth 64 <<< 40
233    let v4 : BitVec 64 := b4.setWidth 64 <<< 32
234    let v3 : BitVec 64 := b3.setWidth 64 <<< 24
235    let v2 : BitVec 64 := b2.setWidth 64 <<< 16
236    let v1 : BitVec 64 := b1.setWidth 64 <<< 8
237    let v0 : BitVec 64 := b0.setWidth 64
238    v7 ||| v6 ||| v5 ||| v4 ||| v3 ||| v2 ||| v1 ||| v0
239  
240  /-- Parse 8 bytes as little-endian u64 -/
241  def parseU64le (bs : Bytes) : ParseResult (BitVec 64) :=
242    if h : bs.size ≥ 8 then
243      have h0 : 0 < bs.size := by omega
244      have h1 : 1 < bs.size := by omega
245      have h2 : 2 < bs.size := by omega
246      have h3 : 3 < bs.size := by omega
247      have h4 : 4 < bs.size := by omega
248      have h5 : 5 < bs.size := by omega
249      have h6 : 6 < bs.size := by omega
250      have h7 : 7 < bs.size := by omega
251      let b0 : BitVec 8 := BitVec.ofNat 8 (bs[0]).toNat
252      let b1 : BitVec 8 := BitVec.ofNat 8 (bs[1]).toNat
253      let b2 : BitVec 8 := BitVec.ofNat 8 (bs[2]).toNat
254      let b3 : BitVec 8 := BitVec.ofNat 8 (bs[3]).toNat
255      let b4 : BitVec 8 := BitVec.ofNat 8 (bs[4]).toNat
256      let b5 : BitVec 8 := BitVec.ofNat 8 (bs[5]).toNat
257      let b6 : BitVec 8 := BitVec.ofNat 8 (bs[6]).toNat
258      let b7 : BitVec 8 := BitVec.ofNat 8 (bs[7]).toNat
259      .ok (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) (bs.extract 8 bs.size)
260    else 
261      .fail
262  
263  /-- Serialize u64 as 8 bytes little-endian -/
264  def serializeU64le (v : BitVec 64) : Bytes :=
265    let b0 := (extractByte v 0).toNat.toUInt8
266    let b1 := (extractByte v 1).toNat.toUInt8
267    let b2 := (extractByte v 2).toNat.toUInt8
268    let b3 := (extractByte v 3).toNat.toUInt8
269    let b4 := (extractByte v 4).toNat.toUInt8
270    let b5 := (extractByte v 5).toNat.toUInt8
271    let b6 := (extractByte v 6).toNat.toUInt8
272    let b7 := (extractByte v 7).toNat.toUInt8
273    [b0, b1, b2, b3, b4, b5, b6, b7].toByteArray
274  
275  -- Key lemma: extractByte extracts the correct byte
276  theorem extractByte_toNat (v : BitVec 64) (i : Nat) (hi : i < 8) :
277      (extractByte v i hi).toNat = (v.toNat >>> (i * 8)) % 256 := by
278    simp only [extractByte, BitVec.toNat_setWidth, BitVec.toNat_ushiftRight]
279  
280  -- Key lemma: size of serialized u64
281  theorem serializeU64le_size (v : BitVec 64) : (serializeU64le v).size = 8 := by
282    simp [serializeU64le, List.size_toByteArray]
283  
284  -- Helper: List of 8 elements has length 8
285  theorem list8_length {α : Type} (a b c d e f g h : α) : 
286      [a, b, c, d, e, f, g, h].length = 8 := rfl
287  
288  -- The key insight: combineBytes and extractByte are inverses.
289  -- This is the fundamental theorem we need for u64le roundtrip.
290  
291  -- Lemma: combining bytes then extracting gives back the original bytes
292  -- This follows from the structure of little-endian encoding
293  -- We prove each case using bv_decide
294  
295  theorem combineBytes_extractByte_0 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
296      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 0 = b0 := by
297    simp only [extractByte, combineBytes]
298    bv_decide
299  
300  theorem combineBytes_extractByte_1 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
301      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 1 = b1 := by
302    simp only [extractByte, combineBytes]
303    bv_decide
304  
305  theorem combineBytes_extractByte_2 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
306      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 2 = b2 := by
307    simp only [extractByte, combineBytes]
308    bv_decide
309  
310  theorem combineBytes_extractByte_3 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
311      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 3 = b3 := by
312    simp only [extractByte, combineBytes]
313    bv_decide
314  
315  theorem combineBytes_extractByte_4 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
316      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 4 = b4 := by
317    simp only [extractByte, combineBytes]
318    bv_decide
319  
320  theorem combineBytes_extractByte_5 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
321      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 5 = b5 := by
322    simp only [extractByte, combineBytes]
323    bv_decide
324  
325  theorem combineBytes_extractByte_6 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
326      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 6 = b6 := by
327    simp only [extractByte, combineBytes]
328    bv_decide
329  
330  theorem combineBytes_extractByte_7 (b0 b1 b2 b3 b4 b5 b6 b7 : BitVec 8) :
331      extractByte (combineBytes b0 b1 b2 b3 b4 b5 b6 b7) 7 = b7 := by
332    simp only [extractByte, combineBytes]
333    bv_decide
334  
335  -- The converse: extracting then combining reconstructs the original value
336  -- This is the key theorem for the serialize->parse direction
337  theorem extractBytes_combineBytes (v : BitVec 64) :
338      combineBytes (extractByte v 0) (extractByte v 1) (extractByte v 2) (extractByte v 3)
339                   (extractByte v 4) (extractByte v 5) (extractByte v 6) (extractByte v 7) = v := by
340    simp only [extractByte, combineBytes]
341    bv_decide
342  
343  -- ═══════════════════════════════════════════════════════════════════════════════
344  -- U64LE BOX (complete with proofs)
345  -- ═══════════════════════════════════════════════════════════════════════════════
346  
347  -- Helper: UInt8 ↔ BitVec 8 roundtrip
348  theorem uint8_IsLt (x : UInt8) : x.toNat < 256 := by
349    unfold UInt8.toNat
350    exact x.toBitVec.isLt
351  
352  theorem bitvec8_IsLt (b : BitVec 8) : b.toNat < 256 := b.isLt
353  
354  -- Key: BitVec.ofNat 8 (x.toNat) where x : UInt8 preserves the value
355  theorem ofNat8_uint8_toNat (x : UInt8) : 
356      (BitVec.ofNat 8 x.toNat).toNat = x.toNat := by
357    simp only [BitVec.toNat_ofNat]
358    exact Nat.mod_eq_of_lt (uint8_IsLt x)
359  
360  -- Key: extractByte then toUInt8 then back to BitVec = extractByte
361  theorem extractByte_uint8_roundtrip (v : BitVec 64) (i : Nat) (hi : i < 8) :
362      BitVec.ofNat 8 ((extractByte v i hi).toNat.toUInt8.toNat) = extractByte v i hi := by
363    apply BitVec.eq_of_toNat_eq
364    simp only [BitVec.toNat_ofNat]
365    have hlt : (extractByte v i hi).toNat < 256 := bitvec8_IsLt _
366    -- toUInt8.toNat of a value < 256 is identity
367    have h1 : (extractByte v i hi).toNat.toUInt8.toNat = (extractByte v i hi).toNat := by
368      unfold Nat.toUInt8 UInt8.ofNat UInt8.toNat
369      simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt hlt]
370    rw [h1]
371    exact Nat.mod_eq_of_lt hlt
372  
373  -- Serialize then get byte i gives extractByte v i
374  theorem serializeU64le_getElem (v : BitVec 64) (i : Nat) (hi : i < 8) :
375      (serializeU64le v)[i]'(by simp [serializeU64le_size]; exact hi) = 
376      (extractByte v i hi).toNat.toUInt8 := by
377    simp only [serializeU64le]
378    -- The serialized bytes are [b0, b1, ..., b7].toByteArray
379    -- We need to show that index i gives the i-th element
380    match i with
381    | 0 => simp
382    | 1 => simp
383    | 2 => simp
384    | 3 => simp
385    | 4 => simp
386    | 5 => simp
387    | 6 => simp
388    | 7 => simp
389  
390  -- Combined lemma: BitVec.ofNat 8 (serializeU64le v)[i].toNat = extractByte v i _
391  -- This allows simp to work instead of conv
392  -- We prove individual instances for each index to make simp work
393  @[simp] theorem serializeU64le_bitvec_0 (v : BitVec 64) (h : 0 < (serializeU64le v).size := by simp) :
394      BitVec.ofNat 8 (serializeU64le v)[0].toNat = extractByte v 0 (by omega) := by
395    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
396  
397  @[simp] theorem serializeU64le_bitvec_1 (v : BitVec 64) (h : 1 < (serializeU64le v).size := by simp) :
398      BitVec.ofNat 8 (serializeU64le v)[1].toNat = extractByte v 1 (by omega) := by
399    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
400  
401  @[simp] theorem serializeU64le_bitvec_2 (v : BitVec 64) (h : 2 < (serializeU64le v).size := by simp) :
402      BitVec.ofNat 8 (serializeU64le v)[2].toNat = extractByte v 2 (by omega) := by
403    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
404  
405  @[simp] theorem serializeU64le_bitvec_3 (v : BitVec 64) (h : 3 < (serializeU64le v).size := by simp) :
406      BitVec.ofNat 8 (serializeU64le v)[3].toNat = extractByte v 3 (by omega) := by
407    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
408  
409  @[simp] theorem serializeU64le_bitvec_4 (v : BitVec 64) (h : 4 < (serializeU64le v).size := by simp) :
410      BitVec.ofNat 8 (serializeU64le v)[4].toNat = extractByte v 4 (by omega) := by
411    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
412  
413  @[simp] theorem serializeU64le_bitvec_5 (v : BitVec 64) (h : 5 < (serializeU64le v).size := by simp) :
414      BitVec.ofNat 8 (serializeU64le v)[5].toNat = extractByte v 5 (by omega) := by
415    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
416  
417  @[simp] theorem serializeU64le_bitvec_6 (v : BitVec 64) (h : 6 < (serializeU64le v).size := by simp) :
418      BitVec.ofNat 8 (serializeU64le v)[6].toNat = extractByte v 6 (by omega) := by
419    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
420  
421  @[simp] theorem serializeU64le_bitvec_7 (v : BitVec 64) (h : 7 < (serializeU64le v).size := by simp) :
422      BitVec.ofNat 8 (serializeU64le v)[7].toNat = extractByte v 7 (by omega) := by
423    rw [serializeU64le_getElem, extractByte_uint8_roundtrip]
424  
425  -- The big theorem: parsing serialized bytes reconstructs the original value
426  theorem parseU64le_serializeU64le (v : BitVec 64) :
427      parseU64le (serializeU64le v) = ParseResult.ok v ByteArray.empty := by
428    simp only [parseU64le]
429    have hsize : (serializeU64le v).size ≥ 8 := by simp [serializeU64le_size]
430    simp only [hsize, ↓reduceDIte]
431    -- Extract goes from 8 to 8, giving empty
432    have hextract : (serializeU64le v).extract 8 (serializeU64le v).size = ByteArray.empty := by
433      simp [serializeU64le_size]
434    -- Now show the combined value equals v and rest is empty
435    -- Goal: ParseResult.ok (combineBytes ...) (extract ...) = ParseResult.ok v empty
436    -- Use congr to split into showing combineBytes ... = v and extract ... = empty
437    -- hextract proves the second component, so we use simp with it first
438    simp only [hextract]
439    -- Now just need to show combineBytes ... = v
440    congr 1
441    simp only [serializeU64le_bitvec_0, serializeU64le_bitvec_1, serializeU64le_bitvec_2,
442               serializeU64le_bitvec_3, serializeU64le_bitvec_4, serializeU64le_bitvec_5,
443               serializeU64le_bitvec_6, serializeU64le_bitvec_7]
444    exact extractBytes_combineBytes v
445  
446  -- Consumption: parsing serialized bytes ++ extra leaves extra
447  theorem parseU64le_serializeU64le_append (v : BitVec 64) (extra : Bytes) :
448      parseU64le (serializeU64le v ++ extra) = ParseResult.ok v extra := by
449    simp only [parseU64le]
450    have hsize : (serializeU64le v ++ extra).size ≥ 8 := by 
451      simp [ByteArray.size_append, serializeU64le_size]
452    simp only [hsize, ↓reduceDIte]
453    -- Extract from position 8 gives extra
454    have hextract : (serializeU64le v ++ extra).extract 8 (serializeU64le v ++ extra).size = extra := by
455      have hi : 8 = (serializeU64le v).size := by simp [serializeU64le_size]
456      have hj : (serializeU64le v ++ extra).size = (serializeU64le v).size + extra.size := by
457        simp [ByteArray.size_append]
458      rw [hj, ByteArray.extract_append_eq_right hi rfl]
459    -- Use hextract to simplify the second component
460    simp only [hextract]
461    -- Now just need to show combineBytes ... = v
462    congr 1
463    -- Same as above but with append
464    have h0 : (0 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
465    have h1 : (1 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
466    have h2 : (2 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
467    have h3 : (3 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
468    have h4 : (4 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
469    have h5 : (5 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
470    have h6 : (6 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
471    have h7 : (7 : Nat) < (serializeU64le v).size := by simp [serializeU64le_size]
472    simp only [ByteArray.getElem_append_left h0, ByteArray.getElem_append_left h1,
473               ByteArray.getElem_append_left h2, ByteArray.getElem_append_left h3,
474               ByteArray.getElem_append_left h4, ByteArray.getElem_append_left h5,
475               ByteArray.getElem_append_left h6, ByteArray.getElem_append_left h7]
476    simp only [serializeU64le_bitvec_0, serializeU64le_bitvec_1, serializeU64le_bitvec_2,
477               serializeU64le_bitvec_3, serializeU64le_bitvec_4, serializeU64le_bitvec_5,
478               serializeU64le_bitvec_6, serializeU64le_bitvec_7]
479    exact extractBytes_combineBytes v
480  
481  /-- The verified u64le box -/
482  def u64leBitVec : Box (BitVec 64) where
483    parse := parseU64le
484    serialize := serializeU64le
485    roundtrip := parseU64le_serializeU64le
486    consumption := parseU64le_serializeU64le_append
487  
488  -- ═══════════════════════════════════════════════════════════════════════════════
489  -- U32LE BOX (32-bit little-endian, for Protobuf fixed32)
490  -- ═══════════════════════════════════════════════════════════════════════════════
491  
492  /-- Extract byte i from a 32-bit value (little-endian) -/
493  def extractByte32 (v : BitVec 32) (i : Nat) (_ : i < 4 := by omega) : BitVec 8 :=
494    (v >>> (i * 8)).setWidth 8
495  
496  /-- Combine 4 bytes into a 32-bit value (little-endian) -/
497  def combineBytes32 (b0 b1 b2 b3 : BitVec 8) : BitVec 32 :=
498    b0.setWidth 32 |||
499    (b1.setWidth 32 <<< 8) |||
500    (b2.setWidth 32 <<< 16) |||
501    (b3.setWidth 32 <<< 24)
502  
503  /-- Serialize a 32-bit value to 4 bytes -/
504  def serializeU32le (v : BitVec 32) : Bytes :=
505    let b0 : UInt8 := (extractByte32 v 0).toNat.toUInt8
506    let b1 : UInt8 := (extractByte32 v 1).toNat.toUInt8
507    let b2 : UInt8 := (extractByte32 v 2).toNat.toUInt8
508    let b3 : UInt8 := (extractByte32 v 3).toNat.toUInt8
509    [b0, b1, b2, b3].toByteArray
510  
511  /-- Parse 4 bytes as a 32-bit value -/
512  def parseU32le (bs : Bytes) : ParseResult (BitVec 32) :=
513    if h : bs.size ≥ 4 then
514      let b0 := BitVec.ofNat 8 bs[0].toNat
515      let b1 := BitVec.ofNat 8 bs[1].toNat
516      let b2 := BitVec.ofNat 8 bs[2].toNat
517      let b3 := BitVec.ofNat 8 bs[3].toNat
518      .ok (combineBytes32 b0 b1 b2 b3) (bs.extract 4 bs.size)
519    else .fail
520  
521  @[simp] theorem serializeU32le_size (v : BitVec 32) : (serializeU32le v).size = 4 := by
522    simp [serializeU32le, List.size_toByteArray]
523  
524  -- Byte extraction lemmas (bv_decide)
525  theorem combineBytes32_extractByte_0 (b0 b1 b2 b3 : BitVec 8) :
526      extractByte32 (combineBytes32 b0 b1 b2 b3) 0 = b0 := by
527    simp only [extractByte32, combineBytes32]
528    bv_decide
529  
530  theorem combineBytes32_extractByte_1 (b0 b1 b2 b3 : BitVec 8) :
531      extractByte32 (combineBytes32 b0 b1 b2 b3) 1 = b1 := by
532    simp only [extractByte32, combineBytes32]
533    bv_decide
534  
535  theorem combineBytes32_extractByte_2 (b0 b1 b2 b3 : BitVec 8) :
536      extractByte32 (combineBytes32 b0 b1 b2 b3) 2 = b2 := by
537    simp only [extractByte32, combineBytes32]
538    bv_decide
539  
540  theorem combineBytes32_extractByte_3 (b0 b1 b2 b3 : BitVec 8) :
541      extractByte32 (combineBytes32 b0 b1 b2 b3) 3 = b3 := by
542    simp only [extractByte32, combineBytes32]
543    bv_decide
544  
545  -- The converse: extracting all bytes and combining gives back original
546  theorem extractBytes32_combineBytes (v : BitVec 32) :
547      combineBytes32 (extractByte32 v 0) (extractByte32 v 1) 
548                     (extractByte32 v 2) (extractByte32 v 3) = v := by
549    simp only [extractByte32, combineBytes32]
550    bv_decide
551  
552  -- UInt8 roundtrip for 32-bit
553  theorem extractByte32_uint8_roundtrip (v : BitVec 32) (i : Nat) (hi : i < 4) :
554      BitVec.ofNat 8 ((extractByte32 v i hi).toNat.toUInt8.toNat) = extractByte32 v i hi := by
555    apply BitVec.eq_of_toNat_eq
556    simp only [BitVec.toNat_ofNat]
557    have hlt : (extractByte32 v i hi).toNat < 256 := bitvec8_IsLt _
558    have h1 : (extractByte32 v i hi).toNat.toUInt8.toNat = (extractByte32 v i hi).toNat := by
559      unfold Nat.toUInt8 UInt8.ofNat UInt8.toNat
560      simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt hlt]
561    rw [h1]
562    exact Nat.mod_eq_of_lt hlt
563  
564  theorem serializeU32le_getElem (v : BitVec 32) (i : Nat) (hi : i < 4) :
565      (serializeU32le v)[i]'(by simp [serializeU32le_size]; exact hi) = 
566      (extractByte32 v i hi).toNat.toUInt8 := by
567    simp only [serializeU32le]
568    match i with
569    | 0 => simp
570    | 1 => simp
571    | 2 => simp
572    | 3 => simp
573  
574  -- Combined simp lemmas for the proof
575  @[simp] theorem serializeU32le_bitvec_0 (v : BitVec 32) (h : 0 < (serializeU32le v).size := by simp) :
576      BitVec.ofNat 8 (serializeU32le v)[0].toNat = extractByte32 v 0 (by omega) := by
577    rw [serializeU32le_getElem, extractByte32_uint8_roundtrip]
578  
579  @[simp] theorem serializeU32le_bitvec_1 (v : BitVec 32) (h : 1 < (serializeU32le v).size := by simp) :
580      BitVec.ofNat 8 (serializeU32le v)[1].toNat = extractByte32 v 1 (by omega) := by
581    rw [serializeU32le_getElem, extractByte32_uint8_roundtrip]
582  
583  @[simp] theorem serializeU32le_bitvec_2 (v : BitVec 32) (h : 2 < (serializeU32le v).size := by simp) :
584      BitVec.ofNat 8 (serializeU32le v)[2].toNat = extractByte32 v 2 (by omega) := by
585    rw [serializeU32le_getElem, extractByte32_uint8_roundtrip]
586  
587  @[simp] theorem serializeU32le_bitvec_3 (v : BitVec 32) (h : 3 < (serializeU32le v).size := by simp) :
588      BitVec.ofNat 8 (serializeU32le v)[3].toNat = extractByte32 v 3 (by omega) := by
589    rw [serializeU32le_getElem, extractByte32_uint8_roundtrip]
590  
591  -- Main roundtrip theorem
592  theorem parseU32le_serializeU32le (v : BitVec 32) :
593      parseU32le (serializeU32le v) = ParseResult.ok v ByteArray.empty := by
594    simp only [parseU32le]
595    have hsize : (serializeU32le v).size ≥ 4 := by simp [serializeU32le_size]
596    simp only [hsize, ↓reduceDIte]
597    have hextract : (serializeU32le v).extract 4 (serializeU32le v).size = ByteArray.empty := by
598      simp [serializeU32le_size]
599    simp only [hextract]
600    congr 1
601    simp only [serializeU32le_bitvec_0, serializeU32le_bitvec_1, 
602               serializeU32le_bitvec_2, serializeU32le_bitvec_3]
603    exact extractBytes32_combineBytes v
604  
605  -- Consumption theorem
606  theorem parseU32le_serializeU32le_append (v : BitVec 32) (extra : Bytes) :
607      parseU32le (serializeU32le v ++ extra) = ParseResult.ok v extra := by
608    simp only [parseU32le]
609    have hsize : (serializeU32le v ++ extra).size ≥ 4 := by 
610      simp [ByteArray.size_append, serializeU32le_size]
611    simp only [hsize, ↓reduceDIte]
612    have hextract : (serializeU32le v ++ extra).extract 4 (serializeU32le v ++ extra).size = extra := by
613      have hi : 4 = (serializeU32le v).size := by simp [serializeU32le_size]
614      have hj : (serializeU32le v ++ extra).size = (serializeU32le v).size + extra.size := by
615        simp [ByteArray.size_append]
616      rw [hj, ByteArray.extract_append_eq_right hi rfl]
617    simp only [hextract]
618    congr 1
619    have h0 : (0 : Nat) < (serializeU32le v).size := by simp [serializeU32le_size]
620    have h1 : (1 : Nat) < (serializeU32le v).size := by simp [serializeU32le_size]
621    have h2 : (2 : Nat) < (serializeU32le v).size := by simp [serializeU32le_size]
622    have h3 : (3 : Nat) < (serializeU32le v).size := by simp [serializeU32le_size]
623    simp only [ByteArray.getElem_append_left h0, ByteArray.getElem_append_left h1,
624               ByteArray.getElem_append_left h2, ByteArray.getElem_append_left h3]
625    simp only [serializeU32le_bitvec_0, serializeU32le_bitvec_1,
626               serializeU32le_bitvec_2, serializeU32le_bitvec_3]
627    exact extractBytes32_combineBytes v
628  
629  /-- The verified u32le box -/
630  def u32leBitVec : Box (BitVec 32) where
631    parse := parseU32le
632    serialize := serializeU32le
633    roundtrip := parseU32le_serializeU32le
634    consumption := parseU32le_serializeU32le_append
635  
636  -- ═══════════════════════════════════════════════════════════════════════════════
637  -- DERIVED BOXES (built from primitives)
638  -- ═══════════════════════════════════════════════════════════════════════════════
639  
640  /-- Two bytes (u8, u8) -/
641  def u8pair : Box (UInt8 × UInt8) := seq u8 u8
642  
643  /-- Three bytes -/
644  def u8triple : Box ((UInt8 × UInt8) × UInt8) := seq u8pair u8
645  
646  /-- Four bytes -/
647  def u8quad : Box (((UInt8 × UInt8) × UInt8) × UInt8) := seq u8triple u8
648  
649  -- ═══════════════════════════════════════════════════════════════════════════════
650  -- EXAMPLE: Using isoBox to create a wrapped type
651  -- ═══════════════════════════════════════════════════════════════════════════════
652  
653  /-- A wrapper type for demonstration -/
654  structure WrappedByte where
655    val : UInt8
656    deriving DecidableEq
657  
658  /-- Box for WrappedByte -/
659  def wrappedByte : Box WrappedByte := 
660    isoBox u8 
661      WrappedByte.mk 
662      WrappedByte.val
663      (fun _ => rfl)
664      (fun ⟨_⟩ => rfl)
665  
666  -- ═══════════════════════════════════════════════════════════════════════════════
667  -- STATISTICS
668  -- ═══════════════════════════════════════════════════════════════════════════════
669  
670  /-!
671  ## Verification Status
672  
673  ### Fully Verified Boxes (0 sorry):
674  
675  | Box/Combinator | Roundtrip | Consumption | Status |
676  |----------------|-----------|-------------|--------|
677  | unit           | ✓ proven  | ✓ proven    | DONE   |
678  | u8             | ✓ proven  | ✓ proven    | DONE   |
679  | u32leBitVec    | ✓ proven  | ✓ proven    | DONE   |
680  | u64leBitVec    | ✓ proven  | ✓ proven    | DONE   |
681  | seq            | ✓ proven  | ✓ proven    | DONE   |
682  | isoBox         | ✓ proven  | ✓ proven    | DONE   |
683  
684  ### BitVec Lemmas (bv_decide, 0 sorry):
685  
686  | Lemma | What's Proven |
687  |-------|---------------|
688  | combineBytes_extractByte_0..7 | extractByte(combine(b0..b7), i) = bi |
689  | combineBytes32_extractByte_0..3 | extractByte32(combine32(b0..b3), i) = bi |
690  | extractBytes_combineBytes | combine(extractByte(v, 0..7)) = v |
691  | extractBytes32_combineBytes | combine32(extractByte32(v, 0..3)) = v |
692  | parseU64le_serializeU64le | parse(serialize(v)) = ok v empty |
693  | parseU32le_serializeU32le | parse(serialize(v)) = ok v empty |
694  
695  ### Derived (compositionally verified):
696  
697  | Box | Built From |
698  |-----|------------|
699  | u8pair | seq u8 u8 |
700  | u8triple | seq u8pair u8 |  
701  | u8quad | seq u8triple u8 |
702  | wrappedByte | isoBox u8 |
703  | u64le (UInt64) | isoBox u64leBitVec (via Basic.lean) |
704  | u32le (UInt32) | isoBox u32leBitVec (via Basic.lean) |
705  | bool64 | isoBox u64leBitVec (via Basic.lean) |
706  
707  **Total: 6 primitive boxes, 50+ theorems, 0 sorry in Proofs.lean**
708  **Compositionally: infinite verified boxes constructible**
709  -/
710  
711  end Cornell.Proofs