Merge branch 'msammler/bv' into 'master'

Add bitvector library with automation

See merge request !408

_CoqProject

@@ -59,3 +59,5 @@ stdpp/telescopes.v
 stdpp/binders.v
 
 stdpp_unstable/bitblast.v
+stdpp_unstable/bitvector.v
+stdpp_unstable/bitvector_tactics.v

tests/bitvector.ref

+"notation_test"
+     : string
+BV 10 3 = BV 10 5
+     : Prop
+The command has indeed failed with message:
+The term "BV 10 5" has type "bv 10" while it is expected to have type "bv 2".
+BV 2 3 = BV 10 5
+     : Prop
+The command has indeed failed with message:
+Unable to satisfy the following constraints:
+
+?bv_is_wf : "BvWf 2 4"
+
+"bvn_to_bv_test"
+     : string
+1 goal
+  
+  ============================
+  Some (BV 2 3) = Some (BV 2 3)

tests/bitvector.v

+From stdpp Require Import strings.
+From stdpp.unstable Require Import bitvector.
+
+Check "notation_test".
+Check (BV 10 3 = BV 10 5).
+Fail Check (BV 2 3 = BV 10 5).
+Check (BV 2 3 =@{bvn} BV 10 5).
+Fail Goal (BV 2 4 = BV 2 5).
+
+Check "bvn_to_bv_test".
+Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.

tests/bitvector_tactics.ref

+1 goal
+  
+  a : Z
+  ============================
+  bv_wrap 64 (a + 1) = bv_wrap 64 (Z.succ a)
+1 goal
+  
+  l, r, xs : bv 64
+  data : list (bv 64)
+  H : bv_unsigned l < bv_unsigned r
+  H0 : bv_unsigned r ≤ Z.of_nat (length data)
+  H1 : bv_unsigned xs + Z.of_nat (length data) * 8 < 2 ^ 52
+  ============================
+  bv_wrap 64
+    (bv_unsigned xs +
+     (bv_unsigned l + bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1) *
+     8) < 2 ^ 52
+2 goals
+  
+  l, r : bv 64
+  data : list (bv 64)
+  H : bv_unsigned l < bv_unsigned r
+  H0 : bv_unsigned r ≤ Z.of_nat (length data)
+  H1 : ¬ bv_swrap 128 (bv_unsigned l) >=
+         bv_swrap 128
+           (bv_wrap 64
+              (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 +
+               bv_unsigned l + 0))
+  ============================
+  bv_unsigned l <
+  bv_wrap 64
+    (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + bv_unsigned l +
+     0)
+
+goal 2 is:
+ bv_wrap 64
+   (bv_wrap 64 (bv_unsigned r - bv_unsigned l) `div` 2 ^ 1 + bv_unsigned l +
+    0) ≤ Z.of_nat (length data)
+1 goal
+  
+  r1 : bv 64
+  H : bv_unsigned r1 ≠ 22
+  ============================
+  bv_wrap 64 (bv_unsigned r1 + 18446744073709551593 + 1) ≠ bv_wrap 64 0
+1 goal
+  
+  i, n : bv 64
+  H : bv_unsigned i < bv_unsigned n
+  H0 : bv_wrap 64
+         (bv_unsigned n + bv_wrap 64 (- bv_wrap 64 (bv_unsigned i + 1) - 1) +
+          1) ≠ 0
+  ============================
+  bv_wrap 64 (bv_unsigned i + 1) < bv_unsigned n
+1 goal
+  
+  b : bv 16
+  v : bv 64
+  ============================
+  bv_wrap 64
+    (Z.lor (Z.land (bv_unsigned v) 18446744069414649855)
+       (bv_wrap 64 (bv_unsigned b ≪ 16))) =
+  bv_wrap 64
+    (Z.lor
+       (bv_wrap (16 * 2) (bv_unsigned v ≫ Z.of_N (16 * 2)) ≪ Z.of_N (16 * 2))
+       (Z.lor (bv_unsigned b ≪ Z.of_N (16 * 1))
+          (bv_wrap (16 * 1) (bv_unsigned v))))

tests/bitvector_tactics.v

+From stdpp Require Import strings.
+From stdpp.unstable Require Import bitblast bitvector_tactics.
+Unset Mangle Names.
+
+Local Open Scope Z_scope.
+Local Open Scope bv_scope.
+
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+(** * Smoke tests *)
+
+(** Simple test *)
+Goal ∀ a : Z, Z_to_bv 64 a `+Z` 1 = Z_to_bv 64 (Z.succ a).
+Proof.
+  intros. bv_simplify. Show.
+  Restart.
+  intros. bv_solve.
+Qed.
+
+(** More complex test *)
+Goal ∀ l r xs : bv 64, ∀ data : list (bv 64),
+    bv_unsigned l < bv_unsigned r →
+    bv_unsigned r ≤ Z.of_nat (length data) →
+    bv_unsigned xs + Z.of_nat (length data) * 8 < 2 ^ 52 →
+    bv_unsigned (xs + (bv_extract 0 64 (bv_zero_extend 128 l) +
+                       bv_extract 0 64 (bv_zero_extend 128 ((r - l) ≫ BV 64 1))) * BV 64 8) < 2 ^ 52.
+Proof.
+  intros. bv_simplify_arith. Show.
+  Restart.
+  intros. bv_solve.
+Qed.
+
+(** Testing simplification in hypothesis *)
+Goal ∀ l r : bv 64, ∀ data : list (bv 64),
+  bv_unsigned l < bv_unsigned r →
+  bv_unsigned r ≤ Z.of_nat (length data) →
+  ¬ bv_signed (bv_zero_extend 128 l) >=
+    bv_signed (bv_zero_extend 128 (bv_zero_extend 128 ((r - l) ≫ BV 64 1 + l + BV 64 0))) →
+  bv_unsigned l < bv_unsigned ((r - l) ≫ BV 64 1 + l + BV 64 0) ≤ Z.of_nat (length data).
+Proof.
+  intros. bv_simplify_arith select (¬ _ >= _). bv_simplify_arith.
+  split. (* We need to split since the [_ < _ ≤ _] notation differs between Coq versions. *) Show.
+  Restart.
+  intros. bv_simplify_arith select (¬ _ >= _). bv_solve.
+Qed.
+
+(** Testing inequality in goal. *)
+Goal ∀ r1 : bv 64,
+  bv_unsigned r1 ≠ 22 →
+  bv_extract 0 64 (bv_zero_extend 128 r1 + BV 128 0xffffffffffffffe9 + BV 128 1) ≠ BV 64 0.
+Proof.
+  intros. bv_simplify. Show.
+  Restart.
+  intros. bv_solve.
+Qed.
+
+(** Testing inequality in hypothesis. *)
+Goal ∀ i n : bv 64,
+  bv_unsigned i < bv_unsigned n →
+  bv_extract 0 64 (bv_zero_extend 128 n + bv_zero_extend 128 (bv_not (bv_extract 0 64 (bv_zero_extend 128 i)
+          + BV 64 1)) + BV 128 1) ≠ BV 64 0 →
+  bv_unsigned (bv_extract 0 64 (bv_zero_extend 128 i) + BV 64 1) < bv_unsigned n.
+Proof.
+  intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_simplify. Show.
+  Restart.
+  intros. bv_simplify_arith select (bv_extract _ _ _ ≠ _). bv_solve.
+Qed.
+
+(** Testing combination of bitvector and bitblast. *)
+Goal ∀ b : bv 16, ∀ v : bv 64,
+  bv_or (bv_and v (BV 64 0xffffffff0000ffff)) (bv_zero_extend 64 b ≪ BV 64 16) =
+  bv_concat 64 (bv_extract (16 * (1 + 1)) (16 * 2) v) (bv_concat (16 * (1 + 1)) b (bv_extract 0 (16 * 1) v)).
+Proof.
+  intros. bv_simplify. Show. bitblast.
+Qed.