Domains.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.Back
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6/-- Caller storage before init. No library invariant or callee contract is supplied. -/
7def InitDomain (h : Heap) (r : ZStreamRef) (version : BPtr) : Prop :=
8  Fresh h ∧ Zlib.Inflate.Spec.Uniq h ∧ LibraryGlobals h ∧
9  VersionValue h version (some 49) ∧
10  ∃ z, r.get h = some z ∧ DefaultOrNull z ∧ z.state = none
11
12/-- Fixed caller storage for top-level non-emptiness obligations. The window remains caller-owned. -/
13def witnessHeap : Heap :=
14  { Heap.empty with
15    streams := upd Heap.empty.streams 0 (some default)
16    bytes := upd (upd Heap.empty.bytes 1 (some #[49, 0])) 2
17      (some (Array.replicate 32768 0))
18    nextBlk := 3
19    static := Zlib.Crc32.initStatics
20      (Zlib.Inftrees.initStatics (Zlib.Trees.trees_statics Heap.empty.static)) }
21
22/-- Every accepted signed window parameter has a non-failing init on every permitted heap.
23The fixed witness additionally rules out an empty caller domain. -/
24def Goal.inflate_initialisation_domain : Prop :=
25  (∀ h r version wb wrap bits,
26    InitDomain h r version → Api.inflWbits wb.toInt = some (wrap, bits) →
27    h.allocOk h.nalloc = true →
28    ∃ after, C.run (Zlib.Inflate.inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) ∧
29      InflateInitial h after r wrap bits ∧ StreamReachable .inflate after r) ∧
30  InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) ∧
31  (∀ wb wrap bits, Api.inflWbits wb.toInt = some (wrap, bits) →
32    ∃ after, C.run (Zlib.Inflate.inflateInit2_ (some (.tab 0)) wb (.ref (.blk 1) 0) 112)
33      witnessHeap = .ok (Z_OK, after) ∧ InflateInitial witnessHeap after (.tab 0) wrap bits)
34
35/-- Full level, method, window, memory-level and strategy coverage, including normalisation.
36No assumption that the post-init invariant already holds is permitted. -/
37def Goal.deflate_initialisation_domain : Prop :=
38  (∀ h r version level method wb mem strategy p,
39    InitDomain h r version →
40    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
41    (∀ j, j < 5 → h.allocOk (h.nalloc + j) = true) →
42    ∃ after, C.run (Zlib.Deflate.deflateInit2_ (some r) level method wb mem strategy version 112) h =
43      .ok (Z_OK, after) ∧ DeflateInitial h after r p ∧ StreamReachable .deflate after r) ∧
44  InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) ∧
45  (∀ level method wb mem strategy p,
46    Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt = some p →
47    ∃ after, C.run (Zlib.Deflate.deflateInit2_ (some (.tab 0)) level method wb mem strategy
48      (.ref (.blk 1) 0) 112) witnessHeap = .ok (Z_OK, after) ∧
49      DeflateInitial witnessHeap after (.tab 0) p)
50
51/-- All eight documented callback-window sizes, with an arbitrary valid caller window.
52Init establishes the back-decoder invariant and retains ownership of the window. -/
53def Goal.inflate_back_initialisation_domain : Prop :=
54  (∀ h r version wb window,
55    InitDomain h r version → 8 ≤ wb.toInt → wb.toInt ≤ 15 →
56    window ≠ .null → Writable h window (2 ^ wb.toInt.toNat) → h.allocOk h.nalloc = true →
57    ∃ after z s, C.run (Zlib.Infback.inflateBackInit_ (some r) wb window version 112) h =
58      .ok (Z_OK, after) ∧ BackValid after r h.nextBlk z s ∧ s.window = window ∧
59      s.wbits = wb.toUInt32 ∧ Frame h after (StreamRoot r) ∧
60      LiveChange h after (fun b => b = h.nextBlk) (fun _ => False)) ∧
61  InitDomain witnessHeap (.tab 0) (.ref (.blk 1) 0) ∧
62  (∀ wb : Int32, 8 ≤ wb.toInt → wb.toInt ≤ 15 →
63    ∃ after z s, C.run (Zlib.Infback.inflateBackInit_ (some (.tab 0)) wb (.ref (.blk 2) 0)
64      (.ref (.blk 1) 0) 112) witnessHeap = .ok (Z_OK, after) ∧
65      BackValid after (.tab 0) witnessHeap.nextBlk z s ∧ s.window = .ref (.blk 2) 0)
66
67def gzWitnessHeap (mode : List UInt8) : Heap :=
68  { witnessHeap with
69    bytes := upd (upd witnessHeap.bytes 3 (some #[120, 0])) 4 (some (mode ++ [0]).toArray)
70    nextBlk := 5 }
71
72def gzWitnessFs (mode : Api.GzMode) : Fs :=
73  if mode = .read then Fs.put default #[120] #[] else default
74
75/-- External open success is specified by the fixed file-system semantics. No gz contract
76is an assumption. Every accepted mode has a successful concrete open witness. -/
77def Goal.gz_initialisation_domain : Prop :=
78  (∀ h fs path mode name flags kind level strategy direct fd world start,
79    Fresh h → Zlib.Gzlib.Spec.Uniq h → LibraryGlobals h → FileSystem fs →
80    NoAllocationFailure h → CString h path name → CString h mode flags →
81    parsedMode flags = some (kind, level, strategy, direct) →
82    OpenWorld h fs world name flags kind none fd start → fd ≠ -1 →
83    ∃ after fs' i s, Zlib.Gzlib.gzopen path mode fs h = .ok ((some (.in_gzstate_x i), fs'), after) ∧
84      OpenState after i s kind level strategy direct fd name ∧ GzReachable after fs' i ∧
85      Frame h after (fun _ => False) ∧ LiveChange h after (GzOwned after i s) (fun _ => False)) ∧
86  (∀ flags kind level strategy direct, 0 ∉ flags →
87    parsedMode flags = some (kind, level, strategy, direct) →
88    ∃ after fs' i s,
89      Zlib.Gzlib.gzopen (.ref (.blk 3) 0) (.ref (.blk 4) 0) (gzWitnessFs kind) (gzWitnessHeap flags) =
90        .ok ((some (.in_gzstate_x i), fs'), after) ∧
91      OpenState after i s kind level strategy direct s.fd [120] ∧ GzReachable after fs' i)
92
93end ZlibF.Spec.Public