		Search-engine friendly clone of the ACL2 documentation.

Committed-anchor-sequences

Committed-anchors-of-next

How the sequence of committed anchors in a validator state changes (or not) for each transition.

A create or accept event does not change the last committed anchor or the blockchain, but it extends the DAG. However, given that collect-all-anchors is stable under DAG extension as already proved in collect-all-anchors-of-unequivocal-superdag, there is no change to the sequence of committed anchors. To discharge the hypothesis of that theorem, saying that the extended DAG is unequivocal, we use the already proved theorem that DAG non-equivocation is preserved by these events.

A commit event is the only kind that changes the sequence of committed anchors (for the target validator), by extending them with a suitable call of collect-anchors. The proof takes a little work. We distinguish the case of the target validator from the case of another validator (which is easy), and within the first case we consider two sub-cases based on whether the last committed round was 0 or not. The case in which it is 0 is relatively simple, because the second argument of the append is nil, since no anchors have been committed yet; we open collect-all-anchors, and we need to simplify away the blockchain extension via the theorem collect-anchors-of-extend-blockchain-no-change, which involved other rules to relieve its hypotheses. The sub-cases in which there are already some committed anchors is the more complex; the most important theorem used there is collect-all-anchors-to-append-of-collect-anchors, and again we need rules to simplify away the blockchain extension. In both sub-cases, the blockchain extension arises from the definition of committed-anchors.

An advance event does not modify the DAG or the blockchain or the last committed round or the last anchor, and thus it is easy to prove that the sequence of committed anchors does not change.

Definitions and Theorems

Theorem: committed-anchors-of-create-next

(defthm committed-anchors-of-create-next
 (implies
   (and (system-committees-fault-tolerant-p systate)
        (backward-closed-p systate)
        (no-self-endorsed-p systate)
        (signer-records-p systate)
        (signer-quorum-p systate)
        (unequivocal-dags-p systate)
        (same-committees-p systate)
        (last-anchor-present-p systate)
        (in val (correct-addresses systate))
        (create-possiblep cert systate))
   (equal (committed-anchors
               (get-validator-state val (create-next cert systate)))
          (committed-anchors (get-validator-state val systate)))))

Theorem: committed-anchors-of-accept-next

(defthm committed-anchors-of-accept-next
 (implies
    (and (system-committees-fault-tolerant-p systate)
         (backward-closed-p systate)
         (signer-quorum-p systate)
         (unequivocal-signed-certs-p systate)
         (unequivocal-dags-p systate)
         (same-committees-p systate)
         (last-anchor-present-p systate)
         (in val (correct-addresses systate))
         (accept-possiblep msg systate)
         (messagep msg))
    (equal (committed-anchors
                (get-validator-state val (accept-next msg systate)))
           (committed-anchors (get-validator-state val systate)))))

Theorem: committed-anchors-of-advance-next

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

Theorem: committed-anchors-of-commit-next-last-not-0

(defthm committed-anchors-of-commit-next-last-not-0
 (implies
  (and
   (last-blockchain-round-p systate)
   (ordered-blockchain-p systate)
   (signer-quorum-p systate)
   (unequivocal-dags-p systate)
   (last-anchor-present-p systate)
   (omni-paths-p systate)
   (in val (correct-addresses systate))
   (commit-possiblep val systate)
   (not
    (equal (validator-state->last (get-validator-state val systate))
           0)))
  (equal
   (committed-anchors
        (get-validator-state val (commit-next val systate)))
   (b* (((validator-state vstate)
         (get-validator-state val systate))
        (round (1- vstate.round))
        (commtt (active-committee-at-round round vstate.blockchain))
        (leader (leader-at-round round commtt))
        (anchor (cert-with-author+round leader round vstate.dag))
        (anchors (collect-anchors anchor (- round 2)
                                  vstate.last
                                  vstate.dag vstate.blockchain)))
     (append
          anchors
          (committed-anchors (get-validator-state val systate)))))))

Theorem: committed-anchors-of-commit-next-last-0

(defthm committed-anchors-of-commit-next-last-0
 (implies
  (and
    (last-blockchain-round-p systate)
    (ordered-blockchain-p systate)
    (signer-quorum-p systate)
    (unequivocal-dags-p systate)
    (last-anchor-present-p systate)
    (omni-paths-p systate)
    (in val (correct-addresses systate))
    (commit-possiblep val systate)
    (equal (validator-state->last (get-validator-state val systate))
           0))
  (equal
   (committed-anchors
        (get-validator-state val (commit-next val systate)))
   (b* (((validator-state vstate)
         (get-validator-state val systate))
        (round (1- vstate.round))
        (commtt (active-committee-at-round round vstate.blockchain))
        (leader (leader-at-round round commtt))
        (anchor (cert-with-author+round leader round vstate.dag))
        (anchors (collect-anchors anchor (- round 2)
                                  vstate.last
                                  vstate.dag vstate.blockchain)))
     (append
          anchors
          (committed-anchors (get-validator-state val systate)))))))

Theorem: committed-anchors-of-commit-next-other-val

(defthm committed-anchors-of-commit-next-other-val
 (implies
   (and (last-blockchain-round-p systate)
        (ordered-blockchain-p systate)
        (signer-quorum-p systate)
        (unequivocal-dags-p systate)
        (last-anchor-present-p systate)
        (omni-paths-p systate)
        (in val1 (correct-addresses systate))
        (commit-possiblep val systate)
        (addressp val)
        (not (equal val1 val)))
   (equal (committed-anchors
               (get-validator-state val1 (commit-next val systate)))
          (committed-anchors (get-validator-state val1 systate)))))

Theorem: committed-anchors-of-commit-next

(defthm committed-anchors-of-commit-next
 (implies
  (and (last-blockchain-round-p systate)
       (ordered-blockchain-p systate)
       (signer-quorum-p systate)
       (unequivocal-dags-p systate)
       (last-anchor-present-p systate)
       (omni-paths-p systate)
       (in val1 (correct-addresses systate))
       (commit-possiblep val systate)
       (addressp val))
  (equal
    (committed-anchors
         (get-validator-state val1 (commit-next val systate)))
    (if
     (equal val1 (address-fix val))
     (b*
       (((validator-state vstate)
         (get-validator-state val1 systate))
        (round (1- vstate.round))
        (commtt (active-committee-at-round round vstate.blockchain))
        (leader (leader-at-round round commtt))
        (anchor (cert-with-author+round leader round vstate.dag))
        (anchors (collect-anchors anchor (- round 2)
                                  vstate.last
                                  vstate.dag vstate.blockchain)))
       (append
            anchors
            (committed-anchors (get-validator-state val1 systate))))
     (committed-anchors (get-validator-state val1 systate))))))