• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
        • Correctness
        • Definition
          • Transitions
          • Operations
          • States
          • Initialization
            • System-init
            • Validator-init
            • Validators-state-initp
            • System-state-initp
            • System-init-loop2
            • System-init-loop1
          • 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

• Initialization

System-init

Initial system state.

Signature

(system-init correct-vals faulty-vals) → systate

Arguments

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

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

Returns

systate — Type (system-statep systate).

The initial state of the sytem depends on the addresses of the correct validators and the addresses of the faulty validators; in fact, it is completely determined by them.

The initial map associates the initial validator state to each correct validator address, and nil to each faulty validator address. The initial network has no message.

Definitions and Theorems

Function: system-init-loop1

(defun system-init-loop1 (correct-vals)
 (declare (xargs :guard (address-setp correct-vals)))
 (let ((__function__ 'system-init-loop1))
  (declare (ignorable __function__))
  (cond
       ((emptyp correct-vals) nil)
       (t (omap::update (head correct-vals)
                        (validator-init)
                        (system-init-loop1 (tail correct-vals)))))))

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

(defthm validators-statep-of-system-init-loop1
  (implies (address-setp correct-vals)
           (b* ((map (system-init-loop1 correct-vals)))
             (validators-statep map)))
  :rule-classes :rewrite)

Function: system-init-loop2

(defun system-init-loop2 (faulty-vals)
 (declare (xargs :guard (address-setp faulty-vals)))
 (let ((__function__ 'system-init-loop2))
  (declare (ignorable __function__))
  (cond ((emptyp faulty-vals) nil)
        (t (omap::update (head faulty-vals)
                         nil
                         (system-init-loop2 (tail faulty-vals)))))))

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

(defthm validators-statep-of-system-init-loop2
  (implies (address-setp faulty-vals)
           (b* ((map (system-init-loop2 faulty-vals)))
             (validators-statep map)))
  :rule-classes :rewrite)

Function: system-init

(defun system-init (correct-vals faulty-vals)
  (declare (xargs :guard (and (address-setp correct-vals)
                              (address-setp faulty-vals))))
  (declare
       (xargs :guard (emptyp (intersect correct-vals faulty-vals))))
  (let ((__function__ 'system-init))
    (declare (ignorable __function__))
    (b* ((correct-map (system-init-loop1 correct-vals))
         (faulty-map (system-init-loop2 faulty-vals))
         (vstates (omap::update* correct-map faulty-map)))
      (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 faulty-vals)))
    (system-statep systate))
  :rule-classes :rewrite)