ByteAddress.lean

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

1import ZlibF.Runtime.Address
2import ZlibF.Runtime.Ptr
3import ZlibF.Zlib.«crc32.c»
4
5/-!
6# Obligations for the CRC low-address-bit model
7
8These goals check the metadata interpretation independently of checksum
9arithmetic. Non-block origins range over all residues. Raw blocks retain
10the existing aligned-origin convention; general ABI layout is not claimed.
11-/
12
13namespace C.ByteAddress.Spec
14
15/-- The exact integer observation made by the CRC alignment condition. -/
16def low (value : UInt64) : Nat := (value &&& 7).toNat
17
18/-- A concrete base-address assignment agrees with the model where the
19program observes it. This is a representation relation, not a caller
20contract required by the general checksum theorem. -/
21def ModelsLowBits (h : Heap) (physicalBase : BRef → Nat) : Prop :=
22  ∀ ref, physicalBase ref % 8 = base h ref
23
24/-- Assign concrete low address bits without rebuilding the existing heap. -/
25def withLayout (h : Heap) (physicalBase : BRef → Nat) : Heap :=
26  { h with byteBase := fun ref =>
27      ⟨physicalBase ref.toBRef % 8, Nat.mod_lt _ (by decide)⟩ }
28
29/-- All heap components that predate the address metadata are unchanged. -/
30def SameStorage (before after : Heap) : Prop :=
31  after.bytes = before.bytes ∧ after.words = before.words ∧
32  after.ro = before.ro ∧ after.streams = before.streams ∧
33  after.gzheaders = before.gzheaders ∧ after.dstates = before.dstates ∧
34  after.istates = before.istates ∧ after.gzstates = before.gzstates ∧
35  after.static = before.static ∧ after.nextBlk = before.nextBlk ∧
36  after.nalloc = before.nalloc ∧ after.allocOk = before.allocOk ∧
37  after.garbage = before.garbage
38
39def Goal.address_read_is_pure : Prop :=
40  ∀ (h : Heap) (p : BPtr),
41    C.run (Zlib.Crc32.addrOf p) h = .ok (value h p, h)
42
43def Goal.raw_block_unchanged : Prop :=
44  ∀ (h : Heap) (block offset : Nat),
45    C.run (Zlib.Crc32.addrOf (.ref (.blk block) offset)) h =
46      .ok (UInt64.ofNat offset, h)
47
48/-- Every concrete non-block origin residue is representable. No static
49or embedded field is forced to be aligned. -/
50def Goal.every_layout_is_representable : Prop :=
51  ∀ physicalBase : BRef → Nat,
52    (∀ block, physicalBase (.blk block) % 8 = 0) →
53    ∃ h : Heap, ModelsLowBits h physicalBase
54
55/-- Every existing heap admits any concrete non-block layout, while all
56pre-existing storage and allocation choices stay exactly the same. -/
57def Goal.every_existing_heap_accepts_layout : Prop :=
58  ∀ (h : Heap) (physicalBase : BRef → Nat),
59    (∀ block, physicalBase (.blk block) % 8 = 0) →
60    ModelsLowBits (withLayout h physicalBase) physicalBase ∧
61      SameStorage h (withLayout h physicalBase)
62
63/-- The source cast followed by its mask agrees with the actual base plus
64offset, including unsigned wrap before masking. -/
65def Goal.mask_refines_base_plus_offset : Prop :=
66  ∀ (h : Heap) (physicalBase : BRef → Nat), ModelsLowBits h physicalBase →
67    ∀ (ref : BRef) (offset : Nat),
68      low (value h (.ref ref offset)) = (physicalBase ref + offset) % 8
69
70def Goal.pointer_advance_preserves_low_bits : Prop :=
71  ∀ (h : Heap) (ref : BRef) (offset count : Nat),
72    low (value h (.ref ref (offset + count))) =
73      (low (value h (.ref ref offset)) + count) % 8
74
75/-- The first aligned position lies at most seven bytes ahead. A source
76loop may exhaust its input earlier; this is a position-arithmetic claim. -/
77def Goal.first_aligned_offset : Prop :=
78  ∀ (h : Heap) (ref : BRef) (offset : Nat),
79    let count := (8 - low (value h (.ref ref offset))) % 8
80    count ≤ 7 ∧ low (value h (.ref ref (offset + count))) = 0 ∧
81      ∀ before, before < count → low (value h (.ref ref (offset + before))) ≠ 0
82
83def Goal.byte_stores_preserve_bases : Prop :=
84  ∀ (h : Heap) (ref : BRef) (bytes : Array UInt8),
85    (Space.put h ref bytes).byteBase = h.byteBase
86
87def Goal.byte_modifies_preserve_bases : Prop :=
88  ∀ (h : Heap) (ref : BRef) (modify : Array UInt8 → Array UInt8),
89    (Space.modify h ref modify).byteBase = h.byteBase
90
91end C.ByteAddress.Spec