ByteAddress.lean

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

1import ZlibF.Spec.ByteAddress
2
3/-!
4# Positive checks of the CRC low-address-bit interpretation
5
6Only residues observed by the alignment mask are represented. The proofs
7range over arbitrary non-block residues and preserve the raw-block case.
8-/
9
10set_option autoImplicit false
11
12namespace C.ByteAddress.Proofs
13open C.ByteAddress C.ByteAddress.Spec
14
15private theorem low_ofNat (n : Nat) : low (UInt64.ofNat n) = n % 8 := by
16  unfold low
17  rw [UInt64.toNat_and,UInt64.toNat_ofNat']
18  have mask : (7 : UInt64).toNat = 2^3-1 := by decide
19  rw [mask,Nat.and_two_pow_sub_one_eq_mod]
20  exact Nat.mod_mod_of_dvd n (Nat.pow_dvd_pow 2 (by decide))
21
22private theorem value_ref (h : Heap) (ref : BRef) (offset : Nat) :
23    value h (.ref ref offset) = UInt64.ofNat (base h ref + offset) := by
24  cases ref <;> simp only [value,base,Nat.zero_add]
25
26/-- The actual translated address observation reads metadata without any
27heap update or pointer access. -/
28theorem address_read_is_pure : Goal.address_read_is_pure := by
29  intro h p
30  rfl
31
32/-- Existing raw-block observations retain their exact original value. -/
33theorem raw_block_unchanged : Goal.raw_block_unchanged := by
34  intro h block offset
35  rfl
36
37/-- Each non-block byte origin can have any concrete residue. The witness
38changes only the symbolic address assignment of the otherwise empty heap. -/
39theorem every_layout_is_representable : Goal.every_layout_is_representable := by
40  intro physical aligned
41  let assignment : ByteBaseRef → Fin 8 := fun ref =>
42    ⟨physical ref.toBRef % 8,Nat.mod_lt _ (by decide)⟩
43  refine ⟨{ Heap.empty with byteBase := assignment },?_⟩
44  intro ref
45  cases ref with
46  | blk block => exact aligned block
47  | str id => rfl
48  | dstate_depth id => rfl
49  | st_dist_code => rfl
50  | st_length_code => rfl
51
52/-- Unsigned conversion before masking preserves the base-plus-offset
53residue, even when the natural-number address exceeds the machine word. -/
54theorem mask_refines_base_plus_offset : Goal.mask_refines_base_plus_offset := by
55  intro h physical represented ref offset
56  rw [value_ref,low_ofNat,← represented ref]
57  simp only [Nat.add_mod,Nat.mod_mod]
58
59/-- Advancing a byte pointer advances its represented residue modulo eight. -/
60theorem pointer_advance_preserves_low_bits : Goal.pointer_advance_preserves_low_bits := by
61  intro h ref offset count
62  rw [value_ref,low_ofNat,value_ref,low_ofNat]
63  omega
64
65/-- Every represented origin reaches alignment at its first such position
66within seven bytes, with no earlier aligned position. -/
67theorem first_aligned_offset : Goal.first_aligned_offset := by
68  intro h ref offset
69  have residueBound : low (value h (.ref ref offset)) < 8 := by
70    rw [value_ref,low_ofNat]
71    exact Nat.mod_lt _ (by decide)
72  dsimp only
73  refine ⟨by omega,?_,?_⟩
74  · rw [pointer_advance_preserves_low_bits h ref offset]
75    omega
76  · intro before shorter
77    rw [pointer_advance_preserves_low_bits h ref offset]
78    omega
79
80/-- Byte-array stores cannot change symbolic origin metadata. -/
81theorem byte_stores_preserve_bases : Goal.byte_stores_preserve_bases := by
82  intro h ref bytes
83  cases ref <;> try rfl
84  simp only [Space.put]
85  split <;> rfl
86
87/-- In-place byte-array modifications preserve the same metadata. -/
88theorem byte_modifies_preserve_bases : Goal.byte_modifies_preserve_bases := by
89  intro h ref modify
90  cases ref <;> rfl
91
92/-- An arbitrary concrete layout can be assigned to any existing heap
93without changing any storage, allocator oracle or garbage assignment. -/
94theorem every_existing_heap_accepts_layout : Goal.every_existing_heap_accepts_layout := by
95  intro h physical aligned
96  refine ⟨?_,?_⟩
97  · intro ref
98    cases ref with
99    | blk block => exact aligned block
100    | str id => rfl
101    | dstate_depth id => rfl
102    | st_dist_code => rfl
103    | st_length_code => rfl
104  · exact ⟨rfl,rfl,rfl,rfl,rfl,rfl,rfl,rfl,rfl,rfl,rfl,rfl,rfl⟩
105
106end C.ByteAddress.Proofs