From 8a260a8b81617e192fc929e0189fd3df1327f80a Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 30 Jun 2020 00:04:39 +0100
Subject: Add equivalence between int add value add

---
 src/verilog/Value.v | 64 ++++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 54 insertions(+), 10 deletions(-)

diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index c380ca7..3c5ed04 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -111,8 +111,7 @@ intros; subst; assumption. Defined.
 Lemma unify_word_unfold :
   forall sz w,
   unify_word sz sz w eq_refl = w.
-Proof.
-  intros. unfold unify_word. Admitted.
+Proof. auto. Qed.
 
 Definition value_eq_size:
   forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }.
@@ -330,6 +329,12 @@ Proof.
   auto using uwordToZ_ZToWord.
 Qed.
 
+Lemma uvalueToZ_ZToValue_full :
+  forall sz : nat,
+  (0 < sz)%nat ->
+  forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z.
+Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed.
+
 Lemma ZToValue_uvalueToZ :
   forall v,
   ZToValue (vsize v) (uvalueToZ v) = v.
@@ -390,19 +395,58 @@ Lemma boolToValue_ValueToBool :
   valueToBool (boolToValue 32 b) = b.
 Proof. destruct b; auto. Qed.
 
-Lemma intToValue_eq_size :
-  forall n1 n2,
-  vsize (intToValue n1) = vsize (intToValue n2).
-Proof. auto. Qed.
-
 Local Open Scope Z.
 
+Ltac eq_op H :=
+  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
+  rewrite <- H; rewrite uwordToZ_ZToWord; auto.
+
 Lemma zadd_vplus :
   forall z1 z2,
-  valueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2.
+  0 <= z1 + z2 < 2 ^ 32 ->
+  uvalueToZ (vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 + z2.
+Proof. eq_op ZToWord_plus. Qed.
+
+Lemma zadd_vplus2 :
+  forall z1 z2,
+  vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2).
 Proof.
-  intros. unfold valueToZ, ZToValue. simpl.
-  Admitted.
+  intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl.
+  rewrite ZToWord_plus; auto.
+Qed.
+
+Lemma intadd_vplus :
+  forall i1 i2,
+  valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2.
+Proof.
+  intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus2.
+  rewrite uvalueToZ_ZToValue_full. rewrite <- Int.unsigned_repr_eq.
+  rewrite Int.repr_unsigned. auto. omega.
+Qed.
+
+Lemma zsub_vminus :
+  forall z1 z2,
+  0 <= z1 - z2 < 2 ^ 32 ->
+  uvalueToZ (vminus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 - z2.
+Proof. eq_op ZToWord_minus. Qed.
+
+Lemma zmul_vmul :
+  forall z1 z2,
+  0 <= z1 * z2 < 2 ^ 32 ->
+  uvalueToZ (vmul (ZToValue 32 z1) (ZToValue 32 z2) eq_refl) = z1 * z2.
+Proof. eq_op ZToWord_mult. Qed.
+
+Local Open Scope N.
+Lemma zdiv_vdiv :
+  forall n1 n2,
+  n1 < 2 ^ 32 ->
+  n2 < 2 ^ 32 ->
+  n1 / n2 < 2 ^ 32 ->
+  valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2.
+Proof.
+  intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv.
+  unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto.
+Qed.
 
 (*Lemma ZToValue_valueToNat :
   forall x sz,
-- 
cgit