Merge branch 'develop'

21 files changed, 2735 insertions, 280 deletions

diff --git a/default.nix b/default.nix
index 1121469..0e5b40d 100644
--- a/default.nix
+++ b/default.nix
@@ -1,4 +1,4 @@
-with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {};
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/1a56d76d718afb6c47dd96602c915b6d23f7c45d.tar.gz") {};
 let
   ncoq = coq_8_13;
   ncoqPackages = coqPackages_8_13;
@@ -9,7 +9,12 @@ stdenv.mkDerivation {
 
   buildInputs = [ ncoq dune_2 gcc
                   ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
-                  ncoq.ocamlPackages.ocamlgraph
+                  ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin
+
+                  ncoqPackages.serapi
+                  python3 python3Packages.docutils python3Packages.pygments
+                  python3Packages.dominate
+                  python3Packages.pelican
                 ];
 
   enableParallelBuilding = true;
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 1ea580f..a36f375 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -65,6 +65,8 @@ let compile_c_file sourcename ifile ofile =
   set_dest Vericert.PrintClight.destination option_dclight ".light.c";
   set_dest Vericert.PrintCminor.destination option_dcminor ".cm";
   set_dest Vericert.PrintRTL.destination option_drtl ".rtl";
+  set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock";
+  set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar";
   set_dest Vericert.PrintHTL.destination option_dhtl ".htl";
   set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
   set_dest Vericert.PrintLTL.destination option_dltl ".ltl";
@@ -92,7 +94,7 @@ let compile_c_file sourcename ifile ofile =
   end else begin
     let verilog =
       let translation = if !option_hls_schedule
-                        then Vericert.Compiler0.transf_hls
+                        then Vericert.Compiler0.transf_hls_temp
                         else Vericert.Compiler0.transf_hls
       in
       match translation csyntax with
@@ -390,6 +392,7 @@ let cmdline_actions =
   Exact "-dcminor", Set option_dcminor;
   Exact "-drtl", Set option_drtl;
   Exact "-drtlblock", Set option_drtlblock;
+  Exact "-drtlpar", Set option_drtlpar;
   Exact "-dhtl", Set option_dhtl;
   Exact "-dltl", Set option_dltl;
   Exact "-dalloctrace", Set option_dalloctrace;
@@ -403,6 +406,7 @@ let cmdline_actions =
     option_dcminor := true;
     option_drtl := true;
     option_drtlblock := true;
+    option_drtlpar := true;
     option_dhtl := true;
     option_dltl := true;
     option_dalloctrace := true;
diff --git a/src/Compiler.v b/src/Compiler.v
index de29889..ecea2fc 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -81,8 +81,9 @@ We then need to declare the external OCaml functions used to print out intermedi
 |*)
 
 Parameter print_RTL: Z -> RTL.program -> unit.
-Parameter print_HTL: HTL.program -> unit.
+Parameter print_HTL: Z -> HTL.program -> unit.
 Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
+Parameter print_RTLPar: Z -> RTLPar.program -> unit.
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
   let unused := printer prog in prog.
@@ -191,8 +192,9 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
   @@@ HTLgen.transl_program
-   @@ print print_HTL
+   @@ print (print_HTL 0)
    @@ total_if HLSOpts.optim_ram Memorygen.transf_program
+   @@ print (print_HTL 1)
    @@ Veriloggen.transl_program.
 
 (*|
@@ -216,7 +218,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
 
 (* This is an unverified version of transf_hls with some experimental additions such as scheduling
 that aren't completed yet. *)
-(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
+Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
   OK p
   @@@ SimplExpr.transl_program
   @@@ SimplLocals.transf_program
@@ -239,13 +241,14 @@ that aren't completed yet. *)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 7)
   @@@ RTLBlockgen.transl_program
-   @@ print (print_RTLBlock 1)
+   @@ print (print_RTLBlock 0)
    @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program
-   @@ print (print_RTLBlock 2)
+   @@ print (print_RTLBlock 1)
   @@@ RTLPargen.transl_program
+   @@ print (print_RTLPar 0)
   @@@ HTLPargen.transl_program
-   @@ print print_HTL
-   @@ Veriloggen.transl_program.*)
+   @@ print (print_HTL 0)
+   @@ Veriloggen.transl_program.
 
 (*|
 Correctness Proof
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 977ca00..ab3c949 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -5,6 +5,7 @@ let option_debug_hls = ref false
 let option_initial = ref false
 let option_dhtl = ref false
 let option_drtlblock = ref false
+let option_drtlpar = ref false
 let option_hls_schedule = ref false
 let option_fif_conv = ref false
 let option_fram = ref true
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 6abe4e0..97f0d2a 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -144,6 +144,7 @@ Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_if".
 Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if".
 Extract Constant Compiler.print_HTL => "PrintHTL.print_if".
+Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if".
 Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
@@ -179,7 +180,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
 Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline".
 Extract Constant RTLBlockgen.partition => "Partition.partition".
-(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*)
+Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".
 
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
@@ -187,11 +188,11 @@ Set Extraction AccessOpaque.
 Cd "src/extraction".
 Separate Extraction
          Verilog.module vericert.Compiler.transf_hls
-(*         vericert.Compiler.transf_hls_temp*)
-(*         RTLBlockgen.transl_program RTLBlockInstr.successors_instr*)
+         vericert.Compiler.transf_hls_temp
+         RTLBlockgen.transl_program RTLBlockInstr.successors_instr
          HTLgen.tbl_to_case_expr
          Pipeline.pipeline
-(*         RTLBlockInstr.sat_pred_temp*)
+         RTLBlockInstr.sat_pred_simple
          Verilog.stmnt_to_list
 
    Compiler.transf_c_program Compiler.transf_cminor_program
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 9e1f156..9746f92 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -641,9 +641,9 @@ Definition add_control_instr_force_state_incr :
        s.(st_arrdecls)
        s.(st_datapath)
        (AssocMap.set n st s.(st_controllogic))).
-Abort.
+Admitted.
 
-(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
+Definition add_control_instr_force (n : node) (st : stmnt) : mon unit :=
   fun s =>
     OK tt (mkstate
       s.(st_st)
@@ -659,7 +659,7 @@ Abort.
 Fixpoint pred_expr (preg: reg) (p: pred_op) :=
   match p with
   | Pvar pred =>
-    Vrange preg (Vlit (natToValue pred)) (Vlit (natToValue pred))
+    Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred))
   | Pnot pred =>
     Vunop Vnot (pred_expr preg pred)
   | Pand p1 p2 =>
@@ -708,7 +708,7 @@ Lemma create_new_state_state_incr:
        s.(st_arrdecls)
        s.(st_datapath)
        s.(st_controllogic)).
-Abort.
+Admitted.
 
 Definition create_new_state (p: node): mon node :=
   fun s => OK s.(st_freshstate)
@@ -876,4 +876,3 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program :
   if main_is_internal p
   then transform_partial_program transl_fundef p
   else Errors.Error (Errors.msg "Main function is not Internal.").
-*)
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 39d9fd2..f8d404c 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -106,7 +106,7 @@ Definition find_blocks_with_cond (c: code) : list (node * bblock) :=
 Definition if_convert_code (p: nat * code) (nb: node * bblock) :=
   let (n, bb) := nb in
   let (p', c) := p in
-  let nbb := if_convert_block c p' bb in
+  let nbb := if_convert_block c (Pos.of_nat p') bb in
   (S p', PTree.set n nbb c).
 
 Definition transf_function (f: function) : function :=
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
new file mode 100644
index 0000000..19c6048
--- /dev/null
+++ b/src/hls/Partition.ml
@@ -0,0 +1,124 @@
+ (*
+ * Vericert: 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/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlockInstr
+open RTLBlock
+
+(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
+   [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
+let find_edge i n =
+  let succ = RTL.successors_instr i in
+  let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in
+  ((match filt with [] -> [] | _ -> [n]), filt)
+
+let find_edges c =
+  PTree.fold (fun l n i ->
+      let f = find_edge i n in
+      (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], [])
+
+let prepend_instr i = function
+  | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
+
+let translate_inst = function
+  | RTL.Inop _ -> Some RBnop
+  | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst))
+  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst))
+  | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src))
+  | _ -> None
+
+let translate_cfi = function
+  | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n))
+  | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls))
+  | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n))
+  | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2))
+  | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls))
+  | RTL.Ireturn r -> Some (RBreturn r)
+  | _ -> None
+
+let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
+  let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in
+  let trans_inst = (translate_inst i, translate_cfi i) in
+  match trans_inst, succ with
+  | (None, Some i'), _ ->
+    if List.exists (fun x -> x = s) (snd e) && not is_start then
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
+    else
+      Errors.OK { bb_body = []; bb_exit = i' }
+  | (Some i', None), (s', Some i_n)::[] ->
+    if List.exists (fun x -> x = s) (fst e) then
+      Errors.OK { bb_body = [i']; bb_exit = RBgoto s' }
+    else if List.exists (fun x -> x = s) (snd e) && not is_start then
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
+    else begin
+      match next_bblock_from_RTL false e c s' i_n with
+      | Errors.OK bb ->
+        Errors.OK (prepend_instr i' bb)
+      | Errors.Error msg -> Errors.Error msg
+    end
+  | _, _ ->
+    Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
+
+let rec traverseacc f l c =
+  match l with
+  | [] -> Errors.OK c
+  | x::xs ->
+    match f x c with
+    | Errors.Error msg -> Errors.Error msg
+    | Errors.OK x' ->
+      match traverseacc f xs x' with
+      | Errors.Error msg -> Errors.Error msg
+      | Errors.OK xs' -> Errors.OK xs'
+
+let rec translate_all edge c s res =
+  let c_bb, translated = res in
+  if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else
+    (match PTree.get s c with
+     | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all."))
+     | Some i ->
+       match next_bblock_from_RTL true edge c s i with
+       | Errors.Error msg -> Errors.Error msg
+       | Errors.OK {bb_body = bb; bb_exit = e} ->
+         let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in
+         (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with
+          | Errors.Error msg -> Errors.Error msg
+          | Errors.OK (c', t') ->
+            Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t')))
+
+(* Partition a function and transform it into RTLBlock. *)
+let function_from_RTL f =
+  let e = find_edges f.RTL.fn_code in
+  match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with
+  | Errors.Error msg -> Errors.Error msg
+  | Errors.OK (c, _) ->
+    Errors.OK { fn_sig = f.RTL.fn_sig;
+                fn_stacksize = f.RTL.fn_stacksize;
+                fn_params = f.RTL.fn_params;
+                fn_entrypoint = f.RTL.fn_entrypoint;
+                fn_code = c
+              }
+
+let partition = function_from_RTL
diff --git a/src/hls/PrintExpression.ml b/src/hls/PrintExpression.ml
new file mode 100644
index 0000000..cfe6750
--- /dev/null
+++ b/src/hls/PrintExpression.ml
@@ -0,0 +1,40 @@
+(*open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open PrintAST
+open RTLPargen
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let pred pp r =
+  fprintf pp "p%d" (P.to_int r)
+
+let print_resource pp = function
+  | Reg r -> reg pp r
+  | Pred r -> pred pp r
+  | Mem -> fprintf pp "M"
+
+let rec to_expr_list = function
+  | Enil -> []
+  | Econs (e, elist) -> e :: to_expr_list elist
+
+let rec print_expression pp = function
+  | Ebase r -> print_resource pp r
+  | Eop (op, elist, e) ->
+    PrintOp.print_operation print_expression pp (op, to_expr_list elist);
+    Printf.printf "; ";
+    print_expression pp e
+  | Eload (chunk, addr, elist, e) ->
+    fprintf pp "%s[%a]; " (name_of_chunk chunk) (PrintOp.print_addressing print_expression) (addr, to_expr_list elist);
+    print_expression pp e
+  | Estore (e, chunk, addr, elist, e') ->
+    fprintf pp "%s[%a] = %a; " (name_of_chunk chunk)
+      (PrintOp.print_addressing print_expression) (addr, to_expr_list elist)
+      print_expression e;
+    print_expression pp e
+  | Esetpred (p, cond, elist, e) ->
+    fprintf pp "%a = %a; " pred p (PrintOp.print_condition print_expression) (cond, to_expr_list elist);
+    print_expression pp e
+*)
diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml
index a75d0ee..5963be0 100644
--- a/src/hls/PrintHTL.ml
+++ b/src/hls/PrintHTL.ml
@@ -71,10 +71,10 @@ let print_program pp prog =
 
 let destination : string option ref = ref None
 
-let print_if prog =
+let print_if passno prog =
   match !destination with
   | None -> ()
   | Some f ->
-    let oc = open_out f in
+    let oc = open_out (f ^ "." ^ Z.to_string passno) in
     print_program oc prog;
     close_out oc
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
new file mode 100644
index 0000000..8fef401
--- /dev/null
+++ b/src/hls/PrintRTLBlock.ml
@@ -0,0 +1,72 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open RTLBlock
+open PrintAST
+open PrintRTLBlockInstr
+
+(* Printing of RTL code *)
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_bblock pp (pc, i) =
+  fprintf pp "%5d:{\n" pc;
+  List.iter (print_bblock_body pp) i.bb_body;
+  print_bblock_exit pp i.bb_exit;
+  fprintf pp "\t}\n\n"
+
+let print_function pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+  let instrs =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.fn_code)) in
+  List.iter (print_bblock pp) instrs;
+  fprintf pp "}\n\n"
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
+
+let print_program pp (prog: program) =
+  List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if passno prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+     let oc = open_out (f ^ "." ^ Z.to_string passno) in
+     print_program oc prog;
+     close_out oc
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
new file mode 100644
index 0000000..979ca38
--- /dev/null
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -0,0 +1,87 @@
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open PrintAST
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let pred pp r =
+  fprintf pp "p%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let rec print_pred_op pp = function
+  | Pvar p -> pred pp p
+  | Pnot p -> fprintf pp "(~ %a)" print_pred_op p
+  | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2
+  | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2
+
+let print_pred_option pp = function
+  | Some x -> fprintf pp "(%a)" print_pred_op x
+  | None -> ()
+
+let print_bblock_body pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBnop -> fprintf pp "nop\n"
+  | RBop(p, op, ls, dst) ->
+     fprintf pp "%a %a = %a\n"
+       print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(p, chunk, addr, args, dst) ->
+     fprintf pp "%a %a = %s[%a]\n"
+       print_pred_option p reg dst (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+  | RBstore(p, chunk, addr, args, src) ->
+     fprintf pp "%a %s[%a] = %a\n"
+       print_pred_option p
+       (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+       reg src
+  | RBsetpred (c, args, p) ->
+    fprintf pp "%a = %a\n"
+      pred p
+      (PrintOp.print_condition reg) (c, args)
+
+let rec print_bblock_exit pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBcall(_, fn, args, res, _) ->
+      fprintf pp "%a = %a(%a)\n"
+        reg res ros fn regs args;
+  | RBtailcall(_, fn, args) ->
+      fprintf pp "tailcall %a(%a)\n"
+        ros fn regs args
+  | RBbuiltin(ef, args, res, _) ->
+      fprintf pp "%a = %s(%a)\n"
+        (print_builtin_res reg) res
+        (name_of_external ef)
+        (print_builtin_args reg) args
+  | RBcond(cond, args, s1, s2) ->
+      fprintf pp "if (%a) goto %d else goto %d\n"
+        (PrintOp.print_condition reg) (cond, args)
+        (P.to_int s1) (P.to_int s2)
+  | RBjumptable(arg, tbl) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "jumptable (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | RBreturn None ->
+      fprintf pp "return\n"
+  | RBreturn (Some arg) ->
+      fprintf pp "return %a\n" reg arg
+  | RBgoto n ->
+     fprintf pp "goto %d\n" (P.to_int n)
+  | RBpred_cf (p, c1, c2) ->
+    fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2
diff --git a/src/hls/PrintRTLPar.ml b/src/hls/PrintRTLPar.ml
new file mode 100644
index 0000000..ab93fa5
--- /dev/null
+++ b/src/hls/PrintRTLPar.ml
@@ -0,0 +1,74 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open RTLPar
+open PrintAST
+open PrintRTLBlockInstr
+
+(* Printing of RTL code *)
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_bblock pp (pc, i) =
+  fprintf pp "%5d:{\n" pc;
+  List.iter (fun x -> fprintf pp "{\n";
+              List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x;
+              fprintf pp "}\n") i.bb_body;
+  print_bblock_exit pp i.bb_exit;
+  fprintf pp "\t}\n\n"
+
+let print_function pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+  let instrs =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.fn_code)) in
+  List.iter (print_bblock pp) instrs;
+  fprintf pp "}\n\n"
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
+
+let print_program pp (prog: program) =
+  List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if passno prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+     let oc = open_out (f ^ "." ^ Z.to_string passno) in
+     print_program oc prog;
+     close_out oc
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 6a3487a..bf5c37a 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -58,11 +58,11 @@ Section RELSEM.
 
   Inductive step: state -> trace -> state -> Prop :=
   | exec_bblock:
-    forall s f sp pc rs rs' m m' t s' bb,
+    forall s f sp pc rs rs' m m' t s' bb pr pr',
       f.(fn_code)!pc = Some bb ->
-      step_instr_list sp (InstrState rs m) bb.(bb_body) (InstrState rs' m') ->
-      step_cf_instr ge (State s f sp pc rs' m') bb.(bb_exit) t s' ->
-      step (State s f sp pc rs m) t s'
+      step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+      step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
+      step (State s f sp pc rs pr m) t s'
   | exec_function_internal:
     forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -72,6 +72,7 @@ Section RELSEM.
                   (Vptr stk Ptrofs.zero)
                   f.(fn_entrypoint)
                   (init_regs args f.(fn_params))
+                  (PMap.init false)
                   m')
   | exec_function_external:
     forall s ef args res t m m',
@@ -79,9 +80,9 @@ Section RELSEM.
       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).
+    forall res f sp pc rs s vres m pr,
+      step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
+        E0 (State s f sp pc (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 3fab464..8d3fde4 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -34,7 +34,7 @@ Require Import vericert.hls.Sat.
 Local Open Scope rtl.
 
 Definition node := positive.
-Definition predicate := nat.
+Definition predicate := positive.
 
 Inductive pred_op : Type :=
 | Pvar: predicate -> pred_op
@@ -44,7 +44,7 @@ Inductive pred_op : Type :=
 
 Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool :=
   match p with
-  | Pvar p' => a p'
+  | Pvar p' => a (Pos.to_nat p')
   | Pnot p' => negb (sat_predicate p' a)
   | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a
   | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a
@@ -152,7 +152,7 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula :=
   | O => None
   | S n =>
     match p with
-    | Pvar p' => Some (((true, p') :: nil) :: nil)
+    | Pvar p' => Some (((true, Pos.to_nat p') :: nil) :: nil)
     | Pand p1 p2 =>
       match trans_pred_temp n p1, trans_pred_temp n p2 with
       | Some p1', Some p2' =>
@@ -165,7 +165,7 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula :=
         Some (mult p1' p2')
       | _, _ => None
       end
-    | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil)
+    | Pnot (Pvar p') => Some (((false, Pos.to_nat p') :: nil) :: nil)
     | Pnot (Pnot p) => trans_pred_temp n p
     | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2))
     | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2))
@@ -180,7 +180,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
    | O => None
    | S n =>
      match p with
-     | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _)
+     | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _)
      | Pand p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
       | Some (exist _ p1' _), Some (exist _ p2' _) =>
@@ -193,7 +193,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
         Some (exist _ (mult p1' p2') _)
       | _, _ => None
       end
-     | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _)
+     | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _)
      | Pnot (Pnot p') =>
        match trans_pred n p' with
        | Some (exist _ p1' _) => Some (exist _ p1' _)
@@ -212,7 +212,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
      end
    end); split; intros; simpl in *; auto.
   - inv H. inv H0; auto.
-  - split; auto. destruct (a p') eqn:?; crush.
+  - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush.
   - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto.
     crush.
   - rewrite negb_involutive in H. apply i in H. auto.
@@ -232,7 +232,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
   - apply orb_true_intro.
     apply satFormula_mult2 in H. inv H. apply i in H0. auto.
     apply i0 in H0. auto.
-Qed.
+Defined.
 
 Definition sat_pred (bound: nat) (p: pred_op) :
   option ({al : alist | sat_predicate p (interp_alist al) = true}
@@ -251,7 +251,7 @@ Definition sat_pred (bound: nat) (p: pred_op) :
   - intros. specialize (n a). specialize (i a).
     destruct (sat_predicate p a). exfalso.
     apply n. apply i. auto. auto.
-Qed.
+Defined.
 
 Definition sat_pred_simple (bound: nat) (p: pred_op) :=
   match sat_pred bound p with
@@ -331,6 +331,15 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
   end.
 
 Definition regset := Regmap.t val.
+Definition predset := PMap.t bool.
+
+Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} :=
+  match p with
+  | Pvar p' => PMap.get p' pr
+  | Pnot p' => negb (eval_predf pr p')
+  | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'')
+  | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'')
+  end.
 
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   match rl, vl with
@@ -338,11 +347,11 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   | _, _ => Regmap.init Vundef
   end.
 
-Inductive instr_state : Type :=
-| InstrState:
-    forall (rs: regset)
-           (m: mem),
-    instr_state.
+Record instr_state := mk_instr_state {
+  instr_st_regset: regset;
+  instr_st_predset: predset;
+  instr_st_mem: mem;
+}.
 
 Section DEFINITION.
 
@@ -379,7 +388,8 @@ Section DEFINITION.
              (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 *)
+             (rs: regset)          (**r register state in calling function *)
+             (pr: predset),        (**r predicate state of the calling function *)
       stackframe.
 
   Inductive state : Type :=
@@ -389,6 +399,7 @@ Section DEFINITION.
              (sp: val)                (**r stack pointer *)
              (pc: node)               (**r current program point in [c] *)
              (rs: regset)             (**r register state *)
+             (pr: predset)            (**r predicate register state *)
              (m: mem),                (**r memory state *)
       state
   | Callstate:
@@ -424,67 +435,89 @@ Section RELSEM.
       end
     end.
 
+  Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+  | eval_pred_true:
+      forall (pr: predset) p rs pr m i,
+      eval_predf pr p = true ->
+      eval_pred (Some p) (mk_instr_state rs pr m) i i
+  | eval_pred_false:
+      forall (pr: predset) p rs pr m i,
+      eval_predf pr p = false ->
+      eval_pred (Some p) (mk_instr_state rs pr m) i (mk_instr_state rs pr m)
+  | eval_pred_none:
+      forall i i',
+      eval_pred None i i' i.
+
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
-      forall rs m sp,
-      step_instr sp (InstrState rs m) RBnop (InstrState rs m)
+      forall sp ist,
+        step_instr sp ist RBnop ist
   | exec_RBop:
-      forall op v res args rs m sp p,
-      eval_operation ge sp op rs##args m = Some v ->
-      step_instr sp (InstrState rs m)
-                 (RBop p op args res)
-                 (InstrState (rs#res <- v) m)
+      forall op v res args rs m sp p ist pr,
+        eval_operation ge sp op rs##args m = Some v ->
+        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
+        step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist
   | exec_RBload:
-      forall addr rs args a chunk m v dst sp p,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
-      step_instr sp (InstrState rs m)
-                 (RBload p chunk addr args dst)
-                 (InstrState (rs#dst <- v) m)
+      forall addr rs args a chunk m v dst sp p pr ist,
+        eval_addressing ge sp addr rs##args = Some a ->
+        Mem.loadv chunk m a = Some v ->
+        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
+        step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist
   | exec_RBstore:
-      forall addr rs args a chunk m src m' sp p,
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.storev chunk m a rs#src = Some m' ->
-      step_instr sp (InstrState rs m)
-                 (RBstore p chunk addr args src)
-                 (InstrState rs m').
+      forall addr rs args a chunk m src m' sp p pr ist,
+        eval_addressing ge sp addr rs##args = Some a ->
+        Mem.storev chunk m a rs#src = Some m' ->
+        eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
+        step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist
+  | exec_RBsetpred:
+      forall sp rs pr m p c b args,
+      Op.eval_condition c rs##args m = Some b ->
+      step_instr sp (mk_instr_state rs pr m) (RBsetpred c args p)
+                 (mk_instr_state rs (PMap.set p b pr) m).
 
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
-    forall s f sp rs m res fd ros sig args pc pc',
+    forall s f sp rs m res fd ros sig args pc pc' pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
-      step_cf_instr (State s f sp pc rs m) (RBcall sig ros args res pc')
-           E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m)
+      step_cf_instr (State s f sp pc rs pr m) (RBcall sig ros args res pc')
+           E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
   | exec_RBtailcall:
-      forall s f stk rs m sig ros args fd m' pc,
+      forall s f stk rs m sig ros args fd m' pc pr,
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBtailcall sig ros args)
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args)
         E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
-      forall s f sp rs m ef args res pc' vargs t vres m' pc,
+      forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
       external_call ef ge vargs m t vres m' ->
-      step_cf_instr (State s f sp pc rs m) (RBbuiltin ef args res pc')
-         t (State s f sp pc' (regmap_setres res vres rs) m')
+      step_cf_instr (State s f sp pc rs pr m) (RBbuiltin ef args res pc')
+         t (State s f sp pc' (regmap_setres res vres rs) pr m')
   | exec_RBcond:
-      forall s f sp rs m cond args ifso ifnot b pc pc',
+      forall s f sp rs m cond args ifso ifnot b pc pc' pr,
       eval_condition cond rs##args m = Some b ->
       pc' = (if b then ifso else ifnot) ->
-      step_cf_instr (State s f sp pc rs m) (RBcond cond args ifso ifnot)
-        E0 (State s f sp pc' rs m)
+      step_cf_instr (State s f sp pc rs pr m) (RBcond cond args ifso ifnot)
+        E0 (State s f sp pc' rs pr m)
   | exec_RBjumptable:
-      forall s f sp rs m arg tbl n pc pc',
+      forall s f sp rs m arg tbl n pc pc' pr,
       rs#arg = Vint n ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      step_cf_instr (State s f sp pc rs m) (RBjumptable arg tbl)
-        E0 (State s f sp pc' rs m)
-  | exec_Ireturn:
-      forall s f stk rs m or pc m',
+      step_cf_instr (State s f sp pc rs pr m) (RBjumptable arg tbl)
+        E0 (State s f sp pc' rs pr m)
+  | exec_RBreturn:
+      forall s f stk rs m or pc m' pr,
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBreturn or)
-        E0 (Returnstate s (regmap_optget or Vundef rs) m').
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or)
+        E0 (Returnstate s (regmap_optget or Vundef rs) m')
+  | exec_RBgoto:
+      forall s f sp pc rs pr m pc',
+      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m)
+  | exec_RBpred_cf:
+      forall s f sp pc rs pr m cf1 cf2 st' p t,
+      step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
+      step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'.
 
 End RELSEM.
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 2e78d36..4986cff 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -80,11 +80,11 @@ Section RELSEM.
 
   Inductive step: state -> trace -> state -> Prop :=
   | exec_bblock:
-    forall s f sp pc rs rs' m m' t s' bb,
+    forall s f sp pc rs rs' m m' t s' bb pr pr',
       f.(fn_code)!pc = Some bb ->
-      step_instr_block sp (InstrState rs m) bb.(bb_body) (InstrState rs' m') ->
-      step_cf_instr ge (State s f sp pc rs' m') bb.(bb_exit) t s' ->
-      step (State s f sp pc rs m) t s'
+      step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+      step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' ->
+      step (State s f sp pc rs pr m) t s'
   | exec_function_internal:
     forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -94,6 +94,7 @@ Section RELSEM.
                   (Vptr stk Ptrofs.zero)
                   f.(fn_entrypoint)
                   (init_regs args f.(fn_params))
+                  (PMap.init false)
                   m')
   | exec_function_external:
     forall s ef args res t m m',
@@ -101,9 +102,9 @@ Section RELSEM.
       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).
+    forall res f sp pc rs s vres m pr,
+      step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
+        E0 (State s f sp pc (rs#res <- vres) pr m).
 
 End RELSEM.
 
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 5ad3f90..2f24a42 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -19,7 +19,7 @@
 Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Globalenvs.
-Require compcert.common.Memory.
+Require Import compcert.common.Memory.
 Require Import compcert.common.Values.
 Require Import compcert.lib.Floats.
 Require Import compcert.lib.Integers.
@@ -31,6 +31,9 @@ Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLPar.
 Require Import vericert.hls.RTLBlockInstr.
 
+#[local]
+Open Scope positive.
+
 (*|
 Schedule Oracle
 ===============
@@ -44,6 +47,7 @@ Definition reg := positive.
 
 Inductive resource : Set :=
 | Reg : reg -> resource
+| Pred : reg -> resource
 | Mem : resource.
 
 (*|
@@ -53,7 +57,7 @@ optimised heavily if written manually, as their proofs are not needed.
 
 Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}.
 Proof.
-  decide equality. apply Pos.eq_dec.
+  decide equality; apply Pos.eq_dec.
 Defined.
 
 Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
@@ -181,7 +185,8 @@ Module R_indexed.
   Definition t := resource.
   Definition index (rs: resource) : positive :=
     match rs with
-    | Reg r => xO r
+    | Reg r => xO (xO r)
+    | Pred r => xI (xI r)
     | Mem => 1%positive
     end.
 
@@ -205,14 +210,230 @@ Then, to make recursion over expressions easier, expression_list is also defined
 that enables mutual recursive definitions over the datatypes.
 |*)
 
-Inductive expression : Set :=
+Definition unsat p := forall a, sat_predicate p a = false.
+Definition sat p := exists a, sat_predicate p a = true.
+
+Inductive expression : Type :=
 | Ebase : resource -> expression
-| Eop : Op.operation -> expression_list -> expression
+| Eop : Op.operation -> expression_list -> expression -> expression
 | Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression
 | Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression
-with expression_list : Set :=
+| Esetpred : Op.condition -> expression_list -> expression -> expression
+with expression_list : Type :=
 | Enil : expression_list
-| Econs : expression -> expression_list -> expression_list.
+| Econs : expression -> expression_list -> expression_list
+.
+
+(*Inductive pred_expr : Type :=
+| PEsingleton : option pred_op -> expression -> pred_expr
+| PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*)
+
+Module NonEmpty.
+
+Inductive non_empty (A: Type) :=
+| singleton : A -> non_empty A
+| cons : A -> non_empty A -> non_empty A
+.
+
+Arguments singleton [A].
+Arguments cons [A].
+
+Declare Scope non_empty_scope.
+Delimit Scope non_empty_scope with non_empty.
+
+Module NonEmptyNotation.
+Infix "::|" := cons (at level 60, right associativity) : non_empty_scope.
+End NonEmptyNotation.
+Import NonEmptyNotation.
+
+#[local] Open Scope non_empty_scope.
+
+Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B :=
+  match l with
+  | singleton a => singleton (f a)
+  | a ::| b => f a ::| map f b
+  end.
+
+Fixpoint to_list {A} (l: non_empty A): list A :=
+  match l with
+  | singleton a => a::nil
+  | a ::| b => a :: to_list b
+  end.
+
+Fixpoint app {A} (l1 l2: non_empty A) :=
+  match l1 with
+  | singleton a => a ::| l2
+  | a ::| b => a ::| app b l2
+  end.
+
+Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) :=
+  match l with
+  | singleton a => map (fun x => (a, x)) l'
+  | a ::| b => app (map (fun x => (a, x)) l') (non_empty_prod b l')
+  end.
+
+Fixpoint of_list {A} (l: list A): option (non_empty A) :=
+  match l with
+  | a::b =>
+    match of_list b with
+    | Some b' => Some (a ::| b')
+    | _ => None
+    end
+  | nil => None
+  end.
+
+End NonEmpty.
+
+Module NE := NonEmpty.
+Import NE.NonEmptyNotation.
+
+#[local] Open Scope non_empty_scope.
+
+Definition predicated A := NE.non_empty (option pred_op * A).
+
+Definition pred_expr := predicated expression.
+
+Definition pred_list_wf l : Prop :=
+  forall a b, In (Some a) l -> In (Some b) l -> a <> b -> unsat (Pand a b).
+
+Definition pred_list_wf_ep (l: pred_expr) : Prop :=
+  pred_list_wf (NE.to_list (NE.map fst l)).
+
+Lemma unsat_correct1 :
+  forall a b c,
+    unsat (Pand a b) ->
+    sat_predicate a c = true ->
+    sat_predicate b c = false.
+Proof.
+  unfold unsat in *. intros.
+  simplify. specialize (H c).
+  apply andb_false_iff in H. inv H. rewrite H0 in H1. discriminate.
+  auto.
+Qed.
+
+Lemma unsat_correct2 :
+  forall a b c,
+    unsat (Pand a b) ->
+    sat_predicate b c = true ->
+    sat_predicate a c = false.
+Proof.
+  unfold unsat in *. intros.
+  simplify. specialize (H c).
+  apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate.
+Qed.
+
+Lemma unsat_not a: unsat (Pand a (Pnot a)).
+Proof. unfold unsat; simplify; auto with bool. Qed.
+
+Lemma unsat_commut a b: unsat (Pand a b) -> unsat (Pand b a).
+Proof. unfold unsat; simplify; eauto with bool. Qed.
+
+Lemma sat_dec a n b: sat_pred n a = Some b -> {sat a} + {unsat a}.
+Proof.
+  unfold sat, unsat. destruct b.
+  intros. left. destruct s.
+  exists (Sat.interp_alist x). auto.
+  intros. tauto.
+Qed.
+
+Lemma sat_equiv :
+  forall a b,
+  unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) ->
+  forall c, sat_predicate a c = sat_predicate b c.
+Proof.
+  unfold unsat. intros. specialize (H c); simplify.
+  destruct (sat_predicate b c) eqn:X;
+  destruct (sat_predicate a c) eqn:X2;
+  crush.
+Qed.
+
+(*Parameter op_le : Op.operation -> Op.operation -> bool.
+Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool.
+Parameter addr_le : Op.addressing -> Op.addressing -> bool.
+Parameter cond_le : Op.condition -> Op.condition -> bool.
+
+Fixpoint pred_le (p1 p2: pred_op) : bool :=
+  match p1, p2 with
+  | Pvar i, Pvar j => (i <=? j)%positive
+  | Pnot p1, Pnot p2 => pred_le p1 p2
+  | Pand p1 p1', Pand p2 p2' => if pred_le p1 p2 then true else pred_le p1' p2'
+  | Por p1 p1', Por p2 p2' => if pred_le p1 p2 then true else pred_le p1' p2'
+  | Pvar _, _ => true
+  | Pnot _, Pvar _ => false
+  | Pnot _, _ => true
+  | Pand _ _, Pvar _ => false
+  | Pand _ _, Pnot _ => false
+  | Pand _ _, _ => true
+  | Por _ _, _ => false
+  end.
+
+Import Lia.
+
+Lemma pred_le_trans :
+  forall p1 p2 p3 b, pred_le p1 p2 = b -> pred_le p2 p3 = b -> pred_le p1 p3 = b.
+Proof.
+  induction p1; destruct p2; destruct p3; crush.
+  destruct b. rewrite Pos.leb_le in *. lia. rewrite Pos.leb_gt in *. lia.
+  firstorder.
+  destruct (pred_le p1_1 p2_1) eqn:?. subst. destruct (pred_le p2_1 p3_1) eqn:?.
+  apply IHp1_1 in Heqb. rewrite Heqb. auto. auto.
+
+
+Fixpoint expr_le (e1 e2: expression) {struct e2}: bool :=
+  match e1, e2 with
+  | Ebase r1, Ebase r2 => (R_indexed.index r1 <=? R_indexed.index r2)%positive
+  | Ebase _, _ => true
+  | Eop op1 elist1 m1, Eop op2 elist2 m2 =>
+    if op_le op1 op2 then true
+    else if elist_le elist1 elist2 then true
+         else expr_le m1 m2
+  | Eop _ _ _, Ebase _ => false
+  | Eop _ _ _, _ => true
+  | Eload chunk1 addr1 elist1 expr1, Eload chunk2 addr2 elist2 expr2 =>
+    if chunk_le chunk1 chunk2 then true
+    else if addr_le addr1 addr2 then true
+         else if elist_le elist1 elist2 then true
+              else expr_le expr1 expr2
+  | Eload _ _ _ _, Ebase _ => false
+  | Eload _ _ _ _, Eop _ _ _ => false
+  | Eload _ _ _ _, _ => true
+  | Estore m1 chunk1 addr1 elist1 expr1, Estore m2 chunk2 addr2 elist2 expr2 =>
+    if expr_le m1 m2 then true
+    else if chunk_le chunk1 chunk2 then true
+         else if addr_le addr1 addr2 then true
+              else if elist_le elist1 elist2 then true
+                   else expr_le expr1 expr2
+  | Estore _ _ _ _ _, Ebase _ => false
+  | Estore _ _ _ _ _, Eop _ _ _ => false
+  | Estore _ _ _ _ _, Eload _ _ _ _ => false
+  | Estore _ _ _ _ _, _ => true
+  | Esetpred p1 cond1 elist1 m1, Esetpred p2 cond2 elist2 m2 =>
+    if (p1 <=? p2)%positive then true
+    else if cond_le cond1 cond2 then true
+         else if elist_le elist1 elist2 then true
+              else expr_le m1 m2
+  | Esetpred _ _ _ _, Econd _ => true
+  | Esetpred _ _ _ _, _ => false
+  | Econd eplist1, Econd eplist2 => eplist_le eplist1 eplist2
+  | Econd eplist1, _ => false
+  end
+with elist_le (e1 e2: expression_list) : bool :=
+  match e1, e2 with
+  | Enil, Enil => true
+  | Econs a1 b1, Econs a2 b2 => if expr_le a1 a2 then true else elist_le b1 b2
+  | Enil, _ => true
+  | _, Enil => false
+  end
+with eplist_le (e1 e2: expr_pred_list) : bool :=
+  match e1, e2 with
+  | EPnil, EPnil => true
+  | EPcons p1 a1 b1, EPcons p2 a2 b2 =>
+    if pred_le p1 p2 then true
+    else if expr_le a1 a2 then true else eplist_le b1 b2
+  | EPnil, _ => true
+  | _, EPnil => false
+  end
+.*)
 
 (*|
 Using IMap we can create a map from resources to any other type, as resources can be uniquely
@@ -221,23 +442,29 @@ identified as positive numbers.
 
 Module Rtree := ITree(R_indexed).
 
-Definition forest : Type := Rtree.t expression.
+Definition forest : Type := Rtree.t pred_expr.
 
-Definition regset := Registers.Regmap.t val.
-
-Definition get_forest v f :=
+Definition get_forest v (f: forest) :=
   match Rtree.get v f with
-  | None => Ebase v
+  | None => NE.singleton (None, (Ebase v))
   | Some v' => v'
   end.
 
 Notation "a # b" := (get_forest b a) (at level 1).
 Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level).
 
-Record sem_state := mk_sem_state {
-                    sem_state_regset : regset;
-                    sem_state_memory : Memory.mem
-                    }.
+Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) :=
+  match p with
+  | Some p' => if eval_predf pr p' then v else vo
+  | None => v
+  end.
+
+Definition get_pr i := match i with mk_instr_state a b c => b end.
+
+Definition get_m i := match i with mk_instr_state a b c => c end.
+
+Definition eval_predf_opt pr p :=
+  match p with Some p' => eval_predf pr p' | None => true end.
 
 (*|
 Finally we want to define the semantics of execution for the expressions with symbolic values, so
@@ -246,82 +473,142 @@ the result of executing the expressions will be an expressions.
 
 Section SEMANTICS.
 
-Context (A : Set) (genv : Genv.t A unit).
+Context {A : Type} (genv : Genv.t A unit).
 
 Inductive sem_value :
-      val -> sem_state -> expression -> val -> Prop :=
-  | Sbase_reg:
-          forall sp st r,
-          sem_value sp st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st))
-  | Sop:
-          forall st op args v lv sp,
-          sem_val_list sp st args lv ->
-          Op.eval_operation genv sp op lv (sem_state_memory st) = Some v ->
-          sem_value sp st (Eop op args) v
-  | Sload :
-          forall st mem_exp addr chunk args a v m' lv sp,
-          sem_mem sp st mem_exp m' ->
-          sem_val_list sp st args lv ->
-          Op.eval_addressing genv sp addr lv = Some a ->
-          Memory.Mem.loadv chunk m' a = Some v ->
-          sem_value sp st (Eload chunk addr args mem_exp) v
+  val -> instr_state -> expression -> val -> Prop :=
+| Sbase_reg:
+    forall sp rs r m pr,
+    sem_value sp (mk_instr_state rs pr m) (Ebase (Reg r)) (rs !! r)
+| Sop:
+    forall rs m op args v lv sp m' mem_exp pr,
+    sem_mem sp (mk_instr_state rs pr m) mem_exp m' ->
+    sem_val_list sp (mk_instr_state rs pr m) args lv ->
+    Op.eval_operation genv sp op lv m' = Some v ->
+    sem_value sp (mk_instr_state rs pr m) (Eop op args mem_exp) v
+| Sload :
+    forall st mem_exp addr chunk args a v m' lv sp,
+    sem_mem sp st mem_exp m' ->
+    sem_val_list sp st args lv ->
+    Op.eval_addressing genv sp addr lv = Some a ->
+    Memory.Mem.loadv chunk m' a = Some v ->
+    sem_value sp st (Eload chunk addr args mem_exp) v
+with sem_pred :
+       val -> instr_state -> expression -> bool -> Prop :=
+| Spred:
+    forall st mem_exp args c lv m' v sp,
+    sem_mem sp st mem_exp m' ->
+    sem_val_list sp st args lv ->
+    Op.eval_condition c lv m' = Some v ->
+    sem_pred sp st (Esetpred c args mem_exp) v
+| Sbase_pred:
+    forall rs pr m p sp,
+    sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (pr !! p)
 with sem_mem :
-          val -> sem_state -> expression -> Memory.mem -> Prop :=
-  | Sstore :
-          forall st mem_exp val_exp m'' addr v a m' chunk args lv sp,
-          sem_mem sp st mem_exp m' ->
-          sem_value sp st val_exp v ->
-          sem_val_list sp st args lv ->
-          Op.eval_addressing genv sp addr lv = Some a ->
-          Memory.Mem.storev chunk m' a v = Some m'' ->
-          sem_mem sp st (Estore mem_exp chunk addr args val_exp) m''
-    | Sbase_mem :
-            forall st m sp,
-            sem_mem sp st (Ebase Mem) m
+       val -> instr_state -> expression -> Memory.mem -> Prop :=
+| Sstore :
+    forall st mem_exp val_exp m'' addr v a m' chunk args lv sp,
+    sem_mem sp st mem_exp m' ->
+    sem_value sp st val_exp v ->
+    sem_val_list sp st args lv ->
+    Op.eval_addressing genv sp addr lv = Some a ->
+    Memory.Mem.storev chunk m' a v = Some m'' ->
+    sem_mem sp st (Estore val_exp chunk addr args mem_exp) m''
+| Sbase_mem :
+    forall rs m sp pr,
+    sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m
 with sem_val_list :
-          val -> sem_state -> expression_list -> list val -> Prop :=
-    | Snil :
-            forall st sp,
-            sem_val_list sp st Enil nil
-    | Scons :
-            forall st e v l lv sp,
-            sem_value sp st e v ->
-            sem_val_list sp st l lv ->
-            sem_val_list sp st (Econs e l) (v :: lv).
+       val -> instr_state -> expression_list -> list val -> Prop :=
+| Snil :
+    forall st sp,
+    sem_val_list sp st Enil nil
+| Scons :
+    forall st e v l lv sp,
+    sem_value sp st e v ->
+    sem_val_list sp st l lv ->
+    sem_val_list sp st (Econs e l) (v :: lv)
+.
+
+Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> Prop):
+  val -> instr_state -> pred_expr -> A -> Prop :=
+| sem_pred_expr_base :
+    forall sp st e v,
+    sem sp st e v ->
+    sem_pred_expr sem sp st (NE.singleton (None, e)) v
+| sem_pred_expr_p :
+    forall sp st e p v,
+    eval_predf (instr_st_predset st) p = true ->
+    sem sp st e v ->
+    sem_pred_expr sem sp st (NE.singleton (Some p, e)) v
+| sem_pred_expr_cons_true :
+    forall sp st e pr p' v,
+    eval_predf (instr_st_predset st) pr = true ->
+    sem sp st e v ->
+    sem_pred_expr sem sp st ((Some pr, e)::|p') v
+| sem_pred_expr_cons_false :
+    forall sp st e pr p' v,
+    eval_predf (instr_st_predset st) pr = false ->
+    sem_pred_expr sem sp st p' v ->
+    sem_pred_expr sem sp st ((Some pr, e)::|p') v
+| sem_pred_expr_cons_None :
+    forall sp st e p' v,
+    sem sp st e v ->
+    sem_pred_expr sem sp st ((None, e)::|p') v
+.
+
+Definition collapse_pe (p: pred_expr) : option expression :=
+  match p with
+  | NE.singleton (None, p) => Some p
+  | _ => None
+  end.
+
+Inductive sem_predset :
+  val -> instr_state -> forest -> predset -> Prop :=
+| Spredset:
+    forall st f sp rs',
+    (forall pe x,
+      collapse_pe (f # (Pred x)) = Some pe ->
+      sem_pred sp st pe (rs' !! x)) ->
+    sem_predset sp st f rs'.
 
 Inductive sem_regset :
-  val -> sem_state -> forest -> regset -> Prop :=
-  | Sregset:
-        forall st f rs' sp,
-        (forall x, sem_value sp st (f # (Reg x)) (Registers.Regmap.get x rs')) ->
-        sem_regset sp st f rs'.
+  val -> instr_state -> forest -> regset -> Prop :=
+| Sregset:
+    forall st f sp rs',
+    (forall x, sem_pred_expr sem_value sp st (f # (Reg x)) (rs' !! x)) ->
+    sem_regset sp st f rs'.
 
 Inductive sem :
-  val -> sem_state -> forest -> sem_state -> Prop :=
-  | Sem:
-        forall st rs' m' f sp,
-        sem_regset sp st f rs' ->
-        sem_mem sp st (f # Mem) m' ->
-        sem sp st f (mk_sem_state rs' m').
+  val -> instr_state -> forest -> instr_state -> Prop :=
+| Sem:
+    forall st rs' m' f sp pr',
+    sem_regset sp st f rs' ->
+    sem_predset sp st f pr' ->
+    sem_pred_expr sem_mem sp st (f # Mem) m' ->
+    sem sp st f (mk_instr_state rs' pr' m').
 
 End SEMANTICS.
 
 Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool :=
   match e1, e2 with
   | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false
-  | Eop op1 el1, Eop op2 el2 =>
-      if operation_eq op1 op2 then beq_expression_list el1 el2 else false
+  | Eop op1 el1 exp1, Eop op2 el2 exp2 =>
+    if operation_eq op1 op2 then
+    beq_expression_list el1 el2 else false
   | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 =>
-      if memory_chunk_eq chk1 chk2
-      then if addressing_eq addr1 addr2
-      then if beq_expression_list el1 el2
-      then beq_expression e1 e2 else false else false else false
-  | Estore m1 chk1 addr1 el1 e1, Estore m2 chk2 addr2 el2 e2=>
-      if memory_chunk_eq chk1 chk2
-      then if addressing_eq addr1 addr2
-      then if beq_expression_list el1 el2
-      then if beq_expression m1 m2
-      then beq_expression e1 e2 else false else false else false else false
+    if memory_chunk_eq chk1 chk2
+    then if addressing_eq addr1 addr2
+         then if beq_expression_list el1 el2
+              then beq_expression e1 e2 else false else false else false
+  | Estore e1 chk1 addr1 el1 m1, Estore e2 chk2 addr2 el2 m2 =>
+    if memory_chunk_eq chk1 chk2
+    then if addressing_eq addr1 addr2
+         then if beq_expression_list el1 el2
+              then if beq_expression m1 m2
+                   then beq_expression e1 e2 else false else false else false else false
+  | Esetpred c1 el1 m1, Esetpred c2 el2 m2 =>
+    if condition_eq c1 c2
+    then beq_expression_list el1 el2 else false
   | _, _ => false
   end
 with beq_expression_list (el1 el2: expression_list) {struct el1} : bool :=
@@ -329,10 +616,12 @@ with beq_expression_list (el1 el2: expression_list) {struct el1} : bool :=
   | Enil, Enil => true
   | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2
   | _, _ => false
-  end.
+  end
+.
 
 Scheme expression_ind2 := Induction for expression Sort Prop
-  with expression_list_ind2 := Induction for expression_list Sort Prop.
+  with expression_list_ind2 := Induction for expression_list Sort Prop
+.
 
 Lemma beq_expression_correct:
   forall e1 e2, beq_expression e1 e2 = true -> e1 = e2.
@@ -342,35 +631,127 @@ Proof.
       (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.
+             forall e2, beq_expression_list e1 e2 = true -> e1 = e2);
+  try solve [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; eauto using Peqb_true_eq].
+  destruct e2; try discriminate. eauto.
+Abort.
+
+Definition hash_tree := PTree.t expression.
+
+Definition find_tree (el: expression) (h: hash_tree) : option positive :=
+  match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with
+  | (p, _) :: nil => Some p
+  | _ => None
+  end.
+
+Definition combine_option {A} (a b: option A) : option A :=
+  match a, b with
+  | Some a', _ => Some a'
+  | _, Some b' => Some b'
+  | _, _ => None
+  end.
+
+Definition max_key {A} (t: PTree.t A) :=
+  fold_right Pos.max 1%positive (map fst (PTree.elements t)).
+
+Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree :=
+  match find_tree e h with
+  | Some p => (p, h)
+  | None =>
+    let nkey := Pos.max max (max_key h) + 1 in
+    (nkey, PTree.set nkey e h)
+  end.
+
+Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree :=
+  match pe with
+  | NE.singleton (None, e) =>
+    let (p, h') := hash_expr max e h in
+    (Pvar p, h')
+  | NE.singleton (Some p, e) =>
+    let (p', h') := hash_expr max e h in
+    (Por (Pnot p) (Pvar p'), h')
+  | (Some p, e)::|pe' =>
+    let (p', h') := hash_expr max e h in
+    let (p'', h'') := encode_expression max pe' h' in
+    (Pand (Por (Pnot p) (Pvar p')) p'', h'')
+  | (None, e)::|pe' =>
+    let (p', h') := hash_expr max e h in
+    let (p'', h'') := encode_expression max pe' h' in
+    (Pand (Pvar p') p'', h'')
+  end.
+
+Fixpoint max_predicate (p: pred_op) : positive :=
+  match p with
+  | Pvar p => p
+  | Pand a b => Pos.max (max_predicate a) (max_predicate b)
+  | Por a b => Pos.max (max_predicate a) (max_predicate b)
+  | Pnot a => max_predicate a
+  end.
+
+Fixpoint max_pred_expr (pe: pred_expr) : positive :=
+  match pe with
+  | NE.singleton (None, _) => 1
+  | NE.singleton (Some p, _) => max_predicate p
+  | (Some p, _) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe')
+  | (None, _) ::| pe' => (max_pred_expr pe')
+  end.
+
+Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool :=
+  match pe1, pe2 with
+  (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2
+  | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 =>
+    if beq_expression e1 e2
+    then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with
+         | Some None => true
+         | _ => false
+         end
+    else false
+  | PEsingleton (Some p) e1, PEsingleton None e2
+  | PEsingleton None e1, PEsingleton (Some p) e2 =>
+    if beq_expression e1 e2
+    then match sat_pred_simple bound (Pnot p) with
+         | Some None => true
+         | _ => false
+         end
+    else false*)
+  | pe1, pe2 =>
+    let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in
+    let (p1, h) := encode_expression max pe1 (PTree.empty _) in
+    let (p2, h') := encode_expression max pe2 h in
+    match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with
+    | Some None => true
+    | _ => false
+    end
+  end.
 
 Definition empty : forest := Rtree.empty _.
 
-(*|
-This function checks if all the elements in [fa] are in [fb], but not the other way round.
-|*)
+Definition check := Rtree.beq (beq_pred_expr 10000).
 
-Definition check := Rtree.beq beq_expression.
+Compute (check (empty # (Reg 2) <-
+                (((Some (Pand (Pvar 4) (Pnot (Pvar 4)))), (Ebase (Reg 9))) ::|
+                        (NE.singleton ((Some (Pvar 2)), (Ebase (Reg 3))))))
+               (empty # (Reg 2) <- (NE.singleton ((Some (Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))),
+                                                (Ebase (Reg 3)))))).
 
-Lemma check_correct: forall (fa fb : forest) (x : resource),
+Lemma check_correct: forall (fa fb : forest),
   check fa fb = true -> (forall x, fa # x = fb # x).
 Proof.
-  unfold check, get_forest; intros;
+  (*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.
+Qed.*)
+  Abort.
 
 Lemma get_empty:
-  forall r, empty#r = Ebase r.
+  forall r, empty#r = NE.singleton (None, Ebase r).
 Proof.
   intros; unfold get_forest;
   destruct_match; auto; [ ];
@@ -422,16 +803,11 @@ Proof.
         apply IHm1_2. intros; apply (H (xI x)).
 Qed.
 
-Lemma map0:
-  forall r,
-  empty # r = Ebase r.
-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; auto; apply map0. Qed.
+  (empty # dst <- w) # dst' = NE.singleton (None, Ebase dst').
+Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed.
 
 Lemma genmap1:
   forall (f : forest) w dst dst',
@@ -440,7 +816,7 @@ Lemma genmap1:
 Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed.
 
 Lemma map2:
-  forall (v : expression) x rs,
+  forall (v : pred_expr) x rs,
   (rs # x <- v) # x = v.
 Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed.
 
@@ -450,8 +826,8 @@ Lemma tri1:
 Proof. crush. Qed.
 
 Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop :=
-  (forall sp op vl, Op.eval_operation ge sp op vl =
-                    Op.eval_operation tge sp op vl)
+  (forall sp op vl m, Op.eval_operation ge sp op vl m =
+                      Op.eval_operation tge sp op vl m)
   /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl =
                          Op.eval_addressing tge sp addr vl).
 
@@ -460,39 +836,50 @@ Lemma ge_preserved_same:
 Proof. unfold ge_preserved; auto. Qed.
 Hint Resolve ge_preserved_same : rtlpar.
 
-Inductive sem_state_ld : sem_state -> sem_state -> Prop :=
-| sem_state_ld_intro:
-  forall rs rs' m m',
-    regs_lessdef rs rs' ->
+Ltac rtlpar_crush := crush; eauto with rtlpar.
+
+Inductive match_states : instr_state -> instr_state -> Prop :=
+| match_states_intro:
+  forall ps ps' rs rs' m m',
+    (forall x, rs !! x = rs' !! x) ->
+    (forall x, ps !! x = ps' !! x) ->
     m = m' ->
-    sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m').
+    match_states (mk_instr_state rs ps  m) (mk_instr_state rs' ps' m').
+
+Inductive match_states_ld : instr_state -> instr_state -> Prop :=
+| match_states_ld_intro:
+  forall ps ps' rs rs' m m',
+    regs_lessdef rs rs' ->
+    (forall x, ps !! x = ps' !! x) ->
+    Mem.extends m m' ->
+    match_states_ld (mk_instr_state rs ps m) (mk_instr_state rs' ps' m').
 
 Lemma sems_det:
   forall A ge tge sp st f,
   ge_preserved ge tge ->
   forall v v' mv mv',
-  (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\
-  (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv').
+  (@sem_value A ge sp st f v /\ @sem_value A tge sp st f v' -> v = v') /\
+  (@sem_mem A ge sp st f mv /\ @sem_mem A tge sp st f mv' -> mv = mv').
 Proof. Abort.
 
 (*Lemma sem_value_det:
   forall A ge tge sp st f v v',
   ge_preserved ge tge ->
-  sem_value A ge sp st f v ->
-  sem_value A tge sp st f v' ->
+  @sem_value A ge sp st f v ->
+  @sem_value A tge sp st f v' ->
   v = v'.
 Proof.
-  intros;
-  generalize (sems_det A ge tge sp st f H v v'
-                      st.(sem_state_memory) st.(sem_state_memory));
+  intros. destruct st.
+  generalize (sems_det A ge tge sp (mk_instr_state rs m) f H v v'
+                      m m);
   crush.
 Qed.
 Hint Resolve sem_value_det : rtlpar.
 
 Lemma sem_value_det':
   forall FF ge sp s f v v',
-  sem_value FF ge sp s f v ->
-  sem_value FF ge sp s f v' ->
+  @sem_value FF ge sp s f v ->
+  @sem_value FF ge sp s f v' ->
   v = v'.
 Proof.
   simplify; eauto with rtlpar.
@@ -501,20 +888,20 @@ Qed.
 Lemma sem_mem_det:
   forall A ge tge sp st f m m',
   ge_preserved ge tge ->
-  sem_mem A ge sp st f m ->
-  sem_mem A tge sp st f m' ->
+  @sem_mem A ge sp st f m ->
+  @sem_mem A tge sp st f m' ->
   m = m'.
 Proof.
-  intros;
-  generalize (sems_det A ge tge sp st f H sp sp m m');
+  intros. destruct st.
+  generalize (sems_det A ge tge sp (mk_instr_state rs m0) f H sp sp m m');
   crush.
 Qed.
 Hint Resolve sem_mem_det : rtlpar.
 
 Lemma sem_mem_det':
   forall FF ge sp s f m m',
-    sem_mem FF ge sp s f m ->
-    sem_mem FF ge sp s f m' ->
+    @sem_mem FF ge sp s f m ->
+    @sem_mem FF ge sp s f m' ->
     m = m'.
 Proof.
   simplify; eauto with rtlpar.
@@ -525,9 +912,9 @@ Hint Resolve Val.lessdef_same : rtlpar.
 Lemma sem_regset_det:
   forall FF ge tge sp st f v v',
     ge_preserved ge tge ->
-    sem_regset FF ge sp st f v ->
-    sem_regset FF tge sp st f v' ->
-    regs_lessdef v v'.
+    @sem_regset FF ge sp st f v ->
+    @sem_regset FF tge sp st f v' ->
+    (forall x, v !! x = v' !! x).
 Proof.
   intros; unfold regs_lessdef.
   inv H0; inv H1;
@@ -538,9 +925,9 @@ Hint Resolve sem_regset_det : rtlpar.
 Lemma sem_det:
   forall FF ge tge sp st f st' st'',
     ge_preserved ge tge ->
-    sem FF ge sp st f st' ->
-    sem FF tge sp st f st'' ->
-    sem_state_ld st' st''.
+    @sem FF ge sp st f st' ->
+    @sem FF tge sp st f st'' ->
+    match_states st' st''.
 Proof.
   intros.
   destruct st; destruct st'; destruct st''.
@@ -551,30 +938,86 @@ Hint Resolve sem_det : rtlpar.
 
 Lemma sem_det':
   forall FF ge sp st f st' st'',
-    sem FF ge sp st f st' ->
-    sem FF ge sp st f st'' ->
-    sem_state_ld st' st''.
+    @sem FF ge sp st f st' ->
+    @sem FF ge sp st f st'' ->
+    match_states st' st''.
 Proof. eauto with rtlpar. Qed.
 
 (*|
 Update functions.
 |*)
+*)
 
-Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_list :=
+Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr :=
   match l with
-  | nil => Enil
-  | i :: l => Econs (f # (Reg i)) (list_translation l f)
+  | nil => nil
+  | i :: l => (f # (Reg i)) :: (list_translation l f)
+  end.
+
+Fixpoint replicate {A} (n: nat) (l: A) :=
+  match n with
+  | O => nil
+  | S n => l :: replicate n l
   end.
 
+Definition merge''' x y :=
+  match x, y with
+  | Some p1, Some p2 => Some (Pand p1 p2)
+  | Some p, None | None, Some p => Some p
+  | None, None => None
+  end.
+
+Definition merge'' x :=
+  match x with
+  | ((a, e), (b, el)) => (merge''' a b, Econs e el)
+  end.
+
+(*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
+Fixpoint merge' (pel: pred_expr) (tpel: predicated expression_list) :=
+  NE.map merge'' (NE.non_empty_prod pel tpel).
+
+Fixpoint merge (pel: list pred_expr): predicated expression_list :=
+  match pel with
+  | nil => NE.singleton (None, Enil)
+  | a :: b => merge' a (merge b)
+  end.
+
+Definition map_pred_op {A B} (pf: option pred_op * (A -> B)) (pa: option pred_op * A): option pred_op * B :=
+  match pa, pf with
+  | (p, a), (p', f) => (merge''' p p', f a)
+  end.
+
+Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): predicated B :=
+  NE.map (fun x => match x with ((p1, f), (p2, a)) => (merge''' p1 p2, f a) end) (NE.non_empty_prod pf pa).
+
+Definition apply1_predicated {A B} (pf: predicated (A -> B)) (pa: A): predicated B :=
+  NE.map (fun x => (fst x, (snd x) pa)) pf.
+
+Definition apply2_predicated {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C :=
+  NE.map (fun x => (fst x, (snd x) pa pb)) pf.
+
+Definition apply3_predicated {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D :=
+  NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
+
+(*Compute merge (((Some (Pvar 2), Ebase (Reg 4))::nil)::((Some (Pvar 3), Ebase (Reg 3))::(Some (Pvar 1), Ebase (Reg 3))::nil)::nil).*)
+
 Definition update (f : forest) (i : instr) : forest :=
   match i with
   | RBnop => f
   | RBop p op rl r =>
-    f # (Reg r) <- (Eop op (list_translation rl f))
+    f # (Reg r) <-
+    (map_predicated (map_predicated (NE.singleton (p, Eop op)) (merge (list_translation rl f))) (f # Mem))
   | RBload p chunk addr rl r =>
-    f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem))
+    f # (Reg r) <-
+    (map_predicated
+     (map_predicated (NE.singleton (p, Eload chunk addr)) (merge (list_translation rl f)))
+     (f # Mem))
   | RBstore p chunk addr rl r =>
-    f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r)))
+    f # Mem <-
+    (map_predicated
+     (map_predicated
+      (apply2_predicated (map_predicated (NE.singleton (p, Estore)) (f # (Reg r))) chunk addr)
+      (merge (list_translation rl f))) (f # Mem))
   | RBsetpred c addr p => f
   end.
 
@@ -588,7 +1031,7 @@ Get a sequence from the basic block.
 Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
   match b with
   | nil => f
-  | i :: l => update (abstract_sequence f l) i
+  | i :: l => abstract_sequence (update f i) l
   end.
 
 (*|
@@ -650,14 +1093,685 @@ Abstract computations
 =====================
 |*)
 
+(*Definition is_regs i := match i with mk_instr_state rs _ => rs end.
+Definition is_mem i := match i with mk_instr_state _ m => m end.
+
+Inductive state_lessdef : instr_state -> instr_state -> Prop :=
+  state_lessdef_intro :
+    forall rs1 rs2 m1,
+    (forall x, rs1 !! x = rs2 !! x) ->
+    state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1).
+
+(*|
+RTLBlock to abstract translation
+--------------------------------
+
+Correctness of translation from RTLBlock to the abstract interpretation language.
+|*)
+
+Lemma match_states_refl x : match_states x x.
+Proof. destruct x; constructor; crush. Qed.
+
+Lemma match_states_commut x y : match_states x y -> match_states y x.
+Proof. inversion 1; constructor; crush. Qed.
+
+Lemma match_states_trans x y z :
+  match_states x y -> match_states y z -> match_states x z.
+Proof. repeat inversion 1; constructor; crush. Qed.
+
+Ltac inv_simp :=
+  repeat match goal with
+  | H: exists _, _ |- _ => inv H
+  end; simplify.
+
+Lemma abstract_interp_empty A ge sp st : @sem A ge sp st empty st.
+Proof. destruct st; repeat constructor. Qed.
+
+Lemma abstract_interp_empty3 :
+  forall A ge sp st st',
+    @sem A ge sp st empty st' ->
+    match_states st st'.
+Proof.
+  inversion 1; subst; simplify.
+  destruct st. inv H1. simplify.
+  constructor. unfold regs_lessdef.
+  intros. inv H0. specialize (H1 x). inv H1; auto.
+  auto.
+Qed.*)
+
+Definition check_dest i r' :=
+  match i with
+  | RBop p op rl r => (r =? r')%positive
+  | RBload p chunk addr rl r => (r =? r')%positive
+  | _ => false
+  end.
+
+Lemma check_dest_dec i r : {check_dest i r = true} + {check_dest i r = false}.
+Proof. destruct (check_dest i r); tauto. Qed.
+
+Fixpoint check_dest_l l r :=
+  match l with
+  | nil => false
+  | a :: b => check_dest a r || check_dest_l b r
+  end.
+
+Lemma check_dest_l_forall :
+  forall l r,
+  check_dest_l l r = false ->
+  Forall (fun x => check_dest x r = false) l.
+Proof. induction l; crush. Qed.
+
+(*Lemma check_dest_l_ex :
+  forall l r,
+  check_dest_l l r = true ->
+  exists a, In a l /\ check_dest a r = true.
+Proof.
+  induction l; crush.
+  destruct (check_dest a r) eqn:?; try solve [econstructor; crush].
+  simplify.
+  exploit IHl. apply H. inv_simp. econstructor. simplify. right. eassumption.
+  auto.
+Qed.
+
+Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}.
+Proof. destruct (check_dest_l i r); tauto. Qed.
+
+Lemma check_dest_l_dec2 l r :
+  {Forall (fun x => check_dest x r = false) l}
+  + {exists a, In a l /\ check_dest a r = true}.
+Proof.
+  destruct (check_dest_l_dec l r); [right | left];
+  auto using check_dest_l_ex, check_dest_l_forall.
+Qed.
+
+Lemma check_dest_l_forall2 :
+  forall l r,
+  Forall (fun x => check_dest x r = false) l ->
+  check_dest_l l r = false.
+Proof.
+  induction l; crush.
+  inv H. apply orb_false_intro; crush.
+Qed.
+
+Lemma check_dest_l_ex2 :
+  forall l r,
+  (exists a, In a l /\ check_dest a r = true) ->
+  check_dest_l l r = true.
+Proof.
+  induction l; crush.
+  specialize (IHl r). inv H.
+  apply orb_true_intro; crush.
+  apply orb_true_intro; crush.
+  right. apply IHl. exists x. auto.
+Qed.
+
+Lemma check_dest_update :
+  forall f i r,
+  check_dest i r = false ->
+  (update f i) # (Reg r) = f # (Reg r).
+Proof.
+  destruct i; crush; try apply Pos.eqb_neq in H; apply genmap1; crush.
+Qed.
+
+Lemma check_dest_update2 :
+  forall f r rl op p,
+  (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f) (f # Mem).
+Proof. crush; rewrite map2; auto. Qed.
+
+Lemma check_dest_update3 :
+  forall f r rl p addr chunk,
+  (update f (RBload p chunk addr rl r)) # (Reg r) = Eload chunk addr (list_translation rl f) (f # Mem).
+Proof. crush; rewrite map2; auto. Qed.
+
+Lemma abstr_comp :
+  forall l i f x x0,
+  abstract_sequence f (l ++ i :: nil) = x ->
+  abstract_sequence f l = x0 ->
+  x = update x0 i.
+Proof. induction l; intros; crush; eapply IHl; eauto. Qed.
+
+Lemma abstract_seq :
+  forall l f i,
+    abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i.
+Proof. induction l; crush. Qed.
+
+Lemma check_list_l_false :
+  forall l x r,
+  check_dest_l (l ++ x :: nil) r = false ->
+  check_dest_l l r = false /\ check_dest x r = false.
+Proof.
+  simplify.
+  apply check_dest_l_forall in H. apply Forall_app in H.
+  simplify. apply check_dest_l_forall2; auto.
+  apply check_dest_l_forall in H. apply Forall_app in H.
+  simplify. inv H1. auto.
+Qed.
+
+Lemma check_list_l_true :
+  forall l x r,
+  check_dest_l (l ++ x :: nil) r = true ->
+  check_dest_l l r = true \/ check_dest x r = true.
+Proof.
+  simplify.
+  apply check_dest_l_ex in H; inv_simp.
+  apply in_app_or in H. inv H. left.
+  apply check_dest_l_ex2. exists x0. auto.
+  inv H0; auto.
+Qed.
+
+Lemma abstract_sequence_update :
+  forall l r f,
+  check_dest_l l r = false ->
+  (abstract_sequence f l) # (Reg r) = f # (Reg r).
+Proof.
+  induction l using rev_ind; crush.
+  rewrite abstract_seq. rewrite check_dest_update. apply IHl.
+  apply check_list_l_false in H. tauto.
+  apply check_list_l_false in H. tauto.
+Qed.
+
+Lemma rtlblock_trans_correct' :
+  forall bb ge sp st x st'',
+  RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' ->
+  exists st', RTLBlock.step_instr_list ge sp st bb st'
+              /\ step_instr ge sp st' x st''.
+Proof.
+  induction bb.
+  crush. exists st.
+  split. constructor. inv H. inv H6. auto.
+  crush. inv H. exploit IHbb. eassumption. inv_simp.
+  econstructor. split.
+  econstructor; eauto. eauto.
+Qed.
+
+Lemma sem_update_RBnop :
+  forall A ge sp st f st',
+  @sem A ge sp st f st' -> sem ge sp st (update f RBnop) st'.
+Proof. crush. Qed.
+
+Lemma gen_list_base:
+  forall FF ge sp l rs exps st1,
+  (forall x, @sem_value FF ge sp st1 (exps # (Reg x)) (rs !! x)) ->
+  sem_val_list ge sp st1 (list_translation l exps) rs ## l.
+Proof.
+  induction l.
+  intros. simpl. constructor.
+  intros. simpl. eapply Scons; eauto.
+Qed.
+
+Lemma abstract_seq_correct_aux:
+  forall FF ge sp i st1 st2 st3 f,
+    @step_instr FF ge sp st3 i st2 ->
+    sem ge sp st1 f st3 ->
+    sem ge sp st1 (update f i) st2.
+Proof.
+  intros; inv H; simplify.
+  { simplify; eauto. } (*apply match_states_refl. }*)
+  { inv H0. inv H6. destruct st1. econstructor. simplify.
+    constructor. intros.
+    destruct (resource_eq (Reg res) (Reg x)). inv e.
+    rewrite map2. econstructor. eassumption. apply gen_list_base; eauto.
+    rewrite Regmap.gss. eauto.
+    assert (res <> x). { unfold not in *. intros. apply n. rewrite H0. auto. }
+    rewrite Regmap.gso by auto.
+    rewrite genmap1 by auto. auto.
+
+    rewrite genmap1; crush. }
+  { inv H0. inv H7. constructor. constructor. intros.
+    destruct (Pos.eq_dec dst x); subst.
+    rewrite map2. econstructor; eauto.
+    apply gen_list_base. auto. rewrite Regmap.gss. auto.
+    rewrite genmap1. rewrite Regmap.gso by auto. auto.
+    unfold not in *; intros. inv H0. auto.
+    rewrite genmap1; crush.
+  }
+  { inv H0. inv H7. constructor. constructor; intros.
+    rewrite genmap1; crush.
+    rewrite map2. econstructor; eauto.
+    apply gen_list_base; auto.
+  }
+Qed.
+
+Lemma regmap_list_equiv :
+  forall A (rs1: Regmap.t A) rs2,
+    (forall x, rs1 !! x = rs2 !! x) ->
+    forall rl, rs1##rl = rs2##rl.
+Proof. induction rl; crush. Qed.
+
+Lemma sem_update_Op :
+  forall A ge sp st f st' r l o0 o m rs v,
+  @sem A ge sp st f st' ->
+  Op.eval_operation ge sp o0 rs ## l m = Some v ->
+  match_states st' (mk_instr_state rs m) ->
+  exists tst,
+  sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst.
+Proof.
+  intros. inv H1. simplify.
+  destruct st.
+  econstructor. simplify.
+  { constructor.
+    { constructor. intros. destruct (Pos.eq_dec x r); subst.
+      { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto.
+        { inv H9. eapply gen_list_base; eauto. }
+        { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } }
+      { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } }
+    { inv H. rewrite genmap1; crush. eauto. } }
+  { constructor; eauto. intros.
+    destruct (Pos.eq_dec r x);
+    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
+Qed.
+
+Lemma sem_update_load :
+  forall A ge sp st f st' r o m a l m0 rs v a0,
+  @sem A ge sp st f st' ->
+  Op.eval_addressing ge sp a rs ## l = Some a0 ->
+  Mem.loadv m m0 a0 = Some v ->
+  match_states st' (mk_instr_state rs m0) ->
+  exists tst : instr_state,
+    sem ge sp st (update f (RBload o m a l r)) tst
+    /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst.
+Proof.
+  intros. inv H2. pose proof H. inv H. inv H9.
+  destruct st.
+  econstructor; simplify.
+  { constructor.
+    { constructor. intros.
+      destruct (Pos.eq_dec x r); subst.
+      { rewrite map2. econstructor; eauto. eapply gen_list_base. intros.
+        rewrite <- H6. eauto.
+        instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. auto. }
+      { rewrite Regmap.gso by auto. rewrite genmap1; crush. } }
+    { rewrite genmap1; crush. eauto. } }
+  { constructor; auto; intros. destruct (Pos.eq_dec r x);
+    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
+Qed.
+
+Lemma sem_update_store :
+  forall A ge sp a0 m a l r o f st m' rs m0 st',
+  @sem A ge sp st f st' ->
+  Op.eval_addressing ge sp a rs ## l = Some a0 ->
+  Mem.storev m m0 a0 rs !! r = Some m' ->
+  match_states st' (mk_instr_state rs m0) ->
+  exists tst, sem ge sp st (update f (RBstore o m a l r)) tst
+              /\ match_states (mk_instr_state rs m') tst.
+Proof.
+  intros. inv H2. pose proof H. inv H. inv H9.
+  destruct st.
+  econstructor; simplify.
+  { econstructor.
+    { econstructor; intros. rewrite genmap1; crush. }
+    { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. rewrite <- H6.
+      eauto. specialize (H6 r). rewrite H6. eauto. } }
+  { econstructor; eauto. }
+Qed.
+
+Lemma sem_update :
+  forall A ge sp st x st' st'' st''' f,
+  sem ge sp st f st' ->
+  match_states st' st''' ->
+  @step_instr A ge sp st''' x st'' ->
+  exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst.
+Proof.
+  intros. destruct x; inv H1.
+  { econstructor. split.
+    apply sem_update_RBnop. eassumption.
+    apply match_states_commut. auto. }
+  { eapply sem_update_Op; eauto. }
+  { eapply sem_update_load; eauto. }
+  { eapply sem_update_store; eauto. }
+Qed.
+
+Lemma sem_update2_Op :
+  forall A ge sp st f r l o0 o m rs v,
+  @sem A ge sp st f (mk_instr_state rs m) ->
+  Op.eval_operation ge sp o0 rs ## l m = Some v ->
+  sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m).
+Proof.
+  intros. destruct st. constructor.
+  inv H. inv H6.
+  { constructor; intros. simplify.
+    destruct (Pos.eq_dec r x); subst.
+    { rewrite map2. econstructor. eauto.
+      apply gen_list_base. eauto.
+      rewrite Regmap.gss. auto. }
+    { rewrite genmap1; crush. rewrite Regmap.gso; auto.  } }
+  { simplify. rewrite genmap1; crush. inv H. eauto. }
+Qed.
+
+Lemma sem_update2_load :
+  forall A ge sp st f r o m a l m0 rs v a0,
+    @sem A ge sp st f (mk_instr_state rs m0) ->
+    Op.eval_addressing ge sp a rs ## l = Some a0 ->
+    Mem.loadv m m0 a0 = Some v ->
+    sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0).
+Proof.
+  intros. simplify. inv H. inv H7. constructor.
+  { constructor; intros. destruct (Pos.eq_dec r x); subst.
+    { rewrite map2. rewrite Regmap.gss. econstructor; eauto.
+      apply gen_list_base; eauto. }
+    { rewrite genmap1; crush. rewrite Regmap.gso; eauto. }
+  }
+  { simplify. rewrite genmap1; crush. }
+Qed.
+
+Lemma sem_update2_store :
+  forall A ge sp a0 m a l r o f st m' rs m0,
+    @sem A ge sp st f (mk_instr_state rs m0) ->
+    Op.eval_addressing ge sp a rs ## l = Some a0 ->
+    Mem.storev m m0 a0 rs !! r = Some m' ->
+    sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m').
+Proof.
+  intros. simplify. inv H. inv H7. constructor; simplify.
+  { econstructor; intros. rewrite genmap1; crush. }
+  { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. }
+Qed.
+
+Lemma sem_update2 :
+  forall A ge sp st x st' st'' f,
+  sem ge sp st f st' ->
+  @step_instr A ge sp st' x st'' ->
+  sem ge sp st (update f x) st''.
+Proof.
+  intros.
+  destruct x; inv H0;
+  eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store.
+Qed.
+
+Lemma rtlblock_trans_correct :
+  forall bb ge sp st st',
+    RTLBlock.step_instr_list ge sp st bb st' ->
+    forall tst,
+      match_states st tst ->
+      exists tst', sem ge sp tst (abstract_sequence empty bb) tst'
+                   /\ match_states st' tst'.
+Proof.
+  induction bb using rev_ind; simplify.
+  { econstructor. simplify. apply abstract_interp_empty.
+    inv H. auto. }
+  { apply rtlblock_trans_correct' in H. inv_simp.
+    rewrite abstract_seq.
+    exploit IHbb; try eassumption; []; inv_simp.
+    exploit sem_update. apply H1. apply match_states_commut; eassumption.
+    eauto. inv_simp. econstructor. split. apply H3.
+    auto. }
+Qed.
+
+Lemma abstr_sem_val_mem :
+  forall A B ge tge st tst sp a,
+    ge_preserved ge tge ->
+    forall v m,
+    (@sem_mem A ge sp st a m /\ match_states st tst -> @sem_mem B tge sp tst a m) /\
+    (@sem_value A ge sp st a v /\ match_states st tst -> @sem_value B tge sp tst a v).
+Proof.
+  intros * H.
+  apply expression_ind2 with
+
+    (P := fun (e1: expression) =>
+    forall v m,
+    (@sem_mem A ge sp st e1 m /\ match_states st tst -> @sem_mem B tge sp tst e1 m) /\
+    (@sem_value A ge sp st e1 v /\ match_states st tst -> @sem_value B tge sp tst e1 v))
+
+    (P0 := fun (e1: expression_list) =>
+    forall lv, @sem_val_list A ge sp st e1 lv /\ match_states st tst -> @sem_val_list B tge sp tst e1 lv);
+  simplify; intros; simplify.
+  { inv H1. inv H2. constructor. }
+  { inv H2. inv H1. rewrite H0. constructor. }
+  { inv H3. }
+  { inv H3. inv H4. econstructor. apply H1; auto. simplify. eauto. constructor. auto. auto.
+    apply H0; simplify; eauto. constructor; eauto.
+    unfold ge_preserved in *. simplify. rewrite <- H2. auto.
+  }
+  { inv H3. }
+  { inv H3. inv H4. econstructor. apply H1; eauto; simplify; eauto. constructor; eauto.
+    apply H0; simplify; eauto. constructor; eauto.
+    inv H. rewrite <- H4. eauto.
+    auto.
+  }
+  { inv H4. inv H5. econstructor. apply H0; eauto. simplify; eauto. constructor; eauto.
+    apply H2; eauto. simplify; eauto. constructor; eauto.
+    apply H1; eauto. simplify; eauto. constructor; eauto.
+    inv H. rewrite <- H5. eauto. auto.
+  }
+  { inv H4. }
+  { inv H1. constructor. }
+  { inv H3. constructor; auto. apply H0; eauto. apply Mem.empty. }
+Qed.
+
+Lemma abstr_sem_value :
+  forall a A B ge tge sp st tst v,
+    @sem_value A ge sp st a v ->
+    ge_preserved ge tge ->
+    match_states st tst ->
+    @sem_value B tge sp tst a v.
+Proof. intros; eapply abstr_sem_val_mem; eauto; apply Mem.empty. Qed.
+
+Lemma abstr_sem_mem :
+  forall a A B ge tge sp st tst v,
+    @sem_mem A ge sp st a v ->
+    ge_preserved ge tge ->
+    match_states st tst ->
+    @sem_mem B tge sp tst a v.
+Proof. intros; eapply abstr_sem_val_mem; eauto. Qed.
+
+Lemma abstr_sem_regset :
+  forall a a' A B ge tge sp st tst rs,
+    @sem_regset A ge sp st a rs ->
+    ge_preserved ge tge ->
+    (forall x, a # x = a' # x) ->
+    match_states st tst ->
+    exists rs', @sem_regset B tge sp tst a' rs' /\ (forall x, rs !! x = rs' !! x).
+Proof.
+  inversion 1; intros.
+  inv H7.
+  econstructor. simplify. econstructor. intros.
+  eapply abstr_sem_value; eauto. rewrite <- H6.
+  eapply H0. constructor; eauto.
+  auto.
+Qed.
+
+Lemma abstr_sem :
+  forall a a' A B ge tge sp st tst st',
+    @sem A ge sp st a st' ->
+    ge_preserved ge tge ->
+    (forall x, a # x = a' # x) ->
+    match_states st tst ->
+    exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'.
+Proof.
+  inversion 1; subst; intros.
+  inversion H4; subst.
+  exploit abstr_sem_regset; eauto; inv_simp.
+  do 3 econstructor; eauto.
+  rewrite <- H3.
+  eapply abstr_sem_mem; eauto.
+Qed.
+
+Lemma abstract_execution_correct':
+  forall A B ge tge sp st' a a' st tst,
+  @sem A ge sp st a st' ->
+  ge_preserved ge tge ->
+  check a a' = true ->
+  match_states st tst ->
+  exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'.
+Proof.
+  intros;
+  pose proof (check_correct a a' H1);
+  eapply abstr_sem; eauto.
+Qed.
+
+Lemma states_match :
+  forall st1 st2 st3 st4,
+  match_states st1 st2 ->
+  match_states st2 st3 ->
+  match_states st3 st4 ->
+  match_states st1 st4.
+Proof.
+  intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4.
+  inv H1. inv H2. inv H3; constructor.
+  unfold regs_lessdef in *. intros.
+  repeat match goal with
+         | H: forall _, _, r : positive |- _ => specialize (H r)
+         end.
+  congruence.
+  auto.
+Qed.
+
+Lemma step_instr_block_same :
+  forall ge sp st st',
+  step_instr_block ge sp st nil st' ->
+  st = st'.
+Proof. inversion 1; auto. Qed.
+
+Lemma step_instr_seq_same :
+  forall ge sp st st',
+  step_instr_seq ge sp st nil st' ->
+  st = st'.
+Proof. inversion 1; auto. Qed.
+
+Lemma match_states_list :
+  forall A (rs: Regmap.t A) rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall l, rs ## l = rs' ## l.
+Proof. induction l; crush. Qed.
+
+Lemma PTree_matches :
+  forall A (v: A) res rs rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
+Proof.
+  intros; destruct (Pos.eq_dec x res); subst;
+  [ repeat rewrite Regmap.gss by auto
+  | repeat rewrite Regmap.gso by auto ]; auto.
+Qed.
+
+Lemma step_instr_matches :
+  forall A a ge sp st st',
+  @step_instr A ge sp st a st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr ge sp tst a tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction 1; simplify;
+  match goal with H: match_states _ _ |- _ => inv H end;
+  repeat econstructor; try erewrite match_states_list;
+  try apply PTree_matches; eauto;
+  match goal with
+    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
+  end.
+Qed.
+
+Lemma step_instr_list_matches :
+  forall a ge sp st st',
+  step_instr_list ge sp st a st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr_list ge sp tst a tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction a; intros; inv H;
+  try (exploit step_instr_matches; eauto; []; inv_simp;
+       exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto.
+Qed.
+
+Lemma step_instr_seq_matches :
+  forall a ge sp st st',
+  step_instr_seq ge sp st a st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr_seq ge sp tst a tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction a; intros; inv H;
+  try (exploit step_instr_list_matches; eauto; []; inv_simp;
+       exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto.
+Qed.
+
+Lemma step_instr_block_matches :
+  forall bb ge sp st st',
+  step_instr_block ge sp st bb st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr_block ge sp tst bb tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction bb; intros; inv H;
+  try (exploit step_instr_seq_matches; eauto; []; inv_simp;
+       exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto.
+Qed.
+
+Lemma sem_update' :
+  forall A ge sp st a x st',
+  sem ge sp st (update (abstract_sequence empty a) x) st' ->
+  exists st'',
+  @step_instr A ge sp st'' x st' /\
+  sem ge sp st (abstract_sequence empty a) st''.
+Proof.
+  Admitted.
+
+Lemma sem_separate :
+  forall A (ge: @RTLBlockInstr.genv A) b a sp st st',
+    sem ge sp st (abstract_sequence empty (a ++ b)) st' ->
+    exists st'',
+         sem ge sp st (abstract_sequence empty a) st''
+      /\ sem ge sp st'' (abstract_sequence empty b) st'.
+Proof.
+  induction b using rev_ind; simplify.
+  { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. }
+  { simplify. rewrite app_assoc in H. rewrite abstract_seq in H.
+    exploit sem_update'; eauto; inv_simp.
+    exploit IHb; eauto; inv_simp.
+    econstructor; split; eauto.
+    rewrite abstract_seq.
+    eapply sem_update2; eauto.
+  }
+Qed.
+
+Lemma rtlpar_trans_correct :
+  forall bb ge sp sem_st' sem_st st,
+  sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' ->
+  match_states sem_st st ->
+  exists st', RTLPar.step_instr_block ge sp st bb st'
+              /\ match_states sem_st' st'.
+Proof.
+  induction bb using rev_ind.
+  { repeat econstructor. eapply abstract_interp_empty3 in H.
+    inv H. inv H0. constructor; congruence. }
+  { simplify. inv H0. repeat rewrite concat_app in H. simplify.
+    rewrite app_nil_r in H.
+    exploit sem_separate; eauto; inv_simp.
+    repeat econstructor. admit. admit.
+  }
+Admitted.
+
 Lemma abstract_execution_correct:
-  forall bb bb' cfi ge tge sp rs m rs' m',
+  forall bb bb' cfi ge tge sp st st' tst,
+    RTLBlock.step_instr_list ge sp st bb st' ->
     ge_preserved ge tge ->
     schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
-    RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') ->
-    exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m')
-                 /\ regs_lessdef rs' rs''.
-Proof. Abort.
+    match_states st tst ->
+    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
+                 /\ match_states st' tst'.
+Proof.
+  intros.
+  unfold schedule_oracle in *. simplify.
+  exploit rtlblock_trans_correct; try eassumption; []; inv_simp.
+  exploit abstract_execution_correct';
+  try solve [eassumption | apply state_lessdef_match_sem; eassumption].
+  apply match_states_commut. eauto. inv_simp.
+  exploit rtlpar_trans_correct; try eassumption; []; inv_simp.
+  exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp.
+  repeat match goal with | H: match_states _ _ |- _ => inv H end.
+  do 2 econstructor; eauto.
+  econstructor; congruence.
+Qed.
+
+(*Lemma abstract_execution_correct_ld:
+  forall bb bb' cfi ge tge sp st st' tst,
+    RTLBlock.step_instr_list ge sp st bb st' ->
+    ge_preserved ge tge ->
+    schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
+    match_states_ld st tst ->
+    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
+                 /\ match_states st' tst'.
+Proof.
+  intros.*)
+*)
 
 (*|
 Top-level functions
@@ -677,16 +1791,7 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :
   else
     Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
 
-Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.function :=
-  let tfcode := fn_code (schedule f) in
-    Errors.OK (mkfunction f.(fn_sig)
-                          f.(fn_params)
-                          f.(fn_stacksize)
-                          tfcode
-                          f.(fn_entrypoint)).
-
-Definition transl_fundef := transf_partial_fundef transl_function_temp.
+Definition transl_fundef := transf_partial_fundef transl_function.
 
 Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
   transform_partial_program transl_fundef p.
-*)
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index a0c01fa..bb1cf97 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -38,34 +38,29 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
 | match_stackframe:
     forall f tf res sp pc rs rs',
       transl_function f = OK tf ->
-      regs_lessdef rs rs' ->
+      (forall x, rs !! x = rs' !! x) ->
       match_stackframes (Stackframe res f sp pc rs)
                         (Stackframe res tf sp pc rs').
 
 Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
 | match_state:
-    forall sf f sp pc rs rs' m m' sf' tf
+    forall sf f sp pc rs rs' m sf' tf
       (TRANSL: transl_function f = OK tf)
       (STACKS: list_forall2 match_stackframes sf sf')
-      (REG: regs_lessdef rs rs')
-      (MEM: Mem.extends m m'),
+      (REG: forall x, rs !! x = rs' !! x),
       match_states (State sf f sp pc rs m)
-                   (State sf' tf sp pc rs' m')
+                   (State sf' tf sp pc rs' m)
 | match_returnstate:
-    forall stack stack' v v' m m'
-      (STACKS: list_forall2 match_stackframes stack stack')
-      (MEM: Mem.extends m m')
-      (LD: Val.lessdef v v'),
+    forall stack stack' v m
+      (STACKS: list_forall2 match_stackframes stack stack'),
       match_states (Returnstate stack v m)
-                   (Returnstate stack' v' m')
+                   (Returnstate stack' v m)
 | match_callstate:
-    forall stack stack' f tf args args' m m'
+    forall stack stack' f tf args m
       (TRANSL: transl_fundef f = OK tf)
-      (STACKS: list_forall2 match_stackframes stack stack')
-      (LD: Val.lessdef_list args args')
-      (MEM: Mem.extends m m'),
+      (STACKS: list_forall2 match_stackframes stack stack'),
       match_states (Callstate stack f args m)
-                   (Callstate stack' tf args' m').
+                   (Callstate stack' tf args m).
 
 Section CORRECTNESS.
 
@@ -121,7 +116,7 @@ Section CORRECTNESS.
 
   Lemma find_function_translated:
     forall ros rs rs' f,
-      regs_lessdef rs rs' ->
+      (forall x, rs !! x = rs' !! x) ->
       find_function ge ros rs = Some f ->
       exists tf, find_function tge ros rs' = Some tf
                  /\ transl_fundef f = OK tf.
@@ -134,7 +129,7 @@ Section CORRECTNESS.
                  | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H]
                  | _ => solve [exploit functions_translated; eauto]
                  end.
-    unfold regs_lessdef; destruct ros; simplify; try rewrite <- H;
+    destruct ros; simplify; try rewrite <- H;
     [| rewrite symbols_preserved; destruct_match;
       try (apply function_ptr_translated); crush ];
     intros;
@@ -160,8 +155,8 @@ Section CORRECTNESS.
   Qed.
 
   Lemma eval_op_eq:
-    forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val),
-      Op.eval_operation ge sp0 op vl = Op.eval_operation tge sp0 op vl.
+    forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m,
+      Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m.
   Proof using TRANSL.
     intros.
     destruct op; auto; unfold Op.eval_operation, Genv.symbol_address, Op.eval_addressing32;
@@ -197,6 +192,16 @@ Section CORRECTNESS.
   Proof using. destruct or; crush. Qed.
   Hint Resolve lessdef_regmap_optget : rtlgp.
 
+  Lemma regmap_equiv_lessdef:
+    forall rs rs',
+      (forall x, rs !! x = rs' !! x) ->
+      regs_lessdef rs rs'.
+  Proof using.
+    intros; unfold regs_lessdef; intros.
+    rewrite H. apply Val.lessdef_refl.
+  Qed.
+  Hint Resolve regmap_equiv_lessdef : rtlgp.
+
   Lemma int_lessdef:
     forall rs rs',
       regs_lessdef rs rs' ->
@@ -227,8 +232,8 @@ Section CORRECTNESS.
       let H2 := fresh "SCHED" in
       learn H as H2;
       apply schedule_oracle_nil in H2
-    | [ H: find_function _ _ _ = Some _ |- _ ] =>
-      learn H; exploit find_function_translated; eauto; inversion 1
+    | [ H: find_function _ _ _ = Some _, H2: forall x, ?rs !! x = ?rs' !! x |- _ ] =>
+      learn H; exploit find_function_translated; try apply H2; eauto; inversion 1
     | [ H: Mem.free ?m _ _ _ = Some ?m', H2: Mem.extends ?m ?m'' |- _ ] =>
       learn H; exploit Mem.free_parallel_extends; eauto; intros
     | [ H: Events.eval_builtin_args _ _ _ _ _ _, H2: regs_lessdef ?rs ?rs' |- _ ] =>
@@ -249,6 +254,29 @@ Section CORRECTNESS.
   Hint Resolve set_reg_lessdef : rtlgp.
   Hint Resolve Op.eval_condition_lessdef : rtlgp.
 
+  Hint Constructors Events.eval_builtin_arg: barg.
+
+  Lemma eval_builtin_arg_eq:
+    forall A ge a v1 m1 e1 e2 sp,
+      (forall x, e1 x = e2 x) ->
+      @Events.eval_builtin_arg A ge e1 sp m1 a v1 ->
+      Events.eval_builtin_arg ge e2 sp m1 a v1.
+Proof. induction 2; try rewrite H; eauto with barg. Qed.
+
+  Lemma eval_builtin_args_eq:
+    forall A ge e1 sp m1 e2 al vl1,
+      (forall x, e1 x = e2 x) ->
+      @Events.eval_builtin_args A ge e1 sp m1 al vl1 ->
+      Events.eval_builtin_args ge e2 sp m1 al vl1.
+  Proof.
+    induction 2.
+    - econstructor; split.
+    - exploit eval_builtin_arg_eq; eauto. intros.
+      destruct IHlist_forall2 as [| y]. constructor; eauto.
+      constructor. constructor; auto.
+      constructor; eauto.
+  Qed.
+
   Lemma step_cf_instr_correct:
     forall cfi t s s',
       step_cf_instr ge s cfi t s' ->
@@ -257,7 +285,22 @@ Section CORRECTNESS.
         exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'.
   Proof using TRANSL.
     induction 1; repeat semantics_simpl;
-    repeat (econstructor; eauto with rtlgp).
+    try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)].
+    { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
+      eapply eval_builtin_args_eq. eapply REG.
+      eapply Events.eval_builtin_args_preserved. eapply symbols_preserved.
+      eauto.
+      intros.
+      unfold regmap_setres. destruct res.
+      destruct (Pos.eq_dec x0 x); subst.
+      repeat rewrite Regmap.gss; auto.
+      repeat rewrite Regmap.gso; auto.
+      eapply REG. eapply REG.
+    }
+    { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp).
+      unfold regmap_optget. destruct or. rewrite REG. constructor; eauto.
+      constructor; eauto.
+    }
   Qed.
 
   Theorem transl_step_correct :
@@ -269,21 +312,69 @@ Section CORRECTNESS.
   Proof.
 
     induction 1; repeat semantics_simpl.
-    Abort.
-
-(*    { destruct bb as [bbc bbe]; destruct x as [bbc' bbe'].
-      assert (bbe = bbe') by admit.
-      rewrite H3 in H5.
-      eapply abstract_execution_correct in H5; eauto with rtlgp.
-      repeat econstructor; eauto with rtlgp. simplify.
-      exploit step_cf_instr_correct. eauto.
-      econstructor; eauto with rtlgp.
+
+    { destruct bb; destruct x.
+      assert (bb_exit = bb_exit0).
+      { unfold schedule_oracle in *. simplify.
+        unfold check_control_flow_instr in *.
+        destruct_match; crush.
+      }
+      subst.
+
+      exploit abstract_execution_correct; try eassumption. eapply ge_preserved_lem.
+      econstructor; eauto.
+      inv_simp. destruct x. inv H7.
+
+      exploit step_cf_instr_correct; try eassumption. econstructor; eauto.
+      inv_simp.
+
+      econstructor. econstructor. eapply Smallstep.plus_one. econstructor.
+      eauto. eauto. simplify. eauto. eauto.
+    }
+    { unfold bind in *. inv TRANSL0. clear Learn. inv H0. destruct_match; crush.
+      inv H2. unfold transl_function in Heqr. destruct_match; crush.
+      inv Heqr. 
+      repeat econstructor; eauto.
+      unfold bind in *. destruct_match; crush.
     }
-    { unfold bind in *. destruct_match; try discriminate. repeat semantics_simpl. inv TRANSL0.
-      repeat econstructor; eauto. }
     { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. }
-    { inv STACKS. inv H2. repeat econstructor; eauto. }
-  Qed.*)
+    { inv STACKS. inv H2. repeat econstructor; eauto.
+      intros. apply PTree_matches; eauto.
+    }
+  Qed.
+
+  Lemma transl_initial_states:
+    forall S,
+      RTLBlock.initial_state prog S ->
+      exists R, RTLPar.initial_state tprog R /\ match_states S R.
+  Proof.
+    induction 1.
+    exploit function_ptr_translated; eauto. intros [tf [A B]].
+    econstructor; split.
+    econstructor. apply (Genv.init_mem_transf_partial TRANSL); eauto.
+    replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto.
+    symmetry; eapply match_program_main; eauto.
+    eexact A.
+    rewrite <- H2. apply sig_transl_function; auto.
+    constructor. auto. constructor.
+  Qed.
+
+  Lemma transl_final_states:
+    forall S R r,
+      match_states S R -> RTLBlock.final_state S r -> RTLPar.final_state R r.
+  Proof.
+    intros. inv H0. inv H. inv STACKS. constructor.
+  Qed.
+
+  Theorem transf_program_correct:
+    Smallstep.forward_simulation (RTLBlock.semantics prog) (RTLPar.semantics tprog).
+  Proof.
+    eapply Smallstep.forward_simulation_plus.
+    apply senv_preserved.
+    eexact transl_initial_states.
+    eexact transl_final_states.
+    exact transl_step_correct.
+  Qed.
 
 End CORRECTNESS.
 *)
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 9549947..679f5ec 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -202,9 +202,9 @@ Local Hint Resolve satLit_contra : core.
   obligations that it can't solve, or obligations that it takes 42 years to
   solve.
   However, if you think enough like me, each of the four definitions you fill in
-  should read like: [[
+  should read like:
 refine some_expression_with_holes; clear function_name; magic_solver.
-]] leaving out the [clear] invocation for non-recursive function definitions.
+ leaving out the [clear] invocation for non-recursive function definitions.
   *)
 Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder;
   match goal with
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
new file mode 100644
index 0000000..1052cb3
--- /dev/null
+++ b/src/hls/Schedule.ml
@@ -0,0 +1,814 @@
+(*
+ * Vericert: 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/>.
+ *)
+
+open Printf
+open Clflags
+open Camlcoq
+open Datatypes
+open Coqlib
+open Maps
+open AST
+open Kildall
+open Op
+open RTLBlockInstr
+open RTLBlock
+open HTL
+open Verilog
+open HTLgen
+open HTLMonad
+open HTLMonadExtra
+
+module SS = Set.Make(P)
+
+type svtype =
+  | BBType of int
+  | VarType of int * int
+
+type sv = {
+  sv_type: svtype;
+  sv_num: int;
+}
+
+let print_sv v =
+  match v with
+  | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n
+  | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n
+
+module G = Graph.Persistent.Digraph.ConcreteLabeled(struct
+  type t = sv
+  let compare = compare
+  let equal = (=)
+  let hash = Hashtbl.hash
+end)(struct
+  type t = int
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let default = 0
+end)
+
+module GDot = Graph.Graphviz.Dot(struct
+    let graph_attributes _ = []
+    let default_vertex_attributes _ = []
+    let vertex_name = print_sv
+    let vertex_attributes _ = []
+    let get_subgraph _ = None
+    let default_edge_attributes _ = []
+    let edge_attributes _ = []
+
+    include G
+  end)
+
+module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct
+  type t = int * instr
+  let compare = compare
+  let equal = (=)
+  let hash = Hashtbl.hash
+end)(struct
+  type t = int
+  let compare = compare
+  let hash = Hashtbl.hash
+  let equal = (=)
+  let default = 0
+end)
+
+let reg r = sprintf "r%d" (P.to_int r)
+let print_pred r = sprintf "p%d" (P.to_int r)
+
+let print_instr = function
+  | RBnop -> ""
+  | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r)
+  | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r)
+  | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p)
+  | RBop (_, op, args, d) ->
+    (match op, args with
+    | Omove, _ -> "mov"
+    | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n)
+    | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n)
+    | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n)
+    | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n)
+    | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id)
+    | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1)
+    | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1)
+    | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1)
+    | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1)
+    | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1)
+    | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2)
+    | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2)
+    | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2)
+    | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2)
+    | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2)
+    | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2)
+    | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2)
+    | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2)
+    | Oorimm n, [r1] ->  sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2)
+    | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1)
+    | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2)
+    | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2)
+    | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2)
+    | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n)
+    | Olea addr, args -> sprintf "%s=addr" (reg d)
+    | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1)
+    | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1)
+    | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1)
+    | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1)
+    | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1)
+    | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2)
+    | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2)
+    | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2)
+    | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2)
+    | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2)
+    | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2)
+    | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2)
+    | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2)
+    | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2)
+    | Oorlimm n, [r1] ->  sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2)
+    | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+    | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1)
+    | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2)
+    | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2)
+    | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2)
+    | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n)
+    | Oleal addr, args -> sprintf "%s=addr" (reg d)
+    | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1)
+    | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1)
+    | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2)
+    | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2)
+    | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2)
+    | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2)
+    | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1)
+    | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1)
+    | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2)
+    | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2)
+    | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2)
+    | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2)
+    | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1)
+    | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1)
+    | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1)
+    | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1)
+    | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1)
+    | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1)
+    | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1)
+    | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1)
+    | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1)
+    | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1)
+    | Ocmp c, args -> sprintf "%s=cmp" (reg d)
+    | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d)
+    | _, _ -> sprintf "N/a")
+
+module DFGDot = Graph.Graphviz.Dot(struct
+    let graph_attributes _ = []
+    let default_vertex_attributes _ = []
+    let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr)
+    let vertex_attributes _ = []
+    let get_subgraph _ = None
+    let default_edge_attributes _ = []
+    let edge_attributes _ = []
+
+    include DFG
+  end)
+
+module DFGDfs = Graph.Traverse.Dfs(DFG)
+
+module IMap = Map.Make (struct
+  type t = int
+
+  let compare = compare
+end)
+
+let gen_vertex instrs i = (i, List.nth instrs i)
+
+(** The DFG type defines a list of instructions with their data dependencies as [edges], which are
+   the pairs of integers that represent the index of the instruction in the [nodes].  The edges
+   always point from left to right. *)
+
+let print_list f out_chan a =
+  fprintf out_chan "[ ";
+  List.iter (fprintf out_chan "%a " f) a;
+  fprintf out_chan "]"
+
+let print_tuple out_chan a =
+  let l, r = a in
+  fprintf out_chan "(%d,%d)" l r
+
+(*let print_dfg out_chan dfg =
+  fprintf out_chan "{ nodes = %a, edges = %a }"
+    (print_list PrintRTLBlockInstr.print_bblock_body)
+    dfg.nodes (print_list print_tuple) dfg.edges*)
+
+let print_dfg = DFGDot.output_graph
+
+let read_process command =
+  let buffer_size = 2048 in
+  let buffer = Buffer.create buffer_size in
+  let string = Bytes.create buffer_size in
+  let in_channel = Unix.open_process_in command in
+  let chars_read = ref 1 in
+  while !chars_read <> 0 do
+    chars_read := input in_channel string 0 buffer_size;
+    Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read
+  done;
+  ignore (Unix.close_process_in in_channel);
+  Buffer.contents buffer
+
+let comb_delay = function
+  | RBnop -> 0
+  | RBop (_, op, _, _) ->
+    (match op with
+     | Omove -> 0
+     | Ointconst _ -> 0
+     | Olongconst _ -> 0
+     | Ocast8signed -> 0
+     | Ocast8unsigned -> 0
+     | Ocast16signed -> 0
+     | Ocast16unsigned -> 0
+     | Oneg -> 0
+     | Onot -> 0
+     | Oor -> 0
+     | Oorimm _ -> 0
+     | Oand -> 0
+     | Oandimm _ -> 0
+     | Oxor -> 0
+     | Oxorimm _ -> 0
+     | Omul -> 8
+     | Omulimm _ -> 8
+     | Omulhs -> 8
+     | Omulhu -> 8
+     | Odiv -> 72
+     | Odivu -> 72
+     | Omod -> 72
+     | Omodu -> 72
+     | _ -> 1)
+  | _ -> 1
+
+let pipeline_stages = function
+  | RBop (_, op, _, _) ->
+    (match op with
+     | Odiv -> 32
+     | Odivu -> 32
+     | Omod -> 32
+     | Omodu -> 32
+     | _ -> 0)
+  | _ -> 0
+
+(** Add a dependency if it uses a register that was written to previously. *)
+let add_dep map i tree dfg curr =
+  match PTree.get curr tree with
+  | None -> dfg
+  | Some ip ->
+    let ipv = (List.nth map ip) in
+    DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i)
+
+(** This function calculates the dependencies of each instruction.  The nodes correspond to previous
+   registers that were allocated and show which instruction caused it.
+
+   This function only gathers the RAW constraints, and will therefore only be active for operations
+   that modify registers, which is this case only affects loads and operations. *)
+let accumulate_RAW_deps map dfg curr =
+  let i, dst_map, graph = dfg in
+  let acc_dep_instruction rs dst =
+    ( i + 1,
+      PTree.set dst i dst_map,
+      List.fold_left (add_dep map i dst_map) graph rs
+    )
+  in
+  let acc_dep_instruction_nodst rs =
+    ( i + 1,
+      dst_map,
+    List.fold_left (add_dep map i dst_map) graph rs)
+  in
+  match curr with
+  | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst
+  | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst
+  | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs)
+  | _ -> (i + 1, dst_map, graph)
+
+(** Finds the next write to the [dst] register.  This is a small optimisation so that only one
+   dependency is generated for a data dependency. *)
+let rec find_next_dst_write i dst i' curr =
+  let check_dst dst' curr' =
+    if dst = dst' then Some (i, i')
+    else find_next_dst_write i dst (i' + 1) curr'
+  in
+  match curr with
+  | [] -> None
+  | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr'
+  | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr'
+  | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr'
+
+let rec find_all_next_dst_read i dst i' curr =
+  let check_dst rs curr' =
+    if List.exists (fun x -> x = dst) rs
+    then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr'
+    else find_all_next_dst_read i dst (i' + 1) curr'
+  in
+  match curr with
+  | [] -> []
+  | RBop (_, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
+  | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
+  | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
+  | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr'
+
+let drop i lst =
+  let rec drop' i' lst' =
+    match lst' with
+    | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls
+    | [] -> []
+  in
+  if i = 0 then lst else drop' 1 lst
+
+let take i lst =
+  let rec take' i' lst' =
+    match lst' with
+    | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls
+    | [] -> []
+  in
+  if i = 0 then [] else take' 1 lst
+
+let rec next_store i = function
+  | [] -> None
+  | RBstore (_, _, _, _, _) :: _ -> Some i
+  | _ :: rst -> next_store (i + 1) rst
+
+let rec next_load i = function
+  | [] -> None
+  | RBload (_, _, _, _, _) :: _ -> Some i
+  | _ :: rst -> next_load (i + 1) rst
+
+let accumulate_RAW_mem_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBload (_, _, _, _, _) -> (
+      match next_store 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAR_mem_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBstore (_, _, _, _, _) -> (
+      match next_load 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAW_mem_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBstore (_, _, _, _, _) -> (
+      match next_store 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+(** Predicate dependencies. *)
+
+let rec in_predicate p p' =
+  match p' with
+  | Pvar p'' -> P.to_int p = P.to_int p''
+  | Pnot p'' -> in_predicate p p''
+  | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
+  | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
+
+let get_predicate = function
+  | RBop (p, _, _, _) -> p
+  | RBload (p, _, _, _, _) -> p
+  | RBstore (p, _, _, _, _) -> p
+  | _ -> None
+
+let rec next_setpred p i = function
+  | [] -> None
+  | RBsetpred (_, _, p') :: rst ->
+    if in_predicate p' p then
+      Some i
+    else
+      next_setpred p (i + 1) rst
+  | _ :: rst -> next_setpred p (i + 1) rst
+
+let rec next_preduse p i instr=
+  let next p' rst =
+    if in_predicate p p' then
+      Some i
+    else
+      next_preduse p (i + 1) rst
+  in
+  match instr with
+  | [] -> None
+  | RBload (Some p', _, _, _, _) :: rst -> next p' rst
+  | RBstore (Some p', _, _, _, _) :: rst -> next p' rst
+  | RBop (Some p', _, _, _) :: rst -> next p' rst
+  | _ :: rst -> next_load (i + 1) rst
+
+let accumulate_RAW_pred_deps instrs dfg curri =
+  let i, curr = curri in
+  match get_predicate curr with
+  | Some p -> (
+      match next_setpred p 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAR_pred_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBsetpred (_, _, p) -> (
+      match next_preduse p 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+let accumulate_WAW_pred_deps instrs dfg curri =
+  let i, curr = curri in
+  match curr with
+  | RBsetpred (_, _, p) -> (
+      match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with
+      | None -> dfg
+      | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
+  | _ -> dfg
+
+(** This function calculates the WAW dependencies, which happen when two writes are ordered one
+   after another and therefore have to be kept in that order.  This accumulation might be redundant
+   if register renaming is done before hand, because then these dependencies can be avoided. *)
+let accumulate_WAW_deps instrs dfg curri =
+  let i, curr = curri in
+  let dst_dep dst =
+    match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with
+    | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b)
+    | _ -> dfg
+  in
+  match curr with
+  | RBop (_, _, _, dst) -> dst_dep dst
+  | RBload (_, _, _, _, dst) -> dst_dep dst
+  | RBstore (_, _, _, _, _) -> (
+      match next_store (i + 1) (drop (i + 1) instrs) with
+      | None -> dfg
+      | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') )
+  | _ -> dfg
+
+let accumulate_WAR_deps instrs dfg curri =
+  let i, curr = curri in
+  let dst_dep dst =
+    let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev)
+        |> List.map (function (d, d') -> (i - d' - 1, d))
+    in
+    List.fold_left (fun g ->
+        function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list
+  in
+  match curr with
+  | RBop (_, _, _, dst) -> dst_dep dst
+  | RBload (_, _, _, _, dst) -> dst_dep dst
+  | _ -> dfg
+
+let assigned_vars vars = function
+  | RBnop -> vars
+  | RBop (_, _, _, dst) -> dst :: vars
+  | RBload (_, _, _, _, dst) -> dst :: vars
+  | RBstore (_, _, _, _, _) -> vars
+  | RBsetpred (_, _, _) -> vars
+
+let get_pred = function
+  | RBnop -> None
+  | RBop (op, _, _, _) -> op
+  | RBload (op, _, _, _, _) -> op
+  | RBstore (op, _, _, _, _) -> op
+  | RBsetpred (_, _, _) -> None
+
+let independant_pred p p' =
+  match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with
+  | Some None -> true
+  | _ -> false
+
+let check_dependent op1 op2 =
+  match op1, op2 with
+  | Some p, Some p' -> not (independant_pred p p')
+  | _, _ -> true
+
+let remove_unnecessary_deps graph =
+  let is_dependent v1 v2 g =
+    let (_, instr1) = v1 in
+    let (_, instr2) = v2 in
+    if check_dependent (get_pred instr1) (get_pred instr2)
+    then g
+    else DFG.remove_edge g v1 v2
+  in
+  DFG.fold_edges is_dependent graph graph
+
+(** All the nodes in the DFG have to come after the source of the basic block, and should terminate
+   before the sink of the basic block.  After that, there should be constraints for data
+   dependencies between nodes. *)
+let gather_bb_constraints debug bb =
+  let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
+  let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in
+  let _, _, dfg' =
+    List.fold_left (accumulate_RAW_deps ibody)
+      (0, PTree.empty, dfg)
+      bb.bb_body
+  in
+  let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg'
+      [ accumulate_WAW_deps;
+        accumulate_WAR_deps;
+        accumulate_RAW_mem_deps;
+        accumulate_WAR_mem_deps;
+        accumulate_WAW_mem_deps;
+        accumulate_RAW_pred_deps;
+        accumulate_WAR_pred_deps;
+        accumulate_WAW_pred_deps
+      ]
+  in
+  let dfg''' = remove_unnecessary_deps dfg'' in
+  (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit)
+
+let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i }
+let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i }
+
+let add_super_nodes n dfg =
+  DFG.fold_vertex (function v1 -> fun g ->
+      (if DFG.in_degree dfg v1 = 0
+       then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0)
+       else g) |>
+      (fun g' ->
+         if DFG.out_degree dfg v1 = 0
+         then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1)
+         else g')) dfg
+
+let add_data_deps n =
+  DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g ->
+      G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0)
+    )
+
+let add_ctrl_deps n succs constr =
+  List.fold_left (fun g n' ->
+      G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0)
+    ) constr succs
+
+module BFDFG = Graph.Path.BellmanFord(DFG)(struct
+    include DFG
+    type t = int
+    let weight = DFG.E.label
+    let compare = compare
+    let add = (+)
+    let zero = 0
+  end)
+
+module TopoDFG = Graph.Topological.Make(DFG)
+
+let negate_graph constr =
+  DFG.fold_edges_e (function (v1, e, v2) -> fun g ->
+      DFG.add_edge_e g (v1, -e, v2)
+    ) constr DFG.empty
+
+let add_cycle_constr max n dfg constr =
+  let negated_dfg = negate_graph dfg in
+  let longest_path v = BFDFG.all_shortest_paths negated_dfg v
+                       |> BFDFG.H.to_seq |> List.of_seq in
+  let constrained_paths = List.filter (function (v, m) -> - m > max) in
+  List.fold_left (fun g -> function (v, v', w) ->
+      G.add_edge_e g (encode_var n (fst v) 0,
+                      - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1),
+                      encode_var n (fst v') 0)
+    ) constr (DFG.fold_vertex (fun v l ->
+      List.append l (longest_path v |> constrained_paths
+                     |> List.map (function (v', w) -> (v, v', - w)))
+    ) dfg [])
+
+type resource =
+  | Mem
+  | SDiv
+  | UDiv
+
+type resources = {
+  res_mem: DFG.V.t list;
+  res_udiv: DFG.V.t list;
+  res_sdiv: DFG.V.t list;
+}
+
+let find_resource = function
+  | RBload _ -> Some Mem
+  | RBstore _ -> Some Mem
+  | RBop (_, op, _, _) ->
+    ( match op with
+      | Odiv -> Some SDiv
+      | Odivu -> Some UDiv
+      | Omod -> Some SDiv
+      | Omodu -> Some UDiv
+      | _ -> None )
+  | _ -> None
+
+let add_resource_constr n dfg constr =
+  let res = TopoDFG.fold (function (i, instr) ->
+    function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r ->
+    match find_resource instr with
+    | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl}
+    | Some UDiv -> {r with res_udiv = (i, instr) :: udl}
+    | Some Mem -> {r with res_mem = (i, instr) :: ml}
+    | None -> r
+    ) dfg {res_mem = []; res_sdiv = []; res_udiv = []}
+  in
+  let get_constraints l g = List.fold_left (fun gv v' ->
+      match gv with
+      | (g, None) -> (g, Some v')
+      | (g, Some v) ->
+        (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v')
+    ) (g, None) l |> fst
+  in
+  get_constraints (List.rev res.res_mem) constr
+  |> get_constraints (List.rev res.res_udiv)
+  |> get_constraints (List.rev res.res_sdiv)
+
+let gather_cfg_constraints c constr curr =
+  let (n, dfg) = curr in
+  match PTree.get (P.of_int n) c with
+  | None -> assert false
+  | Some { bb_exit = ctrl; _ } ->
+    add_super_nodes n dfg constr
+    |> add_data_deps n dfg
+    |> add_ctrl_deps n (successors_instr ctrl
+                        |> List.map P.to_int
+                        |> List.filter (fun n' -> n' < n))
+    |> add_cycle_constr 8 n dfg
+    |> add_resource_constr n dfg
+
+let rec intersperse s = function
+  | [] -> []
+  | [ a ] -> [ a ]
+  | x :: xs -> x :: s :: intersperse s xs
+
+let print_objective constr =
+  let vars = G.fold_vertex (fun v1 l ->
+      match v1 with
+      | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l
+      | _ -> l
+    ) constr []
+  in
+  "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n"
+
+let print_lp constr =
+  print_objective constr ^
+  (G.fold_edges_e (function (e1, w, e2) -> fun s ->
+       s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w
+     ) constr "" |>
+   G.fold_vertex (fun v1 s ->
+       s ^ sprintf "int %s;\n" (print_sv v1)
+     ) constr)
+
+let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
+
+let parse_soln tree s =
+  let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in
+  if Str.string_match r s 0 then
+    IMap.update
+      (Str.matched_group 1 s |> int_of_string)
+      (update_schedule
+         ( Str.matched_group 2 s |> int_of_string,
+           Str.matched_group 3 s |> int_of_string ))
+      tree
+  else tree
+
+let solve_constraints constr =
+  let oc = open_out "lpsolve.txt" in
+  fprintf oc "%s\n" (print_lp constr);
+  close_out oc;
+
+  Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt")
+  |> drop 3
+  |> List.fold_left parse_soln IMap.empty
+
+let subgraph dfg l =
+  let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in
+  List.fold_left (fun g v ->
+      List.fold_left (fun g' v' ->
+          let edges = DFG.find_all_edges dfg v v' in
+          List.fold_left DFG.add_edge_e g' edges
+        ) g l
+    ) dfg' l
+
+let rec all_successors dfg v =
+  List.concat (List.fold_left (fun l v ->
+      all_successors dfg v :: l
+    ) [] (DFG.succ dfg v))
+
+let order_instr dfg =
+  DFG.fold_vertex (fun v li ->
+      if DFG.in_degree dfg v = 0
+      then (List.map snd (v :: all_successors dfg v)) :: li
+      else li
+    ) dfg []
+
+let combine_bb_schedule schedule s =
+  let i, st = s in
+  IMap.update st (update_schedule i) schedule
+
+(**let add_el dfg i l =
+  List.*)
+
+let all_dfs dfg =
+  let roots = DFG.fold_vertex (fun v li ->
+      if DFG.in_degree dfg v = 0 then v :: li else li
+    ) dfg [] in
+  List.map (fun r -> DFGDfs.fold_component (fun v l -> v :: l) [] dfg r) roots
+
+(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
+let transf_rtlpar c c' (schedule : (int * int) list IMap.t) =
+  let f i bb : RTLPar.bblock =
+    match bb with
+    | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c }
+    | { bb_body = bb_body'; bb_exit = ctrl_flow } ->
+      let dfg = match PTree.get i c' with None -> assert false | Some x -> x in
+      let i_sched = IMap.find (P.to_int i) schedule in
+      let i_sched_tree =
+        List.fold_left combine_bb_schedule IMap.empty i_sched
+      in
+      let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd
+                 |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
+      in
+      (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*)
+      let final_body2 = List.map (fun x -> subgraph dfg x
+                                           |> (fun x ->
+                                               all_dfs x
+                                               |> List.map (subgraph x)
+                                               |> List.map (fun y ->
+                                                   TopoDFG.fold (fun i l -> snd i :: l) y []
+                                                   |> List.rev))) body
+      in
+      { bb_body = final_body2;
+        bb_exit = ctrl_flow
+      }
+  in
+  PTree.map f c
+
+let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
+  let debug = true in
+  let transf_graph (_, dfg, _) = dfg in
+  let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in
+  (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg o) c' else PTree.empty in*)
+  let cgraph = PTree.elements c'
+               |> List.map (function (x, y) -> (P.to_int x, y))
+               |> List.fold_left (gather_cfg_constraints c) G.empty
+  in
+  let graph = open_out "constr_graph.dot" in
+  fprintf graph "%a\n" GDot.output_graph cgraph;
+  close_out graph;
+  let schedule' = solve_constraints cgraph in
+  (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
+  (**printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
+  transf_rtlpar c c' schedule'
+
+let rec find_reachable_states c e =
+  match PTree.get e c with
+  | Some { bb_exit = ex; _ } ->
+    e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) []
+      (successors_instr ex |> List.filter (fun x -> P.lt x e))
+  | None -> assert false
+
+let add_to_tree c nt i =
+  match PTree.get i c with
+  | Some p -> PTree.set i p nt
+  | None -> assert false
+
+let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
+  let scheduled = schedule f.fn_entrypoint f.fn_code in
+  let reachable = find_reachable_states scheduled f.fn_entrypoint
+                  |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in
+  { fn_sig = f.fn_sig;
+    fn_params = f.fn_params;
+    fn_stacksize = f.fn_stacksize;
+    fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable;
+    fn_entrypoint = f.fn_entrypoint
+  }
diff --git a/test/test_all.sh b/test/test_all.sh
index f072eba..2d78890 100755
--- a/test/test_all.sh
+++ b/test/test_all.sh
@@ -31,7 +31,7 @@ for cfile in $test_dir/*.c; do
     gcc -o $outbase.gcc $cfile >/dev/null 2>&1
     $outbase.gcc
     expected=$?
-    vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1
+    vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1
     if [[ ! -f $outbase.v ]]; then
         echo "ERROR"
         continue