Resource Bound Certification^{∗}

Karl Crary

Carnegie Mellon University Stephanie Weirich

Cornell University

Abstract

Various code certification systems allow the certification and static verification of important safety properties such as memory and control-flow safety. These systems are valuable tools for verifying that untrusted and potentially malicious code is safe before execution. However, one important safety property that is not usually included is that programs adhere to specific bounds on resource consumption, such as running time.

We present a decidable type system capable of specifying and certifying bounds on resource consumption. Our system makes two advances over previous resource bound certification systems, both of which are necessary for a practical system: We allow the execution time of programs and their subroutines to vary, depending on their arguments, and we provide a fully automatic compiler generating certified executables from source-level programs. The principal device in our approach is a strategy for simulating dependent types using sum and inductive kinds.

1 Introduction

A current trend in systems software is to allow untrusted extensions to be installed in protected services, relying on language technology to protect the integrity of the service instead of hardware-based protection mechanisms [11, 20, 1, 16, 14]. For example, the SPIN project [1] relies on the Modula-3 type system to protect an operating system kernel from erroneous extensions. Similarly, web browsers rely on the Java Virtual Machine bytecode verifier [11] to protect users from malicious applets. In both situations, the goal is to eliminate expensive inter-process communications or boundary crossings by allowing extensions to access directly the resources they require.

Recently, Necula and Lee [16, 15] have proposed Proof-Carrying Code (PCC) and Morrisett et al. [14] have proposed Typed Assembly Language (TAL) as language technologies that provide the security advantages of high-level languages, but without the overheads of interpretation or just-in-time compilation. In both systems, low-level machine code can be heavily optimized, by hand or by compiler, and yet be automatically verified through proof- or type-checking.

Each of these systems (SPIN, Java, TAL, and Touchstone [18], a compiler that generates PCC) automatically certifies a large set of important security properties, such as type safety, memory safety, and control-flow safety. However, one important security property that none of these systems certifies is bounded termination; none can guarantee that an accepted program will terminate within a given amount of time. Such guarantees of running-time bounds (and, more generally, of resource-consumption bounds) are essential to many applications, such as active networks and extensible operating system kernels. To obtain such bounds on resource consumption, code consumers have generally had to rely on operating system monitoring, which can be costly and which works against the direct access afforded by language-based mechanisms.

To redress this shortcoming, we present a decidable type system called LXres for specifying bounds on resource consumption and for certifying that programs satisfy those bounds. In this paper we will focus on specification and certification of running-time bounds; we consider at the end how our mechanisms can be generalized to other sorts of resources, such as space. Note that we make no effort to infer any bounds on resource consumption; rather we provide a mechanism for certifying those bounds once they have been discovered by the programmer or by program analysis.

We have implemented our type system within the framework of the Typed Assembly Language security infrastructure [14, 13]. The implemented version of this work (called TALres) lowers the mechanisms we discuss in this paper down to the TAL level, augmenting TAL’s very low-level safety certification with running-time guarantees. We have also implemented a prototype certifying compiler that generates TALres, taking as its input an impure functional language (called PopCron) derived from a safe dialect of C [13] and annotated with termination information. Many of the low-level details that are the focus of TAL are not germane to certification of resource bounds, so in the interest of clarity we present our results at a higher level before discussing TALres informally.

2 Informal account

At its core, our approach is quite simple. Following Necula and Lee [17], we augment the underlying computing machinery with a virtual clock that winds down as programs execute. The virtual clock exists only in support of the formal semantics; the machine provides no run-time operations that can inspect the clock, and therefore the clock need not be (and is not) implemented at run time. The pertinence of the clock is to the type system: Function types, in addition to specifying the types of a function’s argument and result, also specify that function’s beginning and ending clock readings. For example, a function that takes an integer at time 15 and returns another integer at time 12 could be given the type:

∗This material is based on work supported in part by ARPA grant F19628-95-C-0050, AF grant F49620-97-1-0013, and NSF grant EIA 97-03470. The second author was supported in part by an NSF graduate fellowship.

To appear in the Twenty-Seventh Symposium on Principles of Programming Languages, Boston, Massachusetts, January 2000. Last revised November 3, 1999.

(int, 15) → (int, 12)

However, such a type is unduly specific. By specifying the starting clock to be 15, this type restricts its members so that they may be started only at one particular time. We would prefer a more flexible type the specifies that the function runs in 3 clock steps. Indeed, since there exist no operations that can inspect the clock, that is the entire import of the above type anyway.

We can get the desired type by using polymorphism to abstract over the finishing time. For example, the type

∀n. (int, n + 3) → (int, n)

specifies that for any time n, when presented with an integer at time n + 3, its members return an integer at time n. In other words, its members run in 3 clock steps. The former type can be obtained by instantiating n with 12, but such functions can also be run at any other time (provided the clock reads at least 3) by a suitable instantiation.

As a minor point, we also allow programs to waste clock steps on demand, so a function with the latter type could in fact take 1 or 2 steps and then waste the remaining steps as necessary to meet the specification. Also, due to some practical considerations that we discuss in Section 4, we only step the clock for function calls. However, this decision is only to simplify the compiler, and has no significant impact on the design of the language; one could just as easily use a tighter measure of running time such as the number of instructions executed.

To make this concrete, consider the function map pair, a higher-order function that takes a function f and a pair p, and applies f to both components of p:

Λα:Type, β:Type, k:Nat, n:Nat.

λ(\begin{matrix}fp : (∀m:Nat.(α, m + k) → (β, m)) × (α × α), \\ n + 2k + 2). \end{matrix}

let f = prj_{1} fp in
let p = prj_{2} fp
in

⟨f[n + k + 1](prj_{1} p), f[n](prj_{2} p)⟩

The function first takes four static arguments, two types and two natural numbers: α and β (the domain and codomain types of f), k (the running time of f), and n (the overall finishing time). After taking static arguments, map pair takes f and p as a pair (curried functions quickly become tedious when writing clock values on each end of every arrow), and specifies the function’s starting time to be n + 2k + 2.

The body typechecks as follows: The starting clock, as specified by the abstraction, is n + 2k + 2. The clock only steps for function calls, so the clock is unchanged by extraction of f and p, by the first instantiation of f, and by the projection from p. The first function call expects a starting clock of (n + k + 1) + k, which it receives once the clock is stepped for the function call. The function call then returns with the clock reading n + k + 1, as given by f’s type. Stepping the clock for the second function call leaves it reading n + k, the expected starting clock for the second function call, which then returns with the clock reading n.

Therefore, map pair is given the type:

∀α:Type, β:Type, k:Nat, n:Nat. ((∀m:Nat.(α, m + k) → (β, m)) × (α × α), n + 2k + 2) → (β × β, n)

Effects systems At alternative formulation that one could consider would use an effects type system [19] to track the passage of time. Such a system would allow for a simpler notation for function types (int →^{3} int) as opposed to ∀n. (int, n + 3) → (int, n)) and would eliminate the effort seen in the previous example in matching up clock readings.

We did not adopt an effects formulation because, although such a formulation would works quite neatly for time, it does not neatly generalize to resources that can be recovered, such as space. For example, if we interpret resources to mean space, the type ∀n. (int, n + 15) → (int, n + 12) specifies a function that allocates as many as 15 units of space but deallocates all but 3 of those, and so must be called with at least 15 units of space. There is no convenient way to specify such a function using a conventional effects system. When resources cannot be recovered, such a type is pointless (one would always prefer the more flexible ∀n. (int, n + 3) → (int, n)), but when they can, such types draw clearly important distinctions. Nevertheless, in this paper we will adopt the effects notation as a convenient shorthand:

Notation 2.1 We write τ_{1} →^{n} τ_{2} to mean ∀m:Nat. (τ_{1}, m + n) → (τ_{2}, m).

For example, map pair’s type may be abbreviated:

∀α:Type, β:Type, k:Nat. ((α →^{k} β) × (α × α)) ⟶^{2k+2} (β × β)

2.1 Variable-time functions

The programming idiom seen so far is pleasantly simple, but it supports only constant-time functions, which renders it insufficient for most real programs. Even when whole programs run in constant time, they still very often contain variable-time subroutines. In order to support real programs, we must permit a function’s running time to depend on its arguments. Since this involves type expressions referring to values, we require some notion of dependent type.

One possible design is simply to add dependent types to the system directly. It is possible that a workable design could be constructed using such an approach (following Xi and Pfenning [21], for example), but we adopted another approach to better leverage the type structure already developed for TAL [3], and in order to keep the type system as simple as possible. In our approach, we take sum and inductive kinds and polymorphism as our primitive constructs, and use them to construct a form of synthetic dependent type. As a result, our programming language is simpler, but the programming idiom is more complex. This is reasonable in keeping with our intention for this language to be primarily machine manipulated; we do however include dependent types in our compiler’s source language, PopCron (Section 4).

Our approach to dependent types is based on a device from Crary and Weirich [3] (hereafter, CW), for the compiler intermediate language LX. CW showed how, using sum and inductive kinds, to construct run-time values that represent static type information. This made it possible to perform intensional type analysis [7] while inspecting only values. Here we use the same device for the opposite purpose, to construct static representations of run-time values. We can then make a function’s running time depend on the static representation of an argument, rather than on the argument itself.

We begin with a representative example to illustrate how this works. Suppose we wish to implement a map tree function. The running time of map tree depends on the size of the tree: If k is the running time of the argument function and t is the tree argument, then map tree’s running time is size(t) · (k + 3) (one call to the mapping function and two recursive calls for each node). Using an ordinary dependent type, we might write map tree’s type as something like:

∀α:Type, β:Type, k:Nat.

(α →^{k} β, t : tree α) \overline{}^{size(t)·(k+3)} tree β

In our idiom, we add an additional static argument (s) that represents the argument t, and we compute the running time based on that static argument:

∀α:Type, β:Type, k:Nat, s:TreeRep.

((α →^{k} β) × tree(s)(α)) ⟶^{cost(s)} tree(s)(β)

We define TreeRep using an inductive kind and cost using primitive recursion over that inductive kind. In this section we will use an informal notation for each of these; we show how the example is formalized in the next section:

    kind TreeRep = Leaf
                 | Node of TreeRep * TreeRep
    fun cost(Leaf) = 0
      | cost(Node (s1, s2)) =
           cost(s1) + cost(s2) + k + 3

The example is simplified by the fact that s needs only to represent the shape of the tree, and not its contents, allowing the same representation to be used for the argument and result trees. If the mapping function were a variable-time function, instead of constant-time k, the TreeRep kind would need to be augmented to supply information about the data items lying at each node. Also note that we have simplified the definition of cost by including the variable k free, rather than as an argument.

The most delicate aspect is the definition of tree(s) as a parameterized recursive type that includes only those trees represented by the argument, s. A simple and naively appealing definition is:

    type wrong tree(s)(α) =
       (case s of
           Leaf => unit + void
         | Node (s1, s2) =>
              void + (α * wrong tree(s1)(α)
                         * wrong tree(s2)(α)))

Unfortunately, this definition makes map tree unimplementable, as s, the argument to tree, will nearly always be abstract. In such cases, wrong tree(s)(α) will be a useless, irreducible type. Instead, following CW, if we implement it as (again using an informal notation):

    type tree(s)(α) =
       (case s of
           Leaf => unit
         | Node (s1, s2) => void) +
       (case s of
           Leaf => void
         | Node (s1, s2) =>
              α * tree(s1)(α) * tree(s2)(α))

Given a member of t of tree(s)(α), we can always case-split t. Suppose t is a left injection, inj_{1} t′. Then we know that s is necessarily Leaf, because if it were Node, then t′ would have type void, which is impossible. LXres permits us to propagate this new information back into the type system and refine s according to whatever we learn. In this manner, static representations can keep up with their dynamic counterparts.

With these definitions, we can implement map tree as shown below. The propagation of information into the type system is conducted by a virtual case construct (described in Section 3), but for the sake of clarity in this informal account, we allow that propagation to be implicit in the example.

fix map tree =

Λα:Type, β:Type, k:Nat, s:TreeRep, n:Nat. λ(ft : (α →^{k} β) × tree(s)(α), n + cost(s)).

let⟨f : α →^{k} β, t : tree(s)(α)⟩ = ft in

                                                           case t of

                                                             inj_{1} t′ ⇒ inj_{1} ∗

inj_{2} t′ ⇒

                                                               letNode(s_{1}, s_{2}) = s in

let⟨x : α, t_{1} : tree(s_{1})(α), t_{2} : tree(s_{2})(α)⟩ = t′ in let x′ = f[n + cost(s_{1}) + cost(s_{2}) + 2](x) in

let t′_{1} = map tree[\begin{matrix}α, β, k, s_{1}, \\ n + cost(s_{2}) + 1]⟨f, t_{1}⟩ in \end{matrix}

let t′_{2} = map tree[α, β, k, s_{2}, n]⟨f, t_{2}⟩

                                                               in

inj_{2}⟨x′, t′_{1}, t′_{2}⟩

The function typechecks as follows: We begin with a function f that runs in k steps, an abstract tree representation s, a tree t matching that representation, and n + cost(s) on the clock. The tree t is a member of a sum type, so we can case analyze it. In the first case, t is inj_{1} t′ and therefore, as argued above, s is Leaf. Consequently, cost(s) = 0 and the clock reads n. The result value (inj_{1} ∗) has type tree(Leaf)(α) and constructing it takes no steps off the clock, so the function’s postcondition is satisfied.

In the second case, t is inj_{2} t′ and therefore, since t′ cannot have type void, we may infer that s is Node(s_{1}, s_{2}) (for some tree representations s_{1} and s_{2}) and that t′ has type α × tree(s_{1})(α) × tree(s_{2})(α). A let expression binds x, t_{1} and t_{2} to the respective components of the node. We then compute the components x′, t′_{1} and t′_{2} of a new node in three steps:

1. With the clock reading n + cost(s) = n + cost(s_{1}) + cost(s_{2}) + k + 3, we instantiate f with the finishing time n + cost(s_{1}) + cost(s_{2}) + 2. Thus f expects a starting time of n + cost(s_{1}) + cost(s_{2}) + 2 + k, which is satisfied once the clock is stepped for the function call.

2. With the clock now reading n+cost(s_{1})+cost(s_{2})+2, we instantiate map tree with a tree representation s_{1} and a finishing time n + cost(s_{2}) + 1. Thus map tree expects a starting time of n + cost(s_{2}) + 1 + cost(s_{1}), which is satisfied once the clock is stepped. The argument, t_{1} has type tree(s_{1})(α), so the function call is well-typed.

3. With the clock now reading n+cost(s_{2})+1, we instantiate map tree with s_{2} and a finishing time of n. The starting time, n + cost(s_{2}), is satisfied and the argument has the appropriate type, so the function call is again well-typed.

The function concludes by assembling these components into a tree node with type tree(Node(s_{1}, s_{2}))(α) and the clock reads n, so the function’s postcondition is satisfied.

2.2 Discussion

The map tree example is typical of the use of our system. First, one identifies one or more metric arguments on which a function’s running time depends. In this example, the running time depends on both the running time of f and the size of t, so both f and t are metric arguments.

Second, one defines representations for the metric arguments that are detailed enough both to compute the cost function and to define enforcement types (such as tree(s)) that contain only values that match the representative. The representation for the f argument was simple; all that needed to be known was its running time k and an enforcement type α →^{k} β was easily defined. The t argument is more complicated (and often more typical). We would be happy to represent it by only its size, but our type system is incapable of constructing an enforcement type for a tree given only its size (more on this below), and so consequently we needed to specify the tree’s entire shape.

Finally, after defining a cost function and an enforcement type, the function itself is written. Two main issues arise in this process:

• The cost must be woven through the function; this is done by correct choices of finishing times for function calls and by wasting extra clock cycles in order to make parallel branches match. (The latter was not necessary in the map tree example.)

• Representations must be supplied for all metric arguments to inner function calls. Constructing such representations requires access to representations of all components from which those arguments are built. When a component is part of one of the function’s own metric arguments, the desired representation is easily obtained from that argument’s representation. (In this map tree example, the needed representations were obtained by decomposing s into Node(s_{1}, s_{2}) once it was determined that t was a node.) When a component is the result of another function call, that function’s type must specify the representation of that return value. For example, map tree specified that its result had the same specification as its argument. More generally, the result could have a different specification given by a static function. For example, if map tree also possibly restructured the tree, it would need to have the type

∀α:Type, β:Type, k:Nat, s:TreeRep.

((α →^{k} β) × tree(s)(α))

⟶^{cost(s)} tree(newrep(s))(β)

where newrep is a static function with kind TreeRep → TreeRep. Such functions with specified results are more limited in what they can do than ordinary functions, because static functions are required to be primitive recursive and therefore the specified functions must be primitive recursive, at least as far as the structure described by the representations are concerned. This requirement, which we discuss further in the next section, is necessary to ensure decidability of type checking. In some cases, an argument may be a metric argument to an inner function call even when it does not affect the total running time of the outer function. For example, suppose a function broke a fixed-length array into two variable-sized pieces based on an integer argument, and then mapped a constant-time function over each piece. The total running time does not depend on the integer argument, but each internal call’s time does. In such cases, the “phantom” dependency must be treated as a metric argument and a representation must be required. A similar issue arises when an inner function’s result is a metric argument to another inner function, but that result does not affect the total remaining running time of the outer function. In this case, a representation must again be obtained, but since there is no need to link this representation back to the total cost, it can be existentially quantified rather than specified by a static function. This case is more typical than the case of functions that require specified results.

Returning to the topic of enforcement types, the aspect of trees that makes it impossible to define an enforcement type for them given only a size is that trees have multiple spines. That is, given a total size, the enforcement type does not know how much size to place in the left subtree and how much to place in the right. Therefore, the representation must also specify how much to place in each subtree, and by doing so inductively it specifies the tree’s entire shape. Multiple-spined data structures are quite common, so it is common to require representations of entire data structures. Consequently, our prototype compiler makes no effort to optimize representations, instead providing (nearly) full representations for all metric arguments (other than functions). However, it is important to emphasize that the static representations are not constructed at run time, so the cost of over-representing a metric argument is paid at verification time only.

An alternative strategy that could permit much more succinct representations at the cost of a more complicated type system would be to use union types to enumerate the possible divisions of the total size. We have not explored the ramifications of such a design, but it seems likely that it would complicate typechecking.

3 A Language for Resource Bound Certification

In this section we discuss LXres and its semantics. We present the constructor and term levels individually, concentrating discussion on the novel features of each. The syntax of LXres (shown in Figures 1 and 2) is based on Girard’s F_{ω} [6, 5] augmented mainly by a rich programming language at the constructor level, constructor refinement operators at the term level, and resource bounds in types and terms. LXres is very similar to CW’s LX, the difference being that LXres includes virtual clocks and a primitive natural number kind in support of those clocks. The full static and operational semantics of LXres are given in Appendices A and B.

(kinds)  k ::= Type | Nat | 1 | k_{1} → k_{2} | k_{1} × k_{2} | k_{1} + k_{2} | j | μj.k
(constructors) c, τ ::= ∗ | α | λα:k.c | c_{1}c_{2}  unit, variables and functions
| ⟨c_{1}, c_{2}⟩ | prj_{1} c | prj_{2} c  products
| inj_{1}^{k_{1}+k_{2}} c | inj_{2}^{k_{1}+k_{2}} c | case(c, α_{1}.c_{1}, α_{2}.c_{2})  sums
| fold_{μj.k} c | pr(j, α:k, β:j →k′.c)  primitive recursion
| \overline{n} | c_{1} ∔ c_{2} | prnat(α, β:k.c_{1}; c_{2})  natural numbers
| (τ_{1}, c_{1}) → (τ_{2}, c_{2}) | τ_{1} × τ_{2} | τ_{1} + τ_{2}  types
| ∀α:k.τ | ∃α:k.τ | unit | void | rec_{k}(c_{1}, c_{2})  types

Figure 1: LXres kinds and constructors

3.1 Kinds and constructors

The constructor and kind levels, shown in Figure 1, contain both base constructors of kind Type (called types) for classifying terms, and a variety of programming constructs for computing types. In addition to the variables and lambda abstractions of F_{ω}, LXres also includes a unit kind, products, sums, and the usual introduction and elimination constructs for those kinds. LXres also includes a natural number kind discussed further in Section 3.3.

We denote the simultaneous, capture-avoiding substitution of E_{1}, …, E_{n} for X_{1}, …, X_{n} in E by E[E_{1}, …, E_{n}/X_{1}, …, X_{n}]. As usual, we consider alphaequivalent expressions to be identical. A few constructs (inj_{i}, fold, pr, and rec) are labeled with kinds to assist in kind checking; we will omit such kinds when they are clear from context. When a constructor is intended to have kind Type, we often use the metavariable τ.

To support computing with static representations, LXres includes kind variables (j) and inductive kinds (μj.k). A prospective inductive kind μj.k will be well-formed provided that j appears only positively within k. Inductive kinds are formed using the introductory operator fold_{μj.k}, which coerces constructors from kind k[μj.k/j] to kind μj.k. For example, consider the kind Tlist of lists of types, defined as μj.(1+Type×j). The constructor (inj_{1}^{1+Type×Tlist} ∗) has kind (1+Type×j)[Tlist/j]. Therefore fold_{Tlist}(inj_{1}^{1+Type×Tlist} ∗) has kind Tlist.

Inductive kinds are eliminated using the primitive recursion operator pr. Intuitively, pr(j, α:k, φ:j → k′.c) may be thought of as a recursive function with domain μj.k in which α stands for the argument unfolded and φ recursively stands for the full function. However, in order to ensure that constructor expressions always terminate, we restrict pr to define only primitive recursive functions. Informally speaking, a function is primitive recursive if it can only call itself recursively on a subcomponent of its argument. Following Mendler [12], we ensure this using abstract kind variables. Since α stands for the argument unfolded, we could consider it to have the kind k[μj.k/j], but instead of substituting for j in k, we hold j abstract. Then the recursive variable φ is given kind j → k′ (instead of j[μj.k/j] → k′) thereby ensuring that φ is called only on a subcomponent of α.

The kind k′ in pr(j, α:k, φ:j →k′.c) is permitted to contain (positive) free occurrences of j. In that case, the function’s result kind employs the substitution for j that was internally eschewed. Hence, the result kind of the above constructor is k′[μj.k/j]. This is useful so that some part of the argument may be passed through without φ operating on it. As a particularly useful application, we can define the constructor unfold_{μj.k} with kind μj.k → k[μj.k/j] to be pr(j, α:k, φ:j →k.α).

For example, given a constructor with kind Tlist, we can use primitive recursion to construct the tuple type built from the types in the list (using an informal, expanded notation for case):

tuple =^{def} pr(j, α:1+Type×j, φ:j →Type.

                                                                          case α of
                                                                            inj_{1} β ⇒ unit

inj_{2} γ ⇒ prj_{1} γ × φ(prj_{2} γ))

Suppose we apply tuple to the list [int] (that is, the encoding fold(inj_{2}⟨int, fold(inj_{1} ∗)⟩). By unrolling the pr expression, we may show:

(pr(j, α:1+Type×j, φ:j →Type.

                                                                case α of

                                                                  inj_{1} β ⇒ unit
                                                                  inj_{2} γ ⇒ prj_{1} γ × φ(prj_{2} γ))) [int]

                                                              = case (inj_{2}⟨int, fold(inj_{1} ∗)⟩) of

                                                                  inj_{1} β ⇒ unit

inj_{2} γ ⇒ prj_{1} γ × tuple(prj_{2} γ)

= int × (tuple(fold(inj_{1} ∗))) (that is, int × tuple([]))

                                                              = int × (case (inj_{1} ∗) of inj_{1} β ⇒ unit inj_{2} γ ⇒ prj_{1} γ × tuple(prj_{2} γ))

                                                              = int × unit

The unrolling process is formalized by the following constructor equivalence rule (the relevant judgment forms are summarized in Figure 5):

Δ ⊢ c′ : k[μj.k/j]  Δ, j ⊢ k′ kind
Δ, j, α:k, φ:j →k′ ⊢ c : k′ Δ ⊢ μj.k kind

Δ ⊢ pr(j, α:k, φ:j → k′.c)(fold_{μj.k} c′) = \begin{matrix}c[μj.k, c′, pr(j, α:k, φ:j →k′.c)/j, α, φ] \\ : k′[μj.k/j] \end{matrix}

(j only positive in k′ and j, α, φ ∉ Δ)

Notation 3.1 If k_{1} is of the form μj.k, then we write k_{1}[k_{2}] to mean k[k_{2}/j]. For example, Tlist[Tlist] abbreviates 1 + Type × Tlist.

3.2 Types and terms

The syntax of LXres terms is given in Figure 2. Most LXres terms are standard, including the usual introduction and

(terms) e ::= ∗ | x | λ(x:τ, c).e | e_{1}e_{2}  unit, variables, functions
| waste[c]e  clock advance
| ⟨e_{1}, e_{2}⟩ | prj_{1} e | prj_{2} e  products
| inj_{1}^{τ_{1}+τ_{2}} e | inj_{2}^{τ_{1}+τ_{2}} e | case(e, x_{1}.e_{1}, x_{2}.e_{2})  sums
| Λα:k.v | e[c] | fix f:τ.v  constructor abstractions and recursion
| pack e as ∃α:k.τ hiding c | unpack ⟨α, x⟩ = e_{1} in e_{2}  existential packages
| fold_{rec_{k}(c,c′)} e | unfold e  parameterized recursive types
| vcase_{τ▷c}(c, β. e, γ. dead v) | vcase_{τ▷c}(c, β. dead v, γ. e) constructor refinement operations
| let_{τ▷c} ⟨β, γ⟩ = c in e | let_{τ▷c} (fold β) = c in e  constructor refinement operations

Figure 2: LXres terms

Δ ⊢ τ_{1} : Type Δ ⊢ c_{1} : Nat Δ ⊢ τ_{2} : Type Δ ⊢ c_{2} : Nat

Δ ⊢ (τ_{1}, c_{1}) → (τ_{2}, c_{2}) : Type

Δ ⊢ τ_{1} : Type Δ ⊢ c_{1} : Nat Δ; (Γ, x:τ_{1}); c_{1} ⊢ e : τ_{2} ▷ c_{2}

\begin{matrix}Δ; Γ; c ⊢ λ(x:τ_{1}, c_{1}).e : (τ_{1}, c_{1}) → (τ_{2}, c_{2}) ▷ c \\ (x ∉ Γ) \end{matrix}

\begin{matrix}Δ; Γ; c ⊢ e_{1} : (τ_{1}, c_{1}) → (τ_{2}, c_{2}) ▷ c′ \\ Δ; Γ; c′ ⊢ e_{2} : τ_{1} ▷ (c_{1} ∔ 1) \end{matrix} ; Δ; Γ; c ⊢ e_{1}e_{2} : τ_{2} ▷ c_{2}

Δ; Γ; c ⊢ e : τ ▷ (c_{1} ∔ c_{2}) Δ; Γ; c ⊢ waste[c_{1}]e : τ ▷ c_{2}

Figure 3: Virtual clock rules

elimination forms for products, sums, unit, and universal and existential types.

Function types and lambda abstractions are written with virtual clock specifications, as discussed in Section 2. A few representative rules governing virtual clocks appear in Figure 3, in which the typing judgment Δ; Γ; c ⊢ e : τ ▷ c′ states that (in constructor context Δ and value context Γ) the term e has type τ, and given a clock reading c it finishes evaluating with the clock reading c′.

Constructor abstractions are limited by a value restriction to avoid unsoundness in the presence of effects. The value forms are given in Appendix B. Recursive functions are expressible using fix terms, the bodies of which are syntactically restricted to be functions (usually polymorphic) by their typing rule (Appendix A). As at the constructor level, some constructs are labeled with types or clocks to assist in type checking; we omit these when clear from context.

Parameterized recursive types are written rec_{k}(c_{1}, c_{2}), where k is the parameter kind and c_{1} is a type constructor with kind (k → Type) → (k → Type). Intuitively, c_{1} recursively defines a type constructor with kind k → Type, which is then instantiated with the parameter c_{2} (having kind k). Thus, members of rec_{k}(c_{1}, c_{2}) unfold into the type c_{1}(λα:k. rec_{k}(c_{1}, α))c_{2}, and fold the opposite way. The special case of non-parameterized recursive types are defined as rec(α.τ) = rec_{1}(λφ:1 → Type. λβ:1. τ[φ(∗)/α], ∗). Unlike inductive kinds, no positivity condition is imposed on recursive types.

Refinement The most novel features of the LXres term language are the constructor refinement operations. The main refinement operations are the two virtual case constructs, written vcase(c, β. e, γ. dead v) and dually. These operations may been thought of as branching operations for sum kinds: if c normalizes to inj_{1}(c′), then the term vcase(c, β. e, γ. dead v) evaluates to e[c′/β].

However, constructors are static components of the program only, and therefore may not be relied upon at run time. Consequently, the semantics of vcase(c, β. e, γ. dead v) dictates that it always reduces to the first branch, and the second branch is dead code. To avoid unsoundness, the typing rule for vcase requires that its dead branch be a value with type void, and thus that branch is statically known to be dead code. Somewhat surprisingly, it may be shown [3] that this virtual case construct provides the same expressive power as an unrestricted case construct would.

In the left branch of a virtual case, the constructor being branched on is determined to be a left injection, and conversely in the right branch. When that constructor is a variable, the vcase typing rule propagates this information back into the type system by substituting for that variable:

Δ, β:k_{1}, Δ′; Γ[inj_{1} β/α]; c_{1}[inj_{1} β/α] ⊢

e[inj_{1} β/α] : τ[inj_{1} β/α] ▷ c_{2}[inj_{1} β/α]

Δ, γ:k_{2}, Δ′; Γ[inj_{2} γ/α]; c_{1}[inj_{2} γ/α] ⊢

v[inj_{2} γ/α] : void ▷ c′_{2}

Δ, α:k_{1}+k_{2}, Δ′ ⊢ c = α : k_{1} + k_{2}

Δ, α:k_{1}+k_{2}, Δ′; Γ; c_{1} ⊢ vcase_{τ▷c_{2}}(c, β. e, γ. dead v) : τ ▷ c_{2} (β, γ ∉ Δ)

Within the branches, types that depend on α can be reduced using the new information. For example, if x has type case(α, β.int, β.void), its type can be reduced in each branch, allowing its use as an integer in the active branch and as void value in the dead branch.

In order for LXres to enjoy the subject reduction property, we also require a trivialization rule [4] for vcase, for use when the argument is a sum introduction:

Δ ⊢ c = inj_{1} c′ : k_{1} + k_{2} Δ; Γ; c_{1} ⊢ e[c′/β] : τ ▷ c_{2}
Δ; Γ; c_{1} ⊢ vcase_{τ▷c_{2}}(c, β. e, γ. dead v) : τ ▷ c_{2}

Path refinement There may also be useful refinement to perform when the constructor to be branched on is not a variable. For example, suppose α has kind (1+1)×Type and

TreeRep = μj.(1 + j×j)
cost = pr(\begin{matrix}j, α:TreeRep[j], φ:j → Nat. \\ case α of \\ inj_{1} β ⇒ \overline{0} \\ inj_{2} β ⇒ \\ φ(prj_{1} β) ∔ φ(prj_{2} β) ∔ k ∔ \overline{3}) \end{matrix}

tree(s)(α) =

rec_{TreeRep}(\begin{matrix}λφ:TreeRep → Type. λβ:TreeRep. \\ (caseunfold β of \\ inj_{1} γ ⇒ ∗ \\ inj_{2} γ ⇒ void) + \\ (caseunfold β of \\ inj_{1} γ ⇒ void \\ inj_{2} γ ⇒ \\ α × φ(prj_{1} γ)(α) × φ(prj_{2} γ)(α)), \\ s) \end{matrix}

map tree = fix map tree :

(∀α:Type, β:Type, k:Nat, s:TreeRep.

((α →^{k} β) × tree(s)(α)) ⟶^{cost(s)} tree(s)(β)) .

Λα:Type, β:Type, k:Nat, s:TreeRep, n:Nat. λ(ft : (α →^{k} β) × tree(s)(α), n ∔ cost(s)).

let⟨f : α →^{k} β, t : tree(s)(α)⟩ = ft in

case unfold t of

inj_{1} t′ ⇒

 letfold(s′) = s in
 vcase s′ of

inj_{1} s′′ ⇒ inj_{1} ∗

   inj_{2} s′′ ⇒ dead t′

inj_{2} t′ ⇒

 letfold(s′) = s in
 vcase s′ of
   inj_{1} s′′ ⇒ dead t′

inj_{2} s′′ ⇒ let⟨s_{1}, s_{2}⟩ = s′′ in let⟨x : α, t_{1} : tree(s_{1})(α), t_{2} : tree(s_{2})(α)⟩ = t′ in let x′ = f[n ∔ cost(s_{1}) ∔ cost(s_{2}) ∔ \overline{2}](x) in

let t′_{1} = map tree[\begin{matrix}α, β, k, s_{1}, \\ n ∔ cost(s_{2}) ∔ \overline{1}]⟨f, t_{1}⟩ in \end{matrix}

let t′_{2} = map tree[α, β, k, s_{2}, n]⟨f, t_{2}⟩

     in

inj_{2}⟨x′, t′_{1}, t′_{2}⟩

Figure 4: Formalized map tree example

x has type case(prj_{1} α, β.int, β.void). When branching on prj_{1} α, we should again be able to consider x an integer or a void-value, but the ordinary vcase rule above no longer applies since prj_{1} α is not a variable. This is solved using the product refinement operation, let_{τ▷c} ⟨β, γ⟩ = α in e. Like vcase, the product refinement operation substitutes everywhere for α:

Δ, β:k_{1}, γ:k_{2}, Δ′; Γ[⟨β, γ⟩/α] ▷ c_{1}[⟨β, γ⟩/α] ⊢

e[⟨β, γ⟩/α] : τ[⟨β, γ⟩/α] ▷ c_{2}[⟨β, γ⟩/α]

Δ, α:k_{1} × k_{2}, Δ′ ⊢ c = α : k_{1} × k_{2}

Δ, α:k_{1} × k_{2}, Δ′; Γ; c_{1} ⊢ let_{τ▷c_{2}}⟨β, γ⟩ = c in e : τ ▷ c_{2} (β, γ ∉ Δ)

A similar refinement operation exists for inductive types, and each operation also has a trivialization rule similar to those of vcase.

We may use these refinement operations to turn paths into variables and thereby take advantage of vcase. For example, suppose α has kind Tlist × Tlist and we wish to branch on unfold (prj_{1} α). We do it using product and inductive kind refinement in turn:

let ⟨β_{1}, β_{2}⟩ = α in

let (fold γ) = β_{1} in

vcase(γ, δ. e, δ. dead v)

A formalized version of the map tree example using path refinement appears in Figure 4. For clarity, the example uses a let notation on terms as the informal version in Section 2 did.

Non-path refinement Since there is no refinement operation for functions, sometimes a constructor cannot be reduced to a path. Nevertheless, it is still possible to gain some of the benefits of refinement, using a device due to Harper and Morrisett [7]. Suppose φ has kind Nat → (1+1), x has type case(φ(4), β.int, β.void), and we wish to branch on φ(4) to learn the type of x. First we use a constructor abstraction to assign a variable α to φ(4), thereby enabling vcase, and then we use a lambda abstraction to rebind x with type case(α, β.int, β.void):

(Λα:1+1. λx: case(α, β.int, β.void).
vcase(α, β.e, β. dead v)) [φ(4)] x

Within e, x will be an integer, and similarly within v. This device has all the expressive power of refinement, but is less efficient because of the need for extra beta-expansions. However, this is the best that can be done with unknown functions.

3.3 Natural numbers

LXres includes a primitive natural number kind, even though natural numbers could be defined as the inductive kind μj.(1+j) and addition could be defined using primitive recursion. This is because the inductive kind definition does not provide commutativity and associativity axioms, which are frequently necessary to prove adherence to resource bounds. The problem derives from the absence of an eta-equivalence rule on inductive kinds. For example, the

\underline{Judgment}  \underline{Meaning}
Δ ⊢ k kind  k is a well-formed kind
Δ ⊢ c : k  c is a valid constructor of kind k
Δ ⊢ c_{1} = c_{2} : k  c_{1} and c_{2} are equal constructors
Δ; Γ; c_{1} ⊢ e : τ ▷ c_{2} e is a term of type τ, and, when

starting with clock c_{1}, evaluation of e finishes with clock c_{2}

\underline{Contexts}

\begin{aligned}Δ & ::= & ϵ | Δ, j | Δ, α:k \\ Γ & ::= & ϵ | Γ, x:τ \end{aligned}

Figure 5: Judgments

analog of α + 0 = 0 + α does not hold,

α ≠ pr(\begin{matrix}j, β:1+j, φ:j → μj.(1+j). \\ case β of \\ inj_{1} γ ⇒ fold(inj_{1} γ) \\ inj_{2} γ ⇒ fold(inj_{2} φ(γ)))) α \end{matrix}

because the right-hand side is irreducible, even though the equivalence does hold for all closed instances.

By making natural numbers primitive, we can easily add commutativity and associativity axioms. Addition of natural numbers is written c_{1} ∔ c_{2} to distinguish it from a sum type. Numerals in LXres are written \overline{n} to distinguish them from numbers in the metatheory, but we will often omit the overbar when there is no possibility of confusion.

Natural numbers are eliminated by primitive recursion. The constructor prnat_{k}(α, β.c_{1}; c_{2}) is a function with kind Nat → k. On zero it returns c_{2}, and on n ∔ 1 it returns the body c_{1}, in which α stands for n and β stands for the recursively computed value:

Δ, α:Nat, β:k ⊢ c_{1} : k Δ ⊢ c_{2} : k Δ ⊢ c : Nat

Δ ⊢ prnat_{k}(α, β.c_{1}; c_{2})(c ∔ 1) = c_{1}[c, prnat_{k}(α, β.c_{1}; c_{2})(c)/α, β] : k (α, β ∉ Δ)

The implemented version of this type system, TALres, also provides a variety of other primitive operations (e.g., minimum, proper subtraction, and multiplication) and appropriate axioms for those operations.

3.4 Properties of LXres

The judgments of the static semantics of LXres appear in Figure 5. The important properties to show are decidable type checking and type safety. Due to space considerations, we do not present proofs of these properties here; the proofs are nearly identical to those for LX [3]. For typechecking, the challenging part is deciding equality of type constructors. We do this using a normalize, sort, and compare algorithm employing a reduction relation extracted from the equality rules. The reduction relation is constructed in the obvious manner except for commutativity and associativity, where it simply moves natural number literals outward. A second phase of the algorithm sorts addition expressions to account for full commutativity and associativity.

Lemma 3.2 Reduction of well-formed constructors is strongly normalizing, confluent, preserves kinds, and is respected by equality.

Strong normalization is proven using Mendler’s variation on Girard’s method [12]. Given Lemma 3.2, it is easy to show the normalize, sort, and compare algorithm to be terminating, sound and complete, and decidability of type checking follows in a straightforward manner.

Theorem 3.3 (Decidability) It is decidable whether or not Δ; Γ; c ⊢ e : τ ▷ c′ is derivable in LXres.

We say that a term (together with a clock) is stuck if it is not a value and if no rule of the operational semantics applies to it. Type safety requires that no well-typed term can become stuck:

Theorem 3.4 (Type Safety) If ϵ; ϵ; \overline{n} ⊢ e : τ ▷ c and (e, n) ↦^{∗} (e′, n′) then (e′, n′) is not stuck.

This is shown using the usual subject reduction and progress lemmas, augmented to track clocks.

No rule in the operational semantics will allow a program to perform a function call when its clock reads 0, so any program attempting to exceed its time bounds would become stuck. It therefore follows from type safety that a well-typed program cannot exceed its time bound:

Corollary 3.5 (Adherence to Resource Bounds) If ϵ; ϵ; \overline{n} ⊢ e : τ ▷ c then e executes in at most n clock steps.

4 Implementation

We have implemented this work within the framework of the Typed Assembly Language (TAL) security architecture [14, 13]. Our typechecker implements TALres, a variant of TALx86 [13] augmented to include the key features of LXres. An example of TALres code appears in Figure 8.

The features of TAL and LXres interact pleasantly: LXres’s virtual clocks may conveniently be considered registers, so LXres’s clock-tracking mechanism is easily incorporated into TAL’s existing register file mechanism. The kind and constructor languages of TAL are easily augmented to incorporate those of LXres, and the constructor refinement operations are accounted for in TAL by new pseudoinstructions similar to TAL’s unpack instruction.

TALres also supports a few features in addition to those of LXres. One often requires an enforcement type linking a run-time number to a static natural number. Such an enforcement type can easily be built when numbers are represented by Church numerals, but we wish to avoid the inefficiency of Church numerals and use the built-in integers of TAL. TAL includes a singleton integer type to support the compilation of tagged unions; with the addition of constructor-refining variants of the basic arithmetic operations, TALres allows this type to serve as an enforcement type. TALres also provides primitive natural number operations other than addition, in support of richer cost functions. In all, none of the enhancements to TAL to account for resource bounds have substantially enlarged its trusted computing base.

Outside the trusted computing base, we implemented a prototype compiler generating TALres. Our compiler takes source programs written in PopCron (which includes cost function annotations) and compiles them to TALres, thereby certifying them for safety and for resource bounds. The PopCron language resembles Popcorn [13], which in turn is a safe dialect of C. At the level of a C source program it is difficult to predict the exact number of instructions the resulting executable will use, but the number of jumps is more stable, and for this reason we measure running time in terms of backward jumps. (More precisely, we charge a jump when it cannot be determined to be forward.) The discrepancy between function calls in the source and chargeable jumps in the executable (typically two jumps per function call) is easily compensated for by the compiler.

Each function in PopCron must be annotated with a running time expression given in terms of zero or more of the function’s arguments using a dependent type notation. For example, the notation <|0|> in the following definition of an increment function specifies that this code makes no function calls.

int add1 (int x)<|0|> { return x+1; }

The compiler automatically adds representation arguments, threads the cost through the function, and provides representations for function calls. The PopCron language does not currently provide a facility for a function type to specify the representation of its result (recall Section 2.2), but we plan to add such a facility in the future.

Continuing the trivial example, the generated TALres code for the function add1 is :

_add1:
LABELTYPE <All[k:Sint s:Ts].{CLK: 1 + k,
  ESP:sptr {CLK:k, EAX:B4, ESP:sptr B4::s}::B4::s}>
        MOV     EAX,[ESP+4]
        INC     EAX
        RETN

The type of this label is a precondition for jumping to it. The precondition says that the stack (contained in register ESP) must contain the pointer to a return address, followed by a four byte value (type B4), followed by the rest of the stack, s, which is held abstract. Furthermore, the clock time, in register CLK, is also abstract, though it must be at least 1. This extra clock step is added by the compiler to account for the function’s return.

Example Space considerations preclude a thorough discussion of PopCron and the compiler, so we illustrate them by example. Figure 6 contains an example of a more substantial source program written in PopCron. This program first defines the tree type (specialized in this case to integers), using recursive unions and structs. Note that the left and right branches of each tree node are immutable; the PopCron type system does not permit any mutable data to contribute to a cost function. The bulk of this example is the function app tree that applies its argument function f to every value in the tree.^{1} The type given for f specifies that, like add1, it may make no function calls. This is just for simplicity, like TALres, PopCron does allow functions to be polymorphic over the time taken by a parameter function.

The time annotation for app tree refers to cost tree in calculating the time taken for the tree t. The keyword time indicates that cost tree is only used in timing annotations, and, as it will never be executed, does not need its own time annotation.

The compiler’s TALres output appears in Figures 7 and 8. The only changes to this code for presentation are

                                                               struct tree_node {
                                                                 const tree left;
                                                                 const tree right;
                                                                 int val;
                                                               }
                                                               union tree {
                                                                 void leaf;
                                                                 tree_node node;
                                                               }
                                                               time cost_tree (tree t) {
                                                                 switch t {
                                                                 case leaf : return 0;
                                                                 case node(n): return (cost_tree_node(n));
                                                                 }
                                                               }
                                                               time cost_tree_node (tree_node n) {
                                                                 return (cost_tree (n.left) +
                                                                         cost_tree (n.right) + 3);
                                                               }
                                                               void app_tree (tree t, void f (int x)<|0|>)
                                                                 <| cost_tree(t) |> {
                                                                   switch t {
                                                                   case leaf : return;
                                                                   case node(n) :
                                                                     f(n.val);
                                                                     app_tree(n.left,f);
                                                                     app_tree(n.right,f);
                                                                     return;
                                                                 }
                                                               }

Figure 6: Example of PopCron code

some constructor simplification (in some cases they have been replaced with equivalent, but smaller versions) and formatting. For example, we define two common types at the bottom of Figure 8: ftype is the type of the function argument to app tree, and ra is the type of the return address of the function.

Figure 7 contains the definitions of the TALres kinds constructors and types necessary to annotate the compiled code of app tree. The first two lines of this figure define the mutually recursive kinds representing the tree union and tree node struct.^{2} The next four lines define unfold for these recursive kinds, where RECCON and ANDCON provide a mutually recursive version of LXres’s pr. The two time functions, cost tree and cost tree node, are also defined with these constructs.

Lines 13 through 22 define the parameterized recursive types of trees and tree nodes,^{3} where rec creates a tuple of mutually recursive types, and then the individual components are projected out in lines 21 and 22. Like tree(s)(α), in Figure 4, tree rep forms a tagged sum (the branches are discriminated by the singleton types S(1) and S(2)), and within each branch of the sum, a case constructor allows the argument to be refined with a virtual case.

1PopCron follows the terminology of C by using void to refer to the trivial type; however, TALres follows standard type-theoretic terminology in which void refers to the empty type.

2Both sums and products in TALres may contain an arbitrary number of fields. Sums are denoted by +[ object, ... ], products by *[ object, ... ], and unit is the empty product *[] .

3Product values must be boxed (unless they lie within an outer boxed object), and consequently product types are often indicated to be boxed by a ^prefix. Additionally, product types contain flags indicating that a field is read-only (^r) or read-write (^rw) [13].

For example, a boxed pair of mutable integers would have type ^*[B4^rw,B4^rw]. For brevity, when each field of a sum is boxed, the boxing prefix may be placed on the entire sum.

1        RECKIND <tree_k = +[*[],tree_node_k]>
2        ANDKIND <tree_node_k = *[tree_k,tree_k]>
3        RECCON  <unfold_tree : tree_k -!> +[*[],tree_node_k] =                          \
4                  fn a$15 : +[*[],tree_node_k] . a$15>
5        ANDCON  <unfold_tree_node : tree_node_k -!> *[tree_k,tree_k] =                  \
6                  fn a$13 : *[tree_k,tree_k] . a$13>
7
8        RECCON  <cost_tree : tree_k -!> Nat =                                           \
9                  fn t : +[*[],tree_node_k] . case (t) beta [0,cost_tree_node beta]>
10       ANDCON  <cost_tree_node : tree_node_k -!> Nat =                                 \
11                 fn n : *[tree_k,tree_k] . 3 + (cost_tree n.0)+ (cost_tree n.1)>
12
13       TYPE    <_reptype = rec(
14                 tree_rep:tree_k-!>T4. fn union$16:tree_k .                            \
15                       ^+[*[S(1)^r,case (unfold_tree union$16) b$17 [B4,void[T4]]^r],  \
16                          *[S(2)^r,case (unfold_tree union$16) b$18 [void[T4],         \
17                                      tree_node_rep b$18]^r]],                         \
18                 tree_node_rep:tree_node_k-!>T4. fn struct$14:tree_node_k .            \
19                         ^*[(tree_rep (unfold_tree_node struct$14).0)^r,               \
20                            (tree_rep (unfold_tree_node struct$14).1)^r,B4^rw])>
21       TYPE    <tree_rep      = _reptype.0>
22       TYPE    <tree_node_rep = _reptype.1>

Figure 7: TALres kind and constructor definitions

Figure 8 contains the TALres output of the compiler for app tree. Like add1, the precondition of this label expects that the return address and then the arguments (first the tree, then the function) will be passed to it on the stack. Furthermore, the time annotation of app tree has been compiled to the constructor in the CLK register. As function calls are composed of two jumps, the PopCron time annotation is doubled, and an extra step is added for the final jump at the function return.

The first step of the code is to explicitly unroll the recursive type, and then branch on the sum tag, using TAL’s pseudo-instruction BTAGVAR. If the tag is equal^{4} to 1, the code jumps to label leaf void$21, otherwise it falls through. At leaf void$21, as BTAGVAR has removed all but one branch, EAX contains a pointer to the degenerate sum

^+[*[S(1)^r,case (unfold_tree t)
b$17 [B4,void[T4]]^r]]

so it is explicitly coerced to remove the sum wrapping. Next, t is refined in the next two lines. The VCASE instruction^{5} examines the type of second component of the product, verifying that it would be void if the argument to the case were (fold (inj 1 beta)). After refinement, t has been replaced by (fold (inj 0 beta)) so the clock reads

1 + (cost_tree (fold (inj 0 beta)))
+ (cost_tree (fold (inj 0 beta))) + k

which normalizes to 1+k. After the clock is stepped for the jump, this gives the time expected by the return address.

In the other branch, node value$22 also coerces the EAX from a degenerate sum so that its type becomes

^*[S(2)^r,case (unfold_tree t) b$18
[void[T4], tree_node_rep b$18]^r]

After refinement (Lines 8 and 9), this type is equivalent to

^*[S(2)^r, (tree_node_rep n)^r], for a new variable n.

In lines 10 and 11, the second component of this tuple is pushed onto the stack and also put into EAX. After more refinement in lines 12 and 13, EAX is of type tree node rep

[left3,right4], for new variables left3 and right4. This

recursive type is explicitly unrolled so that the third component can be extracted and placed on the stack in line 15. The argument f is then fetched from the stack and called in line 17. Before the call, the clock reads (through the refinements):

7 + cost_tree(left3) + cost_tree(left3)
  + cost_tree(right4) + cost_tree(right4) + k

As the call to f takes one step, and f takes one step to return, we expect that after the call the clock should read

5 + cost_tree(left3) + cost_tree(left3)
  + cost_tree(right4) + cost_tree(right4) + k

and so pass this constructor argument to f. The second constructor argument is the current state of the stack minus the argument to f.

On return from f we pop the argument off the stack (line 21), move the pointer for f up the stack to prepare for the recursive call (22), and then extract the left child of the tree (23–24). The call (25) requires the type application of the time after the call, the constructor representing the left child, and the stack. Lines 29–34 perform a similar call with the right child. At Line 36, the clock reads 1+k, allowing the return.

5 Conclusion

Adherence to resource bounds is an important safety property for untrusted agents in real-world situations. Our type system certifies programs by augmenting them with virtual clocks, and proving that the clocks of well-typed programs cannot expire. This mechanism was first suggested by Necula and Lee [17] for the PCC framework. This work extends theirs by allowing executions to vary in length depending on their input, and by providing a fully automatic compiler generating executables certified for resource bounds.

4The “E” in the BTAGVAR instruction indicates a test for equality.

5The VCASE instruction takes four arguments: the number of the live branch, a new constructor variable to bind, the constructor being case analyzed, and the value residing in the dead branch.

1       _app_tree:
2       LABELTYPE <All[k:Nat t:tree_k s:Ts].{CLK: 1+(cost_tree t)+(cost_tree t)+k,       \
3         ESP: sptr ra :: (tree_rep t) :: ftype :: s}>
4               MOV     EAX,unroll([ESP+4])
5               BTAGVAR E,[EAX+0],1,leaf_void$21
6       node_value$22:
7               COERCE  unisum(EAX)
8               LETFOLD alpha1,t
9               VCASE   1,n,alpha1,[EAX+4]
10              PUSH    DWORD PTR [EAX+4]
11              MOV     EAX,[ESP+0]
12              LETFOLD r$24,n
13              LETPROD [left3,right4],r$24
14              COERCE  unroll(EAX)
15              PUSH    DWORD PTR [EAX+8]
16              MOV     EAX,[ESP+16]
17              CALL    tapp(EAX,<5 + (cost_tree left3) + (cost_tree right4) +           \
18                                  + (cost_tree left3) + (cost_tree right4) + k,        \
19                                tree_node_rep [left3,right4] :: ra                     \
20                                  :: (tree_rep t) :: ftype :: s >)
21              ADD     ESP,4
22              PUSH    DWORD PTR [ESP+12]
23              MOV     EAX,unroll([ESP+4])
24              PUSH    DWORD PTR [EAX+0]
25              CALL    tapp(_app_tree,<3 + (cost_tree right4) + (cost_tree right4) + k, \
26                                 left3, tree_node_rep [left3,right4] :: ra             \
27                                   :: (tree_rep t) :: ftype :: s >)
28              ADD     ESP,8
29              PUSH    DWORD PTR [ESP+12]
30              MOV     EAX,unroll([ESP+4])
31              PUSH    DWORD PTR [EAX+4]
32              CALL    tapp(_app_tree,<1 + k,  right4,                                  \
33                                 tree_node_rep [left3,right4] :: ra                    \
34                                   :: (tree_rep t) :: ftype :: s>)
35              ADD     ESP,12
36              RETN
37      leaf_void$21:
38              COERCE  unisum(EAX)
39              LETFOLD alpha1,t
40              VCASE   0,beta2,alpha1,[EAX+4]
41              RETN
where ftype =  All[k:Nat s:Ts].{CLK: 1+k, ESP: sptr { CLK: k, ESP: sptr B4::s} :: B4 :: s}
and   ra    =  { CLK: k, ESP: sptr (tree_rep t) :: ftype :: s }

Figure 8: Compilation of the function app tree

Like Necula and Lee, we make no effort to infer resource bounds, and instead rely on annotations supplied by the programmer.

Some other type systems for controlling resource consumption are Hoffman’s linear type system for (asymptotically) bounding time [8] and Hughes, Pareto and Sabry’s sized types for bounding space [10, 9]. These type systems provide different expressive power from ours: Hoffman provides asymptotic bounds, and Hughes et al. account for heap space, but neither allow bounds to depend on input data, and both work at the level of source code, not executables.

Most similar to our work is Reistad and Gifford’s type system for expressing the running time of programs as a function of their inputs [19]; their work differs mainly in that they limit the programmer to what can be done using a set of primitive cost-related constructs, whereas we build such constructs from basic mechanisms, and (like Hoffman and Hughes et al.) they operate at the level of source, not executables. However, Reistad and Gifford consider cost inference, which we do not, so it may well be profitable to combine their source language with our executable language.

A key contribution of this work is a programming idiom for simulating dependent types using sum and inductive kinds. This idiom does make programs more complex than they would be in a language that included dependent types; the benefit of our approach lies in its substantially simpler type theory and resulting ease of type checking (i.e., verification). We prefer a simpler type theory because, aside from a general preference for simpler type theories, simplicity is key to the robustness of our system. The type checker is part of the trusted computing base of our security infrastructure, so any complexity there makes the system less likely to be secure. The compiler, on the other hand, is not part of the trusted computing base, so any error there merely leads to rejected code.

The principal limitation of our approach lies in the limitations that exist on cost functions. First, cost functions must be primitive recursive, which rules out some resource bounds. Second, cost functions are limited to using a fixed set of built-in arithmetic operators. As discussed in Section 3.3, defined arithmetic operators often do not work as intended because of the lack of an eta-equivalence rule for inductive kinds. Third, cost functions are limited to using aspects of their metric arguments that can be statically represented (or, more precisely, statically represented in a manner admitting an enforcement type). In TALres many sorts of data are not easily represented, such as cyclic data structures. Despite these limitations, we believe that our approach is applicable to a wide variety of important applications.

This work easily generalizes to some other sorts of resource bounds. Easiest is stack space; by replacing the virtual clock with a record of remaining stack space, we may statically prevent stack overflow. Our type system already accounts for the complications involved in recovering resources (recall Section 2). Our approach also appears to generalize to heap space, but to do so we must make the type system aware of when heap space is reclaimed, which it is not when memory is reclaimed by a garbage collector. We conjecture that this can be done using elements of the typed memory management language of Crary et al. [2], which was designed to expose memory management primitives in Typed Assembly Language. Finally, we can account for resource consumption rates by having the program intermittently yield and by replenishing its resource allowance when it is next scheduled after a yield.

Acknowledgements

We thank Dan Grossman, Greg Morrisett, David Walker and Steve Zdancewic for helpful comments, and the TAL group at Cornell University for the Popcorn compiler and TALx86 verifier, the basis of our PopCron compiler and TALres verifier.

References

[1] B. Bershad, S. Savage, P. Pardyak, E. Sirer, M. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility, safety and performance in the SPIN operating system. In Fifteenth ACM Symposium on Operating Systems Principles, pages 267–284, Copper Mountain, Dec. 1995.

[2] K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, San Antonio, Texas, Jan. 1999.

[3] K. Crary and S. Weirich. Flexible type analysis. In 1999 ACM International Conference on Functional Programming, pages 233–248, Paris, Sept. 1999.

[4] K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In 1998 ACM International Conference on Functional Programming, pages 301– 312, Baltimore, Sept. 1998. Extended version published as Cornell University technical report TR98-1721.

[5] J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination de coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 63–92. North-Holland Publishing Co., 1971.

[6] J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[7] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 130– 141, San Francisco, Jan. 1995.

[8] M. Hoffman. Linear types and non-size increasing polynomial time computation. In Fourteenth IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999.

[9] J. Hughes and L. Pareto. Recursion and dynamic datastructures in bounded space: Towards embedded ML programming. In 1999 ACM International Conference on Functional Programming, pages 70–81, Paris, Sept. 1999.

[10] J. Hughes, L. Pareto, and A. Sabry. Proving the correctness of reactive systems using sized types. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 410–423, St. Petersburg, Florida, Jan. 1996.

[11] T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.

[12] N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51(1–2):159–172, 1991.

[13] G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support for System Software, Atlanta, May 1999.

[14] G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 1999. To appear. An earlier version appeared in the 1998 Symposium on Principles of Programming Languages.

[15] G. Necula. Proof-carrying code. In Twenty-Fourth ACM Symposium on Principles of Programming Languages, pages 106–119, Paris, Jan. 1997.

[16] G. Necula and P. Lee. Safe kernel extensions without runtime checking. In Second Symposium on Operating Systems Design and Implementation, pages 229–243, Seattle, Oct. 1996.

[17] G. Necula and P. Lee. Safe, untrusted agents using proofcarrying code. In Special Issue on Mobile Agent Security, volume 1419 of Lecture Notes in Computer Science. Springer-Verlag, Oct. 1997.

[18] G. Necula and P. Lee. The design and implementation of a certifying compiler. In 1998 SIGPLAN Conference on Programming Language Design and Implementation, pages 333–344, Montreal, June 1998.

[19] B. Reistad and D. K. Gifford. Static dependent costs for estimating execution time. In 1994 ACM Conference on Lisp and Functional Programming, pages 65–78, Orlando, Florida, June 1994.

[20] R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Efficient software-based fault isolation. In Fourteenth ACM Symposium on Operating Systems Principles, pages 203– 216, Asheville, Dec. 1993.

[21] H. Xi and F. Pfenning. Dependent types in practical programming. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 214–227, San Antonio, Texas, Jan. 1999.

A Static semantics

A.1 Kind formation

Δ ⊢ k kind

Δ ⊢ Type kind  Δ ⊢ Nat kind  Δ ⊢ 1 kind

Δ ⊢ j kind (j ∈ Δ)  Δ, j ⊢ k kind Δ ⊢ μj.k kind ^{(\begin{matrix}j only positive in k \\ j ∉ Δ \end{matrix})}

Δ ⊢ k_{1} kind Δ ⊢ k_{2} kind Δ ⊢ k_{1} → k_{2} kind

Δ ⊢ k_{1} kind Δ ⊢ k_{2} kind
Δ ⊢ k_{1} + k_{2} kind
Δ ⊢ k_{1} kind Δ ⊢ k_{2} kind
Δ ⊢ k_{1} × k_{2} kind

A.2 Constructor Formation

Δ ⊢ c : k

Δ ⊢ ∗ : 1  Δ ⊢ α : Δ(α)
{Δ, α:k′ ⊢ c : k  Δ ⊢ k′ kind \atop Δ ⊢ λα:k′.c : k′ → k} (α ∉ Δ)
{Δ ⊢ c_{1} : k′ → k  Δ ⊢ c_{2} : k′ \atop Δ ⊢ c_{1}c_{2} : k}  {Δ ⊢ c_{1} : k_{1}  Δ ⊢ c_{2} : k_{2} \atop Δ ⊢ ⟨c_{1}, c_{2}⟩ : k_{1} × k_{2}}
{Δ ⊢ c : k_{1} × k_{2} \atop Δ ⊢ prj_{1} c : k_{1}}  {Δ ⊢ c : k_{1} × k_{2} \atop Δ ⊢ prj_{2} c : k_{2}}

Δ ⊢ c : k_{1} Δ ⊢ k_{2} kind Δ ⊢ inj_{1}^{k_{1}+k_{2}} c : k_{1} + k_{2}

Δ ⊢ c : k_{2} Δ ⊢ k_{1} kind
Δ ⊢ inj_{2}^{k_{1}+k_{2}} c : k_{1} + k_{2}
\begin{matrix}Δ ⊢ c : k_{1} + k_{2} \\ Δ, α:k_{1} ⊢ c_{1} : k \\ Δ, α:k_{2} ⊢ c_{2} : k \end{matrix} Δ ⊢ case(c, α.c_{1}, α.c_{2}) : k (α ∉ Δ)  {Δ ⊢ c : k[μj.k/j] \atop Δ ⊢ fold_{μj.k} c : μj.k}

Δ, j, α:k, φ:j → k′ ⊢ c : k′ Δ ⊢ μj.k kind Δ, j ⊢ k′ kind

Δ ⊢ pr(j, α:k, φ:j →k′.c) : μj.k → k′[μj.k/j] (j only positive in k′, and j, α, φ ∉ Δ)

Δ ⊢ \overline{n} : Nat

Δ ⊢ c_{1} : Nat Δ ⊢ c_{2} : Nat
Δ ⊢ c_{1} ∔ c_{2} : Nat
Δ, α:Nat, β:k ⊢ c_{1} : k Δ ⊢ c_{2} : k

Δ ⊢ prnat_{k}(α, β.c_{1}; c_{2}) : k (α, β ∉ Δ)

Δ ⊢ τ_{1} : Type Δ ⊢ τ_{2} : Type Δ ⊢ c_{1} : Nat Δ ⊢ c_{2} : Nat Δ ⊢ (τ_{1}, c_{1}) → (τ_{2}, c_{2}) : Type

Δ ⊢ τ_{1} : Type Δ ⊢ τ_{2} : Type Δ ⊢ τ_{1} × τ_{2} : Type

Δ ⊢ τ_{1} : Type Δ ⊢ τ_{2} : Type
Δ ⊢ τ_{1} + τ_{2} : Type

Δ, α:k ⊢ τ : Type Δ ⊢ k kind

Δ ⊢ ∀α:k.τ : Type (α ∉ Δ)

Δ, α:k ⊢ τ : Type Δ ⊢ k kind

Δ ⊢ ∃α:k.τ : Type (α ∉ Δ)

Δ ⊢ void : Type  Δ ⊢ unit : Type

Δ ⊢ c : (k → Type) → k → Type Δ ⊢ k kind Δ ⊢ c′ : k Δ ⊢ rec_{k}(c, c′) : Type

A.3 Constructor Equivalence

Δ ⊢ c = c′ : k

Δ ⊢ c′ : k[μj.k/j]  Δ, j ⊢ k′ kind
Δ, j, α:k, φ:j → k′ ⊢ c : k′ Δ ⊢ μj.k kind

Δ ⊢ pr(j, α:k, φ:j → k′.c)(fold_{μj.k} c′) = c[μj.k, c′, pr(j, α:k, φ:j →k′.c)/j, α, φ] : k′[μj.k/j] (j only positive in k′ and j, α, φ ∉ Δ)

{Δ ⊢ c_{1} : k Δ ⊢ c_{2} : k′ \atop Δ ⊢ prj_{1}⟨c_{1}, c_{2}⟩ = c_{1} : k}

{Δ ⊢ c_{1} : k′ Δ ⊢ c_{2} : k \atop Δ ⊢ prj_{2}⟨c_{1}, c_{2}⟩ = c_{2} : k}

Δ ⊢ c : k_{1} × k_{2}

Δ ⊢ ⟨prj_{1} c, prj_{2} c⟩ = c : k_{1} × k_{2}

\begin{matrix}Δ ⊢ k′ kind \\ Δ, α:k′ ⊢ c : k Δ ⊢ c′ : k \end{matrix}

Δ ⊢ (λα:k′.c)c′ = c[c′/α] : k (α ∉ Δ)

{Δ ⊢ c : k′ → k \atop Δ ⊢ (λα:k′.cα) = c : k′ → k} (α ∉ F V (c))

Δ, α:k_{1} ⊢ c_{1} : k Δ, α:k_{2} ⊢ c_{2} : k

Δ ⊢ c : k_{1} Δ ⊢ k_{2} kind

Δ ⊢ case(inj_{1}^{k_{1}+k_{2}} c, α.c_{1}, α.c_{2}) = c_{1}[c/α] : k

Δ, α:k_{1} ⊢ c_{1} : k Δ, α:k_{2} ⊢ c_{2} : k

Δ ⊢ c : k_{2} Δ ⊢ k_{1} kind

Δ ⊢ case(inj_{2}^{k_{1}+k_{2}} c, α.c_{1}, α.c_{2}) = c_{2}[c/α] : k

Δ ⊢ c : k_{1} + k_{2}
Δ ⊢ case(c, α_{1}. inj_{1}^{k_{1}+k_{2}} α_{1}, α_{2}. inj_{2}^{k_{1}+k_{2}} α_{2}) = c : k_{1} + k_{2}
Δ ⊢ c_{1} : Nat Δ ⊢ c_{2} : Nat
Δ ⊢ c_{1} ∔ c_{2} = c_{2} ∔ c_{1} : Nat
Δ ⊢ c_{1} : Nat Δ ⊢ c_{2} : Nat Δ ⊢ c_{3} : Nat

Δ ⊢ c_{1} ∔ (c_{2} ∔ c_{3}) = (c_{1} ∔ c_{2}) ∔ c_{3} : Nat

Δ ⊢ c : Nat
Δ ⊢ c ∔ \overline{0} = c : Nat

Δ ⊢ \overline{n_{1}} ∔ \overline{n_{2}} = \overline{n_{1} + n_{2}} : Nat

Δ, α:Nat, β:k ⊢ c_{1} : k Δ ⊢ c_{2} : k

Δ ⊢ prnat_{k}(α, β.c_{1}; c_{2}) \overline{0} = c_{2} : k

(α, β ∉ Δ)
Δ, α:Nat, β:k ⊢ c_{1} : k Δ ⊢ c_{2} : k Δ ⊢ c : Nat
Δ ⊢ prnat_{k}(α, β.c_{1}; c_{2})(c ∔ \overline{1}) = c_{1}[c, prnat_{k}(α, β.c_{1}; c_{2})(c)/α, β] : k

(α, β ∉ Δ)

{Δ ⊢ c : k \atop Δ ⊢ c = c : k}  {Δ ⊢ c′ = c : k \atop Δ ⊢ c = c′ : k}

{Δ ⊢ c_{1} = c_{2} : k Δ ⊢ c_{2} = c_{3} : k \atop Δ ⊢ c_{1} = c_{3} : k}

{Δ, α:k′ ⊢ c = c′ : k  Δ ⊢ k′ kind \atop Δ ⊢ λα:k′.c = λα:k′.c′ : k′ → k} (α ∉ Δ)

{Δ ⊢ c_{1} = c′_{1} : k′ → k Δ ⊢ c_{2} = c′_{2} : k′ \atop Δ ⊢ c_{1}c_{2} = c′_{1}c′_{2} : k}

{Δ ⊢ c_{1} = c′_{1} : k_{1} Δ ⊢ c_{2} = c′_{2} : k_{2} \atop Δ ⊢ ⟨c_{1}, c_{2}⟩ = ⟨c′_{1}, c′_{2}⟩ : k_{1} × c_{2}}

Δ ⊢ c = c′ : k_{1} × k_{2}
Δ ⊢ prj_{1} c = prj_{1} c′ : k_{1}
Δ ⊢ c = c′ : k_{1} × k_{2}
Δ ⊢ prj_{2} c = prj_{2} c′ : k_{2}

Δ ⊢ c = c′ : k_{1} Δ ⊢ k_{2} kind Δ ⊢ inj_{1}^{k_{1}+k_{2}} c = inj_{1}^{k_{1}+k_{2}} c′ : k_{1} + k_{2}

Δ ⊢ c = c′ : k_{2} Δ ⊢ k_{1} kind

Δ ⊢ inj_{2}^{k_{1}+k_{2}} c = inj_{2}^{k_{1}+k_{2}} c′ : k_{1} + k_{2}

Δ ⊢ c = c′ : k_{1} + k_{2} Δ, α:k_{1} ⊢ c_{1} = c′_{1} : k Δ, α:k_{2} ⊢ c_{2} = c′_{2} : k

Δ ⊢ case(c, α.c_{1}, α.c_{2}) = case(c′, α.c′_{1}, α.c′_{2}) : k (α ∉ Δ)

Δ ⊢ c = c′ : k[μj.k/j]

Δ ⊢ fold_{μj.k} c = fold_{μj.k} c′ : μj.k

Δ, j, α:k, φ:j → k′ ⊢ c_{1} = c_{2} : k′ Δ ⊢ μj.k kind Δ, j ⊢ k′ kind

Δ ⊢ pr(j, α:k, φ:j →k′.c_{1}) = pr(j, α:k, φ:j →k′.c_{2}) : μj.k → k′[μj.k/j] (j only positive in k′ and j, α, φ ∉ Δ)

Δ ⊢ c_{1} = c′_{1} : Nat Δ ⊢ c_{2} = c′_{2} : Nat
Δ ⊢ c_{1} ∔ c_{2} = c′_{1} ∔ c′_{2} : Nat
Δ, α:Nat, β:k ⊢ c_{1} = c′_{1} : k Δ ⊢ c_{2} = c′_{2} : k

Δ ⊢ prnat_{k}(α, β.c_{1}; c_{2}) = prnat_{k}(α, β.c′_{1}; c′_{2}) : k (α, β ∉ Δ)

Δ ⊢ τ_{1} = τ′_{1} : Type Δ ⊢ τ_{2} = τ′_{2} : Type Δ ⊢ c_{1} = c′_{1} : Nat Δ ⊢ c_{2} = c′_{2} : Nat

Δ ⊢ (τ_{1}, c_{1}) → (τ_{2}, c_{2}) = (τ′_{1}, c′_{1}) → (τ′_{2}, c′_{2}) : Type

Δ ⊢ τ_{1} = τ′_{1} : Type Δ ⊢ τ_{2} = τ′_{2} : Type Δ ⊢ τ_{1} × τ_{2} = τ′_{1} × τ′_{2} : Type

Δ ⊢ τ_{1} = τ′_{1} : Type Δ ⊢ τ_{2} = τ′_{2} : Type Δ ⊢ τ_{1} + τ_{2} = τ′_{1} + τ′_{2} : Type

Δ, α:k ⊢ τ = τ′ : Type Δ ⊢ k kind

Δ ⊢ ∀α:k.τ = ∀α:k.τ′ : Type (α ∉ Δ)

Δ, α:k ⊢ τ = τ′ : Type Δ ⊢ k kind

Δ ⊢ ∃α:k.τ = ∃α:k.τ′ : Type (α ∉ Δ)

Δ ⊢ k kind Δ ⊢ c_{2} = c′_{2} : k

Δ ⊢ c_{1} = c′_{1} : (k → Type) → k → Type Δ ⊢ rec_{k}(c_{1}, c_{2}) = rec_{k}(c′_{1}, c′_{2}) : Type

A.4 Term Formation

Δ; Γ; c ⊢ e : τ

Δ; Γ; c ⊢ ∗ : unit ▷ c Δ; Γ; c ⊢ x : Γ(x) ▷ c
Δ; (Γ, x:τ_{1}); c_{1} ⊢ e : τ_{2} ▷ c_{2}
Δ ⊢ τ_{1} : Type Δ ⊢ c_{1} : Nat

Δ; Γ; c ⊢ λ(x:τ_{1}, c_{1}).e : (τ_{1}, c_{1}) → (τ_{2}, c_{2}) ▷ c (x ∉ Γ)

\begin{matrix}Δ; Γ; c ⊢ e_{1} : (τ_{1}, c_{1}) → (τ_{2}, c_{2}) ▷ c′ \\ Δ; Γ; c′ ⊢ e_{2} : τ_{1} ▷ (c_{1} ∔ 1) \end{matrix} ; Δ; Γ; c ⊢ e_{1}e_{2} : τ_{2} ▷ c_{2}

Δ; Γ; c ⊢ e : τ ▷ (c_{1} ∔ c_{2})
Δ; Γ; c ⊢ waste[c_{1}]e : τ ▷ c_{2}

{Δ; Γ; c ⊢ e_{1} : τ_{1} ▷ c_{1} Δ; Γ; c_{1} ⊢ e_{2} : τ_{2} ▷ c_{2} \atop Δ; Γ; c ⊢ ⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2} ▷ c_{2}}

{Δ; Γ; c ⊢ e : τ_{1} × τ_{2} ▷ c′ \atop Δ; Γ; c ⊢ prj_{1} e : τ_{1} ▷ c′}  {Δ; Γ; c ⊢ e : τ_{1} × τ_{2} ▷ c′ \atop Δ; Γ; c ⊢ prj_{2} e : τ_{2} ▷ c′}
Δ; Γ; c ⊢ e : τ_{1} ▷ c′ Δ ⊢ τ_{2} : Type
Δ; Γ; c ⊢ inj_{1}^{τ_{1}+τ_{2}} e : τ_{1} + τ_{2} ▷ c′
Δ; Γ; c ⊢ e : τ_{2} ▷ c′ Δ ⊢ τ_{1} : Type
Δ; Γ; c ⊢ inj_{2}^{τ_{1}+τ_{2}} e : τ_{1} + τ_{2} ▷ c′
Δ; Γ; c ⊢ e : τ_{1} + τ_{2} ▷ c′
Δ; (Γ, x:τ_{1}); c′ ⊢ e_{1} : τ ▷ c′′
Δ; (Γ, x:τ_{2}); c′ ⊢ e_{2} : τ ▷ c′′

Δ; Γ; c ⊢ case(e, x.e_{1}, x.e_{2}) : τ ▷ c′′ (x ∉ Γ)

(Δ, α:k); Γ; c ⊢ v : τ ▷ c Δ ⊢ k kind

Δ; Γ; c ⊢ Λα:k.v : ∀α:k.τ ▷ c (α ∉ Δ)

{Δ; Γ; c_{1} ⊢ e : ∀α:k.τ ▷ c_{2} Δ ⊢ c : k \atop Δ; Γ; c_{1} ⊢ e[c] : τ[c′/α] ▷ c_{2}}

Δ; (Γ, f:τ); c ⊢ v : τ ▷ c Δ ⊢ τ : Type

Δ; Γ; c ⊢ fix f:τ.v : τ ▷ c

(f ∉ Γ and v = Λα_{1}:k_{1} … Λα_{n}:k_{n}.λ(x:τ′, c′).e′)

Δ, α:k ⊢ τ : Type

Δ ⊢ c : k Δ; Γ; c_{1} ⊢ e : τ[c/α] ▷ c_{2} Δ; Γ; c_{1} ⊢ pack e as ∃α:k.τ hiding c : ∃α:k.τ ▷ c_{2}

(α ∉ Δ)

\begin{matrix}Δ; Γ; c ⊢ e_{1} : ∃α:k.τ_{2} ▷ c′ \\ (Δ, α:k); (Γ, x:τ_{2}); c′ ⊢ e_{2} : τ_{1} ▷ c′′ \end{matrix}

Δ; Γ; c ⊢ unpack ⟨α, x⟩ = e_{1} in e_{2} : τ_{1} ▷ c′′ (\begin{matrix}α ∉ Δ, F V (τ) \\ x ∉ Γ \end{matrix})

Δ; Γ; c_{1} ⊢ e : rec_{k}(c, c′) ▷ c_{2}
Δ; Γ; c_{1} ⊢ unfold e : c(λα:k. rec_{k}(c, α))c′ ▷ c_{2}

Δ; Γ; c_{1} ⊢ e : c(λα:k. rec_{k}(c, α))c′ ▷ c_{2}

Δ ⊢ rec_{k}(c, c′) : Type

Δ; Γ; c_{1} ⊢ fold_{rec_{k}(c,c′)} e : rec_{k}(c, c′) ▷ c_{2}

Δ, β:k_{1}, Δ′; Γ[inj_{1}^{k_{1}+k_{2}} β/α]; c_{1}[inj_{1}^{k_{1}+k_{2}} β/α] ⊢

v[inj_{1}^{k_{1}+k_{2}} β/α] : void ▷ c′_{2} Δ, β:k_{2}, Δ′; Γ[inj_{2}^{k_{1}+k_{2}} β/α]; c_{1}[inj_{2}^{k_{1}+k_{2}} β/α] ⊢

e[inj_{2}^{k_{1}+k_{2}} β/α] : τ[inj_{2}^{k_{1}+k_{2}} β/α] ▷ c_{2}[inj_{2}^{k_{1}+k_{2}} β/α] Δ, α:k_{1} + k_{2}, Δ′ ⊢ c = α : k_{1} + k_{2} Δ, α:k_{1} + k_{2}, Δ′; Γ; c_{1} ⊢ vcase_{τ▷c_{2}}(c, β. dead v, β.e) : τ ▷ c_{2}

(β ∉ Δ)

Δ, β:k_{1}, Δ′; Γ[inj_{1}^{k_{1}+k_{2}} β/α]; c_{1}[inj_{1}^{k_{1}+k_{2}} β/α] ⊢

e[inj_{1}^{k_{1}+k_{2}} β/α] : τ[inj_{1}^{k_{1}+k_{2}} β/α] ▷ c_{2}[inj_{1}^{k_{1}+k_{2}} β/α] Δ, β:k_{2}, Δ′; Γ[inj_{2}^{k_{1}+k_{2}} β/α]; c_{1}[inj_{2}^{k_{1}+k_{2}} β/α] ⊢

v[inj_{2}^{k_{1}+k_{2}} β/α] : void ▷ c′_{2} Δ, α:k_{1} + k_{2}, Δ′ ⊢ c = α : k_{1} + k_{2} Δ, α:k_{1} + k_{2}, Δ′; Γ; c_{1} ⊢ vcase_{τ▷c_{2}}(c, β.e, β. dead v) : τ ▷ c_{2}

(β ∉ Δ)

Δ, β:k_{1}, γ:k_{2}, Δ′; Γ[⟨β, γ⟩/α]; c_{1}[⟨β, γ⟩/α] ⊢

e[⟨β, γ⟩/α] : τ[⟨β, γ⟩/α] ▷ c_{2}[⟨β, γ⟩/α] Δ, α:k_{1} × k_{2}, Δ′ ⊢ c = α : k_{1} × k_{2}

Δ, α:k_{1} × k_{2}, Δ′; Γ; c_{1} ⊢ let_{τ▷c_{2}}⟨β, γ⟩ = c in e : τ ▷ c_{2} (β, γ ∉ Δ)

Δ, β:k[μj.k/j], Δ′; Γ[fold_{μj.k} β/α] ⊢ c_{1}[fold_{μj.k} β/α] ⊢

e[fold_{μj.k} β/α] : τ[fold_{μj.k} β/α] ▷ c_{2}[fold_{μj.k} β/α] Δ, α:μj.k, Δ′ ⊢ c = α : μj.k Δ, α, Δ′:μj.k; Γ; c_{1} ⊢ let_{τ▷c_{2}}(fold_{μj.k} β) = c in e : τ ▷ c_{2}

(β ∉ Δ)

Δ ⊢ c = inj_{1}^{k_{1}+k_{2}} c′ : k_{1} + k_{2} Δ; Γ; c_{1} ⊢ e_{1}[c′/α] : τ ▷ c_{2} Δ; Γ; c_{1} ⊢ vcase_{τ▷c_{2}}(c, α.e_{1}, α. dead v) : τ ▷ c_{2}

Δ ⊢ c = inj_{2}^{k_{1}+k_{2}} c′ : k_{1} + k_{2} Δ; Γ; c_{1} ⊢ e_{2}[c′/α] : τ ▷ c_{2} Δ; Γ; c_{1} ⊢ vcase_{τ▷c_{2}}(c, α. dead v, α.e_{2}) : τ ▷ c_{2}

Δ ⊢ c = ⟨c′, c′′⟩ : k_{1} × k_{2} Δ; Γ; c_{1} ⊢ e[c′, c′′/β, γ] : τ ▷ c_{2}

Δ; Γ; c_{1} ⊢ let_{τ▷c_{2}} ⟨β, γ⟩ = c in e : τ ▷ c_{2}

Δ ⊢ c = fold_{μj.k}(c′) Δ; Γ; c_{1} ⊢ e[c′/β] : τ ▷ c_{2}

Δ; Γ; c_{1} ⊢ let_{τ▷c_{2}} (fold_{μj.k} β) = c in e : τ ▷ c_{2}

Δ; Γ; c_{1} ⊢ e : τ′ ▷ c′_{2} Δ ⊢ τ = τ′ : Type Δ ⊢ c_{2} = c′_{2} : Nat

Δ; Γ; c_{1} ⊢ e : τ ▷ c_{2}

B Operational semantics Value syntax

v ::= ∗ | λ(x:τ, c).e | ⟨v_{1}, v_{2}⟩ | inj_{1}^{τ_{1}+τ_{2}} v | inj_{2}^{τ_{1}+τ_{2}} v
| Λα:k.v | (fix f:τ.v)[c_{1}] ⋯ [c_{n}] | fold_{rec_{k}(c,c′)} v

| pack v as ∃α.c_{1} hiding c_{2}

| x | prj_{1} v | prj_{2} v

Evaluation rules

((λ(x:τ, c).e)v, n + 1) ↦ (e[v/x], n) (provided n ≥ 0)

{(e_{1}, n) ↦ (e′_{1}, n′) \atop (e_{1}e_{2}, n) ↦ (e′_{1}e_{2}, n′)}  {(e_{2}, n) ↦ (e′_{2}, n′) \atop (ve_{2}, n) ↦ (ve′_{2}, n′)}

(e, n) ↦ (e′, n′) (waste[c]e, n) ↦ (waste[c]e′, n′)

c normalizes to \overline{n} (waste[c]v, n + n′) ↦ (v, n′) (provided n′ ≥ 0)

(prj_{1}⟨v_{1}, v_{2}⟩, n) ↦ (v_{1}, n)  (prj_{2}⟨v_{1}, v_{2}⟩, n) ↦ (v_{2}, n)
{(e, n) ↦ (e′, n′) \atop (prj_{1} e, n) ↦ (prj_{1} e′, n′)}  {(e, n) ↦ (e′, n′) \atop (prj_{2} e, n) ↦ (prj_{2} e′, n′)}
{(e_{1}, n) ↦ (e′_{1}, n′) \atop (⟨e_{1}, e_{2}⟩, n) ↦ (⟨e′_{1}, e_{2}⟩, n′)}  {(e_{2}, n) ↦ (e′_{2}, n′) \atop (⟨v, e_{2}⟩, n) ↦ (⟨v, e′_{2}⟩, n′)}

(case(inj_{1}^{τ_{1}+τ_{2}} v, x_{1}.e_{1}, x_{2}.e_{2}), n) ↦ (e_{1}[v/x_{1}], n)

(case(inj_{2}^{τ_{1}+τ_{2}} v, x_{1}.e_{1}, x_{2}.e_{2}), n) ↦ (e_{2}[v/x_{2}], n)

{(e, n) ↦ (e′, n′) \atop (inj_{1}^{τ_{1}+τ_{2}} e, n) ↦ (inj_{1}^{τ_{1}+τ_{2}} e′, n′)}

{(e, n) ↦ (e′, n′) \atop (inj_{2}^{τ_{1}+τ_{2}} e, n) ↦ (inj_{2}^{τ_{1}+τ_{2}} e′, n′)}

(e, n) ↦ (e′, n′)

(case(e, x_{1}.e_{1}, x_{2}.e_{2}), n) ↦ (case(e′, x_{1}.e_{1}, x_{2}.e_{2}), n′)

(Λα:k.v[c], n) ↦ (v[c/α], n)  {(e, n) ↦ (e′, n′) \atop (e[c], n) ↦ (e′[c], n′)}

c normalizes to inj_{1} c′

(vcase(c, α_{1}.e_{1}, α_{2}. dead v), n) ↦ (e_{1}[c′/α_{1}], n)

c normalizes to inj_{2} c′

(vcase(c, α_{1}. dead v, α_{2}.e_{2}), n) ↦ (e_{2}[c′/α_{2}], n)

c normalizes to ⟨c_{1}, c_{2}⟩

(let⟨β, γ⟩ = c in e, n) ↦ (e[c_{1}, c_{2}/β, γ], n)

c normalizes to fold_{μj.k} c′ (let(fold_{μj.k} β) = c in e, n) ↦ (e[c′/β], n)

((fix f:τ.v)[c_{1}] ⋯ [c_{n}]v′, n) ↦ ((v[fix f:τ.v/f])[c_{1}] ⋯ [c_{n}]v′, n)

(e, n) ↦ (e′, n′)

(pack e as ∃β.c_{1} hiding c_{2}, n) ↦ (pack e′ as ∃β.c_{1} hiding c_{2}, n′)

(unpack ⟨α, x⟩ = (pack v as τ hiding c) in e, n) ↦ (e[c, v/α, x], n)

(e, n) ↦ (e′, n′)

(unpack ⟨α, x⟩ = e in e_{2}, n) ↦ (unpack ⟨α, x⟩ = e′ in e_{2}, n′)

(unfold (fold_{rec_{k}(c,c′)} v), n) ↦ (v, n)

(e, n) ↦ (e′, n′)

(fold_{rec_{k}(c,c′)} e, n) ↦ (fold_{rec_{k}(c,c′)} e′, n′)

(e, n) ↦ (e′, n′) (unfold e, n) ↦ (unfold e′, n′)