Bluish Coder

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:

• Theorem-Proving in ATS
• Programming with Theorem-Proving
• Combining Programming with Theorem-Proving (PDF Paper)