• 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
              • Store-certificate-next
              • Store-certificate-possiblep
            • Transitions-receive-certificate
            • Transitions-create-certificate
            • Transitions-timer-expires
            • Transitions-commit-anchors
            • 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-store-certificate

Store-certificate-next

New state resulting from a store-certificate event.

Signature

(store-certificate-next cert val systate) → new-systate

Arguments

cert — Guard (certificatep cert).

val — Guard (addressp val).

systate — Guard (system-statep systate).

Returns

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

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. Further advancement to the certificate's round is handled in a separate event, namely advance-round.

The network is unaffected.

Definitions and Theorems

Function: store-certificate-next-val

(defun store-certificate-next-val (cert vstate)
  (declare (xargs :guard (and (certificatep cert)
                              (validator-statep vstate))))
  (let ((__function__ 'store-certificate-next-val))
    (declare (ignorable __function__))
    (b* (((certificate cert) cert)
         (buffer (validator-state->buffer vstate))
         (dag (validator-state->dag vstate))
         (round (validator-state->round vstate))
         (new-buffer (delete cert buffer))
         (new-dag (insert cert dag))
         (new-round (if (> cert.round (1+ round))
                        (1- cert.round)
                      round)))
      (change-validator-state vstate
                              :buffer new-buffer
                              :dag new-dag
                              :round new-round))))

Theorem: validator-statep-of-store-certificate-next-val

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

Function: store-certificate-next

(defun store-certificate-next (cert val systate)
 (declare (xargs :guard (and (certificatep cert)
                             (addressp val)
                             (system-statep systate))))
 (declare
      (xargs :guard (store-certificate-possiblep cert val systate)))
 (let ((__function__ 'store-certificate-next))
   (declare (ignorable __function__))
   (b* ((vstate (get-validator-state val systate))
        (new-vstate (store-certificate-next-val cert vstate)))
     (update-validator-state val new-vstate systate))))

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

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

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

(defthm store-certificate-next-of-system-state-fix-systate
 (equal (store-certificate-next cert val (system-state-fix systate))
        (store-certificate-next cert val 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 cert val systate)
                  (store-certificate-next cert val systate-equiv)))
  :rule-classes :congruence)

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

(defthm validator-state->round-of-store-certificate-next
 (implies
  (and (in val (correct-addresses systate))
       (store-certificate-possiblep cert val1 systate))
  (equal
   (validator-state->round
        (get-validator-state
             val
             (store-certificate-next cert val1 systate)))
   (if
    (and
     (equal val val1)
     (>
      (certificate->round cert)
      (1+
       (validator-state->round (get-validator-state val systate)))))
    (1- (certificate->round cert))
    (validator-state->round (get-validator-state val systate))))))

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

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

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

(defthm validator-state->dag-subset-store-certificate-next
 (implies
   (and (in val (correct-addresses systate))
        (store-certificate-possiblep cert val1 systate))
   (subset (validator-state->dag (get-validator-state val systate))
           (validator-state->dag
                (get-validator-state
                     val
                     (store-certificate-next cert val1 systate))))))

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

(defthm validator-state->dag-of-store-certificate-next-same
 (implies
  (and (in val (correct-addresses systate))
       (store-certificate-possiblep cert val1 systate)
       (not (equal val val1)))
  (equal (validator-state->dag
              (get-validator-state
                   val
                   (store-certificate-next cert val1 systate)))
         (validator-state->dag (get-validator-state val systate)))))

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

(defthm validator-state->last-of-store-certificate-next
 (implies
   (and (in val (correct-addresses systate))
        (store-certificate-possiblep cert val1 systate))
   (equal
        (validator-state->last
             (get-validator-state
                  val
                  (store-certificate-next cert val1 systate)))
        (validator-state->last (get-validator-state val systate)))))

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

(defthm validator-state->blockchain-of-store-certificate-next
  (implies
       (and (in val (correct-addresses systate))
            (store-certificate-possiblep cert val1 systate))
       (equal (validator-state->blockchain
                   (get-validator-state
                        val
                        (store-certificate-next cert val1 systate)))
              (validator-state->blockchain
                   (get-validator-state val systate)))))

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

(defthm validator-state->committed-of-store-certificate-next
 (implies
  (and (in val (correct-addresses systate))
       (store-certificate-possiblep cert val1 systate))
  (equal
   (validator-state->committed
        (get-validator-state
             val
             (store-certificate-next cert val1 systate)))
   (validator-state->committed (get-validator-state val systate)))))