Commit 102ec06b authored by Michael Sammler's avatar Michael Sammler
Browse files

more lemmas

parent 4f7f5970
Pipeline #55450 passed with stage
in 7 minutes and 37 seconds
......@@ -192,6 +192,21 @@ 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.
Lemma bv_wrap_spec n z i:
0 i
Z.testbit (bv_wrap n z) i = bool_decide (i < Z.of_N n) && Z.testbit z i.
Proof.
intros ?. rewrite bv_wrap_land, Z.land_spec, Z_ones_spec by lia.
case_bool_decide; simpl; by rewrite ?andb_true_r, ?andb_false_r.
Qed.
Lemma bv_wrap_spec_low n z i:
0 i < Z.of_N n
Z.testbit (bv_wrap n z) i = Z.testbit z i.
Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [done|]. lia. Qed.
Lemma bv_wrap_spec_high n z i:
Z.of_N n i
Z.testbit (bv_wrap n z) i = false.
Proof. intros ?. rewrite bv_wrap_spec; [|lia]. case_bool_decide; [|done]. lia. Qed.
(** * Definition of [bv n] *)
Record bv (n : N) := BV {
......@@ -241,6 +256,10 @@ Lemma bv_unsigned_in_range n (b : bv n):
0 bv_unsigned b < bv_modulus n.
Proof. apply bv_wf_in_range. apply bv_is_wf. Qed.
Lemma Z_to_bv_bv_unsigned n (b : bv n):
Z_to_bv n (bv_unsigned b) = b.
Proof. apply bv_eq. rewrite Z_to_bv_unsigned, bv_wrap_small; [done|apply bv_unsigned_in_range]. Qed.
Lemma bv_eq_wrap n (b1 b2 : bv n) :
b1 = b2 bv_wrap n b1.(bv_unsigned) = bv_wrap n b2.(bv_unsigned).
Proof.
......@@ -251,6 +270,16 @@ Lemma bv_neq_wrap n (b1 b2 : bv n) :
b1 b2 bv_wrap n b1.(bv_unsigned) bv_wrap n b2.(bv_unsigned).
Proof. unfold not. by rewrite bv_eq_wrap. Qed.
Lemma bv_eq_signed n (b1 b2 : bv n) :
b1 = b2 bv_signed b1 = bv_signed b2.
Proof.
split; [naive_solver |].
unfold bv_signed, bv_swrap. intros ?.
assert (bv_wrap n (bv_unsigned b1 + bv_half_modulus n)
= bv_wrap n (bv_unsigned b2 + bv_half_modulus n)) as ?%bv_wrap_add_inj by lia.
by apply bv_eq_wrap.
Qed.
Lemma bv_signed_in_range n (b : bv n):
n 0%N
- bv_half_modulus n bv_signed b < bv_half_modulus n.
......@@ -280,6 +309,13 @@ Proof.
- f_equal. by apply bv_eq.
- by pose proof bv_is_wf b.
Qed.
Lemma Z_to_bv_checked_Some n a (b : bv n):
Z_to_bv_checked n a = Some b a = bv_unsigned b.
Proof.
split.
- unfold Z_to_bv_checked. case_option_guard; [|done]. intros ?. by simplify_eq.
- intros ->. apply Z_to_bv_checked_bv_unsigned.
Qed.
Global Program Instance bv_eq_dec n : EqDecision (bv n) := λ '(BV _ v1 p1) '(BV _ v2 p2),
......@@ -310,6 +346,15 @@ Next Obligation.
- 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.
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.
Qed.
(** * Notation for [bv n] *)
Ltac solve_bitvector_eq :=
......@@ -836,6 +881,16 @@ Section properties.
bv_wrap_simplify_solve.
Qed.
Lemma bv_or_0_l b1 b2 :
bv_unsigned b1 = 0
bv_or b1 b2 = b2.
Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_l. Qed.
Lemma bv_or_0_r b1 b2 :
bv_unsigned b2 = 0
bv_or b1 b2 = b1.
Proof. intros Hb. apply bv_eq. by rewrite bv_or_unsigned, Hb, Z.lor_0_r. Qed.
Lemma bv_concat_0 m n2 b1 (b2 : bv n2) :
bv_unsigned b1 = 0
bv_concat m b1 b2 = bv_zero_extend m b2.
......@@ -887,7 +942,16 @@ Section little.
apply Nat2Z.inj. rewrite Z_to_little_endian_length, ?Z2Nat.id; try lia.
Qed.
Lemma bv_of_to_little_bv x m n (b : bv x):
Lemma little_endian_to_bv_bound n bs :
0 little_endian_to_bv n bs < 2 ^ (Z.of_nat (length bs) * Z.of_N n).
Proof.
unfold little_endian_to_bv. rewrite <-(fmap_length bv_unsigned bs).
apply little_endian_to_Z_bound; [lia|].
apply Forall_forall. intros ? [? [-> ?]]%elem_of_list_fmap.
apply bv_unsigned_in_range.
Qed.
Lemma Z_to_bv_little_endian_to_bv_to_little_endian x m n (b : bv x):
0 m
x = (Z.to_N m * n)%N
Z_to_bv x (little_endian_to_bv n (bv_to_little_endian m n (bv_unsigned b))) = b.
......
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