aneris
aneris copied to clipboard
logsem
Program logic for developing and verifying distributed systems
Implemented an instance of `Lookup nat (St * option (L * St)) (trace St L)` for an easy access to `i`th transition in a trace. An example usage included in...
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...
Compilation of the current external submodules produce warnings, as a result of them not having been bumped since moving to Coq 8.17. These should be bumped, and the Aneris repo...
Currently `state_heaps` and `state_sockets` are required to have the same domain, as they both signify the existence of a node on the given ip. To achieve this constructively, rather than...
Currently, `free_ports` only arise from using `Ht-start`, and giving up `free_ips`. This put unecessary coupling between the `free_ips` and `free_ports` resources. A suggestion is then to separate the two, by...