infback.c.back.lean

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

1import ZlibF.Proof.«infback.c.callbacks»
2
3/-!
4# infback.c: `inflateBack`, the entry checks and the end-of-input exit
5
6Proved here: the `Z_STREAM_ERROR` exits of the entry, and the exit when `in` has no input at the first `PULL`
7(`Z_BUF_ERROR`, `next_in` is `NULL`, `avail_in` is 0, `out` is not called). The loop over the blocks is open (see
8`docs/proof/callbacks.md`).
9-/
10
11namespace Zlib.Infback.Spec
12open C Zlib.Inflate Zlib.Inflate.Spec
13
14/-- The heap after the first two writes of `inflateBack`: `strm->msg = NULL`, and the state set to the start
15(`mode = TYPE`, `last = 0`, `whave = 0`). -/
16def backEntryHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (zs : Nat) (st : InflateState) : Heap :=
17  setI (r.put h { z with msg := .null }) zs { st with mode := TYPE, last := 0, whave := 0 }
18
19/-- The callback `in` never has input: whenever it is called under `R`, it returns the count 0. -/
20def InEof (inCb : InCb) (inDesc : BPtr) (R : Heap → Prop) : Prop :=
21  ∀ h nx, R h → ∃ nx' h', inCb inDesc nx h = .ok ((0, nx'), h')
22
23end Zlib.Infback.Spec
24
25namespace Zlib.Infback.Proofs
26open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
27
28theorem fuel_succ : ∃ n, fuel = n + 1 + 1 := ⟨fuel - 2, by unfold fuel; omega⟩
29
30/-- A loop whose condition holds and whose body leaves (`goto inf_leave`) at the first trip leaves. -/
31theorem xwhile_leave {cond : X Bool} {body : X Unit} {l l' : IL} {h h' : Heap}
32    (hc : StateT.run (ExceptT.run cond) l h = .ok ((Except.ok true, l), h))
33    (hb : StateT.run (ExceptT.run body) l h = .ok ((Except.error Ex.leave, l'), h')) :
34    StateT.run (ExceptT.run (xwhile cond body)) l h = .ok ((Except.error Ex.leave, l'), h') := by
35  unfold xwhile xwhileBrk cwhile
36  obtain ⟨n, hn⟩ := fuel_succ
37  rw [hn]
38  simp [cwhile.go, ExceptT.run, ExceptT.mk, StateT.run, bind, ExceptT.bind, ExceptT.bindCont, StateT.bind, pure,
39    ExceptT.pure, StateT.pure] at *
40  erw [hc]
41  simp only [↓reduceIte]
42  erw [hb]
43  simp [StateT.pure, cwhile.go]
44
45/-! ### Running the monad `X` -/
46
47theorem xrun_bind {α β : Type} (m : X α) (f : α → X β) (l : IL) (h : Heap) :
48    StateT.run (ExceptT.run (m >>= f)) l h =
49      match StateT.run (ExceptT.run m) l h with
50      | .ok ((.ok a, l'), h') => StateT.run (ExceptT.run (f a)) l' h'
51      | .ok ((.error e, l'), h') => .ok ((.error e, l'), h')
52      | .error e => .error e := by
53  cases hm : StateT.run (ExceptT.run m) l h with
54  | error e => simp [bind, ExceptT.bind, ExceptT.bindCont, StateT.bind, ExceptT.run, ExceptT.mk, StateT.run] at hm ⊢; simp [hm]
55  | ok p =>
56    obtain ⟨⟨r, l'⟩, h'⟩ := p
57    cases r <;> simp [bind, ExceptT.bind, ExceptT.bindCont, StateT.bind, ExceptT.run, ExceptT.mk, StateT.run, StateT.pure,
58      pure, ExceptT.pure] at hm ⊢ <;> simp [hm, StateT.pure]
59
60theorem xrun_get (l : IL) (h : Heap) : StateT.run (ExceptT.run (get : X IL)) l h = .ok ((.ok l, l), h) := rfl
61theorem xrun_set (l l0 : IL) (h : Heap) : StateT.run (ExceptT.run (set l0 : X PUnit)) l h = .ok ((.ok ⟨⟩, l0), h) := rfl
62theorem xrun_modify (f : IL → IL) (l : IL) (h : Heap) :
63    StateT.run (ExceptT.run (modify f : X PUnit)) l h = .ok ((.ok ⟨⟩, f l), h) := rfl
64theorem xrun_throw {α : Type} (e : Ex) (l : IL) (h : Heap) :
65    StateT.run (ExceptT.run (throw e : X α)) l h = .ok ((.error e, l), h) := rfl
66theorem xrun_pure {α : Type} (a : α) (l : IL) (h : Heap) :
67    StateT.run (ExceptT.run (pure a : X α)) l h = .ok ((.ok a, l), h) := rfl
68theorem xrun_lift {α : Type} (m : M α) (l : IL) (h : Heap) :
69    StateT.run (ExceptT.run (liftM m : X α)) l h =
70      match m h with | .ok (a, h') => .ok ((.ok a, l), h') | .error e => .error e := by
71  cases hm : m h <;> simp [liftM, monadLift, MonadLift.monadLift, ExceptT.lift, StateT.lift, ExceptT.run, ExceptT.mk,
72    StateT.run, bind, ExceptT.bind, ExceptT.bindCont, StateT.bind, pure, ExceptT.pure, StateT.pure, Functor.map, StateT.map, hm]
73
74theorem PULL_eof {c : BCtx} {l : IL} {h h3 : Heap} {nx : BPtr} (h0 : l.have_ = 0)
75    (hin : c.inCb c.inDesc l.next h = .ok ((0, nx), h3)) :
76    StateT.run (ExceptT.run (PULL c)) l h =
77      .ok ((Except.error Ex.leave, { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }), h3) := by
78  simp [PULL, xrun_bind, xrun_get, xrun_set, xrun_throw, xrun_pure, xrun_lift, hin, h0]
79
80theorem PULLBYTE_eof {c : BCtx} {l : IL} {h h3 : Heap} {nx : BPtr} (h0 : l.have_ = 0)
81    (hin : c.inCb c.inDesc l.next h = .ok ((0, nx), h3)) :
82    StateT.run (ExceptT.run (PULLBYTE c)) l h =
83      .ok ((Except.error Ex.leave, { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }), h3) := by
84  simp [PULLBYTE, xrun_bind, PULL_eof h0 hin]
85
86theorem NEEDBITS_eof {c : BCtx} {l : IL} {h h3 : Heap} {nx : BPtr} {n : UInt32} (h0 : l.have_ = 0) (hb : l.bits < n)
87    (hin : c.inCb c.inDesc l.next h = .ok ((0, nx), h3)) :
88    StateT.run (ExceptT.run (NEEDBITS c n)) l h =
89      .ok ((Except.error Ex.leave, { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }), h3) := by
90  unfold NEEDBITS
91  apply xwhile_leave
92  · simp [xrun_bind, xrun_get, xrun_pure, hb]
93  · exact PULLBYTE_eof h0 hin
94
95theorem back_TYPE_eof {c : BCtx} {zs : Nat} {s : InflateState} {l : IL} {h h3 : Heap} {nx : BPtr}
96    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hl : s.last = 0) (h0 : l.have_ = 0) (hb : l.bits < 3)
97    (hin : c.inCb c.inDesc l.next h = .ok ((0, nx), h3)) :
98    StateT.run (ExceptT.run (back_TYPE c)) l h =
99      .ok ((Except.error Ex.leave, { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }), h3) := by
100  have e : liftM (rdS c.st (·.last)) = (liftM (rdS c.st (·.last)) : X Int32) := rfl
101  unfold back_TYPE
102  simp [xrun_bind, xrun_lift, hc, rdI_eq, hs, hl, NEEDBITS_eof h0 hb hin]
103
104theorem back_dispatch_eof {c : BCtx} {zs : Nat} {s : InflateState} {l : IL} {h h3 : Heap} {nx : BPtr}
105    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hm : s.mode = TYPE) (hl : s.last = 0)
106    (h0 : l.have_ = 0) (hb : l.bits < 3)
107    (hin : c.inCb c.inDesc l.next h = .ok ((0, nx), h3)) :
108    StateT.run (ExceptT.run (back_dispatch c)) l h =
109      .ok ((Except.error Ex.leave, { l with have_ := 0, next := .null, ret := Z_BUF_ERROR }), h3) := by
110  unfold back_dispatch
111  simp [xrun_bind, xrun_lift, hc, rdI_eq, hs, hm, back_TYPE_eof hc hs hl h0 hb hin]
112
113/-- The registers of `inflateBack` right after its set-up. -/
114def entryIL (next : BPtr) (have_ : UInt32) (window : BPtr) (wsize : UInt32) : IL :=
115  { IL.init with next := next, have_ := have_, hold := 0, bits := 0, put := window, left := wsize }
116
117/-- A null stream: `Z_STREAM_ERROR`, nothing changes. -/
118theorem inflateBack_nullstream (inCb : InCb) (inDesc : BPtr) (outCb : OutCb) (outDesc : BPtr) (h : Heap) :
119    inflateBack none inCb inDesc outCb outDesc h = .ok (Z_STREAM_ERROR, h) := by
120  simp [inflateBack]
121
122/-- No state: `Z_STREAM_ERROR`, nothing changes. -/
123theorem inflateBack_nostate {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hno : z.state = none)
124    (inCb : InCb) (inDesc : BPtr) (outCb : OutCb) (outDesc : BPtr) :
125    inflateBack (some r) inCb inDesc outCb outDesc h = .ok (Z_STREAM_ERROR, h) := by
126  isimp [inflateBack, hz, hno]
127
128/-- **inflateBack, no input.** On a stream set up by `inflateBackInit_` with `next_in = NULL`, if `in` returns 0 when it
129is first called (no input at all), the call returns `Z_BUF_ERROR`, calls `out` not at all, and leaves `next_in = NULL`,
130`avail_in = 0` and `msg = NULL` (`zlib.h`: `Z_BUF_ERROR` if `in()` returned zero when input was needed). The call-backs
131keep `CbContract`; `in` has no input (`InEof`). Everything else of the stream and of the heap is as `in` left it
132(`CbFrame`). -/
133theorem inflateBack_eof {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
134    {inCb : InCb} {inDesc : BPtr} {outCb : OutCb} {outDesc : BPtr} {win : Nat} {ownI ownO : Nat → Prop}
135    {R : Heap → Prop}
136    (hG : BackGood h r zs z st) (hni : z.next_in = .null)
137    (hK : CbContract inCb inDesc outCb outDesc win ownI ownO R) (hEof : InEof inCb inDesc R) (hR : R h) :
138    ∃ h3, C.run (inflateBack (some r) inCb inDesc outCb outDesc) h =
139        .ok (Z_BUF_ERROR, r.put h3 { z with msg := .null, next_in := .null, avail_in := 0 }) ∧
140      CbFrame ownI (backEntryHeap h r z zs st) h3 ∧ R h3 := by
141  have hz := hG.hz
142  have hs := hG.hs
143  have hR2 : R (backEntryHeap h r z zs st) := by
144    refine (hK.local_ h _ ?_).1 hR
145    intro b _; simp [backEntryHeap]
146  obtain ⟨n, nx', h3, he, fr, hR3, -⟩ := hK.inOk _ .null hR2
147  obtain ⟨nx0, h30, he0⟩ := hEof _ .null hR2
148  rw [he] at he0
149  simp only [Except.ok.injEq, Prod.mk.injEq] at he0
150  obtain ⟨⟨rfl, -⟩, rfl⟩ := he0
151  refine ⟨h3, ?_, fr, hR3⟩
152  have hdisp := back_dispatch_eof (c := ⟨some r, some (.tab zs), inCb, inDesc, outCb, outDesc⟩) (zs := zs)
153      (s := { st with mode := TYPE, last := 0, whave := 0 })
154      (l := entryIL .null 0 st.window st.wsize)
155      (h := backEntryHeap h r z zs st) (h3 := h3) (nx := nx') rfl (by simp [backEntryHeap]) rfl rfl rfl (by show (0 : UInt32) < 3; decide) he
156  have hloop := xwhile_leave (cond := pure true) (by simp [xrun_pure]) hdisp
157  have hzst := hG.zst
158  have hz3 : r.get h3 = some { z with msg := .null } := by
159    rw [CbFrame.zget fr r]; simp [backEntryHeap, hz]
160  clear hdisp
161  obtain ⟨ni, ai, ti, no, ao, tout, msg, state, za, zf, op, dt, ad, rs⟩ := z
162  simp only at hni hzst
163  subst hni hzst
164  rw [C.run]
165  unfold inflateBack
166  simp only [entryIL, backEntryHeap] at hloop
167  have hi3 : h3.istates zs = some { st with mode := TYPE, last := 0, whave := 0 } := by
168    rw [fr.istates zs]; simp [backEntryHeap]
169  isimp [hz, hs, backEntryHeap, hloop, entryIL, hi3, hz3]
170
171/-- **Witness for `inflateBack_eof`.** The hypotheses hold together on the heap that the real
172`inflateBackInit_(strm, 8, window, "1.3.2", 112)` makes from `wit0`, with the call-backs `eofIn` and `okOut`: the run of
173`inflateBack` is an actual run and returns `Z_BUF_ERROR`. -/
174theorem inflateBack_eof_witness :
175    ∃ h' h'', C.run (inflateBackInit_ (some (.tab 0)) 8 (.ref (.blk 1) 0) (.ref (.blk 2) 0) 112) wit0 = .ok (Z_OK, h') ∧
176      C.run (inflateBack (some (.tab 0)) eofIn .null okOut .null) h' = .ok (Z_BUF_ERROR, h'') := by
177  have hz : (ZStreamRef.tab 0).get wit0 = some ZStream.zeroed := by simp [ZStreamRef.get, wit0]
178  have hwin : WindowOk wit0 (.ref (.blk 1) 0) (2 ^ (i2u 8).toNat) :=
179    ⟨1, 0, Array.replicate 256 0, rfl, by simp [wit0], by simp [wit0, staticHeap, Heap.empty],
180      by rw [Array.size_replicate]; decide⟩
181  obtain ⟨h', hr, -, hG, -⟩ := inflateBackInit__ok (r := .tab 0) (z := ZStream.zeroed) (wb := 8) (window := .ref (.blk 1) 0)
182    (version := .ref (.blk 2) 0) wit0_uniq wit0_fresh hz (by simp [wit0]) (Or.inl rfl) (Or.inl rfl) (by intro c; cases c)
183    (by unfold OkOn; simp [index8, wit0]; rfl) (by decide) (by decide) hwin
184  have hni : (initStream2 ZStream.zeroed wit0.nextBlk).next_in = .null := by
185    simp [initStream2, initStream, ZStream.zeroed, ZStream.garbage, Junk.of]; rfl
186  obtain ⟨h3, he, -⟩ := inflateBack_eof hG hni (cbContract_eof 1) (fun h nx _ => ⟨nx, h, rfl⟩) trivial
187  exact ⟨h', _, hr, he⟩
188
189end Zlib.Infback.Proofs