cleaning BTL_SEtheory

1 files changed, 73 insertions, 0 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 6f699cd0..bf19f4ac 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -540,6 +540,79 @@ Proof.
 Qed.
 *)
 
+(* * Reasoning modulo extensionality of [regset] into BTL semantics *)
+Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
+  | equiv_stackframe_intro res f sp pc rs1 rs2
+      (EQUIV: forall r : positive, rs1 !! r = rs2 !! r):
+      equiv_stackframe (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2)
+  .
+
+Inductive equiv_state: state -> state -> Prop :=
+  | State_equiv stack f sp pc rs1 m rs2
+     (EQUIV: forall r, rs1#r = rs2#r): 
+     equiv_state (State stack f sp pc rs1 m) (State stack f sp pc rs2 m)
+  | Call_equiv stk stk' f args m
+      (STACKS: list_forall2 equiv_stackframe stk stk'):
+      equiv_state (Callstate stk f args m) (Callstate stk' f args m)
+  | Return_equiv stk stk' v m
+      (STACKS: list_forall2 equiv_stackframe stk stk'):
+      equiv_state (Returnstate stk v m) (Returnstate stk' v m)
+  .
+
+Local Hint Constructors equiv_stackframe equiv_state: core.
+
+Lemma equiv_stackframe_refl stf: equiv_stackframe stf stf.
+Proof.
+  destruct stf; eauto.
+Qed.
+
+Lemma equiv_stack_refl stk: list_forall2 equiv_stackframe stk stk.
+Proof.
+  Local Hint Resolve equiv_stackframe_refl: core.
+  induction stk; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_state_refl s: equiv_state s s.
+Proof.
+  Local Hint Resolve equiv_stack_refl: core.
+  induction s; simpl; constructor; auto.
+Qed.
+
+Lemma equiv_stackframe_trans stf1 stf2 stf3:
+  equiv_stackframe stf1 stf2 -> equiv_stackframe stf2 stf3 -> equiv_stackframe stf1 stf3.
+Proof.
+  destruct 1; intros EQ; inv EQ; try econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma equiv_stack_trans stk1 stk2:
+  list_forall2 equiv_stackframe stk1 stk2 -> 
+  forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> 
+  list_forall2 equiv_stackframe stk1 stk3.
+Proof.
+  Local Hint Resolve equiv_stackframe_trans: core.
+  induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
+Qed.
+
+Lemma equiv_state_trans s1 s2 s3: equiv_state s1 s2 -> equiv_state s2 s3 -> equiv_state s1 s3.
+Proof.
+  Local Hint Resolve equiv_stack_trans: core.
+  destruct 1; intros EQ; inv EQ; econstructor; eauto.
+  intros; eapply eq_trans; eauto.
+Qed.
+
+Lemma regmap_setres_eq (rs rs': regset) res vres:
+  (forall r, rs # r = rs' # r) ->
+  forall r, (regmap_setres res vres rs) # r = (regmap_setres res vres rs') # r.
+Proof.
+  intros RSEQ r. destruct res; simpl; try congruence.
+  destruct (peq x r).
+  - subst. repeat (rewrite Regmap.gss). reflexivity.
+  - repeat (rewrite Regmap.gso); auto.
+Qed.
+
+
+
 (** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *)
 
 (** Matching BTL and RTL code