[wp] extended lemmas on div, mod & shifts

src/plugins/wp/Changelog

@@ -30,7 +30,9 @@
 - WP          [2019/01/29] Emit a warning when no goal is generated
 - TIP         [2018/04/03] Create session directory only on demand
 - TIP         [2018/03/19] Specification of JSON script format
+- Wp          [2018/03/18] Additional lemma about remainder (mod)
 - TIP         [2018/03/18] Refactor structure of session directory (remove models)
+- Wp          [2018/02/18] Additional lemmas about logical shift compositions
 
 ##########################
 Plugin WP 20.0 (Calcium)

src/plugins/wp/share/coqwp/Cbits.v

@@ -168,6 +168,118 @@ Proof.
   split; split; split; Zbits.auto_zbits.
 Qed.
 
+(* Why3 goal *)
+Lemma lsl_0 : forall (x:Z), ((Cint.lsl x 0%Z) = x).
+Proof.
+  intros x.
+  unfold Cint.lsl.
+  rewrite Zbits.lsl_pos ; auto with zarith.
+  unfold Zbits.lsl_def. simpl.
+  rewrite Zbits.lsl_arithmetic_shift.
+  unfold Zbits.lsl_arithmetic_def. unfold two_power_nat. simpl.
+  auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma lsl_1 : forall (x:Z), ((Cint.lsl x 1%Z) = (2%Z * x)%Z).
+Proof.
+  intros x.
+  unfold Cint.lsl.
+  rewrite Zbits.lsl_pos ; auto with zarith.
+  unfold Zbits.lsl_def.
+  rewrite Zbits.lsl_arithmetic_shift.
+  unfold Zbits.lsl_arithmetic_def.
+  replace (two_power_nat (Z.abs_nat 1)) with 2%Z ; auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma lsl_add : forall (x:Z) (p:Z) (q:Z), (0%Z <= p)%Z -> ((0%Z <= q)%Z ->
+  ((Cint.lsl (Cint.lsl x p) q) = (Cint.lsl x (p + q)%Z))).
+Proof.
+  intros x p q h1 h2.
+  repeat unfold Cint.lsl.
+  repeat (rewrite Zbits.lsl_pos ; auto with zarith).
+  repeat unfold Zbits.lsl_def.
+  repeat rewrite Zbits.lsl_arithmetic_shift.
+  repeat unfold Zbits.lsl_arithmetic_def.
+  replace (Z.abs_nat (p+q)) with (Z.abs_nat p + Z.abs_nat q).
+    - rewrite Bits.two_power_nat_plus. auto with zarith. 
+    - rewrite Zabs2Nat.inj_add ; auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma lsr_0 : forall (x:Z), ((Cint.lsr x 0%Z) = x).
+Proof.
+  intros x.
+  unfold Cint.lsr.
+  rewrite Zbits.lsr_pos ; auto with zarith.
+  unfold Zbits.lsr_def. simpl.
+  rewrite Zbits.lsr_arithmetic_shift.
+  unfold Zbits.lsr_arithmetic_def. unfold two_power_nat. simpl.
+  auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma lsr_1 : forall (x:Z), (0%Z <= x)%Z -> ((Cint.lsr x
+  1%Z) = (ZArith.BinInt.Z.quot x 2%Z)).
+Proof.
+  intros pos x.
+  unfold Cint.lsr.
+  rewrite Zbits.lsr_pos ; auto with zarith.
+  unfold Zbits.lsr_def.
+  rewrite Zbits.lsr_arithmetic_shift.
+  unfold Zbits.lsr_arithmetic_def.
+  replace (two_power_nat (Z.abs_nat 1)) with 2%Z ; auto with zarith.
+  rewrite Z.quot_div_nonneg ; auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma lsr_add : forall (x:Z) (p:Z) (q:Z), (0%Z <= p)%Z -> ((0%Z <= q)%Z ->
+  ((Cint.lsr (Cint.lsr x p) q) = (Cint.lsr x (p + q)%Z))).
+Proof.
+  intros x p q h1 h2.
+  repeat unfold Cint.lsr.
+  repeat (rewrite Zbits.lsr_pos ; auto with zarith).
+  repeat unfold Zbits.lsr_def.
+  repeat rewrite Zbits.lsr_arithmetic_shift.
+  repeat unfold Zbits.lsr_arithmetic_def.
+  replace (Z.abs_nat (p+q)) with (Z.abs_nat p + Z.abs_nat q).
+    - rewrite Bits.two_power_nat_plus.
+      rewrite Z.div_div ; auto with zarith.
+      generalize (Bits.two_power_nat_is_positive (Z.abs_nat p)).
+      auto with zarith. apply Bits.two_power_nat_is_positive.
+    - rewrite Zabs2Nat.inj_add ; auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma lsl_lsr_add : forall (x:Z) (p:Z) (q:Z), ((0%Z <= q)%Z /\ (q <= p)%Z) ->
+  ((Cint.lsr (Cint.lsl x p) q) = (Cint.lsl x (p - q)%Z)).
+Proof.
+  intros x p q (h1,h2).
+  repeat unfold Cint.lsr.
+  repeat unfold Cint.lsl.
+  repeat (rewrite Zbits.lsr_pos ; auto with zarith).
+  repeat (rewrite Zbits.lsl_pos ; auto with zarith).
+  repeat unfold Zbits.lsr_def.
+  repeat unfold Zbits.lsl_def.
+  repeat rewrite Zbits.lsr_arithmetic_shift.
+  repeat unfold Zbits.lsr_arithmetic_def.
+  repeat rewrite Zbits.lsl_arithmetic_shift.
+  repeat unfold Zbits.lsl_arithmetic_def.
+  pose ( r := (p - q)%Z ).
+  fold r.
+  replace p with (q+r)%Z by (unfold r ; auto with zarith).
+  replace (Z.abs_nat (q+r)) with (Z.abs_nat q + Z.abs_nat r).
+     * rewrite Bits.two_power_nat_plus.
+       replace (two_power_nat (Z.abs_nat q) * two_power_nat (Z.abs_nat r))%Z
+          with (two_power_nat (Z.abs_nat r) * two_power_nat (Z.abs_nat q))%Z by (apply Z.mul_comm).
+       rewrite Z.mul_assoc.
+       rewrite Z_div_mult. auto.
+       generalize (Bits.two_power_nat_is_positive (Z.abs_nat q)).
+       auto with zarith.
+     * rewrite Zabs2Nat.inj_add ; unfold r ; auto with zarith.
+Qed.
+
 Require Import Qedlib.
 Local Open Scope Z_scope.
 Require Import Zbits.

src/plugins/wp/share/coqwp/Qed.v

@@ -204,3 +204,27 @@ Proof.
   exact (Z.quot_same a h1).
 Qed.
 
+(* Why3 goal *)
+Lemma cdiv_closed_remainder : forall (a:Z) (b:Z) (n:Z), (0%Z <= a)%Z ->
+  ((0%Z <= b)%Z -> (((0%Z <= (b - a)%Z)%Z /\ ((b - a)%Z < n)%Z) ->
+  (((ZArith.BinInt.Z.rem a n) = (ZArith.BinInt.Z.rem b n)) -> (a = b)))).
+Proof.
+  intros a b n PA PB Range Rem.
+  Require Import ZArith.
+  Open Scope Z_scope.
+  pose (p := a/n).
+  pose (q := b/n).
+  replace (Z.rem a n) with (a mod n) in Rem by (rewrite Z.rem_mod_nonneg ; auto with zarith).
+  replace (Z.rem b n) with (b mod n) in Rem by (rewrite Z.rem_mod_nonneg ; auto with zarith).
+  assert (A : a = n * (a/n) + (a mod n)) by (apply Z.div_mod ; auto with zarith). fold p in A.
+  assert (B : b = n * (b/n) + (b mod n)) by (apply Z.div_mod ; auto with zarith). fold q in B.
+  assert (D : (b-a) = n * q - n * p) by (auto with zarith).
+  rewrite <- Z.mul_sub_distr_l in D.
+  assert (R : (b-a) = n * ((b-a)/n) + ((b-a) mod n)) by (apply Z.div_mod ; auto with zarith).
+  assert (Q : (q-p) = (b-a) / n) by (apply Z.div_unique_exact ; auto with zarith).
+  rewrite Q in D.
+  assert (Z : (b-a) mod n = 0) by (auto with zarith).
+  replace ((b - a) mod n) with (b-a) in Z by (symmetry ; apply Z.mod_small ; auto with zarith).
+  auto with zarith.
+Qed.
+

src/plugins/wp/share/ergo/Cbits.mlw

@@ -83,6 +83,26 @@ axiom lxor_0 : (forall x:int [lxor(0, x)]. (lxor(0, x) = x))
 
 axiom lxor_0bis : (forall x:int [lxor(x, 0)]. (lxor(x, 0) = x))
 
+axiom lsl_0 : (forall x:int. (lsl(x, 0) = x))
+
+axiom lsl_1 : (forall x:int. (lsl(x, 1) = (2 * x)))
+
+axiom lsl_add :
+  (forall x:int. forall p:int. forall q:int. ((0 <= p) -> ((0 <= q) ->
+  (lsl(lsl(x, p), q) = lsl(x, (p + q))))))
+
+axiom lsr_0 : (forall x:int. (lsr(x, 0) = x))
+
+axiom lsr_1 : (forall x:int. ((0 <= x) -> (lsr(x, 1) = div(x,2))))
+
+axiom lsr_add :
+  (forall x:int. forall p:int. forall q:int. ((0 <= p) -> ((0 <= q) ->
+  (lsr(lsr(x, p), q) = lsr(x, (p + q))))))
+
+axiom lsl_lsr_add :
+  (forall x:int. forall p:int. forall q:int. (((0 <= q) and (q <= p)) ->
+  (lsr(lsl(x, p), q) = lsl(x, (p - q)))))
+
 axiom bit_test_def :
   (forall x:int. forall k:int [bit_testb(x, k)]. ((bit_testb(x, k) = true) ->
   bit_test(x, k)))

src/plugins/wp/share/ergo/Qed.mlw

@@ -152,3 +152,7 @@ axiom cdiv_neutral : (forall a:int [div(a, 1)]. (div(a, 1) = a))
 axiom cdiv_inv :
   (forall a:int [div(a, a)]. ((not (a = 0)) -> (div(a, a) = 1)))
 
+axiom cdiv_closed_remainder :
+  (forall a:int. forall b:int. forall n:int. ((0 <= a) -> ((0 <= b) ->
+  (((0 <= (b - a)) and ((b - a) <  n)) -> ((mod(a,n) = mod(b,n)) ->
+  (a = b))))))

src/plugins/wp/share/why3/frama_c_wp/cbits.mlw

@@ -85,6 +85,22 @@ theory Cbits
         (lxor 0 0) = 0 /\  (lxor 0 1) = 1 /\ (lxor 1 0) = 1 /\ (lxor 1 1) = 0
   meta "remove_for_" axiom lxor_bool
 
+(** ** lsl identities *)
+
+  axiom lsl_0: forall x:int. lsl x 0 = x
+  axiom lsl_1: forall x:int. lsl x 1 = 2 * x
+  axiom lsl_add: forall x p q:int. 0 <= p -> 0 <= q -> lsl (lsl x p) q = lsl x (p+q)
+
+(** ** lsr identities *)
+
+  axiom lsr_0: forall x:int. lsr x 0 = x
+  axiom lsr_1: forall x:int. 0 <= x -> lsr x 1 = CD.div x 2
+  axiom lsr_add: forall x p q :int. 0 <= p -> 0 <= q -> lsr (lsr x p) q = lsr x (p+q)
+
+(** ** lsl+lsr combination *)
+
+  axiom lsl_lsr_add: forall x p q:int. 0 <= q <= p -> lsr (lsl x p) q = lsl x (p-q)
+
 (** * Bit extraction *)
 (** ** Definition of bit_test predicate *)
 

src/plugins/wp/share/why3/frama_c_wp/qed.mlw

@@ -77,4 +77,9 @@ theory Qed
   lemma cdiv_neutral : forall a:int [CD.div a 1]. CD.div a 1 = a
   lemma cdiv_inv : forall a:int [CD.div a a]. a<>0 -> CD.div a a = 1
 
+  lemma cdiv_closed_remainder :
+    forall a,b,n:int.
+    0 <= a -> 0 <= b -> 0 <= b-a < n ->
+    CD.mod a n = CD.mod b n -> a = b
+
 end