Some restructuring

LeanBoogie/AssumeAssert.lean

@@ -0,0 +1,88 @@
+import LeanBoogie.ITree
+-- import LeanBoogie.ITree.ITree0W
+
+namespace LeanBoogie
+open ITree (Effect HasEff)
+
+/-- `Assume` and `Assert` effect. You can write programs such as the following,
+  where you obtain a proof of the proposition you're assuming.
+  ```
+  .vis (.read "i") fun (i : Int) =>
+    .vis (.am (i < 123)) fun (prf : i < 2) =>
+      ...
+  ```
+  It is up to whoever interprets the event stream to provide the actual proof though!
+  For example, if you're executing a memoryful program, you may try to decide the proposition using
+  either a decision procedure or SMT solvers.  But if you can't provide a proof, you get stuck
+  during execution. If you decide the assumption to be false, you are in an impossible branch,
+  so you can safely eliminate that branch, and need not follow it further.
+
+  You can interpret this into a nondeterminism (i.e. set of possible continuations) monad as follows.
+  Namely, the set of all continuations for which we are able to provide a proof.
+  Note that `Pow A = A -> Prop`.
+  ```
+  def interp : ITree (AmAt + E) A -> Pow (ITree E A)
+  | .vis (.am P) k => { t : ITree E A | (prf : P) -> t = k prf }
+  | .vis (.at P) k => { t : ITree E A | (prf : P)  ∧ t = k prf }
+  | ...
+  ```
+
+  *Key insight*: Both the dijkstra monad and the powerset non-deterministic interpretation describe
+    a set of possible computations. Is it the same notion? Only difference is that dijkstra monad
+    additionally also is a predicate transformer.
+
+  So you actually want something like the following. However, if we have effects other than `Am`,
+  it is unknown whether we can write down `ITreeW`. One solution is to interpret e.g. memory effects
+  away before interpreting away `Am`.
+  ```
+  def interp : ITree AmAt A -> ITree0W A :=
+  | .vis (.am P) k =>
+    fun (post : ITree Empty A -> Prop) =>
+      (prf : P) -> interp (k prf) post
+  | .vis (.at P) k =>
+    fun (post : ITree Empty A -> Prop) =>
+      (prf : P) ∧ interp (k prf) post
+  | ...
+  ```
+
+  Now let's denote `if` as a nondet jump to two itrees, each starting with an assumes event:
+  ```
+  def myprog : ITree (AmAt + Choose + Mem) A :=
+    .vis (.choose (Fin 2)) fun
+      | 0 => .vis (.am   φ ) fun (prf :  φ) => t
+      | 1 => .vis (.am (¬φ)) fun (prf : ¬φ) => e
+  ```
+  Then you get something like a `ITreeW Mem A` or an `ITree0W A`, but no more `Choose` and `AmAt`:
+  ```
+  interp myprog = (fun s post => ??)
+  ```
+-/
+inductive AmAt : Type -> Type
+/-- Assume `P`. -/
+| am : (P : Prop) -> AmAt (PLift P)
+/-- Assert `P`. -/
+| at : (P : Prop) -> AmAt (PLift P)
+
+def assume' [HasEff AmAt Es] (P : Prop) : ITree Es (PLift P) := .vis (AmAt.am P) .ret
+abbrev assume [HasEff AmAt Es] (P : Prop) : ITree Es Unit := do let _ <- assume' P
+def assert' [HasEff AmAt Es] (P : Prop) : ITree Es (PLift P) := .vis (AmAt.at P) .ret
+abbrev assert [HasEff AmAt Es] (P : Prop) : ITree Es Unit := do let _ <- assert' P
+
+/-- This is sound! You can have `ITree E False`, but never `False`.
+  This does not spin either, it just asks for the return value (a `False`) from the world.
+  Which the world can not give, unless the world itself introduces an assumption of `False`,
+  as we (intend to) do when interpreting into the Dijkstra monad `ITreeW`. -/
+def ohno [HasEff AmAt E] : ITree E Empty := do
+  let .up prf <- assume' False
+  prf.elim
+
+#print axioms assume'
+#print axioms ohno
+
+-- def interp : ITree AmAt A -> ITree0W A := sorry
+-- theorem interp_assume : interp (.vis (.assume P) k) = ⟨fun post => P -> (interp (k default)).1 post, sorry⟩ := sorry
+-- theorem interp_assert : interp (.vis (.assert P) k) = ⟨fun post => P /\ (interp (k default)).1 post, sorry⟩ := sorry
+
+-- To generate executable code, we ignore AmAt entirely. If we can't decide an assume/assert to be true, we crash.
+-- interpX : ITree (Mem + AmAt) A -> ITree Mem (Option A)
+-- interpV : ITree (Mem + AmAt) A -> ITree0W A

LeanBoogie/Boogie.lean

@@ -23,7 +23,7 @@ instance : EmptyCollection BoogieState := ⟨fun _ => 0⟩
 
 
 /-- State monad during execution of boogie programs. Assigns values to every variable. -/
-abbrev Boogie : Type -> Type 1 := StateT BoogieState (ITree 0)
+abbrev Boogie : Type -> Type 1 := StateT BoogieState (ITree ∅)
 
 def Boogie.read (v : String) : Boogie Int := fun σ => pure (σ v, σ)
 def Boogie.write (v : String) (val : Int) : Boogie Unit := fun σ => pure ((), BoogieState.update v val σ)

LeanBoogie/Dsl.lean

@@ -21,9 +21,9 @@ open ITree
 structure EBlock where
   label : String
   /-- Any leading assumes for this block. -/
-  assumes : Q(ITree MemEv Bool)
+  assumes : Q(ITree Mem Bool)
   /-- Code without the assumes or gotos. -/
-  code : Q(ITree MemEv Unit)
+  code : Q(ITree Mem Unit)
   /-- The labels from `goto A, B, C;`. Empty list `[]` for `return;`. -/
   gotos : Array String
 deriving Inhabited, Repr
@@ -192,14 +192,14 @@ where go
     bind (get "y") fun y =>
       /- whatever m evaluates to -/
   ``` -/
-def withReadMutVars (vs : List Name) (A : Q(Type)) (m : BoogieElabM Q(ITree MemEv $A)) : BoogieElabM Q(ITree MemEv $A) := do
+def withReadMutVars (vs : List Name) (A : Q(Type)) (m : BoogieElabM Q(ITree Mem $A)) : BoogieElabM Q(ITree Mem $A) := do
   match vs with
   | [] => m
   | v :: vs =>
     let vStr : String := v.toString
-    let a : Q(ITree MemEv Int) := q(Mem.read $vStr)
-    let b : Q(Int -> ITree MemEv $A) <- withLocalDeclDQ v q(Int) fun (v : Q(Int)) => do
-      let e : Q(ITree MemEv $A) <- withReadMutVars vs A m
+    let a : Q(ITree Mem Int) := q(Mem.read $vStr)
+    let b : Q(Int -> ITree Mem $A) <- withLocalDeclDQ v q(Int) fun (v : Q(Int)) => do
+      let e : Q(ITree Mem $A) <- withReadMutVars vs A m
       mkLambdaFVars #[v] e
     return q(Bind.bind $a $b)
 
@@ -266,11 +266,11 @@ mutual
   | stx => throwError "elabBoogieExprPure: Unknown syntax {stx}"
 
   /-- Given a boogie expression `x + y`, produces an expression `bind (get "x") (fun x => bind (get "y") (fun y => pure (x + y))) : ITree MemEv Int`. -/
-  partial def elabBoogieExpr (A : Q(Type)) (stx : TSyntax `BoogieExpr) : BoogieElabM Q(ITree MemEv $A) := do
+  partial def elabBoogieExpr (A : Q(Type)) (stx : TSyntax `BoogieExpr) : BoogieElabM Q(ITree Mem $A) := do
     let vars <- collectMutVars stx
     withReadMutVars vars.toList A (do
       let val : Q($A) <- elabBoogieExprPure A stx
-      let m_val : Q(ITree MemEv $A) := q(Pure.pure $val)
+      let m_val : Q(ITree Mem $A) := q(Pure.pure $val)
       return m_val
     )
 end
@@ -315,26 +315,26 @@ where go
   return q($x -> $y)
 | stx => throwError "elabBoogieFormula: Unknown syntax {stx}"
 
-partial def elabBoogieAssume : TSyntax `BoogieAssume -> BoogieElabM Q(ITree MemEv Unit)
+partial def elabBoogieAssume : TSyntax `BoogieAssume -> BoogieElabM Q(ITree Mem Unit)
 | stx@`(BoogieAssume| assume $φ:BoogieFormula; ) => do
   let vars <- collectMutVarsFormula φ
   withReadMutVars vars.toList q(Unit) do
     let φ : Q(Prop) <- elabBoogieFormula φ
     let _dφ <- synthInstanceQ q(Decidable $φ) -- ! Need `Decidable`, or later: Use events
     -- have : Q(Bool) := q(@decide $φ $dφ)
-    let ret : Q(ITree MemEv Unit) := q(ITree.assume $φ)
+    let ret : Q(ITree Mem Unit) := q(ITree.assume $φ)
     Term.addTermInfo' stx ret
     return ret
 | stx => throwError "elabBoogieAssume: Unknown syntax {stx}"
 
 /-- Creates a program which decides the truth value of each assume, returns conjunction of that. -/
-partial def elabBoogieAssume' : TSyntax `BoogieAssume -> BoogieElabM Q(ITree MemEv Bool)
+partial def elabBoogieAssume' : TSyntax `BoogieAssume -> BoogieElabM Q(ITree Mem Bool)
 | _stx@`(BoogieAssume| assume $φ:BoogieFormula; ) => do
   let vars <- collectMutVarsFormula φ
   withReadMutVars vars.toList q(Bool) do
     let φ : Q(Prop) <- elabBoogieFormula φ
     let dφ <- synthInstanceQ q(Decidable $φ) -- ! Need `Decidable`, or later: Use events
-    let ret : Q(ITree MemEv Bool) := q(return @decide $φ $dφ)
+    let ret : Q(ITree Mem Bool) := q(return @decide $φ $dφ)
     return ret
     -- return q(.ret (decide $φ))
 | stx => throwError "elabBoogieAssume: Unknown syntax {stx}"
@@ -356,22 +356,22 @@ def elabBoogieVarCmds (binders: TSyntaxArray `BoogieVarCmd) : BoogieElabM (Array
     | stx => throwError "elabBoogieVarCmds: unknown syntax {stx}"
 
 mutual
-  partial def elabBoogieCommands (cmds : TSyntaxArray `BoogieCommand) : BoogieElabM Q(ITree MemEv Unit) := do
-    cmds.foldlM (fun (acc : Q(ITree MemEv Unit)) (cmd : TSyntax _) => do
-      let cmd : Q(ITree MemEv Unit) <- withRef cmd <| elabBoogieCommand cmd
+  partial def elabBoogieCommands (cmds : TSyntaxArray `BoogieCommand) : BoogieElabM Q(ITree Mem Unit) := do
+    cmds.foldlM (fun (acc : Q(ITree Mem Unit)) (cmd : TSyntax _) => do
+      let cmd : Q(ITree Mem Unit) <- withRef cmd <| elabBoogieCommand cmd
       return q(.seq $acc $cmd)
     ) q(Pure.pure ())
 
   /-- Elaborates a command such as `x := 2 * y;` or `if ... { ... }` into a monadic action. -/
-  partial def elabBoogieCommand (stx : TSyntax `BoogieCommand) : BoogieElabM Q(ITree MemEv Unit) := do
+  partial def elabBoogieCommand (stx : TSyntax `BoogieCommand) : BoogieElabM Q(ITree Mem Unit) := do
     let ret <- withRef stx (go stx)
     Term.addTermInfo' stx ret
     return ret
   where go
   | _stx@`(BoogieCommand| $x:ident := $e:BoogieExpr; ) => do
     let val <- elabBoogieExpr q(Int) e
     let xStr : String := x.getId.toString
-    let cmd : Q(ITree MemEv Unit) := q(Bind.bind $val (fun val => Mem.write $xStr val))
+    let cmd : Q(ITree Mem Unit) := q(Bind.bind $val (fun val => Mem.write $xStr val))
     -- Term.addTermInfo' stx cmd
     return cmd
   | `(BoogieCommand| if $cond { $t* } $[else { $e* }]?) => do
@@ -397,15 +397,15 @@ end
 def elabBoogieBlock : TSyntax `BoogieBlock -> BoogieElabM EBlock
 | `(BoogieBlock| $lbl:ident : $assumes:BoogieAssume* $cmds:BoogieCommand* goto $gotos,* ; ) => do
   let lbl := lbl.getId.toString
-  let assumes : Array Q(ITree MemEv Bool) <- assumes.mapM elabBoogieAssume'
-  let assumes : Q(ITree MemEv Bool) := assumes.foldl (fun (acc a : Q(ITree MemEv Bool)) =>
+  let assumes : Array Q(ITree Mem Bool) <- assumes.mapM elabBoogieAssume'
+  let assumes : Q(ITree Mem Bool) := assumes.foldl (fun (acc a : Q(ITree Mem Bool)) =>
     q(do
       let acc <- ($acc)
       let a <- ($a)
       return acc && a
     ))
     q(return true)
-  let cmds : Q(ITree MemEv Unit) <- elabBoogieCommands cmds
+  let cmds : Q(ITree Mem Unit) <- elabBoogieCommands cmds
   let gotos : Array String := gotos.getElems.map (fun g => g.getId.toString)
   return ⟨lbl, assumes, cmds, gotos⟩
 | `(BoogieBlock| $lbl:ident : $assumes:BoogieAssume* $cmds:BoogieCommand* return%$rtk ; ) => do
@@ -417,11 +417,11 @@ structure EBoogieBlockyProc where
   name : String
   /-- Amount of labels -/
   N : Nat
-  body : Q(ITree MemEv Unit)
+  body : Q(ITree Mem Unit)
 
 /-- Adapter to turn `List (ITree ...)` into `Fin N -> ITree ...`, which is what `iter` expects. -/
-def selectBlock (N : Nat) (blocks : List (ITree MemEv (Fin N ⊕ Unit))) (h : blocks.length = N) (i : Fin N)
-  : ITree MemEv (Fin N ⊕ Unit)
+def selectBlock (N : Nat) (blocks : List (ITree Mem (Fin N ⊕ Unit))) (h : blocks.length = N) (i : Fin N)
+  : ITree Mem (Fin N ⊕ Unit)
   := blocks[i]
 
 /-- Elaborate a boogie procedure. Returns the procedure name and its body. -/
@@ -461,8 +461,8 @@ def elabBoogieBlockyProc : TSyntax `BoogieBlockyProc -> BoogieElabM EBoogieBlock
     Recall that `.inl (block index here)` means continue execution at that block index, but `inr ()`
     means `return;` from the boogie procedure.
     -/
-    let f : EBlock -> Q(ITree MemEv (Fin $N ⊕ Unit)) := fun b =>
-      let brancher : Q(ITree MemEv (Fin $N ⊕ Unit)) := b.gotos.foldr (fun g brancher =>
+    let f : EBlock -> Q(ITree Mem (Fin $N ⊕ Unit)) := fun b =>
+      let brancher : Q(ITree Mem (Fin $N ⊕ Unit)) := b.gotos.foldr (fun g brancher =>
         if let .some g_block_idx := blocks.findIdxH? (le_refl N) (fun b => b.label == g) then -- translate string label e.g. `bb1` into block index.
           -- | throwError "Block {b.label} goes to unknown label {g}"
           let g_block := blocks[g_block_idx]
@@ -472,15 +472,15 @@ def elabBoogieBlockyProc : TSyntax `BoogieBlockyProc -> BoogieElabM EBoogieBlock
       if b.gotos.isEmpty then q(do ($b.code); return .inr ()) -- `goto;` means `return;`, don't spin in that case
       else q(do ($b.code); ($brancher))
 
-    let blocks' : List Q(ITree MemEv (Fin $N ⊕ Unit)) := blocks.map f
+    let blocks' : List Q(ITree Mem (Fin $N ⊕ Unit)) := blocks.map f
     let h_blocks' : blocks'.length = blocks.length := blocks.length_map f
     -- let xx : SatisfiesM (fun arr => arr.size = blocks.size) (blocks.mapM f) := blocks.size_mapM f
 
-    let blocks'' : Q((xs : List (ITree MemEv (Fin $N ⊕ Unit))) ×' xs.length = $N) := List.q_len N blocks' (by omega)
+    let blocks'' : Q((xs : List (ITree Mem (Fin $N ⊕ Unit))) ×' xs.length = $N) := List.q_len N blocks' (by omega)
     -- let q_blocks : Q(List (ITree MemEv (Fin $N ⊕ Unit))) := q($blocks''.1)
     -- let q_blocks_len : Q(($q_blocks).length = $N) := q($blocks''.2)
     -- let q_blocks_notEmpty :
-    let blocks''' : Q(Fin $N -> ITree MemEv (Fin $N ⊕ Unit)) := q(selectBlock $N $blocks''.1 $blocks''.2)
+    let blocks''' : Q(Fin $N -> ITree Mem (Fin $N ⊕ Unit)) := q(selectBlock $N $blocks''.1 $blocks''.2)
     -- let q_n_0 : Q()
     return {
       name := proc.getId.toString
@@ -496,7 +496,7 @@ structure EBoogieProc where
   name : Name
   -- Args : List Q(Type)
   -- R : Q(Type)
-  body : Q(ITree MemEv Unit)
+  body : Q(ITree Mem Unit)
 
 /-- Elaborate a boogie procedure. Returns the procedure name and its body. -/
 def elabBoogieProc : TSyntax `BoogieProc -> BoogieElabM EBoogieProc
@@ -535,7 +535,7 @@ elab stx:BoogieBlockyProc : command => do
       let ⟨name, _N, body⟩ <- elabBoogieBlockyProc stx
       let decl : DefinitionVal := {
         name := (<- getCurrNamespace) ++ name.toName
-        type := q(ITree MemEv Unit)
+        type := q(ITree Mem Unit)
         value := <- instantiateMVars body
         levelParams := []
         hints := .abbrev
@@ -550,7 +550,7 @@ elab stx:BoogieProc : command => do
       let ⟨name, body⟩ <- elabBoogieProc stx
       let decl : DefinitionVal := {
         name := (<- getCurrNamespace) ++ name
-        type := q(ITree MemEv Unit)
+        type := q(ITree Mem Unit)
         value := <- instantiateMVars body
         levelParams := []
         hints := .abbrev