add all the easy-to-prove semantics relations

bedrock2/src/bedrock2/FE310CSemantics.v

@@ -1,5 +1,6 @@
 Require Import Coq.ZArith.ZArith.
-Require Import bedrock2.Syntax bedrock2.Semantics bedrock2.LeakageSemantics bedrock2.MetricLeakageSemantics.
+Require Import bedrock2.Syntax bedrock2.Semantics bedrock2.LeakageSemantics.
+Require Import bedrock2.SemanticsRelations.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Import coqutil.Word.Interface.
 Require Export coqutil.Word.Bitwidth32.

bedrock2/src/bedrock2/MetricLeakageSemantics.v

@@ -546,173 +546,4 @@ Section WithParams.
     - eassumption.
     - eapply exec.extend_env; eassumption.
   Qed.
-
-  Lemma to_plain_eval_expr: forall m l e v,
-      Semantics.eval_expr m l e = Some v ->
-      forall k mc, exists k' mc', eval_expr m l e k mc = Some (v, k', mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _ _, Semantics.eval_expr _ _ _ = Some _ -> _ |- _ =>
-            specialize (IH _ _ ltac:(eassumption))
-        | IH: forall _: leakage, forall _: MetricLog, exists _: leakage, exists _: MetricLog,
-            eval_expr ?m ?l ?e _ _ = Some _
-          |- context[eval_expr ?m ?l ?e ?k ?mc] => specialize (IH k mc)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_metric_eval_expr: forall m l e mc v mc',
-      MetricSemantics.eval_expr m l e mc = Some (v, mc') ->
-      forall k, exists k', eval_expr m l e k mc = Some (v, k', mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _ _ _, MetricSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
-          => specialize (IH _ _ _ ltac:(eassumption))
-        | IH: forall _: leakage, exists _: leakage, eval_expr ?m ?l ?e _ _ = Some _
-          |- context[eval_expr ?m ?l ?e ?k ?mc] => specialize (IH k)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_leakage_eval_expr: forall m l e k v k',
-      LeakageSemantics.eval_expr m l e k = Some (v, k') ->
-      forall mc, exists mc', eval_expr m l e k mc = Some (v, k', mc').
-  Proof.
-    induction e; cbn; intros;
-      repeat match goal with
-        | H: Some _ = Some _ |- _ => eapply Option.eq_of_eq_Some in H; subst
-        | IH: forall _, Some _ = Some _ -> _ |- _ => specialize IH with (1 := eq_refl)
-        | IH: forall _ _ _, LeakageSemantics.eval_expr _ _ _ _ = Some _ -> _ |- _
-          => specialize (IH _ _ _ ltac:(eassumption))
-        | IH: forall _: MetricLog, exists _: MetricLog, eval_expr ?m ?l ?e _ _ = Some _
-          |- context[eval_expr ?m ?l ?e ?k ?mc] => specialize (IH mc)
-        | |- _ => progress fwd
-        | |- _ => Tactics.destruct_one_match
-        end;
-      eauto.
-  Qed.
-
-  Lemma to_plain_eval_call_args: forall m l arges args,
-      Semantics.eval_call_args m l arges = Some args ->
-      forall k mc, exists k' mc', eval_call_args m l arges k mc = Some (args, k', mc').
-  Proof.
-    induction arges; cbn; intros.
-    - eapply Option.eq_of_eq_Some in H. subst. eauto.
-    - fwd.
-      eapply to_plain_eval_expr in E. destruct E as (k' & mc' & E). rewrite E.
-      specialize IHarges with (1 := eq_refl). specialize (IHarges k' mc').
-      destruct IHarges as (k'' & mc'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Lemma to_metric_eval_call_args: forall m l arges mc args mc',
-      MetricSemantics.eval_call_args m l arges mc = Some (args, mc') ->
-      forall k, exists k', eval_call_args m l arges k mc = Some (args, k', mc').
-  Proof.
-    induction arges; cbn; intros.
-    - inversion H. subst. eauto.
-    - fwd.
-      eapply to_metric_eval_expr in E. destruct E as (k' & E). rewrite E.
-      specialize (IHarges _ _ _ ltac:(eassumption) k').
-      destruct IHarges as (k'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Lemma to_leakage_eval_call_args: forall m l arges k args k',
-      LeakageSemantics.eval_call_args m l arges k = Some (args, k') ->
-      forall mc, exists mc', eval_call_args m l arges k mc = Some (args, k', mc').
-  Proof.
-    induction arges; cbn; intros.
-    - inversion H. subst. eauto.
-    - fwd.
-      eapply to_leakage_eval_expr in E. destruct E as (mc' & E). rewrite E.
-      specialize (IHarges _ _ _ ltac:(eassumption) mc').
-      destruct IHarges as (mc'' & IH). rewrite IH. eauto.
-  Qed.
-
-  Definition deleakaged_ext_spec : Semantics.ExtSpec :=
-    fun t mGive a args post => ext_spec t mGive a args (fun mReceive resvals klist => post mReceive resvals).
-
-  Lemma deleakaged_ext_spec_ok {ext_spec_ok: ext_spec.ok ext_spec}:
-    Semantics.ext_spec.ok deleakaged_ext_spec.
-  Proof.
-    destruct ext_spec_ok. cbv [deleakaged_ext_spec]. constructor; eauto.
-    intros. cbv [Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl] in *.
-    intros. eapply weaken; eauto. intros. apply H. simpl in *. assumption.
-  Qed.    
-
-  Context (e: env).
-  Existing Instance deleakaged_ext_spec.
-  Existing Instance deleakaged_ext_spec_ok.
-
-  Lemma to_plain_exec: forall c t m l post,
-      Semantics.exec e c t m l post ->
-      forall k mc, exec e c k t m l mc (fun _ t' m' l' _ => post t' m' l').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: Semantics.eval_expr _ _ _ = Some _ |- _ =>
-            eapply to_plain_eval_expr in H; destruct H as (? & ? & H)
-        | H: Semantics.eval_call_args _ _ _ = Some _ |- _ =>
-            eapply to_plain_eval_call_args in H; destruct H as (? & ? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_metric_exec: forall c t m l mc post,
-      MetricSemantics.exec e c t m l mc post ->
-      forall k, exec e c k t m l mc (fun _ t' m' l' mc' => post t' m' l' mc').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: MetricSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
-            eapply to_metric_eval_expr in H; destruct H as (? & H)
-        | H: MetricSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
-            eapply to_metric_eval_call_args in H; destruct H as (? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_leakage_exec: forall c t m l k post,
-      LeakageSemantics.exec e c k t m l post ->
-      forall mc, exec e c k t m l mc (fun k' t' m' l' _ => post k' t' m' l').
-  Proof.
-    induction 1; intros;
-      repeat match reverse goal with
-        | H: LeakageSemantics.eval_expr _ _ _ _ = Some _ |- _ =>
-            eapply to_leakage_eval_expr in H; destruct H as (? & H)
-        | H: LeakageSemantics.eval_call_args _ _ _ _ = Some _ |- _ =>
-            eapply to_leakage_eval_call_args in H; destruct H as (? & H)
-        end;
-      try solve [econstructor; eauto].
-  Qed.
-
-  Lemma to_plain_call: forall f t m args post,
-      Semantics.call e f t m args post ->
-      forall k mc, call e f k t m args mc (fun _ t' m' rets _ => post t' m' rets).
-  Proof.
-    unfold call, Semantics.call. intros. fwd. eauto 10 using to_plain_exec.
-  Qed.
-
-  Lemma to_metric_call: forall f t m args mc post,
-      MetricSemantics.call e f t m args mc post ->
-      forall k, call e f k t m args mc (fun _ t' m' rets mc' => post t' m' rets mc').
-  Proof.
-    unfold call, MetricSemantics.call. intros. fwd. eauto 10 using to_metric_exec.
-  Qed.
-
-  Lemma to_leakage_call: forall f k t m args post,
-      LeakageSemantics.call e f k t m args post ->
-      forall mc, call e f k t m args mc (fun k' t' m' rets _ => post k' t' m' rets).
-  Proof.
-    unfold call, LeakageSemantics.call. intros. fwd. eauto 10 using to_leakage_exec.
-  Qed.
 End WithParams.