%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46) $$$TOP.pvs % NASA Langley Research Center % Formal Methods Group % Maintainer: Lee Pike (lee.s.pike@nasa.gov) % Proof Files Generated for the paper % Model Checking Failed Conjectures in Theorem Proving: A Case Study % July 20, 2004 TOP [ B : posnat, % number of BIUs R : posnat, % number of RMUs T : NONEMPTY_TYPE % arbitrary message type ]: THEORY BEGIN IMPORTING ROBUS_IC_Protocol[B,R,T] F : VAR Local_State_Type % contains an algamation of all local states % information. `BB is the accessor of the BIUs % accusations of the BIUs; `RB is the accessor % of the RMUs accusations of the BIUs. b_status : VAR node_status[B] % fault status of a BIU r_status : VAR node_status[R] % fault status of an RMU G, b1, b2 : VAR below(B) % G is the general; b1, b2 are arbitrary BIUs msg : VAR T % arbitrary message % Unprovable--generates the counter-example. Agreement: CONJECTURE good?(b_status(b1)) AND good?(b_status(b2)) AND all_correct_accs?(b_status, r_status, F) AND IC_DMFA(b_status, r_status, F) => robus_ic(b_status, r_status, F`BB(b1)(G), F`RB(b1)) (G, msg, b1) = robus_ic(b_status, r_status, F`BB(b2)(G), F`RB(b2)) (G, msg, b2) END TOP $$$TOP.prf (TOP (Agreement 0 (Agreement-1 nil 3301049406 3301068426 ("" (skosimp*) (("" (rewrite "MFA_Agreement") (("1" (expand "all_correct_accs?") (("1" (flatten) (("1" (hide -3 -4 -6) (("1" (expand "correct_active?") (("1" (flatten) (("1" (expand "all_good_trusting?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "all_correct_accs?") (("2" (flatten) (("2" (hide -3 -4 -6) (("2" (expand "correct_active?") (("2" (flatten) (("2" (expand "all_good_trusting?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "all_correct_accs?") (("3" (flatten) (("3" (hide -3 -4 -6) (("3" (expand "correct_active?") (("3" (flatten) (("3" (expand "all_symmetric_agreement?") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "all_correct_accs?") (("4" (flatten) (("4" (hide -5 -4 -6) (("4" (expand "correct_active?") (("4" (flatten) (("4" (expand "all_declaration_agreement?") (("4" (expand "declaration_agreement?") (("4" (iff) (("4" (inst?) (("4" (inst - "b2!1") (("4" (assert) (("4" (inst - "G!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (copy -4) (("5" (expand "IC_DMFA" -5) (("5" (flatten) (("5" (split -6) (("1" (split 3) (("1" (case "declared?(F!1`BB(b2!1)(G!1))") (("1" (expand "all_correct_accs?") (("1" (flatten) (("1" (expand "correct_active?" -7) (("1" (flatten) (("1" (expand "all_declaration_agreement?") (("1" (inst - "b1!1" "b2!1") (("1" (assert) (("1" (expand "declaration_agreement?") (("1" (inst - "G!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "all_no_asymmetric_trusted?") (("2" (expand "no_asymmetric?" -2) (("2" (use "hybrid_majority_exists_good[R]") (("2" (skolem - "r!1") (("2" (inst?) (("2" (split) (("1" (inst?) (("1" (assert) (("1" (hide -4 -5 -7) (("1" (expand "trusted") (("1" (assert) (("1" (expand "no_asymmetric?") (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "all_hybrid_majority_good_trusted?" -6) (("2" (inst?) (("2" (assert) (("2" (lemma "elim_ic_relays_expand_hybrid_majority_good?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "all_hybrid_majority_good_trusted?" -6) (("3" (inst -6 "b2!1") (("3" (assert) (("3" (lemma "elim_ic_relays_expand_hybrid_majority_good?") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "all_no_asymmetric_trusted?") (("2" (inst-cp - "b1!1") (("2" (inst - "b2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 19018548 1550 nil nil))) $$$group_fault_model.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : group_fault_model.pvs % % Purpose : Provides a local fault classification of all LEFT nodes as % seen by all RIGHT nodes. LEFT and RIGHT are parameters. % % Design : SPIDER Version 0 % % Dependencies : hybrid_fault_types, global_fault_model, % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Alfons Geser % ICASE % 3 West Reid Street / MS 132 C % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-8003 % fax: 757-864-6134 % mailto: geser@icase.edu % http://www.icase.edu/~geser/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % February 22, 2002 - Created from material in local_fault_model % April 11, 2002 - Added predicate all_symmetric_declaring? % August 28, 2002 - Added all_agreement? and a few useful lemmas. % November 13, 2002 - Added all_subset? and a few lemmas. % - Added lemma no_asymmetric_agreement. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% group_fault_model [ N : posnat % number of defendants , O : posnat % number of observers ] : THEORY BEGIN IMPORTING local_fault_model[N] obs, o1, o2: var below(O) def: var below(N) G : below(N) statusn: var node_status[N] statuso: var node_status[O] Active_Sources_Type: NONEMPTY_TYPE = [below(O) -> Active_Vector_Type[N]] Active_Sources, act1, act2 : var Active_Sources_Type all_hybrid_majority_good_undeclared?(statusn,statuso,Active_Sources): bool = FORALL obs: good?(statuso(obs)) => hybrid_majority_good?(statusn,undeclared(Active_Sources(obs))) all_hybrid_majority_good_trusted?(statusn,statuso,Active_Sources): bool = FORALL obs: good?(statuso(obs)) => hybrid_majority_good?(statusn,trusted(Active_Sources(obs))) all_no_asymmetric_undeclared?(statusn,statuso,Active_Sources): bool = FORALL obs: good?(statuso(obs)) => no_asymmetric?(statusn,undeclared(Active_Sources(obs))) all_no_asymmetric_trusted?(statusn,statuso,Active_Sources): bool = FORALL obs: good?(statuso(obs)) => no_asymmetric?(statusn,trusted(Active_Sources(obs))) all_symmetric_agreement?(statusn,statuso,Active_Sources): bool = FORALL o1, o2: good?(statuso(o1)) & good?(statuso(o2)) => symmetric_agreement?(statusn,Active_Sources(o1),Active_Sources(o2)) all_good_trusting?(statusn,statuso,Active_Sources): bool = FORALL obs: good?(statuso(obs)) => good_trusting?(statusn,Active_Sources(obs)) all_declaration_agreement?(statuso,Active_Sources): bool = FORALL o1, o2: good?(statuso(o1)) & good?(statuso(o2)) => declaration_agreement?(Active_Sources(o1),Active_Sources(o2)) correct_active?(statusn,statuso,Active_Sources): bool = all_symmetric_agreement?(statusn,statuso,Active_Sources) & all_good_trusting?(statusn,statuso,Active_Sources) & all_declaration_agreement?(statuso,Active_Sources) all_benign_declaring?(statusn,statuso,Active_Sources): bool = FORALL obs: good?(statuso(obs)) => benign_declaring?(statusn,Active_Sources(obs)) all_symmetric_declaring?(statusn,statuso,act1,act2): bool = FORALL o1, o2: good?(statuso(o1)) & good?(statuso(o2)) => symmetric_declaring?(statusn,act1(o1),act2(o2)) all_agreement?(statuso,Active_Sources): bool = FORALL o1, o2: good?(statuso(o1)) & good?(statuso(o2)) => Active_Sources(o1) = Active_Sources(o2) all_subset?(act1,act2): bool = FORALL obs: subset?(trusted(act1(obs)),trusted(act2(obs))) all_no_asymmetric_trusted_subset : LEMMA all_subset?(act1,act2) & all_no_asymmetric_trusted?(statusn,statuso,act2) => all_no_asymmetric_trusted?(statusn,statuso,act1) all_hybrid_majority_good_trusted_subset : LEMMA all_subset?(act1,act2) & all_hybrid_majority_good_trusted?(statusn,statuso,act2) => all_hybrid_majority_good_trusted?(statusn,statuso,act1) good_trusting_lem: LEMMA correct_active?(statusn,statuso,Active_Sources) & good?(statuso(obs)) & good?(statusn(def)) => trusted?(Active_Sources(obs)(def)) symmetric_agreement_lem: LEMMA correct_active?(statusn,statuso,Active_Sources) & good?(statuso(o1)) & good?(statuso(o2)) & NOT asymmetric?(statusn(def)) => (trusted?(Active_Sources(o1)(def)) IFF trusted?(Active_Sources(o2)(def))) declaration_agreement_lem: LEMMA correct_active?(statusn,statuso,Active_Sources) & good?(statuso(o1)) & good?(statuso(o2)) => (declared?(Active_Sources(o1)(def)) IFF declared?(Active_Sources(o2)(def))) no_asymmetric_agreement: LEMMA all_no_asymmetric_trusted?(statusn,statuso,Active_Sources) & correct_active?(statusn,statuso,Active_Sources) => all_agreement?(statuso,Active_Sources) single_not_trusted: LEMMA (good?(statuso(obs)) => FORALL (def: below(N)): NOT (trusted(Active_Sources(obs))(def) & asymmetric?(statusn(def)))) IMPLIES (good?(statuso(obs)) => NOT (trusted(Active_Sources(obs))(G) & asymmetric?(statusn(G)))) END group_fault_model $$$group_fault_model.prf (group_fault_model (G_TCC1 0 (G_TCC1-1 nil 3299772904 3299772916 ("" (inst + "0") (("" (assert) nil nil)) nil) proved-complete ((below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" group_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 12049 450 t shostak)) (all_no_asymmetric_trusted_subset 0 (all_no_asymmetric_trusted_subset-1 nil 3299772891 nil ("" (skosimp*) (("" (expand "all_no_asymmetric_trusted?") (("" (expand "all_subset?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (assert) (("" (expand "no_asymmetric?") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (hide -4 -2) (("" (expand "subset?") (("" (inst - "p!1") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((all_subset? const-decl "bool" group_fault_model nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (O formal-const-decl "posnat" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (N formal-const-decl "posnat" group_fault_model nil) (no_asymmetric? const-decl "bool" global_fault_model nil) (all_no_asymmetric_trusted? const-decl "bool" group_fault_model nil)) nil nil nil nil)) (all_hybrid_majority_good_trusted_subset 0 (all_hybrid_majority_good_trusted_subset-1 nil 3299772891 nil ("" (skosimp*) (("" (expand "all_hybrid_majority_good_trusted?") (("" (expand "all_subset?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (assert) (("" (lemma "hybrid_majority_good_subset[N]") (("" (inst - "trusted(act1!1(obs!1))" "trusted(act2!1(obs!1))" "_") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((all_subset? const-decl "bool" group_fault_model nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (O formal-const-decl "posnat" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (trust type-decl nil hybrid_fault_types nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (Active_Sources_Type nonempty-type-eq-decl nil group_fault_model nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (N formal-const-decl "posnat" group_fault_model nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (all_hybrid_majority_good_trusted? const-decl "bool" group_fault_model nil)) nil nil nil nil)) (good_trusting_lem 0 (good_trusting_lem-1 nil 3299772891 nil ("" (skosimp*) (("" (expand "correct_active?") (("" (flatten) (("" (expand "all_good_trusting?") (("" (inst?) (("" (prop) (("" (expand "good_trusting?") (("" (inst?) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (O formal-const-decl "posnat" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (good_trusting? const-decl "bool" local_fault_model nil) (N formal-const-decl "posnat" group_fault_model nil) (all_good_trusting? const-decl "bool" group_fault_model nil) (correct_active? const-decl "bool" group_fault_model nil)) nil nil nil nil)) (symmetric_agreement_lem 0 (symmetric_agreement_lem-1 nil 3299772891 nil ("" (skosimp*) (("" (expand "correct_active?") (("" (flatten) (("" (expand "all_symmetric_agreement?") (("" (inst - "o1!1" "o2!1") (("" (replace*) (("" (expand "symmetric_agreement?") (("" (inst?) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (O formal-const-decl "posnat" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (symmetric_agreement? const-decl "bool" local_fault_model nil) (N formal-const-decl "posnat" group_fault_model nil) (all_symmetric_agreement? const-decl "bool" group_fault_model nil) (correct_active? const-decl "bool" group_fault_model nil)) nil nil nil nil)) (declaration_agreement_lem 0 (declaration_agreement_lem-1 nil 3299772891 nil ("" (skosimp*) (("" (expand "correct_active?") (("" (flatten) (("" (expand "all_declaration_agreement?") (("" (inst - "o1!1" "o2!1") (("" (replace*) (("" (expand "declaration_agreement?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (O formal-const-decl "posnat" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (declaration_agreement? const-decl "bool" local_fault_model nil) (N formal-const-decl "posnat" group_fault_model nil) (all_declaration_agreement? const-decl "bool" group_fault_model nil) (correct_active? const-decl "bool" group_fault_model nil)) nil nil nil nil)) (no_asymmetric_agreement 0 (no_asymmetric_agreement-1 nil 3299772891 nil ("" (expand "all_agreement?") (("" (expand "correct_active?") (("" (skosimp*) (("" (hide -3) (("" (expand "all_no_asymmetric_trusted?") (("" (inst-cp - "o1!1") (("" (inst - "o2!1") (("" (assert) (("" (expand "all_symmetric_agreement?") (("" (expand "all_declaration_agreement?") (("" (inst - "o1!1" "o2!1") (("" (inst - "o1!1" "o2!1") (("" (assert) (("" (apply-extensionality + :hide? t) (("" (lemma "no_asymmetric_agreement_lem") (("" (inst?) (("" (inst?) (("" (assert) (("" (hide 2 -6 -5 -4 -3) (("" (expand "no_asymmetric?") (("" (inst?) (("" (inst?) (("" (expand "trusted") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((all_agreement? const-decl "bool" group_fault_model nil) (all_no_asymmetric_trusted? const-decl "bool" group_fault_model nil) (all_symmetric_agreement? const-decl "bool" group_fault_model nil) (no_asymmetric_agreement_lem formula-decl nil local_fault_model nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (no_asymmetric? const-decl "bool" global_fault_model nil) (Active_Sources_Type nonempty-type-eq-decl nil group_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (N formal-const-decl "posnat" group_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (all_declaration_agreement? const-decl "bool" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (O formal-const-decl "posnat" group_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (correct_active? const-decl "bool" group_fault_model nil)) nil nil nil nil)) (single_not_trusted 0 (single_not_trusted-1 nil 3299772929 3299773419 ("" (skosimp*) (("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) proved ((G const-decl "below(N)" group_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" group_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 13211 900 t shostak))) $$$local_state.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : local_state.pvs % % Purpose : collects all data that are stored at the SPIDER nodes. % % Design : SPIDER Version 0 % % Dependencies : diagnosis_half % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Alfons Geser % ICASE % 3 West Reid Street / MS 132 C % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-8003 % fax: 757-864-6134 % mailto: geser@icase.edu % http://www.icase.edu/~geser/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % February 12, 2001 - Created from Spider_New_Diagnosis.pvs % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% local_state [ L : posnat % number of LEFTs , R : posnat % number of RIGHTs ] : THEORY BEGIN IMPORTING group_fault_model Local_State_Type : TYPE = [# BB: Active_Sources_Type[L, L], BR: Active_Sources_Type[L, R], RB: Active_Sources_Type[R, L], RR: Active_Sources_Type[R, R] #] ls, new_ls : var Local_State_Type left : var node_status[L] right : var node_status[R] act_lr, new_act_lr : var Active_Sources_Type[L, R] act_rl, new_act_rl : var Active_Sources_Type[R, L] act_ll, new_act_ll : var Active_Sources_Type[L, L] act_rr, new_act_rr : var Active_Sources_Type[R, R] all_correct_accs?(left,right,ls) : bool = correct_active?(left,left,ls`BB) & correct_active?(left,right,ls`BR) & correct_active?(right,left,ls`RB) & correct_active?(right,right,ls`RR) DMFA(left,right,ls): bool = all_hybrid_majority_good_trusted?(left,right,ls`BR) & all_hybrid_majority_good_trusted?(right,left,ls`RB) & (all_no_asymmetric_trusted?(left,right,ls`BR) OR all_no_asymmetric_trusted?(right,left,ls`RB)) IC_DMFA(left,right,ls): bool = % all_hybrid_majority_good_trusted?(left,right,ls`BR) & all_hybrid_majority_good_trusted?(right,left,ls`RB) & (all_no_asymmetric_trusted?(left,right,ls`BR) OR all_no_asymmetric_trusted?(right,left,ls`RB)) END local_state $$$selective_vector_majority.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : selective_vector_majority.pvs % % Purpose : Abstract type declaration for a function that determines a % majority value from a selected subset of values, if % such a majority exists. % % Provides some support lemmas. % % Assumptions : none % % Guarantees : such a function exists % % Design : SPIDER Version 0 % % Dependencies : finite_sets@finite_sets_below % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Paul S. Miner % 1 South Wright St. / MS 130 % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-6201 % fax: 757-864-4234 % mailto:p.s.miner@larc.nasa.gov % http://shemesh.larc.nasa.gov/~psm/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notes % 1. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % July 26, 2000 - Added this header % August 1, 2000 - Added alternate form of uniqueness, % additional comments % November 28, 2000 - Modified definition of majority? to a % simpler, but mathematically equivalent % expression. Added declaration of set % votes_for. These changes helped clean up % (and simplify) proofs throughout these % theories. % March 6, 2002 - Introduced predicate similar_vector and % function majority_voter and its properties. % (Geser) % March 7, 2002 - Introduced function majority as the unique % selective majority function that yields a % specified default value if there is no % majority. This effectively eliminates the % need for selective majority function % parameters everywhere. (Geser) % August 28, 2002 - Added opposition_witness and majority_char_alt. % (Geser) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% selective_vector_majority [N: posnat, V:TYPE+]: THEORY BEGIN value_vector: TYPE = [below(N) -> V] vvec, vvec1, vvec2: var value_vector select, select1, select2: var set[below(N)] i: var below(N) v, v1, v2: var V IMPORTING finite_sets@finite_sets_below[N] votes_for(select, vvec, v): finite_set[below(N)] = {i : below(N) | select(i) & vvec(i) = v} majority?(select)(v, vvec): bool = 2*card(votes_for(select, vvec, v)) > card(select) opposition_witness: LEMMA NOT majority?(select)(v, vvec) & nonempty?(select) => EXISTS i: select(i) & NOT vvec(i) = v majority_exists?(select)(vvec):bool = Exists v: majority?(select)(v, vvec) selective_majority_unique: LEMMA majority?(select)(v1,vvec) & majority?(select)(v2,vvec) => v1 = v2 selective_majority_subset: LEMMA subset?(select2,select1) & subset?(votes_for(select1,vvec1,v),votes_for(select2,vvec2,v)) & majority?(select1)(v,vvec1) => majority?(select2)(v,vvec2) default : var V majority_welldefinedness: LEMMA majority_exists?(select)(vvec) => singleton?({v: V | majority?(select)(v, vvec)}) majority(select,default)(vvec): V = IF majority_exists?(select)(vvec) THEN the({v:V | majority?(select)(v, vvec)}) ELSE default ENDIF the_unique: LEMMA majority?(select)(v, vvec) => the({v:V | majority?(select)(v, vvec)}) = v selective_majority_unique_alt: LEMMA majority?(select)(v, vvec) => majority(select,default)(vvec) = v majority_char: LEMMA majority_exists?(select)(vvec) => (majority(select,default)(vvec) = v IFF majority?(select)(v, vvec)) majority_char_alt: LEMMA default /= v => (majority(select,default)(vvec) = v IFF majority?(select)(v, vvec)) similar_vector?(select,vvec1,vvec2) : bool = FORALL i: select(i) => vvec1(i) = vvec2(i) similar_vector_subset: LEMMA subset?(select1,select2) & similar_vector?(select2,vvec1,vvec2) => similar_vector?(select1,vvec1,vvec2) similar_selective_majority: LEMMA majority?(select)(v,vvec1) & similar_vector?(select, vvec1, vvec2) => majority?(select)(v,vvec2) similar_selective_majority_unique: LEMMA majority?(select)(v1,vvec1) & majority?(select)(v2,vvec2) & similar_vector?(select, vvec1, vvec2) => v1 = v2 similar_selective_majority_exists: LEMMA similar_vector?(select, vvec1, vvec2) => (majority_exists?(select)(vvec1) IFF majority_exists?(select)(vvec2)) majority_unique: LEMMA similar_vector?(select, vvec1, vvec2) => majority(select,default)(vvec1) = majority(select,default)(vvec2) END selective_vector_majority $$$selective_vector_majority.prf (selective_vector_majority (votes_for_TCC1 0 (votes_for_TCC1-1 nil 3263288842 3263288974 ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved ((finite_below formula-decl nil finite_sets_below "finite_sets/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (= const-decl "[T, T -> boolean]" equalities nil) (value_vector type-eq-decl nil selective_vector_majority nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil)) 74 50 nil nil)) (majority?_TCC1 0 (majority?_TCC1-1 nil 3263288842 3263288974 ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved ((finite_below formula-decl nil finite_sets_below "finite_sets/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil)) 43 40 nil nil)) (opposition_witness 0 (opposition_witness-1 nil 3263288842 3263288975 ("" (skosimp*) (("" (expand "majority?") (("" (case "nonempty?(difference(select!1,votes_for(select!1, vvec!1, v!1)))") (("1" (expand "nonempty?" -1) (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "difference") (("1" (expand "member") (("1" (flatten) (("1" (expand "votes_for") (("1" (prop) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "nonempty_card") (("1" (rewrite "nonempty_card") (("1" (rewrite "card_diff_subset") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "votes_for") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "finite_below") nil nil)) nil) ("2" (rewrite "finite_below") nil nil)) nil) ("2" (rewrite "finite_below") nil nil)) nil)) nil)) nil)) nil) proved ((majority? const-decl "bool" selective_vector_majority nil) (nonempty_card formula-decl nil finite_sets nil) (card_diff_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (finite_below formula-decl nil finite_sets_below "finite_sets/") (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (difference const-decl "set" sets nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (votes_for const-decl "finite_set[below(N)]" selective_vector_majority nil)) 963 840 nil nil)) (selective_majority_unique 0 (selective_majority_unique-1 nil 3263288842 3263288978 ("" (skosimp*) (("" (expand "majority?") (("" (lemma "pidgeon_hole") (("" (inst - "votes_for(select!1, vvec!1, v1!1)" "union(votes_for(select!1, vvec!1, v2!1), complement(select!1))" "1") (("" (rewrite "card_disj_union") (("1" (assert) (("1" (prop) (("1" (forward-chain "card_1_has_1") (("1" (skosimp*) (("1" (hide -2) (("1" (expand "intersection") (("1" (expand "union") (("1" (expand "complement") (("1" (expand "member") (("1" (expand "votes_for") (("1" (assert) (("1" (prop) (("1" (replace*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "finite_below[N]") nil nil)) nil) ("2" (case-replace "card(complement(select!1)) = N - card(select!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "card_disj_union[below(N)]") (("2" (inst - "complement(select!1)" "select!1") (("1" (prop) (("1" (case-replace "union(complement(select!1), select!1) = fullset[below(N)]") (("1" (use "card_below_fullset") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (rewrite "finite_below") nil nil) ("3" (rewrite "finite_below") nil nil)) nil)) nil)) nil) ("3" (rewrite "finite_below") nil nil) ("4" (rewrite "finite_below") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "intersection") (("2" (expand "complement") (("2" (expand "member") (("2" (expand "votes_for") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "finite_below") nil nil)) nil)) nil)) nil)) nil)) nil) proved ((majority? const-decl "bool" selective_vector_majority nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (votes_for const-decl "finite_set[below(N)]" selective_vector_majority nil) (union const-decl "set" sets nil) (complement const-decl "set" sets nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_below formula-decl nil finite_sets_below "finite_sets/") (card_below_fullset formula-decl nil finite_sets_below "finite_sets/") (fullset const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (select!1 skolem-const-decl "set[below(N)]" selective_vector_majority nil) (intersection const-decl "set" sets nil) (card_1_has_1 formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (card_disj_union formula-decl nil finite_sets nil) (pidgeon_hole formula-decl nil finite_sets_below "finite_sets/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil)) 3216 2830 nil nil)) (selective_majority_subset 0 (selective_majority_subset-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (expand "majority?") (("" (forward-chain "card_subset[below[N]]") (("1" (hide -2) (("1" (forward-chain "card_subset[below[N]]") (("1" (hide -3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "finite_below[N]") nil nil) ("3" (rewrite "finite_below[N]") nil nil)) nil)) nil)) nil) proved ((majority? const-decl "bool" selective_vector_majority nil) (finite_below formula-decl nil finite_sets_below "finite_sets/") (votes_for const-decl "finite_set[below(N)]" selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (below type-eq-decl nil naturalnumbers nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (card_subset formula-decl nil finite_sets nil)) 730 590 nil nil)) (majority_welldefinedness 0 (majority_welldefinedness-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (expand "majority_exists?") (("" (skosimp*) (("" (expand "singleton?") (("" (inst?) (("" (skosimp*) (("" (typepred "y!1") (("" (lemma "selective_majority_unique") (("" (inst?) (("" (inst - "v!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((majority_exists? const-decl "bool" selective_vector_majority nil) (singleton? const-decl "bool" sets nil) (selective_majority_unique formula-decl nil selective_vector_majority nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (majority? const-decl "bool" selective_vector_majority nil) (select!1 skolem-const-decl "set[below(N)]" selective_vector_majority nil) (v!1 skolem-const-decl "V" selective_vector_majority nil) (vvec!1 skolem-const-decl "value_vector" selective_vector_majority nil)) 161 120 nil nil)) (majority_TCC1 0 (majority_TCC1-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (rewrite "majority_welldefinedness") nil nil)) nil) proved ((majority_welldefinedness formula-decl nil selective_vector_majority nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil)) 47 50 nil nil)) (the_unique_TCC1 0 (the_unique_TCC1-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (lemma "majority_welldefinedness") (("" (inst?) (("" (assert) (("" (expand "majority_exists?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((majority_welldefinedness formula-decl nil selective_vector_majority nil) (majority_exists? const-decl "bool" selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 99 70 nil nil)) (the_unique 0 (the_unique-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (expand "the") (("" (lemma "epsilon_ax[V]") (("" (inst?) (("" (split -1) (("1" (lemma "selective_majority_unique") (("1" (inst?) (("1" (inst - "v!1") (("1" (prop) nil nil)) nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((the const-decl "(p)" sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (value_vector type-eq-decl nil selective_vector_majority nil) (majority? const-decl "bool" selective_vector_majority nil) (selective_majority_unique formula-decl nil selective_vector_majority nil) (epsilon const-decl "T" epsilons nil) (epsilon_ax formula-decl nil epsilons nil) (V formal-nonempty-type-decl nil selective_vector_majority nil)) 120 90 nil nil)) (selective_majority_unique_alt 0 (selective_majority_unique_alt-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (expand "majority") (("" (lift-if) (("" (prop) (("1" (rewrite "the_unique") nil nil) ("2" (expand "majority_exists?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((majority const-decl "V" selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (the_unique formula-decl nil selective_vector_majority nil) (majority_exists? const-decl "bool" selective_vector_majority nil)) 109 90 nil nil)) (majority_char 0 (majority_char-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (expand "majority") (("" (lift-if) (("" (replace*) (("" (prop) (("1" (lemma "epsilon_ax[V]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "epsilon_ax[V]") (("2" (inst?) (("2" (split -) (("1" (lemma "selective_majority_unique") (("1" (inst?) (("1" (inst - "v!1") (("1" (prop) (("1" (expand "the") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((majority const-decl "V" selective_vector_majority nil) (epsilon const-decl "T" epsilons nil) (the const-decl "(p)" sets nil) (selective_majority_unique formula-decl nil selective_vector_majority nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (epsilon_ax formula-decl nil epsilons nil) (majority? const-decl "bool" selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) 167 140 nil nil)) (majority_char_alt 0 (majority_char_alt-1 nil 3263288842 3263288979 ("" (skosimp*) (("" (case "majority_exists?(select!1)(vvec!1)") (("1" (rewrite "majority_char") nil nil) ("2" (expand "majority") (("2" (lift-if) (("2" (assert) (("2" (expand "majority_exists?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((majority_exists? const-decl "bool" selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (majority_char formula-decl nil selective_vector_majority nil) (majority const-decl "V" selective_vector_majority nil)) 118 100 nil nil)) (similar_vector_subset 0 (similar_vector_subset-1 nil 3263288842 3263288980 ("" (expand "similar_vector?") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (expand "subset?") (("" (inst?) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (similar_vector? const-decl "bool" selective_vector_majority nil)) 133 100 nil nil)) (similar_selective_majority 0 (similar_selective_majority-1 nil 3263288842 3263288980 ("" (skosimp*) (("" (expand "majority?") (("" (case "votes_for(select!1, vvec1!1, v!1) = votes_for(select!1, vvec2!1, v!1)") (("1" (replace*) nil nil) ("2" (hide 2 -1) (("2" (expand "similar_vector?") (("2" (apply-extensionality + :hide? t) (("2" (inst?) (("2" (expand "votes_for") (("2" (case "select!1(x!1)") (("1" (assert) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((majority? const-decl "bool" selective_vector_majority nil) (similar_vector? const-decl "bool" selective_vector_majority nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (votes_for const-decl "finite_set[below(N)]" selective_vector_majority nil)) 242 190 nil nil)) (similar_selective_majority_unique 0 (similar_selective_majority_unique-1 nil 3263288842 3263288980 ("" (skosimp*) (("" (lemma "selective_majority_unique") (("" (inst - "_" "v1!1" "v2!1" "vvec2!1") (("" (inst?) (("" (prop) (("" (lemma "similar_selective_majority") (("" (inst?) (("" (inst - "vvec1!1") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((selective_majority_unique formula-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (similar_selective_majority formula-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (V formal-nonempty-type-decl nil selective_vector_majority nil)) 123 100 nil nil)) (similar_selective_majority_exists 0 (similar_selective_majority_exists-1 nil 3263288842 3263288980 ("" (skosimp*) (("" (prop) (("1" (expand "majority_exists?") (("1" (skosimp*) (("1" (inst?) (("1" (lemma "similar_selective_majority") (("1" (inst - "_" "_" "vvec1!1" "vvec2!1") (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "majority_exists?") (("2" (skosimp*) (("2" (inst?) (("2" (lemma "similar_selective_majority") (("2" (inst - "_" "_" "vvec2!1" "vvec1!1") (("2" (inst?) (("2" (prop) (("2" (hide-all-but (1 -2)) (("2" (expand "similar_vector?") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((similar_selective_majority formula-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (value_vector type-eq-decl nil selective_vector_majority nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (majority_exists? const-decl "bool" selective_vector_majority nil) (similar_vector? const-decl "bool" selective_vector_majority nil)) 216 150 nil nil)) (majority_unique 0 (majority_unique-1 nil 3263288842 3263302629 ("" (skosimp*) (("" (use "similar_selective_majority_exists") (("" (prop) (("1" (name-replace "VAL2" "majority(select!1, default!1)(vvec2!1)" :hide? nil) (("1" (name-replace "VAL1" "majority(select!1, default!1)(vvec1!1)" :hide? nil) (("1" (rewrite "majority_char") (("1" (rewrite "majority_char") (("1" (lemma "similar_selective_majority_unique") (("1" (inst - "_" "VAL1" "VAL2" "vvec1!1" "vvec2!1") (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "majority") (("2" (replace*) nil nil)) nil)) nil)) nil)) nil) proved ((similar_selective_majority_exists formula-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (V formal-nonempty-type-decl nil selective_vector_majority nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" selective_vector_majority nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (majority const-decl "V" selective_vector_majority nil) (majority_char formula-decl nil selective_vector_majority nil) (similar_selective_majority_unique formula-decl nil selective_vector_majority nil)) 47267 5870 t nil))) $$$good_selective_majority.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : good_selective_majority.pvs % % Purpose : States properties of selective majority functions % for the case where the good nodes are in the majority % % Design : SPIDER Version 0 % % Dependencies : This theory depends upon the following PVS theories % (and any of their dependencies): % % global_fault_model, selective_vector_majority % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Alfons Geser % ICASE % 3 West Reid Street / MS 132 C % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-8003 % fax: 757-864-6134 % mailto: geser@icase.edu % http://www.icase.edu/~geser/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % November 7, 2001 - Added this header. % March 7, 2002 - Introduced function majority. % March 11, 2002 - Cleaned up proofs. % April 11, 2002 - Added good_vote_for? as an alternative to % predicate good_vote_same?. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% good_selective_majority[N:posnat, V:TYPE+]: THEORY BEGIN IMPORTING global_fault_model[N] , selective_vector_majority[N,V] status: var node_status vvec: var value_vector[N,V] p, q: var below[N] hs : var set[below[N]] good_vote_same?(status,vvec) : bool = (FORALL p,q: good?(status(p)) AND good?(status(q)) => vvec(p) = vvec(q)) same_good_vote_for: LEMMA good_vote_same?(status,vvec) & subset?(trustworthy(status), hs) & good?(status(q)) => subset?(good_votes(status, hs), votes_for(hs, vvec, vvec(q))) same_good_are_majority: LEMMA hybrid_majority_good?(status,hs) & good_vote_same?(status,vvec) & hybrid_select?(status,hs) & good?(status(q)) => majority?(hs)(vvec(q),vvec) default : var V majority_same_good: LEMMA hybrid_majority_good?(status,hs) & good_vote_same?(status,vvec) & hybrid_select?(status,hs) & good?(status(q)) => majority(hs,default)(vvec) = vvec(q) v, v1, v2 : var V good_vote_for?(status,vvec,v) : bool = (FORALL p: good?(status(p)) => vvec(p) = v) good_votes: LEMMA good_vote_for?(status,vvec,v) & subset?(trustworthy(status), hs) => subset?(good_votes(status,hs), votes_for(hs, vvec, v)) good_vote_for_majority_lem: LEMMA hybrid_majority_good?(status,hs) & hybrid_select?(status,hs) & good_vote_for?(status,vvec,v) => majority?(hs)(v,vvec) good_vote_for_majority: THEOREM hybrid_majority_good?(status,hs) & hybrid_select?(status,hs) & good_vote_for?(status,vvec,v) => majority(hs,default)(vvec) = v good_vote_for_same: LEMMA good_vote_same?(status,vvec) IFF EXISTS v: good_vote_for?(status,vvec,v) good_vote_for_instance: LEMMA good?(status(p)) => (good_vote_same?(status,vvec) IFF good_vote_for?(status,vvec,vvec(p))) good_vote_for_uniqueness: THEOREM good_vote_for?(status,vvec,v1) & good_vote_for?(status,vvec,v2) => v1 = v2 END good_selective_majority $$$good_selective_majority.prf (|good_selective_majority| (|same_good_vote_for_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below[N]") NIL NIL)) NIL) (|same_good_vote_for| "" (SKOSIMP*) (("" (EXPAND "subset?") (("" (SKOSIMP*) (("" (EXPAND "good_votes") (("" (EXPAND "union") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (EXPAND "votes_for") (("" (INST?) (("" (EXPAND "trustworthy") (("" (EXPAND "recovering") (("" (EXPAND "good_vote_same?") (("" (INST?) (("" (EXPAND "good?") (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|same_good_are_majority_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL NIL)) NIL) (|same_good_are_majority| "" (SKOSIMP) (("" (EXPAND "hybrid_select?") (("" (FLATTEN) (("" (EXPAND "majority?") (("" (LEMMA "hybrid_majority[N]") (("" (INST?) (("1" (PROP) (("1" (CASE "card(good_votes(status!1,hs!1)) <= card(votes_for(hs!1, vvec!1, vvec!1(q!1)))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 -5 -1) (("2" (REWRITE "card_subset[below(N)]") (("2" (REWRITE "same_good_vote_for") NIL NIL)) NIL)) NIL) ("3" (REWRITE "finite_below") NIL NIL)) NIL)) NIL) ("2" (REWRITE "finite_below") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|majority_same_good| "" (SKOSIMP*) (("" (USE "same_good_are_majority") (("" (PROP) (("" (CASE "majority_exists?(hs!1)(vvec!1)") (("1" (REWRITE "majority_char") NIL NIL) ("2" (EXPAND "majority_exists?") (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_votes| "" (SKOSIMP*) (("" (EXPAND "subset?") (("" (SKOSIMP*) (("" (EXPAND "votes_for") (("" (EXPAND "good_votes") (("" (EXPAND "union") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (EXPAND "trustworthy") (("" (INST?) (("" (EXPAND "good_vote_for?") (("" (INST?) (("" (EXPAND "recovering") (("" (EXPAND "good?") (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_vote_for_majority_lem| "" (SKOSIMP*) (("" (EXPAND "hybrid_select?") (("" (EXPAND "majority?") (("" (LEMMA "hybrid_majority[N]") (("" (INST?) (("1" (PROP) (("1" (CASE "card(good_votes(status!1,hs!1)) <= card(votes_for(hs!1, vvec!1, v!1))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 -4 -1) (("2" (REWRITE "card_subset[below(N)]") (("2" (REWRITE "good_votes") NIL NIL)) NIL)) NIL) ("3" (REWRITE "finite_below") NIL NIL)) NIL)) NIL) ("2" (REWRITE "finite_below") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_vote_for_majority| "" (SKOSIMP*) (("" (USE "good_vote_for_majority_lem") (("" (PROP) (("" (USE "majority_char") (("" (PROP) (("" (EXPAND "majority_exists?") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_vote_for_same| "" (SKOSIMP*) (("" (PROP) (("1" (USE "hybrid_majority_exists_good[N]") (("1" (SKOSIMP*) (("1" (INST + "vvec!1(p!1)") (("1" (EXPAND "good_vote_for?") (("1" (SKOSIMP*) (("1" (EXPAND "good_vote_same?") (("1" (INST - "p!2" "p!1") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "good_vote_same?") (("2" (SKOSIMP*) (("2" (EXPAND "good_vote_for?") (("2" (INST-CP - "p!1") (("2" (INST - "q!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_vote_for_instance| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "good_vote_for?") (("1" (SKOSIMP*) (("1" (EXPAND "good_vote_same?") (("1" (INST - "p!2" "p!1") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "good_vote_same?") (("2" (SKOSIMP*) (("2" (EXPAND "good_vote_for?") (("2" (INST-CP - "p!2") (("2" (INST - "q!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_vote_for_uniqueness| "" (SKOSIMP*) (("" (USE "hybrid_majority_exists_good[N]") (("" (SKOSIMP*) (("" (EXPAND "good_vote_for?") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$local_fault_model.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : local_fault_model.pvs % % Purpose : Provides a local fault classification as seen by some % observer of a set of nodes. This observer does not % know the global fault classification, but has the % capability of locally detecting some misbehavior. % This file introduces the various forms of diagnostic % state maintained by each node, as well as a means of % deriving a correct selection set for the hybrid % votes. % % Assumptions : An observer has some means to locally detect % misbehavior. % % Guarantees : Definitions of type Active_Sources_Type which models % the characteristics of the evolving diagnostic data % in the current frame. % % Defintion of type Conviction_Set_Type which % identifies those nodes that were convicted % previously, and are currently prevented from % participating in a vote. % % Design : SPIDER Version 0 % % Dependencies : global_fault_model, finite_sets@finite_sets_below % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Paul S. Miner % 1 South Wright St. / MS 130 % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-6201 % fax: 757-864-4234 % mailto:p.s.miner@larc.nasa.gov % http://shemesh.larc.nasa.gov/~psm/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notes % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % March 1, 2001 - Created this file to replace % manifest_fault_model % March 29, 2001 - Introduced node_status parameter to % Active_Sources_Type. This allows to remove % the node_status parameter from f. (Geser) % - Introduced premises good(o1), good(o2) so as % to handle bad observer behaviour. (Geser) % October 26, 2001 - Introduced trusted, accused, declared values. % November 7, 2001 - Added conversions to/from accusation matrices. % This material is collected from theories court % and declx. (Geser) % February 22, 2002 - Moved dependency on observer to new theory % group_fault_model. The local fault model here % is as seen by one good observer. Agreement % properties are stated for pairs of good % observers. (Geser) % March 6, 2002 - Introduced function undeclared. (Geser) % March 11, 2002 - Eliminated update_accusations and % update_declarations. Their effect is now % achieved by merge_active together with % extract_accvec and extract_decvec, resp. (Geser) % March 28, 2002 - Introduced lemmas for form/extract_accvec/decvec % and replaced some implications by IFFs. (Geser) % April 11, 2002 - Added predicate symmetric_declaring?. (Geser) % - Changed definition of symmetric_agreement? (Geser) % - Added lemma difference_hybrid_select. (Geser) % April 18, 2002 - Changed definition of symmetric_declaring? and % form_accvec? to demonstrate coding independence. % Pushed through changes. (Geser) % November 13, 2002 - Replaced symmetric_agreement_lem by the stronger % no_asymmetric_agreement_lem. (Geser) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% local_fault_model[N:posnat]: THEORY BEGIN IMPORTING global_fault_model , finite_sets@finite_sets_below[N] p: var below(N) statusn: var node_status[N] Active_Vector_Type: NONEMPTY_TYPE = [below(N)->trust] act_vec, act_vec1, act_vec2, act_vec3, act_vec4: var Active_Vector_Type tr : var [below[N]->trust] trusted(tr) : finite_set[below(N)] = {p | trusted?(tr(p))} accused(tr) : finite_set[below(N)] = {p | accused?(tr(p))} declared(tr) : finite_set[below(N)] = {p | declared?(tr(p))} undeclared(tr) : finite_set[below(N)] = complement(declared(tr)) trusted_subset_undeclared : LEMMA subset?(trusted(tr), undeclared(tr)) good_trusting?(statusn,act_vec): bool = FORALL p: good?(statusn(p)) => trusted?(act_vec(p)) symmetric_agreement?(statusn,act_vec1,act_vec2): bool = FORALL p: NOT asymmetric?(statusn(p)) => (trusted?(act_vec1(p)) IFF trusted?(act_vec2(p))) declaration_agreement?(act_vec1,act_vec2): bool = FORALL p: declared?(act_vec1(p)) IFF declared?(act_vec2(p)) declaration_agreement_undeclared: LEMMA (undeclared(act_vec1) = undeclared(act_vec2)) IFF declaration_agreement?(act_vec1,act_vec2) no_asymmetric_agreement_lem: LEMMA declaration_agreement?(act_vec1,act_vec2) & symmetric_agreement?(statusn,act_vec1,act_vec2) & NOT (asymmetric?(statusn(p)) & trusted?(act_vec1(p))) & NOT (asymmetric?(statusn(p)) & trusted?(act_vec2(p))) => act_vec1(p) = act_vec2(p) all_trusted(p): trust = trusted all_trusted_good_trusting: LEMMA good_trusting?(statusn,all_trusted) symmetric_declaring?(statusn,act_vec1,act_vec2): bool = FORALL p: accused?(act_vec1(p)) & symmetric?(statusn(p)) => declared?(act_vec2(p)) Conviction_Set_Type: NONEMPTY_TYPE = set[below(N)] blackb,blackb1,blackb2: var Conviction_Set_Type convicted_agreement?(blackb1,blackb2) : bool = (blackb1 = blackb2) convicted_validity?(statusn,blackb) : bool = FORALL p: blackb(p) => NOT trustworthy?(statusn(p)) initial_convicted_validity : LEMMA convicted_validity?(statusn,emptyset) benign_not_trusting?(statusn,act_vec): bool = FORALL p: benign?(statusn(p)) => NOT trusted?(act_vec(p)) trusted_hybrid_select: LEMMA good_trusting?(statusn,act_vec) & benign_not_trusting?(statusn,act_vec) => hybrid_select?(statusn,trusted(act_vec)) benign_declaring?(statusn,act_vec): bool = FORALL p: benign?(statusn(p)) => declared?(act_vec(p)) undeclared_hybrid_select : LEMMA good_trusting?(statusn,act_vec) & benign_declaring?(statusn,act_vec) => hybrid_select?(statusn,undeclared(act_vec)) difference_hybrid_select: LEMMA good_trusting?(statusn,act_vec) => hybrid_select?(statusn, difference(undeclared(act_vec), benign(statusn))) Diagnostic_State_Type : NONEMPTY_TYPE = [# active : Active_Vector_Type, convicted : Conviction_Set_Type #] Syndrome : var Diagnostic_State_Type Hybrid_Select(Syndrome): set[below(N)] = intersection(trusted(Syndrome`active), complement(Syndrome`convicted)) hybrid_select_Hybrid_Select: LEMMA convicted_validity?(statusn,Syndrome`convicted) & good_trusting?(statusn,Syndrome`active) & benign_not_trusting?(statusn,Syndrome`active) => hybrid_select?(statusn,Hybrid_Select(Syndrome)) acc_vec, acc1_vec, acc2_vec : var accusation_vector_type[N] any_accusation(act_vec, p) : accusation form_accvec(act_vec): accusation_vector_type[N] = LAMBDA p: IF trusted?(act_vec(p)) THEN working ELSIF accused?(act_vec(p)) THEN failed ELSE any_accusation(act_vec, p) ENDIF form_decvec(act_vec): accusation_vector_type[N] = LAMBDA p: IF declared?(act_vec(p)) THEN failed ELSE working ENDIF form_accvec_working: LEMMA working?(form_accvec(act_vec)(p)) IFF trusted?(act_vec(p)) OR declared?(act_vec(p)) & working?(any_accusation(act_vec, p)) form_decvec_working: LEMMA working?(form_decvec(act_vec)(p)) IFF NOT declared?(act_vec(p)) form_accvec_correct: LEMMA good_trusting?(statusn,act_vec) => correct_accusation_vector?(statusn,form_accvec(act_vec)) form_decvec_correct: LEMMA good_trusting?(statusn,act_vec) => correct_accusation_vector?(statusn,form_decvec(act_vec)) form_decvec_agreement: LEMMA form_decvec(act_vec1) = form_decvec(act_vec2) IFF declaration_agreement?(act_vec1,act_vec2) form_decvec_benign_not_working: LEMMA benign_not_working?(statusn, form_decvec(act_vec)) IFF benign_declaring?(statusn, act_vec) extract_accvec(acc_vec) : Active_Vector_Type = LAMBDA p: IF working?(acc_vec(p)) THEN trusted ELSE accused ENDIF extract_decvec(acc_vec) : Active_Vector_Type = LAMBDA p: IF working?(acc_vec(p)) THEN trusted ELSE declared ENDIF extract_accvec_trusted: LEMMA trusted?(extract_accvec(acc_vec)(p)) IFF working?(acc_vec(p)) extract_accvec_declared: LEMMA NOT declared?(extract_accvec(acc_vec)(p)) extract_decvec_trusted: LEMMA trusted?(extract_decvec(acc_vec)(p)) IFF working?(acc_vec(p)) extract_decvec_declared: LEMMA declared?(extract_decvec(acc_vec)(p)) IFF NOT working?(acc_vec(p)) extract_declared: LEMMA declaration_agreement?(extract_decvec(form_decvec(act_vec)), act_vec) extract_accvec_good_trusting: LEMMA good_trusting?(statusn,extract_accvec(acc_vec)) IFF correct_accusation_vector?(statusn, acc_vec) extract_decvec_good_trusting: LEMMA good_trusting?(statusn,extract_decvec(acc_vec)) IFF correct_accusation_vector?(statusn, acc_vec) extract_decvec_benign_declaring: LEMMA benign_declaring?(statusn,extract_decvec(acc_vec)) IFF benign_not_working?(statusn,acc_vec) merge_active(act_vec1,act_vec2) : Active_Vector_Type = LAMBDA p: merge_trusts(act_vec1(p),act_vec2(p)) merge_active_trusted : LEMMA trusted(merge_active(act_vec1,act_vec2)) = intersection(trusted(act_vec1),trusted(act_vec2)) merge_active_declared : LEMMA declared(merge_active(act_vec1,act_vec2)) = union(declared(act_vec1),declared(act_vec2)) merge_active_symmetric_agreement : LEMMA symmetric_agreement?(statusn,act_vec1,act_vec2) & symmetric_agreement?(statusn,act_vec3,act_vec4) => symmetric_agreement?(statusn,merge_active(act_vec1,act_vec3), merge_active(act_vec2,act_vec4)) merge_active_benign_not_trusting1 : LEMMA benign_not_trusting?(statusn,act_vec1) => benign_not_trusting?(statusn,merge_active(act_vec1,act_vec2)) merge_active_benign_not_trusting2 : LEMMA benign_not_trusting?(statusn,act_vec2) => benign_not_trusting?(statusn,merge_active(act_vec1,act_vec2)) merge_active_good_trusting : LEMMA good_trusting?(statusn,merge_active(act_vec1,act_vec2)) IFF (good_trusting?(statusn,act_vec1) & good_trusting?(statusn,act_vec2)) merge_active_declaration_agreement : LEMMA declaration_agreement?(act_vec1,act_vec2) & declaration_agreement?(act_vec3,act_vec4) => declaration_agreement?(merge_active(act_vec1,act_vec3), merge_active(act_vec2,act_vec4)) merge_active_across_declaration_agreement : LEMMA declaration_agreement?(act_vec1,act_vec4) & declaration_agreement?(act_vec3,act_vec2) => declaration_agreement?(merge_active(act_vec1,act_vec3), merge_active(act_vec2,act_vec4)) merge_active_benign_declaring1 :LEMMA benign_declaring?(statusn,act_vec1) => benign_declaring?(statusn,merge_active(act_vec1,act_vec2)) merge_active_benign_declaring2 :LEMMA benign_declaring?(statusn,act_vec2) => benign_declaring?(statusn,merge_active(act_vec1,act_vec2)) END local_fault_model $$$local_fault_model.prf (|local_fault_model| (|trusted_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL NIL)) NIL) (|accused_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL NIL)) NIL) (|declared_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL NIL)) NIL) (|undeclared_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below[N]") NIL NIL)) NIL) (|trusted_subset_undeclared| "" (SKOSIMP*) (("" (EXPAND "subset?") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "trusted") (("" (EXPAND "undeclared") (("" (EXPAND "complement") (("" (EXPAND "member") (("" (EXPAND "declared") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|declaration_agreement_undeclared| "" (SKOSIMP*) (("" (PROP) (("1" (CASE "FORALL (x: below(N)): undeclared(act_vec1!1)(x) = undeclared(act_vec2!1)(x)") (("1" (HIDE -2) (("1" (EXPAND "declaration_agreement?") (("1" (SKOSIMP*) (("1" (INST?) (("1" (EXPAND "undeclared") (("1" (EXPAND "complement") (("1" (EXPAND "member") (("1" (EXPAND "declared") (("1" (IFF) (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY + :HIDE? T) (("2" (EXPAND "undeclared") (("2" (EXPAND "complement") (("2" (EXPAND "member") (("2" (EXPAND "declared") (("2" (EXPAND "declaration_agreement?") (("2" (INST?) (("2" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|no_asymmetric_agreement_lem| "" (SKOSIMP*) (("" (EXPAND "symmetric_agreement?") (("" (INST?) (("" (EXPAND "declaration_agreement?") (("" (INST?) (("" (CASE "trusted?(act_vec1!1(p!1))") (("1" (ASSERT) NIL NIL) ("2" (CASE "trusted?(act_vec2!1(p!1))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 4 3 -2) (("2" (CASE "accused?(act_vec1!1(p!1)) & accused?(act_vec2!1(p!1))") (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|all_trusted_good_trusting| "" (SKOSIMP*) (("" (EXPAND "good_trusting?") (("" (EXPAND "all_trusted") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|initial_convicted_validity| "" (EXPAND "convicted_validity?") (("" (EXPAND "emptyset") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|trusted_hybrid_select| "" (SKOSIMP*) (("" (EXPAND "hybrid_select?") (("" (SPLIT) (("1" (HIDE -2) (("1" (EXPAND "subset?") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "trusted") (("1" (EXPAND "trustworthy") (("1" (EXPAND "good_trusting?") (("1" (INST?) (("1" (EXPAND "good?") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (EXPAND "subset?") (("2" (SKOSIMP*) (("2" (EXPAND "complement") (("2" (EXPAND "member") (("2" (EXPAND "trusted") (("2" (EXPAND "benign") (("2" (EXPAND "benign_not_trusting?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|undeclared_hybrid_select| "" (SKOSIMP*) (("" (EXPAND "hybrid_select?") (("" (SPLIT +) (("1" (HIDE -2) (("1" (EXPAND "subset?") (("1" (SKOSIMP*) (("1" (EXPAND "undeclared") (("1" (EXPAND "complement") (("1" (EXPAND "member") (("1" (EXPAND "trustworthy") (("1" (EXPAND "declared") (("1" (EXPAND "good_trusting?") (("1" (INST?) (("1" (EXPAND "good?") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (EXPAND "subset?") (("2" (SKOSIMP*) (("2" (EXPAND "undeclared") (("2" (EXPAND "complement") (("2" (EXPAND "member") (("2" (EXPAND "benign") (("2" (EXPAND "declared") (("2" (EXPAND "benign_declaring?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|difference_hybrid_select_TCC1| "" (SUBTYPE-TCC)) (|difference_hybrid_select| "" (SKOSIMP*) (("" (EXPAND "hybrid_select?") (("" (PROP) (("1" (EXPAND "subset?") (("1" (SKOSIMP*) (("1" (EXPAND "difference") (("1" (EXPAND "undeclared") (("1" (EXPAND "complement") (("1" (EXPAND "member") (("1" (EXPAND "trustworthy") (("1" (EXPAND "declared") (("1" (EXPAND "benign") (("1" (EXPAND "good_trusting?") (("1" (INST?) (("1" (EXPAND "good?") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (EXPAND "subset?") (("2" (SKOSIMP*) (("2" (EXPAND "difference") (("2" (EXPAND "undeclared") (("2" (EXPAND "complement") (("2" (EXPAND "member") (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|hybrid_select_Hybrid_Select_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL NIL)) NIL) (|hybrid_select_Hybrid_Select| "" (SKOSIMP*) (("" (EXPAND "hybrid_select?") (("" (EXPAND "Hybrid_Select") (("" (EXPAND "subset?") (("" (EXPAND "intersection") (("" (EXPAND "complement") (("" (EXPAND "member") (("" (EXPAND "trustworthy") (("" (EXPAND "benign") (("" (EXPAND "trusted") (("" (SPLIT) (("1" (SKOSIMP*) (("1" (SPLIT) (("1" (EXPAND "good_trusting?") (("1" (INST?) (("1" (EXPAND "good?") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "convicted_validity?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (EXPAND "benign_not_trusting?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_accvec_working| "" (SKOSIMP*) (("" (EXPAND "form_accvec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|form_decvec_working| "" (SKOSIMP*) (("" (EXPAND "form_decvec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|form_accvec_correct| "" (SKOSIMP*) (("" (EXPAND "correct_accusation_vector?") (("" (SKOSIMP*) (("" (REWRITE "form_accvec_working") (("" (EXPAND "good_trusting?") (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_decvec_correct| "" (SKOSIMP*) (("" (EXPAND "correct_accusation_vector?") (("" (SKOSIMP*) (("" (REWRITE "form_decvec_working") (("" (EXPAND "good_trusting?") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_decvec_agreement| "" (SKOSIMP*) (("" (PROP) (("1" (CASE "FORALL p: form_decvec(act_vec1!1)(p) = form_decvec(act_vec2!1)(p)") (("1" (HIDE -2) (("1" (EXPAND "declaration_agreement?") (("1" (SKOSIMP*) (("1" (INST?) (("1" (EXPAND "form_decvec") (("1" (LIFT-IF -) (("1" (LIFT-IF -) (("1" (ASSERT) (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (REPLACE*) NIL NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY + :HIDE? T) (("2" (EXPAND "form_decvec") (("2" (EXPAND "declaration_agreement?") (("2" (INST?) (("2" (REPLACE*) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_decvec_benign_not_working| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "benign_declaring?") (("1" (SKOSIMP*) (("1" (EXPAND "benign_not_working?") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "form_decvec_working") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "benign_not_working?") (("2" (SKOSIMP*) (("2" (REWRITE "form_decvec_working") (("2" (EXPAND "benign_declaring?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|extract_accvec_trusted| "" (SKOSIMP*) (("" (EXPAND "extract_accvec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|extract_accvec_declared| "" (SKOSIMP*) (("" (EXPAND "extract_accvec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|extract_decvec_trusted| "" (SKOSIMP*) (("" (ASSERT) (("" (EXPAND "extract_decvec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|extract_decvec_declared| "" (SKOSIMP*) (("" (EXPAND "extract_decvec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|extract_declared| "" (SKOSIMP*) (("" (EXPAND "declaration_agreement?") (("" (SKOSIMP*) (("" (REWRITE "extract_decvec_declared") (("" (REWRITE "form_decvec_working") (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|extract_accvec_good_trusting| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "correct_accusation_vector?") (("1" (SKOSIMP*) (("1" (EXPAND "good_trusting?") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "extract_accvec_trusted") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "good_trusting?") (("2" (SKOSIMP*) (("2" (REWRITE "extract_accvec_trusted") (("2" (EXPAND "correct_accusation_vector?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|extract_decvec_good_trusting| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "correct_accusation_vector?") (("1" (SKOSIMP*) (("1" (EXPAND "good_trusting?") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "extract_decvec_trusted") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "good_trusting?") (("2" (SKOSIMP*) (("2" (REWRITE "extract_decvec_trusted") (("2" (EXPAND "correct_accusation_vector?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|extract_decvec_benign_declaring| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "benign_not_working?") (("1" (SKOSIMP*) (("1" (EXPAND "benign_declaring?") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "extract_decvec_declared") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "benign_declaring?") (("2" (SKOSIMP*) (("2" (REWRITE "extract_decvec_declared") (("2" (EXPAND "benign_not_working?") (("2" (INST?) (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_trusted| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY + :HIDE? T) (("" (EXPAND "trusted") (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_trusted") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_declared| "" (SKOSIMP*) (("" (APPLY-EXTENSIONALITY + :HIDE? T) (("" (EXPAND "declared") (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_declared") (("" (EXPAND "union") (("" (EXPAND "member") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_symmetric_agreement| "" (EXPAND "symmetric_agreement?") (("" (SKOSIMP*) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_trusted") (("" (REWRITE "merge_trusts_trusted") (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_benign_not_trusting1| "" (EXPAND "benign_not_trusting?") (("" (SKOSIMP*) (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_trusted") (("" (FLATTEN) (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_benign_not_trusting2| "" (EXPAND "benign_not_trusting?") (("" (SKOSIMP*) (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_trusted") (("" (FLATTEN) (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_good_trusting| "" (SKOSIMP*) (("" (PROP) (("1" (EXPAND "good_trusting?") (("1" (SKOSIMP*) (("1" (INST?) (("1" (PROP) (("1" (EXPAND "merge_active") (("1" (REWRITE "merge_trusts_trusted") (("1" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "good_trusting?") (("2" (SKOSIMP*) (("2" (INST?) (("2" (PROP) (("2" (EXPAND "merge_active") (("2" (REWRITE "merge_trusts_trusted") (("2" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "good_trusting?") (("3" (SKOSIMP*) (("3" (INST?) (("3" (INST?) (("3" (EXPAND "merge_active") (("3" (REWRITE "merge_trusts_trusted") (("3" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_declaration_agreement| "" (EXPAND "declaration_agreement?") (("" (SKOSIMP*) (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_declared") (("" (REWRITE "merge_trusts_declared") (("" (INST?) (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_across_declaration_agreement| "" (SKOSIMP*) (("" (EXPAND "declaration_agreement?") (("" (SKOSIMP*) (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_declared") (("" (REWRITE "merge_trusts_declared") (("" (INST?) (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_benign_declaring1| "" (EXPAND "benign_declaring?") (("" (SKOSIMP*) (("" (EXPAND "merge_active") (("" (INST?) (("" (REWRITE "merge_trusts_declared") (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|merge_active_benign_declaring2| "" (EXPAND "benign_declaring?") (("" (SKOSIMP*) (("" (EXPAND "merge_active") (("" (REWRITE "merge_trusts_declared") (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$consistent_source_exchange.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : consistent_source_exchange.pvs % % Purpose : A message exchange protocol where all good LEFT nodes % are assumed to transmit equal values. This protocol is % used in two ways: % % 1. as part of the Interactive Consistency protocol % 2. for reliable passing of declarations % during the Diagnosis Protocol. % % Assumptions : This protocol depends upon the following assumptions: % % 1. all good LEFTs transmit the same message. % 2. every good LEFT transmits a message that conforms to % the format specified by exp. % % Guarantees : validity and agreement theorems % % Design : SPIDER Version 0 % % Dependencies : local_fault_model, good_selective_majority, % message_quality % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Alfons Geser % ICASE % 3 West Reid Street / MS 132 C % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-8003 % fax: 757-864-6134 % mailto: geser@icase.edu % http://www.icase.edu/~geser/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % March 11, 2001 - Replaces material in reliable_declaration_passing % and (with LEFT and RIGHT interchanged) symmetric % material in Spider_Interactive_Consistency. New % parameter exp indicates which format good LEFTs % use. exp = valid_only for reliable declaration % passing; exp = valid_or_source_error for % Interactive Consistency. % March 22, 2002 - Cleaned up theory hierarchy. (Miner) % April 11, 2002 - Replaced good_vote_same? by good_vote_for? (not % everywhere!) % - Simplified lemma disqualified_relays_trusted? % - Added lemmas trusted_relays_subset? and % elim_csx_relays_hybrid_majority_good? % November 13, 2002 - Renamed cxs_agreement{1,2} into % csx_agreement_{propagation,generation}. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% consistent_source_exchange [ L : posnat % number of LEFTs , R : posnat % number of RIGHTs , T : NONEMPTY_TYPE % Broadcast is defined for any % message type ] : THEORY BEGIN IMPORTING local_fault_model[L] , Broadcast_Primitives[L,R,T] , good_selective_majority[L,robus_data[T]] status : var node_status[L] exp : var expected G : var below(L) r, r1, r2 : var below(R) d_vect, d_vect1, d_vect2 : var [below(L) -> robus_data[T]] d, d1, d2 : var robus_data[T] act_l, act_l1, act_l2 : var Active_Vector_Type[L] relay_data(status)(d_vect,exp)(r)(G) : robus_data[T] = input_filter(send(status)(G,d_vect(G),r),exp) relay_data_validity: LEMMA good_message?(status,d_vect,exp) & good?(status(G)) => relay_data(status)(d_vect,exp)(r)(G) = d_vect(G) relay_data_good_message: LEMMA good_message?(status,d_vect,exp) => good_message?(status,relay_data(status)(d_vect,exp)(r),exp) relay_data_benign_message: LEMMA benign_message?(status,relay_data(status)(d_vect,exp)(r)) relay_data_good_vote_for: LEMMA good_vote_for?(status, d_vect, d) & good_message?(status,d_vect,exp) => good_vote_for?(status, relay_data(status)(d_vect, exp)(r), d) relay_data_consistent: LEMMA no_asymmetric?(status,trusted(act_l)) => similar_vector?(trusted(act_l), relay_data(status)(d_vect, exp)(r1), relay_data(status)(d_vect, exp)(r2)) relay_data_accusation_basis: LEMMA good_message?(status,d_vect,exp) & NOT conforms?(relay_data(status)(d_vect,exp)(r)(G),exp) => NOT good?(status(G)) disqualified_relays(d_vect,exp) : Active_Vector_Type[L] = LAMBDA G: IF conforms?(d_vect(G),exp) THEN trusted ELSE accused ENDIF disqualified_relays_trusted: LEMMA trusted?(disqualified_relays(d_vect,exp)(G)) IFF conforms?(d_vect(G),exp) disqualified_relays_good_trusting: LEMMA good_message?(status,d_vect,exp) => good_trusting?(status,disqualified_relays(d_vect,exp)) disqualified_relays_benign_not_trusting: LEMMA benign_message?(status,d_vect) => benign_not_trusting?(status,disqualified_relays(d_vect,exp)) elim_relays(d_vect,act_l,exp) : Active_Vector_Type[L] = merge_active(disqualified_relays(d_vect,exp),act_l) elim_relays_trusted_agreement: LEMMA no_asymmetric?(status,trusted(act_l1)) & no_asymmetric?(status,trusted(act_l2)) & symmetric_agreement?(status,act_l1,act_l2) & similar_vector?(trusted(act_l1), d_vect1, d_vect2) => trusted(elim_relays(d_vect1,act_l1,exp)) = trusted(elim_relays(d_vect2,act_l2,exp)) elim_relays_good_trusting: LEMMA good_message?(status,d_vect,exp) & good_trusting?(status,act_l) => good_trusting?(status,elim_relays(d_vect,act_l,exp)) elim_relays_benign_not_trusting: LEMMA benign_message?(status,d_vect) => benign_not_trusting?(status,elim_relays(d_vect,act_l,exp)) trusted_relays_hybrid_select: LEMMA good_trusting?(status,act_l) & good_message?(status,d_vect,exp) & benign_message?(status,d_vect) => hybrid_select?(status,trusted(elim_relays(d_vect,act_l,exp))) trusted_relays_subset: LEMMA subset?(trusted(elim_relays(d_vect1, act_l, exp)), trusted(act_l)) trusted_relays_hybrid_majority_good : LEMMA hybrid_majority_good?(status,trusted(act_l)) => hybrid_majority_good?(status, trusted(elim_relays(d_vect,act_l,exp))) trusted_relay_similar : LEMMA similar_vector?(trusted(act_l), d_vect1, d_vect2) => similar_vector?(trusted(elim_relays(d_vect1, act_l, exp)), d_vect1, d_vect2) vote(d_vect,act_l,exp) : robus_data[T] = majority(trusted(elim_relays(d_vect,act_l,exp)),no_majority)(d_vect) vote_validity: LEMMA good_trusting?(status,act_l) & good_message?(status,d_vect,exp) & benign_message?(status,d_vect) & hybrid_majority_good?(status,trusted(elim_relays(d_vect,act_l,exp))) & good_vote_for?(status, d_vect, d) => vote(d_vect,act_l,exp) = d vote_agreement: LEMMA no_asymmetric?(status,trusted(act_l1)) & no_asymmetric?(status,trusted(act_l2)) & symmetric_agreement?(status,act_l1,act_l2) & similar_vector?(trusted(act_l1), d_vect1, d_vect2) => vote(d_vect1,act_l1,exp) = vote(d_vect2,act_l2,exp) spider_csx(status,d_vect,act_l,exp)(r) : robus_data[T] = vote(relay_data(status)(d_vect,exp)(r),act_l,exp) elim_csx_relays(status,d_vect,act_l,exp)(r) : Active_Vector_Type[L] = elim_relays(relay_data(status)(d_vect,exp)(r),act_l,exp) elim_csx_relays_hybrid_majority_good: LEMMA hybrid_majority_good?(status,trusted(act_l)) => hybrid_majority_good?(status, trusted(elim_csx_relays(status,d_vect,act_l,exp)(r))) csx_validity: THEOREM good_trusting?(status,act_l) & good_message?(status,d_vect,exp) & good_vote_for?(status, d_vect, d) & hybrid_majority_good?(status, trusted(elim_csx_relays(status,d_vect,act_l,exp)(r))) => spider_csx(status,d_vect,act_l,exp)(r) = d csx_agreement_propagation: THEOREM good_trusting?(status,act_l1) & good_trusting?(status,act_l2) & good_message?(status,d_vect,exp) & good_vote_same?(status, d_vect) & hybrid_majority_good?(status, trusted(elim_csx_relays(status,d_vect,act_l1,exp)(r1))) & hybrid_majority_good?(status, trusted(elim_csx_relays(status,d_vect,act_l2,exp)(r2))) => spider_csx(status,d_vect,act_l1,exp)(r1) = spider_csx(status,d_vect,act_l2,exp)(r2) csx_agreement_generation: THEOREM symmetric_agreement?(status,act_l1,act_l2) & no_asymmetric?(status,trusted(act_l1)) & no_asymmetric?(status,trusted(act_l2)) => spider_csx(status,d_vect,act_l1,exp)(r1) = spider_csx(status,d_vect,act_l2,exp)(r2) observation_basis: LEMMA good_trusting?(status,act_l) & good_message?(status,d_vect,exp) & hybrid_majority_good?(status, trusted(elim_csx_relays(status,d_vect,act_l,exp)(r))) & spider_csx(status,d_vect,act_l,exp)(r) /= relay_data(status)(d_vect,exp)(r)(G) => NOT good?(status(G)) OR NOT good_vote_same?(status, d_vect) observation_disagreement: LEMMA good_trusting?(status,act_l) & good_message?(status,d_vect,exp) & hybrid_majority_good?(status, trusted(elim_csx_relays(status,d_vect,act_l,exp)(r))) & spider_csx(status,d_vect,act_l,exp)(r) /= relay_data(status)(d_vect,exp)(r)(G) & good?(status(G)) => NOT good_vote_same?(status, d_vect) END consistent_source_exchange $$$consistent_source_exchange.prf (consistent_source_exchange (relay_data_validity 0 (relay_data_validity-1 nil 3300806980 3300807014 ("" (skosimp*) (("" (expand "relay_data") (("" (rewrite "send_validity") (("" (use "input_filter_validity") (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((relay_data const-decl "robus_data[T]" consistent_source_exchange nil) (input_filter_validity formula-decl nil Broadcast_Primitives nil) (expected type-decl nil hybrid_fault_types nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (robus_data type-decl nil robus_data_adt nil) (send_validity formula-decl nil Broadcast_Primitives nil)) 127 110 nil nil)) (relay_data_good_message 0 (relay_data_good_message-1 nil 3300806980 3300807015 ("" (skosimp*) (("" (expand "good_message?" 1) (("" (skosimp*) (("" (rewrite "relay_data_validity") (("" (expand "good_message?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((good_message? const-decl "bool" message_quality nil) (relay_data_validity formula-decl nil consistent_source_exchange nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (robus_data type-decl nil robus_data_adt nil) (expected type-decl nil hybrid_fault_types nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil)) 121 90 nil nil)) (relay_data_benign_message 0 (relay_data_benign_message-1 nil 3300806980 3300807015 ("" (skosimp*) (("" (expand "benign_message?") (("" (skosimp*) (("" (expand "relay_data") (("" (expand "send") (("" (assert) (("" (expand "input_filter") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((benign_message? const-decl "bool" message_quality nil) (relay_data const-decl "robus_data[T]" consistent_source_exchange nil) (input_filter const-decl "robus_data[T]" Broadcast_Primitives nil) (send const-decl "robus_data[T]" Broadcast_Primitives nil)) 155 130 nil nil)) (relay_data_good_vote_for 0 (relay_data_good_vote_for-1 nil 3300806980 3300807015 ("" (skosimp*) (("" (expand "good_vote_for?") (("" (skosimp*) (("" (inst?) (("" (prop) (("" (rewrite "relay_data_validity") nil nil)) nil)) nil)) nil)) nil)) nil) proved ((good_vote_for? const-decl "bool" good_selective_majority nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil nat_types nil) (relay_data_validity formula-decl nil consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (robus_data type-decl nil robus_data_adt nil) (expected type-decl nil hybrid_fault_types nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil)) 151 130 nil nil)) (relay_data_consistent 0 (relay_data_consistent-1 nil 3300806980 3300807015 ("" (skosimp*) (("" (expand "similar_vector?") (("" (skosimp*) (("" (expand "no_asymmetric?") (("" (inst?) (("" (expand "trusted") (("" (assert) (("" (expand "relay_data") (("" (lemma "send_agreement") (("" (inst - "_" "_" "_" "r1!1" "r2!1") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((similar_vector? const-decl "bool" selective_vector_majority nil) (no_asymmetric? const-decl "bool" global_fault_model nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (relay_data const-decl "robus_data[T]" consistent_source_exchange nil) (robus_data type-decl nil robus_data_adt nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (send_agreement formula-decl nil Broadcast_Primitives nil) (below type-eq-decl nil naturalnumbers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 202 110 nil nil)) (relay_data_accusation_basis 0 (relay_data_accusation_basis-1 nil 3300806980 3300807015 ("" (skosimp*) (("" (use "relay_data_good_message") (("" (assert) (("" (expand "good_message?" -1) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((relay_data_good_message formula-decl nil consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (good_message? const-decl "bool" message_quality nil)) 85 80 nil nil)) (disqualified_relays_trusted 0 (disqualified_relays_trusted-1 nil 3300806980 3300807015 ("" (skosimp*) (("" (expand "disqualified_relays") (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil) proved ((disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil)) 50 40 nil nil)) (disqualified_relays_good_trusting 0 (disqualified_relays_good_trusting-1 nil 3300806980 3300807015 ("" (expand "good_trusting?") (("" (skosimp*) (("" (expand "disqualified_relays") (("" (lift-if) (("" (assert) (("" (prop) (("" (expand "good_message?") (("" (inst?) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (good_message? const-decl "bool" message_quality nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (good_trusting? const-decl "bool" local_fault_model nil)) 99 80 nil nil)) (disqualified_relays_benign_not_trusting 0 (disqualified_relays_benign_not_trusting-1 nil 3300806980 3300807016 ("" (skosimp*) (("" (expand "benign_not_trusting?") (("" (skosimp*) (("" (expand "disqualified_relays") (("" (lift-if) (("" (assert) (("" (prop) (("" (expand "benign_message?") (("" (inst?) (("" (assert) (("" (expand "conforms?") (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((benign_not_trusting? const-decl "bool" local_fault_model nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (benign_message? const-decl "bool" message_quality nil) (conforms? const-decl "bool" message_quality nil) (below type-eq-decl nil naturalnumbers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 118 110 nil nil)) (elim_relays_trusted_agreement 0 (elim_relays_trusted_agreement-1 nil 3300806980 3300807587 ("" (skosimp*) (("" (apply-extensionality + :hide? t) (("" (expand "trusted") (("" (expand "elim_relays") (("" (expand "merge_active") (("" (rewrite "merge_trusts_trusted") (("" (rewrite "merge_trusts_trusted") (("" (rewrite "disqualified_relays_trusted") (("" (rewrite "disqualified_relays_trusted") (("" (expand "similar_vector?") (("" (inst?) (("" (expand "no_asymmetric?") (("" (inst?) (("" (inst?) (("" (expand "symmetric_agreement?") (("" (inst?) (("" (case "asymmetric?(status!1(x!1))") (("1" (assert) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (replace -1 :dir rl :hide? t) (("2" (case "trusted?(act_l1!1(x!1))") (("1" (assert) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil nat_types nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (merge_trusts_trusted formula-decl nil hybrid_fault_types nil) (disqualified_relays_trusted formula-decl nil consistent_source_exchange nil) (similar_vector? const-decl "bool" selective_vector_majority nil) (no_asymmetric? const-decl "bool" global_fault_model nil) (trusted? adt-recognizer-decl "[trust -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (asymmetric? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (symmetric_agreement? const-decl "bool" local_fault_model nil) (merge_active const-decl "Active_Vector_Type" local_fault_model nil)) 56315 6210 t nil)) (elim_relays_good_trusting 0 (elim_relays_good_trusting-1 nil 3300806980 3300807016 ("" (skosimp*) (("" (expand "elim_relays") (("" (rewrite "merge_active_good_trusting") (("" (rewrite "disqualified_relays_good_trusting") nil nil)) nil)) nil)) nil) proved ((elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (disqualified_relays_good_trusting formula-decl nil consistent_source_exchange nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (merge_active_good_trusting formula-decl nil local_fault_model nil)) 95 60 nil nil)) (elim_relays_benign_not_trusting 0 (elim_relays_benign_not_trusting-1 nil 3300806980 3300807016 ("" (skosimp*) (("" (expand "elim_relays") (("" (rewrite "merge_active_benign_not_trusting1") (("" (hide 2) (("" (rewrite "disqualified_relays_benign_not_trusting") nil nil)) nil)) nil)) nil)) nil) proved ((elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (disqualified_relays_benign_not_trusting formula-decl nil consistent_source_exchange nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (merge_active_benign_not_trusting1 formula-decl nil local_fault_model nil)) 102 60 nil nil)) (trusted_relays_hybrid_select 0 (trusted_relays_hybrid_select-1 nil 3300806980 3300807016 ("" (skosimp*) (("" (use "trusted_hybrid_select") (("" (prop) (("1" (rewrite "elim_relays_good_trusting") nil nil) ("2" (rewrite "elim_relays_benign_not_trusting") nil nil)) nil)) nil)) nil) proved ((trusted_hybrid_select formula-decl nil local_fault_model nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (elim_relays_benign_not_trusting formula-decl nil consistent_source_exchange nil) (elim_relays_good_trusting formula-decl nil consistent_source_exchange nil)) 106 70 nil nil)) (trusted_relays_subset 0 (trusted_relays_subset-1 nil 3300806980 3300807016 ("" (skosimp*) (("" (expand "subset?") (("" (skosimp*) (("" (expand "elim_relays") (("" (rewrite "merge_active_trusted") (("" (expand "intersection") (("" (expand "member") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((subset? const-decl "bool" sets nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (merge_active_trusted formula-decl nil local_fault_model nil)) 104 80 nil nil)) (trusted_relays_hybrid_majority_good 0 (trusted_relays_hybrid_majority_good-1 nil 3300806980 3300807016 ("" (skosimp*) (("" (lemma "hybrid_majority_good_subset") (("" (inst - "trusted(elim_relays(d_vect!1, act_l!1, exp!1))" "trusted(act_l!1)" "status!1") (("" (assert) (("" (rewrite "trusted_relays_subset") nil nil)) nil)) nil)) nil)) nil) proved ((L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (trusted_relays_subset formula-decl nil consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (trust type-decl nil hybrid_fault_types nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 89 70 nil nil)) (trusted_relay_similar 0 (trusted_relay_similar-1 nil 3300806980 3300807017 ("" (skosimp*) (("" (lemma "similar_vector_subset") (("" (inst - "trusted(elim_relays(d_vect1!1, act_l!1, exp!1))" "trusted(act_l!1)" "_" "_") (("" (inst?) (("" (assert) (("" (rewrite "trusted_relays_subset") nil nil)) nil)) nil)) nil)) nil)) nil) proved ((robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (similar_vector_subset formula-decl nil selective_vector_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (trusted_relays_subset formula-decl nil consistent_source_exchange nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 109 80 nil nil)) (vote_validity 0 (vote_validity-1 nil 3300806980 3300807017 ("" (skosimp*) (("" (expand "vote") (("" (use "good_vote_for_majority") (("" (prop) (("" (rewrite "trusted_relays_hybrid_select") nil nil)) nil)) nil)) nil)) nil) proved ((vote const-decl "robus_data[T]" consistent_source_exchange nil) (trusted_relays_hybrid_select formula-decl nil consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (no_majority? adt-recognizer-decl "[robus_data -> boolean]" robus_data_adt nil) (no_majority adt-constructor-decl "(no_majority?)" robus_data_adt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (expected type-decl nil hybrid_fault_types nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (value_vector type-eq-decl nil selective_vector_majority nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (good_vote_for_majority formula-decl nil good_selective_majority nil)) 123 90 nil nil)) (vote_agreement 0 (vote_agreement-1 nil 3300806980 3300807017 ("" (skosimp*) (("" (expand "vote") (("" (lemma "elim_relays_trusted_agreement") (("" (inst - "act_l1!1" "act_l2!1" "d_vect1!1" "d_vect2!1" "exp!1" "status!1") (("" (assert) (("" (replace -1 :dir rl :hide? t) (("" (rewrite "majority_unique") (("" (rewrite "trusted_relay_similar") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((vote const-decl "robus_data[T]" consistent_source_exchange nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (trust type-decl nil hybrid_fault_types nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (robus_data type-decl nil robus_data_adt nil) (expected type-decl nil hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (trusted_relay_similar formula-decl nil consistent_source_exchange nil) (value_vector type-eq-decl nil selective_vector_majority nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (no_majority adt-constructor-decl "(no_majority?)" robus_data_adt nil) (no_majority? adt-recognizer-decl "[robus_data -> boolean]" robus_data_adt nil) (majority_unique formula-decl nil selective_vector_majority nil) (elim_relays_trusted_agreement formula-decl nil consistent_source_exchange nil)) 159 100 nil nil)) (elim_csx_relays_hybrid_majority_good 0 (elim_csx_relays_hybrid_majority_good-1 nil 3300806980 3300807017 ("" (skosimp*) (("" (lemma "hybrid_majority_good_subset[L]") (("" (inst - "trusted(elim_csx_relays (status!1, d_vect!1, act_l!1, exp!1) (r!1))" "trusted(act_l!1)" "_") (("" (inst?) (("" (assert) (("" (hide-all-but 1) (("" (expand "subset?") (("" (skosimp*) (("" (expand "elim_csx_relays") (("" (expand "elim_relays") (("" (rewrite "merge_active_trusted") (("" (expand "intersection") (("" (expand "member") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (merge_active_trusted formula-decl nil local_fault_model nil) (disqualified_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (relay_data const-decl "robus_data[T]" consistent_source_exchange nil) (subset? const-decl "bool" sets nil) (elim_csx_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (trust type-decl nil hybrid_fault_types nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 169 120 nil nil)) (csx_validity 0 (csx_validity-1 nil 3300806980 3300807017 ("" (skosimp*) (("" (expand "spider_csx") (("" (expand "elim_csx_relays") (("" (lemma "vote_validity") (("" (inst - "_" "_" "relay_data(status!1)(d_vect!1, exp!1)(r!1)" "_" "_") (("" (inst?) (("" (inst?) (("" (assert) (("" (hide 2) (("" (rewrite "relay_data_good_message") (("" (rewrite "relay_data_benign_message") (("" (rewrite "relay_data_good_vote_for") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((spider_csx const-decl "robus_data[T]" consistent_source_exchange nil) (vote_validity formula-decl nil consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (relay_data_good_message formula-decl nil consistent_source_exchange nil) (relay_data_good_vote_for formula-decl nil consistent_source_exchange nil) (relay_data_benign_message formula-decl nil consistent_source_exchange nil) (relay_data const-decl "robus_data[T]" consistent_source_exchange nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (elim_csx_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil)) 205 120 nil nil)) (csx_agreement_propagation 0 (csx_agreement_propagation-1 nil 3300806980 3300807017 ("" (skosimp*) (("" (use "hybrid_majority_exists_good[L]") (("" (skosimp*) (("" (use "good_vote_for_instance") (("" (assert) (("" (lemma "csx_validity") (("" (inst - "_" "d_vect!1(p!1)" "d_vect!1" "exp!1" "_" "status!1") (("" (inst-cp - "act_l1!1" "r1!1") (("" (inst - "act_l2!1" "r2!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((hybrid_majority_exists_good formula-decl nil global_fault_model nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (good_vote_for_instance formula-decl nil good_selective_majority nil) (value_vector type-eq-decl nil selective_vector_majority nil) (below type-eq-decl nil nat_types nil) (csx_validity formula-decl nil consistent_source_exchange nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (expected type-decl nil hybrid_fault_types nil)) 235 190 nil nil)) (csx_agreement_generation 0 (csx_agreement_generation-1 nil 3300806980 3300807018 ("" (skosimp*) (("" (expand "spider_csx") (("" (lemma "relay_data_consistent") (("" (inst?) (("" (inst - "_" "r2!1") (("" (inst?) (("" (prop) (("" (lemma "vote_agreement") (("" (inst?) (("" (inst?) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((spider_csx const-decl "robus_data[T]" consistent_source_exchange nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (robus_data type-decl nil robus_data_adt nil) (expected type-decl nil hybrid_fault_types nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (vote_agreement formula-decl nil consistent_source_exchange nil) (relay_data const-decl "robus_data[T]" consistent_source_exchange nil) (relay_data_consistent formula-decl nil consistent_source_exchange nil)) 133 90 nil nil)) (observation_basis 0 (observation_basis-1 nil 3300806980 3300807018 ("" (skosimp*) (("" (rewrite "relay_data_validity") (("" (rewrite "csx_validity") (("" (use "good_vote_for_instance") (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((relay_data_validity formula-decl nil consistent_source_exchange nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (below type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (robus_data type-decl nil robus_data_adt nil) (expected type-decl nil hybrid_fault_types nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (good_vote_for_instance formula-decl nil good_selective_majority nil) (below type-eq-decl nil nat_types nil) (value_vector type-eq-decl nil selective_vector_majority nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (csx_validity formula-decl nil consistent_source_exchange nil)) 134 100 nil nil)) (observation_disagreement 0 (observation_disagreement-1 nil 3300806980 3300807018 ("" (skosimp*) (("" (use "observation_basis") (("" (assert) nil nil)) nil)) nil) proved ((observation_basis formula-decl nil consistent_source_exchange nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (R formal-const-decl "posnat" consistent_source_exchange nil) (expected type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (T formal-nonempty-type-decl nil consistent_source_exchange nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (L formal-const-decl "posnat" consistent_source_exchange nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 140 130 nil nil))) $$$robus_data_adt.pvs %%% ADT file generated from robus_data robus_data_adt[T: NONEMPTY_TYPE]: THEORY BEGIN ASSUMING T_TCC1: ASSUMPTION EXISTS (x: T): TRUE; ENDASSUMING robus_data: TYPE source_error?, receive_error?, no_majority?, valid?: [robus_data -> boolean] source_error: (source_error?) receive_error: (receive_error?) no_majority: (no_majority?) valid: [T -> (valid?)] value: [(valid?) -> T] ord(x: robus_data): upto(3) = CASES x OF source_error: 0, receive_error: 1, no_majority: 2, valid(valid1_var): 3 ENDCASES robus_data_source_error_extensionality: AXIOM FORALL (source_error?_var: (source_error?), source_error?_var2: (source_error?)): source_error?_var = source_error?_var2; robus_data_receive_error_extensionality: AXIOM FORALL (receive_error?_var: (receive_error?), receive_error?_var2: (receive_error?)): receive_error?_var = receive_error?_var2; robus_data_no_majority_extensionality: AXIOM FORALL (no_majority?_var: (no_majority?), no_majority?_var2: (no_majority?)): no_majority?_var = no_majority?_var2; robus_data_valid_extensionality: AXIOM FORALL (valid?_var: (valid?), valid?_var2: (valid?)): value(valid?_var) = value(valid?_var2) IMPLIES valid?_var = valid?_var2; robus_data_valid_eta: AXIOM FORALL (valid?_var: (valid?)): valid(value(valid?_var)) = valid?_var; robus_data_value_valid: AXIOM FORALL (valid1_var: T): value(valid(valid1_var)) = valid1_var; robus_data_inclusive: AXIOM FORALL (robus_data_var: robus_data): source_error?(robus_data_var) OR receive_error?(robus_data_var) OR no_majority?(robus_data_var) OR valid?(robus_data_var); robus_data_disjoint: AXIOM FORALL (robus_data_var: robus_data): NOT (source_error?(robus_data_var) AND receive_error?(robus_data_var)) AND NOT (source_error?(robus_data_var) AND no_majority?(robus_data_var)) AND NOT (source_error?(robus_data_var) AND valid?(robus_data_var)) AND NOT (receive_error?(robus_data_var) AND no_majority?(robus_data_var)) AND NOT (receive_error?(robus_data_var) AND valid?(robus_data_var)) AND NOT (no_majority?(robus_data_var) AND valid?(robus_data_var)); robus_data_induction: AXIOM FORALL (p: [robus_data -> boolean]): (p(source_error) AND p(receive_error) AND p(no_majority) AND (FORALL (valid1_var: T): p(valid(valid1_var)))) IMPLIES (FORALL (robus_data_var: robus_data): p(robus_data_var)); every(p: PRED[T])(a: robus_data): boolean = CASES a OF source_error: TRUE, receive_error: TRUE, no_majority: TRUE, valid(valid1_var): p(valid1_var) ENDCASES; every(p: PRED[T], a: robus_data): boolean = CASES a OF source_error: TRUE, receive_error: TRUE, no_majority: TRUE, valid(valid1_var): p(valid1_var) ENDCASES; some(p: PRED[T])(a: robus_data): boolean = CASES a OF source_error: FALSE, receive_error: FALSE, no_majority: FALSE, valid(valid1_var): p(valid1_var) ENDCASES; some(p: PRED[T], a: robus_data): boolean = CASES a OF source_error: FALSE, receive_error: FALSE, no_majority: FALSE, valid(valid1_var): p(valid1_var) ENDCASES; subterm(x, y: robus_data): boolean = x = y; <<: (well_founded?[robus_data]) = LAMBDA (x, y: robus_data): FALSE; robus_data_well_founded: AXIOM well_founded?[robus_data](<<); reduce_nat(source_error?_fun, receive_error?_fun, no_majority?_fun: nat, valid?_fun: [T -> nat]): [robus_data -> nat] = LAMBDA (robus_data_adtvar: robus_data): LET red: [robus_data -> nat] = reduce_nat(source_error?_fun, receive_error?_fun, no_majority?_fun, valid?_fun) IN CASES robus_data_adtvar OF source_error: source_error?_fun, receive_error: receive_error?_fun, no_majority: no_majority?_fun, valid(valid1_var): valid?_fun(valid1_var) ENDCASES; REDUCE_nat(source_error?_fun, receive_error?_fun, no_majority?_fun: [robus_data -> nat], valid?_fun: [[T, robus_data] -> nat]): [robus_data -> nat] = LAMBDA (robus_data_adtvar: robus_data): LET red: [robus_data -> nat] = REDUCE_nat(source_error?_fun, receive_error?_fun, no_majority?_fun, valid?_fun) IN CASES robus_data_adtvar OF source_error: source_error?_fun(robus_data_adtvar), receive_error: receive_error?_fun(robus_data_adtvar), no_majority: no_majority?_fun(robus_data_adtvar), valid(valid1_var): valid?_fun(valid1_var, robus_data_adtvar) ENDCASES; reduce_ordinal(source_error?_fun, receive_error?_fun, no_majority?_fun: ordinal, valid?_fun: [T -> ordinal]): [robus_data -> ordinal] = LAMBDA (robus_data_adtvar: robus_data): LET red: [robus_data -> ordinal] = reduce_ordinal(source_error?_fun, receive_error?_fun, no_majority?_fun, valid?_fun) IN CASES robus_data_adtvar OF source_error: source_error?_fun, receive_error: receive_error?_fun, no_majority: no_majority?_fun, valid(valid1_var): valid?_fun(valid1_var) ENDCASES; REDUCE_ordinal(source_error?_fun, receive_error?_fun, no_majority?_fun: [robus_data -> ordinal], valid?_fun: [[T, robus_data] -> ordinal]): [robus_data -> ordinal] = LAMBDA (robus_data_adtvar: robus_data): LET red: [robus_data -> ordinal] = REDUCE_ordinal(source_error?_fun, receive_error?_fun, no_majority?_fun, valid?_fun) IN CASES robus_data_adtvar OF source_error: source_error?_fun(robus_data_adtvar), receive_error: receive_error?_fun(robus_data_adtvar), no_majority: no_majority?_fun(robus_data_adtvar), valid(valid1_var): valid?_fun(valid1_var, robus_data_adtvar) ENDCASES; END robus_data_adt robus_data_adt_map[T: NONEMPTY_TYPE, T1: NONEMPTY_TYPE]: THEORY BEGIN ASSUMING T_TCC1: ASSUMPTION EXISTS (x: T): TRUE; T1_TCC1: ASSUMPTION EXISTS (x: T1): TRUE; ENDASSUMING IMPORTING robus_data_adt map(f: [T -> T1])(a: robus_data[T]): robus_data[T1] = CASES a OF source_error: source_error, receive_error: receive_error, no_majority: no_majority, valid(valid1_var): valid(f(valid1_var)) ENDCASES; map(f: [T -> T1], a: robus_data[T]): robus_data[T1] = CASES a OF source_error: source_error, receive_error: receive_error, no_majority: no_majority, valid(valid1_var): valid(f(valid1_var)) ENDCASES; END robus_data_adt_map robus_data_adt_reduce[T: NONEMPTY_TYPE, range: TYPE]: THEORY BEGIN ASSUMING T_TCC1: ASSUMPTION EXISTS (x: T): TRUE; ENDASSUMING IMPORTING robus_data_adt[T] reduce(source_error?_fun, receive_error?_fun, no_majority?_fun: range, valid?_fun: [T -> range]): [robus_data -> range] = LAMBDA (robus_data_adtvar: robus_data): LET red: [robus_data -> range] = reduce(source_error?_fun, receive_error?_fun, no_majority?_fun, valid?_fun) IN CASES robus_data_adtvar OF source_error: source_error?_fun, receive_error: receive_error?_fun, no_majority: no_majority?_fun, valid(valid1_var): valid?_fun(valid1_var) ENDCASES; REDUCE(source_error?_fun, receive_error?_fun, no_majority?_fun: [robus_data -> range], valid?_fun: [[T, robus_data] -> range]): [robus_data -> range] = LAMBDA (robus_data_adtvar: robus_data): LET red: [robus_data -> range] = REDUCE(source_error?_fun, receive_error?_fun, no_majority?_fun, valid?_fun) IN CASES robus_data_adtvar OF source_error: source_error?_fun(robus_data_adtvar), receive_error: receive_error?_fun(robus_data_adtvar), no_majority: no_majority?_fun(robus_data_adtvar), valid(valid1_var): valid?_fun(valid1_var, robus_data_adtvar) ENDCASES; END robus_data_adt_reduce $$$robus_data.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : robus_data.pvs % % Purpose : datatype declaration for robus data messages % % Assumptions : Parameter T is a NONEMPTY_TYPE % % Guarantees : A source_error is distinguishable from valid data % % Design : SPIDER Version 0 % % Dependencies : none % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Paul S. Miner % 1 South Wright St. / MS 130 % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-6201 % fax: 757-864-4234 % mailto:p.s.miner@larc.nasa.gov % http://shemesh.larc.nasa.gov/~psm/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notes % 1. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % July 26, 2000 - Added this header % December 15, 2000 - Added no_majority field for diagnosis % protocol, added comments % October 17, 2001 - renamed from relay_data to robus_data % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% robus_data[T:NONEMPTY_TYPE]: DATATYPE BEGIN source_error : source_error? % Used to tell other nodes that % the source of a message was % manifestly faulty receive_error : receive_error? % Used within a node, should % never be transmitted no_majority : no_majority? % There was no majority valid(value : T) : valid? % Properly formatted data % messsage END robus_data $$$hybrid_fault_types.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : hybrid_fault_types.pvs % % Purpose : Enumerated type declaration for the hybrid fault % model fault classification. This is in a separate % file with no formal parameters to allow for multiple % uses of this classification scheme. % % Also declares enumerated type `accusation'. % % Assumptions : none % % Guarantees : none % % Design : SPIDER Version 0 % % Dependencies : none % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Paul S. Miner % 1 South Wright St. / MS 130 % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-6201 % fax: 757-864-4234 % mailto:p.s.miner@larc.nasa.gov % http://shemesh.larc.nasa.gov/~psm/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notes % 1. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % July 26, 2000 - Added this header % December 14, 2000 - Added type accusation % November 7, 2001 - Added function merge_trusts (Geser) % March 11, 2002 - Added enumeration type expected (Geser) % March 28, 2002 - Added lemmas for merge_trusts (Geser) % November 13, 2002 - Added lemmas form_acc_char and form_acc_agreement % (Geser) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% hybrid_fault_types: THEORY BEGIN fault_classification: TYPE = {trustworthy, recovering, benign, symmetric, asymmetric} good?(x : fault_classification) : bool = trustworthy?(x) or recovering?(x) trust: TYPE = {trusted, accused, declared} accusation: TYPE = {working, failed} act, act1, act2 : var trust acc, acc1, acc2 : var accusation any_accusation(act) : accusation form_acc(act): accusation = IF trusted?(act) THEN working ELSIF accused?(act) THEN failed ELSE any_accusation(act) ENDIF form_acc_char: LEMMA NOT declared?(act) => form_acc(act) = IF trusted?(act) THEN working ELSE failed ENDIF form_acc_working: LEMMA NOT declared?(act) => (working?(form_acc(act)) IFF trusted?(act)) form_acc_agreement: LEMMA NOT declared?(act1) & NOT declared?(act2) => (form_acc(act1) = form_acc(act2) IFF trusted?(act1) = trusted?(act2)) form_dec(act): accusation = IF declared?(act) THEN failed ELSE working ENDIF form_dec_working: LEMMA working?(form_dec(act)) IFF NOT declared?(act) form_dec_agreement: LEMMA form_dec(act1) = form_dec(act2) IFF declared?(act1) = declared?(act2) extract_acc(acc) : trust = IF working?(acc) THEN trusted ELSE accused ENDIF extract_acc_trusted: LEMMA trusted?(extract_acc(acc)) IFF working?(acc) extract_acc_declared: LEMMA NOT declared?(extract_acc(acc)) extract_dec(acc) : trust = IF working?(acc) THEN trusted ELSE declared ENDIF extract_dec_trusted: LEMMA trusted?(extract_dec(acc)) IFF working?(acc) extract_dec_declared: LEMMA declared?(extract_dec(acc)) IFF NOT working?(acc) tr1, tr2 : var trust merge_trusts(tr1, tr2) : trust = IF trusted?(tr1) & trusted?(tr2) THEN trusted ELSIF declared?(tr1) OR declared?(tr2) THEN declared ELSE accused ENDIF merge_trusts_trusted : LEMMA trusted?(merge_trusts(tr1, tr2)) IFF trusted?(tr1) & trusted?(tr2) merge_trusts_declared : LEMMA declared?(merge_trusts(tr1, tr2)) IFF declared?(tr1) OR declared?(tr2) expected: TYPE = {valid_only, valid_or_source_error} END hybrid_fault_types $$$hybrid_fault_types.prf (|hybrid_fault_types| (|form_acc_char| "" (SKOSIMP*) (("" (EXPAND "form_acc") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|form_acc_working| "" (SKOSIMP*) (("" (EXPAND "form_acc") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|form_acc_agreement| "" (SKOSIMP*) (("" (REWRITE "form_acc_char") (("" (REWRITE "form_acc_char") (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_dec_working| "" (SKOSIMP*) (("" (EXPAND "form_dec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|form_dec_agreement| "" (SKOSIMP*) (("" (EXPAND "form_dec") (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|extract_acc_trusted| "" (SKOSIMP*) (("" (EXPAND "extract_acc") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|extract_acc_declared| "" (SKOSIMP*) (("" (EXPAND "extract_acc") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|extract_dec_trusted| "" (SKOSIMP*) (("" (EXPAND "extract_dec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|extract_dec_declared| "" (SKOSIMP*) (("" (EXPAND "extract_dec") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|merge_trusts_trusted| "" (SKOSIMP*) (("" (EXPAND "merge_trusts") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|merge_trusts_declared| "" (SKOSIMP*) (("" (EXPAND "merge_trusts") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$global_fault_model.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : global_fault_model.pvs % % Purpose : Provide global fault classifications to partition a % set of nodes indexed from 0 to N - 1. For the % verification of the ROBUS, this theory will be % imported twice: Once for the RMUs and once for the % BIUs % % Assumptions : There is always at least one good node. If there are % no good nodes, then there is nothing any protocol % can do. % % Guarantees : Type declaration for node_status. % % Curried form of status classifications so that we may % discuss cardinalities of the partitions. % % Definition of no_asymmetric?(H,status) % % Definition of hybrid_majority_good?(H,status) % % Design : SPIDER Version 0 % % Dependencies : hybrid_fault_types, finite_sets@finite_sets_below % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Paul S. Miner % 1 South Wright St. / MS 130 % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-6201 % fax: 757-864-4234 % mailto:p.s.miner@larc.nasa.gov % http://shemesh.larc.nasa.gov/~psm/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notes % 1. This classification provides a global view of the failure status % for a set of nodes. This classification is not (and can not) be % known *completely* by the individual nodes. Therefore, protocols % cannot use this partitioning of faults in operation. The protocols % will need to use a local classification of the failure status of the % participants. The protocols will employ a different (but related) % partioning of the node status. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % July 26, 2000 - Added this header % August 1, 2000 - Added additional comments % October 26, 2001 - Refined "good" into "trustworthy" and % "recovering". % November 7, 2001 - Dropped premise of Lemma % "hybrid_majority_exists_good". (Geser) % March 6, 2002 - Weakened no_asymmetric and hybrid_majority_good to % respect the diagnostic information (parameter H). % These properties are preserved by subsets of H. % (Geser) % March 28, 2002 - Added predicate benign_not_working? (Geser) % April 11, 2002 - Changed the order of arguments of no_asymmetric?, % hybrid_majority_good?, hybrid_select?, and % good_votes for uniformity reasons. (Geser) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% global_fault_model[N:posnat]: THEORY BEGIN IMPORTING hybrid_fault_types , finite_sets@finite_sets_below[N] p :var below(N) node_status: TYPE = {f : [below(N) -> fault_classification] | EXISTS p: trustworthy?(f(p))} status: var node_status trustworthy(status) : non_empty_finite_set[below(N)] = {p | trustworthy?(status(p))} recovering(status) : finite_set[below(N)] = {p | recovering?(status(p))} benign(status) : finite_set[below(N)] = {p | benign?(status(p))} symmetric(status) : finite_set[below(N)] = {p | symmetric?(status(p))} asymmetric(status) : finite_set[below(N)] = {p | asymmetric?(status(p))} good(status) : non_empty_finite_set[below(N)] = {p | good?(status(p))} H, H1, H2: var finite_set[below[N]] no_asymmetric?(status,H): bool = FORALL p: (H(p) => NOT asymmetric?(status(p))) no_asymmetric_subset : LEMMA subset?(H1, H2) & no_asymmetric?(status,H2) => no_asymmetric?(status,H1) hybrid_majority_good?(status,H): bool = card(trustworthy(status)) > card(intersection(H,symmetric(status))) + card(intersection(H,asymmetric(status))) hybrid_majority_exists_good : LEMMA EXISTS p: good?(status(p)) hybrid_majority_good_subset : LEMMA subset?(H1, H2) & hybrid_majority_good?(status,H2) => hybrid_majority_good?(status,H1) hybrid_select?(status,H) : bool = subset?(trustworthy(status),H) & subset?(H,complement(benign(status))) good_votes(status,H) : finite_set[below(N)] = union(trustworthy(status),intersection(H,recovering(status))) card_good_votes : LEMMA card(good_votes(status,H)) = card(trustworthy(status)) + card(intersection(H,recovering(status))) card_hybrid_select : LEMMA card(H) = card(intersection(H,trustworthy(status))) + card(intersection(H,recovering(status))) + card(intersection(H,benign(status))) + card(intersection(H,symmetric(status))) + card(intersection(H,asymmetric(status))) no_trusted_benign: LEMMA subset?(H,complement(benign(status))) => intersection(H,benign(status)) = emptyset hybrid_majority_alt: LEMMA hybrid_select?(status,H) & hybrid_majority_good?(status,H) => 2*card(good_votes(status,H)) > card(H) hybrid_majority: LEMMA subset?(H,complement(benign(status))) & hybrid_majority_good?(status,H) => 2*card(good_votes(status,H)) > card(H) accusation_vector_type: TYPE = [below(N) -> accusation] acc_vec, acc1_vec, acc2_vec : var accusation_vector_type correct_accusation_vector?(status, acc_vec): bool = FORALL p: good?(status(p)) => working?(acc_vec(p)) accusation_vector_agreement?(status, acc1_vec, acc2_vec): bool = FORALL p: NOT asymmetric?(status(p)) => (acc1_vec(p) = acc2_vec(p)) benign_not_working?(status, acc_vec): bool = FORALL p: benign?(status(p)) => NOT working?(acc_vec(p)) END global_fault_model $$$global_fault_model.prf (global_fault_model (trustworthy_TCC1 0 (trustworthy_TCC1-1 nil 3264354197 nil ("" (skosimp*) (("" (rewrite "finite_below") (("" (expand "empty?") (("" (expand "member") (("" (typepred "status!1") (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_below formula-decl nil finite_sets_below "finite_sets/")) nil nil nil nil)) (recovering_TCC1 0 (recovering_TCC1-1 nil 3264354197 nil ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved-complete ((N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (recovering? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_below formula-decl nil finite_sets_below "finite_sets/")) nil nil nil nil)) (benign_TCC1 0 (benign_TCC1-1 nil 3264354197 nil ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved-complete ((N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (benign? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_below formula-decl nil finite_sets_below "finite_sets/")) nil nil nil nil)) (symmetric_TCC1 0 (symmetric_TCC1-1 nil 3264354197 nil ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved-complete ((N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (symmetric? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_below formula-decl nil finite_sets_below "finite_sets/")) nil nil nil nil)) (asymmetric_TCC1 0 (asymmetric_TCC1-1 nil 3264354197 nil ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved-complete ((N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (asymmetric? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_below formula-decl nil finite_sets_below "finite_sets/")) nil nil nil nil)) (good_TCC1 0 (good_TCC1-1 nil 3264354197 nil ("" (skosimp*) (("" (rewrite "finite_below") (("" (expand "good?") (("" (expand "empty?") (("" (expand "member") (("" (assert) (("" (typepred "status!1") (("" (skosimp) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (good? const-decl "bool" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_below formula-decl nil finite_sets_below "finite_sets/")) nil nil nil nil)) (no_asymmetric_subset 0 (no_asymmetric_subset-1 nil 3264354197 nil ("" (skosimp*) (("" (expand "no_asymmetric?") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (expand "subset?") (("" (inst?) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((below type-eq-decl nil nat_types nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (no_asymmetric? const-decl "bool" global_fault_model nil)) nil nil nil nil)) (hybrid_majority_exists_good 0 (hybrid_majority_exists_good-1 nil 3264354197 nil ("" (skosimp*) (("" (typepred "status!1") (("" (skosimp*) (("" (inst?) (("" (expand "good?") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((good? const-decl "bool" hybrid_fault_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" global_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil)) nil nil nil nil)) (hybrid_majority_good_subset 0 (hybrid_majority_good_subset-1 nil 3264354197 3264355015 ("" (skosimp*) (("" (expand "hybrid_majority_good?") (("" (case "FORALL (S: finite_set[below[N]]): card(intersection(H1!1, S)) <= card(intersection(H2!1, S))") (("1" (inst-cp - "asymmetric(status!1)") (("1" (inst - "symmetric(status!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2 -2) (("2" (skosimp*) (("2" (rewrite "card_subset[below[N]]") (("2" (hide 2) (("2" (expand "subset?") (("2" (skosimp*) (("2" (inst?) (("2" (expand "intersection") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((intersection const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (symmetric const-decl "finite_set[below(N)]" global_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (asymmetric const-decl "finite_set[below(N)]" global_fault_model nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (hybrid_majority_good? const-decl "bool" global_fault_model nil)) 5415 1530 t nil)) (card_good_votes 0 (card_good_votes-1 nil 3264354197 nil ("" (skosimp*) (("" (expand "good_votes") (("" (lemma "card_disj_union[below(N)]") (("" (inst?) (("1" (assert) (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil) ("2" (rewrite "finite_below") nil nil)) nil)) nil)) nil)) nil) proved-complete ((below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (card_disj_union formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (recovering const-decl "finite_set[below(N)]" global_fault_model nil) (intersection const-decl "set" sets nil) (below type-eq-decl nil nat_types nil) (trustworthy const-decl "non_empty_finite_set[below(N)]" global_fault_model nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (good_votes const-decl "finite_set[below(N)]" global_fault_model nil)) nil nil nil nil)) (card_hybrid_select 0 (card_hybrid_select-1 nil 3264354197 nil ("" (skosimp*) (("" (case-replace "H!1 = union(intersection(H!1, trustworthy(status!1)), union(intersection(H!1, recovering(status!1)), union(intersection(H!1, benign(status!1)), union(intersection(H!1, symmetric(status!1)), intersection(H!1, asymmetric(status!1))))))") (("1" (rewrite "card_disj_union[below(N)]") (("1" (rewrite "card_disj_union[below(N)]") (("1" (rewrite "card_disj_union[below(N)]") (("1" (rewrite "card_disj_union[below(N)]") (("1" (assert) nil nil) ("2" (hide 2 -1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "symmetric") (("2" (expand "asymmetric") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2 -1) (("3" (rewrite "finite_below[N]") nil nil)) nil) ("4" (hide 2 -1) (("4" (rewrite "finite_below[N]") nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "union") (("2" (expand "member") (("2" (expand "benign") (("2" (expand "symmetric") (("2" (expand "asymmetric") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2 -1) (("3" (rewrite "finite_below[N]") nil nil)) nil) ("4" (hide 2 -1) (("4" (rewrite "finite_below[N]") nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "union") (("2" (expand "member") (("2" (expand "recovering") (("2" (expand "benign") (("2" (expand "symmetric") (("2" (expand "asymmetric") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2 -1) (("3" (rewrite "finite_below[N]") nil nil)) nil) ("4" (hide 2 -1) (("4" (rewrite "finite_below[N]") nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "union") (("2" (expand "member") (("2" (expand "trustworthy") (("2" (expand "recovering") (("2" (expand "benign") (("2" (expand "symmetric") (("2" (expand "asymmetric") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2 -1) (("3" (rewrite "finite_below[N]") nil nil)) nil) ("4" (hide 2 -1) (("4" (rewrite "finite_below[N]") nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality + :hide? t) (("2" (expand "union") (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "trustworthy") (("2" (expand "recovering") (("2" (expand "benign") (("2" (expand "symmetric") (("2" (expand "asymmetric") (("2" (case "H!1(x!1)") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((card_disj_union formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (asymmetric const-decl "finite_set[below(N)]" global_fault_model nil) (symmetric const-decl "finite_set[below(N)]" global_fault_model nil) (benign const-decl "finite_set[below(N)]" global_fault_model nil) (recovering const-decl "finite_set[below(N)]" global_fault_model nil) (trustworthy const-decl "non_empty_finite_set[below(N)]" global_fault_model nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (intersection const-decl "set" sets nil) (union const-decl "set" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (no_trusted_benign 0 (no_trusted_benign-1 nil 3264354197 nil ("" (skosimp*) (("" (apply-extensionality + :hide? t) (("" (expand "intersection") (("" (expand "subset?") (("" (inst?) (("" (expand "complement") (("" (expand "member") (("" (expand "emptyset") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((member const-decl "bool" sets nil) (complement const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (intersection const-decl "set" sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (benign const-decl "finite_set[below(N)]" global_fault_model nil) (emptyset const-decl "set" sets nil) (below type-eq-decl nil nat_types nil) (N formal-const-decl "posnat" global_fault_model nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil nil nil nil)) (hybrid_majority_alt 0 (hybrid_majority_alt-1 nil 3264354197 nil ("" (skosimp*) (("" (lemma "card_hybrid_select") (("" (inst - "H!1" "_") (("" (inst?) (("" (replace -1 :hide? t) (("" (rewrite "card_good_votes") (("" (rewrite "no_trusted_benign") (("1" (rewrite "card_emptyset") (("1" (case "card(intersection(H!1, trustworthy(status!1))) <= card(trustworthy(status!1))") (("1" (expand "hybrid_majority_good?") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "card_subset[below(N)]") (("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "intersection") (("2" (expand "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "finite_below[N]") nil nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "hybrid_select?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" global_fault_model nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (no_trusted_benign formula-decl nil global_fault_model nil) (trustworthy const-decl "non_empty_finite_set[below(N)]" global_fault_model nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (intersection const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (hybrid_majority_good? const-decl "bool" global_fault_model nil) (card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (card_emptyset formula-decl nil finite_sets nil) (hybrid_select? const-decl "bool" global_fault_model nil) (card_good_votes formula-decl nil global_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (card_hybrid_select formula-decl nil global_fault_model nil)) nil nil nil nil)) (hybrid_majority 0 (hybrid_majority-1 nil 3264354197 nil ("" (skosimp*) (("" (lemma "card_hybrid_select") (("" (inst - "H!1" "_") (("" (inst?) (("" (replace -1 :hide? t) (("" (rewrite "card_good_votes") (("" (rewrite "no_trusted_benign") (("" (rewrite "card_emptyset") (("" (case "card(intersection(H!1, trustworthy(status!1))) <= card(trustworthy(status!1))") (("1" (expand "hybrid_majority_good?") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "card_subset[below(N)]") (("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "intersection") (("2" (expand "member") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "finite_below[N]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "posnat" global_fault_model nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (no_trusted_benign formula-decl nil global_fault_model nil) (trustworthy const-decl "non_empty_finite_set[below(N)]" global_fault_model nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (intersection const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (hybrid_majority_good? const-decl "bool" global_fault_model nil) (card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (card_emptyset formula-decl nil finite_sets nil) (card_good_votes formula-decl nil global_fault_model nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (card_hybrid_select formula-decl nil global_fault_model nil)) nil nil nil nil))) $$$message_quality.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : message_quality.pvs % % Purpose : declaration of predicates for messages % such as "good nodes send valid messages" % for use in various protocols, e.g. Interactive Consistency % or Diagnosis % % Assumptions : Parameter T is a NONEMPTY_TYPE % % Guarantees : None specified % % Design : SPIDER Version 0 % % Dependencies : global_fault_model, robus_data % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Alfons Geser % ICASE % 3 West Reid Street / MS 132 C % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-8003 % fax: 757-864-6134 % mailto: geser@icase.edu % http://www.icase.edu/~geser/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % February 19, 2002 - Added this header % March 11, 2002 - Added predicates conforms? and benign_source? % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% message_quality[N : posnat, T : NONEMPTY_TYPE] : THEORY BEGIN IMPORTING global_fault_model , robus_data[T] status : var node_status[N] rv_vect: var [below(N) -> robus_data[T]] vvec : var [below(N) -> T] G : var below(N) d : var robus_data[T] exp : var expected conforms?(d,exp) : bool = CASES exp OF valid_only : valid?(d) ELSE valid?(d) OR source_error?(d) ENDCASES receive_error_conforms_not: LEMMA NOT conforms?(d,exp) OR NOT receive_error?(d) good_message?(status,rv_vect,exp) : bool = FORALL G: good?(status(G)) => conforms?(rv_vect(G),exp) benign_message?(status,rv_vect) : bool = FORALL G: benign?(status(G)) => receive_error?(rv_vect(G)) benign_source?(status,rv_vect) : bool = FORALL G: benign?(status(G)) => source_error?(rv_vect(G)) END message_quality $$$message_quality.prf (|message_quality| (|receive_error_conforms_not| "" (SKOSIMP*) (("" (ASSERT) (("" (EXPAND "conforms?") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$Broadcast_Primitives.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : Broadcast_Primitives.pvs % % Purpose : Provides a model of the underlying broadcast % primitives in the ROBUS. Defines two functions for % the two types of brodcast that occur during an % interactive consistency exchange. % % Also provides justification for making accusations. % % Assumptions : Communication from benign-faulty nodes will be % detected by the receiver. This is modeled by % receive_error in type robus_data. receive_error is % not an actual message, but rather indicates the % absence of a `proper' message at the expected time. % % Guarantees : Accusations based upon receiver filters are valid. % % Design : SPIDER Version 0 % % Dependencies : This theory depends upon the following PVS theories % (and any of their dependencies): % % message_quality % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Paul S. Miner % 1 South Wright St. / MS 130 % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-6201 % fax: 757-864-4234 % mailto:p.s.miner@larc.nasa.gov % http://shemesh.larc.nasa.gov/~psm/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Notes % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % October 16, 2001 - Created this file using some definitions % extracted from % Spider_Interactive_Consistency. % March 6, 2002 - Added lemma l2r_validity. (Geser) % March 11, 2002 - Unified l2r and r2l to send; source_filter and % relay_filter to input_filter. Introduced % source_filter (with new meaning!). Moved % left2right and right2left to new theories % single_source_broadcast and % consistent_source_exchange, resp. Introduced % parameter exp to accomodate various filter % needs. (Geser) % March 22, 2002 - Cleaned up theory hierarchy. (Miner) % April 11, 2002 - Added the_send, a function that expresses % independence of the receiver for a % non-asymmetric transmitter. (Geser) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Broadcast_Primitives [ L : posnat % number of LEFTs , R : posnat % number of RIGHTs , T : NONEMPTY_TYPE % Broadcast is defined for any % message type ] : THEORY BEGIN IMPORTING message_quality[L,T] % for predicate conforms? left : var node_status[L] % global status vector for the LEFTs G, p, q: var below(L) r, s : var below(R) d: var robus_data[T] v: var T sym_send(p,d) : robus_data[T] % Uninterpreted function to model % broadcast of an arbitrary % value by a symmetrically faulty % LEFT asym_send(p, d, r) : robus_data[T] % Uninterpreted function to % model asymmetric, but unknown, % transmission by an % asymmetrically faulty LEFT send(left)(p, d, r) : robus_data[T] = CASES left(p) OF trustworthy : d, recovering : d, benign : receive_error, symmetric : sym_send(p, d), asymmetric : asym_send(p, d, r) ENDCASES send_agreement : LEMMA not asymmetric?(left(p)) => send(left)(p, d, r) = send(left)(p, d, s) send_validity: LEMMA good?(left(p)) => send(left)(p, d, r) = d the_send_welldefined: LEMMA NOT asymmetric?(left(p)) => singleton?({newd: robus_data[T] | EXISTS r: newd = send(left)(p, d, r)}) the_send(left)(p| NOT asymmetric?(left(p)), d) : robus_data[T] = the({newd: robus_data[T] | EXISTS r: newd = send(left)(p, d, r)}) the_send_agreement: LEMMA NOT asymmetric?(left(p)) => send(left)(p, d, r) = the_send(left)(p, d) exp: var expected input_filter(d,exp) : robus_data[T] = IF conforms?(d,exp) THEN d ELSE receive_error ENDIF d_vect : var [below(L) -> robus_data[T]] input_filter_validity: LEMMA good_message?(left,d_vect,exp) & good?(left(p)) => input_filter(d_vect(p),exp) = d_vect(p) source_filter(d) : robus_data[T] = CASES d OF receive_error : source_error ELSE d ENDCASES source_filter_not_receive_error: LEMMA not receive_error?(source_filter(d)) END Broadcast_Primitives $$$Broadcast_Primitives.prf (|Broadcast_Primitives| (|send_agreement| "" (SKOSIMP*) (("" (EXPAND "send") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|send_validity| "" (SKOSIMP*) (("" (EXPAND "send") (("" (LIFT-IF) (("" (EXPAND "good?") (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|the_send_welldefined| "" (SKOSIMP*) (("" (EXPAND "singleton?") (("" (INST + "send(left!1)(p!1, d!1, 0)") (("1" (SKOSIMP*) (("1" (TYPEPRED "y!1") (("1" (SKOSIMP*) (("1" (REPLACE -1 :HIDE? T) (("1" (REWRITE "send_agreement") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|the_send_TCC1| "" (SKOSIMP*) (("" (REWRITE "the_send_welldefined") NIL NIL)) NIL) (|the_send_agreement| "" (SKOSIMP*) (("" (EXPAND "the_send") (("" (EXPAND "the") (("" (USE "epsilon_ax[robus_data[T]]") (("" (PROP) (("1" (SKOSIMP*) (("1" (REPLACE -1 :HIDE? T) (("1" (REWRITE "send_agreement") NIL NIL)) NIL)) NIL) ("2" (HIDE 3) (("2" (INST + "send(left!1)(p!1, d!1, 0)") (("2" (INST + "0") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|input_filter_validity| "" (SKOSIMP*) (("" (EXPAND "input_filter") (("" (LIFT-IF) (("" (PROP) (("" (EXPAND "good_message?") (("" (INST?) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|source_filter_not_receive_error| "" (SKOSIMP*) (("" (EXPAND "source_filter") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$single_source_broadcast.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : single_source_broadcast.pvs % % Purpose : A message exchange protocol where oine LEFT node % broadcasts to all RIGHT nodes. This protocol is % used as part of the Interactive Consistency protocol. % % Design : SPIDER Version 0 % % Dependencies : Broadcast_Primitives % % PVS : Version 2.3 (patch level 1.2.2.36) % Allegro CL Professional Edition % 5.0 [SPARC] (9/4/99 13:56) % % Author : Alfons Geser % ICASE % 3 West Reid Street / MS 132 C % NASA Langley Research Center % Hampton, VA 23681-2199 % phone: 757-864-8003 % fax: 757-864-6134 % mailto: geser@icase.edu % http://www.icase.edu/~geser/ % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Revision History % March 11, 2001 - Replaces material in theory % Spider_Interactive_Consistency. New % parameter exp indicates which format good LEFTs % may use. % March 22, 2002 - Cleaned up theory hierarchy. (Miner) % April 11, 2002 - Added the_source_data, a function that expresses % independence of the receiver in the case of a % non-asymmetric transmitter. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% single_source_broadcast [ L : posnat % number of LEFTs , R : posnat % number of RIGHTs , T : NONEMPTY_TYPE % Protocol is correct for any % message type ] : THEORY BEGIN IMPORTING Broadcast_Primitives[L,R,T] % Communication primitives left : var node_status[L] G : var below(L) r, s : var below(R) d : var robus_data[T] source_data(left)(d)(G)(r) : robus_data[T] = source_filter(input_filter(send(left)(G,d,r),valid_only)) source_data_agreement: LEMMA NOT asymmetric?(left(G)) => source_data(left)(d)(G)(r) = source_data(left)(d)(G)(s) source_data_validity: LEMMA valid?(d) & good?(left(G)) => source_data(left)(d)(G)(r) = d source_data_source_error: LEMMA benign?(left(G)) => source_error?(source_data(left)(d)(G)(r)) source_data_valid_or_source_error: LEMMA valid?(source_data(left)(d)(G)(r)) OR source_error?(source_data(left)(d)(G)(r)) the_source_data(left)(d)(G| NOT asymmetric?(left(G))) : robus_data[T] = source_filter(input_filter(the_send(left)(G,d),valid_only)) the_source_data_agreement: LEMMA NOT asymmetric?(left(G)) => source_data(left)(d)(G)(r) = the_source_data(left)(d)(G) good_the_source_data: LEMMA valid?(d) & good?(left(G)) => the_source_data(left)(d)(G) = d benign_the_source_data: LEMMA valid?(d) & benign?(left(G)) => the_source_data(left)(d)(G) = source_error symmetric_the_source_data: LEMMA valid?(d) & symmetric?(left(G)) => the_source_data(left)(d)(G) = sym_send(G, d) OR the_source_data(left)(d)(G) = source_error the_source_data_valid_or_source_error: LEMMA NOT asymmetric?(left(G)) => valid?(the_source_data(left)(d)(G)) OR source_error?(the_source_data(left)(d)(G)) END single_source_broadcast $$$single_source_broadcast.prf (|single_source_broadcast| (|source_data_agreement| "" (SKOSIMP*) (("" (EXPAND "source_data") (("" (EXPAND "send") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|source_data_validity| "" (SKOSIMP*) (("" (EXPAND "source_data") (("" (REWRITE "send_validity") (("" (EXPAND "input_filter") (("" (EXPAND "conforms?") (("" (ASSERT) (("" (EXPAND "source_filter") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|source_data_source_error| "" (SKOSIMP*) (("" (EXPAND "source_data") (("" (EXPAND "send") (("" (ASSERT) (("" (EXPAND "input_filter") (("" (EXPAND "source_filter") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|source_data_valid_or_source_error| "" (SKOSIMP*) (("" (EXPAND "source_data") (("" (EXPAND "input_filter") (("" (EXPAND "conforms?") (("" (EXPAND "source_filter") (("" (LIFT-IF) (("" (ASSERT) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|the_source_data_agreement| "" (SKOSIMP*) (("" (EXPAND "the_source_data") (("" (EXPAND "source_data") (("" (REWRITE "congruence") (("" (REWRITE "congruence") (("" (REWRITE "the_send_agreement") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|good_the_source_data_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|good_the_source_data| "" (SKOSIMP*) (("" (LEMMA "the_source_data_agreement") (("" (INST - "_" "_" "_" "0") (("1" (INST?) (("1" (PROP) (("1" (REWRITE "source_data_validity") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "good?") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|benign_the_source_data_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|benign_the_source_data| "" (SKOSIMP*) (("" (LEMMA "the_source_data_agreement") (("" (INST - "_" "_" "_" "0") (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "source_data") (("1" (EXPAND "send") (("1" (EXPAND "input_filter") (("1" (EXPAND "source_filter") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|symmetric_the_source_data_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|symmetric_the_source_data| "" (SKOSIMP*) (("" (LEMMA "the_source_data_agreement") (("" (INST - "_" "_" "_" "0") (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "source_data") (("1" (EXPAND "send") (("1" (EXPAND "input_filter") (("1" (EXPAND "source_filter") (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|the_source_data_valid_or_source_error| "" (SKOSIMP*) (("" (LEMMA "the_source_data_agreement") (("" (INST - "_" "_" "_" "0") (("1" (INST?) (("1" (PROP) (("1" (REPLACE -1 :DIR RL :HIDE? T) (("1" (USE "source_data_valid_or_source_error") (("1" (PROP) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$ROBUS_IC_Protocol.pvs % NASA LaRC Formal Methods Grou % PVS 3.1 ROBUS_IC_Protocol [ B : posnat, % number of BIUs R : posnat, % number of RMUs T : NONEMPTY_TYPE % arbitrary message type ]: THEORY BEGIN IMPORTING single_source_broadcast[B,R,T], consistent_source_exchange[R,B,T], local_state[B,R] ls, new_ls : VAR Local_State_Type % contains an algamation of all local state % information b_status : VAR node_status[B] % fault status of a BIU r_status : VAR node_status[R] % fault status of an RMU G, p, q : VAR below(B) % G is the general; p, q are arbitrary BIUs r, s : VAR below(R) % arbitrary RMUs msg: VAR T % arbitrary message trust, trust1, trust2 : VAR trust % trust levels (of trusted, accused, and declared) F_r, F_r1, F_r2 : VAR Active_Vector_Type[R] % eligible sets of RMUs elim_ic_relays(b_status, r_status, F_r)(G, msg, p) : Active_Vector_Type[R] = elim_csx_relays(r_status, source_data(b_status)(valid(msg))(G), F_r, valid_or_source_error)(p) robus_ic(b_status, r_status, trust, F_r)(G, msg, p) : robus_data[T] = IF declared?(trust) THEN source_error ELSE spider_csx(r_status, source_data(b_status)(valid(msg))(G), F_r, valid_or_source_error)(p) ENDIF elim_ic_relays_preseves_trust : LEMMA member(r, trusted(elim_ic_relays(b_status, r_status, F_r)(G, msg, p))) => member(r, trusted(F_r)) elim_ic_relays_expand_hybrid_majority_good? : LEMMA hybrid_majority_good?(r_status, trusted(F_r)) => hybrid_majority_good?(r_status, trusted(elim_ic_relays(b_status, r_status, F_r) (G, msg, p))) MFA_Agreement: LEMMA good_trusting?(r_status, F_r1) & good_trusting?(r_status, F_r2) & symmetric_agreement?(r_status, F_r1, F_r2) & declared?(trust1) = declared?(trust2) & (no_asymmetric?(r_status, trusted(F_r1)) & no_asymmetric?(r_status, trusted(F_r2)) OR declared?(trust1) OR NOT asymmetric?(b_status(G)) & hybrid_majority_good?(r_status, trusted(elim_ic_relays(b_status, r_status, F_r1) (G, msg, p))) & hybrid_majority_good?(r_status, trusted(elim_ic_relays(b_status, r_status, F_r2) (G, msg, q)))) => robus_ic(b_status, r_status, trust1, F_r1)(G, msg, p) = robus_ic(b_status, r_status, trust2, F_r2)(G, msg, q) END ROBUS_IC_Protocol $$$ROBUS_IC_Protocol.prf (ROBUS_IC_Protocol (elim_ic_relays_preseves_trust 0 (elim_ic_relays_preseves_trust-3 nil 3299517854 3300806999 ("" (skosimp*) (("" (expand "member") (("" (expand "trusted") (("" (expand "elim_ic_relays") (("" (expand "elim_csx_relays") (("" (expand "elim_relays") (("" (expand "merge_active") (("" (expand "merge_trusts") (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((member const-decl "bool" sets nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (merge_trusts const-decl "trust" hybrid_fault_types nil) (merge_active const-decl "Active_Vector_Type" local_fault_model nil) (elim_csx_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil)) 209 140 nil nil) (elim_ic_relays_preseves_trust-2 nil 3299517747 3299517751 ("" (skosimp*) (("" (expand "member") (("" (expand "trusted") (("" (expand "elim_ic_relays") (("" (expand "elim_csx_relays") (("" (expand "elim_relays") (("" (expand "merge_active") (("" (expand "merge_trusts") (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((trusted const-decl "finite_set[below(N)]" local_fault_model nil) (elim_csx_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (merge_active const-decl "Active_Vector_Type" local_fault_model nil) (merge_trusts const-decl "trust" hybrid_fault_types nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (member const-decl "bool" sets nil)) 2252 130 nil nil) (elim_ic_relays_preseves_trust-1 nil 3264264614 3297518434 ("" (skosimp*) (("" (expand "member") (("" (expand "trusted") (("" (expand "elim_ic_relays") (("" (expand "elim_csx_relays") (("" (expand "elim_relays") (("" (expand "merge_active") (("" (expand "merge_trusts") (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((member const-decl "bool" sets nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (elim_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (merge_trusts const-decl "trust" hybrid_fault_types nil) (merge_active const-decl "Active_Vector_Type" local_fault_model nil) (elim_csx_relays const-decl "Active_Vector_Type[L]" consistent_source_exchange nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil)) 150 110 t shostak)) (elim_ic_relays_expand_hybrid_majority_good? 0 (elim_ic_relays_expand_hybrid_majority_good?-6 nil 3297518461 3300806999 ("" (lemma "elim_ic_relays_preseves_trust") (("" (lemma "hybrid_majority_good_subset") (("" (skosimp*) (("" (expand "subset?") (("" (inst -1 _ _ "r_status!1") (("" (inst -1 _ "trusted(F_r!1)") (("" (inst -1 "trusted(elim_ic_relays(b_status!1, r_status!1, F_r!1)(G!1, msg!1, p!1))") (("" (inst? -2) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((R formal-const-decl "posnat" ROBUS_IC_Protocol nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (subset? const-decl "bool" sets nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (trust type-decl nil hybrid_fault_types nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (B formal-const-decl "posnat" ROBUS_IC_Protocol nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (elim_ic_relays_preseves_trust formula-decl nil ROBUS_IC_Protocol nil)) 439 90 nil nil) (elim_ic_relays_expand_hybrid_majority_good?-5 nil 3297504603 3297518434 ("" (lemma "elim_ic_relays_preseves_trust") (("" (lemma "hybrid_majority_good_subset") (("" (skosimp*) (("" (expand "subset?") (("" (inst -1 _ _ "r_status!1") (("" (inst -1 _ "trusted(E_r!1)") (("" (inst -1 "trusted(elim_ic_relays(b_status!1, r_status!1, E_r!1)(G!1, msg!1, p!1))") (("" (inst? -2) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((R formal-const-decl "posnat" ROBUS_IC_Protocol nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (subset? const-decl "bool" sets nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (trust type-decl nil hybrid_fault_types nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (B formal-const-decl "posnat" ROBUS_IC_Protocol nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (elim_ic_relays_preseves_trust formula-decl nil ROBUS_IC_Protocol nil)) 136 90 t nil) (elim_ic_relays_expand_hybrid_majority_good?-4 nil 3297503964 3297504577 ("" (lemma "elim_ic_relays_preseves_trust") (("" (lemma "hybrid_majority_good_subset") (("" (skosimp*) (("" (expand "subset?") (("" (inst -1 _ _ "r_status!1") (("" (inst -1 _ "trusted(act_r!1)") (("" (inst -1 "trusted(elim_ic_relays(b_status!1, r_status!1, act_r!1)(G!1, msg!1, p!1))") (("" (inst? -2) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((elim_ic_relays_preseves_trust formula-decl nil ROBUS_IC_Protocol nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (B formal-const-decl "posnat" ROBUS_IC_Protocol nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (subset? const-decl "bool" sets nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (R formal-const-decl "posnat" ROBUS_IC_Protocol nil)) 113 80 nil nil) (elim_ic_relays_expand_hybrid_majority_good?-3 nil 3297503754 3297503940 ("" (lemma "elim_ic_relays_preseves_trust") (("" (lemma "hybrid_majority_good_subset") (("" (skosimp*) (("" (expand "subset?") (("" (inst -1 _ _ "r_status!1") (("" (inst -1 _ "trusted(act_r!1)") (("" (inst -1 "trusted(elim_ic_relays(b_status!1, r_status!1, act_r!1)(G!1, v!1, p!1))") (("" (inst? -2) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((elim_ic_relays_preseves_trust formula-decl nil ROBUS_IC_Protocol nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (B formal-const-decl "posnat" ROBUS_IC_Protocol nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (below type-eq-decl nil nat_types nil) (subset? const-decl "bool" sets nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (R formal-const-decl "posnat" ROBUS_IC_Protocol nil)) 144 100 nil nil) (elim_ic_relays_expand_hybrid_majority_good?-2 nil 3297503719 3297503741 ("" (lemma "elim_ic_relays_preseves_trust") (("" (lemma "hybrid_majority_good_subset") (("" (skosimp*) (("" (expand "subset?") (("" (inst -1 _ _ "right!1") (("" (inst -1 _ "trusted(act_r!1)") (("" (inst -1 "trusted(elim_ic_relays(b_status!1, r_status!1, act_r!1)(G!1, v!1, p!1))") (("" (inst? -2) (("" (ground) nil)))))))))))))))) nil) unfinished nil 20827 330 t nil) (elim_ic_relays_expand_hybrid_majority_good?-1 nil 3264266615 3297503687 ("" (lemma "elim_ic_relays_preseves_trust") (("" (lemma "hybrid_majority_good_subset") (("" (skosimp*) (("" (expand "subset?") (("" (inst -1 _ _ "right!1") (("" (inst -1 _ "trusted(act_r!1)") (("" (inst -1 "trusted(elim_ic_relays(left!1, right!1, act_r!1)(G!1, v!1, p!1))") (("" (inst? -2) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((R formal-const-decl "posnat" ROBUS_IC_Protocol nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (hybrid_majority_good_subset formula-decl nil global_fault_model nil) (subset? const-decl "bool" sets nil) (below type-eq-decl nil nat_types nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (trust type-decl nil hybrid_fault_types nil) (trusted const-decl "finite_set[below(N)]" local_fault_model nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (elim_ic_relays_preseves_trust formula-decl nil ROBUS_IC_Protocol nil)) 132 100 t shostak)) (MFA_Agreement 0 (MFA_Agreement-2 nil 3299596081 3300807504 ("" (skosimp*) (("" (expand "robus_ic") (("" (replace*) (("" (lift-if) (("" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (replace*) (("2" (prop) (("1" (use "csx_agreement_generation") (("1" (prop) nil nil)) nil) ("2" (expand "elim_ic_relays") (("2" (lemma "csx_agreement_propagation") (("2" (inst?) (("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (assert) (("4" (expand "good_message?") (("4" (skosimp*) (("4" (expand "conforms?") (("4" (use "source_data_valid_or_source_error") nil nil)) nil)) nil)) nil)) nil) ("5" (expand "good_vote_same?") (("5" (skosimp*) (("5" (rewrite "source_data_agreement") nil nil)) nil)) nil) ("6" (propax) nil nil) ("7" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((robus_ic const-decl "robus_data[T]" ROBUS_IC_Protocol nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (trust type-decl nil hybrid_fault_types nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (robus_data type-decl nil robus_data_adt nil) (fault_classification type-decl nil hybrid_fault_types nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (node_status type-eq-decl nil global_fault_model nil) (source_data const-decl "robus_data[T]" single_source_broadcast nil) (valid? adt-recognizer-decl "[robus_data -> boolean]" robus_data_adt nil) (valid adt-constructor-decl "[T -> (valid?)]" robus_data_adt nil) (expected type-decl nil hybrid_fault_types nil) (valid_or_source_error? adt-recognizer-decl "[expected -> boolean]" hybrid_fault_types nil) (valid_or_source_error adt-constructor-decl "(valid_or_source_error?)" hybrid_fault_types nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (B formal-const-decl "posnat" ROBUS_IC_Protocol nil) (R formal-const-decl "posnat" ROBUS_IC_Protocol nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (csx_agreement_generation formula-decl nil consistent_source_exchange nil) (csx_agreement_propagation formula-decl nil consistent_source_exchange nil) (good_message? const-decl "bool" message_quality nil) (conforms? const-decl "bool" message_quality nil) (source_data_valid_or_source_error formula-decl nil single_source_broadcast nil) (source_data_agreement formula-decl nil single_source_broadcast nil) (below type-eq-decl nil nat_types nil) (good_vote_same? const-decl "bool" good_selective_majority nil) (elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil)) 26459 4950 t nil) (MFA_Agreement-1 nil 3299517803 3299517809 ("" (skosimp*) (("" (expand "spider_hom") (("" (replace*) (("" (lift-if) (("" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (replace*) (("2" (prop) (("1" (use "csx_agreement_generation") (("1" (prop) nil nil)) nil) ("2" (expand "elim_ic_relays") (("2" (lemma "csx_agreement_propagation") (("2" (inst?) (("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (assert) (("4" (expand "good_message?") (("4" (skosimp*) (("4" (expand "conforms?") (("4" (use "source_data_valid_or_source_error") nil nil)) nil)) nil)) nil)) nil) ("5" (expand "good_vote_same?") (("5" (skosimp*) (("5" (rewrite "source_data_agreement") nil nil)) nil)) nil) ("6" (propax) nil nil) ("7" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((elim_ic_relays const-decl "Active_Vector_Type[R]" ROBUS_IC_Protocol nil) (good_vote_same? const-decl "bool" good_selective_majority nil) (below type-eq-decl nil nat_types nil) (source_data_agreement formula-decl nil single_source_broadcast nil) (source_data_valid_or_source_error formula-decl nil single_source_broadcast nil) (conforms? const-decl "bool" message_quality nil) (good_message? const-decl "bool" message_quality nil) (csx_agreement_propagation formula-decl nil consistent_source_exchange nil) (csx_agreement_generation formula-decl nil consistent_source_exchange nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (R formal-const-decl "posnat" ROBUS_IC_Protocol nil) (B formal-const-decl "posnat" ROBUS_IC_Protocol nil) (T formal-nonempty-type-decl nil ROBUS_IC_Protocol nil) (valid_or_source_error adt-constructor-decl "(valid_or_source_error?)" hybrid_fault_types nil) (valid_or_source_error? adt-recognizer-decl "[expected -> boolean]" hybrid_fault_types nil) (expected type-decl nil hybrid_fault_types nil) (valid adt-constructor-decl "[T -> (valid?)]" robus_data_adt nil) (valid? adt-recognizer-decl "[robus_data -> boolean]" robus_data_adt nil) (source_data const-decl "robus_data[T]" single_source_broadcast nil) (node_status type-eq-decl nil global_fault_model nil) (trustworthy? adt-recognizer-decl "[fault_classification -> boolean]" hybrid_fault_types nil) (fault_classification type-decl nil hybrid_fault_types nil) (robus_data type-decl nil robus_data_adt nil) (Active_Vector_Type nonempty-type-eq-decl nil local_fault_model nil) (trust type-decl nil hybrid_fault_types nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 4394 400 nil nil)))