Fix definitions of proofs some more

1 files changed, 100 insertions, 48 deletions

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 157d734..01d4542 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,6 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
+Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
 Require Import compcert.common.Linking.
@@ -33,24 +34,26 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
 
 Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
 | match_stackframe:
-    forall f tf res sp pc rs,
+    forall f tf res sp pc rs rs',
       transl_function f = OK tf ->
+      reg_lessdef rs rs' ->
       match_stackframes (Stackframe res f sp pc rs)
-                        (Stackframe res tf 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 mem sf' tf
+    forall sf f sp pc rs rs' mem sf' tf
       (TRANSL: transl_function f = OK tf)
-      (STACKS: list_forall2 match_stackframes sf sf'),
+      (STACKS: list_forall2 match_stackframes sf sf')
+      (REG: reg_lessdef rs rs'),
       match_states (State sf f sp pc rs mem)
-                   (State sf' tf sp pc rs mem)
+                   (State sf' tf sp pc rs' mem)
 | match_returnstate:
     forall stack stack' v mem
       (STACKS: list_forall2 match_stackframes stack stack'),
       match_states (Returnstate stack v mem)
                    (Returnstate stack' v mem)
-| match_initial_call:
+| match_callstate:
     forall stack stack' f tf args m
       (TRANSL: transl_fundef f = OK tf)
       (STACKS: list_forall2 match_stackframes stack stack'),
@@ -67,14 +70,15 @@ Section CORRECTNESS.
 
   Lemma symbols_preserved:
     forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-  Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed.
+  Hint Resolve symbols_preserved : rtlgp.
 
   Lemma function_ptr_translated:
     forall (b: Values.block) (f: RTLBlock.fundef),
       Genv.find_funct_ptr ge b = Some f ->
       exists tf,
         Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
-  Proof.
+  Proof using TRANSL.
     intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
@@ -84,7 +88,7 @@ Section CORRECTNESS.
       Genv.find_funct ge v = Some f ->
       exists tf,
         Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
-  Proof.
+  Proof using TRANSL.
     intros. exploit (Genv.find_funct_match TRANSL); eauto.
     intros (cu & tf & P & Q & R); exists tf; auto.
   Qed.
@@ -92,24 +96,27 @@ Section CORRECTNESS.
   Lemma senv_preserved:
     Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
   Proof (Genv.senv_transf_partial TRANSL).
+  Hint Resolve senv_preserved : rtlgp.
 
   Lemma sig_transl_function:
     forall (f: RTLBlock.fundef) (tf: RTLPar.fundef),
       transl_fundef f = OK tf ->
       funsig tf = funsig f.
-  Proof.
+  Proof using .
     unfold transl_fundef, transf_partial_fundef, transl_function; intros;
     repeat destruct_match; crush;
     match goal with H: OK _ = OK _ |- _ => inv H end; auto.
   Qed.
+  Hint Resolve sig_transl_function : rtlgp.
 
   Lemma find_function_translated:
-    forall ros rs f,
+    forall ros rs rs' f,
+      reg_lessdef rs rs' ->
       find_function ge ros rs = Some f ->
-      exists tf, find_function tge ros rs = Some tf
+      exists tf, find_function tge ros rs' = Some tf
                  /\ transl_fundef f = OK tf.
-  Proof.
-    destruct ros; simplify;
+  Proof using TRANSL.
+    unfold reg_lessdef; destruct ros; simplify; try rewrite <- H;
     [ exploit functions_translated; eauto
     | rewrite symbols_preserved; destruct_match;
       try (apply function_ptr_translated); crush ].
@@ -119,7 +126,7 @@ Section CORRECTNESS.
     forall bb cfi,
       schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true ->
       bb_body bb = nil /\ bb_exit bb = cfi.
-  Proof.
+  Proof using .
     unfold schedule_oracle, check_control_flow_instr.
     simplify; repeat destruct_match; crush.
   Qed.
@@ -128,17 +135,74 @@ Section CORRECTNESS.
     forall cfi,
       schedule_oracle {| bb_body := nil; bb_exit := cfi |}
                       {| bb_body := nil; bb_exit := cfi |} = true.
-  Proof.
+  Proof using .
     unfold schedule_oracle, check_control_flow_instr.
     simplify; repeat destruct_match; crush.
   Qed.
 
-  Lemma schedule_sem_correct:
-    forall bb bb' cfi sp rs m rs' m',
-      schedule_oracle {| bb_body := bb; bb_exit := cfi |} {| bb_body := bb'; bb_exit := cfi |} = true ->
-      step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') ->
-      step_instr_block tge sp (InstrState rs m) bb' (InstrState rs' m').
-  Proof. Admitted.
+  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.
+  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.
+  Hint Resolve eval_op_eq : rtlgp.
+
+  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.
+  Hint Resolve eval_addressing_eq : rtlgp.
+
+  Ltac semantics_simpl :=
+    match goal with
+    | [ H: match_states _ _ |- _ ] =>
+      let H2 := fresh "H" in
+      learn H as H2; inv H2
+    | [ H: transl_function ?f = OK _ |- _ ] =>
+      let H2 := fresh "TRANSL" in
+      learn H as H2;
+      unfold transl_function in H2;
+      destruct (check_scheduled_trees (@fn_code RTLBlock.bb f) (@fn_code RTLPar.bb (schedule f))) eqn:?;
+               [| discriminate ]; inv H2
+    | [ H: context[check_scheduled_trees] |- _ ] =>
+      let H2 := fresh "CHECK" in
+      learn H as H2;
+      eapply check_scheduled_trees_correct in H2; [| solve [eauto] ]
+    | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] =>
+      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: exists _, _ |- _ ] => inv H
+    | _ => progress simplify
+    end.
+
+  Hint Resolve Events.eval_builtin_args_preserved : rtlgp.
+  Hint Resolve Events.external_call_symbols_preserved : rtlgp.
+
+  Lemma step_cf_instr_correct:
+    forall cfi t s s',
+      step_cf_instr ge s cfi t s' ->
+      forall r,
+        match_states s r ->
+        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. }
+    repeat econstructor; eauto with rtlgp.
+  Qed.
 
   Theorem transl_step_correct :
     forall (S1 : RTLBlock.state) t S2,
@@ -147,32 +211,20 @@ Section CORRECTNESS.
         match_states S1 R1 ->
         exists R2, Smallstep.plus RTLPar.step tge R1 t R2 /\ match_states S2 R2.
   Proof.
-    Ltac t :=
-      match goal with
-      | [ H: context[match_states _ _] |- _ ] => inv H
-      | [ H: transl_function ?f = OK _ |- _ ] =>
-        let H2 := fresh "TRANSL" in
-        learn H as H2;
-        unfold transl_function in H2;
-        destruct (check_scheduled_trees (fn_code f) (fn_code (schedule f))) eqn:?;
-                 [| discriminate ]; inv H2
-      | [ H: context[check_scheduled_trees] |- _ ] =>
-        let H2 := fresh "CHECK" in
-        learn H as H2;
-        eapply check_scheduled_trees_correct in H2; [| solve [eauto] ]
-      | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] =>
-        let H2 := fresh "SCHED" in
-        learn H as H2;
-        apply schedule_oracle_nil in H2
-      | [ H: exists _, _ |- _ ] => inv H
-      | _ => progress simplify
-      end.
-
-    induction 1; repeat t.
-
-    admit.
-    { unfold bind in *. destruct_match; try discriminate. repeat t. inv TRANSL0.
+
+    induction 1; repeat semantics_simpl.
+
+    { 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.
+    } step_instr_block ?tge@{bbe:=bbe'; bbe':=bbe'} sp (InstrState rs m) bbc' (InstrState x m')
+  H5 : reg_lessdef rs' x
+                   RTLBlock.step_instr_list ge sp (InstrState rs m) bbc (InstrState rs' m')
+    { 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 H1. repeat econstructor; eauto. }
+    { inv STACKS. inv H2. repeat econstructor; eauto. }
   Qed.