diff options
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 107 |
1 files changed, 96 insertions, 11 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 8ba5138..af2b822 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -21,6 +21,7 @@ From bbv Require Import Word. From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. +From coqup Require Import Coquplib. (* end hide *) (** * Value @@ -39,6 +40,8 @@ Record value : Type := vword: word vsize }. +Search N.of_nat. + (** ** Value conversions Various conversions to different number types such as [N], [Z], [positive] and @@ -85,9 +88,18 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (uvalueToZ i). +Definition ptrToValue (i : Integers.ptrofs) : value := + ZToValue Ptrofs.wordsize (Ptrofs.unsigned i). + +Definition valueToPtr (i : value) : Integers.ptrofs := + Ptrofs.repr (uvalueToZ i). + Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) + | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z + then Some (ptrToValue off) + else None | Values.Vundef => Some (ZToValue 32 0%Z) | _ => None end. @@ -301,8 +313,8 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | val_value_lessdef_ptr: forall b off v', - off = Ptrofs.repr (valueToZ v') -> - (Z.modulo (valueToZ v') 4) = 0%Z -> + off = valueToPtr v' -> + (Z.modulo (uvalueToZ v') 4) = 0%Z -> val_value_lessdef (Vptr b off) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -379,6 +391,41 @@ Proof. apply Z.lt_le_pred in H. apply H. Qed. +Lemma valueToPtr_ptrToValue : + forall v, + valueToPtr (ptrToValue v) = v. +Proof. + intros. + unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned. + split. apply Ptrofs.unsigned_range_2. + assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma intToValue_valueToInt : + forall v, + vsize v = 32%nat -> + intToValue (valueToInt v) = v. +Proof. + intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + +Lemma ptrToValue_valueToPtr : + forall v, + vsize v = 32%nat -> + ptrToValue (valueToPtr v) = v. +Proof. + intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + Lemma valToValue_lessdef : forall v v', valToValue v = Some v' -> @@ -388,6 +435,10 @@ Proof. destruct v; try discriminate; constructor. unfold valToValue in H. inversion H. symmetry. apply valueToInt_intToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. + inv H1. symmetry. apply valueToPtr_ptrToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. + inv H1. apply Z.eqb_eq. apply Heqb0. Qed. Lemma boolToValue_ValueToBool : @@ -415,6 +466,10 @@ Proof. rewrite ZToWord_plus; auto. Qed. +Lemma ZToValue_eq : + forall w1, + (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort. + Lemma wordsize_32 : Int.wordsize = 32%nat. Proof. auto. Qed. @@ -428,6 +483,28 @@ Proof. rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. +(*Lemma intadd_vplus2 : + forall v1 v2 EQ, + vsize v1 = 32%nat -> + Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). +Proof. + intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). + rewrite (@vadd_vplus v1 v2 EQ). trivial. + unfold uvalueToZ. Search word "bound". pose proof (@uwordToZ_bound (vsize v2) (vword v2)). + rewrite H in EQ. rewrite <- EQ in H0 at 3.*) + (*rewrite zadd_vplus3. trivia*) + +Lemma valadd_vplus : + forall v1 v2 v1' v2' v v' EQ, + val_value_lessdef v1 v1' -> + val_value_lessdef v2 v2' -> + Val.add v1 v2 = v -> + vplus v1' v2' EQ = v' -> + val_value_lessdef v v'. +Proof. + intros. inv H; inv H0; constructor; simplify. + Abort. + Lemma zsub_vminus : forall sz z1 z2, (sz > 0)%nat -> @@ -452,17 +529,25 @@ Proof. unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. Qed. -(*Lemma ZToValue_valueToNat : +Lemma ZToValue_valueToNat : forall x sz, - sz > 0 -> - (x < 2^(Z.of_nat sz))%Z -> + (sz > 0)%nat -> + (0 <= x < 2^(Z.of_nat sz))%Z -> valueToNat (ZToValue sz x) = Z.to_nat x. Proof. - destruct x; intros; unfold ZToValue, valueToNat; simpl. + destruct x; intros; unfold ZToValue, valueToNat; crush. - rewrite wzero'_def. apply wordToNat_wzero. - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. - unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. - rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. - Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) - Search "inj" positive nat. -*) + clear H1. + lazymatch goal with + | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H + end. + 2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. } + + rewrite Z2Nat.inj_pow in H2; crush. + replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity. + rewrite Nat2Z.id in H2. + rewrite <- positive_nat_Z in H2. + apply Nat2Z.inj_lt in H2. + assumption. +Qed. |