public-zerror.lean

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

1import ZlibF.Spec.Public.Queries
2
3namespace ZlibF.Spec.Public.Proofs
4open C Zlib.Zutil
5
6private theorem zError_eval (err : Int32) :
7    zError err = strLit (errorText err.toInt) := by
8  funext h
9  by_cases hr : err < -6 || err > 2
10  · have h1 : err.toInt < -6 ∨ 2 < err.toInt := by
11      simp only [Bool.or_eq_true, decide_eq_true_eq] at hr
12      rcases hr with hr | hr
13      · left; have := Int32.lt_iff_toInt_lt.mp hr; simpa using this
14      · right; have := Int32.lt_iff_toInt_lt.mp hr; simpa using this
15    have : errorText err.toInt = "" := by
16      unfold errorText
17      split <;> first | omega | rfl
18    rw [this]
19    simp [zError, hr, z_errmsg, strLit]
20  · have h1 : -6 ≤ err.toInt ∧ err.toInt ≤ 2 := by
21      simp only [Bool.or_eq_true, decide_eq_true_eq, not_or, Int32.not_lt] at hr
22      have a := Int32.le_iff_toInt_le.mp hr.1
23      have b := Int32.le_iff_toInt_le.mp hr.2
24      simpa using And.intro a b
25    obtain ⟨k, hk1, hk2, rfl⟩ : ∃ k : Int, -6 ≤ k ∧ k ≤ 2 ∧ err = Int32.ofInt k :=
26      ⟨err.toInt, h1.1, h1.2, (Int32.ofInt_toInt err).symm⟩
27    rcases (by omega : k = -6 ∨ k = -5 ∨ k = -4 ∨ k = -3 ∨ k = -2 ∨ k = -1 ∨ k = 0 ∨ k = 1 ∨ k = 2) with
28      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> rfl
29
30set_option maxRecDepth 100000 in
31private theorem errorText_lit (k : Int) : errorText k ∈ strTable := by
32  unfold errorText
33  rw [Array.mem_def]
34  split <;> decide +kernel
35
36/-- `const char *zError(int err)` returns the public read-only message on every heap. -/
37theorem zError : Goal.zError := by
38  intro h err
39  obtain ⟨i, hr, hi⟩ := strLitRef_of_mem (h := h) (errorText_lit err.toInt)
40  refine ⟨.ref (.str i) 0, ?_, i, rfl, ?_, rfl⟩
41  · simpa only [C.run, zError_eval, strLit] using hr
42  · simp [hi, strBytes]
43
44#print axioms zError
45end ZlibF.Spec.Public.Proofs