Bound on the value of pedersen-segment-scalar.
Theorem 5.4.1 in [ZPS:5.4.1.7] defines @$(\Delta$) as
a bound on the value of the encoding function
Based on the summation that defines
To prove that these are actual bounds,
we start with a proof by induction for the recursive function and bound.
We need a lemma about the length of
Function:
(defun pedersen-segment-scalar-loop-bound (j segment) (declare (xargs :guard (and (posp j) (bit-listp segment)))) (declare (xargs :guard (integerp (/ (len segment) 3)))) (let ((__function__ 'pedersen-segment-scalar-loop-bound)) (declare (ignorable __function__)) (if (consp segment) (+ (* 4 (expt 2 (* 4 (1- j)))) (pedersen-segment-scalar-loop-bound (1+ j) (nthcdr 3 segment))) 0)))
Theorem:
(defthm natp-of-pedersen-segment-scalar-loop-bound (implies (posp j) (b* ((bound (pedersen-segment-scalar-loop-bound j segment))) (natp bound))) :rule-classes :rewrite)
Function:
(defun pedersen-segment-scalar-bound (segment) (declare (xargs :guard (bit-listp segment))) (declare (xargs :guard (integerp (/ (len segment) 3)))) (let ((__function__ 'pedersen-segment-scalar-bound)) (declare (ignorable __function__)) (pedersen-segment-scalar-loop-bound 1 segment)))
Theorem:
(defthm natp-of-pedersen-segment-scalar-bound (b* ((bound (pedersen-segment-scalar-bound segment))) (natp bound)) :rule-classes :rewrite)
Theorem:
(defthm pedersen-segment-scalar-loop-upper-bound (implies (and (posp j) (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (pedersen-segment-scalar-loop j segment) (pedersen-segment-scalar-loop-bound j segment))) :rule-classes :linear)
Theorem:
(defthm pedersen-segment-scalar-loop-lower-bound (implies (and (posp j) (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (- (pedersen-segment-scalar-loop-bound j segment)) (pedersen-segment-scalar-loop j segment))) :rule-classes :linear)
Theorem:
(defthm pedersen-segment-scalar-upper-bound (implies (and (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (pedersen-segment-scalar segment) (pedersen-segment-scalar-bound segment))) :rule-classes :linear)
Theorem:
(defthm pedersen-segment-scalar-lower-bound (implies (and (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (- (pedersen-segment-scalar-bound segment)) (pedersen-segment-scalar segment))) :rule-classes :linear)