Skip to first unread message

Jun 13, 2015, 3:07:50 PM6/13/15

to ats-lan...@googlegroups.com, ats-lang-users

I'd like to announce a VERY exciting feature that has just been added to ATS+Z3.

The following example shows that one can now added a quantified constraint via the

keyword $solver_assert:

`//`

extern

praxi

fib_bas0(): [fib(0)==0] unit_p

extern

praxi

fib_bas1(): [fib(1)==1] unit_p

extern

praxi

fib_ind2{n:int | n >= 2}(): [fib(n)==fib(n-1)+fib(n-2)] unit_p

//

(* ****** ****** *)

fun

fib

{n:nat} .<>.

(

n: int(n)

) : int(fib(n)) = let

//

val () = $solver_assert(fib_bas0)

val () = $solver_assert(fib_bas1)

val () = $solver_assert(fib_ind2)

//

fun

loop

{i:nat|i <= n} .<n-i>.

(

ni: int(n-i)

, f0: int(fib(i)), f1: int(fib(i+1))

) : int(fib(n)) = (

//

if

ni >= 2

then (

loop{i+1}(ni-1, f1, f0+f1)

) (* end of [then] *)

else (

if ni >= 1 then f1 else f0

) (* end of [else] *)

//

) (* end of [loop] *)

//

in

loop{0}(n, 0, 1)

end // end of [fib]

(* ****** ****** *)

This feature makes it very convenient for one to TRY to avoid a need for

manual proof construction by taking advantage of Z3's powerful support for

automated theorem-proving.

Please compare the above code with the code in the following file:

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

You can see that the following line of proof construction is dropped:

`prval () = fib_ind2{i+2}()`

I feel that this feature will undoubtedly make ATS so much more useful for program verification.

Cheers!

--Hongwei

Jun 13, 2015, 3:30:07 PM6/13/15

to ats-lang-users, ats-lang-users

I agree that's cause for celebration; even if it is only one line removed (actually I noticed another prval line is dropped too, if trivial), I feel more than half the battle with ATS for me, now, is recognizing when a constraint issue arises because the solver cannot solve the constraint because either 1) it is not possible in the solver or 2) it is not possible mathematically. The former could be thought of as a "soft programmer error" and the latter is a "hard programmer error", or traditional error in programming logic. So anything that reduces the occurrence of 1) is nice.

Does $solver_assert work with the original ATS constraint solver as well?

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To post to this group, send email to ats-lan...@googlegroups.com.

Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/d982f806-709f-430b-aa88-9db5938af633%40googlegroups.com.

Jun 13, 2015, 3:41:14 PM6/13/15

to ats-lan...@googlegroups.com

It is about the potential. Quantifier-free constraints and quantified constraints

are totally different beasts in terms of constraint-solving.

The built-in constraint-solver of ATS cannot handle constraints introduced via $solver_assert.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRr9oS%2BkpXcVpWhHLrpFTDso_vPc-Thi-snq-m8A6%3Dkctw%40mail.gmail.com.

Jun 13, 2015, 6:26:38 PM6/13/15

to Brandon Barker, ats-lang-users, ats-lang-users

On 14/06/2015, at 5:29 AM, Brandon Barker wrote:

> I agree that's cause for celebration; even if it is only one line removed (actually I noticed another prval line is dropped too, if trivial), I feel more than half the battle with ATS for me, now, is recognizing when a constraint issue arises because the solver cannot solve the constraint because either 1) it is not possible in the solver or 2) it is not possible mathematically. The former could be thought of as a "soft programmer error" and the latter is a "hard programmer error", or traditional error in programming logic. So anything that reduces the occurrence of 1) is nice.

It would seem sane to (a) issue a warning and (b) assume the assertion

is correct anyhow.

The second issue arises from this: if the assertion (a) returns unknown or

(b) the programmer *suspects* it might return unknown, how can the

programmer give the solver some help?

I believe it is sane in a PL that the solver can be:

(a) dropped altogether whilst debugging and developing

(b) activated during a verification pass

(c) the results should be cached to speed up verification

(d) the solver can be swapped for another solver

When I tried to something similar in Felix I divided assertions into

several categories:

1. Axioms. The basic rules (though not necessarily independent)

2. Lemmas. Simple rules an automatic theorem prover could solve

3. Theorems. Rules that would be too hard for an automatic solver

but which might be proven by a proof assistant if hints

were given (in some as yet unspecified language)

I also provide reductions, which are "directed" axioms, that is,

instructions to the compiler to replace some term with another

(hopefully more efficient one).

In principle there is another option. If an assertion cannot be verified

at compile time, generate a run time check.

I think ATS has now run into the problem that some basic assertions

can always be checked efficiently, however once one starts providing

more advanced capabilities, the performance of the verification

system becomes an issue.

One must recognise that dynamically typed scripting languages

(include crap like Java) are popular because they reduce notational

demands, compile fast, and run at quite reasonable speeds for

many purposes (especially with JITs). What's more, they permit

very high level expression which most statically typed systems do not.

For example few static languages have a type system strong enough

to do functorial polymorphism, not even Haskell can do that.

C++ can do a bit of it, partly *because* the type system is weaker.

Given this, a practical statically typed language .. and ATS is intended

to be a production language not an academic toy .. has to be able

to achieve some kind of balance for which the extra cost is worthwhile.

In Ocaml, for example, type inference relieves *some* of the notational

overhead (at the cost of sometimes incomprehensible error messages).

I will relate a story. I was working at a place on software to verify

C and C++ programs. This was done by constructing a flow model

(control and data) and examining paths: standard static analysis

stuff. However the novel feature of the system was to use a satsolver

to find potential bugs. The satsolver was very fast. However, it wasn't

accurate because the analysis was only first order. To check for

null pointer issues, one needs a full data flow analysis which is O(N^3).

[The solver was basically O(N)]

So how could the product be improved without killing performance?

The very smart suggestion was made: use the satsolve to find

*potential* problem areas and apply the full data flow analysis to

just those areas.

Here's another story. Clang has static analysis and does optimisations.

However some of the optimisations, despite assertions to the contrary

from the developers, are not linear. Most advanced optimisations can't

be linear. So I suggested a simple solution: do the advanced optimisations

under a timer. Just give up if it is taking too long. increase the time period

for better results. That was pooh poohed by the developers because

the output wouldn't be deterministic, but they clearly didn't understand

that the tradeoff between compiler performance and the resulting

program performance is fairly indeterminate anyhow: high level

optimisations are highly sensitive to context, and only work as

expected a small fraction of the time, because one simply cannot

reapply them in every possible context they might be applied.

The bottom line is to do anything advanced you HAVE to develop

some nasty heuristics to keep the compile time/run time tradeoff

reasonable. It's similar to say a garbage collector. The theory is

all very well but the key to a good GC is the tuning parameters.

What I suspect ATS is going to have to do is provide, along with

the proof data, estimates of the costs of finding a solution.

One then uses linear programming to choose which things

to prove and which ones to give up on. TeX uses this to calculate

line breaks in a paragraph efficiently (one provides a "badness"

rating for various possible line breaks and the solver tries

to minimise the overall badness).

In other words, you need a linear model to cost operations

so as to decide when to apply non-linear operations :-)

--

john skaller

ska...@users.sourceforge.net

http://felix-lang.org

Jun 13, 2015, 6:43:14 PM6/13/15

to ats-lan...@googlegroups.com

What kind of arguments can be given to $solver_assert?

From my understanding, adding the calls to $solver_assert in this example adds the following assertions to the Z3 solver when it is constraint solving the fib function.

fib(0) == 0

fib(1) == 1

forall n:int (n >= 2) implies (fib(n) == fib(n-1) + fib(n-2))

Where fib is an uninterpreted function. Is this the correct way to think about solver_assert?

Jun 13, 2015, 10:55:47 PM6/13/15

to ats-lan...@googlegroups.com

Yes, $solver_assert(pf) generates a call to Z3_assert for adding into the underlying Z3 solver

the formula translated from the prop of 'pf'.

the formula translated from the prop of 'pf'.

Jun 14, 2015, 5:39:41 PM6/14/15

to ats-lan...@googlegroups.com, ats-lan...@lists.sourceforge.net

On Saturday, June 13, 2015 at 3:30:07 PM UTC-4, Brandon Barker wrote:

I agree that's cause for celebration; even if it is only one line removed (actually I noticed another prval line is dropped too, if trivial), I feel more than half the battle with ATS for me, now, is recognizing when a constraint issue arises because the solver cannot solve the constraint because either 1) it is not possible in the solver or 2) it is not possible mathematically. The former could be thought of as a "soft programmer error" and the latter is a "hard programmer error", or traditional error in programming logic. So anything that reduces the occurrence of 1) is nice.

Speaking for myself, I rarely pay any attention to the difference between (1) and (2).

I nearly always have good reasons to believe that it is possible to prove what I want to prove

but I could be wrong. In a case where some constraints can not be solved, one can often use

prop_verify (in prelude/SATS/basics_dyn.sats) to figure out the cause.

If you are not so sure whether a constraint can or cannot be verified and want to figure it out by using

a constraint-solver, then I would expect that the constraint cannot actually be verified most of the time.

I would say that a very big part of programming verification is just to run programs in your mind.

Jun 14, 2015, 11:18:46 PM6/14/15

to ats-lan...@googlegroups.com, ats-lan...@lists.sourceforge.net

Le samedi 13 juin 2015 21:30:07 UTC+2, Brandon Barker a écrit :

I agree that's cause for celebration; even if it is only one line removed (actually I noticed another prval line is dropped too, if trivial), I feel more than half the battle with ATS for me, now, is recognizing when a constraint issue arises because the solver cannot solve the constraint because either 1) it is not possible in the solver or 2) it is not possible mathematically. The former could be thought of as a "soft programmer error" and the latter is a "hard programmer error", or traditional error in programming logic. So anything that reduces the occurrence of 1) is nice.Does $solver_assert work with the original ATS constraint solver as well?

So `$solver_assert` is statically checked? If it is, I agree too this is welcome.

Jun 14, 2015, 11:22:27 PM6/14/15

to ats-lan...@googlegroups.com, brandon...@gmail.com, ats-lan...@lists.sourceforge.net

Le dimanche 14 juin 2015 00:26:38 UTC+2, John Skaller a écrit :

There are several issues. What happens if the solver assert returns "unknown"?

It would seem sane to (a) issue a warning and (b) assume the assertion

is correct anyhow.

And add an option “treat warnings as error” :-p

Jun 14, 2015, 11:41:30 PM6/14/15

to ats-lan...@googlegroups.com, ats-lan...@lists.sourceforge.net

$solver_assert is safe. It just translates the type of a proof into a (quantified) formula

so that it can be used by Z3. The built-in constraint-solver of ATS cannot handle quantified

formulas directly.

Jun 14, 2015, 11:54:55 PM6/14/15

to ats-lan...@googlegroups.com, ats-lan...@lists.sourceforge.net

As I am gathering more experience with Z3, I start to see some very

serious issues with proof search involving quantified formulas. One such

issue can be easily understood by trying the following example:

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

I noted that this example works if I use Z3-4.3.2 but it fails to work if I use Z3-4.4.0.

What happens is that Z3-4.4.0 would run out of memory and crash. Given the simplicity

of this example, one has to be wondering about the practicality of Z3 for doing proof-search

involving quantified formulas.

serious issues with proof search involving quantified formulas. One such

issue can be easily understood by trying the following example:

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

I noted that this example works if I use Z3-4.3.2 but it fails to work if I use Z3-4.4.0.

What happens is that Z3-4.4.0 would run out of memory and crash. Given the simplicity

of this example, one has to be wondering about the practicality of Z3 for doing proof-search

involving quantified formulas.

Jun 16, 2015, 5:26:06 PM6/16/15

to ats-lan...@googlegroups.com, ats-lan...@lists.sourceforge.net

You might want to try Kodkod http://alloy.mit.edu/kodkod/ which is designed for this kind of work. It is successfully integrated into Isabelle as Nitpick.

Jun 16, 2015, 6:18:53 PM6/16/15

to H Zhang, ats-lan...@googlegroups.com, ats-lan...@lists.sourceforge.net

On 17/06/2015, at 7:26 AM, H Zhang wrote:

> You might want to try Kodkod http://alloy.mit.edu/kodkod/ which is designed for this kind of work. It is successfully integrated into Isabelle as Nitpick.

Then the prover would be plugable.

A faster alternative would be a client/server interface using

either 0MQ or TCP/IP. More work, better performance,

but still the ability to swap. Using 0MQ would also allow

swapping the interface (i.e. direct memory to memory is

possible by just changing the connection specification).

When I last used it, WHY was designed as an interchange

language (and provided Ergot as the default solver but would

work with many others).

Reply all

Reply to author

Forward

0 new messages