<div dir="ltr">Hi, Ralf --<div><br></div><div>We're generally in agreement about everything, I think this just comes down to a wording question. I think the interesting part of the discussion is modeling halt, see my comments at the end.<br><br><div class="gmail_quote"><div dir="ltr">On Thu, Oct 11, 2018 at 7:54 AM Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Greg,<br>
<br>> I think I understand what you're saying, True is a fine post-condition, it just<br>
> isn't the strongest post-condition. If you have a CPS converted program you have<br>
> a triple like:<br>
> <br>
> { P } \ k x . k x { Q }<br>
> <br>
> Since `k` is an argument, you give it a higher-order assertion in P, so<br>
> something like:<br>
> <br>
> { { P' } k { Q' } } \ k x . k x { Q }<br>
> <br>
> Applying the logic, all we need is that Q' |-- Q, so we can actually prove a<br>
> stronger triple:<br>
> <br>
> forall Q, { { P' } k { Q } } \ k x . k x { Q }<br>
> <br>
> It shouldn't matter if we instantiate Q with True or False (or anything<br>
> inbetween from a proof point of view). My motivation for using False it that it<br>
> requires the program to call k (or loop), it can never simply return (because<br>
> CPSd programs never return, otherwise they aren't in CPS). <br>
<br>
Yes, if we have a triple for the continuation, we can just use that same<br>
postcondition.  We could likely have done the same thing in lambdaRust, but that<br>
would be one more parameter to carry around.  I think that would amount to<br>
making `cont_postcondition` a parameter here [1] and here [2].<br></blockquote><div>This makes sense, simplicity is a fine motivation for using True. I would be willing to bet that if you globally replaced True with False, everything would still work out (parametricity by sed!).</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
[1]<br>
<<a href="https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/programs.v#L10" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/programs.v#L10</a>><br>
[2]<br>
<<a href="https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/cont_context.v#L25" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/cont_context.v#L25</a>><br>
<br>
>     Notice that Hoare triples are anyway just syntactic sugar, what Iris really is<br>
>     about is `WP e { v, P }` saying that expression `e` is safe to execute in the<br>
>     current state and if it terminates, `P` holds for the final state.<br>
> <br>
> If you run WP on the program above, you should get the same thing as above. <br>
<br>
I am not entirely sure what you mean by "running" WP. In Iris, WP is not a<br>
function that computes the weakest precondition (by evaluating to some other<br>
Iris term); it is an Iris statement saying "the resources we own are good enough<br>
to prove safe execution of the program, and subsequently ownership of the<br>
postcondition".  It's a bit like the [a] modality of dynamic logic, with "a"<br>
being the code to execute.</blockquote><div>This was poor wording on my part. Usually I think of WP as a function over the syntax that has the soundness property that you define, but in your case, you directly use the soundness property as the definition.  </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
We have described this in more detail, and explain how WP is defined, in<br>
<<a href="https://iris-project.org/pdfs/2017-esop-iris3-final.pdf" rel="noreferrer" target="_blank">https://iris-project.org/pdfs/2017-esop-iris3-final.pdf</a>>.<br>
<br>
> There isn't anything that prevents you from having operations inside your<br>
> language that have False post-conditions. At the very low level, you could<br>
> imagine the halt instruction has a post-condition of False.<br>
<br>
On our case, that is exactly the problem. If halt halts the machine, it cannot<br>
have post-condition false. I guess we could define the operational semantics of<br>
halt to be "infinite loop", and then indeed postcondition false would work, but<br>
that didn't seem like a nice choice to us. So instead "halt" is just "()" [3] --<br>
unit, a term that is immediately done computing, and we use postcondition true.<br></blockquote><div>I think this is because usually "the machine is off" is not a state of the system. If you wanted to add a true "off" state to the system, then (I think) things would work out pretty easily. Simply interpret your predicates as "state = on -> P". Since "state = off" has no transitions (or the identity transition, however is more convenient to define it) the invariant is trivially preserved by its steps.</div><div><br></div><div>There are three reasons that I like False, though they are matters of taste:</div><div><br></div><div>1. The reason that False makes sense to me is that callers of a function with a False post-condition do not need to specify what happens after the function returns, because they know that False it provable if the function returns so they can simply eliminate that proof. Consider `WP (if (x == 0) { halt(); } else { return 0; }) { \ ret => ret = 0 }`. This program will never fail to execute, so one could argue that the weakest pre-condition should be True, but if halt has post-condition True, then the weakest precondition is actually `x <> 0`.</div><div><br></div><div>2. Another argument for this could be that the globalized program invariant implies some safety condition trivially. Suppose, for example, I have a program such as: { x <> 0 } diverge(); { True }</div><div>If I expand this out into a "whole system" invariant, I would get something like "(pc = 0 -> x <> 0) /\ (pc = 1 -> True)" (assuming appropriate pc variables). Simply looking at this assertion, I don't know that `x <> 0`. In order to prove that `x <> 0` is an invariant of my system, then I need to know that `pc = 1 -> False` which I haven't proven.</div><div><br></div><div>3. `forall x, WP x False |-- WP x True` but not vice versa. If both are provable, then why not prove something stronger? :-)</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
[3]<br>
<<a href="https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/soundness.v#L23" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/soundness.v#L23</a>><br>
<br>
I was never completely happy with this solution either, but it seemed nicer than<br>
making every program diverge.  Also, it is true that now every program can<br>
trivially satisfy the postcondition by not calling the continuation -- however,<br>
every program can also trivially start an endless loop to satisfy *any*<br>
postcondition, or call "halt" to satisfy whatever postcondition we give to the<br>
whole program.<br>
<br>
> Higher up the stack,<br>
> exit has a post-condition of False. In the domain that I'm working in, programs<br>
> don't return to the operating system through normal "return", rather, they need<br>
> to call a special syscall, which is what has the False post-condition, this<br>
> syscall is morally like thread-exit. <br>
<br>
I agree that makes a lot of sense. I am just wondering, how do you model this<br>
"halt" instruction in your operational semantics?<br></blockquote><div>See above. If you wanted to do this at the OS level, then your False would be scoped over the program's memory and things would work similarly. If this program is running, then the invariant holds, if the program is not running, you can't start running it (without re-initializing it). </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Kind regards,<br>
Ralf<br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="https://gmalecha.github.io" target="_blank">gmalecha.github.io</a></div></div></div></div></div></div></div>