Rearrange definitions and create IfConversion template

1 files changed, 197 insertions, 0 deletions

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.