Merge pull request #445 from OwenConoly/master

Add some lemmas relating the different semantics

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/LeakageProgramLogic.v

@@ -6,9 +6,10 @@ Require Import bedrock2.LeakageWeakestPrecondition.
 Require Import bedrock2.LeakageWeakestPreconditionProperties.
 Require Import bedrock2.LeakageLoops.
 Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars.
+Require bedrock2.ProgramLogic.
+Require Import bedrock2.SemanticsRelations.
 
-Definition spec_of (procname:String.string) := Semantics.env -> Prop.
-Existing Class spec_of.
+Notation spec_of := bedrock2.ProgramLogic.spec_of.
 
 Module Import Coercions.
   Import Map.Interface Word.Interface BinInt.
@@ -388,7 +389,6 @@ Ltac straightline_call_noex :=
   | |- LeakageWeakestPrecondition.call ?functions ?callee _ _ _ _ _ =>
     let callee_spec := lazymatch constr:(_:spec_of callee) with ?s => s end in
     let Hcall := lazymatch goal with H: callee_spec functions |- _ => H end in
-    repeat destruct Hcall as [?f Hcall]; 
     eapply LeakageWeakestPreconditionProperties.Proper_call; cycle -1;
       [ eapply Hcall | try eabstract (solve [Morphisms.solve_proper]) .. ];
       [ .. | intros ? ? ? ?]
@@ -406,8 +406,19 @@ Ltac straightline_call_ex :=
         [ .. | intros ? ? ? ? ]
   end.
 
+(*for use when the spec of callee has been written using Semantics, not LeakageSemantics*)
+Ltac straightline_call_from_plain :=
+  lazymatch goal with
+  | |- LeakageWeakestPrecondition.call ?functions ?callee _ _ _ _ _ =>
+    let callee_spec := lazymatch constr:(_:spec_of callee) with ?s => s end in
+    let Hcall := lazymatch goal with H: callee_spec functions |- _ => H end in
+    eapply LeakageWeakestPreconditionProperties.Proper_call; cycle -1;
+      [ eapply leakage_to_plain_call; eapply Hcall | try eabstract (solve [Morphisms.solve_proper]) .. ];
+      [ .. | intros ? ? ? ?]
+  end.
+
 (* TODO: once we can automatically prove some calls, include the success-only version of this in [straightline] *)
-Ltac straightline_call := straightline_call_noex || straightline_call_ex.
+Ltac straightline_call := straightline_call_noex || straightline_call_ex || straightline_call_from_plain.
 
 Ltac current_trace_mem_locals :=
   lazymatch goal with

bedrock2/src/bedrock2/MetricLeakageSemantics.v

@@ -6,10 +6,8 @@ Require Import coqutil.Z.Lia.
 Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Export bedrock2.Memory.
-Require Import Coq.Lists.List.
 Require Import bedrock2.MetricLogging.
 Require Import bedrock2.MetricCosts.
-Require Import bedrock2.MetricSemantics.
 Require Import bedrock2.Semantics.
 Require Import bedrock2.LeakageSemantics.
 Require Import Coq.Lists.List.
@@ -546,173 +544,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.