Check if an
(augment-possiblep prop endor systate) → yes/no
The
The validator affected by this event is the author of the proposal, which must be correct in order for this event to happen, as explained in transitions-augment.
This event occurs when the network contains an endorsement message consisting of the proposal and the endorser (which is thus isomorphic to the event).
The validator must have that proposal pending, in its finite map from proposals to endorsing addresses.
The validator must be able to calculate the active committee for the proposal's round, so it can check that the endorsement comes from a member of the committee. As explained in transitions-propose, although a correct validator only sends proposals to committee members, our model allows it to send proposals also to faulty validators outside the committee, in order to model the possibility that a faulty validator in the committee shares the proposal with a faulty validator outside the committee, and that the latter validator, for whichever reason, endorses it, sending the endorsement to the proposer.
Function:
(defun augment-possiblep (prop endor systate) (declare (xargs :guard (and (proposalp prop) (addressp endor) (system-statep systate)))) (let ((__function__ 'augment-possiblep)) (declare (ignorable __function__)) (b* (((proposal prop) prop) ((unless (in prop.author (correct-addresses systate))) nil) (msg (make-message-endorsement :proposal prop :endorser endor)) ((unless (in msg (get-network-state systate))) nil) ((validator-state vstate) (get-validator-state prop.author systate)) (prop+endors (omap::assoc (proposal-fix prop) vstate.proposed)) ((unless prop+endors) nil) (commtt (active-committee-at-round prop.round vstate.blockchain)) ((unless commtt) nil) ((unless (in (address-fix endor) (committee-members commtt))) nil)) t)))
Theorem:
(defthm booleanp-of-augment-possiblep (b* ((yes/no (augment-possiblep prop endor systate))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm augment-possiblep-of-proposal-fix-prop (equal (augment-possiblep (proposal-fix prop) endor systate) (augment-possiblep prop endor systate)))
Theorem:
(defthm augment-possiblep-proposal-equiv-congruence-on-prop (implies (proposal-equiv prop prop-equiv) (equal (augment-possiblep prop endor systate) (augment-possiblep prop-equiv endor systate))) :rule-classes :congruence)
Theorem:
(defthm augment-possiblep-of-address-fix-endor (equal (augment-possiblep prop (address-fix endor) systate) (augment-possiblep prop endor systate)))
Theorem:
(defthm augment-possiblep-address-equiv-congruence-on-endor (implies (address-equiv endor endor-equiv) (equal (augment-possiblep prop endor systate) (augment-possiblep prop endor-equiv systate))) :rule-classes :congruence)
Theorem:
(defthm augment-possiblep-of-system-state-fix-systate (equal (augment-possiblep prop endor (system-state-fix systate)) (augment-possiblep prop endor systate)))
Theorem:
(defthm augment-possiblep-system-state-equiv-congruence-on-systate (implies (system-state-equiv systate systate-equiv) (equal (augment-possiblep prop endor systate) (augment-possiblep prop endor systate-equiv))) :rule-classes :congruence)