PlatformMemory.lean

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

1import ZlibF.Spec.PlatformMemory
2import ZlibF.Runtime.Libc
3import ZlibF.Zlib.«zutil.c»
4
5/-!
6# Consequences of the explicit byte-object platform bound
7
8The environment premise is used as stated. It is not derived from the
9unrestricted runtime allocator or from stream reachability.
10-/
11
12namespace ZlibF.PlatformMemory
13open C
14set_option autoImplicit false
15
16/-- Retrieve the bound in the form required by existing decoder lemmas. -/
17theorem ByteObjectsFit.size_lt {h : Heap} (fit : ByteObjectsFit h)
18    {ref : BRef} {a : Array UInt8} (get : Space.get h ref = some a) :
19    a.size < 2 ^ 63 := fit ref a get
20
21/-- Raw byte blocks satisfy the same bound as static and embedded views. -/
22theorem ByteObjectsFit.block_size_lt {h : Heap} (fit : ByteObjectsFit h)
23    {block : Nat} {a : Array UInt8} (get : h.bytes block = some a) :
24    a.size < 2 ^ 63 := fit.size_lt (ref := .blk block) get
25
26/-- Both pointers may be one past the object. Their actual signed
27difference is representable without a separate arithmetic premise. -/
28theorem ByteObjectsFit.diff_ok {h : Heap} (fit : ByteObjectsFit h)
29    {ref : BRef} {a : Array UInt8} {p q : Nat}
30    (get : Space.get h ref = some a) (hp : p ≤ a.size) (hq : q ≤ a.size) :
31    OkOn h (Ptr.diff (.ref ref p) (.ref ref q))
32      (Int64.ofInt ((p : Int) - (q : Int))) := by
33  have bound := fit.size_lt get
34  exact Ptr.diff_ok get hp hq (by omega)
35
36/-- Any transition which retains or decreases every live byte-view size
37preserves the platform condition. No callee execution contract is assumed. -/
38theorem ByteObjectsFit.of_sizes_le {before after : Heap}
39    (fit : ByteObjectsFit before)
40    (sizes : ∀ (ref : BRef) (a : Array UInt8), Space.get after ref = some a →
41      ∃ old, Space.get before ref = some old ∧ a.size ≤ old.size) :
42    ByteObjectsFit after := by
43  intro ref a get
44  obtain ⟨old, oldGet, le⟩ := sizes ref a get
45  exact Nat.lt_of_le_of_lt le (fit ref old oldGet)
46
47/-- Byte views depend only on byte blocks, deflate records and static
48storage. Other heap metadata cannot change the size premise. -/
49theorem ByteObjectsFit.of_storage_eq {before after : Heap}
50    (fit : ByteObjectsFit before) (bytes : after.bytes = before.bytes)
51    (dstates : after.dstates = before.dstates) (statics : after.static = before.static) :
52    ByteObjectsFit after := by
53  intro ref a get
54  have same : (Space.get after ref : Option (Array UInt8)) = Space.get before ref := by
55    cases ref <;> simp only [Space.get, bytes, dstates, statics]
56  rw [same] at get
57  exact fit ref a get
58
59/-- Writing a stream record, including an embedded gzip stream, leaves
60every represented byte-view size unchanged. -/
61theorem ByteObjectsFit.put_stream {h : Heap} (fit : ByteObjectsFit h)
62    (ref : ZStreamRef) (z : ZStream) : ByteObjectsFit (ref.put h z) := by
63  apply fit.of_storage_eq
64  all_goals cases ref <;> simp only [ZStreamRef.put] <;> split <;> rfl
65
66/-- Updating decoder state records leaves all represented byte views
67unchanged. Byte arrays embedded in compressor records remain covered. -/
68theorem ByteObjectsFit.with_istates {h : Heap} (fit : ByteObjectsFit h)
69    (states : Tbl (Option InflateState)) : ByteObjectsFit { h with istates := states } :=
70  fit.of_storage_eq rfl rfl rfl
71
72/-- Installing a bounded raw byte block preserves every other byte view.
73This also covers an allocation's fresh storage after its size is bounded. -/
74theorem ByteObjectsFit.with_bytes {h : Heap} (fit : ByteObjectsFit h)
75    {block : Nat} {a : Array UInt8} (bound : a.size < byteObjectLimit) :
76    ByteObjectsFit { h with bytes := upd h.bytes block (some a) } := by
77  intro ref xs get
78  cases ref with
79  | blk b =>
80    change (upd h.bytes block (some a)) b = some xs at get
81    by_cases eq : b = block
82    · subst b
83      rw [upd_same] at get
84      cases get
85      exact bound
86    · rw [upd_ne _ _ _ _ eq] at get
87      exact fit (.blk b) xs get
88  | str i => exact fit (.str i) xs get
89  | dstate_depth i => exact fit (.dstate_depth i) xs get
90  | st_dist_code => exact fit .st_dist_code xs get
91  | st_length_code => exact fit .st_length_code xs get
92
93/-- `void *malloc(size_t n)`.
94For an explicitly bounded request, every returning outcome of the actual
95runtime allocator preserves the byte-object scope. Allocation failure is
96included. This theorem does not change the unrestricted allocator or claim
97that its oracle enforces the platform bound for oversized requests. -/
98theorem ByteObjectsFit.allocB {h after : Heap} (fit : ByteObjectsFit h)
99    {n : Nat} {pointer : BPtr} (bound : n < byteObjectLimit)
100    (run : C.allocB n h = .ok (pointer, after)) : ByteObjectsFit after := by
101  unfold C.allocB at run
102  split at run
103  · split at run
104    · contradiction
105    · cases run
106      have arrayBound : (Array.ofFn (n := n)
107          (fun i => Junk.of (h.garbage h.nalloc i.val) : Fin n → UInt8)).size < byteObjectLimit := by
108        simpa only [Array.size_ofFn] using bound
109      exact (fit.with_bytes (block := h.nextBlk) arrayBound)
110  · cases run
111    exact fit
112
113/-- `voidpf zcalloc(voidpf opaque, unsigned items, unsigned size)`.
114The translated default allocator computes the request with 32-bit unsigned
115multiplication. Thus every returning byte allocation preserves the platform
116size scope, including NULL returns, without an extra size premise. This
117does not establish that a wrapped product provides the intended capacity. -/
118theorem ByteObjectsFit.zcalloc {h after : Heap} (fit : ByteObjectsFit h)
119    {context pointer : BPtr} {items size : UInt32}
120    (run : Zlib.Zutil.zcalloc context items size h = .ok (pointer, after)) :
121    ByteObjectsFit after := by
122  have bound : (items * size).toNat < byteObjectLimit := by
123    have := UInt32.toNat_lt (items * size)
124    unfold byteObjectLimit
125    omega
126  exact fit.allocB bound run
127
128end ZlibF.PlatformMemory