mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 19:05:51 +00:00
initial u256
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c053c7f1c8
commit
babb90832c
22 changed files with 6635 additions and 1 deletions
375
src/math/bigfix/Hacl_Bignum256.h
Normal file
375
src/math/bigfix/Hacl_Bignum256.h
Normal file
|
|
@ -0,0 +1,375 @@
|
|||
/* MIT License
|
||||
*
|
||||
* Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
|
||||
*
|
||||
* Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
* of this software and associated documentation files (the "Software"), to deal
|
||||
* in the Software without restriction, including without limitation the rights
|
||||
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
* copies of the Software, and to permit persons to whom the Software is
|
||||
* furnished to do so, subject to the following conditions:
|
||||
*
|
||||
* The above copyright notice and this permission notice shall be included in all
|
||||
* copies or substantial portions of the Software.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
* SOFTWARE.
|
||||
*/
|
||||
|
||||
|
||||
#ifndef __Hacl_Bignum256_H
|
||||
#define __Hacl_Bignum256_H
|
||||
|
||||
#if defined(__cplusplus)
|
||||
extern "C" {
|
||||
#endif
|
||||
|
||||
#include "kremlin/internal/types.h"
|
||||
#include "kremlin/lowstar_endianness.h"
|
||||
#include <string.h>
|
||||
#include "kremlin/internal/target.h"
|
||||
|
||||
#include "Hacl_Bignum.h"
|
||||
#include "Hacl_Bignum_Base.h"
|
||||
|
||||
/*******************************************************************************
|
||||
|
||||
A verified 256-bit bignum library.
|
||||
|
||||
This is a 64-bit optimized version, where bignums are represented as an array
|
||||
of four unsigned 64-bit integers, i.e. uint64_t[4]. Furthermore, the
|
||||
limbs are stored in little-endian format, i.e. the least significant limb is at
|
||||
index 0. Each limb is stored in native format in memory. Example:
|
||||
|
||||
uint64_t sixteen[4] = { 0x10; 0x00; 0x00; 0x00 }
|
||||
|
||||
We strongly encourage users to go through the conversion functions, e.g.
|
||||
bn_from_bytes_be, to i) not depend on internal representation choices and ii)
|
||||
have the ability to switch easily to a 32-bit optimized version in the future.
|
||||
|
||||
*******************************************************************************/
|
||||
|
||||
/************************/
|
||||
/* Arithmetic functions */
|
||||
/************************/
|
||||
|
||||
|
||||
/*
|
||||
Write `a + b mod 2^256` in `res`.
|
||||
|
||||
This functions returns the carry.
|
||||
|
||||
The arguments a, b and res are meant to be 256-bit bignums, i.e. uint64_t[4]
|
||||
*/
|
||||
uint64_t Hacl_Bignum256_add(uint64_t *a, uint64_t *b, uint64_t *res);
|
||||
|
||||
/*
|
||||
Write `a - b mod 2^256` in `res`.
|
||||
|
||||
This functions returns the carry.
|
||||
|
||||
The arguments a, b and res are meant to be 256-bit bignums, i.e. uint64_t[4]
|
||||
*/
|
||||
uint64_t Hacl_Bignum256_sub(uint64_t *a, uint64_t *b, uint64_t *res);
|
||||
|
||||
/*
|
||||
Write `a * b` in `res`.
|
||||
|
||||
The arguments a and b are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
The outparam res is meant to be a 512-bit bignum, i.e. uint64_t[8].
|
||||
*/
|
||||
void Hacl_Bignum256_mul(uint64_t *a, uint64_t *b, uint64_t *res);
|
||||
|
||||
/*
|
||||
Write `a * a` in `res`.
|
||||
|
||||
The argument a is meant to be a 256-bit bignum, i.e. uint64_t[4].
|
||||
The outparam res is meant to be a 512-bit bignum, i.e. uint64_t[8].
|
||||
*/
|
||||
void Hacl_Bignum256_sqr(uint64_t *a, uint64_t *res);
|
||||
|
||||
/*
|
||||
Write `a mod n` in `res`.
|
||||
|
||||
The argument a is meant to be a 512-bit bignum, i.e. uint64_t[8].
|
||||
The argument n and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
|
||||
The function returns false if any of the following preconditions are violated,
|
||||
true otherwise.
|
||||
• 1 < n
|
||||
• n % 2 = 1
|
||||
*/
|
||||
bool Hacl_Bignum256_mod(uint64_t *n, uint64_t *a, uint64_t *res);
|
||||
|
||||
/*
|
||||
Write `a ^ b mod n` in `res`.
|
||||
|
||||
The arguments a, n and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
|
||||
The argument b is a bignum of any size, and bBits is an upper bound on the
|
||||
number of significant bits of b. A tighter bound results in faster execution
|
||||
time. When in doubt, the number of bits for the bignum size is always a safe
|
||||
default, e.g. if b is a 256-bit bignum, bBits should be 256.
|
||||
|
||||
The function is *NOT* constant-time on the argument b. See the
|
||||
mod_exp_consttime_* functions for constant-time variants.
|
||||
|
||||
The function returns false if any of the following preconditions are violated,
|
||||
true otherwise.
|
||||
• n % 2 = 1
|
||||
• 1 < n
|
||||
• b < pow2 bBits
|
||||
• a < n
|
||||
*/
|
||||
bool
|
||||
Hacl_Bignum256_mod_exp_vartime(
|
||||
uint64_t *n,
|
||||
uint64_t *a,
|
||||
uint32_t bBits,
|
||||
uint64_t *b,
|
||||
uint64_t *res
|
||||
);
|
||||
|
||||
/*
|
||||
Write `a ^ b mod n` in `res`.
|
||||
|
||||
The arguments a, n and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
|
||||
The argument b is a bignum of any size, and bBits is an upper bound on the
|
||||
number of significant bits of b. A tighter bound results in faster execution
|
||||
time. When in doubt, the number of bits for the bignum size is always a safe
|
||||
default, e.g. if b is a 256-bit bignum, bBits should be 256.
|
||||
|
||||
This function is constant-time over its argument b, at the cost of a slower
|
||||
execution time than mod_exp_vartime.
|
||||
|
||||
The function returns false if any of the following preconditions are violated,
|
||||
true otherwise.
|
||||
• n % 2 = 1
|
||||
• 1 < n
|
||||
• b < pow2 bBits
|
||||
• a < n
|
||||
*/
|
||||
bool
|
||||
Hacl_Bignum256_mod_exp_consttime(
|
||||
uint64_t *n,
|
||||
uint64_t *a,
|
||||
uint32_t bBits,
|
||||
uint64_t *b,
|
||||
uint64_t *res
|
||||
);
|
||||
|
||||
/*
|
||||
Write `a ^ (-1) mod n` in `res`.
|
||||
|
||||
The arguments a, n and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
|
||||
Before calling this function, the caller will need to ensure that the following
|
||||
preconditions are observed.
|
||||
• n is a prime
|
||||
|
||||
The function returns false if any of the following preconditions are violated, true otherwise.
|
||||
• n % 2 = 1
|
||||
• 1 < n
|
||||
• 0 < a
|
||||
• a < n
|
||||
*/
|
||||
bool Hacl_Bignum256_mod_inv_prime_vartime(uint64_t *n, uint64_t *a, uint64_t *res);
|
||||
|
||||
typedef struct Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_s
|
||||
{
|
||||
uint32_t len;
|
||||
uint64_t *n;
|
||||
uint64_t mu;
|
||||
uint64_t *r2;
|
||||
}
|
||||
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
|
||||
|
||||
|
||||
/**********************************************/
|
||||
/* Arithmetic functions with precomputations. */
|
||||
/**********************************************/
|
||||
|
||||
|
||||
/*
|
||||
Heap-allocate and initialize a montgomery context.
|
||||
|
||||
The argument n is meant to be a 256-bit bignum, i.e. uint64_t[4].
|
||||
|
||||
Before calling this function, the caller will need to ensure that the following
|
||||
preconditions are observed.
|
||||
• n % 2 = 1
|
||||
• 1 < n
|
||||
|
||||
The caller will need to call Hacl_Bignum256_mont_ctx_free on the return value
|
||||
to avoid memory leaks.
|
||||
*/
|
||||
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *Hacl_Bignum256_mont_ctx_init(uint64_t *n);
|
||||
|
||||
/*
|
||||
Deallocate the memory previously allocated by Hacl_Bignum256_mont_ctx_init.
|
||||
|
||||
The argument k is a montgomery context obtained through Hacl_Bignum256_mont_ctx_init.
|
||||
*/
|
||||
void Hacl_Bignum256_mont_ctx_free(Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k);
|
||||
|
||||
/*
|
||||
Write `a mod n` in `res`.
|
||||
|
||||
The argument a is meant to be a 512-bit bignum, i.e. uint64_t[8].
|
||||
The outparam res is meant to be a 256-bit bignum, i.e. uint64_t[4].
|
||||
The argument k is a montgomery context obtained through Hacl_Bignum256_mont_ctx_init.
|
||||
*/
|
||||
void
|
||||
Hacl_Bignum256_mod_precomp(
|
||||
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
|
||||
uint64_t *a,
|
||||
uint64_t *res
|
||||
);
|
||||
|
||||
/*
|
||||
Write `a ^ b mod n` in `res`.
|
||||
|
||||
The arguments a and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
The argument k is a montgomery context obtained through Hacl_Bignum256_mont_ctx_init.
|
||||
|
||||
The argument b is a bignum of any size, and bBits is an upper bound on the
|
||||
number of significant bits of b. A tighter bound results in faster execution
|
||||
time. When in doubt, the number of bits for the bignum size is always a safe
|
||||
default, e.g. if b is a 256-bit bignum, bBits should be 256.
|
||||
|
||||
The function is *NOT* constant-time on the argument b. See the
|
||||
mod_exp_consttime_* functions for constant-time variants.
|
||||
|
||||
Before calling this function, the caller will need to ensure that the following
|
||||
preconditions are observed.
|
||||
• b < pow2 bBits
|
||||
• a < n
|
||||
*/
|
||||
void
|
||||
Hacl_Bignum256_mod_exp_vartime_precomp(
|
||||
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
|
||||
uint64_t *a,
|
||||
uint32_t bBits,
|
||||
uint64_t *b,
|
||||
uint64_t *res
|
||||
);
|
||||
|
||||
/*
|
||||
Write `a ^ b mod n` in `res`.
|
||||
|
||||
The arguments a and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
The argument k is a montgomery context obtained through Hacl_Bignum256_mont_ctx_init.
|
||||
|
||||
The argument b is a bignum of any size, and bBits is an upper bound on the
|
||||
number of significant bits of b. A tighter bound results in faster execution
|
||||
time. When in doubt, the number of bits for the bignum size is always a safe
|
||||
default, e.g. if b is a 256-bit bignum, bBits should be 256.
|
||||
|
||||
This function is constant-time over its argument b, at the cost of a slower
|
||||
execution time than mod_exp_vartime_*.
|
||||
|
||||
Before calling this function, the caller will need to ensure that the following
|
||||
preconditions are observed.
|
||||
• b < pow2 bBits
|
||||
• a < n
|
||||
*/
|
||||
void
|
||||
Hacl_Bignum256_mod_exp_consttime_precomp(
|
||||
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
|
||||
uint64_t *a,
|
||||
uint32_t bBits,
|
||||
uint64_t *b,
|
||||
uint64_t *res
|
||||
);
|
||||
|
||||
/*
|
||||
Write `a ^ (-1) mod n` in `res`.
|
||||
|
||||
The argument a and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
The argument k is a montgomery context obtained through Hacl_Bignum256_mont_ctx_init.
|
||||
|
||||
Before calling this function, the caller will need to ensure that the following
|
||||
preconditions are observed.
|
||||
• n is a prime
|
||||
• 0 < a
|
||||
• a < n
|
||||
*/
|
||||
void
|
||||
Hacl_Bignum256_mod_inv_prime_vartime_precomp(
|
||||
Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 *k,
|
||||
uint64_t *a,
|
||||
uint64_t *res
|
||||
);
|
||||
|
||||
|
||||
/********************/
|
||||
/* Loads and stores */
|
||||
/********************/
|
||||
|
||||
|
||||
/*
|
||||
Load a bid-endian bignum from memory.
|
||||
|
||||
The argument b points to len bytes of valid memory.
|
||||
The function returns a heap-allocated bignum of size sufficient to hold the
|
||||
result of loading b, or NULL if either the allocation failed, or the amount of
|
||||
required memory would exceed 4GB.
|
||||
|
||||
If the return value is non-null, clients must eventually call free(3) on it to
|
||||
avoid memory leaks.
|
||||
*/
|
||||
uint64_t *Hacl_Bignum256_new_bn_from_bytes_be(uint32_t len, uint8_t *b);
|
||||
|
||||
/*
|
||||
Load a little-endian bignum from memory.
|
||||
|
||||
The argument b points to len bytes of valid memory.
|
||||
The function returns a heap-allocated bignum of size sufficient to hold the
|
||||
result of loading b, or NULL if either the allocation failed, or the amount of
|
||||
required memory would exceed 4GB.
|
||||
|
||||
If the return value is non-null, clients must eventually call free(3) on it to
|
||||
avoid memory leaks.
|
||||
*/
|
||||
uint64_t *Hacl_Bignum256_new_bn_from_bytes_le(uint32_t len, uint8_t *b);
|
||||
|
||||
/*
|
||||
Serialize a bignum into big-endian memory.
|
||||
|
||||
The argument b points to a 256-bit bignum.
|
||||
The outparam res points to 32 bytes of valid memory.
|
||||
*/
|
||||
void Hacl_Bignum256_bn_to_bytes_be(uint64_t *b, uint8_t *res);
|
||||
|
||||
/*
|
||||
Serialize a bignum into little-endian memory.
|
||||
|
||||
The argument b points to a 256-bit bignum.
|
||||
The outparam res points to 32 bytes of valid memory.
|
||||
*/
|
||||
void Hacl_Bignum256_bn_to_bytes_le(uint64_t *b, uint8_t *res);
|
||||
|
||||
|
||||
/***************/
|
||||
/* Comparisons */
|
||||
/***************/
|
||||
|
||||
|
||||
/*
|
||||
Returns 2 ^ 64 - 1 if and only if the argument a is strictly less than the argument b,
|
||||
otherwise returns 0.
|
||||
*/
|
||||
uint64_t Hacl_Bignum256_lt_mask(uint64_t *a, uint64_t *b);
|
||||
|
||||
#if defined(__cplusplus)
|
||||
}
|
||||
#endif
|
||||
|
||||
#define __Hacl_Bignum256_H_DEFINED
|
||||
#endif
|
||||
Loading…
Add table
Add a link
Reference in a new issue