2012-10-04

## Implementing a stack with proofs in ATS

This post works through an example of a `stack`

datatype, adding ATS features as we go along to help prove the implementation is correct. The example starts with a simplified stack of integers. I then add some dependent types to improve checking of the implementation and follow this with `dataprop`

usage for more extensive compile time checking.

I use `datatype`

when defining the `stack`

type. This requires the ATS garbage collector but keeps the code a bit simpler for those not used to reading ATS annotations. The code here is based on examples in the ATS distribution in the `doc/EXAMPLE/SPEC/stack`

directory but simplified for ease of explanation. This post documents the process I went through to understand that example better.

The example code can be found in this github gist:

```
git clone git://gist.github.com/3826469.git
```

## Stack

The code for this is in the gist as stack1.dats.

The definition of the first `stack`

implementation is:

```
datatype stack =
| stack_nil
| stack_cons of (int, stack)
fun stack_new (): stack
fun stack_is_empty (s: stack): bool
fun stack_top (s: stack): int
fun stack_pop (s: &stack): void
fun stack_push (s: &stack, x: int): void
```

The stack is represented as a list with the top of the stack being the head of the list. The stack is created with `stack_new`

and the remaining functions receive a reference to the stack (which is what the "&" means) so that they can modify it when pushing and popping. The implementation is:

```
implement stack_new () = stack_nil ()
implement stack_is_empty (s) =
case+ s of
| stack_nil () => true
| stack_cons _ => false
implement stack_push (s, x) = (s := stack_cons (x, s))
implement stack_top (s) =
case+ s of
| stack_nil () => (assertloc (false); 0)
| stack_cons (x,_) => x
implement stack_pop (s) =
case+ s of
| stack_nil () => assertloc (false)
| stack_cons (_, xs) => s := xs
```

An assertion is thrown if an attempt is made to get the top of an empty stack.

## Checking emptiness

The code for this is in the gist as stack2.dats.

Certain stack operations shouldn't work on an empty stack. This can be seen in the implementation of `stack_top`

and `stack_pop`

where it asserts at runtime if the stack is empty. One way of having the property checked at compile time is to add a boolean type index to the stack type that indicates if it is an empty stack or a non-empty stack:

```
datatype stack (bool) =
| stack_nil (true)
| {b:bool} stack_cons (false) of (int, stack b)
fun stack_new (): stack true
fun stack_is_empty {b:bool} (s: stack b): bool b
fun stack_top {b:bool} (s: stack false): int
fun stack_pop (s: &stack false >> stack b): #[b:bool] void
fun stack_push {b:bool} (s: &stack b >> stack false, x: int): void
```

In this definition `stack_nil`

has the type index set to `true`

to indicate at the type level that it is an empty stack. `stack_cons`

has the type index set to `false`

as a cons is a non-empty stack. A `stack_cons`

can be applied to a empty or non-empty stack as the second argument to the constructor so the definition allows an unconstrained `bool`

there.

The function definitions are changed to encode knowledge of the effect they have on the stack. `stack_new`

always returns an empty stack. `stack_top`

and `stack_pop`

can only work on non-empty stacks. The boolean result of `stack_is_empty`

returns a result which depends on the type of the stack it is given as an argument. This allows the type checker to reason about `stack`

emptiness state when `stack_is_empty`

is called.

The definition of `stack_pop`

uses `>>`

to change the type after calling so that the emptiness of the stack is no longer known. The `#[b:bool]`

syntax identifies `b`

as an existantial variable that can be referenced in the arguments. So we say here the emptiness state of the input stack is now unknown after calling.

`stack_push`

is similar but we say there that the emptiness state is unknown when called but known after calling - it will be a non-empty stack.

With this static checking in place the implementation of `stack_top`

and `stack_pop`

no longer needs the assertion:

```
implement stack_top (s) = let
val+ stack_cons (x,_) = s
in
x
end
implement stack_pop (s) = let
val+ stack_cons (_, xs) = s
in
s := xs
end
```

`val+`

does an exhaustive match. It fails at compile time if any other possible pattern match is valid. Calling code must ensure that a non-empty stack is passed to these functions.

```
implement main () = {
var s1 = stack_new ()
val a = stack_is_empty (s1)
val () = stack_push (s1, 10)
val b = stack_is_empty (s1)
val c = stack_top (s1)
val () = stack_pop (s1)
val d = stack_is_empty (s1)
}
```

This code contains no assertion checks but still type checks. This is because the type checker can follow the flow of the value of the emptiness state of the stack from `stack_new`

, which is always empty, through to the end of the function thanks to our additional type declarations on the stack functions. Checks are needed in the case of code like the following where the initial stack state is unknown:

```
fun mustcheck {b:bool} (s: stack b): void = {
val () = assertloc (not (stack_is_empty (s)))
val c = stack_top (s)
}
```

Without the `assertloc`

this code won't compile as `stack_top`

can't tell statically whether the stack is empty or not. Note that if the function were to push onto the stack then the `assertloc`

isn't needed as the declaration for `stack_push`

indicates the stack can't be empty:

```
fun nocheck {b:bool} (s: &stack b >> stack false): void = {
val () = stack_push (s, 42)
val c = stack_top (s)
}
```

This example can be improved further by using an integer type index representing the number of items on the stack instead of using a `bool`

. The push and pop operations can increment and decrement this index. This would give the type checker more information on pop operations as it could infer when pop results in an empty stack rather than the unknown result the current example results in. I leave this as an exercise for the reader as our next iteration provides this and more by taking a slightly different approach.

## Checking a stack really is a stack

The code for this is in the gist as stack3.dats.

For this iteration of the stack code we'll be changing the approach a bit. Previously we verified our usage of `stack`

was correct in certain cases. In this approach we'll verify that the implementation of `stack`

matches the specification of being a stack. To do this we'll first model a `list`

in the 'static' type system of ATS (the type system of type indexes and done using `datasort`

) and then define some `dataprop`

relations that specify what each stack operation means in terms of this static `list`

:

```
datasort ilist =
| inil
| icons of (int, ilist)
```

The following `dataprop`

constructs look very similar to the `datatype`

construct used in the ATS dynamic type system. The resulting `prop`

is used to encode a relation that can be used as a proof in functions. We define props `EMPTY`

, `IS_EMPTY`

, `TOP`

, `PUSH`

and `POP`

for each of the standard `stack`

operations.

`EMPTY`

is an empty stack. It has one constructor, also called `EMPTY`

that has a list as an argument that must be `inil`

, the constructor for the empty `ilist`

sort.

```
dataprop EMPTY (ilist) =
| EMPTY (inil)
```

`IS_EMPTY`

has two constructors, one for the case when the list is empty and one for when it is not. The prop is indexed by the `ilist`

and a boolean. It encodes the relation that the given `ilist`

is empty if the boolean is `true`

. The `IS_EMPTY_true`

constructor shows that a `inil`

list is empty. The `IS_EMPTY_false`

constructor shows that a `icons`

is not empty.

```
dataprop IS_EMPTY (ilist, bool) =
| IS_EMPTY_true (inil, true)
| {x:int} {xs:ilist} IS_EMPTY_false (icons (x,xs), false)
```

The `TOP`

prop encodes the relation that the given `ilist`

has the given value at the top of the stack. The `TOP`

constructor does this by pattern matching the `icons`

and using the head of the `icons`

as the value.

```
dataprop TOP (ilist, int) =
| {x:int} {xs:ilist} TOP (icons (x,xs), x)
```

The `PUSH`

prop has three index arguments. it encodes the relation that the first list, when having the 2nd argument pushed onto it, results in the third list. The `PUSH`

constructor shows how this is done.

```
dataprop PUSH (ilist, int, ilist) =
| {x:int} {xs,ys:ilist} PUSH (xs, x, icons (x, xs))
```

The `POP`

prop has two index arguments, both are lists. It encodes the relation that the first list, when pop is called on it, will result in the second list. The `POP`

constructor implementation shows this.

```
dataprop POP (ilist, ilist) =
| {x:int} {xs:ilist} POP (icons (x,xs), xs)
```

These `dataprop`

definitions form the basic specification for a stack. Instead of implementing the specification as functions they are encoded as `prop`

types so they can be used in proofs of an actual implementation to test that the implementation conforms to the specification. It's important though to do some checks that the specification itself is correct. These checks can be done as proof functions in ATS. Proof functions are checked during compilation then erased at code generation time so they have no run time overhead.

The following proof function asserts that when a push of a value `x`

on a stack `xs`

results in a stack `ys`

, the `top`

of the `ys`

will be the `x`

that was pushed:

```
prfun stack_push_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> TOP (ys, x) = let
prval PUSH () = pf
in
TOP ()
end
```

Note that the implementation of the proof function is trivial. The assignment in the first implementation line will set the universal variables in the `PUSH`

constructor from the values in the type of `pf`

. The return of `TOP ()`

then matches the appropriate values based on the return type of the proof function. It basically checks that (psuedo code):

```
val ys = icons (x, xs) // PUSH
val icons (x', xs') = ys // TOP
x' == x && xs' = xs
```

The `.<>.`

syntax in the proof function means the function is non-recursive and terminates. The `:<>`

syntax means the proof function is pure (has no side effects). These are requirements for functions involving proofs.

The following proof function asserts that popping a value off the stack resulting from a push operation results in the same stack as the original:

```
prfun stack_pop_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> POP (ys, xs) = let
prval PUSH () = pf
in
POP ()
end
```

This proof function asserts that `is_empty`

on an empty list is true:

```
prfun stack_empty_check {xs:ilist} .<>. (pf: EMPTY xs):<> IS_EMPTY (xs, true) = let
prval EMPTY () = pf
in
IS_EMPTY_true ()
end
```

With these definitions in a file you can run the ATS type checker to confirm that the specifications passes the checks using the `-tc`

command line option:

```
$ atscc -tc stack3.dats
The file [stack3.dats] is successfully typechecked!
```

## Implementing a stack checked against the specification

The code for this is in the gist as stack4.dats.

Given the specification for the stack operations in the previous section we can now write a `stack`

implementation where proofs are used to ensure the implementation matches the spec. The first step is to define the `stack`

datatype indexed by the `ilist`

sort:

```
datatype stack (ilist) =
| stack_nil (inil)
| {x:int} {xs:ilist} stack_cons (icons (x,xs)) of (int x, stack xs)
```

The functions that implement the stack operations take and return the proof objects defined by the `dataprop`

definitions for the stack operations. Proof arguments in ATS functions are seperated from normal function arguments by a pipe,`|`

, symbol. All those arguments to the left of the `|`

are proof arguments:

```
fun stack_new (): [xs:ilist] (EMPTY xs | stack xs)
fun stack_is_empty {xs:ilist} (s: stack xs): [b:bool] (IS_EMPTY (xs, b) | bool b)
fun stack_top {xs:ilist} (pf: IS_EMPTY (xs, false) | s: stack xs): [x:int] (TOP (xs, x) | int x)
fun stack_pop {x:int} {xs:ilist} (pf: IS_EMPTY (xs, false) | s: &stack xs >> stack ys)
: #[ys:ilist] (POP (xs, ys) | void)
fun stack_push {x:int} {xs:ilist} (s: &stack xs >> stack ys, x: int x)
: #[ys:ilist] (PUSH (xs, x, ys) | void)
```

The `stack_top`

and `stack_pop`

functions require the caller to provide a proof that the stack is not empty. All the operations return a proof that is used to ensure the implementation of the function is correct (as defined by the relations we wrote previously).

```
implement stack_new () = (EMPTY () | stack_nil ())
implement stack_is_empty (s) =
case+ s of
| stack_nil () => (IS_EMPTY_true | true)
| stack_cons _ => (IS_EMPTY_false | false)
implement stack_push {x} {xs} (s, x) = (PUSH () | (s := stack_cons (x, s)))
implement stack_top (pf | s) = let
prval IS_EMPTY_false () = pf
val+ stack_cons (x,_) = s
in
(TOP () | x)
end
implement stack_pop (pf | s) = let
prval IS_EMPTY_false () = pf
val+ stack_cons (_, xs) = s
in
(POP () | s := xs)
end
```

The main changes compared to the previous implementations we've done of `stack`

is to handle the proof arguments. The handling is mostly trivial in that we assign the argument to the expected type (eg. `IS_EMPTY_false`

if we expect the stack to be empty) and we use the constructors for returning the proofs for the various operations. The actual checking that the implementation is correct is done by the ATS proof system using the types and variables defined in the `dataprop`

statements in a similar manner to the proof check functions discussed earlier. The proofs are erased at code generation time and the resulting `C`

code is exactly as if it was written without the proofs - with the knowledge that the code is correct as it was checked at compile time.

The additional proof code does impose a syntactical burden to the user of the stack code. For example:

```
fun mustcheck {xs:ilist} (s: stack xs): void = {
val (pf | e) = stack_is_empty (s)
val () = assertloc (not e)
val (_ | c) = stack_top (pf | s)
}
```

In this check we need to pass the proof from the `stack_is_empty`

call to the `stack_top`

call. Even though we don't need the proof result of the `stack_top`

call we still need to match it against the wildcard `_`

symbol to ignore it. For the `nocheck`

example shown previously:

```
fun nocheck {xs:ilist} (s: &stack xs >> stack ys): #[ys:ilist] void = {
val (pf | ()) = stack_push (s, 42)
prval PUSH () = pf
val (_ | c) = stack_top (IS_EMPTY_false () | s)
}
```

We need to do a proof assignment of the `stack_push`

proof result for the code to correctly infer that the stack is not empty and the `IS_EMPTY_false`

proof we construct is correct. The `main`

function showing basic stack usage becomes:

```
implement main () = {
val (_ | s) = stack_new ()
var s1 = s
val (_ | a) = stack_is_empty (s1)
val (pf | ()) = stack_push (s1, 10)
prval PUSH () = pf
val (_ | b) = stack_is_empty (s1)
val (_ | c) = stack_top (IS_EMPTY_false () | s1)
val (pf | ()) = stack_pop (IS_EMPTY_false () | s1)
prval POP () = pf
val (_ | d) = stack_is_empty (s1)
}
```

We can ignore many of the proofs here so they are pattern matched with the wildcard symbol `_`

. The use of `prval PUSH () = pf`

is needed to allow the `stack_top`

and `stack_pop`

calls to to be successfully checked. The equivalent for `POP`

would be needed if we used `stack_top`

or `stack_pop`

after that call.

The benefit of the additional proof code is that we can be assured that the `stack`

implementation matches our stack specification. The implementation is verified to be correct and our usage is verified to be correct. Any changes to the implementation will fail to compile if they don't match the specification (popping too many elements off the stack for example). We can write alternate stack implementations that use the same stack proofs to verify that those implementations are correct. The ATS distribution includes an implementation based on lists and arrays in the `doc/EXAMPLE/SPEC/stack`

directory.

## Non-integer stacks

The code for this is in the gist as stack5.dats.

The implementation shown previously is simplified in that it is a stack of integers. The nicely matches the `ilist`

sort which is a list of integers. Handling verification of a stack that contains a non-integer type requires a workaround. We keep the `ilist`

sort and proofs but introduce a new abstract type that maps our actual stack element type to an int sort. In the following example we create a stack of `double`

values. The abstract type that is the placeholder for the real element type is:

```
abst@ype E (t@ype,int) = double
castfn encode (x: double):<> [x:int] E (double, x)
castfn decode {i:int} (x: E (double, i)):<> double
```

Included are two cast functions to convert from the placeholder value to our real value and back. The abstract type is set to be the same size as our element type so the compiler can treat it exactly as if it was a `double`

. The `stack`

datatype and functions are written to use the abstract type instead of the real type:

```
datatype stack (ilist) =
| stack_nil (inil)
| {x:int} {xs:ilist} stack_cons (icons (x,xs)) of (E (double, x), stack xs)
fun stack_top {xs:ilist} (pf: IS_EMPTY (xs, false) | s: stack xs)
: [x:int] (TOP (xs, x) | E (double, x))
fun stack_push {x:int} {xs:ilist} (s: &stack xs >> stack ys, x: E (double, x))
: #[ys:ilist] (PUSH (xs, x, ys) | void)
```

I only show the functions that have changed here. The changes are minor but the caller will need to use `encode`

and `decode`

when calling and retrieving values:

```
val (pf | ()) = stack_push (s1, encode 10.0)
val (_ | c) = stack_top (IS_EMPTY_false () | s1)
val () = printf("%f\n", @(decode c))
```

The generated `C`

code is as efficient as the original stack however. The compiler knows the exact size of the placeholder type as we assign it in the `abst@ype`

definition. The cast functions are no-ops at generation time.

This approach can be made generic by adding the element type as an index to the `stack`

type and making the stack functions template functions. I leave that as an exercise for the reader but the `doc/EXAMPLE/SPEC/stack`

example shipped with ATS shows the way.

## Conclusion

This approach to proof checking has some syntactical overhead when writing and reading code. One could imagine an IDE (or emacs mode) that allowed the user to hide or display proofs as required to help reduce the overhead. Once familiar with proof code it may not be so noticeable, much like how parenthesis in Lisp disappear to the experienced developer.

More information and examples on proof checking in ATS are available at: