diff options
Diffstat (limited to 'security/nss/lib/freebl/verified/internal')
10 files changed, 919 insertions, 0 deletions
diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Bignum.h b/security/nss/lib/freebl/verified/internal/Hacl_Bignum.h new file mode 100644 index 0000000000..6080d37873 --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Bignum.h @@ -0,0 +1,312 @@ +/* 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 __internal_Hacl_Bignum_H +#define __internal_Hacl_Bignum_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "internal/Hacl_Krmllib.h" +#include "../Hacl_Bignum.h" +#include "lib_intrinsics.h" +void +Hacl_Bignum_Karatsuba_bn_karatsuba_mul_uint32( + uint32_t aLen, + uint32_t *a, + uint32_t *b, + uint32_t *tmp, + uint32_t *res); + +void +Hacl_Bignum_Karatsuba_bn_karatsuba_mul_uint64( + uint32_t aLen, + uint64_t *a, + uint64_t *b, + uint64_t *tmp, + uint64_t *res); + +void +Hacl_Bignum_Karatsuba_bn_karatsuba_sqr_uint32( + uint32_t aLen, + uint32_t *a, + uint32_t *tmp, + uint32_t *res); + +void +Hacl_Bignum_Karatsuba_bn_karatsuba_sqr_uint64( + uint32_t aLen, + uint64_t *a, + uint64_t *tmp, + uint64_t *res); + +void +Hacl_Bignum_bn_add_mod_n_u32( + uint32_t len1, + uint32_t *n, + uint32_t *a, + uint32_t *b, + uint32_t *res); + +void +Hacl_Bignum_bn_add_mod_n_u64( + uint32_t len1, + uint64_t *n, + uint64_t *a, + uint64_t *b, + uint64_t *res); + +void +Hacl_Bignum_bn_sub_mod_n_u32( + uint32_t len1, + uint32_t *n, + uint32_t *a, + uint32_t *b, + uint32_t *res); + +void +Hacl_Bignum_bn_sub_mod_n_u64( + uint32_t len1, + uint64_t *n, + uint64_t *a, + uint64_t *b, + uint64_t *res); + +uint32_t Hacl_Bignum_ModInvLimb_mod_inv_uint32(uint32_t n0); + +uint64_t Hacl_Bignum_ModInvLimb_mod_inv_uint64(uint64_t n0); + +uint32_t Hacl_Bignum_Montgomery_bn_check_modulus_u32(uint32_t len, uint32_t *n); + +void +Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u32( + uint32_t len, + uint32_t nBits, + uint32_t *n, + uint32_t *res); + +void +Hacl_Bignum_Montgomery_bn_mont_reduction_u32( + uint32_t len, + uint32_t *n, + uint32_t nInv, + uint32_t *c, + uint32_t *res); + +void +Hacl_Bignum_Montgomery_bn_to_mont_u32( + uint32_t len, + uint32_t *n, + uint32_t nInv, + uint32_t *r2, + uint32_t *a, + uint32_t *aM); + +void +Hacl_Bignum_Montgomery_bn_from_mont_u32( + uint32_t len, + uint32_t *n, + uint32_t nInv_u64, + uint32_t *aM, + uint32_t *a); + +void +Hacl_Bignum_Montgomery_bn_mont_mul_u32( + uint32_t len, + uint32_t *n, + uint32_t nInv_u64, + uint32_t *aM, + uint32_t *bM, + uint32_t *resM); + +void +Hacl_Bignum_Montgomery_bn_mont_sqr_u32( + uint32_t len, + uint32_t *n, + uint32_t nInv_u64, + uint32_t *aM, + uint32_t *resM); + +uint64_t Hacl_Bignum_Montgomery_bn_check_modulus_u64(uint32_t len, uint64_t *n); + +void +Hacl_Bignum_Montgomery_bn_precomp_r2_mod_n_u64( + uint32_t len, + uint32_t nBits, + uint64_t *n, + uint64_t *res); + +void +Hacl_Bignum_Montgomery_bn_mont_reduction_u64( + uint32_t len, + uint64_t *n, + uint64_t nInv, + uint64_t *c, + uint64_t *res); + +void +Hacl_Bignum_Montgomery_bn_to_mont_u64( + uint32_t len, + uint64_t *n, + uint64_t nInv, + uint64_t *r2, + uint64_t *a, + uint64_t *aM); + +void +Hacl_Bignum_Montgomery_bn_from_mont_u64( + uint32_t len, + uint64_t *n, + uint64_t nInv_u64, + uint64_t *aM, + uint64_t *a); + +void +Hacl_Bignum_Montgomery_bn_mont_mul_u64( + uint32_t len, + uint64_t *n, + uint64_t nInv_u64, + uint64_t *aM, + uint64_t *bM, + uint64_t *resM); + +void +Hacl_Bignum_Montgomery_bn_mont_sqr_u64( + uint32_t len, + uint64_t *n, + uint64_t nInv_u64, + uint64_t *aM, + uint64_t *resM); + +uint32_t +Hacl_Bignum_Exponentiation_bn_check_mod_exp_u32( + uint32_t len, + uint32_t *n, + uint32_t *a, + uint32_t bBits, + uint32_t *b); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_precomp_u32( + uint32_t len, + uint32_t *n, + uint32_t mu, + uint32_t *r2, + uint32_t *a, + uint32_t bBits, + uint32_t *b, + uint32_t *res); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_precomp_u32( + uint32_t len, + uint32_t *n, + uint32_t mu, + uint32_t *r2, + uint32_t *a, + uint32_t bBits, + uint32_t *b, + uint32_t *res); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_u32( + uint32_t len, + uint32_t nBits, + uint32_t *n, + uint32_t *a, + uint32_t bBits, + uint32_t *b, + uint32_t *res); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_u32( + uint32_t len, + uint32_t nBits, + uint32_t *n, + uint32_t *a, + uint32_t bBits, + uint32_t *b, + uint32_t *res); + +uint64_t +Hacl_Bignum_Exponentiation_bn_check_mod_exp_u64( + uint32_t len, + uint64_t *n, + uint64_t *a, + uint32_t bBits, + uint64_t *b); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_precomp_u64( + uint32_t len, + uint64_t *n, + uint64_t mu, + uint64_t *r2, + uint64_t *a, + uint32_t bBits, + uint64_t *b, + uint64_t *res); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_precomp_u64( + uint32_t len, + uint64_t *n, + uint64_t mu, + uint64_t *r2, + uint64_t *a, + uint32_t bBits, + uint64_t *b, + uint64_t *res); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_vartime_u64( + uint32_t len, + uint32_t nBits, + uint64_t *n, + uint64_t *a, + uint32_t bBits, + uint64_t *b, + uint64_t *res); + +void +Hacl_Bignum_Exponentiation_bn_mod_exp_consttime_u64( + uint32_t len, + uint32_t nBits, + uint64_t *n, + uint64_t *a, + uint32_t bBits, + uint64_t *b, + uint64_t *res); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Bignum_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Chacha20.h b/security/nss/lib/freebl/verified/internal/Hacl_Chacha20.h new file mode 100644 index 0000000000..51ecfeef39 --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Chacha20.h @@ -0,0 +1,50 @@ +/* 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 __internal_Hacl_Chacha20_H +#define __internal_Hacl_Chacha20_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Chacha20.h" + +extern const uint32_t Hacl_Impl_Chacha20_Vec_chacha20_constants[4U]; + +void Hacl_Impl_Chacha20_chacha20_init(uint32_t *ctx, uint8_t *k, uint8_t *n, uint32_t ctr); + +void +Hacl_Impl_Chacha20_chacha20_update(uint32_t *ctx, uint32_t len, uint8_t *out, uint8_t *text); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Chacha20_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Curve25519_51.h b/security/nss/lib/freebl/verified/internal/Hacl_Curve25519_51.h new file mode 100644 index 0000000000..d7d05e89f5 --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Curve25519_51.h @@ -0,0 +1,53 @@ +/* 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 __internal_Hacl_Curve25519_51_H +#define __internal_Hacl_Curve25519_51_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "internal/Hacl_Krmllib.h" +#include "../Hacl_Curve25519_51.h" + +void +Hacl_Curve25519_51_fsquare_times( + uint64_t *o, + uint64_t *inp, + FStar_UInt128_uint128 *tmp, + uint32_t n); + +void Hacl_Curve25519_51_finv(uint64_t *o, uint64_t *i, FStar_UInt128_uint128 *tmp); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Curve25519_51_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA1.h b/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA1.h new file mode 100644 index 0000000000..02ee03247a --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA1.h @@ -0,0 +1,49 @@ +/* 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 __internal_Hacl_Hash_SHA1_H +#define __internal_Hacl_Hash_SHA1_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Hash_SHA1.h" + +void Hacl_Hash_Core_SHA1_legacy_init(uint32_t *s); + +void Hacl_Hash_Core_SHA1_legacy_update(uint32_t *h, uint8_t *l); + +void Hacl_Hash_Core_SHA1_legacy_finish(uint32_t *s, uint8_t *dst); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Hash_SHA1_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA2.h b/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA2.h new file mode 100644 index 0000000000..ed9894e717 --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Hash_SHA2.h @@ -0,0 +1,65 @@ +/* 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 __internal_Hacl_Hash_SHA2_H +#define __internal_Hacl_Hash_SHA2_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Hash_SHA2.h" + +void Hacl_Hash_Core_SHA2_init_224(uint32_t *s); + +void Hacl_Hash_Core_SHA2_init_256(uint32_t *s); + +void Hacl_Hash_Core_SHA2_init_384(uint64_t *s); + +void Hacl_Hash_Core_SHA2_init_512(uint64_t *s); + +void Hacl_Hash_Core_SHA2_update_384(uint64_t *hash, uint8_t *block); + +void Hacl_Hash_Core_SHA2_update_512(uint64_t *hash, uint8_t *block); + +void Hacl_Hash_Core_SHA2_pad_256(uint64_t len, uint8_t *dst); + +void Hacl_Hash_Core_SHA2_finish_224(uint32_t *s, uint8_t *dst); + +void Hacl_Hash_Core_SHA2_finish_256(uint32_t *s, uint8_t *dst); + +void Hacl_Hash_Core_SHA2_finish_384(uint64_t *s, uint8_t *dst); + +void Hacl_Hash_Core_SHA2_finish_512(uint64_t *s, uint8_t *dst); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Hash_SHA2_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Krmllib.h b/security/nss/lib/freebl/verified/internal/Hacl_Krmllib.h new file mode 100644 index 0000000000..3778437448 --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Krmllib.h @@ -0,0 +1,45 @@ +/* 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 __internal_Hacl_Krmllib_H +#define __internal_Hacl_Krmllib_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Krmllib.h" + +uint32_t LowStar_Vector_new_capacity(uint32_t cap); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Krmllib_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_128.h b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_128.h new file mode 100644 index 0000000000..d5f257302d --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_128.h @@ -0,0 +1,51 @@ +/* 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 __internal_Hacl_Poly1305_128_H +#define __internal_Hacl_Poly1305_128_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Poly1305_128.h" +#include "libintvector.h" +void +Hacl_Impl_Poly1305_Field32xN_128_load_acc2(Lib_IntVector_Intrinsics_vec128 *acc, uint8_t *b); + +void +Hacl_Impl_Poly1305_Field32xN_128_fmul_r2_normalize( + Lib_IntVector_Intrinsics_vec128 *out, + Lib_IntVector_Intrinsics_vec128 *p); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Poly1305_128_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_256.h b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_256.h new file mode 100644 index 0000000000..9b10379237 --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Poly1305_256.h @@ -0,0 +1,51 @@ +/* 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 __internal_Hacl_Poly1305_256_H +#define __internal_Hacl_Poly1305_256_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Poly1305_256.h" +#include "libintvector.h" +void +Hacl_Impl_Poly1305_Field32xN_256_load_acc4(Lib_IntVector_Intrinsics_vec256 *acc, uint8_t *b); + +void +Hacl_Impl_Poly1305_Field32xN_256_fmul_r4_normalize( + Lib_IntVector_Intrinsics_vec256 *out, + Lib_IntVector_Intrinsics_vec256 *p); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Poly1305_256_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Hacl_Spec.h b/security/nss/lib/freebl/verified/internal/Hacl_Spec.h new file mode 100644 index 0000000000..cf5376abab --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Hacl_Spec.h @@ -0,0 +1,59 @@ +/* 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 __internal_Hacl_Spec_H +#define __internal_Hacl_Spec_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +#include "../Hacl_Spec.h" + +#define Spec_ECDSA_NoHash 0 +#define Spec_ECDSA_Hash 1 + +typedef uint8_t Spec_ECDSA_hash_alg_ecdsa_tags; + +typedef struct Spec_ECDSA_hash_alg_ecdsa_s { + Spec_ECDSA_hash_alg_ecdsa_tags tag; + Spec_Hash_Definitions_hash_alg _0; +} Spec_ECDSA_hash_alg_ecdsa; + +#define Spec_Cipher_Expansion_Hacl_CHACHA20 0 +#define Spec_Cipher_Expansion_Vale_AES128 1 +#define Spec_Cipher_Expansion_Vale_AES256 2 + +typedef uint8_t Spec_Cipher_Expansion_impl; + +#if defined(__cplusplus) +} +#endif + +#define __internal_Hacl_Spec_H_DEFINED +#endif diff --git a/security/nss/lib/freebl/verified/internal/Vale.h b/security/nss/lib/freebl/verified/internal/Vale.h new file mode 100644 index 0000000000..400650e95f --- /dev/null +++ b/security/nss/lib/freebl/verified/internal/Vale.h @@ -0,0 +1,184 @@ +/* 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 __internal_Vale_H +#define __internal_Vale_H + +#if defined(__cplusplus) +extern "C" { +#endif + +#include <string.h> +#include "krml/internal/types.h" +#include "krml/lowstar_endianness.h" +#include "krml/internal/target.h" + +extern uint64_t add_scalar_e(uint64_t *x0, uint64_t *x1, uint64_t x2); + +extern uint64_t fadd_e(uint64_t *x0, uint64_t *x1, uint64_t *x2); + +extern uint64_t sha256_update(uint32_t *x0, uint8_t *x1, uint64_t x2, uint32_t *x3); + +extern uint64_t x64_poly1305(uint8_t *x0, uint8_t *x1, uint64_t x2, uint64_t x3); + +extern uint64_t check_aesni(); + +extern uint64_t check_sha(); + +extern uint64_t check_adx_bmi2(); + +extern uint64_t check_avx(); + +extern uint64_t check_avx2(); + +extern uint64_t check_movbe(); + +extern uint64_t check_sse(); + +extern uint64_t check_rdrand(); + +extern uint64_t check_avx512(); + +extern uint64_t check_osxsave(); + +extern uint64_t check_avx_xcr0(); + +extern uint64_t check_avx512_xcr0(); + +extern uint64_t +gcm128_decrypt_opt( + uint8_t *x0, + uint64_t x1, + uint64_t x2, + uint8_t *x3, + uint8_t *x4, + uint8_t *x5, + uint8_t *x6, + uint8_t *x7, + uint8_t *x8, + uint64_t x9, + uint8_t *x10, + uint8_t *x11, + uint64_t x12, + uint8_t *x13, + uint64_t x14, + uint8_t *x15, + uint8_t *x16); + +extern uint64_t +gcm256_decrypt_opt( + uint8_t *x0, + uint64_t x1, + uint64_t x2, + uint8_t *x3, + uint8_t *x4, + uint8_t *x5, + uint8_t *x6, + uint8_t *x7, + uint8_t *x8, + uint64_t x9, + uint8_t *x10, + uint8_t *x11, + uint64_t x12, + uint8_t *x13, + uint64_t x14, + uint8_t *x15, + uint8_t *x16); + +extern uint64_t aes128_key_expansion(uint8_t *x0, uint8_t *x1); + +extern uint64_t aes256_key_expansion(uint8_t *x0, uint8_t *x1); + +extern uint64_t +compute_iv_stdcall( + uint8_t *x0, + uint64_t x1, + uint64_t x2, + uint8_t *x3, + uint8_t *x4, + uint8_t *x5); + +extern uint64_t +gcm128_encrypt_opt( + uint8_t *x0, + uint64_t x1, + uint64_t x2, + uint8_t *x3, + uint8_t *x4, + uint8_t *x5, + uint8_t *x6, + uint8_t *x7, + uint8_t *x8, + uint64_t x9, + uint8_t *x10, + uint8_t *x11, + uint64_t x12, + uint8_t *x13, + uint64_t x14, + uint8_t *x15, + uint8_t *x16); + +extern uint64_t +gcm256_encrypt_opt( + uint8_t *x0, + uint64_t x1, + uint64_t x2, + uint8_t *x3, + uint8_t *x4, + uint8_t *x5, + uint8_t *x6, + uint8_t *x7, + uint8_t *x8, + uint64_t x9, + uint8_t *x10, + uint8_t *x11, + uint64_t x12, + uint8_t *x13, + uint64_t x14, + uint8_t *x15, + uint8_t *x16); + +extern uint64_t aes128_keyhash_init(uint8_t *x0, uint8_t *x1); + +extern uint64_t aes256_keyhash_init(uint8_t *x0, uint8_t *x1); + +extern uint64_t cswap2_e(uint64_t x0, uint64_t *x1, uint64_t *x2); + +extern uint64_t fsqr_e(uint64_t *x0, uint64_t *x1, uint64_t *x2); + +extern uint64_t fsqr2_e(uint64_t *x0, uint64_t *x1, uint64_t *x2); + +extern uint64_t fmul_e(uint64_t *x0, uint64_t *x1, uint64_t *x2, uint64_t *x3); + +extern uint64_t fmul2_e(uint64_t *x0, uint64_t *x1, uint64_t *x2, uint64_t *x3); + +extern uint64_t fmul_scalar_e(uint64_t *x0, uint64_t *x1, uint64_t x2); + +extern uint64_t fsub_e(uint64_t *x0, uint64_t *x1, uint64_t *x2); + +#if defined(__cplusplus) +} +#endif + +#define __internal_Vale_H_DEFINED +#endif |