<div dir="ltr">Hi, Ralf --<div><br><div class="gmail_quote"><div dir="ltr">On Sun, Oct 7, 2018 at 8:37 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>
sorry for the late reply, and I'd be very happy to arrange a video call if you'd<br>
like! Also see my embedded reply below.<br></blockquote><div>No problem at all. It would be great to chat with you, when would be good for you? </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
> 1/ All of the resources that I have seen have applied Iris to Hoare<br>
> triples. Has anyone tried applying it to Hoare doubles, i.e. `{ P } c`<br>
> means that `P` guarantees that `c` is safe (but says nothing about a<br>
> final state). I thought that the RustBelt work might have done something<br>
> like this since the paper talks about how the logic is applied to a CPS<br>
> language but I didn't find anything in that development.<br>
> <br>
> <br>
> What about just considering triples of the form { P } c {x. True}? This<br>
> ensures that c is safe, so I think it suffices for what you want, right?<br>
> <br>
> This is a good point. I would have thought to use False rather than True in the<br>
> post-condition, is there a reason that you chose False? <br>
<br>
Postcondition "False" would mean that the program never terminates. I don't<br>
think that's what you want? Postcondition "True" is what we use in RustBelt. It<br>
means "the program executes safely and if it terminates, we don't say anything<br>
about the final state".<br></blockquote><div>I think I understand what you're saying, True is a fine post-condition, it just isn't the strongest post-condition. If you have a CPS converted program you have a triple like:</div><div><br></div><div>{ P } \ k x . k x { Q }</div><div><br></div><div>Since `k` is an argument, you give it a higher-order assertion in P, so something like:</div><div><br></div><div>{ { P' } k { Q' } } \ k x . k x { Q }</div><div><br></div><div>Applying the logic, all we need is that Q' |-- Q, so we can actually prove a stronger triple:</div><div><br></div><div>forall Q, { { P' } k { Q } } \ k x . k x { Q }</div><div><br></div><div>It shouldn't matter if we instantiate Q with True or False (or anything inbetween from a proof point of view). My motivation for using False it that it requires the program to call k (or loop), it can never simply return (because CPSd programs never return, otherwise they aren't in CPS). </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<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></blockquote><div>If you run WP on the program above, you should get the same thing as above. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
For RustBelt, we encoded CPS as a mode of use of the lambda calculus<br>
(continuations are just lambda terms), so things overall work a lot like they do<br>
in the simple language we usually consider in the Iris papers. In your setting,<br>
is it even possible to talk about what happens when `c` is executed without<br>
specifying a continuation, or is there some syntactic distinction between `c`<br>
and "whole programs" that have an operational semantics?</blockquote><div>There isn't anything that prevents you from having operations inside your language that have False post-conditions. At the very low level, you could imagine the halt instruction has a post-condition of False. Higher up the stack, exit has a post-condition of False. In the domain that I'm working in, programs don't return to the operating system through normal "return", rather, they need to call a special syscall, which is what has the False post-condition, this syscall is morally like thread-exit. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> </blockquote><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>