F* verification conditions
We encode this to SMT
The encoding
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))))))
type nat = x:int{x>=0}
let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))
nat
:
(assert (forall ((@x Term))
(iff (HasType @x nat) (and (HasType @x int) (>= (BoxInt_proj @x) 0)))))
(declare-fun n () Term)
(assert (not (implies (and (HasType n nat) (not (= n (BoxInt 0))))
(Valid (Precedes (op_Subtraction n (BoxInt 1)) n)))))
(assert (forall ((@x Term) (@y Term))
(implies (and (HasType @x nat) (HasType @y nat)
(< (BoxInt_proj @x) (BoxInt_proj @y)))
(Valid (Precedes @x @y)))))
type nat = x:int{x>=0}
let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))
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 ))))
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))))