inffast.c.call-origin.lean

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

1import ZlibF.Spec.InflateFastCallOrigin
2import ZlibF.Proof.«inffast.c.body-origin»
3import ZlibF.Proof.«inffast.c.origin»
4import ZlibF.Proof.«inffast.c.final»
5
6namespace Zlib.Inffast.Proofs
7open C Zlib.Inffast Zlib.Inffast.Spec Zlib.Inffast.Spec.CallOrigin
8
9private theorem loop_origin_wp (hc : CtxOK e c) (l : L) (i o : Nat) (A : Array UInt8) (msg : BPtr) (mode : UInt32) (used : Nat)
10    (hl : LS e l i o) (hA : A.size = e.A0.size) (hb : l.broke = false)
11    (hi : i + 6 ≤ e.i0 + e.sm0.avail_in.toNat)
12    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
13    (origin : Origin.Inv e l.hold.toNat l.bits.toNat i used) :
14    Wp (cdoWhile (inflate_fast_body c)
15      (fun l => do
16        if l.broke then pure (false, l)
17        else if ← Ptr.lt l.in_ c.last then pure (← Ptr.lt l.out c.end_, l)
18        else pure (false, l)) l) (e.heap A msg mode)
19      (fun l' h' => ∃ i' o' A' msg' mode' used',
20        LS e l' i' o' ∧ o' ≤ e.o0 + e.sm0.avail_out.toNat ∧ A'.size = e.A0.size ∧
21        h' = e.heap A' msg' mode' ∧
22        Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used') := by
23  let Inv : L → Heap → Prop := fun l h => ∃ i o A msg mode cursor,
24    LS e l i o ∧ A.size = e.A0.size ∧ h = e.heap A msg mode ∧ l.broke = false ∧
25    i + 6 ≤ e.i0 + e.sm0.avail_in.toNat ∧ o + 258 ≤ e.o0 + e.sm0.avail_out.toNat ∧
26    Origin.Inv e l.hold.toNat l.bits.toNat i cursor ∧ used ≤ cursor
27  let μ : L → Nat := fun l => match l.out with
28    | .null => 0
29    | .ref _ k => e.o0 + e.sm0.avail_out.toNat - k
30  have hμ : ∀ l i o, LS e l i o → μ l = e.o0 + e.sm0.avail_out.toNat - o := by
31    intro l i o hl
32    simp only [μ, hl.hout]
33  refine Wp.cdoWhile Inv μ _ ?_
34    ⟨i, o, A, msg, mode, used, hl, hA, rfl, hb, hi, ho, origin, Nat.le_refl _⟩ ?_
35  · intro l h hI
36    obtain ⟨i, o, A, msg, mode, cursor, hl, hA, rfl, hb, hi, ho, origin, hused⟩ := hI
37    have hp : StepPre e c A l i o := ⟨hc, hl, hA, hi, ho, hb⟩
38    obtain ⟨l1, h1, hr, hpost, j, k, cursor', resultLocals, resultOrigin, hcursor⟩ :=
39      actual_body_preserves_origin e c A msg mode l i o cursor hp origin
40    obtain ⟨i', o', A', msg', mode', hl', hii, hi6, hoo, ho258, hsz, hh,
41      _, _, hcont, _⟩ := hpost
42    have sameInput : j = i' := by
43      have eq := Ptr.ref.inj (resultLocals.hin.symm.trans hl'.hin)
44      omega
45    have sameOutput : k = o' := by
46      have eq := Ptr.ref.inj (resultLocals.hout.symm.trans hl'.hout)
47      omega
48    subst j k
49    have hAsz : A'.size = e.A0.size := hsz.trans hA
50    have hoend : o' ≤ e.o0 + e.sm0.avail_out.toNat := by omega
51    have hused' : used ≤ cursor' := Nat.le_trans hused hcursor
52    refine ⟨l1, h1, hr, ?_⟩
53    cases hstop : l1.broke with
54    | true =>
55      refine Or.inl ⟨l1, h1, ?_, i', o', A', msg', mode', cursor', hl',
56        hoend, hAsz, hh, resultOrigin, hused'⟩
57      simp [hstop]
58    | false =>
59      obtain ⟨progress, _, _⟩ := hcont hstop
60      have hcnd := fast_cond_live hc A' msg' mode' l1 i' o' hl' hAsz hoend hstop
61      by_cases hroom : i' + 6 ≤ e.i0 + e.sm0.avail_in.toNat ∧
62          o' + 258 ≤ e.o0 + e.sm0.avail_out.toNat
63      · refine Or.inr ⟨l1, h1, ?_, ?_, ?_⟩
64        · rw [hh]; simpa [hstop, hroom.1, hroom.2] using hcnd
65        · exact ⟨i', o', A', msg', mode', cursor', hl', hAsz, hh, hstop,
66            hroom.1, hroom.2, resultOrigin, hused'⟩
67        · rw [hμ _ _ _ hl', hμ _ _ _ hl]
68          omega
69      · refine Or.inl ⟨l1, h1, ?_, i', o', A', msg', mode', cursor', hl',
70          hoend, hAsz, hh, resultOrigin, hused'⟩
71        have hcfalse : (decide (i' + 6 ≤ e.i0 + e.sm0.avail_in.toNat) &&
72            decide (o' + 258 ≤ e.o0 + e.sm0.avail_out.toNat)) = false := by
73          simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not]
74          omega
75        rw [hh]
76        simpa [hstop, hcfalse] using hcnd
77  · rw [hμ _ _ _ hl]
78    apply lt_fuel_of
79    have := UInt32.toNat_lt e.sm0.avail_out
80    have := hl.ho0
81    omega
82
83private theorem finish_origin_wp (e : Env) (A : Array UInt8) (msg : BPtr) (mode : UInt32)
84    (l : L) (i o : Nat) (hl : LS e l i o) (hAsz : A.size = e.A0.size)
85    (ho : o ≤ e.o0 + e.sm0.avail_out.toNat)
86    (usedBits : Nat) (origin : Origin.Inv e l.hold.toNat l.bits.toNat i usedBits) :
87    Wp (do
88      let len := l.bits >>> 3
89      let input ← subn l.in_ len
90      let bits := l.bits - (len <<< 3)
91      let hold := l.hold &&& ((← shl32 1 bits) - 1).toUInt64
92      let ai : Int64 ←
93        if ← Ptr.lt input (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)) then do
94          let d ← Ptr.diff (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)) input
95          chk64 (5 + d.toInt)
96        else do
97          let d ← Ptr.diff input (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5))
98          chk64 (5 - d.toInt)
99      let ao : Int64 ←
100        if ← Ptr.lt l.out (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)) then do
101          let d ← Ptr.diff (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)) l.out
102          chk64 (257 + d.toInt)
103        else do
104          let d ← Ptr.diff l.out (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257))
105          chk64 (257 - d.toInt)
106      let sm ← ldZStream e.strm
107      stZStream e.strm { sm with next_in := input, next_out := l.out, avail_in := ai.toUInt64.toUInt32, avail_out := ao.toUInt64.toUInt32 }
108      let st ← ldInflateState (some (.tab e.stid))
109      stInflateState (some (.tab e.stid)) { st with hold, bits })
110      (e.heap A msg mode) (fun _ after => HasOrigin e after) := by
111  let buf := l.bits.toNat / 8
112  let used := i - e.i0 - buf
113  let produced := o - e.o0
114  let bits := l.bits - ((l.bits >>> 3) <<< 3)
115  let hold := l.hold &&& (((1 : UInt32) <<< bits) - 1).toUInt64
116  have hbuf : buf ≤ i - e.i0 := hl.buffered_le
117  have hsmall : buf ≤ 3 := by dsimp only [buf]; have := hl.hb; omega
118  have hused : used + buf = i - e.i0 := by dsimp only [used]; omega
119  have hui : used + buf ≤ e.sm0.avail_in.toNat := by have := hl.hi0; have := hl.hi1; omega
120  have hup : produced ≤ e.sm0.avail_out.toNat := by dsimp only [produced]; have := hl.ho0; omega
121  have hio : i - (l.bits >>> 3).toNat = e.i0 + used := by
122    rw [bits_whole]
123    change i - buf = e.i0 + used
124    have := hl.hi0
125    omega
126  have hout : o = e.o0 + produced := by dsimp only [produced]; have := hl.ho0; omega
127  have hbits : bits.toNat < 8 := by dsimp only [bits]; rw [bits_residual _ hl.hb]; omega
128  have hinbuf : OkOn (e.heap A msg mode) (subn l.in_ (l.bits >>> 3))
129      (.ref (BRef.blk e.ib) (e.i0 + used)) := by
130    rw [hl.hin]
131    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)
132      (n := l.bits >>> 3) (off := i) (by rw [bits_whole]; have := hl.hi0; omega)
133      (by have := hl.hi1; have := e.hINsz; omega)
134    simpa only [hio] using hr
135  refine Wp.bindO hinbuf ?_
136  refine Wp.bindO (shl32_ok (x := 1) (n := bits) (by omega)) ?_
137  have hu32 : e.sm0.avail_in.toNat - used < 2 ^ 32 := by have := UInt32.toNat_lt e.sm0.avail_in; omega
138  have ho32 : e.sm0.avail_out.toNat - produced < 2 ^ 32 := by have := UInt32.toNat_lt e.sm0.avail_out; omega
139  have hei : e.i0 + e.sm0.avail_in.toNat - 5 + 5 - (e.i0 + used) = e.sm0.avail_in.toNat - used := by
140    have := e.hai; omega
141  refine ptr_avail_wp (h := e.heap A msg mode) (r := BRef.blk e.ib) (A := e.IN)
142    (p := e.i0 + used) (q := e.i0 + e.sm0.avail_in.toNat - 5) (k := 5)
143    (e.heap_bytes_in A msg mode) (by have := e.hINsz; omega) (by have := e.hINsz; omega)
144    e.hINbig (by have := e.hai; omega) (by decide) (by rw [hei]; exact hu32) ?_
145  rw [hei]
146  rw [hl.hout]
147  have heo : e.o0 + e.sm0.avail_out.toNat - 257 + 257 - o = e.sm0.avail_out.toNat - produced := by
148    have := e.hao; omega
149  refine ptr_avail_wp (h := e.heap A msg mode) (r := BRef.blk e.ob) (A := A)
150    (p := o) (q := e.o0 + e.sm0.avail_out.toNat - 257) (k := 257)
151    (e.heap_bytes_ob A msg mode) (by rw [hAsz]; have := e.hAsz; omega) (by rw [hAsz]; have := e.hAsz; omega)
152    (by rw [hAsz]; exact e.hAbig) (by have := e.hao; omega) (by decide) (by rw [heo]; exact ho32) ?_
153  rw [heo]
154  rw [i64_to_u32_eq _ hu32, i64_to_u32_eq _ ho32]
155  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)
156    (UInt32.ofNat (e.sm0.avail_in.toNat - used)) (UInt32.ofNat (e.sm0.avail_out.toNat - produced)) hold bits) ?_
157  have rollback := actual_rollback_preserves_origin e A msg mode l i o usedBits hl origin
158  have newOrigin : Origin.Inv e hold.toNat bits.toNat (e.i0 + used) usedBits := by
159    have sameIndex : i - l.bits.toNat / 8 = e.i0 + used := by simpa only [bits_whole] using hio
160    simpa only [sameIndex] using rollback.2.2.1
161  let stream : ZStream := { e.sm0 with
162    next_in := .ref (.blk e.ib) (e.i0 + used)
163    next_out := .ref (.blk e.ob) o
164    avail_in := UInt32.ofNat (e.sm0.avail_in.toNat - used)
165    avail_out := UInt32.ofNat (e.sm0.avail_out.toNat - produced)
166    msg := msg }
167  refine ⟨{ e.s0 with mode, hold, bits }, stream,
168    e.i0 + used, usedBits, ?_, ?_, rfl, ?_, newOrigin⟩
169  · rw [put_istates]
170    exact upd_same _ _ _
171  · exact put_get e.r _ e.sm0 _ (e.stream_get_frame _ _)
172  · change (e.i0 + used) + (UInt32.ofNat (e.sm0.avail_in.toNat - used)).toNat = _
173    rw [UInt32.toNat_ofNat', Nat.mod_eq_of_lt hu32]
174    omega
175
176theorem actual_fast_preserves_origin : CallOrigin.Goal.actual_fast_preserves_origin := by
177  intro e
178  have hw : Wp (inflate_fast e.strm e.start) e.h0 (fun _ after => HasOrigin e after) := by
179    let c0 : Ctx := {
180      strm := e.strm, state := some (.tab e.stid),
181      last := .ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5),
182      beg := .ref (BRef.blk e.ob) e.bg,
183      end_ := .ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257),
184      wsize := e.s0.wsize, whave := e.s0.whave, wnext := e.s0.wnext, window := e.s0.window,
185      lcode := e.s0.lencode, dcode := e.s0.distcode,
186      lmask := ((1 : UInt32) <<< e.s0.lenbits) - 1, dmask := ((1 : UInt32) <<< e.s0.distbits) - 1 }
187    let l0 : L := {
188      in_ := .ref (BRef.blk e.ib) e.i0, out := .ref (BRef.blk e.ob) e.o0,
189      hold := e.s0.hold, bits := e.s0.bits, here := default, op := 0, len := 0, dist := 0,
190      from_ := default, broke := false, againL := false, againD := false }
191    have hc0 : CtxOK e c0 := ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
192    have hl0 : LS e l0 e.i0 e.o0 := by
193      dsimp only [l0]
194      refine ⟨rfl, rfl, by omega, ?_, by omega, ?_, e.hhold, ?_⟩
195      · have := e.hai; omega
196      · change e.s0.bits.toNat ≤ 30
197        have := e.hbits; omega
198      · change e.s0.bits.toNat + 8 * e.i0 ≤ e.s0.bits.toNat + 8 * e.i0
199        exact Nat.le_refl _
200    have hlast : OkOn e.h0 (Ptr.add e.sm0.next_in (e.sm0.avail_in - 5).toNat)
201        (.ref (BRef.blk e.ib) (e.i0 + e.sm0.avail_in.toNat - 5)) := by
202      rw [e.hnin, u32_toNat_sub (by change 5 ≤ e.sm0.avail_in.toNat; have := e.hai; omega)]
203      have hr := Ptr.add_nat_ok (h := e.h0) (r := BRef.blk e.ib) (a := e.IN)
204        (off := e.i0) (n := e.sm0.avail_in.toNat - 5) e.hIN (by have := e.hINsz; omega)
205      have hoff : e.i0 + (e.sm0.avail_in.toNat - 5) = e.i0 + e.sm0.avail_in.toNat - 5 := by have := e.hai; omega
206      simpa [hoff] using hr
207    have hbeg : OkOn e.h0 (subn e.sm0.next_out (e.start - e.sm0.avail_out))
208        (.ref (BRef.blk e.ob) e.bg) := by
209      rw [e.hnout]
210      have hn : (e.start - e.sm0.avail_out).toNat = e.start.toNat - e.sm0.avail_out.toNat :=
211        u32_toNat_sub e.hstart
212      have hr := subn_ok (h := e.h0) (r := BRef.blk e.ob) (a := e.A0)
213        (off := e.o0) (n := e.start - e.sm0.avail_out) e.hA0 (by rw [hn]; exact e.hbeg)
214        (by have := e.hAsz; omega)
215      simpa only [hn, Env.bg] using hr
216    have hend : OkOn e.h0 (Ptr.add e.sm0.next_out (e.sm0.avail_out - 257).toNat)
217        (.ref (BRef.blk e.ob) (e.o0 + e.sm0.avail_out.toNat - 257)) := by
218      rw [e.hnout, u32_toNat_sub (by change 257 ≤ e.sm0.avail_out.toNat; have := e.hao; omega)]
219      have hr := Ptr.add_nat_ok (h := e.h0) (r := BRef.blk e.ob) (a := e.A0)
220        (off := e.o0) (n := e.sm0.avail_out.toNat - 257) e.hA0 (by have := e.hAsz; omega)
221      have hoff : e.o0 + (e.sm0.avail_out.toNat - 257) = e.o0 + e.sm0.avail_out.toNat - 257 := by have := e.hao; omega
222      simpa [hoff] using hr
223    unfold inflate_fast
224    refine Wp.bindO (x := e.sm0) (by rw [e.hstrm]; exact ldZStream_ok e.hsm) ?_
225    refine Wp.bindO (x := some (InflateStateRef.tab e.stid)) (by rw [e.hstate]; exact castInflateState_ok) ?_
226    refine Wp.bindO hlast ?_
227    refine Wp.bindO hbeg ?_
228    refine Wp.bindO hend ?_
229    refine Wp.bindO (ldInflateState_tab e.hs0) ?_
230    refine Wp.bindO (shl32_ok (x := 1) (n := e.s0.lenbits) (by have := e.hlt.1; omega)) ?_
231    refine Wp.bindO (shl32_ok (x := 1) (n := e.s0.distbits) (by have := e.hdt.1; omega)) ?_
232    rw [e.hnin, e.hnout]
233    have origin0 : Origin.Inv e l0.hold.toNat l0.bits.toNat e.i0 0 := initial_origin e
234    obtain ⟨l, h, hr, hpost⟩ := loop_origin_wp hc0 l0 e.i0 e.o0 e.A0 e.sm0.msg e.s0.mode 0
235      hl0 rfl rfl (by have := e.hai; omega) (by have := e.hao; omega) origin0
236    rw [e.heap_initial] at hr
237    refine Wp.bindE hr ?_
238    obtain ⟨i, o, A, msg, mode, usedBits, hl, ho, hA, hh, origin, _⟩ := hpost
239    rw [hh]
240    exact finish_origin_wp e A msg mode l i o hl hA ho usedBits origin
241  obtain ⟨⟨⟩, after, hr, hp⟩ := hw
242  obtain ⟨safeAfter, safeRun, safePost⟩ := inflate_fast_safe e
243  have same : safeAfter = after := by
244    have eq := safeRun.symm.trans hr
245    cases eq
246    rfl
247  subst safeAfter
248  exact ⟨after, hr, safePost, hp⟩
249
250end Zlib.Inffast.Proofs