7 files changed, 478 insertions, 256 deletions

diff --git a/src/hls/Array.v b/src/hls/Array.v
index 5c7ebc7..dec1335 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -18,9 +18,11 @@
 
 Set Implicit Arguments.
 
-Require Import Lia.
-Require Import Vericertlib.
-From Coq Require Import Lists.List Datatypes.
+Require Import Coq.Init.Datatypes.
+Require Import Coq.Lists.List.
+Require Import Coq.micromega.Lia.
+
+Require Import vericert.common.Vericertlib.
 
 Import ListNotations.
 
@@ -74,7 +76,7 @@ Lemma array_set_wf {A : Type} :
 Proof.
   induction l; intros; destruct i; auto.
 
-  invert H; crush; auto.
+  invert H; crush.
 Qed.
 
 Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 474dfef..70c0454 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -16,11 +16,21 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Errors Globalenvs Integers.
-From compcert Require Import Maps AST.
-From vericert Require Import Verilog RTLPar HTL Vericertlib AssocMap ValueInt Statemonad.
-
-Import Lia.
+Require Import Coq.micromega.Lia.
+
+Require Import compcert.common.AST.
+Require compcert.common.Errors.
+Require compcert.common.Globalenvs.
+Require compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Statemonad.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.Verilog.
+Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.ValueInt.
 
 Hint Resolve AssocMap.gempty : htlh.
 Hint Resolve AssocMap.gso : htlh.
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index dc505ed..a8efa33 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -1,6 +1,6 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2020-2021 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
@@ -16,36 +16,23 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import Coqlib Maps.
-Require Import AST Integers Values Events Memory Globalenvs Smallstep.
-Require Import Op Registers.
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Events.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.verilog.Op.
 
-Definition node := positive.
+Require Import vericert.hls.RTLBlockInstr.
 
-Inductive instruction : Type :=
-| RBnop : instruction
-| RBop : operation -> list reg -> reg -> instruction
-| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction
-| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction.
+Definition bblock_body : Type := list instr.
 
-Definition bblock_body : Type := list instruction.
-
-Inductive control_flow_inst : Type :=
-| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst
-| RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst
-| RBbuiltin : external_function -> list (builtin_arg reg) ->
-              builtin_res reg -> node -> control_flow_inst
-| RBcond : condition -> list reg -> node -> node -> control_flow_inst
-| RBjumptable : reg -> list node -> control_flow_inst
-| RBreturn : option reg -> control_flow_inst
-| RBgoto : node -> control_flow_inst.
-
-Record bblock : Type := mk_bblock {
-    bb_body: bblock_body;
-    bb_exit: option control_flow_inst
-  }.
-
-Definition code : Type := PTree.t bblock.
+Definition code : Type := PTree.t (@bblock bblock_body).
 
 Record function: Type := mkfunction {
   fn_sig: signature;
@@ -65,25 +52,63 @@ Definition funsig (fd: fundef) :=
   | External ef => ef_sig ef
   end.
 
-Definition successors_instr (i : control_flow_inst) : list node :=
-  match i with
-  | RBcall sig ros args res s => s :: nil
-  | RBtailcall sig ros args => nil
-  | RBbuiltin ef args res s => s :: nil
-  | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
-  | RBjumptable arg tbl => tbl
-  | RBreturn optarg => nil
-  | RBgoto n => n :: nil
-  end.
+Inductive stackframe : Type :=
+| Stackframe:
+    forall (res: reg)            (**r where to store the result *)
+           (f: function)         (**r calling function *)
+           (sp: val)             (**r stack pointer in calling function *)
+           (pc: node)            (**r program point in calling function *)
+           (rs: regset),         (**r register state in calling function *)
+    stackframe.
 
-(* Definition genv := Genv.t fundef unit.
-Definition regset := Regmap.t val.
+Inductive state : Type :=
+| State:
+    forall (stack: list stackframe) (**r call stack *)
+           (f: function)            (**r current function *)
+           (sp: val)                (**r stack pointer *)
+           (pc: node)               (**r current program point in [c] *)
+           (rs: regset)             (**r register state *)
+           (m: mem),                (**r memory state *)
+    state
+| Callstate:
+    forall (stack: list stackframe) (**r call stack *)
+           (f: fundef)              (**r function to call *)
+           (args: list val)         (**r arguments to the call *)
+           (m: mem),                (**r memory state *)
+    state
+| Returnstate:
+    forall (stack: list stackframe) (**r call stack *)
+           (v: val)                 (**r return value for the call *)
+           (m: mem),                (**r memory state *)
+    state.
+
+Definition genv := Genv.t fundef unit.
 
-Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
-  match rl, vl with
-  | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
-  | _, _ => Regmap.init Vundef
-  end.
+Section RELSEM.
+
+  Context (ge: genv).
+
+  Definition find_function
+             (ros: reg + ident) (rs: regset) : option fundef :=
+    match ros with
+    | inl r => Genv.find_funct ge rs#r
+    | inr symb =>
+      match Genv.find_symbol ge symb with
+      | None => None
+      | Some b => Genv.find_funct_ptr ge b
+      end
+    end.
+
+  Inductive step: state -> trace -> state -> Prop :=
+  | exec_bblock:
+      forall f pc bb cfi,
+      (fn_code f)!pc = Some (mk_bblock _ bb cfi) ->
+      step_instr_list (InstrState rs m) bb (InstrState rs' m')
+      step .
+
+End RELSEM.
+
+(*
 
 Inductive stackframe : Type :=
   | Stackframe:
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
new file mode 100644
index 0000000..f9d1073
--- /dev/null
+++ b/src/hls/RTLBlockInstr.v
@@ -0,0 +1,154 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * Copyright (C) 2021 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/>.
+ *)
+
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.verilog.Op.
+
+Require Import vericert.common.Vericertlib.
+
+Local Open Scope rtl.
+
+Definition node := positive.
+
+Inductive instr : Type :=
+| RBnop : instr
+| RBop : operation -> list reg -> reg -> instr
+| RBload : memory_chunk -> addressing -> list reg -> reg -> instr
+| RBstore : memory_chunk -> addressing -> list reg -> reg -> instr.
+
+Inductive cf_instr : Type :=
+| RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
+| RBtailcall : signature -> reg + ident -> list reg -> cf_instr
+| RBbuiltin : external_function -> list (builtin_arg reg) ->
+              builtin_res reg -> node -> cf_instr
+| RBcond : condition -> list reg -> node -> node -> cf_instr
+| RBjumptable : reg -> list node -> cf_instr
+| RBreturn : option reg -> cf_instr
+| RBgoto : node -> cf_instr.
+
+Record bblock (bblock_body : Type) : Type := mk_bblock {
+    bb_body: bblock_body;
+    bb_exit: option cf_instr
+  }.
+Arguments mk_bblock [bblock_body].
+Arguments bb_body [bblock_body].
+Arguments bb_exit [bblock_body].
+
+Definition successors_instr (i : cf_instr) : list node :=
+  match i with
+  | RBcall sig ros args res s => s :: nil
+  | RBtailcall sig ros args => nil
+  | RBbuiltin ef args res s => s :: nil
+  | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | RBjumptable arg tbl => tbl
+  | RBreturn optarg => nil
+  | RBgoto n => n :: nil
+  end.
+
+Definition max_reg_instr (m: positive) (i: instr) :=
+  match i with
+  | RBnop => m
+  | RBop op args res => fold_left Pos.max args (Pos.max res m)
+  | RBload chunk addr args dst => fold_left Pos.max args (Pos.max dst m)
+  | RBstore chunk addr args src => fold_left Pos.max args (Pos.max src m)
+  end.
+
+Definition max_reg_cfi (m : positive) (i : cf_instr) :=
+  match i with
+  | RBcall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m))
+  | RBcall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m)
+  | RBtailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m)
+  | RBtailcall sig (inr id) args => fold_left Pos.max args m
+  | RBbuiltin ef args res s =>
+      fold_left Pos.max (params_of_builtin_args args)
+        (fold_left Pos.max (params_of_builtin_res res) m)
+  | RBcond cond args ifso ifnot => fold_left Pos.max args m
+  | RBjumptable arg tbl => Pos.max arg m
+  | RBreturn None => m
+  | RBreturn (Some arg) => Pos.max arg m
+  | RBgoto n => m
+  end.
+
+Definition regset := Regmap.t val.
+
+Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
+  match rl, vl with
+  | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
+  | _, _ => Regmap.init Vundef
+  end.
+
+Inductive instr_state : Type :=
+| InstrState:
+    forall (rs: regset)
+           (m: mem),
+    instr_state.
+
+Inductive cf_instr_state : Type :=
+| CfInstrState:
+    forall ()
+
+Section RELSEM.
+
+  Context (fundef: Type).
+
+  Definition genv := Genv.t fundef unit.
+
+  Context (ge: genv) (sp: val).
+
+  Inductive step_instr: instr_state -> instr -> instr_state -> Prop :=
+  | exec_RBnop:
+      forall rs m,
+      step_instr (InstrState rs m) RBnop (InstrState rs m)
+  | exec_RBop:
+      forall op v res args rs m,
+      eval_operation ge sp op rs##args m = Some v ->
+      step_instr (InstrState rs m)
+                 (RBop op args res)
+                 (InstrState (rs#res <- v) m)
+  | exec_RBload:
+      forall addr rs args a chunk m v dst,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      step_instr (InstrState rs m)
+                 (RBload chunk addr args dst)
+                 (InstrState (rs#dst <- v) m)
+  | exec_RBstore:
+      forall addr rs args a chunk m src m',
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.storev chunk m a rs#src = Some m' ->
+      step_instr (InstrState rs m)
+                 (RBstore chunk addr args src)
+                 (InstrState rs m').
+
+  Inductive step_instr_list: instr_state -> list instr -> instr_state -> Prop :=
+    | exec_RBcons:
+        forall state i state' state'' instrs,
+        step_instr state i state' ->
+        step_instr_list state' instrs state'' ->
+        step_instr_list state (i :: instrs) state''
+    | exec_RBnil:
+        forall state,
+        step_instr_list state nil state.
+
+  Inductive step_cf_instr:
+
+End RELSEM.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index cb755e5..36431ae 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -16,34 +16,21 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Coqlib Maps.
-From compcert Require Import AST Integers Values Events Memory Globalenvs Smallstep.
-From compcert Require Import Op Registers.
-
-Definition node := positive.
-
-Inductive instruction : Type :=
-| RPnop : instruction
-| RPop : operation -> list reg -> reg -> instruction
-| RPload : memory_chunk -> addressing -> list reg -> reg -> instruction
-| RPstore : memory_chunk -> addressing -> list reg -> reg -> instruction.
-
-Definition bblock_body : Type := list (list instruction).
-
-Inductive control_flow_inst : Type :=
-| RPcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst
-| RPtailcall : signature -> reg + ident -> list reg -> control_flow_inst
-| RPbuiltin : external_function -> list (builtin_arg reg) ->
-              builtin_res reg -> node -> control_flow_inst
-| RPcond : condition -> list reg -> node -> node -> control_flow_inst
-| RPjumptable : reg -> list node -> control_flow_inst
-| RPreturn : option reg -> control_flow_inst
-| RPgoto : node -> control_flow_inst.
-
-Record bblock : Type := mk_bblock {
-    bb_body: bblock_body;
-    bb_exit: option control_flow_inst
-  }.
+Require Import compcert.backend.Registers.
+Require Import compcert.common.AST.
+Require Import compcert.common.Events.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.verilog.Op.
+
+Require Import vericert.hls.RTLBlockInstr.
+
+Definition bblock := RTLBlockInstr.bblock (list (list instr)).
 
 Definition code : Type := PTree.t bblock.
 
@@ -65,41 +52,6 @@ Definition funsig (fd: fundef) :=
   | External ef => ef_sig ef
   end.
 
-Definition successors_instr (i : control_flow_inst) : list node :=
-  match i with
-  | RPcall sig ros args res s => s :: nil
-  | RPtailcall sig ros args => nil
-  | RPbuiltin ef args res s => s :: nil
-  | RPcond cond args ifso ifnot => ifso :: ifnot :: nil
-  | RPjumptable arg tbl => tbl
-  | RPreturn optarg => nil
-  | RPgoto n => n :: nil
-  end.
-
-Definition max_reg_instr (m: positive) (i: instruction) :=
-  match i with
-  | RPnop => m
-  | RPop op args res => fold_left Pos.max args (Pos.max res m)
-  | RPload chunk addr args dst => fold_left Pos.max args (Pos.max dst m)
-  | RPstore chunk addr args src => fold_left Pos.max args (Pos.max src m)
-  end.
-
-Definition max_reg_cfi (m : positive) (i : control_flow_inst) :=
-  match i with
-  | RPcall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m))
-  | RPcall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m)
-  | RPtailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m)
-  | RPtailcall sig (inr id) args => fold_left Pos.max args m
-  | RPbuiltin ef args res s =>
-      fold_left Pos.max (params_of_builtin_args args)
-        (fold_left Pos.max (params_of_builtin_res res) m)
-  | RPcond cond args ifso ifnot => fold_left Pos.max args m
-  | RPjumptable arg tbl => Pos.max arg m
-  | RPreturn None => m
-  | RPreturn (Some arg) => Pos.max arg m
-  | RPgoto n => m
-  end.
-
 Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
   let max_body := fold_left (fun x l => fold_left max_reg_instr l x) bb.(bb_body) m in
   match bb.(bb_exit) with
@@ -118,7 +70,24 @@ Definition max_pc_function (f: function) : positive :=
                                            with Z.pos p => p | _ => 1 end))%positive)
              f.(fn_code) 1%positive.
 
-(*Inductive state : Type :=
+Definition genv := Genv.t fundef unit.
+
+Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
+  match rl, vl with
+  | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
+  | _, _ => Regmap.init Vundef
+  end.
+
+Inductive stackframe : Type :=
+  | Stackframe:
+      forall (res: reg)            (**r where to store the result *)
+             (f: function)         (**r calling function *)
+             (sp: val)             (**r stack pointer in calling function *)
+             (pc: node)            (**r program point in calling function *)
+             (rs: regset),         (**r register state in calling function *)
+      stackframe.
+
+Inductive state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
              (f: function)            (**r current function *)
@@ -138,4 +107,108 @@ Definition max_pc_function (f: function) : positive :=
              (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
-*)
+
+Section RELSEM.
+
+  Context (ge : genv).
+
+  Definition find_function
+             (ros: reg + ident) (rs: regset) : option fundef :=
+    match ros with
+    | inl r => Genv.find_funct ge rs#r
+    | inr symb =>
+      match Genv.find_symbol ge symb with
+      | None => None
+      | Some b => Genv.find_funct_ptr ge b
+      end
+    end.
+
+  Inductive step_instruction : state -> trace -> state -> Prop :=
+  | exec_Inop:
+      forall s f sp pc rs m pc',
+        (fn_code f)!pc = Some(RPnop pc') ->
+        step (State s f sp pc rs m)
+             E0 (State s f sp pc' rs m)
+  | exec_Iop:
+      forall s f sp pc rs m op args res pc' v,
+        (fn_code f)!pc = Some(Iop op args res pc') ->
+        eval_operation ge sp op rs##args m = Some v ->
+        step (State s f sp pc rs m)
+             E0 (State s f sp pc' (rs#res <- v) m)
+  | exec_Iload:
+      forall s f sp pc rs m chunk addr args dst pc' a v,
+        (fn_code f)!pc = Some(Iload chunk addr args dst pc') ->
+        eval_addressing ge sp addr rs##args = Some a ->
+        Mem.loadv chunk m a = Some v ->
+        step (State s f sp pc rs m)
+             E0 (State s f sp pc' (rs#dst <- v) m)
+  | exec_Istore:
+      forall s f sp pc rs m chunk addr args src pc' a m',
+        (fn_code f)!pc = Some(Istore chunk addr args src pc') ->
+        eval_addressing ge sp addr rs##args = Some a ->
+        Mem.storev chunk m a rs#src = Some m' ->
+        step (State s f sp pc rs m)
+             E0 (State s f sp pc' rs m')
+  | exec_Icall:
+      forall s f sp pc rs m sig ros args res pc' fd,
+        (fn_code f)!pc = Some(Icall sig ros args res pc') ->
+        find_function ros rs = Some fd ->
+        funsig fd = sig ->
+        step (State s f sp pc rs m)
+             E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
+  | exec_Itailcall:
+      forall s f stk pc rs m sig ros args fd m',
+        (fn_code f)!pc = Some(Itailcall sig ros args) ->
+        find_function ros rs = Some fd ->
+        funsig fd = sig ->
+        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+        step (State s f (Vptr stk Ptrofs.zero) pc rs m)
+             E0 (Callstate s fd rs##args m')
+  | exec_Ibuiltin:
+      forall s f sp pc rs m ef args res pc' vargs t vres m',
+        (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
+        eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
+        external_call ef ge vargs m t vres m' ->
+        step (State s f sp pc rs m)
+             t (State s f sp pc' (regmap_setres res vres rs) m')
+  | exec_Icond:
+      forall s f sp pc rs m cond args ifso ifnot b pc',
+        (fn_code f)!pc = Some(Icond cond args ifso ifnot) ->
+        eval_condition cond rs##args m = Some b ->
+        pc' = (if b then ifso else ifnot) ->
+        step (State s f sp pc rs m)
+             E0 (State s f sp pc' rs m)
+  | exec_Ijumptable:
+      forall s f sp pc rs m arg tbl n pc',
+        (fn_code f)!pc = Some(Ijumptable arg tbl) ->
+        rs#arg = Vint n ->
+        list_nth_z tbl (Int.unsigned n) = Some pc' ->
+        step (State s f sp pc rs m)
+             E0 (State s f sp pc' rs m)
+  | exec_Ireturn:
+      forall s f stk pc rs m or m',
+        (fn_code f)!pc = Some(Ireturn or) ->
+        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+        step (State s f (Vptr stk Ptrofs.zero) pc rs m)
+             E0 (Returnstate s (regmap_optget or Vundef rs) m')
+  | exec_function_internal:
+      forall s f args m m' stk,
+        Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
+        step (Callstate s (Internal f) args m)
+             E0 (State s
+                       f
+                       (Vptr stk Ptrofs.zero)
+                       f.(fn_entrypoint)
+                           (init_regs args f.(fn_params))
+                           m')
+  | exec_function_external:
+      forall s ef args res t m m',
+        external_call ef ge args m t res m' ->
+        step (Callstate s (External ef) args m)
+             t (Returnstate s res m')
+  | exec_return:
+      forall res f sp pc rs s vres m,
+        step (Returnstate (Stackframe res f sp pc rs :: s) vres m)
+             E0 (State s f sp pc (rs#res <- vres) m).
+
+End RELSEM.
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 836ceac..55bf71c 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -16,56 +16,19 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import AST Maps.
-From vericert Require Import Vericertlib RTLBlock RTLPar Scheduleoracle.
+Require Import compcert.common.AST.
+Require Import compcert.lib.Maps.
 
-Fixpoint beq {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool :=
-  match m1, m2 with
-  | PTree.Leaf, _ => PTree.bempty m2
-  | _, PTree.Leaf => PTree.bempty m1
-  | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
-    match o1, o2 with
-    | None, None => true
-    | Some y1, Some y2 => beqA y1 y2
-    | _, _ => false
-    end
-    && beq beqA l1 l2 && beq beqA r1 r2
-  end.
-
-Lemma beq_correct:
-  forall A B beqA m1 m2,
-    @beq A B beqA m1 m2 = true <->
-    (forall (x: PTree.elt),
-        match PTree.get x m1, PTree.get x m2 with
-        | None, None => True
-        | Some y1, Some y2 => beqA y1 y2 = true
-        | _, _ => False
-        end).
-Proof.
-  induction m1; intros.
-  - simpl. rewrite PTree.bempty_correct. split; intros.
-    rewrite PTree.gleaf. rewrite H. auto.
-    generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto.
-  - destruct m2.
-    + unfold beq. rewrite PTree.bempty_correct. split; intros.
-      rewrite H. rewrite PTree.gleaf. auto.
-      generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto.
-    + simpl. split; intros.
-      * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
-        rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
-        destruct x; simpl. apply H1. apply H3.
-        destruct o; destruct o0; auto || congruence.
-      * apply andb_true_intro. split. apply andb_true_intro. split.
-        generalize (H xH); simpl. destruct o; destruct o0; tauto.
-        apply IHm1_1. intros; apply (H (xO x)).
-        apply IHm1_2. intros; apply (H (xI x)).
-Qed.
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.RTLBlock.
+Require Import vericert.hls.RTLPar.
+Require Import vericert.hls.Scheduleoracle.
 
 Parameter schedule : RTLBlock.function -> RTLPar.function.
 
 Definition transl_function (f : RTLBlock.function) : Errors.res RTLPar.function :=
   let tf := schedule f in
-  if beq schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then
+  if beq2 schedule_oracle f.(RTLBlock.fn_code) tf.(fn_code) then
     Errors.OK tf
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
diff --git a/src/hls/Scheduleoracle.v b/src/hls/Scheduleoracle.v
index b5aa86d..7c22995 100644
--- a/src/hls/Scheduleoracle.v
+++ b/src/hls/Scheduleoracle.v
@@ -20,9 +20,18 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import Globalenvs Values Integers Floats Maps.
-Require RTLBlock RTLPar Op Memory AST Registers.
-Require Import Vericertlib.
+Require compcert.backend.Registers.
+Require compcert.common.AST.
+Require Import compcert.common.Globalenvs.
+Require compcert.common.Memory.
+Require Import compcert.common.Values.
+Require Import compcert.lib.Floats.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require compcert.verilog.Op.
+Require vericert.hls.RTLBlock.
+Require vericert.hls.RTLPar.
+Require Import vericert.common.Vericertlib.
 
 (*|
 Schedule Oracle
@@ -154,9 +163,7 @@ Module R_indexed.
     end.
 
   Lemma index_inj:  forall (x y: t), index x = index y -> x = y.
-  Proof.
-    destruct x; destruct y; intro; try (simpl in H; congruence).
-  Qed.
+  Proof. destruct x; destruct y; crush. Qed.
 
   Definition eq := resource_eq.
 End R_indexed.
@@ -309,61 +316,16 @@ Scheme expression_ind2 := Induction for expression Sort Prop
 Lemma beq_expression_correct:
   forall e1 e2, beq_expression e1 e2 = true -> e1 = e2.
 Proof.
-  intro e1.
+  intro e1;
   apply expression_ind2 with
-      (P := fun (e1: expression) => forall e2, beq_expression e1 e2 = true -> e1 = e2)
-      (P0 := fun (e1: expression_list) => forall e2, beq_expression_list e1 e2 = true -> e1 = e2).
-  (* Ebase *)
-  intros r e2.
-  destruct e2; simpl; try congruence.
-  case (resource_eq r r0); congruence.
-
-  (* Eop *)
-   intros o e HR e2. destruct e2; simpl; try congruence.
-   case (operation_eq o o0); intros. generalize (HR _ H).
-   congruence. congruence.
-
-   (* Eload *)
-   intros m a e HR e3 HR3. destruct e2 ; simpl ; try congruence.
-   case (memory_chunk_eq m m0).
-   case (addressing_eq a a0).
-   caseEq (beq_expression_list e e0).
-   caseEq (beq_expression e3 e2).
-   intros.
-   generalize (HR e0 H0). generalize (HR3 e2 H). intros.
-   subst. trivial.
-   intros; discriminate.
-   intros; discriminate.
-   intros; discriminate.
-   intros; discriminate.
-
-   (* Estore *)
-   intros e3 HR2 m a e HR e4 HR4 e2.
-   destruct e2; simpl; try congruence.
-   case (memory_chunk_eq m m0). case (addressing_eq a a0).
-   (*case (beq_expression_list e e0). case (beq_expression e3 e2). *)
-   intros.
-   caseEq (beq_expression_list e e0). intro. rewrite H0 in H.
-   caseEq (beq_expression e3 e2_1). intro. rewrite H1 in H.
-   generalize (HR2 e2_1 H1). intro. generalize (HR e0 H0).
-   generalize (HR4 e2_2 H).
-   congruence.
-   intro. rewrite H1 in H. discriminate.
-   intro. rewrite H0 in H. discriminate.
-   intros; congruence.
-   intros; congruence.
-
-   (* Enil *)
-   intro e2.
-   unfold beq_expression_list.
-   case e2; intros; try congruence; trivial.
-
-   (* Econs *)
-   intros e HR1 e0 HR2 e2.
-   destruct e2; simpl; try congruence.
-   caseEq (beq_expression e e2); caseEq (beq_expression_list e0 e3); simpl; try congruence.
-   intros. clear H1. generalize (HR1 e2 H0). generalize (HR2 e3 H).
-   congruence.
+      (P := fun (e1 : expression) =>
+            forall e2, beq_expression e1 e2 = true -> e1 = e2)
+      (P0 := fun (e1 : expression_list) =>
+             forall e2, beq_expression_list e1 e2 = true -> e1 = e2); simplify;
+    repeat match goal with
+           | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:?
+           | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:?
+           end; subst; f_equal; crush.
 Qed.
 
 Definition empty : forest := Rtree.empty _.
@@ -377,67 +339,93 @@ Definition check := Rtree.beq beq_expression.
 Lemma check_correct: forall (fa fb : forest) (x : resource),
   check fa fb = true -> (forall x, fa # x = fb # x).
 Proof.
-  unfold check, get_forest.
-  intros fa fb res Hbeq x.
-  pose proof Hbeq as Hbeq2.
-  pose proof (Rtree.beq_sound beq_expression fa fb) as Hsound.
-  specialize (Hsound Hbeq2 x).
-  destruct (Rtree.get x fa) eqn:?; destruct (Rtree.get x fb) eqn:?; try contradiction.
-  apply beq_expression_correct. assumption. trivial.
+  unfold check, get_forest; intros;
+  pose proof beq_expression_correct;
+  match goal with
+    [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] =>
+    apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq
+  end;
+  repeat destruct_match; crush.
 Qed.
 
 Lemma get_empty:
   forall r, empty#r = Ebase r.
 Proof.
-  intros r. unfold get_forest.
-  destruct (Rtree.get r empty) eqn:Heq; auto.
-  rewrite Rtree.gempty in Heq. discriminate.
+  intros; unfold get_forest;
+  destruct_match; auto; [ ];
+  match goal with
+    [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H
+  end; discriminate.
+Qed.
+
+Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool :=
+  match m1, m2 with
+  | PTree.Leaf, _ => PTree.bempty m2
+  | _, PTree.Leaf => PTree.bempty m1
+  | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
+    match o1, o2 with
+    | None, None => true
+    | Some y1, Some y2 => beqA y1 y2
+    | _, _ => false
+    end
+    && beq2 beqA l1 l2 && beq2 beqA r1 r2
+  end.
+
+Lemma beq2_correct:
+  forall A B beqA m1 m2,
+    @beq2 A B beqA m1 m2 = true <->
+    (forall (x: PTree.elt),
+        match PTree.get x m1, PTree.get x m2 with
+        | None, None => True
+        | Some y1, Some y2 => beqA y1 y2 = true
+        | _, _ => False
+        end).
+Proof.
+  induction m1; intros.
+  - simpl. rewrite PTree.bempty_correct. split; intros.
+    rewrite PTree.gleaf. rewrite H. auto.
+    generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto.
+  - destruct m2.
+    + unfold beq2. rewrite PTree.bempty_correct. split; intros.
+      rewrite H. rewrite PTree.gleaf. auto.
+      generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto.
+    + simpl. split; intros.
+      * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
+        rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
+        destruct x; simpl. apply H1. apply H3.
+        destruct o; destruct o0; auto || congruence.
+      * apply andb_true_intro. split. apply andb_true_intro. split.
+        generalize (H xH); simpl. destruct o; destruct o0; tauto.
+        apply IHm1_1. intros; apply (H (xO x)).
+        apply IHm1_2. intros; apply (H (xI x)).
 Qed.
 
 Lemma map0:
   forall r,
   empty # r = Ebase r.
-Proof.
-  intros. eapply get_empty.
-Qed.
+Proof. intros; eapply get_empty. Qed.
 
 Lemma map1:
   forall w dst dst',
   dst <> dst' ->
   (empty # dst <- w) # dst' = Ebase dst'.
-Proof.
-  intros.
-  unfold get_forest.
-  rewrite Rtree.gso. eapply map0. auto.
-Qed.
+Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed.
 
 Lemma genmap1:
   forall (f : forest) w dst dst',
   dst <> dst' ->
   (f # dst <- w) # dst' = f # dst'.
-Proof.
-  intros.
-  unfold get_forest.
-  rewrite Rtree.gso. reflexivity. auto.
-Qed.
+Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed.
 
 Lemma map2:
   forall (v : expression) x rs,
   (rs # x <- v) # x = v.
-Proof.
-  intros.
-  unfold get_forest.
-  rewrite Rtree.gss. trivial.
-Qed.
+Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed.
 
 Lemma tri1:
   forall x y,
   Reg x <> Reg y -> x <> y.
-Proof.
-  intros. unfold not in *; intros.
-  rewrite H0 in H. generalize (H (refl_equal (Reg y))).
-  auto.
-Qed.
+Proof. unfold not; intros; subst; auto. Qed.
 
 (*|
 Update functions.
@@ -472,6 +460,13 @@ Definition update_par (f : forest) (i : RTLPar.instruction) : forest :=
   end.
 
 (*|
+Implementing which are necessary to show the correctness of the translation validation by showing
+that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code.
+|*)
+
+
+
+(*|
 Get a sequence from the basic block.
 |*)