Consensus.v

From VLSM.Lib Require Import Itauto.
From stdpp Require Import prelude finite.
From Coq Require Import Streams FunctionalExtensionality Eqdep_dec.
From VLSM.Lib Require Import Preamble ListExtras.
From VLSM.Core Require Import VLSM Plans VLSMProjections.

(** * Paxos: Abstract Specification of Consensus

  A very high-level specification of the consensus problem,
  following Lamport.

  It does not even explicitly model multiple nodes, just
  the set of values which any node thinks have been agreed
  upon as the consensus value.

  The only allowed transition is moving from an empty set
  to a singleton set.

  Note that this captures the safety and liveness properties
  of never thinking multiple (distinct) values have been selected
  and eventually selecting a value, but cannot specify any
  properties about if and when correct nodes learn of the consensus.
*)

Section sec_consensus_spec.

Context
  (V VSet : Type)
  `{FinSet V VSet}
  .

Definition consensus_state : Type := VSet.
Definition consensus_message : Type := False.

(**
  This type can be seen as a degenerate case when
  defining a sum type for expressing different steps
  in a transition system.
*)
Inductive consensus_action : Type :=
| Decided (v : V).

(**
  To enable TLA-style refinement, we need to allow stutter actions
  in our transition system. Hence, we use [None] to express stuttering,
  i.e., a no-op transition.
*)
Definition consensus_label : Type := option consensus_action.

Definition consensus_type : VLSMType False :=
{|
  state := consensus_state;
  label := consensus_label;
|}.

(**
  A [consensus_state] is initial when the the consensus set is empty.
*)
Definition consensus_initial_state_prop (s : consensus_state) : Prop := s ≡ ∅.

(** There are no initial messages. *)
Definition consensus_initial_message_prop (m : consensus_message) : Prop := False.

Definition consensus_valid (l : consensus_label) :
  consensus_state * option consensus_message -> Prop :=
  fun '(s, _) =>
  match l with
  | None => True
  | Some (Decided _) => s ≡ ∅
  end.

Definition consensus_transition (l : consensus_label) :
  consensus_state * option consensus_message -> consensus_state * option consensus_message :=
  fun '(s, _) =>
  match l with
  | None => (s, None)
  | Some (Decided v) => ({[ v ]} ∪ s, None)
  end.

Definition consensus_vlsm_machine : VLSMMachine consensus_type :=
{|
  initial_state_prop := consensus_initial_state_prop;
  s0 := populate (_ ↾ (reflexivity _ : consensus_initial_state_prop ∅));
  initial_message_prop := consensus_initial_message_prop;
  transition := consensus_transition;
  valid := consensus_valid;
|}.

Definition consensus_vlsm := mk_vlsm consensus_vlsm_machine.

Lemma consensus_invariant :
  forall (s : state consensus_vlsm),
    valid_state_prop _ s ->
    s ≡ ∅ \/ exists v : V, s ≡ {[ v ]}.
Proof.
  intros s Hs.
  induction Hs using valid_state_prop_ind; [by left |].
  destruct Ht as [(_ & _ & Hvalid) Hstep]; cbn in Hvalid.
  destruct l as [[v] |]; inversion Hstep; subst s'; [| done].
  right; exists v.
  by rewrite Hvalid, (right_id ∅ (∪)).
Qed.

End sec_consensus_spec.