Ats + z3

Google Group
1

I would like to bring people’s attention to the following ongoing project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

The basic idea is to use Z3 (https://github.com/Z3Prover/z3) to solve the
constraints generated
during ATS2-typechecking. I want to first thank Will Blair for his piloting
work on this project. For more,
please visit:

http://www.illtyped.com/projects/patsolve/

The Makefile in the following directory shows how to export constraints
generated during typechecking
a program in ATS:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST

Basically, it goes like this:

patsopt -tc --constraint-export -o foo_dats_constraint.json -d foo.dats

for exporting the generated constraints. And the exported constraints can
be solved like this:

patsolve_z3 -i foo_dats_constraint.json

where patsolve_z3 is the main command generated from compiling the
ATS-extsolve-z3 project.

Patsolve_z3 starts to be functioning as of now. However, this is really
just the very beginning and
there will be a lot more coming gradually. With Z3, ATS is expected to
reach a much higher level
in terms of program verification.

Cheers!

–Hongwei

2

I would like to bring people’s attention to the following ongoing project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

The basic idea is to use Z3 (GitHub - Z3Prover/z3: The Z3 Theorem Prover) to solve the
constraints generated
during ATS2-typechecking.

I did this kind of thing in Felix at one stage, using compiler stuff to emit
user axioms and theorems in WHY format so WHY should then be
run to invoke automatic theorem provers.

This added two more processes communicating with text that
had to be parsed on both output an input and of course provers
aren’t always fast, so it was done offline.

I eventually removed it because WHY was too experimental and kept
changing, also getting hold of and configuring the external provers wasn’t
too hard
on Linux but on other platforms proved very difficult.

You will also have the tricky problem that the solvers aren’t quite aligned
with what is actually required by your compiler.

Still, congratulations, I think this is the right way to go.
Leveraging separate projects is tricky and the loss of control is worrying
but in the end, a compiler writer simply cannot do everything.
In the end, you have to delegate most of the library development too.
And then, split the compiler into modules and delegate parts of that
as well (eg optimisation, parsing, back end etc).

john skaller
skaller@…
http://felix-lang.org

3

What do you mean with “Z3 crashed”?

In Z3’s C API, whenever you get an object you need to increase its
reference count, and then decrease its reference count when you are
finished with it. With my first prototype, I never decreased any reference
counts so Z3 eventually ran out of memory and stopped with an “out of
memory” error.Am Samstag, 13. Juni 2015 04:07:42 UTC-4 schrieb Yannick Duchêne:

Le vendredi 12 juin 2015 17:26:57 UTC+2, William Blair a écrit :

When I first worked on a prototype, all of Z3’s objects were non-linear
and I didn’t try to manage resources. Eventually, type checking large
programs consumed so much memory Z3 crashed. Fixing this issue was
pretty straightforward. After I made Z3 objects linear and described how
the API produced and consumed objects, the type checker specified every
place where memory could be leaked.

What do you mean with “Z3 crashed”? Do you mean it suddenly stopped
it‑self or do you mean it was stopped after it tried to execute invalid
instructions?

4

I made significant progress today regarding the ATS-extsolve-z3
project. Now the generated command patsolve_z3 can be used to
compile ATSLIB/prelude and ATSLIB/libats.

Following is an example that cannot be handled by patsopt but can be
by patsolve_z3. Note that ‘fact’ is introduced as a “foreign” static
function
in this example.

At this stage, I do not really have a good feel as to what can or cannot be
proven in Z3. However, I do feel that Z3 is very flexible and can become a
very powerful too if one knows how to use it properly.

Cheers!

( ****** ****** )
//
stacst fact: int → int
//
( ****** ****** )
//
extern
praxi
fact_bas(): [fact(0)==1] void
extern
praxi
fact_ind{n:pos}(): [fact(n)==nfact(n-1)] void
//
(* ****** ****** )
//
fun
fact
{n:nat}
(n: int(n))
: int(fact(n)) = let
//
fun
loop
{n:nat}
{r:int} ..
(
n: int(n), r: int(r)
) : int(fact(n)r) = (
//
if
n = 0
then let
prval () = fact_bas() in (r)
end // end of [then]
else let
prval () = fact_ind{n}() in loop(n-1, nr)
end // end of [else]
//
) ( end of [loop] *)
//
in
loop(n, 1)
end // end of [fact]

(* ****** ****** *)On Saturday, June 6, 2015 at 5:26:03 PM UTC-4, gmhwxi wrote:

I would like to bring people’s attention to the following ongoing project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

The basic idea is to use Z3 (GitHub - Z3Prover/z3: The Z3 Theorem Prover) to solve the
constraints generated
during ATS2-typechecking. I want to first thank Will Blair for his
piloting work on this project. For more,
please visit:

http://www.illtyped.com/projects/patsolve/

The Makefile in the following directory shows how to export constraints
generated during typechecking
a program in ATS:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST

Basically, it goes like this:

patsopt -tc --constraint-export -o foo_dats_constraint.json -d foo.dats

for exporting the generated constraints. And the exported constraints can
be solved like this:

patsolve_z3 -i foo_dats_constraint.json

where patsolve_z3 is the main command generated from compiling the
ATS-extsolve-z3 project.

Patsolve_z3 starts to be functioning as of now. However, this is really
just the very beginning and
there will be a lot more coming gradually. With Z3, ATS is expected to
reach a much higher level
in terms of program verification.

Cheers!

–Hongwei

5

At this stage, I do not really have a good feel as to what can or cannot be
proven in Z3. However, I do feel that Z3 is very flexible and can become a
very powerful too if one knows how to use it properly.

Isn’t it entirely transparent from an ATS user point of view?

Also, will this become the default in the future? (the question may raise,
if using Z3 makes so much difference)

6

I made significant progress today regarding the ATS-extsolve-z3
project. Now the generated command patsolve_z3 can be used to
compile ATSLIB/prelude and ATSLIB/libats.

Curious are you using direct C interface or LIB-SMT language text?

john skaller
ska...@users.sourceforge.net
http://felix-lang.org

7

Curious are you using direct C interface or LIB-SMT language text?

Right now, it uses the C API for Z3. You could have the constraint solver
generate smt-lib text without too much trouble though.

Since Z3 requires the programmer manage reference counting for all of its
objects, the C api can be difficult to use. In the constraint solver, all
these objects are linear, so the typechecker can make the process a lot
easier.

When I first worked on a prototype, all of Z3’s objects were non-linear and
I didn’t try to manage resources. Eventually, type checking large programs
consumed so much memory Z3 crashed. Fixing this issue was pretty
straightforward. After I made Z3 objects linear and described how the API
produced and consumed objects, the type checker specified every place where
memory could be leaked.

I think this process of program refinement is a great example of how linear
types can simplify working with low level interfaces.Am Montag, 8. Juni 2015 05:44:18 UTC-4 schrieb John Skaller:

On 08/06/2015, at 4:14 PM, gmhwxi wrote:

I made significant progress today regarding the ATS-extsolve-z3
project. Now the generated command patsolve_z3 can be used to
compile ATSLIB/prelude and ATSLIB/libats.

Curious are you using direct C interface or LIB-SMT language text?

–
john skaller
ska...@users.sourceforge.net <javascript:>
http://felix-lang.org

8

When I first worked on a prototype, all of Z3’s objects were non-linear
and I didn’t try to manage resources. Eventually, type checking large
programs consumed so much memory Z3 crashed. Fixing this issue was
pretty straightforward. After I made Z3 objects linear and described how
the API produced and consumed objects, the type checker specified every
place where memory could be leaked.

What do you mean with “Z3 crashed”? Do you mean it suddenly stopped it‑self
or do you mean it was stopped after it tried to execute invalid
instructions?

9

I updated ATS2-C9-install.sh:

which shows how patsolve_z3 can be built on Ubuntu
(assuming that Z3 is already installed).On Saturday, June 6, 2015 at 5:26:03 PM UTC-4, gmhwxi wrote:

I would like to bring people’s attention to the following ongoing project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

The basic idea is to use Z3 (GitHub - Z3Prover/z3: The Z3 Theorem Prover) to solve the
constraints generated
during ATS2-typechecking. I want to first thank Will Blair for his
piloting work on this project. For more,
please visit:

http://www.illtyped.com/projects/patsolve/

The Makefile in the following directory shows how to export constraints
generated during typechecking
a program in ATS:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST

Basically, it goes like this:

patsopt -tc --constraint-export -o foo_dats_constraint.json -d foo.dats

for exporting the generated constraints. And the exported constraints can
be solved like this:

patsolve_z3 -i foo_dats_constraint.json

where patsolve_z3 is the main command generated from compiling the
ATS-extsolve-z3 project.

Patsolve_z3 starts to be functioning as of now. However, this is really
just the very beginning and
there will be a lot more coming gradually. With Z3, ATS is expected to
reach a much higher level
in terms of program verification.

Cheers!

–Hongwei

10

I would like to bring people’s attention to the following ongoing project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

The basic idea is to use Z3 (GitHub - Z3Prover/z3: The Z3 Theorem Prover) to solve the
constraints generated
during ATS2-typechecking. I want to first thank Will Blair for his
piloting work on this project. For more,
please visit:
[…]

Given that it will be used for ATS, it’s worth to point the license seems
to have changed and no more has the limitation of “not allowed to design
commercial applications” (and an outrageous pricing otherwise) as it was
before. I just noticed it’s now MIT licensed.

11

Isn’t it entirely transparent from an ATS user point of view?

Actually, I feel it is going to be the opposite.

In general, constraint-solving is undecidable. So one may need to
generate both constraints and constraint-solving strategies (which
may depend on a particular constraint-solver).On Monday, June 8, 2015 at 4:07:14 AM UTC-4, Yannick Duchêne wrote:

Le lundi 8 juin 2015 08:14:42 UTC+2, gmhwxi a écrit :

At this stage, I do not really have a good feel as to what can or cannot
be
proven in Z3. However, I do feel that Z3 is very flexible and can become a
very powerful too if one knows how to use it properly.

Isn’t it entirely transparent from an ATS user point of view?

Also, will this become the default in the future? (the question may raise,
if using Z3 makes so much difference)

12

Thanks for sharing your insights.

By pure coincidence, implementing a constraint-solver for ATS based on Z3
is straightforward.

Probably more “synchronicity” than coincidence :slight_smile:

The real focus is
to find a reasonable way to support a style of constraint-solving that is
open-ended:
The programmer should be allowed to not only extend the statics of ATS
with additional
sorts and (static) functions symbols but also supply constraint-solvers
that can handle the
newly introduced functional symbols.

That sounds very hard.

Technically, it is probably not so difficult. But to get a synergistic
integration linguistically should prove an interesting challenge!

john skaller
skaller@…
http://felix-lang.org

13

Thanks for sharing your insights.

By pure coincidence, implementing a constraint-solver for ATS based on Z3
is straightforward. This is due to Z3 supporting a style of solver which I
would
refer to as being “stack-based”. This style precisely matches the way in
which
constraints in ATS are represented.

However, replacing the built-in constraint-solver of ATS with another
Z3-based
solver is really a by-product of the project of ATS-extsolve-z3. The real
focus is
to find a reasonable way to support a style of constraint-solving that is
open-ended:
The programmer should be allowed to not only extend the statics of ATS with
additional
sorts and (static) functions symbols but also supply constraint-solvers
that can handle the
newly introduced functional symbols.

Cheers!On Sat, Jun 6, 2015 at 6:44 PM, john skaller <skaller@…> wrote:

On 07/06/2015, at 7:27 AM, Hongwei Xi wrote:

I would like to bring people’s attention to the following ongoing
project:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3

The basic idea is to use Z3 (GitHub - Z3Prover/z3: The Z3 Theorem Prover) to solve
the constraints generated
during ATS2-typechecking.

I did this kind of thing in Felix at one stage, using compiler stuff to
emit
user axioms and theorems in WHY format so WHY should then be
run to invoke automatic theorem provers.

This added two more processes communicating with text that
had to be parsed on both output an input and of course provers
aren’t always fast, so it was done offline.

I eventually removed it because WHY was too experimental and kept
changing, also getting hold of and configuring the external provers wasn’t
too hard
on Linux but on other platforms proved very difficult.

You will also have the tricky problem that the solvers aren’t quite aligned
with what is actually required by your compiler.

Still, congratulations, I think this is the right way to go.
Leveraging separate projects is tricky and the loss of control is worrying
but in the end, a compiler writer simply cannot do everything.
In the end, you have to delegate most of the library development too.
And then, split the compiler into modules and delegate parts of that
as well (eg optimisation, parsing, back end etc).

–
john skaller
skaller@…
http://felix-lang.org