%
%
% Purpose : Validity and agreement properties for all destination
%           nodes of a k-stage exact exchange.
%           Assumes, no error is introduced during communication (this 
%           is the definition of exact communication).
%
%


exact_reduce
[
    N   : [nat -> posnat],  
    T   : TYPE+,
    <=  : (total_order?[T]),              
    error: [nat -> T]
] : THEORY

  BEGIN

  IMPORTING
    exact_comm[N, T],
    protocol[N, T],
    k_ordered[N, T, <=, error],
    exact_reduce_stage

  i, j, k: VAR nat
  v: VAR T

  node_set: VAR [j : nat -> non_empty_finite_set[below(N(j))]] 

  check: VAR check_function
  sent:  VAR sent_vec
  rcvd:  VAR rcvd_matrix

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

  %
  % Main results
  %

  lower_validity: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_correct?(sent, rcvd, check, tau, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set) 
    IMPLIES
      v_min(sent, node_set)(j) <= v_min(sent, node_set)(j + k)

  upper_validity: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_correct?(sent, rcvd, check, tau, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set) 
    IMPLIES
      v_max(sent, node_set)(j + k) <= v_max(sent, node_set)(j)

  consensus_validity: COROLLARY
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_correct?(sent, rcvd, check, tau, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set) AND
      uniform?(sent(j), v)(node_set(j))
    IMPLIES
      uniform?(sent(j + k), v)(node_set(j + k))

  exact_agreement_propagation: COROLLARY
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      quorum_correct?(sent, rcvd, check, tau, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set) AND
      v_max(sent, node_set)(j) = v_min(sent, node_set)(j)
    IMPLIES
      v_max(sent, node_set)(j + k) = v_min(sent, node_set)(j + k)

  agreement_generation: THEOREM
      protocol(reduce_choice(tau, cf), sent, rcvd, check, j, j + k) AND
      exists_all_symmetric?(sent, rcvd, check, tau, j, j + k) AND
      enabled_within?(rcvd, check, j, j + k)(node_set)
    IMPLIES
      v_max(sent, node_set)(j + k) = v_min(sent, node_set)(j + k) 

END exact_reduce