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

Jump to bottom

WP calls exec #294

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

WP calls exec #294

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion bedrock2/src/bedrock2/ProgramLogic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,7 +210,7 @@ Ltac straightline :=
unfold1_call_goal; cbv match beta delta [call_body];
lazymatch goal with |- if ?test then ?T else _ =>
replace test with true by reflexivity; change T end;
cbv match beta delta [WeakestPrecondition.func]
left; cbv match beta delta [WeakestPrecondition.func]
| |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
unfold1_cmd_goal; cbv beta match delta [cmd_body];
let x := ident_of_string s in
Expand Down
13 changes: 10 additions & 3 deletions bedrock2/src/bedrock2/WeakestPrecondition.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,12 @@ Section WeakestPrecondition.
list_map (get l) outnames (fun rets =>
post t m rets)).

Definition execfunc e '(innames, outnames, c) (t : trace) (m : mem) (args : list word) (post : trace -> mem -> list word -> Prop) :=
exists lf, map.of_list_zip innames args = Some lf /\
forall mc, exec e c t m lf mc (fun t m l _ =>
exists retvs, map.getmany_of_list l outnames = Some retvs /\
post t m retvs).

Definition call_body rec (functions : list (String.string * (list String.string * list String.string * cmd.cmd)))
(fname : String.string) (t : trace) (m : mem) (args : list word)
(post : trace -> mem -> list word -> Prop) : Prop :=
Expand All @@ -130,6 +136,7 @@ Section WeakestPrecondition.
| cons (f, decl) functions =>
if String.eqb f fname
then func (rec functions) decl t m args post
\/ execfunc (map.of_list functions) decl t m args post
else rec functions fname t m args post
end.
Fixpoint call functions := call_body call functions.
Expand Down Expand Up @@ -173,10 +180,10 @@ Ltac unfold1_list_map_goal :=

Ltac unfold1_call e :=
lazymatch e with
@call ?width ?BW ?word ?mem ?locals ?ext_spec ?fs ?fname ?t ?m ?l ?post =>
@call ?width ?BW ?word ?mem ?locals ?env ?ext_spec ?fs ?fname ?t ?m ?l ?post =>
let fs := eval hnf in fs in
constr:(@call_body width BW word mem locals ext_spec
(@call width BW word mem locals ext_spec) fs fname t m l post)
constr:(@call_body width BW word mem locals env ext_spec
(@call width BW word mem locals env ext_spec) fs fname t m l post)
end.
Ltac unfold1_call_goal :=
let G := lazymatch goal with |- ?G => G end in
Expand Down
41 changes: 30 additions & 11 deletions bedrock2/src/bedrock2/WeakestPreconditionProperties.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -180,10 +180,16 @@ Section WeakestPrecondition.
cbv [Proper respectful pointwise_relation Basics.impl]; ind_on (list (String.string * (list String.string * list String.string * Syntax.cmd.cmd)));
cbn in *; intuition (try typeclasses eauto with core).
destruct a.
destruct (String.eqb s a1); eauto.
eapply Proper_func;
destruct (String.eqb s a1); intuition eauto.
1: left; eapply Proper_func;
cbv [Proper respectful pointwise_relation Basics.flip Basics.impl WeakestPrecondition.func];
eauto.
right.
cbv [WeakestPrecondition.execfunc] in *; destruct p as ((?&?)&?).
destruct H2 as (?&?&?).
eexists; split; eauto; intros.
eapply Semantics.exec.weaken; eauto; intros.
destruct H3 as (?&?&?); eauto.
Qed.

Global Instance Proper_program :
Expand Down Expand Up @@ -282,6 +288,11 @@ Section WeakestPrecondition.
{ eapply sound_args in H; t. }
Qed.

Lemma exec_weaken_locals_of_list l E Z t m x mc post :
Semantics.exec.exec (map.of_list l) Z t m x mc post ->
List.Forall (fun '(k, v) => map.get E k = Some v) l ->
Semantics.exec.exec E Z t m x mc post.
Admitted.

Section WithE.
Context fs (E: env) (HE: List.Forall (fun '(k, v) => map.get E k = Some v) fs).
Expand All @@ -295,15 +306,23 @@ Section WeakestPrecondition.
destruct x as [n' ((X&Y)&Z)]; t.
destr (String.eqb n' n); t.
eexists X, Y, Z; split; [assumption|].
eexists; eauto.
eexists; eauto.
intros.
eapply sound_cmd'.
eapply Proper_cmd; try eapply H0.
all : cbv [respectful pointwise_relation Basics.impl]; intros; cbv beta.
1: eapply IHf, Proper_call; eauto.
2: eassumption.
eauto using sound_getmany.
destruct H0; t. {
eexists; eauto.
eexists; eauto.
intros.
eapply sound_cmd'.
eapply Proper_cmd; try eapply H0.
all : cbv [respectful pointwise_relation Basics.impl]; intros; cbv beta.
1: eapply IHf, Proper_call; eauto.
2: eassumption.
eauto using sound_getmany. }
{ eexists; eauto.
eexists; eauto.
intros.
eapply Semantics.exec.weaken.
{ specialize (H1 mc'). inversion HE; subst.
eapply exec_weaken_locals_of_list; eauto. }
{ cbv beta; intros; t; eauto. } }
Qed.

Lemma sound_cmd'' c t m l mc post
Expand Down
4 changes: 2 additions & 2 deletions bedrock2/src/bedrock2Examples/memequal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment
Section WithParameters.
Context {width} {BW: Bitwidth width}.
Context {word: word.word width} {mem: map.map word byte} {locals: map.map string word}.
Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
Context {ext_spec: ExtSpec}.
Import ProgramLogic.Coercions.

Expand All @@ -41,8 +42,7 @@ Section WithParameters.
(r = 1 :>Z <-> xs = ys) }.

Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
{env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
{ext_spec_ok : ext_spec.ok ext_spec}.
{env_ok : map.ok env} {ext_spec_ok : ext_spec.ok ext_spec}.

Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
Require Import coqutil.Word.Properties coqutil.Map.Properties.
Expand Down
5 changes: 2 additions & 3 deletions bedrock2/src/bedrock2Examples/memswap.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment
Section WithParameters.
Context {width} {BW: Bitwidth width}.
Context {word: word.word width} {mem: map.map word byte} {locals: map.map string word}.
Context {ext_spec: ExtSpec}.
Context {env : map.map string (list string * list string * Syntax.cmd)} {ext_spec: ExtSpec}.
Import ProgramLogic.Coercions.

Global Instance spec_of_memswap : spec_of "memswap" :=
Expand All @@ -42,8 +42,7 @@ Section WithParameters.
ensures t' m := m =* ys$@x * xs$@y * R /\ t=t' }.

Context {word_ok: word.ok word} {mem_ok: map.ok mem} {locals_ok : map.ok locals}
{env : map.map string (list string * list string * Syntax.cmd)} {env_ok : map.ok env}
{ext_spec_ok : ext_spec.ok ext_spec}.
{env_ok : map.ok env} {ext_spec_ok : ext_spec.ok ext_spec}.

Import coqutil.Tactics.letexists coqutil.Tactics.Tactics coqutil.Tactics.autoforward.
Require Import coqutil.Word.Properties coqutil.Map.Properties.
Expand Down