%
%
% Purpose : a reduce-select choice multiple-stage exchange
%           under an integration fault model and exact communication.
%
%


exact_reduce_integration
[
  N: [nat -> posnat],
  T: TYPE+,
  <= : (total_order?[T]),
  (IMPORTING ordered_message[T,<=])
  source_error: [nat -> message]
] : THEORY

BEGIN

  i, j, k: VAR nat

  IMPORTING
    ordered_message[T,<=],
    protocol_integration[N, T],
    exact_reduce[N, message, ordered_message.<=, source_error]

  status:       VAR [i : nat -> node_status[N(i)]]
  sent:         VAR [i : nat -> [below(N(i)) -> message]]
  local:        VAR [i : nat -> [below(N(i)) -> T]]
  common_check: VAR [i: nat -> non_empty_finite_set[below(N(i))]]
  msg_check:    VAR valid_check_function
  check:        VAR valid_check_function

  tau: VAR [j: nat -> tau_type]
  cf: VAR k_consensus_function

  lower_validity: THEOREM
      check = conforms(msg_check, common_check) AND
      protocol(sent, check, reduce_choice(tau, cf), status, j, j + k) AND
      quorum_correct?(sent, check, status, tau, j, j + k)
    IMPLIES
      v_min(sent, common_check)(j) <= v_min(sent, common_check)(j + k)

  upper_validity: THEOREM
      check = conforms(msg_check, common_check) AND
      protocol(sent, check, reduce_choice(tau, cf), status, j, j + k) AND
      quorum_correct?(sent, check, status, tau, j, j + k)
    IMPLIES
      v_max(sent, common_check)(j + k) <= v_max(sent, common_check)(j)

  agreement_generation: THEOREM
      check = conforms(msg_check, common_check) AND
      protocol(sent, check, reduce_choice(tau, cf), status, j, j + k) AND
      exists_all_symmetric?(sent, check, status, tau, j, j + k)
    IMPLIES
      v_max(sent, common_check)(j + k) = v_min(sent, common_check)(j + k)

END exact_reduce_integration