Nikhil Swamy

Juan Chen

Cédric Fournet

Pierre-Yves Strub

Karthikeyan Bhargavan

Jean Yang

Secure Distributed Programming with Value-Dependent Types

Keywords: D.3.1 [Formal Definitions and Theory]: Syntax and Semantics General Terms Security, Verification, Languages, Theory Security type systems, refinement types

Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging.

We present F ⋆ , a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F ⋆ provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F ⋆ and controls their interaction. F ⋆ subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F ⋆ .

We have implemented a compiler that translates F ⋆ to .NET bytecode, based on a prototype for Fine. F ⋆ provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification.

To date, we have programmed and verified more than 20,000 lines of F ⋆ including (1) new schemes for multi-party sessions;

(2) a zero-knowledge privacy-preserving payment protocol; (3) a provenance-aware curated database; (4) a suite of 17 web-browser extensions verified for authorization properties; and (5) a cloudhosted multi-tier web application with a verified reference monitor.

Introduction

Distributed applications are difficult to program reliably and securely. To address this problem, researchers have designed new languages with security verification in mind. Early work in this space developed ad hoc type systems targeting verification of specific security idioms, including systems for information flow controls, starting with [START_REF] Volpano | A sound type system for secure flow analysis[END_REF]; for proving authentication properties in cryptographic protocols [START_REF] Gordon | Authenticity by typing for security protocols[END_REF]; and, more recently, for protocols that use zero-knowledge proofs [START_REF] Backes | Type-checking zero-knowledge[END_REF]). More general type systems for security verification have also been proposed, e.g., Fable [START_REF] Swamy | Fable: A language for enforcing user-defined security policies[END_REF]), F7 [START_REF] Bengtson | Refinement types for secure implementations[END_REF][START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF], Aura [START_REF] Jia | Encoding information flow in aura[END_REF][START_REF] Jia | Aura: A programming language for authorization and audit[END_REF][START_REF] Vaughan | Evidence-based audit[END_REF], Fine [START_REF] Chen | Type-preserving compilation of end-toend verification of security enforcement[END_REF][START_REF] Swamy | Enforcing stateful authorization and information flow policies in Fine[END_REF], and PCML5 [START_REF] Avijit | Distributed programming with distributed authorization[END_REF]. All these languages use various forms of dependent types to rea-son about security, following a long tradition of dependent typing for general-purpose theorem proving and program verification, e.g., Coq [START_REF] Bertot | Coq'Art: Interactive Theorem Proving and Program Development[END_REF] and Agda [START_REF] Norell | Towards a practical programming language based on dependent type theory[END_REF].

Although these languages are successful in many aspects, for large-scale distributed programming, we desire languages that (1) feature general programming constructs like effects and recursion, which, while invaluable for building real systems, make it hard to formally reason about programs, specifications, and proofs;

(2) support various styles of proofs and evidence, ranging from cryptographic signatures to logical proof terms; (3) produce proofs that can be efficiently communicated between agents in the system.

This paper presents F ⋆ , a full-fledged design and implementation of a new dependently-typed programming language that addresses all these challenges. F ⋆ subsumes both F7 and Fine. Unlike prior languages, F ⋆ provides arbitrary recursion while maintaining a logically consistent core, resolving the tension between programmability and consistency by restricting the use of recursion in specifications and proofs; it enables modular reasoning about state and other effects and allows specifying refinement properties on affine values; it supports proofs of refinement properties using a mixture of cryptography and logical proof terms; and it allows selective erasure and reconstruction of proofs to reduce the overhead of communicating proofs.

By compiling to verifiable .NET bytecode, F ⋆ provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and other .NET languages. We have formalized the metatheory of F ⋆ , and mechanized a significant part of the metatheory in Coq. We have developed a prototype compiler for F ⋆ (35,000 lines of F#), and used F ⋆ to program and verify more than 20,000 lines of code. We believe F ⋆ is the first language of its kind with such a scale of implementation and evaluation.

Next, we give an overview of F ⋆ and our main contributions. A novel kind system. A central feature of F ⋆ is its kind system, which tracks several sub-languages-for terms, proofs, affine resources, and specifications. This kind system controls the interaction between those, while still providing a single unified language to specify, program, verify, and deploy secure distributed systems.

We use kinds ⋆ for program terms and P for proofs. Program terms that may be effectful and divergent reside in the universe of ⋆ types. Within ⋆, P identifies a universe of pure, total functions; P terms are used (mainly) in the construction of proof terms. Additionally, we use A, the kind of affine (used-at-most-once), stateful resources, to model and reason about effects in a modular style. Finally, the kind E is for types that may have no inhabitants at all. We use E to control the selective erasure of proof terms, when these proofs are either impossible to construct in a distributed setting (e.g., due to cryptography or due to the design of legacy libraries); when the presence of a proof term would curtail expressiveness (e.g., when speaking of properties of affine values); or when proof terms would be too voluminous to construct. As such, E identifies a sub-language that plays a purely specificational role. To improve code reuse, we provide a sub-kinding relation, P <: ⋆ <: E, with A unrelated to the others.

Two flavors of refinements. Refinement types are commonly used to specify program properties. In contrast with prior languages, F ⋆ features both concrete and ghost refinements; §2 illustrates the need for both for secure distributed programming. To reason about the security of distributed applications, with minimal trust between components, explicit proofs of security sometimes need to be communicated and checked at runtime.

Concrete refinements are pairs representing a value and a proof term serving as a logical evidence of the refinement property, similar to those in Coq and Fine. One novelty of F ⋆ is that it assigns a special kind P for proof terms, and restricts types and proof terms in the P universe to guarantee logical consistency.

Ghost refinements are used to state specifications for which proof terms are not maintained at run time. Ghost refinements have the form x:t{φ } where x is a value variable, t is a type, and φ is a logical formula, itself represented as a type that must have kind E and may depend on x and other in-scope variables. Ghost refinements are similar to those of F7; they are smoothly integrated in F ⋆ using the E kind. Ghost refinements provide the following benefits: (1) they enable precise symbolic models for many cryptographic patterns and primitives, and evidence for ghost refinement properties can be constructed and communicated using cryptographic constructions, such as digital signatures; (2) they benefit from a powerful subtyping relation: x:t{φ } is a subtype of t; this structural subtyping is convenient to write and verify higher-order programs; (3) they provide precise specification to legacy code without requiring any modifications; and (4) when used in conjunction with concrete refinements, they support selective erasure and dynamic reconstruction of evidence, enabling a variety of new applications and greatly reducing the performance penalty for runtime proofs. Refinements on affine state. Prior work has shown the usefulness of affine types in reasoning about programs that use mutable state [START_REF] Borgstrom | Verifying stateful programs with substructural state and hoare types[END_REF][START_REF] Lahiri | Linear maps[END_REF]. Relying on its kind system, F ⋆ freely allows the use of affine values within its specifications fragment, while still guaranteeing that affine values are used at most once elsewhere in the code. In §4, we exploit this feature extensively in implementing a new, flexible approach [START_REF] Deniélou | Dynamic multirole session types[END_REF] to enforce protocols on multi-party session types. Prior systems that integrate substructural and dependent types (e.g., Fine and Linear LF by [START_REF] Cervesato | A linear logical framework[END_REF] disallow refinements to speak directly about affine values, and have to rely instead on various encodings to work around this limitation, which is unsuitable for source programming. Automation and logic parametricity. Proof automation is critical for developing large-scale programs. F ⋆ is carefully designed to be parametric in the logic used to describe programming properties and their proofs. §2.5 shows examples with a simple modal authorization logic and an ad hoc logic for database provenance. Logic parametricity enables working with custom authorization logics and, importantly, makes it easy to integrate F ⋆ with SMT solvers for logics extended with specific theories. Thus, program verification in F ⋆ benefits from significant automation-our implementation uses the Z3 SMT solver (de Moura and Bjørner 2008) and scales up to large programs and specifications. Languages like Aura, PCML5, Coq, and Agda commit to a specific logic, limiting their flexibility. This limitation is significant since diverse logics are used and even designed when reasoning about security policies and properties-see [START_REF] Chapin | Authorization in trust management: Features and foundations[END_REF] for a recent survey. Metatheory. We establish several properties of F ⋆ . First, we prove the soundness of F ⋆ in terms of progress and preservation. From this, we derive a safety property for ghost refinements called global deducibility. Next, we show that the P-fragment of F ⋆ is consistent by giving a typed embedding of this fragment into CiC and proving that the translation is a simulation. We also give a typed embedding of a core subset of RCF (the core calculus of F7) into F ⋆ . The subject reduction result (modulo the admission of a few standard lemma) has been mechanized in Coq-we plan to continue to develop our Coq formalization to include the other results.

Since our P-fragment is strongly normalizing, one might imagine extending F ⋆ to permit arbitrary P-terms to index types. However, term reduction in types, particularly with dynamic assumptions and affinity, poses a significant challenge for the metatheory. We remain with value dependency in F ⋆ , while acknowledging that it is less expressive than having expressions in types. However, value dependency is a practical design choice that has not hindered the construction and verification of the programs we have built. Compiler implementation. We have implemented a compiler for F ⋆ based on our prior work on a compiler for Fine. The F ⋆ compiler accepts both Fine and F7 programs as input. To validate this feature, we typecheck and compile a large F7 library implementing symbolic cryptography [START_REF] Bhargavan | Modular verification of security protocol code by typing[END_REF].

Our compiler translates F ⋆ to RDCIL, a dependently typed dialect of .NET bytecode. This translation is considerably more efficient than the one we used for Fine. Due to the use of ghost refinements and the availability of polymorphic kinds, bytecode emitted by the F ⋆ compiler is an order of magnitude (in some cases 45x) smaller than the bytecode emitted by the Fine compiler. Experimental evaluation on a large suite of examples. We have implemented several libraries and applications in F ⋆ , verifying a large corpus of code for various properties. Prominent among our examples are (1) secure implementations of multi-party sessions protocols; (2) a prototype of a new zero-knowledge privacy scheme; (3) a provenance-aware curated database; (4) a suite of 17 web-browser extensions verified for authorization properties; and (5) an Azure-hosted multi-tier web application with a reference monitor verified for stateful authorization properties.

Due to space constraints, we leave the complete semantics of F ⋆ , manual proofs of the metatheory, and additional examples to a technical report, which, along with the compiler source code, the Coq development, and all our example programs, can be found at http://research.microsoft.com/fstar.

F ⋆ by example

This section introduces F ⋆ informally. The syntax of F ⋆ is based loosely on OCaml, F# and related languages in the ML familynotations specific to F ⋆ are primarily in support of its more expressive type and kind language. The dynamic semantics is also in the spirit of ML, in call by value, but the static semantics is significantly more complex. The examples in this section, together with those in §4, are intended to motivate and exercise its main features.

We organize our presentation around the new kind system of F ⋆ . We start with simple programs that use P-kind and F ⋆ 's sublanguage of total functions to construct proof terms for concrete refinements. Next, we discuss E-kind and its use in two different scenarios with ghost refinements-first, when giving specifications to legacy libraries where the construction of explicit proof terms is impractical; and, second, when verifying implementations of cryptographic protocols, where the construction of proof terms is simply impossible. We then turn to A-kind, which, in conjunction with E-kind, can specify and verify properties of stateful computations. We conclude the section with an example that exploits the interaction between P-kind and E-kind, via the sub-kinding relation P <: ⋆ <: E, to construct a model of a high-integrity database with precise data-provenance properties.

Concrete refinement types and total proof terms

Consider a partial specification for a very simple program, tail, that returns the tail of a list:

val tail: ∀α ::⋆ . l1:list α → {l2:list α | ∀x. Mem x l2 =⇒ Mem x l1}
This type is polymorphic, of the form ∀α ::k. t where k is the kind of the abstracted type variable-kinds are ascribed to types using double colons. Here, α has kind ⋆ , the kind given to types that admit arbitrary recursion and effects, i.e., the standard kind of fullyapplied types in an ML-like system. Following ML, by default we omit explicit quantifiers for prenex-quantified type variables, and omit type applications when they can be determined by the context.

The rest of the type of tail shows a dependent function, of the form x:t → t' where the formal parameter x of type t is named, and is in scope in t'. When the function is not dependent, we simply write t → t'. The range type of tail shows our syntax for concrete refinements, {x:t | φ }, where φ is itself a type representing a logical formula, in which the name x is bound. Here, the formula states that the tail l2 contains at most the elements of l1. Concrete refinements and constructive proofs. Also called subset types or Σ-types [START_REF] Sozeau | Subset coercions in coq[END_REF], concrete refinements in F ⋆ are desugared into dependent pairs (as is usual in, say, Coq). The type below shows this desugaring, where the type x:t * t' denotes a dependent pair, where x names the t-typed first component and is bound in t', the type of the second component.

val tail: l1:list α → (l2:list α * (x:α → Mem x l2 → Mem x l1))
When desugaring formulas, quantifiers are desugared to dependent functions, and implications to non-dependent functions. The predicate Mem x l2 is itself a type, which we show below. As such, concrete refinements are represented as pairs of the underlying value, and a proof term witnessing the validity of the refinement formula. A total sub-language for proof terms. We must be careful when representing quantifiers and implication with function arrows. For logical consistency, we require the function arrows that represent the type of proof terms to be total, whereas arrows used in the rest of the program (where we certainly want to use arbitrary recursion) can be partial. Thus, we need to ensure that potential divergence in the program never leaks into fragments of a program used for building proof terms. We achieve this by introducing a kind P , a subkind of ⋆ , where types residing in P are guaranteed to be total.

Using P -kind, we define Mem, an inductive type that axiomatizes list membership in constructive style. Its kind is of the form α ::k ⇒ k', where α binds a k-kinded formal type parameter in the kind k' of the constructed type. Type constructors can also be applied to values; such constructors have kinds of the form x:t ⇒ k where x names the formal argument, a value of type t, and is in scope in k. Below, the kind of Mem says that it is a dependent type constructor that constructs a type of kind P from a type α , a value x of type α , and a value l of type list α . (When x:α , we write Mem x l instead of Mem α x l.) type Mem ::

α ::⋆ ⇒ α ⇒ list α ⇒ P = | Mem hd : x:α → tl:list α → Mem x (Cons x tl) | Mem tl : x:α → y:α → tl:list α → Mem y tl → Mem y (Cons x tl)
Inductive types defined in P -kind are required to be strictly positive, and we place other restrictions ( §3.2) on the elimination rules for P -kinded types to ensure totality. A function type x:t → t' inherits the kind of its range type-it has P kind and is a total function when t'::P . Theorem 2 (Logical consistency of P) provides a well-typed embedding of terms residing in the P -fragment into CiC, ensuring that terms in the P -fragment are valid proof terms. Non-constructive proofs, automation, and logic parametricity. Programming explicitly with proof terms for non-trivial program properties quickly becomes impractical. The F ⋆ implementation provides automation by calling Z3, an SMT solver, to try to decide refinement properties, and then constructing proof terms from the deduction traces reported by Z3. However, since Z3 (and many other automated provers) use classical logics, the proof terms produced in this manner are not constructive.

To support non-constructive proof terms (and more generally, to permit custom logics), F ⋆ allows to define custom proof kernels. A specific proof kernel (the type pf below), is defined in the standard library of F ⋆ and axiomatizes a classical logic, extended with axioms for commonly used data types such as list.

type pf ::

P ⇒ P = | Exc middle: pf (Or α (Not α )) | Not elim: pf (Not α ) → pf α → pf β | Not in nil: x:α → pf (Not (Mem x Nil)) | ... ( * many constructors omitted * ) | Unit pf: α → pf α | Bind pf: pf α → (α → pf β ) → pf β
Each constructor in this kernel is an axiom in the logic, such as the excluded middle; introduction and elimination forms for the standard logical connectives (where Or, Not etc. are also type constructors); and axioms like Not in nil, which are necessary for reasoning in a non-constructive setting, where exhaustiveness arguments for inductive types are inapplicable. The pf kernel also includes constructors Unit pf and Bind pf that allow proofs to be composed monadically. This is particularly useful since F ⋆ is a call-by-value language-Bind pf lets us compose proofs simply by constructor application, without triggering evaluation. Using this approach, F ⋆ translates the type of tail to the type below. Relying on automated proof extraction from Z3, programmers write the code shown below, and the F ⋆ compiler inlines the proof term and compiles (while carrying proofs) to RDCIL ( §5), our dependently typed .NET bytecode. Concrete refinements in this form are based on a similar construct in Fine. Through the use of P -kind (which Fine lacks), F ⋆ proof terms are logically consistent evidence of refinement properties.

Ghost refinements for lightweight specifications

Concrete refinements have a long tradition and a well-understood theory. However, as discussed below, we find them inappropriate for use in some scenarios. As an alternative, F ⋆ also provides ghost refinements, based on a construct of F7, and integrates them with the other features of the system, notably higher kinding, quantification over predicates, and refinements for substructural state.

We illustrate the use of ghost refinements for the problem of verifying clients of libraries, where the libraries are authored separately and are unmodifiable. In recent work, [START_REF] Guha | Verified security for browser extensions[END_REF] consider programming secure web browser extensions using F ⋆ . For this scenario, we use ghost refinement types to specify pre-and post-conditions on the interface provided by the browser, and use the specifications to verify access control properties of extensions. The listing below illustrates this approach on a tiny program- §5 reports new results for compiling a suite of 17 such extensions in a type-preserving style to .NET bytecode.

We aim to enforce a policy that untrusted extensions (line 10) only read data from the header of a web page and not the body. This policy is specified using an assumption at line 8, which states, informally, that extensions hold the CanRead e privilege on DOM nodes e, for which the property The type of innerText has the form x:t{φ } → t', where the formula φ is a ghost refinement applied to the formal parameter x:t, and x is in scope in both φ and t'. The refinement CanRead e is a pre-condition indicating that clients must hold the CanRead e privilege before calling the function. Analogously, the post-condition of tagName relates the returned string t to the argument e, and clients may derive facts using this property and any other assumption (e.g., the policy assumption at line 8). For example, at the call to innerText in the then-branch at line 10, the F ⋆ checker (and Z3) uses the property that, for the value t returned by tagName e, we have EltTagName e t from the post-condition; t="head" from the equality test; and using the policy assumption, we can derive CanRead e, the pre-condition of innerText and authorize the call. Using this approach, once type checked, untrusted extension code need not be examined-only the policy (and the annotations on the DOM API) are trusted.

Two key properties of ghost refinements make them well-suited for use in our scenario. We discuss these below. Ghost refinements and erasure. The type x:t{φ } is a subtype of t and the values of these two types have the same representation. This makes specifications using ghost refinements lightweight, since they do not require modifications to underlying code and data. For example, we did not need to modify or even wrap the DOM implementation in order to verify code in this style. Furthermore, the subtyping relation lifts naturally into the structure of function types, promoting reuse in higher order libraries.

Semantics of ghost refinement derivability. For every value v:t that inhabits x:t{φ } our type system ensures that the formula φ [v/x] is derivable. The definition of derivability is subtle and is made precise in §3. However, intuitively, derivability is a logical entailment relation defined relative to a context of dynamic assumptions A . We think of A as a monotonically increasing log of events and formulas that are assumed during evaluation of the program. Formally, a call to tagName e reduces to t and has the effect of adding the formula EltTagName e t to the log. For values given ghost refinement types, there may be no concrete proof at run time to witness the derivability of the refinement formula. Indeed, when working with libraries like the DOM, explicit proof terms witnessing DOM invariants seem both infeasible and undesirable (as they may be very voluminous); ghost refinements fit the bill nicely. Proof-irrelevance and P vs. E-kind. The distinction between P and E-kinds in F ⋆ may, at first, seem reminiscent of the distinction between Type and Prop in a system like Coq. The proof terms for concrete refinements in Coq are often from the Prop universe, indicating that they are computationally irrelevant (and so can be erased during code extraction). In contrast, concrete refinements in F ⋆ are accompanied by P-kinded proof terms, which are computationally relevant. We view proofs as useful runtime entities that carry important information. We choose to make proofs explicit and useful- §2.5 demonstrates a novel way of using concrete proof terms to construct precise provenance trails in a curated database. As such P-kind is closer to Coq's Type. Indeed, our embedding of F ⋆ 's P fragment in CiC translates P-kinded types to types that reside in Coq's Type universe.

E-kind in F ⋆ plays a role more similar to proof irrelevance in Coq. However, the semantics of E-kinded types and ghost refinements is considerably different. Not only are proofs for ghost refinements irrelevant, these proofs may not be constructible at all and E-kinded types may be uninhabited. Instead, the log-based semantics of ghost refinements makes trust assumptions in external code formal and explicit, and allows the definition of security properties for code that are robust even when code is composed with arbitrary attacker code. For example, [START_REF] Guha | Verified security for browser extensions[END_REF] used the log-based semantics to prove a robust safety property that ensures that verified extensions are authorization-safe even when composed with arbitrary untrusted JavaScript on a web page.

Ghost refinements and indexed types for cryptography

Refinement types (in the style of ghost refinements) have been used in F7 to verify implementations of cryptographic protocols. This section presents a small fragment of a library for public key cryptography implemented in a new style (see our website for a more complete library together with several client programs that use cryptography). This style is enabled by features of F ⋆ not available in F7, specifically, the integration of refinements with higher-kinded and indexed types. This example also illustrates the need for ghost refinements. As we will see, it is infeasible to construct concrete proof terms (whether constructive or not) to justify the soundness of cryptographic evidence.

The listing below shows the signature of a module Crypto that provides an interface to work with public key signatures. Informally, signatures provide a means for a party in a protocol to communicate a value and a property of its local environment to a remote party. For example, Alice can sign a message m and send it to Bob, and, if Bob trusts Alice, Bob can conclude that the message originated with Alice. Additionally, given a prior agreement on the usage of keys, Alice can convince Bob of some additional property Pred of the message m, e.g., that the message originated in Alice's file system. The property Pred need not be an intrinsic property of the contents of m-a constructive proof of Pred m in this setting may be nonsensical.

⋆ ⇒ (α ⇒ E ) ⇒ ⋆ type Says :: prin ⇒ E ⇒ E val rsa verify : ∀α ::⋆ ,β ::α ⇒ E . p:prin → pk p α β → x:α → dsig → r:bool{r=true =⇒ Says p (β x)}
Crypto provides a type dsig for digital signatures, here just an alias for bytes. It also exposes an abstract type prin for principal identifiers, and the type constructors sk and pk are for secret keys and public keys respectively.

A private key of type sk Alice α Pred belongs to the principal Alice:prin, who can use it to sign values m of type α that satisfy Pred m. The function rsa sign allows clients to construct a dsig value by signing a message x:α , where the ghost refinement guarantees that the formula β x is derivable when rsa sign is called. Public keys are complementary: rsa verify verifies a signature using the public key pk p α β and, if it succeeds, the caller knows that Says p (β x) is derivable. The predicate Says p φ is the usual lifting of a proposition φ into a modality Says, similar to forms used in a variety of modal authorization logics [START_REF] Chapin | Authorization in trust management: Features and foundations[END_REF]. Intuitively, Says p φ is weaker than φ , and the two coincide when principal p is trusted.

As in F7, an abstract implementation of the Crypto library can be verified against the specification shown above, and can be proved correct with respect to a Dolev-Yao adversary. However, in F7, types cannot be parametrized by predicates, so predicate parameters are instead simulated through a level of indirection. Instead of the F ⋆ type sk p α Pred, private keys in F7 are given a type of the form sk p α usage, and the predicate Pred is replaced by a global predicate SignSays, indexed by p and usage. Verification relies on a programming convention that each key usage must be unambiguously defined by recording an assumption of the form ∀p,usage,v, SignSays p usage v ⇐⇒ Pred v. This convention is not enforced automatically in F7, and hence this style can lead to logical inconsistencies. In contrast, F ⋆ types are more concise, and require fewer dynamic assumptions and no programming discipline beyond typing.

2.4 Ghost refinements and affine-indexed types for state F ⋆ is designed to enable reasoning about effectful programs, whether the effects be in the form of non-termination, state, or I/O. We have seen how P-kind serves to control non-termination and we consider I/O in §4. This section looks at how F ⋆ uses affine types, in combination with E-kinded types, to reason about state.

One innovation of F ⋆ is that it permits indexing types with affine values, allowing properties to be stated about affine values without having them be consumed immediately. We illustrate this feature by showing how to program with linear maps, a data type proposed by [START_REF] Lahiri | Linear maps[END_REF] to verify heap-manipulating programs. For space reasons, we do not show a client program using linear maps-a complete example is available in the F ⋆ distribution.

Linear maps are a data structure that equips a Floyd-Hoare logic (using a classical assertion logic) with a form of local reasoning in the style of separation logic. Instead of modeling the heap of a program as a single monolithic map H:map α β from α -typed locations to β -typed values, the linear maps methodology advocates partitioning the heap H into several fragments H 1 , . . . , H n where the H i have disjoint domains. Each H i is a linear map of type lin α β , and the disjoint domain condition ensures that modifications to H i leave all the other H j unmodified. This allows to formulate a kind of frame rule for programs that use linear maps. Since the assertion logic remains classical, linear map programs can be automatically verified using classical provers and SMT solvers.

type lin :: ⋆ ⇒ ⋆ ⇒ A type Select :: α ::⋆ ⇒ β ::⋆ ⇒ lin α β ⇒ α ⇒ β ⇒ E type Update :: α ::⋆ ⇒ β ::⋆ ⇒ lin α β ⇒ α ⇒ β ⇒ lin α β ⇒ E type InDomain :: α ::⋆ ⇒ β ::⋆ ⇒ α ⇒ lin α β ⇒ E
The listing above defines an abstract type of linear maps and several predicates to model their properties. The kind of lin:: ⋆ ⇒ ⋆ ⇒ A introduces the fourth base kind in F ⋆ : the kind A of affine types. To enforce the disjoint domains invariant on linear maps, Lahiri et al. require that linear maps be neither copied nor aliased. This corresponds directly to the use of affinity in F ⋆ : values of affine type can be used at most once.

The types Select and Update correspond to standard predicates implemented by SMT solvers like Z3: Select l x y states that the map l at the location x contains the value y; Update l x y m states that m is like the map l, except at the location x where it contains the value y. We omit the standard axiomatization of these predicates. Linear maps are partial maps and include a domain. The predicate InDomain x l has the obvious meaning.

Two operations to read and write locations in maps are shown below. (Other operations are omitted). The read function reads a location x out of a map m1 (when InDomain x m1), and returns the value y:β stored at x. Since m1 is affine, read threads m1 back to the caller as m2, where the refinement on m2 shows that it is unchanged. The write function is similar, and in both cases the Select and Update predicates specify the appropriate post-conditions. Predicates on affine values. While seemingly unremarkable, by refining affine values, the types shown above are a significant advance over prior languages that have included substructural and dependent types. For example, in systems like Fine and Linear LF [START_REF] Cervesato | A linear logical framework[END_REF], types are required to be free of affine (or linear) indices, i.e., type constructors of kind t ⇒ k, where t::A are forbidden. There are several reasons for this restriction in prior systems. Most prominently, expressing properties of affine values using concrete refinements requires constructing proof terms where, simply by using an affine resource in a proof term, the resource is consumed. While there are ways to work around this restriction [START_REF] Borgstrom | Verifying stateful programs with substructural state and hoare types[END_REF], they involve relatively complex whole-program transformations.

A key innovation of F ⋆ is to use the E -kind to allow stating properties on affine values directly. Specifically, since E -kinded predicates have no runtime significance, indexing these predicates with affine values does not consume them-in F ⋆ , kinds of the form t ⇒ E are permitted, even when t::A . In our example, we use affine indexes on E -kinded types to state pre-and post-conditions using ghost refinements. However, when modeling linear maps programs, the dynamic log of assumptions (unlike when modeling DOM programs and cryptography) is constant, so F ⋆ 's metatheory guarantees that refinement formulas in pre-and post-conditions are derivable from the axiomatization of linear maps alone.

We defer further discussion of affine indexed types until §4, where we use affine indexes with higher-rank E -kinded types to model concurrent, message passing programs.

Selective erasure using concrete and ghost refinements

The preceding discussion of ghost refinements may lead the reader to believe that they are always to be preferred to refinements with concrete proof terms. This section illustrates that concrete proof terms are useful too, particularly when one is allowed to compute over these terms, to store them, and to communicate them over the network. The example discussed here is an excerpt from a larger program that models a database of scientific experiments, where each record contains a proof term indicating the provenance of the experiment and its "validity", according to some custom notion of validity. The full example brings together several elements, including the use of cryptography with a simple modal logic to authenticate experimental observations. For brevity, we focus just on one aspect: selective erasure and reconstruction of proofs, which may be implemented for both efficiency and confidentiality reasons.

Each experiment record in our database is given the type exp b (for some boolean parameter b, explained shortly). The record contains an optional primary key field xid; a field r:expsetup that defines what ingredients were used in the experiment; and, importantly, a proof term of type proof b (Valid r), where the proof term contains evidence recording the relationship of this experiment to other experiments in the database, i.e., the proof term reflects the provenance of the experiment. The type proof b t represents a value from a proof kernel defining a custom logic tailored to this specific application-another example of F ⋆ 's logic parametricity. We show a selection of the constructors from this kernel below. The interplay between ghost and concrete proof terms is central in this example-it enables proof terms to be selectively erased and later reconstructed. This allows us to maintain compact, yet detailed and reliable provenance trails. The type proof full (Valid r) represents a fully explicated proof of Valid r, with no selective erasure applied. In contrast, values of type proof partial (Valid r) may have been partially erased-these values are not guaranteed to carry a complete provenance for the experiment setup r.

The constructors in the kernel include axioms for basic connectives and axioms like ChemicalVolcano which state validity of some well-known experiments. Axioms like Combine allow new valid experiments to be constructed from other valid ones. The most interesting constructor is Prune, which allows a ghost refinement of the validity of an experiment (r:expsetup{Valid r}) to be traded for a concrete proof term for the validity. To allow proofs to be reconstructed, Prune takes an extra argument, xid:int, the primary key of a record in the database that holds the complete provenance for r.

Now we can give a typed interface to our database (below). The database db is simply a list of experiments with full proofs. It supports operations to insert new experiments (returning an autogenerated private key); to lookup using the primary keys; and to look up just the provenance trail of a particular experiment setup, using a primary key for the experiment. We implement a client-facing interface to the database that wraps the basic lookup and insert operations. On outbound request, we lookup an experiment by its primary key. But, rather than communicate a (potentially large) proof term with explicit provenance to the requestor, we erase the proof (using Prune) and send only a partial proof to the caller, recording the primary key xid in the proof term for later reconstruction. In our full implementation, rather than simply sending a Prune node, we send an authenticated proof term, signed under a key for the database, so that the requestor can conclude that the returned experiment is indeed valid. To use the Prune constructor, we have to prove that r has the type r:expsetup{Valid r}. Although pf is full proof of Valid r, we cannot use pf directly to derive ghost refinement formulas. To connect concrete and ghost refinements, we introduce the assumption above. Given the soundness of the proof kernel, this assumption is admissible, and the type of Prune ensures that the database program never introduces partial proofs for experiments that do not have a valid provenance trail. Despite the fact that the Valid r type has no inhabitants, the introduction of this assumption does not lead to logical inconsistency. Formally, assumptions are simply recorded as effects in the log, and do not produce values that can be destructed, say, via pattern matching.

Finally, on requests to insert new records in the database, we can reconstruct proofs. The function expand below traverses the structure of a proof tree, and expands Prune nodes by looking them up in the database. The database maintains an invariant that each record in the database has a full proof and thus a fully explicated provenance trail, ensured via type soundness. The function expand is, in effect, a partial, effectful proof-search procedure. Despite the use of non-termination and effects, the type system guarantees that if this function terminates and returns Some pf, then pf is indeed a valid full proof in the P-fragment, F ⋆ 's logically consistent fragment of total functions.

Formalizing F ⋆

This section presents the syntax and the semantics of F ⋆ . We focus on five main themes: (1) the stratification into expressions, types and kinds with the ability to describe functional dependences at each level;

(2) the use of kinds to isolate sub-languages for proofs, specifications, and affinity; (3) relating logical effects described using ghost refinements to propositions witnessed by proof terms;

(4) logic parametricity, allowing us to plug-in proof kernels and automated decision procedures for the logics they define; and (5) the consistency of a core universe of propositions, via strong normalization, and the ability to program over its values, to support applications with mobile proofs and selective erasure.

Syntax

The syntax of F ⋆ is shown below. Values include variables, lambda abstractions over values and types, and fully applied n-ary data constructors. The value v ℓ is a technical device used to prove the soundness of affine typing-ℓ is an identifier drawn from a class of names distinct from term and type names. We use the notation a to stand for a finite sequence of elements a 1 , . . . , a n , for arbitrary n; (a) k is a sequence a 1 , . . . , a k-1 . We adopt a (partially) let-normalized view of the expression language e, in particular requiring function arguments to always be values-this is convenient when using valuedependent types, since it ensures that expressions never escape into the level of types. The only other non-standard expression form is assume φ , which has the effect of adding a formula to the log and is explained in §3.3. Types are ranged over by meta-variables t and φ -we use φ for types that stand for logical formulas. Types include variables α, constants T , dependent functions ranging over values whose domain may be values (x:t → t ′ ) or types (∀α::κ.t, written 'a::k -> t in the concrete syntax), types applied to values (t v) and to types (t t ′ ), type-level functions from values to types (λ x:t.t ′ , concretely written fun (x:t) -> t'), ghost refinements x:t{φ }, and finally coercions to affine types ¡t. This modal operator serves to qualify the type of a closure that captures an affine assumption; we include ¡t in the formalism to avoid duplicating the rules for function arrows, but concretely we write affine functions as x:t >> t' and 'a::k >> t instead of ¡(x:t → t ′ ) and ¡(∀α::κ.t).

Kinds κ include the four base kinds ⋆, P, A, and E-we distinguish the first three of these as concrete kinds, since they classify inhabitable types. As at the type level, we have kinds for dependent function spaces whose range are types and whose domain may be either values (x:t ⇒ κ) or types (α::κ ⇒ κ ′ ). Stratifying the language into terms, types, and kinds allows us to place key restrictions (discussed below) that facilitate automated verification, and Syntax: expressions, types, kinds, signatures, environments

v ::= x | λ x:t.e | Λα::κ.e | D t v | v ℓ values e ::= v | e v | e t | assume φ | let x = e in e ′ terms | match x with D ᾱ x → e else e ′ φ ,t ::= α | T | x:t → t ′ | ∀α::κ.t | t v | t t ′ types | λ x:t.t ′ | x:t{φ } | ¡t c ::= ⋆ | P | A concrete kinds b ::= c | E base kinds κ ::= b | x:t ⇒ κ | α::κ ⇒ κ ′ kinds S ::= • | T ::κ{D:t} | S, S ′ signature Γ ::= • | x:t | α::κ | v 1 = v 2 | t 1 = t 2 | Γ, Γ ′ type env. A ::= • | φ | ℓ | l | A , A ′ dynamic log
to compile efficiently to .NET. However, stratification does come at a cost-several pieces of technical machinery are replicated across the levels.

Signatures S are finite lists of inductively defined types. Each inductive definition T ::κ{D:t} introduces a type constructor T of kind κ and all its constructors D 1 :t 1 , . . . , D n :t n . For simplicity, we do not include mutually inductive types, although these are supported by our implementation and their addition to the formalism poses no significant difficulties. We do not need a fixpoint form in the expression language since inductive types allow us to encode recursive functions. To show that terms given P-kinded types are strongly normalizing, a well-formedness condition on signatures imposes a positivity constraint on inductive definitions for Pkinded types. An additional constraint on signatures is that they must contain a declaration unit:: ⋆ {():unit} for the unit type and its one value (). Finally, typing environments Γ track in-scope value variables (x with type t), type variables (α with kind κ), and equivalences between values (v 1 = v 2 ) and types (t 1 = t 2 ) introduced when checking match expressions. We discuss the log A conjunction with the dynamic semantics in §3.3. Briefly, A maintains a set of facts introduced by the dynamic assumption of ghost refinements, and also a set of names ℓ used to track affine values.

The F ⋆ type system

Figure 1 shows key rules from each judgment in the type system. Well-formedness of kinds. The judgment S; Γ ⊢ κ ok(b) states that κ is well-formed and produces types of base kind b (when κ = b) or type constructors for b-kinded types. The rule (OK-TK) shows a key enhancement of F ⋆ over prior languages, e.g., Fine or Linear LF. Types can be constructed from affine values (b 1 = A), so long as the type constructed is purely specificational (b 2 = E). As illustrated in §2.4 and §4, this improves the expressiveness of affine typing significantly, enabling refinements on affine state. (OK-KK) is also an enhancement over Fine to allow dependences and to ensure that types parameterized by affine types are themselves affine. Although our formalism allows higher-kinds like (⋆ ⇒ ⋆) ⇒ ⋆, such kinds cannot be compiled to the type system of the .NET bytecode language and are currently rejected by our compiler. However, retargeting F ⋆ to a platform with a more flexible typing discipline would lift this restriction. Kinding for value-indexed and affine types. The judgment S; Γ ⊢ t :: κ states that type t has kind κ. The rules shown here reveal a few subtle aspects of the type system, starting with affine typing and affine-value indexing. The rule (K-A) shows how the modal operator coerces the kind of a type. (K-Tv) allows a type function t to be applied to a value v; these type functions are introduced either using (K-Fun) or as type constructors T in the signature. Next, recall that we wish to allow affine values to be freely used at the type level, since specifications should not consume affine resources. For this reason, unlike prior languages, the values passed to type functions may use affine assumptions in the context Γthe restrictions imposed by (OK-TK) ensure that such uses of affine assumptions at the type level cannot influence term-level reduction. The second premise of (K-Tv) uses the expression typing judgment, discussed shortly. This judgment has two modes (m ::= • | ε) indicated on the turnstile. When the mode is ε (indicating that the term being typed occurs at the type-level, effectively as an index of an E-kinded type), affine assumptions in the context can be freely duplicated without resulting in their consumption. We discuss how this works shortly, in the context of the (T-X) rule. Ghost refinements, total functions, and sub-kinding. (K-φ ) requires that formulas in ghost refinements be erasable (E-kinded). Formulas in ghost refinements are erased at runtime and refinements apply only to types given concrete kinds c (the first premise of (K-φ )), i.e., inhabitable types. (K-Arr) handles dependent function arrows, which (as seen in §2.1) can be used to represent both quantified formulas in the logic as well as term-level function abstractions. A function arrow is P-kinded if its range type is P-kinded. Finally, (K-Sub) uses a sub-kinding judgment in its premise. Sub-kinding in F ⋆ is defined by the judgment S; Γ ⊢ κ 1 <: κ 2 . Sub-kinding is based on the relation P <: ⋆ <: E, among base kinds, with A <: A only. These base relations are lifted into the structure of arrow kinds, with co-and contravariance as usual. (K-Sub) includes premises to ensure that sub-kinding preserves wellformedness of kinds. We conjecture that these premises can be eliminated in favor of lemmas establishing that sub-kinding never introduces ill-formed kinds. We have yet to prove it, so we include these premises to facilitate our formal proof of well-formedness of kinds produced by derivations. Expression typing. The judgment S; Γ; X ⊢ m e : t states that expression e has type t, under signature S, environment Γ, and an affine environment

X ::= • | ℓ | x | X, X ′ ,
where X, X ′ denotes disjoint union of sets of names. A well-formedness condition on contexts requires all variables x ∈ X to also be bound in Γ. The context X represents a set of available affine assumptions, and usual context splitting rules apply to X when typing the sub-terms of an expression. (As in Fine, we choose not to split Γ itself, since this complicates wellformedness of contexts in the presence of dependent types.) Finally, as mentioned above, expression typing comes in two modes, indicated on the turnstile. Affine typing in two modes. (T-XA) is typical of affine typing systems. To use an affine assumption x, we require x to be present in the affine environment X. In addition, (T-X) provides two exceptions to (T-XA): first, as is standard, we can use non-affine assumptions without requiring them to be present in X. Second, when the mode is ε, we are typing a term at the level of types; since this does not consume the affine resource, we are free to use it even when X is empty. (T-WknX) provides weakening for the affine context. Finally, (T-Abs) is a standard rule with one subtlety that the introduced function type is tagged with the affine modality (using Q(X, x:t → t ′ )) if the function closure captures an affine assumption. ((T-ℓ) is also related to affine typing, but, values v ℓ are used solely to state our type soundness result-we discuss this rule in conjunction with the dynamic semantics.) Ghost refinements and subtyping. The rules (T-As), (T-V), and the subtyping judgments introduce ghost refinement types. (T-As) introduces a unit refined with the assumed formula φ -no logical evidence is produced for φ . To justify this rule, the dynamic semantics of this expression adds a formula to the dynamic log A . (T-V) allows value v to be refined with the formula φ when φ is derivable: S; Γ ′ |= φ . The context Γ ′ includes bindings x:t, x = v which allow the derivability relation to use information about v; however, for kind-correctness, we require the kinding of the introduced formula to not rely on the introduced equality. Ghost refinements have no impact on the representation of values, so they admit structural subtyping. The subtyping rules include (S-φ I), like (T-V), an in-

S; Γ ⊢ κ ok(b) OK-b S; Γ ⊢ b ok(b) OK-TK b 2 = E if b 1 = A S; Γ ⊢ t::b 1 S; Γ, x:t ⊢ κ ok(b 2 ) S; Γ ⊢ x:t ⇒ κ ok(b 2 ) OK-KK b 2 ∈ {A, E} if b 1 = A S; Γ ⊢ κ 1 ok(b 1 ) S; Γ, α::κ 1 ⊢ κ 2 ok(b 2 ) S; Γ ⊢ α::κ 1 ⇒ κ 2 ok(b 2 ) S; Γ ⊢ t :: κ K-A S;
S; Γ ⊢ κ <: κ ′ S; Γ ⊢ κ ok(b) S; Γ ⊢ κ ′ ok(b) S; Γ ⊢ t :: κ ′ S; Γ ⊢ κ 1 <: κ 2 SK-Refl S; Γ ⊢ κ ≡ κ ′ S; Γ ⊢ κ <: κ ′ SK-PStar S; Γ ⊢ P <: ⋆ SK-StarE S; Γ ⊢ ⋆ <: E SK-Prod S; Γ ⊢ t ′ <: t S; Γ, x:t ′ ⊢ κ <: κ ′ S; Γ ⊢ (x:t ⇒ κ) <: (x:t ′ ⇒ κ ′ ) SK-ProdK S; Γ ⊢ κ ′ 1 <: κ 1 S; Γ, α::κ ′ 1 ⊢ κ 2 <: κ ′ 2 S; Γ ⊢ (α::κ 1 ⇒ κ 2 ) <: (α::κ ′ 1 ⇒ κ ′ 2 ) SK-Trans S; Γ ⊢ κ <: κ 1 S; Γ ⊢ κ 1 <: κ ′ S; Γ ⊢ κ <: κ ′ S; Γ ⊢ κ ≡ κ ′ KE-Refl S; Γ ⊢ κ ≡ κ KE-Prod S; Γ ⊢ t ≡ t ′ S; Γ, x:t ⊢ κ ≡ κ ′ S; Γ ⊢ x:t ⇒ κ ≡ x:t ′ ⇒ κ ′ KE-ProdK S; Γ ⊢ κ 1 ≡ κ ′ 1 S; Γ, α::κ 1 ⊢ κ 2 ≡ κ ′ 2 S; Γ ⊢ α::κ 1 ⇒ κ 2 ≡ α::κ ′ 1 ⇒ κ ′ 2 S; Γ; X ⊢ m e : t T-XA S; Γ ⊢ Γ(x) :: A S; Γ; x ⊢ x : Γ(x) T-X S; Γ ⊢ Γ(x)::b m = ε if b = A S; Γ; . ⊢ m x : Γ(x) T-WknX S; Γ; X ⊢ m e : t S; Γ; X, X ′ ⊢ m e : t T-Abs S; Γ ⊢ t::c S; Γ, x:t; X, x ⊢ m e : t ′ S; Γ; X ⊢ m λ x:t.e : Q(X, x:t → t ′ ) T-As S; Γ ⊢ φ :: E t = x:unit{φ } S; Γ; • ⊢ m assume φ : t T-V S; Γ; X ⊢ m v : t S; Γ ⊢ t :: c S; Γ, x:t, x = v |= φ S; Γ, x:t ⊢ φ :: E S; Γ; X ⊢ m v : x:t{φ } T-Let S; Γ; X 1 ⊢ m e 1 : t 1 S; Γ, x:t 1 ; X 2 , x ⊢ m e 2 : t 2 ∀i.S; Γ ⊢ t i :: κ i κ 2 = P ⇒ κ 1 = P S; Γ; X 1 , X 2 ⊢ m let x = e 1 in e 2 : t 2 T-Match S; Γ; X 1 ⊢ m v : t v S; Γ ⊢ t v :: κ v Γ ′ = Γ, α::κ, x:t ⊢ S; Γ ′ wf S; Γ ′ ; x ⊢ m D ᾱ x : t p FV (t v ,t p ) = β , ȳ t v θ = t p θ θ = [t/ β , v/ ȳ] S; Γ ′ , β = t, y = v, v = D ᾱ x; X 2 , x ⊢ m e 1 : t S; Γ; X 2 ⊢ m e 2 : t S; Γ ⊢ t :: κ b κ b = P ⇒ κ v = P S; Γ; X 1 , X 2 ⊢ m match v with D ᾱ x → e 1 else e 2 : t T-ℓ m = ε ⇒ X ′ = ℓ S; Γ; X ⊢ m v : t S; Γ; X, X ′ ⊢ m v ℓ : t T-Sub S; Γ; X ⊢ e : t ′ S; Γ ⊢ t ′ <: t S; Γ ⊢ t ′ :: c S; Γ ⊢ t :: c S; Γ; X ⊢ e : t where Q(•,t) = t Q(X,t) = ¡t S; Γ ⊢ t <: t ′ S-Refl S; Γ ⊢ t ≡ t ′ S; Γ ⊢ t <: t ′ S-φ I S; Γ ⊢ t <: t ′ S; Γ, x:t |= φ ′ S; Γ ⊢ t <: x:t ′ {φ ′ } S-φ E S; Γ ⊢ x:t{φ } <: t S-Arr S; Γ ⊢ t ′ 1 <: t 1 S; Γ, x:t ′ 1 ⊢ t 2 <: t ′ 2 S; Γ ⊢ x:t 1 → t 2 <: x:t ′ 1 → t ′ 2 S; Γ ⊢ t ≡ t ′ S; Γ ⊢ v ≡ v ′ EQ-T t 1 = t 2 ∈ Γ S; Γ ⊢ t 1 ≡ t 2 EQ-V v 1 = v 2 ∈ Γ S; Γ ⊢ v 1 ≡ v 2 EQ-β S; Γ ⊢ (λ x:t.t ′ )v ≡ t ′ [v/x] EQ-VApp1 S; Γ ⊢ v ≡ v ′ S; Γ ⊢ t v ≡ t v ′ ⊢ S ok WFS-D S;
• ⊢ κ ok(c) ∀i.S, T ::κ{}; (α::κ) i ⊢ κ i ok(b i ) ∀ j.S, T ::κ{}; α:κ, (x:t) j ⊢ t j :: c j S, T ::κ{}; α:κ, x:t ⊢ T t′ v′ :: c ∀ j.apos(c, T,t j ::c j ) S ⊢ T ::κ{D:∀α::κ.x:t → T t′ v′ } ok

(c ′ = A ⇒ c = A) c = P ⇒ ∀1 ≤ i < n.T ∈ FTC(t i ) apos(c, T, ((x : t 1 → . . . → t n )::c ′ ))
Figure 1. Selected static semantics of F ⋆ troduction form for ghost refinements and (S-φ E), an elimination form. (S-Arr) lifts the relation into the structure of function typesomitted rules do the same for other constructions. In contrast, concrete refinements (i.e., the dependent pairs of Coq, Fine etc.) do not enjoy this structural subtyping relation. Instead, via a systematic translation to insert coercions (called derefinement) inherited from Fine, F ⋆ provides programmers with a weaker, non-structural subtyping relation on concrete refinements. Subtyping also includes type conversion, an equivalence relation according to the judgment S; Γ ⊢ t 1 ≡ t 2 . This relation, discussed briefly in conjunction with (T-Match), converts types using equations that appear in the context, and is available everywhere within the structure of types. Logic parametricity is embodied by (T-V) and (S-φ I): various definitions of the derivability relation (S; Γ |= φ ) can be "plugged in" to the type system, as long as the relation meets a few important admissibility constraints. Admissible relations must at least be the identity on refined assumptions (S; x : (x:t{φ }) |= φ ); be closed un-der substitution of free variables in Γ; be allowed to use structural rules such as weakening, duplication and permutation; and be insensitive to the presence of derivable equality assumptions in the context (S; Γ, v = v |= φ ⇐⇒ S; Γ |= φ ). Pragmatically, we often plug in a decision procedure for first order logic with additional theories, as implemented by the Z3 theorem prover-the ability to use structural rules (e.g., weakening) in the logic, enabled by our restrictions on the use of affine indices in types, makes it easy to support automation. Formally, we also exploit logic parametricity to provide an embedding of F7's formal core, RCF, into F ⋆ , plugging into (T-V) RCF's entailment relation (which, unlike F ⋆ , includes the basic first-order connectives and equality, each satisfying their usual introduction and elimination forms). Consistency of the P-universe requires placing restrictions in various parts of the type system. For an expression e to reside in P, e must be free of non-P expressions, since those may divergethe last premise of (T-Let) enforces this property. We disallow discriminating on values that reside in ⋆ or A when constructing propositions in the branches of a match-the last premise of (T-Match) shows this. We also have constraints on the wellformedness of inductive type T (recall that we use (α::κ) i to mean α 1 ::κ 1 , . . . , α i-1 ::κ i-1 ). In (WFS-D), the first premise ensures that the kind κ of T is well-formed; the second and third premises ensure that the arguments of D are well-formed; the fourth premise ensures that the constructed type matches the kind expected for T ; and the final premise imposes two key restrictions: (1) constructors with affine arguments must construct affine results-this is unrelated to totality of P-functions; (2) a positivity constraint on inductive P-kinded types. We use a relatively simple version of positivity, excluding the constructed type T in negative position in any argument of D.

These constraints are similar to those imposed by Aura on its Prop universe-to our knowledge, Aura is the only other language that embeds a strongly normalizing core within a language with arbitrary recursion. However, there are several important differences. First, Aura (like Coq) insists on Prop terms being computationally irrelevant, so its match rule forbids cross-universe elimination-Prop terms cannot be eliminated to construct values in Type. We explicitly wish to program over proofs, so F ⋆ permits P-to-⋆ elimination. Next, Aura does not allow the branches of a match expression to use equality assumptions between the pattern and the scrutinized term. This makes it impossible to program on proof terms, as shown in §2.5, which make essential use of GADT-style programming patterns. In contrast, (T-Match) checks the then-branch e 1 in a context that includes equality assumptions induced by unifying the type of the pattern with the type of the scrutinee (the first three premises on the second line). These equality assumptions are used in S; Γ ⊢ t ≡ t ′ to allow typing derivations to freely refine both type and value indices within types. This feature complicates the consistency proof of F ⋆ 's P-fragment. We discuss this aspect when presenting the metatheory of F ⋆ .

Dynamic semantics: logical effects and affine names

The dynamic semantics of F ⋆ is a small-step reduction relation for a call-by-value language. It has the form (A ; e) → S (A ; e ′ ) where the signature S is unvarying. The interesting part of this relation is the log A , a non-decreasing set of logical facts φ and names ℓ for affine values. As mentioned in §2.2, the set of facts in A is used in the definition of ghost refinement derivability. Facts are added to the log using the assume φ form, which reduces as below.

E-Log (A ; assume φ ) → S (A , φ ; ())

Foreshadowing our safety condition for ghost refinements (Corollary 1), we show that, when a well-typed program e : x:t{φ } reduces to a value, that is (•; e) → * s (A ; v), its refinement formula φ is derivable from the signature and all the accumulated logical effects: S; Facts(A ) |= φ [v/x]. This is in contrast to our soundness result for proof terms, expressions that reside in the P-fragment, for which we obtain a more traditional logical consistency property. In a distributed program, the log is an idealized global view of the logical state of all participants. Ghost refinements accompanied by cryptographic evidence (in the form of digital signatures) enable speaking about this distributed state.

The log also tracks affine values. We aim to show that welltyped programs destruct affine values at most once. For this purpose, we instrument the dynamic semantics to tag an affine value v with a fresh name when it is introduced, recording the name in the log (E-Newℓ). Names held in the log come in two variants: names ℓ are "live", while names l are "dead". When v appears in a destruct position (the context E in (E-Killℓ), which includes the function position of a β redex, and the scrutinee position of a match), we require the name ℓ to be "live" in the log for reduction to not get stuck, kill the name in A , and then proceed. This instrumentation serves as our specification of the use-at-most-once property.

E-Newℓ

S; Facts

(A ) ⊢ t :: A fresh ℓ S; Facts(A ); LiveNames(A ) ⊢ v : t (A ; v) → S (A , ℓ; v ℓ ) E-Killℓ (A 1 , ℓ, A 2 ; E[v ℓ ]) → s (A 1 , l, A 2 ; E[v]) 3.4 Metatheory of F ⋆
Our first theorem is a type soundness result, stated in terms of standard progress and preservation lemmas. In addition to welltyped programs not getting stuck, this result ensures that affinely typed values are destructed at most once, and can thus be soundly implemented using destructive reads and mutation. (The theorem relies on an auxiliary judgment S ⊢ A =⇒ Γ; X which obtains a context Γ; X from the dynamic log, where Γ includes the logical assumptions accumulated in A , and live names in A recorded in X.) THEOREM 1 (Type soundness). For all S, A , Γ, X, X ′ , e, and t such that

(1) S ⊢ A =⇒ Γ; X, (2) ⊢ S; Γ; X wf, and (3) S; Γ; X ′ ⊢ e : t where X ′ ⊆ X, either e is a value, or there exist A ′ , e ′ , Γ ′ , and X ′′ such that

(1) S ⊢ A ′ =⇒ Γ ′ ; X ′′ , (2) X ′′ = (X ′ \ DeadNames(A ′ )) ∪ LiveNames(A ′ \ A ), (3) ∃Γ ′′ .Γ ′ = Γ, Γ ′′ , and (4) S; Γ ′ ; X ′′ ⊢ e ′ : t.
From type soundness, we obtain our main safety property for ghost refinements: their formulas are derivable from the logical effects accumulated in the log.

COROLLARY 1 (Safety for ghost refinements). For all S, A , Γ, e, φ , t, A ′ , Γ ′ , and v such that ⊢ S ok, S ⊢ A =⇒ Γ; X, S; Γ; X ⊢ e : x:t{φ }, and (A ; e) → * S (A ′ ; v), there exists

Γ ′ such that S ⊢ A ′ =⇒ Γ ′ ; and S; Γ ′ |= φ [v/x].
Theorem 2 (Logical consistency of P) shows logical consistency of the P-fragment, by translating P-terms into CiC (The Coq Development Team 2010), which is widely believed to be strongly normalizing. Intuitively, the theorem states that the translation of F ⋆ 's P-fragment into CiC is a (weak) simulation, with regard to F ⋆ and CiC's reduction relations. Since in CiC, all reduction sequences are presumed to be finite, this guarantees the absence of infinite reduction sequences for F ⋆ 's P-terms. A direct proof of strong normalization of F ⋆ 's P-fragment is likely to be challenging since it involves inductive types like CiC. Our proof strategy borrows ideas from a proof of a related property in Aura. However, unlike Aura, F ⋆ supports implicit type conversions using equalities introduced by pattern matching-we find this essential for programming over proof terms. We translate this to CiC through the use of explicit, equality-witnessing conversions in CiC.

In the statement of the theorem below, (S; Γ; • ⊢ p e : t ֒→ τ) is the translation that marks non-P-lambdas in F ⋆ term e and translates them to a CiC term τ. ( ) is the reduction of P-terms; and (-→ β ,ι,δ ) is term conversion in CiC.

THEOREM 2 (Logical consistency of P). For all S, Γ, p, e, e ′ , t, τ such that ⊢ S; Γ ok E and S; Γ ⊢ t :: P, if S; Γ; • ⊢ p e : t ֒→ τ and e e ′ , then there exists τ ′ such that τ -→ * β ,ι,δ τ ′ and S; Γ; • ⊢ p e ′ : t ֒→ τ ′ .

Theorem 3 (Well-typed translation of RCF) is an embedding into F ⋆ of a core fragment of RCF without Public/Tainted kinds, without concurrency, and with restrictions on the use of RCF's isorecursive types. In the statement below, A is an RCF configuration; E is an RCF context; and A → A ′ is a single step of reduction in RCF. The notation [[•]] means translation. The judgment E ⊢ ⋄ means that E is well-formed. The translation is over the structure of RCF typing derivations. The theorem states, roughly, that well-typed RCF terms translate to well-typed F ⋆ terms, and that the translation is a simulation, i.e., reduction steps in RCF correspond to reductions in F ⋆ .

Coq formalization

The proofs of the metatheory of F ⋆ were initially done by hand. As we reached completion of the hand proofs, we started a formalization of the meta-theory of F ⋆ in the Coq proof assistant, using the SSREFLECT extension [START_REF] Gonthier | [END_REF]. At the time of writing, we had formalized the whole calculus definition, along with a major part of its metatheory, including all the key technical lemmas up to substitutivity, and a partial proof of the type soundness result. We found a few oversights in our pencil and paper proofs, which we have since corrected. We expect to have a fully mechanized type soundness proof in the near future. A more challenging, next step is a formalization of the embedding of the propositional part of F ⋆ to CiC. We plan to use the Barras's formalization of CiC 1 as a basis.

Our formalization in Coq is noteworthy in several ways. First, this is the first time the SSREFLECT package has been used to carry out a large development in programming language metatheory. We started out attempting to use the Coq code generator Ott [START_REF] Sewell | Ott: Effective tool support for the working semanticist[END_REF] to help reduce the gap between the formal and informal descriptions of our type system. Although this did help in the maintenance of the two versions of the type system, we found that with the many different kinds of variables in F ⋆ , the code produced by Ott resulted in a very large, incomplete set of lemmas.

Following this experience, we have developed a new framework for metatheory using SSREFLECT, and use it on F ⋆ -a particularly challenging test case, since it involves many kinds of names and binders, with subtle differences across the levels of terms, types and kinds. Furthermore, most central judgments in the type system are mutually recursive. Despite these complications, we are happy to note that our framework has allowed us to develop short, largely automated proofs. Our experience is encouraging initial progress towards an eventual goal: a general framework, based on the reflection pattern and the theory of the pure lambda calculus, dedicated to the study of type systems. We think that the development of the F ⋆ formal meta-theory will serve as a basis of such a framework.

Secure multi-party sessions in F ⋆

This section shows how to use the libraries and programming idioms in §2 to write and verify realistic distributed security applications. The combination of cryptographic evidence, ghost refinements, and affine types proves crucial for this case study and enables more precise specifications and stronger proofs than earlier results obtained using F7 [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF].

Multi-party sessions

Multi-party sessions [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF][START_REF] Deniélou | Dynamic multirole session types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]) offer a powerful method to structure and build distributed message-based applications when their message 1 http://www.lix.polytechnique.fr/ ~barras/proofs/sets/ flow is fixed beforehand. Consider a 3-party session between a customer (c), a website (w), and a credit-card verifier (v), with the message flow below: The customer initiates a Checkout session for buying some items (cart), billed to her credit card cc for the total amount a. The web site then either rejects the transaction outright, or asks for credit card verification. The customer is redirected to a verification server and provides a password (p) to authorize payment of a on her credit card cc. The verifier then either confirms or declines payment to the web site, who completes or aborts the session accordingly.

Such a session specifies a contract between component programs in a distributed application. Every program promises to play one role of the session, and in return, it expects the others to correctly play their roles. For instance, w promises not to charge more than a, and not to abort the transaction if the payment is approved: c can rest assured that if she receives an Abort message, her credit card has not been charged.

A variety of type systems have been proposed to verify that a program complies with a session role, and each type system is tailored to a specific set of session primitives and programming language features. Instead, we encode multi-party sessions as F ⋆ types. By standard F ⋆ typing, we can verify that a program correctly plays a session role. Even if some programs deviate from their role at run-time (because they have been taken over by an attacker, for example), we show how the rest of the application can protect itself by using a custom cryptographic protocol.

A session API in F ⋆

We define a generic session API for distributed applications to enforce a multi-party session discipline. We start with a simplified version of our API, then build up to showing our model of more complex features.

To begin with, we ignore the values (cart, cc, a, p) passed in the session and aim to control the sequence of messages a session participant can send and receive. Using affine types, we can define a type for a role process, type role0::E ⇒ A , where the parameter of the role is a type describing an automaton. The types used to define these automata are purely specificational-they are given E-kind. A value of a role process type is a handle that gives a program the capability to enact the automaton. We show two simple automata types provided by our API, and a function that consumes and returns a role handle. The Send0 automaton is indexed by two types-the first, a type 'm of the message to be sent by the process; the second, a type 'k representing a continuation process, where the process is dependent on the value of type 'm sent in the first state. Done represents a finished automaton. Using these automata, we can define the following role process type that represents a program that first sends an integer x, then an integer y greater than x, and then concludes. (In concrete syntax, we write fun (x:t) ⇒ t' for a typelevel function λ x:t.t ′ ; fun ⇒ t' ignores its type argument.) role0 (Send0 int (fun (x:int) ⇒ Send0 (y:int{y > x}) (fun ⇒ Done)))

Our full API generalizes the automata types above with the notion of a global distributed store for session values; each participant maintains a local view of the store and we ensure, by typing, that these views are consistent. We show below the extended analogs of role0, Send0, and also automata types for receiving a message and for choice-points in the session graph. The type of a role process (role) is parametrized by a store value (of type 'st); automata types (Send, Recv) are indexed by binary predicates δ on 'st values that define the allowed changes to the store during the next step. The function send allows a client to send a message m and update the store from s0 to s1 given that the current role process is a Send and that the stores satisfy the predicate δ attached to Send-client programs calling send have to prove δ s0 s1 for some specific instantiation of δ , and our type checker uses Z3 to assist with the proof of such ghost refinement properties. The code below shows how we can use this session API to model the website role (w) in the example session of §4.1. The type msg defines the set of messages and the type store is the type of the distributed store (including, for this example, the names of each participant in the session, their view of the contents of the shopping cart, etc.) The process automaton involves an alternation of message send and receive, and this type uses two store update predicates (of kind store ⇒ store ⇒ E ): Update id c v cart cc a allows initial assignments from the customer to id, c, v, cart, cc, and a; then Unchanged disallows any changes. Type soundness ensures that a well-typed program is guaranteed to comply with its declared role process. For example, a program that joins a session in role w obtains a role handle of type role proc w init store w. It may then call the receive function (the counterpart of send, not shown here) to receive a Checkout message but cannot call send; subsequently, it may call send with either a Reject or a Verify message, but not both.

In earlier work, [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF] showed how to encode multi-party sessions as refinement types in F7. However, since the F7 type system does not support generic predicate-indexed types, such as Send above, they encode the session using large sessionspecific logical formulas rather than types. Our use of F ⋆ higherorder kinds here yields session specifications that are, in general, one-third the size of the corresponding F7 specifications. Moreover, F7 lacks affine types, and they have to prove by hand, with the help of an awkward continuation-passing style encoding, that their applications use role handles linearly.

Custom cryptographic protocols for session consistency

Distributed applications typically run in an untrusted environment, where the network and one or more of the session participants may be under the control of malicious adversaries. In this scenario, cryptographic mechanisms, such as digital signatures, can be used ensure that all honest session participants have consistent states. For example, when the client c receives an Abort message from the website w, it may demand that this message include a valid signa-ture proving that card verifier v Declined, to prevent a malicious w from double-crossing c. [START_REF] Bhargavan | Cryptographic protocol synthesis and verification for multiparty sessions[END_REF] show how to systematically use cryptographic evidence as proof of session compliance. They compile multi-party sessions to efficient custom cryptographic protocols that exchange and check a minimal number of digital signatures to ensure global session consistency. Their compiled protocols use session types and cryptography in the style of F7: without higherorder kinds, affinity, or predicate-indexed types.

We implement secure multi-party sessions in F ⋆ using protocol libraries adapted from those of Bhargavan et al., but instead using the crypto library of §2.3 and the sessions API shown above. In our example session, the Abort message from w to c carries two digital signatures, one from w and one from v, each signature authenticating the last message sent by the corresponding principal and the values in its store at that time. On receiving the Abort message, c verifies these signatures and checks that they conform to the session type: in particular, that the signature from v says that v sent a Decline message and not an Approve. The resulting type for the recv Abort function (a specialization of the generic receive function in our API) is as follows: The function takes the current store st c at c and a role handle for c that must be in the state after c has sent Auth. The function returns an (unchanged) store st c' and a new (completed) role handle. The E-kinded predicates Aborted and Declined represent the session states at the other roles. For example, Declined p st means that the principal p, playing role v previously sent a Decline when it had a store st. Hence, the post-condition says that the principals st c.w and st c.v (playing w, v) claim to be in the states Aborted st c.w st w and Declined st c.v st v where the stores st w and st v are the same as c's store st c'. So if v is honest, then even if w is malicious, it cannot cause c to accept an Abort unless v sent a Decline. Note that the post-condition is a ghost refinement that is proved here using a combination of cryptographic evidence and F ⋆ typechecking.

Encoding advanced session constructs in F ⋆

The four automata types shown above are adequate to represent a wide variety of static sessions that do not use delegation or parallelism. Adding constructors for recursive sessions is straightforward. We now show how to extend our API to capture a limited form of parallelism, inspired by the dynamic multi-role session types of [START_REF] Deniélou | Dynamic multirole session types[END_REF].

Distributed applications often run several instances of the same role in parallel, for scalability. For example, a web site may run several copies of a web server all connected to the same backend database. Or, a client may fork several processes that may communicate with a server in parallel, in an arbitrary order. To verify such applications we extend our sessions API with three new automata types: Fork, Join, and Await.

The Fork automaton (given below) enables a role to fork multiple instances of a child role, transfer control to them, and then wait for them to complete. These child role processes may either execute sequentially (in any order), or in parallel. Each child process is given a unique principal name which it can use when communicating with its parent or with other roles. The Join automaton enables the child role to transfer control back to the parent; and Await represents a parent role process waiting for its children to complete.

We illustrate Fork and its use in an application below, where we elide the store for simplicity (and so use role0 instead of role). The function go forks a number of children (indexed by a given list of principals ps). Each child sends a Request message, then receives a Response message and then joins its parent (p). Here, the variable client is a role handle that has an automaton type of the form Fork ps Done ChildRole, where the automaton ChildRole sends a Request, receives a Response and then Joins its parent. Since role handles have an affine type, the code here passes client in and out of every session operation. The variable children is given an affine list type, which guarantees that the different child processes cannot interfere with each other; in other words each Response can be accurately correlated with its corresponding Request.

Implementation and Measurement

This section describes the implementation of our prototype F ⋆ compiler and its performance measured on a variety of programs (about 20,000 lines of code in total), including cloud applications, cryptographic protocols, and secure browser extensions. Compilation. The F ⋆ compiler consists of about 35,000 lines of F# code and is still under active development. It is based on the type-preserving compiler for Fine [START_REF] Chen | Type-preserving compilation of end-toend verification of security enforcement[END_REF]. It takes as input an F ⋆ program and typechecks the program by asking logical queries of Z3. The compiler also accepts Fine and F7 programs and translates them into F ⋆ . Source programs are then compiled to RDCIL, a small extension of a functional core of the .NET bytecode language CIL. Like DCIL, the target language of Fine, RDCIL extends CIL with type-level functions and value parameters (in addition to type parameters) in class declarations, to model valuedependent types in the source language. Unlike DCIL, RDCIL also supports ghost refinements. RDCIL encodes these additional type constructs as custom attributes, so RDCIL binaries can run on stock .NET virtual machines, access libraries of other .NET languages (e.g., C# and F#), and be called from those languages. RDCIL is fully typed and can be verified (with the help of Z3) for security, the same way F ⋆ is verified. Checking two forms of refinements in RDCIL. Ghost refinement is a new feature of F ⋆ and RDCIL, not supported by Fine or DCIL. Ghost refinements in F ⋆ are translated to ghost refinements in RDCIL, and the typechecker for RDCIL verifies them using Z3.

Concrete refinements are handled similarly in F ⋆ and Fine. During source typechecking, the F ⋆ compiler extracts proofs of concrete refinements from the SMT solver and injects them as terms in the generated RDCIL. Hence, concrete refinements in the source program are translated to a pair of a value and an explicit proof in RDCIL, which can be verified by the RDCIL type checker. Reducing the size of generated bytecode. Explicit proofs can be costly though. Carrying proofs increases the code size by 50x for a Fine benchmark. The F ⋆ compiler addresses this difficulty by relying on the RDCIL typechecker to reconstruct proofs by refinement type checking, rather than just depend on explicit proofs. As a result, RDCIL programs contain far fewer proofs compared to DCIL, and the overhead of proofs and types is only 60% for our bench-marks. The F ⋆ compiler also reduces the size of generated bytecode (ignoring proofs and custom attributes for types), because higherorder dependent kinds allow more concise translation of polymorphic types and higher-order code, which are prevalent in F ⋆ programs. Combining the two factors, the F ⋆ compiler produces binaries an order of magnitude smaller than those produced by Fine, as much as a 45x improvement.

Benchmarks and Measurements

Code size. We compile the Fine benchmarks in [START_REF] Chen | Type-preserving compilation of end-toend verification of security enforcement[END_REF] with the F ⋆ compiler, treating all refinement types as ghost refinements. This way, no proofs are extracted. The table below shows the names of the benchmarks (column Bench.), the F ⋆ code size (in bytes) with and without custom attributes for the additional types (A+ and A-respectively), and Fine size (in bytes) with and without proofs reported in [START_REF] Chen | Type-preserving compilation of end-toend verification of security enforcement[END_REF]) (Pf+ and Pf-respectively). The Fine numbers reflect only proof overhead, not attributes. Because of no proofs, the code size overhead is simply the custom attributes for encoding more expressive types than the CIL types. Column "A+/A-" shows that RDCIL code with those custom attributes is about 1.3x-1.9x of the code without the custom attributes, with an average 60% overhead for the custom attributes. Our current implementation simply uses compressed strings of pretty-printing types as custom attributes. A smarter encoding may further reduce the size overhead.

The RDCIL code is about an order of magnitude smaller than the DCIL code for the Fine benchmarks. Column "A+/Pf+" shows that the RDCIL code (with custom attributes) is about 3%-70% of the DCIL code (with proofs), with an average of 5%-a 20x improvement. Column "A-/Pf+" shows that the RDCIL code (without custom attributes) is about 2%-38% of the DCIL code (with proofs), with an average of 3%-indicating a 30x improvement in this configuration, although the accurate breakdown is hard to obtain because Fine numbers do not include custom attributes. Benchmarks with less proofs, e.g., Authac and Automaton, show less reduction. Column "A-/Pf-" shows that the pure code size of RDCIL is about 10% to 80% of that of DCIL, with an average of 60%-a 40% reduction because of a more expressive type language. Prooflib is purely refinement-free code. The 10x reduction in code size is entirely due to dependent higher kinds. Compilation and typechecking times. The table below shows the time taken to typecheck and compile the Fine benchmarks as well as several new F ⋆ programs we develop ourselves. For each program, it shows number of lines of source code (LOC), source parsing and checking time (SC, in seconds), compilation of F ⋆ to RD-CIL time (Trans), target checking time (TC), and the number of queries made to Z3 by the source checker (SQ) and target checker (TQ). All measurements were performed on a 2.67 GHz two-core Intel Core i7 CPU running Windows 7. HealthwebEnh is a cloud application managing an electronic medical record database, interacting with code written in ASP.NET, C#, and F#. It is about twice as big as the Fine HealthWeb benchmark, and is deployable on Microsoft Windows Azure.

HigherOrderIter and HigherOrderFoldr implement higher-order library functions that iterate over lists. Permission implements a stateful API of collections and iterators that guarantee that the collection underlying an iterator is never modified while an iteration is in progress. Iflow state provides an information-flow tracking library for stateful programs. Provenance is a larger version of the curated database in §2.5. Browser exts is a suite of 17 browser extensions, verified for authorization and information flow properties. DynSessions is the example of §4, including fork/join parallelism.

Fine and F ⋆ source typechecking times are roughly equivalent. F ⋆ translation is faster than Fine because there are fewer proofs to translate. Conversely, typechecking RDCIL code with refinement types is slower than checking DCIL proofs, but in view of the many advantages of F ⋆ , such as smaller bytecode and more expressive types, we find this tradeoff worthwhile. Verifying cryptographic applications. Finally, we report source code verification results for several cryptographic protocol examples, many of which were previously developed for F7, and are now verified by F ⋆ . CryptoLib is a large F7 library implementing symbolic cryptography, which is used in all subsequent applications. KeyManager is a key management application. AuthRPC implements an authenticated RPC protocol. SessionLib is the generic API for multiparty sessions ( §4), used to securely implement a two-party session Commit and a three-party session Forward. Metering is a privacyfriendly zero-knowledge cryptographic protocol for smart metering (Rial and Danezis 2010).

Related work

We have compared F ⋆ to Fine, F7, Aura, Coq, Agda, and discussed other related work in detail throughout this paper. Here, we briefly cover a few more topics. [START_REF] Guts | Reliable evidence: Auditability by typing[END_REF] show how to build cryptographic audit trails that can be verified by independent third parties; [START_REF] Vaughan | Evidence-based audit[END_REF] argue that logs of logical evidence could also build audit trails. Neither consider the combination of mobile logical and cryptographic proofs, augmented with selective erasure and reconstruction. Related work on session types focuses on enforcing session compliance in the absence of malicious adversaries. [START_REF] Honda | Multiparty asynchronous session types[END_REF] develop special-purpose type systems for multi-party asynchronous sessions. They do not consider security or source code verification. [START_REF] Kiselyov | Fun with type functions[END_REF] add type functions to Haskell and show how these can be used to program simple two-party sessions.

  val tail: l1:list α → (l2:list α * pf (x:α → pf (Mem x l2) → pf (Mem x l1))) let tail = function [] → [] | hd::tl → tl

  module Crypto type dsig = bytes ( * type of digital signatures * ) type prin ( * name of a principal * ) type sk :: prin ⇒ α ::⋆ ⇒ (α ⇒ E ) ⇒ ⋆ val rsa sign : ∀α ::⋆ , β ::α ⇒ E . p:prin → sk p α β → x:α {β x} → dsig type pk :: prin ⇒ α ::

  val read: x:α → m1:lin α β {InDomain x m1} → (y:β * (m2:lin α β {m1=m2 && Select m1 x y}))val write: x:α → y:β → m1:lin α β {InDomain x m1} → (m2:lin α β {Update m1 x y m2})

  type expsetup = list {reagent:string; quantity:int} type Valid :: expsetup ⇒ E type exp (b:bool) = (xid:option int * r:expsetup * proof b (Valid r))

  let full, partial = true, false type proof :: bool ⇒ E ⇒ P = | AndIntro: ... | AndElim1 : ... | ... | ChemicalVolcano: proof full (Valid[{reagent="(NH4)2Cr2O7"; ...}]) | Combine: r1:expsetup → r2:expsetup → r3:expsetup → b:bool → proof b (And (Union r1 r2 r3) (And (Valid r1) (Valid r2))) → proof b (Valid r3) | Prune: r:expsetup{Valid r} → xid:int → proof partial (Valid r)

  type db = list (exp full) val insert: exp full → int val lookup: xid → option (exp full) val lookupProof: r:expsetup → xid:int → option (proof full (Valid r))

(

  * Erasing outbound proofs * ) assume ∀(b:bool) (r:expsetup) (pf:proof b (Valid r)). b=full =⇒ Valid r let readExp xid : option (exp partial) = match lookup xid with | Some (xid, r, pf) → Some (xid, r, Prune r xid) | None → None

(

  * Reconstructing proof terms on inbound requests * ) let rec expand (c:bool) (pf:proof c α ) : option (proof full α ) = if c=full then Some pf else match pf with | Prune r xid → lookupProof r xid | AndElim1 c1 pf → (match expand c1 pf with | Some pf' → Some (AndElim1 full pf') | → None) | ... ( * Inserting a new record in the DB * ) let insertExp (r:expsetup) (c:bool) (pf: proof c (Valid r)) = match (expand c pf) with | Some pf' → Some (insert (None, r, pf')) | → None

THEOREM 3 (

 3 Well-typed translation of RCF). Given E ⊢ [[A]] = (A ; e), ⊢ [[E]] = S; Γ, and E ⊢ ⋄, we have S; Γ; . ⊢ e : t where E ⊢ [[T ]] = t. Additionally A → A ′ if and only if (A ; e) → S (A ; e ′ ) and E ⊢ [[A ′ ]] = (A ′ ; e ′ ).

type

  Send0 :: 'm::⋆ ⇒ 'k::('m ⇒ E ) ⇒ E type Done :: E val send: m:'m → role0 (Send0 m 'k) → role0 ('k m)

  type role:: 'st::⋆ ⇒ E ⇒ 'st ⇒ A type Send:: 'm::⋆ ⇒ 'st::⋆ ⇒ 'm⇒ ('st⇒ 'st⇒ E )⇒ 'k::('m⇒ E )⇒ E type Recv:: 'm::⋆ ⇒ 'st::⋆ ⇒ 'm⇒ ('st⇒ 'st⇒ E )⇒ 'k::('m⇒ E )⇒ E type Choice:: 'l::E ⇒ 'r::E ⇒ E val send: m:'m → s0:'st → s1:'st{δ s0 s1} → role (Send 'm 'st m δ 'k) s0 → role ('k m) s1

  type msg = Checkout | Reject | Verify | Auth | Approve | (...) type store = {id:nat; c:prin; w:prin; v:prin; cart:string; (...) } type proc w = Recv Checkout Update id c v cart cc a (fun ⇒ Choice (Send Reject Unchanged (fun ⇒ Done) (Send Verify Unchanged (fun ⇒ Choice (Recv Approve Unchanged (fun ⇒ Send Complete Unchanged (fun ⇒ Done))) (Recv Decline Unchanged (fun ⇒ Send Abort Unchanged (fun ⇒ Done))))))

type

  Aborted:: w:prin ⇒ st w:store ⇒ E type Declined:: v:prin ⇒ st v:store ⇒ E val recv Abort: st c:store → role (RecvCompleteOrAbort) st c → (st c':store * role Done st c'){ Unchanged st c st c' ∧ Says st c.w (∃ st w. Aborted st c.w st w ∧ Unchanged st w st c') ∧ Says st c.v (∃ st v. Declined st c.v st v ∧ Unchanged st v st c')}

type

  Fork :: ps:list prin ⇒ 'ParentProc::E ⇒ 'ChildProc::(role0 (Await ps 'ParentProc) ⇒ prin ⇒ E ) ⇒ E let go ps : role0 Done = let client = startClient ps in let client, children = fork ps client in let children = map (fun (q, child) → let child = send0 Request child in let Response, child = receive0 child in (q, child)) children in join ps client children

  EltTagName e "head" is derivable. Unlike the Mem predicate in §2.1 (which has P kind), EltTagName and CanRead construct erasable, or E -kinded, types. Erasable types are generally uninhabited and have no constructors. Instead, we use them for specifications, as in the types of innerText and tagName. EltTagName e "head" =⇒ CanRead e 9 ( * Extension code (untrusted) * ) 10 let read e = if tagName e = "head" then innerText e else ""

	4 type CanRead :: elt ⇒ E
	5 val innerText: e:elt{CanRead e} → string
	6 val tagName: e:elt → t:string{EltTagName e t}
	7 ( * Extension policy * )
	8 assume ∀e.
	1 ( * Fragment of DOM API * )
	2 type elt
	3 type EltTagName :: elt ⇒ string ⇒ E