Module 0x1::ristretto255

This module contains functions for Ristretto255 curve arithmetic, assuming addition as the group operation.

The order of the Ristretto255 elliptic curve group is $\ell = 2^252 + 27742317777372353535851937790883648493$, same as the order of the prime-order subgroup of Curve25519.

This module provides two structs for encoding Ristretto elliptic curves to the developer:

• First, a 32-byte-sized CompressedRistretto struct, which is used to persist points in storage.

• Second, a larger, in-memory, RistrettoPoint struct, which is decompressable from a CompressedRistretto struct. This larger struct can be used for fast arithmetic operations (additions, multiplications, etc.). The results can be saved back into storage by compressing RistrettoPoint structs back to CompressedRistretto structs.

This module also provides a Scalar struct for persisting scalars in storage and doing fast arithmetic on them.

One invariant maintained by this module is that all CompressedRistretto structs store a canonically-encoded point, which can always be decompressed into a valid point on the curve as a RistrettoPoint struct. Unfortunately, due to limitations in our underlying curve25519-dalek elliptic curve library, this decompression will unnecessarily verify the validity of the point and thus slightly decrease performance.

Similarly, all Scalar structs store a canonically-encoded scalar, which can always be safely operated on using arithmetic operations.

In the future, we might support additional features:

• For scalars:

• batch_invert()

• For points:

• double()

• The challenge is that curve25519-dalek does NOT export double for Ristretto points (nor for Edwards)

• double_and_compress_batch()

• fixed-base, variable-time via optional_mixed_multiscalar_mul() in VartimePrecomputedMultiscalarMul

• This would require a storage-friendly RistrettoBasepointTable and an in-memory variant of it too
• Similar to the CompressedRistretto and RistrettoPoint structs in this module
• The challenge is that curve25519-dalek’s RistrettoBasepointTable is not serializable

TODO:

• make fetching the RistrettoPoint’s for the basepoint and the hased basepoint instant via natives, by not going through point decompression

• Struct Scalar

• Struct CompressedRistretto

• Struct RistrettoPoint

• Constants

• Function point_identity_compressed

• Function point_identity

• Function basepoint_compressed

• Function basepoint_H_compressed

• Function basepoint_H

• Function hash_to_point_base

• Function basepoint

• Function basepoint_mul

• Function new_compressed_point_from_bytes

• Function new_point_from_bytes

• Function new_point_and_compressed_from_bytes

• Function compressed_point_to_bytes

• Function new_point_from_sha512

• Function new_point_from_sha2_512

• Function new_point_from_64_uniform_bytes

• Function point_decompress

• Function point_clone

• Function point_compress

• Function point_to_bytes

• Function points_to_bytes

• Function point_mul

• Function point_mul_assign

• Function basepoint_double_mul

• Function point_add

• Function point_add_assign

• Function point_sub

• Function point_sub_assign

• Function point_neg

• Function point_neg_assign

• Function point_equals

• Function compressed_point_equals

• Function is_identity

• Function double_scalar_mul

• Function multi_scalar_mul

• Function new_scalar_from_bytes

• Function new_scalar_from_sha512

• Function new_scalar_from_sha2_512

• Function new_scalar_from_u8

• Function new_scalar_from_u32

• Function new_scalar_from_u64

• Function new_scalar_from_u128

• Function new_scalar_reduced_from_32_bytes

• Function new_scalar_uniform_from_64_bytes

• Function scalar_zero

• Function scalar_is_zero

• Function scalar_one

• Function scalar_is_one

• Function scalar_equals

• Function scalar_invert

• Function scalar_mul

• Function scalar_mul_assign

• Function scalar_add

• Function scalar_add_assign

• Function scalar_sub

• Function scalar_sub_assign

• Function scalar_neg

• Function scalar_neg_assign

• Function scalar_to_bytes

• Function new_point_from_sha512_internal

• Function new_point_from_64_uniform_bytes_internal

• Function point_is_canonical_internal

• Function point_identity_internal

• Function point_decompress_internal

• Function point_clone_internal

• Function point_compress_internal

• Function point_mul_internal

• Function basepoint_mul_internal

• Function basepoint_double_mul_internal

• Function point_add_internal

• Function point_sub_internal

• Function point_neg_internal

• Function double_scalar_mul_internal

• Function multi_scalar_mul_internal

• Function scalar_is_canonical_internal

• Function scalar_from_u64_internal

• Function scalar_from_u128_internal

• Function scalar_reduced_from_32_bytes_internal

• Function scalar_uniform_from_64_bytes_internal

• Function scalar_invert_internal

• Function scalar_from_sha512_internal

• Function scalar_mul_internal

• Function scalar_add_internal

• Function scalar_sub_internal

• Function scalar_neg_internal

• Specification

  • Helper functions
  • Function point_equals
  • Function double_scalar_mul
  • Function multi_scalar_mul
  • Function new_scalar_from_bytes
  • Function new_scalar_from_sha2_512
  • Function new_scalar_from_u8
  • Function new_scalar_from_u32
  • Function new_scalar_from_u64
  • Function new_scalar_from_u128
  • Function new_scalar_reduced_from_32_bytes
  • Function new_scalar_uniform_from_64_bytes
  • Function scalar_zero
  • Function scalar_is_zero
  • Function scalar_one
  • Function scalar_is_one
  • Function scalar_equals
  • Function scalar_invert
  • Function scalar_mul
  • Function scalar_mul_assign
  • Function scalar_add
  • Function scalar_add_assign
  • Function scalar_sub
  • Function scalar_sub_assign
  • Function scalar_neg
  • Function scalar_neg_assign
  • Function scalar_to_bytes
  • Function new_point_from_sha512_internal
  • Function new_point_from_64_uniform_bytes_internal
  • Function point_is_canonical_internal
  • Function point_identity_internal
  • Function point_decompress_internal
  • Function point_clone_internal
  • Function point_compress_internal
  • Function point_mul_internal
  • Function basepoint_mul_internal
  • Function basepoint_double_mul_internal
  • Function point_add_internal
  • Function point_sub_internal
  • Function point_neg_internal
  • Function double_scalar_mul_internal
  • Function multi_scalar_mul_internal
  • Function scalar_is_canonical_internal
  • Function scalar_from_u64_internal
  • Function scalar_from_u128_internal
  • Function scalar_reduced_from_32_bytes_internal
  • Function scalar_uniform_from_64_bytes_internal
  • Function scalar_invert_internal
  • Function scalar_from_sha512_internal
  • Function scalar_mul_internal
  • Function scalar_add_internal
  • Function scalar_sub_internal
  • Function scalar_neg_internal

use 0x1::error;
use 0x1::features;
use 0x1::option;
use 0x1::vector;

Struct Scalar

This struct represents a scalar as a little-endian byte encoding of an integer in $\mathbb{Z}_\ell$, which is stored in data. Here, \ell denotes the order of the scalar field (and the underlying elliptic curve group).

struct Scalar has copy, drop, store

Struct CompressedRistretto

This struct represents a serialized point on the Ristretto255 curve, in 32 bytes. This struct can be decompressed from storage into an in-memory RistrettoPoint, on which fast curve arithmetic can be performed.

struct CompressedRistretto has copy, drop, store

Struct RistrettoPoint

This struct represents an in-memory Ristretto255 point and supports fast curve arithmetic.

An important invariant: There will never be two RistrettoPoint’s constructed with the same handle. One can have immutable references to the same RistrettoPoint, of course.

struct RistrettoPoint has drop

Constants

The native function has not been deployed yet.

const E_NATIVE_FUN_NOT_AVAILABLE: u64 = 5;

The basepoint (generator) of the Ristretto255 group

const BASE_POINT: vector<u8> = [226, 242, 174, 10, 106, 188, 78, 113, 168, 132, 169, 97, 197, 0, 81, 95, 88, 227, 11, 106, 165, 130, 221, 141, 182, 166, 89, 69, 224, 141, 45, 118];

The number of scalars does not match the number of points.

const E_DIFFERENT_NUM_POINTS_AND_SCALARS: u64 = 1;

Non-canonical encoding of a Ristretto255 point

const E_NON_CANONICAL_ENCODING: u64 = 6;

Too many points have been created in the current transaction execution.

const E_TOO_MANY_POINTS_CREATED: u64 = 4;

Expected more than zero points as input.

const E_ZERO_POINTS: u64 = 2;

Expected more than zero scalars as input.

const E_ZERO_SCALARS: u64 = 3;

The hash of the basepoint of the Ristretto255 group using SHA3_512 TODO: Can we rename this?

const HASH_BASE_POINT: vector<u8> = [140, 146, 64, 180, 86, 169, 230, 220, 101, 195, 119, 161, 4, 141, 116, 95, 148, 160, 140, 219, 127, 68, 203, 205, 123, 70, 243, 64, 72, 135, 17, 52];

The identity point

const IDENTITY_POINT: vector<u8> = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0];

ORDER_ELL - 1: i.e., the “largest”, reduced scalar in the field This also requires 253 bits to represent.

const L_MINUS_ONE: vector<u8> = [236, 211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222, 20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16];

The maximum size in bytes of a canonically-encoded Ristretto255 point is 32 bytes.

const MAX_POINT_NUM_BYTES: u64 = 32;

The maximum size in bits of a canonically-encoded Scalar is 256 bits.

const MAX_SCALAR_NUM_BITS: u64 = 256;

The maximum size in bytes of a canonically-encoded Scalar is 32 bytes.

const MAX_SCALAR_NUM_BYTES: u64 = 32;

The order of the Ristretto255 group and its scalar field, in little-endian. This requires 253 bits to represent.

const ORDER_ELL: vector<u8> = [237, 211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222, 20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16];

Function point_identity_compressed

Returns the identity point as a CompressedRistretto.

public fun point_identity_compressed(): ristretto255::CompressedRistretto

public fun point_identity_compressed(): CompressedRistretto {
    CompressedRistretto {
        data: IDENTITY_POINT
    }
}

Function point_identity

Returns the identity point as a CompressedRistretto.

public fun point_identity(): ristretto255::RistrettoPoint

public fun point_identity(): RistrettoPoint {
    RistrettoPoint {
        handle: point_identity_internal()
    }
}

Function basepoint_compressed

Returns the basepoint (generator) of the Ristretto255 group as a compressed point

public fun basepoint_compressed(): ristretto255::CompressedRistretto

public fun basepoint_compressed(): CompressedRistretto {
    CompressedRistretto {
        data: BASE_POINT
    }
}

Function basepoint_H_compressed

Returns a Ristretto255 group generator H obtained from hashing (the serialization of) the basepoint G to the group. Useful for using it as the randomness basepoint in Pedersen commitments: i.e., C = v G + r H

public fun basepoint_H_compressed(): ristretto255::CompressedRistretto

public fun basepoint_H_compressed(): CompressedRistretto {
    CompressedRistretto { data: HASH_BASE_POINT }
}

Function basepoint_H

Like hash_to_point_base_compressed but returns a decompressed point.

public fun basepoint_H(): ristretto255::RistrettoPoint

public fun basepoint_H(): RistrettoPoint {
    basepoint_H_compressed().point_decompress()
}

Function hash_to_point_base

Should call basepoint_H instead.

#[deprecated]
public fun hash_to_point_base(): ristretto255::RistrettoPoint

public fun hash_to_point_base(): RistrettoPoint {
    basepoint_H_compressed().point_decompress()
}

Function basepoint

Returns the basepoint (generator) of the Ristretto255 group

public fun basepoint(): ristretto255::RistrettoPoint

public fun basepoint(): RistrettoPoint {
    let (handle, _) = point_decompress_internal(BASE_POINT);

    RistrettoPoint {
        handle
    }
}

Function basepoint_mul

Multiplies the basepoint (generator) of the Ristretto255 group by a scalar and returns the result. This call is much faster than point_mul(&basepoint(), &some_scalar) because of precomputation tables.

public fun basepoint_mul(self: &ristretto255::Scalar): ristretto255::RistrettoPoint

public fun basepoint_mul(self: &Scalar): RistrettoPoint {
    RistrettoPoint {
        handle: basepoint_mul_internal(self.data)
    }
}

Function new_compressed_point_from_bytes

Creates a new CompressedRistretto point from a sequence of 32 bytes. Actually attempts decompression to check that the bytes represent a valid Ristretto255 point. If not, returns None.

public fun new_compressed_point_from_bytes(bytes: vector<u8>): option::Option<ristretto255::CompressedRistretto>

public fun new_compressed_point_from_bytes(bytes: vector<u8>): Option<CompressedRistretto> {
    if (point_is_canonical_internal(bytes)) {
        std::option::some(CompressedRistretto {
            data: bytes
        })
    } else {
        std::option::none<CompressedRistretto>()
    }
}

Function new_point_from_bytes

Creates a new RistrettoPoint from a sequence of 32 bytes. If those bytes do not represent a valid point, returns None.

public fun new_point_from_bytes(bytes: vector<u8>): option::Option<ristretto255::RistrettoPoint>

public fun new_point_from_bytes(bytes: vector<u8>): Option<RistrettoPoint> {
    let (handle, is_canonical) = point_decompress_internal(bytes);
    if (is_canonical) {
        std::option::some(RistrettoPoint { handle })
    } else {
        std::option::none<RistrettoPoint>()
    }
}

Function new_point_and_compressed_from_bytes

Without this function, it is not possible to efficiently parse a 32-byte array both as RistrettoPoint and as a CompressedRistretto without doing two decompressions.

Note: Due to limitations of Move, this function will abort instead of returning an Option::None, because we cannot have tuples as the option’s type.

public fun new_point_and_compressed_from_bytes(bytes: vector<u8>): (ristretto255::RistrettoPoint, ristretto255::CompressedRistretto)

public fun new_point_and_compressed_from_bytes(bytes: vector<u8>): (RistrettoPoint, CompressedRistretto) {
    let (handle, is_canonical) = point_decompress_internal(bytes);
    if (is_canonical) {
        (
            RistrettoPoint { handle },
            CompressedRistretto {
                data: bytes
            }
        )
    } else {
        abort(std::error::invalid_argument(E_NON_CANONICAL_ENCODING))
    }
}

Function compressed_point_to_bytes

Given a compressed ristretto point point, returns the byte representation of that point

public fun compressed_point_to_bytes(self: ristretto255::CompressedRistretto): vector<u8>

public fun compressed_point_to_bytes(self: CompressedRistretto): vector<u8> {
    self.data
}

Function new_point_from_sha512

DEPRECATED: Use the more clearly-named new_point_from_sha2_512

Hashes the input to a uniformly-at-random RistrettoPoint via SHA512.

#[deprecated]
public fun new_point_from_sha512(sha2_512_input: vector<u8>): ristretto255::RistrettoPoint

public fun new_point_from_sha512(sha2_512_input: vector<u8>): RistrettoPoint {
    new_point_from_sha2_512(sha2_512_input)
}

Function new_point_from_sha2_512

Hashes the input to a uniformly-at-random RistrettoPoint via SHA2-512.

public fun new_point_from_sha2_512(sha2_512_input: vector<u8>): ristretto255::RistrettoPoint

public fun new_point_from_sha2_512(sha2_512_input: vector<u8>): RistrettoPoint {
    RistrettoPoint {
        handle: new_point_from_sha512_internal(sha2_512_input)
    }
}

Function new_point_from_64_uniform_bytes

Samples a uniformly-at-random RistrettoPoint given a sequence of 64 uniformly-at-random bytes. This function can be used to build a collision-resistant hash function that maps 64-byte messages to RistrettoPoint’s.

public fun new_point_from_64_uniform_bytes(bytes: vector<u8>): option::Option<ristretto255::RistrettoPoint>

public fun new_point_from_64_uniform_bytes(bytes: vector<u8>): Option<RistrettoPoint> {
    if (bytes.length() == 64) {
        std::option::some(RistrettoPoint {
            handle: new_point_from_64_uniform_bytes_internal(bytes)
        })
    } else {
        std::option::none<RistrettoPoint>()
    }
}

Function point_decompress

Decompresses a CompressedRistretto from storage into a RistrettoPoint which can be used for fast arithmetic.

public fun point_decompress(self: &ristretto255::CompressedRistretto): ristretto255::RistrettoPoint

public fun point_decompress(self: &CompressedRistretto): RistrettoPoint {
    // NOTE: Our CompressedRistretto invariant assures us that every CompressedRistretto in storage is a valid
    // point
    let (handle, _) = point_decompress_internal(self.data);
    RistrettoPoint { handle }
}

Function point_clone

Clones a RistrettoPoint.

public fun point_clone(self: &ristretto255::RistrettoPoint): ristretto255::RistrettoPoint

public fun point_clone(self: &RistrettoPoint): RistrettoPoint {
    if(!features::bulletproofs_enabled()) {
        abort(std::error::invalid_state(E_NATIVE_FUN_NOT_AVAILABLE))
    };

    RistrettoPoint {
        handle: point_clone_internal(self.handle)
    }
}

Function point_compress

Compresses a RistrettoPoint to a CompressedRistretto which can be put in storage.

public fun point_compress(self: &ristretto255::RistrettoPoint): ristretto255::CompressedRistretto

public fun point_compress(self: &RistrettoPoint): CompressedRistretto {
    CompressedRistretto {
        data: point_compress_internal(self)
    }
}

Function point_to_bytes

Returns the sequence of bytes representin this Ristretto point. To convert a RistrettoPoint ‘p’ to bytes, first compress it via c = point_compress(&p), and then call this function on c.

public fun point_to_bytes(self: &ristretto255::CompressedRistretto): vector<u8>

public fun point_to_bytes(self: &CompressedRistretto): vector<u8> {
    self.data
}

Function points_to_bytes

Serializes a vector of RistrettoPoints into a vector of byte vectors. Each point is compressed and then converted to bytes.

public fun points_to_bytes(points: &vector<ristretto255::RistrettoPoint>): vector<vector<u8>>

public fun points_to_bytes(points: &vector<RistrettoPoint>): vector<vector<u8>> {
    points.map_ref(|p| point_compress_internal(p))
}

Function point_mul

Returns a * point.

public fun point_mul(self: &ristretto255::RistrettoPoint, a: &ristretto255::Scalar): ristretto255::RistrettoPoint

public fun point_mul(self: &RistrettoPoint, a: &Scalar): RistrettoPoint {
    RistrettoPoint {
        handle: point_mul_internal(self, a.data, false)
    }
}

Function point_mul_assign

Sets a *= point and returns ‘a’.

public fun point_mul_assign(self: &mut ristretto255::RistrettoPoint, a: &ristretto255::Scalar): &mut ristretto255::RistrettoPoint

public fun point_mul_assign(self: &mut RistrettoPoint, a: &Scalar): &mut RistrettoPoint {
    point_mul_internal(self, a.data, true);
    self
}

Function basepoint_double_mul

Returns (a * a_base + b * base_point), where base_point is the Ristretto basepoint encoded in BASE_POINT.

public fun basepoint_double_mul(a: &ristretto255::Scalar, a_base: &ristretto255::RistrettoPoint, b: &ristretto255::Scalar): ristretto255::RistrettoPoint

public fun basepoint_double_mul(a: &Scalar, a_base: &RistrettoPoint, b: &Scalar): RistrettoPoint {
    RistrettoPoint {
        handle: basepoint_double_mul_internal(a.data, a_base, b.data)
    }
}

Function point_add

Returns a + b

public fun point_add(self: &ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint): ristretto255::RistrettoPoint

public fun point_add(self: &RistrettoPoint, b: &RistrettoPoint): RistrettoPoint {
    RistrettoPoint {
        handle: point_add_internal(self, b, false)
    }
}

Function point_add_assign

Sets a += b and returns ‘a’.

public fun point_add_assign(self: &mut ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint): &mut ristretto255::RistrettoPoint

public fun point_add_assign(self: &mut RistrettoPoint, b: &RistrettoPoint): &mut RistrettoPoint {
    point_add_internal(self, b, true);
    self
}

Function point_sub

Returns a - b

public fun point_sub(self: &ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint): ristretto255::RistrettoPoint

public fun point_sub(self: &RistrettoPoint, b: &RistrettoPoint): RistrettoPoint {
    RistrettoPoint {
        handle: point_sub_internal(self, b, false)
    }
}

Function point_sub_assign

Sets a -= b and returns ‘a’.

public fun point_sub_assign(self: &mut ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint): &mut ristretto255::RistrettoPoint

public fun point_sub_assign(self: &mut RistrettoPoint, b: &RistrettoPoint): &mut RistrettoPoint {
    point_sub_internal(self, b, true);
    self
}

Function point_neg

Returns -a

public fun point_neg(self: &ristretto255::RistrettoPoint): ristretto255::RistrettoPoint

public fun point_neg(self: &RistrettoPoint): RistrettoPoint {
    RistrettoPoint {
        handle: point_neg_internal(self, false)
    }
}

Function point_neg_assign

Sets a = -a, and returns ‘a’.

public fun point_neg_assign(self: &mut ristretto255::RistrettoPoint): &mut ristretto255::RistrettoPoint

public fun point_neg_assign(self: &mut RistrettoPoint): &mut RistrettoPoint {
    point_neg_internal(self, true);
    self
}

Function point_equals

Returns true if the two RistrettoPoints are the same points on the elliptic curve.

public fun point_equals(self: &ristretto255::RistrettoPoint, h: &ristretto255::RistrettoPoint): bool

native public fun point_equals(self: &RistrettoPoint, h: &RistrettoPoint): bool;

Function compressed_point_equals

Returns true if the two compressed points are the same points on the elliptic curve. Recall that serialization is canonical, so testing equality this way is correct.

public fun compressed_point_equals(self: &ristretto255::CompressedRistretto, rhs: &ristretto255::CompressedRistretto): bool

public fun compressed_point_equals(self: &CompressedRistretto, rhs: &CompressedRistretto): bool {
    self.data == rhs.data
}

Function is_identity

Returns true if the compressed point is the identity point.

public fun is_identity(self: &ristretto255::CompressedRistretto): bool

public fun is_identity(self: &CompressedRistretto): bool {
    self.data == IDENTITY_POINT
}

Function double_scalar_mul

Computes a double-scalar multiplication, returning a_1 p_1 + a_2 p_2 This function is much faster than computing each a_i p_i using point_mul and adding up the results using point_add.

public fun double_scalar_mul(scalar1: &ristretto255::Scalar, point1: &ristretto255::RistrettoPoint, scalar2: &ristretto255::Scalar, point2: &ristretto255::RistrettoPoint): ristretto255::RistrettoPoint

public fun double_scalar_mul(scalar1: &Scalar, point1: &RistrettoPoint, scalar2: &Scalar, point2: &RistrettoPoint): RistrettoPoint {
    if(!features::bulletproofs_enabled()) {
        abort(std::error::invalid_state(E_NATIVE_FUN_NOT_AVAILABLE))
    };

    RistrettoPoint {
        handle: double_scalar_mul_internal(point1.handle, point2.handle, scalar1.data, scalar2.data)
    }
}

Function multi_scalar_mul

Computes a multi-scalar multiplication, returning a_1 p_1 + a_2 p_2 + … + a_n p_n. This function is much faster than computing each a_i p_i using point_mul and adding up the results using point_add.

public fun multi_scalar_mul(points: &vector<ristretto255::RistrettoPoint>, scalars: &vector<ristretto255::Scalar>): ristretto255::RistrettoPoint

public fun multi_scalar_mul(points: &vector<RistrettoPoint>, scalars: &vector<Scalar>): RistrettoPoint {
    assert!(!points.is_empty(), std::error::invalid_argument(E_ZERO_POINTS));
    assert!(!scalars.is_empty(), std::error::invalid_argument(E_ZERO_SCALARS));
    assert!(
        points.length() == scalars.length(), std::error::invalid_argument(E_DIFFERENT_NUM_POINTS_AND_SCALARS));

    RistrettoPoint {
        handle: multi_scalar_mul_internal<RistrettoPoint, Scalar>(points, scalars)
    }
}

Function new_scalar_from_bytes

Given a sequence of 32 bytes, checks if they canonically-encode a Scalar and return it. Otherwise, returns None.

public fun new_scalar_from_bytes(bytes: vector<u8>): option::Option<ristretto255::Scalar>

public fun new_scalar_from_bytes(bytes: vector<u8>): Option<Scalar> {
    if (scalar_is_canonical_internal(bytes)) {
        std::option::some(Scalar {
            data: bytes
        })
    } else {
        std::option::none<Scalar>()
    }
}

Function new_scalar_from_sha512

DEPRECATED: Use the more clearly-named new_scalar_from_sha2_512

Hashes the input to a uniformly-at-random Scalar via SHA2-512

#[deprecated]
public fun new_scalar_from_sha512(sha2_512_input: vector<u8>): ristretto255::Scalar

public fun new_scalar_from_sha512(sha2_512_input: vector<u8>): Scalar {
    new_scalar_from_sha2_512(sha2_512_input)
}

Function new_scalar_from_sha2_512

Hashes the input to a uniformly-at-random Scalar via SHA2-512

public fun new_scalar_from_sha2_512(sha2_512_input: vector<u8>): ristretto255::Scalar

public fun new_scalar_from_sha2_512(sha2_512_input: vector<u8>): Scalar {
    Scalar {
        data: scalar_from_sha512_internal(sha2_512_input)
    }
}

Function new_scalar_from_u8

Creates a Scalar from an u8.

public fun new_scalar_from_u8(byte: u8): ristretto255::Scalar

public fun new_scalar_from_u8(byte: u8): Scalar {
    let s = scalar_zero();
    s.data[0] = byte;
    s
}

Function new_scalar_from_u32

Creates a Scalar from an u32.

public fun new_scalar_from_u32(four_bytes: u32): ristretto255::Scalar

public fun new_scalar_from_u32(four_bytes: u32): Scalar {
    Scalar {
        data: scalar_from_u64_internal((four_bytes as u64))
    }
}

Function new_scalar_from_u64

Creates a Scalar from an u64.

public fun new_scalar_from_u64(eight_bytes: u64): ristretto255::Scalar

public fun new_scalar_from_u64(eight_bytes: u64): Scalar {
    Scalar {
        data: scalar_from_u64_internal(eight_bytes)
    }
}

Function new_scalar_from_u128

Creates a Scalar from an u128.

public fun new_scalar_from_u128(sixteen_bytes: u128): ristretto255::Scalar

public fun new_scalar_from_u128(sixteen_bytes: u128): Scalar {
    Scalar {
        data: scalar_from_u128_internal(sixteen_bytes)
    }
}

Function new_scalar_reduced_from_32_bytes

Creates a Scalar from 32 bytes by reducing the little-endian-encoded number in those bytes modulo $\ell$.

public fun new_scalar_reduced_from_32_bytes(bytes: vector<u8>): option::Option<ristretto255::Scalar>

public fun new_scalar_reduced_from_32_bytes(bytes: vector<u8>): Option<Scalar> {
    if (bytes.length() == 32) {
        std::option::some(Scalar {
            data: scalar_reduced_from_32_bytes_internal(bytes)
        })
    } else {
        std::option::none()
    }
}

Function new_scalar_uniform_from_64_bytes

Samples a scalar uniformly-at-random given 64 uniform-at-random bytes as input by reducing the little-endian-encoded number in those bytes modulo $\ell$.

public fun new_scalar_uniform_from_64_bytes(bytes: vector<u8>): option::Option<ristretto255::Scalar>

public fun new_scalar_uniform_from_64_bytes(bytes: vector<u8>): Option<Scalar> {
    if (bytes.length() == 64) {
        std::option::some(Scalar {
            data: scalar_uniform_from_64_bytes_internal(bytes)
        })
    } else {
        std::option::none()
    }
}

Function scalar_zero

Returns 0 as a Scalar.

public fun scalar_zero(): ristretto255::Scalar

public fun scalar_zero(): Scalar {
    Scalar {
        data: x"0000000000000000000000000000000000000000000000000000000000000000"
    }
}

Function scalar_is_zero

Returns true if the given Scalar equals 0.

public fun scalar_is_zero(self: &ristretto255::Scalar): bool

public fun scalar_is_zero(self: &Scalar): bool {
    self.data == x"0000000000000000000000000000000000000000000000000000000000000000"
}

Function scalar_one

Returns 1 as a Scalar.

public fun scalar_one(): ristretto255::Scalar

public fun scalar_one(): Scalar {
    Scalar {
        data: x"0100000000000000000000000000000000000000000000000000000000000000"
    }
}

Function scalar_is_one

Returns true if the given Scalar equals 1.

public fun scalar_is_one(self: &ristretto255::Scalar): bool

public fun scalar_is_one(self: &Scalar): bool {
    self.data == x"0100000000000000000000000000000000000000000000000000000000000000"
}

Function scalar_equals

Returns true if the two scalars are equal.

public fun scalar_equals(self: &ristretto255::Scalar, rhs: &ristretto255::Scalar): bool

public fun scalar_equals(self: &Scalar, rhs: &Scalar): bool {
    self.data == rhs.data
}

Function scalar_invert

Returns the inverse s^{-1} mod \ell of a scalar s. Returns None if s is zero.

public fun scalar_invert(self: &ristretto255::Scalar): option::Option<ristretto255::Scalar>

public fun scalar_invert(self: &Scalar): Option<Scalar> {
    if (self.scalar_is_zero()) {
        std::option::none<Scalar>()
    } else {
        std::option::some(Scalar {
            data: scalar_invert_internal(self.data)
        })
    }
}

Function scalar_mul

Returns the product of the two scalars.

public fun scalar_mul(self: &ristretto255::Scalar, b: &ristretto255::Scalar): ristretto255::Scalar

public fun scalar_mul(self: &Scalar, b: &Scalar): Scalar {
    Scalar {
        data: scalar_mul_internal(self.data, b.data)
    }
}

Function scalar_mul_assign

Computes the product of ‘a’ and ‘b’ and assigns the result to ‘a’. Returns ‘a’.

public fun scalar_mul_assign(self: &mut ristretto255::Scalar, b: &ristretto255::Scalar): &mut ristretto255::Scalar

public fun scalar_mul_assign(self: &mut Scalar, b: &Scalar): &mut Scalar {
    self.data = self.scalar_mul(b).data;
    self
}

Function scalar_add

Returns the sum of the two scalars.

public fun scalar_add(self: &ristretto255::Scalar, b: &ristretto255::Scalar): ristretto255::Scalar

public fun scalar_add(self: &Scalar, b: &Scalar): Scalar {
    Scalar {
        data: scalar_add_internal(self.data, b.data)
    }
}

Function scalar_add_assign

Computes the sum of ‘a’ and ‘b’ and assigns the result to ‘a’ Returns ‘a’.

public fun scalar_add_assign(self: &mut ristretto255::Scalar, b: &ristretto255::Scalar): &mut ristretto255::Scalar

public fun scalar_add_assign(self: &mut Scalar, b: &Scalar): &mut Scalar {
    self.data = self.scalar_add(b).data;
    self
}

Function scalar_sub

Returns the difference of the two scalars.

public fun scalar_sub(self: &ristretto255::Scalar, b: &ristretto255::Scalar): ristretto255::Scalar

public fun scalar_sub(self: &Scalar, b: &Scalar): Scalar {
    Scalar {
        data: scalar_sub_internal(self.data, b.data)
    }
}

Function scalar_sub_assign

Subtracts ‘b’ from ‘a’ and assigns the result to ‘a’. Returns ‘a’.

public fun scalar_sub_assign(self: &mut ristretto255::Scalar, b: &ristretto255::Scalar): &mut ristretto255::Scalar

public fun scalar_sub_assign(self: &mut Scalar, b: &Scalar): &mut Scalar {
    self.data = self.scalar_sub(b).data;
    self
}

Function scalar_neg

Returns the negation of ‘a’: i.e., $(0 - a) \mod \ell$.

public fun scalar_neg(self: &ristretto255::Scalar): ristretto255::Scalar

public fun scalar_neg(self: &Scalar): Scalar {
    Scalar {
        data: scalar_neg_internal(self.data)
    }
}

Function scalar_neg_assign

Replaces ‘a’ by its negation. Returns ‘a’.

public fun scalar_neg_assign(self: &mut ristretto255::Scalar): &mut ristretto255::Scalar

public fun scalar_neg_assign(self: &mut Scalar): &mut Scalar {
    self.data = self.scalar_neg().data;
    self
}

Function scalar_to_bytes

Returns the byte-representation of the scalar.

public fun scalar_to_bytes(self: &ristretto255::Scalar): vector<u8>

public fun scalar_to_bytes(self: &Scalar): vector<u8> {
    self.data
}

Function new_point_from_sha512_internal

fun new_point_from_sha512_internal(sha2_512_input: vector<u8>): u64

native fun new_point_from_sha512_internal(sha2_512_input: vector<u8>): u64;

Function new_point_from_64_uniform_bytes_internal

fun new_point_from_64_uniform_bytes_internal(bytes: vector<u8>): u64

native fun new_point_from_64_uniform_bytes_internal(bytes: vector<u8>): u64;

Function point_is_canonical_internal

fun point_is_canonical_internal(bytes: vector<u8>): bool

native fun point_is_canonical_internal(bytes: vector<u8>): bool;

Function point_identity_internal

fun point_identity_internal(): u64

native fun point_identity_internal(): u64;

Function point_decompress_internal

fun point_decompress_internal(maybe_non_canonical_bytes: vector<u8>): (u64, bool)

native fun point_decompress_internal(maybe_non_canonical_bytes: vector<u8>): (u64, bool);

Function point_clone_internal

fun point_clone_internal(point_handle: u64): u64

native fun point_clone_internal(point_handle: u64): u64;

Function point_compress_internal

fun point_compress_internal(point: &ristretto255::RistrettoPoint): vector<u8>

native fun point_compress_internal(point: &RistrettoPoint): vector<u8>;

Function point_mul_internal

fun point_mul_internal(point: &ristretto255::RistrettoPoint, a: vector<u8>, in_place: bool): u64

native fun point_mul_internal(point: &RistrettoPoint, a: vector<u8>, in_place: bool): u64;

Function basepoint_mul_internal

fun basepoint_mul_internal(a: vector<u8>): u64

native fun basepoint_mul_internal(a: vector<u8>): u64;

Function basepoint_double_mul_internal

fun basepoint_double_mul_internal(a: vector<u8>, some_point: &ristretto255::RistrettoPoint, b: vector<u8>): u64

native fun basepoint_double_mul_internal(a: vector<u8>, some_point: &RistrettoPoint, b: vector<u8>): u64;

Function point_add_internal

fun point_add_internal(a: &ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint, in_place: bool): u64

native fun point_add_internal(a: &RistrettoPoint, b: &RistrettoPoint, in_place: bool): u64;

Function point_sub_internal

fun point_sub_internal(a: &ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint, in_place: bool): u64

native fun point_sub_internal(a: &RistrettoPoint, b: &RistrettoPoint, in_place: bool): u64;

Function point_neg_internal

fun point_neg_internal(a: &ristretto255::RistrettoPoint, in_place: bool): u64

native fun point_neg_internal(a: &RistrettoPoint, in_place: bool): u64;

Function double_scalar_mul_internal

fun double_scalar_mul_internal(point1: u64, point2: u64, scalar1: vector<u8>, scalar2: vector<u8>): u64

native fun double_scalar_mul_internal(point1: u64, point2: u64, scalar1: vector<u8>, scalar2: vector<u8>): u64;

Function multi_scalar_mul_internal

The generic arguments are needed to deal with some Move VM peculiarities which prevent us from borrowing the points (or scalars) inside a &vector in Rust.

WARNING: This function can only be called with P = RistrettoPoint and S = Scalar.

fun multi_scalar_mul_internal<P, S>(points: &vector<P>, scalars: &vector<S>): u64

native fun multi_scalar_mul_internal<P, S>(points: &vector<P>, scalars: &vector<S>): u64;

Function scalar_is_canonical_internal

fun scalar_is_canonical_internal(s: vector<u8>): bool

native fun scalar_is_canonical_internal(s: vector<u8>): bool;

Function scalar_from_u64_internal

fun scalar_from_u64_internal(num: u64): vector<u8>

native fun scalar_from_u64_internal(num: u64): vector<u8>;

Function scalar_from_u128_internal

fun scalar_from_u128_internal(num: u128): vector<u8>

native fun scalar_from_u128_internal(num: u128): vector<u8>;

Function scalar_reduced_from_32_bytes_internal

fun scalar_reduced_from_32_bytes_internal(bytes: vector<u8>): vector<u8>

native fun scalar_reduced_from_32_bytes_internal(bytes: vector<u8>): vector<u8>;

Function scalar_uniform_from_64_bytes_internal

fun scalar_uniform_from_64_bytes_internal(bytes: vector<u8>): vector<u8>

native fun scalar_uniform_from_64_bytes_internal(bytes: vector<u8>): vector<u8>;

Function scalar_invert_internal

fun scalar_invert_internal(bytes: vector<u8>): vector<u8>

native fun scalar_invert_internal(bytes: vector<u8>): vector<u8>;

Function scalar_from_sha512_internal

fun scalar_from_sha512_internal(sha2_512_input: vector<u8>): vector<u8>

native fun scalar_from_sha512_internal(sha2_512_input: vector<u8>): vector<u8>;

Function scalar_mul_internal

fun scalar_mul_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>

native fun scalar_mul_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>;

Function scalar_add_internal

fun scalar_add_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>

native fun scalar_add_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>;

Function scalar_sub_internal

fun scalar_sub_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>

native fun scalar_sub_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>;

Function scalar_neg_internal

fun scalar_neg_internal(a_bytes: vector<u8>): vector<u8>

native fun scalar_neg_internal(a_bytes: vector<u8>): vector<u8>;

Specification

Helper functions

fun spec_scalar_is_zero(s: Scalar): bool {
   s.data == x"0000000000000000000000000000000000000000000000000000000000000000"
}

fun spec_scalar_is_one(s: Scalar): bool {
   s.data == x"0100000000000000000000000000000000000000000000000000000000000000"
}

fun spec_point_is_canonical_internal(bytes: vector<u8>): bool;

fun spec_double_scalar_mul_internal(point1: u64, point2: u64, scalar1: vector<u8>, scalar2: vector<u8>): u64;

fun spec_multi_scalar_mul_internal<P, S>(points: vector<P>, scalars: vector<S>): u64;

fun spec_scalar_is_canonical_internal(s: vector<u8>): bool;

fun spec_scalar_from_u64_internal(num: u64): vector<u8>;

fun spec_scalar_from_u128_internal(num: u128): vector<u8>;

fun spec_scalar_reduced_from_32_bytes_internal(bytes: vector<u8>): vector<u8>;

fun spec_scalar_uniform_from_64_bytes_internal(bytes: vector<u8>): vector<u8>;

fun spec_scalar_invert_internal(bytes: vector<u8>): vector<u8>;

fun spec_scalar_from_sha512_internal(sha2_512_input: vector<u8>): vector<u8>;

fun spec_scalar_mul_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>;

fun spec_scalar_add_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>;

fun spec_scalar_sub_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>;

fun spec_scalar_neg_internal(a_bytes: vector<u8>): vector<u8>;

Function point_equals

public fun point_equals(self: &ristretto255::RistrettoPoint, h: &ristretto255::RistrettoPoint): bool

pragma opaque;

Function double_scalar_mul

public fun double_scalar_mul(scalar1: &ristretto255::Scalar, point1: &ristretto255::RistrettoPoint, scalar2: &ristretto255::Scalar, point2: &ristretto255::RistrettoPoint): ristretto255::RistrettoPoint

pragma opaque;

Function multi_scalar_mul

public fun multi_scalar_mul(points: &vector<ristretto255::RistrettoPoint>, scalars: &vector<ristretto255::Scalar>): ristretto255::RistrettoPoint

aborts_if len(points) == 0;
aborts_if len(scalars) == 0;
aborts_if len(points) != len(scalars);
ensures result.handle == spec_multi_scalar_mul_internal(points, scalars);

Function new_scalar_from_bytes

public fun new_scalar_from_bytes(bytes: vector<u8>): option::Option<ristretto255::Scalar>

aborts_if false;
ensures spec_scalar_is_canonical_internal(bytes) ==> (std::option::is_some(result)
    && std::option::borrow(result).data == bytes);
ensures !spec_scalar_is_canonical_internal(bytes) ==> std::option::is_none(result);

Function new_scalar_from_sha2_512

public fun new_scalar_from_sha2_512(sha2_512_input: vector<u8>): ristretto255::Scalar

aborts_if false;
ensures result.data == spec_scalar_from_sha512_internal(sha2_512_input);

Function new_scalar_from_u8

public fun new_scalar_from_u8(byte: u8): ristretto255::Scalar

aborts_if false;
ensures result.data[0] == byte;
ensures forall i in 1..len(result.data): result.data[i] == 0;

Function new_scalar_from_u32

public fun new_scalar_from_u32(four_bytes: u32): ristretto255::Scalar

aborts_if false;
ensures result.data == spec_scalar_from_u64_internal(four_bytes);

Function new_scalar_from_u64

public fun new_scalar_from_u64(eight_bytes: u64): ristretto255::Scalar

aborts_if false;
ensures result.data == spec_scalar_from_u64_internal(eight_bytes);

Function new_scalar_from_u128

public fun new_scalar_from_u128(sixteen_bytes: u128): ristretto255::Scalar

pragma bv=b"0";
aborts_if false;
ensures result.data == spec_scalar_from_u128_internal(sixteen_bytes);

Function new_scalar_reduced_from_32_bytes

public fun new_scalar_reduced_from_32_bytes(bytes: vector<u8>): option::Option<ristretto255::Scalar>

ensures len(bytes) != 32 ==> std::option::is_none(result);
ensures len(bytes) == 32 ==> std::option::borrow(result).data == spec_scalar_reduced_from_32_bytes_internal(bytes);

Function new_scalar_uniform_from_64_bytes

public fun new_scalar_uniform_from_64_bytes(bytes: vector<u8>): option::Option<ristretto255::Scalar>

ensures len(bytes) != 64 ==> std::option::is_none(result);
ensures len(bytes) == 64 ==> std::option::borrow(result).data == spec_scalar_uniform_from_64_bytes_internal(bytes);

Function scalar_zero

public fun scalar_zero(): ristretto255::Scalar

ensures spec_scalar_is_zero(result);

Function scalar_is_zero

public fun scalar_is_zero(self: &ristretto255::Scalar): bool

ensures result == spec_scalar_is_zero(self);

Function scalar_one

public fun scalar_one(): ristretto255::Scalar

ensures spec_scalar_is_one(result);

Function scalar_is_one

public fun scalar_is_one(self: &ristretto255::Scalar): bool

ensures result == spec_scalar_is_one(self);

Function scalar_equals

public fun scalar_equals(self: &ristretto255::Scalar, rhs: &ristretto255::Scalar): bool

aborts_if false;
ensures result == (self.data == rhs.data);

Function scalar_invert

public fun scalar_invert(self: &ristretto255::Scalar): option::Option<ristretto255::Scalar>

aborts_if false;
ensures spec_scalar_is_zero(self) ==> std::option::is_none(result);
ensures !spec_scalar_is_zero(self) ==> (std::option::is_some(result) && std::option::borrow(result).data == spec_scalar_invert_internal(self.data));

Function scalar_mul

public fun scalar_mul(self: &ristretto255::Scalar, b: &ristretto255::Scalar): ristretto255::Scalar

aborts_if false;
ensures result.data == spec_scalar_mul_internal(self.data, b.data);

Function scalar_mul_assign

public fun scalar_mul_assign(self: &mut ristretto255::Scalar, b: &ristretto255::Scalar): &mut ristretto255::Scalar

aborts_if false;
ensures self.data == spec_scalar_mul_internal(old(self).data, b.data);

Function scalar_add

public fun scalar_add(self: &ristretto255::Scalar, b: &ristretto255::Scalar): ristretto255::Scalar

aborts_if false;
ensures result.data == spec_scalar_add_internal(self.data, b.data);

Function scalar_add_assign

public fun scalar_add_assign(self: &mut ristretto255::Scalar, b: &ristretto255::Scalar): &mut ristretto255::Scalar

aborts_if false;
ensures self.data == spec_scalar_add_internal(old(self).data, b.data);

Function scalar_sub

public fun scalar_sub(self: &ristretto255::Scalar, b: &ristretto255::Scalar): ristretto255::Scalar

aborts_if false;
ensures result.data == spec_scalar_sub_internal(self.data, b.data);

Function scalar_sub_assign

public fun scalar_sub_assign(self: &mut ristretto255::Scalar, b: &ristretto255::Scalar): &mut ristretto255::Scalar

aborts_if false;
ensures self.data == spec_scalar_sub_internal(old(self).data, b.data);

Function scalar_neg

public fun scalar_neg(self: &ristretto255::Scalar): ristretto255::Scalar

pragma opaque;
aborts_if false;
ensures result.data == spec_scalar_neg_internal(self.data);

Function scalar_neg_assign

public fun scalar_neg_assign(self: &mut ristretto255::Scalar): &mut ristretto255::Scalar

aborts_if false;
ensures self.data == spec_scalar_neg_internal(old(self).data);

Function scalar_to_bytes

public fun scalar_to_bytes(self: &ristretto255::Scalar): vector<u8>

aborts_if false;
ensures result == self.data;

Function new_point_from_sha512_internal

fun new_point_from_sha512_internal(sha2_512_input: vector<u8>): u64

pragma opaque;

Function new_point_from_64_uniform_bytes_internal

fun new_point_from_64_uniform_bytes_internal(bytes: vector<u8>): u64

pragma opaque;

Function point_is_canonical_internal

fun point_is_canonical_internal(bytes: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_point_is_canonical_internal(bytes);

Function point_identity_internal

fun point_identity_internal(): u64

pragma opaque;

Function point_decompress_internal

fun point_decompress_internal(maybe_non_canonical_bytes: vector<u8>): (u64, bool)

pragma opaque;

Function point_clone_internal

fun point_clone_internal(point_handle: u64): u64

pragma opaque;

Function point_compress_internal

fun point_compress_internal(point: &ristretto255::RistrettoPoint): vector<u8>

pragma opaque;

Function point_mul_internal

fun point_mul_internal(point: &ristretto255::RistrettoPoint, a: vector<u8>, in_place: bool): u64

pragma opaque;

Function basepoint_mul_internal

fun basepoint_mul_internal(a: vector<u8>): u64

pragma opaque;

Function basepoint_double_mul_internal

fun basepoint_double_mul_internal(a: vector<u8>, some_point: &ristretto255::RistrettoPoint, b: vector<u8>): u64

pragma opaque;

Function point_add_internal

fun point_add_internal(a: &ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint, in_place: bool): u64

pragma opaque;

Function point_sub_internal

fun point_sub_internal(a: &ristretto255::RistrettoPoint, b: &ristretto255::RistrettoPoint, in_place: bool): u64

pragma opaque;

Function point_neg_internal

fun point_neg_internal(a: &ristretto255::RistrettoPoint, in_place: bool): u64

pragma opaque;

Function double_scalar_mul_internal

fun double_scalar_mul_internal(point1: u64, point2: u64, scalar1: vector<u8>, scalar2: vector<u8>): u64

pragma opaque;

Function multi_scalar_mul_internal

fun multi_scalar_mul_internal<P, S>(points: &vector<P>, scalars: &vector<S>): u64

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_multi_scalar_mul_internal<P, S>(points, scalars);

Function scalar_is_canonical_internal

fun scalar_is_canonical_internal(s: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_is_canonical_internal(s);

Function scalar_from_u64_internal

fun scalar_from_u64_internal(num: u64): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_from_u64_internal(num);

Function scalar_from_u128_internal

fun scalar_from_u128_internal(num: u128): vector<u8>

pragma opaque;
pragma bv=b"0";
aborts_if [abstract] false;
ensures result == spec_scalar_from_u128_internal(num);

Function scalar_reduced_from_32_bytes_internal

fun scalar_reduced_from_32_bytes_internal(bytes: vector<u8>): vector<u8>

pragma opaque;
ensures result == spec_scalar_reduced_from_32_bytes_internal(bytes);

Function scalar_uniform_from_64_bytes_internal

fun scalar_uniform_from_64_bytes_internal(bytes: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_uniform_from_64_bytes_internal(bytes);

Function scalar_invert_internal

fun scalar_invert_internal(bytes: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_invert_internal(bytes);

Function scalar_from_sha512_internal

fun scalar_from_sha512_internal(sha2_512_input: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_from_sha512_internal(sha2_512_input);

Function scalar_mul_internal

fun scalar_mul_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_mul_internal(a_bytes, b_bytes);

Function scalar_add_internal

fun scalar_add_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_add_internal(a_bytes, b_bytes);

Function scalar_sub_internal

fun scalar_sub_internal(a_bytes: vector<u8>, b_bytes: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_sub_internal(a_bytes, b_bytes);

Function scalar_neg_internal

fun scalar_neg_internal(a_bytes: vector<u8>): vector<u8>

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_scalar_neg_internal(a_bytes);