Skip to content
Snippets Groups Projects
Commit f214fac6 authored by Michael Sammler's avatar Michael Sammler
Browse files

Add bitvector library with tactics

parent d6c6e66a
No related branches found
No related tags found
1 merge request!408Add bitvector library with automation
......@@ -59,3 +59,5 @@ stdpp/telescopes.v
stdpp/binders.v
stdpp_unstable/bitblast.v
stdpp_unstable/bitvector.v
stdpp_unstable/bitvector_tactics.v
This diff is collapsed.
This diff is collapsed.
"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)
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.
1 goal
a : Z
============================
bv_wrap 64 (a + 1) = bv_wrap 64 (Z.succ a)
1 goal
sp, 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))))
From stdpp Require Import strings.
From stdpp.unstable Require Import bitblast bitvector_tactics.
Unset Mangle Names.
Local Open Scope Z_scope.
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
(** * Smoke tests *)
(** Simple test *)
Goal a : Z, bv_add_Z (Z_to_bv 64 a) 1 = Z_to_bv 64 (Z.succ a).
Proof.
intros. bv_simplify. Show.
Restart.
intros. bv_solve.
Qed.
(** More complex test *)
Goal sp 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
(bv_add xs
(bv_mul
(bv_add (bv_extract 0 64 (bv_zero_extend 128 l))
(bv_extract 0 64 (bv_zero_extend 128 (bv_shiftr (bv_sub 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_add (bv_add (bv_shiftr (bv_sub r l) (BV 64 1)) l) (BV 64 0)))
bv_unsigned l < bv_unsigned (bv_add (bv_add (bv_shiftr (bv_sub 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_add (bv_add (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_add
(bv_add (bv_zero_extend 128 n)
(bv_zero_extend 128 (bv_not (bv_add (bv_extract 0 64 (bv_zero_extend 128 i)) (BV 64 1)))))
(BV 128 1)) BV 64 0
bv_unsigned (bv_add (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_shiftl (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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment