GzState.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.Copy
2import ZlibF.Proof.«gzlib.c.base»
3import ZlibF.Spec.Api.Gz
4
5namespace ZlibF.Spec.Public
6open C Zlib.GzFs ZlibF.Spec
7
8def FileSystem (fs : Fs) : Prop :=
9  fs.fsizeLimit ≤ 2 ^ 63 - 1 ∧
10  (∀ path node, (path, node) ∈ fs.names.toList → node < fs.nodes.size) ∧
11  (∀ (i : Nat) (file : OFile), fs.fds[i]? = some (some file) → file.node < fs.nodes.size ∧
12    file.pos ≤ 2 ^ 63 - 1 ∧ (∀ node : Node, fs.nodes[file.node]? = some node → node.isDir = true → file.wr = false)) ∧
13  (∀ (i : Nat) (node : Node), fs.nodes[i]? = some node → node.data.size ≤ 2 ^ 63 - 1)
14
15def GzOwned (h : Heap) (i : Nat) (s : GzState) (b : Nat) : Prop :=
16  b = i ∨ s.path = .ref (.blk b) 0 ∨ s.msg = .ref (.blk b) 0 ∨
17  (s.size ≠ 0 ∧ (s.in = .ref (.blk b) 0 ∨
18    ((s.mode = GZ_READ ∨ s.direct = 0) ∧
19      (s.out = .ref (.blk b) 0 ∨ StreamOwned h (.in_gzstate_strm i) b))))
20
21def MallocBuffer (h : Heap) (p : BPtr) (n : Nat) : Prop :=
22  ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false ∧ n ≤ a.size
23
24/-- Buffer fields may dangle after a failed lazy allocation. They are inactive when size is
25zero and must be overwritten before reuse. Nonempty cached output must remain privately owned. -/
26def GzValid (h : Heap) (i : Nat) (s : GzState) : Prop :=
27  h.gzstates i = some s ∧ (s.mode = GZ_READ ∨ s.mode = GZ_WRITE) ∧
28  Fresh h ∧ Zlib.Gzlib.Spec.Uniq h ∧ LibraryGlobals h ∧
29  (∃ path, CString h s.path path ∧ MallocBuffer h s.path (path.length + 1)) ∧
30  (s.msg = .null ∨ ∃ message, CString h s.msg message ∧ MallocBuffer h s.msg (message.length + 1)) ∧
31  (s.err = Z_MEM_ERROR → s.msg = .null) ∧ 8 ≤ s.want.toNat ∧ s.want.toNat < 2 ^ 31 ∧
32  (s.size ≠ 0 → s.size = s.want ∧
33    MallocBuffer h s.in (if s.mode = GZ_READ then s.size.toNat else 2 * s.size.toNat) ∧
34    (s.mode = GZ_READ ∨ s.direct = 0 →
35      MallocBuffer h s.out (if s.mode = GZ_READ then 2 * s.size.toNat else s.size.toNat))) ∧
36  (s.x.have ≠ 0 → (∃ xs, Bytes h s.x.next s.x.have.toNat xs) ∧
37    ∀ b, ByteRoot s.x.next b → GzOwned h i s b)
38
39def GzRange (h : Heap) (i : Nat) (s : GzState) (p : BPtr) (n : Nat) (write : Bool) : Prop :=
40  n = 0 ∨ ((∃ xs, Bytes h p n xs) ∧ (write = true → Writable h p n) ∧
41    ∀ b, ByteRoot p b → ¬ GzOwned h i s b)
42
43def Formatted (h : Heap) (format : BPtr) (args : List VaArg) (xs : List UInt8) : Prop :=
44  ∃ fmt, CString h format fmt ∧
45    Zlib.GzFs.formatGo fmt.toArray (Zlib.GzFs.heapStr h) (fmt.length + 1) 0 args #[] = .ok xs.toArray
46
47def GzOperation (i : Nat) : Call → Prop
48  | .gzbuffer p _ | .gzclearerr p | .gzdirect p | .gzeof p | .gzerror p _
49  | .gzflush p _ | .gzgetc p | .gzgetc_ p | .gzgets p _ _ | .gzoffset p | .gzoffset64 p
50  | .gzprintf p _ _ | .gzputc p _ | .gzputs p _ | .gzread p _ _ | .gzrewind p
51  | .gzseek p _ _ | .gzseek64 p _ _ | .gzsetparams p _ _ | .gztell p | .gztell64 p
52  | .gzvprintf p _ _ | .gzwrite p _ _ | .gzungetc _ p | .gzfread _ _ _ p | .gzfwrite _ _ _ p =>
53      p = some (.in_gzstate_x i)
54  | _ => False
55
56def GzArguments (h : Heap) (i : Nat) (s : GzState) : Call → Prop
57  | .gzread _ p n =>
58      if n.toNat ≥ 2 ^ 31 then True else GzRange h i s p n.toNat true
59  | .gzwrite _ p n =>
60      if n.toNat ≥ 2 ^ 31 then True else GzRange h i s p n.toNat false
61  | .gzfread p size n _ =>
62      if size.toNat * n.toNat ≥ 2 ^ 64 then True else GzRange h i s p (size.toNat * n.toNat) true
63  | .gzfwrite p size n _ =>
64      if size.toNat * n.toNat ≥ 2 ^ 64 then True else GzRange h i s p (size.toNat * n.toNat) false
65  | .gzgets _ p n => if n.toInt < 1 ∨ p = .null then True else GzRange h i s p n.toInt.toNat true
66  | .gzputs _ p => ∃ xs, CString h p xs ∧ GzRange h i s p (xs.length + 1) false
67  | .gzprintf _ p args | .gzvprintf _ p args => ∃ xs, Formatted h p args xs
68  | .gzerror _ p => p = .null ∨ GzRange h i s p 4 true
69  | _ => True
70
71def GzCallerFrame (h after : Heap) (i : Nat) (s : GzState) : Prop :=
72  Fresh after ∧ Zlib.Gzlib.Spec.Uniq after ∧ LibraryGlobals after ∧
73  Frame h after (fun b => ¬ GzOwned h i s b)
74
75/-- Actual public histories. No earlier library contract is an assumption.
76Appending input after EOF is admitted explicitly, as required by `gzclearerr`. -/
77inductive GzReachable : Heap → Fs → Nat → Prop
78  | open {h after fs fs' path mode i name flags} :
79      Fresh h → Zlib.Gzlib.Spec.Uniq h → LibraryGlobals h → FileSystem fs →
80      CString h path name → CString h mode flags →
81      Zlib.Gzlib.gzopen path mode fs h = .ok ((some (.in_gzstate_x i), fs'), after) →
82      GzReachable after fs' i
83  | dopen {h after fs fs' fd mode i flags} :
84      Fresh h → Zlib.Gzlib.Spec.Uniq h → LibraryGlobals h → FileSystem fs →
85      CString h mode flags →
86      Zlib.Gzlib.gzdopen fd mode fs h = .ok ((some (.in_gzstate_x i), fs'), after) →
87      GzReachable after fs' i
88  | step {h after fs fs' i s call value} : GzReachable h fs i → h.gzstates i = some s →
89      GzOperation i call → GzArguments h i s call →
90      call.execute fs h = .ok ((value, fs'), after) → GzReachable after fs' i
91  | caller {h after fs i s} : GzReachable h fs i → h.gzstates i = some s →
92      GzCallerFrame h after i s → GzReachable after fs i
93  | append {h fs fs' i s file old new extra} : GzReachable h fs i →
94      h.gzstates i = some s → s.mode = GZ_READ →
95      fs.fds[s.fd.toInt.toNat]? = some (some file) →
96      fs.nodes[file.node]? = some old → new = { old with data := old.data ++ extra } →
97      fs' = { fs with nodes := fs.nodes.set! file.node new } → FileSystem fs' →
98      GzReachable h fs' i
99
100def GzStateFrame (before after : Heap) (fs fs' : Fs) (i : Nat) (s s' : GzState)
101    (regions : List Region) : Prop :=
102  GzValid after i s' ∧ s'.mode = s.mode ∧ s'.fd = s.fd ∧ s'.path = s.path ∧
103  FileSystem fs' ∧ fs'.names = fs.names ∧ fs'.fsizeLimit = fs.fsizeLimit ∧
104  fs'.fds.size = fs.fds.size ∧ fs'.nodes.size = fs.nodes.size ∧
105  (∀ j, j ≠ s.fd.toInt.toNat → fs'.fds[j]? = fs.fds[j]?) ∧
106  (∀ file j, fs.fds[s.fd.toInt.toNat]? = some (some file) → j ≠ file.node →
107    fs'.nodes[j]? = fs.nodes[j]?) ∧
108  BufferFrame before after (GzOwned before i s) regions ∧
109  LiveChange before after
110    (fun b => GzOwned after i s' b ∧ ¬ before.live b)
111    (fun b => GzOwned before i s b ∧ ¬ GzOwned after i s' b)
112
113def gzipMagic (xs : List UInt8) : Prop := xs.take 2 = [31, 139]
114
115inductive GzipMembers : List UInt8 → List UInt8 → Prop
116  | empty : GzipMembers [] []
117  | member {compressed decoded rest output} : Gzip.Decodes compressed decoded →
118      GzipMembers rest output → GzipMembers (compressed ++ rest) (decoded ++ output)
119
120/-- Normal transparent input, or gzip members with an optional non-gzip tail.
121The pinned source uses four consistent bytes for its initial auto-detection. Later members
122are passed straight to inflate, so a two-byte magic check is used only for the tail clause. -/
123def GzData (s : GzState) (raw decoded : List UInt8) : Prop :=
124  (s.direct = 1 ∧ ¬ Api.GzLooksGzip raw ∧ decoded = raw) ∨
125  ∃ members tail, members ≠ [] ∧ raw = members ++ tail ∧ ¬ gzipMagic tail ∧ GzipMembers members decoded
126
127def FileData (fs : Fs) (s : GzState) (decoded : List UInt8) : Prop :=
128  ∃ file node, 0 ≤ s.fd.toInt ∧ fs.fds[s.fd.toInt.toNat]? = some (some file) ∧
129    file.rd = true ∧ fs.nodes[file.node]? = some node ∧ node.isDir = false ∧
130    GzData s (node.data.toList.drop s.start.toInt.toNat) decoded
131
132def Buffered (h : Heap) (s : GzState) (bytes : List UInt8) : Prop :=
133  if s.x.have = 0 then bytes = [] else Bytes h s.x.next s.x.have.toNat bytes
134
135def availableRead (s : GzState) (buffered decoded : List UInt8) : List UInt8 :=
136  (buffered ++ (if s.eof ≠ 0 ∧ s.strm.avail_in = 0 then [] else
137    decoded.drop (s.x.pos.toInt + (buffered.length : Int)).toNat)).drop s.skip.toInt.toNat
138
139def NoAllocationFailure (h : Heap) : Prop := ∀ n, h.allocOk n = true
140
141end ZlibF.Spec.Public