# «Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»

◦ We have used= to deﬁne resource and rmap, indicating that they are opaque to the rest of the proof. The rest of the Coq development does not know that the underlying model uses dependent types. When the rest of the soundness proof wishes to use resource and rmap, it must use the axioms exposed by the module, such as NO and YES as deﬁned in section 7.2.6. Therefore the rest of the proof can be blissfully unaware of the stratiﬁcation going on under the hood.

In contrast, we have used = to deﬁne world and predicate, indicating that those deﬁnitions are fully exposed to the rest of the proof.

7.2.3 Relating the models The deﬁnitions in the third section of ﬁgure 7.2 are used only under the hood. However, as we shall see in section 7.2.6 they are critical to deﬁning some parts of the interface that the rest of the proof does use, such as the YES pseudoconstructor.

Within the model, often it is useful to know the amount of stratication in a given rmap. The function level allows just that, taking a rmap and returning the value of its ﬁrst component.

Another thing the model must be able to do is take an external view of the model (i.e., a predicate) and translate it into the stratiﬁed construction (i.e., a predicaten ). A predicate in some sense is inﬁnitely

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

This is the job of the stratify operator4. The stratify operator takes a natural n and a predicate P, and produces a predicaten Pn, which is P stratiﬁed to level n. It does this by using the recursion operator ﬁx in the Calculus of Constructions to recursively deﬁne the nested structure of the stratiﬁed predicate.

As explained above, a stratiﬁed predicate at level 0 is has type unit;

the value tt has the unit type. A stratiﬁed predicate at level n + 1 is a pair of a stratiﬁed predicate at level n and a function from a pair of rmap at level n and mem to Prop. The ﬁrst component of this pair is deﬁned by the recursive call to the stratify operator. The second component is

**more interesting, since it is the essential point of the stratiﬁcation:**

By the deﬁnition of predicaten, this must have type worldn−1 → Prop, and accordingly the parameter v has type worldn−1. Recall that worldn−1 = locals × rmapn−1 × mem. The result type must be Prop, which is simple enough to satisfy on its own (e.g., with true), but the goal is to build the stratiﬁed Pn from P.

Given that we have a stratiﬁed rmapn−1 as the second component of v, we can build an rmap with the dependent pair {n − 1, v.1}. By Appel et al. [AMRV07] write this operator as ⌊·⌋n, and is deﬁne it in a more mathematical style as deﬁnition 29.

7.2. A SUBSTRUCTURAL MODAL MODEL projecting out the ﬁrst and third components of v as well we are able to build a world, to which we can apply the predicate P.

Since P is being applied to a rmapn−1 of level n − 1, it will only be able to judge properties involving the rmap that are no more than n − 1 levels of stratiﬁcation deep. As an example, consider the value

Simplifying the deﬁnition yields (tt, λv : (locals × rmap0 × mem). P (v.1, {0, v.2}, v.3)).

Unfolding the deﬁnition of rmap0 yields (tt, λv : (locals×(address → resource0 )×mem). P (v.1, {0, v.2}, v.3)).

A resource0 is either NO0 or YES0 (k, π, P0). However, predicate0 is equal to unit, so the list P0 is a list of elements of type unit. Of course, one unit is much like another; this means that stratify 1 P cannot distinguish two YES0 resources by examining their predicates.

The inability to fully distinguish YESn resources by examining their predicates has signiﬁcant implications for inversion. Suppose we have two predicates P and Q, and we know that for a given k

What can we conclude? Certainly not P = Q, since perhaps at some greater level of stratiﬁcation k ′ k the two predicates will diﬀer. In fact, in the worst case k = 0, and we have the horrible-looking fact that

In other words, stratify k P = stratify k Q if and only if P and Q are equivalent for all rmaps with stratiﬁcation level strictly less than k.

7.2.4 Characterizing Increasing Approximation The problem with (C1) is that it both exposes the inner workings of the stratiﬁed model by universally quantifying over φj and exposes the inner workings of the dependent model by explicitly constructing

Since the idea behind (C1) is that P and Q are equivalent for all rmaps with stratiﬁcation level strictly less than k, it seems reasonable to characterize this property in a way that does not expose the underlying model.

In ﬁgure 7.3 we build the machinery to do just that. First we deﬁne three operators, age1 predicaten+1, age1 resourcen+1, and age1 rmapn+1 that remove one level of stratiﬁcation from predicaten+1, resourcen+1, and rmapn+1, respectively, by “forgetting” some stratiﬁcation. A point to note is that age1 predicaten+1, which causes the actual information loss, has a very simple deﬁnition due to the pair structure of predicaten.

All three of these operators are undeﬁned on stratiﬁcation level 0, and, since all of the operators expose the underlying stratiﬁcation, we wish to completely hide them from the rest of the proof.

Now that we have deﬁned aging on the stratiﬁed model, we extend it to the dependent model with the age1 operator, which simply unpacks the dependent pair and then uses the age1 rmapn+1 operator. Since we would like age1 to be deﬁned for all rmaps, we have it return None if j = 0. Since age1 is actually removing structure, it is irreﬂexive, i.e.,

The age1 operator is opaque; the rest of the proof can see that it exists, but is only allowed to use it via axioms deﬁned in the module type.

Finally, we deﬁne the age operator, which is just the nth composition

7.2. A SUBSTRUCTURAL MODAL MODEL of age1. For all n 0, age is irreﬂexive5.

Now that we have deﬁned age, we can use it to characterize the stratify operator by observing that

This is a much better characterization of stratify because it does not expose the stratiﬁed construction. However, it is not ideal, since it requires exposing the private level function. We will see a still more elegant way of expressing this property in section 7.3.

7.2.5 Stratiﬁed separation algebras for the model In section 4.4 we deﬁned a stratiﬁed separation algebra by building on the ideas of Calcagno et al. [COY07]. In section 4.5 we explained that shares are such an algebra. Here we will show how to lift the separation algebra on share to resource, rmap, and world.

For comparison with previous work [AMRV07], the relation R(φ, φ′ ) = ∃n. (age (n + 1) φ = Some φ′ ) is irreﬂexive, transitive, and Noetherian, and moves between the worlds in the underlying Kripke model.

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

Join relations for the stratiﬁed model We deﬁne the join relation ⊕n of resourcen as follows. Two YESn resources join YESn (k, Some π1, Pn ) ⊕n YESn (k, Some π2, Pn ) = YESn (k, Some π3, Pn )In other words, for two YESn resources to join, they must be the same kind, have shares that join, and have identical predicate lists. NOn is the identity element for level n. Two resourcen at diﬀerent levels never join.

As with resourcen, two rmapn at diﬀerent levels do not join.

From the join relation on rmapn, we deﬁne the join relation on worldn by requiring the rmapn to join and all other members of the tuple to be In the presentation we “overload” the ⊕n and ⊕ symbols, using the same symbol for resource, rmap, etc.

7.2. A SUBSTRUCTURAL MODAL MODEL

Join relations for the dependent model

**Once we have deﬁned the join relation ⊕n on elements ξa ξb ξc :**

resourcen, we can deﬁne the join relation ⊕ on resource by saying that

Finally, we can deﬁne the join relation on world by requiring the

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

**rmaps to join and all other members of the tuple to be equal:**

Stratiﬁed separation algebras When the join relation is deﬁned in this way, resourcen, resource, rmapn, rmap, worldn, and world become stratiﬁed separation algebras as deﬁned in section 4.4; proved in Coq7.

The join relations for resourcen, rmapn, and worldn and the proof that they form stratiﬁed separation algebras are completely hidden from the rest of the proof. However, the join relations for resource, rmap, and world and the fact that they form stratiﬁed separation algebras are exposed to the rest of the proof and are used to reason about the substructural elements in the model.

7.2.6 The public interface The rest of the CSL soundness proof should never see the internals of the stratiﬁcation. Instead, the rest of the proof should treat the deﬁnitions of resource and rmap as opaque and handle elements of type resource and rmap by using a carefully designed interface.

In the actual Coq development, a special kind of function constructor, called a Joinmap, was used to lift the separation algebra properties from resource to rmap.

7.2. A SUBSTRUCTURAL MODAL MODEL That interface consists of three parts. The ﬁrst is a number of functions whose existence and type signature are exported to the rest of the proof but whose internals are hidden by the module type. The second is a series of helper deﬁnitions which are deﬁned in terms of the opaque functions and are fully visible to the rest of the proof. We have already discussed the age1 and age operators, which were given in ﬁgure 7.3.

The ﬁrst of these is an opaque deﬁnition; the second is a helper deﬁnition. The third part of the interface is a long series of axioms which show how the opaque functions behave. For example, one exported axiom involving age1 is

In other words, age1 is irreﬂexive.

** Figure 7.4 gives some of the most important opaque functions, with the deﬁnitions of resource at and the pseudoconstructors NO and YES.**

These have the types given in ﬁgure 6.3 and explained in section 6.2.2.

In that section we also explained how to build up the other pseudoconstructors such as LK from YES.

The join relation ⊕ was discussed in section 7.2.5. To reason about the join relation we export all of the axioms of a stratiﬁed separation algebra given in section 4.4, as well as property 8 from section 4.5.

The resource at function takes an rmap and an address and returns the resource associated with that address. As mentioned in section 6.2.2,

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

resource at is usually written inﬁx using the @ symbol, a convention we will follow in this presentation as well.

The NO pseudoconstructor takes an rmap φ; out of this it extracts the level n and constructs the dependent pair {n, NOn }, which has type resource. The YES pseudoconstructor takes an rmap φ, a kind k, a pshare π, and a list of predicates P, extracts the level n from φ, maps the stratify function at level n over P to get Pn, and constructs the dependent pair {n, YESn (k, π, Pn )}, which also has type resource.

We are now in a position to understand the ramiﬁcations for inverting the YES pseudoconstructor, as promised in section 6.2.2. By examining the deﬁnitions and understanding the results of inverting the stratify function, it is clear that

if and only if level φ = level φ′, k = k ′, π = π ′, and the predicates in P and P ′ are equivalent up to stratiﬁcation level φ.

Unfortunately this characterization of YES inversion exposes the underlying model. When we deﬁne our modal substructural logic it will be possible to express this property in a very elegant way (see section 7.3.10).

We also give the helper deﬁnitions ⊥ and same age. ⊥ is deﬁned exactly as explained in section 4.3. The same age relation, which is deﬁned in terms of the join relation, states that two resource maps are

## CHAPTER 7. A MODAL SUBSTRUCTURAL LOGIC

in the same equivalence class, as explained in section 4.4. There is a convenient connection between the public same age relation and the**private level function:**

same age(φ, φ′)

We have now given an explanation of the underlying stratiﬁed separation algebra, and have explained how one can use dependent types to hide the stratiﬁcation from the rest of the proof. However, even reasoning about the dependently typed model can be laborious.

The second major insight of the modal model of Appel et al. [AMRV07] was that one can deﬁne a modal logic for reasoning about the model.

Various operators in the modal logic will reason about diﬀerent aspects of the model. The modal logic then becomes a clean interface to the opaque dependent model, which itself is a clean interface for the ugly details of the stratiﬁcation.

In the Coq development we take this idea a step further [DAH08].

In general we have found that when we get to a point in the Coq development where the way forward is diﬃcult or unclear, the solution