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



David and Andreas,

Thanks for the investigation on quickcheck. Meanwhile I have been looking into tweaking nitpick, though the results thus far have been troubling. See below.


lemma word_lem: "(x :: 4 word) = y"
nitpick[verbose, mono, card int = 32, card nat = 16, card "2 list" = 4, 
    card "1 list" = 4, card "4 word" = 8, card "4" = 4, card "2" = 2, 
    card "1" = 1, card unit = 1]

Nitpicking formula... 
Timestamp: 08:56:02. 
The types "4 word", "4", and "2" are considered monotonic. Nitpick might
be able to skip some scopes. 
Using SAT solver "Lingeling_JNI". The following solvers are configured:
"Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J",
"SAT4J_Light". 
Trying 1 scope:
  card int = 32, card nat = 16, card "2 list" = 4, card "1 list" = 4,
    card "4 word" = 8, card "4" = 4, card "2" = 2, card "1" = 1, and
    card unit = 1. 
Nitpick found a potentially spurious counterexample for card int = 32,
card nat = 16, card "2 list" = 4, card "1 list" = 4, card "4 word" = 8,
card "4" = 4, card "2" = 2, card "1" = 1, and card unit = 1:

  Free variables:
    x = «1»
    y = «0» 
Nitpick could not find a better counterexample. It checked 1 of 1 scope. 
Total time: 3.8 s.


For this contrived example, I was able to get nitpick to focus on one scope, and find the most trivial counterexample, albeit in almost four seconds. Slight perturbations to the cardinalities (i.e. reducing “card int” to 16) may either cause nitpick to find stranger counterexamples, like <<8>> and <<9>>, or not find any counterexamples at all. My experiments have exhausted my understanding of nitpick, and I’m not sure if there is any way of further improving performance.

Though I have a general idea of what you both are suggesting on the quickcheck side, I am not convinced that this solution will scale up to the application which my research group desires: checking Hoare triples over heap abstracted code generated by AutoCorres. 

~Scott


> On Nov 6, 2014, at 2:35 AM, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
> 
> Hi David,
> 
> Now I see that ML's value restriction causes the error. One of the parameters of the enum type class (namely enum) is not of function type. Since its definition 'a ptr does not depend on other type classes' parameters for 'a, the code generator produces a declaration of the form
> 
> val enum_ptr = ...
> 
> which of course should be polymorphic in the element type, but this is not allowed for val declarations in ML. If you restrict the element type to a type class with type parameters, then the code generator will produce a fun declaration, which may be polymorphic. You can define your own type class such as
> 
> class dummy = fixes DUMMY :: "'a itself"
> 
> and declare a corresponding code equation:
> 
> lemma enum_ptr_code [code]:
>  "Enum.enum = (map (Ptr o of_nat) [0 ..< 2 ^ 32] :: 'a :: dummy ptr list)"
> by(simp add: enum_ptr_def)
> 
> Of course, you have to instantiate this class for all your type constructors that you want to store in a ptr.
> 
> instantiation "fun" :: (type, type) dummy begin
> definition "DUMMY = TYPE('a ⇒ 'b)"
> instance ..
> end
> 
> instantiation nat :: dummy begin
> definition "DUMMY = TYPE(nat)"
> instance ..
> end
> 
> Alternatively, you can reuse one of Isabelle/HOL's type classes, e.g. typerep (of which almost every type is an instance of):
> 
> lemma enum_ptr_code [code]:
>  "Enum.enum = (map (Ptr o of_nat) [0 ..< 2 ^ 32] :: 'a :: typerep ptr list)"
> by(simp add: enum_ptr_def)
> 
> With this setup, the code generator outputs valid ML code.
> 
> Best,
> Andreas
> 
> 
> On 05/11/14 23:17, David Greenaway wrote:
>> Hi Andreas,
>> 
>> Thanks for your suggestions about writing some custom state generators.
>> I have some ideas about what might be useful testcases in practice.
>> 
>> Generating custom states by inspecting the precondition sounds fun, but
>> might be a longer-term project. :)
>> 
>> On 05/11/14 20:34, Andreas Lochbihler wrote:
>> [...]
>>> I was not able to look at problem 2, because I have not found a small
>>> example where the ptr causes an exception. If you provide one, I can
>>> have a look at this, too.
>> 
>> I have attached a small, self-contained example that demonstrates the
>> problem.
>> 
>> In particular:
>> 
>>     lemma "(a :: nat ptr ⇒ nat) = b"
>>       quickcheck
>> 
>> seems to work fine, but:
>> 
>>     record lifted_globals =
>>       foo :: "nat ptr ⇒ nat"
>> 
>>     lemma "(a :: lifted_globals) = b"
>>       quickcheck
>> 
>> raises one of the errors:
>> 
>>     Wellsortedness error
>>     (in code equation equal_lifted_globals_ext_inst.equal_lifted_globals_ext
>>                        ⦇foo = ?fooa, … = ?morea⦈ ⦇foo = ?foo, … = ?more⦈ ≡
>>                       ?fooa = ?foo ∧ ?morea = ?more,
>>     with dependency "Pure.dummy_pattern" -> "equal_class.equal [lifted_globals_ext]"):
>>     Type nat ptr ⇒ nat not of sort equal
>>     No type arity ptr :: enum
>> 
>> or:
>> 
>>     Error: Type 'a ptr list includes a free type variable
>>     val
>>        enum_ptra : 'a ptr list =
>>           map (Ptr o ... ...) (upt Zero_nat (... ... (... ...)))
>>     At (line 1331 of "generated code")
>>     Error: Type mismatch in type constraint.
>>        Value:
>>           {finite_enum = finite_ptr, enum = enum_ptra, enum_all = enum_all_ptr,
>>             enum_ex = enum_ex_ptr} :
>>           {enum: 'a ptr list,
>>             enum_all: ('b -> bool) -> bool,
>>             enum_ex: ('c -> bool) -> bool, finite_enum: 'd ptr finite}
>>        Constraint: 'a ptr enum
>>        Reason: Can't unify 'a to 'a (Cannot unify with explicit type variable)
>>     {finite_enum = finite_ptr, enum = enum_ptra, enum_all = enum_all_ptr,
>>          enum_ex = ...} : 'a ptr enum
>>     At (line 1351 of "generated code")
>>     Exception- Fail "Static Errors" raised
>> 
>> Depending on whether "ptr" has been instantiated into the "enum" class
>> or not, respectively.
>> 
>> Thanks for your help,
>> 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.