trees.c.reverse.lean

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

1import ZlibF.Proof.«trees.c.inv»
2
3/-!
4# trees.c: `bi_reverse` (safety and bit reversal)
5
6The arithmetic lemmas `revBits`, `body_step` and `shr1` are the ones of the earlier proof of `bi_reverse`
7(machine-integer facts, unchanged); the loop argument is redone for the present runtime (`Wp.cdoWhile`).
8-/
9
10namespace Zlib.Trees.Proofs.Out
11open C Zlib.Trees
12
13/-- Reverse of the low `k` bits of `c`: bit `i` of `c` becomes bit `k - 1 - i`. -/
14def revBits (c : Nat) : Nat → Nat
15  | 0 => 0
16  | k + 1 => 2 * revBits c k + (c / 2 ^ k) % 2
17
18theorem revBits_lt (c k : Nat) : revBits c k < 2 ^ k := by
19  induction k with
20  | zero => simp [revBits]
21  | succ k ih => simp only [revBits, Nat.pow_succ]; omega
22
23theorem body_step (c r : UInt32) (R : Nat) (hr : r.toNat = 2 * R) (hR : 2 * (2 * R + 1) < 2 ^ 32) :
24    ((r ||| (c &&& 1)) <<< 1).toNat = 2 * (2 * R + c.toNat % 2) := by
25  have hb : (c &&& 1).toNat = c.toNat % 2 := by
26    rw [UInt32.toNat_and]; exact Nat.and_one_is_mod _
27  have hor : (r ||| (c &&& 1)).toNat = 2 * R + c.toNat % 2 := by
28    rw [UInt32.toNat_or, hr, hb, show 2 * R = R <<< 1 by rw [Nat.shiftLeft_eq]; omega,
29      ← Nat.shiftLeft_add_eq_or_of_lt (by omega), Nat.shiftLeft_eq]
30  rw [UInt32.toNat_shiftLeft, hor, show (1 : UInt32).toNat % 32 = 1 from rfl, Nat.shiftLeft_eq]
31  have : c.toNat % 2 ≤ 1 := by omega
32  rw [Nat.mod_eq_of_lt (by omega)]
33  simp only [Nat.pow_one]; omega
34
35theorem shr1 (c : UInt32) : (c >>> 1).toNat = c.toNat / 2 := by
36  rw [UInt32.toNat_shiftRight, show (1 : UInt32).toNat % 32 = 1 from rfl, Nat.shiftRight_eq_div_pow]
37
38theorem i32_toInt_bounds (x : Int32) : -2147483648 ≤ x.toInt ∧ x.toInt ≤ 2147483647 := by
39  have h1 := Int32.le_toInt x
40  have h2 := Int32.toInt_le x
41  have e1 : Int32.minValue.toInt = -2147483648 := by decide
42  have e2 : Int32.maxValue.toInt = 2147483647 := by decide
43  rw [e2] at h2
44  exact ⟨by omega, h2⟩
45
46theorem i32_one_toInt : (1 : Int32).toInt = 1 := by decide
47
48/-- **`bi_reverse`, safety.** For every `len` above `INT_MIN` (so `--len` does not overflow) and every `code`,
49`bi_reverse(code, len)` ends without undefined behaviour (it runs `max(len, 1)` times) and does not touch the heap.
50`gen_codes` calls it with `1 <= len <= 15`. -/
51theorem bi_reverse_safe (h : Heap) (code : UInt32) (len : Int32) (hl : -2147483648 < len.toInt) :
52    ∃ r, bi_reverse code len h = .ok (r, h) := by
53  have key : Wp (cdoWhile (σ := UInt32 × UInt32 × Int32)
54      (fun (code, res, len) => do
55        let res := res ||| (code &&& 1)
56        pure (code >>> 1, res <<< 1, len))
57      (fun (code, res, len) => do
58        let len ← isub len 1
59        pure (decide (len.toInt > 0), (code, res, len))) (code, 0, len)) h (fun _ h' => h' = h) := by
60    refine Wp.cdoWhile (s := (code, 0, len)) (h := h) (fun s h' => h' = h ∧ -2147483648 < s.2.2.toInt) (fun s => s.2.2.toInt.toNat) _ ?_
61      ⟨rfl, hl⟩ (by have := (i32_toInt_bounds len).2; simp only [fuel]; omega)
62    rintro ⟨c, r, l⟩ h' ⟨rfl, hl'⟩
63    have hl' : -2147483648 < l.toInt := hl'
64    have hub := (i32_toInt_bounds l).2
65    refine ⟨_, _, rfl, ?_⟩
66    have e : isub l 1 = pure (Int32.ofInt (l.toInt - 1)) :=
67      (isub_eq (a := l) (b := 1) (by rw [i32_one_toInt]; omega) (by rw [i32_one_toInt]; omega)).trans
68        (by rw [i32_one_toInt])
69    have hn : (Int32.ofInt (l.toInt - 1)).toInt = l.toInt - 1 :=
70      i32_ofInt_toInt (by omega) (by omega)
71    by_cases hp : l.toInt - 1 > 0
72    · right
73      refine ⟨(c >>> 1, (r ||| c &&& 1) <<< 1, Int32.ofInt (l.toInt - 1)), h', ?_, ⟨rfl, ?_⟩, ?_⟩
74      · simp only [e, pure_app, bind_app, hn, hp, decide_true]
75      · simp only [hn]; omega
76      · simp only [hn]; omega
77    · left
78      refine ⟨(c >>> 1, (r ||| c &&& 1) <<< 1, Int32.ofInt (l.toInt - 1)), h', ?_, rfl⟩
79      simp only [e, pure_app, bind_app, hn, hp, decide_false]
80  obtain ⟨r, h', e, rfl⟩ := key
81  refine ⟨r.2.1 >>> 1, ?_⟩
82  unfold bi_reverse
83  simp only [bind_app, e]
84  rfl
85
86
87/-- **`bi_reverse`, correctness.** For `1 <= len <= 31`, `bi_reverse(code, len)` returns the low `len` bits of
88`code` in reverse order (`revBits`: bit `i` of `code` becomes bit `len - 1 - i`) and leaves the heap unchanged.
89zlib calls it with `1 <= len <= 15` (code lengths). (For `len = 32` the C loses the top bit to the final `>> 1`;
90that case is not needed.) -/
91theorem bi_reverse_correct (h : Heap) (code : UInt32) (len : Int32) (h1 : 1 ≤ len.toInt) (h2 : len.toInt ≤ 31) :
92    ∃ r : UInt32, bi_reverse code len h = .ok (r, h) ∧ r.toNat = revBits code.toNat len.toInt.toNat := by
93  obtain ⟨k, hk⟩ : ∃ k : Nat, k = len.toInt.toNat := ⟨_, rfl⟩
94  have hkl : len.toInt = k := by omega
95  have key : Wp (cdoWhile (σ := UInt32 × UInt32 × Int32)
96      (fun (code, res, len) => do
97        let res := res ||| (code &&& 1)
98        pure (code >>> 1, res <<< 1, len))
99      (fun (code, res, len) => do
100        let len ← isub len 1
101        pure (decide (len.toInt > 0), (code, res, len))) (code, 0, len)) h
102      (fun s h' => h' = h ∧ s.2.1.toNat = 2 * revBits code.toNat k) := by
103    refine Wp.cdoWhile (s := (code, 0, len)) (h := h)
104      (fun s h' => h' = h ∧ 1 ≤ s.2.2.toInt ∧ s.2.2.toInt ≤ (k : Int) ∧
105        s.1.toNat = code.toNat / 2 ^ (k - s.2.2.toInt.toNat) ∧ s.2.1.toNat = 2 * revBits code.toNat (k - s.2.2.toInt.toNat))
106      (fun s => s.2.2.toInt.toNat) _ ?_ ⟨rfl, h1, (by show len.toInt ≤ (k : Int); omega), ?_, ?_⟩ (by show len.toInt.toNat < fuel; unfold fuel; omega)
107    · rintro ⟨c, r, l⟩ h' ⟨rfl, hl1, hl2, hc, hr⟩
108      simp only [] at hl1 hl2 hc hr
109      refine ⟨_, _, rfl, ?_⟩
110      have hub := (i32_toInt_bounds l).2
111      have e : isub l 1 = pure (Int32.ofInt (l.toInt - 1)) :=
112        (isub_eq (a := l) (b := 1) (by rw [i32_one_toInt]; omega) (by rw [i32_one_toInt]; omega)).trans
113          (by rw [i32_one_toInt])
114      have hn : (Int32.ofInt (l.toInt - 1)).toInt = l.toInt - 1 :=
115        i32_ofInt_toInt (by omega) (by omega)
116      have hlt := revBits_lt code.toNat (k - l.toInt.toNat)
117      have hpow : 2 ^ (k - l.toInt.toNat) ≤ 2 ^ 30 := Nat.pow_le_pow_right (by decide) (by omega)
118      have hs1 : ((r ||| (c &&& 1)) <<< 1).toNat = 2 * revBits code.toNat (k - (l.toInt - 1).toNat) := by
119        rw [body_step _ _ _ hr (by omega), hc, show k - (l.toInt - 1).toNat = (k - l.toInt.toNat) + 1 by omega,
120          revBits]
121      have hs2 : (c >>> 1).toNat = code.toNat / 2 ^ (k - (l.toInt - 1).toNat) := by
122        rw [shr1, hc, show k - (l.toInt - 1).toNat = (k - l.toInt.toNat) + 1 by omega, Nat.pow_succ,
123          Nat.div_div_eq_div_mul]
124      by_cases hp : l.toInt - 1 > 0
125      · right
126        refine ⟨(c >>> 1, (r ||| c &&& 1) <<< 1, Int32.ofInt (l.toInt - 1)), h', ?_, ⟨rfl, ?_⟩, ?_⟩
127        · simp only [e, pure_app, bind_app, hn, hp, decide_true]
128        · simp only [hn]; exact ⟨by omega, by omega, hs2, hs1⟩
129        · simp only [hn]; omega
130      · left
131        refine ⟨(c >>> 1, (r ||| c &&& 1) <<< 1, Int32.ofInt (l.toInt - 1)), h', ?_, rfl, ?_⟩
132        · simp only [e, pure_app, bind_app, hn, hp, decide_false]
133        · have : l.toInt = 1 := by omega
134          have hk0 : k - (l.toInt - 1).toNat = k := by omega
135          simp only []
136          rw [hs1, hk0]
137    · rw [hkl, Int.toNat_natCast, Nat.sub_self]; simp
138    · rw [hkl, Int.toNat_natCast, Nat.sub_self]; simp [revBits]
139  obtain ⟨r, h', e, rfl, hq⟩ := key
140  refine ⟨r.2.1 >>> 1, ?_, ?_⟩
141  · unfold bi_reverse
142    simp only [bind_app, e]
143    rfl
144  · rw [shr1, hq, ← hk]; omega
145
146end Zlib.Trees.Proofs.Out