inffast.c.flags.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.len»
2
3/-!
4# inffast.c: preservation of the length-loop flag
5
6These lemmas follow successful executions of the actual translated operations.
7They add no safety or termination assumption to the API contract.
8-/
9
10namespace Zlib.Inffast.Proofs
11open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.Spec
12
13theorem cwhile_againL
14    {cond : L → M (Bool × L)} {body : L → M L}
15    (hc : ∀ s h b s' h', cond s h = .ok ((b, s'), h') → s'.againL = s.againL)
16    (hb : ∀ s h s' h', body s h = .ok (s', h') → s'.againL = s.againL)
17    {s s' : L} {h h' : Heap} (hr : cwhile cond body s h = .ok (s', h')) :
18    s'.againL = s.againL := by
19  have go : ∀ n s h s' h', cwhile.go cond body n s h = .ok (s', h') → s'.againL = s.againL := by
20    intro n
21    induction n with
22    | zero => intro s h s' h' hr; cases hr
23    | succ n ih =>
24      intro s h s' h' hr
25      cases hcond : cond s h with
26      | error err => simp [cwhile.go, hcond] at hr
27      | ok v =>
28        rcases v with ⟨⟨b, s1⟩, h1⟩
29        have he1 := hc s h b s1 h1 hcond
30        cases b with
31        | false =>
32          simp only [cwhile.go, bind_app, hcond, Bool.false_eq_true, ite_false, pure_app,
33            Except.ok.injEq, Prod.mk.injEq] at hr
34          rcases hr with ⟨rfl, rfl⟩
35          exact he1
36        | true =>
37          cases hbody : body s1 h1 with
38          | error err => simp [cwhile.go, hcond, hbody] at hr
39          | ok v =>
40            rcases v with ⟨s2, h2⟩
41            simp only [cwhile.go, bind_app, hcond, ite_true, hbody] at hr
42            exact (ih s2 h2 s' h' hr).trans ((hb s1 h1 s2 h2 hbody).trans he1)
43  exact go fuel s h s' h' hr
44
45theorem cdoWhile_againL
46    {cond : L → M (Bool × L)} {body : L → M L}
47    (hc : ∀ s h b s' h', cond s h = .ok ((b, s'), h') → s'.againL = s.againL)
48    (hb : ∀ s h s' h', body s h = .ok (s', h') → s'.againL = s.againL)
49    {s s' : L} {h h' : Heap} (hr : cdoWhile body cond s h = .ok (s', h')) :
50    s'.againL = s.againL := by
51  have go : ∀ n s h s' h', cdoWhile.go body cond n s h = .ok (s', h') → s'.againL = s.againL := by
52    intro n
53    induction n with
54    | zero => intro s h s' h' hr; cases hr
55    | succ n ih =>
56      intro s h s' h' hr
57      cases hbody : body s h with
58      | error err => simp [cdoWhile.go, hbody] at hr
59      | ok v =>
60        rcases v with ⟨s1, h1⟩
61        have he1 := hb s h s1 h1 hbody
62        cases hcond : cond s1 h1 with
63        | error err => simp [cdoWhile.go, hbody, hcond] at hr
64        | ok v =>
65          rcases v with ⟨⟨b, s2⟩, h2⟩
66          have he2 := hc s1 h1 b s2 h2 hcond
67          cases b with
68          | false =>
69            simp only [cdoWhile.go, bind_app, hbody, hcond, Bool.false_eq_true, ite_false, pure_app,
70              Except.ok.injEq, Prod.mk.injEq] at hr
71            rcases hr with ⟨rfl, rfl⟩
72            exact he2.trans he1
73          | true =>
74            simp only [cdoWhile.go, bind_app, hbody, hcond, ite_true] at hr
75            exact (ih s2 h2 s' h' hr).trans (he2.trans he1)
76  exact go fuel s h s' h' hr
77
78theorem ite_M_run {α : Type} (p : Prop) [Decidable p]
79    (f g : M α) (h : Heap) :
80    (if p then f else g) h = if p then f h else g h := by
81  split <;> rfl
82
83theorem pull_againL {l l' : L} {h h' : Heap}
84    (hr : pull l h = .ok (l', h')) : l'.againL = l.againL := by
85  unfold pull at hr
86  repeat' first
87    | split at hr
88    | (rw [bind_app] at hr; try dsimp only at hr)
89    | (rw [ite_M_run] at hr; try dsimp only at hr)
90  all_goals try simp only [pure_app] at hr
91  all_goals grind only
92
93theorem copy1_againL {l l' : L} {h h' : Heap}
94    (hr : copy1 l h = .ok (l', h')) : l'.againL = l.againL := by
95  unfold copy1 at hr
96  repeat' first
97    | split at hr
98    | (rw [bind_app] at hr; try dsimp only at hr)
99    | (rw [ite_M_run] at hr; try dsimp only at hr)
100  all_goals try simp only [pure_app] at hr
101  all_goals grind only
102
103theorem copyOp_againL {l l' : L} {h h' : Heap}
104    (hr : copyOp l h = .ok (l', h')) : l'.againL = l.againL := by
105  apply cdoWhile_againL (body := copy1) (s := l) (s' := l') (h := h) (h' := h') _ _ hr
106  · intro s h b s' h' hc
107    simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hc
108    rcases hc with ⟨⟨_, rfl⟩, _⟩
109    rfl
110  · intro s h s' h' hb
111    exact copy1_againL hb
112
113theorem body3_againL {l l' : L} {h h' : Heap}
114    (hr : body3 l h = .ok (l', h')) : l'.againL = l.againL := by
115  unfold body3 at hr
116  repeat' first
117    | split at hr
118    | (rw [bind_app] at hr; try dsimp only at hr)
119    | (rw [ite_M_run] at hr; try dsimp only at hr)
120  all_goals try simp only [pure_app] at hr
121  all_goals grind only [→ copy1_againL, pure_app]
122
123theorem cond3_againL {l l' : L} {b : Bool} {h h' : Heap}
124    (hr : cond3 l h = .ok ((b, l'), h')) : l'.againL = l.againL := by
125  simp only [cond3, pure_app, Except.ok.injEq, Prod.mk.injEq] at hr
126  rcases hr with ⟨⟨_, rfl⟩, _⟩
127  rfl
128
129theorem whileBody3_againL {l l' : L} {h h' : Heap}
130    (hr : cwhile cond3 body3 l h = .ok (l', h')) : l'.againL = l.againL :=
131  cwhile_againL (fun _ _ _ _ _ h => cond3_againL h) (fun _ _ _ _ h => body3_againL h) hr
132
133theorem doBody3_againL {l l' : L} {h h' : Heap}
134    (hr : cdoWhile body3 cond3 l h = .ok (l', h')) : l'.againL = l.againL :=
135  cdoWhile_againL (fun _ _ _ _ _ h => cond3_againL h) (fun _ _ _ _ h => body3_againL h) hr
136
137set_option maxHeartbeats 2000000 in
138theorem copyMatch_againL {c : Ctx} {l l' : L} {h h' : Heap}
139    (hr : copyMatch c l h = .ok (l', h')) : l'.againL = l.againL := by
140  unfold copyMatch at hr
141  try dsimp only at hr
142  simp only [← body3.eq_def, ← cond3.eq_def] at hr
143  by_cases hd : l.dist > l.op
144  all_goals simp only [hd, ite_true, ite_false] at hr
145  all_goals by_cases hw : l.dist - l.op > c.whave
146  all_goals try simp only [hw, ite_true, ite_false] at hr
147  all_goals repeat' first
148    | split at hr
149    | (rw [bind_app] at hr; try dsimp only at hr)
150    | (rw [ite_M_run] at hr; try dsimp only at hr)
151  all_goals try simp only [pure_app] at hr
152  all_goals grind only [→ copy1_againL, → copyOp_againL, → whileBody3_againL, → doBody3_againL, pure_app]
153
154theorem distCont_againL {c : Ctx} {l l' : L} {h h' : Heap}
155    (hr : distCont c l h = .ok (l', h')) : l'.againL = l.againL := by
156  unfold distCont at hr
157  try dsimp only at hr
158  repeat' first
159    | split at hr
160    | (rw [bind_app] at hr; try dsimp only at hr)
161    | (rw [ite_M_run] at hr; try dsimp only at hr)
162  all_goals try simp only [pure_app] at hr
163  all_goals grind only [→ copyMatch_againL]
164
165theorem dodistBase_againL {c : Ctx} {l l' : L} {h h' : Heap}
166    (hr : dodistBase c l h = .ok (l', h')) : l'.againL = l.againL := by
167  unfold dodistBase at hr
168  repeat' first
169    | split at hr
170    | (rw [bind_app] at hr; try dsimp only at hr)
171    | (rw [ite_M_run] at hr; try dsimp only at hr)
172  all_goals grind only [→ pull_againL, → distCont_againL]
173
174theorem dodist_eq_base (c : Ctx) (l : L) : dodist c l = (do
175  let mut l := { l with againD := false }
176  -- op = (unsigned)(here->bits);
177  let e ← l.here.load
178  l := { l with op := e.bits.toUInt32 }
179  -- hold >>= op; bits -= op;
180  l := { l with hold := ← shr64 l.hold l.op.toUInt64 }
181  l := { l with bits := l.bits - l.op }
182  -- op = (unsigned)(here->op);
183  let e ← l.here.load
184  l := { l with op := e.op.toUInt32 }
185  -- if (op & 16) {                      /* distance base */
186  if l.op &&& 16 != 0 then
187    -- dist = (unsigned)(here->val);
188    let e ← l.here.load
189    l := { l with dist := e.val.toUInt32 }
190    -- op &= 15;                       /* number of extra bits */
191    l := { l with op := l.op &&& 15 }
192    dodistBase c l
193  -- else if ((op & 64) == 0) {          /* 2nd level distance code */
194  else if l.op &&& 64 == 0 then
195    -- here = dcode + here->val + (hold & ((1U << op) - 1));
196    let e ← l.here.load
197    let h1 ← c.dcode.add e.val.toNat
198    let m ← shl32 1 l.op
199    let here ← h1.add (l.hold &&& (m - 1).toUInt64).toNat
200    -- goto dodist;
201    pure { l with here, againD := true }
202  else
203    -- strm->msg = "invalid distance code"; state->mode = BAD; break;
204    badData c "invalid distance code"
205    pure { l with broke := true }) := by rfl
206
207theorem dodist_againL {c : Ctx} {l l' : L} {h h' : Heap}
208    (hr : dodist c l h = .ok (l', h')) : l'.againL = l.againL := by
209  rw [dodist_eq_base] at hr
210  try dsimp only at hr
211  repeat' first
212    | split at hr
213    | (rw [bind_app] at hr; try dsimp only at hr)
214    | (rw [ite_M_run] at hr; try dsimp only at hr)
215  all_goals try simp only [pure_app] at hr
216  all_goals grind only [→ dodistBase_againL]
217
218theorem dodistLoop_againL {c : Ctx} {l l' : L} {h h' : Heap}
219    (hr : cdoWhile (dodist c) (fun l => pure (l.againD, l)) l h = .ok (l', h')) :
220    l'.againL = l.againL := by
221  apply cdoWhile_againL _ (fun _ _ _ _ h => dodist_againL h) hr
222  intro s hp b s' hp' hc
223  simp only [pure_app, Except.ok.injEq, Prod.mk.injEq] at hc
224  rcases hc with ⟨⟨_, rfl⟩, _⟩
225  rfl
226
227theorem dolenDist_againL {c : Ctx} {l l' : L} {h h' : Heap}
228    (hr : dolenDist c l h = .ok (l', h')) : l'.againL = l.againL := by
229  unfold dolenDist at hr
230  repeat' first
231    | split at hr
232    | (rw [bind_app] at hr; try dsimp only at hr)
233  all_goals grind only [→ dodistLoop_againL]
234
235theorem dolenRefill_againL {c : Ctx} {l l' : L} {h h' : Heap}
236    (hr : dolenRefill c l h = .ok (l', h')) : l'.againL = l.againL := by
237  unfold dolenRefill at hr
238  repeat' first
239    | split at hr
240    | (rw [bind_app] at hr; try dsimp only at hr)
241    | (rw [ite_M_run] at hr; try dsimp only at hr)
242  all_goals grind only [→ pull_againL, → dolenDist_againL]
243
244theorem dolenExt_againL {c : Ctx} {l l' : L} {h h' : Heap}
245    (hr : dolenExt c l h = .ok (l', h')) : l'.againL = l.againL := by
246  unfold dolenExt at hr
247  try dsimp only at hr
248  repeat' first
249    | split at hr
250    | (rw [bind_app] at hr; try dsimp only at hr)
251  all_goals grind only [→ dolenRefill_againL]
252
253theorem dolenLen_againL {c : Ctx} {l l' : L} {h h' : Heap}
254    (hr : dolenLen c l h = .ok (l', h')) : l'.againL = l.againL := by
255  unfold dolenLen at hr
256  repeat' first
257    | split at hr
258    | (rw [bind_app] at hr; try dsimp only at hr)
259    | (rw [ite_M_run] at hr; try dsimp only at hr)
260  all_goals grind only [→ pull_againL, → dolenExt_againL, → dolenRefill_againL]
261
262end Zlib.Inffast.Proofs