SimpleIter example ITree proof and reorganize files

Examples/SimpleIter.lean

@@ -0,0 +1,64 @@
+-- import LeanBoogie.BoogieDsl
+import LeanBoogie.ITree
+import LeanBoogie.Boog
+import LeanBoogie.Mem
+import Auto
+import Aesop
+
+open Boogie ITree
+
+set_option auto.smt true
+set_option trace.auto.smt.printCommands true
+set_option trace.auto.smt.result true
+set_option trace.auto.printLemmas true
+set_option auto.smt.trust true
+set_option auto.smt.solver.name "z3"
+set_option pp.fieldNotation.generalized false
+
+-- Very simple example which can be proven using unrolling or a congruence on the while loop
+
+def p1 : ITree MemEv Unit := do
+  Mem.write "i" 0
+  while_ (return (<- Mem.read "i") < 3) do
+    Mem.update "i" (. + 1)
+    Mem.update "x" (. + 2)
+  Mem.write "i" 0 -- need to set `i` to 0 afterwards, otherwise the programs compute the same `x` but not `i`.
+
+def p2 : ITree MemEv Unit := do
+  Mem.write "i" 0
+  while_ (return (<- Mem.read "i") < 6) do
+    Mem.update "x" (. + 1)
+    Mem.update "i" (. + 1)
+  Mem.write "i" 0
+
+example : EuttB (interp p1) (interp p2) := by
+  rw [p1, p2]
+  -- 1. unroll loops
+  conv => lhs; rw [Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1]
+  conv => rhs; rw [Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1, Eutt.eq while_unroll1]
+
+  -- 2. Push `interp` inwards as far as possible,
+  -- this will change `ITree.{pure, bind, iter, ite, read, write}`
+  -- into `Boog.{pure, bind, iter, ite, read, write}`
+  simp [EuttB.eq interp_bind, EuttB.eq interp_write, EuttB.eq interp_ite, EuttB.eq interp_pure,
+    Mem.update, EuttB.eq interp_write, EuttB.eq interp_read, skip]
+  -- Our goal is now of form `b1 b2 : (S -> ITree ∅ (A × S)) ⊢ ∀σ:S, Eutt (b1 σ) (b2 σ)`, with the predominant `bind` being `Boog.bind`.
+
+  -- 3. Push state `σ` inwards as far as possible. This allows us to apply `pure_bind` and obtain
+  -- a pure state transition function, because we no longer have any relevant coinduction.
+  -- Nonetheless, this causes the predominant `bind` to become `ITree.bind` yet again (`Boog.read v : Boog ..`, but `Boog.read v σ : ITree ..`).
+  -- However, we know that `ITree.bind (Boog.read v σ) k` is actually `ITree.bind (ITree.pure (σ v, σ)) k`, which simplifies to `k (σ v) σ` via `pure_bind`. Similar for `.write`.
+  intro σ
+  simp only [Eutt.eq Boog.bind_push_state, Eutt.eq Boog.ite_push_state]
+  simp only [Boog.read, Boog.write, BoogieState.update.eq_unfold]
+  simp only [pure_bind, Nat.ofNat_pos, dite_eq_ite, ↓reduceDIte, ↓reduceIte, String.reduceEq, zero_add, Nat.one_lt_ofNat, Int.reduceAdd, Int.reduceLT, lt_self_iff_false]
+  simp_all only [↓reduceIte]
+
+  dsimp [Pure.pure, ITree.pure]
+  -- Our goal is now of form `σ : S ⊢ .ret (a, f σ) = .ret (b, g σ)`
+  apply Eutt.ret_congr
+  congr 1
+  unfold BoogieState at σ
+  unfold BoogieState
+  -- 4. Solve by auto :)
+  auto

Examples/SimpleMonadicDsl.lean

@@ -2,7 +2,7 @@ import LeanBoogie.BoogieDsl
 import Auto
 import Aesop
 
-open Boog
+open Boogie
 
 set_option auto.smt true
 set_option trace.auto.smt.printCommands true
@@ -13,26 +13,34 @@ set_option auto.smt.solver.name "z3"
 
 namespace Example1
   procedure test1(x: int, y: int) returns (z: int) {
-    x := (x + 1); x := x + 2;
-    y := y + 1; y := y + 2;
-    z := x + y;
+  bb0:
+    z := x;
+    z := z + y;
+    goto;
   }
+
   procedure test2(x: int, y: int) returns (z: int) {
-    y := y + 1; y := y + 2;
-    x := x + 2; x := x + 1;
-    z := x + y;
+  bb0:
+    z := y;
+    z := z + x;
+    goto;
   }
 
-  example (state) : test1 state = test2 state := by
-    unfold BoogieState at state
+  #check test1
+
+  example (s : BoogieState) : Eutt test1 test2 := by
     rw [test1, test2]
-    simp [Boog.skip, Boog.set, Boog.get, Boog.set, Boog.seq, Boog.ifthen, Boog.ifthenelse,
-      bind_eq2,
-      StateT.get, StateT.set, getThe, modifyThe, StateT.modifyGet,
-      pure, StateT.pure, instMonadStateOfMonadStateOf, instMonadStateOfStateTOfMonad]
-    congr 1
-    funext v -- for all vars..
-    auto
+    simp [ITree.skip, ITree.seq, ITree.bind_ret, interp]
+
+    sorry
+
+  -- This is simply not true, because the reads and writes are in a different order.
+  example : Eutt test1 test2 := by
+    rw [test1, test2]
+    simp [ITree.skip, ITree.seq, ITree.bind_ret]
+
+    -- exact Eutt.refl _ -- this takes forever to typecheck (whnf) before failing.
+    -- done
 end Example1
 
 namespace Example2

LeanBoogie/Blocks.lean

@@ -0,0 +1,121 @@
+import LeanBoogie.ITree
+import LeanBoogie.Boog
+
+namespace Boogie
+
+open ITree KTree
+
+/-
+  # Basic, Labels, `goto`
+-/
+
+abbrev Label := Nat
+abbrev Labels := { xs : List Label // xs.length >= 0 }
+
+structure Block : Type where
+  assumes : ITree MemEv Bool := ITree.ret true
+  /-- A block is code which returns at least one label to jump to. -/
+  code : ITree MemEv Labels
+
+/-- Boogie procedure. Just a bunch of blocks. -/
+structure Procedure : Type where
+  blocks : List Block
+
+/-- Get a block, or spin forever if index is invalid. -/
+def getBlock (proc : Procedure) (l : Label) : ITree E Block := do
+  if h : l < proc.blocks.length then return proc.blocks[l]
+  else ITree.spin
+
+/-- Return the label of the first block whose `assume`s decide to true. If none are, spin. -/
+def choose (proc : Procedure) : KTree MemEv Labels Label
+  := fun ⟨ls, _⟩ => impl proc ls
+where impl (proc : Procedure) : KTree MemEv (List Label) Label
+| [] => ITree.spin
+| l :: ls => do
+  let b <- getBlock proc l
+  if <- b.assumes
+    then return l
+    else impl proc ls
+
+#check case
+
+/-- Run a bunch of blocks until no jump label is returned anymore. -/
+-- def Procedure.run (proc : Procedure) : Label -> ITree MemEv Unit :=
+def Procedure.run (proc : Procedure) : KTree MemEv Label Unit :=
+  ITree.iter (A := Label) (B := _) fun (l : Label) => do
+    let block <- getBlock proc l
+    let ls : Labels <- block.code -- run block
+    -- TODO: potentially non-deterministic branching.
+    let l <- choose proc ls
+    if l = 0 then return .inr () -- hard-code label 0 as the exit label for now.
+    else return .inl l
+    /- Here, `run` must somehow know which of the labels to jump to, because we are essentially
+      building an interpreter, and Lean is deterministic. So how can we know this?
+      1. Sometimes, the `assume`s at the beginning of each block are disjoint, so the jump is
+        actually deterministic. The problems with this are:
+        - We'd need to *look inside* those blocks. We have the list of blocks in `proc`, but they
+          are of type `ITree _ _`, which we can't pattern match on. So we have to store this
+          extra information somewhere along with the list of blocks. Now we have information
+          doubling, which is not very pretty.
+          This could be avoided if the blocks were a syntactic construct, so that you could
+          pattern match on them and read out the `assume`s.
+        - We'd have to decide the propositions. Often this will be easy, since those propositions
+          often stem from `if` and the like. However, Boogie allows arbitrary propositions in
+          `assume`, which may even include forall-quantifiers.
+          This means we have to read some variables with `Mem.get`, which we know doesn't change
+          the state after interpretation, but theoretically we can't know this at this point;
+          it also breaks eutt.
+      2. We can use an "event oracle", i.e. add an effect to our ITrees so that we can ask
+        the world which branch to take. This is (oversimplifying) how
+        (Choice Trees)[https://arxiv.org/pdf/2211.06863] paper does it, but there are subtleties
+        to consider, such as:
+        - For `ITree MemEv A`, we have some nice laws such as associativity after interpretation.
+          But you don't want to interpret `ITree (MemEv ⊕ NonDet) A`, because... you can't.
+          So what do you do? You need to recover this structure somehow, and that's what the
+          CTrees paper is for. See section 2.2 of the ctrees paper.
+        - A different notion of program equivalence than eutt, which can deal with non-det.
+      3. So instead, we take a very practical, somewhat hacky, approach for now: For each
+        destination block, jump to the first block whose `assume φ` decides to true.
+        This will coincidentally give us correct semantics if the assumes are disjoint, and will
+        act as a tie-breaker for non-determinism.
+        - The problem with having to *look inside* the blocks and read out the `assume`s remain.
+    -/
+
+
+
+
+-- ## Example:
+
+def bb1 : Block := {
+  code := do
+    Mem.write "i1" 1
+    return ⟨[2], by rw [List.length]; omega⟩
+}
+
+def bb2 : Block := {
+  assumes := do return (<- Mem.read "i") <= 5
+  code := do
+    Mem.write "x" ((<- Mem.read "x") + 2)
+    Mem.write "i" ((<- Mem.read "i") + 1)
+    return ⟨[2, 3], by rw [List.length]; omega⟩
+}
+
+def bb3 : Block := {
+  assumes := do return !((<- Mem.read "i") <= 5)
+  code := do return ⟨[0], by rw [List.length]; omega⟩
+}
+
+def myProc : Procedure := {
+  blocks := [bb1, bb2, bb3]
+}
+
+-- theorem run_step : Procedure.run proc l = proc.blocks[l] >>> proc.run l := sorry
+
+-- example : myProc.run ~~~ myProc.run := by
+
+--   done
+
+-- #check ITree.iter
+-- /-- -/
+-- example : KTree MemEv Nat Nat :=
+--   KTree.iter

LeanBoogie/Boog.lean

@@ -1,5 +1,8 @@
 import Std
 import Aesop
+import LeanBoogie.ITree
+import LeanBoogie.Notation
+import LeanBoogie.Iter
 
 namespace Boogie
 
@@ -10,84 +13,73 @@ open Std (HashSet HashMap)
   Tracks values of boogie variables during execution.
 -/
 
+
 /-- Assigns values to every variable. Ideally you'd want `(v : String) -> v ∈ ValidVars -> Int`. -/
 abbrev BoogieState := String -> Int
+
+def BoogieState.update (v : String) (val : Int) : BoogieState -> BoogieState :=
+  fun σ v' => if _h : v' = v then val else σ v'
 instance : EmptyCollection BoogieState := ⟨fun _ => 0⟩
 
+
 /-- State monad during execution of boogie programs. Assigns values to every variable. -/
-abbrev Boog : Type -> Type := StateM BoogieState
+abbrev Boog (E : Type) : Type -> Type := StateT BoogieState (ITree E)
 
-def Boog.skip : Boog Unit := pure ()
-def Boog.seq (a b : Boog Unit) : Boog Unit := a >>= (fun _ => b)
+def Boog.read (v : String) : Boog E Int := fun σ => pure (σ v, σ)
+def Boog.write (v : String) (val : Int) : Boog E Unit := fun σ => pure ((), BoogieState.update v val σ)
+/-- Apply a pure function to a variable. Useful for simple operations such as increments, setting to zero, etc. -/
+def Boog.update (v : String) (f : Int -> Int) : Boog E Unit
+  := Boog.read v >>= fun x => Boog.write v (f x)
 
-def Boog.get (v : String) : Boog Int := do return (<- getThe BoogieState) v
-def Boog.set (v : String) (e : Boog Int) : Boog Unit := do
-  let val <- e
-  modifyThe BoogieState
-      (fun f x => if x = v then val else f x)
 
-/-- This is a little ugly, because lean `if` actually takes a (decidable) `Prop`, not a `Bool` -/
-def Boog.ifthenelse (c : Boog Bool) (t e : Boog Unit) : Boog Unit := do
-  if <- c then t else e
+/- ## Helpers for writing imperative programs.  -/
 
-def Boog.ifthen (c : Boog Bool) (t : Boog Unit) : Boog Unit := do
-  if <- c then t
+def Boog.iter (f : A -> Boog E (A ⊕ B)) : A -> Boog E B := sorry
+instance : Iter (Boog E) := ⟨Boog.iter⟩
 
-/-- Actually execute a boogie program, starting with every variable being 0-initialized. -/
-def runBoogie (m : Boog Unit) : BoogieState :=
-  let s₀ : BoogieState := (fun _ => 0)
-  let ((), s') := StateT.run m s₀
-  s'
+def Boog.skip : Boog E Unit := pure ()
+def Boog.seq (a b : Boog E Unit) : Boog E Unit := a >>= (fun () => b)
+instance : Seqi (Boog E Unit) := ⟨Boog.seq⟩
 
-/-
-  ## Helper lemmas
-  Elaborated Boogie programs are quite noisy, and not structured in a way that Lean-Auto can deal
-  with very well. So here we define a bunch of lemmas which (hopefully) bring elaborated Boogie
-  programs into a shape that SMT solvers can deal with.
--/
+def Boog.case (t e : Boog E A) : Bool -> Boog E A
+| true => t
+| false => e
 
-theorem bind_eq2 (a: Boog A) (b: A -> Boog B) : (a >>= b : Boog B) = fun s => let x := a s ; b x.fst x.snd
-:= by
-  unfold bind Monad.toBind StateT.instMonad StateT.bind
-  simp
-
-@[aesop unsafe] theorem one_var {t1 t2 : String -> Int} (x : String)
-  (h_x     : t1 x = t2 x)
-  (h_other : (∀v, ¬ v = x -> t1 v = t2 v))
-  : ∀v, t1 v = t2 v
-  := by intro v; if h : x = v then exact h ▸ h_x else aesop
-
-@[simp]
-theorem ite_bind:
-  ∀ [Monad m]
-    {c : Bool}
-    {m1 m2 : m a}
-    {k : a -> m b},
-   (if c then m1       else m2      ) >>= k
-  = if c then m1 >>= k else m2 >>= k
-  := by aesop
+def Boog.ite (c : Boog E Bool) (t e : Boog E A) : Boog E A :=
+  c >>= Boog.case t e
 
-@[simp]
-theorem var_congr_ite
-  [Decidable c]
-  (x : String)
-  {t e t' e' : Boog A}
-  (h_t :   c -> (t st).2 x = (t' st).2 x)
-  (h_e : ¬ c -> (e st).2 x = (e' st).2 x)
-  : ((if c then t else e) st).2 x = ((if c then t' else e') st).2 x
-  := by aesop
-
-@[simp]
-theorem state_congr_ite [Decidable c] {t e : Boog A}
-  : (if c then t else e) st = (if c then t st else e st)
-  := by aesop
+abbrev Boog.pure : A -> Boog E A := Pure.pure
+abbrev Boog.bind : (Boog E A) -> (A -> Boog E B) -> Boog E B := Bind.bind
 
-@[simp]
-theorem state_proj_congr_ite [Decidable c] {tst est :(A × S)}
-  : (if c then tst else est).2 = (if c then (tst).2 else (est).2)
-  := by aesop
-
-@[simp]
-theorem state_var_ite_congr [Decidable c] {t e : String -> Int}
-  : (if c then t else e) v = (if c then t v else e v)
+/-- Actually execute a boogie program, starting with every variable being 0-initialized. -/
+def Boog.run (m : Boog Empty Unit) (fuel : Nat) : Option BoogieState :=
+  let s₀ : BoogieState := (fun _ => 0)
+  let stuff := StateT.run m s₀
+  let ⟨_, ret⟩ := ITree.run stuff Empty.elim fuel
+  ret.map Prod.snd
+
+/-- Equivalence up-to-tau, but adapted for the `Boog` monad. -/
+def EuttB (b1 : Boog E A) (b2 : Boog E A) : Prop := ∀σ : BoogieState, Eutt (b1 σ) (b2 σ)
+infixr:20 " ~=~ " => EuttB
+
+axiom EuttB.eq {E A : Type} {x y : Boog E A} : EuttB x y -> x = y
+
+theorem Boog.ite_push_state [Decidable c] {t e : Boog E A}
+  : (if c then t else e) σ ~~ (if c then t σ else e σ)
+  := by split; repeat exact Eutt.refl _
+
+theorem Boog.bind_push_state {a : Boog E A} {b : A -> Boog E B}
+  : (a >>= b) σ ~~ (a σ >>= fun res => b res.fst res.snd)
+  := sorry
+
+def Boog.while_ (c : Boog E Bool) (body : Boog E Unit) : Boog E Unit :=
+  Boog.iter
+    (fun () => Boog.ite c
+      (do body; return .inl ())
+      (return .inr ()))
+    ()
+
+@[simp] theorem ite_bind [Monad m] [Decidable c] {m1 m2 : m a} {k : a -> m b}
+  : (if c then m1       else m2      ) >>= k
+  =  if c then m1 >>= k else m2 >>= k
   := by aesop