From F* to SMT

SMT encoding

• F* verification conditions

  • classical, dependently typed, higher-order logic

• We encode this to SMT

  • FOL + equality and function symbols + arithmetic + e-matching
  • goals: soundness, predictability, efficiency, scalability
  • pragmatic balance between completeness and practical tractability

• The encoding

  • preserves types
  • combines a deep and a shallow embedding of F* terms
  • allows bounded unrolling of recursive and inductive definitions
  • eliminates first-class functions by lambda lifting
  • uses SMT-patterns extensively to guide instantiation of quantifiers
  • currently targets only Z3 (but some early experiments with CVC4)

Encoding primitive operations and types

• Primitive types (booleans, integers…) are boxed

  (declare-sort Term)
  
  (declare-fun BoxInt (Int) Term)
  (declare-fun BoxInt_proj (Term) Int)
  (assert (forall ((@x Int)) (= (BoxInt_proj (BoxInt @x)) @x)))
  
  (declare-fun Prims.int () Type)
  (assert (forall ((@x Int)) (HasType (BoxInt @x) Prims.int))))

  Operators are given shallow semantics:

   (assert (forall ((@x Term) (@y Term))
     (= (op_Subtraction @x @y) (BoxInt (- (BoxInt_proj @x) (BoxInt_proj @y))))))

Typechecking factorial

type nat = x:int{x>=0}
let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))

• Encoding type nat:

  (assert (forall ((@x Term))
  (iff (HasType @x nat) (and (HasType @x int) (>= (BoxInt_proj @x) 0)))))

• Proving termination:

  (declare-fun n () Term)
  (assert (not (implies (and (HasType n nat) (not (= n (BoxInt 0))))
                        (Valid (Precedes (op_Subtraction n (BoxInt 1)) n)))))

• Can be proved because of this axiom:

  (assert (forall ((@x Term) (@y Term))
           (implies (and (HasType @x nat) (HasType @y nat)
                         (< (BoxInt_proj @x) (BoxInt_proj @y)))
                    (Valid (Precedes @x @y)))))

Typechecking factorial (2)

type nat = x:int{x>=0}
let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))

• Return value is nat

  (declare-fun n () Term)
  (assert (HasType n nat))
  (assert (forall ((@x Term))
                (implies (and (HasType @x nat) (Valid (Precedes @x n)))
                         (HasType (factorial @x) nat))))

  (assert (not (ite (BoxBool_proj (op_Equality int n (BoxInt 0)))
                  (>= 1 0)
                  (>= (BoxInt_proj (op_Multiply n
                        (factorial (op_Subtraction n (BoxInt 1))))) 0 ))))

Allowing SMT solver to do bounded unrolling

type nat = x:int{x>=0}
let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))

(declare-datatypes () ((Fuel (ZFuel) (SFuel (prec Fuel)))))
(declare-fun MaxFuel () Fuel)
(assert (= MaxFuel (SFuel (SFuel ZFuel))))

(assert (forall ((@f Fuel) (x Term))
        (implies (HasType x nat)
                 (= (factorial_fuel (SFuel @f) x)
                    (ite (op_Equality int x (BoxInt 0))
                         (BoxInt 1)
                         (op_Multiply x
                                (factorial_fuel @f
                                     (op_Subtraction x (BoxInt 1)))))))))

(assert (forall ((@x Term)) (= (factorial @x) (factorial_fuel MaxFuel @x))))