		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash-bound-properties

Pedersen-segment-scalar-bound

Bound on the value of pedersen-segment-scalar.

Signature
(pedersen-segment-scalar-bound segment) → bound
Arguments: segment — Guard (bit-listp segment).
Returns: bound — Type (natp bound).

Theorem 5.4.1 in [ZPS:5.4.1.7] defines @$(\Delta$) as a bound on the value of the encoding function \langle\cdot\rangle: the value of the function is between -\Delta and \Delta. In [ZPS], \Delta is a constant because \langle\cdot\rangle is defined over segments of maximum size 3c. However, our pedersen-segment-scalar is more generally defined over segments of any length that is a multiple of 3. Accordingly, we define a function that expresses \Delta in terms of (the length of) the segment. Since pedersen-segment-scalar is defined in terms of an auxiliary recursive function that is defined even more generally over not only a segment of length multiple of 3 but also the index j of the chunk of 3 bits, we also introduce a function that expresses the bound on the recursive function.

Based on the summation that defines \Delta in [ZPS], we define the bound for the recursive function by recursively adding 4\cdot2^{4\cdot(j-1)} while j is incremented until there is no 3-bit chunk left. The bound for pedersen-segment-scalar is obtained from that by setting j to 1.

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 (nthcdr 3 x) being a multiple of 3 when the length of x is: this serves to relieve the hypothesis of the induction hypothesis. We also need a lemma saying that (take 3 segment) is a list of bits under the hypothesis of the theorem: this is needed for the base case, to relieve the hypothesis of the bound rules of pedersen-enc. (These two lemmas are at the beginning of this file.) We also need a few arithmetic lemmas to nudge the proof in the right direction. (These arithmetic lemmas are below.) With linear bound rules for the recursive function in hand, the bound proofs for pedersen-segment-scalar are automatic.

Definitions and Theorems

Function: pedersen-segment-scalar-loop-bound

(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: natp-of-pedersen-segment-scalar-loop-bound

(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: pedersen-segment-scalar-bound

(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: natp-of-pedersen-segment-scalar-bound

(defthm natp-of-pedersen-segment-scalar-bound
  (b* ((bound (pedersen-segment-scalar-bound segment)))
    (natp bound))
  :rule-classes :rewrite)

Theorem: pedersen-segment-scalar-loop-upper-bound

(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: pedersen-segment-scalar-loop-lower-bound

(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: pedersen-segment-scalar-upper-bound

(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: pedersen-segment-scalar-lower-bound

(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)