		Search-engine friendly clone of the ACL2 documentation.

Transitions-accept

Accept-next

New system state resulting from an accept event.

Signature
(accept-next val cert systate) → new-systate
Arguments: val — Guard (addressp val).; cert — Guard (certificatep cert).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The message is removed from the network.

The certificate is added to the DAG of the validator.

The proposal of the certificate is removed from the set of proposals endorsed by the validator. This is a no-op if the validator has not actually endorsed the proposal.

Definitions and Theorems

Function: accept-next

(defun accept-next (val cert systate)
 (declare (xargs :guard (and (addressp val)
                             (certificatep cert)
                             (system-statep systate))))
 (declare (xargs :guard (accept-possiblep val cert systate)))
 (let ((__function__ 'accept-next))
   (declare (ignorable __function__))
   (b* ((msg (make-message-certificate :certificate cert
                                       :destination val))
        (network (get-network-state systate))
        (new-network (delete msg network))
        (systate (update-network-state new-network systate))
        ((validator-state vstate)
         (get-validator-state val systate))
        (new-dag (insert (certificate-fix cert)
                         vstate.dag))
        (new-endorsed (delete (certificate->proposal cert)
                              vstate.endorsed))
        (new-vstate (change-validator-state vstate
                                            :dag new-dag
                                            :endorsed new-endorsed))
        (systate (update-validator-state val new-vstate systate)))
     systate)))

Theorem: system-statep-of-accept-next

(defthm system-statep-of-accept-next
  (b* ((new-systate (accept-next val cert systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: correct-addresses-of-accept-next

(defthm correct-addresses-of-accept-next
  (implies (accept-possiblep val cert systate)
           (b* ((?new-systate (accept-next val cert systate)))
             (equal (correct-addresses new-systate)
                    (correct-addresses systate)))))

Theorem: validator-state->round-of-accept-next

(defthm validator-state->round-of-accept-next
 (b* ((?new-systate (accept-next val cert systate)))
  (equal
     (validator-state->round (get-validator-state val1 new-systate))
     (validator-state->round (get-validator-state val1 systate)))))

Theorem: validator-state->dag-of-accept-next

(defthm validator-state->dag-of-accept-next
 (implies
  (accept-possiblep val cert systate)
  (b* ((?new-systate (accept-next val cert systate)))
   (equal
     (validator-state->dag (get-validator-state val1 new-systate))
     (if
      (and (equal (address-fix val1)
                  (address-fix val))
           (in (address-fix val1)
               (correct-addresses systate)))
      (insert
           (certificate-fix cert)
           (validator-state->dag (get-validator-state val systate)))
      (validator-state->dag (get-validator-state val1 systate)))))))

Theorem: validator-state->proposed-of-accept-next

(defthm validator-state->proposed-of-accept-next
 (b* ((?new-systate (accept-next val cert systate)))
  (equal
   (validator-state->proposed
        (get-validator-state val1 new-systate))
   (validator-state->proposed (get-validator-state val1 systate)))))

Theorem: validator-state->endorsed-of-accept-next

(defthm validator-state->endorsed-of-accept-next
 (b* ((?new-systate (accept-next val cert systate)))
  (equal
   (validator-state->endorsed
        (get-validator-state val1 new-systate))
   (if
    (equal (address-fix val1)
           (address-fix val))
    (delete
     (certificate->proposal cert)
     (validator-state->endorsed (get-validator-state val1 systate)))
    (validator-state->endorsed
         (get-validator-state val1 systate))))))

Theorem: validator-state->last-of-accept-next

(defthm validator-state->last-of-accept-next
 (b* ((?new-systate (accept-next val cert systate)))
  (equal
      (validator-state->last (get-validator-state val1 new-systate))
      (validator-state->last (get-validator-state val1 systate)))))

Theorem: validator-state->blockchain-of-accept-next

(defthm validator-state->blockchain-of-accept-next
  (b* ((?new-systate (accept-next val cert systate)))
    (equal (validator-state->blockchain
                (get-validator-state val1 new-systate))
           (validator-state->blockchain
                (get-validator-state val1 systate)))))

Theorem: validator-state->committed-of-accept-next

(defthm validator-state->committed-of-accept-next
  (b* ((?new-systate (accept-next val cert systate)))
    (equal (validator-state->committed
                (get-validator-state val1 new-systate))
           (validator-state->committed
                (get-validator-state val1 systate)))))

Theorem: get-network-state-of-accept-next

(defthm get-network-state-of-accept-next
  (b* ((?new-systate (accept-next val cert systate)))
    (equal (get-network-state new-systate)
           (delete (message-certificate cert val)
                   (get-network-state systate)))))

Theorem: accept-next-of-address-fix-val

(defthm accept-next-of-address-fix-val
  (equal (accept-next (address-fix val)
                      cert systate)
         (accept-next val cert systate)))

Theorem: accept-next-address-equiv-congruence-on-val

(defthm accept-next-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (accept-next val cert systate)
                  (accept-next val-equiv cert systate)))
  :rule-classes :congruence)

Theorem: accept-next-of-certificate-fix-cert

(defthm accept-next-of-certificate-fix-cert
  (equal (accept-next val (certificate-fix cert)
                      systate)
         (accept-next val cert systate)))

Theorem: accept-next-certificate-equiv-congruence-on-cert

(defthm accept-next-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (accept-next val cert systate)
                  (accept-next val cert-equiv systate)))
  :rule-classes :congruence)

Theorem: accept-next-of-system-state-fix-systate

(defthm accept-next-of-system-state-fix-systate
  (equal (accept-next val cert (system-state-fix systate))
         (accept-next val cert systate)))

Theorem: accept-next-system-state-equiv-congruence-on-systate

(defthm accept-next-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (accept-next val cert systate)
                  (accept-next val cert systate-equiv)))
  :rule-classes :congruence)