%% 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 (leepike @ galois.com) % 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" real