Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add some lemmas relating the different semantics #445

Merged
merged 3 commits into from
Jan 31, 2025
Merged

Add some lemmas relating the different semantics #445

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e7381bb
add all the easy-to-prove semantics relations
OwenConoly Jan 30, 2025
e151241
make LeakageSemantics.straightline_call work with Semantics function …
OwenConoly Jan 30, 2025
8446c9e
remove some unneeded requires and imports
OwenConoly Jan 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion bedrock2/src/bedrock2/FE310CSemantics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
19 changes: 15 additions & 4 deletions bedrock2/src/bedrock2/LeakageProgramLogic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 ? ? ? ?]
Expand All @@ -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
Expand Down
171 changes: 0 additions & 171 deletions bedrock2/src/bedrock2/MetricLeakageSemantics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -546,173 +544,4 @@ Section WithParams.
- eassumption.
- eapply exec.extend_env; eassumption.
Qed.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this mean that a Require could be removed?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure which one you were talking about, but I removed a few that were obviously not needed. (my pushing that disabled your auto-merge thing)

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.
Loading
Loading