|
|
|---|
|
|
|
|---|
Assumption of associativity of Montgomery addition.
We plan to prove the associativity of montgomery-add, but since that will take substantial work (the proof is notoriously laborious), for now we capture the associtivity property in this nullary predicate, which we can use as hypothesis in theorems whose proof needs associativity. This is preferable to stating an axiom, because an incorrect axiom (either because it is misstated or because addition is misdefined) would make the logic inconsistent. In contrast, if this nullary predicate is actually false (due to the same kind of mistake mentioned just above), it just means that any theorem with it as hypothesis is vacuous (a much less severe problem).
We enable the rewrite rule associated to this defun-sk because it is essentially the associativity theorem, which is a good rewrite rule to have enabled, with the only difference that it has this nullary predicate as hypothesis. That rewrite rules rewrites additions to associate to the right. We also add a disabled associativity rule that rewrites additions to associate to the left instead; this may be occasionally useful in algebraic manipulations. We add a theory invariant preventing both rules from being enabled.
Note that we need to assume the closure of addition, in the guard, in order to verify the guards of this function.
Theorem:
(defthm montgomery-add-associative-right (implies (montgomery-add-associativity) (implies (and (point-on-montgomery-p point1 curve) (point-on-montgomery-p point2 curve) (point-on-montgomery-p point3 curve)) (equal (montgomery-add (montgomery-add point1 point2 curve) point3 curve) (montgomery-add point1 (montgomery-add point2 point3 curve) curve)))))
Theorem:
(defthm booleanp-of-montgomery-add-associativity (b* ((yes/no (montgomery-add-associativity))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm montgomery-add-associative-left (implies (and (montgomery-add-associativity) (point-on-montgomery-p point1 curve) (point-on-montgomery-p point2 curve) (point-on-montgomery-p point3 curve)) (equal (montgomery-add point1 (montgomery-add point2 point3 curve) curve) (montgomery-add (montgomery-add point1 point2 curve) point3 curve))))