typedef uint64_t fe_t[LIMB_CNT];
typedef uint64_t limb_t;
+#ifdef OPENSSL_NO_ASM
+#define FIAT_ID_TC26_GOST_3410_2012_512_PARAMSETA_NO_ASM
+#endif
+
#define fe_copy(d, s) memcpy(d, s, sizeof(fe_t))
#define fe_set_zero(d) memset(d, 0, sizeof(fe_t))
* SOFTWARE.
*/
-/* Autogenerated: unsaturated_solinas --static id_tc26_gost_3410_2012_512_paramSetA 64 '(auto)' '2^512 - 569' */
+/* Autogenerated: unsaturated_solinas --static --use-value-barrier id_tc26_gost_3410_2012_512_paramSetA 64 '(auto)' '2^512 - 569' */
/* curve description: id_tc26_gost_3410_2012_512_paramSetA */
/* machine_wordsize = 64 (from "64") */
/* requested operations: (all) */
/* n = 10 (from "(auto)") */
/* s-c = 2^512 - [(1, 569)] (from "2^512 - 569") */
-/* tight_bounds_multiplier = 1.1 (from "") */
+/* tight_bounds_multiplier = 1 (from "") */
/* */
/* Computed values: */
/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] */
/* eval z = z[0] + (z[1] << 52) + (z[2] << 103) + (z[3] << 154) + (z[4] << 205) + (z[5] << 256) + (z[6] << 0x134) + (z[7] << 0x167) + (z[8] << 0x19a) + (z[9] << 0x1cd) */
/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) */
+/* balance = [0x1ffffffffffb8e, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0x1ffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe] */
#include <stdint.h>
typedef unsigned char fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1;
#error "This code only works on a two's complement system"
#endif
+#if !defined(FIAT_ID_TC26_GOST_3410_2012_512_PARAMSETA_NO_ASM) && \
+ (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint64_t
+fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u64(uint64_t a) {
+ __asm__("" : "+r"(a) : /* no inputs */);
+ return a;
+}
+#else
+#define fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u64(x) (x)
+#endif
+
/*
* The function fiat_id_tc26_gost_3410_2012_512_paramSetA_addcarryx_u52 is an addition with carry.
* Postconditions:
x1 = (!(!arg1));
x2 = ((fiat_id_tc26_gost_3410_2012_512_paramSetA_int1)(0x0 - x1) &
UINT64_C(0xffffffffffffffff));
- x3 = ((x2 & arg3) | ((~x2) & arg2));
+ x3 = ((fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u64(x2) &
+ arg3) |
+ (fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u64((~x2)) &
+ arg2));
*out1 = x3;
}
* eval out1 mod m = (eval arg1 * eval arg2) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- * arg2: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ * arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
+ * arg2: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_carry_mul(
uint64_t out1[10], const uint64_t arg1[10], const uint64_t arg2[10]) {
* eval out1 mod m = (eval arg1 * eval arg1) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ * arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_carry_square(
uint64_t out1[10], const uint64_t arg1[10]) {
* eval out1 mod m = eval arg1 mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ * arg1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_carry(
uint64_t out1[10], const uint64_t arg1[10]) {
* eval out1 mod m = (eval arg1 + eval arg2) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- * arg2: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
+ * arg2: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ * out1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_add(
uint64_t out1[10], const uint64_t arg1[10], const uint64_t arg2[10]) {
* eval out1 mod m = (eval arg1 - eval arg2) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- * arg2: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
+ * arg2: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ * out1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_sub(
uint64_t out1[10], const uint64_t arg1[10], const uint64_t arg2[10]) {
* eval out1 mod m = -eval arg1 mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x34cccccccccccb], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
+ * out1: [[0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x30000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_opp(
uint64_t out1[10], const uint64_t arg1[10]) {
* out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..63]
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * arg1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
* Output Bounds:
* out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
*/
uint64_t x47;
uint64_t x48;
uint64_t x49;
- uint64_t x50;
- uint8_t x51;
- uint64_t x52;
- uint8_t x53;
- uint64_t x54;
- uint8_t x55;
- uint64_t x56;
- uint8_t x57;
- uint64_t x58;
- uint8_t x59;
+ uint8_t x50;
+ uint64_t x51;
+ uint8_t x52;
+ uint64_t x53;
+ uint8_t x54;
+ uint64_t x55;
+ uint8_t x56;
+ uint64_t x57;
+ uint8_t x58;
+ uint64_t x59;
uint8_t x60;
uint8_t x61;
uint64_t x62;
- uint64_t x63;
- uint8_t x64;
- uint64_t x65;
- uint8_t x66;
- uint64_t x67;
- uint8_t x68;
- uint64_t x69;
- uint8_t x70;
- uint64_t x71;
- uint8_t x72;
+ uint8_t x63;
+ uint64_t x64;
+ uint8_t x65;
+ uint64_t x66;
+ uint8_t x67;
+ uint64_t x68;
+ uint8_t x69;
+ uint64_t x70;
+ uint8_t x71;
+ uint64_t x72;
uint8_t x73;
uint8_t x74;
uint64_t x75;
- uint64_t x76;
- uint8_t x77;
- uint64_t x78;
- uint8_t x79;
- uint64_t x80;
- uint8_t x81;
- uint64_t x82;
- uint8_t x83;
- uint64_t x84;
- uint8_t x85;
- uint64_t x86;
- uint8_t x87;
+ uint8_t x76;
+ uint64_t x77;
+ uint8_t x78;
+ uint64_t x79;
+ uint8_t x80;
+ uint64_t x81;
+ uint8_t x82;
+ uint64_t x83;
+ uint8_t x84;
+ uint64_t x85;
+ uint8_t x86;
+ uint64_t x87;
uint8_t x88;
uint8_t x89;
uint64_t x90;
- uint64_t x91;
- uint8_t x92;
- uint64_t x93;
- uint8_t x94;
- uint64_t x95;
- uint8_t x96;
- uint64_t x97;
- uint8_t x98;
- uint64_t x99;
- uint8_t x100;
+ uint8_t x91;
+ uint64_t x92;
+ uint8_t x93;
+ uint64_t x94;
+ uint8_t x95;
+ uint64_t x96;
+ uint8_t x97;
+ uint64_t x98;
+ uint8_t x99;
+ uint64_t x100;
uint8_t x101;
uint8_t x102;
uint64_t x103;
- uint64_t x104;
- uint8_t x105;
- uint64_t x106;
- uint8_t x107;
- uint64_t x108;
- uint8_t x109;
- uint64_t x110;
- uint8_t x111;
- uint64_t x112;
- uint8_t x113;
+ uint8_t x104;
+ uint64_t x105;
+ uint8_t x106;
+ uint64_t x107;
+ uint8_t x108;
+ uint64_t x109;
+ uint8_t x110;
+ uint64_t x111;
+ uint8_t x112;
+ uint64_t x113;
uint8_t x114;
uint8_t x115;
uint8_t x116;
uint64_t x125;
uint8_t x126;
uint8_t x127;
- uint8_t x128;
- uint64_t x129;
+ uint64_t x128;
+ uint8_t x129;
uint64_t x130;
uint8_t x131;
uint64_t x132;
uint64_t x138;
uint8_t x139;
uint8_t x140;
- uint8_t x141;
- uint64_t x142;
+ uint64_t x141;
+ uint8_t x142;
uint64_t x143;
uint8_t x144;
uint64_t x145;
uint64_t x153;
uint8_t x154;
uint8_t x155;
- uint8_t x156;
- uint64_t x157;
+ uint64_t x156;
+ uint8_t x157;
uint64_t x158;
uint8_t x159;
uint64_t x160;
uint64_t x166;
uint8_t x167;
uint8_t x168;
- uint8_t x169;
- uint64_t x170;
+ uint64_t x169;
+ uint8_t x170;
uint64_t x171;
uint8_t x172;
uint64_t x173;
uint64_t x179;
uint8_t x180;
uint8_t x181;
- uint8_t x182;
fiat_id_tc26_gost_3410_2012_512_paramSetA_subborrowx_u52(
&x1, &x2, 0x0, (arg1[0]), UINT64_C(0xffffffffffdc7));
fiat_id_tc26_gost_3410_2012_512_paramSetA_subborrowx_u51(
x47 = (x28 << 2);
x48 = (x26 << 7);
x49 = (x24 << 4);
- x50 = (x22 >> 8);
- x51 = (uint8_t)(x22 & UINT8_C(0xff));
- x52 = (x50 >> 8);
- x53 = (uint8_t)(x50 & UINT8_C(0xff));
- x54 = (x52 >> 8);
- x55 = (uint8_t)(x52 & UINT8_C(0xff));
- x56 = (x54 >> 8);
- x57 = (uint8_t)(x54 & UINT8_C(0xff));
- x58 = (x56 >> 8);
- x59 = (uint8_t)(x56 & UINT8_C(0xff));
- x60 = (uint8_t)(x58 >> 8);
- x61 = (uint8_t)(x58 & UINT8_C(0xff));
- x62 = (x60 + x49);
- x63 = (x62 >> 8);
- x64 = (uint8_t)(x62 & UINT8_C(0xff));
- x65 = (x63 >> 8);
- x66 = (uint8_t)(x63 & UINT8_C(0xff));
- x67 = (x65 >> 8);
- x68 = (uint8_t)(x65 & UINT8_C(0xff));
- x69 = (x67 >> 8);
- x70 = (uint8_t)(x67 & UINT8_C(0xff));
- x71 = (x69 >> 8);
- x72 = (uint8_t)(x69 & UINT8_C(0xff));
- x73 = (uint8_t)(x71 >> 8);
- x74 = (uint8_t)(x71 & UINT8_C(0xff));
- x75 = (x73 + x48);
- x76 = (x75 >> 8);
- x77 = (uint8_t)(x75 & UINT8_C(0xff));
- x78 = (x76 >> 8);
- x79 = (uint8_t)(x76 & UINT8_C(0xff));
- x80 = (x78 >> 8);
- x81 = (uint8_t)(x78 & UINT8_C(0xff));
- x82 = (x80 >> 8);
- x83 = (uint8_t)(x80 & UINT8_C(0xff));
- x84 = (x82 >> 8);
- x85 = (uint8_t)(x82 & UINT8_C(0xff));
- x86 = (x84 >> 8);
- x87 = (uint8_t)(x84 & UINT8_C(0xff));
- x88 = (uint8_t)(x86 >> 8);
- x89 = (uint8_t)(x86 & UINT8_C(0xff));
- x90 = (x88 + x47);
- x91 = (x90 >> 8);
- x92 = (uint8_t)(x90 & UINT8_C(0xff));
- x93 = (x91 >> 8);
- x94 = (uint8_t)(x91 & UINT8_C(0xff));
- x95 = (x93 >> 8);
- x96 = (uint8_t)(x93 & UINT8_C(0xff));
- x97 = (x95 >> 8);
- x98 = (uint8_t)(x95 & UINT8_C(0xff));
- x99 = (x97 >> 8);
- x100 = (uint8_t)(x97 & UINT8_C(0xff));
- x101 = (uint8_t)(x99 >> 8);
- x102 = (uint8_t)(x99 & UINT8_C(0xff));
- x103 = (x101 + x46);
- x104 = (x103 >> 8);
- x105 = (uint8_t)(x103 & UINT8_C(0xff));
- x106 = (x104 >> 8);
- x107 = (uint8_t)(x104 & UINT8_C(0xff));
- x108 = (x106 >> 8);
- x109 = (uint8_t)(x106 & UINT8_C(0xff));
- x110 = (x108 >> 8);
- x111 = (uint8_t)(x108 & UINT8_C(0xff));
- x112 = (x110 >> 8);
- x113 = (uint8_t)(x110 & UINT8_C(0xff));
- x114 = (uint8_t)(x112 >> 8);
- x115 = (uint8_t)(x112 & UINT8_C(0xff));
- x116 = (uint8_t)(x114 & UINT8_C(0xff));
+ x50 = (uint8_t)(x22 & UINT8_C(0xff));
+ x51 = (x22 >> 8);
+ x52 = (uint8_t)(x51 & UINT8_C(0xff));
+ x53 = (x51 >> 8);
+ x54 = (uint8_t)(x53 & UINT8_C(0xff));
+ x55 = (x53 >> 8);
+ x56 = (uint8_t)(x55 & UINT8_C(0xff));
+ x57 = (x55 >> 8);
+ x58 = (uint8_t)(x57 & UINT8_C(0xff));
+ x59 = (x57 >> 8);
+ x60 = (uint8_t)(x59 & UINT8_C(0xff));
+ x61 = (uint8_t)(x59 >> 8);
+ x62 = (x49 + (uint64_t)x61);
+ x63 = (uint8_t)(x62 & UINT8_C(0xff));
+ x64 = (x62 >> 8);
+ x65 = (uint8_t)(x64 & UINT8_C(0xff));
+ x66 = (x64 >> 8);
+ x67 = (uint8_t)(x66 & UINT8_C(0xff));
+ x68 = (x66 >> 8);
+ x69 = (uint8_t)(x68 & UINT8_C(0xff));
+ x70 = (x68 >> 8);
+ x71 = (uint8_t)(x70 & UINT8_C(0xff));
+ x72 = (x70 >> 8);
+ x73 = (uint8_t)(x72 & UINT8_C(0xff));
+ x74 = (uint8_t)(x72 >> 8);
+ x75 = (x48 + (uint64_t)x74);
+ x76 = (uint8_t)(x75 & UINT8_C(0xff));
+ x77 = (x75 >> 8);
+ x78 = (uint8_t)(x77 & UINT8_C(0xff));
+ x79 = (x77 >> 8);
+ x80 = (uint8_t)(x79 & UINT8_C(0xff));
+ x81 = (x79 >> 8);
+ x82 = (uint8_t)(x81 & UINT8_C(0xff));
+ x83 = (x81 >> 8);
+ x84 = (uint8_t)(x83 & UINT8_C(0xff));
+ x85 = (x83 >> 8);
+ x86 = (uint8_t)(x85 & UINT8_C(0xff));
+ x87 = (x85 >> 8);
+ x88 = (uint8_t)(x87 & UINT8_C(0xff));
+ x89 = (uint8_t)(x87 >> 8);
+ x90 = (x47 + (uint64_t)x89);
+ x91 = (uint8_t)(x90 & UINT8_C(0xff));
+ x92 = (x90 >> 8);
+ x93 = (uint8_t)(x92 & UINT8_C(0xff));
+ x94 = (x92 >> 8);
+ x95 = (uint8_t)(x94 & UINT8_C(0xff));
+ x96 = (x94 >> 8);
+ x97 = (uint8_t)(x96 & UINT8_C(0xff));
+ x98 = (x96 >> 8);
+ x99 = (uint8_t)(x98 & UINT8_C(0xff));
+ x100 = (x98 >> 8);
+ x101 = (uint8_t)(x100 & UINT8_C(0xff));
+ x102 = (uint8_t)(x100 >> 8);
+ x103 = (x46 + (uint64_t)x102);
+ x104 = (uint8_t)(x103 & UINT8_C(0xff));
+ x105 = (x103 >> 8);
+ x106 = (uint8_t)(x105 & UINT8_C(0xff));
+ x107 = (x105 >> 8);
+ x108 = (uint8_t)(x107 & UINT8_C(0xff));
+ x109 = (x107 >> 8);
+ x110 = (uint8_t)(x109 & UINT8_C(0xff));
+ x111 = (x109 >> 8);
+ x112 = (uint8_t)(x111 & UINT8_C(0xff));
+ x113 = (x111 >> 8);
+ x114 = (uint8_t)(x113 & UINT8_C(0xff));
+ x115 = (uint8_t)(x113 >> 8);
+ x116 = (uint8_t)(x32 & UINT8_C(0xff));
x117 = (x32 >> 8);
- x118 = (uint8_t)(x32 & UINT8_C(0xff));
+ x118 = (uint8_t)(x117 & UINT8_C(0xff));
x119 = (x117 >> 8);
- x120 = (uint8_t)(x117 & UINT8_C(0xff));
+ x120 = (uint8_t)(x119 & UINT8_C(0xff));
x121 = (x119 >> 8);
- x122 = (uint8_t)(x119 & UINT8_C(0xff));
+ x122 = (uint8_t)(x121 & UINT8_C(0xff));
x123 = (x121 >> 8);
- x124 = (uint8_t)(x121 & UINT8_C(0xff));
+ x124 = (uint8_t)(x123 & UINT8_C(0xff));
x125 = (x123 >> 8);
- x126 = (uint8_t)(x123 & UINT8_C(0xff));
+ x126 = (uint8_t)(x125 & UINT8_C(0xff));
x127 = (uint8_t)(x125 >> 8);
- x128 = (uint8_t)(x125 & UINT8_C(0xff));
- x129 = (x127 + x45);
- x130 = (x129 >> 8);
- x131 = (uint8_t)(x129 & UINT8_C(0xff));
+ x128 = (x45 + (uint64_t)x127);
+ x129 = (uint8_t)(x128 & UINT8_C(0xff));
+ x130 = (x128 >> 8);
+ x131 = (uint8_t)(x130 & UINT8_C(0xff));
x132 = (x130 >> 8);
- x133 = (uint8_t)(x130 & UINT8_C(0xff));
+ x133 = (uint8_t)(x132 & UINT8_C(0xff));
x134 = (x132 >> 8);
- x135 = (uint8_t)(x132 & UINT8_C(0xff));
+ x135 = (uint8_t)(x134 & UINT8_C(0xff));
x136 = (x134 >> 8);
- x137 = (uint8_t)(x134 & UINT8_C(0xff));
+ x137 = (uint8_t)(x136 & UINT8_C(0xff));
x138 = (x136 >> 8);
- x139 = (uint8_t)(x136 & UINT8_C(0xff));
+ x139 = (uint8_t)(x138 & UINT8_C(0xff));
x140 = (uint8_t)(x138 >> 8);
- x141 = (uint8_t)(x138 & UINT8_C(0xff));
- x142 = (x140 + x44);
- x143 = (x142 >> 8);
- x144 = (uint8_t)(x142 & UINT8_C(0xff));
+ x141 = (x44 + (uint64_t)x140);
+ x142 = (uint8_t)(x141 & UINT8_C(0xff));
+ x143 = (x141 >> 8);
+ x144 = (uint8_t)(x143 & UINT8_C(0xff));
x145 = (x143 >> 8);
- x146 = (uint8_t)(x143 & UINT8_C(0xff));
+ x146 = (uint8_t)(x145 & UINT8_C(0xff));
x147 = (x145 >> 8);
- x148 = (uint8_t)(x145 & UINT8_C(0xff));
+ x148 = (uint8_t)(x147 & UINT8_C(0xff));
x149 = (x147 >> 8);
- x150 = (uint8_t)(x147 & UINT8_C(0xff));
+ x150 = (uint8_t)(x149 & UINT8_C(0xff));
x151 = (x149 >> 8);
- x152 = (uint8_t)(x149 & UINT8_C(0xff));
+ x152 = (uint8_t)(x151 & UINT8_C(0xff));
x153 = (x151 >> 8);
- x154 = (uint8_t)(x151 & UINT8_C(0xff));
+ x154 = (uint8_t)(x153 & UINT8_C(0xff));
x155 = (uint8_t)(x153 >> 8);
- x156 = (uint8_t)(x153 & UINT8_C(0xff));
- x157 = (x155 + x43);
- x158 = (x157 >> 8);
- x159 = (uint8_t)(x157 & UINT8_C(0xff));
+ x156 = (x43 + (uint64_t)x155);
+ x157 = (uint8_t)(x156 & UINT8_C(0xff));
+ x158 = (x156 >> 8);
+ x159 = (uint8_t)(x158 & UINT8_C(0xff));
x160 = (x158 >> 8);
- x161 = (uint8_t)(x158 & UINT8_C(0xff));
+ x161 = (uint8_t)(x160 & UINT8_C(0xff));
x162 = (x160 >> 8);
- x163 = (uint8_t)(x160 & UINT8_C(0xff));
+ x163 = (uint8_t)(x162 & UINT8_C(0xff));
x164 = (x162 >> 8);
- x165 = (uint8_t)(x162 & UINT8_C(0xff));
+ x165 = (uint8_t)(x164 & UINT8_C(0xff));
x166 = (x164 >> 8);
- x167 = (uint8_t)(x164 & UINT8_C(0xff));
+ x167 = (uint8_t)(x166 & UINT8_C(0xff));
x168 = (uint8_t)(x166 >> 8);
- x169 = (uint8_t)(x166 & UINT8_C(0xff));
- x170 = (x168 + x42);
- x171 = (x170 >> 8);
- x172 = (uint8_t)(x170 & UINT8_C(0xff));
+ x169 = (x42 + (uint64_t)x168);
+ x170 = (uint8_t)(x169 & UINT8_C(0xff));
+ x171 = (x169 >> 8);
+ x172 = (uint8_t)(x171 & UINT8_C(0xff));
x173 = (x171 >> 8);
- x174 = (uint8_t)(x171 & UINT8_C(0xff));
+ x174 = (uint8_t)(x173 & UINT8_C(0xff));
x175 = (x173 >> 8);
- x176 = (uint8_t)(x173 & UINT8_C(0xff));
+ x176 = (uint8_t)(x175 & UINT8_C(0xff));
x177 = (x175 >> 8);
- x178 = (uint8_t)(x175 & UINT8_C(0xff));
+ x178 = (uint8_t)(x177 & UINT8_C(0xff));
x179 = (x177 >> 8);
- x180 = (uint8_t)(x177 & UINT8_C(0xff));
+ x180 = (uint8_t)(x179 & UINT8_C(0xff));
x181 = (uint8_t)(x179 >> 8);
- x182 = (uint8_t)(x179 & UINT8_C(0xff));
- out1[0] = x51;
- out1[1] = x53;
- out1[2] = x55;
- out1[3] = x57;
- out1[4] = x59;
- out1[5] = x61;
- out1[6] = x64;
- out1[7] = x66;
- out1[8] = x68;
- out1[9] = x70;
- out1[10] = x72;
- out1[11] = x74;
- out1[12] = x77;
- out1[13] = x79;
- out1[14] = x81;
- out1[15] = x83;
- out1[16] = x85;
- out1[17] = x87;
- out1[18] = x89;
- out1[19] = x92;
- out1[20] = x94;
- out1[21] = x96;
- out1[22] = x98;
- out1[23] = x100;
- out1[24] = x102;
- out1[25] = x105;
- out1[26] = x107;
- out1[27] = x109;
- out1[28] = x111;
- out1[29] = x113;
- out1[30] = x115;
- out1[31] = x116;
- out1[32] = x118;
- out1[33] = x120;
- out1[34] = x122;
- out1[35] = x124;
- out1[36] = x126;
- out1[37] = x128;
- out1[38] = x131;
- out1[39] = x133;
- out1[40] = x135;
- out1[41] = x137;
- out1[42] = x139;
- out1[43] = x141;
- out1[44] = x144;
- out1[45] = x146;
- out1[46] = x148;
- out1[47] = x150;
- out1[48] = x152;
- out1[49] = x154;
- out1[50] = x156;
- out1[51] = x159;
- out1[52] = x161;
- out1[53] = x163;
- out1[54] = x165;
- out1[55] = x167;
- out1[56] = x169;
- out1[57] = x172;
- out1[58] = x174;
- out1[59] = x176;
- out1[60] = x178;
- out1[61] = x180;
- out1[62] = x182;
+ out1[0] = x50;
+ out1[1] = x52;
+ out1[2] = x54;
+ out1[3] = x56;
+ out1[4] = x58;
+ out1[5] = x60;
+ out1[6] = x63;
+ out1[7] = x65;
+ out1[8] = x67;
+ out1[9] = x69;
+ out1[10] = x71;
+ out1[11] = x73;
+ out1[12] = x76;
+ out1[13] = x78;
+ out1[14] = x80;
+ out1[15] = x82;
+ out1[16] = x84;
+ out1[17] = x86;
+ out1[18] = x88;
+ out1[19] = x91;
+ out1[20] = x93;
+ out1[21] = x95;
+ out1[22] = x97;
+ out1[23] = x99;
+ out1[24] = x101;
+ out1[25] = x104;
+ out1[26] = x106;
+ out1[27] = x108;
+ out1[28] = x110;
+ out1[29] = x112;
+ out1[30] = x114;
+ out1[31] = x115;
+ out1[32] = x116;
+ out1[33] = x118;
+ out1[34] = x120;
+ out1[35] = x122;
+ out1[36] = x124;
+ out1[37] = x126;
+ out1[38] = x129;
+ out1[39] = x131;
+ out1[40] = x133;
+ out1[41] = x135;
+ out1[42] = x137;
+ out1[43] = x139;
+ out1[44] = x142;
+ out1[45] = x144;
+ out1[46] = x146;
+ out1[47] = x148;
+ out1[48] = x150;
+ out1[49] = x152;
+ out1[50] = x154;
+ out1[51] = x157;
+ out1[52] = x159;
+ out1[53] = x161;
+ out1[54] = x163;
+ out1[55] = x165;
+ out1[56] = x167;
+ out1[57] = x170;
+ out1[58] = x172;
+ out1[59] = x174;
+ out1[60] = x176;
+ out1[61] = x178;
+ out1[62] = x180;
out1[63] = x181;
}
* Input Bounds:
* arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
* Output Bounds:
- * out1: [[0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x11999999999999], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
+ * out1: [[0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x10000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_from_bytes(
uint64_t out1[10], const uint8_t arg1[64]) {
uint64_t x63;
uint8_t x64;
uint64_t x65;
- uint8_t x66;
+ uint64_t x66;
uint64_t x67;
uint64_t x68;
uint64_t x69;
uint64_t x70;
uint64_t x71;
- uint64_t x72;
+ uint8_t x72;
uint64_t x73;
uint64_t x74;
uint64_t x75;
uint64_t x76;
uint64_t x77;
- fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x78;
+ uint64_t x78;
uint64_t x79;
- uint64_t x80;
- uint8_t x81;
+ fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x80;
+ uint64_t x81;
uint64_t x82;
uint64_t x83;
- uint8_t x84;
+ uint64_t x84;
uint64_t x85;
uint64_t x86;
uint64_t x87;
- uint8_t x88;
- uint64_t x89;
+ uint64_t x88;
+ uint8_t x89;
uint64_t x90;
- fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x91;
+ uint64_t x91;
uint64_t x92;
uint64_t x93;
- uint8_t x94;
+ uint64_t x94;
uint64_t x95;
uint64_t x96;
uint8_t x97;
uint64_t x98;
uint64_t x99;
+ uint64_t x100;
+ uint64_t x101;
+ uint64_t x102;
+ uint64_t x103;
+ uint64_t x104;
+ uint64_t x105;
+ uint64_t x106;
+ uint64_t x107;
+ uint64_t x108;
+ uint64_t x109;
+ uint64_t x110;
+ uint8_t x111;
+ uint64_t x112;
+ uint64_t x113;
+ uint64_t x114;
+ uint64_t x115;
+ uint64_t x116;
+ uint64_t x117;
+ uint64_t x118;
+ fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x119;
+ uint64_t x120;
+ uint64_t x121;
+ uint64_t x122;
+ uint64_t x123;
+ uint64_t x124;
+ uint64_t x125;
+ uint64_t x126;
+ uint64_t x127;
+ uint8_t x128;
+ uint64_t x129;
+ uint64_t x130;
+ uint64_t x131;
+ uint64_t x132;
+ uint64_t x133;
+ uint64_t x134;
+ uint64_t x135;
+ uint8_t x136;
+ uint64_t x137;
+ uint64_t x138;
+ uint64_t x139;
+ uint64_t x140;
+ uint64_t x141;
+ uint64_t x142;
x1 = ((uint64_t)(arg1[63]) << 43);
x2 = ((uint64_t)(arg1[62]) << 35);
x3 = ((uint64_t)(arg1[61]) << 27);
x62 = ((uint64_t)(arg1[2]) << 16);
x63 = ((uint64_t)(arg1[1]) << 8);
x64 = (arg1[0]);
- x65 = (x64 + (x63 + (x62 + (x61 + (x60 + (x59 + x58))))));
- x66 = (uint8_t)(x65 >> 52);
- x67 = (x65 & UINT64_C(0xfffffffffffff));
- x68 = (x6 + (x5 + (x4 + (x3 + (x2 + x1)))));
- x69 = (x12 + (x11 + (x10 + (x9 + (x8 + x7)))));
- x70 = (x19 + (x18 + (x17 + (x16 + (x15 + (x14 + x13))))));
- x71 = (x25 + (x24 + (x23 + (x22 + (x21 + x20)))));
- x72 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + x26))))));
- x73 = (x38 + (x37 + (x36 + (x35 + (x34 + x33)))));
- x74 = (x44 + (x43 + (x42 + (x41 + (x40 + x39)))));
- x75 = (x51 + (x50 + (x49 + (x48 + (x47 + (x46 + x45))))));
- x76 = (x57 + (x56 + (x55 + (x54 + (x53 + x52)))));
- x77 = (x66 + x76);
- x78 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x77 >> 51);
- x79 = (x77 & UINT64_C(0x7ffffffffffff));
- x80 = (x78 + x75);
- x81 = (uint8_t)(x80 >> 51);
- x82 = (x80 & UINT64_C(0x7ffffffffffff));
- x83 = (x81 + x74);
- x84 = (uint8_t)(x83 >> 51);
- x85 = (x83 & UINT64_C(0x7ffffffffffff));
- x86 = (x84 + x73);
- x87 = (x86 & UINT64_C(0x7ffffffffffff));
- x88 = (uint8_t)(x72 >> 52);
- x89 = (x72 & UINT64_C(0xfffffffffffff));
- x90 = (x88 + x71);
- x91 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x90 >> 51);
- x92 = (x90 & UINT64_C(0x7ffffffffffff));
- x93 = (x91 + x70);
- x94 = (uint8_t)(x93 >> 51);
- x95 = (x93 & UINT64_C(0x7ffffffffffff));
- x96 = (x94 + x69);
- x97 = (uint8_t)(x96 >> 51);
- x98 = (x96 & UINT64_C(0x7ffffffffffff));
- x99 = (x97 + x68);
- out1[0] = x67;
+ x65 = (x63 + (uint64_t)x64);
+ x66 = (x62 + x65);
+ x67 = (x61 + x66);
+ x68 = (x60 + x67);
+ x69 = (x59 + x68);
+ x70 = (x58 + x69);
+ x71 = (x70 & UINT64_C(0xfffffffffffff));
+ x72 = (uint8_t)(x70 >> 52);
+ x73 = (x57 + (uint64_t)x72);
+ x74 = (x56 + x73);
+ x75 = (x55 + x74);
+ x76 = (x54 + x75);
+ x77 = (x53 + x76);
+ x78 = (x52 + x77);
+ x79 = (x78 & UINT64_C(0x7ffffffffffff));
+ x80 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x78 >> 51);
+ x81 = (x51 + (uint64_t)x80);
+ x82 = (x50 + x81);
+ x83 = (x49 + x82);
+ x84 = (x48 + x83);
+ x85 = (x47 + x84);
+ x86 = (x46 + x85);
+ x87 = (x45 + x86);
+ x88 = (x87 & UINT64_C(0x7ffffffffffff));
+ x89 = (uint8_t)(x87 >> 51);
+ x90 = (x44 + (uint64_t)x89);
+ x91 = (x43 + x90);
+ x92 = (x42 + x91);
+ x93 = (x41 + x92);
+ x94 = (x40 + x93);
+ x95 = (x39 + x94);
+ x96 = (x95 & UINT64_C(0x7ffffffffffff));
+ x97 = (uint8_t)(x95 >> 51);
+ x98 = (x38 + (uint64_t)x97);
+ x99 = (x37 + x98);
+ x100 = (x36 + x99);
+ x101 = (x35 + x100);
+ x102 = (x34 + x101);
+ x103 = (x33 + x102);
+ x104 = (x31 + (uint64_t)x32);
+ x105 = (x30 + x104);
+ x106 = (x29 + x105);
+ x107 = (x28 + x106);
+ x108 = (x27 + x107);
+ x109 = (x26 + x108);
+ x110 = (x109 & UINT64_C(0xfffffffffffff));
+ x111 = (uint8_t)(x109 >> 52);
+ x112 = (x25 + (uint64_t)x111);
+ x113 = (x24 + x112);
+ x114 = (x23 + x113);
+ x115 = (x22 + x114);
+ x116 = (x21 + x115);
+ x117 = (x20 + x116);
+ x118 = (x117 & UINT64_C(0x7ffffffffffff));
+ x119 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x117 >> 51);
+ x120 = (x19 + (uint64_t)x119);
+ x121 = (x18 + x120);
+ x122 = (x17 + x121);
+ x123 = (x16 + x122);
+ x124 = (x15 + x123);
+ x125 = (x14 + x124);
+ x126 = (x13 + x125);
+ x127 = (x126 & UINT64_C(0x7ffffffffffff));
+ x128 = (uint8_t)(x126 >> 51);
+ x129 = (x12 + (uint64_t)x128);
+ x130 = (x11 + x129);
+ x131 = (x10 + x130);
+ x132 = (x9 + x131);
+ x133 = (x8 + x132);
+ x134 = (x7 + x133);
+ x135 = (x134 & UINT64_C(0x7ffffffffffff));
+ x136 = (uint8_t)(x134 >> 51);
+ x137 = (x6 + (uint64_t)x136);
+ x138 = (x5 + x137);
+ x139 = (x4 + x138);
+ x140 = (x3 + x139);
+ x141 = (x2 + x140);
+ x142 = (x1 + x141);
+ out1[0] = x71;
out1[1] = x79;
- out1[2] = x82;
- out1[3] = x85;
- out1[4] = x87;
- out1[5] = x89;
- out1[6] = x92;
- out1[7] = x95;
- out1[8] = x98;
- out1[9] = x99;
+ out1[2] = x88;
+ out1[3] = x96;
+ out1[4] = x103;
+ out1[5] = x110;
+ out1[6] = x118;
+ out1[7] = x127;
+ out1[8] = x135;
+ out1[9] = x142;
}
/* END verbatim fiat code */
* {\pm 1, \pm 3, \pm 5, \pm 7, \pm 9, ...}
* i.e. signed odd digits with _no zeroes_ -- that makes it "regular".
*/
-static void scalar_rwnaf(char out[103], const unsigned char in[64]) {
+static void scalar_rwnaf(int8_t out[103], const unsigned char in[64]) {
int i;
- char window, d;
+ int8_t window, d;
window = (in[0] & (DRADIX_WNAF - 1)) | 1;
for (i = 0; i < 102; i++) {
* Compute "textbook" wnaf representation of a scalar.
* NB: not constant time
*/
-static void scalar_wnaf(char out[513], const unsigned char in[64]) {
+static void scalar_wnaf(int8_t out[513], const unsigned char in[64]) {
int i;
- char window, d;
+ int8_t window, d;
window = in[0] & (DRADIX_WNAF - 1);
for (i = 0; i < 513; i++) {
}
/*-
- * Simulateous scalar multiplication: interleaved "textbook" wnaf.
+ * Simultaneous scalar multiplication: interleaved "textbook" wnaf.
* NB: not constant time
*/
static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[64],
const unsigned char b[64], const pt_aff_t *P) {
int i, d, is_neg, is_inf = 1, flipped = 0;
- char anaf[513] = {0};
- char bnaf[513] = {0};
- pt_prj_t Q;
+ int8_t anaf[513] = {0};
+ int8_t bnaf[513] = {0};
+ pt_prj_t Q = {0};
pt_prj_t precomp[DRADIX / 2];
precomp_wnaf(precomp, P);
static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[64],
const pt_aff_t *P) {
int i, j, d, diff, is_neg;
- char rnaf[103] = {0};
- pt_prj_t Q, lut;
+ int8_t rnaf[103] = {0};
+ pt_prj_t Q = {0}, lut = {0};
pt_prj_t precomp[DRADIX / 2];
precomp_wnaf(precomp, P);
*/
static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[64]) {
int i, j, k, d, diff, is_neg = 0;
- char rnaf[103] = {0};
- pt_prj_t Q, R;
- pt_aff_t lut;
+ int8_t rnaf[103] = {0};
+ pt_prj_t Q = {0}, R = {0};
+ pt_aff_t lut = {0};
scalar_rwnaf(rnaf, scalar);
fiat_id_tc26_gost_3410_2012_512_paramSetA_carry_mul(out->Y, Q.Y, Q.Z);
}
+/*-
+ * Wrapper: simultaneous scalar mutiplication.
+ * outx, outy := a * G + b * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
static void point_mul_two(unsigned char outx[64], unsigned char outy[64],
const unsigned char a[64], const unsigned char b[64],
const unsigned char inx[64],
fiat_id_tc26_gost_3410_2012_512_paramSetA_to_bytes(outy, P.Y);
}
+/*-
+ * Wrapper: fixed scalar mutiplication.
+ * outx, outy := scalar * G
+ * Everything is LE byte ordering.
+ */
static void point_mul_g(unsigned char outx[64], unsigned char outy[64],
const unsigned char scalar[64]) {
pt_aff_t P;
fiat_id_tc26_gost_3410_2012_512_paramSetA_to_bytes(outy, P.Y);
}
+/*-
+ * Wrapper: variable point scalar mutiplication.
+ * outx, outy := scalar * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
static void point_mul(unsigned char outx[64], unsigned char outy[64],
const unsigned char scalar[64],
const unsigned char inx[64],
fiat_id_tc26_gost_3410_2012_512_paramSetA_to_bytes(outy, P.Y);
}
+
#include <openssl/ec.h>
+/* the zero field element */
static const unsigned char const_zb[64] = {0};
+/*-
+ * An OpenSSL wrapper for simultaneous scalar multiplication.
+ * r := n * G + m * q
+ */
int
point_mul_two_id_tc26_gost_3410_2012_512_paramSetA(
const EC_GROUP *group, EC_POINT *r, const BIGNUM *n, const EC_POINT *q,
return ret;
}
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
int
point_mul_id_tc26_gost_3410_2012_512_paramSetA(const EC_GROUP *group,
EC_POINT *r,
return ret;
}
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
int
point_mul_g_id_tc26_gost_3410_2012_512_paramSetA(const EC_GROUP *group,
EC_POINT *r,
typedef uint32_t fe_t[LIMB_CNT];
typedef uint32_t limb_t;
+#ifdef OPENSSL_NO_ASM
+#define FIAT_ID_TC26_GOST_3410_2012_512_PARAMSETA_NO_ASM
+#endif
+
#define fe_copy(d, s) memcpy(d, s, sizeof(fe_t))
#define fe_set_zero(d) memset(d, 0, sizeof(fe_t))
* SOFTWARE.
*/
-/* Autogenerated: unsaturated_solinas --static id_tc26_gost_3410_2012_512_paramSetA 32 '(auto)' '2^512 - 569' */
+/* Autogenerated: unsaturated_solinas --static --use-value-barrier id_tc26_gost_3410_2012_512_paramSetA 32 '(auto)' '2^512 - 569' */
/* curve description: id_tc26_gost_3410_2012_512_paramSetA */
/* machine_wordsize = 32 (from "32") */
/* requested operations: (all) */
/* n = 23 (from "(auto)") */
/* s-c = 2^512 - [(1, 569)] (from "2^512 - 569") */
-/* tight_bounds_multiplier = 1.1 (from "") */
+/* tight_bounds_multiplier = 1 (from "") */
/* */
/* Computed values: */
/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 0, 1] */
/* eval z = z[0] + (z[1] << 23) + (z[2] << 45) + (z[3] << 67) + (z[4] << 90) + (z[5] << 112) + (z[6] << 134) + (z[7] << 156) + (z[8] << 179) + (z[9] << 201) + (z[10] << 223) + (z[11] << 245) + (z[12] << 0x10c) + (z[13] << 0x122) + (z[14] << 0x138) + (z[15] << 0x14e) + (z[16] << 0x165) + (z[17] << 0x17b) + (z[18] << 0x191) + (z[19] << 0x1a7) + (z[20] << 0x1be) + (z[21] << 0x1d4) + (z[22] << 0x1ea) */
/* bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) */
+/* balance = [0xfffb8e, 0x7ffffe, 0x7ffffe, 0xfffffe, 0x7ffffe, 0x7ffffe, 0x7ffffe, 0xfffffe, 0x7ffffe, 0x7ffffe, 0x7ffffe, 0xfffffe, 0x7ffffe, 0x7ffffe, 0x7ffffe, 0xfffffe, 0x7ffffe, 0x7ffffe, 0x7ffffe, 0xfffffe, 0x7ffffe, 0x7ffffe, 0x7ffffe] */
#include <stdint.h>
typedef unsigned char fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1;
#error "This code only works on a two's complement system"
#endif
+#if !defined(FIAT_ID_TC26_GOST_3410_2012_512_PARAMSETA_NO_ASM) && \
+ (defined(__GNUC__) || defined(__clang__))
+static __inline__ uint32_t
+fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u32(uint32_t a) {
+ __asm__("" : "+r"(a) : /* no inputs */);
+ return a;
+}
+#else
+#define fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u32(x) (x)
+#endif
+
/*
* The function fiat_id_tc26_gost_3410_2012_512_paramSetA_addcarryx_u22 is an addition with carry.
* Postconditions:
x1 = (!(!arg1));
x2 = ((fiat_id_tc26_gost_3410_2012_512_paramSetA_int1)(0x0 - x1) &
UINT32_C(0xffffffff));
- x3 = ((x2 & arg3) | ((~x2) & arg2));
+ x3 = ((fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u32(x2) &
+ arg3) |
+ (fiat_id_tc26_gost_3410_2012_512_paramSetA_value_barrier_u32((~x2)) &
+ arg2));
*out1 = x3;
}
* eval out1 mod m = (eval arg1 * eval arg2) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
- * arg2: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
+ * arg1: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
+ * arg2: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * out1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_carry_mul(
uint32_t out1[23], const uint32_t arg1[23], const uint32_t arg2[23]) {
* eval out1 mod m = (eval arg1 * eval arg1) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
+ * arg1: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * out1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_carry_square(
uint32_t out1[23], const uint32_t arg1[23]) {
* eval out1 mod m = eval arg1 mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
+ * arg1: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * out1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_carry(
uint32_t out1[23], const uint32_t arg1[23]) {
* eval out1 mod m = (eval arg1 + eval arg2) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
- * arg2: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * arg1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
+ * arg2: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
+ * out1: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_add(
uint32_t out1[23], const uint32_t arg1[23], const uint32_t arg2[23]) {
* eval out1 mod m = (eval arg1 - eval arg2) mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
- * arg2: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * arg1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
+ * arg2: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
+ * out1: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_sub(
uint32_t out1[23], const uint32_t arg1[23], const uint32_t arg2[23]) {
* eval out1 mod m = -eval arg1 mod m
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * arg1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
* Output Bounds:
- * out1: [[0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0x1a66664], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332], [0x0 ~> 0xd33332]]
+ * out1: [[0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0x1800000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000], [0x0 ~> 0xc00000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_opp(
uint32_t out1[23], const uint32_t arg1[23]) {
* out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..63]
*
* Input Bounds:
- * arg1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * arg1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
* Output Bounds:
* out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
*/
uint32_t x111;
uint32_t x112;
uint32_t x113;
- uint32_t x114;
- uint8_t x115;
+ uint8_t x114;
+ uint32_t x115;
uint8_t x116;
uint8_t x117;
uint32_t x118;
- uint32_t x119;
- uint8_t x120;
- uint32_t x121;
- uint8_t x122;
+ uint8_t x119;
+ uint32_t x120;
+ uint8_t x121;
+ uint32_t x122;
uint8_t x123;
uint8_t x124;
uint32_t x125;
- uint32_t x126;
- uint8_t x127;
- uint32_t x128;
- uint8_t x129;
+ uint8_t x126;
+ uint32_t x127;
+ uint8_t x128;
+ uint32_t x129;
uint8_t x130;
uint8_t x131;
uint32_t x132;
- uint32_t x133;
- uint8_t x134;
- uint32_t x135;
- uint8_t x136;
+ uint8_t x133;
+ uint32_t x134;
+ uint8_t x135;
+ uint32_t x136;
uint8_t x137;
uint8_t x138;
uint32_t x139;
- uint32_t x140;
- uint8_t x141;
+ uint8_t x140;
+ uint32_t x141;
uint8_t x142;
uint8_t x143;
uint8_t x144;
uint32_t x145;
uint8_t x146;
uint8_t x147;
- uint8_t x148;
- uint32_t x149;
+ uint32_t x148;
+ uint8_t x149;
uint32_t x150;
uint8_t x151;
uint32_t x152;
uint8_t x153;
uint8_t x154;
- uint8_t x155;
- uint32_t x156;
+ uint32_t x155;
+ uint8_t x156;
uint32_t x157;
uint8_t x158;
uint32_t x159;
uint8_t x160;
uint8_t x161;
- uint8_t x162;
- uint32_t x163;
+ uint32_t x162;
+ uint8_t x163;
uint32_t x164;
uint8_t x165;
uint32_t x166;
uint8_t x167;
fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x168;
- uint8_t x169;
- uint32_t x170;
+ uint32_t x169;
+ uint8_t x170;
uint32_t x171;
uint8_t x172;
uint8_t x173;
- uint8_t x174;
- uint32_t x175;
+ uint32_t x174;
+ uint8_t x175;
uint32_t x176;
uint8_t x177;
uint32_t x178;
uint8_t x179;
uint8_t x180;
- uint8_t x181;
- uint32_t x182;
+ uint32_t x181;
+ uint8_t x182;
uint32_t x183;
uint8_t x184;
uint32_t x185;
uint8_t x186;
uint8_t x187;
- uint8_t x188;
- uint32_t x189;
+ uint32_t x188;
+ uint8_t x189;
uint32_t x190;
uint8_t x191;
uint32_t x192;
uint8_t x193;
uint8_t x194;
- uint8_t x195;
- uint32_t x196;
+ uint32_t x195;
+ uint8_t x196;
uint32_t x197;
uint8_t x198;
uint8_t x199;
uint8_t x200;
- uint8_t x201;
- uint32_t x202;
+ uint32_t x201;
+ uint8_t x202;
uint8_t x203;
- uint8_t x204;
+ uint32_t x204;
uint8_t x205;
uint32_t x206;
- uint32_t x207;
- uint8_t x208;
- uint32_t x209;
+ uint8_t x207;
+ uint32_t x208;
+ uint8_t x209;
uint8_t x210;
- uint8_t x211;
+ uint32_t x211;
uint8_t x212;
uint32_t x213;
- uint32_t x214;
- uint8_t x215;
- uint32_t x216;
+ uint8_t x214;
+ uint32_t x215;
+ uint8_t x216;
uint8_t x217;
- uint8_t x218;
+ uint32_t x218;
uint8_t x219;
uint32_t x220;
- uint32_t x221;
- uint8_t x222;
- uint32_t x223;
- uint8_t x224;
- fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x225;
+ uint8_t x221;
+ uint32_t x222;
+ uint8_t x223;
+ fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x224;
+ uint32_t x225;
uint8_t x226;
uint32_t x227;
- uint32_t x228;
+ uint8_t x228;
uint8_t x229;
- uint8_t x230;
+ uint32_t x230;
uint8_t x231;
uint32_t x232;
- uint32_t x233;
- uint8_t x234;
- uint32_t x235;
+ uint8_t x233;
+ uint32_t x234;
+ uint8_t x235;
uint8_t x236;
- uint8_t x237;
+ uint32_t x237;
uint8_t x238;
uint32_t x239;
- uint32_t x240;
- uint8_t x241;
- uint32_t x242;
+ uint8_t x240;
+ uint32_t x241;
+ uint8_t x242;
uint8_t x243;
- uint8_t x244;
+ uint32_t x244;
uint8_t x245;
uint32_t x246;
- uint32_t x247;
- uint8_t x248;
- uint32_t x249;
+ uint8_t x247;
+ uint32_t x248;
+ uint8_t x249;
uint8_t x250;
- uint8_t x251;
+ uint32_t x251;
uint8_t x252;
uint32_t x253;
- uint32_t x254;
+ uint8_t x254;
uint8_t x255;
- uint8_t x256;
- uint8_t x257;
fiat_id_tc26_gost_3410_2012_512_paramSetA_subborrowx_u23(
&x1, &x2, 0x0, (arg1[0]), UINT32_C(0x7ffdc7));
fiat_id_tc26_gost_3410_2012_512_paramSetA_subborrowx_u22(
x111 = (x54 << 3);
x112 = (x52 << 5);
x113 = (x50 << 7);
- x114 = (x48 >> 8);
- x115 = (uint8_t)(x48 & UINT8_C(0xff));
- x116 = (uint8_t)(x114 >> 8);
- x117 = (uint8_t)(x114 & UINT8_C(0xff));
- x118 = (x116 + x113);
- x119 = (x118 >> 8);
- x120 = (uint8_t)(x118 & UINT8_C(0xff));
- x121 = (x119 >> 8);
- x122 = (uint8_t)(x119 & UINT8_C(0xff));
- x123 = (uint8_t)(x121 >> 8);
- x124 = (uint8_t)(x121 & UINT8_C(0xff));
- x125 = (x123 + x112);
- x126 = (x125 >> 8);
- x127 = (uint8_t)(x125 & UINT8_C(0xff));
- x128 = (x126 >> 8);
- x129 = (uint8_t)(x126 & UINT8_C(0xff));
- x130 = (uint8_t)(x128 >> 8);
- x131 = (uint8_t)(x128 & UINT8_C(0xff));
- x132 = (x130 + x111);
- x133 = (x132 >> 8);
- x134 = (uint8_t)(x132 & UINT8_C(0xff));
- x135 = (x133 >> 8);
- x136 = (uint8_t)(x133 & UINT8_C(0xff));
- x137 = (uint8_t)(x135 >> 8);
- x138 = (uint8_t)(x135 & UINT8_C(0xff));
- x139 = (x137 + x110);
- x140 = (x139 >> 8);
- x141 = (uint8_t)(x139 & UINT8_C(0xff));
- x142 = (uint8_t)(x140 >> 8);
- x143 = (uint8_t)(x140 & UINT8_C(0xff));
- x144 = (uint8_t)(x142 & UINT8_C(0xff));
+ x114 = (uint8_t)(x48 & UINT8_C(0xff));
+ x115 = (x48 >> 8);
+ x116 = (uint8_t)(x115 & UINT8_C(0xff));
+ x117 = (uint8_t)(x115 >> 8);
+ x118 = (x113 + (uint32_t)x117);
+ x119 = (uint8_t)(x118 & UINT8_C(0xff));
+ x120 = (x118 >> 8);
+ x121 = (uint8_t)(x120 & UINT8_C(0xff));
+ x122 = (x120 >> 8);
+ x123 = (uint8_t)(x122 & UINT8_C(0xff));
+ x124 = (uint8_t)(x122 >> 8);
+ x125 = (x112 + (uint32_t)x124);
+ x126 = (uint8_t)(x125 & UINT8_C(0xff));
+ x127 = (x125 >> 8);
+ x128 = (uint8_t)(x127 & UINT8_C(0xff));
+ x129 = (x127 >> 8);
+ x130 = (uint8_t)(x129 & UINT8_C(0xff));
+ x131 = (uint8_t)(x129 >> 8);
+ x132 = (x111 + (uint32_t)x131);
+ x133 = (uint8_t)(x132 & UINT8_C(0xff));
+ x134 = (x132 >> 8);
+ x135 = (uint8_t)(x134 & UINT8_C(0xff));
+ x136 = (x134 >> 8);
+ x137 = (uint8_t)(x136 & UINT8_C(0xff));
+ x138 = (uint8_t)(x136 >> 8);
+ x139 = (x110 + (uint32_t)x138);
+ x140 = (uint8_t)(x139 & UINT8_C(0xff));
+ x141 = (x139 >> 8);
+ x142 = (uint8_t)(x141 & UINT8_C(0xff));
+ x143 = (uint8_t)(x141 >> 8);
+ x144 = (uint8_t)(x58 & UINT8_C(0xff));
x145 = (x58 >> 8);
- x146 = (uint8_t)(x58 & UINT8_C(0xff));
+ x146 = (uint8_t)(x145 & UINT8_C(0xff));
x147 = (uint8_t)(x145 >> 8);
- x148 = (uint8_t)(x145 & UINT8_C(0xff));
- x149 = (x147 + x109);
- x150 = (x149 >> 8);
- x151 = (uint8_t)(x149 & UINT8_C(0xff));
+ x148 = (x109 + (uint32_t)x147);
+ x149 = (uint8_t)(x148 & UINT8_C(0xff));
+ x150 = (x148 >> 8);
+ x151 = (uint8_t)(x150 & UINT8_C(0xff));
x152 = (x150 >> 8);
- x153 = (uint8_t)(x150 & UINT8_C(0xff));
+ x153 = (uint8_t)(x152 & UINT8_C(0xff));
x154 = (uint8_t)(x152 >> 8);
- x155 = (uint8_t)(x152 & UINT8_C(0xff));
- x156 = (x154 + x108);
- x157 = (x156 >> 8);
- x158 = (uint8_t)(x156 & UINT8_C(0xff));
+ x155 = (x108 + (uint32_t)x154);
+ x156 = (uint8_t)(x155 & UINT8_C(0xff));
+ x157 = (x155 >> 8);
+ x158 = (uint8_t)(x157 & UINT8_C(0xff));
x159 = (x157 >> 8);
- x160 = (uint8_t)(x157 & UINT8_C(0xff));
+ x160 = (uint8_t)(x159 & UINT8_C(0xff));
x161 = (uint8_t)(x159 >> 8);
- x162 = (uint8_t)(x159 & UINT8_C(0xff));
- x163 = (x161 + x107);
- x164 = (x163 >> 8);
- x165 = (uint8_t)(x163 & UINT8_C(0xff));
+ x162 = (x107 + (uint32_t)x161);
+ x163 = (uint8_t)(x162 & UINT8_C(0xff));
+ x164 = (x162 >> 8);
+ x165 = (uint8_t)(x164 & UINT8_C(0xff));
x166 = (x164 >> 8);
- x167 = (uint8_t)(x164 & UINT8_C(0xff));
+ x167 = (uint8_t)(x166 & UINT8_C(0xff));
x168 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x166 >> 8);
- x169 = (uint8_t)(x166 & UINT8_C(0xff));
- x170 = (x168 + x106);
- x171 = (x170 >> 8);
- x172 = (uint8_t)(x170 & UINT8_C(0xff));
+ x169 = (x106 + (uint32_t)x168);
+ x170 = (uint8_t)(x169 & UINT8_C(0xff));
+ x171 = (x169 >> 8);
+ x172 = (uint8_t)(x171 & UINT8_C(0xff));
x173 = (uint8_t)(x171 >> 8);
- x174 = (uint8_t)(x171 & UINT8_C(0xff));
- x175 = (x173 + x105);
- x176 = (x175 >> 8);
- x177 = (uint8_t)(x175 & UINT8_C(0xff));
+ x174 = (x105 + (uint32_t)x173);
+ x175 = (uint8_t)(x174 & UINT8_C(0xff));
+ x176 = (x174 >> 8);
+ x177 = (uint8_t)(x176 & UINT8_C(0xff));
x178 = (x176 >> 8);
- x179 = (uint8_t)(x176 & UINT8_C(0xff));
+ x179 = (uint8_t)(x178 & UINT8_C(0xff));
x180 = (uint8_t)(x178 >> 8);
- x181 = (uint8_t)(x178 & UINT8_C(0xff));
- x182 = (x180 + x104);
- x183 = (x182 >> 8);
- x184 = (uint8_t)(x182 & UINT8_C(0xff));
+ x181 = (x104 + (uint32_t)x180);
+ x182 = (uint8_t)(x181 & UINT8_C(0xff));
+ x183 = (x181 >> 8);
+ x184 = (uint8_t)(x183 & UINT8_C(0xff));
x185 = (x183 >> 8);
- x186 = (uint8_t)(x183 & UINT8_C(0xff));
+ x186 = (uint8_t)(x185 & UINT8_C(0xff));
x187 = (uint8_t)(x185 >> 8);
- x188 = (uint8_t)(x185 & UINT8_C(0xff));
- x189 = (x187 + x103);
- x190 = (x189 >> 8);
- x191 = (uint8_t)(x189 & UINT8_C(0xff));
+ x188 = (x103 + (uint32_t)x187);
+ x189 = (uint8_t)(x188 & UINT8_C(0xff));
+ x190 = (x188 >> 8);
+ x191 = (uint8_t)(x190 & UINT8_C(0xff));
x192 = (x190 >> 8);
- x193 = (uint8_t)(x190 & UINT8_C(0xff));
+ x193 = (uint8_t)(x192 & UINT8_C(0xff));
x194 = (uint8_t)(x192 >> 8);
- x195 = (uint8_t)(x192 & UINT8_C(0xff));
- x196 = (x194 + x102);
- x197 = (x196 >> 8);
- x198 = (uint8_t)(x196 & UINT8_C(0xff));
+ x195 = (x102 + (uint32_t)x194);
+ x196 = (uint8_t)(x195 & UINT8_C(0xff));
+ x197 = (x195 >> 8);
+ x198 = (uint8_t)(x197 & UINT8_C(0xff));
x199 = (uint8_t)(x197 >> 8);
- x200 = (uint8_t)(x197 & UINT8_C(0xff));
- x201 = (uint8_t)(x199 & UINT8_C(0xff));
- x202 = (x76 >> 8);
- x203 = (uint8_t)(x76 & UINT8_C(0xff));
- x204 = (uint8_t)(x202 >> 8);
- x205 = (uint8_t)(x202 & UINT8_C(0xff));
- x206 = (x204 + x101);
- x207 = (x206 >> 8);
- x208 = (uint8_t)(x206 & UINT8_C(0xff));
- x209 = (x207 >> 8);
- x210 = (uint8_t)(x207 & UINT8_C(0xff));
- x211 = (uint8_t)(x209 >> 8);
- x212 = (uint8_t)(x209 & UINT8_C(0xff));
- x213 = (x211 + x100);
- x214 = (x213 >> 8);
- x215 = (uint8_t)(x213 & UINT8_C(0xff));
- x216 = (x214 >> 8);
- x217 = (uint8_t)(x214 & UINT8_C(0xff));
- x218 = (uint8_t)(x216 >> 8);
- x219 = (uint8_t)(x216 & UINT8_C(0xff));
- x220 = (x218 + x99);
- x221 = (x220 >> 8);
- x222 = (uint8_t)(x220 & UINT8_C(0xff));
- x223 = (x221 >> 8);
- x224 = (uint8_t)(x221 & UINT8_C(0xff));
- x225 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x223 >> 8);
- x226 = (uint8_t)(x223 & UINT8_C(0xff));
- x227 = (x225 + x98);
- x228 = (x227 >> 8);
- x229 = (uint8_t)(x227 & UINT8_C(0xff));
- x230 = (uint8_t)(x228 >> 8);
- x231 = (uint8_t)(x228 & UINT8_C(0xff));
- x232 = (x230 + x97);
- x233 = (x232 >> 8);
- x234 = (uint8_t)(x232 & UINT8_C(0xff));
- x235 = (x233 >> 8);
- x236 = (uint8_t)(x233 & UINT8_C(0xff));
- x237 = (uint8_t)(x235 >> 8);
- x238 = (uint8_t)(x235 & UINT8_C(0xff));
- x239 = (x237 + x96);
- x240 = (x239 >> 8);
- x241 = (uint8_t)(x239 & UINT8_C(0xff));
- x242 = (x240 >> 8);
- x243 = (uint8_t)(x240 & UINT8_C(0xff));
- x244 = (uint8_t)(x242 >> 8);
- x245 = (uint8_t)(x242 & UINT8_C(0xff));
- x246 = (x244 + x95);
- x247 = (x246 >> 8);
- x248 = (uint8_t)(x246 & UINT8_C(0xff));
- x249 = (x247 >> 8);
- x250 = (uint8_t)(x247 & UINT8_C(0xff));
- x251 = (uint8_t)(x249 >> 8);
- x252 = (uint8_t)(x249 & UINT8_C(0xff));
- x253 = (x251 + x94);
- x254 = (x253 >> 8);
- x255 = (uint8_t)(x253 & UINT8_C(0xff));
- x256 = (uint8_t)(x254 >> 8);
- x257 = (uint8_t)(x254 & UINT8_C(0xff));
- out1[0] = x115;
- out1[1] = x117;
- out1[2] = x120;
- out1[3] = x122;
- out1[4] = x124;
- out1[5] = x127;
- out1[6] = x129;
- out1[7] = x131;
- out1[8] = x134;
- out1[9] = x136;
- out1[10] = x138;
- out1[11] = x141;
- out1[12] = x143;
- out1[13] = x144;
- out1[14] = x146;
- out1[15] = x148;
- out1[16] = x151;
- out1[17] = x153;
- out1[18] = x155;
- out1[19] = x158;
- out1[20] = x160;
- out1[21] = x162;
- out1[22] = x165;
- out1[23] = x167;
- out1[24] = x169;
- out1[25] = x172;
- out1[26] = x174;
- out1[27] = x177;
- out1[28] = x179;
- out1[29] = x181;
- out1[30] = x184;
- out1[31] = x186;
- out1[32] = x188;
- out1[33] = x191;
- out1[34] = x193;
- out1[35] = x195;
- out1[36] = x198;
- out1[37] = x200;
- out1[38] = x201;
- out1[39] = x203;
- out1[40] = x205;
- out1[41] = x208;
- out1[42] = x210;
- out1[43] = x212;
- out1[44] = x215;
- out1[45] = x217;
- out1[46] = x219;
- out1[47] = x222;
- out1[48] = x224;
- out1[49] = x226;
- out1[50] = x229;
- out1[51] = x231;
- out1[52] = x234;
- out1[53] = x236;
- out1[54] = x238;
- out1[55] = x241;
- out1[56] = x243;
- out1[57] = x245;
- out1[58] = x248;
- out1[59] = x250;
- out1[60] = x252;
- out1[61] = x255;
- out1[62] = x257;
- out1[63] = x256;
+ x200 = (uint8_t)(x76 & UINT8_C(0xff));
+ x201 = (x76 >> 8);
+ x202 = (uint8_t)(x201 & UINT8_C(0xff));
+ x203 = (uint8_t)(x201 >> 8);
+ x204 = (x101 + (uint32_t)x203);
+ x205 = (uint8_t)(x204 & UINT8_C(0xff));
+ x206 = (x204 >> 8);
+ x207 = (uint8_t)(x206 & UINT8_C(0xff));
+ x208 = (x206 >> 8);
+ x209 = (uint8_t)(x208 & UINT8_C(0xff));
+ x210 = (uint8_t)(x208 >> 8);
+ x211 = (x100 + (uint32_t)x210);
+ x212 = (uint8_t)(x211 & UINT8_C(0xff));
+ x213 = (x211 >> 8);
+ x214 = (uint8_t)(x213 & UINT8_C(0xff));
+ x215 = (x213 >> 8);
+ x216 = (uint8_t)(x215 & UINT8_C(0xff));
+ x217 = (uint8_t)(x215 >> 8);
+ x218 = (x99 + (uint32_t)x217);
+ x219 = (uint8_t)(x218 & UINT8_C(0xff));
+ x220 = (x218 >> 8);
+ x221 = (uint8_t)(x220 & UINT8_C(0xff));
+ x222 = (x220 >> 8);
+ x223 = (uint8_t)(x222 & UINT8_C(0xff));
+ x224 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x222 >> 8);
+ x225 = (x98 + (uint32_t)x224);
+ x226 = (uint8_t)(x225 & UINT8_C(0xff));
+ x227 = (x225 >> 8);
+ x228 = (uint8_t)(x227 & UINT8_C(0xff));
+ x229 = (uint8_t)(x227 >> 8);
+ x230 = (x97 + (uint32_t)x229);
+ x231 = (uint8_t)(x230 & UINT8_C(0xff));
+ x232 = (x230 >> 8);
+ x233 = (uint8_t)(x232 & UINT8_C(0xff));
+ x234 = (x232 >> 8);
+ x235 = (uint8_t)(x234 & UINT8_C(0xff));
+ x236 = (uint8_t)(x234 >> 8);
+ x237 = (x96 + (uint32_t)x236);
+ x238 = (uint8_t)(x237 & UINT8_C(0xff));
+ x239 = (x237 >> 8);
+ x240 = (uint8_t)(x239 & UINT8_C(0xff));
+ x241 = (x239 >> 8);
+ x242 = (uint8_t)(x241 & UINT8_C(0xff));
+ x243 = (uint8_t)(x241 >> 8);
+ x244 = (x95 + (uint32_t)x243);
+ x245 = (uint8_t)(x244 & UINT8_C(0xff));
+ x246 = (x244 >> 8);
+ x247 = (uint8_t)(x246 & UINT8_C(0xff));
+ x248 = (x246 >> 8);
+ x249 = (uint8_t)(x248 & UINT8_C(0xff));
+ x250 = (uint8_t)(x248 >> 8);
+ x251 = (x94 + (uint32_t)x250);
+ x252 = (uint8_t)(x251 & UINT8_C(0xff));
+ x253 = (x251 >> 8);
+ x254 = (uint8_t)(x253 & UINT8_C(0xff));
+ x255 = (uint8_t)(x253 >> 8);
+ out1[0] = x114;
+ out1[1] = x116;
+ out1[2] = x119;
+ out1[3] = x121;
+ out1[4] = x123;
+ out1[5] = x126;
+ out1[6] = x128;
+ out1[7] = x130;
+ out1[8] = x133;
+ out1[9] = x135;
+ out1[10] = x137;
+ out1[11] = x140;
+ out1[12] = x142;
+ out1[13] = x143;
+ out1[14] = x144;
+ out1[15] = x146;
+ out1[16] = x149;
+ out1[17] = x151;
+ out1[18] = x153;
+ out1[19] = x156;
+ out1[20] = x158;
+ out1[21] = x160;
+ out1[22] = x163;
+ out1[23] = x165;
+ out1[24] = x167;
+ out1[25] = x170;
+ out1[26] = x172;
+ out1[27] = x175;
+ out1[28] = x177;
+ out1[29] = x179;
+ out1[30] = x182;
+ out1[31] = x184;
+ out1[32] = x186;
+ out1[33] = x189;
+ out1[34] = x191;
+ out1[35] = x193;
+ out1[36] = x196;
+ out1[37] = x198;
+ out1[38] = x199;
+ out1[39] = x200;
+ out1[40] = x202;
+ out1[41] = x205;
+ out1[42] = x207;
+ out1[43] = x209;
+ out1[44] = x212;
+ out1[45] = x214;
+ out1[46] = x216;
+ out1[47] = x219;
+ out1[48] = x221;
+ out1[49] = x223;
+ out1[50] = x226;
+ out1[51] = x228;
+ out1[52] = x231;
+ out1[53] = x233;
+ out1[54] = x235;
+ out1[55] = x238;
+ out1[56] = x240;
+ out1[57] = x242;
+ out1[58] = x245;
+ out1[59] = x247;
+ out1[60] = x249;
+ out1[61] = x252;
+ out1[62] = x254;
+ out1[63] = x255;
}
/*
* Input Bounds:
* arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
* Output Bounds:
- * out1: [[0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x8ccccc], [0x0 ~> 0x466666], [0x0 ~> 0x466666], [0x0 ~> 0x466666]]
+ * out1: [[0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x800000], [0x0 ~> 0x400000], [0x0 ~> 0x400000], [0x0 ~> 0x400000]]
*/
static void fiat_id_tc26_gost_3410_2012_512_paramSetA_from_bytes(
uint32_t out1[23], const uint8_t arg1[64]) {
uint32_t x63;
uint8_t x64;
uint32_t x65;
- fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x66;
+ uint32_t x66;
uint32_t x67;
- uint32_t x68;
+ fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x68;
uint32_t x69;
uint32_t x70;
uint32_t x71;
uint32_t x72;
- uint32_t x73;
+ uint8_t x73;
uint32_t x74;
uint32_t x75;
uint32_t x76;
uint32_t x77;
- uint32_t x78;
+ uint8_t x78;
uint32_t x79;
uint32_t x80;
uint32_t x81;
uint32_t x82;
- uint32_t x83;
+ uint8_t x83;
uint32_t x84;
uint32_t x85;
uint32_t x86;
uint32_t x87;
uint32_t x88;
- uint32_t x89;
+ uint8_t x89;
uint32_t x90;
- uint8_t x91;
+ uint32_t x91;
uint32_t x92;
uint32_t x93;
uint8_t x94;
uint32_t x95;
uint32_t x96;
- uint8_t x97;
+ uint32_t x97;
uint32_t x98;
- uint32_t x99;
+ uint8_t x99;
uint32_t x100;
- uint8_t x101;
+ uint32_t x101;
uint32_t x102;
uint32_t x103;
uint8_t x104;
uint32_t x105;
uint32_t x106;
- uint8_t x107;
- uint32_t x108;
+ uint32_t x107;
+ fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x108;
uint32_t x109;
- uint8_t x110;
+ uint32_t x110;
uint32_t x111;
uint32_t x112;
- fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x113;
+ uint8_t x113;
uint32_t x114;
uint32_t x115;
- uint8_t x116;
+ uint32_t x116;
uint32_t x117;
- uint32_t x118;
- uint8_t x119;
+ uint8_t x118;
+ uint32_t x119;
uint32_t x120;
uint32_t x121;
- uint8_t x122;
- uint32_t x123;
+ uint32_t x122;
+ uint8_t x123;
uint32_t x124;
uint32_t x125;
- uint8_t x126;
+ uint32_t x126;
uint32_t x127;
uint32_t x128;
uint8_t x129;
uint32_t x130;
uint32_t x131;
- uint8_t x132;
+ uint32_t x132;
uint32_t x133;
- uint32_t x134;
- uint8_t x135;
+ uint8_t x134;
+ uint32_t x135;
uint32_t x136;
uint32_t x137;
- fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x138;
- uint32_t x139;
+ uint32_t x138;
+ uint8_t x139;
uint32_t x140;
- uint8_t x141;
+ uint32_t x141;
uint32_t x142;
uint32_t x143;
uint8_t x144;
uint32_t x145;
uint32_t x146;
- uint8_t x147;
- uint32_t x148;
+ uint32_t x147;
+ fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1 x148;
uint32_t x149;
+ uint32_t x150;
+ uint32_t x151;
+ uint32_t x152;
+ uint8_t x153;
+ uint32_t x154;
+ uint32_t x155;
+ uint32_t x156;
+ uint32_t x157;
+ uint8_t x158;
+ uint32_t x159;
+ uint32_t x160;
+ uint32_t x161;
+ uint32_t x162;
+ uint8_t x163;
+ uint32_t x164;
+ uint32_t x165;
x1 = ((uint32_t)(arg1[63]) << 14);
x2 = ((uint32_t)(arg1[62]) << 6);
x3 = ((uint32_t)(arg1[61]) << 20);
x62 = ((uint32_t)(arg1[2]) << 16);
x63 = ((uint32_t)(arg1[1]) << 8);
x64 = (arg1[0]);
- x65 = (x64 + (x63 + x62));
- x66 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x65 >> 23);
- x67 = (x65 & UINT32_C(0x7fffff));
- x68 = (x2 + x1);
- x69 = (x5 + (x4 + x3));
- x70 = (x8 + (x7 + x6));
- x71 = (x11 + (x10 + x9));
- x72 = (x13 + x12);
- x73 = (x16 + (x15 + x14));
- x74 = (x19 + (x18 + x17));
- x75 = (x22 + (x21 + x20));
- x76 = (x25 + (x24 + x23));
- x77 = (x27 + x26);
- x78 = (x30 + (x29 + x28));
- x79 = (x33 + (x32 + x31));
- x80 = (x36 + (x35 + x34));
- x81 = (x38 + x37);
- x82 = (x41 + (x40 + x39));
- x83 = (x44 + (x43 + x42));
- x84 = (x47 + (x46 + x45));
- x85 = (x50 + (x49 + x48));
- x86 = (x52 + x51);
- x87 = (x55 + (x54 + x53));
- x88 = (x58 + (x57 + x56));
- x89 = (x61 + (x60 + x59));
- x90 = (x66 + x89);
- x91 = (uint8_t)(x90 >> 22);
- x92 = (x90 & UINT32_C(0x3fffff));
- x93 = (x91 + x88);
- x94 = (uint8_t)(x93 >> 22);
- x95 = (x93 & UINT32_C(0x3fffff));
- x96 = (x94 + x87);
- x97 = (uint8_t)(x96 >> 23);
- x98 = (x96 & UINT32_C(0x7fffff));
- x99 = (x97 + x86);
- x100 = (x99 & UINT32_C(0x3fffff));
- x101 = (uint8_t)(x85 >> 22);
- x102 = (x85 & UINT32_C(0x3fffff));
- x103 = (x101 + x84);
- x104 = (uint8_t)(x103 >> 22);
- x105 = (x103 & UINT32_C(0x3fffff));
- x106 = (x104 + x83);
- x107 = (uint8_t)(x106 >> 23);
- x108 = (x106 & UINT32_C(0x7fffff));
- x109 = (x107 + x82);
- x110 = (uint8_t)(x109 >> 22);
- x111 = (x109 & UINT32_C(0x3fffff));
- x112 = (x110 + x81);
- x113 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x112 >> 22);
- x114 = (x112 & UINT32_C(0x3fffff));
- x115 = (x113 + x80);
- x116 = (uint8_t)(x115 >> 22);
- x117 = (x115 & UINT32_C(0x3fffff));
- x118 = (x116 + x79);
- x119 = (uint8_t)(x118 >> 23);
- x120 = (x118 & UINT32_C(0x7fffff));
- x121 = (x119 + x78);
- x122 = (uint8_t)(x121 >> 22);
- x123 = (x121 & UINT32_C(0x3fffff));
- x124 = (x122 + x77);
- x125 = (x124 & UINT32_C(0x3fffff));
- x126 = (uint8_t)(x76 >> 22);
- x127 = (x76 & UINT32_C(0x3fffff));
- x128 = (x126 + x75);
- x129 = (uint8_t)(x128 >> 23);
- x130 = (x128 & UINT32_C(0x7fffff));
- x131 = (x129 + x74);
- x132 = (uint8_t)(x131 >> 22);
- x133 = (x131 & UINT32_C(0x3fffff));
- x134 = (x132 + x73);
- x135 = (uint8_t)(x134 >> 22);
- x136 = (x134 & UINT32_C(0x3fffff));
- x137 = (x135 + x72);
- x138 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x137 >> 22);
- x139 = (x137 & UINT32_C(0x3fffff));
- x140 = (x138 + x71);
- x141 = (uint8_t)(x140 >> 23);
- x142 = (x140 & UINT32_C(0x7fffff));
- x143 = (x141 + x70);
- x144 = (uint8_t)(x143 >> 22);
- x145 = (x143 & UINT32_C(0x3fffff));
- x146 = (x144 + x69);
- x147 = (uint8_t)(x146 >> 22);
- x148 = (x146 & UINT32_C(0x3fffff));
- x149 = (x147 + x68);
+ x65 = (x63 + (uint32_t)x64);
+ x66 = (x62 + x65);
+ x67 = (x66 & UINT32_C(0x7fffff));
+ x68 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x66 >> 23);
+ x69 = (x61 + (uint32_t)x68);
+ x70 = (x60 + x69);
+ x71 = (x59 + x70);
+ x72 = (x71 & UINT32_C(0x3fffff));
+ x73 = (uint8_t)(x71 >> 22);
+ x74 = (x58 + (uint32_t)x73);
+ x75 = (x57 + x74);
+ x76 = (x56 + x75);
+ x77 = (x76 & UINT32_C(0x3fffff));
+ x78 = (uint8_t)(x76 >> 22);
+ x79 = (x55 + (uint32_t)x78);
+ x80 = (x54 + x79);
+ x81 = (x53 + x80);
+ x82 = (x81 & UINT32_C(0x7fffff));
+ x83 = (uint8_t)(x81 >> 23);
+ x84 = (x52 + (uint32_t)x83);
+ x85 = (x51 + x84);
+ x86 = (x49 + (uint32_t)x50);
+ x87 = (x48 + x86);
+ x88 = (x87 & UINT32_C(0x3fffff));
+ x89 = (uint8_t)(x87 >> 22);
+ x90 = (x47 + (uint32_t)x89);
+ x91 = (x46 + x90);
+ x92 = (x45 + x91);
+ x93 = (x92 & UINT32_C(0x3fffff));
+ x94 = (uint8_t)(x92 >> 22);
+ x95 = (x44 + (uint32_t)x94);
+ x96 = (x43 + x95);
+ x97 = (x42 + x96);
+ x98 = (x97 & UINT32_C(0x7fffff));
+ x99 = (uint8_t)(x97 >> 23);
+ x100 = (x41 + (uint32_t)x99);
+ x101 = (x40 + x100);
+ x102 = (x39 + x101);
+ x103 = (x102 & UINT32_C(0x3fffff));
+ x104 = (uint8_t)(x102 >> 22);
+ x105 = (x38 + (uint32_t)x104);
+ x106 = (x37 + x105);
+ x107 = (x106 & UINT32_C(0x3fffff));
+ x108 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x106 >> 22);
+ x109 = (x36 + (uint32_t)x108);
+ x110 = (x35 + x109);
+ x111 = (x34 + x110);
+ x112 = (x111 & UINT32_C(0x3fffff));
+ x113 = (uint8_t)(x111 >> 22);
+ x114 = (x33 + (uint32_t)x113);
+ x115 = (x32 + x114);
+ x116 = (x31 + x115);
+ x117 = (x116 & UINT32_C(0x7fffff));
+ x118 = (uint8_t)(x116 >> 23);
+ x119 = (x30 + (uint32_t)x118);
+ x120 = (x29 + x119);
+ x121 = (x28 + x120);
+ x122 = (x121 & UINT32_C(0x3fffff));
+ x123 = (uint8_t)(x121 >> 22);
+ x124 = (x27 + (uint32_t)x123);
+ x125 = (x26 + x124);
+ x126 = (x24 + (uint32_t)x25);
+ x127 = (x23 + x126);
+ x128 = (x127 & UINT32_C(0x3fffff));
+ x129 = (uint8_t)(x127 >> 22);
+ x130 = (x22 + (uint32_t)x129);
+ x131 = (x21 + x130);
+ x132 = (x20 + x131);
+ x133 = (x132 & UINT32_C(0x7fffff));
+ x134 = (uint8_t)(x132 >> 23);
+ x135 = (x19 + (uint32_t)x134);
+ x136 = (x18 + x135);
+ x137 = (x17 + x136);
+ x138 = (x137 & UINT32_C(0x3fffff));
+ x139 = (uint8_t)(x137 >> 22);
+ x140 = (x16 + (uint32_t)x139);
+ x141 = (x15 + x140);
+ x142 = (x14 + x141);
+ x143 = (x142 & UINT32_C(0x3fffff));
+ x144 = (uint8_t)(x142 >> 22);
+ x145 = (x13 + (uint32_t)x144);
+ x146 = (x12 + x145);
+ x147 = (x146 & UINT32_C(0x3fffff));
+ x148 = (fiat_id_tc26_gost_3410_2012_512_paramSetA_uint1)(x146 >> 22);
+ x149 = (x11 + (uint32_t)x148);
+ x150 = (x10 + x149);
+ x151 = (x9 + x150);
+ x152 = (x151 & UINT32_C(0x7fffff));
+ x153 = (uint8_t)(x151 >> 23);
+ x154 = (x8 + (uint32_t)x153);
+ x155 = (x7 + x154);
+ x156 = (x6 + x155);
+ x157 = (x156 & UINT32_C(0x3fffff));
+ x158 = (uint8_t)(x156 >> 22);
+ x159 = (x5 + (uint32_t)x158);
+ x160 = (x4 + x159);
+ x161 = (x3 + x160);
+ x162 = (x161 & UINT32_C(0x3fffff));
+ x163 = (uint8_t)(x161 >> 22);
+ x164 = (x2 + (uint32_t)x163);
+ x165 = (x1 + x164);
out1[0] = x67;
- out1[1] = x92;
- out1[2] = x95;
- out1[3] = x98;
- out1[4] = x100;
- out1[5] = x102;
- out1[6] = x105;
- out1[7] = x108;
- out1[8] = x111;
- out1[9] = x114;
- out1[10] = x117;
- out1[11] = x120;
- out1[12] = x123;
+ out1[1] = x72;
+ out1[2] = x77;
+ out1[3] = x82;
+ out1[4] = x85;
+ out1[5] = x88;
+ out1[6] = x93;
+ out1[7] = x98;
+ out1[8] = x103;
+ out1[9] = x107;
+ out1[10] = x112;
+ out1[11] = x117;
+ out1[12] = x122;
out1[13] = x125;
- out1[14] = x127;
- out1[15] = x130;
- out1[16] = x133;
- out1[17] = x136;
- out1[18] = x139;
- out1[19] = x142;
- out1[20] = x145;
- out1[21] = x148;
- out1[22] = x149;
+ out1[14] = x128;
+ out1[15] = x133;
+ out1[16] = x138;
+ out1[17] = x143;
+ out1[18] = x147;
+ out1[19] = x152;
+ out1[20] = x157;
+ out1[21] = x162;
+ out1[22] = x165;
}
/* END verbatim fiat code */
* {\pm 1, \pm 3, \pm 5, \pm 7, \pm 9, ...}
* i.e. signed odd digits with _no zeroes_ -- that makes it "regular".
*/
-static void scalar_rwnaf(char out[103], const unsigned char in[64]) {
+static void scalar_rwnaf(int8_t out[103], const unsigned char in[64]) {
int i;
- char window, d;
+ int8_t window, d;
window = (in[0] & (DRADIX_WNAF - 1)) | 1;
for (i = 0; i < 102; i++) {
* Compute "textbook" wnaf representation of a scalar.
* NB: not constant time
*/
-static void scalar_wnaf(char out[513], const unsigned char in[64]) {
+static void scalar_wnaf(int8_t out[513], const unsigned char in[64]) {
int i;
- char window, d;
+ int8_t window, d;
window = in[0] & (DRADIX_WNAF - 1);
for (i = 0; i < 513; i++) {
}
/*-
- * Simulateous scalar multiplication: interleaved "textbook" wnaf.
+ * Simultaneous scalar multiplication: interleaved "textbook" wnaf.
* NB: not constant time
*/
static void var_smul_wnaf_two(pt_aff_t *out, const unsigned char a[64],
const unsigned char b[64], const pt_aff_t *P) {
int i, d, is_neg, is_inf = 1, flipped = 0;
- char anaf[513] = {0};
- char bnaf[513] = {0};
- pt_prj_t Q;
+ int8_t anaf[513] = {0};
+ int8_t bnaf[513] = {0};
+ pt_prj_t Q = {0};
pt_prj_t precomp[DRADIX / 2];
precomp_wnaf(precomp, P);
static void var_smul_rwnaf(pt_aff_t *out, const unsigned char scalar[64],
const pt_aff_t *P) {
int i, j, d, diff, is_neg;
- char rnaf[103] = {0};
- pt_prj_t Q, lut;
+ int8_t rnaf[103] = {0};
+ pt_prj_t Q = {0}, lut = {0};
pt_prj_t precomp[DRADIX / 2];
precomp_wnaf(precomp, P);
*/
static void fixed_smul_cmb(pt_aff_t *out, const unsigned char scalar[64]) {
int i, j, k, d, diff, is_neg = 0;
- char rnaf[103] = {0};
- pt_prj_t Q, R;
- pt_aff_t lut;
+ int8_t rnaf[103] = {0};
+ pt_prj_t Q = {0}, R = {0};
+ pt_aff_t lut = {0};
scalar_rwnaf(rnaf, scalar);
fiat_id_tc26_gost_3410_2012_512_paramSetA_carry_mul(out->Y, Q.Y, Q.Z);
}
+/*-
+ * Wrapper: simultaneous scalar mutiplication.
+ * outx, outy := a * G + b * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
static void point_mul_two(unsigned char outx[64], unsigned char outy[64],
const unsigned char a[64], const unsigned char b[64],
const unsigned char inx[64],
fiat_id_tc26_gost_3410_2012_512_paramSetA_to_bytes(outy, P.Y);
}
+/*-
+ * Wrapper: fixed scalar mutiplication.
+ * outx, outy := scalar * G
+ * Everything is LE byte ordering.
+ */
static void point_mul_g(unsigned char outx[64], unsigned char outy[64],
const unsigned char scalar[64]) {
pt_aff_t P;
fiat_id_tc26_gost_3410_2012_512_paramSetA_to_bytes(outy, P.Y);
}
+/*-
+ * Wrapper: variable point scalar mutiplication.
+ * outx, outy := scalar * P
+ * where P = (inx, iny).
+ * Everything is LE byte ordering.
+ */
static void point_mul(unsigned char outx[64], unsigned char outy[64],
const unsigned char scalar[64],
const unsigned char inx[64],
fiat_id_tc26_gost_3410_2012_512_paramSetA_to_bytes(outy, P.Y);
}
+
#include <openssl/ec.h>
+/* the zero field element */
static const unsigned char const_zb[64] = {0};
+/*-
+ * An OpenSSL wrapper for simultaneous scalar multiplication.
+ * r := n * G + m * q
+ */
int
point_mul_two_id_tc26_gost_3410_2012_512_paramSetA(
const EC_GROUP *group, EC_POINT *r, const BIGNUM *n, const EC_POINT *q,
return ret;
}
+/*-
+ * An OpenSSL wrapper for variable point scalar multiplication.
+ * r := m * q
+ */
int
point_mul_id_tc26_gost_3410_2012_512_paramSetA(const EC_GROUP *group,
EC_POINT *r,
return ret;
}
+/*-
+ * An OpenSSL wrapper for fixed scalar multiplication.
+ * r := n * G
+ */
int
point_mul_g_id_tc26_gost_3410_2012_512_paramSetA(const EC_GROUP *group,
EC_POINT *r,
projects / openssl-gost / engine.git / blobdiff