[Iris-Club] Classical version of Iris?

[Derek Dreyer]

Thinking a bit more about it, I think the problem with having a
classical Iris is that, even if you require precise tracking of
resources -- i.e. do not bake monotonicity into the model of
assertions -- there will still be the ability to effectively drop
resources by shoving them into a freshly allocated invariant.  So
basically, the invariant mechanism of Iris would give you a backdoor
to intuitionism.  In that case, the only way to regain precise
tracking of resources would be to explicitly keep track of all known
invariants and thread such reasoning through specs, which goes against
the use of invariants to model hidden state.  I think that can't
possibly work.

Derek

On Sun, Aug 14, 2016 at 2:27 PM, Derek Dreyer <dreyer at mpi-sws.org> wrote:
> No one is developing a classical version of Iris, so far as I know.  I
> don't know if I've ever thought much about what a classical version
> would look like, but I imagine that if it makes sense at all, it would
> be very painful to work with because you would lose monotonicity.
>
> To answer your question about applicability to Rust, this point about
> intuitionistic separation logic not being good for explicit storage
> deallocation is an oft-repeated myth.  There is no problem with using
> intuitionistic separation logic to reason safely about explicit
> deallocation -- the only difficulty is in using it to prove absence of
> memory leaks.  Indeed, in classical separation logic, if the
> postcondition of your program is "emp", then you know all the memory
> has been deallocated, whereas you would not know that in
> intuitionistic separation logic since the latter collapses the
> distinction between emp and true.  However, even in intuitionistic
> separation logic, I believe you can use ghost state to effectively
> encode the condition that all memory has been deallocated (e.g. by
> starting with some tokens that represent the capability to allocate
> memory, and then showing in the postcondition that you have regained
> ownership of all of them).  This is maybe more cumbersome but I think
> it's doable.
>
> That said, Rust permits memory leaks via reference-counting cycles, so
> the point is moot, and I can see no motivation for using classical
> rather than intuitionistic separation logic in modeling Rust.
>
> Cheers,
> Derek
>
> On Sun, Aug 14, 2016 at 2:08 PM, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr> wrote:
>> Dear Iris Club,
>>
>> In the ICFP 2016 paper is said "Iris is an intuitionistic separation logic,
>> which gives rise to the monotonicity requirement".  I wonder if someone is
>> developing a classical version of Iris.
>>
>> Background: I heard (from some of the Iris authors ;-) that Iris is related
>> the RustBelt project which aims to verify "unsafe" Rust programs, which (I
>> guess) involves verification of safe memory disposal.  And I just learned
>> from a classic textbook (https://www.cs.cmu.edu/~jcr/copenhagen08.pdf) that
>> verification of safe memory disposal requires classical separation logic..
>>
>> Best,
>> Jeehoon
>>
>> PS. Sorry for cluttering everyone's inbox by sending a lot of emails..  I
>> will at least try to say something useful.  Thank you for answering all the
>> questions!
>>
>> --
>> Jeehoon Kang (Ph.D. student)
>> Software Foundations Laboratory
>> Seoul National University
>>
>> --
>> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
>> Management: https://lists.mpi-sws.org/listinfo/iris-club
>> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>>