inflate.c.main.stored2.lean

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

1import ZlibF.Proof.«inflate.c.main.stored»
2
3namespace Zlib.Inflate.Proofs
4open C Zlib.Inflate Zlib.Inflate.Spec
5
6set_option maxRecDepth 100000 in
7theorem lit_invalid_stored : "invalid stored block lengths" ∈ strTable :=
8  Array.mem_of_getElem? (i := 122) (by rfl)
9
10/-- The registers after `case COPY:` has moved `n` bytes: `next` is `nx`, `put` is `pt`. -/
11def copyRegs (l : IL) (n : UInt32) (nx pt : BPtr) : IL :=
12  { l with copy := n, have_ := l.have_ - n, next := nx, left := l.left - n, put := pt }
13
14/-- `case COPY:` copies `n` bytes (`n` at most what the source and the destination hold; the two ranges do not overlap,
15as `memcpy` requires): the heap changes in the destination block and in `state->length`. -/
16theorem copyTail_run {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) {n : UInt32} (hn : n ≠ 0)
17    {rs : BRef} {os db od : Nat} {da sa : Array UInt8}
18    (hput : l.put = .ref (.blk db) od) (hnext : l.next = .ref rs os)
19    (hd : h.bytes db = some da) (hsrc : (Space.get h rs : Option (Array UInt8)) = some sa)
20    (hro : Space.ro h (BRef.blk db) = false) (h1 : od + n.toNat ≤ da.size) (h2 : os + n.toNat ≤ sa.size)
21    (hdis : BRef.blk db ≠ rs ∨ od + n.toNat ≤ os ∨ os + n.toNat ≤ od) :
22    runX (copyTail c n) l h = .ok ((.ok (), copyRegs l n (Ptr.ref rs (os + n.toNat)) (Ptr.ref (BRef.blk db) (od + n.toNat))),
23      setI { h with bytes := upd h.bytes db (some (copyRange da sa od os n.toNat)) } zs { s with length := s.length - n }) := by
24  have hdg : (Space.get h (BRef.blk db) : Option (Array UInt8)) = some da := hd
25  have hmc : memcpyB l.put l.next n.toNat h = .ok ((), { h with bytes := upd h.bytes db (some (copyRange da sa od os n.toNat)) }) := by
26    rw [hput, hnext]
27    exact Ptr.memcpy_ok (rd := BRef.blk db) (rs := rs) hdg hsrc hro h1 h2 hdis
28  have hsz : (copyRange da sa od os n.toNat).size = da.size := size_copyRange _ _ _ _ _
29  obtain ⟨a2, ha2, hs2⟩ := get_after_put hd hsz hsrc
30  obtain ⟨a3, ha3, hs3⟩ := get_after_put hd hsz hdg
31  have hadd1 : OkOn { h with bytes := upd h.bytes db (some (copyRange da sa od os n.toNat)) } (l.next.add (n.toNat : Int))
32      (.ref rs (os + n.toNat)) := by
33    rw [hnext]; exact Ptr.add_nat_ok ha2 (by omega)
34  have hadd2 : OkOn { h with bytes := upd h.bytes db (some (copyRange da sa od os n.toNat)) } (l.put.add (n.toNat : Int))
35      (.ref (.blk db) (od + n.toNat)) := by
36    rw [hput]; exact Ptr.add_nat_ok ha3 (by omega)
37  have hs' : ({ h with bytes := upd h.bytes db (some (copyRange da sa od os n.toNat)) } : Heap).istates zs = some s := E.hs
38  have E' : Env c { h with bytes := upd h.bytes db (some (copyRange da sa od os n.toNat)) } r zs z s :=
39    ⟨E.strm, E.st, E.hz, hs'⟩
40  have hne : (n == 0) = false := by simpa using hn
41  unfold copyTail
42  rw [runX_bind, runX_get]
43  simp only [hne, Bool.false_eq_true, ↓reduceIte]
44  rw [runX_bind, runX_lift_ok hmc]
45  simp only []
46  rw [runX_bind, runX_lift_ok hadd1]
47  simp only []
48  rw [runX_bind, runX_lift_ok hadd2]
49  simp only []
50  rw [runX_bind, runX_set]
51  simp only []
52  rw [runX_bind, runX_wrS E']
53  rfl
54
55/-- `case COPY:` with input and room: copies `copyAmt` bytes, as `copyTail_run` (the source and destination ranges inside
56their blocks and not overlapping). -/
57theorem inflate_COPY_run {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hnz : s.length ≠ 0)
58    (hn : copyAmt s.length l.have_ l.left ≠ 0)
59    {rs : BRef} {os db od : Nat} {da sa : Array UInt8}
60    (hput : l.put = .ref (.blk db) od) (hnext : l.next = .ref rs os)
61    (hd : h.bytes db = some da) (hsrc : (Space.get h rs : Option (Array UInt8)) = some sa)
62    (hro : Space.ro h (BRef.blk db) = false)
63    (h1 : od + (copyAmt s.length l.have_ l.left).toNat ≤ da.size) (h2 : os + (copyAmt s.length l.have_ l.left).toNat ≤ sa.size)
64    (hdis : BRef.blk db ≠ rs ∨ od + (copyAmt s.length l.have_ l.left).toNat ≤ os ∨
65      os + (copyAmt s.length l.have_ l.left).toNat ≤ od) :
66    runX (inflate_COPY c) l h = .ok ((.ok (), copyRegs l (copyAmt s.length l.have_ l.left)
67        (Ptr.ref rs (os + (copyAmt s.length l.have_ l.left).toNat))
68        (Ptr.ref (BRef.blk db) (od + (copyAmt s.length l.have_ l.left).toNat))),
69      setI { h with bytes := upd h.bytes db (some (copyRange da sa od os (copyAmt s.length l.have_ l.left).toNat)) } zs
70        { s with length := s.length - copyAmt s.length l.have_ l.left }) := by
71  rw [inflate_COPY_split E l hnz]
72  exact copyTail_run E l hn hput hnext hd hsrc hro h1 h2 hdis
73
74/-- `case COPY:` with `length` bytes to go but no input or no room: `goto inf_leave`. -/
75theorem inflate_COPY_leave {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hnz : s.length ≠ 0)
76    (hz : copyAmt s.length l.have_ l.left = 0) :
77    runX (inflate_COPY c) l h = .ok ((.error Ex.leave, { l with copy := 0 }), h) := by
78  rw [inflate_COPY_split E l hnz, hz]
79  exact copyTail_stall c l h
80
81/-- `case COPY_:` sets the mode `COPY` and falls into `case COPY:` (run on the updated state). -/
82theorem inflate_COPY__eq {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) :
83    runX (inflate_COPY_ c) l h = runX (inflate_COPY c) l (setI h zs { s with mode := COPY }) := by
84  unfold inflate_COPY_
85  rw [runX_bind, runX_setMode E]
86
87/-- `case STORED:` when the 32 header bits are not all there (`NEEDBITS(32)` after `BYTEBITS` runs out of input). -/
88theorem inflate_STORED_wait {c : Ctx} (l l1 : IL) (h : Heap) (e : Ex)
89    (hN : runX (NEEDBITS 32) (bytebits l) h = .ok ((.error e, l1), h)) :
90    runX (inflate_STORED c) l h = .ok ((.error e, l1), h) := by
91  unfold inflate_STORED
92  rw [runX_bind, BYTEBITS_run]
93  simp only []
94  rw [runX_bind, hN]
95
96/-- `case STORED:` with a bad length complement: the error "invalid stored block lengths", mode `BAD`. -/
97theorem inflate_STORED_bad {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l l1 : IL)
98    (hN : runX (NEEDBITS 32) (bytebits l) h = .ok ((.ok (), l1), h))
99    (hbad : (l1.hold &&& (0xffff : UInt64)) != ((l1.hold >>> 16) ^^^ (0xffff : UInt64))) :
100    ∃ i, strTable[i]? = some "invalid stored block lengths" ∧
101      runX (inflate_STORED c) l h = .ok ((.ok (), l1), badHeap h r zs z s i) := by
102  obtain ⟨i, hi, hb⟩ := runX_badMode E (msg := "invalid stored block lengths") lit_invalid_stored l1
103  refine ⟨i, hi, ?_⟩
104  unfold inflate_STORED
105  rw [runX_bind, BYTEBITS_run]
106  simp only []
107  rw [runX_bind, hN]
108  simp only []
109  rw [runX_bind, runX_get]
110  simp only [hbad, ↓reduceIte]
111  rw [runX_bind, hb]
112  rfl
113
114/-- `case STORED:` with a good header: `length` is set, the bit buffer emptied, mode `COPY_`; with `flush = Z_TREES` the
115call leaves here, otherwise `case COPY_:` follows. -/
116theorem inflate_STORED_ok {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l l1 : IL)
117    (hN : runX (NEEDBITS 32) (bytebits l) h = .ok ((.ok (), l1), h))
118    (hgood : ¬ ((l1.hold &&& (0xffff : UInt64)) != ((l1.hold >>> 16) ^^^ (0xffff : UInt64))) = true) :
119    runX (inflate_STORED c) l h = runX (if c.flush == Z_TREES then (throw Ex.leave : X Unit) else inflate_COPY_ c)
120      { l1 with hold := 0, bits := 0 }
121      (setI h zs { s with length := l1.hold.toUInt32 &&& 0xffff, mode := COPY_ }) := by
122  unfold inflate_STORED
123  rw [runX_bind, BYTEBITS_run]
124  simp only []
125  rw [runX_bind, hN]
126  simp only []
127  rw [runX_bind, runX_get]
128  simp only [hgood, Bool.false_eq_true, ↓reduceIte]
129  rw [runX_bind, runX_wrS E]
130  simp only []
131  rw [runX_bind, runX_INITBITS]
132  simp only []
133  have E' : Env c (setI h zs { s with length := l1.hold.toUInt32 &&& 0xffff }) r zs z { s with length := l1.hold.toUInt32 &&& 0xffff } :=
134    ⟨E.strm, E.st, by simpa using E.hz, by simp⟩
135  rw [runX_bind, runX_setMode E']
136  simp only [setI_setI]
137  split <;> simp_all [runX_bind, runX_throw]
138
139end Zlib.Inflate.Proofs