From a4c31944db0792cf5b8f4c0ce0c3e4e62295c0c4 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 15:54:32 -0400 Subject: [PATCH] first draft --- Iris/Iris/BI/BigOp/BigSepList.lean | 21 ++ Iris/Iris/BI/Lib/Fractional.lean | 9 + Iris/Iris/HeapLang.lean | 1 + Iris/Iris/HeapLang/DerivedLaws.lean | 313 ++++++++++++++++++++++++++ Iris/Iris/HeapLang/Lib.lean | 1 + Iris/Iris/HeapLang/Lib/Array.lean | 265 ++++++++++++++++++++++ Iris/Iris/HeapLang/PrimitiveLaws.lean | 71 ++++++ Iris/Iris/HeapLang/ProofMode.lean | 43 +++- Iris/Iris/HeapLang/Semantics.lean | 17 ++ Iris/Iris/HeapLang/Syntax.lean | 11 + 10 files changed, 751 insertions(+), 1 deletion(-) create mode 100644 Iris/Iris/HeapLang/DerivedLaws.lean create mode 100644 Iris/Iris/HeapLang/Lib/Array.lean diff --git a/Iris/Iris/BI/BigOp/BigSepList.lean b/Iris/Iris/BI/BigOp/BigSepList.lean index 21aed5e46..0884b79bb 100644 --- a/Iris/Iris/BI/BigOp/BigSepList.lean +++ b/Iris/Iris/BI/BigOp/BigSepList.lean @@ -235,6 +235,27 @@ theorem bigSepL_map {B : Type _} (f : A → B) {Φ : Nat → B → PROP} {l : Li ([∗list] k ↦ y ∈ l.map f, Φ k y) = [∗list] k ↦ x ∈ l, Φ k (f x) := bigOpL_map_eq f Φ l +/-- Collect the witnesses of a list of existentials whose elements are all in the image of `g`. -/ +@[rocq_alias heap_lang.big_sepL_exists_eq] +theorem bigSepL_exists_eq [BIAffine PROP] {B : Type _} {g : B → A} {Ψ : Nat → B → PROP} + {l : List A} : + ([∗list] k ↦ y ∈ l, ∃ x, ⌜y = g x⌝ ∗ Ψ k x) ⊢ + ∃ xs, ⌜l = xs.map g⌝ ∗ [∗list] k ↦ x ∈ xs, Ψ k x := by + induction l generalizing Ψ with + | nil => + refine .trans ?_ (exists_intro ([] : List B)) + exact emp_sep.2.trans (sep_mono (pure_intro rfl) .rfl) + | cons y l ih => + refine (sep_mono_right ih).trans <| sep_exists_left.1.trans <| exists_elim fun xs => ?_ + refine sep_exists_right.1.trans <| exists_elim fun x => ?_ + refine pure_elim (y = g x) (sep_elim_left.trans sep_elim_left) fun hy => ?_ + refine pure_elim (l = xs.map g) (sep_elim_right.trans sep_elim_left) fun hl => ?_ + refine .trans ?_ (exists_intro (Ψ := fun ys => + iprop(⌜y :: l = List.map g ys⌝ ∗ ([∗list] k ↦ z ∈ ys, Ψ k z))) (x :: xs)) + refine (sep_mono sep_elim_right sep_elim_right).trans <| emp_sep.2.trans <| + sep_mono (pure_intro ?_) .rfl + simp [hy, hl] + @[rocq_alias big_sepL_omap] theorem bigSepL_filterMap {B : Type _} (f : A → Option B) {Φ : B → PROP} {l : List A} : ([∗list] y ∈ l.filterMap f, Φ y) = [∗list] x ∈ l, (f x).elim emp Φ := diff --git a/Iris/Iris/BI/Lib/Fractional.lean b/Iris/Iris/BI/Lib/Fractional.lean index 2522c4be2..afb427e3d 100644 --- a/Iris/Iris/BI/Lib/Fractional.lean +++ b/Iris/Iris/BI/Lib/Fractional.lean @@ -100,6 +100,15 @@ instance (priority := default - 10) combineSepAsFractionalHalf _ ⊢ Φ (q.half + q.half) := (hP.as_fractional_fractional.fractional q.half q.half).mpr _ ⊢ Φ q := Qp.half_add_half _ ▸ .rfl +@[rocq_alias fractional_big_sepL] +instance fractional_bigSepL {A : Type _} {l : List A} {Ψ : Nat → A → Qp → PROP} + [∀ k x, Fractional (Ψ k x)] : Fractional (fun q => iprop([∗list] k ↦ x ∈ l, Ψ k x q)) where + fractional p q := + ⟨(BigSepL.bigSepL_mono_of_forall fun {_ _} => (Fractional.fractional p q).1).trans + BigSepL.bigSepL_sep_eqv.1, + BigSepL.bigSepL_sep_eqv.2.trans + (BigSepL.bigSepL_mono_of_forall fun {_ _} => (Fractional.fractional p q).2)⟩ + end Lemmas section Divide diff --git a/Iris/Iris/HeapLang.lean b/Iris/Iris/HeapLang.lean index 138791e1e..7ef8a6853 100644 --- a/Iris/Iris/HeapLang.lean +++ b/Iris/Iris/HeapLang.lean @@ -1,6 +1,7 @@ module public import Iris.HeapLang.Completeness +public import Iris.HeapLang.DerivedLaws public import Iris.HeapLang.Instances public import Iris.HeapLang.Linter public import Iris.HeapLang.Notation diff --git a/Iris/Iris/HeapLang/DerivedLaws.lean b/Iris/Iris/HeapLang/DerivedLaws.lean new file mode 100644 index 000000000..38ecc3e1d --- /dev/null +++ b/Iris/Iris/HeapLang/DerivedLaws.lean @@ -0,0 +1,313 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: +-/ +module + +public import Iris.HeapLang.PrimitiveLaws + +/-! # Derived HeapLang laws + +This file extends the HeapLang program logic with some derived laws (not using the lifting +lemmas) about arrays and prophecies. + +Iris-Lean has no total weakest precondition yet, so only the partial (`wp_`) versions of the +laws are ported. + +For utility functions on arrays (e.g. freeing/copying an array), see `Iris.HeapLang.Lib.Array`. -/ + +@[expose] public section +namespace Iris.HeapLang + +open Iris BI ProofMode ProgramLogic Std + +variable {GF : BundledGFunctors} {hlc : HasLC} [HeapLangGS hlc GF] +variable {s : Stuckness} {E : CoPset} {Φ : Val → IProp GF} +variable {l : Loc} {dq : DFrac} {v : Val} {vs : List Val} + +/-! ## The `array` connective + +`array` is a version of `pointsTo` that works with lists of values. -/ + +@[rocq_alias heap_lang.array] +def array (l : Loc) (dq : DFrac) (vs : List Val) : IProp GF := + iprop([∗list] i ↦ v ∈ vs, (l + Int.ofNat i) ↦{dq} some v) + +@[inherit_doc array] notation:50 l:50 " ↦∗{" dq "} " vs:50 => array l dq vs +@[inherit_doc array] notation:50 l:50 " ↦∗ " vs:50 => array l (DFrac.own 1) vs + +@[rocq_alias heap_lang.array_timeless] +instance instTimelessArray : Timeless (l ↦∗{dq} vs : IProp GF) := by + unfold array; infer_instance + +@[rocq_alias heap_lang.array_fractional] +instance instFractionalArray : Fractional (fun q => (l ↦∗{.own q} vs : IProp GF)) := by + unfold array; infer_instance + +@[rocq_alias heap_lang.array_as_fractional] +instance instAsFractionalArray {q : Qp} : + AsFractional (l ↦∗{.own q} vs : IProp GF) ioΦ (l ↦∗{.own ·} vs) ioq q where + as_fractional := .rfl + as_fractional_fractional := instFractionalArray + +@[rocq_alias heap_lang.array_nil] +theorem array_nil : (l ↦∗{dq} [] : IProp GF) ⊣⊢ emp := .rfl + +@[rocq_alias heap_lang.array_singleton] +theorem array_singleton : (l ↦∗{dq} [v] : IProp GF) ⊣⊢ l ↦{dq} some v := by + unfold array + refine BigSepL.bigSepL_singleton.trans (.of_eq ?_) + rw [show l + Int.ofNat 0 = l from loc_add_zero l] + +@[rocq_alias heap_lang.array_app] +theorem array_app {ws : List Val} : + (l ↦∗{dq} (vs ++ ws) : IProp GF) ⊣⊢ l ↦∗{dq} vs ∗ (l + Int.ofNat vs.length) ↦∗{dq} ws := by + unfold array + refine BigSepL.bigSepL_append.trans + (sep_congr_right (.of_eq (BigSepL.bigSepL_eq_of_forall_eq ?_))) + intro k x + congr 1 + ext + simp + omega + +@[rocq_alias heap_lang.array_cons] +theorem array_cons : + (l ↦∗{dq} (v :: vs) : IProp GF) ⊣⊢ l ↦{dq} some v ∗ (l + (1 : Int)) ↦∗{dq} vs := by + unfold array + refine BigSepL.bigSepL_cons.trans + (sep_congr (.of_eq ?_) (.of_eq (BigSepL.bigSepL_eq_of_forall_eq ?_))) + · rw [show l + Int.ofNat 0 = l from loc_add_zero l] + · intro k x + congr 1 + ext + simp + omega + +@[rocq_alias heap_lang.array_cons_frame] +instance (priority := high) frameArrayCons {R Q : IProp GF} + [h : Frame false R iprop(l ↦{dq} some v ∗ (l + (1 : Int)) ↦∗{dq} vs) Q] : + Frame false R (l ↦∗{dq} (v :: vs)) Q where + frame := h.frame.trans array_cons.2 + +@[rocq_alias heap_lang.update_array] +theorem update_array {off : Nat} (h : vs[off]? = some v) : + (l ↦∗{dq} vs : IProp GF) ⊢ (l + Int.ofNat off) ↦{dq} some v ∗ + ∀ v', (l + Int.ofNat off) ↦{dq} some v' -∗ l ↦∗{dq} vs.set off v' := + BigSepL.bigSepL_insert_acc h + +/-- The array `vs` is unchanged when the element read out of it is written back. -/ +private theorem set_getElem?_self {off : Nat} (h : vs[off]? = some v) : vs.set off v = vs := by + obtain ⟨hlt, rfl⟩ := List.getElem?_eq_some_iff.mp h + exact List.set_getElem_self hlt + +/-- `update_array` specialised to a read: the array is restored unchanged. -/ +private theorem update_array_read {off : Nat} (h : vs[off]? = some v) : + (l ↦∗{dq} vs : IProp GF) ⊢ (l + Int.ofNat off) ↦{dq} some v ∗ + ((l + Int.ofNat off) ↦{dq} some v -∗ l ↦∗{dq} vs) := + (update_array h).trans <| sep_mono_right <| (forall_elim v).trans <| + wand_mono .rfl (BiEntails.of_eq (congrArg (array l dq) (set_getElem?_self h))).1 + +/-- Recast a primitive law whose postcondition pins the returned value into continuation-passing +form, framing the continuation across the step. -/ +private theorem wp_cps_of_pure_post {e : Exp} {P P' : IProp GF} {r : Val} + (hval : toVal e = none) (hwp : ▷ P ⊢ WP e @ s; E {{ v', ⌜v' = r⌝ ∗ P' }}) : + ▷ P ∗ ▷ (P' -∗ Φ r) ⊢ WP e @ s; E {{ Φ }} := by + refine (sep_mono hwp .rfl).trans (sep_comm.1.trans ?_) + refine (wp_frame_step_l' hval LawfulSet.subset_refl).trans (wp_mono fun _ => ?_) + iintro ⟨Hcont, %hv, HP'⟩ + subst hv + iapply Hcont $$ HP' + +/-! ## Rules for allocation -/ + +@[rocq_alias heap_lang.pointsto_seq_array] +theorem pointsTo_seq_array {n : Nat} : + ([∗list] i ∈ List.range n, (l + Int.ofNat i) ↦{dq} some v) ⊢ + (l ↦∗{dq} List.replicate n v : IProp GF) := by + unfold array + induction n with + | zero => exact .rfl + | succ n ih => + rw [List.range_succ, List.replicate_succ'] + refine BigSepL.bigSepL_snoc.1.trans (.trans ?_ BigSepL.bigSepL_snoc.2) + simp only [List.length_replicate] + exact sep_mono ih .rfl + +@[rocq_alias heap_lang.wp_allocN] +theorem wp_allocN (v : Val) {n : Int} (hn : 0 < n) : + ▷ (∀ l : Loc, (l ↦∗ List.replicate n.toNat v ∗ + [∗list] i ∈ List.range n.toNat, metaToken (l + Int.ofNat i) ⊤) -∗ Φ (.lit <| .loc l)) -∗ + WP hl(allocn(#n, &v)) @ s; E {{ Φ }} := by + iintro HΦ + iapply wp_allocN_seq v hn + iintro !> %l Hl + icases BigSepL.bigSepL_sep_eqv.1 $$ Hl with ⟨Hpts, Htok⟩ + iapply HΦ + iframe Htok + iapply pointsTo_seq_array $$ Hpts + +@[rocq_alias heap_lang.wp_allocN_vec] +theorem wp_allocN_vec (v : Val) {n : Int} (hn : 0 < n) : + ▷ (∀ l : Loc, (l ↦∗ (Vector.replicate n.toNat v).toList ∗ + [∗list] i ∈ List.range n.toNat, metaToken (l + Int.ofNat i) ⊤) -∗ Φ (.lit <| .loc l)) -∗ + WP hl(allocn(#n, &v)) @ s; E {{ Φ }} := + Vector.toList_replicate ▸ wp_allocN v hn + +/-! ## Rules for accessing array elements -/ + +@[rocq_alias heap_lang.wp_load_offset] +theorem wp_load_offset {off : Nat} (h : vs[off]? = some v) : + ▷ l ↦∗{dq} vs -∗ ▷ ((l ↦∗{dq} vs : IProp GF) -∗ Φ v) -∗ + WP hl(!v(#(l + Int.ofNat off))) @ s; E {{ Φ }} := by + iintro Hl HΦ + icases (later_mono (update_array_read h)).trans later_sep.1 $$ Hl with ⟨Hpt, Hclose⟩ + iapply wp_load $$ Hpt + iintro !> Hpt + iapply HΦ + iapply Hclose $$ Hpt + +@[rocq_alias heap_lang.wp_load_offset_vec] +theorem wp_load_offset_vec {sz : Nat} {off : Fin sz} {ws : Vector Val sz} : + ▷ l ↦∗{dq} ws.toList -∗ ▷ ((l ↦∗{dq} ws.toList : IProp GF) -∗ Φ ws[off]) -∗ + WP hl(!v(#(l + Int.ofNat off.val))) @ s; E {{ Φ }} := + wp_load_offset (by simp) + +@[rocq_alias heap_lang.wp_store_offset] +theorem wp_store_offset {off : Nat} {w : Val} (h : vs[off]? = some w) : + ▷ l ↦∗ vs -∗ ▷ ((l ↦∗ vs.set off v : IProp GF) -∗ Φ hl_val(#())) -∗ + WP hl(v(#(l + Int.ofNat off)) ← &v) @ s; E {{ Φ }} := by + iintro Hl HΦ + icases (later_mono (update_array (dq := .own 1) h)).trans later_sep.1 $$ Hl with ⟨Hpt, Hclose⟩ + iapply wp_store $$ Hpt + iintro !> Hpt + iapply HΦ + iapply Hclose $$ %v Hpt + +@[rocq_alias heap_lang.wp_store_offset_vec] +theorem wp_store_offset_vec {sz : Nat} {off : Fin sz} {ws : Vector Val sz} : + ▷ l ↦∗ ws.toList -∗ ▷ ((l ↦∗ (ws.set off v).toList : IProp GF) -∗ Φ hl_val(#())) -∗ + WP hl(v(#(l + Int.ofNat off.val)) ← &v) @ s; E {{ Φ }} := by + rw [Vector.toList_set] + exact wp_store_offset (w := ws[off]) (by simp) + +@[rocq_alias heap_lang.wp_xchg_offset] +theorem wp_xchg_offset {off : Nat} {w : Val} (h : vs[off]? = some v) : + ▷ l ↦∗ vs -∗ ▷ ((l ↦∗ vs.set off w : IProp GF) -∗ Φ v) -∗ + WP hl(xchg(#(l + Int.ofNat off), &w)) @ s; E {{ Φ }} := by + iintro Hl HΦ + icases (later_mono (update_array (dq := .own 1) h)).trans later_sep.1 $$ Hl with ⟨Hpt, Hclose⟩ + iapply wp_cps_of_pure_post rfl wp_xchg + iframe Hpt + iintro !> Hpt + iapply HΦ + iapply Hclose $$ %w Hpt + +@[rocq_alias heap_lang.wp_xchg_offset_vec] +theorem wp_xchg_offset_vec {sz : Nat} {off : Fin sz} {ws : Vector Val sz} : + ▷ l ↦∗ ws.toList -∗ ▷ ((l ↦∗ (ws.set off v).toList : IProp GF) -∗ Φ ws[off]) -∗ + WP hl(xchg(#(l + Int.ofNat off.val), &v)) @ s; E {{ Φ }} := by + rw [Vector.toList_set] + exact wp_xchg_offset (by simp) + +@[rocq_alias heap_lang.wp_cmpxchg_suc_offset] +theorem wp_cmpXchg_true_offset {off : Nat} {v1 v2 : Val} (h : vs[off]? = some v) + (heq : v = v1) (hsafe : v.compareSafe v1) : + ▷ l ↦∗ vs -∗ ▷ ((l ↦∗ vs.set off v2 : IProp GF) -∗ Φ hl_val((&v, #true))) -∗ + WP hl(cmpXchg(#(l + Int.ofNat off), &v1, &v2)) @ s; E {{ Φ }} := by + iintro Hl HΦ + icases (later_mono (update_array (dq := .own 1) h)).trans later_sep.1 $$ Hl with ⟨Hpt, Hclose⟩ + iapply wp_cps_of_pure_post rfl (wp_cmpXchg_true rfl rfl hsafe (decide_eq_true heq)) + iframe Hpt + iintro !> Hpt + iapply HΦ + iapply Hclose $$ %v2 Hpt + +@[rocq_alias heap_lang.wp_cmpxchg_suc_offset_vec] +theorem wp_cmpXchg_true_offset_vec {sz : Nat} {off : Fin sz} {ws : Vector Val sz} {v1 v2 : Val} + (heq : ws[off] = v1) (hsafe : ws[off].compareSafe v1) : + ▷ l ↦∗ ws.toList -∗ + ▷ ((l ↦∗ (ws.set off v2).toList : IProp GF) -∗ Φ hl_val((&ws[off], #true))) -∗ + WP hl(cmpXchg(#(l + Int.ofNat off.val), &v1, &v2)) @ s; E {{ Φ }} := by + rw [Vector.toList_set] + exact wp_cmpXchg_true_offset (by simp) heq hsafe + +@[rocq_alias heap_lang.wp_cmpxchg_fail_offset] +theorem wp_cmpXchg_fail_offset {off : Nat} {v1 v2 : Val} (h : vs[off]? = some v) + (hne : v ≠ v1) (hsafe : v.compareSafe v1) : + ▷ l ↦∗{dq} vs -∗ ▷ ((l ↦∗{dq} vs : IProp GF) -∗ Φ hl_val((&v, #false))) -∗ + WP hl(cmpXchg(#(l + Int.ofNat off), &v1, &v2)) @ s; E {{ Φ }} := by + iintro Hl HΦ + icases (later_mono (update_array_read h)).trans later_sep.1 $$ Hl with ⟨Hpt, Hclose⟩ + iapply wp_cps_of_pure_post rfl (wp_cmpXchg_fail rfl rfl hsafe (decide_eq_false hne)) + iframe Hpt + iintro !> Hpt + iapply HΦ + iapply Hclose $$ Hpt + +@[rocq_alias heap_lang.wp_cmpxchg_fail_offset_vec] +theorem wp_cmpXchg_fail_offset_vec {sz : Nat} {off : Fin sz} {ws : Vector Val sz} {v1 v2 : Val} + (hne : ws[off] ≠ v1) (hsafe : ws[off].compareSafe v1) : + ▷ l ↦∗{dq} ws.toList -∗ + ▷ ((l ↦∗{dq} ws.toList : IProp GF) -∗ Φ hl_val((&ws[off], #false))) -∗ + WP hl(cmpXchg(#(l + Int.ofNat off.val), &v1, &v2)) @ s; E {{ Φ }} := + wp_cmpXchg_fail_offset (by simp) hne hsafe + +@[rocq_alias heap_lang.wp_faa_offset] +theorem wp_faa_offset {off : Nat} {i1 i2 : Int} (h : vs[off]? = some hl_val(#i1)) : + ▷ l ↦∗ vs -∗ + ▷ ((l ↦∗ vs.set off hl_val(#(i1 + i2)) : IProp GF) -∗ Φ hl_val(#i1)) -∗ + WP hl(faa(#(l + Int.ofNat off), #i2)) @ s; E {{ Φ }} := by + iintro Hl HΦ + icases (later_mono (update_array (dq := .own 1) h)).trans later_sep.1 $$ Hl with ⟨Hpt, Hclose⟩ + iapply wp_cps_of_pure_post rfl wp_faa + iframe Hpt + iintro !> Hpt + iapply HΦ + iapply Hclose $$ %hl_val(#(i1 + i2)) Hpt + +@[rocq_alias heap_lang.wp_faa_offset_vec] +theorem wp_faa_offset_vec {sz : Nat} {off : Fin sz} {ws : Vector Val sz} {i1 i2 : Int} + (h : ws[off] = hl_val(#i1)) : + ▷ l ↦∗ ws.toList -∗ + ▷ ((l ↦∗ (ws.set off hl_val(#(i1 + i2))).toList : IProp GF) -∗ Φ hl_val(#i1)) -∗ + WP hl(faa(#(l + Int.ofNat off.val), #i2)) @ s; E {{ Φ }} := by + rw [Vector.toList_set] + exact wp_faa_offset (by simpa using h) + +/-! ## Derived prophecy laws -/ + +@[rocq_alias heap_lang.wp_resolve_cmpxchg_suc] +theorem wp_resolve_cmpXchg_true {p : ProphId} {pvs : List (Val × Val)} {v1 v2 w : Val} + (hsafe : v1.compareSafe v1) : + proph p pvs -∗ ▷ l ↦ some v1 -∗ + ▷ ((∃ pvs', ⌜pvs = (hl_val((&v1, #true)), w) :: pvs'⌝ ∗ proph p pvs' ∗ l ↦ some v2) -∗ + Φ hl_val((&v1, #true))) -∗ + WP hl(resolve(cmpXchg(#l, &v1, &v2), v(#p), v(&w))) @ s; E {{ Φ }} := by + iintro Hp Hl HΦ + iapply wp_resolve inferInstance (hne := rfl) $$ Hp + iapply wp_cps_of_pure_post rfl (wp_cmpXchg_true rfl rfl hsafe (decide_eq_true rfl)) + iframe Hl + iintro !> Hl %pvs' %heq Hp + iapply HΦ + iexists pvs' + iframe Hp Hl %heq + +@[rocq_alias heap_lang.wp_resolve_cmpxchg_fail] +theorem wp_resolve_cmpXchg_fail {p : ProphId} {pvs : List (Val × Val)} {v1 v2 w : Val} + (hne : v ≠ v1) (hsafe : v.compareSafe v1) : + proph p pvs -∗ ▷ l ↦{dq} some v -∗ + ▷ ((∃ pvs', ⌜pvs = (hl_val((&v, #false)), w) :: pvs'⌝ ∗ proph p pvs' ∗ l ↦{dq} some v) -∗ + Φ hl_val((&v, #false))) -∗ + WP hl(resolve(cmpXchg(#l, &v1, &v2), v(#p), v(&w))) @ s; E {{ Φ }} := by + iintro Hp Hl HΦ + iapply wp_resolve inferInstance (hne := rfl) $$ Hp + iapply wp_cps_of_pure_post rfl (wp_cmpXchg_fail rfl rfl hsafe (decide_eq_false hne)) + iframe Hl + iintro !> Hl %pvs' %heq Hp + iapply HΦ + iexists pvs' + iframe Hp Hl %heq + +end Iris.HeapLang diff --git a/Iris/Iris/HeapLang/Lib.lean b/Iris/Iris/HeapLang/Lib.lean index fb454b2ef..d8df07755 100644 --- a/Iris/Iris/HeapLang/Lib.lean +++ b/Iris/Iris/HeapLang/Lib.lean @@ -1,6 +1,7 @@ module public import Iris.HeapLang.Lib.Arith +public import Iris.HeapLang.Lib.Array public import Iris.HeapLang.Lib.Assert public import Iris.HeapLang.Lib.Diverge public import Iris.HeapLang.Lib.LandinsKnot diff --git a/Iris/Iris/HeapLang/Lib/Array.lean b/Iris/Iris/HeapLang/Lib/Array.lean new file mode 100644 index 000000000..0e8437063 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/Array.lean @@ -0,0 +1,265 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: +-/ +module + +public import Iris.HeapLang.DerivedLaws +public import Iris.HeapLang.ProofMode + +/-! # Array utilities + +* `arrayFree`, to deallocate an entire array in one go. +* `arrayCopyTo`, a function which copies to an array in-place. +* Using `arrayCopyTo` we also implement `arrayClone`, which allocates a fresh array and copies + to it. +* `arrayInit`, to create and initialize an array with a given function. Specifically, + `arrayInit n f` creates a new array of size `n` in which the `i`th element is initialized + with `f #i`. + +Iris-Lean has no total weakest precondition yet, so only the partial (`wp_`) versions of the +specifications are ported. -/ + +namespace Iris.HeapLang + +open BI Iris ProgramLogic + +@[expose] public section + +@[rocq_alias heap_lang.array_free] +def arrayFree : Val := hl_val% + rec freeN ptr n := + if n ≤ #(0 : Int) then #() + else (free(ptr); freeN (ptr +ₗ #(1 : Int)) (n - #(1 : Int))) + +@[rocq_alias heap_lang.array_copy_to] +def arrayCopyTo : Val := hl_val% + rec copyTo dst src n := + if n ≤ #(0 : Int) then #() + else (dst ← !src; copyTo (dst +ₗ #(1 : Int)) (src +ₗ #(1 : Int)) (n - #(1 : Int))) + +@[rocq_alias heap_lang.array_clone] +def arrayClone : Val := hl_val% + λ src n, + let dst := allocn(n, #()); + &arrayCopyTo dst src n; + dst + +/-- `arrayInitLoop src i n f` initializes elements `i`, `i+1`, …, `n` of the array `src` to +`f #i`, `f #(i+1)`, …, `f #n`. -/ +@[rocq_alias heap_lang.array_init_loop] +def arrayInitLoop : Val := hl_val% + rec loop src i n f := + if i = n then #() + else (src +ₗ i ← f i; loop src (i + #(1 : Int)) n f) + +@[rocq_alias heap_lang.array_init] +def arrayInit : Val := hl_val% + λ n f, + let src := allocn(n, #()); + &arrayInitLoop src #(0 : Int) n f; + src + +section Proof + +variable {GF : BundledGFunctors} {hlc : HasLC} [HeapLangGS hlc GF] + +@[rocq_alias heap_lang.wp_array_free] +theorem wp_array_free (s : Stuckness) (E : CoPset) (l : Loc) (vs : List Val) (n : Int) + (hn : n = vs.length) : + {{ (l ↦∗ vs : IProp GF) }} hl(&arrayFree #l #n) @ s; E {{ RET hl_val(#()); True }} := by + subst hn + induction vs generalizing l with + | nil => + iintro %Φ Hl HΦ + wp_rec + wp_pures + rw [decide_eq_true (show ((([] : List Val).length : Int) ≤ 0) by simp)] + wp_pures + iapply HΦ + itrivial + | cons w vs ih => + iintro %Φ Hl HΦ + icases array_cons.1 $$ Hl with ⟨Hw, Hl⟩ + wp_rec + wp_pures + rw [decide_eq_false (show ¬ (((w :: vs).length : Int) ≤ 0) by simp)] + wp_free + wp_pures + rw [show (((w :: vs).length : Int) - 1) = (vs.length : Int) by simp] + iapply ih $$ Hl HΦ + +@[rocq_alias heap_lang.wp_array_copy_to] +theorem wp_array_copy_to (s : Stuckness) (E : CoPset) (dst src : Loc) (vdst vsrc : List Val) + (dq : DFrac) (n : Int) (hdst : (vdst.length : Int) = n) (hsrc : (vsrc.length : Int) = n) : + {{ (dst ↦∗ vdst ∗ src ↦∗{dq} vsrc : IProp GF) }} hl(&arrayCopyTo #dst #src #n) @ s; E + {{ RET hl_val(#()); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }} := by + subst hdst + revert hsrc + induction vdst generalizing dst src vsrc with + | nil => + cases vsrc with + | cons v2 vsrc => + exact fun hsrc => absurd hsrc (by simp; omega) + | nil => + intro _ + iintro %Φ ⟨Hdst, Hsrc⟩ HΦ + wp_rec + wp_pures + rw [decide_eq_true (show ((([] : List Val).length : Int) ≤ 0) by simp)] + wp_pures + iapply HΦ + iframe + | cons v1 vdst ih => + cases vsrc with + | nil => + exact fun hsrc => absurd hsrc (by simp; omega) + | cons v2 vsrc => + intro hsrc + iintro %Φ ⟨Hdst, Hsrc⟩ HΦ + icases array_cons.1 $$ Hdst with ⟨Hv1, Hdst⟩ + icases array_cons.1 $$ Hsrc with ⟨Hv2, Hsrc⟩ + wp_rec + wp_pures + rw [decide_eq_false (show ¬ (((v1 :: vdst).length : Int) ≤ 0) by simp)] + wp_load + wp_store + wp_pures + rw [show (((v1 :: vdst).length : Int) - 1) = (vdst.length : Int) by simp] + iapply ih (dst + (1 : Int)) (src + (1 : Int)) vsrc (by simp at hsrc; omega) $$ + %Φ [$Hdst $Hsrc] [Hv1 Hv2 HΦ] + iintro !> ⟨Hdst, Hsrc⟩ + iapply HΦ + iframe + +@[rocq_alias heap_lang.wp_array_clone] +theorem wp_array_clone (s : Stuckness) (E : CoPset) (l : Loc) (dq : DFrac) (vl : List Val) + (n : Int) (hvl : (vl.length : Int) = n) (hn : 0 < n) : + {{ (l ↦∗{dq} vl : IProp GF) }} hl(&arrayClone #l #n) @ s; E + {{ l', RET hl_val(#l'); l' ↦∗ vl ∗ l ↦∗{dq} vl }} := by + iintro %Φ Hvl HΦ + wp_lam + wp_allocN dst with Hdst + wp_pures + wp_bind &arrayCopyTo _ _ _ + iapply wp_array_copy_to s E dst l (List.replicate n.toNat hl_val(#())) vl dq n + (by simp only [List.length_replicate]; omega) hvl $$ [$Hdst $Hvl] + iintro !> ⟨Hdst, Hl⟩ + wp_pures + iapply HΦ + iframe + +section ArrayInit + +variable (Q : Nat → Val → IProp GF) + +@[rocq_alias heap_lang.wp_array_init_loop] +theorem wp_array_init_loop (s : Stuckness) (E : CoPset) (l : Loc) (i k : Nat) (n : Int) + (f : Val) (hn : n = Int.ofNat (i + k)) : + {{ (l + Int.ofNat i) ↦∗ List.replicate k hl_val(#()) ∗ + [∗list] j ∈ List.range' i k, WP hl(&f #(Int.ofNat j)) @ s; E {{ Q j }} }} + hl(&arrayInitLoop #l #(Int.ofNat i) #n &f) @ s; E + {{ vs, RET hl_val(#()); ⌜vs.length = k⌝ ∗ (l + Int.ofNat i) ↦∗ vs ∗ + [∗list] j ↦ v ∈ vs, Q (i + j) v }} := by + subst hn + induction k generalizing i with + | zero => + iintro %Φ ⟨Hl, Hf⟩ HΦ + wp_rec + wp_pures + simp only [Nat.add_zero, beq_self_eq_true] + wp_pures + imodintro + iapply HΦ $$ %([] : List Val) + isimp only [array_nil.to_eq, BigSepL.bigSepL_nil.to_eq] + itrivial + | succ k ih => + iintro %Φ ⟨Hl, Hf⟩ HΦ + wp_rec + wp_pures + rw [show (hl_val(#(Int.ofNat i)) == hl_val(#(Int.ofNat (i + (k + 1))))) = false by + simp; omega] + wp_pures + ieval (simp only [List.replicate_succ]) at Hl + ieval (simp only [List.range'_succ]) at Hf + icases array_cons.1 $$ Hl with ⟨Hl, HSl⟩ + icases BigSepL.bigSepL_cons.1 $$ Hf with ⟨Hf, HSf⟩ + wp_bind &f _ + iapply wp_wand $$ Hf + iintro %v Hv + wp_store + wp_pures + rw [show Int.ofNat i + 1 = Int.ofNat (i + 1) from rfl, + show Int.ofNat (i + (k + 1)) = Int.ofNat (i + 1 + k) by congr 1; omega] + iapply ih (i + 1) $$ %Φ [HSl HSf] [Hl Hv HΦ] + · rw [show l + Int.ofNat (i + 1) = l + Int.ofNat i + (1 : Int) from + (loc_add_assoc l (Int.ofNat i) 1).symm] + iframe + · iintro !> %vs ⟨%hlen, HSl, Hvs⟩ + iapply HΦ $$ %(v :: vs) + rw [show l + Int.ofNat (i + 1) = l + Int.ofNat i + (1 : Int) from + (loc_add_assoc l (Int.ofNat i) 1).symm] + ieval (simp only [show ∀ j, i + 1 + j = i + (j + 1) from fun j => by omega]) at Hvs + iframe Hl HSl + isplitl [] + · ipureintro + simp [hlen] + · iapply BigSepL.bigSepL_cons.2 + iframe + +@[rocq_alias heap_lang.wp_array_init] +theorem wp_array_init (s : Stuckness) (E : CoPset) (n : Int) (f : Val) (hn : 0 < n) : + {{ [∗list] i ∈ List.range n.toNat, WP hl(&f #(Int.ofNat i)) @ s; E {{ Q i }} }} + hl(&arrayInit #n &f) @ s; E + {{ l vs, RET hl_val(#l); ⌜(vs.length : Int) = n⌝ ∗ l ↦∗ vs ∗ + [∗list] k ↦ v ∈ vs, Q k v }} := by + iintro %Φ Hf HΦ + wp_lam + wp_allocN src with Hl + wp_pures + wp_bind &arrayInitLoop _ _ _ _ + iapply wp_array_init_loop Q s E src 0 n.toNat n f (by simp; omega) $$ [Hl Hf] + · rw [show src + Int.ofNat 0 = src from loc_add_zero src, List.range_eq_range'] + iframe + · iintro !> %vs ⟨%hlen, Hl, Hvs⟩ + wp_pures + imodintro + iapply HΦ $$ %src %vs + rw [show src + Int.ofNat 0 = src from loc_add_zero src] + ieval (simp only [Nat.zero_add]) at Hvs + isplitl [] + · ipureintro + omega + · iframe Hl Hvs + +end ArrayInit + +section ArrayInitFmap + +variable {α : Type _} (g : α → Val) (Q : Nat → α → IProp GF) + +@[rocq_alias heap_lang.wp_array_init_fmap] +theorem wp_array_init_fmap (s : Stuckness) (E : CoPset) (n : Int) (f : Val) (hn : 0 < n) : + {{ [∗list] i ∈ List.range n.toNat, + WP hl(&f #(Int.ofNat i)) @ s; E {{ v, ∃ x, ⌜v = g x⌝ ∗ Q i x }} }} + hl(&arrayInit #n &f) @ s; E + {{ l xs, RET hl_val(#l); ⌜(xs.length : Int) = n⌝ ∗ l ↦∗ xs.map g ∗ + [∗list] k ↦ x ∈ xs, Q k x }} := by + iintro %Φ Hf HΦ + iapply wp_array_init (fun i v => iprop(∃ x, ⌜v = g x⌝ ∗ Q i x)) s E n f hn $$ Hf + iintro !> %l %vs ⟨%hlen, Hl, Hvs⟩ + icases BigSepL.bigSepL_exists_eq $$ Hvs with ⟨%xs, %heq, Hxs⟩ + subst heq + iapply HΦ $$ %l %xs + isplitl [] + · ipureintro + simpa using hlen + · iframe Hl Hxs + +end ArrayInitFmap + +end Proof + +end +end Iris.HeapLang diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index 6157337ad..fa57f9f95 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -240,6 +240,76 @@ theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) : isplit; ipureintro; rfl iapply HΦ $$ [$] +/-! ## Multi-cell allocation + +The usable rules for `allocN` stated in terms of the `array` proposition are derived in +`Iris.HeapLang.DerivedLaws`. -/ + +@[rocq_alias heap_lang.heap_array_to_seq_pointsto] +theorem allocCells_toSeq_pointsTo {l : Loc} {v : Val} {n : Nat} : + ([∗map] l' ↦ ov ∈ allocCells l n (some v), l' ↦ ov) ⊢ + [∗list] i ∈ List.range n, (l + Int.ofNat i) ↦ some v := by + induction n with + | zero => + rw [allocCells_zero, List.range_zero] + exact BI.BigSepM.bigSepM_empty.1.trans BI.BigSepL.bigSepL_nil.2 + | succ n ih => + rw [allocCells_succ, List.range_succ] + refine (BI.BigSepM.bigSepM_insert get?_allocCells_self).1.trans ?_ + refine .trans ?_ BI.BigSepL.bigSepL_snoc.2 + exact BI.sep_comm.1.trans (BI.sep_mono ih .rfl) + +@[rocq_alias heap_lang.heap_array_to_seq_meta] +theorem allocCells_toSeq_metaToken {l : Loc} {v : Option Val} {n : Nat} : + ([∗map] l' ↦ _ov ∈ allocCells l n v, metaToken l' ⊤) ⊢ + [∗list] i ∈ List.range n, metaToken (l + Int.ofNat i) ⊤ := by + induction n with + | zero => + rw [allocCells_zero, List.range_zero] + exact BI.BigSepM.bigSepM_empty.1.trans BI.BigSepL.bigSepL_nil.2 + | succ n ih => + rw [allocCells_succ, List.range_succ] + refine (BI.BigSepM.bigSepM_insert (Φ := fun l' _ => iprop(metaToken l' ⊤)) + get?_allocCells_self).1.trans ?_ + refine .trans ?_ BI.BigSepL.bigSepL_snoc.2 + exact BI.sep_comm.1.trans (BI.sep_mono ih .rfl) + +@[rocq_alias heap_lang.wp_allocN_seq] +theorem wp_allocN_seq (v : Val) {n : Int} (hn : 0 < n) : + ▷ (∀ l : Loc, ([∗list] i ∈ List.range n.toNat, + (l + Int.ofNat i) ↦ some v ∗ metaToken (l + Int.ofNat i) ⊤) -∗ Φ (.lit <| .loc l)) -∗ + WP hl(allocn(#n, &v)) @ s; E {{ Φ }} := by + iintro HΦ + iapply wp_lift_atomic_step rfl + iintro %σ₁ %ns %obs %obs' %nt Hσ !> + icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + obtain ⟨l, hfresh⟩ := exists_fresh_block σ₁.heap n + have Hred : BaseStep.Reducible (hl(allocn(#n, &v)), σ₁) := + ⟨[], .ofVal (.lit (.loc l)), σ₁.initHeap l n v, [], .allocNS n v σ₁ l hn hfresh⟩ + isplitr + · ipureintro + cases s <;> simp only [Stuckness.MaybeReducible] + exact primStep_reducible_of_baseStep_reducible Hred + iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + rcases baseStep_of_primStep_of_baseStep_reducible Hred Heq + rename_i l' _hn' hfresh' + ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + simp only [stateInterp, Algebra.BigOpL.bigOpL_nil] + imod genHeap_alloc_big (allocCells l' n.toNat v) σ₁.heap (allocCells_disjoint hfresh') $$ Hσ + with ⟨Hσ, Hpts, Htok⟩ + imodintro + isplitl [Hσ Hproph] + · iframe Hproph + iapply genHeapInterp_eqv (.symm _ _ initHeap_heap_eq) $$ Hσ + isplit <;> try itrivial + iexists hl_val(#(BaseLit.loc l')) + isplit; ipureintro; rfl + iapply HΦ + iapply BI.BigSepL.bigSepL_sep_eqv.2 + isplitl [Hpts] + · iapply allocCells_toSeq_pointsTo $$ Hpts + · iapply allocCells_toSeq_metaToken $$ Htok + theorem wp_load {l : Loc} {q} {v : Val} Φ : ▷ l ↦{q} some v -∗ ▷ (l ↦{q} some v -∗ Φ v) -∗ @@ -623,6 +693,7 @@ theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)} iframe Hp iexact Hcont +@[rocq_alias heap_lang.wp_resolve_proph] theorem wp_resolve_proph {p : ProphId} {w : Val} {pvs : List (Val × Val)} : proph p pvs -∗ (∀ pvs', ⌜pvs = (hl_val(#()), w) :: pvs'⌝ -∗ proph p pvs' -∗ Φ hl_val(#())) -∗ diff --git a/Iris/Iris/HeapLang/ProofMode.lean b/Iris/Iris/HeapLang/ProofMode.lean index 6c3b9c110..77bc587ff 100644 --- a/Iris/Iris/HeapLang/ProofMode.lean +++ b/Iris/Iris/HeapLang/ProofMode.lean @@ -9,6 +9,7 @@ public import Iris.ProofMode public import Iris.HeapLang.Tactic public import Iris.HeapLang.Instances public import Iris.HeapLang.PrimitiveLaws +public import Iris.HeapLang.DerivedLaws public import Iris.ProgramLogic.WeakestPre public import Iris.ProgramLogic.Language public import Iris.ProgramLogic.EctxLanguage @@ -556,7 +557,20 @@ public theorem tac_wp_faa [ι : HeapLangGS hlc GF] {Δ Δ' Δ'' : IProp GF} Δ ⊢ WP (ProgramLogic.fill K hl(faa(#l, #z2))) @ s ; E {{ Φ }} := tac_wp_heap_op rfl wp_faa hlater hsplit hcont --- TODO: port `tac_wp_allocN` once `array` and `wp_allocN` are ported +/-- Like `tac_wp_alloc`, but for a multi-cell allocation. The meta tokens handed out by +`wp_allocN` are dropped; use `wp_allocN` directly when they are needed. -/ +public theorem tac_wp_allocN [ι : HeapLangGS hlc GF] {Δ Δ' : IProp GF} + {s : Stuckness} {E : CoPset} {K : List ECtxItem} {v : Val} {n : Int} {Φ} + (hn : 0 < n) + (hlater : Δ ⊢ ▷ Δ') + (hcont : ∀ l : Loc, Δ' ∗ (l ↦∗ List.replicate n.toNat v) ⊢ + WP (ProgramLogic.fill K (Exp.ofVal (Expr := Exp) hl_val(#l))) @ s ; E {{ Φ }}) : + Δ ⊢ WP (ProgramLogic.fill K hl(allocn(#n, &v))) @ s ; E {{ Φ }} := by + refine hlater.trans ?_ + refine .trans ?_ (wp_bind (ProgramLogic.fill K)) + refine .trans ?_ (wand_entails (wp_allocN v hn)) + exact later_mono <| forall_intro fun l => + wand_intro <| (sep_mono_right sep_elim_left).trans (hcont l) /-! ## Shared machinery for the heap tactics -/ @@ -886,6 +900,33 @@ elab "wp_alloc" colGt ppSpace loc:binderIdent " with" colGt ppSpace hyp:binderId macro "wp_alloc" colGt ppSpace loc:binderIdent : tactic => `(tactic| wp_alloc $loc with _) +elab "wp_allocN" colGt ppSpace loc:binderIdent " with" colGt ppSpace hyp:binderIdent : tactic => + runTacticHeapWp `wp_allocN fun mvar {bi, GF, hlc, s, E, e, Φ, hgs, eΔ', hyps', pfLater, ..} => do + let some {result := (n, v), K, ..} ← findECtx e fun e' => do + let ~q(Exp.allocN (Exp.ofVal (Val.lit (BaseLit.int $n))) (Exp.ofVal $v)) := e' | failure + return (n, v) + | throwIPMError "cannot find an `allocn` redex" + trace[wp_heap.redex] "allocn {n} {v}; K = {K}" + + -- a non-positive allocation is stuck, so the bound is the caller's to discharge + let pfPos ← iSolveSidecondition q(0 < $n) (failOnUnsolved := false) + + let (locName, _) ← getFreshName loc + + let pfCont : Q(∀ l : Loc, $eΔ' ∗ array l (DFrac.own 1) (List.replicate ($n).toNat $v) ⊢ + Wp.wp (self := wp.def (ι := @HeapLang $hlc $GF $hgs)) $s $E + (ProgramLogic.fill $K (Exp.ofVal (Expr := Exp) (Val.lit (BaseLit.loc l)))) $Φ) ← + Qq.withLocalDeclDQ locName q(Loc) fun l => do + let ⟨_, _, hyps'', pfEq⟩ ← hyps'.addWithInfo bi hyp q(false) + q(array $l (DFrac.own 1) (List.replicate ($n).toNat $v)) + + let pf ← finishHeapOp hyps'' hgs s E K q(Val.lit (BaseLit.loc $l)) Φ + mkLambdaFVars #[l] q($(pfEq).mp.trans $pf) + + mvar.assign q(tac_wp_allocN (ι := $hgs) (Δ' := $eΔ') $pfPos $pfLater $pfCont) + +macro "wp_allocN" colGt ppSpace loc:binderIdent : tactic => `(tactic| wp_allocN $loc with _) + -- Register the trace classes emitted by the tactics above; enables -- `set_option trace.wp_bind true` (and analogously for the others). initialize registerTraceClass `wp_bind diff --git a/Iris/Iris/HeapLang/Semantics.lean b/Iris/Iris/HeapLang/Semantics.lean index faed75d25..efc381ba0 100644 --- a/Iris/Iris/HeapLang/Semantics.lean +++ b/Iris/Iris/HeapLang/Semantics.lean @@ -154,6 +154,23 @@ theorem get?_allocCells {l : Loc} {n : Nat} {v : Option Val} {k : Loc} : = if (∃ i, i < n ∧ k = l + (i : Int)) then some v else none := by simp [allocCells, get?_foldl_insert, Std.LawfulPartialMap.get?_empty] +@[simp] +theorem allocCells_zero {l : Loc} {v : Option Val} : allocCells l 0 v = ∅ := rfl + +/-- `allocCells` peels off its *last* cell. -/ +theorem allocCells_succ {l : Loc} {n : Nat} {v : Option Val} : + allocCells l (n + 1) v = Std.insert (M := HeapF) (allocCells l n v) (l + (n : Int)) v := by + rw [allocCells, List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil] + rfl + +theorem get?_allocCells_self {l : Loc} {n : Nat} {v : Option Val} : + PartialMap.get? (M := HeapF) (allocCells l n v) (l + (n : Int)) = none := by + rw [get?_allocCells, if_neg] + rintro ⟨i, hi, hik⟩ + have := congrArg Loc.n hik + simp only [loc_add_n] at this + omega + theorem initHeap_heap_eq {σ : State} {l : Loc} {n : Int} {v : Option Val} : Std.PartialMap.equiv (M := HeapF) (σ.initHeap l n v).heap (Std.PartialMap.union (allocCells l n.toNat v) σ.heap) := by diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean index 8b82bd62d..56264995c 100644 --- a/Iris/Iris/HeapLang/Syntax.lean +++ b/Iris/Iris/HeapLang/Syntax.lean @@ -52,6 +52,17 @@ instance : Zero Loc where theorem loc_add_n (l : Loc) n : (l + n).n = l.n + n := by simp [HAdd.hAdd] +@[rocq_alias heap_lang.Loc.add_assoc] +theorem loc_add_assoc (l : Loc) (i j : Int) : l + i + j = l + (i + j) := by + ext; simp [Int.add_assoc] + +@[simp, rocq_alias heap_lang.Loc.add_0] +theorem loc_add_zero (l : Loc) : l + (0 : Int) = l := by ext; simp + +@[rocq_alias heap_lang.Loc.add_inj] +theorem loc_add_inj {l : Loc} {i j : Int} (h : l + i = l + j) : i = j := by + have := congrArg Loc.n h; simp only [loc_add_n] at this; omega + @[ext, rocq_alias heap_lang.heap_lang.proph_id] structure ProphId where mk ::