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 in bedrock2Examples turned out too cumbersome because they rely on cbn, autogenerated hypothesis names, and hnf implicitly happening before eexists, letexists, split, and others. I stashed that experiment on this branch.
Now, I tried something simpler, just focusing on making WeakestPrecondition.cmd complete wrt Semantics.exec: The only two cases where completeness can't be proven are:
1) cmd.while because the shape of the proof tree in exec lives in Prop and can't be extracted into a well_founded measure, at least not easily
2) cmd.call if the function list contains the same name multiple times and a duplicate function makes a recursive call (this shouldn't happen, but carrying around NoDup premises seems much more cumbersome than simply switching to an env, 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 called WP.wp_cmd that's defined to be exec but without being visible to tactics such as repeat 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?
I did try this at https://github.com/mit-plv/bedrock2/pull/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.
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 inbedrock2Examples
turned out too cumbersome because they rely oncbn
, autogenerated hypothesis names, andhnf
implicitly happening beforeeexists
,letexists
,split
, and others. I stashed that experiment on this branch.Now, I tried something simpler, just focusing on making
WeakestPrecondition.cmd
complete wrtSemantics.exec
: The only two cases where completeness can't be proven are: 1)cmd.while
because the shape of the proof tree inexec
lives inProp
and can't be extracted into awell_founded
measure, at least not easily 2)cmd.call
if the function list contains the same name multiple times and a duplicate function makes a recursive call (this shouldn't happen, but carrying aroundNoDup
premises 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_cmd
that's defined to beexec
but 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?