Copy.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.Streams
2
3namespace ZlibF.Spec.Public
4open C
5
6def relocateCode (old fresh : Nat) : CodePtr → CodePtr
7  | .ref (.istate_codes i) off => if i = old then .ref (.istate_codes fresh) off else .ref (.istate_codes i) off
8  | p => p
9
10def relocateByte (fresh old pointer : BPtr) : BPtr :=
11  match fresh, old, pointer with
12  | .ref r start, .ref _ base, .ref _ off => .ref r (start + off - base)
13  | _, _, _ => .null
14
15def SameBytePrefix (before after : Heap) (source dest : BPtr) (n : Nat) : Prop :=
16  ∃ xs, Bytes before source n xs ∧ Bytes after dest n xs
17
18def SameWordPrefix (before after : Heap) (source dest : WPtr) (n : Nat) : Prop :=
19  ∃ r off a r' off' a', source = .ref r off ∧ dest = .ref r' off' ∧
20    Space.get before r = some a ∧ Space.get after r' = some a' ∧
21    off + n ≤ a.size ∧ off' + n ≤ a'.size ∧
22    (a.toList.drop off).take n = (a'.toList.drop off').take n
23
24/-- `int inflateCopy(z_streamp dest, z_streamp source)`.
25Copy every decoder field, relocate internal table pointers, share application header pointers,
26and copy the initialized window bytes. All new storage is independent; failure releases it. -/
27def Goal.inflateCopy : Prop :=
28  (∀ h source, C.run (Zlib.Inflate.inflateCopy none source) h = .ok (Z_STREAM_ERROR, h)) ∧
29  (∀ h dest z, dest.get h = some z →
30    C.run (Zlib.Inflate.inflateCopy (some dest) none) h =
31      .ok (Z_STREAM_ERROR, dest.put h { z with state := none })) ∧
32  (∀ h source i z s dest oldDest,
33    StreamReachable .inflate h source → Zlib.Inflate.Spec.Good h source i z s →
34    Zlib.Inflate.Spec.DefAlloc z → source ≠ dest → dest.get h = some oldDest →
35    ∃ rc after,
36      C.run (Zlib.Inflate.inflateCopy (some dest) (some source)) h = .ok (rc, after) ∧
37      source.get after = some z ∧ after.istates i = some s ∧ Frame h after (StreamRoot dest) ∧
38      ((rc = Z_MEM_ERROR ∧ AllocationFailed h after ∧
39        dest.get after = some { oldDest with state := none } ∧
40        LiveChange h after (fun _ => False) (fun _ => False)) ∨
41       (rc = Z_OK ∧ ∃ copied,
42         Zlib.Inflate.Spec.Good after dest h.nextBlk
43           { z with state := some (.inflate h.nextBlk) } copied ∧
44         copied = { s with
45           strm := some dest, window := copied.window
46           lencode := relocateCode i h.nextBlk s.lencode
47           distcode := relocateCode i h.nextBlk s.distcode
48           next := relocateCode i h.nextBlk s.next } ∧
49         (s.window = .null ↔ copied.window = .null) ∧
50         (s.window ≠ .null → SameBytePrefix h after s.window copied.window s.whave.toNat) ∧
51         (∀ b, InflateOwned h.nextBlk copied b → h.nextBlk ≤ b) ∧
52         LiveChange h after (InflateOwned h.nextBlk copied) (fun _ => False))))
53
54def copiedDeflate (dest : ZStreamRef) (fresh : Nat) (old copied : DeflateState) : DeflateState :=
55  { old with
56    strm := some dest, window := copied.window, prev := copied.prev, head := copied.head
57    pending_buf := copied.pending_buf
58    pending_out := relocateByte copied.pending_buf old.pending_buf old.pending_out
59    sym_buf := advance copied.pending_buf old.lit_bufsize.toNat
60    l_desc := { old.l_desc with dyn_tree := .ref (.dstate_dyn_ltree fresh) 0 }
61    d_desc := { old.d_desc with dyn_tree := .ref (.dstate_dyn_dtree fresh) 0 }
62    bl_desc := { old.bl_desc with dyn_tree := .ref (.dstate_bl_tree fresh) 0 } }
63
64/-- `int deflateCopy(z_streamp dest, z_streamp source)`.
65Copy the initialized window, hash entries, pending bytes and symbols. Relocate the owned
66buffers and tree descriptors. A failure clears destination state and releases every new block. -/
67def Goal.deflateCopy : Prop :=
68  (∀ h source, C.run (Zlib.Deflate.deflateCopy none source) h = .ok (Z_STREAM_ERROR, h)) ∧
69  (∀ h dest z, dest.get h = some z →
70    C.run (Zlib.Deflate.deflateCopy (some dest) none) h =
71      .ok (Z_STREAM_ERROR, dest.put h { z with state := none })) ∧
72  (∀ h source i z s dest oldDest,
73    StreamReachable .deflate h source → Zlib.Deflate.Spec.DGood h source i z s →
74    Zlib.Deflate.Spec.DefAlloc z → source ≠ dest → dest.get h = some oldDest →
75    ∃ rc after,
76      C.run (Zlib.Deflate.deflateCopy (some dest) (some source)) h = .ok (rc, after) ∧
77      source.get after = some z ∧ after.dstates i = some s ∧ Frame h after (StreamRoot dest) ∧
78      ((rc = Z_MEM_ERROR ∧ AllocationFailed h after ∧
79        dest.get after = some { oldDest with state := none } ∧
80        LiveChange h after (fun _ => False) (fun _ => False)) ∨
81       (rc = Z_OK ∧ ∃ copied,
82         Zlib.Deflate.Spec.DGood after dest h.nextBlk
83           { z with state := some (.deflate h.nextBlk) } copied ∧
84         copied = copiedDeflate dest h.nextBlk s copied ∧
85         SameBytePrefix h after s.window copied.window s.high_water.toNat ∧
86         SameWordPrefix h after s.head copied.head s.hash_size.toNat ∧
87         SameWordPrefix h after s.prev copied.prev
88           (if s.slid ≠ 0 ∨ s.strstart - s.insert > s.w_size then s.w_size.toNat
89            else (s.strstart - s.insert).toNat) ∧
90         SameBytePrefix h after s.pending_out copied.pending_out s.pending.toNat ∧
91         SameBytePrefix h after s.sym_buf copied.sym_buf s.sym_next.toNat ∧
92         (∀ b, DeflateOwned h.nextBlk copied b ↔ h.nextBlk ≤ b ∧ b < h.nextBlk + 5) ∧
93         LiveChange h after (DeflateOwned h.nextBlk copied) (fun _ => False))))
94
95end ZlibF.Spec.Public