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

Calculate an 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 is determined by the addresses of the correct validators and the addresses of the faulty validators. The guard requires the disjointness of the addresses of correct and faulty validators and the inclusion of the genesis committee addresses in the union of the addresses.

Definitions and Theorems

Function: system-init-loop1

(defun system-init-loop1 (correct-vals vstates)
  (declare (xargs :guard (and (address-setp correct-vals)
                              (validators-statep vstates))))
  (let ((__function__ 'system-init-loop1))
    (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-loop1 (tail correct-vals)
                         vstates))))

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

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

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

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

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

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

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

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

Theorem: keys-of-system-init-loop1

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

Theorem: correct-addresses-loop-of-system-init-loop1

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

Theorem: lookup-of-system-init-loop1

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

Function: system-init-loop2

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

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

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

Theorem: system-init-loop2-of-address-set-fix-faulty-vals

(defthm system-init-loop2-of-address-set-fix-faulty-vals
  (equal (system-init-loop2 (address-set-fix faulty-vals)
                            vstates)
         (system-init-loop2 faulty-vals vstates)))

Theorem: system-init-loop2-address-set-equiv-congruence-on-faulty-vals

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

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

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

Theorem: keys-of-system-init-loop2

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

Theorem: correct-addresses-loop-of-system-init-loop2

(defthm correct-addresses-loop-of-system-init-loop2
 (implies
  (and (validators-statep vstates)
       (not (intersect (address-set-fix faulty-vals)
                       (omap::keys vstates))))
  (equal
    (correct-addresses-loop (system-init-loop2 faulty-vals vstates))
    (correct-addresses-loop vstates))))

Theorem: lookup-of-system-init-loop2

(defthm lookup-of-system-init-loop2
  (implies
       (validators-statep vstates)
       (equal (omap::lookup val
                            (system-init-loop2 faulty-vals vstates))
              (if (in val (address-set-fix faulty-vals))
                  nil
                (omap::lookup val vstates)))))

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 (and (emptyp (intersect correct-vals faulty-vals))
                     (subset (committee-members (genesis-committee))
                             (union correct-vals faulty-vals)))))
 (let ((__function__ 'system-init))
   (declare (ignorable __function__))
   (b* ((vstates nil)
        (vstates (system-init-loop1 correct-vals vstates))
        (vstates (system-init-loop2 faulty-vals vstates)))
     (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)

Theorem: system-initp-of-system-init

(defthm system-initp-of-system-init
  (implies (and (address-setp correct-vals)
                (address-setp faulty-vals)
                (subset (committee-members (genesis-committee))
                        (union correct-vals faulty-vals))
                (not (intersect correct-vals faulty-vals)))
           (system-initp (system-init correct-vals faulty-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)
                      faulty-vals)
         (system-init correct-vals faulty-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 faulty-vals)
                  (system-init correct-vals-equiv faulty-vals)))
  :rule-classes :congruence)

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

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

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

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