diff options
author | James Pollard <james@pollard.dev> | 2020-06-02 15:28:43 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-02 15:28:43 +0100 |
commit | 6d11e8674a3bf910d0df6600e8db9e8748844cf0 (patch) | |
tree | b395c35b59825df6bc5b6c052499d7aac3a5d83d /src/verilog | |
parent | 66c6f9da947d96683391105a99f570396864491b (diff) | |
parent | 5416713c9d6a64839fabf2a923e4dd3bb25ac5fc (diff) | |
download | vericert-6d11e8674a3bf910d0df6600e8db9e8748844cf0.tar.gz vericert-6d11e8674a3bf910d0df6600e8db9e8748844cf0.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/verilog')
-rw-r--r-- | src/verilog/Value.v | 35 |
1 files changed, 33 insertions, 2 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 34cb0d2..efbd99c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -83,7 +83,7 @@ Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). Definition valueToInt (i : value) : Integers.int := - Int.repr (valueToZ i). + Int.repr (uvalueToZ i). Definition valToValue (v : Values.val) : option value := match v with @@ -292,7 +292,7 @@ End HexNotationValue. Inductive val_value_lessdef: val -> value -> Prop := | val_value_lessdef_int: forall i v', - Integers.Int.unsigned i = valueToZ v' -> + i = valueToInt v' -> val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. @@ -314,6 +314,15 @@ Proof. auto using uwordToZ_ZToWord. Qed. +Lemma ZToValue_uvalueToZ : + forall v, + ZToValue (vsize v) (uvalueToZ v) = v. +Proof. + intros. + unfold ZToValue, uvalueToZ. + rewrite ZToWord_uwordToZ. destruct v; auto. +Qed. + Lemma valueToPos_posToValueAuto : forall p, valueToPos (posToValueAuto p) = p. Proof. @@ -325,3 +334,25 @@ Proof. inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. + intros. + unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned. + split. apply Int.unsigned_range_2. + assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma valToValue_lessdef : + forall v v', + valToValue v = Some v' -> + val_value_lessdef v v'. +Proof. + intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. + symmetry. apply valueToInt_intToValue. +Qed. |