inffast.c.env.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.base»
2import ZlibF.Proof.«inffast.c.tableok»
3
4/-!
5# inffast.c: what `inflate_fast` needs of its situation
6
7`Zlib.Inffast.Spec` states the entry conditions and the facts about the decoding tables as predicates over the heap.
8`Zlib.Inffast.Proofs.Env` bundles them with the witnesses (block numbers, offsets, arrays) that the proofs of the
9loop use.
10
11**Tables.** `TableSafe` is the shape that `inflate_table` gives (`proof/inftrees.md`, theorem T2) and that `lenfix`
12and `distfix` have: the root table has `2^root` entries inside the array, an entry is a leaf (literal, base value,
13end of block, invalid code) or a link to a second level inside the array whose entries are leaves; the number of
14bits of a root entry plus that of a second-level entry is at most 15; the extra bits of a length base are at most 5 and
15those of a distance base at most 13; a length base is between 3 and 258 and a distance base is at least 1.
16-/
17
18
19namespace Zlib.Inffast.Proofs
20open C Zlib.Inffast Zlib.Inffast.Spec
21
22/-! ### `ZStreamRef.put` leaves every table but the stream tables alone -/
23
24theorem put_bytes (r : ZStreamRef) (h : Heap) (v : ZStream) : (r.put h v).bytes = h.bytes := by
25  cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
26
27theorem put_ro (r : ZStreamRef) (h : Heap) (v : ZStream) : (r.put h v).ro = h.ro := by
28  cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
29
30theorem put_istates (r : ZStreamRef) (h : Heap) (v : ZStream) : (r.put h v).istates = h.istates := by
31  cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
32
33theorem put_static (r : ZStreamRef) (h : Heap) (v : ZStream) : (r.put h v).static = h.static := by
34  cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
35
36theorem put_get (r : ZStreamRef) (h : Heap) (v0 v : ZStream) (hg : r.get h = some v0) :
37    r.get (r.put h v) = some v := by
38  cases r with
39  | tab i =>
40    simp only [ZStreamRef.get] at hg
41    simp only [ZStreamRef.put, hg, ZStreamRef.get]
42    exact upd_same _ _ _
43  | in_gzstate_strm i =>
44    simp only [ZStreamRef.get] at hg
45    cases hs : h.gzstates i with
46    | none => simp [hs] at hg
47    | some g => simp [ZStreamRef.put, ZStreamRef.get, hs]
48
49theorem put_put (r : ZStreamRef) (h : Heap) (v0 v v' : ZStream) (hg : r.get h = some v0) :
50    r.put (r.put h v) v' = r.put h v' := by
51  cases r with
52  | tab i =>
53    simp only [ZStreamRef.get] at hg
54    simp [ZStreamRef.put, hg, upd_upd]
55  | in_gzstate_strm i =>
56    simp only [ZStreamRef.get] at hg
57    cases hs : h.gzstates i with
58    | none => simp [hs] at hg
59    | some g => simp [ZStreamRef.put, hs, upd_upd]
60
61theorem put_istates_comm (r : ZStreamRef) (h : Heap) (v : ZStream) (t : Tbl (Option InflateState)) :
62    ({ r.put h v with istates := t } : Heap) = r.put { h with istates := t } v := by
63  cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
64
65theorem put_bytes_comm (r : ZStreamRef) (h : Heap) (v : ZStream) (t : Tbl (Option (Array UInt8))) :
66    ({ r.put h v with bytes := t } : Heap) = r.put { h with bytes := t } v := by
67  cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
68
69/-! ### The situation -/
70
71/-- Everything `inflate_fast` needs of the heap `h0` at entry, with the witnesses. These are the preconditions of
72`inflate_fast_safe` (`Zlib.Inffast.Proofs.Env.of_pre` builds one from the hypotheses of the theorem). -/
73structure Env where
74  h0 : Heap
75  strm : ZStreamPtr
76  start : UInt32
77  -- the stream record and the state
78  r : ZStreamRef
79  sm0 : ZStream
80  stid : Nat
81  s0 : InflateState
82  hstrm : strm = some r
83  hsm : r.get h0 = some sm0
84  hrw : r.isRo = false
85  hstate : sm0.state = some (StateRef.inflate stid)
86  hs0 : h0.istates stid = some s0
87  -- the input
88  ib : Nat
89  i0 : Nat
90  IN : Array UInt8
91  hnin : sm0.next_in = .ref (BRef.blk ib) i0
92  hIN : h0.bytes ib = some IN
93  hai : 6 ≤ sm0.avail_in.toNat
94  hINsz : i0 + sm0.avail_in.toNat ≤ IN.size
95  hINbig : IN.size < 2 ^ 63
96  -- the output
97  ob : Nat
98  o0 : Nat
99  A0 : Array UInt8
100  hnout : sm0.next_out = .ref (BRef.blk ob) o0
101  hA0 : h0.bytes ob = some A0
102  hro : h0.ro ob = false
103  hao : 258 ≤ sm0.avail_out.toNat
104  hAsz : o0 + sm0.avail_out.toNat ≤ A0.size
105  hAbig : A0.size < 2 ^ 63
106  hstart : sm0.avail_out.toNat ≤ start.toNat
107  hbeg : start.toNat - sm0.avail_out.toNat ≤ o0
108  hsep : ib ≠ ob
109  -- the bit buffer
110  hbits : s0.bits.toNat < 8
111  hhold : s0.hold.toNat < 2 ^ s0.bits.toNat
112  hsane : s0.sane ≠ 0
113  -- the window
114  hws : s0.wsize.toNat ≤ 32768
115  hwh : s0.whave.toNat ≤ s0.wsize.toNat
116  hwn : s0.wnext.toNat ≤ s0.wsize.toNat
117  wb : Nat
118  woff : Nat
119  W : Array UInt8
120  hwin : s0.whave ≠ 0 →
121    s0.window = .ref (BRef.blk wb) woff ∧ wb ≠ ob ∧ h0.bytes wb = some W ∧ woff + s0.wsize.toNat ≤ W.size
122  -- the tables
123  rl : CodeRef
124  ol : Nat
125  LCA : Array Code
126  hlc : s0.lencode = .ref rl ol
127  hLCA : Space.get h0 rl = some LCA
128  hlt : LenTableSafe LCA ol s0.lenbits.toNat
129  rd : CodeRef
130  od : Nat
131  DCA : Array Code
132  hdc : s0.distcode = .ref rd od
133  hDCA : Space.get h0 rd = some DCA
134  hdt : DistTableSafe DCA od s0.distbits.toNat
135
136/-- The heap while `inflate_fast` runs: the output block is `A`, the message of the stream is `msg` and the mode of
137the state is `m`; nothing else differs from `h0`. -/
138def Env.heap (e : Env) (A : Array UInt8) (msg : BPtr) (m : UInt32) : Heap :=
139  ZStreamRef.put
140    { e.h0 with bytes := upd e.h0.bytes e.ob (some A),
141                istates := upd e.h0.istates e.stid (some { e.s0 with mode := m }) }
142    e.r { e.sm0 with msg := msg }
143
144/-- The heap of the loop before any `break`: the message and the mode are those of the entry. -/
145def Env.hp (e : Env) (A : Array UInt8) : Heap := e.heap A e.sm0.msg e.s0.mode
146
147variable (e : Env)
148
149theorem Env.heap_bytes (A msg m) : (e.heap A msg m).bytes = upd e.h0.bytes e.ob (some A) := by
150  unfold Env.heap; rw [put_bytes]
151
152theorem Env.heap_ro (A msg m) : (e.heap A msg m).ro = e.h0.ro := by
153  unfold Env.heap; rw [put_ro]
154
155theorem Env.heap_istates (A msg m) :
156    (e.heap A msg m).istates = upd e.h0.istates e.stid (some { e.s0 with mode := m }) := by
157  unfold Env.heap; rw [put_istates]
158
159theorem Env.heap_static (A msg m) : (e.heap A msg m).static = e.h0.static := by
160  unfold Env.heap; rw [put_static]
161
162theorem Env.heap_rget (A msg m) : e.r.get (e.heap A msg m) = some { e.sm0 with msg := msg } := by
163  unfold Env.heap
164  apply put_get e.r _ e.sm0
165  cases hr : e.r with
166  | tab i =>
167    have := e.hsm; rw [hr] at this; simpa [ZStreamRef.get] using this
168  | in_gzstate_strm i =>
169    have := e.hsm; rw [hr] at this; simpa [ZStreamRef.get] using this
170
171theorem Env.heap_bytes_ne (A msg m) {b : Nat} (hb : b ≠ e.ob) : (e.heap A msg m).bytes b = e.h0.bytes b := by
172  rw [e.heap_bytes]; exact upd_ne _ _ _ _ hb
173
174theorem Env.heap_bytes_ob (A msg m) : (e.heap A msg m).bytes e.ob = some A := by
175  rw [e.heap_bytes]; exact upd_same _ _ _
176
177theorem Env.heap_ro_ob (A msg m) : (e.heap A msg m).ro e.ob = false := by
178  rw [e.heap_ro]; exact e.hro
179
180end Zlib.Inffast.Proofs