Generalize loop elimination transformation

Strata/DL/Imperative/Cmd.lean

@@ -73,6 +73,21 @@ instance (P : PureExpr) : SizeOf (Imperative.Cmd P) where
 
 ---------------------------------------------------------------------
 
+class HasPassiveCmds (P : PureExpr) (CmdT : Type) where
+  assume : String → P.Expr → CmdT
+  assert : String → P.Expr → CmdT
+
+instance : HasPassiveCmds P (Cmd P) where
+  assume l e := .assume l e
+  assert l e := .assert l e
+
+class HasHavoc (P : PureExpr) (CmdT : Type) where
+  havoc : P.Ident → CmdT
+
+instance : HasHavoc P (Cmd P) where
+  havoc x := .havoc x
+---------------------------------------------------------------------
+
 mutual
 /-- Get all variables accessed by `c`. -/
 def Cmd.getVars [HasVarsPure P P.Expr] (c : Cmd P) : List P.Ident :=

Strata/DL/Imperative/CmdSemantics.lean

@@ -217,11 +217,11 @@ theorem invStoresExceptComm :
 -- since there could be coercions like [1 >>= True] and [0 >>= False]
 -- or that when δ evaluates to none, δP evaluates to False
   -/
-def WellFormedSemanticEvalBool {P : PureExpr} [HasBool P] [HasBoolNeg P]
+def WellFormedSemanticEvalBool {P : PureExpr} [HasBool P] [HasNot P]
     (δ : SemanticEval P) : Prop :=
     ∀ σ₀ σ e,
-      (δ σ₀ σ e = some Imperative.HasBool.tt ↔ δ σ₀ σ (Imperative.HasBoolNeg.neg e) = (some HasBool.ff)) ∧
-      (δ σ₀ σ e = some Imperative.HasBool.ff ↔ δ σ₀ σ (Imperative.HasBoolNeg.neg e) = (some HasBool.tt))
+      (δ σ₀ σ e = some Imperative.HasBool.tt ↔ δ σ₀ σ (Imperative.HasNot.not e) = (some HasBool.ff)) ∧
+      (δ σ₀ σ e = some Imperative.HasBool.ff ↔ δ σ₀ σ (Imperative.HasNot.not e) = (some HasBool.tt))
 
 def WellFormedSemanticEvalVal {P : PureExpr} [HasVal P]
     (δ : SemanticEval P) : Prop :=
@@ -261,7 +261,7 @@ inductive InitState : SemanticStore P → P.Ident → P.Expr → SemanticStore P
 An inductively-defined operational semantics that depends on
 environment lookup and evaluation functions for expressions.
 -/
-inductive EvalCmd [HasFvar P] [HasBool P] [HasBoolNeg P] :
+inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → SemanticStore P → Cmd P → SemanticStore P → Prop where
   | eval_init :
     δ σ₀ σ e = .some v →

Strata/DL/Imperative/NondetStmtSemantics.lean

@@ -17,7 +17,7 @@ mutual
 statements that depends on environment lookup and evaluation functions
 for expressions.  -/
 inductive EvalNondetStmt (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
-  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → SemanticStore P →
     NondetStmt P Cmd → SemanticStore P → Prop where
   | cmd_sem :

Strata/DL/Imperative/PureExpr.lean

@@ -31,8 +31,17 @@ class HasBool (P : PureExpr) where
   tt : P.Expr
   ff : P.Expr
 
-class HasBoolNeg (P : PureExpr) [HasBool P] where
-  neg : P.Expr → P.Expr
+class HasNot (P : PureExpr) extends HasBool P where
+  not : P.Expr → P.Expr
+
+class HasAnd (P : PureExpr) extends HasBool P where
+  and : P.Expr → P.Expr → P.Expr
+
+class HasImp (P : PureExpr) extends HasBool P where
+  imp : P.Expr → P.Expr → P.Expr
+
+class HasEq (P : PureExpr) where
+  eq : P.Expr → P.Expr → P.Expr
 
 class HasFvar (P : PureExpr) where
   mkFvar : P.Ident → P.Expr

Strata/DL/Imperative/StmtSemantics.lean

@@ -22,7 +22,7 @@ Note that `EvalStmt` is parameterized by commands `Cmd` as well as their
 evaluation relation `EvalCmd`.
 -/
 inductive EvalStmt (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
-  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → SemanticStore P →
   Stmt P Cmd → SemanticStore P → Prop where
   | cmd_sem :
@@ -56,7 +56,7 @@ inductive EvalStmt (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
   -- (TODO): Define semantics of `goto`.
 
 inductive EvalStmts (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
-  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
     SemanticEval P → SemanticStore P → SemanticStore P →
     List (Stmt P Cmd) → SemanticStore P → Prop where
   | stmts_none_sem :
@@ -67,7 +67,7 @@ inductive EvalStmts (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
     EvalStmts P Cmd EvalCmd δ σ₀ σ (s :: ss) σ''
 
 inductive EvalBlock (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
-  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
     SemanticEval P → SemanticStore P → SemanticStore P →
   Block P Cmd → SemanticStore P → Prop where
   | block_sem :
@@ -77,7 +77,7 @@ inductive EvalBlock (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
 end
 
 theorem eval_stmts_singleton
-  [HasVarsImp P (List (Stmt P (Cmd P)))] [HasVarsImp P (Cmd P)] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P (Cmd P)))] [HasVarsImp P (Cmd P)] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
   EvalStmts P (Cmd P) (EvalCmd P) δ σ₀ σ [cmd] σ' ↔
   EvalStmt P (Cmd P) (EvalCmd P) δ σ₀ σ cmd σ' := by
   constructor <;> intro Heval
@@ -86,7 +86,7 @@ theorem eval_stmts_singleton
   apply EvalStmts.stmts_some_sem Heval (EvalStmts.stmts_none_sem)
 
 theorem eval_stmts_concat
-  [HasVarsImp P (List (Stmt P (Cmd P)))] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P (Cmd P)))] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
   EvalStmts P (Cmd P) (EvalCmd P) δ σ₀ σ cmds1 σ' →
   EvalStmts P (Cmd P) (EvalCmd P) δ σ₀ σ' cmds2 σ'' →
   EvalStmts P (Cmd P) (EvalCmd P) δ σ₀ σ (cmds1 ++ cmds2) σ'' := by
@@ -100,7 +100,7 @@ theorem eval_stmts_concat
   apply EvalStmts.stmts_some_sem (by assumption)
   apply ind (by assumption) (by assumption)
 
-theorem EvalCmdDefMonotone [HasFvar P] [HasBool P] [HasBoolNeg P] :
+theorem EvalCmdDefMonotone [HasFvar P] [HasBool P] [HasNot P] :
   isDefined σ v →
   EvalCmd P δ σ₀ σ c σ' →
   isDefined σ' v := by
@@ -112,13 +112,13 @@ theorem EvalCmdDefMonotone [HasFvar P] [HasBool P] [HasBoolNeg P] :
 
 theorem EvalStmtsEmpty {P : PureExpr} {Cmd : Type} {EvalCmd : EvalCmdParam P Cmd}
   { σ σ' σ₀: SemanticStore P } { δ : SemanticEval P }
-  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
   EvalStmts P Cmd EvalCmd δ σ₀ σ ([]: (List (Stmt P Cmd))) σ' → σ = σ' := by
   intros H; cases H <;> simp
 
 mutual
 theorem EvalStmtDefMonotone
-  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasBoolNeg P]
+  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasNot P]
   :
   isDefined σ v →
   EvalStmt P (Cmd P) (EvalCmd P) δ σ₀ σ s σ' →
@@ -143,7 +143,7 @@ theorem EvalStmtDefMonotone
   decreasing_by all_goals simp [*] at * <;> omega
 
 theorem EvalStmtsDefMonotone
-  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasBoolNeg P]
+  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasNot P]
   :
   isDefined σ v →
   EvalStmts P (Cmd P) (EvalCmd P) δ σ₀ σ ss σ' →

Strata/Languages/Boogie/Examples/Loops.lean

@@ -114,10 +114,10 @@ info:
 Obligation: entry_invariant_0
 Result: verified
 
-Obligation: entry_invariant_2
+Obligation: entry_invariant_1
 Result: verified
 
-Obligation: arbitrary_iter_maintain_invariant_2
+Obligation: arbitrary_iter_maintain_invariant_1
 Result: verified
 
 Obligation: entry_invariant_0

Strata/Languages/Boogie/ProcedureEval.lean

@@ -7,7 +7,9 @@
 
 
 import Strata.Languages.Boogie.Procedure
+import Strata.Languages.Boogie.Statement
 import Strata.Languages.Boogie.StatementEval
+import Strata.Languages.Boogie.StatementSemantics
 import Strata.Transform.LoopElim
 
 ---------------------------------------------------------------------
@@ -73,7 +75,7 @@ def eval (E : Env) (p : Procedure) : List (Procedure × Env) :=
       p.spec.postconditions
   let precond_assumes :=
     List.map (fun (label, check) => (.assume label check.expr)) p.spec.preconditions
-  let body' := p.body.map Statement.removeLoops
+  let body' : List Statement := p.body.map Stmt.removeLoops
   let ssEs := Statement.eval E old_var_subst (precond_assumes ++ body' ++ postcond_asserts)
   ssEs.map (fun (ss, sE) => ({ p with body := ss }, fixupError sE))
 

Strata/Languages/Boogie/Statement.lean

@@ -38,6 +38,13 @@ We parameterize Boogie's Commands with Lambda dialect's expressions.
 -/
 abbrev Command := CmdExt Expression
 
+instance : HasPassiveCmds Expression Command where
+  assert l e := .cmd (.assert l e)
+  assume l e := .cmd (.assume l e)
+
+instance : HasHavoc Expression Command where
+  havoc x := .cmd (.havoc x)
+
 def CmdExt.sizeOf (c : CmdExt P) : Nat :=
   match c with
   | .cmd c => SizeOf.sizeOf c

Strata/Languages/Boogie/StatementSemantics.lean

@@ -4,6 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
+import Strata.DL.Lambda.LExpr
 import Strata.DL.Imperative.StmtSemantics
 import Strata.Languages.Boogie.OldExpressions
 
@@ -37,12 +38,11 @@ instance : HasBool Boogie.Expression where
   tt := Boogie.true
   ff := Boogie.false
 
-/-- TODO: extend this to handle non-constants -/
-instance : HasBoolNeg Boogie.Expression where
-  neg
+instance : HasNot Boogie.Expression where
+  not
   | Boogie.true => Boogie.false
   | Boogie.false => Boogie.true
-  | _ => panic! "neg expects either tt or ff"
+  | e => Lambda.LExpr.app Lambda.boolNotFunc.opExpr e
 
 abbrev BoogieEval := SemanticEval Expression
 abbrev BoogieStore := SemanticStore Expression

Strata/Languages/Boogie/StatementSemanticsProps.lean

@@ -41,7 +41,7 @@ theorem TouchVarsEmpty :
 
 theorem EvalStmtsEmpty {P : PureExpr} {Cmd : Type} {EvalCmd : EvalCmdParam P Cmd}
   { σ σ' σ₀: SemanticStore P } { δ : SemanticEval P }
-  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasBoolNeg P] :
+  [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasVal P] [HasBool P] [HasNot P] :
   EvalStmts P Cmd EvalCmd δ σ₀ σ ([]: (List (Stmt P Cmd))) σ' → σ = σ' := by
   intros H; cases H <;> simp
 
@@ -1716,7 +1716,7 @@ theorem EvalCmdDefMonotone :
   next _ _ Hup => exact UpdateStateDefMonotone Hdef Hup
 
 theorem EvalCmdTouch
-  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasBoolNeg P] :
+  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasNot P] :
   EvalCmd P δ σ₀ σ c σ' →
   TouchVars σ (HasVarsImp.touchedVars c) σ' := by
   intro Heval

Strata/Transform/DetToNondet.lean

@@ -16,7 +16,7 @@ mutual
 
 /-- Deterministic-to-nondeterministic transformation for a single
 (deterministic) statement -/
-def StmtToNondetStmt {P : PureExpr} [Imperative.HasBool P] [Imperative.HasBoolNeg P]
+def StmtToNondetStmt {P : PureExpr} [Imperative.HasBool P] [HasNot P]
   (st : Imperative.Stmt P (Cmd P)) :
   Imperative.NondetStmt P (Cmd P) :=
   match st with
@@ -25,7 +25,7 @@ def StmtToNondetStmt {P : PureExpr} [Imperative.HasBool P] [Imperative.HasBoolNe
   | .ite    cond  thenb elseb md =>
     .choice
       (.seq (.assume "true_cond" cond md) (StmtsToNondetStmt thenb.ss))
-      (.seq ((.assume "false_cond" (Imperative.HasBoolNeg.neg cond) md)) (StmtsToNondetStmt elseb.ss))
+      (.seq ((.assume "false_cond" (Imperative.HasNot.not cond) md)) (StmtsToNondetStmt elseb.ss))
   | .loop   guard _measure _inv body md =>
     .loop (.seq (.assume "guard" guard md) (StmtsToNondetStmt body.ss))
   | .goto _ _ => (.assume "skip" Imperative.HasBool.tt)
@@ -34,7 +34,7 @@ def StmtToNondetStmt {P : PureExpr} [Imperative.HasBool P] [Imperative.HasBoolNe
 
 /-- Deterministic-to-nondeterministic transformation for multiple
 (deterministic) statements -/
-def StmtsToNondetStmt {P : Imperative.PureExpr} [Imperative.HasBool P] [Imperative.HasBoolNeg P]
+def StmtsToNondetStmt {P : Imperative.PureExpr} [Imperative.HasBool P] [HasNot P]
   (ss : Imperative.Stmts P (Cmd P)) :
   Imperative.NondetStmt P (Cmd P) :=
   match ss with

Strata/Transform/DetToNondetCorrect.lean

@@ -28,7 +28,7 @@ open Imperative Boogie
   implicit arguments, and it can be hard to find the cause from the generic
   error message similar to "(kernel) application type mismatch".
 -/
-theorem StmtToNondetCorrect [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasBoolNeg P] :
+theorem StmtToNondetCorrect [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasNot P] :
   WellFormedSemanticEvalBool δ →
   WellFormedSemanticEvalVal δ →
   (∀ st,
@@ -135,7 +135,7 @@ theorem StmtToNondetCorrect [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [H
 /-- Proof that the Deterministic-to-nondeterministic transformation is correct
 for a single (deterministic) statement -/
 theorem StmtToNondetStmtCorrect
-  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasBoolNeg P] :
+  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasNot P] :
   WellFormedSemanticEvalBool δ →
   WellFormedSemanticEvalVal δ →
   EvalStmt P (Cmd P) (EvalCmd P) δ σ₀ σ st σ' →
@@ -146,7 +146,7 @@ theorem StmtToNondetStmtCorrect
 /-- Proof that the Deterministic-to-nondeterministic transformation is correct
 for multiple (deterministic) statements -/
 theorem StmtsToNondetStmtCorrect
-  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasBoolNeg P] :
+  [HasVal P] [HasFvar P] [HasBool P] [HasBoolVal P] [HasNot P] :
   WellFormedSemanticEvalBool δ →
   WellFormedSemanticEvalVal δ →
   EvalStmts P (Cmd P) (EvalCmd P) δ σ₀ σ ss σ' →