diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-27 23:38:40 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-27 23:38:40 +0100 |
| commit | 213267be33d714dabd19ca09210b5dc1ad4f6254 (patch) | |
| tree | 4ce40a679e2ac7cf4667911bdeebdb932b56a023 /src/verilog/Value.v | |
| parent | cb00777e134464a01a9e97efb448cee7473df9d5 (diff) | |
| download | vericert-kvx-213267be33d714dabd19ca09210b5dc1ad4f6254.tar.gz vericert-kvx-213267be33d714dabd19ca09210b5dc1ad4f6254.zip | |
Add more proofs and remove Admitted
Diffstat (limited to 'src/verilog/Value.v')
| -rw-r--r-- | src/verilog/Value.v | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 0ce0bc5..34cb0d2 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -85,10 +85,11 @@ Definition intToValue (i : Integers.int) : value := Definition valueToInt (i : value) : Integers.int := Int.repr (valueToZ i). -Definition valToValue (v : Values.val) := +Definition valToValue (v : Values.val) : option value := match v with - | Values.Vint i => intToValue i - | _ => ZToValue 32 0%Z + | Values.Vint i => Some (intToValue i) + | Values.Vundef => Some (ZToValue 32 0%Z) + | _ => None end. (** Convert a [value] to a [bool], so that choices can be made based on the @@ -295,17 +296,22 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. -Search Z positive. - -Search "wordToZ". +Lemma valueToZ_ZToValue : + forall n z, + (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> + valueToZ (ZToValue (S n) z) = z. +Proof. + unfold valueToZ, ZToValue. simpl. + auto using wordToZ_ZToWord. +Qed. Lemma uvalueToZ_ZToValue : forall n z, (0 <= z < 2 ^ Z.of_nat n)%Z -> uvalueToZ (ZToValue n z) = z. Proof. - intros. unfold uvalueToZ, ZToValue. simpl. - apply uwordToZ_ZToWord. apply H. + unfold uvalueToZ, ZToValue. simpl. + auto using uwordToZ_ZToWord. Qed. Lemma valueToPos_posToValueAuto : |