Fix definitions of proofs some more

4 files changed, 162 insertions, 106 deletions

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 2744527..90edc2e 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -202,16 +202,6 @@ Section RELSEM.
                  (RBstore chunk addr args src)
                  (InstrState rs m').
 
-  Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
-    | exec_RBcons:
-        forall state i state' state'' instrs sp,
-        step_instr sp state i state' ->
-        step_instr_list sp state' instrs state'' ->
-        step_instr_list sp state (i :: instrs) state''
-    | exec_RBnil:
-        forall state sp,
-        step_instr_list sp state nil state.
-
   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',
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 3ad54f5..be9ff22 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -46,11 +46,21 @@ Section RELSEM.
 
   Context (ge: genv).
 
+  Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
+    | exec_RBcons:
+        forall state i state' state'' instrs sp,
+        step_instr ge sp state i state' ->
+        step_instr_list sp state' instrs state'' ->
+        step_instr_list sp state (i :: instrs) state''
+    | exec_RBnil:
+        forall state sp,
+        step_instr_list sp state nil state.
+
   Inductive step_instr_block (sp : val)
     : instr_state -> bb -> instr_state -> Prop :=
   | exec_instr_block_cons:
     forall state i state' state'' instrs,
-      step_instr_list ge sp state i state' ->
+      step_instr_list sp state i state' ->
       step_instr_block sp state' instrs state'' ->
       step_instr_block sp state (i :: instrs) state''
   | exec_instr_block_nil:
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 4fdd308..7acf6d2 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require compcert.backend.Registers.
+Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Globalenvs.
 Require compcert.common.Memory.
@@ -449,19 +449,34 @@ Lemma tri1:
   Reg x <> Reg y -> x <> y.
 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 addr vl, Op.eval_addressing ge sp addr vl =
+                         Op.eval_addressing tge sp addr vl).
+
+Lemma ge_preserved_same:
+  forall A B ge, @ge_preserved A B A B ge ge.
+Proof. unfold ge_preserved; auto. Qed.
+Hint Resolve ge_preserved_same : rtlpar.
+
+Definition reg_lessdef (rs rs': regset) := forall x, rs !! x = rs' !! x.
+
+Lemma regs_lessdef_regs:
+  forall rs1 rs2, reg_lessdef rs1 rs2 ->
+  forall rl, rs1##rl = rs2##rl.
+Proof. induction rl; crush. Qed.
+
 Inductive sem_state_ld : sem_state -> sem_state -> Prop :=
 | sem_state_ld_intro:
   forall rs rs' m m',
-    (forall x, rs !! x = rs' !! x) ->
+    reg_lessdef rs rs' ->
     m = m' ->
     sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m').
 
 Lemma sems_det:
   forall A ge tge sp st f,
-  (forall sp op vl, Op.eval_operation ge sp op vl =
-                    Op.eval_operation tge sp op vl) ->
-  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
-                      Op.eval_addressing tge sp addr vl) ->
+  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').
@@ -469,19 +484,17 @@ Proof. Admitted.
 
 Lemma sem_value_det:
   forall A ge tge sp st f v v',
-  (forall sp op vl, Op.eval_operation ge sp op vl =
-                    Op.eval_operation tge sp op vl) ->
-  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
-                      Op.eval_addressing tge sp addr vl) ->
+  ge_preserved ge tge ->
   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 H0 v v'
+  generalize (sems_det A ge tge sp st f H v v'
                       st.(sem_state_memory) st.(sem_state_memory));
   crush.
 Qed.
+Hint Resolve sem_value_det : rtlpar.
 
 Lemma sem_value_det':
   forall FF ge sp s f v v',
@@ -489,75 +502,64 @@ Lemma sem_value_det':
   sem_value FF ge sp s f v' ->
   v = v'.
 Proof.
-  simplify; eauto using sem_value_det.
+  simplify; eauto with rtlpar.
 Qed.
 
 Lemma sem_mem_det:
   forall A ge tge sp st f m m',
-  (forall sp op vl, Op.eval_operation ge sp op vl =
-                    Op.eval_operation tge sp op vl) ->
-  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
-                      Op.eval_addressing tge sp addr vl) ->
+  ge_preserved ge tge ->
   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 H0 sp sp m m');
+  generalize (sems_det A ge tge sp st 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' ->
-  m = m'.
+    sem_mem FF ge sp s f m ->
+    sem_mem FF ge sp s f m' ->
+    m = m'.
 Proof.
-  simplify; eauto using sem_mem_det.
+  simplify; eauto with rtlpar.
 Qed.
 
 Lemma sem_regset_det:
   forall FF ge tge sp st f v v',
-  (forall sp op vl, Op.eval_operation ge sp op vl =
-                    Op.eval_operation tge sp op vl) ->
-  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
-                      Op.eval_addressing tge sp addr vl) ->
-  sem_regset FF ge sp st f v ->
-  sem_regset FF tge sp st f v' ->
-  (forall x, v !! x = v' !! x).
+    ge_preserved ge tge ->
+    sem_regset FF ge sp st f v ->
+    sem_regset FF tge sp st f v' ->
+    reg_lessdef v v'.
 Proof.
-  intros.
-  inversion H1; subst. inversion H2; subst.
-  generalize (H3 x); intro. generalize (H4 x); intro.
-  eapply sem_value_det; eauto.
+  intros; unfold reg_lessdef;
+  inv H0; inv H1;
+  eauto with rtlpar.
 Qed.
-
-Hint Resolve sem_value_det : rtlpar.
-Hint Resolve sem_mem_det : rtlpar.
 Hint Resolve sem_regset_det : rtlpar.
 
 Lemma sem_det:
   forall FF ge tge sp st f st' st'',
-  (forall sp op vl, Op.eval_operation ge sp op vl =
-                    Op.eval_operation tge sp op vl) ->
-  (forall sp addr vl, Op.eval_addressing ge sp addr vl =
-                      Op.eval_addressing tge sp addr vl) ->
-  sem FF ge sp st f st' ->
-  sem FF tge sp st f st'' ->
-  sem_state_ld 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''.
 Proof.
   intros.
   destruct st; destruct st'; destruct st''.
-  inv H1; inv H2.
+  inv H0; inv H1.
   constructor; eauto with rtlpar.
 Qed.
+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''.
-Proof. eauto using sem_det. Qed.
+Proof. eauto with rtlpar. Qed.
 
 (*|
 Update functions.
@@ -660,9 +662,11 @@ Abstract computations
 
 Lemma abstract_execution_correct:
   forall bb bb' cfi ge tge sp rs m rs' m',
-  schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
-  @step_instr_list RTLBlock.fundef ge sp (InstrState rs m) bb (InstrState rs' m') ->
-  step_instr_block tge sp (InstrState rs m) bb' (InstrState rs' m').
+    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')
+                 /\ reg_lessdef rs' rs''.
 Proof. Admitted.
 
 (*|
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.