• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-dynamic
      • Aleobft-stake2
      • Aleobft-stake
        • Correctness
        • Definition
          • Initialization
            • System-init
            • System-init-loop
            • Validator-init
            • System-initp
            • System-validators-initp
          • Transitions
          • States
          • Events
      • 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

• Initialization

System-init

Calculate an initial system state.

Signature

(system-init correct-vals) → systate

Arguments

correct-vals — Guard (address-setp correct-vals).

Returns

systate — Type (system-statep systate).

The initial state of the sytem is determined by the addresses of the correct validators.

We prove that every system state calculated by this function satisfies the predicate that characterized initial states.

Definitions and Theorems

Function: system-init-loop

(defun system-init-loop (correct-vals vstates)
  (declare (xargs :guard (and (address-setp correct-vals)
                              (validators-statep vstates))))
  (let ((__function__ 'system-init-loop))
    (declare (ignorable __function__))
    (b* (((when (or (not (mbt (address-setp correct-vals)))
                    (emptyp correct-vals)))
          (validators-state-fix vstates))
         (vstates (omap::update (head correct-vals)
                                (validator-init)
                                vstates)))
      (system-init-loop (tail correct-vals)
                        vstates))))

Theorem: validators-statep-of-system-init-loop

(defthm validators-statep-of-system-init-loop
  (implies
       (validators-statep vstates)
       (b* ((new-vstates (system-init-loop correct-vals vstates)))
         (validators-statep new-vstates)))
  :rule-classes :rewrite)

Theorem: system-init-loop-of-address-set-fix-correct-vals

(defthm system-init-loop-of-address-set-fix-correct-vals
  (equal (system-init-loop (address-set-fix correct-vals)
                           vstates)
         (system-init-loop correct-vals vstates)))

Theorem: system-init-loop-address-set-equiv-congruence-on-correct-vals

(defthm
      system-init-loop-address-set-equiv-congruence-on-correct-vals
  (implies (address-set-equiv correct-vals correct-vals-equiv)
           (equal (system-init-loop correct-vals vstates)
                  (system-init-loop correct-vals-equiv vstates)))
  :rule-classes :congruence)

Theorem: in-of-keys-of-system-init-loop

(defthm in-of-keys-of-system-init-loop
 (implies
    (validators-statep vstates)
    (equal (in val
               (omap::keys (system-init-loop correct-vals vstates)))
           (or (in val (address-set-fix correct-vals))
               (in val (omap::keys vstates))))))

Theorem: keys-of-system-init-loop

(defthm keys-of-system-init-loop
  (implies
       (validators-statep vstates)
       (equal (omap::keys (system-init-loop correct-vals vstates))
              (union (address-set-fix correct-vals)
                     (omap::keys vstates)))))

Theorem: lookup-of-system-init-loop

(defthm lookup-of-system-init-loop
  (implies
       (validators-statep vstates)
       (equal (omap::lookup val
                            (system-init-loop correct-vals vstates))
              (if (in val (address-set-fix correct-vals))
                  (validator-init)
                (omap::lookup val vstates)))))

Function: system-init

(defun system-init (correct-vals)
  (declare (xargs :guard (address-setp correct-vals)))
  (let ((__function__ 'system-init))
    (declare (ignorable __function__))
    (b* ((vstates (system-init-loop correct-vals nil)))
      (make-system-state :validators vstates
                         :network nil))))

Theorem: system-statep-of-system-init

(defthm system-statep-of-system-init
  (b* ((systate (system-init correct-vals)))
    (system-statep systate))
  :rule-classes :rewrite)

Theorem: system-initp-of-system-init

(defthm system-initp-of-system-init
  (system-initp (system-init correct-vals)))

Theorem: system-init-of-address-set-fix-correct-vals

(defthm system-init-of-address-set-fix-correct-vals
  (equal (system-init (address-set-fix correct-vals))
         (system-init correct-vals)))

Theorem: system-init-address-set-equiv-congruence-on-correct-vals

(defthm system-init-address-set-equiv-congruence-on-correct-vals
  (implies (address-set-equiv correct-vals correct-vals-equiv)
           (equal (system-init correct-vals)
                  (system-init correct-vals-equiv)))
  :rule-classes :congruence)