Logical relation with fundamental theorem and logical compatibility lemmas

For example, the lemmas in https://gitlab.mpi-sws.org/iris/examples/blob/master/theories/logrel/F_mu_ref/fundamental_binary.v use meta-level implication. These should all be strengthened magic wands.

On the other hand, the logical relation on logrel_heaplang does not have a syntactic type system, and hence no fundamental lemma proven in Coq.

Cc @robbertkrebbers @dfrumin

In this development (by @amintimany), it makes no sense to turn these into magic wands---The semantic typing judgment is a Prop, not an iProp.

But indeed, there is some value into turning the typing judgment into an iProp. For ReLoC, @dfrumin actually did do that (but for logical refinements instead of typing), and this works pretty well. In ReLoC this is very important because it allows one to prove a large class of refinements without breaking the abstraction of the logical relation, namely by using the compatibility rules and "symbolic execution" rules.

C.f. Paolo question on Mattermost (https://mattermost.mpi-sws.org/iris/pl/m8xw6cmu7fytur43nxstw65hro), note that the interpretation of types is an iProp in both developments. Making that a Prop, as he tried, will not work.

Which are the "both developments"? You first said it is Prop here in this repo but your 2nd post seems to say it is iProp?

• The interpretation of types, i.e. [[ τ ]] is an iProp in both @amintimany's development in iris-examples and @dfrumin's ReLoC.
• The logical refinement, i.e. Γ ⊨ e1 ≼ e2 : τ is a Prop in @amintimany's development in iris-examples, while it is an iProp in @dfrumin's ReLoC.

Oh, your first statement was about the judgement, the 2nd about the interpretation of types, I see. I am surprised that the judgment is iProp here. But I think having composition lemmas that work in Iris is somewhat orthogonal to that, one can state those lemmas directly on the type interpretation. Not sure how well that works for these developments though, considering they are also handling open terms (which we did not do in LambdaRust).

I am surprised that the judgment is iProp here. But I think having composition lemmas that work in Iris is somewhat orthogonal to that, one can state those lemmas directly on the type interpretation.

As we showed in the ReLoC paper, it's actually very useful to put the judgment in iProp if you want to reason without breaking the abstraction of the logical relation. If you only have composition lemmas in terms of the interpretation of types, you have to break the abstraction.

By the way, to conclude, do you now agree that this is not a bug?

I think this is not just a matter or convenience of abstraction. In LambdaRust, we need composition lemmas that work in Iris, and I do not think that is related to the type system being substructural: If you want to prove that something like fun _ => let x = ref 0 in fun _ => assert (!x == 0) is well-typed (the assert will not fail), you need to be able to carry an invariant established in the outer closure into the proof of semantic well-typedness of the inner closure. The lemmas in iris-examples/logrel are just useless for that purpose, right?

So I think there is a bug: The lemmas shown here are too weak. They establish the fundamental theorem, sure, but they are not the lemmas you need to actually prove syntactically ill-typed terms to be semantically well-typed. Just having the fundamental theorem without the compatibility lemmas, however, defeats the entire point of using logical relations.

What's in this file in iris-examples is the usual compatibility lemmas. I believe they are indeed not useful if you want to combine them with reasoning about unsafe code.

So, there are two ways around that:

• State these lemmas in terms of the expression interpretation. @amintimany did not do that.
• Put the judgment in iProp as done in ReLoC (for the case of program refinements).

That said, the compatibility lemmas in iris-examples are not useless to reason about programs with unsafe code. If you have a module with multiple operations, you indeed cannot state lemmas that take invariants as premises, but instead, you can represent modules using existential types, so, have, e1 : ∃ α. .. * ... * .... That way, you can reason about unsafe code because the invariant can be hidden using the existential type (and I believe this is what @amintimany is doing). However, such proofs have to be done entirely in the model.

mentioned in merge request !12 (merged)

Fair enough -- at the level of the existential type you can compose manual proofs and type-system-derived ones.

such proofs have to be done entirely in the model.

That is, however, a noticeable deficiency IMO.

changed title from Fix logical relations to not use meta-level implication to Logical relation with fundamental theorem logical compatibility lemmas

changed the description

With !12 (merged) merged, this issue is now repurposed to track having a single logical relation that both allows powerful compatibility lemmas (stated in the logic, not as meta-level consequences) and a fundamental theorem.

changed title from Logical relation with fundamental theorem logical compatibility lemmas to Logical relation with fundamental theorem and logical compatibility lemmas

changed the description

mentioned in issue iris#234 (closed)

@robbertkrebbers pointed out that the logical relation in the POPL20 tutorial resolves this issue, and indeed that that relation entirely subsumes the one we have here in iris/examples, so we should likely remove that one.

However, that repo is structured for a tutorial, not as a library (e.g., no lib folder for things built on top of the basic infrastructure, and markers for exercises). Also when someone contributes a case study, I don't think we want to add that to the tutorial, do we?

I see the following options:

1. Just remove logrel/heaplang, and reconsider our options when/if someone actually develops an interesting case study.
2. Remove logreal/heaplang and put a copy of the tutorial (adjusted to be more like a library) into iris/examples. The tutorial seems unlikely to change, but the code duplication could be annoying when fixing Iris incompatibilities.
3. Remove logreal/heaplang and move the tutorial logrel to some place that the tutorial and iris/examples can both depend on, such as Iris itself (requires HeapLang to be a separate package, but that will soon be possible). However, presumably the point of the tutorial is to explain what happens inside it, so that code cannot really be deduplicated.

Any other ideas?

(1) or (2) seem most reasonable.

We could of course automate (2) using a script that strips the exercise markers and removes files that are not needed for case studies.

That said, currently (2) is not even needed, so short term (1) might be better. If we go to (1), I think we want to have a signpost in examples that there's also the tutorial.

Not sure if changes are frequent enough to warrant a script for (2).

But (1) is the least amount of work, for sure. ;)

mentioned in merge request !42 (merged)

closed with merge request !42 (merged)

mentioned in commit d2eb2182