		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash-bound-properties

Pedersen-segment-scalar-not-zero-proof

Proof that pedersen-segment-scalar is not 0.

This is proved by first proving that the loop function is outside the interval between -2^{4\cdot(j-1)} to 2^{4\cdot(j-1)}, both exclusive. Setting j=1, we have that pedersen-segment-scalar is outside the interval from -1 to 1 exclusive, i.e. it is not 0. To prove the lemma about the loop function, to avoid dealing with a disjunction of inequalities, we introduce a predicate for being outside the interval and we prove some theorems about it. Some of these theorems are currently somewhat specific; perhaps there is a way to improve the form of the proof.

The fact, mentioned above, that the loop function is outside a certain interval is also useful to prove other properties. Thus, we export a theorem asserting that.

Definitions and Theorems

Theorem: pedersen-segment-scalar-loop-outside-interval

(defthm pedersen-segment-scalar-loop-outside-interval
  (implies (and (posp j)
                (bit-listp segment)
                (integerp (/ (len segment) 3))
                (consp segment))
           (or (<= (pedersen-segment-scalar-loop j segment)
                   (- (expt 2 (+ -4 (* 4 j)))))
               (<= (expt 2 (+ -4 (* 4 j)))
                   (pedersen-segment-scalar-loop j segment)))))

Theorem: pedersen-segment-scalar-not-zero

(defthm pedersen-segment-scalar-not-zero
  (implies (and (bit-listp segment)
                (integerp (/ (len segment) 3))
                (consp segment))
           (not (equal (pedersen-segment-scalar segment)
                       0)))
  :rule-classes :type-prescription)