inflate.c.window-platform.lean

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

1import ZlibF.Proof.«inflate.c.window-compose»
2import ZlibF.Proof.PlatformMemory
3
4namespace Zlib.Inflate.Proofs
5open C Zlib.Inflate Zlib.Inflate.Spec ZlibF.Spec.Public
6set_option autoImplicit false
7
8/-- The actual fresh-window path preserves the platform byte-object bound.
9The requested allocation and every ring copy have their real bounded size. -/
10theorem uw_null_platform_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
11    {st : InflateState} {eo : Nat} {source : BRef} {ebytes : Array UInt8} {copy : UInt32}
12    (hG : Good h r zs z st) (platform : ZlibF.PlatformMemory.ByteObjectsFit h)
13    (hza : z.zalloc = .fn "zcalloc") (hw : st.window = .null)
14    (hok : h.allocOk h.nalloc = true) (heb : Space.get h source = some ebytes)
15    (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
16    ∃ after state, updatewindow (some r) (.ref source eo) copy h = .ok (0, after) ∧
17      Good after r zs z state ∧ ZlibF.PlatformMemory.ByteObjectsFit after ∧ after.static = h.static := by
18  have hL := hG.live
19  have hI := hG.inv
20  have hF := hG.fresh
21  have hne : source ≠ .blk h.nextBlk := by
22    intro he
23    subst source
24    have hfresh := Fresh.bytes hF (b := h.nextBlk) (Nat.le_refl _)
25    have hbytes : h.bytes h.nextBlk = some ebytes := by simpa using heb
26    rw [hbytes] at hfresh
27    cases hfresh
28  rw [uw_alloc_ok hL hza hI.win.wbits hw hok hF]
29  have hn : ((1 <<< st.wbits : UInt32) * 1).toNat = 2 ^ st.wbits.toNat := by
30    have := shl_toNat_aux hI.win.wbits
31    simpa using this
32  obtain ⟨A0, hA0⟩ : ∃ A0 : Array UInt8, A0 = Array.ofFn (n := ((1 <<< st.wbits : UInt32) * 1).toNat)
33      fun i => Junk.of (h.garbage h.nalloc i.val) := ⟨_, rfl⟩
34  have hA0sz : A0.size = 2 ^ st.wbits.toNat := by rw [hA0, Array.size_ofFn]; exact hn
35  have hws0 := hI.win.nullws hw
36  have hws0n : st.wsize.toNat = 0 := by rw [hws0]; rfl
37  have hA := Zlib.Zutil.Proofs.allocHeap_frame h ((1 <<< st.wbits : UInt32) * 1).toNat
38  have hAb : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).bytes h.nextBlk = some A0 := by
39    rw [hA0]; simp [Zlib.Zutil.Proofs.allocHeap]
40  have hAro : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).ro h.nextBlk = false := by
41    simp [Zlib.Zutil.Proofs.allocHeap]
42  have hS : Shape (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat)
43      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) :=
44    shape_setI (s0 := st) (by simpa [Zlib.Zutil.Proofs.allocHeap] using hL.hs) _
45  have hUa := uniq_allocHeap hG.uniq hF ((1 <<< st.wbits : UInt32) * 1).toNat
46  have hFa := hA.2.1 hF
47  have hG2 : Good (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
48      r zs z (withWin st h.nextBlk) := by
49    refine ⟨⟨?_, by simp, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩, ?_, hS.uniq hUa, hS.fresh rfl hFa⟩
50    · cases r <;> simpa [ZStreamRef.get, Zlib.Zutil.Proofs.allocHeap, setI] using hL.hz
51    · refine ⟨hI.wf, ⟨hI.win.wbits, Or.inr ⟨h.nextBlk, A0, rfl, ?_, ?_, ?_⟩, fun h0 => absurd h0 (by simp [withWin]), ?_, ?_, ?_, ?_⟩,
52        hI.reqbits, hI.bits, hI.ptr⟩
53      · simpa [setI] using hAb
54      · simpa [setI] using hAro
55      · exact hA0sz
56      · exact Or.inl hws0n
57      · have := hI.win.hv; show st.whave.toNat ≤ st.wsize.toNat; exact this
58      · right; refine ⟨hws0n, ?_⟩
59        have := hI.win.wn; show st.wnext.toNat = 0; omega
60      · intro hh; have := hI.win.hv; show st.wnext.toNat = st.whave.toNat; have := hI.win.wn; have := hI.win.hv
61        change st.whave.toNat < st.wsize.toNat at hh; omega
62  have hz2 : r.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) = some z :=
63    hG2.live.hz
64  have hbe : Space.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs
65      (withWin st h.nextBlk)) source = some ebytes := by
66    cases source with
67    | blk b =>
68      have hbn : b ≠ h.nextBlk := fun he => hne (by cases he; rfl)
69      simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hbn] using heb
70    | str b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
71    | st_dist_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
72    | st_length_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
73    | dstate_depth b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
74  have hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
75      (withWin st h.nextBlk).window (2 ^ (withWin st h.nextBlk).wbits.toNat) := by
76    simp [ZlibF.Spec.Public.Separate, withWin, hne]
77  obtain ⟨after, state, hr, heapEq, hstate, hgood, _, _, _, _, _, _⟩ :=
78    uw_post_public (hG := hG2) (w := h.nextBlk) (source := source) (eo := eo)
79      (a := A0) (ebytes := ebytes) (copy := copy) rfl (by simpa [setI] using hAb)
80      (by simpa [setI] using hAro) hA0sz hbe hc hoff hsep
81  have allocated : ZlibF.PlatformMemory.ByteObjectsFit
82      (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) :=
83    platform.zcalloc (Zlib.Zutil.Proofs.zcalloc_ok_run h z.opaque (1 <<< st.wbits) 1 hok hF)
84  have powerBound := Nat.pow_le_pow_right (by decide : 0 < 2) hI.win.wbits
85  have arrayBound : (uwPost (initWinS (withWin st h.nextBlk)) A0 ebytes eo copy).1.size <
86      ZlibF.PlatformMemory.byteObjectLimit := by
87    rw [uwPost_size, hA0sz]
88    unfold ZlibF.PlatformMemory.byteObjectLimit
89    omega
90  refine ⟨after, state, hr, hgood, ?_, ?_⟩
91  · rw [heapEq]
92    exact ((allocated.with_istates _).with_bytes (block := h.nextBlk) arrayBound).with_istates _
93  · rw [heapEq]
94    rfl
95
96/-- Every actual window update preserves the byte-object platform scope.
97Existing-window copying, fresh allocation and genuine allocation failure
98are all covered. No allocator size contract is assumed. -/
99theorem updatewindow_platform_public {h after : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
100    {s : InflateState} {eo : Nat} {source : BRef} {bytes : Array UInt8} {copy : UInt32} {rc : Int32}
101    (good : Good h r zs z s) (platform : ZlibF.PlatformMemory.ByteObjectsFit h)
102    (allocator : z.zalloc = .fn "zcalloc") (get : Space.get h source = some bytes)
103    (count : copy.toNat ≤ eo) (bound : eo ≤ bytes.size)
104    (separate : Separate (.ref source (eo - copy.toNat)) copy.toNat s.window (2 ^ s.wbits.toNat))
105    (run : updatewindow (some r) (.ref source eo) copy h = .ok (rc, after)) :
106    ZlibF.PlatformMemory.ByteObjectsFit after ∧ after.static = h.static := by
107  rcases good.inv.win.block with window | ⟨w, a, window, array, ro, size⟩
108  · by_cases alloc : h.allocOk h.nalloc = true
109    · obtain ⟨result, state, executed, nextGood, fit, static⟩ :=
110        uw_null_platform_public good platform allocator window alloc get count bound
111      have same : after = result := congrArg Prod.snd (Except.ok.inj (run.symm.trans executed))
112      simpa only [same] using And.intro fit static
113    · have executed := uw_alloc_fail good.live allocator good.inv.win.wbits window alloc (.ref source eo) copy
114      have same : after = setI { h with nalloc := h.nalloc + 1 } zs s :=
115        congrArg Prod.snd (Except.ok.inj (run.symm.trans executed))
116      rw [same]
117      exact ⟨platform.of_storage_eq rfl rfl rfl, rfl⟩
118  · obtain ⟨result, state, executed, heapEq, value, nextGood, rest⟩ :=
119      uw_post_public good window array ro size get count bound separate
120    have same : after = result := congrArg Prod.snd (Except.ok.inj (run.symm.trans executed))
121    rw [same, heapEq]
122    have arrayBound : (uwPost (initWinS s) a bytes eo copy).1.size < ZlibF.PlatformMemory.byteObjectLimit := by
123      rw [uwPost_size]
124      exact platform (BRef.blk w) a array
125    exact ⟨((platform.with_istates _).with_bytes (block := w) arrayBound).with_istates _, rfl⟩
126
127end Zlib.Inflate.Proofs