inffast.c.final.lean

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

1import ZlibF.Proof.«inffast.c.loop»
2
3/-!
4# inffast.c: normalization and final writeback
5
6The proof adapts the earlier split into normalization, pointer-derived
7remaining counts, and stream/state stores to the current record heap.
8-/
9
10namespace Zlib.Inffast.Proofs
11open C Zlib.Inffast Zlib.Inffast.Spec
12variable {e : Env} {c : Ctx}
13
14theorem bits_whole (b : UInt32) : (b >>> 3).toNat = b.toNat / 8 := by
15  rw [UInt32.toNat_shiftRight]
16  simp [Nat.shiftRight_eq_div_pow]
17
18theorem bits_whole_shift (b : UInt32) (hb : b.toNat ≤ 30) :
19    ((b >>> 3) <<< 3).toNat = b.toNat / 8 * 8 := by
20  rw [UInt32.toNat_shiftLeft, bits_whole, Nat.shiftLeft_eq]
21  change (b.toNat / 8 * 8) % 4294967296 = b.toNat / 8 * 8
22  exact Nat.mod_eq_of_lt (by omega)
23
24theorem bits_residual (b : UInt32) (hb : b.toNat ≤ 30) :
25    (b - ((b >>> 3) <<< 3)).toNat = b.toNat % 8 := by
26  rw [u32_toNat_sub (by rw [bits_whole_shift b hb]; omega), bits_whole_shift b hb]
27  omega
28
29theorem LS.buffered_le {l : L} {i o : Nat} (hl : LS e l i o) :
30    l.bits.toNat / 8 ≤ i - e.i0 := by
31  have hacc := hl.hacc
32  have hb0 := e.hbits
33  omega
34
35theorem normalized_hold_lt (H : UInt64) (b : UInt32) (hb : b.toNat < 32) :
36    (H &&& (((1 : UInt32) <<< b) - 1).toUInt64).toNat < 2 ^ b.toNat := by
37  have hm : ((((1 : UInt32) <<< b) - 1).toUInt64).toNat = 2 ^ b.toNat - 1 := by
38    rw [UInt32.toNat_toUInt64]
39    exact u32_shl1_sub1 hb
40  rw [u64_and_mask hm]
41  exact Nat.mod_lt _ (Nat.pow_pos (by omega))
42
43/-- The C conditional arithmetic computes the exact nonnegative remaining
44count, in both pointer-order branches. -/
45theorem ptr_avail_run {h : Heap} {r : BRef} {A : Array UInt8} {p q k : Nat}
46    (hg : Space.get h r = some A) (hp : p ≤ A.size) (hq : q ≤ A.size)
47    (hsz : A.size < 2 ^ 63) (hle : p ≤ q + k) (hk : k < 2 ^ 31)
48    (hr : q + k - p < 2 ^ 32) :
49    (do
50      if ← Ptr.lt (.ref r p) (.ref r q) then do
51        let d ← Ptr.diff (.ref r q) (.ref r p)
52        chk64 ((k : Int) + d.toInt)
53      else do
54        let d ← Ptr.diff (.ref r p) (.ref r q)
55        chk64 ((k : Int) - d.toInt)) h =
56    .ok (Int64.ofInt ((q + k - p : Nat) : Int), h) := by
57  rw [bind_ok (Ptr.lt_ok hg hp hq)]
58  by_cases hc : p < q
59  · simp only [hc, decide_true, ite_true]
60    have hd := Ptr.diff_ok hg hq hp (by omega)
61    have hdiff : (q : Int) - (p : Int) = ((q - p : Nat) : Int) := by omega
62    rw [hdiff] at hd
63    rw [bind_ok hd, i64_toInt (q - p) (by omega)]
64    have hv : (k : Int) + (q - p : Nat) = ((q + k - p : Nat) : Int) := by omega
65    rw [hv, chk64_eq (by omega) (by omega)]
66    rfl
67  · simp only [hc, decide_false, Bool.false_eq_true, ite_false]
68    have hd := Ptr.diff_ok hg hp hq (by omega)
69    have hdiff : (p : Int) - (q : Int) = ((p - q : Nat) : Int) := by omega
70    rw [hdiff] at hd
71    rw [bind_ok hd, i64_toInt (p - q) (by omega)]
72    have hv : (k : Int) - (p - q : Nat) = ((q + k - p : Nat) : Int) := by omega
73    rw [hv, chk64_eq (by omega) (by omega)]
74    rfl
75
76/-- The C conditional arithmetic computes the exact nonnegative remaining
77count, in both pointer-order branches. -/
78theorem ptr_avail_cont {α : Type} {h : Heap} {r : BRef} {A : Array UInt8} {p q k : Nat}
79    (hg : Space.get h r = some A) (hp : p ≤ A.size) (hq : q ≤ A.size)
80    (hsz : A.size < 2 ^ 63) (hle : p ≤ q + k) (hk : k < 2 ^ 31)
81    (hr : q + k - p < 2 ^ 32) (K : Int64 → M α) :
82    (do
83      if ← Ptr.lt (.ref r p) (.ref r q) then do
84        let d ← Ptr.diff (.ref r q) (.ref r p)
85        let v ← chk64 ((k : Int) + d.toInt)
86        K v
87      else do
88        let d ← Ptr.diff (.ref r p) (.ref r q)
89        let v ← chk64 ((k : Int) - d.toInt)
90        K v) h =
91    K (Int64.ofInt ((q + k - p : Nat) : Int)) h := by
92  rw [bind_ok (Ptr.lt_ok hg hp hq)]
93  by_cases hc : p < q
94  · simp only [hc, decide_true, ite_true]
95    have hd := Ptr.diff_ok hg hq hp (by omega)
96    have hdiff : (q : Int) - (p : Int) = ((q - p : Nat) : Int) := by omega
97    rw [hdiff] at hd
98    rw [bind_ok hd, i64_toInt (q - p) (by omega)]
99    have hv : (k : Int) + (q - p : Nat) = ((q + k - p : Nat) : Int) := by omega
100    rw [hv, chk64_eq (by omega) (by omega)]
101    rfl
102  · simp only [hc, decide_false, Bool.false_eq_true, ite_false]
103    have hd := Ptr.diff_ok hg hp hq (by omega)
104    have hdiff : (p : Int) - (q : Int) = ((p - q : Nat) : Int) := by omega
105    rw [hdiff] at hd
106    rw [bind_ok hd, i64_toInt (p - q) (by omega)]
107    have hv : (k : Int) - (p - q : Nat) = ((q + k - p : Nat) : Int) := by omega
108    rw [hv, chk64_eq (by omega) (by omega)]
109    rfl
110
111theorem ptr_avail_wp {α : Type} {h : Heap} {r : BRef} {A : Array UInt8} {p q k : Nat}
112    (hg : Space.get h r = some A) (hp : p ≤ A.size) (hq : q ≤ A.size)
113    (hsz : A.size < 2 ^ 63) (hle : p ≤ q + k) (hk : k < 2 ^ 31)
114    (hr : q + k - p < 2 ^ 32) {K : Int64 → M α} {Q : α → Heap → Prop}
115    (hK : Wp (K (Int64.ofInt ((q + k - p : Nat) : Int))) h Q) :
116    Wp (do
117      if ← Ptr.lt (.ref r p) (.ref r q) then do
118        let d ← Ptr.diff (.ref r q) (.ref r p)
119        let v ← chk64 ((k : Int) + d.toInt)
120        K v
121      else do
122        let d ← Ptr.diff (.ref r p) (.ref r q)
123        let v ← chk64 ((k : Int) - d.toInt)
124        K v) h Q := by
125  obtain ⟨v, h', hrK, hpost⟩ := hK
126  exact ⟨v, h', (ptr_avail_cont hg hp hq hsz hle hk hr K).trans hrK, hpost⟩
127
128theorem i64_to_u32_eq (n : Nat) (hn : n < 2 ^ 32) :
129    (Int64.ofInt (n : Int)).toUInt64.toUInt32 = UInt32.ofNat n := by
130  apply UInt32.toNat_inj.mp
131  rw [i64_toU32 n hn, UInt32.toNat_ofNat']
132  exact (Nat.mod_eq_of_lt hn).symm
133
134theorem Env.stream_get_frame (e : Env) (bytes : Tbl (Option (Array UInt8)))
135    (states : Tbl (Option InflateState)) :
136    e.r.get { e.h0 with bytes, istates := states } = some e.sm0 := by
137  have hh := e.hsm
138  cases hr : e.r <;> (rw [hr] at hh; simpa [ZStreamRef.get] using hh)
139
140/-- Exact stream/state stores in the translated epilogue. -/
141theorem fast_stores_run (e : Env) (A : Array UInt8) (msg : BPtr) (mode : UInt32)
142    (input output : BPtr) (ai ao : UInt32) (hold : UInt64) (bits : UInt32) :
143    (do
144      let sm ← ldZStream e.strm
145      stZStream e.strm { sm with next_in := input, next_out := output, avail_in := ai, avail_out := ao }
146      let st ← ldInflateState (some (.tab e.stid))
147      stInflateState (some (.tab e.stid)) { st with hold, bits }) (e.heap A msg mode) =
148    .ok ((), e.r.put
149      { e.h0 with bytes := upd e.h0.bytes e.ob (some A), istates := upd e.h0.istates e.stid (some { e.s0 with mode, hold, bits }) }
150      { e.sm0 with next_in := input, next_out := output, avail_in := ai, avail_out := ao, msg }) := by
151  rw [e.hstrm, bind_ok (ldZStream_ok (e.heap_rget A msg mode)),
152    bind_ok (stZStream_ok (e.heap_rget A msg mode) e.hrw)]
153  let H := e.r.put (e.heap A msg mode)
154    { e.sm0 with next_in := input, next_out := output, avail_in := ai, avail_out := ao, msg }
155  have hg : H.istates e.stid = some { e.s0 with mode } := by
156    dsimp only [H]
157    rw [put_istates, e.heap_istates]
158    exact upd_same _ _ _
159  rw [bind_ok (ldInflateState_tab hg), stInflateState_tab hg]
160  dsimp only [H]
161  unfold Env.heap
162  rw [put_istates_comm, put_istates_comm]
163  simp only [put_istates, upd_upd]
164  rw [put_put _ _ e.sm0 _ _ (e.stream_get_frame _ _)]
165
166/-- The actual normalization and writeback fragment establishes FastPost
167from the proved loop facts. No callee behavior is an assumption. -/
168theorem fast_finish_wp (e : Env) (A : Array UInt8) (msg : BPtr) (mode : UInt32)
169    (l : L) (i o : Nat) (hl : LS e l i o) (hAsz : A.size = e.A0.size)
170    (ho : o ≤ e.o0 + e.sm0.avail_out.toNat)
171    (hf : ∀ j, (j < e.o0 ∨ o ≤ j) → A[j]? = e.A0[j]?)
172    (hclass : (mode = e.s0.mode ∧ msg = e.sm0.msg) ∨ (mode = TYPE ∧ msg = e.sm0.msg) ∨ mode = BAD)
173    (hstop : mode ≠ TYPE → mode ≠ BAD → i + 6 > e.i0 + e.sm0.avail_in.toNat ∨
174      o + 258 > e.o0 + e.sm0.avail_out.toNat) :
175    Wp (do
176      let len := l.bits >>> 3
177      let input ← subn l.in_ len
178      let bits := l.bits - (len <<< 3)
179      let hold := l.hold &&& ((← shl32 1 bits) - 1).toUInt64
180      let ai : Int64 ←
181        if ← Ptr.lt input (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)) then do
182          let d ← Ptr.diff (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)) input
183          chk64 (5 + d.toInt)
184        else do
185          let d ← Ptr.diff input (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5))
186          chk64 (5 - d.toInt)
187      let ao : Int64 ←
188        if ← Ptr.lt l.out (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)) then do
189          let d ← Ptr.diff (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)) l.out
190          chk64 (257 + d.toInt)
191        else do
192          let d ← Ptr.diff l.out (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257))
193          chk64 (257 - d.toInt)
194      let sm ← ldZStream e.strm
195      stZStream e.strm { sm with next_in := input, next_out := l.out, avail_in := ai.toUInt64.toUInt32, avail_out := ao.toUInt64.toUInt32 }
196      let st ← ldInflateState (some (.tab e.stid))
197      stInflateState (some (.tab e.stid)) { st with hold, bits })
198      (e.heap A msg mode) (fun _ after => FastPost e after) := by
199  let buf := l.bits.toNat / 8
200  let used := i - e.i0 - buf
201  let produced := o - e.o0
202  let bits := l.bits - ((l.bits >>> 3) <<< 3)
203  let hold := l.hold &&& (((1 : UInt32) <<< bits) - 1).toUInt64
204  have hbuf : buf ≤ i - e.i0 := hl.buffered_le
205  have hsmall : buf ≤ 3 := by dsimp only [buf]; have := hl.hb; omega
206  have hused : used + buf = i - e.i0 := by dsimp only [used]; omega
207  have hui : used + buf ≤ e.sm0.avail_in.toNat := by have := hl.hi0; have := hl.hi1; omega
208  have hup : produced ≤ e.sm0.avail_out.toNat := by dsimp only [produced]; have := hl.ho0; omega
209  have hio : i - (l.bits >>> 3).toNat = e.i0 + used := by
210    rw [bits_whole]
211    change i - buf = e.i0 + used
212    have := hl.hi0
213    omega
214  have hout : o = e.o0 + produced := by dsimp only [produced]; have := hl.ho0; omega
215  have hbits : bits.toNat < 8 := by dsimp only [bits]; rw [bits_residual _ hl.hb]; omega
216  have hinbuf : OkOn (e.heap A msg mode) (subn l.in_ (l.bits >>> 3))
217      (.ref (BRef.blk e.ib) (e.i0 + used)) := by
218    rw [hl.hin]
219    have hr := subn_ok (h := e.heap A msg mode) (r := BRef.blk e.ib) (a := e.IN) (e.heap_bytes_in A msg mode)
220      (n := l.bits >>> 3) (off := i) (by rw [bits_whole]; have := hl.hi0; omega)
221      (by have := hl.hi1; have := e.hINsz; omega)
222    simpa only [hio] using hr
223  refine Wp.bindO hinbuf ?_
224  refine Wp.bindO (shl32_ok (x := 1) (n := bits) (by omega)) ?_
225  have hu32 : e.sm0.avail_in.toNat - used < 2 ^ 32 := by have := UInt32.toNat_lt e.sm0.avail_in; omega
226  have ho32 : e.sm0.avail_out.toNat - produced < 2 ^ 32 := by have := UInt32.toNat_lt e.sm0.avail_out; omega
227  have hei : e.i0 + e.sm0.avail_in.toNat - 5 + 5 - (e.i0 + used) = e.sm0.avail_in.toNat - used := by
228    have := e.hai; omega
229  refine ptr_avail_wp (h := e.heap A msg mode) (r := BRef.blk e.ib) (A := e.IN)
230    (p := e.i0 + used) (q := e.i0 + e.sm0.avail_in.toNat - 5) (k := 5)
231    (e.heap_bytes_in A msg mode) (by have := e.hINsz; omega) (by have := e.hINsz; omega)
232    e.hINbig (by have := e.hai; omega) (by decide) (by rw [hei]; exact hu32) ?_
233  rw [hei]
234  rw [hl.hout]
235  have heo : e.o0 + e.sm0.avail_out.toNat - 257 + 257 - o = e.sm0.avail_out.toNat - produced := by
236    have := e.hao; omega
237  refine ptr_avail_wp (h := e.heap A msg mode) (r := BRef.blk e.ob) (A := A)
238    (p := o) (q := e.o0 + e.sm0.avail_out.toNat - 257) (k := 257)
239    (e.heap_bytes_ob A msg mode) (by rw [hAsz]; have := e.hAsz; omega) (by rw [hAsz]; have := e.hAsz; omega)
240    (by rw [hAsz]; exact e.hAbig) (by have := e.hao; omega) (by decide) (by rw [heo]; exact ho32) ?_
241  rw [heo]
242  rw [i64_to_u32_eq _ hu32, i64_to_u32_eq _ ho32]
243  refine Wp.of_eq (fast_stores_run e A msg mode (.ref (BRef.blk e.ib) (e.i0 + used)) (.ref (BRef.blk e.ob) o)
244    (UInt32.ofNat (e.sm0.avail_in.toNat - used)) (UInt32.ofNat (e.sm0.avail_out.toNat - produced)) hold bits) ?_
245  refine ⟨used, produced, buf, A, msg, mode, bits, hold, hui, hsmall, hup, hAsz, hbits,
246    normalized_hold_lt l.hold bits (by omega), ?_, ?_, hclass, ?_⟩
247  · rw [← hout]
248  · intro j hj
249    exact hf j (by rw [← hout] at hj; exact hj)
250  · intro hnt hnb
251    rcases hstop hnt hnb with hi | ho
252    · exact Or.inl (by have := hl.hi0; omega)
253    · exact Or.inr (by omega)
254
255/-- The complete actual fast decoder satisfies the unchanged reviewed
256safety, termination, frame, normalization and writeback goal. -/
257theorem inflate_fast_safe : Goal.fast_safe := by
258  intro e
259  have hw : Wp (inflate_fast e.strm e.start) e.h0 (fun _ after => FastPost e after) := by
260    let c0 : Ctx := {
261      strm := e.strm, state := some (.tab e.stid),
262      last := .ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5),
263      beg := .ref (BRef.blk e.ob) e.bg,
264      end_ := .ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257),
265      wsize := e.s0.wsize, whave := e.s0.whave, wnext := e.s0.wnext, window := e.s0.window,
266      lcode := e.s0.lencode, dcode := e.s0.distcode,
267      lmask := ((1 : UInt32) <<< e.s0.lenbits) - 1, dmask := ((1 : UInt32) <<< e.s0.distbits) - 1 }
268    let l0 : L := {
269      in_ := .ref (BRef.blk e.ib) e.i0, out := .ref (BRef.blk e.ob) e.o0,
270      hold := e.s0.hold, bits := e.s0.bits, here := default, op := 0, len := 0, dist := 0,
271      from_ := default, broke := false, againL := false, againD := false }
272    have hc0 : CtxOK e c0 := ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
273    have hl0 : LS e l0 e.i0 e.o0 := by
274      dsimp only [l0]
275      refine ⟨rfl, rfl, by omega, ?_, by omega, ?_, e.hhold, ?_⟩
276      · have := e.hai; omega
277      · change e.s0.bits.toNat ≤ 30
278        have := e.hbits; omega
279      · change e.s0.bits.toNat + 8 * e.i0 ≤ e.s0.bits.toNat + 8 * e.i0
280        exact Nat.le_refl _
281    have hlast : OkOn e.h0 (Ptr.add e.sm0.next_in (e.sm0.avail_in - 5).toNat)
282        (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)) := by
283      rw [e.hnin, u32_toNat_sub (by change 5 ≤ e.sm0.avail_in.toNat; have := e.hai; omega)]
284      have hr := Ptr.add_nat_ok (h := e.h0) (r := BRef.blk e.ib) (a := e.IN)
285        (off := e.i0) (n := e.sm0.avail_in.toNat - 5) e.hIN (by have := e.hINsz; omega)
286      have hoff : e.i0 + (e.sm0.avail_in.toNat - 5) = e.i0 + e.sm0.avail_in.toNat - 5 := by have := e.hai; omega
287      simpa [hoff] using hr
288    have hbeg : OkOn e.h0 (subn e.sm0.next_out (e.start - e.sm0.avail_out))
289        (.ref (BRef.blk e.ob) e.bg) := by
290      rw [e.hnout]
291      have hn : (e.start - e.sm0.avail_out).toNat = e.start.toNat - e.sm0.avail_out.toNat :=
292        u32_toNat_sub e.hstart
293      have hr := subn_ok (h := e.h0) (r := BRef.blk e.ob) (a := e.A0)
294        (off := e.o0) (n := e.start - e.sm0.avail_out) e.hA0 (by rw [hn]; exact e.hbeg)
295        (by have := e.hAsz; omega)
296      simpa only [hn, Env.bg] using hr
297    have hend : OkOn e.h0 (Ptr.add e.sm0.next_out (e.sm0.avail_out - 257).toNat)
298        (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)) := by
299      rw [e.hnout, u32_toNat_sub (by change 257 ≤ e.sm0.avail_out.toNat; have := e.hao; omega)]
300      have hr := Ptr.add_nat_ok (h := e.h0) (r := BRef.blk e.ob) (a := e.A0)
301        (off := e.o0) (n := e.sm0.avail_out.toNat - 257) e.hA0 (by have := e.hAsz; omega)
302      have hoff : e.o0 + (e.sm0.avail_out.toNat - 257) = e.o0 + e.sm0.avail_out.toNat - 257 := by have := e.hao; omega
303      simpa [hoff] using hr
304    unfold inflate_fast
305    refine Wp.bindO (x := e.sm0) (by rw [e.hstrm]; exact ldZStream_ok e.hsm) ?_
306    refine Wp.bindO (x := some (InflateStateRef.tab e.stid)) (by rw [e.hstate]; exact castInflateState_ok) ?_
307    refine Wp.bindO hlast ?_
308    refine Wp.bindO hbeg ?_
309    refine Wp.bindO hend ?_
310    refine Wp.bindO (ldInflateState_tab e.hs0) ?_
311    refine Wp.bindO (shl32_ok (x := 1) (n := e.s0.lenbits) (by have := e.hlt.1; omega)) ?_
312    refine Wp.bindO (shl32_ok (x := 1) (n := e.s0.distbits) (by have := e.hdt.1; omega)) ?_
313    rw [e.hnin, e.hnout]
314    obtain ⟨l, h, hr, hpost⟩ := fast_loop_wp hc0 l0 e.i0 e.o0 e.A0 hl0 rfl rfl
315      (by have := e.hai; omega) (by have := e.hao; omega) (by intro _ _; rfl)
316    rw [e.heap_initial] at hr
317    refine Wp.bindE hr ?_
318    obtain ⟨i, o, A, msg, mode, hl, ho, hA, hh, hf, hclass, hstop⟩ := hpost
319    rw [hh]
320    exact fast_finish_wp e A msg mode l i o hl hA ho hf hclass hstop
321  obtain ⟨⟨⟩, after, hr, hp⟩ := hw
322  exact ⟨after, hr, hp⟩
323
324end Zlib.Inffast.Proofs