History.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Public.Lifecycle
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6inductive StreamKind where
7  | inflate | deflate
8  deriving DecidableEq
9
10/-- Ownership is read from the actual state graph, not chosen by a proof. -/
11def StreamOwned (h : Heap) (r : ZStreamRef) (b : Nat) : Prop :=
12  ∃ z, r.get h = some z ∧
13    ((∃ i s, z.state = some (.inflate i) ∧ h.istates i = some s ∧ InflateOwned i s b) ∨
14     (∃ i s, z.state = some (.deflate i) ∧ h.dstates i = some s ∧ DeflateOwned i s b))
15
16def ByteRoot : BPtr → Nat → Prop
17  | .ref (.blk i) _, b | .ref (.dstate_depth i) _, b => b = i
18  | _, _ => False
19
20def CallerRange (h : Heap) (r : ZStreamRef) (p : BPtr) (n : Nat) (write : Bool) : Prop :=
21  p = .null ∨ ((∃ xs, Bytes h p n xs) ∧ (write = true → Writable h p n) ∧
22    ∀ b, ByteRoot p b → ¬ StreamOwned h r b)
23
24def StreamBuffers (h : Heap) (r : ZStreamRef) : Prop :=
25  ∃ z, r.get h = some z ∧
26    CallerRange h r z.next_in z.avail_in.toNat false ∧
27    CallerRange h r z.next_out z.avail_out.toNat true ∧
28    Separate z.next_in z.avail_in.toNat z.next_out z.avail_out.toNat
29
30def CString (h : Heap) (p : BPtr) (xs : List UInt8) : Prop :=
31  Bytes h p (xs.length + 1) (xs ++ [0]) ∧ 0 ∉ xs ∧ xs.length < 2 ^ 64
32
33def HeaderMemory (h : Heap) (r : ZStreamRef) (p : GzHeaderPtr) (writing : Bool) : Prop :=
34  p = none ∨ ∃ i g, p = some (.tab i) ∧ h.gzheaders i = some g ∧
35    ¬ StreamOwned h r i ∧
36    (g.extra ≠ .null → CallerRange h r g.extra
37      (if writing then g.extra_max.toNat else g.extra_len.toNat) writing) ∧
38    (g.name ≠ .null → if writing then CallerRange h r g.name g.name_max.toNat true
39      else ∃ xs, CString h g.name xs) ∧
40    (g.comment ≠ .null → if writing then CallerRange h r g.comment g.comm_max.toNat true
41      else ∃ xs, CString h g.comment xs)
42
43def ActiveHeader (h : Heap) (r : ZStreamRef) : Prop :=
44  ∃ z, r.get h = some z ∧
45    (∀ i s, z.state = some (.inflate i) → h.istates i = some s → HeaderMemory h r s.head true) ∧
46    (∀ i s, z.state = some (.deflate i) → h.dstates i = some s → HeaderMemory h r s.gzhead false)
47
48/-- Caller edits may replace input and output bindings and change unowned allocations.
49They preserve the stream's control fields, private state, window and registered allocations. -/
50def Rebuffer (h after : Heap) (r : ZStreamRef) : Prop :=
51  Fresh after ∧ Zlib.Inflate.Spec.Uniq after ∧ LibraryGlobals after ∧
52  Frame h after (fun b => ¬ StreamOwned h r b) ∧
53  ∃ z z', r.get h = some z ∧ r.get after = some z' ∧
54    z' = { z with
55      next_in := z'.next_in, avail_in := z'.avail_in
56      next_out := z'.next_out, avail_out := z'.avail_out }
57
58/-- Exactly the public operations belonging to an existing stream. -/
59def StreamOperation (kind : StreamKind) (r : ZStreamRef) : Call → Prop
60  | .inflate p _ | .inflateReset p | .inflateReset2 p _ | .inflateResetKeep p
61  | .inflatePrime p _ _ | .inflateGetDictionary p _ _ | .inflateSetDictionary p _ _
62  | .inflateGetHeader p _ | .inflateSync p | .inflateSyncPoint p | .inflateMark p
63  | .inflateCodesUsed p | .inflateValidate p _ | .inflateUndermine p _ =>
64      kind = .inflate ∧ p = some r
65  | .deflate p _ | .deflateReset p | .deflateResetKeep p | .deflateParams p _ _
66  | .deflatePrime p _ _ | .deflateGetDictionary p _ _ | .deflateSetDictionary p _ _
67  | .deflateSetHeader p _ | .deflateTune p _ _ _ _ | .deflatePending p _ _
68  | .deflateUsed p _ | .deflateBound p _ | .deflateBound_z p _ =>
69      kind = .deflate ∧ p = some r
70  | _ => False
71
72def StreamArguments (h : Heap) (r : ZStreamRef) : Call → Prop
73  | .inflate _ _ | .deflate _ _ | .deflateParams _ _ _ => StreamBuffers h r ∧ ActiveHeader h r
74  | .inflateSync _ => ∃ z, r.get h = some z ∧ CallerRange h r z.next_in z.avail_in.toNat false
75  | .inflateSetDictionary _ p n | .deflateSetDictionary _ p n => CallerRange h r p n.toNat false
76  | .inflateGetDictionary _ p _ => ∃ z i s,
77      r.get h = some z ∧ z.state = some (.inflate i) ∧ h.istates i = some s ∧
78      CallerRange h r p s.whave.toNat true
79  | .deflateGetDictionary _ p _ => ∃ z i s,
80      r.get h = some z ∧ z.state = some (.deflate i) ∧ h.dstates i = some s ∧
81      CallerRange h r p (min s.w_size.toNat (s.strstart.toNat + s.lookahead.toNat)) true
82  | .inflateGetHeader _ p => HeaderMemory h r p true ∧ p ≠ none
83  | .deflateSetHeader _ p => HeaderMemory h r p false
84  | .deflateBound _ _ | .deflateBound_z _ _ => ActiveHeader h r
85  | _ => True
86
87/-- Actual successful histories, with no specification assumed for an earlier call.
88The init targets separately prove that valid, non-failing initialisation produces such a history. -/
89inductive StreamReachable : StreamKind → Heap → ZStreamRef → Prop
90  | inflateInit {h after r z version wb} :
91      Fresh h → Zlib.Inflate.Spec.Uniq h → LibraryGlobals h → r.get h = some z →
92      DefaultOrNull z → VersionValue h version (some 49) →
93      C.run (Zlib.Inflate.inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) →
94      StreamReachable .inflate after r
95  | deflateInit {h after r z version level method wb mem strategy} :
96      Fresh h → Zlib.Deflate.Spec.Uniq h → LibraryGlobals h → r.get h = some z →
97      DefaultOrNull z → VersionValue h version (some 49) →
98      C.run (Zlib.Deflate.deflateInit2_ (some r) level method wb mem strategy version 112) h = .ok (Z_OK, after) →
99      StreamReachable .deflate after r
100  | rebuffer {kind h after r} : StreamReachable kind h r → Rebuffer h after r →
101      StreamReachable kind after r
102  | step {kind h after r call value} : StreamReachable kind h r →
103      StreamOperation kind r call → StreamArguments h r call →
104      call.execute default h = .ok ((value, default), after) → StreamReachable kind after r
105  | inflateCopy {h after source dest z} : StreamReachable .inflate h source →
106      source ≠ dest → dest.get h = some z →
107      C.run (Zlib.Inflate.inflateCopy (some dest) (some source)) h = .ok (Z_OK, after) →
108      StreamReachable .inflate after dest
109  | deflateCopy {h after source dest z} : StreamReachable .deflate h source →
110      source ≠ dest → dest.get h = some z →
111      C.run (Zlib.Deflate.deflateCopy (some dest) (some source)) h = .ok (Z_OK, after) →
112      StreamReachable .deflate after dest
113
114structure Region where
115  pointer : BPtr
116  length : Nat
117
118def Region.covers (region : Region) (r : BRef) (i : Nat) : Prop :=
119  ∃ off, region.pointer = .ref r off ∧ off ≤ i ∧ i < off + region.length
120
121/-- Restore only the caller's byte-array fields, leaving all other fields available to the frame check. -/
122def restoreRegions (before after : Heap) (regions : List Region) : Heap :=
123  regions.foldl (fun current region => match region.pointer with
124    | .null => current
125    | .ref r _ => match Space.get before r with
126      | none => current
127      | some a => Space.put current r a) after
128
129def BufferFrame (before after : Heap) (changed : Nat → Prop) (regions : List Region) : Prop :=
130  Frame before (restoreRegions before after regions) changed ∧
131  ∀ region, region ∈ regions → ∀ r off a,
132    region.pointer = .ref r off → Space.get before r = some a →
133    ∃ a', Space.get after r = some a' ∧ a'.size = a.size ∧
134      ∀ j, j < a.size → (¬ ∃ region', region' ∈ regions ∧ region'.covers r j) → a'[j]? = a[j]?
135
136def HeaderRegions (h : Heap) (head : GzHeaderPtr) : List Region :=
137  match head with
138  | none => []
139  | some (.tab i) => match h.gzheaders i with
140    | none => []
141    | some g => [⟨g.extra, g.extra_max.toNat⟩, ⟨g.name, g.name_max.toNat⟩, ⟨g.comment, g.comm_max.toNat⟩]
142
143end ZlibF.Spec.Public