Re: [isabelle] Disproof methods with Word.thy and AutoCorres



Hi Scott,

On 05/11/14 04:38, Scott Constable wrote:
> I’m currently working with AutoCorres v0.999 a good disproof method to
> check my Hoare triples.

I have no idea what I am doing with either nitpick nor quickcheck, but
thought I would have a bit of a poke around to see if I could understand
what was going on.

> [...] For trivial proofs on words such as
>
> lemma “(x :: 8 word) = y”
>
> quickcheck easily finds a counterexample, but nitpick struggles with
> the potentially massive cardinalities of the underlying types. For
> example,
>
> lemma "(x :: 8 word) = y"
> nitpick[sat_solver = MiniSat_JNI]
>
> outputs:
>
> Nitpicking formula...
> Timestamp: 12:28:39.
> Too many scopes. Skipping 95000 scopes. (Consider using "mono" or
> [...]

It seems like nitpick is generating rather inefficient representations
of words. For example, for the lemma "x = (y :: 2 word)", nitpick
generates:

  Free variables:
    x = «0»
    y = «0»
  Types:
    nat = {0, 1, 2, 3, 4, 5, 6, 7, …}
    int = {- 3, - 2, - 1, 0, 1, 2, 3, 4, …}
    1 list =
      {[], [n⇩,⇩1], [n⇩,⇩1, n⇩,⇩1], [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1],
        [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1], [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1],
        [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1],
        [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1], …}
    unit = {()}
    2 word = {«0», …}
    2 = {«0», …}
  Constants:
    SOME xs. set xs = ⦃True⦄ ∧ distinct xs = [n⇩,⇩1]
    distinct =
      (λx. ?)
      ([] := True, [n⇩,⇩1] := True, [n⇩,⇩1, n⇩,⇩1] := False,
      ...
    set = (λx. ?)
          ([] := {}, [n⇩,⇩1] := {n⇩,⇩1}, [n⇩,⇩1, n⇩,⇩1] := {n⇩,⇩1},
           [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1] := {n⇩,⇩1}, [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1] := {n⇩,⇩1},
           ...
    tl = (λx. ?)
         ([] := [], [n⇩,⇩1] := [], [n⇩,⇩1, n⇩,⇩1] := [n⇩,⇩1],
          [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1] := [n⇩,⇩1, n⇩,⇩1],
          ...
    length =
      (λx. ?)
      ([] := 0, [n⇩,⇩1] := 1, [n⇩,⇩1, n⇩,⇩1] := 2, [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1] := 3,
       [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1] := 4, [n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1, n⇩,⇩1] := 5,
       ...
    op ^ 2 = (λx. ?)(0 := 1, 1 := 2, 2 := 4)

The problem is compounded by nitpick wasting time trying different combinations
of cardinalities for the different intermediate types (nats, ints, lists,
words).

I am sure there would be a way to make nitpick generate more efficient
representations of words, but I don't have the expertise, sorry. I wonder if
Jasmin has any suggestions?

> [...] Quickcheck on the other hand does not seem to cooperate with
> anything that AutoCorres outputs. I typically receive something like
> the following:
>
> Quickchecking...
> Type unification failed: No type arity lifted_globals_ext :: full_exhaustive

AutoCorres defines the "lifted_globals" type using the Record package,
which itself will instantiate "full_exhaustive" if it is able to do so.

In particular, if your C program doesn't use any global state (and hence your
lifted_globals datatype is particularly boring) the "lifted_globals" type is
indeed instantiated into the "full_exhaustive" class by the Record
package. For example, in a C program that doesn't use the heap, we can
write:

    lemma "(a :: lifted_globals) = b"
      quickcheck

and quickcheck produces:

    Quickcheck found a counterexample:

    a = ⦇phantom_machine_state_' = Suc 0, ghost'state_' = ()⦈
    b = ⦇phantom_machine_state_' = 0, ghost'state_' = ()⦈

Things appear to fall apart, however, when either the "lifted_globals"
state or the property being proven become more complex.

On the "lifted_globals" side of things, the moment a program starts to
use the heap, the "ptr" type comes into play. By default, quickcheck
doesn't know how to work with this, so just gives up. We can write the
line:

    quickcheck_generator ptr constructors: Ptr

which teaches quickcheck how to work with the "ptr" type, but quickcheck
still falls over for reasons I don't fully understand. I _suspect_ it
may be related to the dummy type variable in the "ptr" type, which
causes quickcheck to fail with the error message:

    Error: Type 'a ptr list includes a free type variable

This issue might have come up in the past on the list [1, 2].

  [1] : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-July/msg00012.html
  [2] : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-September/msg00075.html

On the property-is-too-complex side of things, quickcheck quickly wants
the "lifted_globals" type to be instantiated into the "enum" class;
presumably so it can evaluate quantifiers. As the lifted_globals type is
frequently of infinite size (it has "nat"'s in its representation), this
isn't feasible.

You also seem to have hit some different errors to me, and its not clear
to me if they are related or not.

So, in short, I think the problems are (at least?):

  1. Many properties you might want to quickcheck appear to require
     "lifted_globals" to be in the "enum" class, which it usually
     can't be.

  2. The "ptr" type causes problems for "quickcheck" for reasons I don't
     fully understand, which means that any property involving
     a non-trivial "lifted_globals" will cause errors.

Is there anyone with quickcheck expertise that might be able to help
resolve these issues?

Cheers,
David

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.