CODEWITHSUNDEEP
frama-calt-ergo
V. Semeria
V. Semeria

Reputation: 3256

Cannot prove euclidean division in frama-c

I'd like to prove this loop implementation of Euclidean division in Frama-C :

/*@
  requires a >= 0 && 0 < b;
  ensures \result == a / b;
*/
int euclid_div(const int a, const int b)
{
  int q = 0;
  int r = a;

  /*@
    loop invariant a == b*q+r && r>=0;
    loop assigns q,r;
    loop variant r;
   */
  while (b <= r)
    {
      q++;
      r -= b;
    }
  return q;
}

But the post condition fails to prove automatically (the loop invariant proved fine) :

Goal Post-condition:
Let x = r + (b * euclid_div_0).
Assume {
  (* Pre-condition *)
  Have: (0 < b) /\ (0 <= x).
  (* Invariant *)
  Have: 0 <= r.
  (* Else *)
  Have: r < b.
}
Prove: (x / b) = euclid_div_0.

--------------------------------------------------------------------------------
Prover Alt-Ergo: Unknown (250ms).

It does have all the hypotheses of Euclidean division, does anyone know why it cannot conclude ?

Upvotes: 2

Views: 251

Answers (2)

Virgile
Virgile

Reputation: 10148

As indicated by Mohamed Iguernlala's answer, automated provers are not very comfortable with non-linear arithmetic. It is possible to do interactive proofs with WP, either directly within the GUI (see section 2.3 of WP Manual for more information), or by using coq (double click on the appropriate cell of the WP Goals tab of the GUI for launching coqide on the corresponding goal).

It is usually better to use coq on ACSL lemmas, as you can focus on the exact formula you want to prove manually, without being bothered by the logical model of the code you're trying to prove. Using this tactic, I've been able to prove your post-condition with the following intermediate lemma:

/*@

// WP's interactive prover select lemmas based on the predicate and
// function names which appear in it, but does not take arithmetic operators
// into account 😭. Hence the DIV definition.

logic integer DIV(integer a,integer b) = a / b ;

lemma div_rem:
  \forall integer a,b,q,r; a >=0 ==> 0 < b ==>  0 <= r < b ==>
  a == b*q+r ==> q == DIV(a, b);
*/

/*@
  requires a >= 0 && 0 < b;
  ensures \result == DIV(a, b);
*/
int euclid_div(const int a, const int b)
{
  int q = 0;
  int r = a;

  /*@
    loop invariant a == b*q+r;
    loop invariant r>=0;
    loop assigns q,r;
    loop variant r;
   */
  while (b <= r)
    {
      q++;
      r -= b;
    }
  /*@ assert 0<=r<b; */
  /*@ assert a == b*q+r; */
  return q;
}

More precisely, the lemma itself is proved with the following Coq script:

intros a b q prod Hb Ha Hle Hge.
unfold L_DIV.
generalize (Cdiv_cases a b).
intros Hcdiv; destruct Hcdiv.
clear H0.
rewrite H; auto with zarith.
clear H.

symmetry; apply (Zdiv_unique a b q (a-prod)); auto with zarith.
unfold prod; simpl.
assert (b*q = q*b); auto with zarith.

While the post-condition only requires to instantiate the lemma with the appropriate arguments.

Upvotes: 3

iguerNL
iguerNL

Reputation: 464

Because it's non-linear arithmetic, which is sometimes hard for automatic (SMT) solvers.

I re-written the goal in SMT2 format, and none of Alt-Ergo 2.2, CVC4 1.5 and Z3 4.6.0 is able to prove it:

(set-logic QF_NIA)

(declare-const i Int)
(declare-const i_1 Int)
(declare-const i_2 Int)

(assert (>= i_1 0))
(assert (>  i_2 0))
(assert (>=  i 0))
(assert (<  i i_2))

; proved by alt-ergo 2.2 and z3 4.6.0 if these two asserts are uncommented
;(assert (<= i_1 10))
;(assert (<= i_2 10))

(assert
 (not
  (= i_1
     (div
      (+ i (* i_1 i_2))
      i_2 )
     )
  )
 )

(check-sat)

If you change your post-condition like this, it is proved by Alt-Ergo

ensures \exists int r ;
   a == b * \result + r && 0 <= r && r < b;

Upvotes: 3

Related Questions