Quantifed constraints

[gmhwxi]

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

[Brandon Barker]

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.

--

Brandon Barker
brandon...@gmail.com

[Hongwei Xi]

Well, it is not really about one line being removed in the mentioned example.

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.

[john skaller]

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.

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.

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

[William Blair]

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?

[gmhwxi]

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'.

[gmhwxi]

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.
 

[Yannick Duchêne]

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.

[Yannick Duchêne]

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

[gmhwxi]

$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.

[gmhwxi]

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.

[H Zhang]

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.

[john skaller]

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.

At some expense interfacing you could use text instead of C.
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).