Prove a spec for the mapping of function params

Extracted the traversal of call args into a function and gave it a spec,
so that it can be used to prove the overall spec for the Icall instruction.

1 files changed, 5 insertions, 6 deletions

diff --git a/src/common/Monad.v b/src/common/Monad.v
index 68233b1..c9cdc1a 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -50,19 +50,18 @@ Module MonadExtra(M : Monad).
   End MonadNotation.
   Import MonadNotation.
 
-  Fixpoint sequence {A: Type} (l: list (mon A)) {struct l}: mon (list A) :=
+  Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
     match l with
     | nil => ret nil
     | x::xs =>
-      do r <- x;
-      do rs <- sequence xs;
+      do r <- f x;
+      do rs <- traverselist f xs;
       ret (r::rs)
     end.
 
-  Fixpoint traverselist {A B: Type} (f: A -> mon B) (l: list A) {struct l}: mon (list B) :=
-    sequence (map f l).
+  Definition sequence {A} : list (mon A) -> mon (list A) := traverselist (fun x => x).
 
-  Fixpoint traverseoption {A B: Type} (f: A -> mon B) (opt: option A) {struct opt}: mon (option B) :=
+  Definition traverseoption {A B: Type} (f: A -> mon B) (opt: option A) : mon (option B) :=
     match opt with
     | None => ret None
     | Some x =>