Re: [isabelle] arith tactic



Hi Amine, thanks for looking into this.

The formulas we are using arith for are those generated from unsigned 32-bit machine word arithmetic. Here's the setup:

We are reasoning about some security-critical system code written in C, which uses unsigned machine word arithmetic. To accurately model the code in Isabelle/HOL, we've defined a predicate subtype "mword" containing just those integers that fall within [0 .. 2^32 - 1], and overloaded the arithmetic operators on mword to return their results mod 2^32. The mword (op <) operator is defined in terms of the corresponding (op <) on ints.

At the moment we reason about machine integer subgoals simply by unfolding the definitions of the operators. For example, here's the machine integer subgoal I was working with a few days back:

  "(x :: mword) < y - 1 ==>  x + 1 > x"

I unwound the definitions of (op <), (op +), and (op -) for machine words, and simplified it using auto, extended with some split rules specially designed for this type. The subgoal that remained is what I sent to the Isabelle mailing list (although I changed all occurrences of 2^32 to 2^8, just to make sure the large constant wasn't an issue):

  [| i < (nb - 1) mod 256; 0 <= nb; nb < 256; 0 <= i; i < 256 |]
  ==> i < (i + 1) mod 256


Just today I noticed that I can also solve this subgoal by case- splitting on whether nb - 1 >= 0, and then just use auto. On the other hand, case-splitting on whether i + 1 >= 0 doesn't help. But perhaps I could write a special case-splitting heuristic on all expressions guarded by the mod operator as a tactic. I'm a bit nervous about the possible exponential blowup, but it sounds like I'm already hitting that or worse with Cooper's algorithm in arith.

On the other hand, it's also really useful that arith can return counterexamples to some invalid Presburger subgoals. Here is a variant of the above machine integer problem that looks harder, but actually can be handled using just auto with split rules:

lemma incr_inbounds_easy:
  "(x :: mword) < y ==> x + 1 > x"
by (auto simp add: mword_ops_defs
         split: mword_splits)

I then wrote a seemingly equivalent subgoal:

lemma incr_inbounds_easy2:
  "(x :: mword) <= y - 1 ==> x + 1 > x"
apply (auto simp add: mword_ops_defs
            split: mword_splits)

Unfolding the definitions and case splitting generates the following two subgoals:

  1. !!nb. [|0 <= nb; nb < 256|]
         ==> (nb - 1) mod 256 < ((nb - 1) mod 256 + 1) mod 256
  2. !!nb i.
       [|0 <= nb; nb < 256; 0 <= i; i < 256; i < (nb - 1) mod 256|]
       ==> i < (i + 1) mod 256

I then tried my case-splitting heuristic on the first subgoal,

 apply (case_tac "nb - 1 >= 0", auto)

which Isabelle simplified to False!

In other words, this "equivalent" lemma is invalid. The arith tactic doesn't appear to terminate on this first subgoal either. But if it had, it would presumably have given me a counterexample assignment to the free variable nb. However, with my current auto plus case- splitting approach I have to figure out by hand what is wrong.

Cheers,
-john

Amine Chaieb wrote:
John,
The reasoning about mod in arith about mod and div is poor and enhancing it is on the TODO list. I recently wrote a more effitient implementation of the same QE algorithm, which is able to solve your problem whithin 3 minutes, running in ML (without proofs) which is just a pitty.

Presburger arithmetic is just too general to deal with mod and div in a practically acceptable manner. The decision problem in Presburger arithmetic is doubly exponential in space with respect to the largest constant occuring in the formula (255).


The bigger issue is that we'll be encountering many, many subgoals like this in our projects here, most of which involve reasoning about machine arithmetic. So we're relying on arith to discharge them automatically and efficiently.


Could you give me a "description" of this formula class?

Amine.






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