[Iris-Club] Using Iris

[Ralf Jung]

Hi Greg,

> No problem at all. It would be great to chat with you, when would be good for you? 

(I will respond to this in private.)

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

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

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.

[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?

Kind regards,
Ralf