/* 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_Impl_FFDHE_Constants_H #define __Hacl_Impl_FFDHE_Constants_H #if defined(__cplusplus) extern "C" { #endif #include "evercrypt_targetconfig.h" #include "libintvector.h" #include "kremlin/internal/types.h" #include "kremlin/lowstar_endianness.h" #include #include "kremlin/internal/target.h" static const uint8_t Hacl_Impl_FFDHE_Constants_ffdhe_g2[1U] = { (uint8_t)0x02U }; static const uint8_t Hacl_Impl_FFDHE_Constants_ffdhe_p2048[256U] = { (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xADU, (uint8_t)0xF8U, (uint8_t)0x54U, (uint8_t)0x58U, (uint8_t)0xA2U, (uint8_t)0xBBU, (uint8_t)0x4AU, (uint8_t)0x9AU, (uint8_t)0xAFU, (uint8_t)0xDCU, (uint8_t)0x56U, (uint8_t)0x20U, (uint8_t)0x27U, (uint8_t)0x3DU, (uint8_t)0x3CU, (uint8_t)0xF1U, (uint8_t)0xD8U, (uint8_t)0xB9U, (uint8_t)0xC5U, (uint8_t)0x83U, (uint8_t)0xCEU, (uint8_t)0x2DU, (uint8_t)0x36U, (uint8_t)0x95U, (uint8_t)0xA9U, (uint8_t)0xE1U, (uint8_t)0x36U, (uint8_t)0x41U, (uint8_t)0x14U, (uint8_t)0x64U, (uint8_t)0x33U, (uint8_t)0xFBU, (uint8_t)0xCCU, (uint8_t)0x93U, (uint8_t)0x9DU, (uint8_t)0xCEU, (uint8_t)0x24U, (uint8_t)0x9BU, (uint8_t)0x3EU, (uint8_t)0xF9U, (uint8_t)0x7DU, (uint8_t)0x2FU, (uint8_t)0xE3U, (uint8_t)0x63U, (uint8_t)0x63U, (uint8_t)0x0CU, (uint8_t)0x75U, (uint8_t)0xD8U, (uint8_t)0xF6U, (uint8_t)0x81U, (uint8_t)0xB2U, (uint8_t)0x02U, (uint8_t)0xAEU, (uint8_t)0xC4U, (uint8_t)0x61U, (uint8_t)0x7AU, (uint8_t)0xD3U, (uint8_t)0xDFU, (uint8_t)0x1EU, (uint8_t)0xD5U, (uint8_t)0xD5U, (uint8_t)0xFDU, (uint8_t)0x65U, (uint8_t)0x61U, (uint8_t)0x24U, (uint8_t)0x33U, (uint8_t)0xF5U, (uint8_t)0x1FU, (uint8_t)0x5FU, (uint8_t)0x06U, (uint8_t)0x6EU, (uint8_t)0xD0U, (uint8_t)0x85U, (uint8_t)0x63U, (uint8_t)0x65U, (uint8_t)0x55U, (uint8_t)0x3DU, (uint8_t)0xEDU, (uint8_t)0x1AU, (uint8_t)0xF3U, (uint8_t)0xB5U, (uint8_t)0x57U, (uint8_t)0x13U, (uint8_t)0x5EU, (uint8_t)0x7FU, (uint8_t)0x57U, (uint8_t)0xC9U, (uint8_t)0x35U, (uint8_t)0x98U, (uint8_t)0x4FU, (uint8_t)0x0CU, (uint8_t)0x70U, (uint8_t)0xE0U, (uint8_t)0xE6U, (uint8_t)0x8BU, (uint8_t)0x77U, (uint8_t)0xE2U, (uint8_t)0xA6U, (uint8_t)0x89U, (uint8_t)0xDAU, (uint8_t)0xF3U, (uint8_t)0xEFU, (uint8_t)0xE8U, (uint8_t)0x72U, (uint8_t)0x1DU, (uint8_t)0xF1U, (uint8_t)0x58U, (uint8_t)0xA1U, (uint8_t)0x36U, (uint8_t)0xADU, (uint8_t)0xE7U, (uint8_t)0x35U, (uint8_t)0x30U, (uint8_t)0xACU, (uint8_t)0xCAU, (uint8_t)0x4FU, (uint8_t)0x48U, (uint8_t)0x3AU, (uint8_t)0x79U, (uint8_t)0x7AU, (uint8_t)0xBCU, (uint8_t)0x0AU, (uint8_t)0xB1U, (uint8_t)0x82U, (uint8_t)0xB3U, (uint8_t)0x24U, (uint8_t)0xFBU, (uint8_t)0x61U, (uint8_t)0xD1U, (uint8_t)0x08U, (uint8_t)0xA9U, (uint8_t)0x4BU, (uint8_t)0xB2U, (uint8_t)0xC8U, (uint8_t)0xE3U, (uint8_t)0xFBU, (uint8_t)0xB9U, (uint8_t)0x6AU, (uint8_t)0xDAU, (uint8_t)0xB7U, (uint8_t)0x60U, (uint8_t)0xD7U, (uint8_t)0xF4U, (uint8_t)0x68U, (uint8_t)0x1DU, (uint8_t)0x4FU, (uint8_t)0x42U, (uint8_t)0xA3U, (uint8_t)0xDEU, (uint8_t)0x39U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xAEU, (uint8_t)0x56U, (uint8_t)0xEDU, (uint8_t)0xE7U, (uint8_t)0x63U, (uint8_t)0x72U, (uint8_t)0xBBU, (uint8_t)0x19U, (uint8_t)0x0BU, (uint8_t)0x07U, (uint8_t)0xA7U, (uint8_t)0xC8U, (uint8_t)0xEEU, (uint8_t)0x0AU, (uint8_t)0x6DU, (uint8_t)0x70U, (uint8_t)0x9EU, (uint8_t)0x02U, (uint8_t)0xFCU, (uint8_t)0xE1U, (uint8_t)0xCDU, (uint8_t)0xF7U, (uint8_t)0xE2U, (uint8_t)0xECU, (uint8_t)0xC0U, (uint8_t)0x34U, (uint8_t)0x04U, (uint8_t)0xCDU, (uint8_t)0x28U, (uint8_t)0x34U, (uint8_t)0x2FU, (uint8_t)0x61U, (uint8_t)0x91U, (uint8_t)0x72U, (uint8_t)0xFEU, (uint8_t)0x9CU, (uint8_t)0xE9U, (uint8_t)0x85U, (uint8_t)0x83U, (uint8_t)0xFFU, (uint8_t)0x8EU, (uint8_t)0x4FU, (uint8_t)0x12U, (uint8_t)0x32U, (uint8_t)0xEEU, (uint8_t)0xF2U, (uint8_t)0x81U, (uint8_t)0x83U, (uint8_t)0xC3U, (uint8_t)0xFEU, (uint8_t)0x3BU, (uint8_t)0x1BU, (uint8_t)0x4CU, (uint8_t)0x6FU, (uint8_t)0xADU, (uint8_t)0x73U, (uint8_t)0x3BU, (uint8_t)0xB5U, (uint8_t)0xFCU, (uint8_t)0xBCU, (uint8_t)0x2EU, (uint8_t)0xC2U, (uint8_t)0x20U, (uint8_t)0x05U, (uint8_t)0xC5U, (uint8_t)0x8EU, (uint8_t)0xF1U, (uint8_t)0x83U, (uint8_t)0x7DU, (uint8_t)0x16U, (uint8_t)0x83U, (uint8_t)0xB2U, (uint8_t)0xC6U, (uint8_t)0xF3U, (uint8_t)0x4AU, (uint8_t)0x26U, (uint8_t)0xC1U, (uint8_t)0xB2U, (uint8_t)0xEFU, (uint8_t)0xFAU, (uint8_t)0x88U, (uint8_t)0x6BU, (uint8_t)0x42U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0x28U, (uint8_t)0x5CU, (uint8_t)0x97U, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU }; static const uint8_t Hacl_Impl_FFDHE_Constants_ffdhe_p3072[384U] = { (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xADU, (uint8_t)0xF8U, (uint8_t)0x54U, (uint8_t)0x58U, (uint8_t)0xA2U, (uint8_t)0xBBU, (uint8_t)0x4AU, (uint8_t)0x9AU, (uint8_t)0xAFU, (uint8_t)0xDCU, (uint8_t)0x56U, (uint8_t)0x20U, (uint8_t)0x27U, (uint8_t)0x3DU, (uint8_t)0x3CU, (uint8_t)0xF1U, (uint8_t)0xD8U, (uint8_t)0xB9U, (uint8_t)0xC5U, (uint8_t)0x83U, (uint8_t)0xCEU, (uint8_t)0x2DU, (uint8_t)0x36U, (uint8_t)0x95U, (uint8_t)0xA9U, (uint8_t)0xE1U, (uint8_t)0x36U, (uint8_t)0x41U, (uint8_t)0x14U, (uint8_t)0x64U, (uint8_t)0x33U, (uint8_t)0xFBU, (uint8_t)0xCCU, (uint8_t)0x93U, (uint8_t)0x9DU, (uint8_t)0xCEU, (uint8_t)0x24U, (uint8_t)0x9BU, (uint8_t)0x3EU, (uint8_t)0xF9U, (uint8_t)0x7DU, (uint8_t)0x2FU, (uint8_t)0xE3U, (uint8_t)0x63U, (uint8_t)0x63U, (uint8_t)0x0CU, (uint8_t)0x75U, (uint8_t)0xD8U, (uint8_t)0xF6U, (uint8_t)0x81U, (uint8_t)0xB2U, (uint8_t)0x02U, (uint8_t)0xAEU, (uint8_t)0xC4U, (uint8_t)0x61U, (uint8_t)0x7AU, (uint8_t)0xD3U, (uint8_t)0xDFU, (uint8_t)0x1EU, (uint8_t)0xD5U, (uint8_t)0xD5U, (uint8_t)0xFDU, (uint8_t)0x65U, (uint8_t)0x61U, (uint8_t)0x24U, (uint8_t)0x33U, (uint8_t)0xF5U, (uint8_t)0x1FU, (uint8_t)0x5FU, (uint8_t)0x06U, (uint8_t)0x6EU, (uint8_t)0xD0U, (uint8_t)0x85U, (uint8_t)0x63U, (uint8_t)0x65U, (uint8_t)0x55U, (uint8_t)0x3DU, (uint8_t)0xEDU, (uint8_t)0x1AU, (uint8_t)0xF3U, (uint8_t)0xB5U, (uint8_t)0x57U, (uint8_t)0x13U, (uint8_t)0x5EU, (uint8_t)0x7FU, (uint8_t)0x57U, (uint8_t)0xC9U, (uint8_t)0x35U, (uint8_t)0x98U, (uint8_t)0x4FU, (uint8_t)0x0CU, (uint8_t)0x70U, (uint8_t)0xE0U, (uint8_t)0xE6U, (uint8_t)0x8BU, (uint8_t)0x77U, (uint8_t)0xE2U, (uint8_t)0xA6U, (uint8_t)0x89U, (uint8_t)0xDAU, (uint8_t)0xF3U, (uint8_t)0xEFU, (uint8_t)0xE8U, (uint8_t)0x72U, (uint8_t)0x1DU, (uint8_t)0xF1U, (uint8_t)0x58U, (uint8_t)0xA1U, (uint8_t)0x36U, (uint8_t)0xADU, (uint8_t)0xE7U, (uint8_t)0x35U, (uint8_t)0x30U, (uint8_t)0xACU, (uint8_t)0xCAU, (uint8_t)0x4FU, (uint8_t)0x48U, (uint8_t)0x3AU, (uint8_t)0x79U, (uint8_t)0x7AU, (uint8_t)0xBCU, (uint8_t)0x0AU, (uint8_t)0xB1U, (uint8_t)0x82U, (uint8_t)0xB3U, (uint8_t)0x24U, (uint8_t)0xFBU, (uint8_t)0x61U, (uint8_t)0xD1U, (uint8_t)0x08U, (uint8_t)0xA9U, (uint8_t)0x4BU, (uint8_t)0xB2U, (uint8_t)0xC8U, (uint8_t)0xE3U, (uint8_t)0xFBU, (uint8_t)0xB9U, (uint8_t)0x6AU, (uint8_t)0xDAU, (uint8_t)0xB7U, (uint8_t)0x60U, (uint8_t)0xD7U, (uint8_t)0xF4U, (uint8_t)0x68U, (uint8_t)0x1DU, (uint8_t)0x4FU, (uint8_t)0x42U, (uint8_t)0xA3U, (uint8_t)0xDEU, (uint8_t)0x39U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xAEU, (uint8_t)0x56U, (uint8_t)0xEDU, (uint8_t)0xE7U, (uint8_t)0x63U, (uint8_t)0x72U, (uint8_t)0xBBU, (uint8_t)0x19U, (uint8_t)0x0BU, (uint8_t)0x07U, (uint8_t)0xA7U, (uint8_t)0xC8U, (uint8_t)0xEEU, (uint8_t)0x0AU, (uint8_t)0x6DU, (uint8_t)0x70U, (uint8_t)0x9EU, (uint8_t)0x02U, (uint8_t)0xFCU, (uint8_t)0xE1U, (uint8_t)0xCDU, (uint8_t)0xF7U, (uint8_t)0xE2U, (uint8_t)0xECU, (uint8_t)0xC0U, (uint8_t)0x34U, (uint8_t)0x04U, (uint8_t)0xCDU, (uint8_t)0x28U, (uint8_t)0x34U, (uint8_t)0x2FU, (uint8_t)0x61U, (uint8_t)0x91U, (uint8_t)0x72U, (uint8_t)0xFEU, (uint8_t)0x9CU, (uint8_t)0xE9U, (uint8_t)0x85U, (uint8_t)0x83U, (uint8_t)0xFFU, (uint8_t)0x8EU, (uint8_t)0x4FU, (uint8_t)0x12U, (uint8_t)0x32U, (uint8_t)0xEEU, (uint8_t)0xF2U, (uint8_t)0x81U, (uint8_t)0x83U, (uint8_t)0xC3U, (uint8_t)0xFEU, (uint8_t)0x3BU, (uint8_t)0x1BU, (uint8_t)0x4CU, (uint8_t)0x6FU, (uint8_t)0xADU, (uint8_t)0x73U, (uint8_t)0x3BU, (uint8_t)0xB5U, (uint8_t)0xFCU, (uint8_t)0xBCU, (uint8_t)0x2EU, (uint8_t)0xC2U, (uint8_t)0x20U, (uint8_t)0x05U, (uint8_t)0xC5U, (uint8_t)0x8EU, (uint8_t)0xF1U, (uint8_t)0x83U, (uint8_t)0x7DU, (uint8_t)0x16U, (uint8_t)0x83U, (uint8_t)0xB2U, (uint8_t)0xC6U, (uint8_t)0xF3U, (uint8_t)0x4AU, (uint8_t)0x26U, (uint8_t)0xC1U, (uint8_t)0xB2U, (uint8_t)0xEFU, (uint8_t)0xFAU, (uint8_t)0x88U, (uint8_t)0x6BU, (uint8_t)0x42U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0x1FU, (uint8_t)0xCFU, (uint8_t)0xDCU, (uint8_t)0xDEU, (uint8_t)0x35U, (uint8_t)0x5BU, (uint8_t)0x3BU, (uint8_t)0x65U, (uint8_t)0x19U, (uint8_t)0x03U, (uint8_t)0x5BU, (uint8_t)0xBCU, (uint8_t)0x34U, (uint8_t)0xF4U, (uint8_t)0xDEU, (uint8_t)0xF9U, (uint8_t)0x9CU, (uint8_t)0x02U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0xB4U, (uint8_t)0x6FU, (uint8_t)0xC9U, (uint8_t)0xD6U, (uint8_t)0xE6U, (uint8_t)0xC9U, (uint8_t)0x07U, (uint8_t)0x7AU, (uint8_t)0xD9U, (uint8_t)0x1DU, (uint8_t)0x26U, (uint8_t)0x91U, (uint8_t)0xF7U, (uint8_t)0xF7U, (uint8_t)0xEEU, (uint8_t)0x59U, (uint8_t)0x8CU, (uint8_t)0xB0U, (uint8_t)0xFAU, (uint8_t)0xC1U, (uint8_t)0x86U, (uint8_t)0xD9U, (uint8_t)0x1CU, (uint8_t)0xAEU, (uint8_t)0xFEU, (uint8_t)0x13U, (uint8_t)0x09U, (uint8_t)0x85U, (uint8_t)0x13U, (uint8_t)0x92U, (uint8_t)0x70U, (uint8_t)0xB4U, (uint8_t)0x13U, (uint8_t)0x0CU, (uint8_t)0x93U, (uint8_t)0xBCU, (uint8_t)0x43U, (uint8_t)0x79U, (uint8_t)0x44U, (uint8_t)0xF4U, (uint8_t)0xFDU, (uint8_t)0x44U, (uint8_t)0x52U, (uint8_t)0xE2U, (uint8_t)0xD7U, (uint8_t)0x4DU, (uint8_t)0xD3U, (uint8_t)0x64U, (uint8_t)0xF2U, (uint8_t)0xE2U, (uint8_t)0x1EU, (uint8_t)0x71U, (uint8_t)0xF5U, (uint8_t)0x4BU, (uint8_t)0xFFU, (uint8_t)0x5CU, (uint8_t)0xAEU, (uint8_t)0x82U, (uint8_t)0xABU, (uint8_t)0x9CU, (uint8_t)0x9DU, (uint8_t)0xF6U, (uint8_t)0x9EU, (uint8_t)0xE8U, (uint8_t)0x6DU, (uint8_t)0x2BU, (uint8_t)0xC5U, (uint8_t)0x22U, (uint8_t)0x36U, (uint8_t)0x3AU, (uint8_t)0x0DU, (uint8_t)0xABU, (uint8_t)0xC5U, (uint8_t)0x21U, (uint8_t)0x97U, (uint8_t)0x9BU, (uint8_t)0x0DU, (uint8_t)0xEAU, (uint8_t)0xDAU, (uint8_t)0x1DU, (uint8_t)0xBFU, (uint8_t)0x9AU, (uint8_t)0x42U, (uint8_t)0xD5U, (uint8_t)0xC4U, (uint8_t)0x48U, (uint8_t)0x4EU, (uint8_t)0x0AU, (uint8_t)0xBCU, (uint8_t)0xD0U, (uint8_t)0x6BU, (uint8_t)0xFAU, (uint8_t)0x53U, (uint8_t)0xDDU, (uint8_t)0xEFU, (uint8_t)0x3CU, (uint8_t)0x1BU, (uint8_t)0x20U, (uint8_t)0xEEU, (uint8_t)0x3FU, (uint8_t)0xD5U, (uint8_t)0x9DU, (uint8_t)0x7CU, (uint8_t)0x25U, (uint8_t)0xE4U, (uint8_t)0x1DU, (uint8_t)0x2BU, (uint8_t)0x66U, (uint8_t)0xC6U, (uint8_t)0x2EU, (uint8_t)0x37U, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU }; static const uint8_t Hacl_Impl_FFDHE_Constants_ffdhe_p4096[512U] = { (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xADU, (uint8_t)0xF8U, (uint8_t)0x54U, (uint8_t)0x58U, (uint8_t)0xA2U, (uint8_t)0xBBU, (uint8_t)0x4AU, (uint8_t)0x9AU, (uint8_t)0xAFU, (uint8_t)0xDCU, (uint8_t)0x56U, (uint8_t)0x20U, (uint8_t)0x27U, (uint8_t)0x3DU, (uint8_t)0x3CU, (uint8_t)0xF1U, (uint8_t)0xD8U, (uint8_t)0xB9U, (uint8_t)0xC5U, (uint8_t)0x83U, (uint8_t)0xCEU, (uint8_t)0x2DU, (uint8_t)0x36U, (uint8_t)0x95U, (uint8_t)0xA9U, (uint8_t)0xE1U, (uint8_t)0x36U, (uint8_t)0x41U, (uint8_t)0x14U, (uint8_t)0x64U, (uint8_t)0x33U, (uint8_t)0xFBU, (uint8_t)0xCCU, (uint8_t)0x93U, (uint8_t)0x9DU, (uint8_t)0xCEU, (uint8_t)0x24U, (uint8_t)0x9BU, (uint8_t)0x3EU, (uint8_t)0xF9U, (uint8_t)0x7DU, (uint8_t)0x2FU, (uint8_t)0xE3U, (uint8_t)0x63U, (uint8_t)0x63U, (uint8_t)0x0CU, (uint8_t)0x75U, (uint8_t)0xD8U, (uint8_t)0xF6U, (uint8_t)0x81U, (uint8_t)0xB2U, (uint8_t)0x02U, (uint8_t)0xAEU, (uint8_t)0xC4U, (uint8_t)0x61U, (uint8_t)0x7AU, (uint8_t)0xD3U, (uint8_t)0xDFU, (uint8_t)0x1EU, (uint8_t)0xD5U, (uint8_t)0xD5U, (uint8_t)0xFDU, (uint8_t)0x65U, (uint8_t)0x61U, (uint8_t)0x24U, (uint8_t)0x33U, (uint8_t)0xF5U, (uint8_t)0x1FU, (uint8_t)0x5FU, (uint8_t)0x06U, (uint8_t)0x6EU, (uint8_t)0xD0U, (uint8_t)0x85U, (uint8_t)0x63U, (uint8_t)0x65U, (uint8_t)0x55U, (uint8_t)0x3DU, (uint8_t)0xEDU, (uint8_t)0x1AU, (uint8_t)0xF3U, (uint8_t)0xB5U, (uint8_t)0x57U, (uint8_t)0x13U, (uint8_t)0x5EU, (uint8_t)0x7FU, (uint8_t)0x57U, (uint8_t)0xC9U, (uint8_t)0x35U, (uint8_t)0x98U, (uint8_t)0x4FU, (uint8_t)0x0CU, (uint8_t)0x70U, (uint8_t)0xE0U, (uint8_t)0xE6U, (uint8_t)0x8BU, (uint8_t)0x77U, (uint8_t)0xE2U, (uint8_t)0xA6U, (uint8_t)0x89U, (uint8_t)0xDAU, (uint8_t)0xF3U, (uint8_t)0xEFU, (uint8_t)0xE8U, (uint8_t)0x72U, (uint8_t)0x1DU, (uint8_t)0xF1U, (uint8_t)0x58U, (uint8_t)0xA1U, (uint8_t)0x36U, (uint8_t)0xADU, (uint8_t)0xE7U, (uint8_t)0x35U, (uint8_t)0x30U, (uint8_t)0xACU, (uint8_t)0xCAU, (uint8_t)0x4FU, (uint8_t)0x48U, (uint8_t)0x3AU, (uint8_t)0x79U, (uint8_t)0x7AU, (uint8_t)0xBCU, (uint8_t)0x0AU, (uint8_t)0xB1U, (uint8_t)0x82U, (uint8_t)0xB3U, (uint8_t)0x24U, (uint8_t)0xFBU, (uint8_t)0x61U, (uint8_t)0xD1U, (uint8_t)0x08U, (uint8_t)0xA9U, (uint8_t)0x4BU, (uint8_t)0xB2U, (uint8_t)0xC8U, (uint8_t)0xE3U, (uint8_t)0xFBU, (uint8_t)0xB9U, (uint8_t)0x6AU, (uint8_t)0xDAU, (uint8_t)0xB7U, (uint8_t)0x60U, (uint8_t)0xD7U, (uint8_t)0xF4U, (uint8_t)0x68U, (uint8_t)0x1DU, (uint8_t)0x4FU, (uint8_t)0x42U, (uint8_t)0xA3U, (uint8_t)0xDEU, (uint8_t)0x39U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xAEU, (uint8_t)0x56U, (uint8_t)0xEDU, (uint8_t)0xE7U, (uint8_t)0x63U, (uint8_t)0x72U, (uint8_t)0xBBU, (uint8_t)0x19U, (uint8_t)0x0BU, (uint8_t)0x07U, (uint8_t)0xA7U, (uint8_t)0xC8U, (uint8_t)0xEEU, (uint8_t)0x0AU, (uint8_t)0x6DU, (uint8_t)0x70U, (uint8_t)0x9EU, (uint8_t)0x02U, (uint8_t)0xFCU, (uint8_t)0xE1U, (uint8_t)0xCDU, (uint8_t)0xF7U, (uint8_t)0xE2U, (uint8_t)0xECU, (uint8_t)0xC0U, (uint8_t)0x34U, (uint8_t)0x04U, (uint8_t)0xCDU, (uint8_t)0x28U, (uint8_t)0x34U, (uint8_t)0x2FU, (uint8_t)0x61U, (uint8_t)0x91U, (uint8_t)0x72U, (uint8_t)0xFEU, (uint8_t)0x9CU, (uint8_t)0xE9U, (uint8_t)0x85U, (uint8_t)0x83U, (uint8_t)0xFFU, (uint8_t)0x8EU, (uint8_t)0x4FU, (uint8_t)0x12U, (uint8_t)0x32U, (uint8_t)0xEEU, (uint8_t)0xF2U, (uint8_t)0x81U, (uint8_t)0x83U, (uint8_t)0xC3U, (uint8_t)0xFEU, (uint8_t)0x3BU, (uint8_t)0x1BU, (uint8_t)0x4CU, (uint8_t)0x6FU, (uint8_t)0xADU, (uint8_t)0x73U, (uint8_t)0x3BU, (uint8_t)0xB5U, (uint8_t)0xFCU, (uint8_t)0xBCU, (uint8_t)0x2EU, (uint8_t)0xC2U, (uint8_t)0x20U, (uint8_t)0x05U, (uint8_t)0xC5U, (uint8_t)0x8EU, (uint8_t)0xF1U, (uint8_t)0x83U, (uint8_t)0x7DU, (uint8_t)0x16U, (uint8_t)0x83U, (uint8_t)0xB2U, (uint8_t)0xC6U, (uint8_t)0xF3U, (uint8_t)0x4AU, (uint8_t)0x26U, (uint8_t)0xC1U, (uint8_t)0xB2U, (uint8_t)0xEFU, (uint8_t)0xFAU, (uint8_t)0x88U, (uint8_t)0x6BU, (uint8_t)0x42U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0x1FU, (uint8_t)0xCFU, (uint8_t)0xDCU, (uint8_t)0xDEU, (uint8_t)0x35U, (uint8_t)0x5BU, (uint8_t)0x3BU, (uint8_t)0x65U, (uint8_t)0x19U, (uint8_t)0x03U, (uint8_t)0x5BU, (uint8_t)0xBCU, (uint8_t)0x34U, (uint8_t)0xF4U, (uint8_t)0xDEU, (uint8_t)0xF9U, (uint8_t)0x9CU, (uint8_t)0x02U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0xB4U, (uint8_t)0x6FU, (uint8_t)0xC9U, (uint8_t)0xD6U, (uint8_t)0xE6U, (uint8_t)0xC9U, (uint8_t)0x07U, (uint8_t)0x7AU, (uint8_t)0xD9U, (uint8_t)0x1DU, (uint8_t)0x26U, (uint8_t)0x91U, (uint8_t)0xF7U, (uint8_t)0xF7U, (uint8_t)0xEEU, (uint8_t)0x59U, (uint8_t)0x8CU, (uint8_t)0xB0U, (uint8_t)0xFAU, (uint8_t)0xC1U, (uint8_t)0x86U, (uint8_t)0xD9U, (uint8_t)0x1CU, (uint8_t)0xAEU, (uint8_t)0xFEU, (uint8_t)0x13U, (uint8_t)0x09U, (uint8_t)0x85U, (uint8_t)0x13U, (uint8_t)0x92U, (uint8_t)0x70U, (uint8_t)0xB4U, (uint8_t)0x13U, (uint8_t)0x0CU, (uint8_t)0x93U, (uint8_t)0xBCU, (uint8_t)0x43U, (uint8_t)0x79U, (uint8_t)0x44U, (uint8_t)0xF4U, (uint8_t)0xFDU, (uint8_t)0x44U, (uint8_t)0x52U, (uint8_t)0xE2U, (uint8_t)0xD7U, (uint8_t)0x4DU, (uint8_t)0xD3U, (uint8_t)0x64U, (uint8_t)0xF2U, (uint8_t)0xE2U, (uint8_t)0x1EU, (uint8_t)0x71U, (uint8_t)0xF5U, (uint8_t)0x4BU, (uint8_t)0xFFU, (uint8_t)0x5CU, (uint8_t)0xAEU, (uint8_t)0x82U, (uint8_t)0xABU, (uint8_t)0x9CU, (uint8_t)0x9DU, (uint8_t)0xF6U, (uint8_t)0x9EU, (uint8_t)0xE8U, (uint8_t)0x6DU, (uint8_t)0x2BU, (uint8_t)0xC5U, (uint8_t)0x22U, (uint8_t)0x36U, (uint8_t)0x3AU, (uint8_t)0x0DU, (uint8_t)0xABU, (uint8_t)0xC5U, (uint8_t)0x21U, (uint8_t)0x97U, (uint8_t)0x9BU, (uint8_t)0x0DU, (uint8_t)0xEAU, (uint8_t)0xDAU, (uint8_t)0x1DU, (uint8_t)0xBFU, (uint8_t)0x9AU, (uint8_t)0x42U, (uint8_t)0xD5U, (uint8_t)0xC4U, (uint8_t)0x48U, (uint8_t)0x4EU, (uint8_t)0x0AU, (uint8_t)0xBCU, (uint8_t)0xD0U, (uint8_t)0x6BU, (uint8_t)0xFAU, (uint8_t)0x53U, (uint8_t)0xDDU, (uint8_t)0xEFU, (uint8_t)0x3CU, (uint8_t)0x1BU, (uint8_t)0x20U, (uint8_t)0xEEU, (uint8_t)0x3FU, (uint8_t)0xD5U, (uint8_t)0x9DU, (uint8_t)0x7CU, (uint8_t)0x25U, (uint8_t)0xE4U, (uint8_t)0x1DU, (uint8_t)0x2BU, (uint8_t)0x66U, (uint8_t)0x9EU, (uint8_t)0x1EU, (uint8_t)0xF1U, (uint8_t)0x6EU, (uint8_t)0x6FU, (uint8_t)0x52U, (uint8_t)0xC3U, (uint8_t)0x16U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xFBU, (uint8_t)0x79U, (uint8_t)0x30U, (uint8_t)0xE9U, (uint8_t)0xE4U, (uint8_t)0xE5U, (uint8_t)0x88U, (uint8_t)0x57U, (uint8_t)0xB6U, (uint8_t)0xACU, (uint8_t)0x7DU, (uint8_t)0x5FU, (uint8_t)0x42U, (uint8_t)0xD6U, (uint8_t)0x9FU, (uint8_t)0x6DU, (uint8_t)0x18U, (uint8_t)0x77U, (uint8_t)0x63U, (uint8_t)0xCFU, (uint8_t)0x1DU, (uint8_t)0x55U, (uint8_t)0x03U, (uint8_t)0x40U, (uint8_t)0x04U, (uint8_t)0x87U, (uint8_t)0xF5U, (uint8_t)0x5BU, (uint8_t)0xA5U, (uint8_t)0x7EU, (uint8_t)0x31U, (uint8_t)0xCCU, (uint8_t)0x7AU, (uint8_t)0x71U, (uint8_t)0x35U, (uint8_t)0xC8U, (uint8_t)0x86U, (uint8_t)0xEFU, (uint8_t)0xB4U, (uint8_t)0x31U, (uint8_t)0x8AU, (uint8_t)0xEDU, (uint8_t)0x6AU, (uint8_t)0x1EU, (uint8_t)0x01U, (uint8_t)0x2DU, (uint8_t)0x9EU, (uint8_t)0x68U, (uint8_t)0x32U, (uint8_t)0xA9U, (uint8_t)0x07U, (uint8_t)0x60U, (uint8_t)0x0AU, (uint8_t)0x91U, (uint8_t)0x81U, (uint8_t)0x30U, (uint8_t)0xC4U, (uint8_t)0x6DU, (uint8_t)0xC7U, (uint8_t)0x78U, (uint8_t)0xF9U, (uint8_t)0x71U, (uint8_t)0xADU, (uint8_t)0x00U, (uint8_t)0x38U, (uint8_t)0x09U, (uint8_t)0x29U, (uint8_t)0x99U, (uint8_t)0xA3U, (uint8_t)0x33U, (uint8_t)0xCBU, (uint8_t)0x8BU, (uint8_t)0x7AU, (uint8_t)0x1AU, (uint8_t)0x1DU, (uint8_t)0xB9U, (uint8_t)0x3DU, (uint8_t)0x71U, (uint8_t)0x40U, (uint8_t)0x00U, (uint8_t)0x3CU, (uint8_t)0x2AU, (uint8_t)0x4EU, (uint8_t)0xCEU, (uint8_t)0xA9U, (uint8_t)0xF9U, (uint8_t)0x8DU, (uint8_t)0x0AU, (uint8_t)0xCCU, (uint8_t)0x0AU, (uint8_t)0x82U, (uint8_t)0x91U, (uint8_t)0xCDU, (uint8_t)0xCEU, (uint8_t)0xC9U, (uint8_t)0x7DU, (uint8_t)0xCFU, (uint8_t)0x8EU, (uint8_t)0xC9U, (uint8_t)0xB5U, (uint8_t)0x5AU, (uint8_t)0x7FU, (uint8_t)0x88U, (uint8_t)0xA4U, (uint8_t)0x6BU, (uint8_t)0x4DU, (uint8_t)0xB5U, (uint8_t)0xA8U, (uint8_t)0x51U, (uint8_t)0xF4U, (uint8_t)0x41U, (uint8_t)0x82U, (uint8_t)0xE1U, (uint8_t)0xC6U, (uint8_t)0x8AU, (uint8_t)0x00U, (uint8_t)0x7EU, (uint8_t)0x5EU, (uint8_t)0x65U, (uint8_t)0x5FU, (uint8_t)0x6AU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU }; static const uint8_t Hacl_Impl_FFDHE_Constants_ffdhe_p6144[768U] = { (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xADU, (uint8_t)0xF8U, (uint8_t)0x54U, (uint8_t)0x58U, (uint8_t)0xA2U, (uint8_t)0xBBU, (uint8_t)0x4AU, (uint8_t)0x9AU, (uint8_t)0xAFU, (uint8_t)0xDCU, (uint8_t)0x56U, (uint8_t)0x20U, (uint8_t)0x27U, (uint8_t)0x3DU, (uint8_t)0x3CU, (uint8_t)0xF1U, (uint8_t)0xD8U, (uint8_t)0xB9U, (uint8_t)0xC5U, (uint8_t)0x83U, (uint8_t)0xCEU, (uint8_t)0x2DU, (uint8_t)0x36U, (uint8_t)0x95U, (uint8_t)0xA9U, (uint8_t)0xE1U, (uint8_t)0x36U, (uint8_t)0x41U, (uint8_t)0x14U, (uint8_t)0x64U, (uint8_t)0x33U, (uint8_t)0xFBU, (uint8_t)0xCCU, (uint8_t)0x93U, (uint8_t)0x9DU, (uint8_t)0xCEU, (uint8_t)0x24U, (uint8_t)0x9BU, (uint8_t)0x3EU, (uint8_t)0xF9U, (uint8_t)0x7DU, (uint8_t)0x2FU, (uint8_t)0xE3U, (uint8_t)0x63U, (uint8_t)0x63U, (uint8_t)0x0CU, (uint8_t)0x75U, (uint8_t)0xD8U, (uint8_t)0xF6U, (uint8_t)0x81U, (uint8_t)0xB2U, (uint8_t)0x02U, (uint8_t)0xAEU, (uint8_t)0xC4U, (uint8_t)0x61U, (uint8_t)0x7AU, (uint8_t)0xD3U, (uint8_t)0xDFU, (uint8_t)0x1EU, (uint8_t)0xD5U, (uint8_t)0xD5U, (uint8_t)0xFDU, (uint8_t)0x65U, (uint8_t)0x61U, (uint8_t)0x24U, (uint8_t)0x33U, (uint8_t)0xF5U, (uint8_t)0x1FU, (uint8_t)0x5FU, (uint8_t)0x06U, (uint8_t)0x6EU, (uint8_t)0xD0U, (uint8_t)0x85U, (uint8_t)0x63U, (uint8_t)0x65U, (uint8_t)0x55U, (uint8_t)0x3DU, (uint8_t)0xEDU, (uint8_t)0x1AU, (uint8_t)0xF3U, (uint8_t)0xB5U, (uint8_t)0x57U, (uint8_t)0x13U, (uint8_t)0x5EU, (uint8_t)0x7FU, (uint8_t)0x57U, (uint8_t)0xC9U, (uint8_t)0x35U, (uint8_t)0x98U, (uint8_t)0x4FU, (uint8_t)0x0CU, (uint8_t)0x70U, (uint8_t)0xE0U, (uint8_t)0xE6U, (uint8_t)0x8BU, (uint8_t)0x77U, (uint8_t)0xE2U, (uint8_t)0xA6U, (uint8_t)0x89U, (uint8_t)0xDAU, (uint8_t)0xF3U, (uint8_t)0xEFU, (uint8_t)0xE8U, (uint8_t)0x72U, (uint8_t)0x1DU, (uint8_t)0xF1U, (uint8_t)0x58U, (uint8_t)0xA1U, (uint8_t)0x36U, (uint8_t)0xADU, (uint8_t)0xE7U, (uint8_t)0x35U, (uint8_t)0x30U, (uint8_t)0xACU, (uint8_t)0xCAU, (uint8_t)0x4FU, (uint8_t)0x48U, (uint8_t)0x3AU, (uint8_t)0x79U, (uint8_t)0x7AU, (uint8_t)0xBCU, (uint8_t)0x0AU, (uint8_t)0xB1U, (uint8_t)0x82U, (uint8_t)0xB3U, (uint8_t)0x24U, (uint8_t)0xFBU, (uint8_t)0x61U, (uint8_t)0xD1U, (uint8_t)0x08U, (uint8_t)0xA9U, (uint8_t)0x4BU, (uint8_t)0xB2U, (uint8_t)0xC8U, (uint8_t)0xE3U, (uint8_t)0xFBU, (uint8_t)0xB9U, (uint8_t)0x6AU, (uint8_t)0xDAU, (uint8_t)0xB7U, (uint8_t)0x60U, (uint8_t)0xD7U, (uint8_t)0xF4U, (uint8_t)0x68U, (uint8_t)0x1DU, (uint8_t)0x4FU, (uint8_t)0x42U, (uint8_t)0xA3U, (uint8_t)0xDEU, (uint8_t)0x39U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xAEU, (uint8_t)0x56U, (uint8_t)0xEDU, (uint8_t)0xE7U, (uint8_t)0x63U, (uint8_t)0x72U, (uint8_t)0xBBU, (uint8_t)0x19U, (uint8_t)0x0BU, (uint8_t)0x07U, (uint8_t)0xA7U, (uint8_t)0xC8U, (uint8_t)0xEEU, (uint8_t)0x0AU, (uint8_t)0x6DU, (uint8_t)0x70U, (uint8_t)0x9EU, (uint8_t)0x02U, (uint8_t)0xFCU, (uint8_t)0xE1U, (uint8_t)0xCDU, (uint8_t)0xF7U, (uint8_t)0xE2U, (uint8_t)0xECU, (uint8_t)0xC0U, (uint8_t)0x34U, (uint8_t)0x04U, (uint8_t)0xCDU, (uint8_t)0x28U, (uint8_t)0x34U, (uint8_t)0x2FU, (uint8_t)0x61U, (uint8_t)0x91U, (uint8_t)0x72U, (uint8_t)0xFEU, (uint8_t)0x9CU, (uint8_t)0xE9U, (uint8_t)0x85U, (uint8_t)0x83U, (uint8_t)0xFFU, (uint8_t)0x8EU, (uint8_t)0x4FU, (uint8_t)0x12U, (uint8_t)0x32U, (uint8_t)0xEEU, (uint8_t)0xF2U, (uint8_t)0x81U, (uint8_t)0x83U, (uint8_t)0xC3U, (uint8_t)0xFEU, (uint8_t)0x3BU, (uint8_t)0x1BU, (uint8_t)0x4CU, (uint8_t)0x6FU, (uint8_t)0xADU, (uint8_t)0x73U, (uint8_t)0x3BU, (uint8_t)0xB5U, (uint8_t)0xFCU, (uint8_t)0xBCU, (uint8_t)0x2EU, (uint8_t)0xC2U, (uint8_t)0x20U, (uint8_t)0x05U, (uint8_t)0xC5U, (uint8_t)0x8EU, (uint8_t)0xF1U, (uint8_t)0x83U, (uint8_t)0x7DU, (uint8_t)0x16U, (uint8_t)0x83U, (uint8_t)0xB2U, (uint8_t)0xC6U, (uint8_t)0xF3U, (uint8_t)0x4AU, (uint8_t)0x26U, (uint8_t)0xC1U, (uint8_t)0xB2U, (uint8_t)0xEFU, (uint8_t)0xFAU, (uint8_t)0x88U, (uint8_t)0x6BU, (uint8_t)0x42U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0x1FU, (uint8_t)0xCFU, (uint8_t)0xDCU, (uint8_t)0xDEU, (uint8_t)0x35U, (uint8_t)0x5BU, (uint8_t)0x3BU, (uint8_t)0x65U, (uint8_t)0x19U, (uint8_t)0x03U, (uint8_t)0x5BU, (uint8_t)0xBCU, (uint8_t)0x34U, (uint8_t)0xF4U, (uint8_t)0xDEU, (uint8_t)0xF9U, (uint8_t)0x9CU, (uint8_t)0x02U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0xB4U, (uint8_t)0x6FU, (uint8_t)0xC9U, (uint8_t)0xD6U, (uint8_t)0xE6U, (uint8_t)0xC9U, (uint8_t)0x07U, (uint8_t)0x7AU, (uint8_t)0xD9U, (uint8_t)0x1DU, (uint8_t)0x26U, (uint8_t)0x91U, (uint8_t)0xF7U, (uint8_t)0xF7U, (uint8_t)0xEEU, (uint8_t)0x59U, (uint8_t)0x8CU, (uint8_t)0xB0U, (uint8_t)0xFAU, (uint8_t)0xC1U, (uint8_t)0x86U, (uint8_t)0xD9U, (uint8_t)0x1CU, (uint8_t)0xAEU, (uint8_t)0xFEU, (uint8_t)0x13U, (uint8_t)0x09U, (uint8_t)0x85U, (uint8_t)0x13U, (uint8_t)0x92U, (uint8_t)0x70U, (uint8_t)0xB4U, (uint8_t)0x13U, (uint8_t)0x0CU, (uint8_t)0x93U, (uint8_t)0xBCU, (uint8_t)0x43U, (uint8_t)0x79U, (uint8_t)0x44U, (uint8_t)0xF4U, (uint8_t)0xFDU, (uint8_t)0x44U, (uint8_t)0x52U, (uint8_t)0xE2U, (uint8_t)0xD7U, (uint8_t)0x4DU, (uint8_t)0xD3U, (uint8_t)0x64U, (uint8_t)0xF2U, (uint8_t)0xE2U, (uint8_t)0x1EU, (uint8_t)0x71U, (uint8_t)0xF5U, (uint8_t)0x4BU, (uint8_t)0xFFU, (uint8_t)0x5CU, (uint8_t)0xAEU, (uint8_t)0x82U, (uint8_t)0xABU, (uint8_t)0x9CU, (uint8_t)0x9DU, (uint8_t)0xF6U, (uint8_t)0x9EU, (uint8_t)0xE8U, (uint8_t)0x6DU, (uint8_t)0x2BU, (uint8_t)0xC5U, (uint8_t)0x22U, (uint8_t)0x36U, (uint8_t)0x3AU, (uint8_t)0x0DU, (uint8_t)0xABU, (uint8_t)0xC5U, (uint8_t)0x21U, (uint8_t)0x97U, (uint8_t)0x9BU, (uint8_t)0x0DU, (uint8_t)0xEAU, (uint8_t)0xDAU, (uint8_t)0x1DU, (uint8_t)0xBFU, (uint8_t)0x9AU, (uint8_t)0x42U, (uint8_t)0xD5U, (uint8_t)0xC4U, (uint8_t)0x48U, (uint8_t)0x4EU, (uint8_t)0x0AU, (uint8_t)0xBCU, (uint8_t)0xD0U, (uint8_t)0x6BU, (uint8_t)0xFAU, (uint8_t)0x53U, (uint8_t)0xDDU, (uint8_t)0xEFU, (uint8_t)0x3CU, (uint8_t)0x1BU, (uint8_t)0x20U, (uint8_t)0xEEU, (uint8_t)0x3FU, (uint8_t)0xD5U, (uint8_t)0x9DU, (uint8_t)0x7CU, (uint8_t)0x25U, (uint8_t)0xE4U, (uint8_t)0x1DU, (uint8_t)0x2BU, (uint8_t)0x66U, (uint8_t)0x9EU, (uint8_t)0x1EU, (uint8_t)0xF1U, (uint8_t)0x6EU, (uint8_t)0x6FU, (uint8_t)0x52U, (uint8_t)0xC3U, (uint8_t)0x16U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xFBU, (uint8_t)0x79U, (uint8_t)0x30U, (uint8_t)0xE9U, (uint8_t)0xE4U, (uint8_t)0xE5U, (uint8_t)0x88U, (uint8_t)0x57U, (uint8_t)0xB6U, (uint8_t)0xACU, (uint8_t)0x7DU, (uint8_t)0x5FU, (uint8_t)0x42U, (uint8_t)0xD6U, (uint8_t)0x9FU, (uint8_t)0x6DU, (uint8_t)0x18U, (uint8_t)0x77U, (uint8_t)0x63U, (uint8_t)0xCFU, (uint8_t)0x1DU, (uint8_t)0x55U, (uint8_t)0x03U, (uint8_t)0x40U, (uint8_t)0x04U, (uint8_t)0x87U, (uint8_t)0xF5U, (uint8_t)0x5BU, (uint8_t)0xA5U, (uint8_t)0x7EU, (uint8_t)0x31U, (uint8_t)0xCCU, (uint8_t)0x7AU, (uint8_t)0x71U, (uint8_t)0x35U, (uint8_t)0xC8U, (uint8_t)0x86U, (uint8_t)0xEFU, (uint8_t)0xB4U, (uint8_t)0x31U, (uint8_t)0x8AU, (uint8_t)0xEDU, (uint8_t)0x6AU, (uint8_t)0x1EU, (uint8_t)0x01U, (uint8_t)0x2DU, (uint8_t)0x9EU, (uint8_t)0x68U, (uint8_t)0x32U, (uint8_t)0xA9U, (uint8_t)0x07U, (uint8_t)0x60U, (uint8_t)0x0AU, (uint8_t)0x91U, (uint8_t)0x81U, (uint8_t)0x30U, (uint8_t)0xC4U, (uint8_t)0x6DU, (uint8_t)0xC7U, (uint8_t)0x78U, (uint8_t)0xF9U, (uint8_t)0x71U, (uint8_t)0xADU, (uint8_t)0x00U, (uint8_t)0x38U, (uint8_t)0x09U, (uint8_t)0x29U, (uint8_t)0x99U, (uint8_t)0xA3U, (uint8_t)0x33U, (uint8_t)0xCBU, (uint8_t)0x8BU, (uint8_t)0x7AU, (uint8_t)0x1AU, (uint8_t)0x1DU, (uint8_t)0xB9U, (uint8_t)0x3DU, (uint8_t)0x71U, (uint8_t)0x40U, (uint8_t)0x00U, (uint8_t)0x3CU, (uint8_t)0x2AU, (uint8_t)0x4EU, (uint8_t)0xCEU, (uint8_t)0xA9U, (uint8_t)0xF9U, (uint8_t)0x8DU, (uint8_t)0x0AU, (uint8_t)0xCCU, (uint8_t)0x0AU, (uint8_t)0x82U, (uint8_t)0x91U, (uint8_t)0xCDU, (uint8_t)0xCEU, (uint8_t)0xC9U, (uint8_t)0x7DU, (uint8_t)0xCFU, (uint8_t)0x8EU, (uint8_t)0xC9U, (uint8_t)0xB5U, (uint8_t)0x5AU, (uint8_t)0x7FU, (uint8_t)0x88U, (uint8_t)0xA4U, (uint8_t)0x6BU, (uint8_t)0x4DU, (uint8_t)0xB5U, (uint8_t)0xA8U, (uint8_t)0x51U, (uint8_t)0xF4U, (uint8_t)0x41U, (uint8_t)0x82U, (uint8_t)0xE1U, (uint8_t)0xC6U, (uint8_t)0x8AU, (uint8_t)0x00U, (uint8_t)0x7EU, (uint8_t)0x5EU, (uint8_t)0x0DU, (uint8_t)0xD9U, (uint8_t)0x02U, (uint8_t)0x0BU, (uint8_t)0xFDU, (uint8_t)0x64U, (uint8_t)0xB6U, (uint8_t)0x45U, (uint8_t)0x03U, (uint8_t)0x6CU, (uint8_t)0x7AU, (uint8_t)0x4EU, (uint8_t)0x67U, (uint8_t)0x7DU, (uint8_t)0x2CU, (uint8_t)0x38U, (uint8_t)0x53U, (uint8_t)0x2AU, (uint8_t)0x3AU, (uint8_t)0x23U, (uint8_t)0xBAU, (uint8_t)0x44U, (uint8_t)0x42U, (uint8_t)0xCAU, (uint8_t)0xF5U, (uint8_t)0x3EU, (uint8_t)0xA6U, (uint8_t)0x3BU, (uint8_t)0xB4U, (uint8_t)0x54U, (uint8_t)0x32U, (uint8_t)0x9BU, (uint8_t)0x76U, (uint8_t)0x24U, (uint8_t)0xC8U, (uint8_t)0x91U, (uint8_t)0x7BU, (uint8_t)0xDDU, (uint8_t)0x64U, (uint8_t)0xB1U, (uint8_t)0xC0U, (uint8_t)0xFDU, (uint8_t)0x4CU, (uint8_t)0xB3U, (uint8_t)0x8EU, (uint8_t)0x8CU, (uint8_t)0x33U, (uint8_t)0x4CU, (uint8_t)0x70U, (uint8_t)0x1CU, (uint8_t)0x3AU, (uint8_t)0xCDU, (uint8_t)0xADU, (uint8_t)0x06U, (uint8_t)0x57U, (uint8_t)0xFCU, (uint8_t)0xCFU, (uint8_t)0xECU, (uint8_t)0x71U, (uint8_t)0x9BU, (uint8_t)0x1FU, (uint8_t)0x5CU, (uint8_t)0x3EU, (uint8_t)0x4EU, (uint8_t)0x46U, (uint8_t)0x04U, (uint8_t)0x1FU, (uint8_t)0x38U, (uint8_t)0x81U, (uint8_t)0x47U, (uint8_t)0xFBU, (uint8_t)0x4CU, (uint8_t)0xFDU, (uint8_t)0xB4U, (uint8_t)0x77U, (uint8_t)0xA5U, (uint8_t)0x24U, (uint8_t)0x71U, (uint8_t)0xF7U, (uint8_t)0xA9U, (uint8_t)0xA9U, (uint8_t)0x69U, (uint8_t)0x10U, (uint8_t)0xB8U, (uint8_t)0x55U, (uint8_t)0x32U, (uint8_t)0x2EU, (uint8_t)0xDBU, (uint8_t)0x63U, (uint8_t)0x40U, (uint8_t)0xD8U, (uint8_t)0xA0U, (uint8_t)0x0EU, (uint8_t)0xF0U, (uint8_t)0x92U, (uint8_t)0x35U, (uint8_t)0x05U, (uint8_t)0x11U, (uint8_t)0xE3U, (uint8_t)0x0AU, (uint8_t)0xBEU, (uint8_t)0xC1U, (uint8_t)0xFFU, (uint8_t)0xF9U, (uint8_t)0xE3U, (uint8_t)0xA2U, (uint8_t)0x6EU, (uint8_t)0x7FU, (uint8_t)0xB2U, (uint8_t)0x9FU, (uint8_t)0x8CU, (uint8_t)0x18U, (uint8_t)0x30U, (uint8_t)0x23U, (uint8_t)0xC3U, (uint8_t)0x58U, (uint8_t)0x7EU, (uint8_t)0x38U, (uint8_t)0xDAU, (uint8_t)0x00U, (uint8_t)0x77U, (uint8_t)0xD9U, (uint8_t)0xB4U, (uint8_t)0x76U, (uint8_t)0x3EU, (uint8_t)0x4EU, (uint8_t)0x4BU, (uint8_t)0x94U, (uint8_t)0xB2U, (uint8_t)0xBBU, (uint8_t)0xC1U, (uint8_t)0x94U, (uint8_t)0xC6U, (uint8_t)0x65U, (uint8_t)0x1EU, (uint8_t)0x77U, (uint8_t)0xCAU, (uint8_t)0xF9U, (uint8_t)0x92U, (uint8_t)0xEEU, (uint8_t)0xAAU, (uint8_t)0xC0U, (uint8_t)0x23U, (uint8_t)0x2AU, (uint8_t)0x28U, (uint8_t)0x1BU, (uint8_t)0xF6U, (uint8_t)0xB3U, (uint8_t)0xA7U, (uint8_t)0x39U, (uint8_t)0xC1U, (uint8_t)0x22U, (uint8_t)0x61U, (uint8_t)0x16U, (uint8_t)0x82U, (uint8_t)0x0AU, (uint8_t)0xE8U, (uint8_t)0xDBU, (uint8_t)0x58U, (uint8_t)0x47U, (uint8_t)0xA6U, (uint8_t)0x7CU, (uint8_t)0xBEU, (uint8_t)0xF9U, (uint8_t)0xC9U, (uint8_t)0x09U, (uint8_t)0x1BU, (uint8_t)0x46U, (uint8_t)0x2DU, (uint8_t)0x53U, (uint8_t)0x8CU, (uint8_t)0xD7U, (uint8_t)0x2BU, (uint8_t)0x03U, (uint8_t)0x74U, (uint8_t)0x6AU, (uint8_t)0xE7U, (uint8_t)0x7FU, (uint8_t)0x5EU, (uint8_t)0x62U, (uint8_t)0x29U, (uint8_t)0x2CU, (uint8_t)0x31U, (uint8_t)0x15U, (uint8_t)0x62U, (uint8_t)0xA8U, (uint8_t)0x46U, (uint8_t)0x50U, (uint8_t)0x5DU, (uint8_t)0xC8U, (uint8_t)0x2DU, (uint8_t)0xB8U, (uint8_t)0x54U, (uint8_t)0x33U, (uint8_t)0x8AU, (uint8_t)0xE4U, (uint8_t)0x9FU, (uint8_t)0x52U, (uint8_t)0x35U, (uint8_t)0xC9U, (uint8_t)0x5BU, (uint8_t)0x91U, (uint8_t)0x17U, (uint8_t)0x8CU, (uint8_t)0xCFU, (uint8_t)0x2DU, (uint8_t)0xD5U, (uint8_t)0xCAU, (uint8_t)0xCEU, (uint8_t)0xF4U, (uint8_t)0x03U, (uint8_t)0xECU, (uint8_t)0x9DU, (uint8_t)0x18U, (uint8_t)0x10U, (uint8_t)0xC6U, (uint8_t)0x27U, (uint8_t)0x2BU, (uint8_t)0x04U, (uint8_t)0x5BU, (uint8_t)0x3BU, (uint8_t)0x71U, (uint8_t)0xF9U, (uint8_t)0xDCU, (uint8_t)0x6BU, (uint8_t)0x80U, (uint8_t)0xD6U, (uint8_t)0x3FU, (uint8_t)0xDDU, (uint8_t)0x4AU, (uint8_t)0x8EU, (uint8_t)0x9AU, (uint8_t)0xDBU, (uint8_t)0x1EU, (uint8_t)0x69U, (uint8_t)0x62U, (uint8_t)0xA6U, (uint8_t)0x95U, (uint8_t)0x26U, (uint8_t)0xD4U, (uint8_t)0x31U, (uint8_t)0x61U, (uint8_t)0xC1U, (uint8_t)0xA4U, (uint8_t)0x1DU, (uint8_t)0x57U, (uint8_t)0x0DU, (uint8_t)0x79U, (uint8_t)0x38U, (uint8_t)0xDAU, (uint8_t)0xD4U, (uint8_t)0xA4U, (uint8_t)0x0EU, (uint8_t)0x32U, (uint8_t)0x9CU, (uint8_t)0xD0U, (uint8_t)0xE4U, (uint8_t)0x0EU, (uint8_t)0x65U, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU }; static const uint8_t Hacl_Impl_FFDHE_Constants_ffdhe_p8192[1024U] = { (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xADU, (uint8_t)0xF8U, (uint8_t)0x54U, (uint8_t)0x58U, (uint8_t)0xA2U, (uint8_t)0xBBU, (uint8_t)0x4AU, (uint8_t)0x9AU, (uint8_t)0xAFU, (uint8_t)0xDCU, (uint8_t)0x56U, (uint8_t)0x20U, (uint8_t)0x27U, (uint8_t)0x3DU, (uint8_t)0x3CU, (uint8_t)0xF1U, (uint8_t)0xD8U, (uint8_t)0xB9U, (uint8_t)0xC5U, (uint8_t)0x83U, (uint8_t)0xCEU, (uint8_t)0x2DU, (uint8_t)0x36U, (uint8_t)0x95U, (uint8_t)0xA9U, (uint8_t)0xE1U, (uint8_t)0x36U, (uint8_t)0x41U, (uint8_t)0x14U, (uint8_t)0x64U, (uint8_t)0x33U, (uint8_t)0xFBU, (uint8_t)0xCCU, (uint8_t)0x93U, (uint8_t)0x9DU, (uint8_t)0xCEU, (uint8_t)0x24U, (uint8_t)0x9BU, (uint8_t)0x3EU, (uint8_t)0xF9U, (uint8_t)0x7DU, (uint8_t)0x2FU, (uint8_t)0xE3U, (uint8_t)0x63U, (uint8_t)0x63U, (uint8_t)0x0CU, (uint8_t)0x75U, (uint8_t)0xD8U, (uint8_t)0xF6U, (uint8_t)0x81U, (uint8_t)0xB2U, (uint8_t)0x02U, (uint8_t)0xAEU, (uint8_t)0xC4U, (uint8_t)0x61U, (uint8_t)0x7AU, (uint8_t)0xD3U, (uint8_t)0xDFU, (uint8_t)0x1EU, (uint8_t)0xD5U, (uint8_t)0xD5U, (uint8_t)0xFDU, (uint8_t)0x65U, (uint8_t)0x61U, (uint8_t)0x24U, (uint8_t)0x33U, (uint8_t)0xF5U, (uint8_t)0x1FU, (uint8_t)0x5FU, (uint8_t)0x06U, (uint8_t)0x6EU, (uint8_t)0xD0U, (uint8_t)0x85U, (uint8_t)0x63U, (uint8_t)0x65U, (uint8_t)0x55U, (uint8_t)0x3DU, (uint8_t)0xEDU, (uint8_t)0x1AU, (uint8_t)0xF3U, (uint8_t)0xB5U, (uint8_t)0x57U, (uint8_t)0x13U, (uint8_t)0x5EU, (uint8_t)0x7FU, (uint8_t)0x57U, (uint8_t)0xC9U, (uint8_t)0x35U, (uint8_t)0x98U, (uint8_t)0x4FU, (uint8_t)0x0CU, (uint8_t)0x70U, (uint8_t)0xE0U, (uint8_t)0xE6U, (uint8_t)0x8BU, (uint8_t)0x77U, (uint8_t)0xE2U, (uint8_t)0xA6U, (uint8_t)0x89U, (uint8_t)0xDAU, (uint8_t)0xF3U, (uint8_t)0xEFU, (uint8_t)0xE8U, (uint8_t)0x72U, (uint8_t)0x1DU, (uint8_t)0xF1U, (uint8_t)0x58U, (uint8_t)0xA1U, (uint8_t)0x36U, (uint8_t)0xADU, (uint8_t)0xE7U, (uint8_t)0x35U, (uint8_t)0x30U, (uint8_t)0xACU, (uint8_t)0xCAU, (uint8_t)0x4FU, (uint8_t)0x48U, (uint8_t)0x3AU, (uint8_t)0x79U, (uint8_t)0x7AU, (uint8_t)0xBCU, (uint8_t)0x0AU, (uint8_t)0xB1U, (uint8_t)0x82U, (uint8_t)0xB3U, (uint8_t)0x24U, (uint8_t)0xFBU, (uint8_t)0x61U, (uint8_t)0xD1U, (uint8_t)0x08U, (uint8_t)0xA9U, (uint8_t)0x4BU, (uint8_t)0xB2U, (uint8_t)0xC8U, (uint8_t)0xE3U, (uint8_t)0xFBU, (uint8_t)0xB9U, (uint8_t)0x6AU, (uint8_t)0xDAU, (uint8_t)0xB7U, (uint8_t)0x60U, (uint8_t)0xD7U, (uint8_t)0xF4U, (uint8_t)0x68U, (uint8_t)0x1DU, (uint8_t)0x4FU, (uint8_t)0x42U, (uint8_t)0xA3U, (uint8_t)0xDEU, (uint8_t)0x39U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xAEU, (uint8_t)0x56U, (uint8_t)0xEDU, (uint8_t)0xE7U, (uint8_t)0x63U, (uint8_t)0x72U, (uint8_t)0xBBU, (uint8_t)0x19U, (uint8_t)0x0BU, (uint8_t)0x07U, (uint8_t)0xA7U, (uint8_t)0xC8U, (uint8_t)0xEEU, (uint8_t)0x0AU, (uint8_t)0x6DU, (uint8_t)0x70U, (uint8_t)0x9EU, (uint8_t)0x02U, (uint8_t)0xFCU, (uint8_t)0xE1U, (uint8_t)0xCDU, (uint8_t)0xF7U, (uint8_t)0xE2U, (uint8_t)0xECU, (uint8_t)0xC0U, (uint8_t)0x34U, (uint8_t)0x04U, (uint8_t)0xCDU, (uint8_t)0x28U, (uint8_t)0x34U, (uint8_t)0x2FU, (uint8_t)0x61U, (uint8_t)0x91U, (uint8_t)0x72U, (uint8_t)0xFEU, (uint8_t)0x9CU, (uint8_t)0xE9U, (uint8_t)0x85U, (uint8_t)0x83U, (uint8_t)0xFFU, (uint8_t)0x8EU, (uint8_t)0x4FU, (uint8_t)0x12U, (uint8_t)0x32U, (uint8_t)0xEEU, (uint8_t)0xF2U, (uint8_t)0x81U, (uint8_t)0x83U, (uint8_t)0xC3U, (uint8_t)0xFEU, (uint8_t)0x3BU, (uint8_t)0x1BU, (uint8_t)0x4CU, (uint8_t)0x6FU, (uint8_t)0xADU, (uint8_t)0x73U, (uint8_t)0x3BU, (uint8_t)0xB5U, (uint8_t)0xFCU, (uint8_t)0xBCU, (uint8_t)0x2EU, (uint8_t)0xC2U, (uint8_t)0x20U, (uint8_t)0x05U, (uint8_t)0xC5U, (uint8_t)0x8EU, (uint8_t)0xF1U, (uint8_t)0x83U, (uint8_t)0x7DU, (uint8_t)0x16U, (uint8_t)0x83U, (uint8_t)0xB2U, (uint8_t)0xC6U, (uint8_t)0xF3U, (uint8_t)0x4AU, (uint8_t)0x26U, (uint8_t)0xC1U, (uint8_t)0xB2U, (uint8_t)0xEFU, (uint8_t)0xFAU, (uint8_t)0x88U, (uint8_t)0x6BU, (uint8_t)0x42U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0x1FU, (uint8_t)0xCFU, (uint8_t)0xDCU, (uint8_t)0xDEU, (uint8_t)0x35U, (uint8_t)0x5BU, (uint8_t)0x3BU, (uint8_t)0x65U, (uint8_t)0x19U, (uint8_t)0x03U, (uint8_t)0x5BU, (uint8_t)0xBCU, (uint8_t)0x34U, (uint8_t)0xF4U, (uint8_t)0xDEU, (uint8_t)0xF9U, (uint8_t)0x9CU, (uint8_t)0x02U, (uint8_t)0x38U, (uint8_t)0x61U, (uint8_t)0xB4U, (uint8_t)0x6FU, (uint8_t)0xC9U, (uint8_t)0xD6U, (uint8_t)0xE6U, (uint8_t)0xC9U, (uint8_t)0x07U, (uint8_t)0x7AU, (uint8_t)0xD9U, (uint8_t)0x1DU, (uint8_t)0x26U, (uint8_t)0x91U, (uint8_t)0xF7U, (uint8_t)0xF7U, (uint8_t)0xEEU, (uint8_t)0x59U, (uint8_t)0x8CU, (uint8_t)0xB0U, (uint8_t)0xFAU, (uint8_t)0xC1U, (uint8_t)0x86U, (uint8_t)0xD9U, (uint8_t)0x1CU, (uint8_t)0xAEU, (uint8_t)0xFEU, (uint8_t)0x13U, (uint8_t)0x09U, (uint8_t)0x85U, (uint8_t)0x13U, (uint8_t)0x92U, (uint8_t)0x70U, (uint8_t)0xB4U, (uint8_t)0x13U, (uint8_t)0x0CU, (uint8_t)0x93U, (uint8_t)0xBCU, (uint8_t)0x43U, (uint8_t)0x79U, (uint8_t)0x44U, (uint8_t)0xF4U, (uint8_t)0xFDU, (uint8_t)0x44U, (uint8_t)0x52U, (uint8_t)0xE2U, (uint8_t)0xD7U, (uint8_t)0x4DU, (uint8_t)0xD3U, (uint8_t)0x64U, (uint8_t)0xF2U, (uint8_t)0xE2U, (uint8_t)0x1EU, (uint8_t)0x71U, (uint8_t)0xF5U, (uint8_t)0x4BU, (uint8_t)0xFFU, (uint8_t)0x5CU, (uint8_t)0xAEU, (uint8_t)0x82U, (uint8_t)0xABU, (uint8_t)0x9CU, (uint8_t)0x9DU, (uint8_t)0xF6U, (uint8_t)0x9EU, (uint8_t)0xE8U, (uint8_t)0x6DU, (uint8_t)0x2BU, (uint8_t)0xC5U, (uint8_t)0x22U, (uint8_t)0x36U, (uint8_t)0x3AU, (uint8_t)0x0DU, (uint8_t)0xABU, (uint8_t)0xC5U, (uint8_t)0x21U, (uint8_t)0x97U, (uint8_t)0x9BU, (uint8_t)0x0DU, (uint8_t)0xEAU, (uint8_t)0xDAU, (uint8_t)0x1DU, (uint8_t)0xBFU, (uint8_t)0x9AU, (uint8_t)0x42U, (uint8_t)0xD5U, (uint8_t)0xC4U, (uint8_t)0x48U, (uint8_t)0x4EU, (uint8_t)0x0AU, (uint8_t)0xBCU, (uint8_t)0xD0U, (uint8_t)0x6BU, (uint8_t)0xFAU, (uint8_t)0x53U, (uint8_t)0xDDU, (uint8_t)0xEFU, (uint8_t)0x3CU, (uint8_t)0x1BU, (uint8_t)0x20U, (uint8_t)0xEEU, (uint8_t)0x3FU, (uint8_t)0xD5U, (uint8_t)0x9DU, (uint8_t)0x7CU, (uint8_t)0x25U, (uint8_t)0xE4U, (uint8_t)0x1DU, (uint8_t)0x2BU, (uint8_t)0x66U, (uint8_t)0x9EU, (uint8_t)0x1EU, (uint8_t)0xF1U, (uint8_t)0x6EU, (uint8_t)0x6FU, (uint8_t)0x52U, (uint8_t)0xC3U, (uint8_t)0x16U, (uint8_t)0x4DU, (uint8_t)0xF4U, (uint8_t)0xFBU, (uint8_t)0x79U, (uint8_t)0x30U, (uint8_t)0xE9U, (uint8_t)0xE4U, (uint8_t)0xE5U, (uint8_t)0x88U, (uint8_t)0x57U, (uint8_t)0xB6U, (uint8_t)0xACU, (uint8_t)0x7DU, (uint8_t)0x5FU, (uint8_t)0x42U, (uint8_t)0xD6U, (uint8_t)0x9FU, (uint8_t)0x6DU, (uint8_t)0x18U, (uint8_t)0x77U, (uint8_t)0x63U, (uint8_t)0xCFU, (uint8_t)0x1DU, (uint8_t)0x55U, (uint8_t)0x03U, (uint8_t)0x40U, (uint8_t)0x04U, (uint8_t)0x87U, (uint8_t)0xF5U, (uint8_t)0x5BU, (uint8_t)0xA5U, (uint8_t)0x7EU, (uint8_t)0x31U, (uint8_t)0xCCU, (uint8_t)0x7AU, (uint8_t)0x71U, (uint8_t)0x35U, (uint8_t)0xC8U, (uint8_t)0x86U, (uint8_t)0xEFU, (uint8_t)0xB4U, (uint8_t)0x31U, (uint8_t)0x8AU, (uint8_t)0xEDU, (uint8_t)0x6AU, (uint8_t)0x1EU, (uint8_t)0x01U, (uint8_t)0x2DU, (uint8_t)0x9EU, (uint8_t)0x68U, (uint8_t)0x32U, (uint8_t)0xA9U, (uint8_t)0x07U, (uint8_t)0x60U, (uint8_t)0x0AU, (uint8_t)0x91U, (uint8_t)0x81U, (uint8_t)0x30U, (uint8_t)0xC4U, (uint8_t)0x6DU, (uint8_t)0xC7U, (uint8_t)0x78U, (uint8_t)0xF9U, (uint8_t)0x71U, (uint8_t)0xADU, (uint8_t)0x00U, (uint8_t)0x38U, (uint8_t)0x09U, (uint8_t)0x29U, (uint8_t)0x99U, (uint8_t)0xA3U, (uint8_t)0x33U, (uint8_t)0xCBU, (uint8_t)0x8BU, (uint8_t)0x7AU, (uint8_t)0x1AU, (uint8_t)0x1DU, (uint8_t)0xB9U, (uint8_t)0x3DU, (uint8_t)0x71U, (uint8_t)0x40U, (uint8_t)0x00U, (uint8_t)0x3CU, (uint8_t)0x2AU, (uint8_t)0x4EU, (uint8_t)0xCEU, (uint8_t)0xA9U, (uint8_t)0xF9U, (uint8_t)0x8DU, (uint8_t)0x0AU, (uint8_t)0xCCU, (uint8_t)0x0AU, (uint8_t)0x82U, (uint8_t)0x91U, (uint8_t)0xCDU, (uint8_t)0xCEU, (uint8_t)0xC9U, (uint8_t)0x7DU, (uint8_t)0xCFU, (uint8_t)0x8EU, (uint8_t)0xC9U, (uint8_t)0xB5U, (uint8_t)0x5AU, (uint8_t)0x7FU, (uint8_t)0x88U, (uint8_t)0xA4U, (uint8_t)0x6BU, (uint8_t)0x4DU, (uint8_t)0xB5U, (uint8_t)0xA8U, (uint8_t)0x51U, (uint8_t)0xF4U, (uint8_t)0x41U, (uint8_t)0x82U, (uint8_t)0xE1U, (uint8_t)0xC6U, (uint8_t)0x8AU, (uint8_t)0x00U, (uint8_t)0x7EU, (uint8_t)0x5EU, (uint8_t)0x0DU, (uint8_t)0xD9U, (uint8_t)0x02U, (uint8_t)0x0BU, (uint8_t)0xFDU, (uint8_t)0x64U, (uint8_t)0xB6U, (uint8_t)0x45U, (uint8_t)0x03U, (uint8_t)0x6CU, (uint8_t)0x7AU, (uint8_t)0x4EU, (uint8_t)0x67U, (uint8_t)0x7DU, (uint8_t)0x2CU, (uint8_t)0x38U, (uint8_t)0x53U, (uint8_t)0x2AU, (uint8_t)0x3AU, (uint8_t)0x23U, (uint8_t)0xBAU, (uint8_t)0x44U, (uint8_t)0x42U, (uint8_t)0xCAU, (uint8_t)0xF5U, (uint8_t)0x3EU, (uint8_t)0xA6U, (uint8_t)0x3BU, (uint8_t)0xB4U, (uint8_t)0x54U, (uint8_t)0x32U, (uint8_t)0x9BU, (uint8_t)0x76U, (uint8_t)0x24U, (uint8_t)0xC8U, (uint8_t)0x91U, (uint8_t)0x7BU, (uint8_t)0xDDU, (uint8_t)0x64U, (uint8_t)0xB1U, (uint8_t)0xC0U, (uint8_t)0xFDU, (uint8_t)0x4CU, (uint8_t)0xB3U, (uint8_t)0x8EU, (uint8_t)0x8CU, (uint8_t)0x33U, (uint8_t)0x4CU, (uint8_t)0x70U, (uint8_t)0x1CU, (uint8_t)0x3AU, (uint8_t)0xCDU, (uint8_t)0xADU, (uint8_t)0x06U, (uint8_t)0x57U, (uint8_t)0xFCU, (uint8_t)0xCFU, (uint8_t)0xECU, (uint8_t)0x71U, (uint8_t)0x9BU, (uint8_t)0x1FU, (uint8_t)0x5CU, (uint8_t)0x3EU, (uint8_t)0x4EU, (uint8_t)0x46U, (uint8_t)0x04U, (uint8_t)0x1FU, (uint8_t)0x38U, (uint8_t)0x81U, (uint8_t)0x47U, (uint8_t)0xFBU, (uint8_t)0x4CU, (uint8_t)0xFDU, (uint8_t)0xB4U, (uint8_t)0x77U, (uint8_t)0xA5U, (uint8_t)0x24U, (uint8_t)0x71U, (uint8_t)0xF7U, (uint8_t)0xA9U, (uint8_t)0xA9U, (uint8_t)0x69U, (uint8_t)0x10U, (uint8_t)0xB8U, (uint8_t)0x55U, (uint8_t)0x32U, (uint8_t)0x2EU, (uint8_t)0xDBU, (uint8_t)0x63U, (uint8_t)0x40U, (uint8_t)0xD8U, (uint8_t)0xA0U, (uint8_t)0x0EU, (uint8_t)0xF0U, (uint8_t)0x92U, (uint8_t)0x35U, (uint8_t)0x05U, (uint8_t)0x11U, (uint8_t)0xE3U, (uint8_t)0x0AU, (uint8_t)0xBEU, (uint8_t)0xC1U, (uint8_t)0xFFU, (uint8_t)0xF9U, (uint8_t)0xE3U, (uint8_t)0xA2U, (uint8_t)0x6EU, (uint8_t)0x7FU, (uint8_t)0xB2U, (uint8_t)0x9FU, (uint8_t)0x8CU, (uint8_t)0x18U, (uint8_t)0x30U, (uint8_t)0x23U, (uint8_t)0xC3U, (uint8_t)0x58U, (uint8_t)0x7EU, (uint8_t)0x38U, (uint8_t)0xDAU, (uint8_t)0x00U, (uint8_t)0x77U, (uint8_t)0xD9U, (uint8_t)0xB4U, (uint8_t)0x76U, (uint8_t)0x3EU, (uint8_t)0x4EU, (uint8_t)0x4BU, (uint8_t)0x94U, (uint8_t)0xB2U, (uint8_t)0xBBU, (uint8_t)0xC1U, (uint8_t)0x94U, (uint8_t)0xC6U, (uint8_t)0x65U, (uint8_t)0x1EU, (uint8_t)0x77U, (uint8_t)0xCAU, (uint8_t)0xF9U, (uint8_t)0x92U, (uint8_t)0xEEU, (uint8_t)0xAAU, (uint8_t)0xC0U, (uint8_t)0x23U, (uint8_t)0x2AU, (uint8_t)0x28U, (uint8_t)0x1BU, (uint8_t)0xF6U, (uint8_t)0xB3U, (uint8_t)0xA7U, (uint8_t)0x39U, (uint8_t)0xC1U, (uint8_t)0x22U, (uint8_t)0x61U, (uint8_t)0x16U, (uint8_t)0x82U, (uint8_t)0x0AU, (uint8_t)0xE8U, (uint8_t)0xDBU, (uint8_t)0x58U, (uint8_t)0x47U, (uint8_t)0xA6U, (uint8_t)0x7CU, (uint8_t)0xBEU, (uint8_t)0xF9U, (uint8_t)0xC9U, (uint8_t)0x09U, (uint8_t)0x1BU, (uint8_t)0x46U, (uint8_t)0x2DU, (uint8_t)0x53U, (uint8_t)0x8CU, (uint8_t)0xD7U, (uint8_t)0x2BU, (uint8_t)0x03U, (uint8_t)0x74U, (uint8_t)0x6AU, (uint8_t)0xE7U, (uint8_t)0x7FU, (uint8_t)0x5EU, (uint8_t)0x62U, (uint8_t)0x29U, (uint8_t)0x2CU, (uint8_t)0x31U, (uint8_t)0x15U, (uint8_t)0x62U, (uint8_t)0xA8U, (uint8_t)0x46U, (uint8_t)0x50U, (uint8_t)0x5DU, (uint8_t)0xC8U, (uint8_t)0x2DU, (uint8_t)0xB8U, (uint8_t)0x54U, (uint8_t)0x33U, (uint8_t)0x8AU, (uint8_t)0xE4U, (uint8_t)0x9FU, (uint8_t)0x52U, (uint8_t)0x35U, (uint8_t)0xC9U, (uint8_t)0x5BU, (uint8_t)0x91U, (uint8_t)0x17U, (uint8_t)0x8CU, (uint8_t)0xCFU, (uint8_t)0x2DU, (uint8_t)0xD5U, (uint8_t)0xCAU, (uint8_t)0xCEU, (uint8_t)0xF4U, (uint8_t)0x03U, (uint8_t)0xECU, (uint8_t)0x9DU, (uint8_t)0x18U, (uint8_t)0x10U, (uint8_t)0xC6U, (uint8_t)0x27U, (uint8_t)0x2BU, (uint8_t)0x04U, (uint8_t)0x5BU, (uint8_t)0x3BU, (uint8_t)0x71U, (uint8_t)0xF9U, (uint8_t)0xDCU, (uint8_t)0x6BU, (uint8_t)0x80U, (uint8_t)0xD6U, (uint8_t)0x3FU, (uint8_t)0xDDU, (uint8_t)0x4AU, (uint8_t)0x8EU, (uint8_t)0x9AU, (uint8_t)0xDBU, (uint8_t)0x1EU, (uint8_t)0x69U, (uint8_t)0x62U, (uint8_t)0xA6U, (uint8_t)0x95U, (uint8_t)0x26U, (uint8_t)0xD4U, (uint8_t)0x31U, (uint8_t)0x61U, (uint8_t)0xC1U, (uint8_t)0xA4U, (uint8_t)0x1DU, (uint8_t)0x57U, (uint8_t)0x0DU, (uint8_t)0x79U, (uint8_t)0x38U, (uint8_t)0xDAU, (uint8_t)0xD4U, (uint8_t)0xA4U, (uint8_t)0x0EU, (uint8_t)0x32U, (uint8_t)0x9CU, (uint8_t)0xCFU, (uint8_t)0xF4U, (uint8_t)0x6AU, (uint8_t)0xAAU, (uint8_t)0x36U, (uint8_t)0xADU, (uint8_t)0x00U, (uint8_t)0x4CU, (uint8_t)0xF6U, (uint8_t)0x00U, (uint8_t)0xC8U, (uint8_t)0x38U, (uint8_t)0x1EU, (uint8_t)0x42U, (uint8_t)0x5AU, (uint8_t)0x31U, (uint8_t)0xD9U, (uint8_t)0x51U, (uint8_t)0xAEU, (uint8_t)0x64U, (uint8_t)0xFDU, (uint8_t)0xB2U, (uint8_t)0x3FU, (uint8_t)0xCEU, (uint8_t)0xC9U, (uint8_t)0x50U, (uint8_t)0x9DU, (uint8_t)0x43U, (uint8_t)0x68U, (uint8_t)0x7FU, (uint8_t)0xEBU, (uint8_t)0x69U, (uint8_t)0xEDU, (uint8_t)0xD1U, (uint8_t)0xCCU, (uint8_t)0x5EU, (uint8_t)0x0BU, (uint8_t)0x8CU, (uint8_t)0xC3U, (uint8_t)0xBDU, (uint8_t)0xF6U, (uint8_t)0x4BU, (uint8_t)0x10U, (uint8_t)0xEFU, (uint8_t)0x86U, (uint8_t)0xB6U, (uint8_t)0x31U, (uint8_t)0x42U, (uint8_t)0xA3U, (uint8_t)0xABU, (uint8_t)0x88U, (uint8_t)0x29U, (uint8_t)0x55U, (uint8_t)0x5BU, (uint8_t)0x2FU, (uint8_t)0x74U, (uint8_t)0x7CU, (uint8_t)0x93U, (uint8_t)0x26U, (uint8_t)0x65U, (uint8_t)0xCBU, (uint8_t)0x2CU, (uint8_t)0x0FU, (uint8_t)0x1CU, (uint8_t)0xC0U, (uint8_t)0x1BU, (uint8_t)0xD7U, (uint8_t)0x02U, (uint8_t)0x29U, (uint8_t)0x38U, (uint8_t)0x88U, (uint8_t)0x39U, (uint8_t)0xD2U, (uint8_t)0xAFU, (uint8_t)0x05U, (uint8_t)0xE4U, (uint8_t)0x54U, (uint8_t)0x50U, (uint8_t)0x4AU, (uint8_t)0xC7U, (uint8_t)0x8BU, (uint8_t)0x75U, (uint8_t)0x82U, (uint8_t)0x82U, (uint8_t)0x28U, (uint8_t)0x46U, (uint8_t)0xC0U, (uint8_t)0xBAU, (uint8_t)0x35U, (uint8_t)0xC3U, (uint8_t)0x5FU, (uint8_t)0x5CU, (uint8_t)0x59U, (uint8_t)0x16U, (uint8_t)0x0CU, (uint8_t)0xC0U, (uint8_t)0x46U, (uint8_t)0xFDU, (uint8_t)0x82U, (uint8_t)0x51U, (uint8_t)0x54U, (uint8_t)0x1FU, (uint8_t)0xC6U, (uint8_t)0x8CU, (uint8_t)0x9CU, (uint8_t)0x86U, (uint8_t)0xB0U, (uint8_t)0x22U, (uint8_t)0xBBU, (uint8_t)0x70U, (uint8_t)0x99U, (uint8_t)0x87U, (uint8_t)0x6AU, (uint8_t)0x46U, (uint8_t)0x0EU, (uint8_t)0x74U, (uint8_t)0x51U, (uint8_t)0xA8U, (uint8_t)0xA9U, (uint8_t)0x31U, (uint8_t)0x09U, (uint8_t)0x70U, (uint8_t)0x3FU, (uint8_t)0xEEU, (uint8_t)0x1CU, (uint8_t)0x21U, (uint8_t)0x7EU, (uint8_t)0x6CU, (uint8_t)0x38U, (uint8_t)0x26U, (uint8_t)0xE5U, (uint8_t)0x2CU, (uint8_t)0x51U, (uint8_t)0xAAU, (uint8_t)0x69U, (uint8_t)0x1EU, (uint8_t)0x0EU, (uint8_t)0x42U, (uint8_t)0x3CU, (uint8_t)0xFCU, (uint8_t)0x99U, (uint8_t)0xE9U, (uint8_t)0xE3U, (uint8_t)0x16U, (uint8_t)0x50U, (uint8_t)0xC1U, (uint8_t)0x21U, (uint8_t)0x7BU, (uint8_t)0x62U, (uint8_t)0x48U, (uint8_t)0x16U, (uint8_t)0xCDU, (uint8_t)0xADU, (uint8_t)0x9AU, (uint8_t)0x95U, (uint8_t)0xF9U, (uint8_t)0xD5U, (uint8_t)0xB8U, (uint8_t)0x01U, (uint8_t)0x94U, (uint8_t)0x88U, (uint8_t)0xD9U, (uint8_t)0xC0U, (uint8_t)0xA0U, (uint8_t)0xA1U, (uint8_t)0xFEU, (uint8_t)0x30U, (uint8_t)0x75U, (uint8_t)0xA5U, (uint8_t)0x77U, (uint8_t)0xE2U, (uint8_t)0x31U, (uint8_t)0x83U, (uint8_t)0xF8U, (uint8_t)0x1DU, (uint8_t)0x4AU, (uint8_t)0x3FU, (uint8_t)0x2FU, (uint8_t)0xA4U, (uint8_t)0x57U, (uint8_t)0x1EU, (uint8_t)0xFCU, (uint8_t)0x8CU, (uint8_t)0xE0U, (uint8_t)0xBAU, (uint8_t)0x8AU, (uint8_t)0x4FU, (uint8_t)0xE8U, (uint8_t)0xB6U, (uint8_t)0x85U, (uint8_t)0x5DU, (uint8_t)0xFEU, (uint8_t)0x72U, (uint8_t)0xB0U, (uint8_t)0xA6U, (uint8_t)0x6EU, (uint8_t)0xDEU, (uint8_t)0xD2U, (uint8_t)0xFBU, (uint8_t)0xABU, (uint8_t)0xFBU, (uint8_t)0xE5U, (uint8_t)0x8AU, (uint8_t)0x30U, (uint8_t)0xFAU, (uint8_t)0xFAU, (uint8_t)0xBEU, (uint8_t)0x1CU, (uint8_t)0x5DU, (uint8_t)0x71U, (uint8_t)0xA8U, (uint8_t)0x7EU, (uint8_t)0x2FU, (uint8_t)0x74U, (uint8_t)0x1EU, (uint8_t)0xF8U, (uint8_t)0xC1U, (uint8_t)0xFEU, (uint8_t)0x86U, (uint8_t)0xFEU, (uint8_t)0xA6U, (uint8_t)0xBBU, (uint8_t)0xFDU, (uint8_t)0xE5U, (uint8_t)0x30U, (uint8_t)0x67U, (uint8_t)0x7FU, (uint8_t)0x0DU, (uint8_t)0x97U, (uint8_t)0xD1U, (uint8_t)0x1DU, (uint8_t)0x49U, (uint8_t)0xF7U, (uint8_t)0xA8U, (uint8_t)0x44U, (uint8_t)0x3DU, (uint8_t)0x08U, (uint8_t)0x22U, (uint8_t)0xE5U, (uint8_t)0x06U, (uint8_t)0xA9U, (uint8_t)0xF4U, (uint8_t)0x61U, (uint8_t)0x4EU, (uint8_t)0x01U, (uint8_t)0x1EU, (uint8_t)0x2AU, (uint8_t)0x94U, (uint8_t)0x83U, (uint8_t)0x8FU, (uint8_t)0xF8U, (uint8_t)0x8CU, (uint8_t)0xD6U, (uint8_t)0x8CU, (uint8_t)0x8BU, (uint8_t)0xB7U, (uint8_t)0xC5U, (uint8_t)0xC6U, (uint8_t)0x42U, (uint8_t)0x4CU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU, (uint8_t)0xFFU }; #if defined(__cplusplus) } #endif #define __Hacl_Impl_FFDHE_Constants_H_DEFINED #endif