• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
        • Correctness
        • Definition
          • Transitions
            • Events-possiblep
            • Events-next
            • Event-next
            • Event-possiblep
            • Transitions-store-certificate
            • Transitions-receive-certificate
            • Transitions-create-certificate
            • Transitions-timer-expires
            • Transitions-commit-anchors
              • Commit-anchors-next
              • Commit-anchors-possiblep
            • Transitions-advance-round
          • Operations
          • States
          • Initialization
          • Events
      • Aleobft-dynamic
      • 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).

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 anchor at the even round.

Definitions and Theorems

Function: commit-anchors-next-val

(defun commit-anchors-next-val (vals vstate)
 (declare (xargs :guard (and (address-setp vals)
                             (validator-statep vstate))))
 (declare
  (xargs :guard (and (not (emptyp vals))
                     (b* ((round (validator-state->round vstate)))
                       (and (oddp round)
                            (not (equal round 1))
                            (certificate-with-author+round
                                 (leader-at-round (1- round) vals)
                                 (1- round)
                                 (validator-state->dag vstate)))))))
 (let ((__function__ 'commit-anchors-next-val))
  (declare (ignorable __function__))
  (b*
   ((current-round (validator-state->round vstate))
    (commit-round (1- current-round))
    (leader (leader-at-round commit-round vals))
    (dag (validator-state->dag vstate))
    (anchor (certificate-with-author+round leader commit-round dag))
    (last-committed-round (validator-state->last vstate))
    (anchors (collect-anchors anchor (- commit-round 2)
                              last-committed-round dag vals))
    (blockchain (validator-state->blockchain vstate))
    (committed-certs (validator-state->committed vstate))
    ((mv new-blockchain new-committed-certs)
     (extend-blockchain anchors
                        dag blockchain committed-certs)))
   (change-validator-state vstate
                           :blockchain new-blockchain
                           :last commit-round
                           :committed new-committed-certs))))

Theorem: validator-statep-of-commit-anchors-next-val

(defthm validator-statep-of-commit-anchors-next-val
  (b* ((new-vstate (commit-anchors-next-val vals vstate)))
    (validator-statep new-vstate))
  :rule-classes :rewrite)

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* ((vstate (get-validator-state val systate))
         (vals (all-addresses systate))
         (new-vstate (commit-anchors-next-val vals vstate)))
      (update-validator-state val new-vstate 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: 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)

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

(defthm validator-state->round-of-commit-anchors-next
 (implies
  (and (in val (correct-addresses systate))
       (commit-anchors-possiblep val1 systate))
  (equal
   (validator-state->round
       (get-validator-state val (commit-anchors-next val1 systate)))
   (validator-state->round (get-validator-state val systate)))))

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

(defthm validator-state->dag-of-commit-anchors-next
 (implies
  (and (in val (correct-addresses systate))
       (commit-anchors-possiblep val1 systate))
  (equal
   (validator-state->dag
       (get-validator-state val (commit-anchors-next val1 systate)))
   (validator-state->dag (get-validator-state val systate)))))

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

(defthm validator-state->last-of-commit-anchors-next
 (implies
  (and (in val (correct-addresses systate))
       (commit-anchors-possiblep val1 systate))
  (equal
   (validator-state->last
       (get-validator-state val (commit-anchors-next val1 systate)))
   (if
    (equal val val1)
    (1- (validator-state->round (get-validator-state val systate)))
    (validator-state->last (get-validator-state val systate))))))

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

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