2018-01-03

## Writing basic proofs in ATS

This post covers using the latest version of ATS, ATS 2, and goes through proving some basic algorithms. I've written a couple of posts before on using proofs in ATS 1:

Writing proofs in ATS is complicated by the fact that the dependent types and proof component of the language does not use the full ATS language. It uses a restricted subset of the language. When implementing a proof for something like the factorial function you can't write factorial in the type system in the same way as you write it in the runtime system. Factorial in the latter is written using a function but in the former it needs to be encoded as relations in dataprop or dataview definitions.

Recent additions to ATS 2 have simplified the task of writing some proofs by enabling the constraint checking of ATS to be done by an external SMT solver rather than the built in solver. External solvers like Z3 have more features than the builtin solver and can solve constraints that the ATS solver cannot. For example, non-linear constraints are not solveable by ATS directly but are by using Z3 as the solver.

In this post I'll start by describing how to write proofs using quantified constraints. This is the easiest proof writing method in ATS but requires Z3 as the solver. Next I'll continue with Z3 as the solver but describe how to write proofs using Z3 without quantified constraints. Finally I'll go through writing the proofs by encoding the algorithm as relations in dataprop. This approach progressively goes from an easy, less intrusive to the code method, to more the more difficult system requiring threading proofs throughout the code.

## Installing Z3

Z3 is the external solver used in the examples in this post. To install from the Z3 github on Linux:

```
$ git clone https://github.com/Z3Prover/z3
$ cd z3
$ mkdir build
$ cd build
$ cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../
$ make && sudo make install
```

## Installing ATS

I used ATS2-0.3.8 for the examples in this post. There are various scripts for installing but to do install manually from the git repository on an Ubuntu based system:

```
$ sudo apt-get install build-essential libgmp-dev libgc-dev libjson-c-dev
$ git clone git://git.code.sf.net/p/ats2-lang/code ATS2
$ git clone https://github.com/githwxi/ATS-Postiats-contrib.git ATS2-contrib
$ export PATSHOME=`pwd`/ATS2
$ export PATSCONTRIB=`pwd`/ATS2-contrib
$ export PATH=$PATSHOME/bin:$PATH
$ (cd ATS2 && ./configure && make all)
$ (cd ATS2/contrib/ATS-extsolve && make DATS_C)
$ (cd ATS2/contrib/ATS-extsolve-z3 && make all && mv -f patsolve_z3 $PATSHOME/bin)
$ (cd ATS2/contrib/ATS-extsolve-smt2 && make all && mv -f patsolve_smt2 $PATSHOME/bin)
```

Optionally you can install the various ATS backends for generating code in other languages:

```
$ (cd ATS2/contrib/CATS-parsemit && make all)
$ (cd ATS2/contrib/CATS-atscc2js && make all && mv -f bin/atscc2js $PATSHOME/bin)
$ (cd ATS2/contrib/CATS-atscc2php && make all && mv -f bin/atscc2php $PATSHOME/bin)
$ (cd ATS2/contrib/CATS-atscc2py3 && make all && mv -f bin/atscc2py3 $PATSHOME/bin)
```

Add `PATSHOME`

, `PATSCONTRIB`

and the change to `PATH`

to `.bash-rc`

, `.profile`

, or some other system file to have these environment variables populated when starting a new shell.

## Dependent Types

A function to add numbers in ATS can be proven correct using dependent types by specifying the expected result using dependently typed integers:

```
fun add_int {m,n:int} (a: int m, b: int n): int (m + n) = a + b
```

This won't compile if the implementation does anything but result in the addition of the two integers. The constraint language used in dependent types is a restricted subset of the ATS language. I wrote a bit about this in my post on dependent types in ATS.

The following is an implementation of the factorial function without proofs:

```
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
fun fact (n: int): int =
if n > 0 then n * fact(n- 1) else 1
implement main0() = let
val r = fact(5)
in
println!("5! = ", r)
end
```

Compile and run with something like:

```
$ patscc -o f0 f0.dats
$ ./f0
5! = 120
```

To prove that the implementation of factorial is correct we need to specify what factorial is in the constraint language of ATS. Ideally we'd like to write something like the following:

```
fun fact {n: nat} (n: int n): int (fact(n)) = ...
```

This would check that the body of the function implements something that matches the result of `fact`

. Unfortunately the restricted constraint language of ATS doesn't allow implementing or using arbitary functions in the type definition.

## Using Z3 as an external solver

By default ATS solves constraints using its built in constraint solver. It has a mechanism for using an external solver, in this case Z3. To type check the previous factorial example using Z3 use the following commands:

```
$ patsopt -tc --constraint-export -d f0.dats |patsolve_z3 -i
Hello from [patsolve_z3]!
typechecking is finished successfully!
```

Note the change to use `patsopt`

instead of `patscc`

. The `-tc`

flag does the type checking phase only. `--constraint-export`

results in the constraints to be exported to `stdout`

which is piped to `patsolve_z3`

. That command invokes Z3 and checks the constraint results.

Since the resulting program may contain code that ATS can't typecheck itself, to actually build the final executable we invoke `patscc`

with a command line option to disable type checking. It's important that the checking has succeeded through the external solver before doing this!

```
$ patscc --constraint-ignore -o f0 f0.dats
```

## Z3 and quantified constraints

Using Z3 with quantified constraints is a new feature of ATS and quite experimental. Hongwei notes some issues due to different versions of Z3 that can cause problems. It is however an interesting approach to proofs with ATS so I include the process of using it here and hope it becomes more stable as it progresses.

ATS provides the `stacst`

keyword to introduce a constant into the 'statics' part of the type system. The 'statics' is the restricted constraint language used when specifying types. There are some examples of `stacst`

usage in the prelude file basics_pre.sats.

Using `stacst`

we can introduce a function in the statics system for factorial:

```
stacst fact: int -> int
```

Now the following code is valid:

```
fun fact {n:nat} (n: int n): int (fact(n)) = ...
```

ATS doesn't know about `fact`

in the statics system, it only knows it's a function that takes an `int`

and returns an `int`

. With Z3 as the external solver we can extend ATS' constraint knowledge by adding assertions to the Z3 solver engine using `$static_assert`

:

```
praxi fact_base(): [fact(0) == 1] void
praxi fact_ind {n:int | n >= 1} (): [fact(n) == n * fact(n-1)] void
```

The keyword `praxi`

is used for defining axioms, whereas `prfun`

is used for proof functions that need an implementation. This is currently not checked by the compiler but may be at some future time. From a documentation perspective using `praxi`

shows no plan to actually prove the axiom.

The two axioms here will add to the proof store the facts about the factorial function. The first, `fact_base`

, asserts that the factorial of zero is one. The second asserts that for all `n`

, where `n`

is greater than or equal to `1`

, that the factorial of `n`

is equivalent to `n * fact (n - 1)`

.

To add these facts to Z3's knowledge, use `$solver_assert`

:

```
fun fact {n:int | n >= 0} (n: int n): int (fact(n)) = let
prval () = $solver_assert(fact_base)
prval () = $solver_assert(fact_ind)
in
if n = 0 then 1 else n * fact(n - 1)
end
```

This typechecks successfully. Changing the implementation to be incorrect results in a failed typecheck. Unfortunately, as is often the case with experimental code, sometimes an incorrect implementation will hang Z3 causing it to consume large amounts of memory as noted earlier.

The implementation of `fact`

here closely mirrors the specification. The following is a tail recursive implementation of `fact`

that is also proved correct to the specification:

```
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
stacst fact: int -> int
extern praxi fact_base(): [fact(0) == 1] unit_p
extern praxi fact_ind{n:pos}(): [fact(n)==n*fact(n-1)] unit_p
fun fact {n:nat} (n: int n): int (fact(n)) = let
prval () = $solver_assert(fact_base)
prval () = $solver_assert(fact_ind)
fun loop {n,r:nat} (n: int n, r: int r): int (fact(n) * r) =
if n > 0 then loop (n - 1, n * r) else r
in
loop (n, 1)
end
implement main0() = let
val r = fact(5)
in
println!("5! = ", r)
end
```

This was tested and built with:

```
$ patsopt -tc --constraint-export -d f4.dats |patsolve_z3 -i
Hello from [patsolve_z3]!
typechecking is finished successfully!
$ patscc --constraint-ignore -o f4 f4.dats
./f4
5! = 120
```

## Z3 with threaded proofs

Another approach to using the external solver is not to add constraints to the Z3 store via `$solver_assert`

but instead call the axioms explicitly as proof functions threaded in the body of the function. This is `fact`

implemented in such a way:

```
stacst fact: int -> int
extern praxi fact_base(): [fact(0) == 1] void
extern praxi fact_ind {n:int | n >= 1} (): [fact(n) == n * fact(n-1)] void
fun fact {n:nat} (n: int n): int (fact(n)) =
if n > 0 then let
prval () = fact_ind {n} ()
in
n * fact(n - 1)
end
else let
prval () = fact_base()
in
1
end
```

The code is more verbose due to needing to embed the `prval`

statements in a `let`

block but it doesn't suffer the Z3 incompatibility that the quantified constraint example did. An incorrect implementation will give an error from Z3.

The equivalent tail recursive version is:

```
fun fact {n:nat} (n: int n): int (fact(n)) = let
fun loop {n,r:nat} (n: int n, r: int r): int (fact(n) * r) =
if n > 0 then let
prval () = fact_ind {n} ()
in
loop (n - 1, n * r)
end
else let
prval () = fact_base()
in
r + 1
end
in
loop (n, 1)
end
```

## Dataprops and Datatypes

It's still possible to write a verified version of factorial without using an external solver but the syntactic overhead is higher. The specification of `fact`

needs to be implemented as a relation using `dataprop`

. A `dataprop`

introduces a type for the proof system in much the same way as declaring a datatype in the runtime system of ATS. Proof objects constructed from this type exist only at proof checking time and are erased at runtime. They can be taken as proof arguments in functions or included in return values. Proof functions can also be written to use them. In the words of Hongwei Xi:

A prop is like a type; a value classified by a prop is often called a proof, which is dynamic but erased by the compiler. So while proofs are dynamic, there is no proof construction at run-time.

For a comparison of the syntax of `dataprop`

and `datatype`

, here is a type for "list of integers" implement as both:

```
dataprop prop_list =
| prop_nil
| prop_cons of (int, prop_list)
datatype list =
| list_nil
| list_cons of (int, list)
```

To specifiy `fact`

as a relation it is useful to see how it is implemented in a logic based progamming language like Prolog:

```
fact(0, 1).
fact(N, R) :-
N > 0,
N1 is N - 1,
fact(N1, R1),
R is R1 * N.
```

The equivalent as a `dataprop`

is:

```
dataprop FACT (int, int) =
| FACTzero (0, 1)
| {n,r1:int | n > 0} FACTsucc (n, r1 * n) of (FACT (n-1, r1))
```

`FACT(n,r)`

encodes the relation that `fact(n) = r`

where fact is defined as:

- fact(0) = 1, and
- fact(n) where n > 0 = n * fact(n - 1)

The `dataprop`

creates a `FACT(int, int)`

prop with two constructors:

`FACTzero()`

which encodes the relation that`fact(0) = 1`

, and`FACTsucc(FACT(n-1, r1))`

which encodes the relation that`fact(n) = n * fact(n-1)`

The declaration of the `fact`

function uses this prop as a proof return value to enforce that the result must match this relation:

```
fun fact {n:nat} (n: int n): [r:int] (FACT (n, r) | int r) = ...
```

The return value there is a tuple, where the first element is a proof value (the left of the pipe symbol) and the second element is the factorial result. The existential variable `[r:int]`

is used to associate the returned value with the result of the `FACT`

relation and the universal variable, `{n:nat}`

is used to provide the first argument of the fact prop. Through unification the compiler checks that the relationships between the variables match.

The implementation of the function is:

```
fun fact {n:nat} (n: int n): [r:int] (FACT (n, r) | int r) =
if n > 0 then let
val (pf1 | r1) = fact (n - 1)
val r = n * r1
in
(FACTsucc (pf1) | r)
end else begin
(FACTzero () | 1)
end
```

Note that the result of the recursive call to `fact`

deconstructs the proof result into `pf1`

and the value into `r1`

and that proof is used in the result of the `FACTsucc`

constructor. Proofs are constructed like datatypes. For example:

`FACTsucc(FACTzero())`

is`fact(1)`

(the successor, or next factorial, from`fact(0)`

.`FACTsucc(FACTsucc(FACTzero()))`

is`fact(2)`

, etc.

In this way it can be seen that a call to `fact(1)`

will hit the first branch of the `if`

condition which recursively calls `fact(0)`

. That hits the second branch of the conditional to return the prop `FACTzero()`

. On return back to the caller this is returned as `FACTsucc(FACTzero())`

, giving our prop return type as `FACT(1, 1)`

. Plugging these values into the `n`

and `r`

of the return type for the `int r`

value means that value the function returns must be `1`

for the function to pass type checking.

Although these proofs have syntactic overhead, the runtime overhead is nil. Proofs are erased after typechecking and only the factorial computation code remains. The full compilable program is:

```
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
dataprop FACT (int, int) =
| FACTzero (0, 1)
| {n,r1:int | n > 0} FACTsucc (n, r1 * n) of (FACT (n-1, r1))
fun fact {n:nat} (n: int n): [r:int] (FACT (n, r) | int r) =
if n > 0 then let
val (pf1 | r1) = fact (n - 1)
val r = n * r1
in
(FACTsucc (pf1) | r)
end else begin
(FACTzero () | 1)
end
implement main0() = let
val (pf | r) = fact(5)
in
println!("5! = ", r)
end
```

To compile and run:

```
$ patscc -o f8 f8.dats
$ ./f8
5! = 120
```

A tail recursive implementation of `fact`

using dataprop that type checks is:

```
fun fact {n:nat} (n: int n): [r:int] (FACT (n, r) | int r) = let
fun loop {r:int}{i:nat | i <= n}
(pf: FACT(i, r) | n: int n, r: int r, i: int i):
[r1:int] (FACT(n, r1) | int (r1)) =
if n - i > 0 then
loop (FACTsucc(pf) | n, (i + 1) * r, i + 1)
else (pf | r)
in
loop (FACTzero() | n, 1, 0)
end
```

Because our dataprop is defined recursively based on successors to a previous factorial, and we can't get a predecessor, the tail recursive loop is structured to count up. This means we have to pass in the previous factorial prop as a proof argument, in `pf`

, and pass an index, `i`

, to be the current factorial being computed.

## Fibonacci

Fibonacci is similar to factorial in the way the proofs are constructed. The quantified constraints versions is trivial:

```
stacst fib: int -> int
extern praxi fib0(): [fib(0) == 0] unit_p
extern praxi fib1(): [fib(1) == 1] unit_p
extern praxi fib2 {n:nat|n >= 2} (): [fib(n) == fib(n-1) + fib(n-2)] unit_p
fun fib {n:int | n >= 0} (n: int n): int (fib(n)) = let
prval () = $solver_assert(fib0)
prval () = $solver_assert(fib1)
prval () = $solver_assert(fib2)
in
if n = 0 then 0
else if n = 1 then 1
else fib(n-1) + fib(n -2)
end
```

The threaded version using the external solver isn't much more verbose:

```
stacst fib: int -> int
extern praxi fib0(): [fib(0) == 0] void
extern praxi fib1(): [fib(1) == 1] void
extern praxi fib2 {n:nat|n >= 2} (): [fib(n) == fib(n-1) + fib(n-2)] void
fun fib {n:int | n >= 0} (n: int n): int (fib(n)) =
if n = 0 then let
prval () = fib0()
in
0
end
else if n = 1 then let
prval () = fib1()
in
1
end
else let
prval () = fib2 {n} ()
in
fib(n-1) + fib(n -2)
end
```

The dataprop version is quite readable too and has the advantage of not needing an external solver:

```
dataprop FIB (int, int) =
| FIB0 (0, 0)
| FIB1 (1, 1)
| {n:nat}{r0,r1:int} FIB2(n, r1+r0) of (FIB(n-1, r0), FIB(n-2, r1))
fun fib {n:nat} (n: int n): [r:int] (FIB (n, r) | int r) =
if n = 0 then (FIB0() | 0)
else if n = 1 then (FIB1() | 1)
else let
val (pf0 | r0) = fib(n-1)
val (pf1 | r1) = fib(n-2)
in
(FIB2(pf0, pf1) | r0 + r1)
end
```

The dataprop maps nicely to the Prolog implementation of fibonacci:

```
fib(0,0).
fib(1,1).
fib(N,R) :- N1 is N-1, N2 is N-2, fib(N1,R1),fib(N2,R2),R is R1+R2.
```

I leave proving different implementations of `fib`

to the reader.

## Conclusion

There are more algorithms that could be demonstrated but this post is getting long. Some pointers to other interesting examples and articles on ATS and proofs:

- Rock, Paper, Scissors in the type system
- ATS/LF for Coq Users
- Theorem proving in ATS/LF
- Programming with Theorem proving
- Encoding Propositional Logic
- Two styles of theorem proving in ATS

In general proof code adds a syntactic overhead to the code. With more work on using external solvers it looks like things will become easier with automated solving. ATS allows the programmer to write normal code and add proofs as needed so the barrier to entry to applying proofs is quite low, given suitable documentation and examples.