Fix the top-level proofs with new state_match

1 files changed, 63 insertions, 19 deletions

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.