Skip to content

Instantly share code, notes, and snippets.

@andres-erbsen

andres-erbsen/sat_add.log Secret

Created May 8, 2023 21:22
Show Gist options
  • Save andres-erbsen/bbfb1994c4e8294be35c5ab59966faf2 to your computer and use it in GitHub Desktop.
Save andres-erbsen/bbfb1994c4e8294be35c5ab59966faf2 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sat_add.log
check_args
/* Autogenerated: './src/ExtractionOCaml/solinas_reduction' 25519 64 2^255-19 add */
/* curve description: 25519 */
/* machine_wordsize = 64 (from "64") */
/* requested operations: add */
/* s-c = 2^255 - [(1, 19)] (from "2^255-19") */
/* */
/* Computed values: */
/* */
#include <stdint.h>
#if defined(__GNUC__) || defined(__clang__)
# define FIAT_25519_FIAT_INLINE __inline__
#else
# define FIAT_25519_FIAT_INLINE
#endif
#if (-1 & 3) != 3
#error "This code only works on a two's complement system"
#endif
After rewriting PartialEvaluate:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
let x7 := 0 + x6₂ in
if if if 0 ≤ x3₁ then (λ ()_8, x3₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x4₁ then (λ ()_9, x4₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x5₁ then (λ ()_10, x5₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₁ then (λ ()_11, x6₁ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, if if 0 ≤ x7 then (λ ()_12, x7 ≤ 2^64-1) else (λ ()_12, false) then (λ ()_12, true) else (λ ()_12, false)) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false) then (λ ()_8,
let x9 := Z.mul_split((2^64), (38, x7)) in
let x10 := 1 * x9₂ in
let x11 := 1 * x9₁ in
let x12 := 1 * x6₁ in
let x13 := 1 * x5₁ in
let x14 := 1 * x4₁ in
let x15 := 1 * x3₁ in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x11))) in
let x17 := Z.add_with_get_carry((2^64), (x16₂, (x14, x10))) in
let x18 := Z.add_with_get_carry((2^64), (x17₂, (x13, 0))) in
let x19 := Z.add_with_get_carry((2^64), (x18₂, (x12, 0))) in
let x20 := Z.add_with_get_carry((2^64), (x19₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_21, x3₁ ≤ 2^64-1) else (λ ()_21, false) then (λ ()_21, if if 0 ≤ x4₁ then (λ ()_22, x4₁ ≤ 2^64-1) else (λ ()_22, false) then (λ ()_22, if if 0 ≤ x5₁ then (λ ()_23, x5₁ ≤ 2^64-1) else (λ ()_23, false) then (λ ()_23, if if 0 ≤ x6₁ then (λ ()_24, x6₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x7 then (λ ()_25, x7 ≤ 2^16-1) else (λ ()_25, false) then (λ ()_25, true) else (λ ()_25, false)) else (λ ()_24, false)) else (λ ()_23, false)) else (λ ()_22, false)) else (λ ()_21, false) then (λ ()_21,
let x22 := Z.zselect(x20₁, (0, 38)) in
let x23 := Z.add_with_get_carry((2^64), (0, (x22, x16₁))) in
if if if 0 ≤ x16₁ then (λ ()_24, x16₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x17₁ then (λ ()_25, x17₁ ≤ 2^64-1) else (λ ()_25, false) then (λ ()_25, if if 0 ≤ x18₁ then (λ ()_26, x18₁ ≤ 2^64-1) else (λ ()_26, false) then (λ ()_26, if if 0 ≤ x19₁ then (λ ()_27, x19₁ ≤ 2^64-1) else (λ ()_27, false) then (λ ()_27, if if 0 ≤ x20₁ then (λ ()_28, x20₁ ≤ 1) else (λ ()_28, false) then (λ ()_28, true) else (λ ()_28, false)) else (λ ()_27, false)) else (λ ()_26, false)) else (λ ()_25, false)) else (λ ()_24, false) then (λ ()_24, x23₁ :: x17₁ :: x18₁ :: x19₁ :: []) else (λ ()_24, 38 * x20₁ + x16₁ :: x17₁ :: x18₁ :: x19₁ :: [])
) else (λ ()_21, 2^256 * x7 + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_8,
let x9 := Z.mul_split((2^64), (38, x7)) in
let x10 := 1 * x9₂ in
let x11 := 1 * x9₁ in
let x12 := 1 * x6₁ in
let x13 := 1 * x5₁ in
let x14 := 1 * x4₁ in
let x15 := 1 * x3₁ in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x11))) in
let x17 := Z.add_with_get_carry((2^64), (x16₂, (x14, x10))) in
let x18 := Z.add_with_get_carry((2^64), (x17₂, (x13, 0))) in
let x19 := Z.add_with_get_carry((2^64), (x18₂, (x12, 0))) in
let x20 := Z.add_with_get_carry((2^64), (x19₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_21, x3₁ ≤ 2^64-1) else (λ ()_21, false) then (λ ()_21, if if 0 ≤ x4₁ then (λ ()_22, x4₁ ≤ 2^64-1) else (λ ()_22, false) then (λ ()_22, if if 0 ≤ x5₁ then (λ ()_23, x5₁ ≤ 2^64-1) else (λ ()_23, false) then (λ ()_23, if if 0 ≤ x6₁ then (λ ()_24, x6₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x7 then (λ ()_25, x7 ≤ 2^16-1) else (λ ()_25, false) then (λ ()_25, true) else (λ ()_25, false)) else (λ ()_24, false)) else (λ ()_23, false)) else (λ ()_22, false)) else (λ ()_21, false) then (λ ()_21,
let x22 := Z.zselect(x20₁, (0, 38)) in
let x23 := Z.add_with_get_carry((2^64), (0, (x22, (2^320 * (0 + x20₂) + x16₁)))) in
if if if 0 ≤ 2^320 * (0 + x20₂) + x16₁ then (λ ()_24, 2^320 * (0 + x20₂) + x16₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x17₁ then (λ ()_25, x17₁ ≤ 2^64-1) else (λ ()_25, false) then (λ ()_25, if if 0 ≤ x18₁ then (λ ()_26, x18₁ ≤ 2^64-1) else (λ ()_26, false) then (λ ()_26, if if 0 ≤ x19₁ then (λ ()_27, x19₁ ≤ 2^64-1) else (λ ()_27, false) then (λ ()_27, if if 0 ≤ x20₁ then (λ ()_28, x20₁ ≤ 1) else (λ ()_28, false) then (λ ()_28, true) else (λ ()_28, false)) else (λ ()_27, false)) else (λ ()_26, false)) else (λ ()_25, false)) else (λ ()_24, false) then (λ ()_24, x23₁ :: x17₁ :: x18₁ :: x19₁ :: []) else (λ ()_24, 38 * x20₁ + 2^320 * (0 + x20₂) + x16₁ :: x17₁ :: x18₁ :: x19₁ :: [])
) else (λ ()_21, 2^256 * x7 + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
)
)
After rewriting RewriteUnfoldValueBarrier:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
let x7 := 0 + x6₂ in
if if if 0 ≤ x3₁ then (λ ()_8, x3₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x4₁ then (λ ()_9, x4₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x5₁ then (λ ()_10, x5₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₁ then (λ ()_11, x6₁ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, if if 0 ≤ x7 then (λ ()_12, x7 ≤ 2^64-1) else (λ ()_12, false) then (λ ()_12, true) else (λ ()_12, false)) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false) then (λ ()_8,
let x9 := Z.mul_split((2^64), (38, x7)) in
let x10 := 1 * x9₂ in
let x11 := 1 * x9₁ in
let x12 := 1 * x6₁ in
let x13 := 1 * x5₁ in
let x14 := 1 * x4₁ in
let x15 := 1 * x3₁ in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x11))) in
let x17 := Z.add_with_get_carry((2^64), (x16₂, (x14, x10))) in
let x18 := Z.add_with_get_carry((2^64), (x17₂, (x13, 0))) in
let x19 := Z.add_with_get_carry((2^64), (x18₂, (x12, 0))) in
let x20 := Z.add_with_get_carry((2^64), (x19₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_21, x3₁ ≤ 2^64-1) else (λ ()_21, false) then (λ ()_21, if if 0 ≤ x4₁ then (λ ()_22, x4₁ ≤ 2^64-1) else (λ ()_22, false) then (λ ()_22, if if 0 ≤ x5₁ then (λ ()_23, x5₁ ≤ 2^64-1) else (λ ()_23, false) then (λ ()_23, if if 0 ≤ x6₁ then (λ ()_24, x6₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x7 then (λ ()_25, x7 ≤ 2^16-1) else (λ ()_25, false) then (λ ()_25, true) else (λ ()_25, false)) else (λ ()_24, false)) else (λ ()_23, false)) else (λ ()_22, false)) else (λ ()_21, false) then (λ ()_21,
let x22 := Z.zselect(x20₁, (0, 38)) in
let x23 := Z.add_with_get_carry((2^64), (0, (x22, x16₁))) in
if if if 0 ≤ x16₁ then (λ ()_24, x16₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x17₁ then (λ ()_25, x17₁ ≤ 2^64-1) else (λ ()_25, false) then (λ ()_25, if if 0 ≤ x18₁ then (λ ()_26, x18₁ ≤ 2^64-1) else (λ ()_26, false) then (λ ()_26, if if 0 ≤ x19₁ then (λ ()_27, x19₁ ≤ 2^64-1) else (λ ()_27, false) then (λ ()_27, if if 0 ≤ x20₁ then (λ ()_28, x20₁ ≤ 1) else (λ ()_28, false) then (λ ()_28, true) else (λ ()_28, false)) else (λ ()_27, false)) else (λ ()_26, false)) else (λ ()_25, false)) else (λ ()_24, false) then (λ ()_24, x23₁ :: x17₁ :: x18₁ :: x19₁ :: []) else (λ ()_24, 38 * x20₁ + x16₁ :: x17₁ :: x18₁ :: x19₁ :: [])
) else (λ ()_21, 2^256 * x7 + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_8,
let x9 := Z.mul_split((2^64), (38, x7)) in
let x10 := 1 * x9₂ in
let x11 := 1 * x9₁ in
let x12 := 1 * x6₁ in
let x13 := 1 * x5₁ in
let x14 := 1 * x4₁ in
let x15 := 1 * x3₁ in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x11))) in
let x17 := Z.add_with_get_carry((2^64), (x16₂, (x14, x10))) in
let x18 := Z.add_with_get_carry((2^64), (x17₂, (x13, 0))) in
let x19 := Z.add_with_get_carry((2^64), (x18₂, (x12, 0))) in
let x20 := Z.add_with_get_carry((2^64), (x19₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_21, x3₁ ≤ 2^64-1) else (λ ()_21, false) then (λ ()_21, if if 0 ≤ x4₁ then (λ ()_22, x4₁ ≤ 2^64-1) else (λ ()_22, false) then (λ ()_22, if if 0 ≤ x5₁ then (λ ()_23, x5₁ ≤ 2^64-1) else (λ ()_23, false) then (λ ()_23, if if 0 ≤ x6₁ then (λ ()_24, x6₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x7 then (λ ()_25, x7 ≤ 2^16-1) else (λ ()_25, false) then (λ ()_25, true) else (λ ()_25, false)) else (λ ()_24, false)) else (λ ()_23, false)) else (λ ()_22, false)) else (λ ()_21, false) then (λ ()_21,
let x22 := Z.zselect(x20₁, (0, 38)) in
let x23 := Z.add_with_get_carry((2^64), (0, (x22, (2^320 * (0 + x20₂) + x16₁)))) in
if if if 0 ≤ 2^320 * (0 + x20₂) + x16₁ then (λ ()_24, 2^320 * (0 + x20₂) + x16₁ ≤ 2^64-1) else (λ ()_24, false) then (λ ()_24, if if 0 ≤ x17₁ then (λ ()_25, x17₁ ≤ 2^64-1) else (λ ()_25, false) then (λ ()_25, if if 0 ≤ x18₁ then (λ ()_26, x18₁ ≤ 2^64-1) else (λ ()_26, false) then (λ ()_26, if if 0 ≤ x19₁ then (λ ()_27, x19₁ ≤ 2^64-1) else (λ ()_27, false) then (λ ()_27, if if 0 ≤ x20₁ then (λ ()_28, x20₁ ≤ 1) else (λ ()_28, false) then (λ ()_28, true) else (λ ()_28, false)) else (λ ()_27, false)) else (λ ()_26, false)) else (λ ()_25, false)) else (λ ()_24, false) then (λ ()_24, x23₁ :: x17₁ :: x18₁ :: x19₁ :: []) else (λ ()_24, 38 * x20₁ + 2^320 * (0 + x20₂) + x16₁ :: x17₁ :: x18₁ :: x19₁ :: [])
) else (λ ()_21, 2^256 * x7 + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
)
)
After rewriting RewriteArith_0:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
if if if 0 ≤ x3₁ then (λ ()_7, x3₁ ≤ 2^64-1) else (λ ()_7, false) then (λ ()_7, if if 0 ≤ x4₁ then (λ ()_8, x4₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x5₁ then (λ ()_9, x5₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x6₁ then (λ ()_10, x6₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₂ then (λ ()_11, x6₂ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x9₁))) in
if if if 0 ≤ x9₁ then (λ ()_17, x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, ((x13₂ << 0x140) + x9₁)))) in
if if if 0 ≤ (x13₂ << 0x140) + x9₁ then (λ ()_17, (x13₂ << 0x140) + x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + (x13₂ << 0x140) + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
)
)
After rewriting DCE for RewriteArith_0:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
if if if 0 ≤ x3₁ then (λ ()_7, x3₁ ≤ 2^64-1) else (λ ()_7, false) then (λ ()_7, if if 0 ≤ x4₁ then (λ ()_8, x4₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x5₁ then (λ ()_9, x5₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x6₁ then (λ ()_10, x6₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₂ then (λ ()_11, x6₂ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x9₁))) in
if if if 0 ≤ x9₁ then (λ ()_17, x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, ((x13₂ << 0x140) + x9₁)))) in
if if if 0 ≤ (x13₂ << 0x140) + x9₁ then (λ ()_17, (x13₂ << 0x140) + x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + (x13₂ << 0x140) + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
)
)
After rewriting LetBindReturn for RewriteArith_0:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
let x7 := if if if 0 ≤ x3₁ then (λ ()_7, x3₁ ≤ 2^64-1) else (λ ()_7, false) then (λ ()_7, if if 0 ≤ x4₁ then (λ ()_8, x4₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x5₁ then (λ ()_9, x5₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x6₁ then (λ ()_10, x6₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₂ then (λ ()_11, x6₂ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x9₁))) in
if if if 0 ≤ x9₁ then (λ ()_17, x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, ((x13₂ << 0x140) + x9₁)))) in
if if if 0 ≤ (x13₂ << 0x140) + x9₁ then (λ ()_17, (x13₂ << 0x140) + x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + (x13₂ << 0x140) + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) in
x7
)
After rewriting RewriteArith_0:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
let x7 := if if if 0 ≤ x3₁ then (λ ()_7, x3₁ ≤ 2^64-1) else (λ ()_7, false) then (λ ()_7, if if 0 ≤ x4₁ then (λ ()_8, x4₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x5₁ then (λ ()_9, x5₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x6₁ then (λ ()_10, x6₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₂ then (λ ()_11, x6₂ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, x9₁))) in
if if if 0 ≤ x9₁ then (λ ()_17, x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_7,
let x8 := Z.mul_split((2^64), (38, x6₂)) in
let x9 := Z.add_with_get_carry((2^64), (0, (x3₁, x8₁))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x4₁, x8₂))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x5₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (x6₁, 0))) in
let x13 := Z.add_with_get_carry((2^64), (x12₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_14, x3₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x4₁ then (λ ()_15, x4₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x5₁ then (λ ()_16, x5₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₁ then (λ ()_17, x6₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x6₂ then (λ ()_18, x6₂ ≤ 2^16-1) else (λ ()_18, false) then (λ ()_18, true) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false) then (λ ()_14,
let x15 := Z.zselect(x13₁, (0, 38)) in
let x16 := Z.add_with_get_carry((2^64), (0, (x15, ((x13₂ << 0x140) + x9₁)))) in
if if if 0 ≤ (x13₂ << 0x140) + x9₁ then (λ ()_17, (x13₂ << 0x140) + x9₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x10₁ then (λ ()_18, x10₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x11₁ then (λ ()_19, x11₁ ≤ 2^64-1) else (λ ()_19, false) then (λ ()_19, if if 0 ≤ x12₁ then (λ ()_20, x12₁ ≤ 2^64-1) else (λ ()_20, false) then (λ ()_20, if if 0 ≤ x13₁ then (λ ()_21, x13₁ ≤ 1) else (λ ()_21, false) then (λ ()_21, true) else (λ ()_21, false)) else (λ ()_20, false)) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false) then (λ ()_17, x16₁ :: x10₁ :: x11₁ :: x12₁ :: []) else (λ ()_17, 38 * x13₁ + (x13₂ << 0x140) + x9₁ :: x10₁ :: x11₁ :: x12₁ :: [])
) else (λ ()_14, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) in
x7
)
After rewriting DCE after RewriteArith_0:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
let x7 := if if if 0 ≤ x3₁ then (λ ()_7, x3₁ ≤ 2^64-1) else (λ ()_7, false) then (λ ()_7, if if 0 ≤ x4₁ then (λ ()_8, x4₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x5₁ then (λ ()_9, x5₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x6₁ then (λ ()_10, x6₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₂ then (λ ()_11, x6₂ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := Z.add_with_get_carry((2^64), (0, (x3₁, (Z.mul_split((2^64), (38, x6₂)))₁))) in
let x9 := Z.add_with_get_carry((2^64), (x8₂, (x4₁, (Z.mul_split((2^64), (38, x6₂)))₂))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x5₁, 0))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x6₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_13, x3₁ ≤ 2^64-1) else (λ ()_13, false) then (λ ()_13, if if 0 ≤ x4₁ then (λ ()_14, x4₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x5₁ then (λ ()_15, x5₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x6₁ then (λ ()_16, x6₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₂ then (λ ()_17, x6₂ ≤ 2^16-1) else (λ ()_17, false) then (λ ()_17, true) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false)) else (λ ()_13, false) then (λ ()_13,
let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), x8₁))) in
if if if 0 ≤ x8₁ then (λ ()_15, x8₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x9₁ then (λ ()_16, x9₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x10₁ then (λ ()_17, x10₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x11₁ then (λ ()_18, x11₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x12₁ then (λ ()_19, x12₁ ≤ 1) else (λ ()_19, false) then (λ ()_19, true) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false) then (λ ()_15, x14₁ :: x9₁ :: x10₁ :: x11₁ :: []) else (λ ()_15, 38 * x12₁ + x8₁ :: x9₁ :: x10₁ :: x11₁ :: [])
) else (λ ()_13, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_7,
let x8 := Z.add_with_get_carry((2^64), (0, (x3₁, (Z.mul_split((2^64), (38, x6₂)))₁))) in
let x9 := Z.add_with_get_carry((2^64), (x8₂, (x4₁, (Z.mul_split((2^64), (38, x6₂)))₂))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x5₁, 0))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x6₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_13, x3₁ ≤ 2^64-1) else (λ ()_13, false) then (λ ()_13, if if 0 ≤ x4₁ then (λ ()_14, x4₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x5₁ then (λ ()_15, x5₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x6₁ then (λ ()_16, x6₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₂ then (λ ()_17, x6₂ ≤ 2^16-1) else (λ ()_17, false) then (λ ()_17, true) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false)) else (λ ()_13, false) then (λ ()_13,
let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), ((x12₂ << 0x140) + x8₁)))) in
if if if 0 ≤ (x12₂ << 0x140) + x8₁ then (λ ()_15, (x12₂ << 0x140) + x8₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x9₁ then (λ ()_16, x9₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x10₁ then (λ ()_17, x10₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x11₁ then (λ ()_18, x11₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x12₁ then (λ ()_19, x12₁ ≤ 1) else (λ ()_19, false) then (λ ()_19, true) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false) then (λ ()_15, x14₁ :: x9₁ :: x10₁ :: x11₁ :: []) else (λ ()_15, 38 * x12₁ + (x12₂ << 0x140) + x8₁ :: x9₁ :: x10₁ :: x11₁ :: [])
) else (λ ()_13, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) in
x7
)
After rewriting RewriteArith_2⁸:
(λ x1 x2,
let x3 := Z.add_with_get_carry((2^64), (0, (x1[0], x2[0]))) in
let x4 := Z.add_with_get_carry((2^64), (x3₂, (x1[1], x2[1]))) in
let x5 := Z.add_with_get_carry((2^64), (x4₂, (x1[2], x2[2]))) in
let x6 := Z.add_with_get_carry((2^64), (x5₂, (x1[3], x2[3]))) in
let x7 := if if if 0 ≤ x3₁ then (λ ()_7, x3₁ ≤ 2^64-1) else (λ ()_7, false) then (λ ()_7, if if 0 ≤ x4₁ then (λ ()_8, x4₁ ≤ 2^64-1) else (λ ()_8, false) then (λ ()_8, if if 0 ≤ x5₁ then (λ ()_9, x5₁ ≤ 2^64-1) else (λ ()_9, false) then (λ ()_9, if if 0 ≤ x6₁ then (λ ()_10, x6₁ ≤ 2^64-1) else (λ ()_10, false) then (λ ()_10, if if 0 ≤ x6₂ then (λ ()_11, x6₂ ≤ 2^64-1) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := Z.add_with_get_carry((2^64), (0, (x3₁, (Z.mul_split((2^64), (38, x6₂)))₁))) in
let x9 := Z.add_with_get_carry((2^64), (x8₂, (x4₁, (Z.mul_split((2^64), (38, x6₂)))₂))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x5₁, 0))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x6₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_13, x3₁ ≤ 2^64-1) else (λ ()_13, false) then (λ ()_13, if if 0 ≤ x4₁ then (λ ()_14, x4₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x5₁ then (λ ()_15, x5₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x6₁ then (λ ()_16, x6₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₂ then (λ ()_17, x6₂ ≤ 2^16-1) else (λ ()_17, false) then (λ ()_17, true) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false)) else (λ ()_13, false) then (λ ()_13,
let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), x8₁))) in
if if if 0 ≤ x8₁ then (λ ()_15, x8₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x9₁ then (λ ()_16, x9₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x10₁ then (λ ()_17, x10₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x11₁ then (λ ()_18, x11₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x12₁ then (λ ()_19, x12₁ ≤ 1) else (λ ()_19, false) then (λ ()_19, true) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false) then (λ ()_15, x14₁ :: x9₁ :: x10₁ :: x11₁ :: []) else (λ ()_15, x12₁ * 38 + x8₁ :: x9₁ :: x10₁ :: x11₁ :: [])
) else (λ ()_13, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) else (λ ()_7,
let x8 := Z.add_with_get_carry((2^64), (0, (x3₁, (Z.mul_split((2^64), (38, x6₂)))₁))) in
let x9 := Z.add_with_get_carry((2^64), (x8₂, (x4₁, (Z.mul_split((2^64), (38, x6₂)))₂))) in
let x10 := Z.add_with_get_carry((2^64), (x9₂, (x5₁, 0))) in
let x11 := Z.add_with_get_carry((2^64), (x10₂, (x6₁, 0))) in
let x12 := Z.add_with_get_carry((2^64), (x11₂, (0, 0))) in
if if if 0 ≤ x3₁ then (λ ()_13, x3₁ ≤ 2^64-1) else (λ ()_13, false) then (λ ()_13, if if 0 ≤ x4₁ then (λ ()_14, x4₁ ≤ 2^64-1) else (λ ()_14, false) then (λ ()_14, if if 0 ≤ x5₁ then (λ ()_15, x5₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x6₁ then (λ ()_16, x6₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x6₂ then (λ ()_17, x6₂ ≤ 2^16-1) else (λ ()_17, false) then (λ ()_17, true) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false)) else (λ ()_13, false) then (λ ()_13,
let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), ((x12₂ << 0x140) + x8₁)))) in
if if if 0 ≤ (x12₂ << 0x140) + x8₁ then (λ ()_15, (x12₂ << 0x140) + x8₁ ≤ 2^64-1) else (λ ()_15, false) then (λ ()_15, if if 0 ≤ x9₁ then (λ ()_16, x9₁ ≤ 2^64-1) else (λ ()_16, false) then (λ ()_16, if if 0 ≤ x10₁ then (λ ()_17, x10₁ ≤ 2^64-1) else (λ ()_17, false) then (λ ()_17, if if 0 ≤ x11₁ then (λ ()_18, x11₁ ≤ 2^64-1) else (λ ()_18, false) then (λ ()_18, if if 0 ≤ x12₁ then (λ ()_19, x12₁ ≤ 1) else (λ ()_19, false) then (λ ()_19, true) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false) then (λ ()_15, x14₁ :: x9₁ :: x10₁ :: x11₁ :: []) else (λ ()_15, x12₁ * 38 + (x12₂ << 0x140) + x8₁ :: x9₁ :: x10₁ :: x11₁ :: [])
) else (λ ()_13, (x6₂ << 256) + x3₁ :: x4₁ :: x5₁ :: x6₁ :: [])
) in
x7
)
After rewriting CheckedPartialEvaluateWithBounds:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, ((uint64_t)(x1[0]), (uint64_t)(x2[0]))))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := if if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x3₁ then (λ ()_7, (uint64_t)(uint64_t, uint1_t)x3₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_7, false) then (λ ()_7, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x4₁ then (λ ()_8, (uint64_t)(uint64_t, uint1_t)x4₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_8, false) then (λ ()_8, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x5₁ then (λ ()_9, (uint64_t)(uint64_t, uint1_t)x5₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_9, false) then (λ ()_9, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x6₁ then (λ ()_10, (uint64_t)(uint64_t, uint1_t)x6₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_10, false) then (λ ()_10, if if (uint0_t)0 ≤ (uint1_t)(uint64_t, uint1_t)x6₂ then (λ ()_11, (uint1_t)(uint64_t, uint1_t)x6₂ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_11, false) then (λ ()_11, true) else (λ ()_11, false)) else (λ ()_10, false)) else (λ ()_9, false)) else (λ ()_8, false)) else (λ ()_7, false) then (λ ()_7,
let x8 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂)))₁)))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂)))₂)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint1_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, (uint0_t)0)))) (* : uint1_t, uint0_t *) in
if if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x3₁ then (λ ()_13, (uint64_t)(uint64_t, uint1_t)x3₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_13, false) then (λ ()_13, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x4₁ then (λ ()_14, (uint64_t)(uint64_t, uint1_t)x4₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_14, false) then (λ ()_14, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x5₁ then (λ ()_15, (uint64_t)(uint64_t, uint1_t)x5₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_15, false) then (λ ()_15, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x6₁ then (λ ()_16, (uint64_t)(uint64_t, uint1_t)x6₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_16, false) then (λ ()_16, if if (uint0_t)0 ≤ (uint1_t)(uint64_t, uint1_t)x6₂ then (λ ()_17, (uint1_t)(uint64_t, uint1_t)x6₂ ≤ ([0xffff ~> 0xffff])(2^16-1)) else (λ ()_17, false) then (λ ()_17, true) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false)) else (λ ()_13, false) then (λ ()_13,
let x14 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint1_t, uint0_t)x12₁, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁)))) (* : uint64_t, uint1_t *) in
if if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x8₁ then (λ ()_15, (uint64_t)(uint64_t, uint1_t)x8₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_15, false) then (λ ()_15, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x9₁ then (λ ()_16, (uint64_t)(uint64_t, uint1_t)x9₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_16, false) then (λ ()_16, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x10₁ then (λ ()_17, (uint64_t)(uint64_t, uint1_t)x10₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_17, false) then (λ ()_17, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x11₁ then (λ ()_18, (uint64_t)(uint64_t, uint1_t)x11₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_18, false) then (λ ()_18, if if (uint0_t)0 ≤ (uint1_t)(uint1_t, uint0_t)x12₁ then (λ ()_19, (uint1_t)(uint1_t, uint0_t)x12₁ ≤ ([0x1 ~> 0x1])1) else (λ ()_19, false) then (λ ()_19, true) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false) then (λ ()_15, (uint64_t)(uint64_t, uint1_t)x14₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []) else (λ ()_15, ([0x0 ~> 0x10000000000000025])(([0x0 ~> 0x26])((uint1_t)(uint1_t, uint0_t)x12₁ * ([0x26 ~> 0x26])38) + (uint64_t)(uint64_t, uint1_t)x8₁) :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: [])
) else (λ ()_13, ([0x0 ~> 0x1000000000000000000000000000000000000000000000000ffffffffffffffff])(([0x0 ~> 0x10000000000000000000000000000000000000000000000000000000000000000])((uint1_t)(uint64_t, uint1_t)x6₂ << ([0x100 ~> 0x100])256) + (uint64_t)(uint64_t, uint1_t)x3₁) :: (uint64_t)(uint64_t, uint1_t)x4₁ :: (uint64_t)(uint64_t, uint1_t)x5₁ :: (uint64_t)(uint64_t, uint1_t)x6₁ :: [])
) else (λ ()_7,
let x8 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂)))₁)))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂)))₂)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint1_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, (uint0_t)0)))) (* : uint1_t, uint0_t *) in
if if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x3₁ then (λ ()_13, (uint64_t)(uint64_t, uint1_t)x3₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_13, false) then (λ ()_13, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x4₁ then (λ ()_14, (uint64_t)(uint64_t, uint1_t)x4₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_14, false) then (λ ()_14, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x5₁ then (λ ()_15, (uint64_t)(uint64_t, uint1_t)x5₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_15, false) then (λ ()_15, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x6₁ then (λ ()_16, (uint64_t)(uint64_t, uint1_t)x6₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_16, false) then (λ ()_16, if if (uint0_t)0 ≤ (uint1_t)(uint64_t, uint1_t)x6₂ then (λ ()_17, (uint1_t)(uint64_t, uint1_t)x6₂ ≤ ([0xffff ~> 0xffff])(2^16-1)) else (λ ()_17, false) then (λ ()_17, true) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false)) else (λ ()_14, false)) else (λ ()_13, false) then (λ ()_13,
let x14 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint1_t, uint0_t)x12₁, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)((uint0_t)((uint0_t)(uint1_t, uint0_t)x12₂ << ([0x140 ~> 0x140])0x140) + (uint64_t)(uint64_t, uint1_t)x8₁))))) (* : uint64_t, uint1_t *) in
if if if (uint0_t)0 ≤ (uint64_t)((uint0_t)((uint0_t)(uint1_t, uint0_t)x12₂ << ([0x140 ~> 0x140])0x140) + (uint64_t)(uint64_t, uint1_t)x8₁) then (λ ()_15, (uint64_t)((uint0_t)((uint0_t)(uint1_t, uint0_t)x12₂ << ([0x140 ~> 0x140])0x140) + (uint64_t)(uint64_t, uint1_t)x8₁) ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_15, false) then (λ ()_15, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x9₁ then (λ ()_16, (uint64_t)(uint64_t, uint1_t)x9₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_16, false) then (λ ()_16, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x10₁ then (λ ()_17, (uint64_t)(uint64_t, uint1_t)x10₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_17, false) then (λ ()_17, if if (uint0_t)0 ≤ (uint64_t)(uint64_t, uint1_t)x11₁ then (λ ()_18, (uint64_t)(uint64_t, uint1_t)x11₁ ≤ ([0xffffffffffffffff ~> 0xffffffffffffffff])(2^64-1)) else (λ ()_18, false) then (λ ()_18, if if (uint0_t)0 ≤ (uint1_t)(uint1_t, uint0_t)x12₁ then (λ ()_19, (uint1_t)(uint1_t, uint0_t)x12₁ ≤ ([0x1 ~> 0x1])1) else (λ ()_19, false) then (λ ()_19, true) else (λ ()_19, false)) else (λ ()_18, false)) else (λ ()_17, false)) else (λ ()_16, false)) else (λ ()_15, false) then (λ ()_15, (uint64_t)(uint64_t, uint1_t)x14₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []) else (λ ()_15, ([0x0 ~> 0x10000000000000025])(([0x0 ~> 0x26])((uint1_t)(uint1_t, uint0_t)x12₁ * ([0x26 ~> 0x26])38) + (uint64_t)((uint0_t)((uint0_t)(uint1_t, uint0_t)x12₂ << ([0x140 ~> 0x140])0x140) + (uint64_t)(uint64_t, uint1_t)x8₁)) :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: [])
) else (λ ()_13, ([0x0 ~> 0x1000000000000000000000000000000000000000000000000ffffffffffffffff])(([0x0 ~> 0x10000000000000000000000000000000000000000000000000000000000000000])((uint1_t)(uint64_t, uint1_t)x6₂ << ([0x100 ~> 0x100])256) + (uint64_t)(uint64_t, uint1_t)x3₁) :: (uint64_t)(uint64_t, uint1_t)x4₁ :: (uint64_t)(uint64_t, uint1_t)x5₁ :: (uint64_t)(uint64_t, uint1_t)x6₁ :: [])
) in
x7
)
After rewriting RewriteArithWithCasts:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x11₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x13 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint64_t, uint1_t)x12₂, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x13₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: (uint64_t)(uint64_t, uint1_t)x12₁ :: []
)
After rewriting DCE for RewriteArithWithCasts:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
After rewriting LetBindReturn for RewriteArithWithCasts:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
After rewriting RewriteArithWithCasts:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
After rewriting DCE after RewriteArithWithCasts:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
After rewriting CheckedPartialEvaluateWithBounds 2:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := ([0x0 ~> 0x26], uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x26 ~> 0x26])38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : [0x0 ~> 0x26], uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, ([0x0 ~> 0x26])([0x0 ~> 0x26], uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0x26])(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, ([0x26 ~> 0x26])38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
After rewriting CheckedPartialEvaluateWithBounds 3:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := (uint64_t, uint0_t)(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : uint64_t, uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, (uint64_t)(uint64_t, uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, (uint0_t)0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, ((uint0_t)0, (uint64_t)38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
After rewriting RewriteStripLiteralCasts:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := (uint64_t, uint0_t)(Z.mul_split((2^64), (38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : uint64_t, uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, (uint64_t)(uint64_t, uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, 0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, 0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, 0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, (0, 38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
In fiat_25519_add:
Stringification failed on the syntax tree:
(λ x1 x2,
let x3 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, uint1_t *) in
let x4 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1]))))) (* : uint64_t, uint1_t *) in
let x5 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2]))))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3]))))) (* : uint64_t, uint1_t *) in
let x7 := (uint64_t, uint0_t)(Z.mul_split((2^64), (38, (uint1_t)(uint64_t, uint1_t)x6₂))) (* : uint64_t, uint0_t *) in
let x8 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(uint64_t, uint1_t)x3₁, (uint64_t)(uint64_t, uint0_t)x7₁))) (* : uint64_t, uint1_t *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x8₂, ((uint64_t)(uint64_t, uint1_t)x4₁, 0)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x9₂, ((uint64_t)(uint64_t, uint1_t)x5₁, 0)))) (* : uint64_t, uint1_t *) in
let x11 := (uint64_t, uint1_t)(Z.add_with_get_carry((2^64), ((uint1_t)(uint64_t, uint1_t)x10₂, ((uint64_t)(uint64_t, uint1_t)x6₁, 0)))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(Z.zselect((uint1_t)(uint64_t, uint1_t)x11₂, (0, 38))), (uint64_t)(uint64_t, uint1_t)x8₁))) (* : uint64_t, uint1_t *) in
(uint64_t)(uint64_t, uint1_t)x12₁ :: (uint64_t)(uint64_t, uint1_t)x9₁ :: (uint64_t)(uint64_t, uint1_t)x10₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: []
)
Which with some casts elided is:
(λ x1 x2,
let x3 := Z.add_get_carry((2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0]))) (* : uint64_t, uint1_t *) in
let x4 := Z.add_with_get_carry((2^64), ((uint1_t)x3₂, ((uint64_t)(x1[1]), (uint64_t)(x2[1])))) (* : uint64_t, uint1_t *) in
let x5 := Z.add_with_get_carry((2^64), ((uint1_t)x4₂, ((uint64_t)(x1[2]), (uint64_t)(x2[2])))) (* : uint64_t, uint1_t *) in
let x6 := Z.add_with_get_carry((2^64), ((uint1_t)x5₂, ((uint64_t)(x1[3]), (uint64_t)(x2[3])))) (* : uint64_t, uint1_t *) in
let x7 := Z.mul_split((2^64), (38, (uint1_t)x6₂)) (* : uint64_t, uint0_t *) in
let x8 := Z.add_get_carry((2^64), ((uint64_t)x3₁, (uint64_t)x7₁)) (* : uint64_t, uint1_t *) in
let x9 := Z.add_with_get_carry((2^64), ((uint1_t)x8₂, ((uint64_t)x4₁, 0))) (* : uint64_t, uint1_t *) in
let x10 := Z.add_with_get_carry((2^64), ((uint1_t)x9₂, ((uint64_t)x5₁, 0))) (* : uint64_t, uint1_t *) in
let x11 := Z.add_with_get_carry((2^64), ((uint1_t)x10₂, ((uint64_t)x6₁, 0))) (* : uint64_t, uint1_t *) in
let x12 := Z.add_get_carry((2^64), ((uint64_t)(Z.zselect((uint1_t)x11₂, (0, 38))), (uint64_t)x8₁)) (* : uint64_t, uint1_t *) in
x12₁ :: x9₁ :: x10₁ :: x11₁ :: []
)
Error in converting fiat_25519_add to C:
Invalid identifier in arithmetic expression Z.zselect
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment