Weakest precondition in pure smtlib2 using reflection and define-fun-rec

README.md

Computing weakest precondition of Imp programs directly in Z3. Requires reflection of smtlib expressions into expression datatypes and representing the variable store as an array. In principle, smtlib is it's own macro system.

Typically people use python or some other language to generate smtlib. Boogie and Why3 are frameworks that generate smtlib (among other things) from imperative code. We can remove one level of indirection by directly programming in Z3. There are so many other good abstractions that smtlib is just barely able to express in this style.

Upside:

• All in one system. Custom DSLs and logics that embed in the super power that is Z3

Downside:

• More for solver to do. There is no way to express everything can be done at compile time. The behavior of define-fun-rec is a bit finicky
• My encoding for WP of loops didn't seem to be playing very nice with define-fun-rec unfolding. Loops are kind of a big deal
• Verbose. Lots of boiler plate. Lack of higher order functions makes shallow embedding difficult / impossible. Some calculations in WP play with binding structures, so we have to go deep embedding

wp.smt2

(define-sort Var () String)
(define-sort Env () (Array Var Int))
(declare-datatypes ()(
  (Term ; Reflect Int Expressions
    (Var (var1 Var))
    (Lit (lit1 Int))
    (Add (add1 Term) (add2 Term))
    (Sub (sub1 Term) (sub2 Term))
    ; And so on
  )
  (Formula ; Reflect Bool Expr
    (And (and1 Formula) (and2 Formula))
    (Or (or1 Formula) (or2 Formula))
    (Impl (impl1 Formula) (impl2 Formula))
    (Eq (eq1 Term) (eq2 Term))
    (Lte (lte1 Term) (lte2 Term))
    (Not (not1 Formula))
    (Let (let1 String) (let2 Term) (let3 Formula))
    (IteF (ite1 Formula) (ite2 Formula) (ite3 Formula))
     ; (Forall (forall1 Formula))
    ; And so on
  )
  (Stmt 
    (Skip)
    (Set (set1 Var) (set2 Term))
    (Seq (seq1 Stmt) (seq2 Stmt))
    (IteS (ite-cond Formula) (ite-then Stmt) (ite-else Stmt))
     ; (While (while-cond Formula) (while-inv Formula) (while-body Stmt))
)))

(define-fun-rec eval-term ((t Term) (rho Env)) Int
  (match t (
    ((Lit i) i)
    ((Var v) (select rho v))
    ((Add x y) (+ (eval-term x rho) (eval-term y rho)))
    ((Sub x y) (- (eval-term x rho) (eval-term y rho)))
)))

(define-fun-rec eval-form ((f Formula) (rho Env)) Bool
  (match f (
    ((Eq x y) (= (eval-term x rho) (eval-term y rho)))
    ((Lte x y) (<= (eval-term x rho) (eval-term y rho))) 
    ((And x y) (and (eval-form x rho) (eval-form y rho)))
    ((Or x y) (or (eval-form x rho) (eval-form y rho)))
    ((Impl x y) (=> (eval-form x rho) (eval-form y rho)))
    ((Not x) (not (eval-form x rho)))
    ((Let v t f) (eval-form f (store rho v (eval-term t rho))))
    ;((Forall b)  (forall ((rho Env)) (eval-form b rho)))
    ((IteF c t e) (ite (eval-form c rho) 
                       (eval-form t rho) (eval-form e rho)))
)))
; Term is a first order representation of Env -> Int
; Formula is a first order representation of Env -> Bool.
(define-fun-rec eval-wp ((prog Stmt) (post Formula)) Formula
  (match prog (
    (Skip post)
    ((Seq s1 s2) (eval-wp s1 (eval-wp s2 post)))
    ((Set v e) (Let v e post))
    ((IteS c t e) (IteF c (eval-wp t post) (eval-wp e post)))
    ; ((While cond inv body) (And inv (Forall (Impl inv (IteF cond (eval-wp body inv) post)))))
  )
  )
)
  
(define-const myprog Stmt
  (Seq (Set "x" (Lit 7))
       (IteS (Lte (Var "z") (Lit 0))
            (Set "y" (Var "x"))
            (Set "y" (Lit 1))
)))

(check-sat)
(get-model)
(declare-const rho Env)
(eval (eval-form (eval-wp myprog (Eq (Var "y") (Var "z"))) rho))
; (ite (<= (select rho "z") 0) 
;      (= 7 (select rho "z")) 
;      (= 1 (select rho "z")))


; helpers for longer sequences of statements
(define-fun begin2 ((s0 Stmt) (s1 Stmt)) Stmt
  (Seq s0 s1)
)
(define-fun begin3 ((s0 Stmt) (s1 Stmt) (s2 Stmt)) Stmt
  (Seq s0 (begin2 s1 s2))
)
(define-fun begin4 ((s0 Stmt) (s1 Stmt) (s2 Stmt) (s3 Stmt)) Stmt
  (Seq s0 (begin3 s1 s2 s3))
)