[Iris-Club] Using Iris

[Gregory Malecha]

Hello --

I'm interested in using Iris in a large (industry) development and I have a
few questions about it to see if it is something that would work for us.
Two questions come to mind right now, but more will probably come up as I
dig deeper.

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.

2/ One of the things that I need to track in the development is
interactions with the outside world (for our project, this is hardware like
ethernet nics). Right now, I'm thinking that a nice way to do this would be
through a pre-condition that states what traces are possible when running
the program. Essentially, I want to add a spatial predicate `TRACE p` such
that `{ TRACE p } c` means that the only interaction that `c` can do is to
follow the protocol defined by `p` which is morally something akin to
`trace -> Prop`. My intuition suggests that this should be fairly simple in
Iris if I model it as a module that carries around the trace behind an
abstract predicate. The difficulty is that I need to ensure totality,
mainly that I have to follow the protocol, i.e. I can't diverge. Normally,
this would just require a total Hoare logic, but if my protocol is
infinite, things become a little more complex. Has anyone done something
like this before? Is there anything that I should be weary of?

I'd be interested in chatting more with anyone if they have an hour or so,
I am in Boston and have a relatively flexible schedule to accommodate other
time zones.

Thanks for any feedback.

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