[Iris-Club] Several small questions on Iris

[Ralf Jung]

Hi Jeehoon,

> As usual, I have several small questions on Iris :)

As usual, thanks for all your feedback :)

> First things first, here are references:
> - [1] Iris 3.0 paper
> - [2] Iris 3.0 appendix
> 
> 
> Now questions:
> 
> - I don't understand why it is okay *not* to have "Own(\iota,
> \gamma_{EN})" at the conclusion of the rules (WSAT-ALLOC) and
> (INV-ALLOC) [1].  More specifically, why is it okay to "forget" the fact
> that the "\iota" invariant is enabled when it is created?

The enabled tokens are *not* created by allocation.  They all exist from
the beginning of time.  When proving a Hoare triple with the full (\top)
mask, the tripe actually obtains ownership of all these tokens -- and it
has to produce ownership of all these tokens in its postcondition.  This
is implicitly handled by the fancy update modality.
In other words, WSAT-ALLOC and INV-ALLOC could only return the enabled
token for the new invariant \iota if they required that token to begin
with.  However, they don't -- it is possible to create an invariant
without knowing that it is currently enabled.

There is a token that WSAT-ALLOC *does* create, and it is the disabled
token.  That one however is not returned, it is put into W.

> - Why "K" should be countably infinite for the CMRA construction of
> finite partial function [2, S3.4, p11]?  More precisely, why not
> (possibly) uncountably infinite K?

The short answer is that our Coq proof only holds for countable domains.
;)  Considering that only finitely many elements can ever be allocated,
I cannot imagine when larger sets would be useful.
It may be possible to write a finite map in Coq that just requires
decidable equality, but (a) are there even uncountable types with
decidable equality, and (b) it's probably not worth the effort.

> - What is "c" in the definition of AG(T) [2, S3.5, p11]?

That "c" should be an "a" ;)

> - I don't quite understand what "Variable conventions." means [2, S4.1]:
> "We assume that, if a term occurs multiple times in a rule, its free
> variables are exactly those binders which are available at every
> occurrence."

Say we have a rule like Bind for Hoare triples

  { P } e { v. Q }
  \All v. { Q } K[v] { w. R }
  ---------------------------
  { P } K[e} { w. R }

The convention says that P must be a closed term, but Q can depend on v
(because v is free in both places where Q appears), and R can depend on
w (because w is free in both places where R appears).
Does this make sense?

> - I think "Res" in the definition of the interpretation of entailment in
> [2, p20], should be "M".

I think you are right.

> - It seems the semantics of "\Gamma | P => Q" and "\Gamma | P |- Q" are
> much related [2].  I wonder if the notion of logical entailment can be
> encoded with the semantics of implications.  (Yes, I know it is a
> program logic newbie question :-)  I just want to know the motivation
> behind the concept of logical entailment.)

I think what you are asking here is essentially whether we could write
our logic in Hilbert-style, with a fixed (and possibly fixed empty)
logical context.  The answer is yes, since (as you observed)
"\Gamma | True |- P => Q" holds (is derivable) iff
"\Gamma | P |- Q" holds (is derivable).  This is fairly easy to do in
any logic that has implication, I guess, you just need to apply the
above transformation to every single proof rule.  I don't think though
that this would gain you much; everything would be more confusing to
read, but you'd still have all the same work to do in Coq.

The way I like to think about this (coming from the model) is that we
first have a domain [|Prop|] of assertions, then we introduce a notion
of *entailment* on assertions (the turnstile), and then we reflect that
entailment *into the logic* (the implication).  The entailment "comes
first", it's a core part of what makes up an assertion.  In fact, once
the domain and entailment are defined, the models of conjunction,
disjunction, implication as well as universal and existential
quantification and even equality are already uniquely defined (if we
want to support the proof rules we have).  We have a whole bunch of
definitions for this stuff in Coq, but really, we have zero choice.

> - typo: "ruels" in [2, p22]
> 
> - typo: "Stateof" in [2, p24] (rather than "State of")

Thanks!

Kind regards,
Ralf