Porting LARA
We need to port LARA from iGPS to GPFSL. The following files are to be ported:
-
/logically_atomic.v → /logic/logically_atomic.v -
/invariants.v → /logic/obj_invariants.v -
/examples/snapshot.v → /examples/frac_auth.v and snapshot.v -
/examples/hist_protocol.v? -
/examples/list_lemmas.v → /base_logic/list_lemmas.v -
/examples/abs_hashtable.v → /examples/abs_hashtable.v -
/examples/hashtable.v -
/examples/for_loop.v → /logic/for_loop.v -
/examples/repeat.v → /logic/repeat.v -
/examples/kvnode.v → /examples/kvnode.v -
/examples/kvnode2.v -
/gps/shared2.v -
recursive protocol?