Reliable communication components (#9)

* [lf] Notes with specs discussed at the meeting for the leader-followers replication.

* [repdb] API Specifications.

* [repdb] fix spec w.r.t. ras.

* [repdb] Two closed examples to verify.

* [repdb] more specs.

* [repdb] A sketch of dependent sep. protocols for generic server and two instantiations for leader-client interaction.

* [repdb] Complete and factor out the multithreaded server as a library. Now leader-followers do not use directly client-server at all, only relying on the mt-server.

* [repdb] User_spec_params class and the specified API for the MT server.

* [repdb] Spec and Proof of the multi-threaded service library.

* [repdb] wip on resources.

* [lf] wip.

* [lf] Sketch of resources.

* [lf] fix local validity gmap.

* [lf] wip on resources and fixes.

* [lf] Sketch of mt_spec_params for the leader.

* [lf and mt] A fix splitting mt_params so that socket_protocols are definable at the adequacy.

* [lf] Back to keeping indexes (time) in the physical log - to please the Inject class but also it makes sense.

* [lf] wip on logs (needs mono_list straight away).

* [lf] Further anticipations for instanciating resources, proving init class and adequacy.

* [lf] Proof of client proxy (relying on the assumed proof of the handler in the MT spec params).

* [lf] Generic definition logical logs and the proof of the physical log (including the proof of log_wait_until).

* [lf] wip.

* [lf] Defining monitor resources using generic log_monitor definition.

* [lf] wip on update_log_copy proof.

* [lf] Proof of update log copy at leader.

* [lf] Proof of init_leader.

* [lf] Proof of follower_request_handler.

* [lf] First sketch of dlm_db_example proof skeleton (to be improved in the next commit).

* [lf] Wip on the dlm_db_example proof.

* [lf] Assembled proof of dlm_db_example including adequacy (but assuming proof of the code and instance of db_init class (TODO).

* [lf] More proofs for the dlm_db_example.

* [lf] More proof for dlm_db_example.

* [lf] Proof of the do_writes.

* [lf] Proof of do_reads in the dlm_db_example.

* [lf] small clean up.

* [lf] The proof of the dlm_db_example.

* Clean up of redundant `True` preconditions

* Clean up and removed some `Unshelve`s

* Added proof of do_writes / do_reads of causality

* [lf] wip and sketch for causality example with reading at a follower.

* [lf] some ideas on proving causality example (in a sep. file) but no success so fart.

* [lf] Proof of the read request at the leader's handler.

* [lf] wip on proof of client handler (almost done).

* [lf] Proof of the client handler at the leader done.

* [lf] Proof of the client request handler at the follower.

* [lf] Wip on follower's sync loop.

* [lf] Fix the proof of followers handler.

* [lf] Proof of follower sync loop done.

* [lf] Various fixes in the spec due to an error in the db_init_class. Proof of the client proxy at follower done (but the problem with ghost names is to be fixed).

* [lf] 1. Introducing a global N of type gmap saddr gname. 2. Proof of init client proxy for followers. 3. Fixes.

* [lf] Wip on proof of init follower (last bit before proving setup and spec refinement).

* [lf] The internal proof of the leader followers done (up to logical setup).

* [lf] Wip on init_setup proof.

* [lf] more proof for init_setup.

* Causality example (#4)

* [lf] wip on proof of init.

* [lf] fix.

* [lf] fixes.

* Lifted log_resources lemmas

* Proved resources_def lemmas

* Progress on global resource lemmas

* [lf] Wip on proof of db init.

* Bumped strengthened lemmas

* [lf] More wip on proof of init setup.

* [lf] Proof of init setup for leader follower done.

* Proved two alloc lemmas

* prove some admitted lemmas

* Proved last init lemma

* Commented out API lemmas that are not used

* Proved another lemma

* one more admitted now proved

* Prove two lemmas in resources_global_inv

* Proved another global lemma

* Closed final lemma

* Clean up: Unshelves, indents, etc.

* Spec clean up

* Removed inline universal quantifications from abstract specs

* Simplified specs with unit as a return value

* Fixed pure postcondition

* Removed some more explicit arguments

* Removed more true preconditions

* Removed unused hypothesis from dlm spec

* Improved DLM protocol definition

* [lf, mt-rpc] Improved implementation and spec of the rpc lib, following Jonas' suggestion.

* Hide locked inside of CanRelease

* DLM sa -> ip

* MT sa -> ip

* Reliable communication monitorless rpc (#7)

* Removed the monitors from the RPC library (still used in closures)

* [repl] Ocaml code.

Co-authored-by: Leon Gondelman <gondelman@cs.au.dk>

* Reliable communication rpc closures (#8)

Co-authored-by: Leon Gondelman <gondelman@cs.au.dk>
Co-authored-by: Amin Timany <amintimany@gmail.com>