• 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
              • Commit-anchors-next
              • Commit-anchors-possiblep
            • Transitions-store-certificate
            • 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-commit-anchors

Commit-anchors-next

New state resulting from a commit-anchors event.

Signature

(commit-anchors-next val systate) → new-systate

Arguments

val — Guard (addressp val).

systate — Guard (system-statep systate).

Returns

new-systate — Type (system-statep new-systate).

The val input of this function is the address in the commit-anchors event; see event.

Because of commit-anchors-possiblep, the validator is in an odd round greater than one, and the even round immediately before it has an anchor for the leader at that round. We retrieve that anchor, and we use collect-anchors to collect that anchor and all the preceding anchors that must be committed and have not already been committed. Then we use extend-blockchain to extend the blockchain, and the set of all committed certificates. We also update the last committed round to the one for the latest anchor we committed.

Note that we instantiate the all-vals parameter of create-certificate-endorser-possiblep with the set of all the addresses of all validators in the system; that is indeed the rols of all-vals, as explained in update-committee-with-transaction.

Definitions and Theorems

Function: commit-anchors-next

(defun commit-anchors-next (val systate)
 (declare (xargs :guard (and (addressp val)
                             (system-statep systate))))
 (declare (xargs :guard (commit-anchors-possiblep val systate)))
 (let ((__function__ 'commit-anchors-next))
  (declare (ignorable __function__))
  (b*
   (((validator-state vstate)
     (get-validator-state val systate))
    (commit-round (1- vstate.round))
    (commtt
         (active-committee-at-round commit-round vstate.blockchain
                                    (all-addresses systate)))
    (leader (leader-at-round commit-round commtt))
    (anchor
     (certificate-with-author+round leader commit-round vstate.dag))
    (anchors
         (collect-anchors anchor (- commit-round 2)
                          vstate.last vstate.dag vstate.blockchain
                          (all-addresses systate)))
    ((mv new-blockchain new-committed)
     (extend-blockchain anchors vstate.dag
                        vstate.blockchain vstate.committed))
    (new-vstate (change-validator-state vstate
                                        :blockchain new-blockchain
                                        :last commit-round
                                        :committed new-committed))
    (systate (update-validator-state val new-vstate systate)))
   systate)))

Theorem: system-statep-of-commit-anchors-next

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

Theorem: all-addresses-of-commit-anchors-next

(defthm all-addresses-of-commit-anchors-next
  (implies (commit-anchors-possiblep val systate)
           (b* ((?new-systate (commit-anchors-next val systate)))
             (equal (all-addresses new-systate)
                    (all-addresses systate)))))

Theorem: correct-addresses-of-commit-anchors-next

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

Theorem: faulty-addresses-of-commit-anchors-next

(defthm faulty-addresses-of-commit-anchors-next
  (implies (commit-anchors-possiblep val systate)
           (b* ((?new-systate (commit-anchors-next val systate)))
             (equal (faulty-addresses new-systate)
                    (faulty-addresses systate)))))

Theorem: validator-state->dag-of-commit-anchors-next

(defthm validator-state->dag-of-commit-anchors-next
 (implies
  (commit-anchors-possiblep val systate)
  (b* ((?new-systate (commit-anchors-next val systate)))
   (equal
       (validator-state->dag (get-validator-state val1 new-systate))
       (validator-state->dag (get-validator-state val1 systate))))))

Theorem: validator-state->buffer-of-commit-anchors-next

(defthm validator-state->buffer-of-commit-anchors-next
 (implies
  (commit-anchors-possiblep val systate)
  (b* ((?new-systate (commit-anchors-next val systate)))
   (equal
    (validator-state->buffer (get-validator-state val1 new-systate))
    (validator-state->buffer (get-validator-state val1 systate))))))

Theorem: validator-state->endorsed-of-commit-anchors-next

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

Theorem: validator-state->last-of-commit-anchors-next

(defthm validator-state->last-of-commit-anchors-next
 (implies
  (commit-anchors-possiblep val systate)
  (b* ((?new-systate (commit-anchors-next val systate)))
   (equal
    (validator-state->last (get-validator-state val1 new-systate))
    (if
     (equal (address-fix val1)
            (address-fix val))
     (1- (validator-state->round (get-validator-state val systate)))
     (validator-state->last (get-validator-state val1 systate)))))))

Theorem: validator-state->blockchain-of-commit-anchors-next

(defthm validator-state->blockchain-of-commit-anchors-next
 (implies
  (and (in val1 (correct-addresses systate))
       (commit-anchors-possiblep val systate))
  (b* ((?new-systate (commit-anchors-next val systate)))
   (equal
    (validator-state->blockchain
         (get-validator-state val1 new-systate))
    (if
     (equal val1 (address-fix val))
     (b*
      (((validator-state vstate)
        (get-validator-state val1 systate))
       (commit-round (1- vstate.round))
       (commtt
           (active-committee-at-round commit-round vstate.blockchain
                                      (all-addresses systate)))
       (leader (leader-at-round commit-round commtt))
       (anchor (certificate-with-author+round
                    leader commit-round vstate.dag))
       (anchors
           (collect-anchors anchor (- commit-round 2)
                            vstate.last vstate.dag vstate.blockchain
                            (all-addresses systate))))
      (mv-nth
           0
           (extend-blockchain anchors vstate.dag
                              vstate.blockchain vstate.committed)))
     (validator-state->blockchain
          (get-validator-state val1 systate)))))))

Theorem: validator-state->committed-of-commit-anchors-next

(defthm validator-state->committed-of-commit-anchors-next
 (implies
  (and (in val1 (correct-addresses systate))
       (commit-anchors-possiblep val systate))
  (b* ((?new-systate (commit-anchors-next val systate)))
   (equal
    (validator-state->committed
         (get-validator-state val1 new-systate))
    (if
     (equal val1 (address-fix val))
     (b*
      (((validator-state vstate)
        (get-validator-state val systate))
       (commit-round (1- vstate.round))
       (commtt
           (active-committee-at-round commit-round vstate.blockchain
                                      (all-addresses systate)))
       (leader (leader-at-round commit-round commtt))
       (anchor (certificate-with-author+round
                    leader commit-round vstate.dag))
       (anchors
           (collect-anchors anchor (- commit-round 2)
                            vstate.last vstate.dag vstate.blockchain
                            (all-addresses systate))))
      (mv-nth
           1
           (extend-blockchain anchors vstate.dag
                              vstate.blockchain vstate.committed)))
     (validator-state->committed
          (get-validator-state val1 systate)))))))

Theorem: get-network-state-of-commit-anchors-next

(defthm get-network-state-of-commit-anchors-next
  (b* ((?new-systate (commit-anchors-next val systate)))
    (equal (get-network-state new-systate)
           (get-network-state systate))))

Theorem: commit-anchors-next-of-address-fix-val

(defthm commit-anchors-next-of-address-fix-val
  (equal (commit-anchors-next (address-fix val)
                              systate)
         (commit-anchors-next val systate)))

Theorem: commit-anchors-next-address-equiv-congruence-on-val

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

Theorem: commit-anchors-next-of-system-state-fix-systate

(defthm commit-anchors-next-of-system-state-fix-systate
  (equal (commit-anchors-next val (system-state-fix systate))
         (commit-anchors-next val systate)))

Theorem: commit-anchors-next-system-state-equiv-congruence-on-systate

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