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, 12 insertions, 5 deletions

diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 6a2fc82..a7e3584 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -469,6 +469,17 @@ Definition return_val fin rtrn r :=
 
 Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)).
 
+Fixpoint xmap_externctrl_params (n : nat) (fn : ident) (l : list reg) :=
+  match l with
+  | nil => ret nil
+  | arg::args =>
+    do param_reg <- map_externctrl fn (ctrl_param n);
+    do rest <- xmap_externctrl_params (S n) fn args;
+    ret ((param_reg, arg) :: rest)
+  end.
+
+Definition map_externctrl_params := xmap_externctrl_params 0.
+
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
     (n, i) =>
@@ -497,11 +508,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.")
     | Icall sig (inr fn) args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
-        do params <- traverselist
-                  (fun (a: nat * reg) => let (idx, arg) := a in
-                                    do param_reg <- map_externctrl fn (ctrl_param idx);
-                                    ret (param_reg, arg))
-                  (enumerate 0 args);
+        do params <- map_externctrl_params fn args;
 
         do _ <- declare_reg None dst 32;
         do join_state <- create_state;