inflate.c.main.check0.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.simple»
2
3/-!
4# inflate.c: helpers for the table, check and leave modes
5
6`badMode` (`strm->msg = "..."; state->mode = BAD`) as a heap function, and the evaluation rules of the mode
7monad for the accesses to the stream and the state record that the modes of the dynamic tables and of the trailer use.
8-/
9
10namespace Zlib.Inflate.Proofs
11open C Zlib.Inflate Zlib.Inflate.Spec
12
13/-- The heap after `badMode` with the literal number `i`: the stream's `msg` points to it and the mode is `BAD`. -/
14def tcBadHeap (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (s : InflateState) (i : Nat) : Heap :=
15  setI (r.put h { z with msg := .ref (.str i) 0 }) zs { s with mode := BAD }
16
17theorem tcStrLit_run (h : Heap) (msg : String) (hm : msg ∈ strTable) :
18    ∃ i, Zlib.Zutil.strLit msg h = .ok (.ref (.str i) 0, h) ∧ strTable[i]? = some msg :=
19  Zlib.Zutil.Proofs.strLit_run h msg hm
20
21/-- `badMode` writes the message pointer into the stream record and `BAD` into the state record. -/
22theorem tcBadMode_run {h : Heap} {c : Ctx} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState} (msg : String)
23    (hm : msg ∈ strTable) (hr : c.strm = some r) (hc : c.st = some (.tab zs)) (hz : r.get h = some z)
24    (hs : h.istates zs = some s) :
25    ∃ i, strTable[i]? = some msg ∧ badMode c msg h = .ok ((), tcBadHeap h r zs z s i) := by
26  obtain ⟨i, hi, hti⟩ := tcStrLit_run h msg hm
27  refine ⟨i, hti, ?_⟩
28  unfold badMode setMsg
29  rw [hr, hc]
30  simp [bind_app, hi, ldZ_eq, hz, stZ_eq, setMode, wrI_eq, ZStreamRef.put_istates, tcBadHeap, hs]
31
32/-! ### The error messages of these modes are string literals of the sources -/
33
34set_option maxRecDepth 100000 in
35theorem lit_length_check : "incorrect length check" ∈ strTable := by
36  rw [Array.mem_def]
37  decide +kernel
38
39set_option maxRecDepth 100000 in
40theorem lit_data_check : "incorrect data check" ∈ strTable := by
41  rw [Array.mem_def]
42  decide +kernel
43
44set_option maxRecDepth 100000 in
45theorem lit_many_symbols : "too many length or distance symbols" ∈ strTable := by
46  rw [Array.mem_def]
47  decide +kernel
48
49set_option maxRecDepth 100000 in
50theorem lit_code_lengths : "invalid code lengths set" ∈ strTable := by
51  rw [Array.mem_def]
52  decide +kernel
53
54set_option maxRecDepth 100000 in
55theorem lit_bit_length_repeat : "invalid bit length repeat" ∈ strTable := by
56  rw [Array.mem_def]
57  decide +kernel
58
59set_option maxRecDepth 100000 in
60theorem lit_missing_eob : "invalid code -- missing end-of-block" ∈ strTable := by
61  rw [Array.mem_def]
62  decide +kernel
63
64set_option maxRecDepth 100000 in
65theorem lit_literal_lengths : "invalid literal/lengths set" ∈ strTable := by
66  rw [Array.mem_def]
67  decide +kernel
68
69set_option maxRecDepth 100000 in
70theorem lit_distances : "invalid distances set" ∈ strTable := by
71  rw [Array.mem_def]
72  decide +kernel
73
74end Zlib.Inflate.Proofs