inffast.c.len.lean

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

1import ZlibF.Proof.«inffast.c.lp»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
5
6variable {e : Env} {c : Ctx}
7
8/-- `dodist:` reached from the length block: look up the distance code and run the distance block. -/
9def dolenDist (c : Ctx) (l : L) : M L := do
10  let __do_lift ← Ptr.add c.dcode ↑(l.hold &&& c.dmask.toUInt64).toNat
11  let l : L := { l with here := __do_lift }
12  cdoWhile (dodist c) (fun l => pure (l.againD, l)) l
13
14theorem dolenDist_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o : Nat)
15    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
16    (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)
17    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
18    (hb15 : 15 ≤ l.bits.toNat)
19    (hpull : i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨ (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) :
20    Wp (dolenDist c l) (e.heap A msg m) (fun l' h' =>
21      ∃ E cb, cb ≤ 15 ∧ DistLook e l.hold.toNat (l.hold.toNat % 2 ^ e.s0.distbits.toNat) E cb ∧
22        DistEnd e A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop cb) i o l.len.toNat E l' h') := by
23  unfold dolenDist
24  have hdc : c.dcode = .ref e.rd e.od := by rw [hc.dcode]; exact e.hdc
25  have hR : e.s0.distbits.toNat < 32 := by have := hts.1; omega
26  have hmask : c.dmask.toUInt64.toNat = 2 ^ e.s0.distbits.toNat - 1 := by
27    rw [hc.dmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
28  have hidx := u64_and_mask (x := l.hold) hmask
29  have hmod : l.hold.toNat % 2 ^ e.s0.distbits.toNat < 2 ^ e.s0.distbits.toNat :=
30    Nat.mod_lt _ (Nat.pow_pos (by omega))
31  refine Wp.bindO (x := Ptr.ref e.rd (e.od + l.hold.toNat % 2 ^ e.s0.distbits.toNat)) ?_ ?_
32  · rw [hdc, hidx]
33    exact Ptr.add_nat_ok (e.heap_cget_DCA A msg m) (by have := hts.2.1; omega)
34  · exact Wp.mono (dodistLoop_wp hc A msg m { l with here := Ptr.ref e.rd (e.od + l.hold.toNat % 2 ^ e.s0.distbits.toNat) }
35      i o _ hts hmod (LS.congr hls rfl rfl rfl rfl) hA ho hAb hbroke hlen rfl hb15 hpull) (fun _ _ h => h)
36
37
38/-- The refill before the distance lookup (`if (bits < 15) { two bytes }`) and the distance block. -/
39def dolenRefill (c : Ctx) (l : L) : M L :=
40  if l.bits < 15 then do
41    let __x ← pull l
42    let __x ← pull __x
43    dolenDist c __x
44  else dolenDist c l
45
46/-- What follows the refill: the stream, and the lookup and the end of the distance block. -/
47def RefillPost (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) (S : List Bool) (i o len : Nat)
48    (l' : L) (h' : Heap) : Prop :=
49  ∃ i3 H3 b3 E cb, i ≤ i3 ∧ i3 ≤ i + 2 ∧ Sg e H3 b3 i3 = S ∧ H3 < 2 ^ b3 ∧ 15 ≤ b3 ∧ b3 ≤ 30 ∧ cb ≤ 15 ∧
50    DistLook e H3 (H3 % 2 ^ e.s0.distbits.toNat) E cb ∧ DistEnd e A msg m (S.drop cb) i3 o len E l' h'
51
52theorem dolenRefill_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
53    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
54    (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)
55    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
56    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3) (hT3 : i = s + 3 → 4 ≤ l.bits.toNat) :
57    Wp (dolenRefill c l) (e.heap A msg m) (fun l' h' =>
58      RefillPost e A msg m (Sg e l.hold.toNat l.bits.toNat i) i o l.len.toNat l' h') := by
59  unfold dolenRefill
60  by_cases h1 : l.bits < 15
61  · simp only [h1, ite_true]
62    have h1' : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
63    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
64    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
65    have hl3 := hls.pullL (by omega) hiin
66    have hs3 := Sg_pullL hls (by omega) hiin
67    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
68    have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
69    have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
70      simp only [pullL] at hb3 ⊢; omega
71    refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
72    have hl4 := hl3.pullL hb3' hi2
73    have hs4 := Sg_pullL hl3 hb3' hi2
74    have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
75      (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
76    simp only [pullL] at hb3 hb4
77    refine Wp.mono (dolenDist_wp hc A msg m _ (i + 1 + 1) o hts hl4 hA ho hAb hbroke hlen (by simp only [pullL]; omega) ?_) ?_
78    · by_cases hc3 : i = s + 3
79      · right; have := hT3 hc3; simp only [pullL]; omega
80      · left; omega
81    · intro l' h' hq
82      obtain ⟨E, cb, hcb, hlk, hend⟩ := hq
83      refine ⟨i + 1 + 1, (pullL (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0) (.ref (BRef.blk e.ib) (i + 1 + 1))).hold.toNat,
84        (pullL (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0) (.ref (BRef.blk e.ib) (i + 1 + 1))).bits.toNat,
85        E, cb, by omega, by omega, ?_, ?_, ?_, ?_, hcb, hlk, ?_⟩
86      · exact hs4.trans hs3
87      · exact hl4.hH
88      · simp only [pullL]; omega
89      · exact hl4.hb
90      · rw [hs4, hs3] at hend; exact hend
91  · simp only [h1, ite_false]
92    have h1' : 15 ≤ l.bits.toNat := by
93      have : ¬ (l.bits.toNat < 15) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
94      omega
95    refine Wp.mono (dolenDist_wp hc A msg m l i o hts hls hA ho hAb hbroke hlen h1' (Or.inl (by omega))) ?_
96    intro l' h' hq
97    obtain ⟨E, cb, hcb, hlk, hend⟩ := hq
98    exact ⟨i, l.hold.toNat, l.bits.toNat, E, cb, by omega, by omega, rfl, hls.hH, h1', hls.hb, hcb, hlk, hend⟩
99
100
101/-- The extra bits of a length are read and added to the base, then the refill and the distance block follow. -/
102def dolenExt (c : Ctx) (l : L) : M L := do
103  let m ← shl32 1 l.op
104  let l : L := { l with len := l.len + (l.hold.toUInt32 &&& m - 1) }
105  let __do_lift ← shr64 l.hold l.op.toUInt64
106  let l : L := { l with hold := __do_lift }
107  let l : L := { l with bits := l.bits - l.op }
108  dolenRefill c l
109
110theorem dolenExt_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
111    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
112    (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)
113    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5) (hxb : l.op.toNat ≤ l.bits.toNat)
114    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
115    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3)
116    (hT3 : i = s + 3 → 4 + l.op.toNat ≤ l.bits.toNat) :
117    Wp (dolenExt c l) (e.heap A msg m) (fun l' h' =>
118      ∃ lx S1, readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (lx, S1) ∧
119        RefillPost e A msg m S1 i o (l.len.toNat + lx) l' h') := by
120  unfold dolenExt
121  have hxs : l.op.toNat < 32 := by omega
122  refine Wp.bindO (shl32_ok hxs) ?_
123  dsimp only
124  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
125  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
126  have hpow : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
127  have hlen' : (l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.len.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
128    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
129  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
130  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
131  have hbn := dropL_bits l l.op hxb
132  have hrb := readBits_bitsOfNat l.op.toNat l.bits.toNat l.hold.toNat (inBits e i) hxb
133  have hsg := Sg_dropL (e := e) l l.op i hxb (by omega)
134  refine Wp.mono (dolenRefill_wp hc A msg m
135    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits - l.op, here := l.here, op := l.op,
136      len := l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1), dist := l.dist, from_ := l.from_, broke := l.broke,
137      againL := l.againL, againD := l.againD } i o s hts (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
138    (by rw [hlen']; omega) hs6 hT (by intro h3; have := hT3 h3; show 4 ≤ (l.bits - l.op).toNat; simp only [dropL] at hbn; omega)) ?_
139  intro l' h' hq
140  refine ⟨l.hold.toNat % 2 ^ l.op.toNat, Sg e (dropL l l.op).hold.toNat (dropL l l.op).bits.toNat i, ?_, ?_⟩
141  · unfold Sg; rw [hrb, dropL_hold l l.op (by omega), dropL_bits l l.op hxb]
142  · simp only [hlen'] at hq
143    exact hq
144
145
146/-- After `op &= 15`: the extra bits of the length (read after at most one more byte), then `dolenExt`. -/
147def dolenLen (c : Ctx) (l : L) : M L :=
148  if l.op != 0 then
149    if l.bits < l.op then do
150      let __x ← pull l
151      dolenExt c __x
152    else dolenExt c l
153  else dolenRefill c l
154
155theorem dolenLen_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
156    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
157    (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)
158    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5)
159    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
160    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 2) (hb2 : i = s + 2 → 1 ≤ l.bits.toNat) :
161    Wp (dolenLen c l) (e.heap A msg m) (fun l' h' =>
162      ∃ i2 lx S1, i ≤ i2 ∧ i2 ≤ i + 1 ∧ readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (lx, S1) ∧
163        RefillPost e A msg m S1 i2 o (l.len.toNat + lx) l' h') := by
164  unfold dolenLen
165  by_cases h0 : l.op != 0
166  · simp only [h0, ite_true]
167    have h0' : l.op.toNat ≠ 0 := by
168      intro h; apply (by simpa using h0 : l.op ≠ 0); exact UInt32.toNat_inj.mp (by simpa using h)
169    by_cases h1 : l.bits < l.op
170    · simp only [h1, ite_true]
171      have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
172      have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
173      refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
174      have hl3 := hls.pullL (by omega) hiin
175      have hs3 := Sg_pullL hls (by omega) hiin
176      have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
177      refine Wp.mono (dolenExt_wp hc A msg m _ (i + 1) o s hts hl3 hA ho hAb hbroke (by simp only [pullL]; omega)
178        (by simp only [pullL] at hb3 ⊢; omega) (by simp only [pullL]; omega) hs6 (by omega)
179        (by intro h3; simp only [pullL] at hb3 ⊢; have := hb2 (by omega); omega)) ?_
180      intro l' h' hq
181      obtain ⟨lx, S1, hr, hrp⟩ := hq
182      refine ⟨i + 1, lx, S1, by omega, by omega, ?_, ?_⟩
183      · simp only [pullL] at hr hs3 ⊢; rw [hs3] at hr; exact hr
184      · simp only [pullL] at hrp ⊢; exact hrp
185    · simp only [h1, ite_false]
186      have h1' : l.op.toNat ≤ l.bits.toNat := by
187        have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
188        omega
189      refine Wp.mono (dolenExt_wp hc A msg m l i o s hts hls hA ho hAb hbroke hx h1' hlen hs6 (by omega)
190        (by intro h3; omega)) ?_
191      intro l' h' hq
192      obtain ⟨lx, S1, hr, hrp⟩ := hq
193      exact ⟨i, lx, S1, by omega, by omega, hr, hrp⟩
194  · simp only [h0, ite_false]
195    have h0' : l.op.toNat = 0 := by
196      have : l.op = 0 := by simpa using h0
197      rw [this]; rfl
198    refine Wp.mono (dolenRefill_wp hc A msg m l i o s hts hls hA ho hAb hbroke ⟨hlen.1, by
199      have : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
200      omega⟩ hs6 (by omega) (by intro h3; omega)) ?_
201    intro l' h' hq
202    refine ⟨i, 0, Sg e l.hold.toNat l.bits.toNat i, by omega, by omega, ?_, ?_⟩
203    · rw [h0']; rfl
204    · simpa using hq
205
206end Zlib.Inffast.Proofs