There are multiple accumulated nuisances that permeates Aneris, which can be tricky to solve, as they often require a full recompilation for even simple name-changes.
In this issue we document such nuisances, so that we can eventually fix them altogether.
Adequacy:
- Name clash between base adequacy theorems [./aneris_lang/adequacy.v] and Aneris adequacy theorems [./aneris_lang/program_logic/aneris_adequacy.v]
- Aneris adequacy theorems should have the
aneris_ prefix
- Inconsistency between expressivity of base-line adequacy theorems and Aneris adequacy theorems (e.g. Aneris ones do not expose
tid and thus cannot be used with locales)
- Incorrect use of base adequacy theorems instead of Aneris adequacy theorems in various examples
- Inconsistencies between parameter conventions in adequacy theorems (order, implicit parameters, WP obligation as a definition etc.)
Model:
- Group sockets protocols are very invasive in all definitions/theorems/etc. but have never seen any use outside of toy examples, we should consider removing them again.
Also see #23, #24, #31
There are multiple accumulated nuisances that permeates Aneris, which can be tricky to solve, as they often require a full recompilation for even simple name-changes.
In this issue we document such nuisances, so that we can eventually fix them altogether.
Adequacy:
aneris_prefixtidand thus cannot be used with locales)Model:
Also see #23, #24, #31