Commit 4168f736 authored by Michael Sammler's avatar Michael Sammler
Browse files

add BvWf typeclass

parent f7c561a4
Pipeline #58256 passed with stage
in 4 minutes and 42 seconds
......@@ -4,6 +4,15 @@ From stdpp Require Import options.
Local Open Scope Z_scope.
(* Checks that a term is closed using a trick by Jason Gross. *)
Ltac check_closed t :=
assert_succeeds (
let x := fresh "x" in
exfalso; pose t as x; revert x;
repeat match goal with H : _ |- _ => clear H end;
lazymatch goal with H : _ |- _ => fail | _ => idtac end
).
Lemma list_fmap_inj1 {A B} (f1 f2 : A B) (l : list A) x:
f1 <$> l = f2 <$> l x l f1 x = f2 x.
Proof.
......@@ -59,7 +68,6 @@ Definition bv_modulus (n : N) : Z := 2 ^ (Z.of_N n).
Definition bv_half_modulus (n : N) : Z := bv_modulus n `div` 2.
Definition bv_wrap (n : N) (z : Z) : Z := z `mod` bv_modulus n.
Definition bv_swrap (n : N) (z : Z) : Z := bv_wrap n (z + bv_half_modulus n) - bv_half_modulus n.
Local Definition bv_wf (n : N) (z : Z) : Prop := -1 < z < bv_modulus n.
Lemma bv_modulus_pos n :
0 < bv_modulus n.
......@@ -109,12 +117,8 @@ Lemma bv_half_modulus_0:
Proof. done. Qed.
Lemma bv_half_modulus_twice_mult n:
bv_half_modulus n + bv_half_modulus n = (if (decide (n = 0%N)) then 0 else 1) * bv_modulus n.
Proof. case_decide; subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
Lemma bv_wf_in_range n z:
bv_wf n z 0 z < bv_modulus n.
Proof. unfold bv_wf. lia. Qed.
bv_half_modulus n + bv_half_modulus n = (Z.of_N n `min` 1) * bv_modulus n.
Proof. destruct (decide (n = 0%N)); subst; [ rewrite bv_half_modulus_0 | rewrite bv_half_modulus_twice]; lia. Qed.
Lemma bv_wrap_in_range n z:
0 bv_wrap n z < bv_modulus n.
......@@ -130,10 +134,6 @@ Proof.
lia.
Qed.
Lemma bv_wrap_wf n z :
bv_wf n (bv_wrap n z).
Proof. pose proof (bv_wrap_in_range n z). split; lia. Qed.
Lemma bv_wrap_small n z :
0 z < bv_modulus n bv_wrap n z = z.
Proof. intros. by apply Z.mod_small. Qed.
......@@ -257,20 +257,6 @@ Proof.
rewrite <-Z.pow_add_r by lia. f_equal. lia.
Qed.
Lemma bv_wf_bitwise_op {n} op bop n1 n2 :
( k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k))
(0 n1 0 n2 0 op n1 n2)
bop false false = false
bv_wf n n1 bv_wf n n2 bv_wf n (op n1 n2).
Proof.
intros Hbits Hnonneg Hop [? Hok1]%bv_wf_in_range [? Hok2]%bv_wf_in_range. apply bv_wf_in_range.
split; [lia|].
apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l ?.
eapply Z_bounded_iff_bits_nonneg in Hok1;[|try done; lia..].
eapply Z_bounded_iff_bits_nonneg in Hok2;[|try done; lia..].
by rewrite Hbits, Hok1, Hok2.
Qed.
Lemma bv_wrap_land n z :
bv_wrap n z = Z.land z (Z.ones (Z.of_N n)).
Proof. by rewrite Z.land_ones by lia. Qed.
......@@ -290,13 +276,57 @@ Lemma bv_wrap_spec_high n z i:
Z.testbit (bv_wrap n z) i = false.
Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [|done]. lia. Qed.
(** Definition of BvWf *)
Class BvWf (n : N) (z : Z) : Prop :=
bv_wf : (0 <=? z) && (z <? bv_modulus n)
.
Global Hint Mode BvWf + + : typeclass_instances.
Global Instance bv_wf_pi n z : ProofIrrel (BvWf n z).
Proof. unfold BvWf. apply _. Qed.
Global Instance bv_wf_dec n z : Decision (BvWf n z).
Proof. unfold BvWf. apply _. Defined.
Typeclasses Opaque BvWf.
Ltac solve_BvWf :=
lazymatch goal with
|- BvWf ?n ?v =>
check_closed v;
try (vm_compute; exact I);
fail "Bitvector constant" v "does not fit into" n "bits"
end.
Global Hint Extern 10 (BvWf _ _) => solve_BvWf : typeclass_instances.
Lemma bv_wf_in_range n z:
BvWf n z 0 z < bv_modulus n.
Proof. unfold BvWf. by rewrite andb_True, !Is_true_true, Z.leb_le, Z.ltb_lt. Qed.
Lemma bv_wrap_wf n z :
BvWf n (bv_wrap n z).
Proof. apply bv_wf_in_range. apply bv_wrap_in_range. Qed.
Lemma bv_wf_bitwise_op {n} op bop n1 n2 :
( k, Z.testbit (op n1 n2) k = bop (Z.testbit n1 k) (Z.testbit n2 k))
(0 n1 0 n2 0 op n1 n2)
bop false false = false
BvWf n n1 BvWf n n2 BvWf n (op n1 n2).
Proof.
intros Hbits Hnonneg Hop [? Hok1]%bv_wf_in_range [? Hok2]%bv_wf_in_range. apply bv_wf_in_range.
split; [lia|].
apply Z_bounded_iff_bits_nonneg; [lia..|]. intros l ?.
eapply Z_bounded_iff_bits_nonneg in Hok1;[|try done; lia..].
eapply Z_bounded_iff_bits_nonneg in Hok2;[|try done; lia..].
by rewrite Hbits, Hok1, Hok2.
Qed.
(** * Definition of [bv n] *)
Record bv (n : N) := BV {
bv_unsigned : Z;
bv_is_wf : bv_wf n bv_unsigned;
bv_is_wf : BvWf n bv_unsigned;
}.
Global Arguments bv_unsigned {_}.
Global Arguments bv_is_wf {_}.
Global Arguments BV _ _ {_}.
Add Printing Constructor bv.
Global Arguments bv_unsigned : simpl never.
......@@ -315,10 +345,10 @@ Lemma bv_neq n (b1 b2 : bv n) :
Proof. unfold not. by rewrite bv_eq. Qed.
Definition Z_to_bv_checked (n : N) (z : Z) : option (bv n) :=
guard (bv_wf n z) as H; Some (BV n z H).
guard (BvWf n z) as H; Some (@BV n z H).
Program Definition Z_to_bv (n : N) (z : Z) : bv n :=
BV n (bv_wrap n z) _.
@BV n (bv_wrap n z) _.
Next Obligation. apply bv_wrap_wf. Qed.
Lemma Z_to_bv_unsigned n z:
......@@ -335,11 +365,11 @@ Lemma Z_to_bv_small n z:
Proof. rewrite Z_to_bv_unsigned. apply bv_wrap_small. Qed.
Lemma bv_unsigned_BV n z Hwf:
bv_unsigned (BV n z Hwf) = z.
bv_unsigned (@BV n z Hwf) = z.
Proof. done. Qed.
Lemma bv_signed_BV n z Hwf:
bv_signed (BV n z Hwf) = bv_swrap n z.
bv_signed (@BV n z Hwf) = bv_swrap n z.
Proof. done. Qed.
Lemma bv_unsigned_in_range n (b : bv n):
......@@ -421,7 +451,7 @@ Proof.
Qed.
Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(BV _ v1 p1) '(BV _ v2 p2),
Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(@BV _ v1 p1) '(@BV _ v2 p2),
match decide (v1 = v2) with
| left eqv => left _
| right eqv => right _
......@@ -448,30 +478,14 @@ Next Obligation.
- apply lookup_seqZ. split; [done|]. rewrite Z2Nat.id; lia.
- apply bv_eq. rewrite Z_to_bv_small; rewrite Z2Nat.id; lia.
Qed.
Lemma bv_1_ind (P : bv 1 Prop) :
P (BV 1 1 ltac:(done)) P (BV 1 0 ltac:(done)) b : bv 1, P b.
P (@BV 1 1 I) P (@BV 1 0 I) b : bv 1, P b.
Proof.
intros ??. apply Forall_finite. repeat constructor.
- by assert ((BV 1 0 (conj eq_refl eq_refl)) = (Z_to_bv 1 (Z.of_nat 0 + 0))) as <- by by apply bv_eq.
- by assert ((BV 1 1 (conj eq_refl eq_refl)) = (Z_to_bv 1 (Z.of_nat 1 + 0))) as <- by by apply bv_eq.
- by assert ((@BV 1 0 I) = (Z_to_bv 1 (Z.of_nat 0 + 0))) as <- by by apply bv_eq.
- by assert ((@BV 1 1 I) = (Z_to_bv 1 (Z.of_nat 1 + 0))) as <- by by apply bv_eq.
Qed.
(** * Notation for [bv n] *)
Ltac solve_bitvector_eq :=
try (vm_compute; exact (conj eq_refl eq_refl));
lazymatch goal with
|- bv_wf ?n ?v =>
fail "Bitvector constant" v "does not fit into" n "bits"
end.
Notation "'[BV{' l } v ]" := (BV l v _) (at level 9, only printing) : stdpp_scope.
(* TODO: Somehow the following version creates a warning. *)
(* Notation "'[BV{' l } v ]" := (BV l v _) (at level 9, format "[BV{ l } v ]", only printing) : stdpp_scope. *)
Notation "'[BV{' l } v ]" := (BV l v ltac:(solve_bitvector_eq)) (at level 9, only parsing) : stdpp_scope.
(** * Automation *)
Ltac bv_saturate :=
repeat match goal with b : bv _ |- _ => first [
......@@ -568,107 +582,9 @@ Ltac bv_wrap_simplify :=
Ltac bv_wrap_simplify_solve :=
bv_wrap_simplify; f_equal; lia.
(** ** ring_simplify-based automation for simplifying bv_wrap *)
(* TODO: Where to put the following automation? And how should it best be implemented? *)
Definition bv_wrap_simplify_marker (z1 z2 : Z) : Z := z1 + z2.
Lemma bv_wrap_simplify_marker_intro n z x:
bv_wrap n (bv_wrap_simplify_marker z 0) = x
bv_wrap n z = x.
Proof. intros <-. unfold bv_wrap_simplify_marker. f_equal. lia. Qed.
Lemma bv_wrap_simplify_marker_move n z1 z2 x m:
bv_wrap n (bv_wrap_simplify_marker z1 (z2 + m)) = x
bv_wrap n (bv_wrap_simplify_marker (z1 + z2) m) = x.
Proof. intros <-. unfold bv_wrap_simplify_marker. f_equal. lia. Qed.
Lemma bv_wrap_simplify_marker_remove n z1 z2 x m:
bv_wrap n (bv_wrap_simplify_marker z1 m) = x
bv_wrap n (bv_wrap_simplify_marker (z1 + z2 * bv_modulus n) m) = x.
Proof.
intros <-. unfold bv_wrap_simplify_marker.
assert ((z1 + z2 * bv_modulus n + m) = (z1 + m + z2 * bv_modulus n)) as -> by lia.
by apply bv_wrap_add_modulus.
Qed.
Lemma bv_wrap_simplify_marker_remove_sub n z1 z2 x m:
bv_wrap n (bv_wrap_simplify_marker z1 m) = x
bv_wrap n (bv_wrap_simplify_marker (z1 - z2 * bv_modulus n) m) = x.
Proof.
intros <-. unfold bv_wrap_simplify_marker.
assert ((z1 - z2 * bv_modulus n + m) = (z1 + m - z2 * bv_modulus n)) as -> by lia.
by apply bv_wrap_sub_modulus.
Qed.
Lemma bv_wrap_simplify_marker_move_end n z x m:
bv_wrap n (z + m) = x
bv_wrap n (bv_wrap_simplify_marker z m) = x.
Proof. intros <-. unfold bv_wrap_simplify_marker. f_equal. Qed.
Lemma bv_wrap_simplify_marker_remove_end n z x m:
bv_wrap n m = x
bv_wrap n (bv_wrap_simplify_marker (z * bv_modulus n) m) = x.
Proof. intros <-. unfold bv_wrap_simplify_marker. rewrite Z.add_comm. apply bv_wrap_add_modulus. Qed.
Lemma bv_wrap_simplify_marker_remove_end_opp n z x m:
bv_wrap n m = x
bv_wrap n (bv_wrap_simplify_marker (- z * bv_modulus n) m) = x.
Proof. intros <-. unfold bv_wrap_simplify_marker. rewrite Z.add_comm. apply bv_wrap_add_modulus. Qed.
Lemma Zmul_assoc_comm n2 n1 n3 : n1 * n2 * n3 = n1 * n3 * n2.
Proof. lia. Qed.
Lemma Zpow_2_mul a : a ^ 2 = a * a.
Proof. lia. Qed.
Local Ltac bv_wrap_simplify_cancel :=
apply bv_wrap_simplify_marker_intro;
repeat first [ apply bv_wrap_simplify_marker_remove | apply bv_wrap_simplify_marker_remove_sub | apply bv_wrap_simplify_marker_move];
first [ apply bv_wrap_simplify_marker_remove_end | apply bv_wrap_simplify_marker_remove_end_opp | apply bv_wrap_simplify_marker_move_end].
(** [bv_wrap_simplify_left] applies for goals of the form [bv_wrap n z1 = _] and
tries to simplify them by removing any [bv_wrap] inside z1. *)
Ltac bv_wrap_simplify_left' :=
repeat lazymatch goal with
| |- bv_wrap _ ?x = _ =>
match x with
| context [ bv_wrap ?n ?z ] =>
let x := fresh "x" in
let Heq := fresh "Heq" in
pose proof (bv_wrap_factor_intro n z) as [x [_ Heq]];
rewrite !Heq;
clear Heq
end
end;
match goal with | |- bv_wrap _ ?z = _ => ring_simplify z end;
repeat match goal with | |- context [- bv_modulus ?n * ?z] => rewrite (Z.mul_opp_comm (bv_modulus n) z) end;
repeat match goal with | |- context [bv_modulus ?n * ?z] => rewrite (Z.mul_comm (bv_modulus n) z) end;
repeat match goal with | |- context [(bv_modulus ?n ^ ?m) * ?z] => rewrite (Z.mul_comm (bv_modulus n ^ m) z) end;
repeat match goal with | |- context [?z1 * bv_modulus ?n * ?z2] => rewrite (Zmul_assoc_comm (bv_modulus n) z1 z2) end;
repeat match goal with | |- context [?z1 * (bv_modulus ?n ^ ?m) * ?z2] => rewrite (Zmul_assoc_comm (bv_modulus n ^ m) z1 z2) end;
repeat match goal with | |- context [?n ^ 2] => rewrite (Zpow_2_mul n) end;
repeat match goal with | |- context [?z1 * (?z2 * ?z3)] => rewrite (Z.mul_assoc z1 z2 z3) end;
bv_wrap_simplify_cancel;
match goal with | |- bv_wrap _ ?z = _ => ring_simplify z end.
(** [bv_wrap_simplify] applies for goals of the form [bv_wrap n z1 = bv_wrap n z2] and
[bv_swrap n z1 = bv_swrap n z2] and tries to simplify them by removing any [bv_wrap]
and [bv_swrap] inside z1 and z2. *)
Ltac bv_wrap_simplify' :=
unfold bv_signed, bv_swrap;
try match goal with | |- _ - _ = _ - _ => f_equal end;
bv_wrap_simplify_left;
symmetry;
bv_wrap_simplify_left;
symmetry.
Ltac bv_wrap_simplify_solve' :=
bv_wrap_simplify; f_equal; lia.
(** * Operations on [bv n] *)
Program Definition bv_0 (n : N) :=
BV n 0 _.
@BV n 0 _.
Next Obligation.
intros n. apply bv_wf_in_range. split; [done| apply bv_modulus_pos].
Qed.
......@@ -689,7 +605,7 @@ Definition bv_opp {n} (x : bv n) : bv n := (* SMT: bvneg *)
Definition bv_mul {n} (x y : bv n) : bv n := (* SMT: bvmul *)
Z_to_bv n (Z.mul (bv_unsigned x) (bv_unsigned y)).
Program Definition bv_divu {n} (x y : bv n) : bv n := (* SMT: bvudiv *)
BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
@BV n (Z.div (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
intros n x y. apply bv_wf_in_range. bv_saturate.
destruct (decide (bv_unsigned y = 0)) as [->|?].
......@@ -699,7 +615,7 @@ Next Obligation.
apply Z.div_le_upper_bound; [ lia|]. nia.
Qed.
Program Definition bv_modu {n} (x y : bv n) : bv n := (* SMT: bvurem *)
BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
@BV n (Z.modulo (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
intros n x y. apply bv_wf_in_range. bv_saturate.
destruct (decide (bv_unsigned y = 0)) as [->|?].
......@@ -720,7 +636,7 @@ Definition bv_rems {n} (x y : bv n) : bv n := (* SMT: bvsrem *)
Definition bv_shiftl {n} (x y : bv n) : bv n := (* SMT: bvshl *)
Z_to_bv n (Z.shiftl (bv_unsigned x) (bv_unsigned y)).
Program Definition bv_shiftr {n} (x y : bv n) : bv n := (* SMT: bvlshr *)
BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
@BV n (Z.shiftr (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
intros n x y. apply bv_wf_in_range. bv_saturate.
split; [ apply Z.shiftr_nonneg; lia|].
......@@ -733,17 +649,17 @@ Definition bv_ashiftr {n} (x y : bv n) : bv n := (* SMT: bvashr *)
Z_to_bv n (Z.shiftr (bv_signed x) (bv_unsigned y)).
Program Definition bv_or {n} (x y : bv n) : bv n := (* SMT: bvor *)
BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
@BV n (Z.lor (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
intros. eapply bv_wf_bitwise_op; [ apply Z.lor_spec | by intros; eapply Z.lor_nonneg | done | apply bv_is_wf..].
Qed.
Program Definition bv_and {n} (x y : bv n) : bv n := (* SMT: bvand *)
BV n (Z.land (bv_unsigned x) (bv_unsigned y)) _.
@BV n (Z.land (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
intros. eapply bv_wf_bitwise_op; [ apply Z.land_spec | intros; eapply Z.land_nonneg; by left | done | apply bv_is_wf..].
Qed.
Program Definition bv_xor {n} (x y : bv n) : bv n := (* SMT: bvxor *)
BV n (Z.lxor (bv_unsigned x) (bv_unsigned y)) _.
@BV n (Z.lxor (bv_unsigned x) (bv_unsigned y)) _.
Next Obligation.
intros. eapply bv_wf_bitwise_op; [ apply Z.lxor_spec | intros; eapply Z.lxor_nonneg; naive_solver | done | apply bv_is_wf..].
Qed.
......@@ -1337,13 +1253,7 @@ Lemma bvn_eq (b1 b2 : bvn) :
Proof. split; [ naive_solver|]. destruct b1, b2; simpl; intros [??]. subst. f_equal. by apply bv_eq. Qed.
Global Program Instance bvn_eq_dec : EqDecision bvn := λ '(@bv_to_bvn n1 b1) '(@bv_to_bvn n2 b2),
match decide (n1 = n2) with
| left eqv => match decide (bv_unsigned b1 = bv_unsigned b2) with
| left eqb => left _
| right eqb => right _
end
| right eqv => right _
end.
cast_if_and (decide (n1 = n2)) (decide (bv_unsigned b1 = bv_unsigned b2)).
(* TODO: The following does not compute to eq_refl*)
Next Obligation. intros. apply bvn_eq. naive_solver. Qed.
Next Obligation. intros. intros ?%bvn_eq. naive_solver. Qed.
......@@ -1360,9 +1270,9 @@ Global Coercion bv_to_bvn : bv >-> bvn.
(** * tests *)
Section test.
Goal ([BV{10} 3 ] = [BV{10} 5]). Abort.
Fail Goal ([BV{2} 3 ] = [BV{10} 5]).
Goal ([BV{2} 3 ] =@{bvn} [BV{10} 5]). Abort.
Fail Goal ([BV{2} 4 ] = [BV{2} 5]).
Goal bvn_to_bv 2 [BV{2} 3] = Some [BV{2} 3]. done. Abort.
Goal (BV 10 3 = BV 10 5). Abort.
Fail Goal (BV 2 3 = BV 10 5).
Goal (BV 2 3 =@{bvn} BV 10 5). Abort.
Fail Goal (BV 2 4 = BV 2 5).
Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). done. Abort.
End test.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment