pointer-arithmetic.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# Natural-offset pointer arithmetic for implementation proofs
5
6These helpers use the runtime's checked pointer addition. The rules retain the
7same live-array, bounds and subtraction premises as the runtime lemmas.
8-/
9
10namespace ZlibF.Proof.PointerArithmetic
11open C
12
13/-- `p + n` for a pointer into an array. -/
14def addNat {R T : Type} [Space Heap R T] (p : Ptr R) (n : Nat) : M (Ptr R) := Ptr.add p (n : Int)
15/-- `p - n` for a pointer into an array. -/
16def subNat {R T : Type} [Space Heap R T] (p : Ptr R) (n : Nat) : M (Ptr R) := Ptr.add p (-(n : Int))
17
18theorem addNat_ok {R T : Type} [Space Heap R T] {h : Heap} {r : R} {a : Array T} {off n : Nat}
19    (hg : Space.get h r = some a) (hn : off + n ≤ a.size) : addNat (.ref r off) n h = .ok (.ref r (off + n), h) :=
20  Ptr.add_nat_ok hg hn
21theorem subNat_ok {R T : Type} [Space Heap R T] {h : Heap} {r : R} {a : Array T} {off n : Nat}
22    (hg : Space.get h r = some a) (h1 : n ≤ off) (h2 : off ≤ a.size) :
23    subNat (.ref r off) n h = .ok (.ref r (off - n), h) :=
24  Ptr.sub_nat_ok hg h1 h2
25
26end ZlibF.Proof.PointerArithmetic