From 2b88268485000a98e61d24cfde6678de06a1faf3 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Thu, 25 Sep 2025 15:53:17 +0200 Subject: [PATCH 01/12] Initial heaplang --- src/Iris.lean | 1 + src/Iris/IrisHeapLang.lean | 1 + src/Iris/IrisHeapLang/Lang.lean | 159 ++++++++++++++++++++++++++++++++ 3 files changed, 161 insertions(+) create mode 100644 src/Iris/IrisHeapLang.lean create mode 100644 src/Iris/IrisHeapLang/Lang.lean diff --git a/src/Iris.lean b/src/Iris.lean index 2bd468667..8723e2dc2 100644 --- a/src/Iris.lean +++ b/src/Iris.lean @@ -1,6 +1,7 @@ import Iris.Algebra import Iris.BI import Iris.Examples +import Iris.IrisHeapLang import Iris.Instances import Iris.ProofMode import Iris.Std diff --git a/src/Iris/IrisHeapLang.lean b/src/Iris/IrisHeapLang.lean new file mode 100644 index 000000000..dd35db81e --- /dev/null +++ b/src/Iris/IrisHeapLang.lean @@ -0,0 +1 @@ +import Iris.IrisHeapLang.Lang diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean new file mode 100644 index 000000000..0c4f11a04 --- /dev/null +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -0,0 +1,159 @@ + +namespace HeapLang + +abbrev loc := Int +abbrev ProphId := {x : Int // x ≥ 0} -- Why does Rocq Iris do this? + +inductive BaseLit where + | Int (n : Int) + | Bool (b : Bool) + | Unit + | LitPoison + | Loc (l : loc) + | Prophecy (p : ProphId) + + +-- Why are there two different ways to negate? +inductive UnOp where + | Neg + | Minus + +inductive BinOp where + | Plus + | Minus + | Mult + | Quot + | Rem + | And + | Or + | Xor + | ShiftL + | ShiftR + | Le + | Lt + | Eq + | Offset + + +inductive Binder + | BAnon + | BNamed (name : Lean.Ident) + +mutual +inductive Val where + | Lit (l : BaseLit) + | Rec (f x : Binder) (e : Expr) + | Pair (v₁ v₂ : Val) + | InjL (v : Val) + | InjR (v : Val) + +-- The comments are borrowed as is from Iris Rocq +inductive Expr where + -- values + | Val (v : Val) + -- basic lambda calculus + | Var (x : String) + | Rec (f x : Binder) (e : Expr) + | App (e₁ e₂ : Expr) + -- Base types and their operations + | Unop (op : UnOp) (e : Expr) + | Binop (op : BinOp) (e₁ e₂ : Expr) + | If (e₁ e₂ e₂ : Expr) + -- Products + | Pair (e₁ e₂ : Expr) + | Fst (e : Expr) + | Snd (e : Expr) + -- Sums + | InjL (e : Expr) + | InjR (e : Expr) + | Case (e₀ e₁ e₂ : Expr) + -- Heap + | AllocN (e₁ e₂ : Expr) -- array length (positive number), initial value + | Free (e : Expr) + | Load (e : Expr) + | Store (e₁ e₂ : Expr) + | CmpXchg (e₀ e₁ e₂ : Expr) -- Compare-exchange + | Xchg (e₀ e₁ : Expr) -- exchange + | FAA (e₁ e₂ : Expr) -- Fetch-and-add + -- Concurrency + | Fork (e : Expr) + -- Prophecy + | NewProph + | Resolve (e₀ e₁ e₂ : Expr) -- wrapped expr, proph, val +end + +def toVal (e : Expr) : Option Val := + match e with + | .Val v => some v + | _ => none + +def BaseLit.isUnboxed (l : BaseLit) := + match l with + | .Prophecy _ => False + | .LitPoison => False + | _ => True +end HeapLang + + +/- +val := + | LitV (l : base_lit) + | RecV (f x : binder) (e : expr) + | PairV (v1 v2 : val) + | InjLV (v : val) + | InjRV (v : val). +Inductive base_lit : Set := + | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitPoison + | LitLoc (l : loc) | LitProphecy (p: proph_id). +Inductive un_op : Set := + | NegOp | MinusUnOp. +Inductive bin_op : Set := + (** We use "quot" and "rem" instead of "div" and "mod" to + better match the behavior of 'real' languages: + e.g., in Rust, -30 -4 == 7. ("div" would return 8.) *) + | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *) + | AndOp | OrOp | XorOp (* Bitwise *) + | ShiftLOp | ShiftROp (* Shifts *) + | LeOp | LtOp | EqOp (* Relations *) + | OffsetOp. (* Pointer offset *) + +Inductive expr := + (* Values *) + | Val (v : val) + (* Base lambda calculus *) + | Var (x : string) + | Rec (f x : binder) (e : expr) + | App (e1 e2 : expr) + (* Base types and their operations *) + | UnOp (op : un_op) (e : expr) + | BinOp (op : bin_op) (e1 e2 : expr) + | If (e0 e1 e2 : expr) + (* Products *) + | Pair (e1 e2 : expr) + | Fst (e : expr) + | Snd (e : expr) + (* Sums *) + | InjL (e : expr) + | InjR (e : expr) + | Case (e0 : expr) (e1 : expr) (e2 : expr) + (* Heap *) + | AllocN (e1 e2 : expr) (* array length (positive number), initial value *) + | Free (e : expr) + | Load (e : expr) + | Store (e1 : expr) (e2 : expr) + | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *) + | Xchg (e0 : expr) (e1 : expr) (* exchange *) + | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *) + (* Concurrency *) + | Fork (e : expr) + (* Prophecy *) + | NewProph + | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *) +with val := + | LitV (l : base_lit) + | RecV (f x : binder) (e : expr) + | PairV (v1 v2 : val) + | InjLV (v : val) + | InjRV (v : val). + +-/ From 1607c9248025bd12f2be47452888a9e72d784354 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Thu, 25 Sep 2025 16:25:56 +0200 Subject: [PATCH 02/12] Stuck at deriving DecidableEq instances for mutually inductive Var and Expr --- src/Iris/IrisHeapLang/Lang.lean | 41 ++++++++++++++++++++++++++++++--- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 0c4f11a04..8b8587408 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -8,7 +8,7 @@ inductive BaseLit where | Int (n : Int) | Bool (b : Bool) | Unit - | LitPoison + | Poison | Loc (l : loc) | Prophecy (p : ProphId) @@ -37,7 +37,8 @@ inductive BinOp where inductive Binder | BAnon - | BNamed (name : Lean.Ident) + | BNamed (name : String) +deriving DecidableEq mutual inductive Val where @@ -47,6 +48,7 @@ inductive Val where | InjL (v : Val) | InjR (v : Val) + -- The comments are borrowed as is from Iris Rocq inductive Expr where -- values @@ -80,18 +82,51 @@ inductive Expr where -- Prophecy | NewProph | Resolve (e₀ e₁ e₂ : Expr) -- wrapped expr, proph, val + end + def toVal (e : Expr) : Option Val := match e with | .Val v => some v | _ => none +-- Defined for completeness with the Rocq version +abbrev ofVal (v : Val) : Expr := .Val v + def BaseLit.isUnboxed (l : BaseLit) := match l with | .Prophecy _ => False - | .LitPoison => False + | .Poison => False | _ => True + +def Val.isUnboxed (l : Val) := + match l with + | .Lit l => l.isUnboxed + | .InjL x => x.isUnboxed + | .InjR x => x.isUnboxed + | _ => False + +structure State where + heap : loc → Option Val + usedPropId : ProphId → Prop + +theorem toOfVal : ∀ v, toVal (ofVal v) = some v := by + intro v + simp [toVal, ofVal] + +theorem ofToVal : ∀ e : Expr, ∀ v : Val, + toVal e = some v → ofVal v = e := by + intro e v h + revert v + cases h : e <;> simp [Expr.Val, ofVal, toVal] + + + + + + + end HeapLang From 7f978e2fab529655abbc1325abbe07a4e3d8fb79 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Thu, 25 Sep 2025 17:47:12 +0200 Subject: [PATCH 03/12] Add BEq instances --- src/Iris/IrisHeapLang/Lang.lean | 75 +++++++++++++++++++++++++++++++-- 1 file changed, 71 insertions(+), 4 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 8b8587408..90945059d 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -11,12 +11,13 @@ inductive BaseLit where | Poison | Loc (l : loc) | Prophecy (p : ProphId) - +deriving DecidableEq, Inhabited -- Why are there two different ways to negate? inductive UnOp where | Neg | Minus +deriving Inhabited, DecidableEq inductive BinOp where | Plus @@ -33,7 +34,7 @@ inductive BinOp where | Lt | Eq | Offset - +deriving Inhabited, DecidableEq inductive Binder | BAnon @@ -48,7 +49,6 @@ inductive Val where | InjL (v : Val) | InjR (v : Val) - -- The comments are borrowed as is from Iris Rocq inductive Expr where -- values @@ -75,7 +75,7 @@ inductive Expr where | Load (e : Expr) | Store (e₁ e₂ : Expr) | CmpXchg (e₀ e₁ e₂ : Expr) -- Compare-exchange - | Xchg (e₀ e₁ : Expr) -- exchange + | Xchg (e₁ e₂ : Expr) -- exchange | FAA (e₁ e₂ : Expr) -- Fetch-and-add -- Concurrency | Fork (e : Expr) @@ -85,6 +85,73 @@ inductive Expr where end +instance : Inhabited Val where + default := .Lit BaseLit.Unit + +instance : Inhabited Expr where + default := .Val default + + +mutual +def valEq (v₁ v₂ : Val) : Bool := + match v₁, v₂ with + | .Lit x, .Lit y => decide (x = y) + | .InjL x, .InjL y => valEq x y + | .InjR x, .InjR y => valEq x y + | .Pair x₁ x₂, .Pair y₁ y₂ => valEq x₁ y₁ && valEq x₂ y₂ + | .Rec f₁ x₁ e₁, .Rec f₂ x₂ e₂ => decide (f₁ = f₂) && decide (x₁ = x₂) && exprEq e₁ e₂ + | _, _ => false + +def exprEq (e₁ e₂ : Expr) : Bool := + match e₁, e₂ with + | .Val v₁, .Val v₂ => valEq v₁ v₂ + | .Var x₁, .Var x₂ => decide (x₁ = x₂) + | .Rec f₁ x₁ e₁, .Rec f₂ x₂ e₂ => + decide (f₁ = f₂) + && decide (x₁ = x₂) + && exprEq e₁ e₂ + | .App e₁ f₁, .App e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .Unop op₁ e₁, .Unop op₂ e₂ => decide (op₁ = op₂) && exprEq e₁ e₂ + | .Binop op₁ e₁ f₁, .Binop op₂ e₂ f₂ => + decide (op₁ = op₂) + && exprEq e₁ e₂ + && exprEq f₁ f₂ + | .If cond₁ left₁ right₁, .If cond₂ left₂ right₂ => + exprEq cond₁ cond₂ + && exprEq left₁ left₂ + && exprEq right₁ right₂ + | .Pair e₁ f₁, .Pair e₂ f₂ => + exprEq e₁ e₂ && exprEq f₁ f₂ + | .Fst e₁, .Fst e₂ => exprEq e₁ e₂ + | .Snd e₁, .Snd e₂ => exprEq e₁ e₂ + | .InjL e₁, .InjL e₂ => exprEq e₁ e₂ + | .InjR e₁, .InjR e₂ => exprEq e₁ e₂ + | .Case e₁ f₁ g₁, .Case e₂ f₂ g₂ => exprEq e₁ e₂ && exprEq f₁ f₂ && exprEq g₁ g₂ + | .AllocN n₁ v₁, .AllocN n₂ v₂ => exprEq n₁ n₂ && exprEq v₁ v₂ + | .Free e₁, .Free e₂ => exprEq e₁ e₂ + | .Load e₁, .Load e₂ => exprEq e₁ e₂ + | .Store e₁ f₁, .Store e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .CmpXchg e₁ f₁ g₁, .CmpXchg e₂ f₂ g₂ => + exprEq e₁ e₂ + && exprEq f₁ f₂ + && exprEq g₁ g₂ + | .Xchg e₁ f₁, .Xchg e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .FAA e₁ f₁, .FAA e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .Fork e₁, .Fork e₂ => exprEq e₁ e₂ + | .NewProph, .NewProph => True + | .Resolve e₁ f₁ g₁, .Resolve e₂ f₂ g₂ => + exprEq e₁ e₂ + && exprEq f₁ f₂ + && exprEq g₁ g₂ + | _, _ => false +end + +instance : BEq Val where + beq := valEq +instance : BEq Expr where + beq := exprEq + + def toVal (e : Expr) : Option Val := match e with From 6531de0c9f2ea012c08d52811824284760eda0db Mon Sep 17 00:00:00 2001 From: Shreyas Date: Thu, 25 Sep 2025 19:01:56 +0200 Subject: [PATCH 04/12] Add DecidableEq instances --- src/Iris/IrisHeapLang/Lang.lean | 114 ++++++++++++++++++++++++++++++++ 1 file changed, 114 insertions(+) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 90945059d..2eb735b05 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -146,6 +146,120 @@ def exprEq (e₁ e₂ : Expr) : Bool := | _, _ => false end +macro "big_decide_tactic" : tactic => do + `(tactic| + all_goals + try { + apply isFalse + simp_all + } + try { + apply isTrue + simp_all + } + ) +macro "decide_tactic" : tactic => do + `(tactic| + ( + · apply isTrue + simp_all + all_goals + apply isFalse + simp_all + + ) + ) +mutual +noncomputable instance exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := by + cases e₁ <;> cases e₂ + big_decide_tactic + case Val.Val x y => + by_cases x = y + decide_tactic + case Var.Var x y => + by_cases x = y + decide_tactic + case InjL.InjL x y => + by_cases x = y + decide_tactic + case InjR.InjR x y => + by_cases x = y + decide_tactic + case Pair.Pair x₁ x₂ y₁ y₂ => + by_cases h₁ : x₁ = y₁ <;> by_cases h₂ : x₂ = y₂ + decide_tactic + case Rec.Rec f₁ x₁ e₁ f₂ x₂ e₂ => + by_cases h₁ : f₁ = f₂ <;> by_cases h₂ : x₁ = x₂ <;> by_cases h₃ : e₁ = e₂ + decide_tactic + case App.App e₁ f₁ e₂ f₂ => + by_cases h₁ : e₁ = e₂ <;> by_cases h₂ : f₁ = f₂ + decide_tactic + case Unop.Unop op₁ f₁ op₂ f₂ => + by_cases op₁ = op₂ <;> by_cases f₁ = f₂ + decide_tactic + case Binop.Binop op₁ f₁ g₁ op₂ f₂ g₂ => + by_cases op₁ = op₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ + decide_tactic + case If.If cond₁ l₁ r₁ cond₂ l₂ r₂ => + by_cases cond₁ = cond₂ <;> by_cases l₁ = l₂ <;> by_cases r₁ = r₂ + decide_tactic + case Fst.Fst e₁ e₂ => + by_cases e₁ = e₂ + decide_tactic + case Snd.Snd e₁ e₂ => + by_cases e₁ = e₂ + decide_tactic + case Case.Case c₁ f₁ g₁ c₂ f₂ g₂ => + by_cases c₁ = c₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ + decide_tactic + case AllocN.AllocN e₁ f₁ e₂ f₂ => + by_cases e₁ = e₂ <;> by_cases f₁ = f₂ + decide_tactic + case Free.Free e₁ e₂ => + by_cases e₁ = e₂ + decide_tactic + case Load.Load e₁ e₂ => + by_cases e₁ = e₂ + decide_tactic + case Store.Store f₁ e₁ f₂ e₂ => + by_cases f₁ = f₂ <;> by_cases e₁ = e₂ + decide_tactic + case CmpXchg.CmpXchg e₁ f₁ g₁ e₂ f₂ g₂ => + by_cases e₁ = e₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ + decide_tactic + case Xchg.Xchg e₁ f₁ e₂ f₂ => + by_cases e₁ = e₂ <;> by_cases f₁ = f₂ + decide_tactic + case FAA.FAA e₁ f₁ e₂ f₂ => + by_cases e₁ = e₂ <;> by_cases f₁ = f₂ + decide_tactic + case Fork.Fork e₁ e₂ => + by_cases e₁ = e₂ + decide_tactic + case Resolve e₁ f₁ g₁ e₂ f₂ g₂ => + by_cases e₁ = e₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ + decide_tactic + +noncomputable instance valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := by + cases v₁ <;> cases v₂ + big_decide_tactic + case Lit.Lit x y => + by_cases x = y + decide_tactic + case InjL.InjL x y => + by_cases x = y + decide_tactic + case InjR.InjR x y => + by_cases x = y + decide_tactic + case Pair.Pair x₁ x₂ y₁ y₂ => + by_cases x₁ = y₁ <;> by_cases x₂ = y₂ + decide_tactic + case Rec.Rec f₁ x₁ e₁ f₂ x₂ e₂ => + by_cases f₁ = f₂ <;> by_cases x₁ = x₂ <;> by_cases e₁ = e₂ + decide_tactic + +end instance : BEq Val where beq := valEq instance : BEq Expr where From 21c3a191d6db6caf598bca1aae5d3713e33a4cf0 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Thu, 25 Sep 2025 19:56:38 +0200 Subject: [PATCH 05/12] trivial context stuff. Context and context item --- src/Iris/IrisHeapLang/Lang.lean | 139 ++++++++++++++++---------------- 1 file changed, 68 insertions(+), 71 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 2eb735b05..0a0b67ec4 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -145,7 +145,10 @@ def exprEq (e₁ e₂ : Expr) : Bool := && exprEq g₁ g₂ | _, _ => false end - +instance : BEq Val where + beq := valEq +instance : BEq Expr where + beq := exprEq macro "big_decide_tactic" : tactic => do `(tactic| all_goals @@ -260,10 +263,7 @@ noncomputable instance valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := b decide_tactic end -instance : BEq Val where - beq := valEq -instance : BEq Expr where - beq := exprEq + @@ -303,73 +303,70 @@ theorem ofToVal : ∀ e : Expr, ∀ v : Val, cases h : e <;> simp [Expr.Val, ofVal, toVal] - - +inductive ECtxItem where + | AppL (v₂ : Val) + | AppR (e₁ : Expr) + | Unop (op : UnOp) + | BinopL (op : BinOp) (v₂ : Val) + | BinopR (op : BinOp) (e₁ : Expr) + | If (e₁ e₂ : Expr) + | PairL (v₂ : Val) + | PairR (e₁ : Expr) + | Fst + | Snd + | InjL + | InjR + | Case (e₁ e₂ : Expr) + | AllocNL (v₂ : Val) + | AllocNR (e₁ : Expr) + | Free + | Load + | StoreL (v₂ : Val) + | StoreR (e₁ : Expr) + | XchgL (v₂ : Val) + | XchgR (e₁ : Expr) + | CmpXchgL (v₁ v₂ : Val) + | CmpXchgM (e₀ : Expr) (v₂ : Val) + | CmpXchgR (e₀ e₁ : Expr) + | FaaL (v₂ : Val) + | FaaR (e₁ : Expr) + | ResolveL (ctx : ECtxItem) (v₁ v₂ : Val) + | ResolveM (e₀ : Expr) (v₂ : Val) + | ResolveR (e₀ e₁ : Expr) + + +def FillItem (Ki : ECtxItem) (e : Expr) : Expr := + match Ki with + | .AppL v₂ => .App e (ofVal v₂) + | .AppR e₁ => .App e₁ e + | .Unop op => .Unop op e + | .BinopL op v₂ => .Binop op e (.Val v₂) + | .BinopR op e₁ => .Binop op e₁ e + | .If e₁ e₂ => .If e e₁ e₂ + | .PairL v₂ => .Pair e (.Val v₂) + | .PairR e₁ => .Pair e₁ e + | .Fst => .Fst e + | .Snd => .Snd e + | .InjL => .InjL e + | .InjR => .InjR e + | .Case e₁ e₂ => .Case e e₁ e₂ + | .AllocNL v₂ => .AllocN e (.Val v₂) + | .AllocNR e₁ => .AllocN e₁ e + | .Free => .Free e + | .Load => .Load e + | .StoreL v₂ => .Store e (.Val v₂) + | .StoreR e₁ => .Store e₁ e + | .XchgL v₂ => .Xchg e (.Val v₂) + | .XchgR e₁ => .Xchg e₁ e + | .CmpXchgL v₁ v₂ => .CmpXchg e (.Val v₁) (.Val v₂) + | .CmpXchgM e₀ v₂ => .CmpXchg e₀ e (.Val v₂) + | .CmpXchgR e₀ e₁ => .CmpXchg e₀ e₁ e + | .FaaL v₂ => .FAA e (.Val v₂) + | .FaaR e₁ => .FAA e₁ e + | .ResolveL K v₁ v₂ => .Resolve (FillItem K e) (.Val v₁) (.Val v₂) + | .ResolveM ex v₂ => .Resolve ex e (.Val v₂) + | .ResolveR ex e₁ => .Resolve ex e₁ e end HeapLang - - -/- -val := - | LitV (l : base_lit) - | RecV (f x : binder) (e : expr) - | PairV (v1 v2 : val) - | InjLV (v : val) - | InjRV (v : val). -Inductive base_lit : Set := - | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitPoison - | LitLoc (l : loc) | LitProphecy (p: proph_id). -Inductive un_op : Set := - | NegOp | MinusUnOp. -Inductive bin_op : Set := - (** We use "quot" and "rem" instead of "div" and "mod" to - better match the behavior of 'real' languages: - e.g., in Rust, -30 -4 == 7. ("div" would return 8.) *) - | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *) - | AndOp | OrOp | XorOp (* Bitwise *) - | ShiftLOp | ShiftROp (* Shifts *) - | LeOp | LtOp | EqOp (* Relations *) - | OffsetOp. (* Pointer offset *) - -Inductive expr := - (* Values *) - | Val (v : val) - (* Base lambda calculus *) - | Var (x : string) - | Rec (f x : binder) (e : expr) - | App (e1 e2 : expr) - (* Base types and their operations *) - | UnOp (op : un_op) (e : expr) - | BinOp (op : bin_op) (e1 e2 : expr) - | If (e0 e1 e2 : expr) - (* Products *) - | Pair (e1 e2 : expr) - | Fst (e : expr) - | Snd (e : expr) - (* Sums *) - | InjL (e : expr) - | InjR (e : expr) - | Case (e0 : expr) (e1 : expr) (e2 : expr) - (* Heap *) - | AllocN (e1 e2 : expr) (* array length (positive number), initial value *) - | Free (e : expr) - | Load (e : expr) - | Store (e1 : expr) (e2 : expr) - | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *) - | Xchg (e0 : expr) (e1 : expr) (* exchange *) - | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *) - (* Concurrency *) - | Fork (e : expr) - (* Prophecy *) - | NewProph - | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *) -with val := - | LitV (l : base_lit) - | RecV (f x : binder) (e : expr) - | PairV (v1 v2 : val) - | InjLV (v : val) - | InjRV (v : val). - --/ From 8d6b9d69028dcd862c7b0d297eac429849c97f53 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Fri, 26 Sep 2025 10:27:30 +0200 Subject: [PATCH 06/12] Need mathlib bitwise defs for int --- src/Iris/IrisHeapLang/Lang.lean | 57 +++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 0a0b67ec4..440fbdfd5 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -367,6 +367,63 @@ def FillItem (Ki : ECtxItem) (e : Expr) : Expr := | .ResolveM ex v₂ => .Resolve ex e (.Val v₂) | .ResolveR ex e₁ => .Resolve ex e₁ e +-- Substitution +def subst (x : String) (v : Val) (e : Expr) : Expr := + match e with + | .Val _ => e + | .Var y => if decide (x = y) then .Val v else .Var y + | .Rec f y e => + .Rec f y $ if decide (.BNamed x ≠ f ∧ .BNamed x ≠ y) then subst x v e else e + | .App e₁ e₂ => .App (subst x v e₁) (subst x v e₂) + | .Unop op e => .Unop op (subst x v e) + | .Binop op e₁ e₂ => .Binop op (subst x v e₁) (subst x v e₂) + | .If e₀ e₁ e₂ => .If (subst x v e₀) (subst x v e₁) (subst x v e₂) + | .Pair e₁ e₂ => .Pair (subst x v e₁) (subst x v e₂) + | .Fst e => .Fst (subst x v e) + | .Snd e => .Snd (subst x v e) + | .InjL e => .InjL (subst x v e) + | .InjR e => .InjR (subst x v e) + | .Case e₀ e₁ e₂ => .Case (subst x v e₀) (subst x v e₁) (subst x v e₂) + | .AllocN e₁ e₂ => .AllocN (subst x v e₁) (subst x v e₂) + | .Free e => .Free (subst x v e) + | .Load e => .Load (subst x v e) + | .Xchg e₁ e₂ => .Xchg (subst x v e₁) (subst x v e₂) + | .Store e₁ e₂ => .Store (subst x v e₁) (subst x v e₂) + | .CmpXchg e₀ e₁ e₂ => .CmpXchg (subst x v e₀) (subst x v e₁) (subst x v e₂) + | .FAA e₁ e₂ => .FAA (subst x v e₁) (subst x v e₂) + | .Fork e => .Fork (subst x v e) + | .NewProph => .NewProph + | .Resolve ex e₁ e₂ => .Resolve (subst x v ex) (subst x v e₁) (subst x v e₂) + +def subst' (mx : Binder) (v : Val) : Expr → Expr := + match mx with + | .BNamed x => subst x v + | .BAnon => id + +def unOpEval (op : UnOp) (v : Val) : Option Val := + match op, v with + | .Neg, .Lit (.Bool b) => some $ .Lit $ .Bool (not b) + | .Neg, .Lit (.Int n) => some $ .Lit $ .Int (Int.not n) -- find a lean equivalent here + | .Minus, .Lit (.Int n) => some $ .Lit $ .Int (- n) + | _, _ => none + + +def binOpEvalInt (op : BinOp) (n₁ n₂ : Int) : Option BaseLit := + match op with + | .Plus => some $ .Int (n₁ + n₂) + | .Minus => some $ .Int (n₁ - n₂) + | .Mult => some $ .Int (n₁ * n₂) + | .Quot => some $ .Int (n₁ / n₂) + | .Rem => some $ .Int (n₁ % n₂) + | .And => some $ .Int (n₁ &&& n₂) -- need the mathlib bitwise defs + | .Or => some $ .Int (n₁ ||| n₂) + | .Xor => some $ .Int (Int.xor n₁ n₂) + | .ShiftL => some $ .Int (n₁ <<< n₂) + | .ShiftR => some $ .Int (n₁ >>> n₂) + | .Le => some $ .Bool (decide (n₁ ≤ n₂)) + | .Lt => some $ .Bool (decide (n₁ < n₂)) + | .Eq => some $ .Bool (decide (n₁ = n₂)) + | .Offset => none end HeapLang From 39298779dfe2f25ec147e9ea6b2fae48c25b2247 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Fri, 26 Sep 2025 14:31:40 +0200 Subject: [PATCH 07/12] Remove comment which is incorrect now --- src/Iris/IrisHeapLang/Lang.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 440fbdfd5..b4825f479 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -403,7 +403,7 @@ def subst' (mx : Binder) (v : Val) : Expr → Expr := def unOpEval (op : UnOp) (v : Val) : Option Val := match op, v with | .Neg, .Lit (.Bool b) => some $ .Lit $ .Bool (not b) - | .Neg, .Lit (.Int n) => some $ .Lit $ .Int (Int.not n) -- find a lean equivalent here + | .Neg, .Lit (.Int n) => some $ .Lit $ .Int (Int.not n) | .Minus, .Lit (.Int n) => some $ .Lit $ .Int (- n) | _, _ => none From 48c1adaf824cb9236b2e430c92bf514d0f6ddc3c Mon Sep 17 00:00:00 2001 From: Shreyas Date: Sat, 27 Sep 2025 00:19:14 +0200 Subject: [PATCH 08/12] Some stuff --- src/Iris/IrisHeapLang/Lang.lean | 81 ++++++++++++++++++++++++++++----- 1 file changed, 70 insertions(+), 11 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index b4825f479..c3b8f1505 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -1,7 +1,13 @@ +import Std namespace HeapLang -abbrev loc := Int +abbrev Loc := Int + +instance : Inhabited (Loc) := inferInstance +instance : BEq (Loc) := inferInstance +instance : DecidableEq (Loc) := inferInstance + abbrev ProphId := {x : Int // x ≥ 0} -- Why does Rocq Iris do this? inductive BaseLit where @@ -9,7 +15,7 @@ inductive BaseLit where | Bool (b : Bool) | Unit | Poison - | Loc (l : loc) + | Loc (l : Loc) | Prophecy (p : ProphId) deriving DecidableEq, Inhabited @@ -145,10 +151,13 @@ def exprEq (e₁ e₂ : Expr) : Bool := && exprEq g₁ g₂ | _, _ => false end + instance : BEq Val where beq := valEq + instance : BEq Expr where beq := exprEq + macro "big_decide_tactic" : tactic => do `(tactic| all_goals @@ -288,9 +297,6 @@ def Val.isUnboxed (l : Val) := | .InjR x => x.isUnboxed | _ => False -structure State where - heap : loc → Option Val - usedPropId : ProphId → Prop theorem toOfVal : ∀ v, toVal (ofVal v) = some v := by intro v @@ -403,7 +409,7 @@ def subst' (mx : Binder) (v : Val) : Expr → Expr := def unOpEval (op : UnOp) (v : Val) : Option Val := match op, v with | .Neg, .Lit (.Bool b) => some $ .Lit $ .Bool (not b) - | .Neg, .Lit (.Int n) => some $ .Lit $ .Int (Int.not n) + | .Neg, .Lit (.Int n) => some $ .Lit $ .Int (Int.not n) | .Minus, .Lit (.Int n) => some $ .Lit $ .Int (- n) | _, _ => none @@ -415,15 +421,68 @@ def binOpEvalInt (op : BinOp) (n₁ n₂ : Int) : Option BaseLit := | .Mult => some $ .Int (n₁ * n₂) | .Quot => some $ .Int (n₁ / n₂) | .Rem => some $ .Int (n₁ % n₂) - | .And => some $ .Int (n₁ &&& n₂) -- need the mathlib bitwise defs - | .Or => some $ .Int (n₁ ||| n₂) - | .Xor => some $ .Int (Int.xor n₁ n₂) - | .ShiftL => some $ .Int (n₁ <<< n₂) - | .ShiftR => some $ .Int (n₁ >>> n₂) + | .And => sorry -- some $ .Int (n₁ &&& n₂) -- need the mathlib bitwise defs + | .Or => sorry -- some $ .Int (n₁ ||| n₂) + | .Xor => sorry -- some $ .Int (Int.xor n₁ n₂) + | .ShiftL => sorry -- some $ .Int (n₁ <<< n₂) + | .ShiftR => sorry -- some $ .Int (n₁ >>> n₂) | .Le => some $ .Bool (decide (n₁ ≤ n₂)) | .Lt => some $ .Bool (decide (n₁ < n₂)) | .Eq => some $ .Bool (decide (n₁ = n₂)) | .Offset => none +def binOpEvalBool (op : BinOp) (b₁ b₂ : Bool) : Option BaseLit := + match op with + | .Plus | .Minus | .Mult | .Quot | .Rem => none -- (* Arithmetic *) + | .And => some <| .Bool <| b₁ && b₂ + | .Or => some <| .Bool <| b₁ || b₂ + | .Xor => some <| .Bool <| xor b₁ b₂ + | .ShiftL | .ShiftR => none -- (* Shifts *) + | .Le | .Lt => none -- (* InEquality *) + | .Eq => some <| .Bool <| decide (b₁ = b₂) + | .Offset => none + +def binOpEvalLoc (op : BinOp) (l₁ : Loc) (v₂ : BaseLit) : Option BaseLit := + match op, v₂ with + | .Offset, .Int offset => some <| .Loc (l₁ + offset) + | .Le, .Loc l₂ => some <| .Bool (decide (l₁ ≤ l₂)) + | .Lt, .Loc l₂ => some $ .Bool (decide (l₁ < l₂)) + | _, _ => none + +def valsCompareSafe (vl v₁ : Val) : Prop := + Val.isUnboxed vl ∨ Val.isUnboxed v₁ + + +-- Replace this with a proper decidable instance later. +open Classical in +noncomputable def binOpEval (op : BinOp) (v₁ v₂ : Val) : Option Val := + if decide (op = .Eq) then + if decide (valsCompareSafe v₁ v₂) then + some <| .Lit <| .Bool <| decide (v₁ = v₂) + else + none + else + match v₁, v₂ with + | .Lit (.Int n₁), .Lit (.Int n₂) => do + let val ← binOpEvalInt op n₁ n₂ + return .Lit <| val + | .Lit (.Bool b₁), .Lit (.Bool b₂) => do + let val ← binOpEvalBool op b₁ b₂ + return .Lit <| val + | .Lit (.Loc l₁), .Lit v₂ => do + let val ← binOpEvalLoc op l₁ v₂ + return .Lit <| val + | _, _ => none + + +structure State where + heap : Loc → Option Val + usedProphId : ProphId → Prop + +def stateUpdHeap + (update: (Loc → Option Val) → (Loc → Option Val)) + (σ: State) : State where + heap := update σ.heap + usedProphId := σ.usedProphId end HeapLang From f02162f95d598a433317f8dc76d78b4c6614055c Mon Sep 17 00:00:00 2001 From: Shreyas Date: Tue, 2 Dec 2025 14:36:10 +0100 Subject: [PATCH 09/12] Start again from here --- src/Iris/IrisHeapLang/Lang.lean | 151 +++++++++++++++++++++++++++++++- 1 file changed, 149 insertions(+), 2 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index c3b8f1505..89c5f2941 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -19,12 +19,16 @@ inductive BaseLit where | Prophecy (p : ProphId) deriving DecidableEq, Inhabited +abbrev iDecEqBaseLit := instDecidableEqBaseLit + -- Why are there two different ways to negate? inductive UnOp where | Neg | Minus deriving Inhabited, DecidableEq +abbrev iDecEqUnOp := instDecidableEqUnOp + inductive BinOp where | Plus | Minus @@ -42,10 +46,14 @@ inductive BinOp where | Offset deriving Inhabited, DecidableEq +abbrev iDecEqBinOp := instDecidableEqBinOp + inductive Binder | BAnon | BNamed (name : String) -deriving DecidableEq +deriving DecidableEq, Inhabited + +abbrev iDecEqBinder := instDecidableEqBinder mutual inductive Val where @@ -97,7 +105,6 @@ instance : Inhabited Val where instance : Inhabited Expr where default := .Val default - mutual def valEq (v₁ v₂ : Val) : Bool := match v₁, v₂ with @@ -152,12 +159,152 @@ def exprEq (e₁ e₂ : Expr) : Bool := | _, _ => false end + +example (v₁ v₂ : Val) : Val.InjL v₁ ≠ Val.InjR v₂ := by + apply Val.noConfusion +mutual +def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := + match v₁, v₂ with + | .Lit x, .Lit y => + let h := iDecEqBaseLit x y + match h with + | .isTrue p => isTrue (by congr) + | .isFalse p => isFalse (by simp [p]) + | .InjL x, .InjL y => + let h := valDecEq x y + match h with + | .isTrue p => isTrue (by simp_all) + | .isFalse p => isFalse (by simp_all) + | .InjR x, .InjR y => + match (valDecEq x y) with + | .isTrue p => isTrue (by simp_all) + | .isFalse p => isFalse (by simp_all) + | .Pair x₁ x₂, .Pair y₁ y₂ => + match hh : (valDecEq x₁ y₁), (valDecEq x₂ y₂) with + | .isTrue p₁, .isTrue p₂ => isTrue (by simp [p₁, p₂]) + | .isTrue p₁, .isFalse p₂ + | .isFalse p₁, .isTrue p₂ + | .isFalse p₁, .isFalse p₂ => + .isFalse (by simp[p₁,p₂]) + | .Rec f₁ x₁ e₁, .Rec f₂ x₂ e₂ => + match hf : (iDecEqBinder f₁ f₂), hx : (iDecEqBinder x₁ x₂), he : (exprDecEq e₁ e₂) with + | .isTrue pf, .isTrue px, .isTrue pe => .isTrue (by simp [pf, px, pe]) + | f, x, e => + have h : f ≠ isTrue _ ∨ x ≠ isTrue _ ∨ e ≠ isTrue _ := by + simp[hf, hx, he] + + .isFalse (by + intro h' + cases h' + + <;> simp_all[h]) + | .Lit _, .InjL _ + | .Lit _, .InjR _ + | .Lit _, .Pair _ _ + | .Lit _, .Rec _ _ _ + | .InjL _, .Lit _ + | .InjL _, .InjR _ + | .InjL _, .Pair _ _ + | .InjL _, .Rec _ _ _ + | .InjR _, .InjL _ + | .InjR _, .Lit _ + | .InjR _, .Pair _ _ + | .InjR _, .Rec _ _ _ + | .Pair _ _, .InjL _ + | .Pair _ _, .InjR _ + | .Pair _ _, .Lit _ + | .Pair _ _, .Rec _ _ _ + | .Rec _ _ _, .InjL _ + | .Rec _ _ _, .InjR _ + | .Rec _ _ _, .Pair _ _ + | .Rec _ _ _, .Lit _ => + .isFalse (by simp_all) + + + +def exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := + match e₁, e₂ with + | .Val v₁, .Val v₂ => + match valDecEq v₁ v₂ with + | isTrue p => isTrue (by simp[p]) + | isFalse p => isFalse (by simp[p]) + | .Var x₁, .Var x₂ => + match instDecidableEqString x₁ x₂ with + | .isTrue p => isTrue (by congr) + | .isFalse p => isFalse (by simp [p]) + | .Rec f₁ x₁ e₁, .Rec f₂ x₂ e₂ => + match iDecEqBinder f₁ f₂, iDecEqBinder x₁ x₂, exprDecEq e₁ e₂ with + | .isTrue _, isTrue _, isTrue _ => isTrue (by simp_all) + | .isTrue _, .isTrue _, .isFalse _ + | .isTrue _, .isFalse _, .isTrue _ + | .isTrue _, .isFalse _, .isFalse _ + | .isFalse _, .isTrue _, .isTrue _ + | .isFalse _, .isTrue _, .isFalse _ + | .isFalse _, .isFalse _, .isTrue _ + | .isFalse _, .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .App e₁ f₁, .App e₂ f₂ => + match h1 : exprDecEq e₁ e₂, h2: exprDecEq f₁ f₂ with + | isTrue _, isTrue _ => isTrue (by simp_all) + | he, hf => + have h : exprDecEq e₁ e₂ ≠ isTrue _ ∨ exprDecEq f₁ f₂ ≠ isTrue _ := by + cases + simp [h1, h2] + intro h' + + isFalse (by + cases he + <;> cases hf + <;> simp_all [h1, h2] + ) + | .Unop op₁ e₁, .Unop op₂ e₂ => + match (iDecEqUnOp op₁ op₂), (exprDecEq e₁ e₂) with + | .isTrue hop, .isTrue he => .isTrue (by simp [hop, he]) + | .isTrue _, .isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, isFalse _ => isFalse (by simp_all) + | .Binop op₁ e₁ f₁, .Binop op₂ e₂ f₂ => + decide (op₁ = op₂) + && exprEq e₁ e₂ + && exprEq f₁ f₂ + | .If cond₁ left₁ right₁, .If cond₂ left₂ right₂ => + exprEq cond₁ cond₂ + && exprEq left₁ left₂ + && exprEq right₁ right₂ + | .Pair e₁ f₁, .Pair e₂ f₂ => + exprEq e₁ e₂ && exprEq f₁ f₂ + | .Fst e₁, .Fst e₂ => exprEq e₁ e₂ + | .Snd e₁, .Snd e₂ => exprEq e₁ e₂ + | .InjL e₁, .InjL e₂ => exprEq e₁ e₂ + | .InjR e₁, .InjR e₂ => exprEq e₁ e₂ + | .Case e₁ f₁ g₁, .Case e₂ f₂ g₂ => exprEq e₁ e₂ && exprEq f₁ f₂ && exprEq g₁ g₂ + | .AllocN n₁ v₁, .AllocN n₂ v₂ => exprEq n₁ n₂ && exprEq v₁ v₂ + | .Free e₁, .Free e₂ => exprEq e₁ e₂ + | .Load e₁, .Load e₂ => exprEq e₁ e₂ + | .Store e₁ f₁, .Store e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .CmpXchg e₁ f₁ g₁, .CmpXchg e₂ f₂ g₂ => + exprEq e₁ e₂ + && exprEq f₁ f₂ + && exprEq g₁ g₂ + | .Xchg e₁ f₁, .Xchg e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .FAA e₁ f₁, .FAA e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + | .Fork e₁, .Fork e₂ => exprEq e₁ e₂ + | .NewProph, .NewProph => True + | .Resolve e₁ f₁ g₁, .Resolve e₂ f₂ g₂ => + exprEq e₁ e₂ + && exprEq f₁ f₂ + && exprEq g₁ g₂ + | _, _ => false +end + + instance : BEq Val where beq := valEq instance : BEq Expr where beq := exprEq + + macro "big_decide_tactic" : tactic => do `(tactic| all_goals From c438f2258cfac11911008a7c9d5cbe5a439be885 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Tue, 2 Dec 2025 14:51:07 +0100 Subject: [PATCH 10/12] Changed the dec instance. Next : Fix the val decEq definition --- src/Iris/IrisHeapLang/Lang.lean | 237 ++++++++++++++++---------------- 1 file changed, 118 insertions(+), 119 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 89c5f2941..5fccacc07 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -38,12 +38,10 @@ inductive BinOp where | And | Or | Xor - | ShiftL - | ShiftR | Le | Lt | Eq - | Offset + deriving Inhabited, DecidableEq abbrev iDecEqBinOp := instDecidableEqBinOp @@ -162,6 +160,7 @@ end example (v₁ v₂ : Val) : Val.InjL v₁ ≠ Val.InjR v₂ := by apply Val.noConfusion + mutual def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := match v₁, v₂ with @@ -196,7 +195,6 @@ def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := .isFalse (by intro h' cases h' - <;> simp_all[h]) | .Lit _, .InjL _ | .Lit _, .InjR _ @@ -247,7 +245,7 @@ def exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := | isTrue _, isTrue _ => isTrue (by simp_all) | he, hf => have h : exprDecEq e₁ e₂ ≠ isTrue _ ∨ exprDecEq f₁ f₂ ≠ isTrue _ := by - cases + cases simp [h1, h2] intro h' @@ -305,120 +303,121 @@ instance : BEq Expr where -macro "big_decide_tactic" : tactic => do - `(tactic| - all_goals - try { - apply isFalse - simp_all - } - try { - apply isTrue - simp_all - } - ) -macro "decide_tactic" : tactic => do - `(tactic| - ( - · apply isTrue - simp_all - all_goals - apply isFalse - simp_all - - ) - ) -mutual -noncomputable instance exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := by - cases e₁ <;> cases e₂ - big_decide_tactic - case Val.Val x y => - by_cases x = y - decide_tactic - case Var.Var x y => - by_cases x = y - decide_tactic - case InjL.InjL x y => - by_cases x = y - decide_tactic - case InjR.InjR x y => - by_cases x = y - decide_tactic - case Pair.Pair x₁ x₂ y₁ y₂ => - by_cases h₁ : x₁ = y₁ <;> by_cases h₂ : x₂ = y₂ - decide_tactic - case Rec.Rec f₁ x₁ e₁ f₂ x₂ e₂ => - by_cases h₁ : f₁ = f₂ <;> by_cases h₂ : x₁ = x₂ <;> by_cases h₃ : e₁ = e₂ - decide_tactic - case App.App e₁ f₁ e₂ f₂ => - by_cases h₁ : e₁ = e₂ <;> by_cases h₂ : f₁ = f₂ - decide_tactic - case Unop.Unop op₁ f₁ op₂ f₂ => - by_cases op₁ = op₂ <;> by_cases f₁ = f₂ - decide_tactic - case Binop.Binop op₁ f₁ g₁ op₂ f₂ g₂ => - by_cases op₁ = op₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ - decide_tactic - case If.If cond₁ l₁ r₁ cond₂ l₂ r₂ => - by_cases cond₁ = cond₂ <;> by_cases l₁ = l₂ <;> by_cases r₁ = r₂ - decide_tactic - case Fst.Fst e₁ e₂ => - by_cases e₁ = e₂ - decide_tactic - case Snd.Snd e₁ e₂ => - by_cases e₁ = e₂ - decide_tactic - case Case.Case c₁ f₁ g₁ c₂ f₂ g₂ => - by_cases c₁ = c₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ - decide_tactic - case AllocN.AllocN e₁ f₁ e₂ f₂ => - by_cases e₁ = e₂ <;> by_cases f₁ = f₂ - decide_tactic - case Free.Free e₁ e₂ => - by_cases e₁ = e₂ - decide_tactic - case Load.Load e₁ e₂ => - by_cases e₁ = e₂ - decide_tactic - case Store.Store f₁ e₁ f₂ e₂ => - by_cases f₁ = f₂ <;> by_cases e₁ = e₂ - decide_tactic - case CmpXchg.CmpXchg e₁ f₁ g₁ e₂ f₂ g₂ => - by_cases e₁ = e₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ - decide_tactic - case Xchg.Xchg e₁ f₁ e₂ f₂ => - by_cases e₁ = e₂ <;> by_cases f₁ = f₂ - decide_tactic - case FAA.FAA e₁ f₁ e₂ f₂ => - by_cases e₁ = e₂ <;> by_cases f₁ = f₂ - decide_tactic - case Fork.Fork e₁ e₂ => - by_cases e₁ = e₂ - decide_tactic - case Resolve e₁ f₁ g₁ e₂ f₂ g₂ => - by_cases e₁ = e₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ - decide_tactic - -noncomputable instance valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := by - cases v₁ <;> cases v₂ - big_decide_tactic - case Lit.Lit x y => - by_cases x = y - decide_tactic - case InjL.InjL x y => - by_cases x = y - decide_tactic - case InjR.InjR x y => - by_cases x = y - decide_tactic - case Pair.Pair x₁ x₂ y₁ y₂ => - by_cases x₁ = y₁ <;> by_cases x₂ = y₂ - decide_tactic - case Rec.Rec f₁ x₁ e₁ f₂ x₂ e₂ => - by_cases f₁ = f₂ <;> by_cases x₁ = x₂ <;> by_cases e₁ = e₂ - decide_tactic - -end +-- macro "big_decide_tactic" : tactic => do +-- `(tactic| +-- all_goals +-- try { +-- apply isFalse +-- simp_all +-- } +-- try { +-- apply isTrue +-- simp_all +-- } +-- ) +-- macro "decide_tactic" : tactic => do +-- `(tactic| +-- ( +-- · apply isTrue +-- simp_all +-- all_goals +-- apply isFalse +-- simp_all + +-- ) +-- ) + +-- mutual +-- noncomputable instance exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := by +-- cases e₁ <;> cases e₂ +-- big_decide_tactic +-- case Val.Val x y => +-- by_cases x = y +-- decide_tactic +-- case Var.Var x y => +-- by_cases x = y +-- decide_tactic +-- case InjL.InjL x y => +-- by_cases x = y +-- decide_tactic +-- case InjR.InjR x y => +-- by_cases x = y +-- decide_tactic +-- case Pair.Pair x₁ x₂ y₁ y₂ => +-- by_cases h₁ : x₁ = y₁ <;> by_cases h₂ : x₂ = y₂ +-- decide_tactic +-- case Rec.Rec f₁ x₁ e₁ f₂ x₂ e₂ => +-- by_cases h₁ : f₁ = f₂ <;> by_cases h₂ : x₁ = x₂ <;> by_cases h₃ : e₁ = e₂ +-- decide_tactic +-- case App.App e₁ f₁ e₂ f₂ => +-- by_cases h₁ : e₁ = e₂ <;> by_cases h₂ : f₁ = f₂ +-- decide_tactic +-- case Unop.Unop op₁ f₁ op₂ f₂ => +-- by_cases op₁ = op₂ <;> by_cases f₁ = f₂ +-- decide_tactic +-- case Binop.Binop op₁ f₁ g₁ op₂ f₂ g₂ => +-- by_cases op₁ = op₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ +-- decide_tactic +-- case If.If cond₁ l₁ r₁ cond₂ l₂ r₂ => +-- by_cases cond₁ = cond₂ <;> by_cases l₁ = l₂ <;> by_cases r₁ = r₂ +-- decide_tactic +-- case Fst.Fst e₁ e₂ => +-- by_cases e₁ = e₂ +-- decide_tactic +-- case Snd.Snd e₁ e₂ => +-- by_cases e₁ = e₂ +-- decide_tactic +-- case Case.Case c₁ f₁ g₁ c₂ f₂ g₂ => +-- by_cases c₁ = c₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ +-- decide_tactic +-- case AllocN.AllocN e₁ f₁ e₂ f₂ => +-- by_cases e₁ = e₂ <;> by_cases f₁ = f₂ +-- decide_tactic +-- case Free.Free e₁ e₂ => +-- by_cases e₁ = e₂ +-- decide_tactic +-- case Load.Load e₁ e₂ => +-- by_cases e₁ = e₂ +-- decide_tactic +-- case Store.Store f₁ e₁ f₂ e₂ => +-- by_cases f₁ = f₂ <;> by_cases e₁ = e₂ +-- decide_tactic +-- case CmpXchg.CmpXchg e₁ f₁ g₁ e₂ f₂ g₂ => +-- by_cases e₁ = e₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ +-- decide_tactic +-- case Xchg.Xchg e₁ f₁ e₂ f₂ => +-- by_cases e₁ = e₂ <;> by_cases f₁ = f₂ +-- decide_tactic +-- case FAA.FAA e₁ f₁ e₂ f₂ => +-- by_cases e₁ = e₂ <;> by_cases f₁ = f₂ +-- decide_tactic +-- case Fork.Fork e₁ e₂ => +-- by_cases e₁ = e₂ +-- decide_tactic +-- case Resolve e₁ f₁ g₁ e₂ f₂ g₂ => +-- by_cases e₁ = e₂ <;> by_cases f₁ = f₂ <;> by_cases g₁ = g₂ +-- decide_tactic + +-- noncomputable instance valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := by +-- cases v₁ <;> cases v₂ +-- big_decide_tactic +-- case Lit.Lit x y => +-- by_cases x = y +-- decide_tactic +-- case InjL.InjL x y => +-- by_cases x = y +-- decide_tactic +-- case InjR.InjR x y => +-- by_cases x = y +-- decide_tactic +-- case Pair.Pair x₁ x₂ y₁ y₂ => +-- by_cases x₁ = y₁ <;> by_cases x₂ = y₂ +-- decide_tactic +-- case Rec.Rec f₁ x₁ e₁ f₂ x₂ e₂ => +-- by_cases f₁ = f₂ <;> by_cases x₁ = x₂ <;> by_cases e₁ = e₂ +-- decide_tactic + +-- end From e0457465375dff751b9c4d04f3028a3715f46af9 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Tue, 2 Dec 2025 14:54:24 +0100 Subject: [PATCH 11/12] Only decEq fix for now --- src/Iris/IrisHeapLang/Lang.lean | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index 5fccacc07..c1adf8d47 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -41,7 +41,7 @@ inductive BinOp where | Le | Lt | Eq - + | Offset deriving Inhabited, DecidableEq abbrev iDecEqBinOp := instDecidableEqBinOp @@ -160,7 +160,6 @@ end example (v₁ v₂ : Val) : Val.InjL v₁ ≠ Val.InjR v₂ := by apply Val.noConfusion - mutual def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := match v₁, v₂ with @@ -195,6 +194,7 @@ def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := .isFalse (by intro h' cases h' + <;> simp_all[h]) | .Lit _, .InjL _ | .Lit _, .InjR _ @@ -326,7 +326,6 @@ instance : BEq Expr where -- ) -- ) - -- mutual -- noncomputable instance exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := by -- cases e₁ <;> cases e₂ @@ -524,8 +523,7 @@ def subst (x : String) (v : Val) (e : Expr) : Expr := match e with | .Val _ => e | .Var y => if decide (x = y) then .Val v else .Var y - | .Rec f y e => - .Rec f y $ if decide (.BNamed x ≠ f ∧ .BNamed x ≠ y) then subst x v e else e + | .Rec f y e => .Rec f y $ if decide (.BNamed x ≠ f ∧ .BNamed x ≠ y) then subst x v e else e | .App e₁ e₂ => .App (subst x v e₁) (subst x v e₂) | .Unop op e => .Unop op (subst x v e) | .Binop op e₁ e₂ => .Binop op (subst x v e₁) (subst x v e₂) @@ -567,11 +565,10 @@ def binOpEvalInt (op : BinOp) (n₁ n₂ : Int) : Option BaseLit := | .Mult => some $ .Int (n₁ * n₂) | .Quot => some $ .Int (n₁ / n₂) | .Rem => some $ .Int (n₁ % n₂) - | .And => sorry -- some $ .Int (n₁ &&& n₂) -- need the mathlib bitwise defs - | .Or => sorry -- some $ .Int (n₁ ||| n₂) - | .Xor => sorry -- some $ .Int (Int.xor n₁ n₂) - | .ShiftL => sorry -- some $ .Int (n₁ <<< n₂) - | .ShiftR => sorry -- some $ .Int (n₁ >>> n₂) + | .And => none -- some $ .Int (n₁ &&& n₂) -- need the mathlib bitwise defs + | .Or => none -- some $ .Int (n₁ ||| n₂) + | .Xor => none -- some $ .Int (Int.xor n₁ n₂) + | .Le => some $ .Bool (decide (n₁ ≤ n₂)) | .Lt => some $ .Bool (decide (n₁ < n₂)) | .Eq => some $ .Bool (decide (n₁ = n₂)) @@ -583,7 +580,6 @@ def binOpEvalBool (op : BinOp) (b₁ b₂ : Bool) : Option BaseLit := | .And => some <| .Bool <| b₁ && b₂ | .Or => some <| .Bool <| b₁ || b₂ | .Xor => some <| .Bool <| xor b₁ b₂ - | .ShiftL | .ShiftR => none -- (* Shifts *) | .Le | .Lt => none -- (* InEquality *) | .Eq => some <| .Bool <| decide (b₁ = b₂) | .Offset => none From cdf9983b623a8509d1b49cec66bec424233e0a97 Mon Sep 17 00:00:00 2001 From: Shreyas Date: Tue, 2 Dec 2025 15:46:51 +0100 Subject: [PATCH 12/12] One annoying sorry --- src/Iris/IrisHeapLang/Lang.lean | 183 ++++++++++++++++++++++---------- 1 file changed, 128 insertions(+), 55 deletions(-) diff --git a/src/Iris/IrisHeapLang/Lang.lean b/src/Iris/IrisHeapLang/Lang.lean index c1adf8d47..dcb08f0ba 100644 --- a/src/Iris/IrisHeapLang/Lang.lean +++ b/src/Iris/IrisHeapLang/Lang.lean @@ -157,9 +157,15 @@ def exprEq (e₁ e₂ : Expr) : Bool := | _, _ => false end +instance : BEq Val where + beq := valEq + +instance : BEq Expr where + beq := exprEq example (v₁ v₂ : Val) : Val.InjL v₁ ≠ Val.InjR v₂ := by apply Val.noConfusion + mutual def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := match v₁, v₂ with @@ -187,15 +193,13 @@ def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := | .Rec f₁ x₁ e₁, .Rec f₂ x₂ e₂ => match hf : (iDecEqBinder f₁ f₂), hx : (iDecEqBinder x₁ x₂), he : (exprDecEq e₁ e₂) with | .isTrue pf, .isTrue px, .isTrue pe => .isTrue (by simp [pf, px, pe]) - | f, x, e => - have h : f ≠ isTrue _ ∨ x ≠ isTrue _ ∨ e ≠ isTrue _ := by - simp[hf, hx, he] - - .isFalse (by - intro h' - cases h' - - <;> simp_all[h]) + | .isTrue pf, .isFalse px, .isFalse pe + | .isTrue pf, .isTrue px, isFalse pe + | .isTrue pf, .isFalse px, isTrue pe + | .isFalse pf, .isTrue px, .isTrue pe + | .isFalse pf, .isFalse px, .isFalse pe + | .isFalse pf, .isTrue px, isFalse pe + | .isFalse pf, .isFalse px, .isTrue pe => .isFalse (by simp [pf, px, pe]) | .Lit _, .InjL _ | .Lit _, .InjR _ | .Lit _, .Pair _ _ @@ -221,7 +225,7 @@ def valDecEq (v₁ v₂ : Val) : Decidable (v₁ = v₂) := def exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := - match e₁, e₂ with + match h₁ : e₁, h₂ : e₂ with | .Val v₁, .Val v₂ => match valDecEq v₁ v₂ with | isTrue p => isTrue (by simp[p]) @@ -243,63 +247,132 @@ def exprDecEq (e₁ e₂ : Expr) : Decidable (e₁ = e₂) := | .App e₁ f₁, .App e₂ f₂ => match h1 : exprDecEq e₁ e₂, h2: exprDecEq f₁ f₂ with | isTrue _, isTrue _ => isTrue (by simp_all) - | he, hf => - have h : exprDecEq e₁ e₂ ≠ isTrue _ ∨ exprDecEq f₁ f₂ ≠ isTrue _ := by - cases - simp [h1, h2] - intro h' - - isFalse (by - cases he - <;> cases hf - <;> simp_all [h1, h2] - ) + | isTrue _ , isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, .isFalse _ => isFalse (by simp_all) + | .Unop op₁ e₁, .Unop op₂ e₂ => match (iDecEqUnOp op₁ op₂), (exprDecEq e₁ e₂) with | .isTrue hop, .isTrue he => .isTrue (by simp [hop, he]) | .isTrue _, .isFalse _ | .isFalse _, .isTrue _ - | .isFalse _, isFalse _ => isFalse (by simp_all) + | .isFalse _, .isFalse _ => .isFalse (by simp_all) | .Binop op₁ e₁ f₁, .Binop op₂ e₂ f₂ => - decide (op₁ = op₂) - && exprEq e₁ e₂ - && exprEq f₁ f₂ + match iDecEqBinOp op₁ op₂, exprDecEq e₁ e₂, exprDecEq f₁ f₂ with + | .isTrue _, .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isTrue _, .isFalse _ + | .isTrue _, .isFalse _, .isTrue _ + | .isTrue _, .isFalse _, .isFalse _ + | .isFalse _, .isTrue _, .isTrue _ + | .isFalse _, .isTrue _, .isFalse _ + | .isFalse _, .isFalse _, .isTrue _ + | .isFalse _, .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .If cond₁ left₁ right₁, .If cond₂ left₂ right₂ => - exprEq cond₁ cond₂ - && exprEq left₁ left₂ - && exprEq right₁ right₂ + match exprDecEq cond₁ cond₂, exprDecEq left₁ left₂, exprDecEq right₁ right₂ with + | .isTrue _, .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isTrue _, .isFalse _ + | .isTrue _, .isFalse _, .isTrue _ + | .isTrue _, .isFalse _, .isFalse _ + | .isFalse _, .isTrue _, .isTrue _ + | .isFalse _, .isTrue _, .isFalse _ + | .isFalse _, .isFalse _, .isTrue _ + | .isFalse _, .isFalse _, .isFalse _ => .isFalse (by simp_all) | .Pair e₁ f₁, .Pair e₂ f₂ => - exprEq e₁ e₂ && exprEq f₁ f₂ - | .Fst e₁, .Fst e₂ => exprEq e₁ e₂ - | .Snd e₁, .Snd e₂ => exprEq e₁ e₂ - | .InjL e₁, .InjL e₂ => exprEq e₁ e₂ - | .InjR e₁, .InjR e₂ => exprEq e₁ e₂ - | .Case e₁ f₁ g₁, .Case e₂ f₂ g₂ => exprEq e₁ e₂ && exprEq f₁ f₂ && exprEq g₁ g₂ - | .AllocN n₁ v₁, .AllocN n₂ v₂ => exprEq n₁ n₂ && exprEq v₁ v₂ - | .Free e₁, .Free e₂ => exprEq e₁ e₂ - | .Load e₁, .Load e₂ => exprEq e₁ e₂ - | .Store e₁ f₁, .Store e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ + match exprDecEq e₁ e₂, exprDecEq f₁ f₂ with + | .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .Fst e₁, .Fst e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .Snd e₁, .Snd e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .InjL e₁, .InjL e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .InjR e₁, .InjR e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .Case e₁ f₁ g₁, .Case e₂ f₂ g₂ => + match exprDecEq e₁ e₂, exprDecEq f₁ f₂, exprDecEq g₁ g₂ with + | .isTrue _, .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isTrue _, .isFalse _ + | .isTrue _, .isFalse _, .isTrue _ + | .isTrue _, .isFalse _, .isFalse _ + | .isFalse _, .isTrue _, .isTrue _ + | .isFalse _, .isTrue _, .isFalse _ + | .isFalse _, .isFalse _, .isTrue _ + | .isFalse _, .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .AllocN n₁ v₁, .AllocN n₂ v₂ => + match exprDecEq n₁ n₂, exprDecEq v₁ v₂ with + | .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .Free e₁, .Free e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .Load e₁, .Load e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .Store e₁ f₁, .Store e₂ f₂ => + match exprDecEq e₁ e₂, exprDecEq f₁ f₂ with + | .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, .isFalse _ => .isFalse (by simp_all) | .CmpXchg e₁ f₁ g₁, .CmpXchg e₂ f₂ g₂ => - exprEq e₁ e₂ - && exprEq f₁ f₂ - && exprEq g₁ g₂ - | .Xchg e₁ f₁, .Xchg e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ - | .FAA e₁ f₁, .FAA e₂ f₂ => exprEq e₁ e₂ && exprEq f₁ f₂ - | .Fork e₁, .Fork e₂ => exprEq e₁ e₂ - | .NewProph, .NewProph => True + match exprDecEq e₁ e₂, exprDecEq f₁ f₂, exprDecEq g₁ g₂ with + | .isTrue _, .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isTrue _, .isFalse _ + | .isTrue _, .isFalse _, .isTrue _ + | .isTrue _, .isFalse _, .isFalse _ + | .isFalse _, .isTrue _, .isTrue _ + | .isFalse _, .isTrue _, .isFalse _ + | .isFalse _, .isFalse _, .isTrue _ + | .isFalse _, .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .Xchg e₁ f₁, .Xchg e₂ f₂ => + match exprDecEq e₁ e₂, exprDecEq f₁ f₂ with + | .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .FAA e₁ f₁, .FAA e₂ f₂ => + match exprDecEq e₁ e₂, exprDecEq f₁ f₂ with + | .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isFalse _ + | .isFalse _, .isTrue _ + | .isFalse _, .isFalse _ => .isFalse (by simp_all) + | .Fork e₁, .Fork e₂ => + match exprDecEq e₁ e₂ with + | .isTrue _ => .isTrue (by simp_all) + | .isFalse _ => .isFalse (by simp_all) + | .NewProph, .NewProph => .isTrue (by rfl) | .Resolve e₁ f₁ g₁, .Resolve e₂ f₂ g₂ => - exprEq e₁ e₂ - && exprEq f₁ f₂ - && exprEq g₁ g₂ - | _, _ => false -end - + match exprDecEq e₁ e₂, exprDecEq f₁ f₂, exprDecEq g₁ g₂ with + | .isTrue _, .isTrue _, .isTrue _ => .isTrue (by simp_all) + | .isTrue _, .isTrue _, .isFalse _ + | .isTrue _, .isFalse _, .isTrue _ + | .isTrue _, .isFalse _, .isFalse _ + | .isFalse _, .isTrue _, .isTrue _ + | .isFalse _, .isTrue _, .isFalse _ + | .isFalse _, .isFalse _, .isTrue _ + | .isFalse _, .isFalse _, .isFalse _ => .isFalse (by simp_all) + | _, _ => .isFalse (by + + sorry) -instance : BEq Val where - beq := valEq +end -instance : BEq Expr where - beq := exprEq