Syntax for Boogie with denotations, some WP

LeanBoogie/ConTy.lean

@@ -46,7 +46,7 @@ abbrev TyA : Ty -> Type
 | .unit => Unit
 | .int => Int
 | .real => Real
-| .bool => Prop
+| .bool => Bool
 | .bv bits => BitVec bits
 | .map A B => TyA A -> TyA B
 

LeanBoogie/Denotation.lean

@@ -0,0 +1,132 @@
+import Lean
+import ITree
+import LeanBoogie.ConTy
+import LeanBoogie.State
+import LeanBoogie.Syntax
+import LeanBoogie.Effect.AssumeAssert
+import LeanBoogie.Effect.Choice
+import LeanBoogie.Effect.Mem
+
+open ITree
+open LeanBoogie
+namespace LeanBoogie
+
+-- Syntax-free definitions
+
+def goto : List (Fin b) -> ITree Choice (Fin b ⊕ Unit)
+| [] => (.ret (.inr ())) -- Shouldn't actually happen
+| [l] => (.ret (.inl l))
+| ls => do
+   let li <- choice (Fin ls.length)
+   .ret (.inl (ls.get li))
+
+-- Conditional goto, for deterministic programs
+def cgoto : Bool -> Fin b -> Fin b -> ITree E (Fin b ⊕ Unit)
+| c, t, e => if c then (.ret (.inl t)) else (.ret (.inl e))
+
+class ToITree (α : Type) (E : Type -> Type) (R : Type) where
+  -- TODO: do we need E'?
+  toITree : α -> ITree (E & E') R
+
+-- TODO: don't need separate constructors?
+def denoteLiteral : Literal A -> TyA A
+| .intL n => n
+| .boolL b => b
+| .bvL bv => bv
+| .realL r => r
+
+--noncomputable
+def denoteBinaryOp : BinaryOp A -> TyA A -> TyA A -> TyA A
+| .addI, x, y => x + y
+| .subI, x, y => x - y
+| .mulI, x, y => x * y
+| .divI, x, y => x / y -- TODO: double-check semantics
+| .modI, x, y => x % y -- TODO: double-check semantics
+--| .addR, x, y => x + y
+--| .subR, x, y => x - y
+--| .mulR, x, y => x * y
+--| .divR, x, y => x / y -- TODO: double-check semantics
+| .imp, a, b => a → b
+| .and, a, b => a ∧ b
+| .or, a, b => a ∨ b
+| .equiv, a, b => a = b
+
+def denoteRelationOp : (BEq (TyA A)) -> RelationOp A -> TyA A -> TyA A -> Bool
+| _, .eq, a, b => a == b
+| _, .neq, a, b => a != b
+| _, .lessI, x, y => x < y
+
+def denoteAppliable [Monad m] : Appliable A B -> m (TyA A -> TyA B)
+| .binop op => pure (denoteBinaryOp op)
+| .unop op => pure (denoteUnaryOp op)
+| .relop eq op => pure (denoteRelationOp eq op)
+| .mapSelect => pure (λ x => x)
+
+-- We can denote an expression using an arbitrary function to retrieve
+-- the value of a variable. We make it monadic so that it can, if desired
+-- work in a state or ITree monad.
+def denoteExpr [Monad m] : Ctx m Γ -> Expr Γ A -> m (TyA A)
+| _, .lit l => pure (denoteLiteral l)
+| γ, .apply a e => do
+  pure ((<- denoteAppliable a) (<- denoteExpr γ e))
+| γ, .applyExpr fe e => do
+  pure ((<- denoteExpr γ fe) (<- denoteExpr γ e))
+| γ, .var x => γ x
+
+-- Within an ITree, we don't need to pass around a context, and can just
+-- use Mem.read.
+def denoteExprI : Expr Γ A -> ITree (Mem Γ) (TyA A) :=
+  denoteExpr Mem.read
+
+instance exprITree : ToITree (Expr Γ A) (Mem Γ) (TyA A) where
+  toITree e := denoteExprI e
+
+def denotePassiveCommand : PassiveCommand Γ -> ITree (Mem Γ & AmAt) Unit
+| .assert e => do assert (<- denoteExprI e)
+| .assume e => do assume (<- denoteExprI e)
+
+def denoteCommand : Command Γ -> ITree (Mem Γ & AmAt & E) Unit
+| .passive p => denotePassiveCommand p
+| .assign x e => do Mem.write x (<- denoteExprI e)
+
+def denoteTransferCommand : (c: TransferCommand b Γ) -> ITree (Mem Γ & AmAt & Choice) (Fin b ⊕ Unit)
+| .goto ls => goto ls
+| .ret => .ret (.inr ())
+
+def denoteBlock (blk: Block (Command Γ) Unit b Γ) : ITree (Mem Γ & AmAt & Choice) (Fin b ⊕ Unit) := do
+  forM blk.simpleCmds denoteCommand
+  denoteTransferCommand blk.transferCmd
+
+def denoteBlocks (bs: Fin b -> Block (Command Γ) Unit b Γ) (b0: Fin b) : ITree (Mem Γ & AmAt & Choice) Unit :=
+  Iter.iter (λ bi => denoteBlock (bs bi)) b0
+
+def WhileEarly [Iter M] (c : M Bool) (body : M (Fin b ⊕ Unit)) : M (Fin b ⊕ Unit) :=
+  iter (fun () => do
+    if (<- c) then
+      match (<- body) with
+      | .inl b => return .inr (.inl b)
+      | .inr _ => return .inl ()
+    else
+      return .inr (.inr ())
+  )
+  ()
+
+mutual
+def denoteStructuredCommand : StructuredCommand b Γ -> ITree (Mem Γ & AmAt & Choice) (Fin b ⊕ Unit)
+| .ite c t e =>
+  do if (<- denoteExprI c)
+     then denoteStructuredCommands t
+     else denoteStructuredCommands e
+| .while c b => WhileEarly (denoteExprI c) (denoteStructuredCommands b)
+| .cmd c => do denoteCommand c ; .pure (.inr ())
+| .transfer t => denoteTransferCommand t
+
+def denoteStructuredCommands :
+  List (StructuredCommand b Γ) ->
+  ITree (Mem Γ & AmAt & Choice) (Fin b ⊕ Unit)
+| [] => .pure (.inr ())
+| c :: cs => do
+  match (<- denoteStructuredCommand c) with
+  | .inl b => .pure (.inl b)
+  | .inr _ => denoteStructuredCommands cs
+end

LeanBoogie/Dsl.lean

@@ -103,6 +103,8 @@ section Syntax
   syntax "if " BoogieExpr " { " BoogieCommand* " }" ("else" " { " BoogieCommand* " }")? : BoogieCommand
   syntax "while " BoogieExpr " { " BoogieCommand* " }" : BoogieCommand
   syntax "call " BoogieIdent "(" BoogieExpr,* ")" "; " : BoogieCommand
+  syntax ident " := " "call " BoogieIdent "(" BoogieExpr,* ")" "; " : BoogieCommand
+  syntax "assert " BoogieExpr "; " : BoogieCommand
   syntax BoogieAssume : BoogieCommand
 
   declare_syntax_cat BoogieBlock
@@ -113,13 +115,18 @@ section Syntax
 
   declare_syntax_cat BoogieProc
   syntax "procedure " ident "(" BoogieVarBinder,* ")"
+    -- TODO: multiple returns
     (" returns " "(" BoogieVarBinder ")")?
     " { "
       BoogieVarCmd*
       BoogieCommand* -- these "blockless" commands will get wrapped into a block of their own, if there are any subsequent blocks
       (BoogieBlockGotoOrReturn)?
       BoogieBlock*
     " }" : BoogieProc
+
+  declare_syntax_cat BoogieFunc
+  syntax "function " ident "(" BoogieVarBinder,* ")" ": " BoogieType  : BoogieFunc
+
 end Syntax
 
 

LeanBoogie/Effect/Mem.lean

@@ -49,5 +49,5 @@ private def i : Var Γ .int := .v0
 private def b : Var Γ (.bv32) := .v1
 private def f : Var Γ (.bool ~> .int) := .v2
 private example : ITree (Mem Γ) Unit := do
-  let fn : Prop -> Int <- Mem.read f
+  let fn : Bool -> Int <- Mem.read f
   Mem.write b (fn false)

LeanBoogie/State.lean

@@ -24,6 +24,7 @@ variable {M : Type _ -> Type _} [Monad M] [Iter M]
 variable {E F : Type -> Type}
 
 def State.read (Γ) (v : Var Γ A) : StateT Γ M A := fun γ => return (γ.get v, γ)
+def State.readAll (Γ) : StateT Γ M Γ := fun γ => return (γ, γ)
 def State.write (Γ) (v : Var Γ A) (val : A) : StateT Γ M Unit := fun γ => return (.unit, γ.set v val)
 
 def State.iter [Monad M] [Iter M] {Γ : Type} (f : A -> StateT Γ M (A ⊕ B)) (a₀ : A) : StateT Γ M B :=

LeanBoogie/Syntax.lean

@@ -0,0 +1,146 @@
+import Lean
+import LeanBoogie.ConTy
+
+open LeanBoogie
+namespace LeanBoogie
+
+inductive Literal : Ty -> Type
+| intL : Int -> Literal .int
+| boolL : Bool -> Literal .bool
+| bvL : BitVec n -> Literal (.bv n)
+| realL : Real -> Literal .real
+
+inductive UnaryOp : Ty -> Type
+| notB : UnaryOp .bool
+| negI : UnaryOp .int
+
+def denoteUnaryOp : UnaryOp A -> TyA A -> TyA A
+| .notB, b => ¬b
+| .negI, n => -n
+
+inductive BinaryOp : Ty -> Type
+| addI : BinaryOp .int
+| subI : BinaryOp .int
+| mulI : BinaryOp .int
+| divI : BinaryOp .int
+| modI : BinaryOp .int
+--| addR : BinaryOp .real
+--| subR : BinaryOp .real
+--| mulR : BinaryOp .real
+--| divR : BinaryOp .real
+| imp : BinaryOp .bool
+| and : BinaryOp .bool
+| or : BinaryOp .bool
+| equiv : BinaryOp .bool -- TODO: have this in addition to .eq .bool?
+
+inductive RelationOp : Ty -> Type
+| eq : RelationOp A
+| neq : RelationOp A
+| lessI : RelationOp .int
+
+inductive Appliable : Ty -> Ty -> Type
+| unop : UnaryOp A -> Appliable A A
+| binop : BinaryOp A -> Appliable A (.map A A)
+| relop : BEq (TyA A) -> RelationOp A -> Appliable A (.map A .bool)
+| mapSelect : Appliable (.map A B) (.map A B)
+
+inductive Expr : Con -> Ty -> Type
+| lit : Literal A -> Expr Γ A
+| var : Var Γ A -> Expr Γ A
+| apply : Appliable A B -> Expr Γ A -> Expr Γ B
+| applyExpr : Expr Γ (.map A B) -> Expr Γ A -> Expr Γ B
+
+abbrev mkUn (op : UnaryOp A) (l : Expr Γ A) : Expr Γ A :=
+  .apply (.unop op) l
+abbrev mkBin (op : BinaryOp A) (l : Expr Γ A) (r : Expr Γ A) : Expr Γ A :=
+  .applyExpr (.apply (.binop op) l) r
+
+inductive PassiveCommand : Con -> Type
+| assert : Expr Γ .bool -> PassiveCommand Γ
+| assume : Expr Γ .bool -> PassiveCommand Γ
+
+inductive Command : Con -> Type
+| assign : (v : Var Γ A) -> Expr Γ A -> Command Γ
+| passive : PassiveCommand Γ -> Command Γ
+
+inductive TransferCommand (b : Nat) : Con -> Type
+-- For now, if the list is empty, it means the same thing as ret. We
+-- could choose to simply not have ret.
+| goto : List (Fin b) -> TransferCommand b Γ
+| ret : TransferCommand b Γ
+
+structure Block (C: Type) (S: Type) (b : Nat) (Γ : Con) where
+  -- These are executed in the given sequence
+  label : Fin b
+  simpleCmds : List C
+  -- This is a BigBlock, in the Boogie implementation, if structuredCmd
+  -- is present
+  structuredCmd : S
+  transferCmd : TransferCommand b Γ
+
+abbrev SimpleBlock Γ b := Block (PassiveCommand Γ) Unit b Γ
+
+inductive StructuredCommand (b: Nat) : Con -> Type
+| ite : Expr Γ .bool ->
+        List (StructuredCommand b Γ) ->
+        List (StructuredCommand b Γ) ->
+        StructuredCommand b Γ
+| while : Expr Γ .bool ->
+          List (StructuredCommand b Γ) ->
+          StructuredCommand b Γ
+| cmd : Command Γ -> StructuredCommand b Γ
+-- break is translated to goto by the front end
+| transfer : TransferCommand b Γ -> StructuredCommand b Γ
+
+abbrev BigBlock (b : Nat) (Γ : Con) := Block (Command Γ) (StructuredCommand b Γ) b Γ
+
+abbrev Command.assert (p : Expr Γ .bool) : Command Γ := .passive (.assert p)
+abbrev Command.assume (p : Expr Γ .bool) : Command Γ := .passive (.assume p)
+-- abbrev Command.goto (ns : List (Fin b)) : Command b Γ := .passive (.goto ns)
+abbrev Command.skip : Command Γ := .assume (.lit (.boolL True))
+
+structure Axiom (Γ : Con) where
+  name : Option Lean.Name
+  body : Expr Γ .bool
+
+structure Function (Γ : Con) where
+  name : Lean.Name
+  -- TODO: type parameters
+  args : Con
+  resTy : Ty
+  body : Expr (Γ ++ args) resTy
+
+structure Constant where
+  name : Lean.Name
+  ty : Ty
+  isUnique : Bool
+
+structure Variable where
+  name : Lean.Name
+  ty : Ty
+
+structure Procedure (C: Type) (S: Type) (Γ : Con) where
+  name : Lean.Name
+  b : Nat
+  effects : Type -> Type
+  inParams : Con
+  locals : Con
+  outParams : Con
+  -- TODO: contracts
+  body : Fin b -> Block C S b (Γ ++ inParams ++ locals ++ outParams)
+
+inductive Declaration (Γ : Con) : Type 1
+| axiomDecl : Axiom Γ -> Declaration Γ
+| functionDecl : Function Γ -> Declaration Γ
+| constantDecl : Constant -> Declaration Γ
+| procedureDecl : Procedure C S Γ -> Declaration Γ
+| globalVarDecl : Variable -> Declaration Γ
+
+structure Program where
+  Γ : Con
+  declarations : Declaration Γ
+
+abbrev Ctx m [Monad m] (Γ : Con) := {A : Ty} -> Var Γ A -> m (TyA A)
+abbrev Ctx.get [Monad m] : Ctx m Γ -> Var Γ A -> m (TyA A)
+| γ => γ
+abbrev Ctx.extend [Monad m] : Ctx m Γ -> TyA A -> Ctx m (A :: Γ) := sorry

LeanBoogie/WP.lean

@@ -0,0 +1,55 @@
+import Lean
+import ITree
+import LeanBoogie.ConTy
+import LeanBoogie.Denotation
+import LeanBoogie.State
+import LeanBoogie.Syntax
+import LeanBoogie.Effect.AssumeAssert
+import LeanBoogie.Effect.Mem
+
+open ITree
+open LeanBoogie
+
+namespace LeanBoogie
+
+def wpPassiveS : PassiveCommand Γ -> Expr Γ .bool -> Expr Γ .bool
+| .assert P, Q => mkBin .and P Q
+| .assume P, Q => mkBin .imp P Q
+
+def wpPassiveCommandsS : List (PassiveCommand Γ) -> Expr Γ .bool -> Expr Γ .bool
+| [], Q => Q
+| c :: cs, Q => wpPassiveS c (wpPassiveCommandsS cs Q)
+
+def wpTransferCommandS : (Fin b -> Expr Γ .bool) -> TransferCommand b Γ -> Expr Γ .bool -> Expr Γ .bool
+| blkVar, .goto ls, _ => List.foldl (λ a b => mkBin .and a b) (.lit (.boolL True)) (List.map blkVar ls)
+| _, .ret, Q => Q
+
+def wpPassiveBlockS (blkVar: Fin b -> Expr Γ .bool) (blk: SimpleBlock Γ b) (Q: Expr Γ .bool) : Expr Γ .bool :=
+  mkBin .equiv (blkVar blk.label) (wpPassiveCommandsS blk.simpleCmds (wpTransferCommandS blkVar blk.transferCmd Q))
+
+def wpPassiveD : Ctx Id Γ -> PassiveCommand Γ -> Prop -> Prop
+| γ, .assert P, Q => (Id.run (denoteExpr γ P)) ∧ Q
+| γ, .assume P, Q => (Id.run (denoteExpr γ P)) → Q
+
+theorem wpPassiveDCorrect :
+  { Γ : Con } ->
+  { γ : Ctx Id Γ } ->
+  { Q : Expr Γ .bool } ->
+  ( c : PassiveCommand Γ ) ->
+  wpPassiveD γ c (Id.run (denoteExpr γ Q)) = Id.run (denoteExpr γ (wpPassiveS c Q)) :=
+  by intros Γ γ Q c
+     unfold wpPassiveS wpPassiveD
+     unfold mkBin
+     cases c <;>
+       (simp [denoteExpr, denoteAppliable, denoteBinaryOp] ; repeat rw [Id.run])
+
+def wpPassiveCommandsD : Ctx Id Γ -> List (PassiveCommand Γ) -> Prop -> Prop
+| _, [], Q => Q
+| γ, c :: cs, Q => wpPassiveD γ c (wpPassiveCommandsD γ cs Q)
+
+def wpTransferCommandD : (Fin b -> Prop) -> TransferCommand b Γ -> Prop -> Prop
+| blkVar, .goto ls, _ => List.foldl (λ a b => a ∧ b) True (List.map blkVar ls)
+| _, .ret, Q => Q
+
+def wpPassiveBlockD (γ : Ctx Id Γ) (blkVar: Fin b -> Prop) (blk: SimpleBlock Γ b) (Q: Prop) : Prop :=
+  blkVar blk.label = wpPassiveCommandsD γ blk.simpleCmds (wpTransferCommandD blkVar blk.transferCmd Q)