Queries.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.Calls
2import ZlibF.Spec.Api.Compress
3
4/-!
5# Complete contracts for pure bounds and public identification queries
6
7These goals name actual translated entries. They have no extra stream invariant or callee
8contract hypothesis. Heap equality supplies frame and ownership preservation for the queries.
9The numeric bound contract states the returned formula, not compressed-output adequacy.
10-/
11
12namespace ZlibF.Spec.Public
13open C
14
15/-- A result points to the stated NUL-terminated read-only static string. -/
16def StaticString (h : Heap) (p : BPtr) (text : String) : Prop :=
17  ∃ i, p = .ref (.str i) 0 ∧
18    Space.get h (BRef.str i) = some (text.toUTF8.data.push 0) ∧
19    Space.ro h (BRef.str i) = true
20
21/-- Public error text; every integer outside the documented return-code range gives empty text. -/
22def errorText : Int → String
23  | 2 => "need dictionary"
24  | 1 => "stream end"
25  | -1 => "file error"
26  | -2 => "stream error"
27  | -3 => "data error"
28  | -4 => "insufficient memory"
29  | -5 => "buffer error"
30  | -6 => "incompatible version"
31  | _ => ""
32
33/-- `uLong compressBound(uLong sourceLen)`.
34Every LP64 input returns the saturated public bound formula. No heap is accessed. -/
35def Goal.compressBound : Prop :=
36  ∀ n : UInt64, (Zlib.Compress.compressBound n).toNat = Api.compressBound n.toNat
37
38/-- `z_size_t compressBound_z(z_size_t sourceLen)`.
39Every LP64 input returns the saturated public bound formula. No heap is accessed. -/
40def Goal.compressBound_z : Prop :=
41  ∀ n : UInt64, (Zlib.Compress.compressBound_z n).toNat = Api.compressBound n.toNat
42
43/-- `const char *zlibVersion(void)`.
44Every heap returns the pinned header's version string, as static read-only storage.
45The call terminates without a fault, allocates nothing and changes no heap observation. -/
46def Goal.zlibVersion : Prop :=
47  ∀ h : Heap, ∃ p,
48    C.run Zlib.Zutil.zlibVersion h = .ok (p, h) ∧ StaticString h p ZLIB_VERSION
49
50/-- `uLong zlibCompileFlags(void)`.
51The default LP64 build reports sizes 4, 8, 8 and 8 in its four two-bit size fields,
52with the default feature flags. Every heap is unchanged and execution does not fault. -/
53def Goal.zlibCompileFlags : Prop :=
54  ∀ h : Heap, C.run Zlib.Zutil.zlibCompileFlags h = .ok ((1 + 2 * 4 + 2 * 16 + 2 * 64), h)
55
56/-- `const char *zError(int err)`.
57Every signed argument returns the public error text as static read-only storage.
58Every heap is unchanged; no allocation, leak or runtime fault is permitted. -/
59def Goal.zError : Prop :=
60  ∀ (h : Heap) (err : Int32), ∃ p,
61    C.run (Zlib.Zutil.zError err) h = .ok (p, h) ∧ StaticString h p (errorText err.toInt)
62
63end ZlibF.Spec.Public