• 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
              • Timer-expires-next
              • Timer-expires-possiblep
            • Transitions-commit-anchors
            • Transitions-advance-round
          • Operations
          • States
          • Initialization
          • Events
      • Aleobft-stake2
      • Aleobft-dynamic
      • 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
    • Riscv
    • Yul
    • 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-timer-expires

Timer-expires-next

New state resulting from a timer-expires event.

Signature

(timer-expires-next val systate) → new-systate

Arguments

val — Guard (addressp val).

systate — Guard (system-statep systate).

Returns

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

The timer state is set to expired. Recall that we do not model real time here, just the sequences of events that may happen in the system.

Definitions and Theorems

Function: timer-expires-next-val

(defun timer-expires-next-val (vstate)
  (declare (xargs :guard (validator-statep vstate)))
  (let ((__function__ 'timer-expires-next-val))
    (declare (ignorable __function__))
    (change-validator-state vstate
                            :timer (timer-expired))))

Theorem: validator-statep-of-timer-expires-next-val

(defthm validator-statep-of-timer-expires-next-val
  (b* ((new-vstate (timer-expires-next-val vstate)))
    (validator-statep new-vstate))
  :rule-classes :rewrite)

Function: timer-expires-next

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

Theorem: system-statep-of-timer-expires-next

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

Theorem: timer-expires-next-of-system-state-fix-systate

(defthm timer-expires-next-of-system-state-fix-systate
  (equal (timer-expires-next val (system-state-fix systate))
         (timer-expires-next val systate)))

Theorem: timer-expires-next-system-state-equiv-congruence-on-systate

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

Theorem: validator-state->round-of-timer-expires-next

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

Theorem: validator-state->dag-of-timer-expires-next

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

Theorem: validator-state->last-of-timer-expires-next

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

Theorem: validator-state->blockchain-of-timer-expires-next

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

Theorem: validator-state->committed-of-timer-expires-next

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