## 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))))