Improve rewriter speed

Andres and I met today, and discovered that there's a source of
non-linear complexity in the rewriter which is not type casts.

In adding side-conditions to the rewrite rules (which are not discussed
in the pattern-matching compilation paper), I represented them by
allowing rewrite rules to fail.  So, for example,

    # + x ~~> x (when # == 0)

is represented as

    # + x ~~> if (# =? 0) then Some x else None

In the case that a rewrite rule fails, we need to try all other rewrite
rules that might still apply.  However, doing this in the naive-CPS way
leads to non-linear blowup, because wildcard rewrite rules get
duplicated in the failure branches.  (This is similar to the issue that
`match x with "some string" => true | _ => false end%string` will
generate a large number of "false" branches, and duplicate "false"
across all of them, rather than having a single default case.)
For example, if we had the rewrite rules

    # + # ~~> literal sum
    x + (-y) ~~> x - y
    (-x) + y ~~> y - x

then the compiled code would look like
    fun x y
      => if x is a literal
         then if y is a literal
              then literal sum
              else if y is an opp
                   then x - y
                   else x + y
         else if y is an opp
         then x - y
         else if x is an opp
              then y - x
              else x + y

where we actually want the code

    fun x y
      => if x is a literal
         then if y is a literal
              then return (literal sum);
         if y is an opp
         then return (x - y);
         if x is an opp
         then return (y - x);
         return (x + y)

in the sequence+return monad.  i.e., we want to not duplicate the "if y
is an opp" code multiple times.

I think the solution to this is to have the discrimination tree
evaluator return an option, and to have the function that computes the
discrimination tree not duplicate rewrite rules among different cases.

Note that this leads to slightly inefficient matching sometimes: when
two rules with the same structure are separated by a rule with a
wildcard instead of structure, we will now try to match on the structure
twice.  It might be useful to be able to denote that some rewrite rules
can be commuted.

After     | File Name                                                            | Before    || Change     | % Change
----------------------------------------------------------------------------------------------------------------------
40m35.83s | Total                                                                | 30m00.99s || +10m34.84s | +35.24%
----------------------------------------------------------------------------------------------------------------------
21m46.37s | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   | 6m01.39s  || +15m44.97s | +261.48%
6m37.40s  | p384_32.c                                                            | 0m22.47s  || +6m14.92s  | +1668.58%
0m18.00s  | Experiments/NewPipeline/Rewriter                                     | 5m16.50s  || -4m58.50s  | -94.31%
0m30.49s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 1m54.20s  || -1m23.71s  | -73.30%
0m27.41s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 1m39.40s  || -1m11.99s  | -72.42%
0m47.78s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 1m54.50s  || -1m06.71s  | -58.27%
0m40.28s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 1m23.77s  || -0m43.48s  | -51.91%
0m15.21s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m55.86s  || -0m40.64s  | -72.77%
0m23.39s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 1m00.22s  || -0m36.82s  | -61.15%
0m21.85s  | p256_32.c                                                            | 0m04.01s  || +0m17.84s  | +444.88%
0m20.97s  | secp256k1_32.c                                                       | 0m03.26s  || +0m17.71s  | +543.25%
0m04.60s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m20.33s  || -0m15.72s  | -77.37%
0m09.48s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m23.28s  || -0m13.80s  | -59.27%
1m33.63s  | Experiments/NewPipeline/Toplevel2                                    | 1m45.56s  || -0m11.93s  | -11.30%
0m08.29s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m18.64s  || -0m10.35s  | -55.52%
0m05.93s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m16.74s  || -0m10.80s  | -64.57%
0m32.41s  | p521_64.c                                                            | 0m41.42s  || -0m09.01s  | -21.75%
0m04.93s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m14.92s  || -0m09.99s  | -66.95%
0m04.40s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m12.57s  || -0m08.16s  | -64.99%
0m08.52s  | p224_32.c                                                            | 0m01.95s  || +0m06.56s  | +336.92%
0m13.99s  | p384_64.c                                                            | 0m10.64s  || +0m03.34s  | +31.48%
4m07.13s  | Experiments/NewPipeline/Toplevel1                                    | 4m05.83s  || +0m01.29s  | +0.52%
0m38.96s  | p521_32.c                                                            | 0m40.09s  || -0m01.13s  | -2.81%
0m02.28s  | p224_64.c                                                            | 0m01.66s  || +0m00.61s  | +37.34%
0m02.27s  | curve25519_32.c                                                      | 0m01.98s  || +0m00.29s  | +14.64%
0m01.78s  | p256_64.c                                                            | 0m01.65s  || +0m00.13s  | +7.87%
0m01.70s  | secp256k1_64.c                                                       | 0m01.96s  || -0m00.26s  | -13.26%
0m01.65s  | curve25519_64.c                                                      | 0m01.51s  || +0m00.13s  | +9.27%
0m01.37s  | Experiments/NewPipeline/CLI                                          | 0m01.26s  || +0m00.11s  | +8.73%
0m01.15s  | Experiments/NewPipeline/StandaloneHaskellMain                        | 0m01.21s  || -0m00.06s  | -4.95%
0m01.14s  | Experiments/NewPipeline/StandaloneOCamlMain                          | 0m01.16s  || -0m00.02s  | -1.72%
0m01.07s  | Experiments/NewPipeline/CompilersTestCases                           | 0m01.05s  || +0m00.02s  | +1.90%

1 files changed, 745 insertions, 536 deletions

diff --git a/curve25519_64.c b/curve25519_64.c
index 899f37e40..f13404de3 100644
--- a/curve25519_64.c
+++ b/curve25519_64.c
@@ -1,3 +1,4 @@
+check_args
 /* Autogenerated */
 /* curve description: 25519 */
 /* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */
@@ -13,541 +14,749 @@ typedef signed __int128 fiat_25519_int128;
 typedef unsigned __int128 fiat_25519_uint128;
 
 
-/*
- * Input Bounds:
- *   arg1: [0x0 ~> 0x1]
- *   arg2: [0x0 ~> 0x7ffffffffffff]
- *   arg3: [0x0 ~> 0x7ffffffffffff]
- * Output Bounds:
- *   out1: [0x0 ~> 0x7ffffffffffff]
- *   out2: [0x0 ~> 0x1]
- */
-static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
-  uint64_t x1 = ((arg1 + arg2) + arg3);
-  uint64_t x2 = (x1 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint1 x3 = (fiat_25519_uint1)(x1 >> 51);
-  *out1 = x2;
-  *out2 = x3;
-}
 
-/*
- * Input Bounds:
- *   arg1: [0x0 ~> 0x1]
- *   arg2: [0x0 ~> 0x7ffffffffffff]
- *   arg3: [0x0 ~> 0x7ffffffffffff]
- * Output Bounds:
- *   out1: [0x0 ~> 0x7ffffffffffff]
- *   out2: [0x0 ~> 0x1]
- */
-static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
-  int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
-  fiat_25519_int1 x2 = (fiat_25519_int1)((uint64_t)x1 >> 51);
-  uint64_t x3 = (x1 & UINT64_C(0x7ffffffffffff));
-  *out1 = x3;
-  *out2 = (fiat_25519_uint1)(0x0 - x2);
-}
-
-/*
- * Input Bounds:
- *   arg1: [0x0 ~> 0x1]
- *   arg2: [0x0 ~> 0xffffffffffffffff]
- *   arg3: [0x0 ~> 0xffffffffffffffff]
- * Output Bounds:
- *   out1: [0x0 ~> 0xffffffffffffffff]
- */
-static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
-  fiat_25519_uint1 x1 = (!(!arg1));
-  uint64_t x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff));
-  uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_25519_uint128)(~x2) & arg2));
-  *out1 = x3;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- *   arg2: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- */
-static void fiat_25519_carry_mul(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
-  fiat_25519_uint128 x1 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x2 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x3 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[2]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x4 = ((fiat_25519_uint128)(arg1[4]) * ((arg2[1]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x5 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x6 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x7 = ((fiat_25519_uint128)(arg1[3]) * ((arg2[2]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x8 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x9 = ((fiat_25519_uint128)(arg1[2]) * ((arg2[3]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x10 = ((fiat_25519_uint128)(arg1[1]) * ((arg2[4]) * (uint64_t)UINT8_C(0x13)));
-  fiat_25519_uint128 x11 = ((fiat_25519_uint128)(arg1[4]) * (arg2[0]));
-  fiat_25519_uint128 x12 = ((fiat_25519_uint128)(arg1[3]) * (arg2[1]));
-  fiat_25519_uint128 x13 = ((fiat_25519_uint128)(arg1[3]) * (arg2[0]));
-  fiat_25519_uint128 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg2[2]));
-  fiat_25519_uint128 x15 = ((fiat_25519_uint128)(arg1[2]) * (arg2[1]));
-  fiat_25519_uint128 x16 = ((fiat_25519_uint128)(arg1[2]) * (arg2[0]));
-  fiat_25519_uint128 x17 = ((fiat_25519_uint128)(arg1[1]) * (arg2[3]));
-  fiat_25519_uint128 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg2[2]));
-  fiat_25519_uint128 x19 = ((fiat_25519_uint128)(arg1[1]) * (arg2[1]));
-  fiat_25519_uint128 x20 = ((fiat_25519_uint128)(arg1[1]) * (arg2[0]));
-  fiat_25519_uint128 x21 = ((fiat_25519_uint128)(arg1[0]) * (arg2[4]));
-  fiat_25519_uint128 x22 = ((fiat_25519_uint128)(arg1[0]) * (arg2[3]));
-  fiat_25519_uint128 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg2[2]));
-  fiat_25519_uint128 x24 = ((fiat_25519_uint128)(arg1[0]) * (arg2[1]));
-  fiat_25519_uint128 x25 = ((fiat_25519_uint128)(arg1[0]) * (arg2[0]));
-  fiat_25519_uint128 x26 = (x25 + (x10 + (x9 + (x7 + x4))));
-  uint64_t x27 = (uint64_t)(x26 >> 51);
-  uint64_t x28 = (uint64_t)(x26 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x29 = (x21 + (x17 + (x14 + (x12 + x11))));
-  fiat_25519_uint128 x30 = (x22 + (x18 + (x15 + (x13 + x1))));
-  fiat_25519_uint128 x31 = (x23 + (x19 + (x16 + (x5 + x2))));
-  fiat_25519_uint128 x32 = (x24 + (x20 + (x8 + (x6 + x3))));
-  fiat_25519_uint128 x33 = (x27 + x32);
-  uint64_t x34 = (uint64_t)(x33 >> 51);
-  uint64_t x35 = (uint64_t)(x33 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x36 = (x34 + x31);
-  uint64_t x37 = (uint64_t)(x36 >> 51);
-  uint64_t x38 = (uint64_t)(x36 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x39 = (x37 + x30);
-  uint64_t x40 = (uint64_t)(x39 >> 51);
-  uint64_t x41 = (uint64_t)(x39 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x42 = (x40 + x29);
-  uint64_t x43 = (uint64_t)(x42 >> 51);
-  uint64_t x44 = (uint64_t)(x42 & UINT64_C(0x7ffffffffffff));
-  uint64_t x45 = (x43 * (uint64_t)UINT8_C(0x13));
-  uint64_t x46 = (x28 + x45);
-  uint64_t x47 = (x46 >> 51);
-  uint64_t x48 = (x46 & UINT64_C(0x7ffffffffffff));
-  uint64_t x49 = (x47 + x35);
-  uint64_t x50 = (x49 >> 51);
-  uint64_t x51 = (x49 & UINT64_C(0x7ffffffffffff));
-  uint64_t x52 = (x50 + x38);
-  out1[0] = x48;
-  out1[1] = x51;
-  out1[2] = x52;
-  out1[3] = x41;
-  out1[4] = x44;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- */
-static void fiat_25519_carry_square(uint64_t out1[5], const uint64_t arg1[5]) {
-  uint64_t x1 = ((arg1[4]) * (uint64_t)UINT8_C(0x13));
-  uint64_t x2 = (x1 * (uint64_t)0x2);
-  uint64_t x3 = ((arg1[4]) * (uint64_t)0x2);
-  uint64_t x4 = ((arg1[3]) * (uint64_t)UINT8_C(0x13));
-  uint64_t x5 = (x4 * (uint64_t)0x2);
-  uint64_t x6 = ((arg1[3]) * (uint64_t)0x2);
-  uint64_t x7 = ((arg1[2]) * (uint64_t)0x2);
-  uint64_t x8 = ((arg1[1]) * (uint64_t)0x2);
-  fiat_25519_uint128 x9 = ((fiat_25519_uint128)(arg1[4]) * x1);
-  fiat_25519_uint128 x10 = ((fiat_25519_uint128)(arg1[3]) * x2);
-  fiat_25519_uint128 x11 = ((fiat_25519_uint128)(arg1[3]) * x4);
-  fiat_25519_uint128 x12 = ((fiat_25519_uint128)(arg1[2]) * x2);
-  fiat_25519_uint128 x13 = ((fiat_25519_uint128)(arg1[2]) * x5);
-  fiat_25519_uint128 x14 = ((fiat_25519_uint128)(arg1[2]) * (arg1[2]));
-  fiat_25519_uint128 x15 = ((fiat_25519_uint128)(arg1[1]) * x2);
-  fiat_25519_uint128 x16 = ((fiat_25519_uint128)(arg1[1]) * x6);
-  fiat_25519_uint128 x17 = ((fiat_25519_uint128)(arg1[1]) * x7);
-  fiat_25519_uint128 x18 = ((fiat_25519_uint128)(arg1[1]) * (arg1[1]));
-  fiat_25519_uint128 x19 = ((fiat_25519_uint128)(arg1[0]) * x3);
-  fiat_25519_uint128 x20 = ((fiat_25519_uint128)(arg1[0]) * x6);
-  fiat_25519_uint128 x21 = ((fiat_25519_uint128)(arg1[0]) * x7);
-  fiat_25519_uint128 x22 = ((fiat_25519_uint128)(arg1[0]) * x8);
-  fiat_25519_uint128 x23 = ((fiat_25519_uint128)(arg1[0]) * (arg1[0]));
-  fiat_25519_uint128 x24 = (x23 + (x15 + x13));
-  uint64_t x25 = (uint64_t)(x24 >> 51);
-  uint64_t x26 = (uint64_t)(x24 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x27 = (x19 + (x16 + x14));
-  fiat_25519_uint128 x28 = (x20 + (x17 + x9));
-  fiat_25519_uint128 x29 = (x21 + (x18 + x10));
-  fiat_25519_uint128 x30 = (x22 + (x12 + x11));
-  fiat_25519_uint128 x31 = (x25 + x30);
-  uint64_t x32 = (uint64_t)(x31 >> 51);
-  uint64_t x33 = (uint64_t)(x31 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x34 = (x32 + x29);
-  uint64_t x35 = (uint64_t)(x34 >> 51);
-  uint64_t x36 = (uint64_t)(x34 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x37 = (x35 + x28);
-  uint64_t x38 = (uint64_t)(x37 >> 51);
-  uint64_t x39 = (uint64_t)(x37 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x40 = (x38 + x27);
-  uint64_t x41 = (uint64_t)(x40 >> 51);
-  uint64_t x42 = (uint64_t)(x40 & UINT64_C(0x7ffffffffffff));
-  uint64_t x43 = (x41 * (uint64_t)UINT8_C(0x13));
-  uint64_t x44 = (x26 + x43);
-  uint64_t x45 = (x44 >> 51);
-  uint64_t x46 = (x44 & UINT64_C(0x7ffffffffffff));
-  uint64_t x47 = (x45 + x33);
-  uint64_t x48 = (x47 >> 51);
-  uint64_t x49 = (x47 & UINT64_C(0x7ffffffffffff));
-  uint64_t x50 = (x48 + x36);
-  out1[0] = x46;
-  out1[1] = x49;
-  out1[2] = x50;
-  out1[3] = x39;
-  out1[4] = x42;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- */
-static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[5]) {
-  fiat_25519_uint128 x1 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[4]));
-  fiat_25519_uint128 x2 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[3]));
-  fiat_25519_uint128 x3 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[2]));
-  fiat_25519_uint128 x4 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[1]));
-  fiat_25519_uint128 x5 = (UINT32_C(0x1db42) * (fiat_25519_uint128)(arg1[0]));
-  uint64_t x6 = (uint64_t)(x5 >> 51);
-  uint64_t x7 = (uint64_t)(x5 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x8 = (x6 + x4);
-  uint64_t x9 = (uint64_t)(x8 >> 51);
-  uint64_t x10 = (uint64_t)(x8 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x11 = (x9 + x3);
-  uint64_t x12 = (uint64_t)(x11 >> 51);
-  uint64_t x13 = (uint64_t)(x11 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x14 = (x12 + x2);
-  uint64_t x15 = (uint64_t)(x14 >> 51);
-  uint64_t x16 = (uint64_t)(x14 & UINT64_C(0x7ffffffffffff));
-  fiat_25519_uint128 x17 = (x15 + x1);
-  uint64_t x18 = (uint64_t)(x17 >> 51);
-  uint64_t x19 = (uint64_t)(x17 & UINT64_C(0x7ffffffffffff));
-  uint64_t x20 = (x18 * (uint64_t)UINT8_C(0x13));
-  uint64_t x21 = (x7 + x20);
-  uint64_t x22 = (x21 >> 51);
-  uint64_t x23 = (x21 & UINT64_C(0x7ffffffffffff));
-  uint64_t x24 = (x22 + x10);
-  uint64_t x25 = (x24 >> 51);
-  uint64_t x26 = (x24 & UINT64_C(0x7ffffffffffff));
-  uint64_t x27 = (x25 + x13);
-  out1[0] = x23;
-  out1[1] = x26;
-  out1[2] = x27;
-  out1[3] = x16;
-  out1[4] = x19;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- */
-static void fiat_25519_carry(uint64_t out1[5], const uint64_t arg1[5]) {
-  uint64_t x1 = (arg1[0]);
-  uint64_t x2 = ((x1 >> 51) + (arg1[1]));
-  uint64_t x3 = ((x2 >> 51) + (arg1[2]));
-  uint64_t x4 = ((x3 >> 51) + (arg1[3]));
-  uint64_t x5 = ((x4 >> 51) + (arg1[4]));
-  uint64_t x6 = ((x1 & UINT64_C(0x7ffffffffffff)) + ((x5 >> 51) * (uint64_t)UINT8_C(0x13)));
-  uint64_t x7 = ((x6 >> 51) + (x2 & UINT64_C(0x7ffffffffffff)));
-  uint64_t x8 = (x6 & UINT64_C(0x7ffffffffffff));
-  uint64_t x9 = (x7 & UINT64_C(0x7ffffffffffff));
-  uint64_t x10 = ((x7 >> 51) + (x3 & UINT64_C(0x7ffffffffffff)));
-  uint64_t x11 = (x4 & UINT64_C(0x7ffffffffffff));
-  uint64_t x12 = (x5 & UINT64_C(0x7ffffffffffff));
-  out1[0] = x8;
-  out1[1] = x9;
-  out1[2] = x10;
-  out1[3] = x11;
-  out1[4] = x12;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- *   arg2: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- */
-static void fiat_25519_add(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
-  uint64_t x1 = ((arg1[0]) + (arg2[0]));
-  uint64_t x2 = ((arg1[1]) + (arg2[1]));
-  uint64_t x3 = ((arg1[2]) + (arg2[2]));
-  uint64_t x4 = ((arg1[3]) + (arg2[3]));
-  uint64_t x5 = ((arg1[4]) + (arg2[4]));
-  out1[0] = x1;
-  out1[1] = x2;
-  out1[2] = x3;
-  out1[3] = x4;
-  out1[4] = x5;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- *   arg2: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- */
-static void fiat_25519_sub(uint64_t out1[5], const uint64_t arg1[5], const uint64_t arg2[5]) {
-  uint64_t x1 = ((UINT64_C(0xfffffffffffda) + (arg1[0])) - (arg2[0]));
-  uint64_t x2 = ((UINT64_C(0xffffffffffffe) + (arg1[1])) - (arg2[1]));
-  uint64_t x3 = ((UINT64_C(0xffffffffffffe) + (arg1[2])) - (arg2[2]));
-  uint64_t x4 = ((UINT64_C(0xffffffffffffe) + (arg1[3])) - (arg2[3]));
-  uint64_t x5 = ((UINT64_C(0xffffffffffffe) + (arg1[4])) - (arg2[4]));
-  out1[0] = x1;
-  out1[1] = x2;
-  out1[2] = x3;
-  out1[3] = x4;
-  out1[4] = x5;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
- */
-static void fiat_25519_opp(uint64_t out1[5], const uint64_t arg1[5]) {
-  uint64_t x1 = (UINT64_C(0xfffffffffffda) - (arg1[0]));
-  uint64_t x2 = (UINT64_C(0xffffffffffffe) - (arg1[1]));
-  uint64_t x3 = (UINT64_C(0xffffffffffffe) - (arg1[2]));
-  uint64_t x4 = (UINT64_C(0xffffffffffffe) - (arg1[3]));
-  uint64_t x5 = (UINT64_C(0xffffffffffffe) - (arg1[4]));
-  out1[0] = x1;
-  out1[1] = x2;
-  out1[2] = x3;
-  out1[3] = x4;
-  out1[4] = x5;
-}
-
-/*
- * Input Bounds:
- *   arg1: [0x0 ~> 0x1]
- *   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
- *   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
- */
-static void fiat_25519_selectznz(uint64_t out1[5], fiat_25519_uint1 arg1, const uint64_t arg2[5], const uint64_t arg3[5]) {
-  uint64_t x1;
-  fiat_25519_cmovznz_u64(&x1, arg1, (arg2[0]), (arg3[0]));
-  uint64_t x2;
-  fiat_25519_cmovznz_u64(&x2, arg1, (arg2[1]), (arg3[1]));
-  uint64_t x3;
-  fiat_25519_cmovznz_u64(&x3, arg1, (arg2[2]), (arg3[2]));
-  uint64_t x4;
-  fiat_25519_cmovznz_u64(&x4, arg1, (arg2[3]), (arg3[3]));
-  uint64_t x5;
-  fiat_25519_cmovznz_u64(&x5, arg1, (arg2[4]), (arg3[4]));
-  out1[0] = x1;
-  out1[1] = x2;
-  out1[2] = x3;
-  out1[3] = x4;
-  out1[4] = x5;
-}
-
-/*
- * Input Bounds:
- *   arg1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- * 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 ~> 0x7f]]
- */
-static void fiat_25519_to_bytes(uint8_t out1[32], const uint64_t arg1[5]) {
-  uint64_t x1;
-  fiat_25519_uint1 x2;
-  fiat_25519_subborrowx_u51(&x1, &x2, 0x0, (arg1[0]), UINT64_C(0x7ffffffffffed));
-  uint64_t x3;
-  fiat_25519_uint1 x4;
-  fiat_25519_subborrowx_u51(&x3, &x4, x2, (arg1[1]), UINT64_C(0x7ffffffffffff));
-  uint64_t x5;
-  fiat_25519_uint1 x6;
-  fiat_25519_subborrowx_u51(&x5, &x6, x4, (arg1[2]), UINT64_C(0x7ffffffffffff));
-  uint64_t x7;
-  fiat_25519_uint1 x8;
-  fiat_25519_subborrowx_u51(&x7, &x8, x6, (arg1[3]), UINT64_C(0x7ffffffffffff));
-  uint64_t x9;
-  fiat_25519_uint1 x10;
-  fiat_25519_subborrowx_u51(&x9, &x10, x8, (arg1[4]), UINT64_C(0x7ffffffffffff));
-  uint64_t x11;
-  fiat_25519_cmovznz_u64(&x11, x10, 0x0, UINT64_C(0xffffffffffffffff));
-  uint64_t x12;
-  fiat_25519_uint1 x13;
-  fiat_25519_addcarryx_u51(&x12, &x13, 0x0, (x11 & UINT64_C(0x7ffffffffffed)), x1);
-  uint64_t x14;
-  fiat_25519_uint1 x15;
-  fiat_25519_addcarryx_u51(&x14, &x15, x13, (x11 & UINT64_C(0x7ffffffffffff)), x3);
-  uint64_t x16;
-  fiat_25519_uint1 x17;
-  fiat_25519_addcarryx_u51(&x16, &x17, x15, (x11 & UINT64_C(0x7ffffffffffff)), x5);
-  uint64_t x18;
-  fiat_25519_uint1 x19;
-  fiat_25519_addcarryx_u51(&x18, &x19, x17, (x11 & UINT64_C(0x7ffffffffffff)), x7);
-  uint64_t x20;
-  fiat_25519_uint1 x21;
-  fiat_25519_addcarryx_u51(&x20, &x21, x19, (x11 & UINT64_C(0x7ffffffffffff)), x9);
-  uint64_t x22 = (x20 << 4);
-  uint64_t x23 = (x18 * (uint64_t)0x2);
-  uint64_t x24 = (x16 << 6);
-  uint64_t x25 = (x14 << 3);
-  uint64_t x26 = (x12 >> 8);
-  uint8_t x27 = (uint8_t)(x12 & UINT8_C(0xff));
-  uint64_t x28 = (x26 >> 8);
-  uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff));
-  uint64_t x30 = (x28 >> 8);
-  uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff));
-  uint64_t x32 = (x30 >> 8);
-  uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff));
-  uint64_t x34 = (x32 >> 8);
-  uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff));
-  uint8_t x36 = (uint8_t)(x34 >> 8);
-  uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff));
-  uint64_t x38 = (x36 + x25);
-  uint64_t x39 = (x38 >> 8);
-  uint8_t x40 = (uint8_t)(x38 & UINT8_C(0xff));
-  uint64_t x41 = (x39 >> 8);
-  uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff));
-  uint64_t x43 = (x41 >> 8);
-  uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff));
-  uint64_t x45 = (x43 >> 8);
-  uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff));
-  uint64_t x47 = (x45 >> 8);
-  uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff));
-  uint8_t x49 = (uint8_t)(x47 >> 8);
-  uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff));
-  uint64_t x51 = (x49 + x24);
-  uint64_t x52 = (x51 >> 8);
-  uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff));
-  uint64_t x54 = (x52 >> 8);
-  uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff));
-  uint64_t x56 = (x54 >> 8);
-  uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff));
-  uint64_t x58 = (x56 >> 8);
-  uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff));
-  uint64_t x60 = (x58 >> 8);
-  uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff));
-  uint64_t x62 = (x60 >> 8);
-  uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff));
-  fiat_25519_uint1 x64 = (fiat_25519_uint1)(x62 >> 8);
-  uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff));
-  uint64_t x66 = (x64 + x23);
-  uint64_t x67 = (x66 >> 8);
-  uint8_t x68 = (uint8_t)(x66 & UINT8_C(0xff));
-  uint64_t x69 = (x67 >> 8);
-  uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff));
-  uint64_t x71 = (x69 >> 8);
-  uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff));
-  uint64_t x73 = (x71 >> 8);
-  uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff));
-  uint64_t x75 = (x73 >> 8);
-  uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff));
-  uint8_t x77 = (uint8_t)(x75 >> 8);
-  uint8_t x78 = (uint8_t)(x75 & UINT8_C(0xff));
-  uint64_t x79 = (x77 + x22);
-  uint64_t x80 = (x79 >> 8);
-  uint8_t x81 = (uint8_t)(x79 & UINT8_C(0xff));
-  uint64_t x82 = (x80 >> 8);
-  uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff));
-  uint64_t x84 = (x82 >> 8);
-  uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff));
-  uint64_t x86 = (x84 >> 8);
-  uint8_t x87 = (uint8_t)(x84 & UINT8_C(0xff));
-  uint64_t x88 = (x86 >> 8);
-  uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff));
-  uint8_t x90 = (uint8_t)(x88 >> 8);
-  uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff));
-  out1[0] = x27;
-  out1[1] = x29;
-  out1[2] = x31;
-  out1[3] = x33;
-  out1[4] = x35;
-  out1[5] = x37;
-  out1[6] = x40;
-  out1[7] = x42;
-  out1[8] = x44;
-  out1[9] = x46;
-  out1[10] = x48;
-  out1[11] = x50;
-  out1[12] = x53;
-  out1[13] = x55;
-  out1[14] = x57;
-  out1[15] = x59;
-  out1[16] = x61;
-  out1[17] = x63;
-  out1[18] = x65;
-  out1[19] = x68;
-  out1[20] = x70;
-  out1[21] = x72;
-  out1[22] = x74;
-  out1[23] = x76;
-  out1[24] = x78;
-  out1[25] = x81;
-  out1[26] = x83;
-  out1[27] = x85;
-  out1[28] = x87;
-  out1[29] = x89;
-  out1[30] = x91;
-  out1[31] = x90;
-}
-
-/*
- * 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 ~> 0x7f]]
- * Output Bounds:
- *   out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
- */
-static void fiat_25519_from_bytes(uint64_t out1[5], const uint8_t arg1[32]) {
-  uint64_t x1 = ((uint64_t)(arg1[31]) << 44);
-  uint64_t x2 = ((uint64_t)(arg1[30]) << 36);
-  uint64_t x3 = ((uint64_t)(arg1[29]) << 28);
-  uint64_t x4 = ((uint64_t)(arg1[28]) << 20);
-  uint64_t x5 = ((uint64_t)(arg1[27]) << 12);
-  uint64_t x6 = ((uint64_t)(arg1[26]) << 4);
-  uint64_t x7 = ((uint64_t)(arg1[25]) << 47);
-  uint64_t x8 = ((uint64_t)(arg1[24]) << 39);
-  uint64_t x9 = ((uint64_t)(arg1[23]) << 31);
-  uint64_t x10 = ((uint64_t)(arg1[22]) << 23);
-  uint64_t x11 = ((uint64_t)(arg1[21]) << 15);
-  uint64_t x12 = ((uint64_t)(arg1[20]) << 7);
-  uint64_t x13 = ((uint64_t)(arg1[19]) << 50);
-  uint64_t x14 = ((uint64_t)(arg1[18]) << 42);
-  uint64_t x15 = ((uint64_t)(arg1[17]) << 34);
-  uint64_t x16 = ((uint64_t)(arg1[16]) << 26);
-  uint64_t x17 = ((uint64_t)(arg1[15]) << 18);
-  uint64_t x18 = ((uint64_t)(arg1[14]) << 10);
-  uint64_t x19 = ((uint64_t)(arg1[13]) << 2);
-  uint64_t x20 = ((uint64_t)(arg1[12]) << 45);
-  uint64_t x21 = ((uint64_t)(arg1[11]) << 37);
-  uint64_t x22 = ((uint64_t)(arg1[10]) << 29);
-  uint64_t x23 = ((uint64_t)(arg1[9]) << 21);
-  uint64_t x24 = ((uint64_t)(arg1[8]) << 13);
-  uint64_t x25 = ((uint64_t)(arg1[7]) << 5);
-  uint64_t x26 = ((uint64_t)(arg1[6]) << 48);
-  uint64_t x27 = ((uint64_t)(arg1[5]) << 40);
-  uint64_t x28 = ((uint64_t)(arg1[4]) << 32);
-  uint64_t x29 = ((uint64_t)(arg1[3]) << 24);
-  uint64_t x30 = ((uint64_t)(arg1[2]) << 16);
-  uint64_t x31 = ((uint64_t)(arg1[1]) << 8);
-  uint8_t x32 = (arg1[0]);
-  uint64_t x33 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + x26))))));
-  uint8_t x34 = (uint8_t)(x33 >> 51);
-  uint64_t x35 = (x33 & UINT64_C(0x7ffffffffffff));
-  uint64_t x36 = (x6 + (x5 + (x4 + (x3 + (x2 + x1)))));
-  uint64_t x37 = (x12 + (x11 + (x10 + (x9 + (x8 + x7)))));
-  uint64_t x38 = (x19 + (x18 + (x17 + (x16 + (x15 + (x14 + x13))))));
-  uint64_t x39 = (x25 + (x24 + (x23 + (x22 + (x21 + x20)))));
-  uint64_t x40 = (x34 + x39);
-  uint8_t x41 = (uint8_t)(x40 >> 51);
-  uint64_t x42 = (x40 & UINT64_C(0x7ffffffffffff));
-  uint64_t x43 = (x41 + x38);
-  uint8_t x44 = (uint8_t)(x43 >> 51);
-  uint64_t x45 = (x43 & UINT64_C(0x7ffffffffffff));
-  uint64_t x46 = (x44 + x37);
-  uint8_t x47 = (uint8_t)(x46 >> 51);
-  uint64_t x48 = (x46 & UINT64_C(0x7ffffffffffff));
-  uint64_t x49 = (x47 + x36);
-  out1[0] = x35;
-  out1[1] = x42;
-  out1[2] = x45;
-  out1[3] = x48;
-  out1[4] = x49;
-}
+In fiat_25519_to_bytes:
+Stringification failed on the syntax tree:
+(λ x1,
+  expr_let x2 := Z.add_with_get_carry(2^51, 0, -0x7ffffffffffed, x1[0]) (* : uint51_t, int1_t *) in
+  expr_let x3 := Z.add_with_get_carry(2^51, x2₂, -(2^51-1), x1[1]) (* : uint51_t, int1_t *) in
+  expr_let x4 := Z.add_with_get_carry(2^51, x3₂, -(2^51-1), x1[2]) (* : uint51_t, int1_t *) in
+  expr_let x5 := Z.add_with_get_carry(2^51, x4₂, -(2^51-1), x1[3]) (* : uint51_t, int1_t *) in
+  expr_let x6 := Z.add_with_get_carry(2^51, x5₂, -(2^51-1), x1[4]) (* : uint51_t, int1_t *) in
+  expr_let x7 := Z.zselect((-x6₂), 0, 2^64-1) (* : uint64_t *) in
+  expr_let x8 := Z.add_with_get_carry(2^51, 0, (x7 & 0x7ffffffffffed), x2₁) (* : uint64_t, uint1_t *) in
+  expr_let x9 := Z.add_with_get_carry(2^51, x8₂, (x7 & 2^51-1), x3₁) (* : uint64_t, uint1_t *) in
+  expr_let x10 := Z.add_with_get_carry(2^51, x9₂, (x7 & 2^51-1), x4₁) (* : uint64_t, uint1_t *) in
+  expr_let x11 := Z.add_with_get_carry(2^51, x10₂, (x7 & 2^51-1), x5₁) (* : uint64_t, uint1_t *) in
+  expr_let x12 := Z.add_with_get_carry(2^51, x11₂, (x7 & 2^51-1), x6₁) (* : uint64_t, uint1_t *) in
+  expr_let x13 := x12₁ * 16 (* : uint64_t *) in
+  expr_let x14 := x11₁ * 2 (* : uint64_t *) in
+  expr_let x15 := x10₁ * 64 (* : uint64_t *) in
+  expr_let x16 := x9₁ * 8 (* : uint64_t *) in
+  expr_let x17 := x8₁ * 1 (* : uint64_t *) in
+  expr_let x18 := x17 >> 8 (* : uint64_t *) in
+  expr_let x19 := x17 & 255 (* : uint8_t *) in
+  expr_let x20 := x13 * 1 (* : uint64_t *) in
+  expr_let x21 := x14 * 1 (* : uint64_t *) in
+  expr_let x22 := x15 * 1 (* : uint64_t *) in
+  expr_let x23 := x16 * 1 (* : uint64_t *) in
+  expr_let x24 := x19 * 1 (* : uint8_t *) in
+  expr_let x25 := x18 * 1 (* : uint64_t *) in
+  expr_let x26 := x25 >> 8 (* : uint64_t *) in
+  expr_let x27 := x25 & 255 (* : uint8_t *) in
+  expr_let x28 := x20 * 1 (* : uint64_t *) in
+  expr_let x29 := x21 * 1 (* : uint64_t *) in
+  expr_let x30 := x22 * 1 (* : uint64_t *) in
+  expr_let x31 := x23 * 1 (* : uint64_t *) in
+  expr_let x32 := x27 * 1 (* : uint8_t *) in
+  expr_let x33 := x26 * 1 (* : uint64_t *) in
+  expr_let x34 := x24 * 1 (* : uint8_t *) in
+  expr_let x35 := x33 >> 8 (* : uint64_t *) in
+  expr_let x36 := x33 & 255 (* : uint8_t *) in
+  expr_let x37 := x28 * 1 (* : uint64_t *) in
+  expr_let x38 := x29 * 1 (* : uint64_t *) in
+  expr_let x39 := x30 * 1 (* : uint64_t *) in
+  expr_let x40 := x31 * 1 (* : uint64_t *) in
+  expr_let x41 := x36 * 1 (* : uint8_t *) in
+  expr_let x42 := x35 * 1 (* : uint64_t *) in
+  expr_let x43 := x32 * 1 (* : uint8_t *) in
+  expr_let x44 := x34 * 1 (* : uint8_t *) in
+  expr_let x45 := x42 >> 8 (* : uint64_t *) in
+  expr_let x46 := x42 & 255 (* : uint8_t *) in
+  expr_let x47 := x37 * 1 (* : uint64_t *) in
+  expr_let x48 := x38 * 1 (* : uint64_t *) in
+  expr_let x49 := x39 * 1 (* : uint64_t *) in
+  expr_let x50 := x40 * 1 (* : uint64_t *) in
+  expr_let x51 := x46 * 1 (* : uint8_t *) in
+  expr_let x52 := x45 * 1 (* : uint64_t *) in
+  expr_let x53 := x41 * 1 (* : uint8_t *) in
+  expr_let x54 := x43 * 1 (* : uint8_t *) in
+  expr_let x55 := x44 * 1 (* : uint8_t *) in
+  expr_let x56 := x52 >> 8 (* : uint64_t *) in
+  expr_let x57 := x52 & 255 (* : uint8_t *) in
+  expr_let x58 := x47 * 1 (* : uint64_t *) in
+  expr_let x59 := x48 * 1 (* : uint64_t *) in
+  expr_let x60 := x49 * 1 (* : uint64_t *) in
+  expr_let x61 := x50 * 1 (* : uint64_t *) in
+  expr_let x62 := x57 * 1 (* : uint8_t *) in
+  expr_let x63 := x56 * 1 (* : uint64_t *) in
+  expr_let x64 := x51 * 1 (* : uint8_t *) in
+  expr_let x65 := x53 * 1 (* : uint8_t *) in
+  expr_let x66 := x54 * 1 (* : uint8_t *) in
+  expr_let x67 := x55 * 1 (* : uint8_t *) in
+  expr_let x68 := x63 >> 8 (* : uint8_t *) in
+  expr_let x69 := x63 & 255 (* : uint8_t *) in
+  expr_let x70 := x58 * 1 (* : uint64_t *) in
+  expr_let x71 := x59 * 1 (* : uint64_t *) in
+  expr_let x72 := x60 * 1 (* : uint64_t *) in
+  expr_let x73 := x61 * 1 (* : uint64_t *) in
+  expr_let x74 := x69 * 1 (* : uint8_t *) in
+  expr_let x75 := x68 * 1 (* : uint8_t *) in
+  expr_let x76 := x62 * 1 (* : uint8_t *) in
+  expr_let x77 := x64 * 1 (* : uint8_t *) in
+  expr_let x78 := x65 * 1 (* : uint8_t *) in
+  expr_let x79 := x66 * 1 (* : uint8_t *) in
+  expr_let x80 := x67 * 1 (* : uint8_t *) in
+  expr_let x81 := x75 + x73 (* : uint64_t *) in
+  expr_let x82 := x81 >> 8 (* : uint64_t *) in
+  expr_let x83 := x81 & 255 (* : uint8_t *) in
+  expr_let x84 := x70 * 1 (* : uint64_t *) in
+  expr_let x85 := x71 * 1 (* : uint64_t *) in
+  expr_let x86 := x72 * 1 (* : uint64_t *) in
+  expr_let x87 := x83 * 1 (* : uint8_t *) in
+  expr_let x88 := x82 * 1 (* : uint64_t *) in
+  expr_let x89 := x74 * 1 (* : uint8_t *) in
+  expr_let x90 := x76 * 1 (* : uint8_t *) in
+  expr_let x91 := x77 * 1 (* : uint8_t *) in
+  expr_let x92 := x78 * 1 (* : uint8_t *) in
+  expr_let x93 := x79 * 1 (* : uint8_t *) in
+  expr_let x94 := x80 * 1 (* : uint8_t *) in
+  expr_let x95 := x88 >> 8 (* : uint64_t *) in
+  expr_let x96 := x88 & 255 (* : uint8_t *) in
+  expr_let x97 := x84 * 1 (* : uint64_t *) in
+  expr_let x98 := x85 * 1 (* : uint64_t *) in
+  expr_let x99 := x86 * 1 (* : uint64_t *) in
+  expr_let x100 := x96 * 1 (* : uint8_t *) in
+  expr_let x101 := x95 * 1 (* : uint64_t *) in
+  expr_let x102 := x87 * 1 (* : uint8_t *) in
+  expr_let x103 := x89 * 1 (* : uint8_t *) in
+  expr_let x104 := x90 * 1 (* : uint8_t *) in
+  expr_let x105 := x91 * 1 (* : uint8_t *) in
+  expr_let x106 := x92 * 1 (* : uint8_t *) in
+  expr_let x107 := x93 * 1 (* : uint8_t *) in
+  expr_let x108 := x94 * 1 (* : uint8_t *) in
+  expr_let x109 := x101 >> 8 (* : uint64_t *) in
+  expr_let x110 := x101 & 255 (* : uint8_t *) in
+  expr_let x111 := x97 * 1 (* : uint64_t *) in
+  expr_let x112 := x98 * 1 (* : uint64_t *) in
+  expr_let x113 := x99 * 1 (* : uint64_t *) in
+  expr_let x114 := x110 * 1 (* : uint8_t *) in
+  expr_let x115 := x109 * 1 (* : uint64_t *) in
+  expr_let x116 := x100 * 1 (* : uint8_t *) in
+  expr_let x117 := x102 * 1 (* : uint8_t *) in
+  expr_let x118 := x103 * 1 (* : uint8_t *) in
+  expr_let x119 := x104 * 1 (* : uint8_t *) in
+  expr_let x120 := x105 * 1 (* : uint8_t *) in
+  expr_let x121 := x106 * 1 (* : uint8_t *) in
+  expr_let x122 := x107 * 1 (* : uint8_t *) in
+  expr_let x123 := x108 * 1 (* : uint8_t *) in
+  expr_let x124 := x115 >> 8 (* : uint64_t *) in
+  expr_let x125 := x115 & 255 (* : uint8_t *) in
+  expr_let x126 := x111 * 1 (* : uint64_t *) in
+  expr_let x127 := x112 * 1 (* : uint64_t *) in
+  expr_let x128 := x113 * 1 (* : uint64_t *) in
+  expr_let x129 := x125 * 1 (* : uint8_t *) in
+  expr_let x130 := x124 * 1 (* : uint64_t *) in
+  expr_let x131 := x114 * 1 (* : uint8_t *) in
+  expr_let x132 := x116 * 1 (* : uint8_t *) in
+  expr_let x133 := x117 * 1 (* : uint8_t *) in
+  expr_let x134 := x118 * 1 (* : uint8_t *) in
+  expr_let x135 := x119 * 1 (* : uint8_t *) in
+  expr_let x136 := x120 * 1 (* : uint8_t *) in
+  expr_let x137 := x121 * 1 (* : uint8_t *) in
+  expr_let x138 := x122 * 1 (* : uint8_t *) in
+  expr_let x139 := x123 * 1 (* : uint8_t *) in
+  expr_let x140 := x130 >> 8 (* : uint64_t *) in
+  expr_let x141 := x130 & 255 (* : uint8_t *) in
+  expr_let x142 := x126 * 1 (* : uint64_t *) in
+  expr_let x143 := x127 * 1 (* : uint64_t *) in
+  expr_let x144 := x128 * 1 (* : uint64_t *) in
+  expr_let x145 := x141 * 1 (* : uint8_t *) in
+  expr_let x146 := x140 * 1 (* : uint64_t *) in
+  expr_let x147 := x129 * 1 (* : uint8_t *) in
+  expr_let x148 := x131 * 1 (* : uint8_t *) in
+  expr_let x149 := x132 * 1 (* : uint8_t *) in
+  expr_let x150 := x133 * 1 (* : uint8_t *) in
+  expr_let x151 := x134 * 1 (* : uint8_t *) in
+  expr_let x152 := x135 * 1 (* : uint8_t *) in
+  expr_let x153 := x136 * 1 (* : uint8_t *) in
+  expr_let x154 := x137 * 1 (* : uint8_t *) in
+  expr_let x155 := x138 * 1 (* : uint8_t *) in
+  expr_let x156 := x139 * 1 (* : uint8_t *) in
+  expr_let x157 := x146 >> 8 (* : uint8_t *) in
+  expr_let x158 := x146 & 255 (* : uint8_t *) in
+  expr_let x159 := x142 * 1 (* : uint64_t *) in
+  expr_let x160 := x143 * 1 (* : uint64_t *) in
+  expr_let x161 := x144 * 1 (* : uint64_t *) in
+  expr_let x162 := x158 * 1 (* : uint8_t *) in
+  expr_let x163 := x157 * 1 (* : uint8_t *) in
+  expr_let x164 := x145 * 1 (* : uint8_t *) in
+  expr_let x165 := x147 * 1 (* : uint8_t *) in
+  expr_let x166 := x148 * 1 (* : uint8_t *) in
+  expr_let x167 := x149 * 1 (* : uint8_t *) in
+  expr_let x168 := x150 * 1 (* : uint8_t *) in
+  expr_let x169 := x151 * 1 (* : uint8_t *) in
+  expr_let x170 := x152 * 1 (* : uint8_t *) in
+  expr_let x171 := x153 * 1 (* : uint8_t *) in
+  expr_let x172 := x154 * 1 (* : uint8_t *) in
+  expr_let x173 := x155 * 1 (* : uint8_t *) in
+  expr_let x174 := x156 * 1 (* : uint8_t *) in
+  expr_let x175 := x163 + x161 (* : uint64_t *) in
+  expr_let x176 := x175 >> 8 (* : uint64_t *) in
+  expr_let x177 := x175 & 255 (* : uint8_t *) in
+  expr_let x178 := x159 * 1 (* : uint64_t *) in
+  expr_let x179 := x160 * 1 (* : uint64_t *) in
+  expr_let x180 := x177 * 1 (* : uint8_t *) in
+  expr_let x181 := x176 * 1 (* : uint64_t *) in
+  expr_let x182 := x162 * 1 (* : uint8_t *) in
+  expr_let x183 := x164 * 1 (* : uint8_t *) in
+  expr_let x184 := x165 * 1 (* : uint8_t *) in
+  expr_let x185 := x166 * 1 (* : uint8_t *) in
+  expr_let x186 := x167 * 1 (* : uint8_t *) in
+  expr_let x187 := x168 * 1 (* : uint8_t *) in
+  expr_let x188 := x169 * 1 (* : uint8_t *) in
+  expr_let x189 := x170 * 1 (* : uint8_t *) in
+  expr_let x190 := x171 * 1 (* : uint8_t *) in
+  expr_let x191 := x172 * 1 (* : uint8_t *) in
+  expr_let x192 := x173 * 1 (* : uint8_t *) in
+  expr_let x193 := x174 * 1 (* : uint8_t *) in
+  expr_let x194 := x181 >> 8 (* : uint64_t *) in
+  expr_let x195 := x181 & 255 (* : uint8_t *) in
+  expr_let x196 := x178 * 1 (* : uint64_t *) in
+  expr_let x197 := x179 * 1 (* : uint64_t *) in
+  expr_let x198 := x195 * 1 (* : uint8_t *) in
+  expr_let x199 := x194 * 1 (* : uint64_t *) in
+  expr_let x200 := x180 * 1 (* : uint8_t *) in
+  expr_let x201 := x182 * 1 (* : uint8_t *) in
+  expr_let x202 := x183 * 1 (* : uint8_t *) in
+  expr_let x203 := x184 * 1 (* : uint8_t *) in
+  expr_let x204 := x185 * 1 (* : uint8_t *) in
+  expr_let x205 := x186 * 1 (* : uint8_t *) in
+  expr_let x206 := x187 * 1 (* : uint8_t *) in
+  expr_let x207 := x188 * 1 (* : uint8_t *) in
+  expr_let x208 := x189 * 1 (* : uint8_t *) in
+  expr_let x209 := x190 * 1 (* : uint8_t *) in
+  expr_let x210 := x191 * 1 (* : uint8_t *) in
+  expr_let x211 := x192 * 1 (* : uint8_t *) in
+  expr_let x212 := x193 * 1 (* : uint8_t *) in
+  expr_let x213 := x199 >> 8 (* : uint64_t *) in
+  expr_let x214 := x199 & 255 (* : uint8_t *) in
+  expr_let x215 := x196 * 1 (* : uint64_t *) in
+  expr_let x216 := x197 * 1 (* : uint64_t *) in
+  expr_let x217 := x214 * 1 (* : uint8_t *) in
+  expr_let x218 := x213 * 1 (* : uint64_t *) in
+  expr_let x219 := x198 * 1 (* : uint8_t *) in
+  expr_let x220 := x200 * 1 (* : uint8_t *) in
+  expr_let x221 := x201 * 1 (* : uint8_t *) in
+  expr_let x222 := x202 * 1 (* : uint8_t *) in
+  expr_let x223 := x203 * 1 (* : uint8_t *) in
+  expr_let x224 := x204 * 1 (* : uint8_t *) in
+  expr_let x225 := x205 * 1 (* : uint8_t *) in
+  expr_let x226 := x206 * 1 (* : uint8_t *) in
+  expr_let x227 := x207 * 1 (* : uint8_t *) in
+  expr_let x228 := x208 * 1 (* : uint8_t *) in
+  expr_let x229 := x209 * 1 (* : uint8_t *) in
+  expr_let x230 := x210 * 1 (* : uint8_t *) in
+  expr_let x231 := x211 * 1 (* : uint8_t *) in
+  expr_let x232 := x212 * 1 (* : uint8_t *) in
+  expr_let x233 := x218 >> 8 (* : uint64_t *) in
+  expr_let x234 := x218 & 255 (* : uint8_t *) in
+  expr_let x235 := x215 * 1 (* : uint64_t *) in
+  expr_let x236 := x216 * 1 (* : uint64_t *) in
+  expr_let x237 := x234 * 1 (* : uint8_t *) in
+  expr_let x238 := x233 * 1 (* : uint64_t *) in
+  expr_let x239 := x217 * 1 (* : uint8_t *) in
+  expr_let x240 := x219 * 1 (* : uint8_t *) in
+  expr_let x241 := x220 * 1 (* : uint8_t *) in
+  expr_let x242 := x221 * 1 (* : uint8_t *) in
+  expr_let x243 := x222 * 1 (* : uint8_t *) in
+  expr_let x244 := x223 * 1 (* : uint8_t *) in
+  expr_let x245 := x224 * 1 (* : uint8_t *) in
+  expr_let x246 := x225 * 1 (* : uint8_t *) in
+  expr_let x247 := x226 * 1 (* : uint8_t *) in
+  expr_let x248 := x227 * 1 (* : uint8_t *) in
+  expr_let x249 := x228 * 1 (* : uint8_t *) in
+  expr_let x250 := x229 * 1 (* : uint8_t *) in
+  expr_let x251 := x230 * 1 (* : uint8_t *) in
+  expr_let x252 := x231 * 1 (* : uint8_t *) in
+  expr_let x253 := x232 * 1 (* : uint8_t *) in
+  expr_let x254 := x238 >> 8 (* : uint64_t *) in
+  expr_let x255 := x238 & 255 (* : uint8_t *) in
+  expr_let x256 := x235 * 1 (* : uint64_t *) in
+  expr_let x257 := x236 * 1 (* : uint64_t *) in
+  expr_let x258 := x255 * 1 (* : uint8_t *) in
+  expr_let x259 := x254 * 1 (* : uint64_t *) in
+  expr_let x260 := x237 * 1 (* : uint8_t *) in
+  expr_let x261 := x239 * 1 (* : uint8_t *) in
+  expr_let x262 := x240 * 1 (* : uint8_t *) in
+  expr_let x263 := x241 * 1 (* : uint8_t *) in
+  expr_let x264 := x242 * 1 (* : uint8_t *) in
+  expr_let x265 := x243 * 1 (* : uint8_t *) in
+  expr_let x266 := x244 * 1 (* : uint8_t *) in
+  expr_let x267 := x245 * 1 (* : uint8_t *) in
+  expr_let x268 := x246 * 1 (* : uint8_t *) in
+  expr_let x269 := x247 * 1 (* : uint8_t *) in
+  expr_let x270 := x248 * 1 (* : uint8_t *) in
+  expr_let x271 := x249 * 1 (* : uint8_t *) in
+  expr_let x272 := x250 * 1 (* : uint8_t *) in
+  expr_let x273 := x251 * 1 (* : uint8_t *) in
+  expr_let x274 := x252 * 1 (* : uint8_t *) in
+  expr_let x275 := x253 * 1 (* : uint8_t *) in
+  expr_let x276 := x259 >> 8 (* : uint64_t *) in
+  expr_let x277 := x259 & 255 (* : uint8_t *) in
+  expr_let x278 := x256 * 1 (* : uint64_t *) in
+  expr_let x279 := x257 * 1 (* : uint64_t *) in
+  expr_let x280 := x277 * 1 (* : uint8_t *) in
+  expr_let x281 := x276 * 1 (* : uint64_t *) in
+  expr_let x282 := x258 * 1 (* : uint8_t *) in
+  expr_let x283 := x260 * 1 (* : uint8_t *) in
+  expr_let x284 := x261 * 1 (* : uint8_t *) in
+  expr_let x285 := x262 * 1 (* : uint8_t *) in
+  expr_let x286 := x263 * 1 (* : uint8_t *) in
+  expr_let x287 := x264 * 1 (* : uint8_t *) in
+  expr_let x288 := x265 * 1 (* : uint8_t *) in
+  expr_let x289 := x266 * 1 (* : uint8_t *) in
+  expr_let x290 := x267 * 1 (* : uint8_t *) in
+  expr_let x291 := x268 * 1 (* : uint8_t *) in
+  expr_let x292 := x269 * 1 (* : uint8_t *) in
+  expr_let x293 := x270 * 1 (* : uint8_t *) in
+  expr_let x294 := x271 * 1 (* : uint8_t *) in
+  expr_let x295 := x272 * 1 (* : uint8_t *) in
+  expr_let x296 := x273 * 1 (* : uint8_t *) in
+  expr_let x297 := x274 * 1 (* : uint8_t *) in
+  expr_let x298 := x275 * 1 (* : uint8_t *) in
+  expr_let x299 := x281 >> 8 (* : uint1_t *) in
+  expr_let x300 := x281 & 255 (* : uint8_t *) in
+  expr_let x301 := x278 * 1 (* : uint64_t *) in
+  expr_let x302 := x279 * 1 (* : uint64_t *) in
+  expr_let x303 := x300 * 1 (* : uint8_t *) in
+  expr_let x304 := x299 * 1 (* : uint1_t *) in
+  expr_let x305 := x280 * 1 (* : uint8_t *) in
+  expr_let x306 := x282 * 1 (* : uint8_t *) in
+  expr_let x307 := x283 * 1 (* : uint8_t *) in
+  expr_let x308 := x284 * 1 (* : uint8_t *) in
+  expr_let x309 := x285 * 1 (* : uint8_t *) in
+  expr_let x310 := x286 * 1 (* : uint8_t *) in
+  expr_let x311 := x287 * 1 (* : uint8_t *) in
+  expr_let x312 := x288 * 1 (* : uint8_t *) in
+  expr_let x313 := x289 * 1 (* : uint8_t *) in
+  expr_let x314 := x290 * 1 (* : uint8_t *) in
+  expr_let x315 := x291 * 1 (* : uint8_t *) in
+  expr_let x316 := x292 * 1 (* : uint8_t *) in
+  expr_let x317 := x293 * 1 (* : uint8_t *) in
+  expr_let x318 := x294 * 1 (* : uint8_t *) in
+  expr_let x319 := x295 * 1 (* : uint8_t *) in
+  expr_let x320 := x296 * 1 (* : uint8_t *) in
+  expr_let x321 := x297 * 1 (* : uint8_t *) in
+  expr_let x322 := x298 * 1 (* : uint8_t *) in
+  expr_let x323 := x304 + x302 (* : uint64_t *) in
+  expr_let x324 := x323 >> 8 (* : uint64_t *) in
+  expr_let x325 := x323 & 255 (* : uint8_t *) in
+  expr_let x326 := x301 * 1 (* : uint64_t *) in
+  expr_let x327 := x325 * 1 (* : uint8_t *) in
+  expr_let x328 := x324 * 1 (* : uint64_t *) in
+  expr_let x329 := x303 * 1 (* : uint8_t *) in
+  expr_let x330 := x305 * 1 (* : uint8_t *) in
+  expr_let x331 := x306 * 1 (* : uint8_t *) in
+  expr_let x332 := x307 * 1 (* : uint8_t *) in
+  expr_let x333 := x308 * 1 (* : uint8_t *) in
+  expr_let x334 := x309 * 1 (* : uint8_t *) in
+  expr_let x335 := x310 * 1 (* : uint8_t *) in
+  expr_let x336 := x311 * 1 (* : uint8_t *) in
+  expr_let x337 := x312 * 1 (* : uint8_t *) in
+  expr_let x338 := x313 * 1 (* : uint8_t *) in
+  expr_let x339 := x314 * 1 (* : uint8_t *) in
+  expr_let x340 := x315 * 1 (* : uint8_t *) in
+  expr_let x341 := x316 * 1 (* : uint8_t *) in
+  expr_let x342 := x317 * 1 (* : uint8_t *) in
+  expr_let x343 := x318 * 1 (* : uint8_t *) in
+  expr_let x344 := x319 * 1 (* : uint8_t *) in
+  expr_let x345 := x320 * 1 (* : uint8_t *) in
+  expr_let x346 := x321 * 1 (* : uint8_t *) in
+  expr_let x347 := x322 * 1 (* : uint8_t *) in
+  expr_let x348 := x328 >> 8 (* : uint64_t *) in
+  expr_let x349 := x328 & 255 (* : uint8_t *) in
+  expr_let x350 := x326 * 1 (* : uint64_t *) in
+  expr_let x351 := x349 * 1 (* : uint8_t *) in
+  expr_let x352 := x348 * 1 (* : uint64_t *) in
+  expr_let x353 := x327 * 1 (* : uint8_t *) in
+  expr_let x354 := x329 * 1 (* : uint8_t *) in
+  expr_let x355 := x330 * 1 (* : uint8_t *) in
+  expr_let x356 := x331 * 1 (* : uint8_t *) in
+  expr_let x357 := x332 * 1 (* : uint8_t *) in
+  expr_let x358 := x333 * 1 (* : uint8_t *) in
+  expr_let x359 := x334 * 1 (* : uint8_t *) in
+  expr_let x360 := x335 * 1 (* : uint8_t *) in
+  expr_let x361 := x336 * 1 (* : uint8_t *) in
+  expr_let x362 := x337 * 1 (* : uint8_t *) in
+  expr_let x363 := x338 * 1 (* : uint8_t *) in
+  expr_let x364 := x339 * 1 (* : uint8_t *) in
+  expr_let x365 := x340 * 1 (* : uint8_t *) in
+  expr_let x366 := x341 * 1 (* : uint8_t *) in
+  expr_let x367 := x342 * 1 (* : uint8_t *) in
+  expr_let x368 := x343 * 1 (* : uint8_t *) in
+  expr_let x369 := x344 * 1 (* : uint8_t *) in
+  expr_let x370 := x345 * 1 (* : uint8_t *) in
+  expr_let x371 := x346 * 1 (* : uint8_t *) in
+  expr_let x372 := x347 * 1 (* : uint8_t *) in
+  expr_let x373 := x352 >> 8 (* : uint64_t *) in
+  expr_let x374 := x352 & 255 (* : uint8_t *) in
+  expr_let x375 := x350 * 1 (* : uint64_t *) in
+  expr_let x376 := x374 * 1 (* : uint8_t *) in
+  expr_let x377 := x373 * 1 (* : uint64_t *) in
+  expr_let x378 := x351 * 1 (* : uint8_t *) in
+  expr_let x379 := x353 * 1 (* : uint8_t *) in
+  expr_let x380 := x354 * 1 (* : uint8_t *) in
+  expr_let x381 := x355 * 1 (* : uint8_t *) in
+  expr_let x382 := x356 * 1 (* : uint8_t *) in
+  expr_let x383 := x357 * 1 (* : uint8_t *) in
+  expr_let x384 := x358 * 1 (* : uint8_t *) in
+  expr_let x385 := x359 * 1 (* : uint8_t *) in
+  expr_let x386 := x360 * 1 (* : uint8_t *) in
+  expr_let x387 := x361 * 1 (* : uint8_t *) in
+  expr_let x388 := x362 * 1 (* : uint8_t *) in
+  expr_let x389 := x363 * 1 (* : uint8_t *) in
+  expr_let x390 := x364 * 1 (* : uint8_t *) in
+  expr_let x391 := x365 * 1 (* : uint8_t *) in
+  expr_let x392 := x366 * 1 (* : uint8_t *) in
+  expr_let x393 := x367 * 1 (* : uint8_t *) in
+  expr_let x394 := x368 * 1 (* : uint8_t *) in
+  expr_let x395 := x369 * 1 (* : uint8_t *) in
+  expr_let x396 := x370 * 1 (* : uint8_t *) in
+  expr_let x397 := x371 * 1 (* : uint8_t *) in
+  expr_let x398 := x372 * 1 (* : uint8_t *) in
+  expr_let x399 := x377 >> 8 (* : uint64_t *) in
+  expr_let x400 := x377 & 255 (* : uint8_t *) in
+  expr_let x401 := x375 * 1 (* : uint64_t *) in
+  expr_let x402 := x400 * 1 (* : uint8_t *) in
+  expr_let x403 := x399 * 1 (* : uint64_t *) in
+  expr_let x404 := x376 * 1 (* : uint8_t *) in
+  expr_let x405 := x378 * 1 (* : uint8_t *) in
+  expr_let x406 := x379 * 1 (* : uint8_t *) in
+  expr_let x407 := x380 * 1 (* : uint8_t *) in
+  expr_let x408 := x381 * 1 (* : uint8_t *) in
+  expr_let x409 := x382 * 1 (* : uint8_t *) in
+  expr_let x410 := x383 * 1 (* : uint8_t *) in
+  expr_let x411 := x384 * 1 (* : uint8_t *) in
+  expr_let x412 := x385 * 1 (* : uint8_t *) in
+  expr_let x413 := x386 * 1 (* : uint8_t *) in
+  expr_let x414 := x387 * 1 (* : uint8_t *) in
+  expr_let x415 := x388 * 1 (* : uint8_t *) in
+  expr_let x416 := x389 * 1 (* : uint8_t *) in
+  expr_let x417 := x390 * 1 (* : uint8_t *) in
+  expr_let x418 := x391 * 1 (* : uint8_t *) in
+  expr_let x419 := x392 * 1 (* : uint8_t *) in
+  expr_let x420 := x393 * 1 (* : uint8_t *) in
+  expr_let x421 := x394 * 1 (* : uint8_t *) in
+  expr_let x422 := x395 * 1 (* : uint8_t *) in
+  expr_let x423 := x396 * 1 (* : uint8_t *) in
+  expr_let x424 := x397 * 1 (* : uint8_t *) in
+  expr_let x425 := x398 * 1 (* : uint8_t *) in
+  expr_let x426 := x403 >> 8 (* : uint64_t *) in
+  expr_let x427 := x403 & 255 (* : uint8_t *) in
+  expr_let x428 := x401 * 1 (* : uint64_t *) in
+  expr_let x429 := x427 * 1 (* : uint8_t *) in
+  expr_let x430 := x426 * 1 (* : uint64_t *) in
+  expr_let x431 := x402 * 1 (* : uint8_t *) in
+  expr_let x432 := x404 * 1 (* : uint8_t *) in
+  expr_let x433 := x405 * 1 (* : uint8_t *) in
+  expr_let x434 := x406 * 1 (* : uint8_t *) in
+  expr_let x435 := x407 * 1 (* : uint8_t *) in
+  expr_let x436 := x408 * 1 (* : uint8_t *) in
+  expr_let x437 := x409 * 1 (* : uint8_t *) in
+  expr_let x438 := x410 * 1 (* : uint8_t *) in
+  expr_let x439 := x411 * 1 (* : uint8_t *) in
+  expr_let x440 := x412 * 1 (* : uint8_t *) in
+  expr_let x441 := x413 * 1 (* : uint8_t *) in
+  expr_let x442 := x414 * 1 (* : uint8_t *) in
+  expr_let x443 := x415 * 1 (* : uint8_t *) in
+  expr_let x444 := x416 * 1 (* : uint8_t *) in
+  expr_let x445 := x417 * 1 (* : uint8_t *) in
+  expr_let x446 := x418 * 1 (* : uint8_t *) in
+  expr_let x447 := x419 * 1 (* : uint8_t *) in
+  expr_let x448 := x420 * 1 (* : uint8_t *) in
+  expr_let x449 := x421 * 1 (* : uint8_t *) in
+  expr_let x450 := x422 * 1 (* : uint8_t *) in
+  expr_let x451 := x423 * 1 (* : uint8_t *) in
+  expr_let x452 := x424 * 1 (* : uint8_t *) in
+  expr_let x453 := x425 * 1 (* : uint8_t *) in
+  expr_let x454 := x430 >> 8 (* : uint8_t *) in
+  expr_let x455 := x430 & 255 (* : uint8_t *) in
+  expr_let x456 := x428 * 1 (* : uint64_t *) in
+  expr_let x457 := x455 * 1 (* : uint8_t *) in
+  expr_let x458 := x454 * 1 (* : uint8_t *) in
+  expr_let x459 := x429 * 1 (* : uint8_t *) in
+  expr_let x460 := x431 * 1 (* : uint8_t *) in
+  expr_let x461 := x432 * 1 (* : uint8_t *) in
+  expr_let x462 := x433 * 1 (* : uint8_t *) in
+  expr_let x463 := x434 * 1 (* : uint8_t *) in
+  expr_let x464 := x435 * 1 (* : uint8_t *) in
+  expr_let x465 := x436 * 1 (* : uint8_t *) in
+  expr_let x466 := x437 * 1 (* : uint8_t *) in
+  expr_let x467 := x438 * 1 (* : uint8_t *) in
+  expr_let x468 := x439 * 1 (* : uint8_t *) in
+  expr_let x469 := x440 * 1 (* : uint8_t *) in
+  expr_let x470 := x441 * 1 (* : uint8_t *) in
+  expr_let x471 := x442 * 1 (* : uint8_t *) in
+  expr_let x472 := x443 * 1 (* : uint8_t *) in
+  expr_let x473 := x444 * 1 (* : uint8_t *) in
+  expr_let x474 := x445 * 1 (* : uint8_t *) in
+  expr_let x475 := x446 * 1 (* : uint8_t *) in
+  expr_let x476 := x447 * 1 (* : uint8_t *) in
+  expr_let x477 := x448 * 1 (* : uint8_t *) in
+  expr_let x478 := x449 * 1 (* : uint8_t *) in
+  expr_let x479 := x450 * 1 (* : uint8_t *) in
+  expr_let x480 := x451 * 1 (* : uint8_t *) in
+  expr_let x481 := x452 * 1 (* : uint8_t *) in
+  expr_let x482 := x453 * 1 (* : uint8_t *) in
+  expr_let x483 := x458 + x456 (* : uint64_t *) in
+  expr_let x484 := x483 >> 8 (* : uint64_t *) in
+  expr_let x485 := x483 & 255 (* : uint8_t *) in
+  expr_let x486 := x485 * 1 (* : uint8_t *) in
+  expr_let x487 := x484 * 1 (* : uint64_t *) in
+  expr_let x488 := x457 * 1 (* : uint8_t *) in
+  expr_let x489 := x459 * 1 (* : uint8_t *) in
+  expr_let x490 := x460 * 1 (* : uint8_t *) in
+  expr_let x491 := x461 * 1 (* : uint8_t *) in
+  expr_let x492 := x462 * 1 (* : uint8_t *) in
+  expr_let x493 := x463 * 1 (* : uint8_t *) in
+  expr_let x494 := x464 * 1 (* : uint8_t *) in
+  expr_let x495 := x465 * 1 (* : uint8_t *) in
+  expr_let x496 := x466 * 1 (* : uint8_t *) in
+  expr_let x497 := x467 * 1 (* : uint8_t *) in
+  expr_let x498 := x468 * 1 (* : uint8_t *) in
+  expr_let x499 := x469 * 1 (* : uint8_t *) in
+  expr_let x500 := x470 * 1 (* : uint8_t *) in
+  expr_let x501 := x471 * 1 (* : uint8_t *) in
+  expr_let x502 := x472 * 1 (* : uint8_t *) in
+  expr_let x503 := x473 * 1 (* : uint8_t *) in
+  expr_let x504 := x474 * 1 (* : uint8_t *) in
+  expr_let x505 := x475 * 1 (* : uint8_t *) in
+  expr_let x506 := x476 * 1 (* : uint8_t *) in
+  expr_let x507 := x477 * 1 (* : uint8_t *) in
+  expr_let x508 := x478 * 1 (* : uint8_t *) in
+  expr_let x509 := x479 * 1 (* : uint8_t *) in
+  expr_let x510 := x480 * 1 (* : uint8_t *) in
+  expr_let x511 := x481 * 1 (* : uint8_t *) in
+  expr_let x512 := x482 * 1 (* : uint8_t *) in
+  expr_let x513 := x487 >> 8 (* : uint64_t *) in
+  expr_let x514 := x487 & 255 (* : uint8_t *) in
+  expr_let x515 := x514 * 1 (* : uint8_t *) in
+  expr_let x516 := x513 * 1 (* : uint64_t *) in
+  expr_let x517 := x486 * 1 (* : uint8_t *) in
+  expr_let x518 := x488 * 1 (* : uint8_t *) in
+  expr_let x519 := x489 * 1 (* : uint8_t *) in
+  expr_let x520 := x490 * 1 (* : uint8_t *) in
+  expr_let x521 := x491 * 1 (* : uint8_t *) in
+  expr_let x522 := x492 * 1 (* : uint8_t *) in
+  expr_let x523 := x493 * 1 (* : uint8_t *) in
+  expr_let x524 := x494 * 1 (* : uint8_t *) in
+  expr_let x525 := x495 * 1 (* : uint8_t *) in
+  expr_let x526 := x496 * 1 (* : uint8_t *) in
+  expr_let x527 := x497 * 1 (* : uint8_t *) in
+  expr_let x528 := x498 * 1 (* : uint8_t *) in
+  expr_let x529 := x499 * 1 (* : uint8_t *) in
+  expr_let x530 := x500 * 1 (* : uint8_t *) in
+  expr_let x531 := x501 * 1 (* : uint8_t *) in
+  expr_let x532 := x502 * 1 (* : uint8_t *) in
+  expr_let x533 := x503 * 1 (* : uint8_t *) in
+  expr_let x534 := x504 * 1 (* : uint8_t *) in
+  expr_let x535 := x505 * 1 (* : uint8_t *) in
+  expr_let x536 := x506 * 1 (* : uint8_t *) in
+  expr_let x537 := x507 * 1 (* : uint8_t *) in
+  expr_let x538 := x508 * 1 (* : uint8_t *) in
+  expr_let x539 := x509 * 1 (* : uint8_t *) in
+  expr_let x540 := x510 * 1 (* : uint8_t *) in
+  expr_let x541 := x511 * 1 (* : uint8_t *) in
+  expr_let x542 := x512 * 1 (* : uint8_t *) in
+  expr_let x543 := x516 >> 8 (* : uint64_t *) in
+  expr_let x544 := x516 & 255 (* : uint8_t *) in
+  expr_let x545 := x544 * 1 (* : uint8_t *) in
+  expr_let x546 := x543 * 1 (* : uint64_t *) in
+  expr_let x547 := x515 * 1 (* : uint8_t *) in
+  expr_let x548 := x517 * 1 (* : uint8_t *) in
+  expr_let x549 := x518 * 1 (* : uint8_t *) in
+  expr_let x550 := x519 * 1 (* : uint8_t *) in
+  expr_let x551 := x520 * 1 (* : uint8_t *) in
+  expr_let x552 := x521 * 1 (* : uint8_t *) in
+  expr_let x553 := x522 * 1 (* : uint8_t *) in
+  expr_let x554 := x523 * 1 (* : uint8_t *) in
+  expr_let x555 := x524 * 1 (* : uint8_t *) in
+  expr_let x556 := x525 * 1 (* : uint8_t *) in
+  expr_let x557 := x526 * 1 (* : uint8_t *) in
+  expr_let x558 := x527 * 1 (* : uint8_t *) in
+  expr_let x559 := x528 * 1 (* : uint8_t *) in
+  expr_let x560 := x529 * 1 (* : uint8_t *) in
+  expr_let x561 := x530 * 1 (* : uint8_t *) in
+  expr_let x562 := x531 * 1 (* : uint8_t *) in
+  expr_let x563 := x532 * 1 (* : uint8_t *) in
+  expr_let x564 := x533 * 1 (* : uint8_t *) in
+  expr_let x565 := x534 * 1 (* : uint8_t *) in
+  expr_let x566 := x535 * 1 (* : uint8_t *) in
+  expr_let x567 := x536 * 1 (* : uint8_t *) in
+  expr_let x568 := x537 * 1 (* : uint8_t *) in
+  expr_let x569 := x538 * 1 (* : uint8_t *) in
+  expr_let x570 := x539 * 1 (* : uint8_t *) in
+  expr_let x571 := x540 * 1 (* : uint8_t *) in
+  expr_let x572 := x541 * 1 (* : uint8_t *) in
+  expr_let x573 := x542 * 1 (* : uint8_t *) in
+  expr_let x574 := x546 >> 8 (* : uint64_t *) in
+  expr_let x575 := x546 & 255 (* : uint8_t *) in
+  expr_let x576 := x575 * 1 (* : uint8_t *) in
+  expr_let x577 := x574 * 1 (* : uint64_t *) in
+  expr_let x578 := x545 * 1 (* : uint8_t *) in
+  expr_let x579 := x547 * 1 (* : uint8_t *) in
+  expr_let x580 := x548 * 1 (* : uint8_t *) in
+  expr_let x581 := x549 * 1 (* : uint8_t *) in
+  expr_let x582 := x550 * 1 (* : uint8_t *) in
+  expr_let x583 := x551 * 1 (* : uint8_t *) in
+  expr_let x584 := x552 * 1 (* : uint8_t *) in
+  expr_let x585 := x553 * 1 (* : uint8_t *) in
+  expr_let x586 := x554 * 1 (* : uint8_t *) in
+  expr_let x587 := x555 * 1 (* : uint8_t *) in
+  expr_let x588 := x556 * 1 (* : uint8_t *) in
+  expr_let x589 := x557 * 1 (* : uint8_t *) in
+  expr_let x590 := x558 * 1 (* : uint8_t *) in
+  expr_let x591 := x559 * 1 (* : uint8_t *) in
+  expr_let x592 := x560 * 1 (* : uint8_t *) in
+  expr_let x593 := x561 * 1 (* : uint8_t *) in
+  expr_let x594 := x562 * 1 (* : uint8_t *) in
+  expr_let x595 := x563 * 1 (* : uint8_t *) in
+  expr_let x596 := x564 * 1 (* : uint8_t *) in
+  expr_let x597 := x565 * 1 (* : uint8_t *) in
+  expr_let x598 := x566 * 1 (* : uint8_t *) in
+  expr_let x599 := x567 * 1 (* : uint8_t *) in
+  expr_let x600 := x568 * 1 (* : uint8_t *) in
+  expr_let x601 := x569 * 1 (* : uint8_t *) in
+  expr_let x602 := x570 * 1 (* : uint8_t *) in
+  expr_let x603 := x571 * 1 (* : uint8_t *) in
+  expr_let x604 := x572 * 1 (* : uint8_t *) in
+  expr_let x605 := x573 * 1 (* : uint8_t *) in
+  expr_let x606 := x577 >> 8 (* : uint64_t *) in
+  expr_let x607 := x577 & 255 (* : uint8_t *) in
+  expr_let x608 := x607 * 1 (* : uint8_t *) in
+  expr_let x609 := x606 * 1 (* : uint64_t *) in
+  expr_let x610 := x576 * 1 (* : uint8_t *) in
+  expr_let x611 := x578 * 1 (* : uint8_t *) in
+  expr_let x612 := x579 * 1 (* : uint8_t *) in
+  expr_let x613 := x580 * 1 (* : uint8_t *) in
+  expr_let x614 := x581 * 1 (* : uint8_t *) in
+  expr_let x615 := x582 * 1 (* : uint8_t *) in
+  expr_let x616 := x583 * 1 (* : uint8_t *) in
+  expr_let x617 := x584 * 1 (* : uint8_t *) in
+  expr_let x618 := x585 * 1 (* : uint8_t *) in
+  expr_let x619 := x586 * 1 (* : uint8_t *) in
+  expr_let x620 := x587 * 1 (* : uint8_t *) in
+  expr_let x621 := x588 * 1 (* : uint8_t *) in
+  expr_let x622 := x589 * 1 (* : uint8_t *) in
+  expr_let x623 := x590 * 1 (* : uint8_t *) in
+  expr_let x624 := x591 * 1 (* : uint8_t *) in
+  expr_let x625 := x592 * 1 (* : uint8_t *) in
+  expr_let x626 := x593 * 1 (* : uint8_t *) in
+  expr_let x627 := x594 * 1 (* : uint8_t *) in
+  expr_let x628 := x595 * 1 (* : uint8_t *) in
+  expr_let x629 := x596 * 1 (* : uint8_t *) in
+  expr_let x630 := x597 * 1 (* : uint8_t *) in
+  expr_let x631 := x598 * 1 (* : uint8_t *) in
+  expr_let x632 := x599 * 1 (* : uint8_t *) in
+  expr_let x633 := x600 * 1 (* : uint8_t *) in
+  expr_let x634 := x601 * 1 (* : uint8_t *) in
+  expr_let x635 := x602 * 1 (* : uint8_t *) in
+  expr_let x636 := x603 * 1 (* : uint8_t *) in
+  expr_let x637 := x604 * 1 (* : uint8_t *) in
+  expr_let x638 := x605 * 1 (* : uint8_t *) in
+  expr_let x639 := x609 >> 8 (* : uint8_t *) in
+  expr_let x640 := x609 & 255 (* : uint8_t *) in
+  expr_let x641 := x640 * 1 (* : uint8_t *) in
+  expr_let x642 := x639 * 1 (* : uint8_t *) in
+  expr_let x643 := x608 * 1 (* : uint8_t *) in
+  expr_let x644 := x610 * 1 (* : uint8_t *) in
+  expr_let x645 := x611 * 1 (* : uint8_t *) in
+  expr_let x646 := x612 * 1 (* : uint8_t *) in
+  expr_let x647 := x613 * 1 (* : uint8_t *) in
+  expr_let x648 := x614 * 1 (* : uint8_t *) in
+  expr_let x649 := x615 * 1 (* : uint8_t *) in
+  expr_let x650 := x616 * 1 (* : uint8_t *) in
+  expr_let x651 := x617 * 1 (* : uint8_t *) in
+  expr_let x652 := x618 * 1 (* : uint8_t *) in
+  expr_let x653 := x619 * 1 (* : uint8_t *) in
+  expr_let x654 := x620 * 1 (* : uint8_t *) in
+  expr_let x655 := x621 * 1 (* : uint8_t *) in
+  expr_let x656 := x622 * 1 (* : uint8_t *) in
+  expr_let x657 := x623 * 1 (* : uint8_t *) in
+  expr_let x658 := x624 * 1 (* : uint8_t *) in
+  expr_let x659 := x625 * 1 (* : uint8_t *) in
+  expr_let x660 := x626 * 1 (* : uint8_t *) in
+  expr_let x661 := x627 * 1 (* : uint8_t *) in
+  expr_let x662 := x628 * 1 (* : uint8_t *) in
+  expr_let x663 := x629 * 1 (* : uint8_t *) in
+  expr_let x664 := x630 * 1 (* : uint8_t *) in
+  expr_let x665 := x631 * 1 (* : uint8_t *) in
+  expr_let x666 := x632 * 1 (* : uint8_t *) in
+  expr_let x667 := x633 * 1 (* : uint8_t *) in
+  expr_let x668 := x634 * 1 (* : uint8_t *) in
+  expr_let x669 := x635 * 1 (* : uint8_t *) in
+  expr_let x670 := x636 * 1 (* : uint8_t *) in
+  expr_let x671 := x637 * 1 (* : uint8_t *) in
+  expr_let x672 := x638 * 1 (* : uint8_t *) in
+  expr_let x673 := x642 * 1 (* : uint8_t *) in
+  expr_let x674 := x641 * 1 (* : uint8_t *) in
+  expr_let x675 := x643 * 1 (* : uint8_t *) in
+  expr_let x676 := x644 * 1 (* : uint8_t *) in
+  expr_let x677 := x645 * 1 (* : uint8_t *) in
+  expr_let x678 := x646 * 1 (* : uint8_t *) in
+  expr_let x679 := x647 * 1 (* : uint8_t *) in
+  expr_let x680 := x648 * 1 (* : uint8_t *) in
+  expr_let x681 := x649 * 1 (* : uint8_t *) in
+  expr_let x682 := x650 * 1 (* : uint8_t *) in
+  expr_let x683 := x651 * 1 (* : uint8_t *) in
+  expr_let x684 := x652 * 1 (* : uint8_t *) in
+  expr_let x685 := x653 * 1 (* : uint8_t *) in
+  expr_let x686 := x654 * 1 (* : uint8_t *) in
+  expr_let x687 := x655 * 1 (* : uint8_t *) in
+  expr_let x688 := x656 * 1 (* : uint8_t *) in
+  expr_let x689 := x657 * 1 (* : uint8_t *) in
+  expr_let x690 := x658 * 1 (* : uint8_t *) in
+  expr_let x691 := x659 * 1 (* : uint8_t *) in
+  expr_let x692 := x660 * 1 (* : uint8_t *) in
+  expr_let x693 := x661 * 1 (* : uint8_t *) in
+  expr_let x694 := x662 * 1 (* : uint8_t *) in
+  expr_let x695 := x663 * 1 (* : uint8_t *) in
+  expr_let x696 := x664 * 1 (* : uint8_t *) in
+  expr_let x697 := x665 * 1 (* : uint8_t *) in
+  expr_let x698 := x666 * 1 (* : uint8_t *) in
+  expr_let x699 := x667 * 1 (* : uint8_t *) in
+  expr_let x700 := x668 * 1 (* : uint8_t *) in
+  expr_let x701 := x669 * 1 (* : uint8_t *) in
+  expr_let x702 := x670 * 1 (* : uint8_t *) in
+  expr_let x703 := x671 * 1 (* : uint8_t *) in
+  expr_let x704 := x672 * 1 (* : uint8_t *) in
+  expr_let x705 := Z.add_with_get_carry(256, 0, 0, x704) (* : uint8_t, uint1_t *) in
+  expr_let x706 := Z.add_with_get_carry(256, x705₂, 0, x703) (* : uint8_t, uint1_t *) in
+  expr_let x707 := Z.add_with_get_carry(256, x706₂, 0, x702) (* : uint8_t, uint1_t *) in
+  expr_let x708 := Z.add_with_get_carry(256, x707₂, 0, x701) (* : uint8_t, uint1_t *) in
+  expr_let x709 := Z.add_with_get_carry(256, x708₂, 0, x700) (* : uint8_t, uint1_t *) in
+  expr_let x710 := Z.add_with_get_carry(256, x709₂, 0, x699) (* : uint8_t, uint1_t *) in
+  expr_let x711 := Z.add_with_get_carry(256, x710₂, 0, x698) (* : uint8_t, uint1_t *) in
+  expr_let x712 := Z.add_with_get_carry(256, x711₂, 0, x697) (* : uint8_t, uint1_t *) in
+  expr_let x713 := Z.add_with_get_carry(256, x712₂, 0, x696) (* : uint8_t, uint1_t *) in
+  expr_let x714 := Z.add_with_get_carry(256, x713₂, 0, x695) (* : uint8_t, uint1_t *) in
+  expr_let x715 := Z.add_with_get_carry(256, x714₂, 0, x694) (* : uint8_t, uint1_t *) in
+  expr_let x716 := Z.add_with_get_carry(256, x715₂, 0, x693) (* : uint8_t, uint1_t *) in
+  expr_let x717 := Z.add_with_get_carry(256, x716₂, 0, x692) (* : uint8_t, uint1_t *) in
+  expr_let x718 := Z.add_with_get_carry(256, x717₂, 0, x691) (* : uint8_t, uint1_t *) in
+  expr_let x719 := Z.add_with_get_carry(256, x718₂, 0, x690) (* : uint8_t, uint1_t *) in
+  expr_let x720 := Z.add_with_get_carry(256, x719₂, 0, x689) (* : uint8_t, uint1_t *) in
+  expr_let x721 := Z.add_with_get_carry(256, x720₂, 0, x688) (* : uint8_t, uint1_t *) in
+  expr_let x722 := Z.add_with_get_carry(256, x721₂, 0, x687) (* : uint8_t, uint1_t *) in
+  expr_let x723 := Z.add_with_get_carry(256, x722₂, 0, x686) (* : uint8_t, uint1_t *) in
+  expr_let x724 := Z.add_with_get_carry(256, x723₂, 0, x685) (* : uint8_t, uint1_t *) in
+  expr_let x725 := Z.add_with_get_carry(256, x724₂, 0, x684) (* : uint8_t, uint1_t *) in
+  expr_let x726 := Z.add_with_get_carry(256, x725₂, 0, x683) (* : uint8_t, uint1_t *) in
+  expr_let x727 := Z.add_with_get_carry(256, x726₂, 0, x682) (* : uint8_t, uint1_t *) in
+  expr_let x728 := Z.add_with_get_carry(256, x727₂, 0, x681) (* : uint8_t, uint1_t *) in
+  expr_let x729 := Z.add_with_get_carry(256, x728₂, 0, x680) (* : uint8_t, uint1_t *) in
+  expr_let x730 := Z.add_with_get_carry(256, x729₂, 0, x679) (* : uint8_t, uint1_t *) in
+  expr_let x731 := Z.add_with_get_carry(256, x730₂, 0, x678) (* : uint8_t, uint1_t *) in
+  expr_let x732 := Z.add_with_get_carry(256, x731₂, 0, x677) (* : uint8_t, uint1_t *) in
+  expr_let x733 := Z.add_with_get_carry(256, x732₂, 0, x676) (* : uint8_t, uint1_t *) in
+  expr_let x734 := Z.add_with_get_carry(256, x733₂, 0, x675) (* : uint8_t, uint1_t *) in
+  expr_let x735 := Z.add_with_get_carry(256, x734₂, 0, x674) (* : uint8_t, uint1_t *) in
+  expr_let x736 := Z.add_with_get_carry(256, x735₂, 0, x673) (* : uint8_t, uint1_t *) in
+  x705₁ :: x706₁ :: x707₁ :: x708₁ :: x709₁ :: x710₁ :: x711₁ :: x712₁ :: x713₁ :: x714₁ :: x715₁ :: x716₁ :: x717₁ :: x718₁ :: x719₁ :: x720₁ :: x721₁ :: x722₁ :: x723₁ :: x724₁ :: x725₁ :: x726₁ :: x727₁ :: x728₁ :: x729₁ :: x730₁ :: x731₁ :: x732₁ :: x733₁ :: x734₁ :: x735₁ :: x736₁ :: []
+)
+Errors in converting fiat_25519_to_bytes to C:
+Final bounds check failed on second argument to Z.add_with_get_carry; expected an unsigned 51-bit number (uint64), but found a int64.
+Final bounds check failed on third argument to Z.add_with_get_carry; expected an unsigned 51-bit number (uint64), but found a int64.
+Final bounds check failed on second (carry) return value of Z.add_with_get_carry; expected an unsigned 1-bit number (uint1), but found a int1.