PlatformMemory.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Runtime.Ptr
2
3/-!
4# Byte-object sizes for the initial LP64 platform scope
5
6The signed 64-bit pointer-difference limit is distinct from the unsigned
764-bit address width. These predicates state an explicit environment scope;
8they do not alter the allocator or establish that scope for arbitrary heaps.
9-/
10
11namespace ZlibF.PlatformMemory
12open C
13set_option autoImplicit false
14
15/-- One past the largest admitted byte-object size. The initial platform
16scope uses `PTRDIFF_MAX = 2^63 - 1`, not the unsigned `SIZE_MAX`. -/
17def byteObjectLimit : Nat := 2 ^ 63
18
19/-- Every live represented byte array, including static and embedded views,
20fits the signed pointer-difference range. This is an explicit platform
21premise. For caller storage not obtained from the default allocator, it is
22an additional object-realizability requirement, not a malloc conclusion.
23It does not bound the sum of allocations or the total stream length. -/
24def ByteObjectsFit (h : Heap) : Prop :=
25  ∀ (ref : BRef) (a : Array UInt8), Space.get h ref = some a →
26    a.size < byteObjectLimit
27
28end ZlibF.PlatformMemory