Memory.lean

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

1import ZlibF.Spec.Public.Checksums
2
3namespace ZlibF.Spec.Public
4open C
5
6/-- A readable range. A null pointer denotes only an empty range here; checksum queries
7have their separate null-buffer convention in `BufferBytes`. -/
8def Bytes (h : Heap) (p : BPtr) (n : Nat) (xs : List UInt8) : Prop :=
9  (p = .null ∧ n = 0 ∧ xs = []) ∨
10  ∃ r i a, p = .ref r i ∧ Space.get h r = some a ∧ i + n ≤ a.size ∧
11    xs = (a.toList.drop i).take n
12
13/-- A writable range, including a null empty range. -/
14def Writable (h : Heap) (p : BPtr) (n : Nat) : Prop :=
15  (p = .null ∧ n = 0) ∨ ∃ r i a,
16    p = .ref r i ∧ Space.get h r = some a ∧ Space.ro h r = false ∧ i + n ≤ a.size
17
18/-- Two ranges may share an allocation, but their occupied intervals must be disjoint. -/
19def Separate (p : BPtr) (n : Nat) (q : BPtr) (m : Nat) : Prop :=
20  n = 0 ∨ m = 0 ∨
21  match p, q with
22  | .ref r i, .ref s j => r ≠ s ∨ i + n ≤ j ∨ j + m ≤ i
23  | _, _ => True
24
25/-- The exact byte-array update, preserving both sides of the written interval. -/
26def Store (h : Heap) (p : BPtr) (xs : List UInt8) (after : Heap) : Prop :=
27  (xs = [] ∧ after = h) ∨ ∃ r i a,
28    p = .ref r i ∧ Space.get h r = some a ∧ Space.ro h r = false ∧
29    i + xs.length ≤ a.size ∧
30    after = Space.put h r (a.extract 0 i ++ xs.toArray ++ a.extract (i + xs.length) a.size)
31
32/-- Successful temporary allocations may advance the allocation metadata. They must leave
33every object and read-only flag as specified, and leave no new live object behind. -/
34def SameObjects (expected after : Heap) : Prop :=
35  after.bytes = expected.bytes ∧ after.words = expected.words ∧
36  (∀ b, expected.live b → after.ro b = expected.ro b) ∧
37  after.streams = expected.streams ∧ after.gzheaders = expected.gzheaders ∧
38  after.dstates = expected.dstates ∧ after.istates = expected.istates ∧
39  after.gzstates = expected.gzstates ∧ after.static = expected.static ∧
40  after.allocOk = expected.allocOk ∧ after.garbage = expected.garbage ∧
41  expected.nextBlk ≤ after.nextBlk ∧ expected.nalloc ≤ after.nalloc
42
43/-- A little-endian length cell in the current scalar-pointer representation. -/
44def LengthCell (h : Heap) (p : BPtr) (value : UInt64) : Prop :=
45  Bytes h p 8 ((List.range 8).map fun i => UInt8.ofNat (value.toNat / 256 ^ i % 256)) ∧
46  Writable h p 8
47
48/-- Only genuine allocator failures can justify an allocation-error result. -/
49def AllocationFailed (before after : Heap) : Prop :=
50  ∃ i, before.nalloc ≤ i ∧ i < after.nalloc ∧ before.allocOk i = false
51
52/-- The constant tables of the selected build. -/
53def LibraryGlobals (h : Heap) : Prop :=
54  h.static = Zlib.Crc32.initStatics
55    (Zlib.Inftrees.initStatics (Zlib.Trees.trees_statics Heap.empty.static))
56
57def lengthBytes (n : UInt64) : List UInt8 :=
58  (List.range 8).map fun i => UInt8.ofNat (n.toNat / 256 ^ i % 256)
59
60end ZlibF.Spec.Public