• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Aleobft
      • Aleobft-static
      • Aleobft-stake2
      • Aleobft-dynamic
      • Aleobft-stake
      • Aleobft-proposals
        • Definition
          • Initialization
            • System-init
            • System-init-loop
            • System-initp
            • Validator-init
            • System-validators-initp
          • Transitions
          • States
          • Events
          • Reachability
        • Correctness
      • Library-extensions
    • Acre
    • Milawa
    • Smtlink
    • 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
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • 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

• 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 valmap)
  (declare
       (xargs :guard (and (address-setp correct-vals)
                          (address-validator-state-mapp valmap))))
  (let ((__function__ 'system-init-loop))
    (declare (ignorable __function__))
    (b* (((when (emptyp (address-set-fix correct-vals)))
          (address-validator-state-map-fix valmap))
         (valmap (omap::update (head correct-vals)
                               (validator-init)
                               valmap)))
      (system-init-loop (tail correct-vals)
                        valmap))))

Theorem: address-validator-state-mapp-of-system-init-loop

(defthm address-validator-state-mapp-of-system-init-loop
  (implies (address-validator-state-mapp valmap)
           (b* ((new-valmap (system-init-loop correct-vals valmap)))
             (address-validator-state-mapp new-valmap)))
  :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)
                           valmap)
         (system-init-loop correct-vals valmap)))

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 valmap)
                  (system-init-loop correct-vals-equiv valmap)))
  :rule-classes :congruence)

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

(defthm in-of-keys-of-system-init-loop
 (implies
     (address-validator-state-mapp valmap)
     (equal (in val
                (omap::keys (system-init-loop correct-vals valmap)))
            (or (in val (address-set-fix correct-vals))
                (in val (omap::keys valmap))))))

Theorem: keys-of-system-init-loop

(defthm keys-of-system-init-loop
 (implies (address-validator-state-mapp valmap)
          (equal (omap::keys (system-init-loop correct-vals valmap))
                 (union (address-set-fix correct-vals)
                        (omap::keys valmap)))))

Theorem: lookup-of-system-init-loop

(defthm lookup-of-system-init-loop
  (implies
       (address-validator-state-mapp valmap)
       (equal (omap::lookup val
                            (system-init-loop correct-vals valmap))
              (if (in val (address-set-fix correct-vals))
                  (validator-init)
                (omap::lookup val valmap)))))

Function: system-init

(defun system-init (correct-vals)
  (declare (xargs :guard (address-setp correct-vals)))
  (let ((__function__ 'system-init))
    (declare (ignorable __function__))
    (b* ((valmap (system-init-loop correct-vals nil)))
      (make-system-state :validators valmap
                         :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)