Address.lean

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

1import ZlibF.Runtime.Monad
2
3/-!
4# Low address bits of byte pointers
5
6CRC observes only an address modulo eight. Raw blocks retain the existing
7aligned-origin convention. Every static or embedded byte array has an
8arbitrary, stable origin residue in the heap. No ABI field alignment is
9silently replaced by zero. These residues are metadata, not writable bytes.
10This does not provide general record layout or pointer-to-integer semantics.
11-/
12
13namespace C
14
15def ByteBaseRef.toBRef : C.ByteBaseRef → BRef
16  | .str id => .str id
17  | .dstate_depth id => .dstate_depth id
18  | .st_dist_code => .st_dist_code
19  | .st_length_code => .st_length_code
20
21namespace ByteAddress
22
23/-- Origin residue. Raw heap blocks have the pre-existing aligned origin. -/
24def base (h : Heap) : BRef → Nat
25  | .blk _ => 0
26  | .str id => (h.byteBase (.str id)).val
27  | .dstate_depth id => (h.byteBase (.dstate_depth id)).val
28  | .st_dist_code => (h.byteBase .st_dist_code).val
29  | .st_length_code => (h.byteBase .st_length_code).val
30
31/-- A representative whose low three bits agree with the represented
32address. Upper address bits are not observed by the CRC translation. -/
33def value (h : Heap) : BPtr → UInt64
34  | .null => 0
35  | .ref (.blk _) off => UInt64.ofNat off
36  | .ref r off => UInt64.ofNat (base h r + off)
37
38/-- Reading address metadata has no memory effect. -/
39def address (p : BPtr) : M UInt64 := fun h => .ok (value h p, h)
40
41end ByteAddress
42end C