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 is exec #362

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Wp is exec #362

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
7a43f3a
define a WP.cmd' in terms of exec, might soon replace WP.cmd
samuelgruetter Jul 26, 2023
4b3e917
dead simple `call` based on `map.get`
samuelgruetter Jul 26, 2023
b98be1f
convert from "fs everywhere" to "env everywhere"
samuelgruetter Jul 26, 2023
867c49b
instead of unfold1_cmd_goal, eapply lemma_corresponding_to_command
samuelgruetter Jul 28, 2023
36882d9
wip "env everywhere" approach
samuelgruetter Jul 29, 2023
36780ed
make the new `cmd` opaque to `hnf` and `repeat split`
samuelgruetter Jul 29, 2023
978d785
trying to pretend the new `cmd` is unfoldable by
samuelgruetter Jul 29, 2023
b46e864
port more examples from wp to exec
andres-erbsen Aug 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
96 changes: 47 additions & 49 deletions bedrock2/src/bedrock2/Loops.v
View file
Open in desktop

Large diffs are not rendered by default.

33 changes: 23 additions & 10 deletions bedrock2/src/bedrock2/ProgramLogic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,12 @@
From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string.
Require Import coqutil.Map.Interface.
Require Import bedrock2.Syntax.
Require Import bedrock2.WeakestPrecondition.
Require Import bedrock2.WeakestPreconditionProperties.
Require Import bedrock2.Loops.
Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars.

Definition spec_of (procname:String.string) := list (String.string * (list String.string * list String.string * Syntax.cmd.cmd)) -> Prop.
Definition spec_of (procname:String.string) := env -> Prop.
Existing Class spec_of.

Module Import Coercions.
Expand Down Expand Up @@ -55,9 +56,9 @@ Ltac program_logic_goal_for_function proc :=
let __ := constr:(proc : Syntax.func) in
constr_string_basename_of_constr_reference_cps ltac:(Tactics.head proc) ltac:(fun fname =>
let spec := lazymatch constr:(_:spec_of fname) with ?s => s end in
exact (forall functions : list (string * Syntax.func), ltac:(
exact (forall (functions : @map.rep _ _ env) (EnvContains : map.get functions fname = Some proc), ltac:(
let callees := eval cbv in (callees (snd proc)) in
let s := assuming_correctness_of_in callees functions (spec (cons (fname, proc) functions)) in
let s := assuming_correctness_of_in callees functions (spec functions) in
exact s))).
Definition program_logic_goal_for (_ : Syntax.func) (P : Prop) := P.

Expand All @@ -84,7 +85,7 @@ Ltac bind_body_of_function f_ :=

(* note: f might have some implicit parameters (eg a record of constants) *)
Ltac enter f :=
cbv beta delta [program_logic_goal_for]; intros;
cbv beta delta [program_logic_goal_for];
bind_body_of_function f;
lazymatch goal with |- ?s ?p => let s := rdelta s in change (s p); cbv beta end.

Expand Down Expand Up @@ -228,13 +229,16 @@ Ltac straightline :=
match goal with
| _ => straightline_cleanup
| |- program_logic_goal_for ?f _ =>
enter f; intros;
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;
enter f;
cbv beta delta [call];
lazymatch goal with
| H: map.get ?functions ?fname = Some _ |- context[map.get ?functions ?fname] =>
rewrite H; clear H
end;
intros;
cbv match beta delta [WeakestPrecondition.func]
| |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
unfold1_cmd_goal; cbv beta match delta [cmd_body];
unfold1_cmd_goal;
let __ := match s with String.String _ _ => idtac | String.EmptyString => idtac end in
ident_of_constr_string_cps s ltac:(fun x =>
ensure_free x;
Expand All @@ -246,7 +250,7 @@ Ltac straightline :=
| cmd.while _ _ => fail
| cmd.cond _ _ _ => fail
| cmd.interact _ _ _ => fail
| _ => unfold1_cmd_goal; cbv beta match delta [cmd_body]
| _ => apply_rule_for_command c
end
| |- @list_map _ _ (get _) _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body]
| |- @list_map _ _ (expr _ _) _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body]
Expand Down Expand Up @@ -343,6 +347,15 @@ Ltac straightline_call :=
[ .. | intros ? ? ? ?]
end.

(* not as eager as it might look, because each rule only has one premise,
and it is of the form (_ /\ _) or (exists _, _),
except wp_seq, which has another cmd as its premise, but there, we
indeed want to unfold the head cmd again *)
Ltac apply_rules_until_propositional := repeat unfold1_cmd_goal.

Export coqutil.Tactics.letexists.
Ltac expose_exists_for_letexists ::= hnf; apply_rules_until_propositional.

Ltac current_trace_mem_locals :=
lazymatch goal with
| |- WeakestPrecondition.cmd _ _ ?t ?m ?l _ => constr:((t, m, l))
Expand Down