make WeakestPrecondition.cmd complete wrt Semantics.exec
#361
Conversation
and rules for cmd' whose premises are copied from WP.cmd. This one is "fs everywhere" (ie list of functions everywhere). The wp_call rule requires a NoDup, which would be cumbersome to carry around.
In an "env everywhere" setting, where program_logic_goal_for! adds a (map.get fs fname = Some fimpl) hypothesis. Surprise #1: There's no case in straightline that handles if-then-else Surprise #2: unfold1_... tactics are not the only place that depend on conversion: There also exists a letexists in SPI that turns a (WP (cmd.cond e _ _) ...) into an (exists v, eval e v /\ ...), and probably more elsewhere.
by leaving the structurally recursive cases of cmd_body unchanged, and defining the two non-structurally recursive cases (loop and call) directly in terms of exec. This seems to be the only approach that does not break proofs in bedrock2Examples too badly.
and update compiler, LiveVerif, end2end
|
I did try this at #294 and ended up thinking we should just delete wp and port the examples... but what you're doing here might be better than what I tried there. |
|
|
||
| Definition refinement(c1 c2: cmd) := forall functions t m l post, | ||
| Semantics.exec.exec functions c1 t m l post -> | ||
| Semantics.exec.exec functions c2 t m l post. |
There was a problem hiding this comment.
Perhaps let's flip the arguments to match c1 <= c2 and "refines" pronounciation.
There was a problem hiding this comment.
good point, done in 535eec4
| @@ -78,205 +75,142 @@ Section binops. | |||
| end. | |||
| End binops. | |||
|
|
|||
| #[export] Instance env: map.map String.string Syntax.func := SortedListString.map _. | |||
| #[export] Instance env_ok: map.ok env := SortedListString.ok _. | |||
There was a problem hiding this comment.
Are these instances required, and where? What mode do the classes have?
There was a problem hiding this comment.
I just pushed this commit that makes env a Definition, which requires almost no changes. Haven't tried env_ok yet.
This makes me wonder why we declared map.map a Class at all and not just a Record?
The Hint Mode of map.map is + (input), as it should be, but for map.ok, it seems no Hint Mode is registered, is this correct/intended?
There was a problem hiding this comment.
Making env_ok a Lemma instead of an Instance would require mentioning it explicitly whenever we do pose proof (map.some_lemma ...), eapply map.some_lemma etc. Might be doable, but then it would be more consistent to make map.ok not a typeclass any more, and to make the map.ok argument an explicit one instead of an implicit one.
Or, if we keep declaring map.ok as a typeclass, then we could/should still see if it should get a Hint Mode + + + (key, value, and map implementation all are inputs to typeclass search).
But in either case, I'd say that should be separate from this PR.
| (* this is the expr evaluator that is used to verify execution time, the just-correctness-oriented version is below *) | ||
| Section WithMemAndLocals. | ||
| Context (m : mem) (l : locals). | ||
|
|
||
| Local Notation "' x <- a | y ; f" := (match a with x => f | _ => y end) | ||
| (right associativity, at level 70, x pattern). | ||
| Local Notation "x <- a ; f" := (match a with Some x => f | None => None end) |
| | cmd.call binds fname arges => | ||
| exists args, dexprs m l arges args /\ | ||
| call fname t m args (fun t m rets => | ||
| Semantics.call e fname t m args (fun t m rets => |
| Fixpoint call functions := call_body call functions. | ||
|
|
||
| Definition program funcs main t m l post : Prop := cmd (call funcs) main t m l post. | ||
| Definition program := cmd. |
There was a problem hiding this comment.
🤔 hopefully this one is almost dead and can be removed soon
There was a problem hiding this comment.
yes, I think only rupicola has some occurrences of this
| End WeakestPrecondition. | ||
| Notation call := Semantics.call (only parsing). |
| @@ -50,6 +50,32 @@ Definition uart0_rxdata := 0x10013004. Definition uart0_txdata := 0x10013000. | |||
| False | |||
| end%list%bool. | |||
|
|
|||
| Ltac u := | |||
There was a problem hiding this comment.
Do we care to keep this file?
There was a problem hiding this comment.
I have no strong attachment to this file 😉
At first I tried to delete the
Fixpoint-based wp gen and base all of the program logic on wp rules. Conceptually that could have worked, but adapting all the examples inbedrock2Examplesturned out too cumbersome because they rely oncbn, autogenerated hypothesis names, andhnfimplicitly happening beforeeexists,letexists,split, and others. I stashed that experiment on this branch.Now, I tried something simpler, just focusing on making
WeakestPrecondition.cmdcomplete wrtSemantics.exec: The only two cases where completeness can't be proven are:cmd.whilebecause the shape of the proof tree inexeclives inPropand can't be extracted into awell_foundedmeasure, at least not easilycmd.callif the function list contains the same name multiple times and a duplicate function makes a recursive call (this shouldn't happen, but carrying aroundNoDuppremises seems much more cumbersome than simply switching to anenv, ie map from string to function implementation, instead of using a list).And it turns out that these two disagreeing cases are also exactly the two cases where a wp gen cannot be defined by structural recursion.
So I simply defined these two cases to be
exec(or, more precisely, a thoroughly opaque definition calledWP.wp_cmdthat's defined to beexecbut without being visible to tactics such asrepeat split).There's probably room for more improvements/cleanup/refactoring/simplification, but this one already gets us completeness, in a quite "minimally" invasive way.
What do you think @andres-erbsen?