Hello, I'm Jeremy, I work on the certified kernel Certicos, and I'm going to present

some of our research on refinement-based game semantics. Certified software comes with a formal specification and a mechanized proof of correctness. The projects that I've listed here all use the Coq proof assistant, so there's

interest in connecting them as certified components to create larger scale certified systems. However, each one uses its own semantic models and verification techniques, so we need to identify a general-purpose model which could embed all of them.

This model should support composition and help us bridge the gap between components which operate at different levels of abstraction. Our work on Certicos illustrates some of these concepts. In our verification effort, we divided the kernel into 37 layers, which we specified

and verified individually. Then we used their specifications as interfaces to connect them and to derive a correctness property for the whole system. Here I've shown the structure of a single certified abstraction layer. The underlay interface L1 describes and specifies the functionality provided by the layer below,

and the overlay interface L2 describes the functionality that we want to implement. So by verifying that the layer code M correctly implements L2 in terms of L1, we're able

to derive the contextual refinement property that I've shown on the right. Because the overlay interface L2 could be described in more abstract terms than the underlay interface, we also need to include a simulation relation R which explains how the more abstract data structures in L1 are realized in terms of the more concrete data

structures in L2. So that's how certified abstraction layers work, and our goal will be to expand this paradigm and make it more flexible so that it can cover a broader range of certified components.

Fortunately, there's a lot of interesting research that we can draw from. For example, game semantics can model the behavior of systems in very general and compositional ways, and the refinement calculus can express a broad range of specifications and support

stepwise refinement. Yet if you look at a typical verification project, you'll find that they use fairly old-school technology, so there's a question of why these new ideas haven't been adopted

in that context. One reason is that these models can get fairly sophisticated, and so they're hard to mechanize in a proof assistant, but more importantly, for our purposes, we need all of these features to work together in a single framework, and it's not clear how these different lines

of research could be combined to accomplish this. For example, in game semantics, there hasn't been a lot of work on refinement and on determinism, but on the other hand, in the refinement calculus, we can only model imperative programs

and specifications. So refinement-based game semantics is going to bridge this gap by synthesizing ideas from game semantics, the refinement calculus, and other lines of work. We build general and compositional models, which support stepwise refinement and data

abstraction, and we believe they are suitable for building large-scale certified systems. Our key insight is that strategies in game semantics are already inherently non-deterministic, and we construct our models by lifting restrictions on this non-determinism and upgrading it

to dual non-determinism. Before I explain in detail how our model works, I'll present the main ideas behind our approach.

Traditionally, programs and specifications are two very different kinds of things. In a hard-triple PCQ, there's a strong distinction between the program C and the pre- and post-conditions P and Q. By contrast, in refinement-based approaches, programs and specifications will be treated

as objects of the same kind. We start from a specification S, which could be very abstract and declarative, and then incrementally refine it until we obtain an executable program Cn. In this context, non-determinism is a very useful tool for expressing

specifications, and there are two ways to interpret non-deterministic choice. On one hand, an angelic choice of specifications means that the implementation must refine both of them. It makes the specification stronger and provides more guarantees to the user.

On the other hand, demonic choice means that the implementation can refine either one of them. It weakens the specification, but it gives us more implementation freedom. Some models offer both kinds of non-determinism.

In the refinement calculus, this takes the form of a completely distributive lattice for the refinement ordering. The properties of lattices mean that the model is insensitive to angelic and demonic branching, and distributivity means that angelic and demonic choices

also commute with one another. So let's look at an example to see how this works. A function can be seen as a very simple system which performs one input followed by one output. As a specification, we can ask that a given input x

should be mapped to a given output y. For instance, a function f which doubles its argument satisfies the specification that I've shown here. Then, using angelic non-determinism, we can strengthen this specification and ask that a function both maps 0 to 0, but also maps 1 to 2.

Going one step further, with infinite choice, we can ask that all possible inputs x should be mapped to 2x. And in fact, this is how we encode the function f itself as a specification.

On the other hand, demonic non-determinism works in the opposite direction. For example, this specification is fairly weak and it only asks that a function map 1 of the possible inputs x to its successor x plus 1.

We can narrow down the choice of x to either 0 or 1 to obtain a stronger specification, and if we narrow it down further to retain only the right hand side, we can see that since our function indeed maps 1 to 2, it's gonna refine all of these specifications.

Finally, we can use angelic and demonic choice together to express more complicated constraints. For example, this specification expresses that f should map all odd numbers to even numbers. The bottom line is that on the left of the refinement relation,

angelic choice behaves similarly to the forward quantifier, and demonic choice behaves like there exists. It's gonna be very powerful when we talk about data abstraction. For example, consider the representation of integers as pairs of natural numbers.

If you see the pair as a credit and debit columns of a bank account, then the balance is the corresponding integer. Now, the question is, what does it mean for a function g defined on pairs of natural numbers to implement a function f defined on integers?

We can express this relation with the simulation diagram I've shown here which says that related inputs should be taken to related outputs, but since this relation involves objects of different types, it's not clear how it fits into our refinement framework.

With dual non-determinism, we can actually use R to translate the specification f to obtain a corresponding specification on pairs of natural numbers. We use angelic choice to decode the input because the environment is free to choose the input representation.

On the other hand, the output representation is chosen by the system, so we use demonic choice to encode the result of f. This translation also has an upper adjoint which works in the opposite direction. It translates g into a refinement of f,

and so that's similar to what happens in abstract interpretation where we use Galois connections to establish a correspondence between the concrete and abstract states. Next, I'm going to talk about refinement and non-determinism in the context of game semantics.

In game semantics, strategies are represented as sets of plays, or traces, and our elementary function specifications can be seen as a very simple form of plays. Each move in a play is assigned to either the environment or the system,

and in our case, the function's input is a move of the environment, and the output is a move of the system. When we look at a set like this one, we can use the polarity of moves to interpret non-determinism in the corresponding direction. So, this set can be read as a specification

which requires 0 to be mapped to 0, but allows 1 to be mapped to either 1 or minus 1. The problem with this approach is that the refinement ordering we get is quite hard to describe, and this gets much worse when we consider complex plays which interleave several moves of the system and the environment.

On the other hand, if we revisit the way strategies are constructed and decouple non-determinism from the polarity of moves, we'll get a model that is both simpler and more expressive. Our approach will be to think of plays as elementary specifications

that dictate the behavior of the system for one behavior of the environment. Then, using angelic non-determinism, we can arrange over all possible behaviors of the environment to obtain a notion of strategy, and, adding demonic non-determinism,

we can introduce choices for the system as well, and obtain a notion of strategy specification. So, roughly speaking, strategy specifications will be sets of sets of plays, but a nice way to describe this is to use a monad to capture dual non-determinism as an effect.

Without going into too much detail, the FCD monad can extend any partially ordered set with dual non-determinism by adding arbitrary angelic and demonic choices. It will do that by constructing the free, completely distributive lattice

generated by the poset. Every element in this lattice can be described as an angelic choice of demonic choices of elements of the poset, and sequential composition will accumulate the non-determinism

in both computations. Now that I've described the main ideas behind our work, I'm going to talk about the game model that we constructed.

Since we're only interested in modeling first-order computation, we can use a very simple kind of games. We will use signatures of the form that I have shown here, which are sets of questions where each question is assigned a set of possible answers. As a running example,

we're going to consider how a queue can be implemented in terms of an array. So, a queue is simply a sequence of elements with two operations to unqueue an element at the end and dequeue an element from the front.

Since the enqueue operation takes an argument, we'll encode it in the signature as a family of questions, one for each possible argument value. We'll implement the queue using an array and two counters which will mark the beginning and end of the queue within the array.

We have operations to access the array and operations which increment counters and return their previous values. Given a signature, we can define the corresponding set of plays. Each player represents an execution of a computation which asks questions from a signature E

and gets answers from the environment. A play will be a sequence of questions and answers and the computation can also terminate with an outcome in a given set A. For clarity, we underline the moves of the system and leave the moves of the environment as is.

As an example, I've shown one possible scenario where an element is dequeued from an array. We increment the first counter, find that its original value was 3, and then access the array to query the value at position 3 and return the answer.

From this kind of play, we can build a notion of interaction specification. We'll represent them using the free, completely distributive lattice generated by a set of plays ordered under a prefix relation. Then, we can describe our dequeue operation

in more detail and in more general terms by using angelic non-determinism to arrange over all possible answers we get from the environment. Interaction specifications are equipped with a monadic structure which allows us to decompose strategies sequentially.

If we have a computation X and specify for each possible outcome how the computation should continue, then we can define a composite computation which has the cumulated effects of both. The unit is a simple computation

which immediately returns a given value v and we can also define for each possible question m in the signature an elementary operation which asks the question and returns the answer. By combining these, we can describe the dequeue operation

in an easier and more familiar way. So far, we have only described the client side of things but strategies in game semantics are usually two-sided. They play one game in the role of the client and the other game in the opposite role.

Like certified abstraction layers, they use one interface to provide another interface. In our case, we can provide the interface F by specifying how to answer each possible question in a signature. And for that, we'll give an interaction specification

which uses the signature E. So, a morphism from E to F will first accept a question Q in the signature F then ask a series of questions in E and finally produce an answer for their original question Q.

As an example, I've shown a morphism which implements Q operations by performing series of array operations. The dequeue operation is as I've shown before and the enqueue operation works in a very similar way. Morphisms add a new dimension of composition to our model.

So, if we have a computation which asks question in F and a morphism from E to F then we can combine them so that every question of X is translated by the morphism. The result is a computation which asks question in E

and produces the same outcome as X. For instance, if we have code for rotating a Q which performs first a dequeue operation and then an enqueue operation we can use the morphism we have defined before to translate these Q operations into the corresponding array operations.

So, this basic substitution operation can also be used to define the composition of morphisms by using one morphism to translate all of the interaction specifications that have been used to define the other morphisms.

So, now we have almost everything we need to describe certified abstraction layers. But in such a course, layer interfaces are specified using sets of abstract states. In this model, we can add the state by annotating every question and answer in a signature

with a current state. Then, the Q and array can be specified in the following way. For the Q, the states are just sequences of values. The specification doesn't perform any operations itself so it can be modeled as a morphism from the empty signature.

The enqueue operation simply returns the unit value annotated with a state which has been updated to include the value that we have enqueued. The dequeue operation uses angelic non-determinism to decompose the Q into a head and tail. Then it returns the head and uses the tail

as the new state of the Q. If the Q was empty, the result would be the bottom specification and then the implementation is free to do anything because the client breached their contract by trying to dequeue from an empty queue. Now, if we have some client code

which uses Q operations like our rotation code from before we can extend it so that it maintains a current state at all times. We get an initial state as input, then every outgoing question is annotated with the current state and once we get the answer, we use it to update the state.

When the computation ends, we can return the final state as well as the computation's outcome. This can then be composed with our Q specification to describe the behavior of the code in terms of Q states.

I won't describe the array operation in detail but we can use a similar approach to specify them. And again, we can compose our Q implementation MQ with the specification LA to obtain the behavior of the implementation

in terms of array states. The last step is data abstraction. As before, if we have layer interfaces which use different kinds of states we can define a simulation relation R between them. This relation can then be embedded as a joint morphisms

which translate between the two interfaces. In the case of queues and arrays, the relation will read out values stored in the array between the two counters and then compare them with the contents of the queue. Applying this relation to our Q interface

will get a specification for what the Q implementation should be doing in terms of array states. The specification uses angelic non-determinism to decode a Q from the array and demonic non-determinism to choose a representation for the new Q.

And that's it. Now we can use our model to describe certified abstraction layers. For each interface, we give a signature, a set of states and a morphism that gives the specifications for its operations. Then, the layer implementation MQ

can be evaluated on top of the underlay LA and the simulation relation can be used to translate states so that we can express our layer correctness property as a refinement property. This illustrates the expressivity of our model.

We're able to represent various kinds of components in a uniform way. The model that I have presented can also embed a compositional semantics for the compiler CompCert and interaction trees which are another model that is used for verification

and this doesn't have to be the end of the story. In the paper, we sketch a model built on the same principles which allows state to be encapsulated hidden from the interface and retained from one environment question to the next. And there's no reason why the principles we've used

couldn't be applied to more complex game models which could support things like high order function or concurrency. Wrapping up, we've seen that game semantics and dual non-determinism go hand in hand

in a beautiful way and that if we reinterpret traditional constructions with this lens, we can build very expressive models that can be used for large scale verification. The model that I've described built on these principles introduces several innovations.

For the first time, we combine the game semantics with the full specification power of the refinement calculus. We have shown that we can decouple non-determinism from the structure of plays and that our approach allows us to handle the very different components of certified abstraction layers

in a uniform and algebraic way. So, I will leave you with that. I hope you enjoyed the talk and thanks for listening.