module Fstar_verification
open FStar.Mul
(** There are two approaches to verification in F*
(1) Intrinsically at definition time
(2) Extrinsically through SMT-backed lemmas
We have already seen several examples of intrinsic verification.
*)
val factorial : nat -> Tot nat (* type nat = x:int{x >= 0} *)
let rec factorial n =
if n = 0 then 1 else n * factorial (n-1)
(* We can also equivalently write pre- and post-conditions for this *)
val factorial2 : x : int -> Pure int (requires (x >= 0))
(ensures (fun y -> y >= 0))
let rec factorial2 n =
if n = 0 then 1 else n * factorial2 (n-1)
(* In fact, [Tot] is essentially just an abbreviation:
[Tot t = Pure t (requires True) (ensures (fun _ -> True))]
Similarly, [Dv] is just an abbreviation for:
[Dv t = Div t (requires True) (ensures (fun _ -> True))]
Also, requires and ensures are there only for readability. You can drop them
if you want.
*)
val factorial3 : x : int -> Pure int (x >= 0) (fun y -> y >= 0)
let rec factorial3 n =
if n = 0 then 1 else n * factorial3 (n-1)
(******************************************************************************)
(** A high-level view of types in F*
You can view types in F* as belonging to two "kinds"
* Value types (V) -- int, int list, ...
* Computation types (C) -- Tot t, Dv t, ...
Types can also be refined:
* Refined value types -- x:t{p}
* Refined computation types
+ Pure t pre post
+ Div t pre post
Dependent functions are of the form
[x0:t0 -> ... -> xn:tn{x1...xn-1} -> C ]
where the notation {x1...xn-1} sal2 that the variables x1 to xn-1 may appear
free in the refinement.
*)
(******************************************************************************)
(* Intrinsically verifying append *)
val length : list 'a -> Tot nat
let rec length l =
match l with
| [] -> 0
| _::ls -> length ls + 1
val append : l1:list 'a -> l2:list 'a -> l3:list 'a{length l3 = length l1 + length l2}
let rec append l1 l2 =
match l1 with
| [] -> l2
| x::xs -> x::(append xs l2)
(******************************************************************************)
(* Extrinsically verifying append
We can under specify the type of [append] and verify the fact about length as
a separate lemma.
*)
val append2 : list 'a -> list 'a -> list 'a
let rec append2 l1 l2 =
match l1 with
| [] -> l2
| x::xs -> x::(append2 xs l2)
val append_len :
l1:list 'a -> l2:list 'a ->
Pure unit (requires True)
(ensures (fun _ -> length (append2 l1 l2) = length l1 + length l2))
let rec append_len l1 l2 =
match l1 with
| [] -> ()
(* To show: length (append2 [] l2) = length [] + length l2 *)
(* Still to show after computation: length l2 = 0 + length l2 *)
| x::xs -> append_len xs l2
(* Know recursive call's postcondition (rec_post): length (app xs l2) = length xs + length l2 *)
(* To show: len (append2 (x::xs) l2) = length (x::xs) + length l2 *)
(* Simplify: 1 + len (append2 xs l2) = (1 + length xs) + length l2 *)
(* Still to show: rec_post ==> 1 + length (append2 xs l2) = (1 + length xs) + length l2 *)
(** Lemma Syntactic Sugar
Lemma (post) = Pure unit (requires True) (ensures (fun _ -> post))
Lemma (pre) (post) = Pure unit (requires pre) (ensures (fun _ -> post))
*)
let rec append_len2 (l1 l2 : list 'a) :
Lemma (length (append2 l1 l2) = length l1 + length l2) =
match l1 with
| [] -> ()
| x::xs -> append_len2 xs l2
(******************************************************************************)
(** Some times Lemmas are unavoidable. *)
let snoc l h = l @ [h]
(* [#a] is an implicit argument for the [rev] function. You don't need to
specify it explicitly when calling the function. But can be optionally
added. *)
val rev: #a:Type -> list a -> Tot (list a)
let rec rev (#a:Type) l =
match l with
| [] -> []
| hd::tl -> snoc (rev (* #a *) tl) hd
(* We want to show that [forall l. rev(rev l) = l]. But this cannot be directly
expressed as refinement as F* needs to apply two separate inductions,
neither of which it can apply *)
(*
val rev2 : #a:Type -> f:(list a -> Tot (list a)){forall l. f(f(l)) == l}
let rev2 (#a:Type) l =
match l with
| [] -> []
| hd::tl -> snoc (rev tl) hd
*)
val rev_snoc: #a:Type -> l:list a -> h:a -> Lemma (rev (snoc l h) == h::rev l)
let rec rev_snoc (#a:Type) l h =
match l with
| [] -> ()
| hd::tl -> rev_snoc tl h
val rev_involutive: #a:Type -> l:list a -> Lemma (rev (rev l) == l)
let rec rev_involutive (#a:Type) l =
match l with
| [] -> ()
| hd::tl ->
// (1) [rev (rev tl) == tl]
rev_involutive tl;
// (2) [rev (snoc (rev tl) hd) == hd::(rev (rev tl))]
rev_snoc (rev tl) hd
// These two facts are enough for Z3 to prove the lemma:
// rev (rev (hd :: tl)) == hd::tl {To Prove}
// rev (snoc (rev tl) hd) == hd::tl {By def}
// hd::(rev (rev tl)) == hd::tl {By (2)}
// hd::tl == hd::tl {By (1)}
(******************************************************************************)
(** More verification
Let's define membership on list. Unlike OCaml, F* doesn't provide equality
on every type. This is because not all types have decidable equality. So in
order to write mem we cannot quantify over arbitrary types, but only over
those with decidable equality. *)
(* [#a:eqtype] is syntactic sugar for [#a:Type{hasEq a}] *)
val mem: #a:eqtype -> a -> list a -> Tot bool
let rec mem #a x xs =
match xs with
| [] -> false
| hd :: tl -> hd = x || mem x tl
val append_mem: #a:eqtype -> l1:list a -> l2:list a -> x:a
-> Lemma (mem x (append l1 l2) <==> mem x l1 || mem x l2)
let rec append_mem (#a:eqtype) l1 l2 x =
match l1 with
| [] -> ()
| hd::tl -> append_mem tl l2 x
// mem x (hd::(append tl l2)) <==> hd=x || mem x tl || mem x l2.
(* [rev] is injective *)
val rev_injective : #a:Type -> l1:list a -> l2:list a
-> Lemma (requires (rev l1 == rev l2))
(ensures (l1 == l2))
let rec rev_injective (#a:Type) l1 l2 =
rev_involutive l1; rev_involutive l2
//Use the fact that every involutive function is injective
(******************************************************************************)
(** Insertion Sort
Let us implement and verify an insertion sort algorithm.
*)
val sorted: list int -> Tot bool
let rec sorted l = match l with
| [] -> true
| [x] -> true
| x::y::xs -> (x <= y) && (sorted (y::xs))
val meml: int -> list int -> Tot bool
let rec meml a l = match l with
| [] -> false
| hd::tl -> hd=a || meml a tl
val sorted_smaller:
x:int ->
xs:list int ->
m:int ->
Lemma (requires (sorted (x::xs) /\ mem m xs))
(ensures (x <= m))
(* [SMTPat (sorted (x::xs)); SMTPat (mem m xs)] *)
let rec sorted_smaller x xs m = match xs with
| [] -> ()
| y::ys -> if y=m then () else sorted_smaller x ys m
val insert_sorted :
a:int ->
l:list int{sorted l} ->
Tot (r:list int{sorted r /\ (forall x. mem x r <==> x==a \/ mem x l)})
let rec insert_sorted a l = match l with
| [] -> [a]
| x::xs ->
if a <= x then
a::l
else
(* Solver implicitly uses the lemma: sorted_smaller x xs a *)
x::(insert_sorted a xs)
(* Insertion sort *)
val sort : l:list int -> Tot (m:list int{sorted m /\ (forall x. mem x l == mem x m)})
let rec sort l = match l with
| [] -> []
| x::xs -> insert_sorted x (sort xs)