Pedersen-segment-point
The function \mathcal{I} in [ZPS:5.4.1.7].
- Signature
(pedersen-segment-point d i) → point?
- Arguments
- d — Guard (byte-listp d).
- i — Guard (posp i).
- Returns
- point? — Type (maybe-jubjub-pointp point?).
This returns a Jubjub point from (the index of) a segment.
However, find-group-hash may return nil,
so we need to allow that case here.
[ZPS] does not explicitly handle that case,
perhaps because it is not going to happen with overwhelming probability.
We need to turn the index i, diminished by one,
into a byte sequence consisting of 32 bits, i.e. 4 bytes.
The first paragraph of [ZPS:5.1] says that, unless otherwise specified,
integers are unsigned, fixed-length, and encoded in little endian bytes;
thus, we take the little endian byte representation of i-1.
Definitions and Theorems
Function: pedersen-segment-point
(defun pedersen-segment-point (d i)
(declare (xargs :guard (and (byte-listp d) (posp i))))
(declare (xargs :guard (= (len d) 8)))
(let ((__function__ 'pedersen-segment-point))
(declare (ignorable __function__))
(b* ((i1 (1- i))
(i1-32bit (mod i1 (expt 2 32)))
(m (acl2::nat=>lebytes 4 i1-32bit)))
(find-group-hash d m))))
Theorem: maybe-jubjub-pointp-of-pedersen-segment-point
(defthm maybe-jubjub-pointp-of-pedersen-segment-point
(b* ((point? (pedersen-segment-point d i)))
(maybe-jubjub-pointp point?))
:rule-classes :rewrite)
