Alternate Byzantine Behavior definition based on message dependencies

[traiansf]

Attempting an alternate approach to defining byzantine traces.

[wkolowski]

This looks like a perfect thing to refactor into a Record, since you have already come up with the field names : )

Suggested change

	Definition fixed_byzantine_trace_prop
	(is : composite_state (sub_IM IM non_byzantine))
	(tr : list (composite_transition_item (sub_IM IM non_byzantine)))
	: Prop :=
	exists
	(byzantine_replacements_IM : sub_index byzantine -> VLSM message)
	(no_initial_messages_in_byzantine_IM : no_initial_messages_in_IM_prop byzantine_replacements_IM)
	(can_emit_signed_byzantine : channel_authentication_prop byzantine_replacements_IM (sub_IM_A byzantine A) (sub_IM_sender byzantine A sender)),
	exists bis btr,
	finite_valid_trace (fixed_byantine_composite_vlsm byzantine_replacements_IM) bis btr /\
	pre_loaded_fixed_non_byzantine_state_projection byzantine_replacements_IM bis = is /\
	VLSM_projection_trace_project (pre_loaded_fixed_non_byzantine_vlsm_projection byzantine_replacements_IM) btr = tr.
	Record fixed_byzantine_trace_prop
	(is : composite_state (sub_IM IM non_byzantine))
	(tr : list (composite_transition_item (sub_IM IM non_byzantine)))
	: Prop := {
	byzantine_replacements_IM : sub_index byzantine -> VLSM message;
	no_initial_messages_in_byzantine_IM : no_initial_messages_in_IM_prop byzantine_replacements_IM;
	can_emit_signed_byzantine : channel_authentication_prop byzantine_replacements_IM (sub_IM_A byzantine A) (sub_IM_sender byzantine A sender);
	bis : _;
	btr : _;
	eq_1 : finite_valid_trace (fixed_byantine_composite_vlsm byzantine_replacements_IM) bis btr;
	eq_2 : pre_loaded_fixed_non_byzantine_state_projection byzantine_replacements_IM bis = is;
	eq_3 : VLSM_projection_trace_project (pre_loaded_fixed_non_byzantine_vlsm_projection byzantine_replacements_IM) btr = tr;
	}.