|
%
%
% 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
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
