*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Disproof methods with Word.thy and AutoCorres*From*: David Greenaway <david.greenaway at nicta.com.au>*Date*: Wed, 5 Nov 2014 18:14:00 +1100*Cc*: sdconsta at syr.edu*In-reply-to*: <898ADE59-B0AB-461E-AE17-AA4D5FCDCE48@syr.edu>*References*: <898ADE59-B0AB-461E-AE17-AA4D5FCDCE48@syr.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.2

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.

**Follow-Ups**:**Re: [isabelle] Disproof methods with Word.thy and AutoCorres***From:*Andreas Lochbihler

**References**:**[isabelle] Disproof methods with Word.thy and AutoCorres***From:*Scott Constable

- Previous by Date: Re: [isabelle] Ad-hoc-proving attributes
- Next by Date: Re: [isabelle] Disproof methods with Word.thy and AutoCorres
- Previous by Thread: [isabelle] Disproof methods with Word.thy and AutoCorres
- Next by Thread: Re: [isabelle] Disproof methods with Word.thy and AutoCorres
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list