inffast.c.dist.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«inffast.c.sig»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
5
6theorem u8_forall (P : UInt8 → Prop) (h : ∀ n, n < 256 → P (UInt8.ofNat n)) : ∀ x, P x := by
7  intro x
8  have := h x.toNat x.toNat_lt
9  simpa using this
10
11theorem mask16 : ∀ x : UInt8, ((x.toUInt32 &&& 16) != 0) = ((x &&& 16) != 0) :=
12  u8_forall _ (by decide +kernel)
13theorem mask64 : ∀ x : UInt8, ((x.toUInt32 &&& 64) == 0) = ((x &&& 64) == 0) :=
14  u8_forall _ (by decide +kernel)
15theorem mask32 : ∀ x : UInt8, ((x.toUInt32 &&& 32) != 0) = ((x &&& 32) != 0) :=
16  u8_forall _ (by decide +kernel)
17theorem mask15 : ∀ x : UInt8, (x.toUInt32 &&& 15).toNat = (x &&& 15).toNat :=
18  u8_forall _ (by decide +kernel)
19theorem toNat32 : ∀ x : UInt8, x.toUInt32.toNat = x.toNat :=
20  u8_forall _ (by decide +kernel)
21
22variable {e : Env} {c : Ctx}
23
24theorem LS.congr {l l' : L} {i o : Nat} (hl : LS e l i o) (h1 : l'.in_ = l.in_) (h2 : l'.out = l.out)
25    (h3 : l'.hold = l.hold) (h4 : l'.bits = l.bits) : LS e l' i o := by
26  obtain ⟨a, b, c, d, f, g, h, k⟩ := hl
27  exact ⟨by rw [h1]; exact a, by rw [h2]; exact b, c, d, f, by rw [h4]; exact g, by rw [h3, h4]; exact h,
28    by rw [h4]; exact k⟩
29
30/-- `hold >>= k; bits -= k;` -/
31def dropL (l : L) (k : UInt32) : L := { l with hold := l.hold >>> k.toUInt64, bits := l.bits - k }
32
33theorem dropL_hold (l : L) (k : UInt32) (hk : k.toNat < 64) :
34    (dropL l k).hold.toNat = l.hold.toNat / 2 ^ k.toNat := u64_shr hk
35
36theorem dropL_bits (l : L) (k : UInt32) (hk : k.toNat ≤ l.bits.toNat) :
37    (dropL l k).bits.toNat = l.bits.toNat - k.toNat := u32_toNat_sub hk
38
39theorem LS.dropL {l : L} {i o : Nat} (hl : LS e l i o) (k : UInt32) (hk : k.toNat ≤ l.bits.toNat) (hk64 : k.toNat < 64) :
40    LS e (dropL l k) i o := by
41  have h1 := dropL_hold l k hk64
42  have h2 := dropL_bits l k hk
43  refine ⟨hl.hin, hl.hout, hl.hi0, hl.hi1, hl.ho0, by rw [h2]; have := hl.hb; omega, ?_, by rw [h2]; have := hl.hacc; omega⟩
44  rw [h1, h2]
45  have := hl.hH
46  have hp : 2 ^ l.bits.toNat = 2 ^ (l.bits.toNat - k.toNat) * 2 ^ k.toNat := by
47    rw [← Nat.pow_add]; congr 1; omega
48  apply (Nat.div_lt_iff_lt_mul (Nat.pow_pos (by omega))).mpr
49  rw [hp] at this
50  exact this
51
52theorem Sg_drop (H b i k : Nat) (hk : k ≤ b) : Sg e (H / 2 ^ k) (b - k) i = (Sg e H b i).drop k := by
53  unfold Sg
54  rw [bitsOfNat_drop H b k hk, List.drop_append_of_le_length (by rw [bitsOfNat_length]; exact hk)]
55
56theorem Sg_dropL (l : L) (k : UInt32) (i : Nat) (hk : k.toNat ≤ l.bits.toNat) (hk64 : k.toNat < 64) :
57    Sg e (dropL l k).hold.toNat (dropL l k).bits.toNat i = (Sg e l.hold.toNat l.bits.toNat i).drop k.toNat := by
58  rw [dropL_hold l k hk64, dropL_bits l k hk]
59  exact Sg_drop _ _ _ _ hk
60
61theorem LS.pullL {l : L} {i o : Nat} (hl : LS e l i o) (hb : l.bits.toNat ≤ 22) (hi : i < e.i0 + e.sm0.avail_in.toNat) :
62    LS e (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (i + 1) o :=
63  LS.pull e hl hb hi _
64
65theorem Sg_pullL {l : L} {i o : Nat} (hl : LS e l i o) (hb : l.bits.toNat ≤ 22) (hi : i < e.i0 + e.sm0.avail_in.toNat) :
66    Sg e (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).hold.toNat
67      (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat (i + 1) = Sg e l.hold.toNat l.bits.toNat i := by
68  rw [pullL_hold _ _ _ hl.hb hl.hH, pullL_bits _ _ _ hl.hb]
69  exact Sg_pull e _ _ _ hl.hH hi
70
71
72theorem shl32_ok {h : Heap} {x n : UInt32} (hn : n.toNat < 32) : OkOn h (shl32 x n) (x <<< n) := by
73  rw [shl32_eq hn]; rfl
74
75theorem shr64_ok {h : Heap} {x n : UInt64} (hn : n.toNat < 64) : OkOn h (shr64 x n) (x >>> n) := by
76  rw [shr64_eq hn]; rfl
77
78theorem i64_toU32 (n : Nat) (h : n < 2 ^ 32) :
79    (Int64.ofInt (n : Int)).toUInt64.toUInt32.toNat = n := by
80  rw [Int64.ofInt_eq_ofNat, UInt64.toNat_toUInt32, ← Int64.toNat_toBitVec]
81  simp
82  omega
83
84theorem i64_toInt (n : Nat) (h : n < 2 ^ 62) : (Int64.ofInt (n : Int)).toInt = n := by
85  rw [Int64.ofInt_eq_ofNat]; exact Int64.toInt_ofNat_of_lt (by omega)
86
87theorem Env.bg_le (e : Env) : e.bg ≤ e.o0 := by unfold Env.bg; omega
88
89/-- `strm->avail_in`-style facts used everywhere. -/
90theorem Env.hroomA (e : Env) : e.o0 + e.sm0.avail_out.toNat ≤ e.A0.size := e.hAsz
91
92/-- The continuation of the distance block after the extra bits were read: add the extra bits to the base, drop them,
93compute how much of the output of this call there is, and copy. -/
94def distCont (c : Ctx) (l : L) : M L := do
95  let m ← shl32 1 l.op
96  let l : L := { l with dist := l.dist + (l.hold.toUInt32 &&& m - 1) }
97  let __do_lift ← shr64 l.hold l.op.toUInt64
98  let l : L := { l with hold := __do_lift }
99  let l : L := { l with bits := l.bits - l.op }
100  let d ← Ptr.diff l.out c.beg
101  let l : L := { l with op := d.toUInt64.toUInt32 }
102  copyMatch c l
103
104theorem distCont_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
105    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
106    (hAb : A.size < 2 ^ 63)
107    (hx : l.op.toNat ≤ 13) (hxb : l.op.toNat ≤ l.bits.toNat) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
108    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false) :
109    Wp (distCont c l) (e.heap A msg m) (fun l' h' =>
110      ∃ xv rest, readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (xv, rest) ∧
111        l'.in_ = l.in_ ∧ l'.againD = l.againD ∧
112        ((l'.broke = false ∧ LS e l' i (o + l.len.toNat) ∧ Sg e l'.hold.toNat l'.bits.toNat i = rest ∧
113            h' = e.heap (matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o (l.dist.toNat + xv) l.len.toNat A) msg m) ∨
114         (l'.broke = true ∧ LS e l' i o ∧ Sg e l'.hold.toNat l'.bits.toNat i = rest ∧ ∃ p, h' = e.heap A p BAD))) := by
115  have hbgo : e.bg ≤ o := by have := e.bg_le; have := hls.ho0; omega
116  have hoA : o ≤ A.size := by omega
117  have hxs : l.op.toNat < 32 := by omega
118  unfold distCont
119  refine Wp.bindO (shl32_ok hxs) ?_
120  dsimp only
121  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
122  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
123  have hpow : 2 ^ l.op.toNat ≤ 2 ^ 13 := Nat.pow_le_pow_right (by omega) hx
124  have hdist' : (l.dist + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.dist.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
125    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
126  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
127  have hbgdef : e.bg = e.o0 - (e.start.toNat - e.sm0.avail_out.toNat) := rfl
128  have hst32 := UInt32.toNat_lt e.start
129  have hstart := e.hstart
130  have hbeg := e.hbeg
131  have hdiff : OkOn (e.heap A msg m) (Ptr.diff l.out c.beg) (Int64.ofInt (((o - e.bg : Nat)) : Int)) := by
132    rw [hls.hout, hc.beg]
133    have := Ptr.diff_ok (r := BRef.blk e.ob) (a := A) (o1 := o) (o2 := e.bg) (e.heap_bytes_ob A msg m) hoA (by omega)
134      ⟨by omega, by omega⟩
135    have e1 : (o : Int) - (e.bg : Int) = ((o - e.bg : Nat) : Int) := by omega
136    rw [e1] at this
137    exact this
138  refine Wp.bindO hdiff ?_
139  have hopn : (Int64.ofInt (((o - e.bg : Nat)) : Int)).toUInt64.toUInt32.toNat = o - e.bg := i64_toU32 _ (by omega)
140  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
141  have hrb := readBits_bitsOfNat l.op.toNat l.bits.toNat l.hold.toNat (inBits e i) hxb
142  have hsg := Sg_dropL (e := e) l l.op i hxb (by omega)
143  refine Wp.mono (copyMatch_run (e := e) (c := c) hc A msg m
144    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits - l.op, here := l.here,
145      op := (Int64.ofInt (((o - e.bg : Nat)) : Int)).toUInt64.toUInt32, len := l.len,
146      dist := l.dist + (l.hold.toUInt32 &&& 1 <<< l.op - 1), from_ := l.from_, broke := l.broke, againL := l.againL,
147      againD := l.againD } o hls.hout hbgo hopn (by simp only [hdist']; omega) hlen.1 (by simp; omega) hbroke) ?_
148  intro l' h' hq
149  have hho0 := hls.ho0
150  obtain ⟨hin, hhold, hbits, -, hagD, hres⟩ := hq
151  refine ⟨l.hold.toNat % 2 ^ l.op.toNat, Sg e (dropL l l.op).hold.toNat (dropL l l.op).bits.toNat i, ?_, hin, hagD, ?_⟩
152  · unfold Sg; rw [hrb, dropL_hold l l.op (by omega), dropL_bits l l.op hxb]
153  · rcases hres with ⟨hb, hout, hh⟩ | ⟨hb, p, hh, hout⟩
154    · refine Or.inl ⟨hb, ⟨?_, hout, hls.hi0, hls.hi1, by omega, ?_, ?_, ?_⟩, ?_, ?_⟩
155      · rw [hin]; exact hls.hin
156      · rw [hbits]; exact hls1.hb
157      · rw [hhold, hbits]; exact hls1.hH
158      · rw [hbits]; exact hls1.hacc
159      · rw [hhold, hbits]; rfl
160      · rw [hh, hdist']
161    · refine Or.inr ⟨hb, ⟨?_, ?_, hls.hi0, hls.hi1, hls.ho0, ?_, ?_, ?_⟩, ?_, p, hh⟩
162      · rw [hin]; exact hls.hin
163      · rw [hout]; exact hls.hout
164      · rw [hbits]; exact hls1.hb
165      · rw [hhold, hbits]; exact hls1.hH
166      · rw [hbits]; exact hls1.hacc
167      · rw [hhold, hbits]; rfl
168
169
170theorem Env.heap_cget (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) (r : CodeRef) :
171    Space.get (e.heap A msg m) r = Space.get e.h0 r := by
172  cases r with
173  | istate_codes id =>
174    simp only [Space.get, e.heap_istates]
175    by_cases hid : id = e.stid
176    · subst hid; simp [e.hs0, upd_same]
177    · simp [upd_ne _ _ _ _ hid]
178  | st_lenfix => simp [Space.get, e.heap_static]
179  | st_distfix => simp [Space.get, e.heap_static]
180
181theorem Env.heap_cget_DCA (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) :
182    Space.get (e.heap A msg m) e.rd = some e.DCA := by rw [e.heap_cget]; exact e.hDCA
183
184theorem Env.heap_cget_LCA (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) :
185    Space.get (e.heap A msg m) e.rl = some e.LCA := by rw [e.heap_cget]; exact e.hLCA
186
187theorem Env.heap_bytes_in (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) :
188    (e.heap A msg m).bytes e.ib = some e.IN := by rw [e.heap_bytes_ne A msg m e.hsep]; exact e.hIN
189
190/-- How a distance-table entry is treated by `dodist`. -/
191abbrev DistClass (e : Env) (E : Code) : Prop :=
192  (E.op &&& 16 ≠ 0 ∧ (E.op &&& 15).toNat ≤ 13 ∧ 1 ≤ E.val.toNat) ∨
193  (E.op &&& 16 = 0 ∧ E.op &&& 64 = 0 ∧ 1 ≤ E.op.toNat ∧ E.op.toNat ≤ 15 ∧ e.od + E.val.toNat + 2 ^ E.op.toNat ≤ e.DCA.size) ∨
194  (E.op &&& 16 = 0 ∧ E.op &&& 64 ≠ 0)
195
196/-- A distance block that ended (no link): a match of length `len` was copied, or an error was found. `S` is the bit
197stream after the code of the distance symbol. -/
198def DistEnd (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) (S : List Bool) (i o len : Nat) (E : Code) (l' : L)
199    (h' : Heap) : Prop :=
200  ¬ DistLink E ∧ l'.againD = false ∧
201  ((∃ i' xv rest, i ≤ i' ∧ i' ≤ i + 2 ∧ readBits (E.op &&& 15).toNat S = some (xv, rest) ∧
202      l'.broke = false ∧ LS e l' i' (o + len) ∧ Sg e l'.hold.toNat l'.bits.toNat i' = rest ∧
203      h' = e.heap (matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o (E.val.toNat + xv) len A) msg m) ∨
204   (∃ i' p, i ≤ i' ∧ i' ≤ i + 2 ∧ l'.broke = true ∧ LS e l' i' o ∧ h' = e.heap A p BAD))
205
206
207/-- After the distance base and the number `op` of extra bits are set: refill the bit buffer (at most twice) and copy. -/
208def dodistBase (c : Ctx) (l_2 : L) : M L := do
209  if l_2.bits < l_2.op then do
210    let __x ← pull l_2
211    if __x.bits < __x.op then do
212      let __x ← pull __x
213      distCont c __x
214    else distCont c __x
215  else distCont c l_2
216
217theorem dodistBase_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
218    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
219    (hAb : A.size < 2 ^ 63) (hx : l.op.toNat ≤ 13) (hd1 : 1 ≤ l.dist.toNat) (hd2 : l.dist.toNat ≤ 65536)
220    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) (hbroke : l.broke = false)
221    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 5 ≤ l.bits.toNat)) :
222    Wp (dodistBase c l) (e.heap A msg m) (fun l' h' =>
223      ∃ i' xv rest, i ≤ i' ∧ i' ≤ i + 2 ∧ readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (xv, rest) ∧
224        l'.againD = l.againD ∧
225        ((l'.broke = false ∧ LS e l' i' (o + l.len.toNat) ∧ Sg e l'.hold.toNat l'.bits.toNat i' = rest ∧
226            h' = e.heap (matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o (l.dist.toNat + xv) l.len.toNat A) msg m) ∨
227         (l'.broke = true ∧ LS e l' i' o ∧ ∃ p, h' = e.heap A p BAD))) := by
228  unfold dodistBase
229  by_cases h1 : l.bits < l.op
230  · simp only [h1, ite_true]
231    have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
232    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
233    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
234    have hl3 := hls.pullL (by omega) hiin
235    have hs3 := Sg_pullL hls (by omega) hiin
236    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
237    by_cases h2 : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits <
238        (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op
239    · simp only [h2, ite_true]
240      have h2' : l.bits.toNat + 8 < l.op.toNat := by
241        have := UInt32.lt_iff_toNat_lt.mp h2
242        simp only [pullL] at this hb3 ⊢
243        omega
244      have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
245      have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by omega
246      refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
247      have hl4 := hl3.pullL hb3' hi2
248      have hs4 := Sg_pullL hl3 hb3' hi2
249      have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
250        (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
251      refine Wp.mono (distCont_wp hc A msg m _ (i + 1 + 1) o hl4 hA ho hAb (by simp only [pullL]; omega)
252        (by simp only [pullL] at hb3 hb4 ⊢; omega) (by simp only [pullL]; omega) (by simp only [pullL]; omega)
253        (by simp only [pullL]; omega) (by simp only [pullL]; omega)) ?_
254      intro l' h' hq
255      obtain ⟨xv, rest, hr, hin, hagD, hres⟩ := hq
256      refine ⟨i + 1 + 1, xv, rest, by omega, by omega, ?_, hagD, ?_⟩
257      · simp only [pullL] at hr hs4 hs3 ⊢
258        rw [hs4, hs3] at hr
259        exact hr
260      · simp only [pullL] at hres ⊢
261        exact Or.imp id (fun h => ⟨h.1, h.2.1, h.2.2.2⟩) hres
262    · simp only [h2, ite_false]
263      have h2n : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op.toNat ≤
264          (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat := by
265        have : ¬ ((pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat <
266            (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).op.toNat) :=
267          fun h => h2 (UInt32.lt_iff_toNat_lt.mpr h)
268        omega
269      refine Wp.mono (distCont_wp hc A msg m _ (i + 1) o hl3 hA ho hAb (by simp only [pullL]; omega)
270        h2n (by simp only [pullL]; omega) (by simp only [pullL]; omega)
271        (by simp only [pullL]; omega) (by simp only [pullL]; omega)) ?_
272      intro l' h' hq
273      obtain ⟨xv, rest, hr, hin, hagD, hres⟩ := hq
274      refine ⟨i + 1, xv, rest, by omega, by omega, ?_, hagD, ?_⟩
275      · simp only [pullL] at hr hs3 ⊢
276        rw [hs3] at hr
277        exact hr
278      · simp only [pullL] at hres ⊢
279        exact Or.imp id (fun h => ⟨h.1, h.2.1, h.2.2.2⟩) hres
280  · simp only [h1, ite_false]
281    have h1' : l.op.toNat ≤ l.bits.toNat := by
282      have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
283      omega
284    refine Wp.mono (distCont_wp hc A msg m l i o hls hA ho hAb hx h1' hd1 hd2 hlen hbroke) ?_
285    intro l' h' hq
286    obtain ⟨xv, rest, hr, hin, hagD, hres⟩ := hq
287    exact ⟨i, xv, rest, by omega, by omega, hr, hagD, Or.imp id (fun h => ⟨h.1, h.2.1, h.2.2.2⟩) hres⟩
288
289end Zlib.Inffast.Proofs