public-zlib-version.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
5
6set_option maxRecDepth 100000 in
7/-- `const char *zlibVersion(void)`: return the read-only pinned version string. -/
8theorem zlibVersion : Goal.zlibVersion := by
9  intro h
10  have hm : ZLIB_VERSION ∈ strTable := by
11    rw [Array.mem_def]
12    decide +kernel
13  obtain ⟨i, hr, hi⟩ := strLitRef_of_mem (h := h) hm
14  refine ⟨.ref (.str i) 0, ?_, i, rfl, ?_, rfl⟩
15  · exact hr
16  · simp [hi, strBytes]
17
18#print axioms zlibVersion
19end ZlibF.Spec.Public.Proofs