diff --git a/Iris/Iris/HeapLang/Lib.lean b/Iris/Iris/HeapLang/Lib.lean index c08608d16..fb454b2ef 100644 --- a/Iris/Iris/HeapLang/Lib.lean +++ b/Iris/Iris/HeapLang/Lib.lean @@ -1,5 +1,8 @@ module +public import Iris.HeapLang.Lib.Arith +public import Iris.HeapLang.Lib.Assert +public import Iris.HeapLang.Lib.Diverge public import Iris.HeapLang.Lib.LandinsKnot public import Iris.HeapLang.Lib.LazyCoin public import Iris.HeapLang.Lib.Lock @@ -8,3 +11,4 @@ public import Iris.HeapLang.Lib.Par public import Iris.HeapLang.Lib.Quicksort public import Iris.HeapLang.Lib.Spawn public import Iris.HeapLang.Lib.SpinLock +public import Iris.HeapLang.Lib.Unwrap diff --git a/Iris/Iris/HeapLang/Lib/Arith.lean b/Iris/Iris/HeapLang/Lib/Arith.lean new file mode 100644 index 000000000..16e29949e --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/Arith.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ +module + +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang.Notation +public import Iris.HeapLang.Instances +public import Iris.HeapLang.PrimitiveLaws +public import Iris.HeapLang.ProofMode + +namespace Iris.HeapLang + +open BI Iris ProgramLogic + +@[expose] public section + +namespace Arith + +@[rocq_alias heap_lang.minimum] +def minimum : Val := hl_val% + λ m n, if m < n then m else n + +@[rocq_alias heap_lang.maximum] +def maximum : Val := hl_val% + λ m n, if m < n then n else m + +section Spec + +variable {GF : BundledGFunctors} [HeapLangGS hlc GF] + +@[rocq_alias heap_lang.minimum_spec] +theorem minimum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Int) : + ▷ Φ (Val.lit (.int (min m n))) -∗ + WP hl(&minimum #m #n) @ s; E {{ Φ }} := by + iintro HΦ + wp_lam + wp_pures + by_cases h : m < n + · rw [decide_eq_true h] + wp_pures + rw [Int.min_eq_left (by omega)] + itrivial + · rw [decide_eq_false h] + wp_pures + rw [Int.min_eq_right (by omega)] + itrivial + +@[rocq_alias heap_lang.minimum_spec_nat] +theorem minimum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Nat) : + ▷ Φ (Val.lit (.int (Int.ofNat (min m n)))) -∗ + WP hl(&minimum #m #n) @ s; E {{ Φ }} := by + iintro HΦ + iapply minimum_spec + rw [show min (↑m : Int) ↑n = ↑(min m n) by omega] + itrivial + +@[rocq_alias heap_lang.maximum_spec] +theorem maximum_spec (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Int) : + ▷ Φ (Val.lit (.int (max m n))) -∗ + WP hl(&maximum #m #n) @ s; E {{ Φ }} := by + iintro HΦ + wp_lam + wp_pures + by_cases h : m < n + · rw [decide_eq_true h] + wp_pures + rw [Int.max_eq_right (by omega)] + itrivial + · rw [decide_eq_false h] + wp_pures + rw [Int.max_eq_left (by omega)] + itrivial + +@[rocq_alias heap_lang.maximum_spec_nat] +theorem maximum_spec_nat (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (m n : Nat) : + ▷ Φ (Val.lit (.int (Int.ofNat (max m n)))) -∗ + WP hl(&maximum #m #n) @ s; E {{ Φ }} := by + iintro HΦ + iapply maximum_spec + rw [show max (↑m : Int) ↑n = ↑(max m n) by omega] + itrivial + +end Spec + +end Arith +end diff --git a/Iris/Iris/HeapLang/Lib/Assert.lean b/Iris/Iris/HeapLang/Lib/Assert.lean new file mode 100644 index 000000000..9b1982360 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/Assert.lean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ +module + +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang.Notation +public import Iris.HeapLang.Instances +public import Iris.HeapLang.PrimitiveLaws +public import Iris.HeapLang.ProofMode + +namespace Iris.HeapLang + +open BI Iris ProgramLogic + +@[expose] public section + +namespace Assert + +section Spec + +variable {GF : BundledGFunctors} [HeapLangGS hlc GF] + +-- TODO: use wp_smart_apply +@[rocq_alias heap_lang.wp_assert] +theorem wp_assert (E : CoPset) (Φ : Val → IProp GF) (e : Exp) : + WP e @ E {{ v, ⌜v = hl_val(#true)⌝ ∧ ▷ Φ hl_val(#()) }} -∗ + WP hl(assert(&e)) @ E {{ Φ }} := by + iintro HΦ + unfold Exp.assert + wp_bind &e + iapply wp_wand $$ HΦ + iintro %v ⟨%Heq, _⟩ ; subst Heq + wp_if; itrivial + +end Spec + +end Assert +end diff --git a/Iris/Iris/HeapLang/Lib/Diverge.lean b/Iris/Iris/HeapLang/Lib/Diverge.lean new file mode 100644 index 000000000..492a5135d --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/Diverge.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ +module + +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang.Notation +public import Iris.HeapLang.Instances +public import Iris.HeapLang.PrimitiveLaws +public import Iris.HeapLang.ProofMode + +namespace Iris.HeapLang + +open BI Iris ProgramLogic + +@[expose] public section + +namespace Diverge + +@[rocq_alias heap_lang.diverge] +def diverge : Val := hl_val% + rec diverge v := diverge v + +section Spec + +variable {GF : BundledGFunctors} [HeapLangGS hlc GF] + +@[rocq_alias heap_lang.wp_diverge] +theorem wp_diverge (s : Stuckness) (E : CoPset) (Φ : Val → IProp GF) (v : Val) : + ⊢ WP hl(&diverge &v) @ s; E {{ Φ }} := by + iloeb as IH + wp_lam + iapply IH + +end Spec + +end Diverge +end diff --git a/Iris/Iris/HeapLang/Lib/Unwrap.lean b/Iris/Iris/HeapLang/Lib/Unwrap.lean new file mode 100644 index 000000000..65bae9674 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/Unwrap.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ +module + +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang.Notation +public import Iris.HeapLang.Instances +public import Iris.HeapLang.PrimitiveLaws +public import Iris.HeapLang.ProofMode +public import Iris.HeapLang.Lib.Assert + +namespace Iris.HeapLang + +open BI Iris ProgramLogic + +@[expose] public section + +namespace Unwrap + +/-- `unwrap o` unsafely asserts that `o` is `some v` and returns `v`. The +`none` case is unreachable (it aborts via `assert`). -/ +@[rocq_alias heap_lang.unwrap] +def unwrap : Val := hl_val% + λ o, + match o with + | none() => assert(#false) + | some(v) => v + +section Spec + +variable {GF : BundledGFunctors} [HeapLangGS hlc GF] + +@[rocq_alias heap_lang.unwrap_spec] +theorem unwrap_spec (Φ : Val → IProp GF) (v : Val) : + ▷ Φ v ⊢ WP hl(&unwrap v(some(&v))) {{ Φ }} := by + iintro HΦ + wp_lam + wp_pures + iapply HΦ + +end Spec + +end Unwrap +end diff --git a/Iris/Iris/HeapLang/Syntax.lean b/Iris/Iris/HeapLang/Syntax.lean index 0db3fd4a6..8b82bd62d 100644 --- a/Iris/Iris/HeapLang/Syntax.lean +++ b/Iris/Iris/HeapLang/Syntax.lean @@ -247,6 +247,7 @@ theorem Exp.stuck_subst {x v} : Exp.substStr x v Exp.stuck = Exp.stuck := by simp [Exp.stuck, Exp.substStr] simp only [substStr, ofVal] +@[rocq_alias heap_lang.assert] def Exp.assert (e : Exp) := Exp.if e (.ofVal $ .lit .unit) Exp.stuck @[simp]