1 files changed, 39 insertions, 0 deletions
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index 5d2f557e0..0678c80bb 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -50,11 +50,31 @@ End Evaluability.
 
 Section Z.
   Context {n: nat}.
+
   Instance ZEvaluable : Evaluable Z := {
     ezero := 0%Z;
 
     (* Conversions *)
     toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x => Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x));
+
+    (* Operations *)
+    eadd    := Z.add;
+    esub    := Z.sub;
+    emul    := Z.mul;
+    eshiftr := Z.shiftr;
+    eand    := Z.land;
+
+    (* Comparisons *)
+    eltb    := Z.ltb;
+    eeqb    := Z.eqb
+  }.
+
+  Instance ConstEvaluable : Evaluable Z := {
+    ezero := 0%Z;
+
+    (* Conversions *)
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
     fromT   := fun x =>
       if (Nge_dec (N.pred (Npow2 n)) (Z.to_N x))
       then Some (rwv (Z.to_N x) (Z.to_N x) (Z.to_N x))
@@ -71,6 +91,25 @@ Section Z.
     eltb    := Z.ltb;
     eeqb    := Z.eqb
   }.
+
+  Instance InputEvaluable : Evaluable Z := {
+    ezero := 0%Z;
+
+    (* Conversions *)
+    toT     := fun x => Z.of_N (orElse 0%N (option_map rwv_value x));
+    fromT   := fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x));
+
+    (* Operations *)
+    eadd    := Z.add;
+    esub    := Z.sub;
+    emul    := Z.mul;
+    eshiftr := Z.shiftr;
+    eand    := Z.land;
+
+    (* Comparisons *)
+    eltb    := Z.ltb;
+    eeqb    := Z.eqb
+  }.
 End Z.
 
 Section Word.