This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. Learn more

F* is a verification-oriented programming language developed at Microsoft Research. It follows in the tradition of the ML family of languages in that it is a typed, strict, higher-order programming language. However, its type system is significantly richer than ML's, allowing functional correctness specifications to be stated and checked semi-automatically.

This tutorial provides a first taste of verified programming in
F*. We will focus initially on writing several small, purely
functional programs and write specifications for these programs that
can be automatically verified by F*. Next, we will discuss verifying
higher-order programs that also make use of state. Finally, we
consider designing and implementing a small cryptographic protocol in
a style suitable for verification. Be sure to follow along with the
examples by clicking the **load in editor** link in the corner. See
what F* says, try your own programs, and experiment!

It will help if the reader is already familiar with functional programming languages in the ML family, e.g., Standard ML, Ocaml, F#, or Haskell---we provide a quick review of basic concepts for those a little rusty. If you lack this background, there are several useful resources on the web, e.g., TryF#, or this introduction to Caml.

Please send feedback, comments and/or corrections regarding this tutorial to Nikhil Swamy by email at the following address: nswamy 'AT' microsoft 'DOT' com.

We have used F* to construct many verified programs, including implementations of security protocols, web servers, web browser extensions, and even parts of the F* compiler itself. F* can also be used as an intermediate verification language. Rather than writing programs in F* directly, programs written in other languages can be translated to F* and then verified. We have built translations from a variety of languages to F*, including JavaScript, F7, and DKAL. F* can also be securely compiled to various platforms. For example, this paper describes how we compile F* to .NET bytecode while preserving types; and this page describes a fully abstract translation from F* to JavaScript.

To find out more, check out the F* website: you'll find links to several papers and to a compiler download (including sources). With the compiler, you will be able to run F* programs, provided you have the .NET 4.0 virtual machine installed.

Here's a quick review of the language, including its syntax and key typing rules.

Kinds k ::= S //Kind of non-affine value types | E //Kind of non-constructive propositions | P //Kind of constructive propositions | A //Kind of affine types | x:t => k //Dependent product from values to kinds | 'a:k => k //Dependent product from types to kinds Binders b ::= (x:t) | ('a:k) //Value- or type-binder | x | 'a //Unascribed binder Types t ::= 'a //Variable | Tc //Constant | x:t[{phi}] -> t' //Dependent function, optionally refined domain | 'a:k -> t //Dependent function, from types to values | t t' //Type/type application | t v //Type/value application | x:t{phi} //Refined type | x:t[{phi}] * t //Dependent pair, optionally refined lhs | fun b => t //Type function literal Formulas phi ::= forall b1..bn.{:pattern (phi1;...;phim)} phi //forall with instantiation patterns | exists b1..bn.{:pattern (phi1;...;phim)} phi //exists with instantiation patterns | phi /\ phi | phi \/ phi | not phi //usual connectives | v1 = v2 | v1 > v2 | v1 < v2 | ... //theory terms | t //extensible with other connectives described by types Data/logic D ::= C //[Qualified] Data constructor name | L //[Qualified] Logic function name Values v ::= x //Variable | () | 0 | 1 | ... | c //Constants | D [(t1|v1)...(tn|vn)] //Fully-applied data constr. or logic func. | fun b -> e //Lambda abstraction over values or types Expressions e ::= v //Value | e1 e2 //Application | e t //Type application | let x = e1 in e2 //Let binding | let rec f = v //[Mutually] recursive let binding [and f1=v1 ... and fn=vn] in e | match e with br1..brn //Pattern matching | assert phi //Checked assertion | assume phi //Admitted formula | {[e with] f1=e1;...;fn=en} //Record literal | e.f //Projection | (e <: t) //Ascription (with subtyping) | e1 := e2 //Assignment | !e //Dereference | ref e //Allocation | raise e //Raising exceptions | try e with br1..brn //Handling exceptions | ... branches br ::= BAR pat -> e //Pattern matching branch pattern pat ::= _ | b | C p1 .. pn | c //Nested patterns Type decl td ::= [logic data] type t b1..bn //Type declaration (with parameters) Type def tdef ::= td //abstract type | td = t //type abbreviation | td = BAR D1:t1 BAR ... BAR Dn:tn //algebraic type | {f1:t1; ...; fn:tn} //record Top level tl ::= val x : t //value declaration | logic val L:t //logic value decl. | let [rec] x1 = e1 //let binding with mutual rec. [and ... and xn = en] | open M //open namespace | tdef //type definition | (assume | define | query) Name:phi //assumption, definition, query Module m ::= module M tl1 ... tln ;; e [end] Program p ::= m | m p

In addition to the syntax above, F* provides many syntactic conveniences familiar to ML programmers, e.g., sequencing is e1;e2; let bindings may use patterns, etc.

G |- e : x:t -> t' G |- v : t ------------------------------------ G |- e v : t'[v/x] G |- e : t G,x:t |- e' : t' x not in FV(t') ------------------------------------------------------ G |- let x = e in e' : t' G |- v : t G, b1..bn |- C b1..bn : t' t ~ t ~~> eqs G, b1..bn, eqs, v=C b1..bn |- e : t'' ----------------------------------------------------------- G |- match v with C b1..bn -> e | ... : t'' G |- v : t ----------------------------- G |- v : x:t{x=v} G |- unit <: x:unit{phi] G |- phi : E ---------------------------------- --------------------------------- G |- assert phi : x:unit{phi} G |- assume phi : x:unit{phi} G |- t <: t' ----------------------------- G |- e : t' Subtyping: G,x:t |=_{Z3} phi ---------------------- ---------------------- G |- x:t{phi} <: t G |- t <: x:t{phi} G |- s1 <: t1 G,x:s1 |- t2 <: s2 ----------------------------------------- G |- x:t1 -> t2 <: x:s1 -> s2 G |- t ~ t' G |- t1 <: t2 G |- t2 <: t3 ---------------------- --------------------------------- G |- t <: t' G |- t1 <: t3 Type equivalence: G |- t ~ t' G |=_{Z3} v = v' --------------------------------- ... G |- t v ~ t' v' Sub-kinding: ---------- ----------- ----------- ... S <: E A <: E P <: E

An F* program is composed of several modules. Each module begins with a module declaration, defining the name of the module. Here's "hello world" in F*:

load in editormodule HelloWorld let _ = print "Hello world!"

The let _ = e construct at the end of a module declaration defines its "main" function.

Types in F* are used to describe properties of program expressions. For example, the expression 0 can be given the type int. The standard prelude of F* (a module called Prims) defines several types such as unit, int, and string. Values for each of these types are defined primitively in F*. The following snippet shows a few ways in which expressions can be ascribed types in F* (via the ":" operator on binders and "<:" on any subterm in a program).

load in editorlet u = (() <: unit) let z = (0 <: int) let z' : int = 1 - 1 let z'' = (1 - 1 <: int) let hello : string = "hello"

Just as types describe properties of expressions, F*
uses *kinds* to describe properties of types. In most
programming languages, the kinds that describe properties of types are
implicit. Usually, there is just a single kind of types,
called *
(pronounced "star"). Common types
like int, or
string
all usually have
kind *.
In F*, these kinds are more evident---for reasons that we will see
shortly, and we need more than one base kind. So, instead of
writing *,
the base
module Prims
defines all these types to have
kind S
in F* (using the "double colon" operator, as shown below).

type unit : S type int : S type string : S

When defining a type, if no kind is specified explicitly and the kind cannot be inferred from the RHS of the definition, the default kind is S.

Prims also defines some commonly used derived types like the type of polymorphic lists, shown below.

type list 'a = | Nil : list 'a | Cons : 'a -> list 'a -> list 'a

The type list 'a (of kind S) is the datatype of finite lists of 'a-typed values. The type variable 'a ranges over all S-kinded types. If you're used to programming in a language like C# or Java, you're probably familiar with the generic types given to collections---the list 'a type is similar.

The datatype list 'a has two data constructors. The first constructor, Nil, is an empty list. The second constructor, Cons, is given a function type, showing that it builds a list 'a value from an 'a-typed value and another list 'a.

The F* parser provides special syntax for building and pattern matching list values, as shown below.

load in editorlet empty_list = Nil let empty_list_sugar = [] let cons = Cons 1 Nil let cons_sugar = 1::[] let list_3 = Cons 0 (Cons 1 (Cons 2 Nil)) let list_3_sugar = [0;1;2] let rec length = function | [] -> 0 | _::tl -> 1 + (length tl) let rec nth n = function | [] -> fail "Not enough elements" | hd::tl -> if n=0 then hd else nth (n - 1) tl

As in ML, the function length has type list 'a -> int. Likewise, the function nth has type list 'a -> 'a. Note that nth is a partial function---if the list does not have enough elements, it calls the function fail : string -> 'a defined in Prims, which aborts the program. F* also provides support for catching exceptions, but we do not describe this further in this tutorial.

As we have just noted, the
type list
'a has
kind S. But,
what
about list
itself? Intuitively, the
type list
is quite different from the
other S-kinded
types we have seen so far
(like int). There
are no values of
type list
itself, only values of types
like list
int. We think
of list
as *type constructor*, a function that builds a type of
kind S
when applied to an argument type of
kind S. We
describe such type constructors using the arrow kind,
i.e., list
has kind S =>
S.

In more explicit syntax, the type list can be defined as shown below.

type list : S => S = | Nil : 'a:S -> list 'a | Cons : 'a:S -> 'a -> list 'a -> list 'a

We have defined a type
constructor list
of kind S =>
S, with two data constructors. This time,
the Nil
constructor takes a single * type argument*, a
type 'a
of
kind S,
and build an empty list of
type list
'a. (In other languages, such a type may sometimes be
written forall
'a::*. list 'a.) The type
of Cons
is similar, except, like
Nil, it also takes an explicit
type argument.

In general, a polymorphic type is written using the notation 'a:k -> t, where the type variable 'a is of kind k, and the variable appears free to the right of the arrow, i.e., in the type t. By default, as in ML, a type t is understood to be implicitly prenex quantified over its free type variables, each of which are, by default, of kind S. For example, the function length which we said before has type list 'a -> int---this type is a synonym for the type 'a:S -> list 'a -> int, which explicitly quantifies over the type variable.

For the most part, as in ML, F* programmers do not have to explicitly write type applications---whether declared as Cons: 'a -> list 'a -> list 'a, or Cons: 'a:S -> 'a -> list 'a -> list 'a, programmers can just write (Cons 1 Nil) and the F* typechecker will infer the type argument to be int.

However, as the types become more elaborate, in particular when using first-class polymorphism or when quantifying over non-S-kinded types, the problem of inferring these type arguments becomes undecidable. Thus, when using the full power of the F* type system, programmers may have to provide explicit type arguments. In any case, a programmer can always write explicit type applications (with the same juxtaposition syntax as for value applications), as shown below.

load in editorlet intlist = Cons 0 Nil let intlist' = Cons int 0 (Nil int) let mkCons ('a:S) (x:'a) (tl:list 'a) = Cons 'a x tl

For the remainder of this guide, unless strictly required, we will omit explicit quantification over type arguments as well as type applications.

type ref : S => S val ref : 'a -> ref 'a val (:=) : ref 'a -> 'a -> unit val (!) : ref 'a -> 'a

This snippet defines an abstract type ref of references to S-kinded types. The type support three operations---the signatures of these operations uses F*'s syntax for val-declarations. The value ref allocates a new reference; the binary operator (:=) updates a ref cell; and the unary operator (!) is for dereference.

So far, what we have seen is not particularly remarkable: this is the fragment that F* shares with other ML-like programming languages. In this section, we begin to do some dependently typed programming in F*, going beyond what is expressible in ML directly.

The list 'a type we saw earlier is relatively imprecise. For example, from the type alone, it is impossible to distinguish an empty list from other lists. Using dependent types in F* we can enrich the type of lists not only to distinguish the empty list, but to keep track of the length of a list in its type. Using such types, we will be able to prove that a function like nth never aborts with a failure.

The type ilist n 'a below represents the type of a list of n 'a-typed elements, for some integer n.

load in editortype ilist : int => S => S = | INil : ilist 0 'a | ICons : x:'a -> n:int -> ilist n 'a -> ilist (n + 1) 'a

The kind of ilist is int => S => S, indicating that it constructs an S-kinded type from two arguments, an int-typed term and an S-kinded type.

The constructor INil builds an empty list---note that the type ilist 0 'a indicates that the size of constructed lists is zero. The ICons constructor builds list of length one greater than its tail. We describe its type in detail below.

The type
of ICons
is an instance of a dependent function type. In general, these types
have the form x:t ->
t',
where x
names
the t-typed
formal parameter and the
variable x
is in scope to the right of the arrow, i.e., in the
type t'. In
other words, the return
type t'
of the function *depends* on the value of the formal parameter.

This may seem a bit strange at first, but if you're used to writing
polymorphic functions, then you have already been writing dependently
typed programs in disguise. In the
type, 'a:S -> list
'a, the type of the co-domain (the right-hand side of
the arrow) depends on the formal type parameter, i.e., instantiating
the
type 'a
for int
and string
yields two different
types, list
int
and list
string, respectively. A dependent function is similar,
except rather than having the co-domain dependent on a type it is
dependent on the *value argument* in the function's
domain.

Looking at the type of ICons again, we see that its first argument is hd:'a is the head of the new list to be constructed; its second argument n is the length of the tail of the list; the third argument tl is the tail of the list itself. The constructed type is ilist (n + 1) 'a, indicating that the length of the constructed list is one greater than the length of tl.

We can write functions to manipulate length-indexed lists just as we would for normal lists. But, now, the types to ensure that we always keep proper track of the length of a list. For example, here's a function that appends two lists. Notice how its type captures that the length of the resulting list is the sum of the lengths of its arguments. Try playing with this example: is there any other type you could give to iappend?

load in editorval iappend: n1:int -> ilist n1 'a -> n2:int -> ilist n2 'a -> ilist (n1 + n2) 'a let rec iappend n1 l1 n2 l2 = match l1 with | INil -> l2 | ICons x n1_minus_1 l1tl -> ICons x (n1_minus_1 + n2) (iappend n1_minus_1 l1tl n2 l2)

The algorithm used by F* to typecheck iappend is roughly as follows.

- When typechecking the body of the function has its annotated type, F* assumes all the variables in scope have the types described by their annotations (or as inferred by the Hindley-Milner type inference algorithm if types are not fully provided). For the example above, F* tries to prove that the body of the function has type ilist (n1 + n2) 'a, assuming that iappend, n1, l2, n2, and l2 all have the types described in the val declaration at line 1, and that ilist and its data constructors have their declared types.
- At the third line above, F* tries to prove that the expression l2 has the type ilist (n1 + n2) 'a. F* also assumes that all conditions that guard the control flow of the program at that program point hold true. For our example, F* assumes that l1=INil. Since the type of INil is ilist 0 'a, F* can conclude that n1=0.
- Collecting all these typing assumptions and equalities, F* calls the Z3 theorem prover and asks it to prove that (n1 + n2) = n2. Z3, which is able to reason about arithmetic, easily proves this goal from the assumptions.
- At line 5, from the typing assumption about iappend, F* concludes that (iappend n1_minus_1 l1tl n2 l2) has type ilist (n1_minus_1 + n2) 'a. As at line 3, from the assumption that l1=(ICons x n1_minus_1 l1tl), F* concludes that (n1_minus_1 + 1)=n1.
- Collecting these assumptions, the goal F* presents to Z3 is to show that ((n1_minus_1 + n2) + 1)=(n1 + n2), which again Z3 is able to prove easily.

As the algorithm sketch above hints, a key part of the F* type system is an equivalence relation on types which allows converting the type of an expression from on type to another. For example, the type of l2 is annotated as ilist n2 'a, but at line 3, we see that this type is equal to ilist (n1 + n2) 'a.

Try writing the following functions on length-indexed lists. (The function signatures on normal lists are shown below.)

- reverse:list 'a -> list 'a, a function to reverse a list.
- map:('a -> 'b) -> list 'a -> list 'b.
- Try writing the same functions tail recursively.

Before moving on to more examples, a brief technical note on the language of types. So far, the language of F* types that we have seen can be summarized by the following grammar.

kinds k ::= S | t => k | k => k types t ::= 'a | Tc | x:t -> t' | 'a:k -> t | t t' | t a index terms a ::= v | a1 + a2 | a1 - a2 | ... values v ::= x | () | 0 | 1 | ... | D t1..tn v1..vm | fun x -> e | fun 'a -> e

Kinds include the S-kind; and arrows from types to kinds and from kinds to kinds.

Types include type variables; type constructors Tc (like int, or list); dependent function types from values to types (x:t -> t'), and from types to types ('a::k -> t); types applied to types like list int; and types applied to terms like ilist 0.

The language of terms a used to describe the indexes on types includes the values v of F*, i.e., variables, constants, the application of data constructors, and lambda abstractions. Additionally, index terms include some constructions like arithmetic expressions, which are not proper values in F* but, nevertheless can be used as indexes, since Z3 can reason effectively about arithmetic. Later, we show how the language of index terms can be extended in F* to include other user-defined terms and terms for other Z3 theories.

Given this language of types, we can sketch F*'s type equivalence relation. Roughly, the equivalence relation on pair of types t1 and t2 is defined in a particular typing context Γ, and is written Γ |- t1 =~= t2. The relation is defined inductively on the structure of types, where the basic case defines Γ |- t1 a1 ~ t2 a2 whenever Γ |- t1 ~ t2 and when Z3 is able to prove a1=a2 from the assumptions in Γ.

The ilist type, while useful, is sub-optimal for at least two reasons. First, our definition allows writing types like ilist (-1) 'a, which is clearly nonsensical---no list has length -1!. Second, just in order to state a property about a length of lists, we had to redefine the list type from scratch, forcing us to reimplement common functions like appending two lists. In the next two sections, we show how to address these two problems using F*'s refinement types.

We would like to adjust
our ilist
so that it only describes actual lists with non-negative lengths. For
this, we start by defining the
type nat,
the type of natural numbers, a *refinement* of the
type int.
load in editor

type nat = i:int{0 <= i}

Refinement types in F* have the form x:t{t'}, where the type t' is a type interpreted as a predicate on the bound variable x:t. We extend the syntax of types as shown below. We use the metavariable φ for types that stand for refinement formulas---formally, it's just an alias for t, although F*'s parser provides some syntactic sugar to make formulas easier to write. As we will see, the F* type system is parameterized by the choice of formulas φ---regardless of that choice, we can use the language of types to represent the syntax of refinement formulas.

types φ, t ::= ... | x:t{φ}

In the definition of nat, the predicate on the bound variable i is (0 <= i). Intuitively, an integer n can be given the type nat when the F* typechecker (using Z3) can prove that 0 <= n (i.e., that 0 is less than, or equal to, n).

Refinement types in F* are equipped with a built-in subtyping
relation. Any expression of
type x:t{t'}
is also an expression of
type t. On
the other hand, in a typing
context Γ,
a *value* v
of
type t
can be viewed as a value of
type x:t{t'}
if the
proposition t'[v/x]
is derivable from the assumptions
on Γ. We
write Γ |- t
<: t'
when t
is a subtype
of t'
in a
context Γ.

This basic subtyping relation also lifts into the structure of types. So, the subtyping relation on function types Γ |- x:t1 -> t1' <: x:t2 -> t2' is valid when Γ |- t2 <: t1 and when Γ, x:t2 |- t1' <: t2'.

For example, we have Γ |- nat <: int, and Γ |- int -> nat <: nat -> int, etc.

Let's try proving some simple properties involving natural numbers.

load in editorlet z:nat = 0 let bad:nat = -1 (* Should fail to typecheck *) let int2nat x : nat = if x < 0 then 0 else x let abs x : nat = if x < 0 then -x else x let sqr x : nat = x * x

We can easily define other refinements of integers as well. The module below defines a function countTo100, which, when given an integer n in the range [0,100], increments its argument makes (100 - n) recursive calls, incrementing its argument each time, and then returns 100.

load in editorval countTo100: n:int{0 <= n /\ n <= 100} -> x:int{x=100} let rec countTo100 n = if n < 100 then countTo100 (n + 1) else n let _ = let x = countTo100 17 in assert (x=100); ()

Using the assert construct, programmers can assert program properties and get F* to check these properties during typechecking. Note, unlike assertions in other languages, assert in F* has no runtime significance---assertions are always checked at compile time, and if the assertion cannot be proved by the typechecker, F* refuses to compile the program. Note, the argument to assert is always a type representing the proposition that must be proved statically. Here, the type is (x=0).

At this point, maybe you're a bit puzzled. How come we think of (x=0), (0 <= n) as types? They sure look like expressions in the programming language, don't they? The section clarifies this point.

In some languages, the predicates that are used in refinement formulas are just pure, boolean-valued expressions. However, what this means is that all refinement formulas must be decidable, i.e., every refinement formula is either true or false. In order to support refinement logics with undecidable or semi-decidable propositions, F* refinement formulas are viewed types that may or may not be derivable from the assumptions in a particular typing context Γ.

To distinguish the types that F* uses to describe program expressions (like int and the other *-kinded types), F* introduces a new base kind, E, for types that represent propositions in the refinement logic. E-kinded types have no operational signficance---they are, in effect, Erasable. With this extenion, our syntax of kinds now becomes:

kinds k ::= S | E | t => k | k => k

We can now see how the basic refinement predicates we have been using so far are encoded in F*---the following snippet is extracted from Prims.

type True : E type False : E type (/\) : E => E => E type (\/) : E => E => E type not : E => E type (==>) : E => E => E type (<==>) : E => E => E type (<) : int => int => E type (<) : int => int => E type (>) : int => int => E

The propositional connectives are easy to represent---we write ==> for implication (distinguishing it from the kind arrow); and <==> for bidirectional implication. The integer comparison operators are also easily encoded. F* provides special support for all these operators, allowing them to be written infix, with the usual precedence.

But, what about equality? We would like to be able to have a single equality operator to describe equality over values of all types, but, our kind language is not yet sufficiently expressive for that. Think about it: we would like to be able to give (=) the kind int => int => E as well as the kind string => string => E. We can solve this by enriching our language of kinds to include dependent kinds, just as we had dependent types at the level below.

With this in mind, we enrich the language of kinds and types to the syntax below.

kinds k ::= S | E | x:t => k | 'a:k => k types t ::= ... | fun (x:t) => t' | fun ('a:k) => t

Both the arrow forms now bind the name of the formal parameter to the right of the arrow. We also define the corresponding lambda abstractions in the type language. Concretely, a type fun (x:t) => t' has kind x:t => k in a context Γ, when t is well-kinded in Γ and when t' has kind k in the context Γ,x:t.

Using these kinds, we can now show the kind of the equality operator, and several other constructs provided by F*'s default refinement logic in Prims. As at the term level, the type and kind annotation on the formal parameters of a type-level lambda abstraction can often be left out and F* will infer it.

type (=) : 'a:S => 'b:S => 'a => 'b => E type (<=) = fun (x:int) (y:int) => x < y \/ x = y type (>=) = fun x y => x > y \/ x=y

Quantifiers are also provided by F*'s default refinement logic. We show the kinds of the universal and existential quantifiers below. F* also provides syntactic sugar to make it easier to write quantified formulas. We show the type of infinity written with and without sugar for quantified formulas---both forms are valid.

type Forall :: 'a:S => ('a => E) => E type Exists :: 'a:S => ('a => E) => E type infty = x:int{Forall int (fun y => y<>x ==> y < x)} type infty_sugar = x:int{forall y. y<>x ==> y < x}

Being able to represent the usual logical connectives and operators within the syntax of types and kinds in F* is nice, but that's only one part of the story. The kinds alone say nothing about semantics of these connectives in the refinement logic, e.g., the kinds of the universal an existential quantifiers are the same, although, clearly, they should have different interpretations in the logic.

For each refinement logic used by an F* program, a semantic encoding of the logical connectives must be provided within the typechecker. For the default logic provided by Prims, F* already provides an interpretation of the logic via a translation into (a fragment of) the logic of Z3. This is roughly first-order logic, with uninterpreted functions, equality, integer arithmetic, datatypes, and the theory of functional arrays. Describing this encoding precisely is beyond the scope of this tutorial---unless explicitly mentioned otherwise, the refinement formulas have their usual interpretation in first-order logic.

We now turn to some more simple examples of programming with a mixture of refinement and indexed types.

load in editortype ilist : nat => S => S = | INil : ilist 0 'a | ICons : x:'a -> n:nat -> ilist n 'a -> ilist (n + 1) 'a type pos = i:nat{i > 0} val head: n:pos -> ilist n 'a -> 'a let head n = function | ICons hd _ _ -> hd | INil -> assert False; fail "unreachable" val tail: n:pos -> ilist n 'a -> ilist (n - 1) 'a let tail n = function | ICons _ _ tl -> tl | INil -> assert False; fail "unreachable"

We can easily prove that taking the head or tail of list of positive length never fails. By asserting False in the default case, we prove that that branch is not reachable.

Rewrite the nth function for ilist and give it a pre-condition to ensure that it never fails. Also, give an implementation of length for ilist. (These were originally defined here.)

Length-indexed types are fun, but they're also a bit cumbersome. Just because some part of our program needs to carefully track the length of a list, we needed to redefine our list type completely, and also rewrite common library functions to manipulate our new list type. Can we do better? Intuitively, if we were able to define a length-indexed type that was a subtype of the normal list 'a type, then we could get much more reuse. F*'s refinement types provides us with the subtyping we need.

We begin by writing a specifcation for the length of a list,
entirely independent of the definition of
the list
'a datatype itself. We do this using *logical
functions* in F*, purely specificational functions that can be
used in refinement formulas but not in code itself.

logic val Len : list 'a -> nat assume Len_nil: Len []=0 assume Len_cons: forall (hd:'a) (tl:list 'a). Len (hd::tl) = (Len tl) + 1

This snippet defines a logical function Len, using the logic val construct, which defines a function symbol and its type. This, in effect, creates an uninterpreted function symbol in the refinement logic used by the F* typechecker (and Z3), and the semantics of this function is determined by an axiomatization provided by the programmer.

The axioms for Len are defined using the the assume construct. The Len_nil assumption states that the length of the empty list is zero, and the Len_cons assumption says that the length of a cons cell is one greater than the length of its tail.

In addition to the assumes, by defining the type of Len to be list 'a -> nat, we are implicitly stating that for all lists l, the formula (Len l) >= 0 is valid---Z3 will make use of this fact also when reasoning about Len.

Remember to use the assume consruct with care, paying attention, in particular, to the interaction of the assumptions with the types---the types matter! If you're not careful, you can end up with an inconsistent set of axioms from which all formulas will become derivable, making your verification efforts pointless. For example, an axiom like exists x. (Len x) < 0 would be inconsistent with the typing of Len. One way to make sure that your axioms are reasonable is to attempt to assert False immediately after introducing some assumptions. If you succeed, then something's gone wrong. Let's try:

load in editorassume Bad: exists (x:list 'a). Len x < 0 let _ = assert False

See, we're able to prove False by assuming something bad about the length of lists. So, be careful what you assume!

Using the logical function Len, we can define the type below llist n 'a as a refinement of list 'a.

load in editortype llist = fun (n:nat) ('a:S) => l:list 'a{Len l=n}

The snippet above defines a new type abbreviation llist. The right-hand side defines a type function---in effect, llist n t is an abbreviation for l:list 'a{Len l=n}.

The example below shows an implementation of append for the llist type.

load in editorval lappend: n1:nat -> llist n1 'a -> n2:nat -> llist n2 'a -> llist (n1 + n2) 'a let rec lappend n1 l1 n2 l2 = match l1 with | [] -> l2 | hd::tl -> hd::lappend (n1 - 1) tl n2 l2

You will have noticed that lappend is similar to what we had before with iappend. But, because of refinement subtyping, we can also pass llists to the functions in the list library, e.g., map : ('a -> 'b) -> list 'a -> list 'b, or even to the standard list append : list 'a -> list 'a -> list 'a.

But, there's no free lunch here, I'm afraid. Notice that the type signature of lappend is quite different from append---it even takes two additional parameters. (Note, the additional parameters could be remedied by considering the two integer parameters to be implicit, but, currently, F* does not support implicit parameters.) Further, if we were to use the normal append with llists, we get back a value in the plain list type, losing the refinement property. Thus, while refinements give you some useful code re-use, if you want to capture precise properties about your data structures, you still need to write and verify functions specialized to those properties.

Before going further, let's look closely at how lappend is typechecked.

- As before, we try to typecheck the
body of the function at the
type llist (n1 + n2)
'a, in a context that assuming the types and kinds of
all the term and type variables in scope,
*as well as all the formulas introduced by all the assumes in scope*. - At the third line, we need to prove that l2 has type llist (n1 + n2) 'a, with the additional assumption that l1=[]. Using the assumption Len_nil, Z3 can prove that n1=0, and the proof concludes easily.
- To check the recursive call
to lappend,
the typechecker has a few things to prove using Z3.
- It must first prove that (n1 - 1) has type nat, with the additional assumption that l2=(hd::tl). Using the forward implication in Len_cons, it can conclude that n1 = (Len tl) + 1, and thus (n1 - 1) = (Len tl). At this point, we can make use of the typing assumption of Len, and since (Len tl) : nat, we can prove our goal.
- Next, it needs to prove that (Len tl)=(n1 - 1), which follows from the forward implication in Len_cons and arithmetic.
- The typechecker must also prove that n2 is a nat and that it is the length of l2, but these follow directly from the assumptions.

- Finally, to prove that hd::lappend (n1 - 1) tl n2 l2 has the desired type, F* relies on the assumption of the typing of lappend to conclude that Len (lappend (n1 - 1) t1 n2 l2)= (n1 - 1) + n2, and then uses the backward implication in Len_cons to prove that (n1 - 1) + n2 + 1 is the length of the result, which is equivalent to the result.

Redefine head, tail, nth, map, reverse, fold_right, and fold_left for the llist type.

In this section, we give a flavor of some of the techniques used to model cryptographic protocols in F*. To keep things simple, we will gloss over many issues. We will not model key compromise, where keys can be leaked to the attacker. We will ignore the marshaling formats of messages. We will freely use a single key-pair to sign arbitrary messages from a principal, when in practice, key use should be much more fine-grained. For a treatment of these and other issues, please see these lecture notes, which provides a more thorough treatment.

There are many possible paradigms for modeling cryptographic protocols. We will consider the Dolev-Yao model, a simple, but widely used framework. Roughly, the Dolev-Yao model assumes the cryptographic primitives used in a protocol to be perfect, e.g., that a hash has no collisions; or, that a cipher cannot be decrypted unless the correct decryption key is provided, etc. However, the adversary has the ability to intercept messages on the network, to rewrite and reroute these messages as it sees fit, and can use any key material that it already possesses to encrypt messages.

Verification of cryptographic protocols in the more powerful computational model has also been carried out using refinement types---see this paper for details. Describing this model is beyond the scope of this tutorial.

We start by looking at a library that provides basic support for digital signatures based on public-key cryptography. The module signature below shows a simplified version of the interface exposed by, say, the .NET standard library System.Security.Cryptography.

module SimpleCrypto type pubkey type privkey type dsig val keygen: unit -> (pubkey * privkey) val sign: privkey -> bytes -> dsig val verify: pubkey -> bytes -> dsig -> bool

We have three abstract types pubkey, for public keys; privkey, for private keys; and dsig for digital signatures. Concretely, all these three types may be aliases for bytes, the type of a byte array, but this is irrelevant for the moment.

SimpleCrypto also provides three functions. keygen constructs a new key pair. Given a private key and a plain text, sign builds a digital signature. Finally, verify allows a plain text and a claimed signature of it to be checked for authenticity using a public key. If verify pk m d = true, then the cryptography guarantees (with high probability, which we will consider to be 1) that the digital signature d = sign sk m, where sk is the secret key corresponding to pk.

Our formal model begins by precisely capturing the properties of the SimpleCrypto interface using F*'s dependent types.

load in editortype prin = string type pubkey : prin => S type privkey : prin => S type dsig val keygen: p:prin -> (pubkey p * privkey p) type Says : prin => bytes => E val sign: p:prin -> privkey p -> msg:bytes{Says p msg} -> dsig val verify: p:prin -> pubkey p -> msg:bytes -> dsig -> b:bool{b=true ==> Says p msg}

The key idea is to index the type of keys with the name of
a *principal* who owns the key---a value of
type (pubkey p *
privkey p) is a pair of a public and private key for the
principal p. When
building a new key
pair, keygen
requires the caller to provide the name of the
principal p:prin
for whom the keys are being generated.

Next, to connect the behavior of sign to verify, we define a predicate Says, relating a principal to a message. When signing a message msg using a key of type privkey p, we require the predicate Says p msg to be valid. Conversely, when a signature check verify p pk msg d succeeds, the type of verify states that the the predicate Says p msg is valid.

We can now program client and server programs using our crypto
library to authenticate their communications. The property we want to
prove is a *correspondence assertion* on the traces of
program. Specifically, we want to show that whenever the client and
server programs are executed in parallel, then in every execution of
the system, if at time *t* in the trace the
server asserts
that a message was sent by the client at some time, then, at some
prior time in the trace, the client must have issued a *protocol
event* recording that it did in fact send the message. (Similarly,
with the roles of client and server reversed.) To mark protocol
events, we overload the use of
F*'s assume
construct, as we will see below. First, though, we need a simple
interface for marshalling, sending and receiving messages, and for forking threads.

val string2bytes: string -> bytes val send: prin -> (bytes * dsig) -> unit val recv: prin -> (bytes * dsig) val fork: list (unit -> unit) -> unit

Now, here's a client program. As arguments, it has its own principal identifier me and key pair; the name of the server and its public key; and it returns unit.

load in editorval client: me:prin -> pubkey me -> privkey me -> server:prin -> pubkey server -> unit let client me mypk mysk server serverpk = let req = string2bytes "Hi server" in assume (Says me req); (* Protocol event *) let ds = sign me mysk req in send server (req, ds); let (resp, ds') = recv server in if verify server serverpk resp ds' then assert (Says server resp); () else ()

The program begins by marking a protocol event Says me req which indicates the client's intent to send the message req. It then builds a digital signature, where the pre-condition of sign is established by the protocol event. The message is sent to the server and then the client blocks waiting for a response.

When a response arrives, the client checks the signature using the server's public key and then asserts that the message was indeed from the server principal. This assertion marks the end of a correspondence assertion---for the program to be secure, we require that there be a corresponding protocol event in a server program establishing that it did indeed send the response, and, by typing, we get just such a property.

Write the server program corresponding to client.

What have we just verified? Formally, the metatheory of F* gives us a robust safety property for programs like our example. Consider the composition of the SimpleCrypto, Util, Client and Server modules, with any adversary program A that is itself a program that is well-typed against the interface exposed by these modules, then, so long as the program A does not itself contain any assume commands, then every correspondence assertion in client and server succeeds.

Specifically, we can write a main program that executes a run of this protocol, and allow the adversary program to call this function, to intercept the network, to call into the crypto library, etc. but in every run of the protocol, each assert is preceded by an assumption of the corresponding protocol event.

load in editorlet main attacker = let cpk, csk = keygen "client" in let spk, ssk = keygen "server" in fork [attacker; (fun () -> client "client" cpk csk "server" spk); (fun () -> server "server" spk ssk "client" cpk)]

Implement the crypto library using an ideal functionality for signatures. For example, you could implement signatures using some local state within the Crypto module to record all prior signature constructions in the state when signing and implementing verify by consulting the local state.

We now turn to a slightly larger example: proving the soundness of the simply typed lambda calculus (STLC) in F*.

We start by defining below the syntax of STLC with a collection of algebraic datatypes. We have just one base type TUnit, and a function type constructor. Values include a unit constant, variables (represented as concrete string names), and typed lambda abstractions. Expressions additionally include function applications.

load in editorlogic data type typ = | TUnit : typ | TArrow : typ -> typ -> typ logic data type value = | Unit : value | Var : string -> value | Lam : string -> typ -> exp -> value and exp = | Value : value -> exp | App : exp -> exp -> exp

These datatype declarations should be familiar from ML, except you may wonder about the logic data qualifier that precedes them. To appreciate this, recall that the Z3 theorem prover provides a theory of datatypes. The logic data qualifier instructs F* to map these datatypes to Z3 datatypes when encoding the refinement logic. We call such datatypes "logical".

Logical datatypes come with some additional conveniences. For
example, for each constructor in a datatype, the logic
provides *discriminator* and *projector* functions. For
example, given a
value t:typ,
the discriminator
predicates TUnit_is:typ => E
and TArrow_is:typ => E
decide whether x=TUnit
or x=TArrow _ _, respectively.
For each argument of a constructor, a projector function allows
extracting that argument. For
example, TLam_proj_0:value
-> string,
TLam_proj_1:value -> typ, TLam_proj_2:value -> exp,
are the projectors for the Lam constructor, returning each of its three arguments, respectively.

Next, to define the static semantics of STLC, we define a type env of typing environments. The env type is just an alias for a type Map.map provided by the Map module in F*'s standard prelude. The map type is a model of a polymorphic, heterogenous map, mapping keys of any type to values of any type. For example, we may have a single map value mapping the integer 0 to the string "zero", and the boolean false to the integer 0.

For STLC, our maps for typing environments are rather more specialized: we only need to map strings to typs. So, we define a few abbreviations to make the syntax of maps a bit lighter.

load in editortype env = Map.map logic val Emp : env logic val Sel : env -> string -> typ logic val Concat : env -> env -> env logic val Singleton : string -> typ -> env type In = Map.In string logic val Upd : env -> string -> typ -> env type Equal = Map.Equal define Emp_def:Emp = Map.Emp define Sel_def:forall g x. Sel g x = Map.Sel string typ g x define Concat_def:forall g1 g2. Concat g1 g2 = Map.Concat g1 g2 define Singleton_def:forall x t. Singleton x t = Map.Singleton string typ x t define Upd_def:forall g x t. Upd g x t=Map.Upd string typ g x t

For the full axiomatization our theory of the map type, click here. Its key concepts are defined next.

**Constructing environments:**
Emp
is the empty environment,
and Singleton x
t is a singleton map. Maps can be concatenated
with Concat.
As is customary with typing
environments, env
maps "grow on the right". That is, the typing
environment x1:t1,
x2:t2 is
represented Concat
(Singleton x1 t1) (Singleton x2 t2). It is sometimes
convenient to
write Upd g x
t
for Concat g
(Singleton x t).

**Domain of an environment:**Technically, in the refinement
logic all maps are total. However, typing environments are partial
maps. To keep track of the domain of interest of the map, we have a
predicate In,
where
In g x
is valid if and only
if g=Concat g1
(Concat g2 ... gn) and one of
the gi
is Singleton x
t, for some t.

**Looking up bindings:**The
function Sel g
x=t
if g=Concat g1
... gi ... gn,
where gi=Singleton x
t,
and x
is not in the domain
of g_{i+1}
... gn. If no
such gi
exists, then Sel g
x is determined by arbitrary.

**Extensional equality of env:**The
predicate Equal g1
g2 is valid
if Sel g1 x = Sel g2
x, for all
keys x.
Maps are also extensionally equal, in the sense
that Equal g1
g2
imlies g1=g2.

Next, we axiomatize the typing judgment of the STLC by introducing a classical relation Typing g e t to state that the expression e has type t in environment g.

To define the relation, we begin by writing down the four axioms below. These should be familiar.

load in editortype Typing : env => exp => typ => E assume Typing_unit: forall g. Typing g (Value Unit) TUnit assume Typing_var: forall g x. In g x ==> Typing g (Value (Var x)) (Sel g x) assume Typing_lam: forall g x t t' e. Typing (Upd g x t) e t' ==> Typing g (Value (Lam x t e)) (TArrow t t') assume Typing_app: forall g e1 e2 t1 t2. Typing g e1 (TArrow t1 t2) /\ Typing g e2 t1 ==> Typing g (App e1 e2) t2 type WellTyped = fun g e => exists t. Typing g e t

Note, since we are working with a classical logic, these four axioms on their own are not sufficient to fully define Typing. Unlike in constructive logic, these axioms do not ensure that the only way for Typing g e t to be valid is for a derivation to be built using only the four rules above. To ensure that, we need to axiomatize the necessary inversions, as shown below.

load in editorassume Typing_value_inv: forall g v t.{:pattern (Typing g (Value v) t)} Typing g (Value v) t ==> (Unit_is v ==> TUnit_is t) /\ (TUnit_is t ==> Var_is v \/ Unit_is v) /\ (Var_is v ==> In g (Var_proj_0 v) /\ t=Sel g (Var_proj_0 v)) /\ (Lam_is v ==> TArrow_is t /\ TArrow_proj_0 t = Lam_proj_1 v /\ Typing (Upd g (Lam_proj_0 v) (Lam_proj_1 v)) (Lam_proj_2 v) (TArrow_proj_1 t)) /\ (TArrow_is t ==> Lam_is v \/ Var_is v) assume Typing_app_inv: forall g e1 e2 t2. Typing g (App e1 e2) t2 ==> (exists t t'. Typing g e1 t /\ Typing g e2 t') /\ (forall t1. Typing g e2 t1 ==> (forall t'. Typing g e1 t' ==> t'=TArrow t1 t2))

If you're familiar with formalizing programming languages in a system like Coq, axiomatizing these inversions may appear strange. In a constructive setting, one usually proves them as theorems from the definition of the typing judgment. This is possible to relatively easily in F* also, but that will have to wait until the next subsection of this tutorial. For now, we just assume the inversions. On the plus side, as we will see, working with SMT-backed refinement types in F* makes our soundness proof for STLC pretty easy.

With these definitions in hand, we can now program a simply typechecker for STLC and prove it correct. The specification of compute_type g e below ensures that if e is well-typed in g, then compute_type g e returns a t:typ such that Typing g e t is valid.

A disclaimer: we do not prove termination of the recursive functions below. This can be done in F*'s P-fragment---but that's for a later date.

load in editorval compute_type: g:env -> e:exp -> o:option (t:typ{Typing g e t}){WellTyped g e ==> Some_is o} let rec compute_type g e = match e with | Value (Var x) -> if Map.contains g x then Some (Sel g x <: t:typ{Typing g e t}) else None | Value Unit -> Some (TUnit <: t:typ{Typing g e t}) | Value (Lam x t body) -> (match compute_type (Upd g x t) body with | None -> None | Some t' -> Some (TArrow t t' <: t:typ{Typing g e t})) | App e1 e2 -> match compute_type g e2 with | None -> None | Some targ -> match compute_type g e1 with | None -> None | Some t -> match t with | TUnit -> None | TArrow targ' tres -> if targ=targ' then Some (tres <: t:typ{Typing g e t}) else None

Our goal is to prove a standard syntactic progress and preservation theorem for STLC. Our strategy for doing this is, roughly, to program a big-step evaluator for STLC and give it the type shown below. The type states that the evaluation of a well-typed STLC term may diverge, but if it converges, it produces a value of the same type as the original term, i.e., the type ensures progress and preservation.

val eval: e:exp -> t:typ{Typing Emp e t} -> v:value{Typing Emp (Value v) t}

We show the implementation of eval next.

let rec eval e t = match e with | Value v -> v | App e1 e2 -> match compute_type Emp e1 with | None -> unreachable () | Some TUnit -> unreachable () | Some (TArrow t1 t2) -> match eval e1 (TArrow t1 t2) with | Unit -> unreachable () | Var x -> unreachable () | Lam x t body -> let arg = eval e2 t1 in eval (subst Emp Emp t1 t2 x arg body) t2

In the case where e is already a value, we just return it. Otherwise, it is an application App e1 e2, and we need to recursively evaluate e1 and e2 and then apply a β-reduction.

To make these recursive calls in the App case, we need to pass the type of e1 as an argument. For this, we call compute_type, whose specification ensures that it must return an arrow type---so the other two cases are unreachable.

Note: computing the type of e1 can be considered a "ghost" operation---it does not influence the semantics of evaluation in anyway, aside from providing us with the metadata (in this case the type) we need in order to prove the property we are after. Unfortunately, F*'s does not currently provide a way to distinguish ghost expressions from other computationally relevant ones. Marking certain expressions as ghost and erasing them would be an interesting extension of the type system.

Now, having computed the type of e1, we can make our recursive call and prove that the result must be a λ-term. Next, following a call-by-value reduction strategy, we evaluate the argument and substitute it in (using subst, programed and verified below), and continue evaluating.

To complete our type soundness proof, we have to prove that substitution preserves types. Its specification and implementation is shown below. The main interesting case is substituting underneath a lambda-term while avoiding variable capture.

In the case where the bound variable of the λ-term matches the variable x that we are substituting, then we simply return the term unchanged. However, to prove this case is well-typed, we need to provide the SMT solver with a hint in the form of a lemma. The hint in this case is to make use of extensional equality of environments, and we provide the hint using an assertion. Providing assertions as hints is a common programming idiom in F*.

If the bound variable of the λ-term does not match, then we have to carefully rename the variable to avoid variable capture, then apply a weakening lemma to the value being substituted in, and then substitute recursively in the renamed body.

val subst: g:env -> g':env -> tx:typ -> te:typ -> x:string{not(In g' x)} -> v:value{Typing (Concat g g') (Value v) tx} -> e:exp{Typing (Concat (Upd g x tx) g') e te} -> e':exp{Typing (Concat g g') e' te} let rec subst g g' tx te x v e = match e with | Value (Var y) -> if x=y then Value v else Value (Var y) | Value Unit -> Value Unit | Value (Lam y targ body) -> if x=y then assert (Equal (Upd (Concat (Upd g x tx) g') y targ) (Upd (Concat g g') y targ)); e else let z = Map.fresh (Concat (Concat (Upd g x tx) g') (bvars e)) in weakening (Concat g g') Emp (Value v) tx z targ; (* Typing (Upd (Concat g g') z targ) (Value v) tx *) let body = rename (Concat (Upd g x tx) g') Emp y z targ body (TArrow_proj_1 te) in (* Typing (Upd (Concat (Upd g x tx) g') z targ) body (TArrow_proj_1 te) *) let body' = subst g (Upd g' z targ) tx (TArrow_proj_1 te) x v body in (* Typing (Upd (Concat g g') z targ) body te *) Value (Lam z targ body') | App e1 e2 -> match compute_type (Concat (Upd g x tx) g') e1 with | None -> unreachable () | Some TUnit -> unreachable () | Some (TArrow t1 t2) -> let e1' = subst g g' tx (TArrow t1 t2) x v e1 in let e2' = subst g g' tx t1 x v e2 in App e1' e2'

The weakening lemma is programmed and verified below---it is fairly standard. Note how the inductive invariant requires that we weaken a derivation by adding a hypothesis in the "middle" of an environment.

val weakening:g1:env -> g2:env -> e:exp -> t:typ{Typing (Concat g1 g2) e t} -> y:string{not(In g1 y)} -> ty:typ -> u:unit{Typing (Concat (Upd g1 y ty) g2) e t} let rec weakening g1 g2 e t y ty = match e with | Value Unit -> () | Value (Var x) -> () | Value (Lam z tz body) -> weakening g1 (Upd g2 z tz) body (TArrow_proj_1 t) y ty | App e1 e2 -> match compute_type (Concat g1 g2) e1 with | None -> unreachable () | Some TUnit -> unreachable () | Some (TArrow t1 t2) -> weakening g1 g2 e1 (TArrow t1 t2) y ty; weakening g1 g2 e2 t1 y ty

Finally, we come to our renaming lemma, which ensures that a variable y in a term may be renamed to z if z does not clash with either the bound- or free-variables in the term.x

logic val bvars: exp -> env assume Bvar_Unit: bvars (Value Unit) = Emp assume Bvar_Var: forall x.{:pattern (bvars (Value (Var x)))} bvars (Value (Var x)) = Emp assume Bvar_Lam: forall x t e.{:pattern (bvars (Value (Lam x t e)))} bvars (Value (Lam x t e)) = Concat (Singleton x t) (bvars e) assume Bvar_App: forall e1 e2.{:pattern (bvars (App e1 e2))} bvars (App e1 e2) = Concat (bvars e1) (bvars e2) val rename: g:env -> g':env -> y:string{not(In g' y)} -> z:string{not(In g z \/ In g' z)} -> tyz:typ -> e:exp{not(In (bvars e) z)} -> te:typ{Typing (Concat (Upd g y tyz) g') e te} -> e':exp{Typing (Concat (Upd g z tyz) g') e' te} let rec rename g g' y z tyz e te = match e with | Value Unit -> e | Value (Var w) -> if w=y then Value (Var z) else e | Value (Lam w tw body) -> if w=y then assert (Equal (Upd (Concat (Upd g y tyz) g') w tw) (Upd (Concat g g') w tw)); weakening g (Upd g' w tw) body (TArrow_proj_1 te) z tyz; e else let body' = rename g (Upd g' w tw) y z tyz body (TArrow_proj_1 te) in Value (Lam w tw body') | App e1 e2 -> match compute_type (Concat (Upd g y tyz) g') e1 with | None -> unreachable () | Some t -> let e1' = rename g g' y z tyz e1 t in let e2' = rename g g' y z tyz e2 (TArrow_proj_0 t) in App e1' e2'

The full development is reproduced in a single listing below.

load in editorval weakening:g1:env -> g2:env -> e:exp -> t:typ{Typing (Concat g1 g2) e t} -> y:string{not(In g1 y)} -> ty:typ -> u:unit{Typing (Concat (Upd g1 y ty) g2) e t} let rec weakening g1 g2 e t y ty = match e with | Value Unit -> () | Value (Var x) -> () | Value (Lam z tz body) -> weakening g1 (Upd g2 z tz) body (TArrow_proj_1 t) y ty | App e1 e2 -> match compute_type (Concat g1 g2) e1 with | None -> unreachable () | Some TUnit -> unreachable () | Some (TArrow t1 t2) -> weakening g1 g2 e1 (TArrow t1 t2) y ty; weakening g1 g2 e2 t1 y ty logic val bvars: exp -> env assume Bvar_Unit: bvars (Value Unit) = Emp assume Bvar_Var: forall x.{:pattern (bvars (Value (Var x)))} bvars (Value (Var x)) = Emp assume Bvar_Lam: forall x t e.{:pattern (bvars (Value (Lam x t e)))} bvars (Value (Lam x t e)) = Concat (Singleton x t) (bvars e) assume Bvar_App: forall e1 e2.{:pattern (bvars (App e1 e2))} bvars (App e1 e2) = Concat (bvars e1) (bvars e2) val rename: g:env -> g':env -> y:string{not(In g' y)} -> z:string{not(In g z \/ In g' z)} -> tyz:typ -> e:exp{not(In (bvars e) z)} -> te:typ{Typing (Concat (Upd g y tyz) g') e te} -> e':exp{Typing (Concat (Upd g z tyz) g') e' te} let rec rename g g' y z tyz e te = match e with | Value Unit -> e | Value (Var w) -> if w=y then Value (Var z) else e | Value (Lam w tw body) -> if w=y then assert (Equal (Upd (Concat (Upd g y tyz) g') w tw) (Upd (Concat g g') w tw)); weakening g (Upd g' w tw) body (TArrow_proj_1 te) z tyz; e else let body' = rename g (Upd g' w tw) y z tyz body (TArrow_proj_1 te) in Value (Lam w tw body') | App e1 e2 -> match compute_type (Concat (Upd g y tyz) g') e1 with | None -> unreachable () | Some t -> let e1' = rename g g' y z tyz e1 t in let e2' = rename g g' y z tyz e2 (TArrow_proj_0 t) in App e1' e2' val subst: g:env -> g':env -> tx:typ -> te:typ -> x:string{not(In g' x)} -> v:value{Typing (Concat g g') (Value v) tx} -> e:exp{Typing (Concat (Upd g x tx) g') e te} -> e':exp{Typing (Concat g g') e' te} let rec subst g g' tx te x v e = match e with | Value (Var y) -> if x=y then Value v else Value (Var y) | Value Unit -> Value Unit | Value (Lam y targ body) -> if x=y then assert (Equal (Upd (Concat (Upd g x tx) g') y targ) (Upd (Concat g g') y targ)); e else let z = Map.fresh (Concat (Concat (Upd g x tx) g') (bvars e)) in weakening (Concat g g') Emp (Value v) tx z targ; (* Typing (Upd (Concat g g') z targ) (Value v) tx *) let body = rename (Concat (Upd g x tx) g') Emp y z targ body (TArrow_proj_1 te) in (* Typing (Upd (Concat (Upd g x tx) g') z targ) body (TArrow_proj_1 te) *) let body' = subst g (Upd g' z targ) tx (TArrow_proj_1 te) x v body in (* Typing (Upd (Concat g g') z targ) body te *) Value (Lam z targ body') | App e1 e2 -> match compute_type (Concat (Upd g x tx) g') e1 with | None -> unreachable () | Some TUnit -> unreachable () | Some (TArrow t1 t2) -> let e1' = subst g g' tx (TArrow t1 t2) x v e1 in let e2' = subst g g' tx t1 x v e2 in App e1' e2' val eval: e:exp -> t:typ{Typing Emp e t} -> v:value{Typing Emp (Value v) t} let rec eval e t = match e with | Value v -> v | App e1 e2 -> match compute_type Emp e1 with | None -> unreachable () | Some TUnit -> unreachable () | Some (TArrow t1 t2) -> match eval e1 (TArrow t1 t2) with | Unit -> unreachable () | Var x -> unreachable () | Lam x t body -> let arg = eval e2 t1 in eval (subst Emp Emp t1 t2 x arg body) t2