From e1b3f1d7ae62e7aab4032cf1b02979abf6eb8595 Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Wed, 22 Dec 2021 10:37:54 +1100 Subject: [PATCH 1/2] Remove asserts from consensus validity checks --- src/dvspec/consensus.py | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/dvspec/consensus.py b/src/dvspec/consensus.py index e05f15d..20d9434 100644 --- a/src/dvspec/consensus.py +++ b/src/dvspec/consensus.py @@ -25,10 +25,11 @@ def consensus_is_valid_attestation_data(slashing_db: SlashingDB, attestation_data: AttestationData, attestation_duty: AttestationDuty) -> bool: """Determines if the given attestation is valid for the attestation duty. """ - assert attestation_data.slot == attestation_duty.slot - assert attestation_data.index == attestation_duty.committee_index - assert not is_slashable_attestation_data(slashing_db, attestation_data, attestation_duty.pubkey) - return True + return \ + attestation_data.slot == attestation_duty.slot and \ + attestation_data.index == attestation_duty.committee_index and \ + not is_slashable_attestation_data(slashing_db, attestation_data, attestation_duty.pubkey) + def consensus_on_attestation(slashing_db: SlashingDB, attestation_duty: AttestationDuty) -> AttestationData: @@ -44,10 +45,9 @@ def consensus_on_attestation(slashing_db: SlashingDB, attestation_duty: Attestat def consensus_is_valid_block(slashing_db: SlashingDB, block: BeaconBlock, proposer_duty: ProposerDuty) -> bool: """Determines if the given block is valid for the proposer duty. """ - assert block.slot == proposer_duty.slot - # TODO: Assert correct block.proposer_index - assert not is_slashable_block(slashing_db, block, proposer_duty.pubkey) - return True + # TODO: Add correct block.proposer_index check \ + return block.slot == proposer_duty.slot and \ + not is_slashable_block(slashing_db, block, proposer_duty.pubkey) def consensus_on_block(slashing_db: SlashingDB, proposer_duty: ProposerDuty) -> AttestationData: From 99399003491fd14e4dc890a9372e6553f9bc4898 Mon Sep 17 00:00:00 2001 From: Roberto Saltini Date: Fri, 24 Dec 2021 00:13:53 +1100 Subject: [PATCH 2/2] Add postconditions to consensus.py using nagini --- requirements.txt | 1 + src/dvspec/consensus.py | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/requirements.txt b/requirements.txt index c7057ef..3a72634 100644 --- a/requirements.txt +++ b/requirements.txt @@ -4,6 +4,7 @@ eth2spec==1.1.2 # dev requirements mypy flake8 +nagini # test requirements pytest \ No newline at end of file diff --git a/src/dvspec/consensus.py b/src/dvspec/consensus.py index 20d9434..e6f21e5 100644 --- a/src/dvspec/consensus.py +++ b/src/dvspec/consensus.py @@ -15,6 +15,8 @@ is_slashable_block, ) +from nagini_contracts.contracts import * + """ Consensus Specification @@ -39,6 +41,7 @@ def consensus_on_attestation(slashing_db: SlashingDB, attestation_duty: Attestat The consensus protocol must use `consensus_is_valid_attestation_data` to determine validity of the proposed attestation value. """ + Ensures(consensus_is_valid_attestation_data(slashing_db, Result(), attestation_duty)); pass @@ -57,6 +60,7 @@ def consensus_on_block(slashing_db: SlashingDB, proposer_duty: ProposerDuty) -> The consensus protocol must use `consensus_is_valid_block` to determine validity of the proposed block value. """ + Ensures(consensus_is_valid_block(slashing_db, Result(), proposer_duty)); pass @@ -75,4 +79,5 @@ def consensus_on_sync_committee_contribution(sync_committee_duty: SyncCommitteeD The consensus protocol must use `consensus_is_valid_sync_committee_contribution` to determine validity of the proposed block value. """ + Ensures(consensus_is_valid_sync_committee_contribution(sync_committee_duty, Result())); pass