Make EqType more realistic

This MR makes EqTypes (types on which you can CAS) more realistic. EqTypes are now: unit, boolean natural numbers and references. Having references in EqTypes makes the fine-grained stack example syntactically well-typed.

@jung I was expecting CI to run in MRs! Is there a way to trigger a CI test for this MR?

@amintimany CI in GitLab is a branch-thing, not an MR-thing. if you want your branch to have CI, make sure its name starts with ci/, e.g. ci/amin/logrel.

So is this just a type system change or a change in the operational semantics?

It is just the type system that has changed.

I see. To make things realistic, the operational semantics should not permit such CASes to begin with.

But I don't care strongly; we don't model this in heap_lang either. I also can't really review this anyway, so feel free to merge.

I see. To make things realistic, the operational semantics should not permit such CASes to begin with.

I agree but that makes to operational semantics complicated for no good reason. At least now the type system is restricted to single word values.

But that is not the main point of this MR. The main point is that the fine-grained stack was not syntactically well-typed up to now. Because of this our definition contextual refinement did not require well-typedness which is different from what we write on paper.

But that is not the main point of this MR. The main point is that the fine-grained stack was not syntactically well-typed up to now. Because of this our definition contextual refinement did not require well-typedness which is different from what we write on paper.

That's great! Thanks, @amintimany

Whatever proofs you added seem pretty crzy. Any intuition why this is so difficult to prove (and why you did not have it in the first place)?

Anyway, feel free to merge.

Whatever proofs you added seem pretty crzy. Any intuition why this is so difficult to prove (and why you did not have it in the first place)?

The original reason why I didn't do it in the first place is POPL deadline for the IPM paper ;-)

The problem is that there are many cases that need to be considered. Maybe if I take another look at it I can factor some of the commonalities into more high-level lemmas but I don't have time to do this now. The general idea is that for references, you have to argue that if one side of CAS succeeds and the other doesn't then the masks on invariants allow us to open invariants (corresponding to references) in such a way that we get some points-to twice!

mentioned in commit 61e0e3fa

merged

mentioned in commit 6d98dc66