SSL inexact_comm.pvs

%
% Purpose: properties of inexact communication through 
%          multiple-stages
%
%

inexact_comm
[
    N   : [nat -> posnat]
] : THEORY

  BEGIN

  IMPORTING
    node_functions[N, real],
    inexact_comm_stage

  i, j, k: VAR nat

  sources: VAR [j : nat -> finite_set[below(N(j))]] 

  sent:  VAR sent_vec
  rcvd:  VAR rcvd_matrix
  check: VAR check_function
  epsilon: VAR [nat -> nonneg_real]
  tau: VAR [i: nat -> tau_type]
  cf: VAR [nat -> consensus_function]


  %
  % Abstracted fault assumptions
  %

  % same predicate is in exact_comm
  enabled_within?(rcvd, check, j, k)(sources): bool = 
    FORALL i : j <= i AND i < k IMPLIES
      enabled_within?[N(i), N(i + 1), real](rcvd(i), check(i))(sources(i))
  
  % (simple) majority

  majority_lower?(sent, rcvd, check, epsilon, j, k): bool =
    FORALL i : j <= i AND i < k IMPLIES
      majority_lower?[N(i), N(i + 1)](sent(i), rcvd(i), check(i), epsilon(i))

  majority_upper?(sent, rcvd, check, epsilon, j, k): bool =
    FORALL i : j <= i AND i < k IMPLIES
      majority_upper?[N(i), N(i + 1)](sent(i), rcvd(i), check(i), epsilon(i))

  majority_imprecision?(sent, rcvd, check, epsilon, j, k): bool =
    FORALL i : j <= i AND i < k IMPLIES
      majority_imprecision?[N(i), N(i + 1)](sent(i), rcvd(i), check(i), epsilon(i))

  exists_all_symmetric?(sent, rcvd, check, epsilon, cf, j, k): bool =
    EXISTS i: j <= i AND i < k AND
      inexact_consensus?(cf(i)) AND
      all_symmetric?(rcvd(i), check(i), epsilon(i)) AND
      majority_imprecision?(sent, rcvd, check, epsilon, i + 1, k)

  % quorum, a generalized majority (from simple to consensus to unamimous)

  quorum_lower?(sent, rcvd, check, tau, epsilon, j, k): bool =
    FORALL i : j <= i AND i < k IMPLIES
      quorum_lower?[N(i), N(i + 1)](sent(i), rcvd(i), check(i), tau(i), epsilon(i))

  quorum_upper?(sent, rcvd, check, tau, epsilon, j, k): bool =
    FORALL i : j <= i AND i < k IMPLIES
      quorum_upper?[N(i), N(i + 1)](sent(i), rcvd(i), check(i), tau(i), epsilon(i))

  quorum_imprecision?(sent, rcvd, check, tau, epsilon, j, k): bool =
    FORALL i : j <= i AND i < k IMPLIES
      quorum_imprecision?[N(i), N(i + 1)](sent(i), rcvd(i), check(i), tau(i), epsilon(i))

  exists_all_symmetric?(sent, rcvd, check, tau, epsilon, cf, j, k): bool =
    EXISTS i: j <= i AND i < k AND
      inexact_consensus?(cf(i)) AND
      all_symmetric?(rcvd(i), check(i), epsilon(i)) AND
      quorum_imprecision?(sent, rcvd, check, tau, epsilon, i + 1, k)


END inexact_comm