Skip to content

Instantly share code, notes, and snippets.

@andres-erbsen

andres-erbsen/s.v Secret

Last active August 14, 2023 22:24
Show Gist options
  • Save andres-erbsen/e83ed379e3ca19dbcba38a8b05b91993 to your computer and use it in GitHub Desktop.
Save andres-erbsen/e83ed379e3ca19dbcba38a8b05b91993 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
s.v
Error Computed bounds (Some [Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], None, None, None]) are not tight enough (expected bounds not looser than (Some [Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff], Some [0x0 ~> 0xffffffffffffffff]])).
Found None where Some was expected
(Unprintible syntax tree used in bounds analysis)
Stringification failed on the syntax tree:
(λ x1 x2,
let x3 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x4 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[1])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x5 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x3₂, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x4₁))) (* : uint64_t, uint1_t *) in
let x6 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[2])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x7 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x5₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x4₂, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x6₁)))) (* : uint64_t, uint1_t *) in
let x8 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[3])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x9 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x7₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x6₂, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₁)))) (* : uint64_t, uint1_t *) in
let x10 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[0])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x11 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x5₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x10₁))) (* : uint64_t, uint1_t *) in
let x12 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[1])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x13 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x7₁, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x10₂))) (* : uint64_t, uint1_t *) in
let x14 := (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)x13₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x12₁)))) (* : uint64_t, uint1_t *) in
let x15 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[2])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x16 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x13₂, ((uint64_t)(uint64_t, uint1_t)x9₁, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x12₂)))) (* : uint64_t, uint1_t *) in
let x17 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x14₂, ((uint64_t)(uint64_t, uint1_t)x16₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x15₁)))) (* : uint64_t, uint1_t *) in
let x18 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[3])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x19 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x16₂, ((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂), ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x15₂)))) (* : uint64_t, uint1_t *) in
let x20 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x17₂, ((uint64_t)(uint64_t, uint1_t)x19₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₁)))) (* : uint64_t, uint1_t *) in
let x21 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[0])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x22 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x14₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x21₁))) (* : uint64_t, uint1_t *) in
let x23 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[1])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x24 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x17₁, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x21₂))) (* : uint64_t, uint1_t *) in
let x25 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x22₂, ((uint64_t)(uint64_t, uint1_t)x24₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x23₁)))) (* : uint64_t, uint1_t *) in
let x26 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[2])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x27 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x24₂, ((uint64_t)(uint64_t, uint1_t)x20₁, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x23₂)))) (* : uint64_t, uint1_t *) in
let x28 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x25₂, ((uint64_t)(uint64_t, uint1_t)x27₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x26₁)))) (* : uint64_t, uint1_t *) in
let x29 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[3])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x30 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x27₂, ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_30, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_30, false) then (λ ()_30, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_30, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)), ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x26₂))) in
let x31 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x28₂, (x30₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₁))) in
let x32 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[0])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x33 := (uint64_t, uint1_t)(Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(uint64_t, uint1_t)x25₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x32₁))) (* : uint64_t, uint1_t *) in
let x34 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[1])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x35 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, ((uint64_t)(uint64_t, uint1_t)x28₁, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x32₂)))) (* : uint64_t, uint1_t *) in
let x36 := (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x33₂, ((uint64_t)(uint64_t, uint1_t)x35₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x34₁)))) (* : uint64_t, uint1_t *) in
let x37 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[2])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x38 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x35₂, (x31₁, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x34₂))) in
let x39 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x36₂, (x38₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x37₁))) in
let x40 := (uint64_t, [0x0 ~> 0xfffffffffffffffe])(Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[3])))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x41 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x38₂, ((if if (uint0_t)0 ≤ ((uint64_t)(uint64_t, uint1_t)x14₁ + (((uint64_t)(uint64_t, uint1_t)x17₁ + (((uint64_t)(uint64_t, uint1_t)x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_41, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_41, false) then (λ ()_41, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_41, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[2]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 then (λ ()_41, ((uint64_t)(uint64_t, uint1_t)x14₁ + (((uint64_t)(uint64_t, uint1_t)x17₁ + (((uint64_t)(uint64_t, uint1_t)x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_42, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_42, false) then (λ ()_42, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_42, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[2]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_41, false) then (λ ()_41, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x31₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x30₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_41, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₂ + x30₂ + x31₂)), ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x37₂))) in
let x42 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x39₂, (x41₁, (uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x40₁))) in
let x43 := if if (uint0_t)0 ≤ ((uint64_t)(uint64_t, uint1_t)x25₁ + (((uint64_t)(uint64_t, uint1_t)x28₁ + ((x31₁ + ((if if (uint0_t)0 ≤ ((uint64_t)(uint64_t, uint1_t)x14₁ + (((uint64_t)(uint64_t, uint1_t)x17₁ + (((uint64_t)(uint64_t, uint1_t)x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_43, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_43, false) then (λ ()_43, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_43, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[2]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 then (λ ()_43, ((uint64_t)(uint64_t, uint1_t)x14₁ + (((uint64_t)(uint64_t, uint1_t)x17₁ + (((uint64_t)(uint64_t, uint1_t)x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_44, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_44, false) then (λ ()_44, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_44, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[2]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_43, false) then (λ ()_43, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x31₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x30₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_43, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₂ + x30₂ + x31₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[3]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 then (λ ()_43, ((uint64_t)(uint64_t, uint1_t)x25₁ + (((uint64_t)(uint64_t, uint1_t)x28₁ + ((x31₁ + ((if if (uint0_t)0 ≤ ((uint64_t)(uint64_t, uint1_t)x14₁ + (((uint64_t)(uint64_t, uint1_t)x17₁ + (((uint64_t)(uint64_t, uint1_t)x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_44, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_44, false) then (λ ()_44, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_44, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[2]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 then (λ ()_44, ((uint64_t)(uint64_t, uint1_t)x14₁ + (((uint64_t)(uint64_t, uint1_t)x17₁ + (((uint64_t)(uint64_t, uint1_t)x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) then (λ ()_45, (uint64_t)(([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint256_t)((uint64_t)(uint64_t, uint1_t)x5₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(uint64_t, uint1_t)x7₁ + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(uint64_t, uint1_t)x9₁ + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)((uint1_t)(uint64_t, uint1_t)x9₂ + ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x8₂) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[1]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_45, false) then (λ ()_45, (uint64_t, uint1_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x20₂, ((uint64_t)(uint64_t, uint0_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)(uint64_t, uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_45, (uint64_t)(([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x18₂ + (uint1_t)(uint64_t, uint1_t)x19₂) + (uint1_t)(uint64_t, uint1_t)x20₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[2]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_44, false) then (λ ()_44, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x31₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x30₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_44, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x29₂ + x30₂ + x31₂)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64) + ([0x0 ~> 0xfffffffffffffffeffffffffffffffffffffffffffffffffffffffffffffffff0000000000000001])((uint64_t)(x1[3]) * (uint256_t)((uint64_t)(x2[0]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000])((uint192_t)((uint64_t)(x2[1]) + ([0x0 ~> 0xffffffffffffffffffffffffffffffff0000000000000000])((uint128_t)((uint64_t)(x2[2]) + ([0x0 ~> 0xffffffffffffffff0000000000000000])((uint64_t)(x2[3]) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)) << ([0x40 ~> 0x40])64)))) >> ([0x100 ~> 0x100])256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_43, false) then (λ ()_43, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x42₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x41₂, (([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x40₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_43, ([0x0 ~> 0xfffffffffffffffe])(uint64_t, [0x0 ~> 0xfffffffffffffffe])x40₂ + x41₂ + x42₂) in
(uint64_t)(uint64_t, [0x0 ~> 0xfffffffffffffffe])x3₁ :: (uint64_t)(uint64_t, uint1_t)x11₁ :: (uint64_t)(uint64_t, uint1_t)x22₁ :: (uint64_t)(uint64_t, uint1_t)x33₁ :: (uint64_t)(uint64_t, uint1_t)x36₁ :: x39₁ :: x42₁ :: x43 :: []
)
Which with some casts elided is:
(λ x1 x2,
let x3 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[0]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x4 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[1]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x5 := Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (([0x0 ~> 0xfffffffffffffffe])x3₂, (uint64_t)x4₁)) (* : uint64_t, uint1_t *) in
let x6 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[2]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x7 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x5₂, (([0x0 ~> 0xfffffffffffffffe])x4₂, (uint64_t)x6₁))) (* : uint64_t, uint1_t *) in
let x8 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[0]), (uint64_t)(x2[3]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x9 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x7₂, (([0x0 ~> 0xfffffffffffffffe])x6₂, (uint64_t)x8₁))) (* : uint64_t, uint1_t *) in
let x10 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[0]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x11 := Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)x5₁, (uint64_t)x10₁)) (* : uint64_t, uint1_t *) in
let x12 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[1]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x13 := Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)x7₁, ([0x0 ~> 0xfffffffffffffffe])x10₂)) (* : uint64_t, uint1_t *) in
let x14 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x11₂, ((uint64_t)x13₁, (uint64_t)x12₁))) (* : uint64_t, uint1_t *) in
let x15 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[2]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x16 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x13₂, ((uint64_t)x9₁, ([0x0 ~> 0xfffffffffffffffe])x12₂))) (* : uint64_t, uint1_t *) in
let x17 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x14₂, ((uint64_t)x16₁, (uint64_t)x15₁))) (* : uint64_t, uint1_t *) in
let x18 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[1]), (uint64_t)(x2[3]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x19 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x16₂, ((uint64_t)(x9₂ + x8₂), ([0x0 ~> 0xfffffffffffffffe])x15₂))) (* : uint64_t, uint1_t *) in
let x20 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x17₂, ((uint64_t)x19₁, (uint64_t)x18₁))) (* : uint64_t, uint1_t *) in
let x21 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[0]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x22 := Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)x14₁, (uint64_t)x21₁)) (* : uint64_t, uint1_t *) in
let x23 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[1]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x24 := Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)x17₁, ([0x0 ~> 0xfffffffffffffffe])x21₂)) (* : uint64_t, uint1_t *) in
let x25 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x22₂, ((uint64_t)x24₁, (uint64_t)x23₁))) (* : uint64_t, uint1_t *) in
let x26 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[2]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x27 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x24₂, ((uint64_t)x20₁, ([0x0 ~> 0xfffffffffffffffe])x23₂))) (* : uint64_t, uint1_t *) in
let x28 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x25₂, ((uint64_t)x27₁, (uint64_t)x26₁))) (* : uint64_t, uint1_t *) in
let x29 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[2]), (uint64_t)(x2[3]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x30 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x27₂, ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_30, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_30, false) then (λ ()_30, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_30, x18₂ + x19₂ + x20₂)), ([0x0 ~> 0xfffffffffffffffe])x26₂))) in
let x31 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x28₂, (x30₁, (uint64_t)x29₁))) in
let x32 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[0]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x33 := Z.add_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)x25₁, (uint64_t)x32₁)) (* : uint64_t, uint1_t *) in
let x34 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[1]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x35 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint0_t)0, ((uint64_t)x28₁, ([0x0 ~> 0xfffffffffffffffe])x32₂))) (* : uint64_t, uint1_t *) in
let x36 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x33₂, ((uint64_t)x35₁, (uint64_t)x34₁))) (* : uint64_t, uint1_t *) in
let x37 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[2]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x38 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x35₂, (x31₁, ([0x0 ~> 0xfffffffffffffffe])x34₂))) in
let x39 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x36₂, (x38₁, (uint64_t)x37₁))) in
let x40 := Z.mul_split(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint64_t)(x1[3]), (uint64_t)(x2[3]))) (* : uint64_t, [0x0 ~> 0xfffffffffffffffe] *) in
let x41 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x38₂, ((if if (uint0_t)0 ≤ (x14₁ + ((x17₁ + ((x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_41, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_41, false) then (λ ()_41, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_41, x18₂ + x19₂ + x20₂)) << 64)) << 64)) << 64) + x1[2] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 then (λ ()_41, (x14₁ + ((x17₁ + ((x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_42, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_42, false) then (λ ()_42, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_42, x18₂ + x19₂ + x20₂)) << 64)) << 64)) << 64) + x1[2] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_41, false) then (λ ()_41, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x31₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x30₂, (([0x0 ~> 0xfffffffffffffffe])x29₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_41, x29₂ + x30₂ + x31₂)), ([0x0 ~> 0xfffffffffffffffe])x37₂))) in
let x42 := Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x39₂, (x41₁, (uint64_t)x40₁))) in
let x43 := if if (uint0_t)0 ≤ (x25₁ + ((x28₁ + ((x31₁ + ((if if (uint0_t)0 ≤ (x14₁ + ((x17₁ + ((x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_43, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_43, false) then (λ ()_43, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_43, x18₂ + x19₂ + x20₂)) << 64)) << 64)) << 64) + x1[2] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 then (λ ()_43, (x14₁ + ((x17₁ + ((x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_44, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_44, false) then (λ ()_44, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_44, x18₂ + x19₂ + x20₂)) << 64)) << 64)) << 64) + x1[2] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_43, false) then (λ ()_43, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x31₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x30₂, (([0x0 ~> 0xfffffffffffffffe])x29₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_43, x29₂ + x30₂ + x31₂)) << 64)) << 64)) << 64) + x1[3] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 then (λ ()_43, (x25₁ + ((x28₁ + ((x31₁ + ((if if (uint0_t)0 ≤ (x14₁ + ((x17₁ + ((x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_44, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_44, false) then (λ ()_44, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_44, x18₂ + x19₂ + x20₂)) << 64)) << 64)) << 64) + x1[2] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 then (λ ()_44, (x14₁ + ((x17₁ + ((x20₁ + ((if if (uint0_t)0 ≤ (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) then (λ ()_45, (uint64_t)((x5₁ + ((x7₁ + ((x9₁ + ((x9₂ + x8₂) << 64)) << 64)) << 64) + x1[1] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256) < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_45, false) then (λ ()_45, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x20₂, ((uint64_t)(Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), ((uint1_t)x19₂, (([0x0 ~> 0xfffffffffffffffe])x18₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_45, x18₂ + x19₂ + x20₂)) << 64)) << 64)) << 64) + x1[2] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_44, false) then (λ ()_44, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x31₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x30₂, (([0x0 ~> 0xfffffffffffffffe])x29₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_44, x29₂ + x30₂ + x31₂)) << 64)) << 64)) << 64) + x1[3] * (x2[0] + ((x2[1] + ((x2[2] + (x2[3] << 64)) << 64)) << 64))) >> 256 < ([0x10000000000000000 ~> 0x10000000000000000])(2^64)) else (λ ()_43, false) then (λ ()_43, (Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x42₂, ((Z.add_with_get_carry(([0x10000000000000000 ~> 0x10000000000000000])(2^64), (x41₂, (([0x0 ~> 0xfffffffffffffffe])x40₂, (uint0_t)0))))₁, (uint0_t)0))))₁) else (λ ()_43, x40₂ + x41₂ + x42₂) in
x3₁ :: x11₁ :: x22₁ :: x33₁ :: x36₁ :: x39₁ :: x42₁ :: x43 :: []
)
Error in converting f to C:
Invalid non-arithmetic let-bound App of type 𝔹 → 𝔹
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment