[isabelle] Disproof methods with Word.thy and AutoCorres



I’m currently working with AutoCorres v0.999, and I am trying to find a good disproof method to check my Hoare triples. 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
"merge_type_vars" to prevent this.) 
Batch 1 of 100: Trying 50 scopes:
  card int = 1, card nat = 1, card "4 list" = 1, card "2 list" = 1,
    card "1 list" = 1, card "1" = 1, card unit = 1, card "8 word" = 1,
    card "8" = 1, card "4" = 1, and card "2" = 1;
  card int = 2, card nat = 2, card "4 list" = 2, card "2 list" = 2,
    card "1 list" = 2, card "1" = 1, card unit = 1, card "8 word" = 2,
    card "8" = 2, card "4" = 2, and card "2" = 2;
…

In my experience nitpick’s recommendations do not seem to alleviate the problem. By manually constraining the cardinalities, I was however able to found a counterexample for 4 bit words, but nothing greater. 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

Type error in application: incompatible operand type

Operator:  full_exhaustive_class.full_exhaustive ::
  (??'a × (unit ⇒ term) ⇒ (bool × term list) option)
  ⇒ natural ⇒ (bool × term list) option
Operand:
  λ(s, t_s__).
     Quickcheck_Random.catch_match
...
 ::
  ??'b lifted_globals_scheme × (unit ⇒ term) ⇒ (bool × term list) option

though to me it looks like this should work.

Any help would be much appreciated.



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