The addend point in the definition of
(pedersen-segment-addend d segment i) → point?
(defun pedersen-segment-addend (d segment i) (declare (xargs :guard (and (byte-listp d) (bit-listp segment) (posp i)))) (declare (xargs :guard (and (= (len d) 8) (integerp (/ (len segment) 3))))) (let ((__function__ 'pedersen-segment-addend)) (declare (ignorable __function__)) (b* ((ipoint (pedersen-segment-point d i)) ((unless (jubjub-pointp ipoint)) nil) (scalar (pedersen-segment-scalar segment))) (jubjub-mul scalar ipoint))))
(defthm maybe-jubjub-pointp-of-pedersen-segment-addend (b* ((point? (pedersen-segment-addend d segment i))) (maybe-jubjub-pointp point?)) :rule-classes :rewrite)