		Search-engine friendly clone of the ACL2 documentation.

Unequivocal-dags-def-and-init

Unequivocal-dags-p

Definition of the invariant: the DAGs of each pair of correct validators are mutually unequivocal.

We prove that this invariant, which is defined as non-equivocation for two validators, implies non-equivocation for a single validator. This is similar to the -necc rule generated by the definition, but it involves a single validator; this similarity is the reason for the name of the rule.

Definitions and Theorems

Theorem: unequivocal-dags-p-necc

(defthm unequivocal-dags-p-necc
 (implies
  (unequivocal-dags-p systate)
  (implies
   (and (in val1 (correct-addresses systate))
        (in val2 (correct-addresses systate)))
   (certificate-sets-unequivocalp
       (validator-state->dag (get-validator-state val1 systate))
       (validator-state->dag (get-validator-state val2 systate))))))

Theorem: booleanp-of-unequivocal-dags-p

(defthm booleanp-of-unequivocal-dags-p
  (b* ((yes/no (unequivocal-dags-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: unequivocal-dags-p-of-system-state-fix-systate

(defthm unequivocal-dags-p-of-system-state-fix-systate
  (equal (unequivocal-dags-p (system-state-fix systate))
         (unequivocal-dags-p systate)))

Theorem: unequivocal-dags-p-system-state-equiv-congruence-on-systate

(defthm unequivocal-dags-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (unequivocal-dags-p systate)
                  (unequivocal-dags-p systate-equiv)))
  :rule-classes :congruence)

Theorem: unequivocal-dags-p-necc-single

(defthm unequivocal-dags-p-necc-single
 (implies
    (and (unequivocal-dags-p systate)
         (in val (correct-addresses systate)))
    (certificate-set-unequivocalp
         (validator-state->dag (get-validator-state val systate)))))