Back.lean

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

1import ZlibF.Spec.Public.GzClose
2
3namespace ZlibF.Spec.Public
4open C Zlib.Infback ZlibF.Spec
5
6def BackValid (h : Heap) (r : ZStreamRef) (i : Nat) (z : ZStream) (s : InflateState) : Prop :=
7  r.get h = some z ∧ h.istates i = some s ∧ z.state = some (.inflate i) ∧
8  z.zalloc = .fn "zcalloc" ∧ z.zfree = .fn "zcfree" ∧ s.WellFormed ∧
9  8 ≤ s.wbits.toNat ∧ s.wbits.toNat ≤ 15 ∧ s.wsize.toNat = 2 ^ s.wbits.toNat ∧
10  s.window ≠ .null ∧ Writable h s.window s.wsize.toNat ∧
11  Fresh h ∧ Zlib.Inflate.Spec.Uniq h ∧ LibraryGlobals h
12
13def backInitialState (garbage : Nat → UInt64) (window : BPtr) (bits : Int32) : InflateState :=
14  { InflateState.garbage garbage with
15    dmax := 32768, wbits := bits.toUInt32, wsize := 1 <<< bits.toUInt32
16    window := window, wnext := 0, whave := 0, sane := 1 }
17
18/-- `int inflateBackInit_(z_streamp strm, int windowBits, unsigned char *window,
19const char *version, int stream_size)`.
20The caller retains the window. Only the state record is allocated; its other integer fields
21remain arbitrary. Refusal precedes allocation, and allocation failure retains the old state field. -/
22def Goal.inflateBackInit_ : Prop :=
23  (∀ h p wb window version head size, VersionValue h version head →
24    (head ≠ some 49 ∨ size ≠ 112) →
25    C.run (Zlib.Infback.inflateBackInit_ p wb window version size) h = .ok (Z_VERSION_ERROR, h)) ∧
26  (∀ h p wb window version, VersionValue h version (some 49) →
27    (p = none ∨ window = .null ∨ wb.toInt < 8 ∨ 15 < wb.toInt) →
28    C.run (Zlib.Infback.inflateBackInit_ p wb window version 112) h = .ok (Z_STREAM_ERROR, h)) ∧
29  (∀ h r z wb window version,
30    Fresh h → Zlib.Inflate.Spec.Uniq h → LibraryGlobals h → r.get h = some z →
31    DefaultOrNull z → VersionValue h version (some 49) →
32    8 ≤ wb.toInt → wb.toInt ≤ 15 → window ≠ .null → Writable h window (2 ^ wb.toInt.toNat) →
33    ∃ rc after,
34      C.run (Zlib.Infback.inflateBackInit_ (some r) wb window version 112) h = .ok (rc, after) ∧
35      after.nalloc = h.nalloc + 1 ∧
36      if h.allocOk h.nalloc = false then
37        rc = Z_MEM_ERROR ∧ SameObjects (r.put h (preparedStream z)) after
38      else rc = Z_OK ∧
39        let z' := { preparedStream z with state := some (.inflate h.nextBlk) }
40        let s := backInitialState (h.garbage h.nalloc) window wb
41        BackValid after r h.nextBlk z' s ∧
42        Frame h after (StreamRoot r) ∧
43        LiveChange h after (fun b => b = h.nextBlk) (fun _ => False))
44
45structure BackLog where
46  supplied : List UInt8
47  chunks : List (List UInt8)
48  active : BPtr
49  held : List UInt8
50  exhausted : Bool := false
51  failed : Bool := false
52
53/-- Caller callbacks may allocate, free, and update any of their own objects, including records. -/
54def ExternalFrame (own : Nat → Prop) (h after : Heap) : Prop :=
55  Frame h after own ∧ Fresh after ∧ Zlib.Inflate.Spec.Uniq after ∧
56  (∀ b, ¬ h.live b → after.live b → own b)
57
58def ExternalAgreement (own : Nat → Prop) (h after : Heap) : Prop :=
59  h.nextBlk = after.nextBlk ∧ h.nalloc = after.nalloc ∧ h.allocOk = after.allocOk ∧
60  h.garbage = after.garbage ∧ h.static = after.static ∧
61  ∀ b, own b → h.bytes b = after.bytes b ∧ h.words b = after.words b ∧
62    h.streams b = after.streams b ∧ h.gzheaders b = after.gzheaders b ∧
63    h.dstates b = after.dstates b ∧ h.istates b = after.istates b ∧
64    h.gzstates b = after.gzstates b ∧ h.ro b = after.ro b
65
66/-- Hide only the window slice when comparing a callback's private state. A descriptor can
67share the allocation while using bytes outside that slice. -/
68def restoreWindow (before after : Heap) (window : BPtr) (capacity : Nat) : Heap :=
69  match window with
70  | .null => after
71  | .ref r off => match Space.get before r, Space.get after r with
72    | some old, some current => Space.put after r
73        (current.extract 0 off ++ old.extract off (off + capacity) ++
74          current.extract (off + capacity) current.size)
75    | _, _ => after
76
77def CallbackFrame (own : Nat → Prop) (h after : Heap) (r : ZStreamRef) (state : Nat)
78    (window : BPtr) (capacity : Nat) : Prop :=
79  Frame h after (fun b => StreamRoot r b ∨ b = state ∨ own b ∨ ByteRoot window b) ∧
80  ((∀ b, ByteRoot window b → ¬ own b) →
81    BufferFrame h after (fun b => StreamRoot r b ∨ b = state ∨ own b) [⟨window, capacity⟩])
82
83/-- These are contracts of caller code, not assumed library callee contracts.
84The input may depend on previous output. A finite source has an explicit total-input bound.
85Output must preserve the current input until the next input callback. -/
86structure CallbackProtocol (r : ZStreamRef) (state : Nat) (window : BPtr) (capacity : Nat)
87    (input : InCb) (inDesc : BPtr) (output : OutCb) (outDesc : BPtr) where
88  own : Nat → Prop
89  invariant : Heap → BackLog → Prop
90  inputBound : Nat
91  disjoint : (¬ own state) ∧ (∀ b, StreamRoot r b → ¬ own b)
92  local_ : ∀ h after log, ExternalAgreement own h (restoreWindow h after window capacity) →
93    (invariant h log ↔ invariant after log)
94  bounded : ∀ h log, invariant h log → log.supplied.length ≤ inputBound
95  liveInput : ∀ h log, invariant h log → log.held ≠ [] → Bytes h log.active log.held.length log.held
96  inStep : ∀ h log next, invariant h log → ∃ n pointer after bytes,
97    input inDesc next h = .ok ((n, pointer), after) ∧
98    bytes.length = n.toNat ∧ ExternalFrame own h after ∧
99    SameBytePrefix h after window window capacity ∧
100    (n ≠ 0 → Bytes after pointer n.toNat bytes ∧ Separate pointer n.toNat window capacity ∧
101      ∀ b, ByteRoot pointer b → b ≠ state ∧ ¬ StreamRoot r b) ∧
102    invariant after { log with
103      supplied := log.supplied ++ bytes, active := pointer, held := bytes, exhausted := n == 0 }
104  outStep : ∀ h log pointer n bytes, invariant h log →
105    Bytes h pointer n.toNat bytes → n.toNat ≤ capacity →
106    ∃ rc after, output outDesc pointer n h = .ok (rc, after) ∧ ExternalFrame own h after ∧
107      SameBytePrefix h after window window capacity ∧
108      (log.held ≠ [] → Bytes after log.active log.held.length log.held) ∧
109      invariant after { log with chunks := log.chunks ++ [bytes], failed := log.failed || rc != 0 }
110
111/-- `int inflateBack(z_streamp strm, in_func in, void *in_desc, out_func out, void *out_desc)`.
112For every finite, returning caller protocol, decode raw DEFLATE and deliver the chunks through
113that actual output callback. The protocol's observation relation records the bytes delivered.
114No allocation or free by the library is charged to the caller's callbacks. -/
115def Goal.inflateBack : Prop :=
116  (∀ h input inDesc output outDesc,
117    C.run (Zlib.Infback.inflateBack none input inDesc output outDesc) h = .ok (Z_STREAM_ERROR, h)) ∧
118  (∀ h r i z s input inDesc output outDesc
119      (protocol : CallbackProtocol r i s.window s.wsize.toNat input inDesc output outDesc) first,
120    BackValid h r i z s →
121    (if z.next_in = .null then first = [] else Bytes h z.next_in z.avail_in.toNat first) →
122    Separate z.next_in first.length s.window s.wsize.toNat →
123    protocol.invariant h { supplied := first, chunks := [], active := z.next_in, held := first } →
124    ∃ rc after z' s' log unused consumed,
125      C.run (Zlib.Infback.inflateBack (some r) input inDesc output outDesc) h = .ok (rc, after) ∧
126      BackValid after r i z' s' ∧ s'.window = s.window ∧ s'.wsize = s.wsize ∧
127      protocol.invariant after log ∧
128      (rc = Z_STREAM_END ∨ rc = Z_DATA_ERROR ∨ rc = Z_BUF_ERROR) ∧
129      consumed ++ unused = log.supplied ∧ unused.length = z'.avail_in.toNat ∧
130      unused <:+ log.held ∧
131      (log.exhausted = true → z'.next_in = .null ∧ unused = []) ∧
132      (log.exhausted = false → z'.next_in = advance log.active (log.held.length - unused.length)) ∧
133      (∀ chunk, chunk ∈ log.chunks → chunk ≠ [] ∧ chunk.length ≤ s.wsize.toNat) ∧
134      (rc = Z_STREAM_END → Deflate.Decodes [] consumed log.chunks.flatten ∧ log.failed = false) ∧
135      (rc = Z_BUF_ERROR → log.exhausted = true ∨ log.failed = true) ∧
136      z'.total_in = z.total_in ∧ z'.total_out = z.total_out ∧ z'.adler = z.adler ∧
137      CallbackFrame protocol.own h after r i s.window s.wsize.toNat ∧
138      (∀ b, ¬ protocol.own b → (after.live b ↔ h.live b)))
139
140/-- `int inflateBackEnd(z_streamp strm)`.
141Free only the state record. The caller's window is retained, even when it is a slice of another object. -/
142def Goal.inflateBackEnd : Prop :=
143  (∀ h, C.run (Zlib.Infback.inflateBackEnd none) h = .ok (Z_STREAM_ERROR, h)) ∧
144  (∀ h r z, r.get h = some z → z.state = none ∨ z.zfree = .null →
145    C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_STREAM_ERROR, h)) ∧
146  (∀ h r i z s, BackValid h r i z s →
147    ∃ after, C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_OK, after) ∧
148      r.get after = some { z with state := none } ∧
149      LiveChange h after (fun _ => False) (fun b => b = i) ∧
150      Frame h after (fun b => StreamRoot r b ∨ b = i) ∧
151      after.nalloc = h.nalloc ∧ after.nextBlk = h.nextBlk)
152
153end ZlibF.Spec.Public