		Search-engine friendly clone of the ACL2 documentation.

Zcash

Pedersen-hash

A formalization of Zcash's Pedersen hash.

This is described in [ZPS:5.4.1.7], which refers to several other parts of [ZPS]. We may split this file and XDOC topic into multiple ones that correspond to different parts of [ZPS], but for now we put here everything needed to define Pedersen hash.

Subtopics

Pedersen-segment-scalar: The function \langle\cdot\rangle in [ZPS:5.4.1.7].
Pedersen-segment-point: The function \mathcal{I} in [ZPS:5.4.1.7].
Find-group-hash: The function \mathsf{FindGroupHash^{\mathbb{J}^{(r)*}}} [ZPS:5.4.9.5].
Pedersen-point: The function \mathsf{PedersenHashToPoint} [ZPS:5.4.1.7].
Pedersen-enc: The function \mathsf{enc} in [ZPS:5.4.1.7].
Group-hash: The function \mathsf{GroupHash_\mathsf{URS}^{\mathbb{J}^{(r)*}}} [ZPS:5.4.9.5].
Coordinate-extract: The function \mathsf{Extract}_{\mathbb{J}^{(r)}} [ZPS:5.4.9.4].
Pedersen-segment-addend: The addend point in the definition of \mathsf{PedersenHashToPoint} [ZPS:5.4.1.7].
Pedersen: The function \mathsf{PedersenHash} [ZPS:5.4.1.7].
Pedersen-pad: Pedersen hash padding [ZPS:5.4.1.7].
Pedersen-hash-injectivity-properties: Injectivity of pedersen-segment-scalar.
Pedersen-hash-bound-properties: Some properties about bounds of pedersen-segment-scalar.
Pedersen-hash-image-properties: Some properties about the image of pedersen.
*pedersen-c*: The constant c in [ZPS:5.4.1.7].