AdeAtlas
Invariants / DC-PROTO-01

DC-PROTO-01

DC derived enforced

Protocol state machines have deterministic transitions

Source

Project constitution §3, T-CORE-03

Enforcement trace

Code

Tests 90

  • chain_sync::transition::tests::idle_request_next_with_immediate_data_yields_can_await_then_roll_forward
  • chain_sync::transition::tests::idle_request_next_with_no_data_yields_must_reply_via_await
  • chain_sync::transition::tests::roll_forward_signal_carries_header_and_tip_byte_identical
  • chain_sync::transition::tests::roll_backward_signal_carries_point_and_tip_byte_identical
  • chain_sync::transition::tests::find_intersect_with_known_point_yields_intersected_signal
  • chain_sync::transition::tests::find_intersect_with_unknown_points_yields_no_intersection
  • chain_sync::transition::tests::client_done_terminates_session
  • chain_sync::transition::tests::illegal_message_in_idle_returns_error
  • chain_sync::transition::tests::wrong_agency_returns_error
  • chain_sync::transition::tests::version_gating_rejects_out_of_version_message
  • chain_sync::transition::tests::empty_find_intersect_points_returns_malformed
  • signal_trace_synthetic_divergence_corpus
  • block_fetch::transition::tests::idle_request_range_yields_busy_then_start_batch
  • block_fetch::transition::tests::busy_no_blocks_returns_to_idle_with_event
  • block_fetch::transition::tests::streaming_block_delivers_bytes_byte_identical
  • block_fetch::transition::tests::streaming_batch_done_returns_to_idle
  • block_fetch::transition::tests::multi_block_streaming_preserves_order
  • block_fetch::transition::tests::client_done_terminates_session
  • block_fetch::transition::tests::illegal_message_in_idle_returns_error
  • block_fetch::transition::tests::wrong_agency_returns_error
  • block_fetch::transition::tests::version_gating_rejects_out_of_version_message
  • block_fetch::transition::tests::inverted_range_returns_malformed
  • block_fetch::transition::tests::block_delivered_event_carries_bytes_verbatim
  • block_fetch_frame_corpus
  • tx_submission::transition::tests::init_handshake_opens_session
  • tx_submission::transition::tests::request_blocking_ids_then_reply_round_trips
  • tx_submission::transition::tests::request_non_blocking_ids_with_empty_reply_round_trips
  • tx_submission::transition::tests::request_txs_then_reply_delivers_bytes_byte_identical
  • tx_submission::transition::tests::request_txs_with_partial_reply_legal
  • tx_submission::transition::tests::blocking_reply_empty_is_malformed
  • tx_submission::transition::tests::reply_ids_overfill_is_malformed
  • tx_submission::transition::tests::request_txs_empty_is_malformed
  • tx_submission::transition::tests::reply_txs_overfill_is_malformed
  • tx_submission::transition::tests::done_terminates_session
  • tx_submission::transition::tests::illegal_message_in_init_returns_error
  • tx_submission::transition::tests::wrong_agency_returns_error
  • tx_submission::transition::tests::version_gating_rejects_out_of_version_message
  • tx_submission2_mempool_trace
  • keep_alive::transition::tests::client_ping_then_server_pong_round_trips
  • keep_alive::transition::tests::cookie_mismatch_returns_malformed
  • keep_alive::transition::tests::client_done_terminates_session
  • keep_alive::transition::tests::illegal_message_in_idle_returns_error
  • keep_alive::transition::tests::wrong_agency_returns_error
  • keep_alive::transition::tests::version_gating_rejects_out_of_version_message
  • peer_sharing::transition::tests::share_request_then_full_reply_round_trips
  • peer_sharing::transition::tests::share_request_then_empty_reply_is_legal
  • peer_sharing::transition::tests::reply_exceeds_amount_returns_malformed
  • peer_sharing::transition::tests::client_done_terminates_session
  • peer_sharing::transition::tests::illegal_message_in_idle_returns_error
  • peer_sharing::transition::tests::wrong_agency_returns_error
  • peer_sharing::transition::tests::version_gating_rejects_out_of_version_message
  • keep_alive_event_trace
  • peer_sharing_event_trace
  • n2c::local_chain_sync::transition::tests::local_chain_sync_request_next_then_roll_forward
  • n2c::local_chain_sync::transition::tests::local_chain_sync_roll_backward_signal
  • n2c::local_chain_sync::transition::tests::local_chain_sync_find_intersect_known_point
  • n2c::local_chain_sync::transition::tests::local_chain_sync_find_intersect_unknown
  • n2c::local_chain_sync::transition::tests::local_chain_sync_client_done_terminates
  • n2c::local_chain_sync::transition::tests::local_chain_sync_wrong_agency_returns_error
  • n2c::local_chain_sync::transition::tests::local_chain_sync_version_gating
  • n2c::local_tx_submission::transition::tests::submit_tx_then_accept_round_trips
  • n2c::local_tx_submission::transition::tests::submit_tx_then_reject_carries_reason_bytes
  • n2c::local_tx_submission::transition::tests::client_done_terminates
  • n2c::local_tx_submission::transition::tests::wrong_agency_returns_error
  • n2c::local_tx_submission::transition::tests::version_gating
  • n2c::local_state_query::transition::tests::acquire_then_acquired_transitions_to_acquired
  • n2c::local_state_query::transition::tests::acquire_then_failure_returns_to_idle
  • n2c::local_state_query::transition::tests::query_then_result_round_trips
  • n2c::local_state_query::transition::tests::release_returns_to_idle
  • n2c::local_state_query::transition::tests::re_acquire_from_acquired_transitions_to_acquiring
  • n2c::local_state_query::transition::tests::client_done_from_idle_terminates
  • n2c::local_state_query::transition::tests::client_done_from_acquired_terminates
  • n2c::local_state_query::transition::tests::wrong_agency_returns_error
  • n2c::local_tx_monitor::transition::tests::idle_acquire_then_acquired
  • n2c::local_tx_monitor::transition::tests::acquired_release_returns_to_idle
  • n2c::local_tx_monitor::transition::tests::acquired_await_acquire_re_acquires
  • n2c::local_tx_monitor::transition::tests::acquired_next_tx_then_reply_with_tx
  • n2c::local_tx_monitor::transition::tests::acquired_next_tx_then_reply_empty_mempool
  • n2c::local_tx_monitor::transition::tests::acquired_has_tx_then_reply_present
  • n2c::local_tx_monitor::transition::tests::acquired_has_tx_then_reply_absent
  • n2c::local_tx_monitor::transition::tests::acquired_get_sizes_then_reply
  • n2c::local_tx_monitor::transition::tests::acquired_get_measures_then_reply
  • n2c::local_tx_monitor::transition::tests::get_measures_rejected_below_v2
  • n2c::local_tx_monitor::transition::tests::client_done_terminates_from_idle
  • n2c::local_tx_monitor::transition::tests::wrong_agency_returns_error
  • n2c::local_tx_monitor::transition::tests::version_gating_rejects_out_of_version_message
  • local_chain_sync_event_trace
  • local_tx_submission_event_trace
  • local_state_query_event_trace
  • local_tx_monitor_event_trace

CI 1

Cross-references

DC-CORE-01DC-PROTO-06

Strengthened in

PHASE4-N-A