• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-dynamic
        • Correctness
        • Definition
          • Initialization
          • Transitions
            • Transitions-receive-certificate
            • Transitions-create-certificate
            • Dags
            • Transitions-advance-round
            • Events-next
            • Events-possiblep
            • Event-next
            • Elections
            • Transitions-commit-anchors
            • Transitions-store-certificate
              • Store-certificate-next
              • Store-certificate-possiblep
            • Event-possiblep
            • Anchors
            • Blockchains
            • Transitions-timer-expires
          • States
          • Events
      • Aleobft-stake2
      • Aleobft-stake
      • Library-extensions
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Transitions-store-certificate

Store-certificate-next

New system state resulting from a store-certificate event.

Signature

(store-certificate-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 val and cert inputs of this function are the address and certificate in the store-certificate event; see event.

The certificate is added to the DAG and removed from the buffer.

In addition, if the certificate's round number is greater than the current round number plus one, the current round number is fast-forwarded to the certificate's round number minus one. The idea is that, if there are certificates, such as the one being stored in the DAG, which must necessarily come from another validator, which are two or more rounds ahead of the validator that is storing the certificate into the DAG, it indicates that this validator is behind. Note that, as required in store-certificate-possiblep, the DAG must contain all the previous certificates, which must form a quorum because of the way certificates are created (that there is an agreement on the quorum is proved via same-committees); thus, if the validator's round is advanced to the certificate's round, the validator can immediately generate its own new certificate for that round in our model (or a proposal in a more detailed model). This aspect of the protocol needs further study, along with the logic for round advancement in advance-round events.

If we advance the round, we also reset the timer, by setting it to `running'. Although the timer also needs further study, its purpose appears to be that a validator does not spend excessive time in a round, regardless of certificates received. In that case, it seems appropriate to reset the timer every time the round is advanced.

The network is unaffected.

Definitions and Theorems

Function: store-certificate-next

(defun store-certificate-next (val cert systate)
 (declare (xargs :guard (and (addressp val)
                             (certificatep cert)
                             (system-statep systate))))
 (declare
      (xargs :guard (store-certificate-possiblep val cert systate)))
 (let ((__function__ 'store-certificate-next))
   (declare (ignorable __function__))
   (b* (((certificate cert) cert)
        ((validator-state vstate)
         (get-validator-state val systate))
        (new-buffer (delete (certificate-fix cert)
                            vstate.buffer))
        (new-dag (insert (certificate-fix cert)
                         vstate.dag))
        ((mv new-round new-timer)
         (if (> cert.round (1+ vstate.round))
             (mv (1- cert.round) (timer-running))
           (mv vstate.round vstate.timer)))
        (new-vstate (change-validator-state vstate
                                            :buffer new-buffer
                                            :dag new-dag
                                            :round new-round
                                            :timer new-timer))
        (systate (update-validator-state val new-vstate systate)))
     systate)))

Theorem: system-statep-of-store-certificate-next

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

Theorem: all-addresses-of-store-certificate-next

(defthm all-addresses-of-store-certificate-next
 (implies
      (store-certificate-possiblep val cert systate)
      (b* ((?new-systate (store-certificate-next val cert systate)))
        (equal (all-addresses new-systate)
               (all-addresses systate)))))

Theorem: correct-addresses-of-store-certificate-next

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

Theorem: faulty-addresses-of-store-certificate-next

(defthm faulty-addresses-of-store-certificate-next
 (implies
      (store-certificate-possiblep val cert systate)
      (b* ((?new-systate (store-certificate-next val cert systate)))
        (equal (faulty-addresses new-systate)
               (faulty-addresses systate)))))

Theorem: validator-state->dag-of-store-certificate-next

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

Theorem: validator-state->buffer-of-store-certificate-next

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

Theorem: validator-state->endorsed-of-store-certificate-next

(defthm validator-state->endorsed-of-store-certificate-next
 (implies
      (store-certificate-possiblep val cert systate)
      (b* ((?new-systate (store-certificate-next val cert systate)))
        (equal (validator-state->endorsed
                    (get-validator-state val1 new-systate))
               (validator-state->endorsed
                    (get-validator-state val1 systate))))))

Theorem: validator-state->last-of-store-certificate-next

(defthm validator-state->last-of-store-certificate-next
 (implies
  (store-certificate-possiblep val cert systate)
  (b* ((?new-systate (store-certificate-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-store-certificate-next

(defthm validator-state->blockchain-of-store-certificate-next
 (implies
      (store-certificate-possiblep val cert systate)
      (b* ((?new-systate (store-certificate-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-store-certificate-next

(defthm validator-state->committed-of-store-certificate-next
 (implies
      (store-certificate-possiblep val cert systate)
      (b* ((?new-systate (store-certificate-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-store-certificate-next

(defthm get-network-state-of-store-certificate-next
 (b* nil
  (equal
       (get-network-state (store-certificate-next val cert systate))
       (get-network-state systate))))

Theorem: store-certificate-next-of-address-fix-val

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

Theorem: store-certificate-next-address-equiv-congruence-on-val

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

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

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

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

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

Theorem: store-certificate-next-of-system-state-fix-systate

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

Theorem: store-certificate-next-system-state-equiv-congruence-on-systate

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