inffast.c.loop.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.message»
2
3/-!
4# inffast.c: the complete fast loop
5
6The loop uses the checked actual body theorem. Its measure is remaining
7output room, following the earlier output-room proof method. The invariant
8is local to the proof and introduces no additional caller contract.
9-/
10
11namespace Zlib.Inffast.Proofs
12open C Zlib.Inffast Zlib.Inffast.Spec
13variable {e : Env} {c : Ctx}
14
15theorem zstream_put_self {h : Heap} {r : ZStreamRef} {z : ZStream}
16    (hz : r.get h = some z) : r.put h z = h := by
17  cases r with
18  | tab i =>
19    simp only [ZStreamRef.get] at hz
20    simp [ZStreamRef.put, hz, upd_self _ _ _ hz]
21  | in_gzstate_strm i =>
22    simp only [ZStreamRef.get] at hz
23    obtain ⟨g, hg, rfl⟩ := Option.map_eq_some_iff.mp hz
24    simp [ZStreamRef.put, hg, upd_self _ _ _ hg]
25
26theorem Env.heap_initial (e : Env) : e.heap e.A0 e.sm0.msg e.s0.mode = e.h0 := by
27  unfold Env.heap
28  rw [upd_self _ _ _ e.hA0, upd_self _ _ _ e.hs0]
29  exact zstream_put_self e.hsm
30
31theorem Env.heap_msg_mode_eq (e : Env) {A B : Array UInt8} {p q : BPtr} {m n : UInt32}
32    (hh : e.heap A p m = e.heap B q n) : p = q ∧ m = n := by
33  have hz := congrArg (fun h => e.r.get h) hh
34  simp only [e.heap_rget, Option.some.injEq] at hz
35  have hs := congrArg (fun h => h.istates e.stid) hh
36  simp only [e.heap_istates, upd_same, Option.some.injEq] at hs
37  exact ⟨congrArg ZStream.msg hz, congrArg InflateState.mode hs⟩
38
39/-- On a running state, the actual loop condition is exactly the two margins. -/
40theorem fast_cond_live (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
41    (l : L) (i o : Nat) (hl : LS e l i o) (hA : A.size = e.A0.size)
42    (ho : o ≤ e.o0 + e.sm0.avail_out.toNat) (hb : l.broke = false) :
43    (do
44      if l.broke then pure (false, l)
45      else if ← Ptr.lt l.in_ c.last then pure (← Ptr.lt l.out c.end_, l)
46      else pure (false, l)) (e.heap A msg m) =
47    .ok ((decide (i + 6 ≤ e.i0 + e.sm0.avail_in.toNat) &&
48      decide (o + 258 ≤ e.o0 + e.sm0.avail_out.toNat), l), e.heap A msg m) := by
49  have hi : OkOn (e.heap A msg m) (Ptr.lt l.in_ c.last)
50      (decide (i < e.i0 + e.sm0.avail_in.toNat - 5)) := by
51    rw [hl.hin, hc.last]
52    exact Ptr.lt_ok (e.heap_bytes_in A msg m) (by have := hl.hi1; have := e.hINsz; omega)
53      (by have := e.hINsz; omega)
54  have hout : OkOn (e.heap A msg m) (Ptr.lt l.out c.end_)
55      (decide (o < e.o0 + e.sm0.avail_out.toNat - 257)) := by
56    rw [hl.hout, hc.end_]
57    exact Ptr.lt_ok (e.heap_bytes_ob A msg m) (by rw [hA]; have := e.hAsz; omega)
58      (by rw [hA]; have := e.hAsz; omega)
59  have hei : decide (i < e.i0 + e.sm0.avail_in.toNat - 5) =
60      decide (i + 6 ≤ e.i0 + e.sm0.avail_in.toNat) := by
61    simp only [decide_eq_decide]; have := e.hai; omega
62  have heo : decide (o < e.o0 + e.sm0.avail_out.toNat - 257) =
63      decide (o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) := by
64    simp only [decide_eq_decide]; have := e.hao; omega
65  simp only [hb, Bool.false_eq_true, ite_false]
66  rw [bind_ok hi]
67  by_cases hi' : i < e.i0 + e.sm0.avail_in.toNat - 5
68  · simp only [hi', decide_true, ite_true]
69    rw [bind_ok hout, ← hei, ← heo]
70    simp [hi']
71  · simp only [hi', decide_false, Bool.false_eq_true, ite_false]
72    rw [← hei]
73    simp [hi']
74
75/-- Every actual loop execution terminates, frames the output, and records
76whether a margin or an error/end-of-block stopped it. -/
77theorem fast_loop_wp (hc : CtxOK e c) (l : L) (i o : Nat) (A : Array UInt8)
78    (hl : LS e l i o) (hA : A.size = e.A0.size) (hb : l.broke = false)
79    (hi : i + 6 ≤ e.i0 + e.sm0.avail_in.toNat)
80    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
81    (hf : ∀ j, (j < e.o0 ∨ o ≤ j) → A[j]? = e.A0[j]?) :
82    Wp (cdoWhile (inflate_fast_body c)
83      (fun l => do
84        if l.broke then pure (false, l)
85        else if ← Ptr.lt l.in_ c.last then pure (← Ptr.lt l.out c.end_, l)
86        else pure (false, l)) l) (e.heap A e.sm0.msg e.s0.mode)
87      (fun l' h' => ∃ i' o' A' msg' m',
88        LS e l' i' o' ∧ o' ≤ e.o0 + e.sm0.avail_out.toNat ∧ A'.size = e.A0.size ∧
89        h' = e.heap A' msg' m' ∧
90        (∀ j, (j < e.o0 ∨ o' ≤ j) → A'[j]? = e.A0[j]?) ∧
91        ((m' = e.s0.mode ∧ msg' = e.sm0.msg) ∨ (m' = TYPE ∧ msg' = e.sm0.msg) ∨ m' = BAD) ∧
92        (m' ≠ TYPE → m' ≠ BAD → i' + 6 > e.i0 + e.sm0.avail_in.toNat ∨
93          o' + 258 > e.o0 + e.sm0.avail_out.toNat)) := by
94  let Inv : L → Heap → Prop := fun l h => ∃ i o A,
95    LS e l i o ∧ A.size = e.A0.size ∧ h = e.heap A e.sm0.msg e.s0.mode ∧ l.broke = false ∧
96    i + 6 ≤ e.i0 + e.sm0.avail_in.toNat ∧ o + 258 ≤ e.o0 + e.sm0.avail_out.toNat ∧
97    (∀ j, (j < e.o0 ∨ o ≤ j) → A[j]? = e.A0[j]?)
98  let μ : L → Nat := fun l => match l.out with
99    | .null => 0
100    | .ref _ k => e.o0 + e.sm0.avail_out.toNat - k
101  have hμ : ∀ l i o, LS e l i o → μ l = e.o0 + e.sm0.avail_out.toNat - o := by
102    intro l i o hl
103    simp only [μ, hl.hout]
104  refine Wp.cdoWhile Inv μ _ ?_ ⟨i, o, A, hl, hA, rfl, hb, hi, ho, hf⟩ ?_
105  · intro l h hI
106    obtain ⟨i, o, A, hl, hA, rfl, hb, hi, ho, hf⟩ := hI
107    have hp : StepPre e c A l i o := ⟨hc, hl, hA, hi, ho, hb⟩
108    obtain ⟨l1, h1, hr, hpost⟩ := inflate_fast_body_step_safe e c A e.sm0.msg e.s0.mode l i o hp
109    obtain ⟨B, p, q, hmsgheap, _, htype⟩ := Wp.at_run
110      (inflate_fast_body_type_message e c A e.sm0.msg e.s0.mode l i o hp) hr
111    obtain ⟨i', o', A', msg', m', hl', hii, hi6, hoo, ho258, hsz, hh, _, hframe, hcont, hbreak⟩ := hpost
112    have hAsz : A'.size = e.A0.size := hsz.trans hA
113    have hoend : o' ≤ e.o0 + e.sm0.avail_out.toNat := by omega
114    have hft : ∀ j, (j < e.o0 ∨ o' ≤ j) → A'[j]? = e.A0[j]? := by
115      intro j hj
116      rw [hframe j (by have := hl.ho0; omega)]
117      exact hf j (by omega)
118    have hmq := e.heap_msg_mode_eq (hh.symm.trans hmsgheap)
119    have htype' : m' = TYPE → msg' = e.sm0.msg := by
120      intro hm
121      exact hmq.1.trans (htype (hmq.2.symm.trans hm))
122    refine ⟨l1, h1, hr, ?_⟩
123    cases hstop : l1.broke with
124    | true =>
125      refine Or.inl ⟨l1, h1, ?_, i', o', A', msg', m', hl', hoend, hAsz, hh, hft, ?_, ?_⟩
126      · simp [hstop]
127      · rcases hbreak hstop with hm | hm
128        · exact Or.inr (Or.inl ⟨hm, htype' hm⟩)
129        · exact Or.inr (Or.inr hm)
130      · intro hnt hnb
131        rcases hbreak hstop with hm | hm
132        · exact False.elim (hnt hm)
133        · exact False.elim (hnb hm)
134    | false =>
135      obtain ⟨hout, hmsg, hmode⟩ := hcont hstop
136      have hcnd := fast_cond_live hc A' msg' m' l1 i' o' hl' hAsz hoend hstop
137      by_cases hroom : i' + 6 ≤ e.i0 + e.sm0.avail_in.toNat ∧
138          o' + 258 ≤ e.o0 + e.sm0.avail_out.toNat
139      · refine Or.inr ⟨l1, h1, ?_, ?_, ?_⟩
140        · rw [hh]; simpa [hstop, hroom.1, hroom.2] using hcnd
141        · exact ⟨i', o', A', hl', hAsz, by rw [hh, hmsg, hmode], hstop, hroom.1, hroom.2, hft⟩
142        · rw [hμ _ _ _ hl', hμ _ _ _ hl]
143          omega
144      · refine Or.inl ⟨l1, h1, ?_, i', o', A', msg', m', hl', hoend, hAsz, hh, hft,
145          Or.inl ⟨hmode, hmsg⟩, ?_⟩
146        · have hcfalse : (decide (i' + 6 ≤ e.i0 + e.sm0.avail_in.toNat) &&
147              decide (o' + 258 ≤ e.o0 + e.sm0.avail_out.toNat)) = false := by
148            simp only [Bool.and_eq_false_iff, decide_eq_false_iff_not]
149            omega
150          rw [hh]
151          simpa [hstop, hcfalse] using hcnd
152        · intro _ _; omega
153  · rw [hμ _ _ _ hl]
154    apply lt_fuel_of
155    have := UInt32.toNat_lt e.sm0.avail_out
156    have := hl.ho0
157    omega
158
159end Zlib.Inffast.Proofs