Add new value type to fix Iop proof

5 files changed, 217 insertions, 67 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index a2b77e6..f58c9ae 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -19,7 +19,7 @@
 From compcert Require Import Maps.
 From compcert Require Errors Globalenvs Integers.
 From compcert Require Import AST RTL.
-From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
+From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
@@ -88,7 +88,7 @@ Import HTLMonadExtra.
 Export MonadNotation.
 
 Definition state_goto (st : reg) (n : node) : stmnt :=
-  Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
+  Vnonblock (Vvar st) (Vlit (posToValue n)).
 
 Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
   Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index 5d531d5..c5cfa3f 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import Coquplib Value.
+From coqup Require Import Coquplib ValueInt.
 From compcert Require Import Maps.
 
 Definition reg := positive.
@@ -192,7 +192,7 @@ Import AssocMapExt.
 Definition assocmap := AssocMap.t value.
 
 Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
-  get_default value (ZToValue n 0).
+  get_default value (ZToValue 0).
 
 Definition empty_assocmap : assocmap := AssocMap.empty value.
 
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index b80b614..2718a46 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -466,16 +466,9 @@ Proof.
   rewrite ZToWord_plus; auto.
 Qed.
 
-Lemma zadd_vplus3 :
-  forall w1 w2,
-  (wordToN w1 + wordToN w2 < Npow2 32)%N ->
-  valueToN (vplus (mkvalue 32 w1) (mkvalue 32 w2) eq_refl) =
-  (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N.
-Proof.
-  intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN.
-  simplify. unfold wplus. unfold wordBin.
-  rewrite wordToN_NToWord_2. trivial. assumption.
-Qed.
+Lemma ZToValue_eq :
+  forall w1,
+  (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted.
 
 Lemma wordsize_32 :
   Int.wordsize = 32%nat.
@@ -490,13 +483,7 @@ Proof.
   rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega.
 Qed.
 
-Lemma vadd_vplus :
-  forall v1 v2 EQ,
-  uvalueToZ v1 + uvalueToZ v2 = uvalueToZ (vplus v1 v2 EQ).
-Proof.
-  Admitted.
-
-Lemma intadd_vplus2 :
+(*Lemma intadd_vplus2 :
   forall v1 v2 EQ,
   vsize v1 = 32%nat ->
   Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ).
@@ -504,7 +491,7 @@ 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.
+  rewrite H in EQ. rewrite <- EQ in H0 at 3.*)
   (*rewrite zadd_vplus3. trivia*)
 
 Lemma valadd_vplus :
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
new file mode 100644
index 0000000..cc1d404
--- /dev/null
+++ b/src/verilog/ValueInt.v
@@ -0,0 +1,160 @@
+(*
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+(* begin hide *)
+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
+
+A [value] is a bitvector with a specific size. We are using the implementation
+of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
+However, we need to wrap it with an [Inductive] so that we can specify and match
+on the size of the [value]. This is necessary so that we can easily store
+[value]s of different sizes in a list or in a map.
+
+Using the default [word], this would not be possible, as the size is part of the type. *)
+
+Definition value : Type := int.
+
+(** ** Value conversions
+
+Various conversions to different number types such as [N], [Z], [positive] and
+[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
+
+Definition valueToNat (v : value) : nat :=
+  Z.to_nat (Int.unsigned v).
+
+Definition natToValue (n : nat) : value :=
+  Int.repr (Z.of_nat n).
+
+Definition valueToN (v : value) : N :=
+  Z.to_N (Int.unsigned v).
+
+Definition NToValue (n : N) : value :=
+  Int.repr (Z.of_N n).
+
+Definition ZToValue (z : Z) : value :=
+  Int.repr z.
+
+Definition valueToZ (v : value) : Z :=
+  Int.signed v.
+
+Definition uvalueToZ (v : value) : Z :=
+  Int.unsigned v.
+
+Definition posToValue (p : positive) : value :=
+  Int.repr (Z.pos p).
+
+Definition valueToPos (v : value) : positive :=
+  Z.to_pos (Int.unsigned v).
+
+Definition intToValue (i : Integers.int) : value := i.
+
+Definition valueToInt (i : value) : Integers.int := i.
+
+Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i.
+
+Definition valueToPtr (i : value) : Integers.ptrofs :=
+  Ptrofs.of_int i.
+
+Search Ptrofs.of_int Ptrofs.to_int.
+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 0%Z)
+  | _ => None
+  end.
+
+(** Convert a [value] to a [bool], so that choices can be made based on the
+result. This is also because comparison operators will give back [value] instead
+of [bool], so if they are in a condition, they will have to be converted before
+they can be used. *)
+
+Definition valueToBool (v : value) : bool :=
+  if Z.eqb (uvalueToZ v) 0 then true else false.
+
+Definition boolToValue (b : bool) : value :=
+  natToValue (if b then 1 else 0).
+
+(** ** Arithmetic operations *)
+
+Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.
+intros; subst; assumption. Defined.
+
+Lemma unify_word_unfold :
+  forall sz w,
+  unify_word sz sz w eq_refl = w.
+Proof. auto. Qed.
+
+Inductive val_value_lessdef: val -> value -> Prop :=
+| val_value_lessdef_int:
+    forall i v',
+    i = valueToInt v' ->
+    val_value_lessdef (Vint i) v'
+| val_value_lessdef_ptr:
+    forall b off v',
+    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.
+
+Inductive opt_val_value_lessdef: option val -> value -> Prop :=
+| opt_lessdef_some:
+    forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v'
+| opt_lessdef_none: forall v, opt_val_value_lessdef None v.
+
+Lemma valueToZ_ZToValue :
+  forall z,
+  (Int.min_signed <= z <= Int.max_signed)%Z ->
+  valueToZ (ZToValue z) = z.
+Proof. auto using Int.signed_repr. Qed.
+
+Lemma uvalueToZ_ZToValue :
+  forall z,
+  (0 <= z <= Int.max_unsigned)%Z ->
+  uvalueToZ (ZToValue z) = z.
+Proof. auto using Int.unsigned_repr. 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.
+  unfold valueToInt. unfold intToValue in H1. auto.
+  inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate.
+  inv H1. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial.
+  inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate.
+  inv H1. apply Z.eqb_eq. apply Heqb0.
+Qed.
+
+Local Open Scope Z.
+
+Ltac word_op_value H :=
+  intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold;
+  rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega.
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 555ddbd..5ef4dda 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -29,11 +29,9 @@ Require Import Lia.
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array.
-From compcert Require Integers Events.
-From compcert Require Import Errors Smallstep Globalenvs.
-
-Import HexNotationValue.
+From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array.
+From compcert Require Events.
+From compcert Require Import Integers Errors Smallstep Globalenvs.
 
 Local Open Scope assocmap.
 
@@ -80,7 +78,7 @@ Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr :
 Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value :=
   match a ! r with
   | None => None
-  | Some arr => Some (Option.default (NToValue 32 0) (Option.join (array_get_error i arr)))
+  | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr)))
   end.
 
 Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr :=
@@ -164,8 +162,8 @@ Inductive expr : Type :=
 | Vunop : unop -> expr -> expr
 | Vternary : expr -> expr -> expr -> expr.
 
-Definition posToExpr (sz : nat) (p : positive) : expr :=
-  Vlit (posToValue sz p).
+Definition posToExpr (p : positive) : expr :=
+  Vlit (posToValue p).
 
 (** ** Statements *)
 
@@ -245,7 +243,7 @@ Definition program := AST.program fundef unit.
 (** Convert a [positive] to an expression directly, setting it to the right
     size. *)
 Definition posToLit (p : positive) : expr :=
-  Vlit (posToValueAuto p).
+  Vlit (posToValue p).
 
 Coercion Vlit : value >-> expr.
 Coercion Vvar : reg >-> expr.
@@ -298,37 +296,43 @@ Inductive state : Type :=
            (m : module)
            (args : list value), state.
 
-Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value :=
+Definition binop_run (op : binop) (v1 v2 : value) : option value :=
   match op with
-  | Vadd => vplus
-  | Vsub => vminus
-  | Vmul => vmul
-  | Vdiv => vdivs
-  | Vdivu => vdiv
-  | Vmod => vmods
-  | Vmodu => vmod
-  | Vlt => vlts
-  | Vltu => vlt
-  | Vgt => vgts
-  | Vgtu => vgt
-  | Vle => vles
-  | Vleu => vle
-  | Vge => vges
-  | Vgeu => vge
-  | Veq => veq
-  | Vne => vne
-  | Vand => vand
-  | Vor => vor
-  | Vxor => vxor
-  | Vshl => vshl
-  | Vshr => vshr
-  | Vshru => vshr (* FIXME: should not be the same operation. *)
+  | Vadd => Some (Int.add v1 v2)
+  | Vsub => Some (Int.sub v1 v2)
+  | Vmul => Some (Int.mul v1 v2)
+  | Vdiv => if Int.eq v2 Int.zero
+               || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone
+            then None
+            else Some (Int.divs v1 v2)
+  | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2)
+  | Vmod => if Int.eq v2 Int.zero
+               || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone
+            then None
+            else Some (Int.mods v1 v2)
+  | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2)
+  | Vlt => Some (boolToValue (Int.lt v1 v2))
+  | Vltu => Some (boolToValue (Int.ltu v1 v2))
+  | Vgt => Some (boolToValue (Int.lt v2 v1))
+  | Vgtu => Some (boolToValue (Int.ltu v2 v1))
+  | Vle => Some (boolToValue (negb (Int.lt v2 v1)))
+  | Vleu => Some (boolToValue (negb (Int.ltu v2 v1)))
+  | Vge => Some (boolToValue (negb (Int.lt v1 v2)))
+  | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2)))
+  | Veq => Some (boolToValue (Int.eq v1 v2))
+  | Vne => Some (boolToValue (negb (Int.eq v1 v2)))
+  | Vand => Some (Int.and v1 v2)
+  | Vor => Some (Int.or v1 v2)
+  | Vxor => Some (Int.xor v1 v2)
+  | Vshl => Some (Int.shl v1 v2)
+  | Vshr => Some (Int.shr v1 v2)
+  | Vshru => Some (Int.shru v1 v2)
   end.
 
-Definition unop_run (op : unop) : value -> value :=
+Definition unop_run (op : unop) (v1 : value) : value :=
   match op with
-  | Vneg => vnot
-  | Vnot => vbitneg
+  | Vneg => Int.notbool v1
+  | Vnot => Int.not v1
   end.
 
 Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop :=
@@ -349,11 +353,10 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       fext!r = Some v ->
       expr_runp fext reg stack (Vinputvar r) v
   | erun_Vbinop :
-      forall fext reg stack op l r lv rv oper EQ resv,
+      forall fext reg stack op l r lv rv resv,
       expr_runp fext reg stack l lv ->
       expr_runp fext reg stack r rv ->
-      oper = binop_run op ->
-      resv = oper lv rv EQ ->
+      Some resv = binop_run op lv rv ->
       expr_runp fext reg stack (Vbinop op l r) resv
   | erun_Vunop :
       forall fext reg stack u vu op oper resv,
@@ -394,7 +397,7 @@ Local Open Scope error_monad_scope.
 Definition access_fext (f : fext) (r : reg) : res value :=
   match AssocMap.get r f with
   | Some v => OK v
-  | _ => OK (ZToValue 1 0)
+  | _ => OK (ZToValue 0)
   end.
 
 (* TODO FIX Vvar case without default *)
@@ -652,8 +655,8 @@ other arguments to the module are also to be supported. *)
 
 Definition initial_fextclk (m : module) : fextclk :=
   fun x => match x with
-           | S O => (AssocMap.set (mod_reset m) (ZToValue 1 1) empty_assocmap)
-           | _ => (AssocMap.set (mod_reset m) (ZToValue 1 0) empty_assocmap)
+           | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap)
+           | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap)
            end.
 
 (*Definition module_run (n : nat) (m : module) : res assocmap :=
@@ -727,21 +730,21 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
       step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa')
 | step_finish :
     forall asr asa sf retval m st g,
-    asr!(m.(mod_finish)) = Some (1'h"1") ->
+    asr!(m.(mod_finish)) = Some (ZToValue 1) ->
     asr!(m.(mod_return)) = Some retval ->
     step g (State sf m st asr asa) Events.E0 (Returnstate sf retval)
 | step_call :
     forall g res m args,
     step g (Callstate res m args) Events.E0
          (State res m m.(mod_entrypoint)
-          (AssocMap.set m.(mod_st) (posToValue 32 m.(mod_entrypoint))
+          (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint))
            (init_params args m.(mod_args)))
           (empty_stack m))
 | step_return :
     forall g m asr i r sf pc mst asa,
     mst = mod_st m ->
     step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0
-         (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i)
+         (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i)
                 (empty_stack m)).
 Hint Constructors step : verilog.