Give a (questionable) translation spec for HTLgen

I am not yet convinced it is the right one, particularly around the way
I've used existentials. I will be updating it as I progress with the proof.

2 files changed, 61 insertions, 39 deletions

diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index a3c0ca6..5f9e17d 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -461,26 +461,28 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
                   end)
            (enumerate 0 ns).
 
-(** [mk_fork] creates a datapath statement which sets up the execution of a *)
-Definition mk_fork (m : ident) (args : list reg) : mon datapath_stmnt :=
-  do reset_reg <- map_externctrl m ctrl_reset;
-  do param_assigns <- traverselist
-                (fun (a: (nat * reg)) => let (idx, arg) := a in
-                                    do param_reg <- map_externctrl m (ctrl_param idx);
-                                    ret (Vnonblock (Vvar param_reg) (Vvar arg)))
-                (enumerate 0 args);
-  let reset_mod := Vnonblock (Vvar reset_reg) (posToLit 1) in
+(** [fork] a datapath statement which sets up the execution of a function *)
+Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt :=
+  let reset_mod := Vnonblock (Vvar rst) (posToLit 1) in
   let assign_params :=
-      List.fold_left (fun (acc : stmnt) (s : stmnt) => Vseq acc s)
-                     param_assigns Vskip in
-  ret (Vseq reset_mod assign_params).
+      List.fold_left (fun acc (a : reg*reg) => let (dst, src) := a in Vseq (nonblock dst (Vvar src)) acc)
+                     params Vskip in
+  Vseq reset_mod assign_params.
 
-Definition mk_join (m : ident) (dst : reg) : mon datapath_stmnt :=
-  do return_reg <- map_externctrl m ctrl_return;
-  do reset_reg <- map_externctrl m ctrl_reset;
-  let set_result := Vnonblock (Vvar dst) (Vvar return_reg) in
-  let stop_reset := Vnonblock (Vvar reset_reg) (Vlit (ZToValue 0)) in
-  ret (Vseq stop_reset set_result).
+Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt :=
+  let set_result := Vnonblock (Vvar fn_dst) (Vvar fn_rtrn) in
+  let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in
+  Vseq stop_reset set_result.
+
+Definition return_val fin rtrn r :=
+  let retval :=
+      match r with
+      | Some r' => Vvar r'
+      | None => Vlit (ZToValue 0%Z)
+      end in
+  Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval).
+
+Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)).
 
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
   match ni with
@@ -511,12 +513,24 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Icall sig (inr fn) args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
         do _ <- declare_reg None dst 32;
-        do finish_reg <- map_externctrl fn ctrl_finish;
         do join_state <- create_state;
-        do fork_instr <- mk_fork fn args;
-        do join_instr <- mk_join fn dst;
+
+        do finish_reg <- map_externctrl fn ctrl_finish;
+        do reset_reg <- map_externctrl fn ctrl_reset;
+        do return_reg <- map_externctrl fn ctrl_return;
+
+        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);
+
+        let fork_instr := fork reset_reg params in
+        let join_instr := join return_reg reset_reg dst in
+
         do _ <- add_instr n join_state fork_instr;
         add_instr_wait finish_reg join_state n' join_instr
+
       else error (Errors.msg "State is larger than 2^32.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
@@ -531,12 +545,8 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
       error (Errors.msg "Ijumptable: Case statement not supported.")
     | Ireturn r =>
       do idle_state <- create_state;
-      let retval := match r with
-                    | Some r' => Vvar r'
-                    | None => Vlit (ZToValue 0%Z)
-                    end in
-      do _ <- add_instr n idle_state (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval));
-      add_instr_skip idle_state (nonblock fin (Vlit (ZToValue 0%Z)))
+      do _ <- add_instr n idle_state (return_val fin rtrn r);
+      add_instr_skip idle_state (idle fin)
     end
   end.
 
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index f3c375c..51a5206 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -125,6 +125,7 @@ Ltac monadInv H :=
 statemachine that is created by the translation contains the correct
 translations for each of the elements *)
 
+(** [tr_instr] describes the translation of instructions that are directly translated into a single state *)
 Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop :=
 | tr_instr_Inop :
     forall n,
@@ -135,23 +136,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -
       Z.pos n <= Int.max_unsigned ->
       translate_instr op args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
-(* | tr_instr_Icall : *)
-(*     forall n sig fn args dst, *)
-(*       Z.pos n <= Int.max_unsigned -> *)
-(*       tr_instr fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) (HTLfork fn args) (state_goto st n) *)
 | tr_instr_Icond :
     forall n1 n2 cond args s s' i c,
       Z.pos n1 <= Int.max_unsigned ->
       Z.pos n2 <= Int.max_unsigned ->
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
-(* | tr_instr_Ireturn_None : *)
-(*     tr_instr fin rtrn st stk (RTL.Ireturn None) (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) *)
-(*                                                   (block rtrn (Vlit (ZToValue 0%Z))))) (ctrl_vstmnt Vskip) *)
-(* | tr_instr_Ireturn_Some : *)
-(*     forall r, *)
-(*       tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) *)
-(*                (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) (ctrl_vstmnt Vskip) *)
 | tr_instr_Iload :
     forall mem addr args s s' i c dst n,
       Z.pos n <= Int.max_unsigned ->
@@ -171,12 +161,34 @@ Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts : datapath) (trans : controllogic)
           (fin rtrn st stk : reg) : Prop :=
-  tr_code_intro :
+| tr_code_single :
     forall s t,
       c!pc = Some i ->
       stmnts!pc = Some s ->
       trans!pc = Some t ->
       tr_instr fin rtrn st stk i s t ->
+      tr_code c pc i stmnts trans fin rtrn st stk
+| tr_code_call :
+    forall sig fn args dst n,
+      c!pc = Some (RTL.Icall sig (inr fn) args dst n) ->
+      Z.pos n <= Int.max_unsigned ->
+
+      (exists pc2 fn_rst fn_return fn_finish fn_params,
+          stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) ->
+          trans!pc = Some (state_goto st pc2) ->
+          stmnts!pc2 = Some (join fn_return fn_rst dst) ->
+          trans!pc2 = Some (state_wait st fn_finish n)) ->
+
+      tr_code c pc i stmnts trans fin rtrn st stk
+| tr_code_return :
+    forall r,
+      c!pc = Some (RTL.Ireturn r) ->
+      (exists pc2,
+          stmnts!pc = Some (return_val fin rtrn r) ->
+          trans!pc = Some (state_goto st pc2) ->
+          stmnts!pc2 = Some (idle fin) ->
+          trans!pc2 = Some Vskip) ->
+
       tr_code c pc i stmnts trans fin rtrn st stk.
 Hint Constructors tr_code : htlspec.