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