Merge COMPASS (ci/compass) into gpfsl-examples

_CoqProject

gpfsl-examples/algebra/mono_list_list.v

gpfsl-examples/big_op.v

gpfsl-examples/event/event.v

gpfsl-examples/event/ghost.v

gpfsl-examples/exchanger/code.v

gpfsl-examples/exchanger/proof_graph.v

gpfsl-examples/exchanger/proof_graph_piggyback.v

gpfsl-examples/exchanger/proof_graph_resource.v

gpfsl-examples/exchanger/proof_graph_resource_closed.v

gpfsl-examples/exchanger/proof_mp_client.v

gpfsl-examples/exchanger/proof_sequential_client.v

gpfsl-examples/exchanger/spec_graph.v

gpfsl-examples/exchanger/spec_graph_piggyback.v

gpfsl-examples/exchanger/spec_graph_resource.v

gpfsl-examples/graph/ghost.v

gpfsl-examples/graph/graph.v

gpfsl-examples/graph/graph_extend.v

gpfsl-examples/graph/map_helper.v

gpfsl-examples/graph/spec.v