[Iris-Club] Using Iris

[Gregory Malecha]

Hi, Ralf --

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.

On Thu, Oct 11, 2018 at 7:54 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi Greg,
>
> > 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).
>
> Yes, if we have a triple for the continuation, we can just use that same
> postcondition.  We could likely have done the same thing in lambdaRust,
> but that
> would be one more parameter to carry around.  I think that would amount to
> making `cont_postcondition` a parameter here [1] and here [2].
>
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!).

>
> [1]
> <
> https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/programs.v#L10
> >
> [2]
> <
> https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/cont_context.v#L25
> >
>
> >     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.
>
> I am not entirely sure what you mean by "running" WP. In Iris, WP is not a
> function that computes the weakest precondition (by evaluating to some
> other
> Iris term); it is an Iris statement saying "the resources we own are good
> enough
> to prove safe execution of the program, and subsequently ownership of the
> postcondition".  It's a bit like the [a] modality of dynamic logic, with
> "a"
> being the code to execute.

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.

>
> We have described this in more detail, and explain how WP is defined, in
> <https://iris-project.org/pdfs/2017-esop-iris3-final.pdf>.
>
> > 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.
>
> On our case, that is exactly the problem. If halt halts the machine, it
> cannot
> have post-condition false. I guess we could define the operational
> semantics of
> halt to be "infinite loop", and then indeed postcondition false would
> work, but
> that didn't seem like a nice choice to us. So instead "halt" is just "()"
> [3] --
> unit, a term that is immediately done computing, and we use postcondition
> true.
>
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.

There are three reasons that I like False, though they are matters of taste:

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

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

3. `forall x, WP x False |-- WP x True` but not vice versa. If both are
provable, then why not prove something stronger? :-)

>
> [3]
> <
> https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/e58546a08e690c8b05567544efbd3fbbfe4746cf/theories/typing/soundness.v#L23
> >
>
> I was never completely happy with this solution either, but it seemed
> nicer than
> making every program diverge.  Also, it is true that now every program can
> trivially satisfy the postcondition by not calling the continuation --
> however,
> every program can also trivially start an endless loop to satisfy *any*
> postcondition, or call "halt" to satisfy whatever postcondition we give to
> the
> whole program.
>
> > 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.
>
> I agree that makes a lot of sense. I am just wondering, how do you model
> this
> "halt" instruction in your operational semantics?
>
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).

>
> 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/20181011/27cc2a63/attachment-0001.html>