[Iris-Club] Using Iris

Gregory Malecha gmalecha at gmail.com
Sun Oct 7 16:59:20 CEST 2018


Hi, Ralf --

On Sun, Oct 7, 2018 at 8:37 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi Greg,
>
> sorry for the late reply, and I'd be very happy to arrange a video call if
> you'd
> like!  Also see my embedded reply below.
>
No problem at all. It would be great to chat with you, when would be good
for you?

>
> >         1/ All of the resources that I have seen have applied Iris to
> Hoare
> >         triples. Has anyone tried applying it to Hoare doubles, i.e. `{
> P } c`
> >         means that `P` guarantees that `c` is safe (but says nothing
> about a
> >         final state). I thought that the RustBelt work might have done
> something
> >         like this since the paper talks about how the logic is applied
> to a CPS
> >         language but I didn't find anything in that development.
> >
> >
> >     What about just considering triples of the form { P } c {x. True}?
> This
> >     ensures that c is safe, so I think it suffices for what you want,
> right?
> >
> > This is a good point. I would have thought to use False rather than True
> in the
> > post-condition, is there a reason that you chose False?
>
> Postcondition "False" would mean that the program never terminates. I don't
> think that's what you want? Postcondition "True" is what we use in
> RustBelt. It
> means "the program executes safely and if it terminates, we don't say
> anything
> about the final state".
>
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:

{ P } \ k x . k x { Q }

Since `k` is an argument, you give it a higher-order assertion in P, so
something like:

{ { P' } k { Q' } } \ k x . k x { Q }

Applying the logic, all we need is that Q' |-- Q, so we can actually prove
a stronger triple:

forall Q, { { P' } k { Q } } \ k x . k x { Q }

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).

>
> Notice that Hoare triples are anyway just syntactic sugar, what Iris
> really is
> about is `WP e { v, P }` saying that expression `e` is safe to execute in
> the
> current state and if it terminates, `P` holds for the final state.
>
If you run WP on the program above, you should get the same thing as above.

>
> For RustBelt, we encoded CPS as a mode of use of the lambda calculus
> (continuations are just lambda terms), so things overall work a lot like
> they do
> in the simple language we usually consider in the Iris papers.  In your
> setting,
> is it even possible to talk about what happens when `c` is executed without
> specifying a continuation, or is there some syntactic distinction between
> `c`
> and "whole programs" that have an operational semantics?

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.

>


> Kind regards,
> Ralf
>


-- 
gregory malecha
gmalecha.github.io
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181007/febd5f50/attachment.html>


More information about the Iris-Club mailing list