Update Trillium to Rocq 9.0 and latest Iris / stdpp

[fresheed]

The main changes are:

• codebase updated to the latest Iris (4.3.0) and its dependencies
• Trillium is turned into an opam package
• the new directory structure is:
  • trillium/ - as before
  • fairness/ - various trace and model utilities; most notably - a uniform definition of trace fairness and state/label trace lookups. The definition of FairModel is also moved there from fairis
  • heap_lang/ - our version of heap_lang. For the most part it is former fairis/heap_lang, but model-agnostic - so it can be used by different projects. Plus some new lemmas in locales_helpers_hl.v
  • fairis/ - almost as before, except the extracted heap_lang part

I'd refactor this a bit and try to find other general lemmas from Lawyer that are worth moving here

[jihgfee]

Looks good to me, and feels ready to merge.
I have some overall feedback, and suggestions for future work improvements.
Even so, I think we should get this merged ASAP and then consider next steps afterwards
Maybe @amintimany wants to gloss over the new structure, to be in the loop.

Feedback

Good that it is now based on OPAM!

A bit unfortunate that fairis is contingent on HeapLang (see future work)

• Particularly, heap1GS instance is a bit unfortunate, but suitable for now

Would be good if we could have a way of lifting sswp to wp for trivial models, and then let heap_lang be a self-contained program logic in that case (see future work)

We still have three different traces, which is a bit awkward to work with at times (see future work):

• trillium/traces/trace.v: finite_trace
• trillium/traces/infinite_trace.v: inflist
• fairness/inftraces: trace

Questions:

• Is Lawyer based on top of the HeapLang separation?
  • If not, separation from Fairis does not seem that beneficial (for now, see future work)

Future Work

Further refactoring suggestions

Move non-trace utils stuff (from utils) into its own folder preamble

• Consider moving trillium/preamble stuff there too, as some of the fairness utils stuff depends on it.

Suggested folder structure, with dependencies only going up:

• preamble
  • utils*.v
• traces
  • All trace stuff goes here
• fairness (possibly merged with traces
  • All fairnes stuff goes here
• trillium
• heap_lang
• fairis

Streamline trace infrastructure

Consolidate trace infrastructure to only have 2 traces; finite and infinite.

Move all trace infrastructure to its own directory (possibly merged with fairness)

• Should not depend on trillium

Might need major work, as trace definitions do not coincide, and its unclear how exactly to transform existing uses

• Might be fine to have current 3 definitions, but defined in one place, with compatibility lemmas between them, so distinction/correspondence is explicit

Compositional Languages and Models

Split trillium infrastructure (primarily irisG) into separate language and model parts

• Introduce model update from Fairneris/Lawyer projects
• Let state_interp and model_interp be two separate resources with compatibility laws

Let SSWP be language agnostic (currently explicitly defined for heap_lang (and aneris_lang in Fairneris project))

• Define sswp via separated state_interp from above
• Define trivial model instance (where wp and sswp coincide)
  • Define proofmode support for lifting sswp rules to wp obligations

Let heap_lang be model agnostic

• Obtain proofmode for model agnostic version
  • Recover examples from Iris (to show backwards compatibility)

Let Fairis be language agnostic

• Use separated irisG instances and model update
• Define model update rules for fuel steps and model steps

Instantiate Fairis with HeapLang

• Define custom rule for wp-fork
• Recover proofmode
• Recover examples

[fresheed]

Is Lawyer based on top of the HeapLang separation?
Particularly, heap1GS instance is a bit unfortunate

Thing is, the current heapGS class is specialized to the combination of heap_lang + Fairis, whereas Lawyer uses heap_lang + Lawyer. I'd like to reuse the heap part of instantiation and don't bring the rest. So heap1GS is needed anyway (probably under a different name).
In general, I think we need to generalize heapGS with something like TrilliumGS {\Lambda: language} {M: model} (LangGS \Lambda \Sigma) (ModelGS M \Sigma), where the two last parameters specify how to interpret the physical and the model part of the trace; plus something else (see below).

Would be good if we could have a way of lifting sswp to wp for trivial models

I guess one only needs \vdash MU { True } to hold for such a model?

We still have three different traces

Yeah, that's somewhat confusing.
The main definition I used is trace (possibly infinite one). IIRC finite_trace is mostly used in the wp definition, and inflist is purely a helper definition representing a trace without a head state (so the concatenation of a trace and inflist is defined). I guess we could replace finite_trace with something like { (tr: trace, n: nat) | trace_length_is tr n }. I don't think it's worth to get rid of inflist, as its use seems very local.

Suggested folder structure

Sounds good

Let state_interp and model_interp be two separate resources with compatibility laws

By state_interp you mean the physical trace?
If so, yes, but there should also be something that ties the physical and model states together; e.g. in Fairis it is a restriction that roles are held by non-terminated threads. Is that what you meant by 'compatibility laws'?

Obtain proofmode for model agnostic version; Recover examples from Iris (to show backwards compatibility)

It sounds like not a model-agnostic version, but rather a Trillium instantiation of heap_lang + trivial model. I guess "a model-agnostic heap_lang" would be just the sswp rules

Define model update rules for fuel steps and model steps

I guess you'd only need to replace locale heap_lang with arbitrary set?