Skip to content

Commit

Permalink
Merge more changes during thesis writing.
Browse files Browse the repository at this point in the history
  • Loading branch information
@piyush-kurur
piyush-kurur committed May 16, 2023
2 parents 3436565 + 48e696d commit 969ce8d
Show file tree
Hide file tree
Showing 12 changed files with 218 additions and 111 deletions.
23 changes: 19 additions & 4 deletions src/Verse/AnnotatedCode.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,10 +69,25 @@ Arguments repCodeDenote [tyD sc].
(*Notation "'CODE' c" := (List.map (@inst _ _) c) (at level 58).*)
(* Notations for annotations *)

Notation "'INIT' v" := (fst (oldAndNew (str := Str _ _)) _ v) (at level 50).
(* TODO - VAL level has to be changed to be stronger than that of '='
and of b itvector arithmetic notations *)
Notation "'VAL' v" := (snd (oldAndNew (str := Str _ _)) _ v) (at level 50).
Class Evaluate (v : VariableT) tyD varType
:= eval : forall [k] [ty : verse_type_system k],
Variables.renaming v tyD -> varType v _ ty -> varType tyD _ ty.

Definition INIT [v k ty tyD f] `{StoreP (Str tyD v)} `{Evaluate v tyD f} (x : f v k ty)
:= eval (fst (oldAndNew (str := Str tyD v))) x.

Definition VAL [v k ty tyD f] `{StoreP (Str tyD v)} `{Evaluate v tyD f} (x : f v k ty)
:= eval (snd (oldAndNew (str := Str tyD v))) x.

#[export] Instance EvalVar v tyD : Evaluate v tyD (fun x k ty => x (existT _ k ty))
:= fun _ _ f x => f _ x.

Definition VecVar n (x : VariableT) [k] ty := Vector.t (x (existT _ k ty)) n.

#[export] Instance EvalVec v tyD n `{eVar : Evaluate v tyD (fun x k ty => x (existT _ k ty))}
: Evaluate v tyD (VecVar n)
:= fun _ _ f x => Vector.map (eval f (Evaluate := eVar)) x.


Notation "'ASSERT' P" := (CODE ((fun _ : StoreP (Str _ _) => P) : ann _ _)) (at level 100).

Expand Down
74 changes: 42 additions & 32 deletions src/Verse/BitVector.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,11 +41,6 @@ Definition BVones : forall sz, Bvector sz
Definition BVzeros : forall sz, Bvector sz
:= Bvect_false.


Check BVand. (* Comes directly from Bvector *)
Check BVor. (* Comes directly from Bvector *)
Check BVxor. (* Comes directly from Bvector *)

Definition BVcomp := Bneg. (* renaming for better naming convention *)

Definition BVshiftL1 sz : Bvector sz -> Bvector sz :=
Expand Down Expand Up @@ -141,6 +136,7 @@ macros that we have in the library. Facts about them will help dealing
with semantics.
*)

Definition selectLower {sz} n (vec : Bvector sz) := BVand vec (lower_ones n).
Definition selectUpper {sz} n (vec : Bvector sz) := BVand vec (upper_ones n).
Definition clearUpper {sz} n := @selectLower sz (sz -n).
Expand Down Expand Up @@ -180,14 +176,28 @@ coqdoc's pdf generation does not get stuck.
(* begin hide *)
Require Export setoid_ring.Algebra_syntax.

Instance zero_Bvector sz : Zero (Bvector sz) := N2Bv_sized sz 0.
Instance one_Bvector sz : One (Bvector sz) := N2Bv_sized sz 1.
Instance add_Bvector sz : Addition (Bvector sz) := @BVplus sz.
Instance mul_Bvector sz : Multiplication := @BVmul sz.
Instance sub_Bvector sz : Subtraction (Bvector sz) := @BVminus sz.
Instance opp_Bvector sz : Opposite (Bvector sz) := (@BVnegative sz).
(* Note : The following typeclasses (somehow) allow operators to be
used when writing bitvector annotations. Typeclass unification
allowing delayed unification is the favored theory as to why.
*)
Class AND A := and : A -> A -> A.
Class OR A := or : A -> A -> A.
Class XOR A := xor : A -> A -> A.
Class NOT A := not : A -> A.

#[export] Instance BV_and sz : AND (Bvector sz) := @BVand sz.
#[export] Instance BV_or sz : OR (Bvector sz) := @BVor sz.
#[export] Instance BV_xor sz : XOR (Bvector sz) := @BVxor sz.
#[export] Instance BV_not sz : NOT (Bvector sz) := @BVcomp sz.

#[export] Instance zero_Bvector sz : Zero (Bvector sz) := N2Bv_sized sz 0.
#[export] Instance one_Bvector sz : One (Bvector sz) := N2Bv_sized sz 1.
#[export] Instance add_Bvector sz : Addition (Bvector sz) := @BVplus sz.
#[export] Instance mul_Bvector sz : Multiplication := @BVmul sz.
#[export] Instance sub_Bvector sz : Subtraction (Bvector sz) := @BVminus sz.
#[export] Instance opp_Bvector sz : Opposite (Bvector sz) := (@BVnegative sz).

Instance setoid_bvector sz : Setoid (Bvector sz) := {| SetoidClass.equiv := eq |}.
#[export] Instance setoid_bvector sz : Setoid (Bvector sz) := {| SetoidClass.equiv := eq |}.

(* end hide *)
Definition of_Z {sz} (z : Z) : Bvector sz:=
Expand All @@ -205,33 +215,33 @@ Fixpoint pow {sz}(eta : Bvector sz)(n : nat) : Bvector sz :=
| S m => (eta * (pow eta m))
end.

Instance bitvector_power_nat (sz : nat) : Power := @pow sz.
#[export] Instance bitvector_power_nat (sz : nat) : Power := @pow sz.

Infix "=?" := (bveq) (at level 70): bitvector_scope.
(* begin hide *)

Declare Custom Entry bits.
Infix "/" := BVquot (at level 40, left associativity) : bitvector_scope.
Infix "%" := BVrem (at level 40, left associativity) : bitvector_scope.

Notation "[bits| e |]" := e (e custom bits).
Notation "( x )" := x (in custom bits at level 0).
Notation "` x `" := x (in custom bits at level 0, x constr, format "` x `").
Infix "&" := and (at level 56).
Infix "⊕" := xor (at level 57).
Infix "∣" := or (at level 59, left associativity).

Infix "*" := BVmul (in custom bits at level 40, left associativity).
Infix "&" := BVand (at level 56, only printing) : bitvector_scope.
Infix "⊕" := BVxor (at level 57, only printing) : bitvector_scope.
Infix "∣" := BVor (at level 59, left associativity, only printing) : bitvector_scope.

Infix "/" := BVquot (in custom bits at level 40, left associativity).
Infix "%" := BVrem (in custom bits at level 40, left associativity).

Infix "+" := BVplus (in custom bits at level 50, left associativity).
Infix "-" := BVminus (in custom bits at level 50, left associativity).
(* TODO : `~` should be < level 40. But conformance with some other
`~` makes it 75 here *)
Notation "~ E" := (not E) (at level 75, right associativity).


Notation "~ E" := (BVcomp E) (in custom bits at level 30, right associativity).
Infix "&" := BVand (in custom bits at level 56, left associativity).
Infix "⊕" := BVxor (in custom bits at level 57, left associativity).
Infix "|" := BVor (in custom bits at level 59, left associativity).
Notation "A ≫ m" := (BVshiftR m A) (in custom bits at level 54, left associativity).
Notation "A ≪ m" := (BVshiftL m A) (in custom bits at level 54, left associativity).
Notation "A ⋘ m" := (BVrotL m A) (in custom bits at level 54, left associativity).
Notation "A ⋙ m" := (BVrotR m A) (in custom bits at level 54, left associativity).
Notation "⟦ A ⟧" := (@Bv2N _ A) (in custom bits).
(* TODO : Why do we have bitvector_scope at all? These notations don't
really overload any existing notations.
*)
Notation "A ≫ m" := (BVshiftR m A) (at level 54, left associativity) : bitvector_scope.
Notation "A ≪ m" := (BVshiftL m A) (at level 54, left associativity) : bitvector_scope.
Notation "A ⋘ m" := (BVrotL m A) (at level 54, left associativity) : bitvector_scope.
Notation "A ⋙ m" := (BVrotR m A) (at level 54, left associativity) : bitvector_scope.
Notation "⟦ A ⟧" := (@Bv2N _ A) : bitvector_scope.
(* end hide *)
22 changes: 11 additions & 11 deletions src/Verse/BitVector/ArithRing.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,18 +3,18 @@ Require Import Verse.BitVector.
Require Import Verse.BitVector.Facts.
Import ArithmInternals.

Global Hint Resolve Bv2N_lt_pow_2_size Bv2N_mod_2_size : bitvector_arithm.
#[export] Hint Resolve Bv2N_lt_pow_2_size Bv2N_mod_2_size : bitvector_arithm.

(* These rewrites will take care of expressing the bitwise addition
multiplications in terms of its modulo definitions.
*)

Hint Rewrite Bv2N_plus_mod Bv2N_mul_mod Bv2N_N2Bv_sized_mod
#[export] Hint Rewrite Bv2N_plus_mod Bv2N_mul_mod Bv2N_N2Bv_sized_mod
: bitvector_arithm.

(* This rewrites will take care of pushing the modulo outwards *)

Hint Rewrite
#[export] Hint Rewrite
N.add_mod_idemp_r N.add_mod_idemp_l
N.mul_mod_idemp_l N.mul_mod_idemp_r N.mod_1_l
N.mod_same
Expand All @@ -39,12 +39,12 @@ Ltac arithm_crush :=
Lemma Bv2N_zero_is_0 : forall sz, @Bv2N sz 0 = 0%N.
Proof.
intros.
Hint Rewrite Bv2N_false : bitvector_arithm.
#[local] Hint Rewrite Bv2N_false : bitvector_arithm.
arithm_crush.
Qed.


Hint Rewrite Bv2N_zero_is_0 : bitvector_arithm.
#[export] Hint Rewrite Bv2N_zero_is_0 : bitvector_arithm.


Lemma BVadd_0_l : forall sz (v : Bvector sz), 0 + v = v.
Expand Down Expand Up @@ -72,7 +72,7 @@ Lemma Bv2N_le_2_power : forall sz (v : Bvector sz), (Bv2N v <= 2 ^ (N.of_nat sz)
arithm_crush.
Qed.

Global Hint Resolve Bv2N_le_2_power : bitvector_arithm.
#[export] Hint Resolve Bv2N_le_2_power : bitvector_arithm.

Lemma one_lt_2_power : forall sz, (1 < 2 ^ N.of_nat (S sz))%N.
intros.
Expand All @@ -84,14 +84,14 @@ Lemma one_lt_2_power : forall sz, (1 < 2 ^ N.of_nat (S sz))%N.
apply N.neq_succ_0.
Qed.

Global Hint Resolve one_lt_2_power : bitvector_arithm.
#[export] Hint Resolve one_lt_2_power : bitvector_arithm.

Lemma Bv2N_one_is_1 : forall sz, @Bv2N (S sz) 1 = 1%N.
intro.
arithm_crush.
Qed.

Hint Rewrite Bv2N_one_is_1 : bitvector_arithm.
#[export] Hint Rewrite Bv2N_one_is_1 : bitvector_arithm.

Lemma BVmul_1_l : forall sz (v : Bvector (S sz)), 1 * v = v.
arithm_crush.
Expand Down Expand Up @@ -119,8 +119,8 @@ Qed.
Lemma BVsub_def : forall sz (v1 v2 : Bvector sz), v1 - v2 = v1 + (- v2).
Proof.
intros.
Hint Rewrite Bv2N_N2Bv_sized_mod N.sub_diag : bitvector_arithm.
Local Hint Resolve Bv2N_lt_pow_2_size : bitvector_arithm.
#[local] Hint Rewrite Bv2N_N2Bv_sized_mod N.sub_diag : bitvector_arithm.
#[local] Hint Resolve Bv2N_lt_pow_2_size : bitvector_arithm.
arithm_crush.
rewrite N.add_sub_assoc;
arithm_crush.
Expand All @@ -129,7 +129,7 @@ Qed.

Lemma BVopp_def : forall sz (v : Bvector sz), v + (- v) = 0.
Proof.
Hint Rewrite Bv2N_N2Bv_sized_mod N.sub_diag
#[local] Hint Rewrite Bv2N_N2Bv_sized_mod N.sub_diag
N.add_sub_assoc N.add_sub_swap
: bitvector_arithm.
arithm_crush.
Expand Down
52 changes: 26 additions & 26 deletions src/Verse/BitVector/Facts.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,21 +19,21 @@ Require Import Arith.
Require Import Verse.BitVector.
Require Import Verse.NFacts.

Global Hint Resolve
#[export] Hint Resolve
andb_comm andb_assoc andb_orb_distrib_r
orb_comm orb_assoc orb_andb_distrib_r
xorb_comm xorb_assoc
: bitvector.

Hint Rewrite andb_true_r orb_false_r xorb_true_r xorb_false_r xorb_true_l xorb_false_l : bitvector.
#[export] Hint Rewrite andb_true_r orb_false_r xorb_true_r xorb_false_r xorb_true_l xorb_false_l : bitvector.

Hint Rewrite
#[export] Hint Rewrite
Nat.sub_0_r Nat.sub_diag Nat.mod_0_l Nat.mod_mod
Nat.double_twice Nat.div2_succ_double Nat.div2_double
Nat.add_1_r Nat.add_0_r Nat.add_0_l
: bitvector.

Global Hint Unfold BVshiftR BVshiftL : bitvector.
#[export] Hint Unfold BVshiftR BVshiftL : bitvector.

Module Internal.
Lemma vector_0_nil : forall A (vec : Vector.t A 0), vec = [].
Expand Down Expand Up @@ -254,8 +254,8 @@ End BinOpInternals.


Import BinOpInternals.
Global Hint Resolve map2_comm map2_assoc map2_distr : bitvector.
Hint Rewrite BVzeros_nth BVones_nth : bitvector.
#[export] Hint Resolve map2_comm map2_assoc map2_distr : bitvector.
#[export] Hint Rewrite BVzeros_nth BVones_nth : bitvector.

(* end hide *)

Expand Down Expand Up @@ -424,8 +424,8 @@ Qed.
Lemma rotMSB_LSB_inv : forall sz (v : Bvector sz),
rotTowardsMSB sz (rotTowardsLSB sz v) = v.
Proof.
Hint Rewrite rotMSB_S_n popout_shiftin :bitvector.
Global Hint Unfold rotTowardsLSB : bitvector.
#[local] Hint Rewrite rotMSB_S_n popout_shiftin :bitvector.
#[export] Hint Unfold rotTowardsLSB : bitvector.
intros sz v.
destruct v; crush.
Qed.
Expand Down Expand Up @@ -478,7 +478,7 @@ Module ArithmInternals.
intros sz vec. induct_on sz.
Qed.

Hint Rewrite shiftin_false : bitvector.
#[export] Hint Rewrite shiftin_false : bitvector.


Lemma Bv2N_shiftR_1 : forall sz b (vec : Bvector sz),
Expand All @@ -488,26 +488,26 @@ Module ArithmInternals.
induct_on vec.
Qed.

Hint Rewrite Bv2N_shiftR_1 : bitvector.
#[export] Hint Rewrite Bv2N_shiftR_1 : bitvector.


Lemma Bv2N_shiftR_1_div : forall sz (vec : Bvector sz), Bv2N (BVshiftR1 vec) = N.div2 (Bv2N vec).
Proof.
intros sz vec.
Hint Rewrite shiftin_cons shiftin_false N.div2_double Ndouble_twice : bitvector.
#[local] Hint Rewrite shiftin_cons shiftin_false N.div2_double Ndouble_twice : bitvector.
unfold BVshiftR1.
unfold BshiftRl; unfold Bhigh;
induction vec; crush.
Qed.

Hint Rewrite Bv2N_shiftR_1_div : bitvector.
#[export] Hint Rewrite Bv2N_shiftR_1_div : bitvector.

Lemma inj_shiftR : forall sz n (vec : Bvector sz),
Bv2N (BVshiftR n vec) = N.shiftr (Bv2N vec) (N.of_nat n).
Proof.
intros sz n vec.
unfold BVshiftR.
Hint Rewrite N.shiftr_succ_r : bitvector.
#[local] Hint Rewrite N.shiftr_succ_r : bitvector.
induction n; crush.
NFacts.crush.
Qed.
Expand Down Expand Up @@ -572,7 +572,7 @@ Qed.

Lemma Bv2N_N2Bv_sized_mod : forall sz x, Bv2N (N2Bv_sized sz x) = (x mod 2^N.of_nat sz)%N.
Proof.
Hint Rewrite
#[local] Hint Rewrite
N2Bv_sized_0 N2Bv_sized_succ
N.mod_1_r Bv2N_cons
N.div2_div
Expand All @@ -581,7 +581,7 @@ Proof.
Nat2N.inj_succ
: bitvector.

Global Hint Resolve Nb2n_mod N.le_0_l : bitvector.
#[export] Hint Resolve Nb2n_mod N.le_0_l : bitvector.
intro sz.
induction sz as [|n IHsz]. intro x; crush.
intro x; autorewrite with bitvector; try (rewrite IHsz; rewrite N.add_cancel_r); crush.
Expand All @@ -590,9 +590,9 @@ Qed.
Lemma Bv2N_N2Bv_sized : forall sz x, N.size_nat x <= sz -> Bv2N (N2Bv_sized sz x) = x.
Proof.
intros.
Global Hint Resolve Nsize_nat_pow_2 : bitvector.
Hint Rewrite N.mod_small : bitvector.
Hint Rewrite Bv2N_N2Bv_sized_mod : bitvector.
#[export] Hint Resolve Nsize_nat_pow_2 : bitvector.
#[local] Hint Rewrite N.mod_small : bitvector.
#[local] Hint Rewrite Bv2N_N2Bv_sized_mod : bitvector.
crush.
Qed.

Expand All @@ -603,7 +603,7 @@ Proof.
(* N.size_nat (Bv2N v) <= sz *)
apply Bv2N_Nsize.
Qed.
Global Hint Resolve Bv2N_lt_pow_2_size : bitvector.
#[export] Hint Resolve Bv2N_lt_pow_2_size : bitvector.

Lemma Bv2N_mod_2_size : forall sz (v : Bvector sz), (Bv2N v mod 2^(N.of_nat sz) = Bv2N v)%N.
Proof.
Expand Down Expand Up @@ -639,13 +639,13 @@ Qed.

Lemma N_ones_size_gen : forall sz n, n <= sz -> N.size_nat (N.ones (N.of_nat n)) <= sz.
Proof.
Global Hint Resolve Nat.le_trans : bitvector.
Global Hint Resolve N_ones_size : bitvector.
#[export] Hint Resolve Nat.le_trans : bitvector.
#[export] Hint Resolve N_ones_size : bitvector.
intros sz n pfSzLeN.
crush.
Qed.

Global Hint Resolve Bv2N_N2Bv_sized_mod : bitvector.
#[export] Hint Resolve Bv2N_N2Bv_sized_mod : bitvector.

(* end hide *)

Expand All @@ -665,8 +665,8 @@ the bitvector size.

Lemma Bv2N_shiftR : forall sz n (vec : Bvector sz), Bv2N (BVshiftR n vec) = (Bv2N vec / 2^N.of_nat n)%N.
Proof.
Hint Rewrite inj_shiftR : bitvector.
Global Hint Resolve N.shiftr_div_pow2 : bitvector.
#[local] Hint Rewrite inj_shiftR : bitvector.
#[export] Hint Resolve N.shiftr_div_pow2 : bitvector.
intros sz n vec.
crush.
Qed.
Expand All @@ -680,7 +680,7 @@ Proof.
unfold lower_ones.
rewrite Nand_BVand.

Global Hint Resolve N_ones_size_gen N.land_ones : bitvector.
#[export] Hint Resolve N_ones_size_gen N.land_ones : bitvector.
rewrite Bv2N_N2Bv_sized; eauto with bitvector.
Qed.

Expand Down Expand Up @@ -710,7 +710,7 @@ Lemma Bv2N_plus : forall sz n (v0 v1 : Bvector sz),
BVN_size_nat v0 <= n -> BVN_size_nat v1 <= n -> n < sz ->
(Bv2N (BVplus v0 v1) = Bv2N v0 + Bv2N v1)%N.
Proof.
Global Hint Resolve Nadd_bound_nat_gen : bitvector.
#[export] Hint Resolve Nadd_bound_nat_gen : bitvector.
intros.
rewrite Bv2N_plus_mod;
rewrite N.mod_small; trivial.
Expand Down
Loading

0 comments on commit 969ce8d

Please sign in to comment.