Rearrange definitions and create IfConversion template

6 files changed, 301 insertions, 105 deletions

diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v
index 4369d5a..f4362d7 100644
--- a/src/hls/CondElimproof.v
+++ b/src/hls/CondElimproof.v
@@ -42,57 +42,6 @@ Require Import vericert.hls.Predicate.
 
 #[local] Open Scope positive.
 
-Lemma forbidden_term_trans :
-  forall A B ge sp i c b i' c',
-    ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c').
-Proof. induction b; unfold not; intros; inv H. Qed.
-
-Lemma step_instr_false :
-  forall A B ge sp i c a i0,
-    ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0).
-Proof. destruct a; unfold not; intros; inv H. Qed.
-
-Lemma step_list2_false :
-  forall A B ge l0 sp i c i0',
-    ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0').
-Proof.
-  induction l0; unfold not; intros.
-  inv H. inv H. destruct i1. eapply step_instr_false in H4. auto.
-  eapply IHl0; eauto.
-Qed.
-
-Lemma append' :
-  forall A B l0 cf i0 i1 l1 sp ge i0',
-    step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') ->
-    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf) ->
-    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
-Proof.
-  induction l0; crush. inv H. eauto. inv H. destruct i3.
-  econstructor; eauto. eapply IHl0; eauto.
-  eapply step_list2_false in H7. exfalso; auto.
-Qed.
-
-Lemma append :
-  forall A B cf i0 i1 l0 l1 sp ge,
-      (exists i0', step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') /\
-                    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
-    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
-Proof. intros. simplify. eapply append'; eauto. Qed.
-
-Lemma append2 :
-  forall A B l0 cf i0 i1 l1 sp ge,
-    @SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) ->
-    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
-Proof.
-  induction l0; crush.
-  inv H.
-  inv H. econstructor; eauto. eapply IHl0; eauto.
-  constructor; auto.
-Qed.
-
-Definition to_cf c :=
-  match c with | Iterm _ cf => Some cf | _ => None end.
-
 #[local] Notation "'mki'" := (mk_instr_state) (at level 1).
 
 Variant match_ps : positive -> predset -> predset -> Prop :=
@@ -145,18 +94,6 @@ Lemma eval_pred_eq_predset :
     ps' = ps.
 Proof. inversion 1; subst; crush. Qed.
 
-Lemma predicate_lt :
-  forall p p0,
-    In p0 (predicate_use p) -> p0 <= max_predicate p.
-Proof.
-  induction p; crush.
-  - destruct_match. inv H; try lia; contradiction.
-  - eapply Pos.max_le_iff.
-    eapply in_app_or in H. inv H; eauto.
-  - eapply Pos.max_le_iff.
-    eapply in_app_or in H. inv H; eauto.
-Qed.
-
 Lemma truthy_match_ps :
   forall v ps tps p,
     truthy ps p ->
@@ -180,11 +117,6 @@ Proof.
   inv H2; auto.
 Qed.
 
-Ltac truthy_falsy :=
-  match goal with
-  | H1: truthy _ _, H2: instr_falsy _ _ |- _ => inv H1; inv H2; solve [crush]
-  end.
-
 Lemma elim_cond_s_spec :
   forall A B ge sp rs m rs' m' ps tps ps' p a p0 l v,
     step_instr ge sp (Iexec (mki rs ps m)) a (Iexec (mki rs' ps' m')) ->
@@ -506,18 +438,6 @@ Section CORRECTNESS.
       repeat (econstructor; eauto).
   Qed.
 
-  Lemma step_cf_instr_det :
-    forall ge st cf t st1 st2,
-      step_cf_instr ge st cf t st1 ->
-      step_cf_instr ge st cf t st2 ->
-      st1 = st2.
-  Proof using TRANSL.
-    inversion 1; subst; simplify; clear H;
-      match goal with H: context[step_cf_instr] |- _ => inv H end; crush;
-    assert (vargs0 = vargs) by eauto using eval_builtin_args_determ; subst;
-    assert (vres = vres0 /\ m' = m'0) by eauto using external_call_deterministic; crush.
-  Qed.
-
   Lemma step_list2_ge :
     forall sp l i i',
       step_list2 (step_instr ge) sp i l i' ->
@@ -539,14 +459,6 @@ Section CORRECTNESS.
     - eauto using exec_RBterm, step_instr_ge.
   Qed.
 
-  Lemma max_pred_function_use :
-    forall f pc bb i p,
-      f.(fn_code) ! pc = Some bb ->
-      In i bb ->
-      In p (pred_uses i) ->
-      p <= max_pred_function f.
-  Proof. Admitted.
-
   Lemma elim_cond_s_wf_predicate :
     forall a p p0 l v,
       elim_cond_s p a = (p0, l) ->
diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index 4cecd2c..399935b 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -549,6 +549,18 @@ support if-conversion.
         step_cf_instr (State s f sp pc rs pr m)
                       (RBgoto pc') E0 (State s f sp pc' rs pr m).
 
+    Lemma step_cf_instr_det :
+      forall st cf t st1 st2,
+        step_cf_instr st cf t st1 ->
+        step_cf_instr st cf t st2 ->
+        st1 = st2.
+    Proof using.
+      inversion 1; subst; simplify; clear H;
+        match goal with H: context[step_cf_instr] |- _ => inv H end; crush;
+        assert (vargs0 = vargs) by eauto using eval_builtin_args_determ; subst;
+        assert (vres = vres0 /\ m' = m'0) by eauto using external_call_deterministic; crush.
+    Qed.
+
 (*|
 Top-level step
 --------------
diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v
index e66451d..acc47ed 100644
--- a/src/hls/GibleSeq.v
+++ b/src/hls/GibleSeq.v
@@ -28,6 +28,7 @@ Require Import compcert.lib.Integers.
 Require Import compcert.lib.Maps.
 Require Import compcert.verilog.Op.
 
+Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.Gible.
 
 (*|
@@ -71,3 +72,61 @@ Fixpoint replace_section {A: Type} (f: A -> instr -> (A * SeqBB.t)) (s: A) (b: S
       (s'', i' ++ b'')
   | nil => (s, nil)
   end.
+
+Lemma forbidden_term_trans :
+  forall A B ge sp i c b i' c',
+    ~ @SeqBB.step A B ge sp (Iterm i c) b (Iterm i' c').
+Proof. induction b; unfold not; intros; inv H. Qed.
+
+Lemma step_instr_false :
+  forall A B ge sp i c a i0,
+    ~ @step_instr A B ge sp (Iterm i c) a (Iexec i0).
+Proof. destruct a; unfold not; intros; inv H. Qed.
+
+Lemma step_list2_false :
+  forall A B ge l0 sp i c i0',
+    ~ step_list2 (@step_instr A B ge) sp (Iterm i c) l0 (Iexec i0').
+Proof.
+  induction l0; unfold not; intros.
+  inv H. inv H. destruct i1. eapply step_instr_false in H4. auto.
+  eapply IHl0; eauto.
+Qed.
+
+Lemma append' :
+  forall A B l0 cf i0 i1 l1 sp ge i0',
+    step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') ->
+    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf) ->
+    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
+Proof.
+  induction l0; crush. inv H. eauto. inv H. destruct i3.
+  econstructor; eauto. eapply IHl0; eauto.
+  eapply step_list2_false in H7. exfalso; auto.
+Qed.
+
+Lemma append :
+  forall A B cf i0 i1 l0 l1 sp ge,
+      (exists i0', step_list2 (@step_instr A B ge) sp (Iexec i0) l0 (Iexec i0') /\
+                    @SeqBB.step A B ge sp (Iexec i0') l1 (Iterm i1 cf)) ->
+    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
+Proof. intros. simplify. eapply append'; eauto. Qed.
+
+Lemma append2 :
+  forall A B l0 cf i0 i1 l1 sp ge,
+    @SeqBB.step A B ge sp (Iexec i0) l0 (Iterm i1 cf) ->
+    @SeqBB.step A B ge sp (Iexec i0) (l0 ++ l1) (Iterm i1 cf).
+Proof.
+  induction l0; crush.
+  inv H.
+  inv H. econstructor; eauto. eapply IHl0; eauto.
+  constructor; auto.
+Qed.
+
+#[local] Open Scope positive.
+
+Lemma max_pred_function_use :
+  forall f pc bb i p,
+    f.(fn_code) ! pc = Some bb ->
+    In i bb ->
+    In p (pred_uses i) ->
+    p <= max_pred_function f.
+Proof. Admitted.
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 961182c..7f6b59e 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -1,20 +1,24 @@
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2021-2022 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/>.
+
+.. coq:: none
+|*)
+
 
 Require Import Coq.Structures.Orders.
 Require Import Coq.Sorting.Mergesort.
diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v
new file mode 100644
index 0000000..b8ed617
--- /dev/null
+++ b/src/hls/IfConversionproof.v
@@ -0,0 +1,197 @@
+(*|
+..
+   Vericert: Verified high-level synthesis.
+   Copyright (C) 2022 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/>.
+
+===================
+If Conversion Proof
+===================
+
+.. coq:: none
+|*)
+
+Require Import compcert.common.AST.
+Require Import compcert.common.Errors.
+Require Import compcert.common.Globalenvs.
+Require Import compcert.lib.Maps.
+Require Import compcert.backend.Registers.
+Require Import compcert.common.Smallstep.
+Require Import compcert.common.Events.
+Require Import compcert.common.Memory.
+Require Import compcert.common.Values.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.common.DecEq.
+Require Import vericert.hls.Gible.
+Require Import vericert.hls.GibleSeq.
+Require Import vericert.hls.IfConversion.
+Require Import vericert.hls.Predicate.
+
+#[local] Open Scope positive.
+#[local] Notation "'mki'" := (mk_instr_state) (at level 1).
+
+Variant match_stackframe : stackframe -> stackframe -> Prop :=
+  | match_stackframe_init :
+    forall res f tf sp pc rs p
+           (TF: transf_function f = tf),
+      match_stackframe (Stackframe res f sp pc rs p) (Stackframe res tf sp pc rs p).
+
+Variant match_states : state -> state -> Prop :=
+  | match_state :
+    forall stk stk' f tf sp pc rs p m
+           (TF: transf_function f = tf)
+           (STK: Forall2 match_stackframe stk stk'),
+      match_states (State stk f sp pc rs p m) (State stk' tf sp pc rs p m)
+  | match_callstate :
+    forall cs cs' f tf args m
+           (TF: transf_fundef f = tf)
+           (STK: Forall2 match_stackframe cs cs'),
+      match_states (Callstate cs f args m) (Callstate cs' tf args m)
+  | match_returnstate :
+    forall cs cs' v m
+           (STK: Forall2 match_stackframe cs cs'),
+      match_states (Returnstate cs v m) (Returnstate cs' v m).
+
+Definition match_prog (p: program) (tp: program) :=
+  Linking.match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+
+Section CORRECTNESS.
+
+  Context (prog tprog : program).
+
+  Let ge : genv := Globalenvs.Genv.globalenv prog.
+  Let tge : genv := Globalenvs.Genv.globalenv tprog.
+
+  Context (TRANSL : match_prog prog tprog).
+
+    Lemma symbols_preserved:
+    forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+
+  Lemma senv_preserved:
+    Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+  Proof using TRANSL. intros; eapply (Genv.senv_transf TRANSL). Qed.
+
+  Lemma function_ptr_translated:
+    forall b f,
+      Genv.find_funct_ptr ge b = Some f ->
+      Genv.find_funct_ptr tge b = Some (transf_fundef f).
+  Proof (Genv.find_funct_ptr_transf TRANSL).
+
+  Lemma sig_transf_function:
+    forall (f tf: fundef),
+      funsig (transf_fundef f) = funsig f.
+  Proof using.
+    unfold transf_fundef. unfold AST.transf_fundef; intros. destruct f.
+    unfold transf_function. destruct_match; auto. auto.
+  Qed.
+
+  Lemma functions_translated:
+    forall (v: Values.val) (f: GibleSeq.fundef),
+      Genv.find_funct ge v = Some f ->
+      Genv.find_funct tge v = Some (transf_fundef f).
+  Proof using TRANSL.
+    intros. exploit (Genv.find_funct_match TRANSL); eauto. simplify. eauto.
+  Qed.
+
+  Lemma find_function_translated:
+    forall ros rs f,
+      find_function ge ros rs = Some f ->
+      find_function tge ros rs = Some (transf_fundef f).
+  Proof using TRANSL.
+    Ltac ffts := match goal with
+                 | [ H: forall _, Val.lessdef _ _, r: Registers.reg |- _ ] =>
+                     specialize (H r); inv H
+                 | [ H: Vundef = ?r, H1: Genv.find_funct _ ?r = Some _ |- _ ] =>
+                     rewrite <- H in H1
+                 | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H]
+                 | _ => solve [exploit functions_translated; eauto]
+                 end.
+    destruct ros; simplify; try rewrite <- H;
+      [| rewrite symbols_preserved; destruct_match;
+         try (apply function_ptr_translated); crush ];
+      intros;
+      repeat ffts.
+  Qed.
+
+  Lemma transf_initial_states :
+    forall s1,
+      initial_state prog s1 ->
+      exists s2, initial_state tprog s2 /\ match_states s1 s2.
+  Proof using TRANSL.
+    induction 1.
+    exploit function_ptr_translated; eauto; intros.
+    do 2 econstructor; simplify. econstructor.
+    apply (Genv.init_mem_transf TRANSL); eauto.
+    replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto.
+    symmetry; eapply Linking.match_program_main; eauto. eauto.
+    erewrite sig_transf_function; eauto. constructor. auto. auto.
+  Qed.
+
+  Lemma transf_final_states :
+    forall s1 s2 r,
+      match_states s1 s2 -> final_state s1 r -> final_state s2 r.
+  Proof using.
+    inversion 2; crush. subst. inv H. inv STK. econstructor.
+  Qed.
+
+  Lemma eval_op_eq:
+    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;
+    [| destruct a; unfold Genv.symbol_address ];
+    try rewrite symbols_preserved; auto.
+  Qed.
+
+  Lemma eval_addressing_eq:
+    forall sp addr vl,
+      Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl.
+  Proof using TRANSL.
+    intros.
+    destruct addr;
+      unfold Op.eval_addressing, Op.eval_addressing32;
+      unfold Genv.symbol_address;
+      try rewrite symbols_preserved; auto.
+  Qed.
+
+  #[local] Hint Resolve eval_builtin_args_preserved : core.
+  #[local] Hint Resolve symbols_preserved : core.
+  #[local] Hint Resolve external_call_symbols_preserved : core.
+  #[local] Hint Resolve senv_preserved : core.
+  #[local] Hint Resolve find_function_translated : core.
+  #[local] Hint Resolve sig_transf_function : core.
+
+  Lemma transf_step_correct:
+    forall (s1 : state) (t : trace) (s1' : state),
+      step ge s1 t s1' ->
+      forall s2 : state,
+        match_states s1 s2 ->
+        exists s2' : state, step tge s2 t s2' /\ match_states s1' s2'.
+  Proof using TRANSL. Admitted.
+
+  Theorem transf_program_correct:
+    forward_simulation (semantics prog) (semantics tprog).
+  Proof using TRANSL.
+    eapply forward_simulation_step.
+    + apply senv_preserved.
+    + apply transf_initial_states.
+    + apply transf_final_states.
+    + apply transf_step_correct.
+  Qed.
+
+End CORRECTNESS.
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index 7a4ed60..b9333d9 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -697,3 +697,15 @@ Definition combine_pred (p1 p2: option pred_op): option pred_op :=
   | Some p, _ | _, Some p => Some p
   | None, None => None
   end.
+
+Lemma predicate_lt :
+  forall p p0,
+    In p0 (predicate_use p) -> p0 <= max_predicate p.
+Proof.
+  induction p; crush.
+  - destruct_match. inv H; try lia; contradiction.
+  - eapply Pos.max_le_iff.
+    eapply in_app_or in H. inv H; eauto.
+  - eapply Pos.max_le_iff.
+    eapply in_app_or in H. inv H; eauto.
+Qed.