• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-dynamic
      • Aleobft-stake2
        • Definition
          • Initialization
          • Transitions
            • Transitions-accept
            • Transitions-create
              • Create-signer-possiblep
              • Create-next
              • Create-endorsers-next
              • Create-endorsers-possiblep
              • Create-author-possiblep
              • Create-possiblep
              • Create-endorser-possiblep
              • Create-endorser-next
              • Create-author-next
            • Dags
            • Elections
            • Event-next
            • Transitions-commit
            • Event-possiblep
            • Events-possiblep
            • Events-next
            • Transitions-advance
            • Blockchains
            • Anchors
          • States
          • Events
      • 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-create

Create-endorsers-next

Update, in a system state, to a certificate's endorsers' states resulting from a create event.

Signature

(create-endorsers-next cert systate) → new-systate

Arguments

cert — Guard (certificatep cert).

systate — Guard (system-statep systate).

Returns

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

The input cert of this function is the certificate in the create event; see event.

We update the states of the correct endorsers. The faulty endorsers have no internal state.

Definitions and Theorems

Function: create-endorsers-next-loop

(defun create-endorsers-next-loop (cert endorsers systate)
  (declare (xargs :guard (and (certificatep cert)
                              (address-setp endorsers)
                              (system-statep systate))))
  (let ((__function__ 'create-endorsers-next-loop))
    (declare (ignorable __function__))
    (b* (((when (emptyp endorsers))
          (system-state-fix systate))
         (endorser (head endorsers))
         ((unless (in endorser (correct-addresses systate)))
          (create-endorsers-next-loop cert (tail endorsers)
                                      systate))
         (vstate (get-validator-state endorser systate))
         (new-vstate (create-endorser-next cert vstate))
         (new-systate
              (update-validator-state endorser new-vstate systate)))
      (create-endorsers-next-loop cert (tail endorsers)
                                  new-systate))))

Theorem: system-statep-of-create-endorsers-next-loop

(defthm system-statep-of-create-endorsers-next-loop
  (b* ((new-systate
            (create-endorsers-next-loop cert endorsers systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: create-endorsers-next-loop-of-system-state-fix-systate

(defthm create-endorsers-next-loop-of-system-state-fix-systate
 (equal
   (create-endorsers-next-loop cert
                               endorsers (system-state-fix systate))
   (create-endorsers-next-loop cert endorsers systate)))

Theorem: create-endorsers-next-loop-system-state-equiv-congruence-on-systate

(defthm
 create-endorsers-next-loop-system-state-equiv-congruence-on-systate
 (implies
  (system-state-equiv systate systate-equiv)
  (equal (create-endorsers-next-loop cert endorsers systate)
         (create-endorsers-next-loop cert endorsers systate-equiv)))
 :rule-classes :congruence)

Theorem: create-endorsers-next-loop-of-certificate-fix-cert

(defthm create-endorsers-next-loop-of-certificate-fix-cert
  (equal (create-endorsers-next-loop (certificate-fix cert)
                                     endorsers systate)
         (create-endorsers-next-loop cert endorsers systate)))

Theorem: create-endorsers-next-loop-certificate-equiv-congruence-on-cert

(defthm
    create-endorsers-next-loop-certificate-equiv-congruence-on-cert
 (implies
  (certificate-equiv cert cert-equiv)
  (equal (create-endorsers-next-loop cert endorsers systate)
         (create-endorsers-next-loop cert-equiv endorsers systate)))
 :rule-classes :congruence)

Theorem: correct-addresses-of-create-endorsers-next-loop

(defthm correct-addresses-of-create-endorsers-next-loop
  (b* ((?new-systate
            (create-endorsers-next-loop cert endorsers systate)))
    (equal (correct-addresses new-systate)
           (correct-addresses systate))))

Theorem: validator-state->round-of-create-endorsers-next-loop

(defthm validator-state->round-of-create-endorsers-next-loop
 (b* ((?new-systate
           (create-endorsers-next-loop cert endorsers systate)))
  (equal
      (validator-state->round (get-validator-state val new-systate))
      (validator-state->round (get-validator-state val systate)))))

Theorem: validator-state->dag-of-create-endorsers-next-loop

(defthm validator-state->dag-of-create-endorsers-next-loop
 (b* ((?new-systate
           (create-endorsers-next-loop cert endorsers systate)))
   (equal
        (validator-state->dag (get-validator-state val new-systate))
        (validator-state->dag (get-validator-state val systate)))))

Theorem: validator-state->endorsed-of-create-endorsers-next-loop

(defthm validator-state->endorsed-of-create-endorsers-next-loop
 (implies
  (in val (correct-addresses systate))
  (b* ((?new-systate
            (create-endorsers-next-loop cert endorsers systate)))
   (equal
    (validator-state->endorsed
         (get-validator-state val new-systate))
    (if
     (in val endorsers)
     (insert
      (make-address+pos :address (certificate->author cert)
                        :pos (certificate->round cert))
      (validator-state->endorsed (get-validator-state val systate)))
     (validator-state->endorsed
          (get-validator-state val systate)))))))

Theorem: validator-state->last-of-create-endorsers-next-loop

(defthm validator-state->last-of-create-endorsers-next-loop
 (b* ((?new-systate
           (create-endorsers-next-loop cert endorsers systate)))
  (equal
       (validator-state->last (get-validator-state val new-systate))
       (validator-state->last (get-validator-state val systate)))))

Theorem: validator-state->blockchain-of-create-endorsers-next-loop

(defthm validator-state->blockchain-of-create-endorsers-next-loop
  (b* ((?new-systate
            (create-endorsers-next-loop cert endorsers systate)))
    (equal (validator-state->blockchain
                (get-validator-state val new-systate))
           (validator-state->blockchain
                (get-validator-state val systate)))))

Theorem: validator-state->committed-of-create-endorsers-next-loop

(defthm validator-state->committed-of-create-endorsers-next-loop
 (b* ((?new-systate
           (create-endorsers-next-loop cert endorsers systate)))
  (equal
   (validator-state->committed
        (get-validator-state val new-systate))
   (validator-state->committed (get-validator-state val systate)))))

Theorem: get-network-state-of-create-endorsers-next-loop

(defthm get-network-state-of-create-endorsers-next-loop
  (b* ((?new-systate
            (create-endorsers-next-loop cert endorsers systate)))
    (equal (get-network-state new-systate)
           (get-network-state systate))))

Function: create-endorsers-next

(defun create-endorsers-next (cert systate)
  (declare (xargs :guard (and (certificatep cert)
                              (system-statep systate))))
  (let ((__function__ 'create-endorsers-next))
    (declare (ignorable __function__))
    (create-endorsers-next-loop cert (certificate->endorsers cert)
                                systate)))

Theorem: system-statep-of-create-endorsers-next

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

Theorem: correct-addresses-of-create-endorsers-next

(defthm correct-addresses-of-create-endorsers-next
  (b* ((?new-systate (create-endorsers-next cert systate)))
    (equal (correct-addresses new-systate)
           (correct-addresses systate))))

Theorem: validator-state->round-of-create-endorsers-next

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

Theorem: validator-state->dag-of-create-endorsers-next

(defthm validator-state->dag-of-create-endorsers-next
 (b* ((?new-systate (create-endorsers-next cert systate)))
   (equal
        (validator-state->dag (get-validator-state val new-systate))
        (validator-state->dag (get-validator-state val systate)))))

Theorem: validator-state->endorsed-of-create-endorsers-next

(defthm validator-state->endorsed-of-create-endorsers-next
 (implies
  (in val (correct-addresses systate))
  (b* ((?new-systate (create-endorsers-next cert systate)))
   (equal
    (validator-state->endorsed
         (get-validator-state val new-systate))
    (if
     (in val (certificate->endorsers cert))
     (insert
      (make-address+pos :address (certificate->author cert)
                        :pos (certificate->round cert))
      (validator-state->endorsed (get-validator-state val systate)))
     (validator-state->endorsed
          (get-validator-state val systate)))))))

Theorem: validator-state->last-of-create-endorsers-next

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

Theorem: validator-state->blockchain-of-create-endorsers-next

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

Theorem: validator-state->committed-of-create-endorsers-next

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

Theorem: get-network-state-of-create-endorsers-next

(defthm get-network-state-of-create-endorsers-next
  (b* ((?new-systate (create-endorsers-next cert systate)))
    (equal (get-network-state new-systate)
           (get-network-state systate))))

Theorem: create-endorsers-next-of-certificate-fix-cert

(defthm create-endorsers-next-of-certificate-fix-cert
  (equal (create-endorsers-next (certificate-fix cert)
                                systate)
         (create-endorsers-next cert systate)))

Theorem: create-endorsers-next-certificate-equiv-congruence-on-cert

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

Theorem: create-endorsers-next-of-system-state-fix-systate

(defthm create-endorsers-next-of-system-state-fix-systate
  (equal (create-endorsers-next cert (system-state-fix systate))
         (create-endorsers-next cert systate)))

Theorem: create-endorsers-next-system-state-equiv-congruence-on-systate

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