From 8e012d446357cd4f7f1ef25814ea7891c45086ae Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 29 Apr 2020 18:04:27 +0100
Subject: Add documentation and conform to specification

---
 src/translation/Veriloggen.v | 65 ++++++++++++++++++++++++++++----------------
 1 file changed, 41 insertions(+), 24 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 6aa94df..aa12a67 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -359,6 +359,10 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
     | _, _, _ => Error (Errors.msg "Veriloggen.add_instr")
     end.
 
+(** Add a register to the state without changing the [st_freshreg], as this
+should already be the right value.  This can be assumed because the max register
+is taken from the RTL code. *)
+
 Definition add_reg (r: reg) (s: state) : state :=
   mkstate (st_freshreg s)
           (st_freshstate s)
@@ -398,6 +402,9 @@ Lemma decl_io_state_incr:
          (st_wf s)).
 Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed.
 
+(** Declare a new register by incrementing the [st_freshreg] by one and
+returning the old [st_freshreg]. *)
+
 Definition decl_io (sz: nat): mon (reg * nat) :=
   fun s => let r := s.(st_freshreg) in
            OK (r, sz) (mkstate
@@ -409,6 +416,9 @@ Definition decl_io (sz: nat): mon (reg * nat) :=
                      (st_wf s))
               (decl_io_state_incr s).
 
+(** Declare a new register which is given, by changing [st_decl] and without
+affecting anything else. *)
+
 Definition declare_reg (r: reg) (sz: nat): mon (reg * nat) :=
   fun s => OK (r, sz) (mkstate
                       (st_freshreg s)
@@ -419,6 +429,9 @@ Definition declare_reg (r: reg) (sz: nat): mon (reg * nat) :=
                       (st_wf s))
               (change_decl_state_incr s (PositiveMap.add r sz s.(st_decl))).
 
+(** Declare a new fresh register by first getting a valid register to increment,
+and then adding it to the declaration list. *)
+
 Definition decl_fresh_reg (sz : nat) : mon (reg * nat) :=
   do (r, s) <- decl_io sz;
   declare_reg r s.
@@ -529,11 +542,8 @@ Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr *
 Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
   Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip).
 
-Fixpoint allocate_regs (e : list (reg * nat)) {struct e} : list module_item :=
-  match e with
-  | (r, n)::es => Vdecl r n :: allocate_regs es
-  | nil => nil
-  end.
+Definition allocate_reg (e : reg * nat) : module_item :=
+  match e with (r, n) => Vdecl r n end.
 
 Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item :=
   (Valways_ff (Vposedge clk)
@@ -541,7 +551,7 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m
       (nonblock st (posToExpr 32 entry))
       (make_statetrans st s.(st_statetrans))))
   :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm)))
-  :: (allocate_regs (PositiveMap.elements s.(st_decl))).
+  :: (map allocate_reg (PositiveMap.elements s.(st_decl))).
 
 (** To start out with, the assumption is made that there is only one
     function/module in the original code. *)
@@ -549,27 +559,16 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m
 Definition set_int_size (r: reg) : reg * nat := (r, 32%nat).
 
 Definition transf_module (f: function) : mon module :=
-  do fin <- decl_io 1%nat;
-  do rtrn <- decl_io 32%nat;
+  do fin <- decl_io 1;
+  do rtrn <- decl_io 32;
   do _ <- traverselist (transf_instr (fst fin) (fst rtrn)) (Maps.PTree.elements f.(fn_code));
-  do start <- decl_io 1%nat;
-  do rst <- decl_io 1%nat;
-  do clk <- decl_io 1%nat;
-  do st <- decl_fresh_reg 32%nat;
+  do start <- decl_io 1;
+  do rst <- decl_io 1;
+  do clk <- decl_io 1;
+  do st <- decl_fresh_reg 32;
   do current_state <- get;
   let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in
-  ret (mkmodule start rst clk fin rtrn (map set_int_size f.(fn_params)) mi).
-
-Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
-{struct flist} : option function :=
-  match flist with
-  | (i, AST.Gfun (AST.Internal f)) :: xs =>
-    if Pos.eqb i main
-    then Some f
-    else main_function main xs
-  | _ :: xs => main_function main xs
-  | nil => None
-  end.
+  ret (mkmodule start rst clk fin rtrn st (map set_int_size f.(fn_params)) mi).
 
 Lemma max_state_valid_freshstate:
   forall f,
@@ -591,6 +590,24 @@ Definition max_state (f: function) : state :=
           (st_decl init_state)
           (max_state_st_wf f).
 
+Definition transl_module (f : function) : Errors.res module :=
+  run_mon (max_state f) (transf_module f).
+
+(** Retrieve the main function from the RTL, this should probably be replaced by
+retrieving a designated function instead.  This could be passed on the
+commandline and be assumed as a [Parameter] in this code. *)
+
+Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
+{struct flist} : option function :=
+  match flist with
+  | (i, AST.Gfun (AST.Internal f)) :: xs =>
+    if Pos.eqb i main
+    then Some f
+    else main_function main xs
+  | _ :: xs => main_function main xs
+  | nil => None
+  end.
+
 Definition transf_program (d : program) : Errors.res module :=
   match main_function d.(AST.prog_main) d.(AST.prog_defs) with
   | Some f => run_mon (max_state f) (transf_module f)
-- 
cgit 


From 6a204dda8e46d2d491de599c9c0dc6bceed5e971 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 3 May 2020 17:12:39 +0100
Subject: Add state transition conversion functions

---
 src/translation/Veriloggen.v | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index aa12a67..40876f7 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -38,6 +38,18 @@ Inductive statetrans : Type :=
 | StateGoto (p : node)
 | StateCond (c : expr) (t f : node).
 
+Definition state_goto (st : reg) (n : node) : stmnt :=
+  Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
+
+Definition statetrans_transl (stvar : reg) (st : statetrans) : stmnt :=
+  match st with
+  | StateGoto p => state_goto stvar p
+  | StateCond c t f => state_cond stvar c t f
+  end.
+
 Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) :=
   forall (n: node),
     Plt n fs \/ stm!n = None.
@@ -535,8 +547,8 @@ Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt :=
 
 Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt :=
   match st with
-  | (n, StateGoto n') => (posToExpr 32 n, nonblock r (posToExpr 32 n'))
-  | (n, StateCond c n1 n2) => (posToExpr 32 n, nonblock r (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)))
+  | (n, StateGoto n') => (posToExpr 32 n, state_goto r n')
+  | (n, StateCond c n1 n2) => (posToExpr 32 n, state_cond r c n1 n2)
   end.
 
 Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt :=
-- 
cgit 


From d2c3d5a4fdb35b861be9df0795ef83f9b83c7bb7 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 3 May 2020 17:12:57 +0100
Subject: Add proofs and specification of Verilog conversion

---
 src/translation/Veriloggenproof.v |  46 ++++++++++++++++
 src/translation/Veriloggenspec.v  | 112 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 158 insertions(+)
 create mode 100644 src/translation/Veriloggenproof.v
 create mode 100644 src/translation/Veriloggenspec.v

(limited to 'src/translation')

diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
new file mode 100644
index 0000000..cc884b4
--- /dev/null
+++ b/src/translation/Veriloggenproof.v
@@ -0,0 +1,46 @@
+(* -*- mode: coq -*-
+ * 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/>.
+ *)
+
+From compcert Require Import Smallstep.
+From compcert Require RTL.
+From coqup Require Verilog.
+
+Section CORRECTNESS.
+
+  Variable prog: RTL.program.
+  Variable tprog: Verilog.module.
+
+  Inductive match_states: RTL.state -> Verilog.state -> Prop :=
+  | match_state:
+      forall,
+        
+        match_states (RTL.State f s k sp e m)
+                     (Verilog.State m mi mis assoc nbassoc f cycle pc)
+  | match_returnstate:
+      forall v tv k m tm cs
+             (MS: match_stacks k cs)
+             (LD: Val.lessdef v tv)
+             (MEXT: Mem.extends m tm),
+        match_states (CminorSel.Returnstate v k m)
+                     (RTL.Returnstate cs tv tm).
+
+  Theorem transf_program_correct:
+    forward_simulation (RTL.semantics prog) (Verilog.semantics tprog).
+  Admitted.
+
+End CORRECTNESS.
diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v
new file mode 100644
index 0000000..67e2cad
--- /dev/null
+++ b/src/translation/Veriloggenspec.v
@@ -0,0 +1,112 @@
+From Coq Require Import FSets.FMapPositive.
+From compcert Require RTL Op Maps.
+From coqup Require Import Coquplib Verilog Veriloggen Value.
+
+(** * Relational specification of the translation *)
+
+(** We now define inductive predicates that characterise the fact that the
+statemachine that is created by the translation contains the correct
+translations for each of the elements *)
+
+Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
+| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r)
+| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n))
+| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r))
+| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2)
+| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2)
+| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n)
+| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2)
+| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2)
+| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2)
+| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2)
+| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2)
+| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n)
+| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2)
+| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n)
+| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2)
+| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n)
+| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r))
+| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2)
+| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n)
+| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
+| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
+| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+
+Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+| tr_instr_Inop :
+    forall n,
+      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+| tr_instr_Iop :
+    forall n op args e dst,
+      tr_op op args e ->
+      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+| tr_instr_Icond :
+    forall n1 n2 cond args s s' i c,
+      translate_condition cond args s = OK c s' i ->
+      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+| tr_instr_Ireturn_None :
+      tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip
+| tr_instr_Ireturn_Some :
+    forall r,
+      tr_instr fin rtrn st (RTL.Ireturn (Some r))
+               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+
+Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt)
+          (fin rtrn st : reg) : Prop :=
+| tr_code_intro :
+    forall i s t n,
+      Maps.PTree.get n c = Some i ->
+      stmnts!n = Some s ->
+      trans!n = Some t ->
+      tr_instr fin rtrn st i s t ->
+      tr_code c stmnts trans fin rtrn st.
+
+(** [tr_module_items start clk st rst s mis] holds if the state is correctly
+translated to actual Verilog, meaning it is correctly implemented as a state
+machine in Verilog.  Currently it does not seem that useful because it models
+the [make_module_items] nearly exactly.  Therefore it might have to be changed
+to make up for that. *)
+
+Inductive tr_module_items : node -> reg -> reg -> reg -> state -> list module_item -> Prop :=
+  tr_module_items_intro :
+    forall start clk st rst s mis,
+      Valways_ff (Vposedge clk)
+                 (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1)))
+                        (nonblock st (posToExpr 32 start))
+                        (make_statetrans st s.(st_statetrans)))
+      :: Valways_ff (Vposedge clk) (make_stm st s.(st_stm))
+      :: List.map allocate_reg (PositiveMap.elements s.(st_decl)) = mis ->
+      tr_module_items start clk st rst s mis.
+
+(** [tr_module function module] Holds if the [module] is the correct translation
+of the [function] that it was given. *)
+
+Inductive tr_module : RTL.function -> module -> Prop :=
+  tr_module_intro :
+    forall f mi st rtrn fin clk rst start s0 s1 s2 s3 s4 s5 s6 i1 i2 i3 i4 i5 i6,
+      decl_io 1 s0 = OK fin s1 i1 ->
+      decl_io 32 s1 = OK rtrn s2 i2 ->
+      decl_io 1 s2 = OK start s3 i3 ->
+      decl_io 1 s3 = OK rst s4 i4 ->
+      decl_io 1 s4 = OK clk s5 i5 ->
+      decl_fresh_reg 32 s5 = OK st s6 i6 ->
+      tr_code f.(RTL.fn_code) s6.(st_stm)
+                                   (PositiveMap.map (statetrans_transl (fst st)) s6.(st_statetrans))
+                                   (fst fin) (fst rtrn) (fst st) ->
+      tr_module_items f.(RTL.fn_entrypoint) (fst clk) (fst st) (fst rst) s6 mi ->
+      tr_module f (mkmodule
+                     start
+                     rst
+                     clk
+                     fin
+                     rtrn
+                     st
+                     (List.map set_int_size f.(RTL.fn_params))
+                     mi).
+
+Lemma tr_module_correct:
+  forall f m,
+  transl_module f = Errors.OK m ->
+  tr_module f m.
+Admitted.
-- 
cgit 


From 5cfa4af9c6e4d9703e3142c24ae78c7da0ac575f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 4 May 2020 16:13:16 +0100
Subject: Add equality check for value

---
 src/translation/Veriloggen.v      | 2 +-
 src/translation/Veriloggenproof.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 40876f7..f127b11 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v
index cc884b4..942a83a 100644
--- a/src/translation/Veriloggenproof.v
+++ b/src/translation/Veriloggenproof.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq -*-
+(*
  * CoqUp: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
-- 
cgit 


From 4bdabd1828c48e74c6b1f701f57a1b3c421a95fb Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 7 May 2020 23:13:25 +0100
Subject: Redefine HTL for intermediate Verilog language

---
 src/translation/Veriloggenspec.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'src/translation')

diff --git a/src/translation/Veriloggenspec.v b/src/translation/Veriloggenspec.v
index 67e2cad..09d08ed 100644
--- a/src/translation/Veriloggenspec.v
+++ b/src/translation/Veriloggenspec.v
@@ -1,3 +1,21 @@
+(*
+ * 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/>.
+ *)
+
 From Coq Require Import FSets.FMapPositive.
 From compcert Require RTL Op Maps.
 From coqup Require Import Coquplib Verilog Veriloggen Value.
-- 
cgit 


From 78a7b735373c0607f66d863b224cb6bb7742d1f1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 7 May 2020 23:13:54 +0100
Subject: Remove HTLgen and create the specification

---
 src/translation/HTLgen.v     | 163 -------------------------------------------
 src/translation/HTLgenspec.v |  92 ++++++++++++++++++++++++
 2 files changed, 92 insertions(+), 163 deletions(-)
 create mode 100644 src/translation/HTLgenspec.v

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index d7f88c1..8eac48c 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -17,170 +17,7 @@
  *)
 
 From coqup Require Import HTL Coquplib.
-
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST RTL.
 
-Record state: Type := mkstate {
-  st_nextinst: positive;
-  st_instances: instances;
-}.
-
-Inductive res (A: Type) (S: Type): Type :=
-  | Error: Errors.errmsg -> res A S
-  | OK: A -> S -> res A S.
-
-Arguments OK [A S].
-Arguments Error [A S].
-
-Definition mon (A: Type) : Type := res A state.
-
-Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s.
-
-Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
-    match f with
-    | Error msg => Error msg
-    | OK a s => g a
-    end.
-
-Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
-  bind f (fun xy => g (fst xy) (snd xy)).
-
-Definition bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B :=
-  match f with
-  | Error msg => Error msg
-  | OK a s => g a s
-  end.
-
-Notation "'do' X <- A ; B" := (bind A (fun X => B))
-   (at level 200, X ident, A at level 100, B at level 200).
-Notation "'do' ( X , Y ) <- A ; B" := (bindS A (fun X Y => B))
-   (at level 200, X ident, Y ident, A at level 100, B at level 200).
-
-Definition handle_error {A: Type} (f g: mon A) : mon A :=
-  match f with
-  | OK a s' => OK a s'
-  | Error _ => g
-  end.
-
-Definition init_state : state :=
-  mkstate 1%positive empty_instances.
-
-Module PTree.
-  Export Maps.PTree.
-
-  Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B)
-           (m : PTree.t A) (s : state) (i : positive)
-           {struct m} : mon (PTree.t B) :=
-    match m with
-    | Leaf => OK Leaf s
-    | Node l o r =>
-      let newo :=
-          match o with
-          | None => OK None s
-          | Some x =>
-            match f (prev i) x s with
-            | Error err => Error err
-            | OK val s' => OK (Some val) s'
-            end
-          end in
-      match newo with
-      | OK no s =>
-        do (nl, s') <- xtraverse f l s (xO i);
-        do (nr, s'') <- xtraverse f r s' (xI i);
-        OK (Node nl no nr) s''
-      | Error msg => Error msg
-      end
-    end.
-
-  Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m :=
-    xtraverse f m init_state xH.
-
-  Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f).
-
-End PTree.
-
-Definition transf_instr (pc: node) (rtl: RTL.instruction) (s: state)
-  : mon HTL.instruction :=
-  match rtl with
-  | RTL.Inop n =>
-    (** Nop instruction should just become a Skip in Verilog, which is just a
-        semicolon. *)
-    ret (HTL.Hnop n) s
-  | RTL.Iop op args res n =>
-    (** Perform an arithmetic operation over registers.  This will just become
-        one binary operation in Verilog.  This will contain a list of registers,
-        so these will just become a chain of binary operations in Verilog. *)
-    ret (HTL.Hnonblock op args res n) s
-  | RTL.Iload chunk addr args dst n =>
-    (** Load from memory, which will maybe become a load from RAM, however, I'm
-        not sure yet how memory will be implemented or how it will formalised
-        be. *)
-    ret (HTL.Hload chunk addr args dst n) s
-  | RTL.Istore chunk addr args src n =>
-    (** How memory will be laid out will also affect how stores are handled.  For
-        now hopefully these can be ignored, and hopefull they are not used that
-        often when they are not required in C. *)
-    ret (HTL.Hstore chunk addr args src n) s
-  | RTL.Icall sig ros args res n =>
-    (** Function call should become a module instantiation with start and end
-        signals appropriately wired up. *)
-    match ros with
-    | inr i =>
-      let inst := mkinst i args in
-      let newinstances := PTree.set s.(st_nextinst) inst s.(st_instances) in
-      ret (HTL.Hinst sig i res n)
-          (mkstate ((s.(st_nextinst) + 1)%positive)
-                   newinstances)
-    | _ => Error (Errors.msg "Function pointers are not supported.")
-    end
-  | RTL.Itailcall sig ros args =>
-    (** Should be converted into a reset of the modules state, setting the
-        initial variables correctly.  This would simulate a tailcall as it is
-        similar to jumping back to the top of the function in assembly. *)
-    match ros with
-    | inr i => ret (HTL.Htailcall sig i args) s
-    | _ => Error (Errors.msg "Function pointers are not supported.")
-    end
-  | RTL.Ibuiltin ef args res n =>
-    (** Builtin functions will have to supported manually, by implementing the
-        Verilog myself. *)
-    Error (Errors.msg "builtin functions are not supported.")
-  | RTL.Icond cond args n1 n2 =>
-    (** Will be converted into two separate processes that are combined by a mux
-        at the end, with a start flag that propagates in the construct that should
-        be chosen. *)
-    ret (HTL.Hcond cond args n1 n2) s
-  | RTL.Ijumptable arg tbl =>
-    (** A jump to a specific instruction in the list, this will require setting
-        the state in the state machine appropriately.  This is trivial to
-        implement if no scheduling is involved, but as soon as that isn't the
-        case it might be difficult to find that location.  It would help to
-        transform the CFG to a few basic blocks first which cannot have any
-        branching. *)
-    ret (HTL.Hjumptable arg tbl) s
-  | RTL.Ireturn r =>
-    (** The return value of the function, which will just mean that the finished
-        signal goes high and the result is stored in the result register. *)
-    ret (HTL.Hfinish r) s
-  end.
-
-Definition transf_function (f: function) : Errors.res module :=
-  match (PTree.traverse transf_instr f.(fn_code)) with
-  | OK code s =>
-    Errors.OK (mkmodule
-          f.(fn_sig)
-          f.(fn_params)
-          f.(fn_stacksize)
-          code
-          s.(st_instances)
-          f.(fn_entrypoint))
-  | Error err => Errors.Error err
-  end.
-
-Definition transf_fundef (fd: fundef) : Errors.res moddecl :=
-  transf_partial_fundef transf_function fd.
-
-Definition transf_program (p: program) : Errors.res design :=
-  transform_partial_program transf_fundef p.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
new file mode 100644
index 0000000..fb1c70d
--- /dev/null
+++ b/src/translation/HTLgenspec.v
@@ -0,0 +1,92 @@
+(*
+ * 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/>.
+ *)
+
+From Coq Require Import FSets.FMapPositive.
+From compcert Require RTL Op Maps.
+From coqup Require Import Coquplib Verilog Veriloggen Value HTL.
+
+(** * Relational specification of the translation *)
+
+(** We now define inductive predicates that characterise the fact that the
+statemachine that is created by the translation contains the correct
+translations for each of the elements *)
+
+Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
+| tr_op_Omove : forall r, tr_op Op.Omove (r::nil) (Vvar r)
+| tr_op_Ointconst : forall n l, tr_op (Op.Ointconst n) l (Vlit (intToValue n))
+| tr_op_Oneg : forall r, tr_op Op.Oneg (r::nil) (Vunop Vneg (Vvar r))
+| tr_op_Osub : forall r1 r2, tr_op Op.Osub (r1::r2::nil) (bop Vsub r1 r2)
+| tr_op_Omul : forall r1 r2, tr_op Op.Omul (r1::r2::nil) (bop Vmul r1 r2)
+| tr_op_Omulimm : forall r n, tr_op (Op.Omulimm n) (r::nil) (boplit Vmul r n)
+| tr_op_Odiv : forall r1 r2, tr_op Op.Odiv (r1::r2::nil) (bop Vdiv r1 r2)
+| tr_op_Odivu : forall r1 r2, tr_op Op.Odivu (r1::r2::nil) (bop Vdivu r1 r2)
+| tr_op_Omod : forall r1 r2, tr_op Op.Omod (r1::r2::nil) (bop Vmod r1 r2)
+| tr_op_Omodu : forall r1 r2, tr_op Op.Omodu (r1::r2::nil) (bop Vmodu r1 r2)
+| tr_op_Oand : forall r1 r2, tr_op Op.Oand (r1::r2::nil) (bop Vand r1 r2)
+| tr_op_Oandimm : forall n r, tr_op (Op.Oandimm n) (r::nil) (boplit Vand r n)
+| tr_op_Oor : forall r1 r2, tr_op Op.Oor (r1::r2::nil) (bop Vor r1 r2)
+| tr_op_Oorimm : forall n r, tr_op (Op.Oorimm n) (r::nil) (boplit Vor r n)
+| tr_op_Oxor : forall r1 r2, tr_op Op.Oxor (r1::r2::nil) (bop Vxor r1 r2)
+| tr_op_Oxorimm : forall n r, tr_op (Op.Oxorimm n) (r::nil) (boplit Vxor r n)
+| tr_op_Onot : forall r, tr_op Op.Onot (r::nil) (Vunop Vnot (Vvar r))
+| tr_op_Oshl : forall r1 r2, tr_op Op.Oshl (r1::r2::nil) (bop Vshl r1 r2)
+| tr_op_Oshlimm : forall n r, tr_op (Op.Oshlimm n) (r::nil) (boplit Vshl r n)
+| tr_op_Oshr : forall r1 r2, tr_op Op.Oshr (r1::r2::nil) (bop Vshr r1 r2)
+| tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
+| tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
+| tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+
+Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
+| tr_instr_Inop :
+    forall n,
+      tr_instr fin rtrn st (RTL.Inop n) Vskip (state_goto st n)
+| tr_instr_Iop :
+    forall n op args e dst,
+      tr_op op args e ->
+      tr_instr fin rtrn st (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
+| tr_instr_Icond :
+    forall n1 n2 cond args s s' i c,
+      translate_condition cond args s = OK c s' i ->
+      tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+| tr_instr_Ireturn_None :
+      tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip
+| tr_instr_Ireturn_Some :
+    forall r,
+      tr_instr fin rtrn st (RTL.Ireturn (Some r))
+               (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+
+Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt)
+          (fin rtrn st : reg) : Prop :=
+  tr_code_intro :
+    forall i s t n,
+      Maps.PTree.get n c = Some i ->
+      stmnts!n = Some s ->
+      trans!n = Some t ->
+      tr_instr fin rtrn st i s t ->
+      tr_code c stmnts trans fin rtrn st.
+
+Inductive tr_module (f : RTL.function) : module -> Prop :=
+  tr_module_intro :
+    forall c data control fin rtrn st,
+      tr_code c data control fin rtrn st ->
+      tr_module f (mkmodule
+                     f.(RTL.fn_params)
+                     data
+                     control
+                     f.(RTL.fn_entrypoint)
+                     st fin rtrn).
-- 
cgit 


From 32f0f542c18b73303613b53573e6c61bc7ae6890 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 7 May 2020 23:14:48 +0100
Subject: Add match_states Inductive

---
 src/translation/HTLgenproof.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 src/translation/HTLgenproof.v

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
new file mode 100644
index 0000000..898fafd
--- /dev/null
+++ b/src/translation/HTLgenproof.v
@@ -0,0 +1,29 @@
+(*
+ * 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/>.
+ *)
+
+From coqup Require Import HTLgenspec.
+From coqup Require HTL Verilog.
+From compcert Require RTL.
+
+Parameter match_assocset : RTL.regset -> Verilog.assocset -> Prop.
+
+Inductive match_states : RTL.state -> HTL.state -> Prop :=
+| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st,
+    match_assocset rs assoc ->
+    match_states (RTL.State sf f sp st rs mem)
+                 (HTL.State m st assoc).
-- 
cgit 


From ebcba2714fdba588fb31c5a5307a8f21b39e0ac5 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 8 May 2020 23:35:06 +0100
Subject: Add simulation diagram

---
 src/translation/HTLgenproof.v | 58 +++++++++++++++++++++++++++++++++++++++----
 1 file changed, 53 insertions(+), 5 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 898fafd..7a4ec34 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -16,14 +16,62 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import HTLgenspec.
+From coqup Require Import HTLgenspec Value AssocMap.
 From coqup Require HTL Verilog.
-From compcert Require RTL.
+From compcert Require RTL Registers Globalenvs AST.
 
-Parameter match_assocset : RTL.regset -> Verilog.assocset -> Prop.
+Import AssocMapNotation.
+
+Inductive match_assocmaps : RTL.regset -> assocmap -> Prop :=
+| match_assocmap : forall r rs am,
+    val_value_lessdef (Registers.Regmap.get r rs) am#r ->
+    match_assocmaps rs am.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st,
-    match_assocset rs assoc ->
+    match_assocmaps rs assoc ->
+    tr_module f m ->
     match_states (RTL.State sf f sp st rs mem)
-                 (HTL.State m st assoc).
+                 (HTL.State m st assoc)
+| match_returnstate : forall v v' stack m,
+    val_value_lessdef v v' ->
+    match_states (RTL.Returnstate stack v m) (HTL.Returnstate v').
+
+Inductive match_program : RTL.program -> HTL.module -> Prop :=
+  match_program_intro :
+    forall ge p b m f,
+    ge = Globalenvs.Genv.globalenv p ->
+    Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b ->
+    Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) ->
+    tr_module f m ->
+    match_program p m.
+
+Section CORRECTNESS.
+
+  Variable prog : RTL.program.
+  Variable tprog : HTL.module.
+
+  Hypothesis TRANSL : match_program prog tprog.
+
+  Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
+  Let tge : HTL.genv := HTL.genv_empty.
+
+  (** The proof of semantic preservation for the translation of instructions
+      is a simulation argument based on diagrams of the following form:
+<<
+                    I /\ P
+    code st rs ---------------- State m st assoc
+         ||                             |
+         ||                             |
+         ||                             |
+         \/                             v
+    code st rs' --------------- State m st assoc'
+                    I /\ Q
+>>
+      where [tr_code c data control fin rtrn st] is assumed to hold.
+   *)
+
+  Definition transl_code_prop : Prop :=
+    HTL.step tge (HTL.State)
+
+End CORRECTNESS.
-- 
cgit 


From 60ab47c6ff0db1b690afe6fd2c2b63cf5843ced1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 20 May 2020 10:51:49 +0100
Subject: Add proof of translation correctness

Modified-by: Yann Herklotz <git@yannherklotz.com>
---
 src/translation/HTLgenproof.v | 201 ++++++++++++++++++++++++++++++++++++++++--
 src/translation/HTLgenspec.v  |  16 ++--
 2 files changed, 200 insertions(+), 17 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 7a4ec34..ff7c24d 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -23,14 +23,22 @@ From compcert Require RTL Registers Globalenvs AST.
 Import AssocMapNotation.
 
 Inductive match_assocmaps : RTL.regset -> assocmap -> Prop :=
-| match_assocmap : forall r rs am,
-    val_value_lessdef (Registers.Regmap.get r rs) am#r ->
+| match_assocmap : forall rs am,
+    (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
     match_assocmaps rs am.
 
+Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
+  forall st assoc,
+  s = HTL.State m st assoc ->
+  assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
+
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st,
-    match_assocmaps rs assoc ->
-    tr_module f m ->
+| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
+    (MASSOC : match_assocmaps rs assoc)
+    (TF : tr_module f m)
+    (TC : tr_code f.(RTL.fn_code) st m.(HTL.mod_datapath) m.(HTL.mod_controllogic)
+                  m.(HTL.mod_finish) m.(HTL.mod_return) m.(HTL.mod_st))
+    (WF : state_st_wf m (HTL.State m st assoc)),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State m st assoc)
 | match_returnstate : forall v v' stack m,
@@ -46,6 +54,80 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
     tr_module f m ->
     match_program p m.
 
+Lemma regs_lessdef_regs :
+  forall rs1 rs2 n v,
+    match_assocmaps rs1 rs2 ->
+    match_assocmaps rs1 (AssocMap.add n v rs2).
+Admitted.
+
+Lemma regs_add_match :
+  forall rs am r v v',
+    match_assocmaps rs am ->
+    val_value_lessdef v v' ->
+    match_assocmaps (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
+Admitted.
+
+Lemma merge_inj :
+  forall am am' r v,
+    merge_assocmap (AssocMap.add r v am) am' = AssocMap.add r v (merge_assocmap am am').
+Admitted.
+
+Lemma valToValue_lessdef :
+  forall v,
+    val_value_lessdef v (valToValue v).
+Admitted.
+
+Lemma assocmap_merge_add :
+  forall k v assoc,
+    AssocMap.add k v assoc = merge_assocmap (AssocMap.add k v empty_assocmap) assoc.
+Admitted.
+
+(* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
+Lemma assumption_32bit :
+  forall v,
+    valueToPos (posToValue 32 v) = v.
+Admitted.
+
+Lemma regset_assocmap_get :
+  forall r rs am v v',
+    match_assocmaps rs am ->
+    v = Registers.Regmap.get r rs ->
+    v' = am#r ->
+    val_value_lessdef v v'.
+Proof. inversion 1. intros. subst. apply H0. Qed.
+
+Lemma regset_assocmap_wf :
+  forall r rs am i,
+    match_assocmaps rs am ->
+    Values.Vint i <> Registers.Regmap.get r rs ->
+    am!r = None.
+Admitted.
+
+Lemma regset_assocmap_wf2 :
+  forall r rs am i,
+    match_assocmaps rs am ->
+    Values.Vint i = Registers.Regmap.get r rs ->
+    am!r = Some (intToValue i).
+Admitted.
+
+Lemma access_merge_assocmap :
+  forall nb r v am,
+  nb!r = Some v ->
+  (merge_assocmap nb am) ! r = Some v.
+Admitted.
+
+Lemma st_greater_than_res :
+  forall m res,
+    (HTL.mod_st m) <> res.
+Admitted.
+
+Ltac subst_eq_hyp :=
+  match goal with
+    H1: ?x = Some ?i, H2: ?x = Some ?j |- _ =>
+    let H := fresh "H" in
+    rewrite H1 in H2; injection H2; intro H; clear H2; subst
+  end.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -56,22 +138,123 @@ Section CORRECTNESS.
   Let ge : RTL.genv := Globalenvs.Genv.globalenv prog.
   Let tge : HTL.genv := HTL.genv_empty.
 
+  Lemma eval_correct :
+    forall sp op rs args m v e assoc f,
+      Op.eval_operation ge sp op
+(List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
+      tr_op op args e ->
+      Verilog.expr_runp f assoc e (valToValue v).
+  Admitted.
+
   (** The proof of semantic preservation for the translation of instructions
       is a simulation argument based on diagrams of the following form:
 <<
-                    I /\ P
+                      match_states
     code st rs ---------------- State m st assoc
          ||                             |
          ||                             |
          ||                             |
          \/                             v
     code st rs' --------------- State m st assoc'
-                    I /\ Q
+                      I
 >>
       where [tr_code c data control fin rtrn st] is assumed to hold.
+
+      The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
    *)
 
-  Definition transl_code_prop : Prop :=
-    HTL.step tge (HTL.State)
+  Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
+    forall m assoc fin rtrn st stmt trans,
+      tr_instr fin rtrn st instr stmt trans ->
+      exists assoc',
+        HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc').
+
+  Theorem transl_step_correct:
+    forall (S1 : RTL.state) t S2,
+      RTL.step ge S1 t S2 ->
+      forall (R1 : HTL.state),
+        match_states S1 R1 ->
+        exists R2, HTL.step tge R1 t R2 /\ match_states S2 R2.
+  Proof.
+    induction 1; intros R1 MSTATE.
+    - (* Inop *)
+      inversion MSTATE. subst.
+      econstructor.
+      split.
+
+      inversion TC.
+      eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H3; subst.
+      apply H2.
+      apply H1.
+      (* processing of state *)
+      econstructor.
+      simpl. trivial.
+      econstructor. trivial.
+      inversion H3. subst.
+      econstructor.
+
+      (* prove merge *)
+      apply assocmap_merge_add.
+
+      (* prove stval *)
+      apply AssocMap.gss.
+      apply assumption_32bit.
+
+      (* prove match_state *)
+      constructor.
+      apply rs.
+      apply regs_lessdef_regs.
+      assumption.
+      inversion TF. simpl. apply H0.
+      assumption.
+      unfold state_st_wf. intros. inversion H0. subst.
+      apply AssocMap.gss.
+    - (* Iop *)
+      inversion MSTATE. subst.
+      econstructor.
+      split.
+
+      inversion TC.
+      eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H4; subst.
+      apply H3.
+      apply H2.
+      econstructor.
+      simpl. trivial.
+      constructor. trivial.
+      econstructor.
+      simpl. trivial.
+      eapply eval_correct. apply H0. apply H10. trivial. trivial.
+      apply access_merge_assocmap. rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+      trivial.
+
+      (* match_states *)
+      assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit.
+      rewrite <- H1.
+      constructor. apply rs0.
+      rewrite merge_inj.
+      apply regs_add_match.
+      rewrite merge_inj.
+      unfold merge_assocmap. rewrite AssocMapExt.merge_base.
+      apply regs_lessdef_regs.
+      assumption.
+      apply valToValue_lessdef.
+
+      inversion TF. simpl. apply H2.
+      assumption.
+
+      unfold state_st_wf. intros. inversion H2. subst.
+      rewrite merge_inj.
+      rewrite AssocMap.gso.
+      rewrite merge_inj.
+      apply AssocMap.gss.
+      apply st_greater_than_res.
+    - inversion MSTATE. inversion TC. subst.
+      econstructor. constructor.
+      inversion H12; subst_eq_hyp; discriminate.
+      apply match_state. apply rs0.
+      apply regs_add_match. apply MASSOC. apply valToValue_lessdef.
+      inversion TF. rewrite H3.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index fb1c70d..e2d788c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -70,20 +70,20 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
 
-Inductive tr_code (c : RTL.code) (stmnts trans : PositiveMap.t stmnt)
+Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts trans : PositiveMap.t stmnt)
           (fin rtrn st : reg) : Prop :=
   tr_code_intro :
-    forall i s t n,
-      Maps.PTree.get n c = Some i ->
-      stmnts!n = Some s ->
-      trans!n = Some t ->
+    forall i s t,
+      Maps.PTree.get pc c = Some i ->
+      stmnts!pc = Some s ->
+      trans!pc = Some t ->
       tr_instr fin rtrn st i s t ->
-      tr_code c stmnts trans fin rtrn st.
+      tr_code c pc stmnts trans fin rtrn st.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall c data control fin rtrn st,
-      tr_code c data control fin rtrn st ->
+    forall data control fin rtrn st,
+      (forall pc, tr_code f.(RTL.fn_code) pc data control fin rtrn st) ->
       tr_module f (mkmodule
                      f.(RTL.fn_params)
                      data
-- 
cgit 


From 39a4348657c2f3efb3feafe9cf65b0f2a1a263c2 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 21 May 2020 23:10:45 +0100
Subject: Finish the proof with most assumptions

---
 src/translation/HTLgenproof.v | 177 +++++++++++++++++++++++++++++++++++-------
 src/translation/HTLgenspec.v  |   2 +-
 2 files changed, 150 insertions(+), 29 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index ff7c24d..cb621a8 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -88,6 +88,11 @@ Lemma assumption_32bit :
     valueToPos (posToValue 32 v) = v.
 Admitted.
 
+Lemma assumption_32bit_bool :
+  forall b,
+    valueToBool (boolToValue 32 b) = b.
+Admitted.
+
 Lemma regset_assocmap_get :
   forall r rs am v v',
     match_assocmaps rs am ->
@@ -110,15 +115,19 @@ Lemma regset_assocmap_wf2 :
     am!r = Some (intToValue i).
 Admitted.
 
-Lemma access_merge_assocmap :
-  forall nb r v am,
-  nb!r = Some v ->
-  (merge_assocmap nb am) ! r = Some v.
-Admitted.
-
 Lemma st_greater_than_res :
   forall m res,
-    (HTL.mod_st m) <> res.
+    HTL.mod_st m <> res.
+Admitted.
+
+Lemma finish_not_return :
+  forall m,
+    HTL.mod_finish m <> HTL.mod_return m.
+Admitted.
+
+Lemma finish_not_res :
+  forall m r,
+    HTL.mod_finish m <> r.
 Admitted.
 
 Ltac subst_eq_hyp :=
@@ -128,6 +137,9 @@ Ltac subst_eq_hyp :=
     rewrite H1 in H2; injection H2; intro H; clear H2; subst
   end.
 
+Ltac unfold_merge :=
+  try (repeat (rewrite merge_inj)); unfold merge_assocmap; rewrite AssocMapExt.merge_base.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -146,6 +158,13 @@ Section CORRECTNESS.
       Verilog.expr_runp f assoc e (valToValue v).
   Admitted.
 
+  Lemma eval_cond_correct :
+    forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc,
+    Veriloggen.translate_condition cond args s1 = Veriloggen.OK c s' i ->
+    Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b ->
+    Verilog.expr_runp f assoc c (boolToValue 32 b).
+  Admitted.
+
   (** The proof of semantic preservation for the translation of instructions
       is a simulation argument based on diagrams of the following form:
 <<
@@ -156,7 +175,7 @@ Section CORRECTNESS.
          ||                             |
          \/                             v
     code st rs' --------------- State m st assoc'
-                      I
+                      match_states
 >>
       where [tr_code c data control fin rtrn st] is assumed to hold.
 
@@ -174,16 +193,17 @@ Section CORRECTNESS.
       RTL.step ge S1 t S2 ->
       forall (R1 : HTL.state),
         match_states S1 R1 ->
-        exists R2, HTL.step tge R1 t R2 /\ match_states S2 R2.
+        exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    induction 1; intros R1 MSTATE.
+    induction 1; intros R1 MSTATE;
+      try (inversion MSTATE; inversion TC; inversion H12; subst_eq_hyp; discriminate).
     - (* Inop *)
       inversion MSTATE. subst.
       econstructor.
       split.
-
+      apply Smallstep.plus_one.
       inversion TC.
-      eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H3; subst.
+      eapply HTL.step_module; subst_eq_hyp; inversion H3; subst.
       apply H2.
       apply H1.
       (* processing of state *)
@@ -205,17 +225,17 @@ Section CORRECTNESS.
       apply rs.
       apply regs_lessdef_regs.
       assumption.
-      inversion TF. simpl. apply H0.
       assumption.
+      inversion TF. simpl. apply H0.
       unfold state_st_wf. intros. inversion H0. subst.
       apply AssocMap.gss.
     - (* Iop *)
       inversion MSTATE. subst.
       econstructor.
       split.
-
+      apply Smallstep.plus_one.
       inversion TC.
-      eapply HTL.step_module; subst_eq_hyp; remember (HTL.mod_st m0) as st; inversion H4; subst.
+      eapply HTL.step_module; subst_eq_hyp; inversion H4; subst.
       apply H3.
       apply H2.
       econstructor.
@@ -224,7 +244,8 @@ Section CORRECTNESS.
       econstructor.
       simpl. trivial.
       eapply eval_correct. apply H0. apply H10. trivial. trivial.
-      apply access_merge_assocmap. rewrite AssocMap.gso.
+      unfold_merge.
+      rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
       trivial.
@@ -233,28 +254,128 @@ Section CORRECTNESS.
       assert (pc' = valueToPos (posToValue 32 pc')). symmetry. apply assumption_32bit.
       rewrite <- H1.
       constructor. apply rs0.
-      rewrite merge_inj.
+      unfold_merge.
       apply regs_add_match.
-      rewrite merge_inj.
-      unfold merge_assocmap. rewrite AssocMapExt.merge_base.
       apply regs_lessdef_regs.
       assumption.
       apply valToValue_lessdef.
-
-      inversion TF. simpl. apply H2.
       assumption.
+      inversion TF. simpl. apply H2.
 
       unfold state_st_wf. intros. inversion H2. subst.
-      rewrite merge_inj.
+      unfold_merge.
       rewrite AssocMap.gso.
-      rewrite merge_inj.
       apply AssocMap.gss.
       apply st_greater_than_res.
-    - inversion MSTATE. inversion TC. subst.
-      econstructor. constructor.
-      inversion H12; subst_eq_hyp; discriminate.
+    - inversion MSTATE; inversion TC;
+        inversion H12; subst_eq_hyp; inversion H13.
+    - inversion MSTATE. inversion TC. subst_eq_hyp. inversion H12. subst.
+      econstructor. split. apply Smallstep.plus_one.
+      eapply HTL.step_module. subst. apply H11. apply H10.
+      eapply Verilog.stmnt_runp_Vnonblock with
+          (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
+      simpl. trivial.
+      destruct b.
+      eapply Verilog.erun_Vternary_true.
+      eapply eval_cond_correct. apply args.
+      apply H7. apply H0.
+      constructor.
+      apply assumption_32bit_bool.
+      eapply Verilog.erun_Vternary_false.
+      eapply eval_cond_correct. apply args.
+      apply H7. apply H0.
+      constructor.
+      apply assumption_32bit_bool.
+      trivial.
+      constructor.
+      trivial.
+      unfold_merge.
+      apply AssocMap.gss.
+      trivial.
+
+      destruct b.
+      rewrite assumption_32bit.
+      apply match_state. apply rs0.
+      unfold_merge.
+      apply regs_lessdef_regs. assumption.
+      assumption.
+
+      inversion TF. simpl. apply H1.
+
+      unfold state_st_wf. intros. inversion H1.
+      subst. unfold_merge.
+      apply AssocMap.gss.
+      rewrite assumption_32bit.
       apply match_state. apply rs0.
-      apply regs_add_match. apply MASSOC. apply valToValue_lessdef.
-      inversion TF. rewrite H3.
+      unfold_merge.
+      apply regs_lessdef_regs. assumption.
+      assumption.
+
+      inversion TF. simpl. apply H1.
+
+      unfold state_st_wf. intros. inversion H1.
+      subst. unfold_merge.
+      apply AssocMap.gss.
+
+    - (* Return *)
+      inversion MSTATE. inversion TC. subst_eq_hyp.
+      inversion H11. subst.
+      econstructor. split.
+      eapply Smallstep.plus_two.
+      
+      eapply HTL.step_module.
+      apply H10.
+      apply H9.
+      constructor.
+      econstructor; simpl; trivial.
+      econstructor; simpl; trivial.
+      constructor.
+      econstructor; simpl; trivial.
+      constructor.
+      unfold_merge.
+      trivial.
+      rewrite AssocMap.gso.
+      rewrite AssocMap.gso.
+      unfold state_st_wf in WF. apply WF. trivial.
+      apply st_greater_than_res. apply st_greater_than_res. trivial.
+
+      apply HTL.step_finish.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply finish_not_return.
+      apply AssocMap.gss.
+      rewrite Events.E0_left. trivial.
+
+      constructor. constructor.
+      destruct (assoc!r) eqn:?.
+      inversion H11. subst.
+      econstructor. split.
+      eapply Smallstep.plus_two.
+      eapply HTL.step_module.
+      apply H10.
+      apply H9.
+      constructor.
+      econstructor; simpl; trivial.
+      econstructor; simpl; trivial.
+      constructor.
+      econstructor; simpl; trivial.
+      apply Verilog.erun_Vvar.
+      rewrite AssocMap.gso.
+      apply Heqo. apply not_eq_sym. apply finish_not_res.
+      unfold_merge.
+      trivial.
+      rewrite AssocMap.gso.
+      rewrite AssocMap.gso.
+      unfold state_st_wf in WF. apply WF. trivial.
+      apply st_greater_than_res. apply st_greater_than_res. trivial.
+
+      apply HTL.step_finish.
+      rewrite AssocMap.gso.
+      apply AssocMap.gss.
+      apply finish_not_return.
+      apply AssocMap.gss.
+      rewrite Events.E0_left. trivial.
+
+      constructor. simpl. Search Registers.Regmap.get.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index e2d788c..a7d65fc 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -64,7 +64,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-      tr_instr fin rtrn st (RTL.Ireturn None) (block fin (Vlit (ZToValue 1%nat 1%Z))) Vskip
+      tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
-- 
cgit 


From bb8a935f9143e65102a3a498a96dd13a3b8a4801 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 24 May 2020 13:36:53 +0100
Subject: Add HTLgen

---
 src/translation/HTLgen.v | 338 ++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 337 insertions(+), 1 deletion(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 8eac48c..7bb5030 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -16,8 +16,344 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import HTL Coquplib.
 From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST RTL.
+From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad.
 
+Hint Resolve AssocMap.gempty : htlh.
+Hint Resolve AssocMap.gso : htlh.
+Hint Resolve AssocMap.gss : htlh.
+Hint Resolve Ple_refl : htlh.
+Hint Resolve Ple_succ : htlh.
+
+Record state: Type := mkstate {
+  st_st : reg;
+  st_freshreg: reg;
+  st_freshstate: node;
+  st_datapath: datapath;
+  st_controllogic: controllogic;
+}.
+
+Definition init_state (st : reg) : state :=
+  mkstate st
+          1%positive
+          1%positive
+          (AssocMap.empty stmnt)
+          (AssocMap.empty stmnt).
+
+Module HTLState <: State.
+
+  Definition st := state.
+
+  Inductive st_incr: state -> state -> Prop :=
+    state_incr_intro:
+      forall (s1 s2: state),
+        st_st s1 = st_st s2 ->
+        Ple s1.(st_freshreg) s2.(st_freshreg) ->
+        Ple s1.(st_freshstate) s2.(st_freshstate) ->
+        (forall n,
+            s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) ->
+        (forall n,
+            s1.(st_controllogic)!n = None
+            \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) ->
+        st_incr s1 s2.
+  Hint Constructors st_incr : htlh.
+
+  Definition st_prop := st_incr.
+  Hint Unfold st_prop : htlh.
+
+  Lemma st_refl : forall s, st_prop s s.
+  Proof. auto with htlh. Qed.
+
+  Lemma st_trans :
+    forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
+  Proof.
+    intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans.
+    - rewrite H1. rewrite H. reflexivity.
+    - intros. destruct H4 with n.
+      + left; assumption.
+      + destruct H8 with n;
+          [ rewrite <- H0; left; assumption
+          | right; rewrite <- H0; apply H10
+          ].
+    - intros. destruct H5 with n.
+      + left; assumption.
+      + destruct H9 with n.
+        * rewrite <- H0. left. assumption.
+        * right. rewrite <- H0. apply H10.
+  Qed.
+
+End HTLState.
+Import HTLState.
+
+Module HTLMonad := Statemonad(HTLState).
+Import HTLMonad.
+
+Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
+Import HTLMonadExtra.
+Import MonadNotation.
+
+Definition state_goto (st : reg) (n : node) : stmnt :=
+  Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
+
+Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=
+  Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)).
+
+Definition check_empty_node_datapath:
+  forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_datapath)!n); intros. right; auto. left; auto.
+Defined.
+
+Definition check_empty_node_controllogic:
+  forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.
+Proof.
+  intros. case (s.(st_controllogic)!n); intros. right; auto. left; auto.
+Defined.
+
+Lemma add_instr_state_incr :
+  forall s n n' st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       (AssocMap.add n st s.(st_datapath))
+       (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               (AssocMap.add n st s.(st_datapath))
+               (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic)))
+         (add_instr_state_incr s n n' st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
+Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
+Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
+
+Definition bop (op : binop) (r1 r2 : reg) : expr :=
+  Vbinop op (Vvar r1) (Vvar r2).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=
+  Vbinop op (Vvar r) (Vlit (intToValue l)).
+
+Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=
+  Vbinop op (Vvar r) (Vlit (ZToValue 32%nat l)).
+
+Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=
+  match c, args with
+  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
+  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
+  | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)
+  | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)
+  | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)
+  | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)
+  | _, _ => error (Errors.msg "Veriloggen: comparison instruction not implemented: other")
+  end.
+
+Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)
+  : mon expr :=
+  match c, args with
+  | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
+  | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
+  | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)
+  | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)
+  | Integers.Cle, r1::nil => ret (boplit Vle r1 i)
+  | Integers.Cge, r1::nil => ret (boplit Vge r1 i)
+  | _, _ => error (Errors.msg "Veriloggen: comparison_imm instruction not implemented: other")
+  end.
+
+Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=
+  match c, args with
+  | Op.Ccomp c, _ => translate_comparison c args
+  | Op.Ccompu c, _ => translate_comparison c args
+  | Op.Ccompimm c i, _ => translate_comparison_imm c args i
+  | Op.Ccompuimm c i, _ => translate_comparison_imm c args i
+  | Op.Cmaskzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmaskzero")
+  | Op.Cmasknotzero n, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: Cmasknotzero")
+  | _, _ => error (Errors.msg "Veriloggen: condition instruction not implemented: other")
+  end.
+
+Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
+  match a, args with
+  | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off)
+  | Op.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off))
+  | Op.Ascaled scale offset, r1::nil =>
+    ret (Vbinop Vadd (boplitz Vadd r1 scale) (Vlit (ZToValue 32%nat offset)))
+  | Op.Aindexed2scaled scale offset, r1::r2::nil =>
+    ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
+  | _, _ => error (Errors.msg "Veriloggen: eff_addressing instruction not implemented: other")
+  end.
+
+(** Translate an instruction to a statement. *)
+Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
+  match op, args with
+  | Op.Omove, r::nil => ret (Vvar r)
+  | Op.Ointconst n, _ => ret (Vlit (intToValue n))
+  | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
+  | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
+  | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
+  | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
+  | Op.Omulhs, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhs")
+  | Op.Omulhu, _ => error (Errors.msg "Veriloggen: Instruction not implemented: Omulhu")
+  | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
+  | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)
+  | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)
+  | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)
+  | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)
+  | Op.Oandimm n, r::nil => ret (boplit Vand r n)
+  | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)
+  | Op.Oorimm n, r::nil => ret (boplit Vor r n)
+  | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
+  | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
+  | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
+  | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
+  | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
+  | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
+  | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)
+  | Op.Oshrximm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshrximm")
+  | Op.Oshru, r1::r2::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshru")
+  | Op.Oshruimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshruimm")
+  | Op.Ororimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Ororimm")
+  | Op.Oshldimm n, r::nil => error (Errors.msg "Veriloggen: Instruction not implemented: Oshldimm")
+  | Op.Ocmp c, _ => translate_condition c args
+  | Op.Olea a, _ => translate_eff_addressing a args
+  | _, _ => error (Errors.msg "Veriloggen: Instruction not implemented: other")
+  end.
+
+Lemma add_branch_instr_state_incr:
+  forall s e n n1 n2,
+    (st_datapath s) ! n = None ->
+    (st_controllogic s) ! n = None ->
+    st_incr s (mkstate
+                 s.(st_st)
+                (st_freshreg s)
+                (st_freshstate s)
+                (AssocMap.add n Vskip (st_datapath s))
+                (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+Proof.
+  intros. apply state_incr_intro; simpl;
+            try (intros; destruct (peq n0 n); subst);
+            auto with htlh.
+Qed.
+
+Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left NSTM, left NTRANS =>
+      OK tt (mkstate
+               s.(st_st)
+                (st_freshreg s)
+                (st_freshstate s)
+                (AssocMap.add n Vskip (st_datapath s))
+                (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+         (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
+    | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
+    end.
+
+Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
+  match ni with
+    (n, i) =>
+    match i with
+    | Inop n' => add_instr n n' Vskip
+    | Iop op args dst n' =>
+      do instr <- translate_instr op args;
+      add_instr n n' (block dst instr)
+    | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.")
+    | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.")
+    | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
+    | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
+    | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
+    | Icond cond args n1 n2 =>
+      do e <- translate_condition cond args;
+      add_branch_instr e n n1 n2
+    | Ijumptable _ _ => error (Errors.msg "Jumptable not implemented")
+    | Ireturn r =>
+      match r with
+      | Some r' =>
+        add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
+      | None =>
+        add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z)))
+      end
+    end
+  end.
+
+Lemma create_reg_state_incr:
+  forall s,
+    st_incr s (mkstate
+         s.(st_st)
+         (Pos.succ (st_freshreg s))
+         (st_freshstate s)
+         (st_datapath s)
+         (st_controllogic s)).
+Proof. constructor; simpl; auto with htlh. Qed.
+
+Definition create_reg: mon reg :=
+  fun s => let r := s.(st_freshreg) in
+           OK r (mkstate
+                   s.(st_st)
+                   (Pos.succ r)
+                   (st_freshstate s)
+                   (st_datapath s)
+                   (st_controllogic s))
+              (create_reg_state_incr s).
+
+Definition transf_module (f: function) : mon module :=
+  do fin <- create_reg;
+  do rtrn <- create_reg;
+  do _ <- traverselist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code));
+  do start <- create_reg;
+  do rst <- create_reg;
+  do clk <- create_reg;
+  do current_state <- get;
+  ret (mkmodule
+         f.(RTL.fn_params)
+         current_state.(st_datapath)
+         current_state.(st_controllogic)
+         f.(fn_entrypoint)
+         current_state.(st_st)
+         fin
+         rtrn).
+
+Definition max_state (f: function) : state :=
+  let st := Pos.succ (max_reg_function f) in
+  mkstate st
+          (Pos.succ st)
+          (Pos.succ (max_pc_function f))
+          (st_datapath (init_state st))
+          (st_controllogic (init_state st)).
+
+Definition transl_module (f : function) : Errors.res module :=
+  run_mon (max_state f) (transf_module f).
+
+Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit))
+{struct flist} : option function :=
+  match flist with
+  | (i, AST.Gfun (AST.Internal f)) :: xs =>
+    if Pos.eqb i main
+    then Some f
+    else main_function main xs
+  | _ :: xs => main_function main xs
+  | nil => None
+  end.
+
+Definition transf_program (d : program) : Errors.res module :=
+  match main_function d.(AST.prog_main) d.(AST.prog_defs) with
+  | Some f => run_mon (max_state f) (transf_module f)
+  | _ => Errors.Error (Errors.msg "HTL: could not find main function")
+  end.
-- 
cgit 


From 9f631b114e1cdcbaf3610eefd6f9fd7baeeda0c1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 25 May 2020 22:17:11 +0100
Subject: Continuing work on proving specification

---
 src/translation/HTLgen.v     |  13 ++-
 src/translation/HTLgenspec.v | 227 ++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 218 insertions(+), 22 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 7bb5030..714cf98 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -63,8 +63,7 @@ Module HTLState <: State.
   Definition st_prop := st_incr.
   Hint Unfold st_prop : htlh.
 
-  Lemma st_refl : forall s, st_prop s s.
-  Proof. auto with htlh. Qed.
+  Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.
 
   Lemma st_trans :
     forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.
@@ -85,14 +84,14 @@ Module HTLState <: State.
   Qed.
 
 End HTLState.
-Import HTLState.
+Export HTLState.
 
 Module HTLMonad := Statemonad(HTLState).
-Import HTLMonad.
+Export HTLMonad.
 
 Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).
 Import HTLMonadExtra.
-Import MonadNotation.
+Export MonadNotation.
 
 Definition state_goto (st : reg) (n : node) : stmnt :=
   Vnonblock (Vvar st) (Vlit (posToValue 32 n)).
@@ -316,7 +315,7 @@ Definition create_reg: mon reg :=
 Definition transf_module (f: function) : mon module :=
   do fin <- create_reg;
   do rtrn <- create_reg;
-  do _ <- traverselist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code));
+  do _ <- collectlist (transf_instr fin rtrn) (Maps.PTree.elements f.(RTL.fn_code));
   do start <- create_reg;
   do rst <- create_reg;
   do clk <- create_reg;
@@ -354,6 +353,6 @@ Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef
 
 Definition transf_program (d : program) : Errors.res module :=
   match main_function d.(AST.prog_main) d.(AST.prog_defs) with
-  | Some f => run_mon (max_state f) (transf_module f)
+  | Some f => transl_module f
   | _ => Errors.Error (Errors.msg "HTL: could not find main function")
   end.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index a7d65fc..8ea4384 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -17,8 +17,92 @@
  *)
 
 From Coq Require Import FSets.FMapPositive.
-From compcert Require RTL Op Maps.
-From coqup Require Import Coquplib Verilog Veriloggen Value HTL.
+From compcert Require RTL Op Maps Errors.
+From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap.
+
+Remark bind_inversion:
+  forall (A B: Type) (f: mon A) (g: A -> mon B)
+         (y: B) (s1 s3: st) (i: st_incr s1 s3),
+    bind f g s1 = OK y s3 i ->
+    exists x, exists s2, exists i1, exists i2,
+            f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2.
+Proof.
+  intros until i. unfold bind. destruct (f s1); intros.
+  discriminate.
+  exists a; exists s'; exists s.
+  destruct (g a s'); inv H.
+  exists s0; auto.
+Qed.
+
+Remark bind2_inversion:
+  forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C)
+         (z: C) (s1 s3: st) (i: st_incr s1 s3),
+    bind2 f g s1 = OK z s3 i ->
+    exists x, exists y, exists s2, exists i1, exists i2,
+              f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2.
+Proof.
+  unfold bind2; intros.
+  exploit bind_inversion; eauto.
+  intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q.
+  exists x; exists y; exists s2; exists i1; exists i2; auto.
+Qed.
+
+Ltac monadInv1 H :=
+  match type of H with
+  | (OK _ _ _ = OK _ _ _) =>
+    inversion H; clear H; try subst
+  | (Error _ _ = OK _ _ _) =>
+    discriminate
+  | (ret _ _ = OK _ _ _) =>
+    inversion H; clear H; try subst
+  | (error _ _ = OK _ _ _) =>
+    discriminate
+  | (bind ?F ?G ?S = OK ?X ?S' ?I) =>
+    let x := fresh "x" in (
+      let s := fresh "s" in (
+        let i1 := fresh "INCR" in (
+          let i2 := fresh "INCR" in (
+            let EQ1 := fresh "EQ" in (
+              let EQ2 := fresh "EQ" in (
+                destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]];
+                clear H;
+                try (monadInv1 EQ2)))))))
+  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) =>
+    let x1 := fresh "x" in (
+      let x2 := fresh "x" in (
+        let s := fresh "s" in (
+          let i1 := fresh "INCR" in (
+            let i2 := fresh "INCR" in (
+              let EQ1 := fresh "EQ" in (
+                let EQ2 := fresh "EQ" in (
+                  destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]];
+                  clear H;
+                  try (monadInv1 EQ2))))))))
+  end.
+
+Ltac monadInv H :=
+  match type of H with
+  | (ret _ _ = OK _ _ _) => monadInv1 H
+  | (error _ _ = OK _ _ _) => monadInv1 H
+  | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
+  | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H
+  | (?F _ _ _ _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  | (?F _ = OK _ _ _) =>
+    ((progress simpl in H) || unfold F in H); monadInv1 H
+  end.
 
 (** * Relational specification of the translation *)
 
@@ -64,29 +148,142 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-      tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
+    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
 
-Inductive tr_code (c : RTL.code) (pc : RTL.node) (stmnts trans : PositiveMap.t stmnt)
+Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PositiveMap.t stmnt)
           (fin rtrn st : reg) : Prop :=
   tr_code_intro :
-    forall i s t,
-      Maps.PTree.get pc c = Some i ->
+    forall s t,
       stmnts!pc = Some s ->
       trans!pc = Some t ->
       tr_instr fin rtrn st i s t ->
-      tr_code c pc stmnts trans fin rtrn st.
+      tr_code pc i stmnts trans fin rtrn st.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
-    forall data control fin rtrn st,
-      (forall pc, tr_code f.(RTL.fn_code) pc data control fin rtrn st) ->
-      tr_module f (mkmodule
-                     f.(RTL.fn_params)
-                     data
-                     control
-                     f.(RTL.fn_entrypoint)
-                     st fin rtrn).
+    forall data control fin rtrn st m,
+      (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i ->
+                    tr_code pc i data control fin rtrn st) ->
+      m = (mkmodule f.(RTL.fn_params)
+                        data
+                        control
+                        f.(RTL.fn_entrypoint)
+                            st fin rtrn) ->
+      tr_module f m.
+
+Lemma create_reg_datapath_trans :
+  forall s s' x i,
+    create_reg s = OK x s' i ->
+    s.(st_datapath) = s'.(st_datapath).
+Proof. intros. monadInv H. trivial. Qed.
+
+Lemma create_reg_controllogic_trans :
+  forall s s' x i,
+    create_reg s = OK x s' i ->
+    s.(st_controllogic) = s'.(st_controllogic).
+Proof. intros. monadInv H. trivial. Qed.
+
+Lemma get_refl_x :
+  forall s s' x i,
+    get s = OK x s' i ->
+    s = x.
+Proof. inversion 1. trivial. Qed.
+
+Lemma get_refl_s :
+  forall s s' x i,
+    get s = OK x s' i ->
+    s = s'.
+Proof. inversion 1. trivial. Qed.
+
+Ltac inv_incr :=
+  match goal with
+  | [ H: create_reg ?s = OK _ ?s' _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); eapply create_reg_datapath_trans in H;
+    eapply create_reg_controllogic_trans in H1; inv_incr
+  | [ H: get ?s = OK _ _ _ |- _ ] =>
+    let H1 := fresh "H" in
+    assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
+    subst; inv_incr
+  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H; inv_incr
+  | [ H: st_incr _ _ |- _ ] => destruct st_incr; inv_incr
+  | _ => idtac
+  end.
+
+Ltac rewrite_states :=
+  match goal with
+  | [ H: ?x ?s = ?x ?s' |- _ ] =>
+    let c1 := fresh "c" in
+    let c2 := fresh "c" in
+    remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
+  end.
+
+Lemma iter_expand_instr_spec :
+  forall l fin rtrn s s' i x,
+    HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
+    list_norepet (List.map fst l) ->
+    (forall pc instr, In (pc, instr) l ->
+                      tr_code pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
+Proof.
+  induction l; simpl; intros.
+  - contradiction.
+  - destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
+    destruct (peq pc pc1).
+
+    + subst.
+      destruct instr1.
+      econstructor.
+      unfold add_instr in EQ.
+      destruct (check_empty_node_datapath s1 pc1); try discriminate.
+      destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+      inversion EQ.
+      destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+
+      unfold add_instr in EQ.
+      destruct (check_empty_node_datapath s1 pc1); try discriminate.
+      destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+      inversion EQ.
+      destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+
+    + eapply IHl. apply EQ0. assumption.
+      destruct H1. inversion H1. subst. contradiction.
+      assumption.
+
+Qed.
+
+Theorem transl_module_correct :
+  forall f m,
+    transl_module f = Errors.OK m -> tr_module f m.
+Proof.
+  intros until m.
+  unfold transl_module.
+  unfold run_mon.
+  destruct (transf_module f (max_state f)) eqn:?; try discriminate.
+  intros. inv H.
+  inversion s; subst.
+
+  unfold transf_module in *.
+  monadInv Heqr.
+  econstructor; simpl; trivial.
+  intros.
+  inv_incr.
+  assert (st_controllogic s8 = st_controllogic s2).
+  { rewrite <- H5. rewrite <- H6. rewrite <- H7. trivial. }
+  rewrite <- H10.
+  assert (st_datapath s8 = st_datapath s2).
+  { rewrite <- EQ4. rewrite <- EQ3. rewrite <- EQ2. trivial. }
+  assert (st_st s5 = st_st s2).
+  { rewrite H10. rewrite <- H50. trivial. }
+  rewrite H80. rewrite H81. rewrite H82.
+  eapply iter_expand_instr_spec.
+  apply EQ0.
+  apply Maps.PTree.elements_keys_norepet.
+  apply Maps.PTree.elements_correct.
+  assumption.
+Qed.
-- 
cgit 


From 43b078ba35aec32840f459d67de3fe6408184cea Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 25 May 2020 22:32:33 +0100
Subject: Finished proving the first case

---
 src/translation/HTLgenspec.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 8ea4384..f01ab1c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -235,7 +235,7 @@ Proof.
     destruct (peq pc pc1).
 
     + subst.
-      destruct instr1.
+      destruct instr1 eqn:?.
       econstructor.
       unfold add_instr in EQ.
       destruct (check_empty_node_datapath s1 pc1); try discriminate.
@@ -251,10 +251,15 @@ Proof.
       destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
         [ discriminate | apply H7 ].
 
+      inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
     + eapply IHl. apply EQ0. assumption.
       destruct H1. inversion H1. subst. contradiction.
       assumption.
 
+      
+
 Qed.
 
 Theorem transl_module_correct :
-- 
cgit 


From bdd3b6734690100a7c696cf57bfe52963ec2c6ef Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 26 May 2020 12:04:59 +0100
Subject: Finished second pass and fixed bug

---
 src/translation/HTLgen.v     |  2 +-
 src/translation/HTLgenspec.v | 53 ++++++++++++++++++++++++++++++--------------
 2 files changed, 37 insertions(+), 18 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 714cf98..670dcd4 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -272,7 +272,7 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
     | Inop n' => add_instr n n' Vskip
     | Iop op args dst n' =>
       do instr <- translate_instr op args;
-      add_instr n n' (block dst instr)
+      add_instr n n' (nonblock dst instr)
     | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.")
     | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.")
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index f01ab1c..c8f1751 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -222,6 +222,12 @@ Ltac rewrite_states :=
     remember (?x ?s) as c1; remember (?x ?s') as c2; try subst
   end.
 
+Lemma translate_instr_tr_op :
+  forall op args s s' e i,
+    translate_instr op args s = OK e s' i ->
+    tr_op op args e.
+Admitted.
+
 Lemma iter_expand_instr_spec :
   forall l fin rtrn s s' i x,
     HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
@@ -236,30 +242,43 @@ Proof.
 
     + subst.
       destruct instr1 eqn:?.
-      econstructor.
-      unfold add_instr in EQ.
-      destruct (check_empty_node_datapath s1 pc1); try discriminate.
-      destruct (check_empty_node_controllogic s1 pc1); try discriminate.
-      inversion EQ.
-      destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-        [ discriminate | apply H7 ].
 
-      unfold add_instr in EQ.
-      destruct (check_empty_node_datapath s1 pc1); try discriminate.
-      destruct (check_empty_node_controllogic s1 pc1); try discriminate.
-      inversion EQ.
-      destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-        [ discriminate | apply H7 ].
+      * unfold add_instr in EQ.
+        destruct (check_empty_node_datapath s1 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+        inversion EQ.
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+      * monadInv EQ.
+        inv_incr.
+        unfold add_instr in EQ2.
+        destruct (check_empty_node_datapath s0 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s0 pc1); try discriminate.
+        inversion EQ2.
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
 
-      inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
-      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor.
+        eapply translate_instr_tr_op. apply EQ1.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
     + eapply IHl. apply EQ0. assumption.
       destruct H1. inversion H1. subst. contradiction.
       assumption.
 
-      
-
 Qed.
 
 Theorem transl_module_correct :
-- 
cgit 


From b3c58bddaa0aa06f2c0905eeb3eb5318cb6361aa Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 26 May 2020 13:02:15 +0100
Subject: Finished proof of spec completely

---
 src/translation/HTLgen.v     | 35 ++++++++++++++++++++++--
 src/translation/HTLgenspec.v | 64 +++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 94 insertions(+), 5 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 670dcd4..26dc630 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -142,6 +142,37 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
 
+Lemma add_instr_skip_state_incr :
+  forall s n st,
+    (st_datapath s)!n = None ->
+    (st_controllogic s)!n = None ->
+    st_incr s
+    (mkstate
+       s.(st_st)
+       s.(st_freshreg)
+       (st_freshstate s)
+       (AssocMap.add n st s.(st_datapath))
+       (AssocMap.add n Vskip s.(st_controllogic))).
+Proof.
+  constructor; intros;
+    try (simpl; destruct (peq n n0); subst);
+    auto with htlh.
+Qed.
+
+Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
+  fun s =>
+    match check_empty_node_datapath s n, check_empty_node_controllogic s n with
+    | left STM, left TRANS =>
+      OK tt (mkstate
+               s.(st_st)
+               s.(st_freshreg)
+               (st_freshstate s)
+               (AssocMap.add n st s.(st_datapath))
+               (AssocMap.add n Vskip s.(st_controllogic)))
+         (add_instr_skip_state_incr s n st STM TRANS)
+    | _, _ => Error (Errors.msg "HTL.add_instr")
+    end.
+
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.
 
@@ -285,9 +316,9 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit :=
     | Ireturn r =>
       match r with
       | Some r' =>
-        add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r')))
       | None =>
-        add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z)))
+        add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z))))
       end
     end
   end.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index c8f1751..06ed68d 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -148,7 +148,8 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
       translate_condition cond args s = OK c s' i ->
       tr_instr fin rtrn st (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
-    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
+    tr_instr fin rtrn st (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)))
+                                                  (block rtrn (Vlit (ZToValue 1%nat 0%Z)))) Vskip
 | tr_instr_Ireturn_Some :
     forall r,
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
@@ -226,7 +227,15 @@ Lemma translate_instr_tr_op :
   forall op args s s' e i,
     translate_instr op args s = OK e s' i ->
     tr_op op args e.
-Admitted.
+Proof.
+  intros.
+  destruct op eqn:?; try (econstructor; apply H); try discriminate; simpl in *;
+    try (match goal with
+           [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] =>
+           repeat (destruct args; try discriminate)
+         end);
+    monadInv H; constructor.
+Qed.
 
 Lemma iter_expand_instr_spec :
   forall l fin rtrn s s' i x,
@@ -241,7 +250,7 @@ Proof.
     destruct (peq pc pc1).
 
     + subst.
-      destruct instr1 eqn:?.
+      destruct instr1 eqn:?; try discriminate.
 
       * unfold add_instr in EQ.
         destruct (check_empty_node_datapath s1 pc1); try discriminate.
@@ -275,6 +284,55 @@ Proof.
 
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
+      * monadInv EQ.
+        inv_incr.
+        unfold add_branch_instr in EQ2.
+        destruct (check_empty_node_datapath s0 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s0 pc1); try discriminate.
+        inversion EQ2.
+
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor.
+        apply EQ1.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+      * destruct o3 eqn:?.
+        unfold add_instr_skip in EQ.
+        destruct (check_empty_node_datapath s1 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+        inversion EQ.
+
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. constructor.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+        unfold add_instr_skip in EQ.
+        destruct (check_empty_node_datapath s1 pc1); try discriminate.
+        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
+        inversion EQ.
+
+        econstructor.
+        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+
+        inversion H1. inversion H7. apply constructor.
+
+        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
     + eapply IHl. apply EQ0. assumption.
       destruct H1. inversion H1. subst. contradiction.
       assumption.
-- 
cgit 


From e4dac24479752b7d2645c9ba9dc23b73051f0f9e Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 26 May 2020 17:33:45 +0100
Subject: Working on automation

---
 src/translation/HTLgenspec.v | 110 +++++++++++++++++++------------------------
 1 file changed, 48 insertions(+), 62 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 06ed68d..9c46b48 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -237,6 +237,37 @@ Proof.
     monadInv H; constructor.
 Qed.
 
+Ltac unfold_match H :=
+  match type of H with
+  | context[match ?g with _ => _ end] => destruct g; try discriminate
+  end.
+
+Ltac inv_add_instr' H :=
+  match type of H with
+  | ?f _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ = OK _ _ _ => unfold f in H
+  | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H
+  end; repeat unfold_match H; inversion H.
+
+Ltac inv_add_instr :=
+  match goal with
+  | H: context[add_instr_skip _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_instr_skip _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_instr _ _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_instr _ _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  | H: context[add_branch_instr _ _ _ _ _] |- _ =>
+    inv_add_instr' H
+  | H: context[add_branch_instr _ _ _ _] |- _ =>
+    monadInv H; inv_incr; inv_add_instr
+  end.
+
+Ltac destruct_optional :=
+  match goal with H: option ?r |- _ => destruct H end.
+
 Lemma iter_expand_instr_spec :
   forall l fin rtrn s s' i x,
     HTLMonadExtra.collectlist (transf_instr fin rtrn) l s = OK x s' i ->
@@ -250,87 +281,42 @@ Proof.
     destruct (peq pc pc1).
 
     + subst.
-      destruct instr1 eqn:?; try discriminate.
-
-      * unfold add_instr in EQ.
-        destruct (check_empty_node_datapath s1 pc1); try discriminate.
-        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
-        inversion EQ.
-        econstructor.
-        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
+      destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor.
 
-        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-
-        inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
+      * destruct o0 with pc1; destruct  H9; simpl in *; rewrite AssocMap.gss in H7;
+          [ discriminate | apply H7 ].
+      * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
-      * monadInv EQ.
-        inv_incr.
-        unfold add_instr in EQ2.
-        destruct (check_empty_node_datapath s0 pc1); try discriminate.
-        destruct (check_empty_node_controllogic s0 pc1); try discriminate.
-        inversion EQ2.
-        econstructor.
-        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-
-        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-
-        inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor.
+      * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor.
         eapply translate_instr_tr_op. apply EQ1.
-
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
-      * monadInv EQ.
-        inv_incr.
-        unfold add_branch_instr in EQ2.
-        destruct (check_empty_node_datapath s0 pc1); try discriminate.
-        destruct (check_empty_node_controllogic s0 pc1); try discriminate.
-        inversion EQ2.
-
-        econstructor.
-        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-
-        inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor.
-        apply EQ1.
-
+      * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1.
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
-      * destruct o3 eqn:?.
-        unfold add_instr_skip in EQ.
-        destruct (check_empty_node_datapath s1 pc1); try discriminate.
-        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
-        inversion EQ.
-
-        econstructor.
-        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-
-        inversion H1. inversion H7. constructor.
-
+      * inversion H1. inversion H7. constructor.
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
-        unfold add_instr_skip in EQ.
-        destruct (check_empty_node_datapath s1 pc1); try discriminate.
-        destruct (check_empty_node_controllogic s1 pc1); try discriminate.
-        inversion EQ.
-
-        econstructor.
-        destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-        destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
           [ discriminate | apply H7 ].
-
-        inversion H1. inversion H7. apply constructor.
-
+      * inversion H1. inversion H7. constructor.
         eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
 
     + eapply IHl. apply EQ0. assumption.
-- 
cgit 


From cb00777e134464a01a9e97efb448cee7473df9d5 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 27 May 2020 15:05:20 +0100
Subject: Add top level definition

---
 src/translation/HTLgenproof.v | 166 ++++++++++++++++++++++--------------------
 src/translation/HTLgenspec.v  | 125 ++++++++++++++++---------------
 2 files changed, 153 insertions(+), 138 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index cb621a8..b07c654 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -16,34 +16,39 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From coqup Require Import HTLgenspec Value AssocMap.
+From coqup Require Import Coquplib HTLgenspec HTLgen Value AssocMap.
 From coqup Require HTL Verilog.
 From compcert Require RTL Registers Globalenvs AST.
 
 Import AssocMapNotation.
 
+Hint Resolve Smallstep.forward_simulation_plus : htlproof.
+Hint Resolve AssocMap.gss : htlproof.
+Hint Resolve AssocMap.gso : htlproof.
+
 Inductive match_assocmaps : RTL.regset -> assocmap -> Prop :=
 | match_assocmap : forall rs am,
     (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
     match_assocmaps rs am.
+Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
   forall st assoc,
   s = HTL.State m st assoc ->
   assoc!(m.(HTL.mod_st)) = Some (posToValue 32 st).
+Hint Unfold state_st_wf : htlproof.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
     (MASSOC : match_assocmaps rs assoc)
     (TF : tr_module f m)
-    (TC : tr_code f.(RTL.fn_code) st m.(HTL.mod_datapath) m.(HTL.mod_controllogic)
-                  m.(HTL.mod_finish) m.(HTL.mod_return) m.(HTL.mod_st))
     (WF : state_st_wf m (HTL.State m st assoc)),
     match_states (RTL.State sf f sp st rs mem)
                  (HTL.State m st assoc)
 | match_returnstate : forall v v' stack m,
     val_value_lessdef v v' ->
     match_states (RTL.Returnstate stack v m) (HTL.Returnstate v').
+Hint Constructors match_states : htlproof.
 
 Inductive match_program : RTL.program -> HTL.module -> Prop :=
   match_program_intro :
@@ -53,6 +58,7 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
     Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal f) ->
     tr_module f m ->
     match_program p m.
+Hint Constructors match_program : htlproof.
 
 Lemma regs_lessdef_regs :
   forall rs1 rs2 n v,
@@ -77,11 +83,6 @@ Lemma valToValue_lessdef :
     val_value_lessdef v (valToValue v).
 Admitted.
 
-Lemma assocmap_merge_add :
-  forall k v assoc,
-    AssocMap.add k v assoc = merge_assocmap (AssocMap.add k v empty_assocmap) assoc.
-Admitted.
-
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
   forall v,
@@ -116,30 +117,43 @@ Lemma regset_assocmap_wf2 :
 Admitted.
 
 Lemma st_greater_than_res :
-  forall m res,
-    HTL.mod_st m <> res.
+  forall m res : positive,
+    m <> res.
 Admitted.
 
 Lemma finish_not_return :
-  forall m,
-    HTL.mod_finish m <> HTL.mod_return m.
+  forall r f : positive,
+    r <> f.
 Admitted.
 
 Lemma finish_not_res :
-  forall m r,
-    HTL.mod_finish m <> r.
+  forall f r : positive,
+    f <> r.
 Admitted.
 
-Ltac subst_eq_hyp :=
-  match goal with
-    H1: ?x = Some ?i, H2: ?x = Some ?j |- _ =>
-    let H := fresh "H" in
-    rewrite H1 in H2; injection H2; intro H; clear H2; subst
-  end.
-
 Ltac unfold_merge :=
   try (repeat (rewrite merge_inj)); unfold merge_assocmap; rewrite AssocMapExt.merge_base.
 
+Ltac inv_state :=
+  match goal with
+    MSTATE : match_states _ _ |- _ =>
+    inversion MSTATE;
+    match goal with
+      TF : tr_module _ _ |- _ =>
+      inversion TF;
+      match goal with
+        TC : forall _ _,
+          Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _,
+        H : Maps.PTree.get _ _ = Some _ |- _ =>
+        apply TC in H; inversion H;
+        match goal with
+          TI : tr_instr _ _ _ _ _ _ |- _ =>
+          inversion TI
+        end
+      end
+    end
+  end; subst.
+
 Section CORRECTNESS.
 
   Variable prog : RTL.program.
@@ -160,7 +174,7 @@ Section CORRECTNESS.
 
   Lemma eval_cond_correct :
     forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc,
-    Veriloggen.translate_condition cond args s1 = Veriloggen.OK c s' i ->
+    translate_condition cond args s1 = OK c s' i ->
     Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b ->
     Verilog.expr_runp f assoc c (boolToValue 32 b).
   Admitted.
@@ -195,56 +209,37 @@ Section CORRECTNESS.
         match_states S1 R1 ->
         exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    induction 1; intros R1 MSTATE;
-      try (inversion MSTATE; inversion TC; inversion H12; subst_eq_hyp; discriminate).
+    induction 1; intros R1 MSTATE; try inv_state.
     - (* Inop *)
-      inversion MSTATE. subst.
       econstructor.
       split.
       apply Smallstep.plus_one.
-      inversion TC.
-      eapply HTL.step_module; subst_eq_hyp; inversion H3; subst.
-      apply H2.
-      apply H1.
+      eapply HTL.step_module; eauto.
       (* processing of state *)
       econstructor.
       simpl. trivial.
       econstructor. trivial.
-      inversion H3. subst.
       econstructor.
 
-      (* prove merge *)
-      apply assocmap_merge_add.
-
       (* prove stval *)
+      unfold_merge; simpl.
       apply AssocMap.gss.
-      apply assumption_32bit.
 
       (* prove match_state *)
-      constructor.
-      apply rs.
-      apply regs_lessdef_regs.
-      assumption.
-      assumption.
-      inversion TF. simpl. apply H0.
-      unfold state_st_wf. intros. inversion H0. subst.
-      apply AssocMap.gss.
+      unfold_merge. rewrite assumption_32bit.
+      constructor; auto.
+      apply regs_lessdef_regs. assumption.
+      unfold state_st_wf. inversion 1. subst. apply AssocMap.gss.
     - (* Iop *)
-      inversion MSTATE. subst.
       econstructor.
       split.
       apply Smallstep.plus_one.
-      inversion TC.
-      eapply HTL.step_module; subst_eq_hyp; inversion H4; subst.
-      apply H3.
-      apply H2.
-      econstructor.
-      simpl. trivial.
-      constructor. trivial.
-      econstructor.
-      simpl. trivial.
-      eapply eval_correct. apply H0. apply H10. trivial. trivial.
-      unfold_merge.
+      eapply HTL.step_module; eauto.
+      econstructor; simpl; trivial.
+      constructor; trivial.
+      econstructor; simpl; eauto.
+      eapply eval_correct; eauto.
+      unfold_merge. simpl.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
@@ -260,30 +255,24 @@ Section CORRECTNESS.
       assumption.
       apply valToValue_lessdef.
       assumption.
-      inversion TF. simpl. apply H2.
 
       unfold state_st_wf. intros. inversion H2. subst.
       unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply st_greater_than_res.
-    - inversion MSTATE; inversion TC;
-        inversion H12; subst_eq_hyp; inversion H13.
-    - inversion MSTATE. inversion TC. subst_eq_hyp. inversion H12. subst.
-      econstructor. split. apply Smallstep.plus_one.
-      eapply HTL.step_module. subst. apply H11. apply H10.
+    - econstructor. split. apply Smallstep.plus_one.
+      eapply HTL.step_module; eauto.
       eapply Verilog.stmnt_runp_Vnonblock with
           (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot).
       simpl. trivial.
       destruct b.
       eapply Verilog.erun_Vternary_true.
-      eapply eval_cond_correct. apply args.
-      apply H7. apply H0.
+      eapply eval_cond_correct; eauto.
       constructor.
       apply assumption_32bit_bool.
       eapply Verilog.erun_Vternary_false.
-      eapply eval_cond_correct. apply args.
-      apply H7. apply H0.
+      eapply eval_cond_correct; eauto.
       constructor.
       apply assumption_32bit_bool.
       trivial.
@@ -300,8 +289,6 @@ Section CORRECTNESS.
       apply regs_lessdef_regs. assumption.
       assumption.
 
-      inversion TF. simpl. apply H1.
-
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
       apply AssocMap.gss.
@@ -311,21 +298,15 @@ Section CORRECTNESS.
       apply regs_lessdef_regs. assumption.
       assumption.
 
-      inversion TF. simpl. apply H1.
-
       unfold state_st_wf. intros. inversion H1.
       subst. unfold_merge.
       apply AssocMap.gss.
 
     - (* Return *)
-      inversion MSTATE. inversion TC. subst_eq_hyp.
-      inversion H11. subst.
       econstructor. split.
       eapply Smallstep.plus_two.
       
-      eapply HTL.step_module.
-      apply H10.
-      apply H9.
+      eapply HTL.step_module; eauto.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
@@ -340,6 +321,7 @@ Section CORRECTNESS.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
+      unfold_merge; simpl.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply finish_not_return.
@@ -347,13 +329,11 @@ Section CORRECTNESS.
       rewrite Events.E0_left. trivial.
 
       constructor. constructor.
-      destruct (assoc!r) eqn:?.
+    - destruct (assoc!r) eqn:?.
       inversion H11. subst.
       econstructor. split.
       eapply Smallstep.plus_two.
-      eapply HTL.step_module.
-      apply H10.
-      apply H9.
+      eapply HTL.step_module; eauto.
       constructor.
       econstructor; simpl; trivial.
       econstructor; simpl; trivial.
@@ -370,12 +350,42 @@ Section CORRECTNESS.
       apply st_greater_than_res. apply st_greater_than_res. trivial.
 
       apply HTL.step_finish.
+      unfold_merge.
       rewrite AssocMap.gso.
       apply AssocMap.gss.
       apply finish_not_return.
       apply AssocMap.gss.
       rewrite Events.E0_left. trivial.
 
-      constructor. simpl. Search Registers.Regmap.get.
+      constructor. simpl.
+      Admitted.
+  Hint Resolve transl_step_correct : htlproof.
+
+  Lemma senv_preserved :
+    forall id : AST.ident,
+      Globalenvs.Senv.public_symbol (Smallstep.symbolenv (HTL.semantics tprog)) id =
+      Globalenvs.Senv.public_symbol (Smallstep.symbolenv (RTL.semantics prog)) id.
+  Proof. Admitted.
+  Hint Resolve senv_preserved : htlproof.
+
+  Lemma transl_initial_states :
+    forall s1 : Smallstep.state (RTL.semantics prog),
+      Smallstep.initial_state (RTL.semantics prog) s1 ->
+      exists s2 : Smallstep.state (HTL.semantics tprog),
+        Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2.
+  Proof. Admitted.
+  Hint Resolve transl_initial_states : htlproof.
+
+  Lemma transl_final_states :
+    forall (s1 : Smallstep.state (RTL.semantics prog)) (s2 : Smallstep.state (HTL.semantics tprog))
+           (r : Integers.Int.int),
+      match_states s1 s2 ->
+      Smallstep.final_state (RTL.semantics prog) s1 r -> Smallstep.final_state (HTL.semantics tprog) s2 r.
+  Proof. Admitted.
+  Hint Resolve transl_final_states : htlproof.
+
+  Theorem transf_program_correct:
+    Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog).
+  Proof. eauto with htlproof. Qed.
 
 End CORRECTNESS.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 9c46b48..b9d483c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -20,6 +20,9 @@ From Coq Require Import FSets.FMapPositive.
 From compcert Require RTL Op Maps Errors.
 From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap.
 
+Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
+Hint Resolve Maps.PTree.elements_correct : htlspec.
+
 Remark bind_inversion:
   forall (A B: Type) (f: mon A) (g: A -> mon B)
          (y: B) (s1 s3: st) (i: st_incr s1 s3),
@@ -134,6 +137,7 @@ Inductive tr_op : Op.operation -> list reg -> expr -> Prop :=
 | tr_op_Oshrimm : forall n r, tr_op (Op.Oshrimm n) (r::nil) (boplit Vshr r n)
 | tr_op_Ocmp : forall c l e s s' i, translate_condition c l s = OK e s' i -> tr_op (Op.Ocmp c) l e
 | tr_op_Olea : forall a l e s s' i, translate_eff_addressing a l s = OK e s' i -> tr_op (Op.Olea a) l e.
+Hint Constructors tr_op : htlspec.
 
 Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
 | tr_instr_Inop :
@@ -154,6 +158,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
     forall r,
       tr_instr fin rtrn st (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
+Hint Constructors tr_instr : htlspec.
 
 Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PositiveMap.t stmnt)
           (fin rtrn st : reg) : Prop :=
@@ -163,6 +168,7 @@ Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : Positive
       trans!pc = Some t ->
       tr_instr fin rtrn st i s t ->
       tr_code pc i stmnts trans fin rtrn st.
+Hint Constructors tr_code : htlspec.
 
 Inductive tr_module (f : RTL.function) : module -> Prop :=
   tr_module_intro :
@@ -175,44 +181,48 @@ Inductive tr_module (f : RTL.function) : module -> Prop :=
                         f.(RTL.fn_entrypoint)
                             st fin rtrn) ->
       tr_module f m.
+Hint Constructors tr_module : htlspec.
 
 Lemma create_reg_datapath_trans :
   forall s s' x i,
     create_reg s = OK x s' i ->
     s.(st_datapath) = s'.(st_datapath).
 Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_datapath_trans : htlspec.
 
 Lemma create_reg_controllogic_trans :
   forall s s' x i,
     create_reg s = OK x s' i ->
     s.(st_controllogic) = s'.(st_controllogic).
 Proof. intros. monadInv H. trivial. Qed.
+Hint Resolve create_reg_controllogic_trans : htlspec.
 
 Lemma get_refl_x :
   forall s s' x i,
     get s = OK x s' i ->
     s = x.
 Proof. inversion 1. trivial. Qed.
+Hint Resolve get_refl_x : htlspec.
 
 Lemma get_refl_s :
   forall s s' x i,
     get s = OK x s' i ->
     s = s'.
 Proof. inversion 1. trivial. Qed.
+Hint Resolve get_refl_s : htlspec.
 
 Ltac inv_incr :=
-  match goal with
+  repeat match goal with
   | [ H: create_reg ?s = OK _ ?s' _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); eapply create_reg_datapath_trans in H;
-    eapply create_reg_controllogic_trans in H1; inv_incr
+    eapply create_reg_controllogic_trans in H1
   | [ H: get ?s = OK _ _ _ |- _ ] =>
     let H1 := fresh "H" in
     assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1;
-    subst; inv_incr
-  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H; inv_incr
-  | [ H: st_incr _ _ |- _ ] => destruct st_incr; inv_incr
-  | _ => idtac
+    subst
+  | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H
+  | [ H: st_incr _ _ |- _ ] => destruct st_incr
   end.
 
 Ltac rewrite_states :=
@@ -229,13 +239,14 @@ Lemma translate_instr_tr_op :
     tr_op op args e.
 Proof.
   intros.
-  destruct op eqn:?; try (econstructor; apply H); try discriminate; simpl in *;
+  destruct op eqn:?; eauto with htlspec; try discriminate; simpl in *;
     try (match goal with
            [ H: match ?args with _ => _ end _ = _ _ _ |- _ ] =>
            repeat (destruct args; try discriminate)
          end);
     monadInv H; constructor.
 Qed.
+Hint Resolve translate_instr_tr_op : htlspec.
 
 Ltac unfold_match H :=
   match type of H with
@@ -275,55 +286,53 @@ Lemma iter_expand_instr_spec :
     (forall pc instr, In (pc, instr) l ->
                       tr_code pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st)).
 Proof.
-  induction l; simpl; intros.
-  - contradiction.
-  - destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
-    destruct (peq pc pc1).
-
-    + subst.
-      destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor.
-
-      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * destruct o0 with pc1; destruct  H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
-        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
-
-      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor.
-        eapply translate_instr_tr_op. apply EQ1.
-        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
-
-      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1.
-        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
-
-      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * inversion H1. inversion H7. constructor.
-        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
-
-      * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
-          [ discriminate | apply H7 ].
-      * inversion H1. inversion H7. constructor.
-        eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
-
-    + eapply IHl. apply EQ0. assumption.
-      destruct H1. inversion H1. subst. contradiction.
-      assumption.
-
+  induction l; simpl; intros; try contradiction.
+  destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
+  destruct (peq pc pc1).
+  + subst.
+    destruct instr1 eqn:?; try discriminate; try destruct_optional; inv_add_instr; econstructor.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct  H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. rewrite H. apply tr_instr_Inop.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. unfold nonblock. rewrite <- e2. rewrite H. constructor.
+      eapply translate_instr_tr_op. apply EQ1.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. rewrite <- e2. rewrite H. econstructor. apply EQ1.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. constructor.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+    * destruct o with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * destruct o0 with pc1; destruct H9; simpl in *; rewrite AssocMap.gss in H7;
+        [ discriminate | apply H7 ].
+    * inversion H1. inversion H7. constructor.
+      eapply in_map with (f := fst) in H7. simpl in H7. contradiction.
+
+  + eapply IHl. apply EQ0. assumption.
+    destruct H1. inversion H1. subst. contradiction.
+    assumption.
 Qed.
+Hint Resolve iter_expand_instr_spec : htlspec.
 
 Theorem transl_module_correct :
   forall f m,
@@ -349,9 +358,5 @@ Proof.
   assert (st_st s5 = st_st s2).
   { rewrite H10. rewrite <- H50. trivial. }
   rewrite H80. rewrite H81. rewrite H82.
-  eapply iter_expand_instr_spec.
-  apply EQ0.
-  apply Maps.PTree.elements_keys_norepet.
-  apply Maps.PTree.elements_correct.
-  assumption.
+  eauto with htlspec.
 Qed.
-- 
cgit 


From 213267be33d714dabd19ca09210b5dc1ad4f6254 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 27 May 2020 23:38:40 +0100
Subject: Add more proofs and remove Admitted

---
 src/translation/HTLgenproof.v | 92 ++++++++++++++++++++-----------------------
 1 file changed, 43 insertions(+), 49 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index b07c654..499b6b5 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -26,10 +26,11 @@ Hint Resolve Smallstep.forward_simulation_plus : htlproof.
 Hint Resolve AssocMap.gss : htlproof.
 Hint Resolve AssocMap.gso : htlproof.
 
-Inductive match_assocmaps : RTL.regset -> assocmap -> Prop :=
-| match_assocmap : forall rs am,
-    (forall r, val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
-    match_assocmaps rs am.
+Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
+  match_assocmap : forall f rs am,
+    (forall r, Ple r (RTL.max_reg_function f) ->
+               val_value_lessdef (Registers.Regmap.get r rs) am#r) ->
+    match_assocmaps f rs am.
 Hint Constructors match_assocmaps : htlproof.
 
 Definition state_st_wf (m : HTL.module) (s : HTL.state) :=
@@ -40,7 +41,7 @@ Hint Unfold state_st_wf : htlproof.
 
 Inductive match_states : RTL.state -> HTL.state -> Prop :=
 | match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st
-    (MASSOC : match_assocmaps rs assoc)
+    (MASSOC : match_assocmaps f rs assoc)
     (TF : tr_module f m)
     (WF : state_st_wf m (HTL.State m st assoc)),
     match_states (RTL.State sf f sp st rs mem)
@@ -61,27 +62,45 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
 Hint Constructors match_program : htlproof.
 
 Lemma regs_lessdef_regs :
-  forall rs1 rs2 n v,
-    match_assocmaps rs1 rs2 ->
-    match_assocmaps rs1 (AssocMap.add n v rs2).
-Admitted.
+  forall f rs1 rs2 n v,
+    Plt (RTL.max_reg_function f) n ->
+    match_assocmaps f rs1 rs2 ->
+    match_assocmaps f rs1 (AssocMap.add n v rs2).
+Proof.
+  inversion 2; subst.
+  intros. constructor.
+  intros. unfold find_assocmap. unfold AssocMapExt.find_default.
+  rewrite AssocMap.gso. eauto.
+  apply Pos.le_lt_trans with _ _ n in H2.
+  unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
+Qed.
 
 Lemma regs_add_match :
-  forall rs am r v v',
-    match_assocmaps rs am ->
+  forall f rs am r v v',
     val_value_lessdef v v' ->
-    match_assocmaps (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
-Admitted.
-
-Lemma merge_inj :
-  forall am am' r v,
-    merge_assocmap (AssocMap.add r v am) am' = AssocMap.add r v (merge_assocmap am am').
-Admitted.
+    match_assocmaps f rs am ->
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
+Proof.
+  inversion 2; subst.
+  constructor. intros.
+  destruct (peq r0 r); subst.
+  rewrite Registers.Regmap.gss.
+  unfold find_assocmap. unfold AssocMapExt.find_default.
+  rewrite AssocMap.gss. assumption.
+
+  rewrite Registers.Regmap.gso; try assumption.
+  unfold find_assocmap. unfold AssocMapExt.find_default.
+  rewrite AssocMap.gso; eauto.
+Qed.
 
 Lemma valToValue_lessdef :
-  forall v,
-    val_value_lessdef v (valToValue v).
-Admitted.
+  forall v v',
+    valToValue v = Some v' <->
+    val_value_lessdef v v'.
+Proof.
+  split; intros.
+  destruct v; try discriminate; constructor.
+  unfold valToValue in H. inversion H. unfold intToValue
 
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
@@ -94,28 +113,6 @@ Lemma assumption_32bit_bool :
     valueToBool (boolToValue 32 b) = b.
 Admitted.
 
-Lemma regset_assocmap_get :
-  forall r rs am v v',
-    match_assocmaps rs am ->
-    v = Registers.Regmap.get r rs ->
-    v' = am#r ->
-    val_value_lessdef v v'.
-Proof. inversion 1. intros. subst. apply H0. Qed.
-
-Lemma regset_assocmap_wf :
-  forall r rs am i,
-    match_assocmaps rs am ->
-    Values.Vint i <> Registers.Regmap.get r rs ->
-    am!r = None.
-Admitted.
-
-Lemma regset_assocmap_wf2 :
-  forall r rs am i,
-    match_assocmaps rs am ->
-    Values.Vint i = Registers.Regmap.get r rs ->
-    am!r = Some (intToValue i).
-Admitted.
-
 Lemma st_greater_than_res :
   forall m res : positive,
     m <> res.
@@ -131,9 +128,6 @@ Lemma finish_not_res :
     f <> r.
 Admitted.
 
-Ltac unfold_merge :=
-  try (repeat (rewrite merge_inj)); unfold merge_assocmap; rewrite AssocMapExt.merge_base.
-
 Ltac inv_state :=
   match goal with
     MSTATE : match_states _ _ |- _ =>
@@ -222,12 +216,12 @@ Section CORRECTNESS.
       econstructor.
 
       (* prove stval *)
-      unfold_merge; simpl.
-      apply AssocMap.gss.
+      unfold merge_assocmap. apply AssocMapExt.merge_add. simpl. apply AssocMap.gss.
 
       (* prove match_state *)
-      unfold_merge. rewrite assumption_32bit.
+      rewrite assumption_32bit.
       constructor; auto.
+      unfold merge_assocmap. rewrite AssocMapExt.merge_add. simpl. apply AssocMap.gss.
       apply regs_lessdef_regs. assumption.
       unfold state_st_wf. inversion 1. subst. apply AssocMap.gss.
     - (* Iop *)
-- 
cgit 


From 3beb6e00213c5e7409d4574b663e5c6bf7490d66 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 29 May 2020 14:42:09 +0100
Subject: Change AssocMap to Maps.PTree

---
 src/translation/HTLgenproof.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 499b6b5..b7b9d27 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -100,7 +100,8 @@ Lemma valToValue_lessdef :
 Proof.
   split; intros.
   destruct v; try discriminate; constructor.
-  unfold valToValue in H. inversion H. unfold intToValue
+  unfold valToValue in H. inversion H.
+  Admitted.
 
 (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *)
 Lemma assumption_32bit :
@@ -159,11 +160,12 @@ Section CORRECTNESS.
   Let tge : HTL.genv := HTL.genv_empty.
 
   Lemma eval_correct :
-    forall sp op rs args m v e assoc f,
+    forall sp op rs args m v v' e assoc f,
       Op.eval_operation ge sp op
 (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v ->
       tr_op op args e ->
-      Verilog.expr_runp f assoc e (valToValue v).
+      valToValue v = Some v' ->
+      Verilog.expr_runp f assoc e v'.
   Admitted.
 
   Lemma eval_cond_correct :
-- 
cgit 


From 6c4e2ba64c17952b432a0f01122c065cae24dacf Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Fri, 29 May 2020 18:04:28 +0100
Subject: Improve automation in HTLgenspec.

---
 src/translation/HTLgenspec.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index b9d483c..9c08959 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -350,13 +350,10 @@ Proof.
   econstructor; simpl; trivial.
   intros.
   inv_incr.
-  assert (st_controllogic s8 = st_controllogic s2).
-  { rewrite <- H5. rewrite <- H6. rewrite <- H7. trivial. }
+  assert (st_controllogic s8 = st_controllogic s2) by congruence.
   rewrite <- H10.
-  assert (st_datapath s8 = st_datapath s2).
-  { rewrite <- EQ4. rewrite <- EQ3. rewrite <- EQ2. trivial. }
-  assert (st_st s5 = st_st s2).
-  { rewrite H10. rewrite <- H50. trivial. }
+  assert (st_datapath s8 = st_datapath s2) by congruence.
+  assert (st_st s5 = st_st s2) by congruence.
   rewrite H80. rewrite H81. rewrite H82.
   eauto with htlspec.
 Qed.
-- 
cgit 


From e06577fe952a3c268520b280b020bb2bff252529 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 29 May 2020 18:14:59 +0100
Subject: Fix compilation moving to PTree

---
 src/translation/HTLgen.v      | 24 ++++++++++++------------
 src/translation/HTLgenproof.v | 31 ++++++++++++++++++++-----------
 src/translation/HTLgenspec.v  |  4 ++--
 3 files changed, 34 insertions(+), 25 deletions(-)

(limited to 'src/translation')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 26dc630..4564237 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -120,8 +120,8 @@ Lemma add_instr_state_incr :
        s.(st_st)
        s.(st_freshreg)
        (st_freshstate s)
-       (AssocMap.add n st s.(st_datapath))
-       (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic))).
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).
 Proof.
   constructor; intros;
     try (simpl; destruct (peq n n0); subst);
@@ -136,8 +136,8 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=
                s.(st_st)
                s.(st_freshreg)
                (st_freshstate s)
-               (AssocMap.add n st s.(st_datapath))
-               (AssocMap.add n (state_goto s.(st_st) n') s.(st_controllogic)))
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))
          (add_instr_state_incr s n n' st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
@@ -151,8 +151,8 @@ Lemma add_instr_skip_state_incr :
        s.(st_st)
        s.(st_freshreg)
        (st_freshstate s)
-       (AssocMap.add n st s.(st_datapath))
-       (AssocMap.add n Vskip s.(st_controllogic))).
+       (AssocMap.set n st s.(st_datapath))
+       (AssocMap.set n Vskip s.(st_controllogic))).
 Proof.
   constructor; intros;
     try (simpl; destruct (peq n n0); subst);
@@ -167,8 +167,8 @@ Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=
                s.(st_st)
                s.(st_freshreg)
                (st_freshstate s)
-               (AssocMap.add n st s.(st_datapath))
-               (AssocMap.add n Vskip s.(st_controllogic)))
+               (AssocMap.set n st s.(st_datapath))
+               (AssocMap.set n Vskip s.(st_controllogic)))
          (add_instr_skip_state_incr s n st STM TRANS)
     | _, _ => Error (Errors.msg "HTL.add_instr")
     end.
@@ -274,8 +274,8 @@ Lemma add_branch_instr_state_incr:
                  s.(st_st)
                 (st_freshreg s)
                 (st_freshstate s)
-                (AssocMap.add n Vskip (st_datapath s))
-                (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).
 Proof.
   intros. apply state_incr_intro; simpl;
             try (intros; destruct (peq n0 n); subst);
@@ -290,8 +290,8 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
                s.(st_st)
                 (st_freshreg s)
                 (st_freshstate s)
-                (AssocMap.add n Vskip (st_datapath s))
-                (AssocMap.add n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
+                (AssocMap.set n Vskip (st_datapath s))
+                (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))
          (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)
     | _, _ => Error (Errors.msg "Veriloggen: add_branch_instr")
     end.
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index b7b9d27..2d2129c 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -26,6 +26,8 @@ Hint Resolve Smallstep.forward_simulation_plus : htlproof.
 Hint Resolve AssocMap.gss : htlproof.
 Hint Resolve AssocMap.gso : htlproof.
 
+Hint Unfold find_assocmap AssocMapExt.get_default : htlproof.
+
 Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop :=
   match_assocmap : forall f rs am,
     (forall r, Ple r (RTL.max_reg_function f) ->
@@ -61,37 +63,39 @@ Inductive match_program : RTL.program -> HTL.module -> Prop :=
     match_program p m.
 Hint Constructors match_program : htlproof.
 
-Lemma regs_lessdef_regs :
+Lemma regs_lessdef_add_greater :
   forall f rs1 rs2 n v,
     Plt (RTL.max_reg_function f) n ->
     match_assocmaps f rs1 rs2 ->
-    match_assocmaps f rs1 (AssocMap.add n v rs2).
+    match_assocmaps f rs1 (AssocMap.set n v rs2).
 Proof.
   inversion 2; subst.
   intros. constructor.
-  intros. unfold find_assocmap. unfold AssocMapExt.find_default.
+  intros. unfold find_assocmap. unfold AssocMapExt.get_default.
   rewrite AssocMap.gso. eauto.
   apply Pos.le_lt_trans with _ _ n in H2.
   unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption.
 Qed.
+Hint Resolve regs_lessdef_add_greater : htlproof.
 
-Lemma regs_add_match :
+Lemma regs_lessdef_add_match :
   forall f rs am r v v',
     val_value_lessdef v v' ->
     match_assocmaps f rs am ->
-    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.add r v' am).
+    match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am).
 Proof.
   inversion 2; subst.
   constructor. intros.
   destruct (peq r0 r); subst.
   rewrite Registers.Regmap.gss.
-  unfold find_assocmap. unfold AssocMapExt.find_default.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
   rewrite AssocMap.gss. assumption.
 
   rewrite Registers.Regmap.gso; try assumption.
-  unfold find_assocmap. unfold AssocMapExt.find_default.
+  unfold find_assocmap. unfold AssocMapExt.get_default.
   rewrite AssocMap.gso; eauto.
 Qed.
+Hint Resolve regs_lessdef_add_match : htlproof.
 
 Lemma valToValue_lessdef :
   forall v v',
@@ -198,6 +202,11 @@ Section CORRECTNESS.
       exists assoc',
         HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc').
 
+  Lemma greater_than_max_func :
+    forall f st,
+      Plt (RTL.max_reg_function f) st.
+  Proof. Admitted.
+
   Theorem transl_step_correct:
     forall (S1 : RTL.state) t S2,
       RTL.step ge S1 t S2 ->
@@ -218,14 +227,14 @@ Section CORRECTNESS.
       econstructor.
 
       (* prove stval *)
-      unfold merge_assocmap. apply AssocMapExt.merge_add. simpl. apply AssocMap.gss.
+      unfold_merge. simpl. apply AssocMap.gss.
 
       (* prove match_state *)
       rewrite assumption_32bit.
       constructor; auto.
-      unfold merge_assocmap. rewrite AssocMapExt.merge_add. simpl. apply AssocMap.gss.
-      apply regs_lessdef_regs. assumption.
-      unfold state_st_wf. inversion 1. subst. apply AssocMap.gss.
+      unfold_merge. simpl. apply regs_lessdef_regs. apply greater_than_max_func.
+      assumption.
+      unfold state_st_wf. inversion 1. subst. unfold_merge. apply AssocMap.gss.
     - (* Iop *)
       econstructor.
       split.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index b9d483c..5a61a9c 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -16,8 +16,8 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import FSets.FMapPositive.
 From compcert Require RTL Op Maps Errors.
+From compcert Require Import Maps.
 From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap.
 
 Hint Resolve Maps.PTree.elements_keys_norepet : htlspec.
@@ -160,7 +160,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr
                (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip.
 Hint Constructors tr_instr : htlspec.
 
-Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PositiveMap.t stmnt)
+Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt)
           (fin rtrn st : reg) : Prop :=
   tr_code_intro :
     forall s t,
-- 
cgit