InflatePrefixes.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Api.Inflate
2import ZlibF.Proof.Format.Wrapper
3import ZlibF.Proof.«inffast.c.sig»
4
5/-! Bit-prefix comparison for byte streams. No heap or execution hypothesis is used. -/
6
7namespace ZlibF.Spec.Api.Proofs
8open ZlibF.Spec
9
10theorem bytesToBits_prefix {a b : List UInt8} (h : a <+: b) :
11    bytesToBits a <+: bytesToBits b := by
12  obtain ⟨tail, rfl⟩ := h
13  exact ⟨bytesToBits tail, by simp [bytesToBits, List.flatMap_append]⟩
14
15theorem bit_compatible_of_byte_compatible {pfx : List Bool} {input stream : List UInt8}
16    (hp : pfx <+: bytesToBits input) (hc : input <+: stream ∨ stream <+: input) :
17    Layer.BitCompatible pfx stream := by
18  rcases hc with hc | hc
19  · exact Or.inl (hp.trans (bytesToBits_prefix hc))
20  · have hs := bytesToBits_prefix hc
21    by_cases hl : pfx.length ≤ (bytesToBits stream).length
22    · exact Or.inl (List.prefix_of_prefix_length_le hp hs hl)
23    · exact Or.inr (List.prefix_of_prefix_length_le hs hp (by omega))
24
25private theorem read_byte_bits (byte : UInt8) (tail : List Bool) :
26    readBits 8 (byteBits byte ++ tail) = some (byte.toNat, tail) := by
27  change readBits 8 (Zlib.Inffast.Proofs.bitsOfNat byte.toNat 8 ++ tail) = _
28  simpa only [show 2 ^ 8 = (256 : Nat) from rfl, Nat.mod_eq_of_lt byte.toNat_lt,
29    Nat.sub_self, Zlib.Inffast.Proofs.bitsOfNat_zero, List.nil_append] using
30    Zlib.Inffast.Proofs.readBits_bitsOfNat 8 8 byte.toNat tail (by omega)
31
32/-- Whole-byte prefix comparison is reflected by the bit encoding. -/
33theorem bytesToBits_prefix_reflect {a b : List UInt8}
34    (h : bytesToBits a <+: bytesToBits b) : a <+: b := by
35  induction a generalizing b with
36  | nil => exact List.nil_prefix
37  | cons byte a ih =>
38    cases b with
39    | nil =>
40      have hl := h.length_le
41      simp [ZlibF.Spec.Proofs.bytesToBits_len] at hl
42    | cons other b =>
43      obtain ⟨tail, heq⟩ := h
44      have hr := congrArg (readBits 8) heq
45      change readBits 8 ((byteBits byte ++ bytesToBits a) ++ tail) =
46        readBits 8 (byteBits other ++ bytesToBits b) at hr
47      rw [List.append_assoc, read_byte_bits, read_byte_bits] at hr
48      simp only [Option.some.injEq, Prod.mk.injEq] at hr
49      have hbyte : byte = other := UInt8.toNat_inj.mp hr.1
50      subst other
51      obtain ⟨suffix, hs⟩ := ih ⟨tail, hr.2⟩
52      exact ⟨suffix, by simp only [List.cons_append, hs]⟩
53
54
55end ZlibF.Spec.Api.Proofs