%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46) $$$top.pvs % --------------------------------------------------------------------------- % % Fault Assumptions for the Guardian in the Time-Triggered Architecture (TTA) % % accompanying paper available at % http://www.informatik.uni-ulm.de/ki/Pfeifer/safecomp2004.html % % Author: % Dr. Holger Pfeifer Tel.: (+49) 731 / 502-4124 % Universitaet Ulm Fax: (+49) 731 / 502-4119 % Abt. Kuenstliche Intelligenz pfeifer@ki.informatik.uni-ulm.de % D-89069 Ulm http://www.informatik.uni-ulm.de/ki/pfeifer.html % % Copyright (c) 2004, Holger Pfeifer % % --------------------------------------------------------------------------- top : THEORY BEGIN IMPORTING strong_fault_hypothesis, guardian END top $$$guardian.pvs guardian : THEORY BEGIN IMPORTING faultmodel_defs, frame t : VAR Slot p,q : VAR Proc c : VAR Channel d : VAR {rt:realtime | rt >= 0} f : VAR Frame sent(t,c,p) : Frame IMPORTING sending_defs[sent], window_timing_defs nonfaulty_sender : AXIOM p = sender(t) AND nonfaulty(t,p) => (FORALL c: sends_correct(t,c,p)) OR (FORALL c: NOT sends(t,c,p)) nonfaulty_not_sender_not_sends : AXIOM p /= sender(t) AND nonfaulty(t,p) => NOT sends(t,c,p) nonfaulty_sender_sendingtime : COROLLARY p = sender(t) AND nonfaulty(t,p) AND sends(t,c,p) => sending_time_OK(t,sent(t,c,p),p) % --------------------------------------------------------------------------- Guardian : TYPE+ grd : VAR Guardian faulty(t,grd) : bool nonfaulty(t,grd) : bool = NOT faulty(t,grd) g : [Channel -> Guardian] relay(t,grd,p) : Frame relay_only_from_specific_node : AXIOM sends(t,c,q) AND relay(t,g(c),p) = sent(t,c,q) => p = q guardian_passive : AXIOM relay(t,g(c),p) /= null => sends(t,c,p) nonfaulty_guardian_relay : AXIOM p = sender(t) AND nonfaulty(t,g(c)) AND sends_correct(t,c,p) => relay(t,g(c),p) = sent(t,c,p) nonfaulty_guardian_block : AXIOM p /= sender(t) AND nonfaulty(t,g(c)) => relay(t,g(c),p) = null nonfaulty_guardian_invalid_sending_time : AXIOM p = sender(t) AND nonfaulty(t,g(c)) AND NOT sending_time_OK(t,sent(t,c,p),p) => relay(t,g(c),p) = null nonfaulty_guardian_invalid_phys_encoding : AXIOM p = sender(t) AND nonfaulty(t,g(c)) AND NOT phys_encoding_OK(sent(t,c,p)) => corrupted(relay(t,g(c),p)) nonfaulty_guardian_invalid_cstate_encoding : AXIOM p = sender(t) AND nonfaulty(t,g(c)) AND NOT cstate_encoding_OK(t,sent(t,c,p),p) => corrupted(relay(t,g(c),p)) nonfaulty_guardian_exists : AXIOM EXISTS c: nonfaulty(t,g(c)) faulty_guardian_fail_silence : AXIOM faulty(t,g(c)) => relay(t,g(c),p) = null nonfaulty_guardian_max_delay : AXIOM nonfaulty(t,g(c)) AND sends(t,c,p) AND relay(t,g(c),p) /= null => EXISTS d: d <= max_broadcast_delay AND delivery_time(relay(t,g(c),p)) = transmission_time(sent(t,c,p)) + d simultaneous_access(t,c) : bool = FALSE nonfaulty(t,c) : bool = nonfaulty(t,g(c)) % --------------------------------------------------------------------------- broadcast(t,c) : Frame = epsilon! f: EXISTS p: relay(t,g(c),p) = f AND FORALL q: q /= p => relay(t,g(c),q) = null % --------------------------------------------------------------------------- % -- the following propositions correspond to the assumptions of the theory % imported below nonfaulty_channel_broadcast : PROPOSITION nonfaulty(t,c) => broadcast(t,c) = sent(t,c,sender(t)) OR broadcast(t,c) = null OR corrupted(broadcast(t,c)) nonfaulty_channel_broadcast_sender : PROPOSITION nonfaulty(t,c) AND sends_correct(t,c,p) AND p = sender(t) => broadcast(t,c) = sent(t,c,p) channel_broadcast_only_if_sent : PROPOSITION broadcast(t,c) /= null => EXISTS p: sends(t,c,p) nonfaulty_channel_max_delay : PROPOSITION nonfaulty(t,c) AND p = sender(t) AND sends_correct(t,c,p) => EXISTS d: d <= max_broadcast_delay AND delivery_time(broadcast(t,c)) = transmission_time(sent(t,c,p)) + d nonfaulty_channel_broadcast_cstate_encoding : PROPOSITION nonfaulty(t,c) AND sends(t,c,p) AND broadcast(t,c) = sent(t,c,p) AND phys_encoding_OK(broadcast(t,c)) => cstate_encoding_OK(t,sent(t,c,p),p) nonfaulty_channel_correct_cstate_sender_only : PROPOSITION nonfaulty(t,c) AND sends_correct(t,c,p) AND broadcast(t,c) = sent(t,c,p) AND cstate_encoding_OK(t,sent(t,c,p),p) => p = sender(t) no_simultaneous_access : PROPOSITION EXISTS c: nonfaulty(t,c) AND NOT simultaneous_access(t,c) IMPORTING ttpc[sent,broadcast,simultaneous_access,nonfaulty] END guardian $$$guardian.prf (guardian (nonfaulty_sender_sendingtime 0 (nonfaulty_sender_sendingtime-1 nil 3294740566 3295507318 ("" (skosimp*) (("" (use "nonfaulty_sender") (("" (ground) (("1" (inst?) (("1" (expand "sends_correct") (("1" (propax) nil nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil) unchecked ((nonfaulty_sender formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil)) 86 40 t shostak)) (nonfaulty_channel_broadcast 0 (nonfaulty_channel_broadcast-1 nil 3294741631 3295507319 ("" (skosimp*) (("" (expand "broadcast") (("" (use "epsilon_ax[Frame]") (("" (ground) (("1" (skosimp*) (("1" (replace -1 :dir rl :hide? t) (("1" (case "p!1 = sender(t!1)") (("1" (use "nonfaulty_guardian_relay") (("1" (ground) (("1" (expand "nonfaulty") (("1" (expand "nonfaulty") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "sends_correct") (("2" (prop) (("1" (use "guardian_passive") (("1" (ground) nil nil)) nil) ("2" (use "nonfaulty_guardian_invalid_sending_time") (("2" (ground) (("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (use "nonfaulty_guardian_invalid_phys_encoding") (("3" (ground) (("3" (expand "nonfaulty") (("3" (expand "nonfaulty") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("4" (use "nonfaulty_guardian_invalid_cstate_encoding") (("4" (ground) (("4" (expand "nonfaulty") (("4" (expand "nonfaulty") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_guardian_block") (("2" (ground) (("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 4 5) (("2" (inst + "relay(t!1,g(c!1),sender(t!1))") (("2" (inst?) (("2" (skosimp*) (("2" (use "nonfaulty_guardian_block") (("2" (ground) (("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((broadcast const-decl "Frame" guardian nil) (nonfaulty_guardian_block formula-decl nil guardian nil) (nonfaulty_guardian_relay formula-decl nil guardian nil) (sends_correct const-decl "bool" sending_defs nil) (nonfaulty_guardian_invalid_cstate_encoding formula-decl nil guardian nil) (nonfaulty_guardian_invalid_phys_encoding formula-decl nil guardian nil) (nonfaulty_guardian_invalid_sending_time formula-decl nil guardian nil) (guardian_passive formula-decl nil guardian nil) nil nil (sender const-decl "Proc" types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (Proc nonempty-type-decl nil types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (Slot nonempty-type-eq-decl nil types nil) (Guardian nonempty-type-decl nil guardian nil) (relay const-decl "Frame" guardian nil) (Channel nonempty-type-decl nil types nil) (g const-decl "[Channel -> Guardian]" guardian nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (null const-decl "Frame" frame nil) (Frame nonempty-type-decl nil frame nil) (epsilon_ax formula-decl nil epsilons nil)) 331 230 t shostak)) (nonfaulty_channel_broadcast_sender 0 (nonfaulty_channel_broadcast_sender-1 nil 3255717879 3295507319 ("" (skosimp*) (("" (use "nonfaulty_guardian_relay") (("" (ground) (("1" (expand "broadcast") (("1" (use "epsilon_ax[Frame]") (("1" (ground) (("1" (skosimp*) (("1" (replace -1 :dir rl :hide? t) (("1" (expand "sends_correct") (("1" (flatten) (("1" (inst?) (("1" (ground) (("1" (expand "sends") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (ground) (("2" (skosimp*) (("2" (use "nonfaulty_guardian_block") (("2" (ground) (("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((nonfaulty_guardian_relay formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (broadcast const-decl "Frame" guardian nil) (sends const-decl "bool" sending_defs nil) (sends_correct const-decl "bool" sending_defs nil) (nonfaulty_guardian_block formula-decl nil guardian nil) nil nil (sent const-decl "Frame" guardian nil) (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Guardian nonempty-type-decl nil guardian nil) (relay const-decl "Frame" guardian nil) (g const-decl "[Channel -> Guardian]" guardian nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (null const-decl "Frame" frame nil) (epsilon_ax formula-decl nil epsilons nil) (Frame nonempty-type-decl nil frame nil)) 126 110 t shostak)) (channel_broadcast_only_if_sent 0 (channel_broadcast_only_if_sent-1 nil 3255717900 3295507319 ("" (skosimp*) (("" (expand "broadcast") (("" (use "epsilon_ax[Frame]") (("" (ground) (("1" (skosimp*) (("1" (replace -1 :dir rl :hide? t) (("1" (use "guardian_passive") (("1" (ground) (("1" (inst?) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst? :subst ("x" "relay(t!1,g(c!1),sender(t!1))")) (("2" (inst?) (("2" (skosimp*) (("2" (use "nonfaulty_guardian_block") (("2" (ground) (("2" (expand "nonfaulty") (("2" (use "faulty_guardian_fail_silence") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((broadcast const-decl "Frame" guardian nil) (guardian_passive formula-decl nil guardian nil) (nonfaulty_guardian_block formula-decl nil guardian nil) nil (faulty_guardian_fail_silence formula-decl nil guardian nil) (sender const-decl "Proc" types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (Proc nonempty-type-decl nil types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (Slot nonempty-type-eq-decl nil types nil) (Guardian nonempty-type-decl nil guardian nil) (relay const-decl "Frame" guardian nil) (Channel nonempty-type-decl nil types nil) (g const-decl "[Channel -> Guardian]" guardian nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (null const-decl "Frame" frame nil) (Frame nonempty-type-decl nil frame nil) (epsilon_ax formula-decl nil epsilons nil)) 121 90 t shostak)) (nonfaulty_channel_max_delay 0 (nonfaulty_channel_max_delay-1 nil 3294905700 3295507319 ("" (skosimp*) (("" (use "nonfaulty_guardian_max_delay") (("" (use "nonfaulty_guardian_relay") (("" (use "nonfaulty_channel_broadcast_sender") (("" (expand "nonfaulty") (("" (expand "nonfaulty") (("" (expand "sends") (("" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "sends_correct") (("2" (expand "sends") (("2" (propax) nil nil)) nil)) nil) ("3" (expand "sends_correct") (("3" (expand "sends") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((nonfaulty_guardian_max_delay formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (nonfaulty_channel_broadcast_sender formula-decl nil guardian nil) (realtime nonempty-type-eq-decl nil time nil) (sends_correct const-decl "bool" sending_defs nil) (sends const-decl "bool" sending_defs nil) nil nil (nonfaulty_guardian_relay formula-decl nil guardian nil)) 175 120 t shostak)) (nonfaulty_channel_broadcast_cstate_encoding 0 (nonfaulty_channel_broadcast_cstate_encoding-1 nil 3295507427 3295508739 ("" (skosimp*) (("" (expand "broadcast") (("" (use "epsilon_ax[Frame]") (("" (ground) (("1" (skosimp*) (("1" (replace -1 :dir rl :hide? t) (("1" (inst? :subst ("q_1" "p!1")) (("1" (ground) (("1" (use "relay_only_from_specific_node") (("1" (expand "sends") (("1" (ground) nil nil)) nil)) nil) ("2" (replace*) (("2" (use "nonfaulty_guardian_invalid_cstate_encoding") (("2" (ground) (("1" (use "corrupted_is_not_OK") (("1" (ground) nil nil)) nil) ("2" (use "nonfaulty_guardian_block") (("2" (ground) (("1" (expand "sends") (("1" (ground) nil nil)) nil) ("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "nonfaulty") (("3" (expand "nonfaulty") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst? :subst ("x" "relay(t!1,g(c!1),sender(t!1))" "p" "sender(t!1)")) (("2" (skosimp*) (("2" (use "nonfaulty_guardian_block") (("2" (ground) (("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((epsilon_ax formula-decl nil epsilons nil) (Frame nonempty-type-decl nil frame nil) (null const-decl "Frame" frame nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (g const-decl "[Channel -> Guardian]" guardian nil) (Channel nonempty-type-decl nil types nil) (relay const-decl "Frame" guardian nil) (Guardian nonempty-type-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Proc nonempty-type-decl nil types nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sender const-decl "Proc" types nil) (sent const-decl "Frame" guardian nil) (corrupted_is_not_OK formula-decl nil frame nil) (nonfaulty const-decl "bool" guardian nil) (nonfaulty const-decl "bool" guardian nil) (nonfaulty_guardian_block formula-decl nil guardian nil) (nonfaulty_guardian_invalid_cstate_encoding formula-decl nil guardian nil) (relay_only_from_specific_node formula-decl nil guardian nil) (sends const-decl "bool" sending_defs nil) (broadcast const-decl "Frame" guardian nil)) 316506 4970 t shostak)) (nonfaulty_channel_correct_cstate_sender_only 0 (nonfaulty_channel_correct_cstate_sender_only-1 nil 3294769374 3295507319 ("" (skosimp*) (("" (expand "broadcast") (("" (use "epsilon_ax[Frame]") (("" (ground) (("1" (skosimp*) (("1" (replace -1 :dir rl :hide? t) (("1" (use "relay_only_from_specific_node") (("1" (ground) (("1" (use "nonfaulty_guardian_block") (("1" (ground) (("1" (expand "sends_correct") (("1" (expand "sends") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "sends_correct") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst? :subst ("x" "relay(t!1,g(c!1),sender(t!1))" "p" "sender(t!1)")) (("2" (skosimp*) (("2" (use "nonfaulty_guardian_block") (("2" (ground) (("2" (expand "nonfaulty") (("2" (expand "nonfaulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((broadcast const-decl "Frame" guardian nil) (sends const-decl "bool" sending_defs nil) (sends_correct const-decl "bool" sending_defs nil) nil nil (nonfaulty_guardian_block formula-decl nil guardian nil) (relay_only_from_specific_node formula-decl nil guardian nil) (sender const-decl "Proc" types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (Proc nonempty-type-decl nil types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (Slot nonempty-type-eq-decl nil types nil) (Guardian nonempty-type-decl nil guardian nil) (relay const-decl "Frame" guardian nil) (Channel nonempty-type-decl nil types nil) (g const-decl "[Channel -> Guardian]" guardian nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (null const-decl "Frame" frame nil) (Frame nonempty-type-decl nil frame nil) (epsilon_ax formula-decl nil epsilons nil)) 165 130 t shostak)) (no_simultaneous_access 0 (no_simultaneous_access-1 nil 3294741179 3295507319 ("" (skosimp*) (("" (expand "simultaneous_access") (("" (expand "nonfaulty") (("" (use "nonfaulty_guardian_exists") nil nil)) nil)) nil)) nil) unchecked ((simultaneous_access const-decl "bool" guardian 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) (Slot nonempty-type-eq-decl nil types nil) (nonfaulty_guardian_exists formula-decl nil guardian nil) nil) 16 20 t shostak)) (IMP_ttpc_TCC1 0 (IMP_ttpc_TCC1-1 nil 3294737986 3295507319 ("" (use "nonfaulty_sender") nil nil) proved-complete ((nonfaulty_sender formula-decl nil guardian nil)) 4 0 t shostak)) (IMP_ttpc_TCC2 0 (IMP_ttpc_TCC2-1 nil 3294737986 3295507319 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast") (("" (ground) (("" (inst?) nil nil)) nil)) nil)) nil) proved-complete ((nonfaulty_channel_broadcast formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Channel nonempty-type-decl nil types nil) (sender const-decl "Proc" types nil) (Proc nonempty-type-decl nil types nil)) 40 30 t shostak)) (IMP_ttpc_TCC3 0 (IMP_ttpc_TCC3-1 nil 3294737986 3295507319 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast_sender") (("" (ground) nil nil)) nil)) nil) proved-complete ((nonfaulty_channel_broadcast_sender formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 20 20 t shostak)) (IMP_ttpc_TCC4 0 (IMP_ttpc_TCC4-1 nil 3294737986 3295507319 ("" (skosimp*) (("" (use "channel_broadcast_only_if_sent") (("" (ground) nil nil)) nil)) nil) proved-complete ((channel_broadcast_only_if_sent formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Channel nonempty-type-decl nil types nil)) 31 20 t shostak)) (IMP_ttpc_TCC5 0 (IMP_ttpc_TCC5-1 nil 3294737986 3295507319 ("" (skosimp*) (("" (use "nonfaulty_channel_max_delay") (("" (ground) nil nil)) nil)) nil) proved-complete ((nonfaulty_channel_max_delay formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 26 20 t shostak)) (IMP_ttpc_TCC6 0 (IMP_ttpc_TCC6-1 nil 3294737986 3295507319 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast_cstate_encoding") (("" (ground) (("" (postpone) nil nil)) nil)) nil)) nil) proved-incomplete ((nonfaulty_channel_broadcast_cstate_encoding formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 37 10 t shostak)) (IMP_ttpc_TCC7 0 (IMP_ttpc_TCC7-1 nil 3294737986 3295507320 ("" (skosimp*) (("" (use "nonfaulty_channel_correct_cstate_sender_only") (("" (ground) (("" (expand "sends_correct") (("" (propax) nil nil)) nil)) nil)) nil)) nil) proved-incomplete ((nonfaulty_channel_correct_cstate_sender_only formula-decl nil guardian nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil)) 41 20 t shostak)) (IMP_ttpc_TCC8 0 (IMP_ttpc_TCC8-1 nil 3294737986 3295507320 ("" (skosimp*) (("" (use "no_simultaneous_access") nil nil)) nil) proved-incomplete ((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) (Slot nonempty-type-eq-decl nil types nil) (no_simultaneous_access formula-decl nil guardian nil)) 14 20 t shostak))) $$$window_timing.pvs window_timing [(IMPORTING frame) sent, rcvd : [Slot,Channel,Proc -> Frame], broadcast : [Slot,Channel -> Frame] ] : THEORY BEGIN IMPORTING window_timing_defs t : VAR Slot p,q,r : VAR Proc c : VAR Channel rt : VAR realtime d : VAR {rt | rt >= 0} transmission_timing : AXIOM % -- cf. Rushby's Window-Timing Proof synchronized(t,p,r) AND sending_time_OK(t,sent(t,c,p),p) AND window_timing_OK(t) AND (EXISTS d: d <= max_broadcast_delay AND delivery_time(broadcast(t,c)) = transmission_time(sent(t,c,p)) + d) => in_receive_window(t,receive_time(r,rcvd(t,c,r))) in_receive_window_only_if_sent_in_time : AXIOM in_receive_window(t,receive_time(r,rcvd(t,c,r))) => sending_time_OK(t,sent(t,c,p),p) END window_timing $$$window_timing.prf (window_timing (max_broadcast_delay_TCC1 0 (max_broadcast_delay_TCC1-1 nil 3255083351 3255083370 ("" (inst + 0) nil nil) proved ((>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (realtime nonempty-type-eq-decl nil time 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)) 5901 170 t shostak)) (transmission_timing_TCC1 0 (transmission_timing_TCC1-1 nil 3255083351 3255083352 ("" (subtype-tcc) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil) unfinished nil 799 150 nil shostak))) $$$ttpc.pvs ttpc [(IMPORTING frame) sent : [Slot,Channel,Proc -> Frame], broadcast : [Slot,Channel -> Frame], simultaneous_access, nonfaulty : pred[[Slot,Channel]] ] : THEORY BEGIN ASSUMING IMPORTING faultmodel_defs, sending_defs[sent] t : VAR Slot p,q : VAR Proc c : VAR Channel d : VAR {rt:realtime | rt >= 0} nonfaulty_sender : ASSUMPTION p = sender(t) AND nonfaulty(t,p) => (FORALL c: sends_correct(t,c,p)) OR (FORALL c: NOT sends(t,c,p)) nonfaulty_channel_broadcast : ASSUMPTION nonfaulty(t,c) => (EXISTS p: broadcast(t,c) = sent(t,c,p)) OR broadcast(t,c) = null OR corrupted(broadcast(t,c)) nonfaulty_channel_broadcast_sender : ASSUMPTION nonfaulty(t,c) AND sends_correct(t,c,p) AND NOT simultaneous_access(t,c) AND p = sender(t) => broadcast(t,c) = sent(t,c,p) channel_passive : ASSUMPTION broadcast(t,c) /= null => EXISTS p: sends(t,c,p) nonfaulty_channel_max_delay : ASSUMPTION nonfaulty(t,c) AND sends_correct(t,c,p) AND NOT simultaneous_access(t,c) AND p = sender(t) => EXISTS d: d <= max_broadcast_delay AND delivery_time(broadcast(t,c)) = transmission_time(sent(t,c,p)) + d nonfaulty_channel_broadcast_cstate_encoding : ASSUMPTION nonfaulty(t,c) AND broadcast(t,c) = sent(t,c,p) AND sends(t,c,p) AND phys_encoding_OK(broadcast(t,c)) => cstate_encoding_OK(t,sent(t,c,p),p) nonfaulty_channel_correct_cstate_sender_only : ASSUMPTION nonfaulty(t,c) AND sends_correct(t,c,p) AND broadcast(t,c) = sent(t,c,p) => p = sender(t) no_simultaneous_access : ASSUMPTION EXISTS c: nonfaulty(t,c) AND NOT simultaneous_access(t,c) ENDASSUMING nonfaulty_sender_sendingtime : COROLLARY p = sender(t) AND nonfaulty(t,p) AND sends(t,c,p) => sending_time_OK(t,sent(t,c,p),p) r : VAR Proc f : VAR Frame rt : VAR realtime CT : VAR Clocktime % ---------------------------------------------------------------------- rcvd(t,c,p) : Frame % ---------------------------------------------------------------------- nonfaulty_receiver : AXIOM nonfaulty(t,r) => rcvd(t,c,r) = broadcast(t,c) receiver_passive : AXIOM rcvd(t,c,r) = broadcast(t,c) OR rcvd(t,c,p) = null % ---------- activity_detected(t,c,r) : bool = rcvd(t,c,r) /= null % ---------- no_other_transmission(t,c,r) : bool nonfaulty_receiver_other_transmission : AXIOM nonfaulty(t,r) => (no_other_transmission(t,c,r) <=> NOT simultaneous_access(t,c)) % ---------- no_code_violations(t,c,r) : bool = phys_encoding_OK(rcvd(t,c,r)) % ---------- IMPORTING window_timing[sent,rcvd,broadcast] transmission_time_OK(t,c,r) : bool = in_receive_window(t,receive_time(r,rcvd(t,c,r))) in_receive_window_when_sending_time_OK_only : AXIOM transmission_time_OK(t,c,r) AND nonfaulty(t,r) AND sends(t,c,p) AND NOT simultaneous_access(t,c) => synchronized(t,p,r) AND sending_time_OK(t,sent(t,c,p),p) transmission_timing_consistent : AXIOM synchronized(t,p,r) AND in_receive_window(t,receive_time(p,rcvd(t,c,p))) AND nonfaulty(t,r) => in_receive_window(t,receive_time(r,rcvd(t,c,r))) % ---------- crc_check_OK(t,c,r) : bool = correct_crc(rcvd(t,c,r)) crc_check_no_transmission_fault : AXIOM nonfaulty(t,c) AND nonfaulty(t,r) => crc_check_OK(t,c,r) % ---------- c_state_agreement_OK(t,c,r) : bool = decode_cstate(rcvd(t,c,r)) = cstate(t,r) cstate_agreement_correct_medl_pos : PROPOSITION c_state_agreement_OK(t,c,r) AND nonfaulty(t,r) => medl_position(decode_cstate(rcvd(t,c,r))) = t same_clique(t,p,r) : bool = cstate(t,p) = cstate(t,r) nonfaulty_same_clique : AXIOM nonfaulty(t,p) AND nonfaulty(t,r) => same_clique(t,p,r) % ---------------------------------------------------------------------- Status : TYPE+ = {correct, incorrect, null_frame, invalid} valid_frame(t,c,r) : bool = transmission_time_OK(t,c,r) AND no_code_violations(t,c,r) AND no_other_transmission(t,c,r) frame_status(t,c,r) : Status = IF NOT activity_detected(t,c,r) THEN null_frame ELSIF NOT valid_frame(t,c,r) THEN invalid ELSIF NOT (crc_check_OK(t,c,r) AND c_state_agreement_OK(t,c,r)) THEN incorrect ELSE correct ENDIF slot_status(t,r) : Status = IF EXISTS c: frame_status(t,c,r) = correct THEN correct ELSIF EXISTS c: frame_status(t,c,r) = incorrect THEN incorrect ELSIF EXISTS c: frame_status(t,c,r) = null_frame THEN null_frame ELSE invalid ENDIF % ---------------------------------------------------------------------- correct_reception_no_faults : THEOREM % -- Validity EXISTS c: nonfaulty(t,sender(t)) AND sends(t,c,sender(t)) => FORALL r: nonfaulty(t,r) => rcvd(t,c,r) = sent(t,c,sender(t)) AND frame_status(t,c,r) = correct correct_reception_slot_status : COROLLARY nonfaulty(t,sender(t)) AND (EXISTS c: sends(t,c,sender(t))) => FORALL r: nonfaulty(t,r) => slot_status(t,r) = correct % ---------------------------------------------------------------------- consistent_transmission_part : LEMMA nonfaulty(t,p) AND nonfaulty(t,q) and nonfaulty(t,c) => frame_status(t,c,p) = correct => frame_status(t,c,q) = correct consistent_transmission : THEOREM % -- Agreement nonfaulty(t,p) AND nonfaulty(t,q) AND nonfaulty(t,c) => (frame_status(t,c,p) = correct <=> frame_status(t,c,q) = correct) % ---------------------------------------------------------------------- correct_reception_from_sender_only : THEOREM % -- Authenticity nonfaulty(t,r) AND nonfaulty(t,c) AND frame_status(t,c,r) = correct => rcvd(t,c,r) = sent(t,c,sender(t)) END ttpc $$$ttpc.prf (ttpc (nonfaulty_sender_sendingtime 0 (nonfaulty_sender_sendingtime-1 nil 3294658842 3294906281 ("" (skosimp*) (("" (use "nonfaulty_sender") (("" (ground) (("1" (inst?) (("1" (expand "sends_correct") (("1" (propax) nil nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil) proved ((nonfaulty_sender formula-decl nil ttpc nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil)) 65 40 t shostak)) (cstate_agreement_correct_medl_pos 0 (cstate_agreement_correct_medl_pos-1 nil 3255244463 3294906281 ("" (skosimp*) (("" (expand "c_state_agreement_OK") (("" (use "medl_nonfaulty") (("" (ground) nil nil)) nil)) nil)) nil) proved ((c_state_agreement_OK const-decl "bool" ttpc nil) (Proc nonempty-type-decl nil types 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) (Slot nonempty-type-eq-decl nil types nil) (medl_nonfaulty formula-decl nil CState nil)) 57 30 t shostak)) (correct_reception_no_faults 0 (correct_reception_no_faults-3 "" 3255722300 3294906449 ("" (skosimp*) (("" (use "no_simultaneous_access") (("" (skosimp*) (("" (inst?) (("" (skosimp*) (("" (case "rcvd(t!1, c!1, r!1) = sent(t!1, c!1, sender(t!1))") (("1" (use "nonfaulty_sender") (("1" (ground) (("1" (inst?) (("1" (expand "sends_correct") (("1" (flatten) (("1" (expand "frame_status") (("1" (lift-if) (("1" (expand "sends") (("1" (ground) (("1" (expand "activity_detected") (("1" (assert) nil nil)) nil) ("2" (expand "valid_frame") (("2" (prop) (("1" (expand "transmission_time_OK") (("1" (use "transmission_timing") (("1" (ground) (("1" (use "nonfaulty_synchronized") (("1" (assert) nil nil)) nil) ("2" (use "window_timing") nil nil) ("3" (use "nonfaulty_channel_max_delay") (("3" (use "nonfaulty_channel_broadcast_sender") (("3" (use "corrupted_is_not_OK") (("3" (ground) (("1" (expand "sends_correct") (("1" (propax) nil nil)) nil) ("2" (expand "sends_correct") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "no_code_violations") (("2" (assert) nil nil)) nil) ("3" (use "nonfaulty_receiver_other_transmission") (("3" (ground) nil nil)) nil)) nil)) nil) ("3" (use "crc_check_no_transmission_fault") (("3" (assert) nil nil)) nil) ("4" (expand "c_state_agreement_OK") (("4" (expand "cstate_encoding_OK") (("4" (use "nonfaulty_same_clique" :subst ("r" "r!1")) (("4" (assert) (("4" (expand "same_clique") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil) ("2" (use "nonfaulty_receiver") (("2" (assert) (("2" (use "nonfaulty_channel_broadcast_sender") (("2" (assert) (("2" (use "nonfaulty_sender") (("2" (ground) (("1" (inst?) nil nil) ("2" (inst?) nil nil) ("3" (inst?) nil nil) ("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((nonfaulty_receiver formula-decl nil ttpc nil) (nonfaulty_sender formula-decl nil ttpc nil) (activity_detected const-decl "bool" ttpc nil) (broadcast formal-const-decl "[Slot, Channel -> Frame]" ttpc nil) (transmission_timing formula-decl nil window_timing nil) (nonfaulty_channel_max_delay formula-decl nil ttpc nil) (corrupted_is_not_OK formula-decl nil frame nil) (nonfaulty_channel_broadcast_sender formula-decl nil ttpc nil) (window_timing formula-decl nil window_timing_defs nil) (nonfaulty_synchronized formula-decl nil localclocks nil) (transmission_time_OK const-decl "bool" ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (valid_frame const-decl "bool" ttpc nil) (crc_check_no_transmission_fault formula-decl nil ttpc nil) (cstate_encoding_OK const-decl "bool" frame nil) (same_clique const-decl "bool" ttpc nil) (nonfaulty_same_clique formula-decl nil ttpc nil) (c_state_agreement_OK const-decl "bool" ttpc nil) (sends const-decl "bool" sending_defs nil) (frame_status const-decl "Status" ttpc nil) (sends_correct const-decl "bool" sending_defs nil) (Frame nonempty-type-decl nil frame nil) (= const-decl "[T, T -> boolean]" equalities nil) (Proc nonempty-type-decl nil types nil) (rcvd const-decl "Frame" ttpc nil) (sent formal-const-decl "[Slot, Channel, Proc -> Frame]" ttpc nil) (sender const-decl "Proc" types nil) (Channel nonempty-type-decl nil types 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) (Slot nonempty-type-eq-decl nil types nil) (no_simultaneous_access formula-decl nil ttpc nil)) 144370 3110 t nil) (correct_reception_no_faults-2 "" 3255721270 3255722273 ("" (skosimp*) (("" (use "no_simultaneous_access") (("" (skosimp*) (("" (inst?) (("" (skosimp*) (("" (case "rcvd(t!1, c!1, r!1) = sent(t!1, c!1, sender(t!1))") (("1" (use "nonfaulty_receiver" :subst ("r" "r!1")) (("1" (assert) (("1" (expand "frame_status") (("1" (lift-if) (("1" (ground) (("1" (expand "activity_detected") (("1" (use "nonfaulty_channel_broadcast_sent") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "valid_frame") (("2" (prop) (("1" (expand "transmission_time_OK") (("1" (use "transmission_timing") (("1" (ground) (("1" (use "nonfaulty_synchronized") (("1" (assert) nil nil)) nil) ("2" (use "nonfaulty_sender_sendingtime") (("2" (ground) nil nil)) nil) ("3" (use "window_timing") nil nil) ("4" (use "nonfaulty_channel_max_delay") (("4" (ground) (("4" (expand "sends") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "no_code_violations") (("2" (use "nonfaulty_channel_broadcast_phys_encoding") (("2" (assert) (("2" (use "nonfaulty_sender_sendingtime") (("2" (ground) (("2" (use "nonfaulty_channel_broadcast_sent") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (use "nonfaulty_receiver_other_transmission") (("3" (ground) nil nil)) nil)) nil)) nil) ("3" (use "crc_check_no_transmission_fault") (("3" (assert) nil nil)) nil) ("4" (expand "c_state_agreement_OK") (("4" (use "nonfaulty_channel_broadcast_cstate_encoding") (("4" (assert) (("4" (expand "cstate_encoding_OK") (("4" (use "nonfaulty_same_clique" :subst ("r" "r!1")) (("4" (assert) (("4" (expand "same_clique") (("4" (ground) (("4" (use "nonfaulty_channel_broadcast_phys_encoding") (("4" (assert) (("4" (use "nonfaulty_sender_sendingtime") (("4" (ground) (("4" (use "nonfaulty_channel_broadcast_sent") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_receiver") (("2" (use "nonfaulty_channel_broadcast_sender") (("2" (case "NOT corrupted(broadcast(t!1, c!1))") (("1" (ground) nil nil) ("2" (assert) (("2" (use "nonfaulty_channel_broadcast_phys_encoding") (("2" (assert) (("2" (hide -3 3) (("2" (ground) (("1" (use "corrupted_is_not_OK") (("1" (ground) nil nil)) nil) ("2" (use "nonfaulty_sender_sendingtime") (("2" (ground) nil nil)) nil) ("3" (use "corrupted_is_non_null") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((nonfaulty_channel_broadcast_sender formula-decl nil ttpc nil) (nonfaulty_receiver formula-decl nil ttpc nil) (frame_status const-decl "Status" ttpc nil) (activity_detected const-decl "bool" ttpc nil) (broadcast formal-const-decl "[Slot, Channel -> Frame]" ttpc nil) (transmission_timing formula-decl nil window_timing nil) (nonfaulty_channel_max_delay formula-decl nil ttpc nil) (sends const-decl "bool" sending_defs nil) (window_timing formula-decl nil window_timing_defs nil) (nonfaulty_sender_sendingtime formula-decl nil ttpc nil) (nonfaulty_synchronized formula-decl nil localclocks nil) (transmission_time_OK const-decl "bool" ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (valid_frame const-decl "bool" ttpc nil) (crc_check_no_transmission_fault formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_cstate_encoding formula-decl nil ttpc nil) (cstate_encoding_OK const-decl "bool" frame nil) (same_clique const-decl "bool" ttpc nil) (nonfaulty_same_clique formula-decl nil ttpc nil) (c_state_agreement_OK const-decl "bool" ttpc nil) (Frame nonempty-type-decl nil frame nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (upfrom nonempty-type-eq-decl nil integers nil) (rcvd const-decl "Frame" ttpc nil) (sent formal-const-decl "[Slot, Channel, Proc -> Frame]" ttpc 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) (no_simultaneous_access formula-decl nil ttpc nil)) 48511 11620 t shostak) (correct_reception_no_faults-1 nil 3255161281 3255720275 ("" (skosimp*) (("" (use "no_simultaneous_access") (("" (skosimp*) (("" (inst?) (("" (skosimp*) (("" (case "rcvd(t!1, c!1, r!1) = sent(t!1, c!1, sender(t!1))") (("1" (use "nonfaulty_receiver" :subst ("r" "r!1")) (("1" (assert) (("1" (expand "frame_status") (("1" (lift-if) (("1" (ground) (("1" (expand "activity_detected") (("1" (use "nonfaulty_channel_broadcast_sent") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "valid_frame") (("2" (prop) (("1" (expand "transmission_time_OK") (("1" (use "transmission_timing") (("1" (ground) (("1" (use "nonfaulty_synchronized") (("1" (assert) nil nil)) nil) ("2" (use "nonfaulty_sender_sendingtime") (("2" (ground) nil nil)) nil) ("3" (use "window_timing") nil nil) ("4" (use "nonfaulty_channel_max_delay") (("4" (ground) (("4" (expand "sends") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "no_code_violations") (("2" (use "nonfaulty_channel_broadcast_phys_encoding") (("2" (assert) (("2" (use "nonfaulty_sender_sendingtime") (("2" (ground) (("2" (use "nonfaulty_channel_broadcast_sent") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (use "nonfaulty_receiver_other_transmission") (("3" (ground) nil nil)) nil)) nil)) nil) ("3" (use "crc_check_no_transmission_fault") (("3" (assert) nil nil)) nil) ("4" (expand "c_state_agreement_OK") (("4" (use "nonfaulty_channel_broadcast_cstate_encoding") (("4" (assert) (("4" (expand "cstate_encoding_OK") (("4" (use "nonfaulty_same_clique" :subst ("r" "r!1")) (("4" (assert) (("4" (expand "same_clique") (("4" (ground) (("4" (use "nonfaulty_channel_broadcast_phys_encoding") (("4" (assert) (("4" (use "nonfaulty_sender_sendingtime") (("4" (ground) (("4" (use "nonfaulty_channel_broadcast_sent") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_receiver") (("2" (use "nonfaulty_channel_broadcast_sender") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((corrupted const-decl "bool" frame nil) (NOT const-decl "[bool -> bool]" booleans nil) (corrupted_is_non_null formula-decl nil frame nil) (corrupted_is_not_OK formula-decl nil frame nil) (nonfaulty_channel_broadcast_sender formula-decl nil ttpc nil) (nonfaulty_receiver formula-decl nil ttpc nil) (frame_status const-decl "Status" ttpc nil) (activity_detected const-decl "bool" ttpc nil) (broadcast formal-const-decl "[Slot, Channel -> Frame]" ttpc nil) (transmission_timing formula-decl nil window_timing nil) (nonfaulty_channel_max_delay formula-decl nil ttpc nil) (sends const-decl "bool" sending_defs nil) (window_timing formula-decl nil window_timing_defs nil) (nonfaulty_sender_sendingtime formula-decl nil ttpc nil) (nonfaulty_synchronized formula-decl nil localclocks nil) (transmission_time_OK const-decl "bool" ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (valid_frame const-decl "bool" ttpc nil) (crc_check_no_transmission_fault formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_cstate_encoding formula-decl nil ttpc nil) (cstate_encoding_OK const-decl "bool" frame nil) (same_clique const-decl "bool" ttpc nil) (nonfaulty_same_clique formula-decl nil ttpc nil) (c_state_agreement_OK const-decl "bool" ttpc nil) (Frame nonempty-type-decl nil frame nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (upfrom nonempty-type-eq-decl nil integers nil) (rcvd const-decl "Frame" ttpc nil) (sent formal-const-decl "[Slot, Channel, Proc -> Frame]" ttpc 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) (no_simultaneous_access formula-decl nil ttpc nil)) 14664 11900 nil nil)) (correct_reception_slot_status 0 (correct_reception_slot_status-1 nil 3254654002 3294906282 ("" (skosimp*) (("" (use "correct_reception_no_faults") (("" (skosimp*) (("" (ground) (("1" (inst - "r!1") (("1" (ground) (("1" (expand "slot_status") (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_sender") (("2" (ground) (("1" (inst?) (("1" (expand "sends_correct") (("1" (propax) nil nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((correct_reception_no_faults formula-decl nil ttpc nil) (Slot nonempty-type-eq-decl nil types 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) (Channel nonempty-type-decl nil types nil) (slot_status const-decl "Status" ttpc nil) (Proc nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil) (sender const-decl "Proc" types nil) (nonfaulty_sender formula-decl nil ttpc nil)) 129 100 t shostak)) (consistent_transmission_part 0 (consistent_transmission_part-1 nil 3254738412 3294906282 ("" (skosimp*) (("" (expand "frame_status") (("" (lift-if) (("" (ground) (("1" (expand "activity_detected") (("1" (use "nonfaulty_receiver") (("1" (use "nonfaulty_receiver" :subst ("r" "p!1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand "valid_frame") (("2" (prop) (("1" (expand "transmission_time_OK") (("1" (assert) (("1" (use "transmission_timing_consistent" :subst ("p" "p!1")) (("1" (use "nonfaulty_synchronized") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "no_code_violations") (("2" (use "nonfaulty_receiver") (("2" (assert) (("2" (use "nonfaulty_receiver" :subst ("r" "p!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (use "nonfaulty_receiver_other_transmission") (("3" (use "nonfaulty_receiver_other_transmission" :subst ("r" "p!1")) (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (use "crc_check_no_transmission_fault" :polarity? t) (("3" (assert) nil nil)) nil) ("4" (expand "c_state_agreement_OK") (("4" (use "nonfaulty_same_clique" :subst ("r" "q!1")) (("4" (assert) (("4" (expand "same_clique") (("4" (use "nonfaulty_receiver" :subst ("r" "p!1")) (("4" (use "nonfaulty_receiver" :subst ("r" "q!1")) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((frame_status const-decl "Status" ttpc nil) (nonfaulty_receiver formula-decl nil ttpc nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (activity_detected const-decl "bool" ttpc nil) (nonfaulty_synchronized formula-decl nil localclocks nil) (transmission_timing_consistent formula-decl nil ttpc nil) (transmission_time_OK const-decl "bool" ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (valid_frame const-decl "bool" ttpc nil) (crc_check_no_transmission_fault formula-decl nil ttpc nil) (nonfaulty_same_clique formula-decl nil ttpc nil) (same_clique const-decl "bool" ttpc nil) (c_state_agreement_OK const-decl "bool" ttpc nil)) 349 290 t shostak)) (consistent_transmission 0 (consistent_transmission-1 nil 3254736827 3294906282 ("" (skosimp*) (("" (prop) (("1" (use "consistent_transmission_part" :subst ("q" "q!1")) (("1" (ground) nil nil)) nil) ("2" (use "consistent_transmission_part" :subst ("q" "p!1")) (("2" (ground) nil nil)) nil)) nil)) nil) proved ((Channel nonempty-type-decl nil types 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) (Slot nonempty-type-eq-decl nil types nil) (Proc nonempty-type-decl nil types nil) (consistent_transmission_part formula-decl nil ttpc nil)) 58 50 t shostak)) (correct_reception_from_sender_only 0 (correct_reception_from_sender_only-4 "" 3255720433 3294906283 ("" (skosimp*) (("" (expand "frame_status") (("" (lift-if) (("" (ground) (("" (expand "valid_frame") (("" (flatten) (("" (expand "no_code_violations") (("" (use "nonfaulty_receiver") (("" (assert) (("" (expand "activity_detected") (("" (use "channel_passive") (("" (ground) (("" (skosimp*) (("" (use "nonfaulty_receiver_other_transmission") (("" (ground) (("" (use "nonfaulty_channel_correct_cstate_sender_only" :polarity? t) (("" (use "corrupted_is_not_OK") (("" (ground) (("" (use "nonfaulty_channel_broadcast") (("" (ground) (("" (skosimp*) (("" (inst?) (("" (assert) (("" (expand "sends_correct") (("" (expand "sends") (("" (ground) (("1" (use "in_receive_window_when_sending_time_OK_only") (("1" (ground) (("1" (expand "sends") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (use "nonfaulty_channel_broadcast_cstate_encoding") (("2" (ground) (("2" (expand "sends") (("2" (ground) 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)) nil)) nil)) nil)) nil)) nil)) nil) proved ((frame_status const-decl "Status" ttpc nil) (nonfaulty_receiver formula-decl nil ttpc nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (activity_detected const-decl "bool" ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (nonfaulty_channel_correct_cstate_sender_only formula-decl nil ttpc nil) (sends_correct const-decl "bool" sending_defs nil) (in_receive_window_when_sending_time_OK_only formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_cstate_encoding formula-decl nil ttpc nil) (sends const-decl "bool" sending_defs nil) (nonfaulty_channel_broadcast formula-decl nil ttpc nil) (rcvd const-decl "Frame" ttpc nil) (Frame nonempty-type-decl nil frame nil) (corrupted_is_not_OK formula-decl nil frame nil) (channel_passive formula-decl nil ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (valid_frame const-decl "bool" ttpc nil)) 324 290 t shostak) (correct_reception_from_sender_only-3 "" 3255246804 3255720281 ("" (skosimp*) (("" (expand "frame_status") (("" (lift-if) (("" (ground) (("" (expand "valid_frame") (("" (flatten) (("" (expand "no_code_violations") (("" (use "nonfaulty_receiver") (("" (assert) (("" (expand "activity_detected") (("" (use "channel_passive") (("" (ground) (("" (skosimp*) (("" (use "nonfaulty_receiver_other_transmission") (("" (ground) (("" (use "nonfaulty_channel_correct_cstate_sender_only") (("" (ground) (("1" (use "nonfaulty_channel_broadcast_sender") (("1" (ground) nil nil)) nil) ("2" (expand "transmission_time_OK") (("2" (use "in_receive_window_only_if_sent_in_time") (("2" (ground) nil nil)) nil)) nil) ("3" (use "nonfaulty_channel_broadcast_cstate_encoding") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((frame_status const-decl "Status" ttpc nil) (nonfaulty_receiver formula-decl nil ttpc nil) (upfrom 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) (activity_detected const-decl "bool" ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (nonfaulty_channel_correct_cstate_sender_only formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_cstate_encoding formula-decl nil ttpc nil) (transmission_time_OK const-decl "bool" ttpc nil) (in_receive_window_only_if_sent_in_time formula-decl nil window_timing nil) (sent formal-const-decl "[Slot, Channel, Proc -> Frame]" ttpc nil) (broadcast formal-const-decl "[Slot, Channel -> Frame]" ttpc nil) (nonfaulty_channel_broadcast_sender formula-decl nil ttpc nil) (corrupted_is_not_OK formula-decl nil frame nil) (Frame nonempty-type-decl nil frame nil) (rcvd const-decl "Frame" ttpc nil) (channel_passive formula-decl nil ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (valid_frame const-decl "bool" ttpc nil)) 5337 4470 t shostak) (correct_reception_from_sender_only-2 nil 3255240683 3255246405 ("" (skosimp*) (("" (expand "frame_status") (("" (lift-if) (("" (ground) (("" (expand "valid_frame") (("" (flatten) (("" (expand "no_code_violations") (("" (use "nonfaulty_receiver") (("" (assert) (("" (expand "activity_detected") (("" (use "channel_passive") (("" (ground) (("" (skosimp*) (("" (use "nonfaulty_channel_correct_cstate_sender_only") (("" (assert) (("" (use "nonfaulty_receiver_other_transmission") (("" (ground) (("1" (use "nonfaulty_channel_broadcast_sender") (("1" (ground) nil nil)) nil) ("2" (use "nonfaulty_channel_broadcast") (("2" (ground) (("2" (use "nonfaulty_channel_broadcast_cstate_encoding") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((valid_frame const-decl "bool" ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (channel_passive formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_sender formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_cstate_encoding formula-decl nil ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (nonfaulty_channel_correct_cstate_sender_only formula-decl nil ttpc nil) (activity_detected const-decl "bool" ttpc 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) (upfrom nonempty-type-eq-decl nil integers nil) (nonfaulty_receiver formula-decl nil ttpc nil) (frame_status const-decl "Status" ttpc nil)) 186637 5540 t nil) (correct_reception_from_sender_only-1 nil 3255175960 3255240662 ("" (skosimp*) (("" (expand "frame_status") (("" (lift-if) (("" (ground) (("" (expand "valid_frame") (("" (flatten) (("" (expand "no_code_violations") (("" (use "nonfaulty_receiver") (("" (assert) (("" (expand "activity_detected") (("" (use "nonfaulty_channel_broadcast_passive") (("" (ground) (("" (skosimp*) (("" (use "nonfaulty_channel_correct_cstate_sender_only") (("" (assert) (("" (use "nonfaulty_receiver_other_transmission") (("" (ground) (("1" (use "nonfaulty_channel_broadcast_sender") (("1" (ground) nil nil)) nil) ("2" (use "nonfaulty_channel_broadcast") (("2" (ground) (("2" (use "nonfaulty_channel_broadcast_cstate_encoding") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((frame_status const-decl "Status" ttpc nil) (nonfaulty_receiver formula-decl nil ttpc nil) (upfrom 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) (activity_detected const-decl "bool" ttpc nil) (nonfaulty_channel_correct_cstate_sender_only formula-decl nil ttpc nil) (nonfaulty_receiver_other_transmission formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_cstate_encoding formula-decl nil ttpc nil) (nonfaulty_channel_broadcast_sender formula-decl nil ttpc nil) (no_code_violations const-decl "bool" ttpc nil) (valid_frame const-decl "bool" ttpc nil)) 190 150 t shostak))) $$$localclocks.pvs localclocks : THEORY BEGIN IMPORTING faultmodel_defs,time p,q,r : VAR Proc rt : VAR realtime d : VAR {rt | rt >= 0} t : VAR Slot LC(p,rt) : Clocktime % -- processor p's local clock LC_monotonic : AXIOM LC(p,rt) <= LC(p,rt+d) synchronized(t,p,r) : bool nonfaulty_synchronized : AXIOM nonfaulty(t,p) AND nonfaulty(t,r) => synchronized(t,p,r) END localclocks $$$window_timing_defs.pvs window_timing_defs : THEORY BEGIN IMPORTING frame, localclocks, faultmodel_defs t : VAR Slot p,q,r : VAR Proc f : VAR Frame c : VAR Channel rt : VAR realtime CT : VAR Clocktime sending_time_OK(t,f,p) : bool = LET start = transmission_time(f)`start, finish = transmission_time(f)`finish IN LC(p,start) = nominal_send_start(t) AND LC(p,finish) = nominal_send_finish(t) receive_time(r,f) : Window = (# start := LC(r,frame.delivery_time(f)`start), finish := LC(r,frame.delivery_time(f)`finish) #) max_broadcast_delay : {rt | rt >= 0} window_timing_OK(t) : bool window_timing : AXIOM % -- assume that the parameters nominal_* window_timing_OK(t) % are set appropriately END window_timing_defs $$$window_timing_defs.prf (window_timing_defs (receive_time_TCC1 0 (receive_time_TCC1-1 nil 3254815761 3255155780 ("" (skosimp*) (("" (lemma "LC_monotonic") (("" (inst - "delivery_time(f!1)`finish - delivery_time(f!1)`start" "r!1" "delivery_time(f!1)`start") (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil) proved ((LC_monotonic formula-decl nil localclocks nil) (Proc nonempty-type-eq-decl nil proc nil) (number_of_procs const-decl "upfrom(3)" proc nil) (upfrom nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Frame nonempty-type-decl nil frame nil) (realtime nonempty-type-eq-decl nil time nil) (window nonempty-type-eq-decl nil frame nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "window" frame nil) (transmission_time const-decl "window" frame nil) (delivery_time const-decl "{w | EXISTS d: w = transmission_time(f) + d}" frame nil) (f!1 skolem-const-decl "Frame" window_timing_defs nil)) 11488 1020 t shostak)) (max_broadcast_delay_TCC1 0 (max_broadcast_delay_TCC1-1 nil 3255154455 3255155763 ("" (inst + 0) nil nil) proved ((>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (realtime nonempty-type-eq-decl nil time 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)) 12 10 t shostak))) $$$sending_defs.pvs sending_defs [(IMPORTING frame) sent : [Slot,Channel,Proc -> Frame] ] : THEORY BEGIN IMPORTING window_timing_defs t : VAR Slot p,q : VAR Proc f : VAR Frame c : VAR Channel sends(t,c,p) : bool = % -- node p accesses channel c in sent(t,c,p) /= null % slot t, i.e. sends some data sends_correct(t,c,p) : bool = sends(t,c,p) AND sending_time_OK(t,sent(t,c,p),p) AND phys_encoding_OK(sent(t,c,p)) AND cstate_encoding_OK(t,sent(t,c,p),p) END sending_defs $$$CState.pvs CState: THEORY BEGIN IMPORTING faultmodel_defs CState : TYPE+ t : VAR Slot p : VAR Proc cstate(t,p) : CState medl_position(c:CState) : Slot medl_nonfaulty : AXIOM nonfaulty(t,p) => medl_position(cstate(t,p)) = t END CState $$$frame.pvs frame : THEORY BEGIN Frame : TYPE+ null : Frame IMPORTING CState t : VAR Slot p,q,r : VAR Proc f : VAR Frame c : VAR Channel rt : VAR realtime CT : VAR Clocktime % ---------------------------------------------------------------------- d : VAR {rt | rt >= 0} window : TYPE+ = [# start : realtime, finish : {rt:realtime | rt >= start} #] Window : TYPE+ = [# start : Clocktime, finish : {t:Clocktime | t >= start} #] w : VAR window W : VAR Window ; +(w,d) : window = (# start := w`start + d, finish := w`finish + d #) transmission_time(f) : window delivery_time(f) : {w | EXISTS d: w = transmission_time(f) +d} nominal_send_start(t) : Clocktime nominal_send_finish(t) : {CT:Clocktime | CT >= nominal_send_start(t)} SndWindow(t) : Window = (# start := nominal_send_start(t), finish := nominal_send_finish(t) #) nominal_receive_start(t) : Clocktime nominal_receive_finish(t) : {CT:Clocktime | CT >= nominal_receive_start(t)} RcvWindow(t) : Window = (# start := nominal_receive_start(t), finish := nominal_receive_finish(t) #) in_receive_window(t,W) : bool = RcvWindow(t)`start <= W`start AND W`finish <= RcvWindow(t)`finish % ---------------------------------------------------------------------- corrupted(f) : bool phys_encoding_OK(f) : bool corrupted_is_not_OK : AXIOM corrupted(f) => NOT phys_encoding_OK(f) corrupted_is_non_null : AXIOM corrupted(f) => f /= null correct_crc(f) : bool decode_cstate(f) : CState cstate_encoding_OK(t,f,p) : bool = decode_cstate(f) = cstate(t,p) AND sender(medl_position(decode_cstate(f))) = p % ?? END frame $$$frame.prf (frame (window_TCC1 0 (window_TCC1-1 nil 3254814133 3254814158 ("" (inst + "(#start := 0, finish := 0#)") nil nil) proved-complete ((>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (realtime nonempty-type-eq-decl nil time nil)) 16496 190 t shostak)) (Window_TCC1 0 (Window_TCC1-1 nil 3254814133 3254814166 ("" (inst + "(#start := 0, finish := 0#)") nil nil) proved-complete ((>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (Clocktime nonempty-type-eq-decl nil time nil)) 3421 190 t shostak)) (plus_TCC1 0 (plus_TCC1-1 nil 3254814133 3254814134 ("" (subtype-tcc) nil nil) proved-complete ((realtime nonempty-type-eq-decl nil time nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (duration nonempty-type-eq-decl nil time nil)) 228 190 nil shostak)) (delivery_time_TCC1 0 (delivery_time_TCC1-1 nil 3255155805 3255155994 ("" (inst + "lambda f: transmission_time(f)") (("" (skosimp*) (("" (inst + 0) (("" (apply-extensionality :hide? t) (("1" (expand "+ ") (("1" (propax) nil nil)) nil) ("2" (expand "+ ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((transmission_time const-decl "window" frame nil) (+ const-decl "window" frame nil) (= const-decl "[T, T -> boolean]" equalities nil) (window nonempty-type-eq-decl nil frame nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (realtime nonempty-type-eq-decl nil time nil) (Frame nonempty-type-decl nil frame nil)) 13874 1080 t shostak)) (nominal_send_finish_TCC1 0 (nominal_send_finish_TCC1-1 nil 3254814134 3254814191 ("" (inst + "lambda t: nominal_send_start(t)") nil nil) proved-complete ((nominal_send_start const-decl "Clocktime" frame nil) (Clocktime nonempty-type-eq-decl nil time nil) (Slot nonempty-type-eq-decl nil slots 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)) 20560 200 t shostak)) (nominal_receive_finish_TCC1 0 (nominal_receive_finish_TCC1-1 nil 3254814134 3254814204 ("" (existence-tcc) (("" (inst + "lambda t: nominal_receive_start(t)") nil nil)) nil) proved-complete ((nominal_receive_start const-decl "Clocktime" frame nil) (Clocktime nonempty-type-eq-decl nil time nil) (Slot nonempty-type-eq-decl nil slots 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)) 10614 200 t shostak))) $$$time.pvs time : THEORY BEGIN realtime : TYPE+ = real duration : TYPE+ = posreal Clocktime : TYPE+ = integer Duration : TYPE+ = posint END time $$$types.pvs types : THEORY BEGIN Proc : TYPE+ Slot : TYPE+ = nat slot : VAR Slot sender(slot) : Proc Channel : TYPE+ IMPORTING time END types $$$types.prf (|types| (INT_TCC1 "" (EXISTENCE-TCC))) $$$faultmodel_defs.pvs faultmodel_defs : THEORY BEGIN IMPORTING types t : VAR Slot p : VAR Proc c : VAR Channel % -- faultiness of nodes: faulty(t,p) : bool % -- proc p is faulty in round/slot/at time t nonfaulty(t,p) : MACRO bool = NOT faulty(t,p) % -- faultiness of the bus (channel) faulty(t,c) : bool nonfaulty(t,c) : MACRO bool = NOT faulty(t,c) END faultmodel_defs $$$faultmodel_defs.prf (|faultmodel_defs| (|not_comm_faulty_is_send_and_rcvs_OK| "" (GRIND) NIL NIL)) $$$strong_fault_hypothesis.pvs strong_fault_hypothesis : THEORY BEGIN IMPORTING faultmodel_defs, frame t : VAR Slot p,q : VAR Proc c : VAR Channel d : VAR {rt:realtime | rt >= 0} sent(t,c,p) : Frame IMPORTING sending_defs[sent], window_timing_defs nonfaulty_sender : AXIOM p = sender(t) AND nonfaulty(t,p) => (FORALL c: sends_correct(t,c,p)) OR (FORALL c: NOT sends(t,c,p)) nonfaulty_not_sender_not_sends : AXIOM p /= sender(t) AND nonfaulty(t,p) => NOT sends(t,c,p) nonfaulty_sender_sendingtime : COROLLARY p = sender(t) AND nonfaulty(t,p) AND sends(t,c,p) => sending_time_OK(t,sent(t,c,p),p) % --------------------------------------------------------------------------- accessed(t,c) : bool = EXISTS p: sends(t,c,p) simultaneous_access(t,c) : bool = (EXISTS p,q: p /= q AND sends(t,c,p) AND sends(t,c,q)) % -- Node Faults % -- only one faulty node at a time one_faulty_proc_only : AXIOM faulty(t,p) AND faulty(t,q) => p = q % -- even a faulty node does not send data outside its assigned % sending slot on all *non-faulty* channels only_within_own_slots : AXIOM faulty(t,p) AND p /= sender(t) => NOT FORALL c: nonfaulty(t,c) => sends(t,c,p) % -- a node will never send a correct frame outside its assigned % sending slots correct_frames_by_sender_only : AXIOM sends_correct(t,c,p) => p = sender(t) % -- a node will never hide its identity when sending frames sender_provides_correct_Cstate_information : AXIOM sends(t,c,p) => cstate_encoding_OK(t,sent(t,c,p),p) % --------------------------------------------------------------------------- broadcast(t,c) : Frame nonfaulty_channel_broadcast : AXIOM nonfaulty(t,c) AND sends(t,c,p) AND NOT simultaneous_access(t,c) => broadcast(t,c) = sent(t,c,p) collision : AXIOM simultaneous_access(t,c) => corrupted(broadcast(t,c)) % -- Network Faults % -- only one channel is faulty during a TDMA round % Remark: number of channels is not restricted here, therefore we allow % all but one channels to be faulty nonfaulty_channel_exists : AXIOM EXISTS c: nonfaulty(t,c) % -- a channel does not spontaneously create correct frames channel_passive : AXIOM NOT accessed(t,c) => broadcast(t,c) = null % -- a channel will deliver a frame either within some known maximum % delay or never nonfaulty_channel_max_delay : AXIOM nonfaulty(t,c) AND sends(t,c,p) AND broadcast(t,c) /= null AND NOT corrupted(broadcast(t,c)) => EXISTS d: d <= max_broadcast_delay AND delivery_time(broadcast(t,c)) = transmission_time(sent(t,c,p)) + d channel_fail_silence : AXIOM faulty(t,c) => broadcast(t,c) = null % --------------------------------------------------------------------------- % -- the following propositions correspond to the assumptions of the theory % imported below nonfaulty_channel_broadcasts_correctly_sent_frame : PROPOSITION nonfaulty(t,c) AND sends_correct(t,c,p) AND NOT simultaneous_access(t,c) AND p = sender(t) => broadcast(t,c) = sent(t,c,p) channel_broadcast_only_if_sent : PROPOSITION broadcast(t,c) /= null => EXISTS p: sends(t,c,p) nonfaulty_channel_broadcast_cstate_encoding : PROPOSITION nonfaulty(t,c) AND broadcast(t,c) = sent(t,c,p) AND sends(t,c,p) AND phys_encoding_OK(broadcast(t,c)) => cstate_encoding_OK(t,sent(t,c,p),p) nonfaulty_channel_correct_cstate_sender_only : PROPOSITION nonfaulty(t,c) AND sends_correct(t,c,p) AND broadcast(t,c) = sent(t,c,p) => p = sender(t) no_simultaneous_access : PROPOSITION EXISTS c: nonfaulty(t,c) AND NOT simultaneous_access(t,c) IMPORTING ttpc[sent,broadcast,simultaneous_access,nonfaulty] END strong_fault_hypothesis $$$strong_fault_hypothesis.prf (strong_fault_hypothesis (nonfaulty_sender_sendingtime 0 (nonfaulty_sender_sendingtime-1 nil 3255091731 3294920571 ("" (skosimp*) (("" (use "nonfaulty_sender") (("" (ground) (("1" (inst?) (("1" (expand "sends_correct") (("1" (propax) nil nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil) proved ((nonfaulty_sender formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil)) 70 30 t shostak)) (nonfaulty_channel_broadcasts_correctly_sent_frame 0 (nonfaulty_channel_broadcasts_correctly_sent_frame-1 nil 3294728436 3294920571 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast") (("" (ground) (("" (expand "sends_correct") (("" (propax) nil nil)) nil)) nil)) nil)) nil) proved ((nonfaulty_channel_broadcast formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil)) 88 30 t shostak)) (channel_broadcast_only_if_sent 0 (channel_broadcast_only_if_sent-1 nil 3255240737 3294920571 ("" (skosimp*) (("" (use "channel_passive") (("" (ground) (("" (expand "accessed") (("" (propax) nil nil)) nil)) nil)) nil)) nil) proved ((channel_passive formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Channel nonempty-type-decl nil types nil) (accessed const-decl "bool" strong_fault_hypothesis nil)) 50 20 t shostak)) (nonfaulty_channel_broadcast_cstate_encoding 0 (nonfaulty_channel_broadcast_cstate_encoding-1 nil 3255154289 3294920571 ("" (skosimp*) (("" (use "sender_provides_correct_Cstate_information") (("" (assert) nil nil)) nil)) nil) proved ((sender_provides_correct_Cstate_information formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 56 30 t shostak)) (nonfaulty_channel_correct_cstate_sender_only 0 (nonfaulty_channel_correct_cstate_sender_only-1 nil 3255241388 3294920571 ("" (skosimp*) (("" (use "correct_frames_by_sender_only") (("" (assert) nil nil)) nil)) nil) proved ((correct_frames_by_sender_only formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 31 20 t shostak)) (no_simultaneous_access 0 (no_simultaneous_access-3 nil 3294657202 3294920572 ("" (skosimp*) (("" (case "exists p: faulty(t!1,p)") (("1" (skosimp*) (("1" (use "only_within_own_slots") (("1" (case "p!1/=sender(t!1)") (("1" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "simultaneous_access") (("1" (skosimp*) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("1" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("1" (assert) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "q!1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "/=") (("2" (use "nonfaulty_channel_exists" :subst ("t" "t!1")) (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (expand "simultaneous_access") (("2" (skosimp*) (("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("2" (case "q!1 /= sender(t!1)") (("1" (ground) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "q!1")) (("1" (ground) nil nil)) nil)) nil) ("2" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("1" (ground) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("2" (ground) (("2" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_channel_exists") (("2" (skosimp*) (("2" (inst? :subst ("c" "c!1")) (("2" (ground) (("2" (expand "simultaneous_access") (("2" (skosimp*) (("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!1")) (("2" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("1" (ground) (("1" (inst?) nil nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((faulty const-decl "bool" faultmodel_defs nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (only_within_own_slots formula-decl nil strong_fault_hypothesis nil) (nonfaulty_channel_exists formula-decl nil strong_fault_hypothesis nil) (Channel nonempty-type-decl nil types nil) (simultaneous_access const-decl "bool" strong_fault_hypothesis nil) (nonfaulty_not_sender_not_sends formula-decl nil strong_fault_hypothesis nil) (one_faulty_proc_only formula-decl nil strong_fault_hypothesis nil) (/= const-decl "boolean" notequal nil) (sender const-decl "Proc" types nil)) 527 300 nil nil) (no_simultaneous_access-2 nil 3294656996 3294657029 ("" (auto-rewrite "nonfaulty") (("" (skosimp*) (("" (case "exists p: faulty(t!1,p)") (("1" (skosimp*) (("1" (use "only_within_own_slots") (("1" (case "p!1/=sender(t!1)") (("1" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "simultaneous_access") (("1" (skosimp*) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("1" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("1" (assert) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "q!1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "/=") (("2" (use "nonfaulty_channel_exists" :subst ("t" "t!1")) (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (expand "simultaneous_access") (("2" (skosimp*) (("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("2" (case "q!1 /= sender(t!1)") (("1" (ground) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "q!1")) (("1" (ground) nil nil)) nil)) nil) ("2" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("1" (ground) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("2" (ground) (("2" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_channel_exists") (("2" (skosimp*) (("2" (inst? :subst ("c" "c!1")) (("2" (ground) (("2" (expand "simultaneous_access") (("2" (skosimp*) (("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!1")) (("2" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("1" (ground) (("1" (inst?) nil nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) untried ((Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (only_within_own_slots formula-decl nil strong_fault_hypothesis nil) (nonfaulty_channel_exists formula-decl nil strong_fault_hypothesis nil) (Channel nonempty-type-decl nil types nil) (simultaneous_access const-decl "bool" strong_fault_hypothesis nil) (nonfaulty_not_sender_not_sends formula-decl nil strong_fault_hypothesis nil) (one_faulty_proc_only formula-decl nil strong_fault_hypothesis nil) (/= const-decl "boolean" notequal nil) (sender const-decl "Proc" types nil)) 32477 2250 nil nil) (no_simultaneous_access-1 nil 3255154307 3294656980 ("" (skosimp*) (("" (case "exists p: faulty(t!1,p)") (("1" (skosimp*) (("1" (use "only_within_own_slots") (("1" (case "p!1/=sender(t!1)") (("1" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "simultaneous_access") (("1" (skosimp*) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("1" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("1" (assert) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "q!1")) (("1" (expand "faulty") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("2" (expand "faulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "/=") (("2" (use "nonfaulty_channel_exists" :subst ("t" "t!1")) (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (expand "simultaneous_access") (("2" (skosimp*) (("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("2" (case "q!1 /= sender(t!1)") (("1" (ground) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "q!1")) (("1" (expand "faulty") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("1" (ground) (("1" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("1" (expand "faulty") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!2")) (("2" (ground) (("2" (use "one_faulty_proc_only" :subst ("p" "p!1" "q" "p!2")) (("2" (expand "faulty") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "nonfaulty_channel_exists") (("2" (skosimp*) (("2" (inst? :subst ("c" "c!1")) (("2" (ground) (("2" (expand "simultaneous_access") (("2" (skosimp*) (("2" (use "nonfaulty_not_sender_not_sends" :subst ("p" "p!1")) (("2" (ground) (("1" (use "nonfaulty_not_sender_not_sends" :subst ("p" "q!1")) (("1" (ground) (("1" (expand "faulty") (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (expand "faulty") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((upfrom 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) (only_within_own_slots formula-decl nil strong_fault_hypothesis nil) (nonfaulty_channel_exists formula-decl nil strong_fault_hypothesis nil) (simultaneous_access const-decl "bool" strong_fault_hypothesis nil) (nonfaulty_not_sender_not_sends formula-decl nil strong_fault_hypothesis nil) (one_faulty_proc_only formula-decl nil strong_fault_hypothesis nil) (/= const-decl "boolean" notequal nil)) 21217 1680 t shostak)) (IMP_ttpc_TCC1 0 (IMP_ttpc_TCC1-1 nil 3255086763 3294920572 ("" (use "nonfaulty_sender") nil nil) proved ((nonfaulty_sender formula-decl nil strong_fault_hypothesis nil)) 16 0 t shostak)) (IMP_ttpc_TCC2 0 (IMP_ttpc_TCC2-1 nil 3255086764 3294920572 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast") (("" (use "channel_passive") (("" (ground) (("" (expand "accessed") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (ground) (("" (use "collision") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((nonfaulty_channel_broadcast formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Channel nonempty-type-decl nil types nil) (collision formula-decl nil strong_fault_hypothesis nil) (Proc nonempty-type-decl nil types nil) (accessed const-decl "bool" strong_fault_hypothesis nil) (channel_passive formula-decl nil strong_fault_hypothesis nil)) 95 70 t shostak)) (IMP_ttpc_TCC3 0 (IMP_ttpc_TCC3-2 nil 3294728426 3294920572 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcasts_correctly_sent_frame") (("" (ground) (("" (expand "sends_correct") (("" (propax) nil)))))))) nil) proved ((nonfaulty_channel_broadcasts_correctly_sent_frame formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 43 20 nil nil) (IMP_ttpc_TCC3-1 nil 3255086765 3294728272 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast_sender") (("" (ground) (("" (expand "sends_correct") (("" (propax) nil nil)) nil)) nil)) nil)) nil) proved-complete ((nonfaulty_channel_broadcast formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil) (sends_correct const-decl "bool" sending_defs nil)) 19160 1140 t shostak)) (IMP_ttpc_TCC4 0 (IMP_ttpc_TCC4-1 nil 3255086765 3294920572 ("" (skosimp*) (("" (use "channel_broadcast_only_if_sent") (("" (ground) nil nil)) nil)) nil) proved ((channel_broadcast_only_if_sent formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Channel nonempty-type-decl nil types nil)) 30 20 t shostak)) (IMP_ttpc_TCC5 0 (IMP_ttpc_TCC5-1 nil 3255086765 3294920821 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast") (("" (use "nonfaulty_channel_max_delay") (("" (expand "sends_correct") (("" (expand "sends") (("" (ground) (("" (use "corrupted_is_not_OK") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((nonfaulty_channel_max_delay formula-decl nil strong_fault_hypothesis nil) (sends const-decl "bool" sending_defs nil) (corrupted_is_not_OK formula-decl nil frame nil) (sent const-decl "Frame" strong_fault_hypothesis nil) (Frame nonempty-type-decl nil frame nil) (sends_correct const-decl "bool" sending_defs nil) (Channel nonempty-type-decl nil types nil) (Proc nonempty-type-decl nil types 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) (Slot nonempty-type-eq-decl nil types nil) (nonfaulty_channel_broadcast formula-decl nil strong_fault_hypothesis nil)) 228180 4410 t shostak)) (IMP_ttpc_TCC6 0 (IMP_ttpc_TCC6-1 nil 3255086765 3294920572 ("" (skosimp*) (("" (use "nonfaulty_channel_broadcast_cstate_encoding") (("" (ground) nil nil)) nil)) nil) proved ((nonfaulty_channel_broadcast_cstate_encoding formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 32 20 t shostak)) (IMP_ttpc_TCC7 0 (IMP_ttpc_TCC7-1 nil 3255169021 3294920572 ("" (skosimp*) (("" (use "nonfaulty_channel_correct_cstate_sender_only") (("" (ground) nil nil)) nil)) nil) proved ((nonfaulty_channel_correct_cstate_sender_only formula-decl nil strong_fault_hypothesis nil) (Slot nonempty-type-eq-decl nil types 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) (Proc nonempty-type-decl nil types nil) (Channel nonempty-type-decl nil types nil)) 32 20 t shostak)) (IMP_ttpc_TCC8 0 (IMP_ttpc_TCC8-1 nil 3255240762 3294920572 ("" (skosimp*) (("" (use "no_simultaneous_access") nil nil)) nil) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Slot nonempty-type-eq-decl nil types nil) (no_simultaneous_access formula-decl nil strong_fault_hypothesis nil)) 13 10 t shostak)))