public-gzbuffer.lean

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

1import ZlibF.Spec.Public.GzControl
2import ZlibF.Proof.«gzlib.c.base»
3
4namespace ZlibF.Spec.Public.Proofs
5open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
6
7/-- `int gzbuffer(gzFile file, unsigned size)` checks the mode, existing
8allocation and overflow before changing the requested size. -/
9theorem gzbuffer_record {h : Heap} {i : Nat} {s : GzState} (hs : h.gzstates i = some s)
10    (size : UInt32) :
11    C.run (gzbuffer (hnd i) size) h =
12      if (s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE) ∨ s.size ≠ 0 ∨ 2 ^ 31 ≤ size.toNat then
13        .ok (-1, h)
14      else .ok (0, setS h i { s with want := UInt32.ofNat (max size.toNat 8) }) := by
15  have heq : (if size < 8 then 8 else size) = UInt32.ofNat (max size.toNat 8) := by
16    by_cases hs8 : size < 8
17    · have hn : size.toNat < 8 := by simpa using (UInt32.lt_iff_toNat_lt.mp hs8)
18      simp [hs8, Nat.max_eq_right (by omega : size.toNat ≤ 8)]
19    · have hn : 8 ≤ size.toNat := by
20        have hp : ¬ size.toNat < 8 := fun hp => hs8 (UInt32.lt_iff_toNat_lt.mpr (by simpa using hp))
21        omega
22      simp [hs8, Nat.max_eq_left hn]
23  have hd : (size <<< 1) < size ↔ 2 ^ 31 ≤ size.toNat := by
24    rw [UInt32.lt_iff_toNat_lt, UInt32.toNat_shiftLeft]
25    have := size.toNat_lt
26    simp only [UInt32.toNat_ofNat, Nat.reducePow] at *
27    rcases Nat.lt_or_ge size.toNat (2 ^ 31) with h1 | h1
28    · have : (1 : UInt32).toNat % 32 = 1 := rfl
29      simp [this]; omega
30    · have : (1 : UInt32).toNat % 32 = 1 := rfl
31      simp [this]; omega
32  unfold C.run gzbuffer
33  by_cases hm : s.mode ≠ GZ_READ ∧ s.mode ≠ GZ_WRITE
34  · gsimp [hs, hm.1, hm.2]
35  · have hm' : s.mode = GZ_READ ∨ s.mode = GZ_WRITE := by
36      by_cases hr : s.mode = GZ_READ
37      · exact Or.inl hr
38      · exact Or.inr (Classical.byContradiction (fun hw => hm ⟨hr, hw⟩))
39    by_cases hsize : s.size ≠ 0
40    · rcases hm' with hm1 | hm1 <;> gsimp [hs, hm1, hsize, GZ_READ, GZ_WRITE]
41    · by_cases hov : (size <<< 1) < size
42      · have hn := hd.mp hov
43        rcases hm' with hm1 | hm1 <;> gsimp [hs, hm1, hsize, hov, hn, GZ_READ, GZ_WRITE]
44      · have hn : ¬ 2 ^ 31 ≤ size.toNat := fun x => hov (hd.mpr x)
45        have hz : s.size = 0 := by simpa using hsize
46        rcases hm' with hm1 | hm1 <;> gsimp [hs, hm1, hz, hov, hn, heq, GZ_READ, GZ_WRITE]
47
48/-- `int gzbuffer(gzFile file, unsigned size)` satisfies the public goal. -/
49theorem gzbuffer_public : Goal.gzbuffer := by
50  constructor
51  · intro h size
52    rfl
53  · intro h i s size hs
54    simpa [hnd, setS, putGz] using gzbuffer_record hs size
55
56#print axioms gzbuffer_record
57#print axioms gzbuffer_public
58
59end ZlibF.Spec.Public.Proofs