Lifecycle.lean

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

1import ZlibF.Spec.Public.Initialisation
2
3namespace ZlibF.Spec.Public
4open C ZlibF.Spec
5
6def inflateResetState (i : Nat) (s : InflateState) : InflateState :=
7  { s with
8    total := 0, mode := HEAD, last := 0, havedict := 0, flags := -1, dmax := 32768
9    head := none, hold := 0, bits := 0
10    lencode := .ref (.istate_codes i) 0, distcode := .ref (.istate_codes i) 0
11    next := .ref (.istate_codes i) 0, sane := 1, back := -1 }
12
13def inflateResetStream (z : ZStream) (s : InflateState) : ZStream :=
14  { z with
15    total_in := 0, total_out := 0, msg := .null, data_type := 0
16    adler := if s.wrap = 0 then z.adler else (s.wrap &&& 1).toInt64.toUInt64 }
17
18/-- `int inflateResetKeep(z_streamp strm)`.
19Clear decode progress and counters; retain the allocated window and its dictionary. -/
20def Goal.inflateResetKeep : Prop :=
21  ∀ h r i z s, InflateView h r i z s →
22    C.run (Zlib.Inflate.inflateResetKeep (some r)) h = .ok (Z_OK,
23      putInflate (r.put h (inflateResetStream z s)) i (inflateResetState i s))
24
25def inflateResetPre (s : InflateState) : InflateState :=
26  { s with
27    window := if s.wbits = s.reqbits then s.window else .null
28    wbits := s.reqbits, wrap := s.reqwrap, wsize := 0, whave := 0, wnext := 0 }
29
30/-- `int inflateReset(z_streamp strm)`.
31Restore the requested wrapper and window, forget the dictionary, and free an obsolete window. -/
32def Goal.inflateReset : Prop :=
33  ∀ h r i z s, InflateView h r i z s → z.zfree = .fn "zcfree" →
34    WindowAllocation h s.window →
35    let base := if s.wbits = s.reqbits then h else dropWindow h s.window
36    let reset := inflateResetPre s
37    C.run (Zlib.Inflate.inflateReset (some r)) h = .ok (Z_OK,
38      putInflate (r.put base (inflateResetStream z reset)) i (inflateResetState i reset))
39
40/-- `int inflateReset2(z_streamp strm, int windowBits)`.
41Invalid parameters leave the heap unchanged. A changed window size releases the old window.
42The new request restores validation even if `inflateValidate` previously disabled it. -/
43def Goal.inflateReset2 : Prop :=
44  ∀ h r i z s wb, InflateView h r i z s → z.zfree = .fn "zcfree" →
45    WindowAllocation h s.window →
46    C.run (Zlib.Inflate.inflateReset2 (some r) wb) h =
47      match Api.inflWbits wb.toInt with
48      | none => .ok (Z_STREAM_ERROR, h)
49      | some (wrap, bits) =>
50        let w : Int32 := match wrap with | .raw => 0 | .zlib => 5 | .gzip => 6 | .auto => 7
51        let base := if s.wbits.toNat = bits then h else dropWindow h s.window
52        let reset := { s with
53          window := if s.wbits.toNat = bits then s.window else .null
54          reqbits := UInt32.ofNat bits, wbits := UInt32.ofNat bits
55          wrap := w, reqwrap := w, wsize := 0, whave := 0, wnext := 0 }
56        .ok (Z_OK, putInflate (r.put base (inflateResetStream z reset)) i (inflateResetState i reset))
57
58/-- `int inflateEnd(z_streamp strm)`.
59Release exactly the state and its optional window; retain caller buffers and clear `state`. -/
60def Goal.inflateEnd : Prop :=
61  ∀ h r i z s, Zlib.Inflate.Spec.Good h r i z s → z.zfree = .fn "zcfree" →
62    ∃ after, C.run (Zlib.Inflate.inflateEnd (some r)) h = .ok (Z_OK, after) ∧
63      r.get after = some { z with state := none } ∧
64      LiveChange h after (fun _ => False) (InflateOwned i s) ∧
65      Frame h after (fun b => StreamRoot r b ∨ InflateOwned i s b) ∧
66      after.nalloc = h.nalloc ∧ after.nextBlk = h.nextBlk
67
68def InflateDictionary (h : Heap) (s : InflateState) (xs : List UInt8) : Prop :=
69  (s.whave = 0 ∧ xs = []) ∨ ∃ r off a,
70    s.window = .ref r off ∧ Space.get h r = some a ∧
71    off + s.wsize.toNat ≤ a.size ∧
72    xs = ((a.toList.drop (off + s.wnext.toNat)).take (s.whave - s.wnext).toNat ++
73          (a.toList.drop off).take s.wnext.toNat)
74
75/-- `int inflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`.
76Return the chronological window, optionally copy it, and preserve an omitted length cell. -/
77def Goal.inflateGetDictionary : Prop :=
78  ∀ h r i z s dest oldLength xs,
79    Zlib.Inflate.Spec.Good h r i z s → InflateDictionary h s xs →
80    (dest ≠ .null → Writable h dest xs.length ∧ Separate dest xs.length s.window s.wsize.toNat) →
81    ∃ after, C.run (Zlib.Inflate.inflateGetDictionary (some r) dest oldLength) h =
82      .ok ((Z_OK, oldLength.map (fun _ => UInt32.ofNat xs.length)), after) ∧
83      Store h dest (if dest = .null then [] else xs) after
84
85/-- `int inflateGetHeader(z_streamp strm, gz_headerp head)`.
86Only gzip-capable wrappers accept the header. Set `done` to zero and retain all other fields. -/
87def Goal.inflateGetHeader : Prop :=
88  ∀ h r i z s head, InflateView h r i z s →
89    ((s.wrap &&& 2) ≠ 0 → ∃ g gh, head = some (.tab g) ∧ h.gzheaders g = some gh) →
90    ∃ rc after, C.run (Zlib.Inflate.inflateGetHeader (some r) head) h = .ok (rc, after) ∧
91      (if (s.wrap &&& 2) = 0 then rc = Z_STREAM_ERROR ∧ after = h
92       else ∃ g gh, head = some (.tab g) ∧ h.gzheaders g = some gh ∧ rc = Z_OK ∧
93         after = { putInflate h i { s with head := head } with
94           gzheaders := upd h.gzheaders g (some { gh with done := 0 }) })
95
96def DeflateDictionary (h : Heap) (s : DeflateState) (xs : List UInt8) : Prop :=
97  ∃ r off a, s.window = .ref r off ∧ Space.get h r = some a ∧
98    off + s.strstart.toNat + s.lookahead.toNat ≤ a.size ∧
99    xs = (a.toList.drop (off + s.strstart.toNat + s.lookahead.toNat -
100      min s.w_size.toNat (s.strstart.toNat + s.lookahead.toNat))).take
101      (min s.w_size.toNat (s.strstart.toNat + s.lookahead.toNat))
102
103/-- `int deflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`.
104Return the last window of accepted input, including pending lookahead. -/
105def Goal.deflateGetDictionary : Prop :=
106  ∀ h r i z s dest lengthPresent xs,
107    Zlib.Deflate.Spec.DGood h r i z s → DeflateDictionary h s xs →
108    (dest ≠ .null → Writable h dest xs.length ∧ Separate dest xs.length s.window s.window_size.toNat) →
109    ∃ after, C.run (Zlib.Deflate.deflateGetDictionary (some r) dest lengthPresent) h =
110      .ok ((Z_OK, if lengthPresent then some (UInt32.ofNat xs.length) else none), after) ∧
111      Store h dest (if dest = .null then [] else xs) after
112
113/-- `int deflateEnd(z_streamp strm)`.
114Free all five owned blocks. An unfinished busy stream returns `Z_DATA_ERROR` after freeing. -/
115def Goal.deflateEnd : Prop :=
116  ∀ h r i z s, Zlib.Deflate.Spec.DGood h r i z s → z.zfree = .fn "zcfree" →
117    ∃ after, C.run (Zlib.Deflate.deflateEnd (some r)) h =
118      .ok ((if s.status = BUSY_STATE then Z_DATA_ERROR else Z_OK), after) ∧
119      r.get after = some { z with state := none } ∧
120      LiveChange h after (fun _ => False) (DeflateOwned i s) ∧
121      Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) ∧
122      after.nalloc = h.nalloc ∧ after.nextBlk = h.nextBlk
123
124def DeflateResetContract (program : ZStreamPtr → M Int32) (keep : Bool) : Prop :=
125  ∀ h r i z s, Zlib.Deflate.Spec.DGood h r i z s →
126    ∃ after z' s', C.run (program (some r)) h = .ok (Z_OK, after) ∧
127      Zlib.Deflate.Spec.DGood after r i z' s' ∧
128      z' = { z with
129        total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN
130        adler := if s.wrap = 2 ∨ s.wrap = -2 then 0 else 1 } ∧
131      s'.wrap.toInt = s.wrap.toInt.natAbs ∧ s'.pending = 0 ∧ s'.pending_out = s.pending_buf ∧
132      s'.last_flush = -2 ∧ s'.gzhead = none ∧ s'.lookahead = 0 ∧
133      s'.bi_valid = 0 ∧ s'.bi_buf = 0 ∧ s'.bi_used = 0 ∧
134      s'.level = s.level ∧ s'.strategy = s.strategy ∧
135      s'.window = s.window ∧ s'.head = s.head ∧ s'.prev = s.prev ∧ s'.pending_buf = s.pending_buf ∧
136      after.bytes = h.bytes ∧
137      (keep = true → s'.strstart = s.strstart ∧ s'.block_start = s.strstart.toUInt64.toInt64 ∧
138        after.words = h.words) ∧
139      (keep = false → s'.strstart = 0 ∧ s'.block_start = 0 ∧ s'.insert = 0 ∧ s'.ins_h = 0 ∧
140        ∀ ref off a, s.head = .ref ref off → Space.get after ref = some a →
141          ∀ j, j < s.hash_size.toNat → a[off + j]? = some 0) ∧
142      Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) ∧
143      LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc
144
145/-- `int deflateResetKeep(z_streamp strm)`; reset progress while retaining the match history. -/
146def Goal.deflateResetKeep : Prop := DeflateResetContract Zlib.Deflate.deflateResetKeep true
147
148/-- `int deflateReset(z_streamp strm)`; reset progress and clear the dictionary hash. -/
149def Goal.deflateReset : Prop := DeflateResetContract Zlib.Deflate.deflateReset false
150
151/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`.
152Raw streams append to their window. Wrapped streams require DICT mode and the exact Adler id. -/
153def Goal.inflateSetDictionary : Prop :=
154  ∀ h r i z s source n xs old,
155    Zlib.Inflate.Spec.Good h r i z s → z.zalloc = .fn "zcalloc" →
156    InflateDictionary h s old → (source ≠ .null → Bytes h source n.toNat xs) →
157    Separate source n.toNat s.window (2 ^ s.wbits.toNat) →
158    ((s.wrap = 0 ∨ s.mode = DICT) → 8 ≤ s.wbits.toNat) →
159    ∃ rc after, C.run (Zlib.Inflate.inflateSetDictionary (some r) source n) h = .ok (rc, after) ∧
160      (source = .null ∨ (s.wrap ≠ 0 ∧ s.mode ≠ DICT) → rc = Z_STREAM_ERROR ∧ after = h) ∧
161      (source ≠ .null → (s.wrap = 0 ∨ s.mode = DICT) →
162        if s.mode = DICT ∧ s.check ≠ (ZlibF.Spec.adler32 xs).toUInt64 then rc = Z_DATA_ERROR ∧ after = h
163        else (rc = Z_MEM_ERROR ∧ AllocationFailed h after ∧
164          ∃ s', Zlib.Inflate.Spec.Good after r i z s' ∧ s'.mode = MEM) ∨
165          (rc = Z_OK ∧ ∃ s', Zlib.Inflate.Spec.Good after r i z s' ∧
166            s'.havedict = 1 ∧ s'.mode = s.mode ∧
167            InflateDictionary after s' ((old ++ xs).drop ((old ++ xs).length - 2 ^ s.wbits.toNat)))) ∧
168      Frame h after (fun b => StreamRoot r b ∨ InflateOwned i s b) ∧
169      (∃ s', h.istates i = some s ∧ after.istates i = some s' ∧
170        LiveChange h after (fun b => InflateOwned i s' b ∧ ¬ h.live b) (fun _ => False))
171
172/-- `int deflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`.
173The raw path checks the block boundary. Repeated zlib dictionaries accumulate their checksum.
174The temporary input binding is restored, and no allocation is performed. -/
175def Goal.deflateSetDictionary : Prop :=
176  ∀ h r i z s source n xs old,
177    Zlib.Deflate.Spec.DGood h r i z s → LibraryGlobals h →
178    DeflateDictionary h s old → (source ≠ .null → Bytes h source n.toNat xs) →
179    Separate source n.toNat s.window s.window_size.toNat →
180    ∃ rc after, C.run (Zlib.Deflate.deflateSetDictionary (some r) source n) h = .ok (rc, after) ∧
181      (if source = .null ∨ s.wrap = 2 ∨ (s.wrap = 1 ∧ s.status ≠ INIT_STATE) ∨
182          s.lookahead ≠ 0 ∨ (s.wrap = 0 ∧ s.strstart.toUInt64.toInt64 ≠ s.block_start) then
183        rc = Z_STREAM_ERROR ∧ after = h
184       else rc = Z_OK ∧ ∃ z' s' dict,
185         Zlib.Deflate.Spec.DGood after r i z' s' ∧ DeflateDictionary after s' dict ∧
186         z' = { z with
187           total_in := z.total_in + UInt64.ofNat (min xs.length s.w_size.toNat)
188           adler := if s.wrap = 1 then adlerValue z.adler xs else z.adler } ∧
189         s'.wrap = s.wrap ∧ s'.lookahead = 0 ∧ s'.block_start = s'.strstart.toUInt64.toInt64 ∧
190         dict <:+ old ++ xs ∧ dict.length ≤ s.w_size.toNat ∧
191         min (old.length + xs.length) (s.w_size.toNat - 262) ≤ dict.length) ∧
192      Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) ∧
193      LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc
194
195end ZlibF.Spec.Public