Require Export Quorum.
Require Export Process.


Section SM2.

  Local Open Scope eo.
  Local Open Scope proc.

  Context { dtc : @DTimeContext }.
  Context { pt  : @TimeConstraint dtc }.

  Class SMcontext :=
    MkSMcontext
      {
        (* number of faults *)
        F : nat;

        (* ++++++++ Nodes ++++++++ *)
        num_generals : nat;
        num_generals_non_empty : 0 < num_generals;
        num_generals_constraint : F <= num_generals;

        Gen : Set; (* same as in paper, replica 0 is commander *)
        gen_deq : Deq Gen;
        gens2nat : Gen -> nat_n num_generals;
        gens_bij : bijective gens2nat;

        SMtoken    : Set;
        SMtokendeq : Deq SMtoken;

        sm_value : Set;
        sm_default_value : sm_value;
        sm_value_deq : Deq sm_value;
        sm_choice : list sm_value -> sm_value;
        sm_choice_cond1 : forall v, sm_choice [v] = v;
        sm_choice_cond2 : sm_choice [] = sm_default_value;
        sm_choice_cond3 : forall l1 l2, eqset l1 l2 -> sm_choice l1 = sm_choice l2;

        sm_initial_values : Gen -> sm_value;

        SMsending_key   : Set;
        SMreceiving_key : Set;
      }.

  Context { sm_context : SMcontext }.


  Lemma sm_choice_diff :
    forall l1 l2,
      sm_choice l1 <> sm_choice l2
      ->
      exists v,
        (In v l1 /\ ~ In v l2)
        \/
        (In v l2 /\ ~ In v l1).
  Proof.
    introv h.
    destruct (eqset_dec l1 l2 sm_value_deq) as [d|d].
    { apply sm_choice_cond3 in d; rewrite d in *; tcsp. }
    apply not_eqset_implies; auto.
    apply sm_value_deq.
  Qed.


  (* ===============================================================
     No trusted component
     =============================================================== *)

  Global Instance SM_I_IOTrusted : IOTrusted := Build_IOTrusted unit unit tt.


  Inductive General :=
  | general (n : Gen).

  Coercion general : Gen >-> General.

  Definition General2Gen (g : General) : Gen :=
    match g with
    | general n => n
    end.

  Coercion General2Gen : General >-> Gen.

  Lemma GeneralDeq : Deq General.
  Proof.
    introv; destruct x as [g1], y as [g2].
    destruct (gen_deq g1 g2);[left|right]; subst; auto.
    intro xx; inversion xx; subst; tcsp.
  Defined.

  Global Instance SM_I_Node : Node := MkNode General GeneralDeq.

  Lemma general_inj : injective general.
  Proof.
    introv h; ginv; auto.
  Qed.

  Definition General2GenOp (g : General) : option Gen :=
    Some (General2Gen g).

  Lemma Gen2General_cond : forall n, General2GenOp (general n) = Some n.
  Proof.
    tcsp.
  Qed.

  Lemma General2Gen_cond : forall n m, General2GenOp m = Some n -> general n = m.
  Proof.
    introv h.
    unfold General2GenOp in h; ginv; simpl; destruct m; auto.
  Qed.

  Global Instance SM_I_Quorum : Quorum_context :=
    MkQuorumContext
      Gen
      num_generals
      gen_deq
      gens2nat
      gens_bij
      _
      _
      Gen2General_cond
      General2Gen_cond
      general_inj.

  Definition SMtokens := list SMtoken.

  Global Instance SM_I_AuthTok : AuthTok :=
    MkAuthTok
      SMtoken
      SMtokendeq.


  (* 0 is less than F+2 *)
  Definition nat_n_Fp2_0 : nat_n num_generals.
  Proof.
    exists 0.
    apply leb_correct.
    apply num_generals_non_empty.
  Defined.

  Definition general0 : Gen := bij_inv gens_bij nat_n_Fp2_0.

  Definition nat2gen (n : nat) : Gen.
  Proof.
    destruct gens_bij as [f a b].
    destruct (lt_dec n num_generals) as [d|d].
    - exact (f (mk_nat_n d)).
    - exact general0.
  Defined.

  Definition SMcommander : Gen := nat2gen 0.

  Definition is_commander (g : Gen) : bool :=
    if gen_deq g SMcommander then true else false.

  Definition is_lieutenant (g : Gen) : bool := negb (is_commander g).

  Lemma is_commander_false :
    forall n, is_commander n = false <-> n <> SMcommander.
  Proof.
    introv.
    unfold is_commander.
    dest_cases w; split; intro h; tcsp.
  Qed.

  Lemma is_commander_true :
    forall n, is_commander n = true <-> n = SMcommander.
  Proof.
    introv.
    unfold is_commander.
    dest_cases w; split; intro h; tcsp.
  Qed.

  Definition sm_signs := list Sign.

  (* here message contains a Set of generals who already saw this value *)
  Record sm_signed_msg :=
    MkSmSignedMsg
      { sm_signed_msg_value : sm_value;
        sm_signed_msg_signs : list Sign;
        sm_signed_msg_sign  : Sign}.

  Inductive SMmsg : Type :=
  | sm_msg_init
  | sm_msg_alarm
  | sm_msg_signed (v : sm_signed_msg)
  | sm_msg_result (v : sm_value).

  Global Instance SM_I_Msg : Msg := MkMsg SMmsg.


  Definition SMmsg2status (m : SMmsg) : msg_status :=
    match m with
    | sm_msg_init     => MSG_STATUS_INTERNAL
    | sm_msg_alarm    => MSG_STATUS_INTERNAL
    | sm_msg_signed _ => MSG_STATUS_PROTOCOL
    | sm_msg_result _ => MSG_STATUS_INTERNAL (* sent to itself *)
    end.

  Global Instance SM_I_get_msg_status : MsgStatus := MkMsgStatus SMmsg2status.

  Record sm_bare_signed_msg :=
    MkSmBareSignedMsg
      { sm_bare_signed_msg_value : sm_value;
        sm_bare_signed_msg_gen   : Gen }.

  Inductive SMbare_msg : Type :=
  | sm_bare_msg_signed (v : sm_bare_signed_msg)
  | sm_bare_msg_result (v : sm_value).

  Global Instance SM_I_Data : Data := MkData SMbare_msg.


  Definition sm_signed_msg2value (m : sm_signed_msg) : sm_value :=
    sm_signed_msg_value m.

  Definition SMmsg2value (m : SMmsg) : option sm_value :=
    match m with
    | sm_msg_init     => None
    | sm_msg_alarm    => None
    | sm_msg_signed v => Some (sm_signed_msg2value v)
    | sm_msg_result v => Some v
    end.

  Definition sm_signed_msg2sign (m : sm_signed_msg) : Sign :=
    match m with
    | MkSmSignedMsg v l a => a
    end.

  Definition sm_signed_msg2auth (m : sm_signed_msg) : SMtokens :=
    sign_token (sm_signed_msg2sign m).

  Definition sm_signed_msg2sender (m : sm_signed_msg) : Gen :=
    sign_name (sm_signed_msg2sign m).

  (* Note: add the last signature at the beginning of the list *)
  Definition sm_signed_msg2signs_old (m : sm_signed_msg) : list Sign :=
    match m with
    | MkSmSignedMsg _ l a => [a] ++ l
    end.

  Fixpoint sm_signed_msg2signs_temp
           (v   : sm_value)
           (l   : list Sign)
           (a   : Sign) : list Sign :=
    match l with
    | [] => [a]
    | el :: l' => snoc (sm_signed_msg2signs_temp v l' el) a
    end.

  Definition sm_signed_msg2signs (m : sm_signed_msg) : list Sign :=
    match m with
    | MkSmSignedMsg v l a => sm_signed_msg2signs_temp v l a
    end.


  (* only the last sender *)
  Definition SMmsg2sender (m : SMmsg) : option Gen :=
    match m with
    | sm_msg_init     => None
    | sm_msg_alarm    => None
    | sm_msg_signed v => Some (sm_signed_msg2sender v)
    | sm_msg_result v => None
    end.

  Definition sm_signed_msg2senders_old (m : sm_signed_msg) : list Gen :=
    match m with
    | MkSmSignedMsg v l a => snoc (rev (map sign_name l))  (sign_name a)
    end.

  Fixpoint sm_signed_msg2senders_temp
           (v  : sm_value)
           (l  : list Sign)
           (a  : Sign)  : list Gen :=
    match l with
    | [] => [(sign_name a)]
    | el :: l' => snoc (sm_signed_msg2senders_temp v l' el) (sign_name a)
    end.

  Definition sm_signed_msg2senders (m : sm_signed_msg) : list Gen :=
    match m with
    | MkSmSignedMsg v l a => sm_signed_msg2senders_temp v l a
    end.

  (* all senders; correct order *)
  Definition SMmsg2senders (m : SMmsg) : list Gen :=
    match m with
    | sm_msg_init     => []
    | sm_msg_alarm    => []
    | sm_msg_signed v => sm_signed_msg2senders v
    | sm_msg_result v => []
    end.

  (* only the last signature *)
  Definition SMmsg2sign (m : SMmsg) : option SMtokens :=
    match m with
    | sm_msg_init     => None
    | sm_msg_alarm    => None
    | sm_msg_signed v => Some (sign_token (sm_signed_msg2sign v))
    | sm_msg_result v => None
    end.

  (* all signatures; correct order *)
  Fixpoint SMmsg2signs (m : SMmsg) : list SMtokens :=
    match m with
    | sm_msg_init     => []
    | sm_msg_alarm    => []
    | sm_msg_signed v => map sign_token (sm_signed_msg2signs v)
    | sm_msg_result v => []
    end.

  Definition gens : list Gen := nodes.
  Definition ngens : list name := map general gens.

  Lemma gens_prop : forall (x : Gen), In x gens.
  Proof.
    exact nodes_prop.
  Qed.
  Hint Resolve gens_prop : sm2.

  Global Instance SM_I_Key : Key := MkKey SMsending_key SMreceiving_key.

  Class SMauth :=
    MkSMauth
      {
        SMcreate : data -> sending_keys -> SMtokens;
        SMverify : data -> name -> receiving_key -> SMtoken -> bool
      }.
  Context { sm_auth : SMauth }.

  Global Instance SM_I_AuthFun : AuthFun :=
    MkAuthFun
      SMcreate
      SMverify.

  Class SMinitial_keys :=
    MkSMinitial_keys {
        initial_keys : key_map;
      }.

  Context { sm_initial_keys : SMinitial_keys }.

  Definition sm_values := list sm_value.

  Record SMstate :=
    Build_SMstate
      {
        (* some initial value *)
        init          : sm_value;

        (* the values we received *)
        V             : sm_values;

        (* The keys that we're holding to communicate with the other replicas *)
        local_keys    : local_key_map;
      }.


  Definition SMinitial_state (g : Gen) (init : sm_value) : SMstate :=
    Build_SMstate
      init
      []
      (initial_keys (general g)).


  (****************************************************************************************)

  Definition sm_bare_signed_msg2general (m : sm_bare_signed_msg) : General :=
    match m with
    | MkSmBareSignedMsg v g => general g
    end.

  Definition SMdata_auth (n : name) (m : data) : option name :=
    match m with
    | sm_bare_msg_signed v => Some (sm_bare_signed_msg2general v)
    | sm_bare_msg_result v => Some n
    end.

  Global Instance SM_I_DataAuth : DataAuth := MkDataAuth SMdata_auth.

  Definition sm_signed_msg2bare (m : sm_signed_msg) : sm_bare_signed_msg :=
    match m with
    | MkSmSignedMsg v l a => MkSmBareSignedMsg v (node2name (sign_name a))
    end.

  Definition sm_signed_msg2top_auth_data (m : sm_signed_msg) : AuthenticatedData :=
    MkAuthData (sm_bare_msg_signed (sm_signed_msg2bare m)) (sm_signed_msg2auth m).

  Definition sm_signed_msg2main_auth_data (m : sm_bare_signed_msg) (t  : SMtokens) : AuthenticatedData :=
    MkAuthData (sm_bare_msg_signed m) t.

  Fixpoint sm_signed_msg2list_auth_data_temp
             (v    : sm_value)
             (l    : list Sign)
             (a    : Sign) : list AuthenticatedData :=
    let m := MkSmBareSignedMsg v (sign_name a) in
    match l with
    | [] => [sm_signed_msg2main_auth_data m (sign_token a)]
    | el :: ol =>  let m' := MkSmBareSignedMsg v (sign_name a) in
                   snoc (sm_signed_msg2list_auth_data_temp v ol el) (sm_signed_msg2main_auth_data m (sign_token a))
    end.


  Definition sm_signed_msg2list_auth_data (m : sm_signed_msg) : list AuthenticatedData :=
    match m with
    | MkSmSignedMsg v l a => sm_signed_msg2list_auth_data_temp v l a
    end.

  Definition SMget_contained_auth_data (m : SMmsg) : list AuthenticatedData :=
    match m with
    | sm_msg_init     => []
    | sm_msg_alarm    => []
    | sm_msg_signed v => sm_signed_msg2list_auth_data v
    | sm_msg_result v => [] (* these are not signed *)
    end.

  Global Instance SM_I_ContainedAuthData : ContainedAuthData :=
    MkContainedAuthData SMget_contained_auth_data.

  (* Here, we check that all signatures are correct *)
  Definition verify_signed_msg_sign (slf : Gen) (lkm : local_key_map) (m : sm_signed_msg) : bool :=
    forallb
      (fun a => verify_authenticated_data (general slf) a lkm)
      (sm_signed_msg2list_auth_data m).

  Fixpoint sm_signed_msg2sing_temp (v : sm_value) (l : list Sign) (a : Sign) : sm_value * Sign :=
    match l with
    | [] => (v, a)
    | el :: ol => sm_signed_msg2sing_temp v ol el
    end.

  Definition sm_signed_msg2sing (m : sm_signed_msg) : sm_value * Sign :=
    match m with
    | MkSmSignedMsg v l a => sm_signed_msg2sing_temp v l a
    end.

  (* Here, we check that the first one to sign was the commander *)
  Definition verify_msg_commander (m : SMmsg) : bool :=
    match m with
    | sm_msg_init  => false
    | sm_msg_alarm => false
    | sm_msg_signed v =>
      let (_,a) := sm_signed_msg2sing v in
      is_commander (sign_name a)
    | sm_msg_result _ => false
    end.

  (* Here, we check that the first one to sign was the commander *)
  Definition verify_signed_msg_commander (m : sm_signed_msg) : bool :=
    is_commander (sign_name (snd (sm_signed_msg2sing m))).

  Definition is_sm_signed_msg2directly_from_commander (m : sm_signed_msg) : bool :=
    match m with
    | MkSmSignedMsg v l a  => match l with
                              | [] => is_commander (sign_name a)
                              | _ => false
                              end
    end.

  Definition verify_signed_msg (slf : Gen) (lkm : local_key_map) (m : sm_signed_msg) : bool :=
    (* all signatures have to be correct *)
    (verify_signed_msg_sign slf lkm m)
      (* the first signer has to be the commander *)
      && (verify_signed_msg_commander m)
      (* the senders have to be different from each other *)
      && (norepeatsb gen_deq (sm_signed_msg2senders m))
      (* the receiver should not be in the list of signers *)
      && (not_inb gen_deq slf (sm_signed_msg2senders m)).


  Definition check_new_value
             (V : sm_values (*value_and_senders*))
             (m : sm_signed_msg) : bool :=
    if in_dec sm_value_deq (sm_signed_msg2value m) V then false
    else true.


  (* message has the form (v:0) *)
  Definition commander_message (m : SMmsg) : bool := verify_msg_commander m.

  (* message has the form (v:0:j1:...jk) *)
  Definition commander_lieutenant (m : SMmsg) : bool := negb (verify_msg_commander m).

  (* general have not received any order yet *)
  Definition no_order_yet (V : sm_values (*value_and_senders*)) : bool := nullb V.


  Definition add_to_V (s : SMstate) (v : sm_value) : SMstate :=
    Build_SMstate
      (init          s)
      (v ::        V s)
      (local_keys    s).


  Definition extend_signed_msg
             (m    : sm_signed_msg)
             (g    : General)
             (keys : local_key_map) : sm_signed_msg :=
    match m with
    | MkSmSignedMsg v ls a =>  let ls' := [a] ++ ls in
                               let b  := MkSmBareSignedMsg v g in
                               let a' := authenticate (sm_bare_msg_signed b) keys in
                               MkSmSignedMsg v ls' (MkSign (General2Gen g) a')
    end.


  Definition extend_msg
             (m    : SMmsg)
             (g    : General)
             (keys : local_key_map) : SMmsg :=
    match m with
    | sm_msg_init     => m
    | sm_msg_alarm    => m
    | sm_msg_signed v => sm_msg_signed (extend_signed_msg v g keys)
    | sm_msg_result v => m
    end.

  Definition send_sm_msg_commander (m : SMmsg) (n : list name) : DirectedMsg :=
    MkDMsg m n ('0).

  Definition send_sm_msg_lieutenant (m : SMmsg) (n : list name) : DirectedMsg :=
    MkDMsg m n ('0).

  Definition gens_not_in_list (l : list Gen) : list Gen :=
    diff gen_deq l gens.

  Definition names_not_in_list (l : list Gen) : list name :=
    map general (gens_not_in_list l).

  Definition broadcast2not_in_list (l : list Gen) F : DirectedMsg :=
    F (names_not_in_list l).

  Definition create_new_sm_signed_msg
             (v    : sm_value)
             (keys : local_key_map) : sm_signed_msg :=
    let b  := MkSmBareSignedMsg v (general SMcommander) in
    let a := authenticate (sm_bare_msg_signed b) keys in
    MkSmSignedMsg v [] (MkSign SMcommander a).

  Definition create_new_msg_commander
             (v    : sm_value)
             (keys : local_key_map) : SMmsg :=
    sm_msg_signed (create_new_sm_signed_msg v keys).

  Definition create_new_msg_result (v : sm_value) : SMmsg:=
    let b := sm_bare_msg_result v in
    sm_msg_result v.

  (* NOTE: The paper is not clear what lieutenants do with their decision at the end.
     We send the final decision to ourselves. *)
  Definition send_sm_msg_result (slf : Gen) (m : sm_value) : DirectedMsg :=
    MkDMsg (sm_msg_result m) [general slf] ('0).


  Definition send_alarm (slf : Gen) : DirectedMsg :=
    MkDMsg sm_msg_alarm [general slf] (pdt_mult ('(S F)) (pdt_plus mu tau)).


  (* handler of initial message sent to commander to start it *)
  Definition SMhandler_initial (slf : Gen) : Update SMstate unit DirectedMsgs :=
    fun state v t =>
      let keys   := local_keys state in
      let V_list := V state in

      if dt_eq_dec t (nat2pdt 0) then

        if is_commander slf then
          let new_msg := create_new_msg_commander (init state) keys in
          let new_state1 := add_to_V state (init state) in

          (* commander broadcasts new message to all replicas *)
          (Some new_state1, [broadcast2not_in_list [SMcommander] (send_sm_msg_commander new_msg)])

        else
          (Some state, [send_alarm slf])

      else (* initial messages are supposed to be received at time 0 *)
        (Some state, []).



  Definition message_is_on_time (m : sm_signed_msg) (t : PosDTime) : bool :=
    let signs := sm_signed_msg2signs m in
    if dt_le_lt_dec t (nat2pdt (length signs) * (mu + tau))%dtime then
      (* We don't care about messages with more than F+1 signatures,
         we're not supposed to send any: *)
      if le_dec (length signs) (S F) then true else false
    else false.


  Definition SMhandler_lieutenant (slf : Gen) : Update SMstate sm_signed_msg DirectedMsgs :=
    fun state m time =>
      let keys := local_keys state in
      let Vs   := V state in

      if is_lieutenant slf then

        if verify_signed_msg slf keys m then

          if message_is_on_time m time then

            (* is message of the form (v:0), i.e., commander message *)
            if is_sm_signed_msg2directly_from_commander m then

              (* lieutenant have not received any order yet *)
              if no_order_yet Vs then

                (* add value (received with msg m) to the V, assuming that general have not received any order yet *)
                let new_state1 := add_to_V state (sm_signed_msg2value m) in

                if 1 <=? F then

                  (* create new message v:0:i *)
                  let new_signed_msg := extend_signed_msg m (general slf) keys in
                  let new_msg := sm_msg_signed new_signed_msg in

                  (* we broadcast new message to all replicas that are not in the message i.e. commander in this case *)
                  (Some new_state1, [broadcast2not_in_list [slf,SMcommander] (send_sm_msg_lieutenant new_msg)])

                else
                  (Some new_state1, [])

              else (* message has the form (v:0), but lieutenant has some order already received *)
                (Some state, [])

            else (* message is not of the form (v:0), i.e., commander message
              i.e., message has the form (v:0:j1:..:jk *)

              (* if this is the value that was not received before *)
              if check_new_value Vs m then

                (* add value (received with msg m) to the V, assuming that general already received some value *)
                let new_state1 := add_to_V state (sm_signed_msg2value m) in

                (* if k < m , i.e., (if number of senders is less than number of faults) then broadcast the message *)
                (* NOTE : F + 1 because commander is one of the senders *)
                if length (sm_signed_msg2senders m) <=? F then

                  (* create new message v:0:j1:...:jk:i *)
                  let new_signed_msg := extend_signed_msg m (general slf) keys in
                  let new_msg := sm_msg_signed new_signed_msg in

                  let ls := sm_signed_msg2senders m in

                  (* we broadcast new message to all replicas that were not in the message *)
                  (Some new_state1, [broadcast2not_in_list (slf :: ls) (send_sm_msg_lieutenant new_msg)])

                else (* number of senders is not less than number of faults,
                  i.e., in this case lieutenant obeys the order determined with choice(V) *)
                  (Some new_state1, [])

              else (* this value was received before *)
                (Some state, [])

          else (* message is not on time *)
            (Some state, [])

        else (* message is not signed properly *)
          (Some state, [])

      else (* not a lieutenant *)
        (Some state, []).


  Definition SMhandler_result (slf : Gen) : Update SMstate sm_value DirectedMsgs :=
    fun state _ _ => (Some state, []).


  Definition SMhandler_alarm (slf : Gen) : Update SMstate unit DirectedMsgs :=
    fun state _ t =>
      if is_lieutenant slf then
        if dt_le_lt_dec t (pdt_mult ('(S F)) (pdt_plus mu tau))
        then (Some state, []) (* this shouldn't happen because the alarm was set to [(F+1)*(mu+tau)] *)
        else
          let choice := sm_choice (V state) in
          (* we send the signed msg that contains choice to all other replicas *)
(*          let new_msg := create_new_msg_result choice in *)
          (Some state, [send_sm_msg_result slf choice])
      else (Some state, []).


  (*
     NOTE:

     - The init message has to be sent to the commander at time T0
     - Alarms have to be sent to the lieutenants at time T0, and have to be
       set as in [send_alarm].
   *)
  Definition SMupdate (slf : Gen) : MUpdate SMstate :=
    fun state m =>
      match m with
      | sm_msg_init     => SMhandler_initial    slf state tt
      | sm_msg_alarm    => SMhandler_alarm      slf state tt
      | sm_msg_signed v => SMhandler_lieutenant slf state v
      | sm_msg_result v => SMhandler_result     slf state v
      end.

  Definition SMreplicaSM (slf : Gen) : MStateMachine _ :=
    mkSM
      (SMupdate slf)
      (SMinitial_state slf (sm_initial_values slf)).

  Definition SMsys : MUSystem (fun n => SMstate) := SMreplicaSM.

End SM2.


Hint Resolve gens_prop : sm2.
