inflate.c.main.type.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«inflate.c.main.common»
2
3/-!
4# inflate.c: `TYPE` and `TYPEDO` (the block header)
5-/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9
10/-- `case TYPE:` with `flush` of `Z_BLOCK` or `Z_TREES`: `goto inf_leave` at once, nothing changes. -/
11theorem inflate_TYPE_leave (c : Ctx) (l : IL) (h : Heap) (hf : c.flush = Z_BLOCK ∨ c.flush = Z_TREES) :
12    runX (inflate_TYPE c) l h = .ok ((.error Ex.leave, l), h) := by
13  unfold inflate_TYPE
14  have : (c.flush == Z_BLOCK || c.flush == Z_TREES) = true := by rcases hf with e | e <;> simp [e]
15  simp only [this, ↓reduceIte]
16  rw [runX_bind, runX_throw]
17
18/-- `case TYPE:` with any other `flush`: it is `case TYPEDO:`. -/
19theorem inflate_TYPE_go (c : Ctx) (l : IL) (h : Heap) (hf : c.flush ≠ Z_BLOCK ∧ c.flush ≠ Z_TREES) :
20    runX (inflate_TYPE c) l h = runX (inflate_TYPEDO c) l h := by
21  unfold inflate_TYPE
22  have : (c.flush == Z_BLOCK || c.flush == Z_TREES) = false := by simp [hf.1, hf.2]
23  simp [this]
24
25/-- `case TYPEDO:` after a last block: align to a byte, mode `CHECK`. -/
26theorem inflate_TYPEDO_last {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hl : s.last ≠ 0) :
27    runX (inflate_TYPEDO c) l h = .ok ((.ok (), bytebits l), setI h zs { s with mode := CHECK }) := by
28  unfold inflate_TYPEDO
29  rw [runX_bind, runX_rdS E]
30  simp only [hl, bne_iff_ne, ne_eq, not_false_eq_true, ↓reduceIte]
31  rw [runX_bind, BYTEBITS_run]
32  simp only []
33  rw [runX_bind, runX_setMode E]
34  rfl
35
36/-- `case TYPEDO:` when `NEEDBITS(3)` runs out of input: `goto inf_leave` with what `NEEDBITS` left. -/
37theorem inflate_TYPEDO_wait {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l l1 : IL) (hl : s.last = 0)
38    (e : Ex) (hN : runX (NEEDBITS 3) l h = .ok ((.error e, l1), h)) :
39    runX (inflate_TYPEDO c) l h = .ok ((.error e, l1), h) := by
40  unfold inflate_TYPEDO
41  rw [runX_bind, runX_rdS E]
42  simp only [hl, bne_iff_ne, ne_eq, not_true_eq_false, ↓reduceIte]
43  rw [runX_bind, hN]
44
45/-- The rest of `case TYPEDO:` after the last-block flag is stored. -/
46def typedoTail (c : Ctx) : X Unit := do
47  match (← BITS 2) with
48  | 0 => setMode c.st STORED
49  | 1 =>
50    Zlib.Inftrees.inflate_fixed c.st
51    setMode c.st LEN_
52    if c.flush == Z_TREES then
53      DROPBITS 2
54      throw Ex.leave
55  | 2 => setMode c.st TABLE
56  | _ => badMode c "invalid block type"
57  DROPBITS 2
58
59/-- `case TYPEDO:` with the header bits available (`NEEDBITS(3)` returned with registers `l1`): the last-block flag is
60stored, one bit dropped, and the rest is `typedoTail`. -/
61theorem inflate_TYPEDO_head {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l l1 : IL) (hl : s.last = 0)
62    (hN : runX (NEEDBITS 3) l h = .ok ((.ok (), l1), h)) :
63    runX (inflate_TYPEDO c) l h = runX (typedoTail c) { l1 with hold := l1.hold >>> 1, bits := l1.bits - 1 }
64      (setI h zs { s with last := u2i (l1.hold.toUInt32 &&& ((1 : UInt32) <<< 1 - 1)) }) := by
65  unfold inflate_TYPEDO
66  rw [runX_bind, runX_rdS E]
67  simp only [hl, bne_iff_ne, ne_eq, not_true_eq_false, ↓reduceIte]
68  rw [runX_bind, hN]
69  simp only []
70  rw [runX_bind, BITS_run l1 h 1 (by decide)]
71  simp only []
72  rw [runX_bind, runX_wrS E]
73  simp only []
74  have E' : Env c (setI h zs { s with last := u2i (l1.hold.toUInt32 &&& ((1 : UInt32) <<< 1 - 1)) }) r zs z
75      { s with last := u2i (l1.hold.toUInt32 &&& ((1 : UInt32) <<< 1 - 1)) } := by
76    refine ⟨E.strm, E.st, by simpa using E.hz, by simp⟩
77  rw [runX_bind, DROPBITS_run l1 _ 1 (by decide)]
78  rfl
79
80theorem bits2_eq (l : IL) (k : Nat) (hk : k < 4) (e : l.hold.toNat % 4 = k) :
81    (l.hold.toUInt32 &&& ((1 : UInt32) <<< 2 - 1)) = (k.toUInt32) := by
82  have := BITS_toNat l 2 (by decide)
83  apply UInt32.toNat_inj.mp
84  have h4 : (2 : UInt32).toNat = 2 := rfl
85  rw [h4] at this
86  rw [this]
87  show _ = k % 2 ^ 32
88  rw [Nat.mod_eq_of_lt (by omega : k < 2 ^ 32)]
89  omega
90
91/-- Block type 0: mode `STORED`, then two bits dropped. -/
92theorem typedoTail_stored {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hv : l.hold.toNat % 4 = 0) :
93    runX (typedoTail c) l h = .ok ((.ok (), { l with hold := l.hold >>> 2, bits := l.bits - 2 }),
94      setI h zs { s with mode := STORED }) := by
95  unfold typedoTail
96  rw [runX_bind, BITS_run l h 2 (by decide), bits2_eq l 0 (by decide) hv]
97  simp only [show Nat.toUInt32 0 = (0 : UInt32) from rfl]
98  rw [runX_bind, runX_setMode E]
99  simp only []
100  rw [DROPBITS_run l _ 2 (by decide)]
101  rfl
102
103/-- Block type 2: mode `TABLE`, then two bits dropped. -/
104theorem typedoTail_table {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hv : l.hold.toNat % 4 = 2) :
105    runX (typedoTail c) l h = .ok ((.ok (), { l with hold := l.hold >>> 2, bits := l.bits - 2 }),
106      setI h zs { s with mode := TABLE }) := by
107  unfold typedoTail
108  rw [runX_bind, BITS_run l h 2 (by decide), bits2_eq l 2 (by decide) hv]
109  simp only [show Nat.toUInt32 2 = (2 : UInt32) from rfl]
110  rw [runX_bind, runX_setMode E]
111  simp only []
112  rw [DROPBITS_run l _ 2 (by decide)]
113  rfl
114
115/-- Block type 1 (fixed codes), `flush` not `Z_TREES`: the static tables become current, mode `LEN_`, two bits dropped. -/
116theorem typedoTail_fixed {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hv : l.hold.toNat % 4 = 1)
117    (hf : c.flush ≠ Z_TREES) :
118    runX (typedoTail c) l h = .ok ((.ok (), { l with hold := l.hold >>> 2, bits := l.bits - 2 }),
119      setI h zs { fixedState s with mode := LEN_ }) := by
120  unfold typedoTail
121  rw [runX_bind, BITS_run l h 2 (by decide), bits2_eq l 1 (by decide) hv]
122  simp only [show Nat.toUInt32 1 = (1 : UInt32) from rfl]
123  rw [runX_bind, runX_fixed E]
124  simp only []
125  have E' : Env c (setI h zs (fixedState s)) r zs z (fixedState s) := ⟨E.strm, E.st, by simpa using E.hz, by simp⟩
126  rw [runX_bind, runX_setMode E']
127  simp only [beq_iff_eq, hf, ↓reduceIte, setI_setI]
128  rw [DROPBITS_run l _ 2 (by decide)]
129  rfl
130
131/-- Block type 1 with `flush = Z_TREES`: the same, but two bits are dropped and the call leaves (`goto inf_leave`). -/
132theorem typedoTail_fixed_trees {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL)
133    (hv : l.hold.toNat % 4 = 1) (hf : c.flush = Z_TREES) :
134    runX (typedoTail c) l h = .ok ((.error Ex.leave, { l with hold := l.hold >>> 2, bits := l.bits - 2 }),
135      setI h zs { fixedState s with mode := LEN_ }) := by
136  unfold typedoTail
137  rw [runX_bind, BITS_run l h 2 (by decide), bits2_eq l 1 (by decide) hv]
138  simp only [show Nat.toUInt32 1 = (1 : UInt32) from rfl]
139  rw [runX_bind, runX_fixed E]
140  simp only []
141  have E' : Env c (setI h zs (fixedState s)) r zs z (fixedState s) := ⟨E.strm, E.st, by simpa using E.hz, by simp⟩
142  rw [runX_bind, runX_setMode E']
143  simp only [beq_iff_eq, hf, ↓reduceIte, setI_setI]
144  rw [runX_bind, DROPBITS_run l _ 2 (by decide)]
145  simp only []
146  rw [runX_bind, runX_throw]
147  rfl
148
149set_option maxRecDepth 100000 in
150theorem lit_invalid_block_type : "invalid block type" ∈ strTable :=
151  Array.mem_of_getElem? (i := 112) (by rfl)
152
153/-- Block type 3: the error "invalid block type", mode `BAD`; the two bits are still dropped. -/
154theorem typedoTail_bad {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hv : l.hold.toNat % 4 = 3) :
155    ∃ i, strTable[i]? = some "invalid block type" ∧
156      runX (typedoTail c) l h = .ok ((.ok (), { l with hold := l.hold >>> 2, bits := l.bits - 2 }), badHeap h r zs z s i) := by
157  obtain ⟨i, hi, hb⟩ := runX_badMode E (msg := "invalid block type") lit_invalid_block_type l
158  refine ⟨i, hi, ?_⟩
159  unfold typedoTail
160  rw [runX_bind, BITS_run l h 2 (by decide), bits2_eq l 3 (by decide) hv]
161  simp only [show Nat.toUInt32 3 = (3 : UInt32) from rfl]
162  split
163  · rename_i hh; exact absurd hh (by decide)
164  · rename_i hh; exact absurd hh (by decide)
165  · rename_i hh; exact absurd hh (by decide)
166  rw [runX_bind, hb]
167  simp only []
168  rw [DROPBITS_run l _ 2 (by decide)]
169  rfl
170
171end Zlib.Inflate.Proofs