diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-14 23:36:18 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-14 23:36:18 -0400 |
| commit | 9fe362f4630d13244d947a23d908bf16bf31a719 (patch) | |
| tree | 72587a8c5dceaaecd336b1af53fe8e091023b24d | |
| parent | d626e82b7286d44f41ef5e03a201573f019bbd8b (diff) | |
Update display of ladderstep130
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 7 | ||||
| -rw-r--r-- | src/Compilers/Z/CNotations.v | 89 | ||||
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 11 | ||||
| -rw-r--r-- | src/Compilers/Z/JavaNotations.v | 89 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestLadderstep130.v | 86 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestLadderstep130Display.log | 1792 |
6 files changed, 561 insertions, 1513 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index d1f782597..cd0adf4d1 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -6,10 +6,12 @@ Require Export Crypto.Util.Notations. Local Notation Const x := (Op (OpConst x) TT). (* python: << +#!/usr/bin/env python print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n := (Const %s).''' % (b, d, h, i) for d, h, b, i in sorted([(eval(bv), hex(eval(bv)), bv, i) for (bv, i) in (('0b' + i[2:].replace('~', ''), i) for i in r"""WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0 WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0 @@ -31,6 +33,7 @@ WO~0~0~0~1~1~1~0~0 WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0 WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 WO~0~0~1~1~0~0~1~1 +WO~0~1~0~1~0~1~0~1 WO~1~0 WO~1~0~0~1 WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 @@ -61,6 +64,8 @@ Notation "'0b00011100'" (* 28 (0x1c) *) := (Const WO~0~0~0~1~1~1~0~0). Notation "'0b00110011'" (* 51 (0x33) *) := (Const WO~0~0~1~1~0~0~1~1). +Notation "'0b01010101'" (* 85 (0x55) *) + := (Const WO~0~1~0~1~0~1~0~1). Notation "'0b00000000011111111111111111111111'" (* 8388607 (0x7fffff) *) := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b00000001111111111111111111111111'" (* 33554431 (0x1ffffff) *) @@ -95,3 +100,5 @@ Notation "'0b0000000000001111111111111111111111111111111111111111111111111110'" := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). Notation "'0b0000000000001111111111111111111111111111111111111111111111111111'" (* 4503599627370495 (0xfffffffffffff) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b00000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111111111111111111111111'" (* 38685626227668133590597631 (0x1fffffffffffffffffffffL) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v index 8ec885db3..c6abd3481 100644 --- a/src/Compilers/Z/CNotations.v +++ b/src/Compilers/Z/CNotations.v @@ -11,7 +11,9 @@ Global Open Scope expr_scope. Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. (* python: << -types = ('bool', 'uint8_t', 'uint8_t', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uint128_t') +#!/usr/bin/env python +# -*- coding: utf-8 -*- +types = ('bool', 'uint8_t', 'uint8_t', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uint128_t', 'uint256_t') for lgwordsz in range(0, len(types)): print('Notation "\'%s\'" := (Tbase (TWord %d)).' % (types[lgwordsz], lgwordsz)) print('Notation ℤ := (Tbase TZ).') @@ -71,6 +73,7 @@ Notation "'uint16_t'" := (Tbase (TWord 4)). Notation "'uint32_t'" := (Tbase (TWord 5)). Notation "'uint64_t'" := (Tbase (TWord 6)). Notation "'uint128_t'" := (Tbase (TWord 7)). +Notation "'uint256_t'" := (Tbase (TWord 8)). Notation ℤ := (Tbase TZ). Notation "x * y" := (Op (Mul _ _ _) (Pair x y)). @@ -205,6 +208,22 @@ Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x + y" := (Op (Add _ _ _) (Pair x y)). Notation "x + y" := (Op (Add _ _ _) (Pair x (Var y))). Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) y)). @@ -337,6 +356,22 @@ Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x - y" := (Op (Sub _ _ _) (Pair x y)). Notation "x - y" := (Op (Sub _ _ _) (Pair x (Var y))). Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) y)). @@ -469,6 +504,22 @@ Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x & y" := (Op (Land _ _ _) (Pair x y)). Notation "x & y" := (Op (Land _ _ _) (Pair x (Var y))). Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) y)). @@ -601,6 +652,22 @@ Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x << y" := (Op (Shl _ _ _) (Pair x y)). Notation "x << y" := (Op (Shl _ _ _) (Pair x (Var y))). Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) y)). @@ -733,6 +800,22 @@ Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 30). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x >> y" := (Op (Shr _ _ _) (Pair x y)). Notation "x >> y" := (Op (Shr _ _ _) (Pair x (Var y))). Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) y)). @@ -769,5 +852,9 @@ Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) ( Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). Notation Return x := (Var x). Notation C_like := (Expr base_type op _). diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 1fa48ad6a..40279b6dc 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -7,10 +7,12 @@ Require Export Crypto.Util.Notations. Notation Const x := (Op (OpConst x) TT). (* python: << +#!/usr/bin/env python print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n := (Const %s%%Z).\nNotation "'%s'" (* %d (%s) *)\n := (Const %s).''' % (h, d, h, d, h, d, h, w) for d, h, b, w in sorted([(eval(bv), hex(eval(bv)), bv, i) for (bv, i) in (('0b' + i[2:].replace('~', ''), i) for i in r"""WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 +WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0 WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0 @@ -32,6 +34,7 @@ WO~0~0~0~1~1~1~0~0 WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0 WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0 WO~0~0~1~1~0~0~1~1 +WO~0~1~0~1~0~1~0~1 WO~1~0 WO~1~0~0~1 WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 @@ -84,6 +87,10 @@ Notation "'0x33'" (* 51 (0x33) *) := (Const 51%Z). Notation "'0x33'" (* 51 (0x33) *) := (Const WO~0~0~1~1~0~0~1~1). +Notation "'0x55'" (* 85 (0x55) *) + := (Const 85%Z). +Notation "'0x55'" (* 85 (0x55) *) + := (Const WO~0~1~0~1~0~1~0~1). Notation "'0x7fffff'" (* 8388607 (0x7fffff) *) := (Const 8388607%Z). Notation "'0x7fffff'" (* 8388607 (0x7fffff) *) @@ -152,3 +159,7 @@ Notation "'0xfffffffffffff'" (* 4503599627370495 (0xfffffffffffff) *) := (Const 4503599627370495%Z). Notation "'0xfffffffffffff'" (* 4503599627370495 (0xfffffffffffff) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0x1fffffffffffffffffffffL'" (* 38685626227668133590597631 (0x1fffffffffffffffffffffL) *) + := (Const 38685626227668133590597631%Z). +Notation "'0x1fffffffffffffffffffffL'" (* 38685626227668133590597631 (0x1fffffffffffffffffffffL) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). diff --git a/src/Compilers/Z/JavaNotations.v b/src/Compilers/Z/JavaNotations.v index bab120b0a..c14787e02 100644 --- a/src/Compilers/Z/JavaNotations.v +++ b/src/Compilers/Z/JavaNotations.v @@ -30,7 +30,9 @@ Notation "'M32' & x" := (Op (Cast _ (TWord 6)) (Var x)). Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)).*) (* python: << -types = ('int', 'int', 'int', 'int', 'int', 'int', 'long', 'uint128_t') +#!/usr/bin/env python +# -*- coding: utf-8 -*- +types = ('int', 'int', 'int', 'int', 'int', 'int', 'long', 'uint128_t', 'uint256_t') for lgwordsz in range(0, len(types)): print('Notation "\'%s\'" := (Tbase (TWord %d)).' % (types[lgwordsz], lgwordsz)) print('Notation ℤ := (Tbase TZ).') @@ -90,6 +92,7 @@ Notation "'int'" := (Tbase (TWord 4)). Notation "'int'" := (Tbase (TWord 5)). Notation "'long'" := (Tbase (TWord 6)). Notation "'uint128_t'" := (Tbase (TWord 7)). +Notation "'uint256_t'" := (Tbase (TWord 8)). Notation ℤ := (Tbase TZ). Notation "x * y" := (Op (Mul _ _ _) (Pair x y)). @@ -224,6 +227,22 @@ Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x * y" := (Op (Mul (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x * '(uint256_t)' y" := (Op (Mul (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "x * '(uint256_t)' y" := (Op (Mul (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint256_t)' x * y" := (Op (Mul (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x + y" := (Op (Add _ _ _) (Pair x y)). Notation "x + y" := (Op (Add _ _ _) (Pair x (Var y))). Notation "x + y" := (Op (Add _ _ _) (Pair (Var x) y)). @@ -356,6 +375,22 @@ Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x + y" := (Op (Add (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x + '(uint256_t)' y" := (Op (Add (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "x + '(uint256_t)' y" := (Op (Add (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint256_t)' x + y" := (Op (Add (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x + y" := (Op (Add (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x - y" := (Op (Sub _ _ _) (Pair x y)). Notation "x - y" := (Op (Sub _ _ _) (Pair x (Var y))). Notation "x - y" := (Op (Sub _ _ _) (Pair (Var x) y)). @@ -488,6 +523,22 @@ Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x - y" := (Op (Sub (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x - '(uint256_t)' y" := (Op (Sub (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 50). +Notation "x - '(uint256_t)' y" := (Op (Sub (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "'(uint256_t)' x - y" := (Op (Sub (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 50). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x & y" := (Op (Land _ _ _) (Pair x y)). Notation "x & y" := (Op (Land _ _ _) (Pair x (Var y))). Notation "x & y" := (Op (Land _ _ _) (Pair (Var x) y)). @@ -620,6 +671,22 @@ Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x & y" := (Op (Land (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x & '(uint256_t)' y" := (Op (Land (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 40). +Notation "x & '(uint256_t)' y" := (Op (Land (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "'(uint256_t)' x & y" := (Op (Land (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 40). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x & y" := (Op (Land (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x << y" := (Op (Shl _ _ _) (Pair x y)). Notation "x << y" := (Op (Shl _ _ _) (Pair x (Var y))). Notation "x << y" := (Op (Shl _ _ _) (Pair (Var x) y)). @@ -752,6 +819,22 @@ Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x y)). Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair x (Var y))). Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) y)). Notation "x << y" := (Op (Shl (TWord 7) (TWord 7) (TWord 7)) (Pair (Var x) (Var y))). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 30). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "'(uint256_t)' x << '(uint256_t)' y" := (Op (Shl (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair x y)) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair x y)) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "x << '(uint256_t)' y" := (Op (Shl (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint256_t)' x << y" := (Op (Shl (TWord _) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair x y)). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)). +Notation "x << y" := (Op (Shl (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))). Notation "x >> y" := (Op (Shr _ _ _) (Pair x y)). Notation "x >> y" := (Op (Shr _ _ _) (Pair x (Var y))). Notation "x >> y" := (Op (Shr _ _ _) (Pair (Var x) y)). @@ -788,5 +871,9 @@ Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) ( Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair x (Var y))) (at level 30). Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) y)) (at level 30). Notation "'(uint128_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 7)) (Pair (Var x) (Var y))) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair x y)) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair x (Var y))) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) y)) (at level 30). +Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). Notation Return x := (Var x). Notation Java_like := (Expr base_type op _). diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index be1be63ac..74b2ce674 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -42,9 +42,11 @@ Section BoundedField25p5. Let bitwidth := Eval compute in (2^lgbitwidth)%nat. Let feZ : Type := tuple Z sz. Let feW : Type := tuple (wordT lgbitwidth) sz. + Let feW_bounded : feW -> Prop + := fun w => is_bounded_by None bounds (map wordToZ w). Let feBW : Type := BoundedWord sz bitwidth bounds. - Let phi : feBW -> F m := - fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). + Let phi : feW -> F m := + fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x). (** TODO(jadep,andreser): Move to NewBaseSystemTest? *) Definition FMxzladderstep := @M.xzladderstep (F m) F.add F.sub F.mul. @@ -64,56 +66,52 @@ Section BoundedField25p5. (* TODO : change this to field once field isomorphism happens *) Definition xzladderstep : - { xzladderstep : feBW -> feBW -> feBW * feBW -> feBW * feBW -> feBW * feBW * (feBW * feBW) - | forall a24 x1 Q Q', Tuple.map (n:=2) (Tuple.map (n:=2) phi) (xzladderstep a24 x1 Q Q') = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. + { xzladderstep : feW -> feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW) + | forall a24 x1 Q Q', + let xz := xzladderstep a24 x1 Q Q' in + feW_bounded a24 + -> feW_bounded x1 + -> feW_bounded (fst Q) /\ feW_bounded (snd Q) + -> feW_bounded (fst Q') /\ feW_bounded (snd Q') + -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz))) + /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) + /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. Proof. lazymatch goal with - | [ |- { f | forall a b c d, ?phi (f a b c d) = @?rhs a b c d } ] - => apply lift4_sig with (P:=fun a b c d f => phi f = rhs a b c d) - end. - intros. - eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- !(Tuple.map_map (B.Positional.Fdecode wt) (BoundedWordToZ sz bitwidth bounds)). - rewrite <- (proj2_sig Mxzladderstep_sig). - apply f_equal. - cbv [proj1_sig]; cbv [Mxzladderstep_sig]. - context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _). - set (k := @M.xzladderstep _ _ _ _); context_to_dlet_in_rhs k; subst k. - cbv [M.xzladderstep]. - lazymatch goal with - | [ |- context[@proj1_sig ?a ?b carry_sig] ] - => context_to_dlet_in_rhs (@proj1_sig a b carry_sig) + | [ |- { op | forall (a:?A) (b:?B) (c:?C) (d:?D), + let v := op a b c d in + @?P a b c d v } ] + => refine (@lift4_sig A B C D _ P _) end. + intros a b c d; cbv beta iota zeta. lazymatch goal with - | [ |- context[@proj1_sig ?a ?b mul_sig] ] - => context_to_dlet_in_rhs (@proj1_sig a b mul_sig) + | [ |- { e | ?A -> ?B -> ?C -> ?D -> @?E e } ] + => refine (proj2_sig_map (P:=fun e => A -> B -> C -> D -> (_:Prop)) _ _) end. - lazymatch goal with - | [ |- context[@proj1_sig ?a ?b add_sig] ] - => context_to_dlet_in_rhs (@proj1_sig a b add_sig) - end. - lazymatch goal with - | [ |- context[@proj1_sig ?a ?b sub_sig] ] - => context_to_dlet_in_rhs (@proj1_sig a b sub_sig) - end. - cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. - reflexivity. - eexists_sig_etransitivity_for_rewrite_fun. - { intro; cbv beta. - subst feBW. - set_evars. - do 2 lazymatch goal with - | [ |- context[Tuple.map (n:=?n) (fun x => ?f (?g x))] ] - => rewrite <- (Tuple.map_map (n:=n) f g : pointwise_relation _ eq _ _) + { intros ? FINAL. + repeat let H := fresh in intro H; specialize (FINAL H). + cbv [phi]. + split; [ refine (proj1 FINAL); shelve | ]. + do 4 match goal with + | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ] + => rewrite <- (Tuple.map_map (n:=N) f g + : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x)))) + end. + rewrite <- (proj2_sig Mxzladderstep_sig). + apply f_equal. + cbv [proj1_sig]; cbv [Mxzladderstep_sig]. + context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _). + cbv [M.xzladderstep]. + do 4 lazymatch goal with + | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] + => context_to_dlet_in_rhs (@proj1_sig a b f_sig) end. - subst_evars. - reflexivity. } - cbv beta. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - apply adjust_tuple2_tuple2_sig. + cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd]. + refine (proj2 FINAL). } + subst feW feW_bounded; cbv beta. (* jgross start here! *) - Set Ltac Profiling. (* + Set Ltac Profiling. Time Glue.refine_to_reflective_glue (128::256::nil)%nat%list. Time ReflectiveTactics.refine_with_pipeline_correct. { Time ReflectiveTactics.do_reify. } diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log index fd4d8d28b..ee1b0e5ec 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.log +++ b/src/Specific/IntegrationTestLadderstep130Display.log @@ -1,5 +1,5 @@ λ x x0 x1 x2 x3 x4 : word128 * word128 * word128, -(let (x5, _) := let (x5, _) := Interp-η +let (a, b) := Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), (x34, x35, x33, (x38, x39, x37)))%core, uint128_t x40 = x24 + x28; @@ -11,180 +11,180 @@ uint128_t x46 = x45 - x29; uint128_t x47 = Const 77371252455336267181195254 + x23; uint128_t x48 = x47 - x27; - ℤ x49 = x42 * x40; - ℤ x50 = x41 * x41; - ℤ x51 = x40 * x42; - ℤ x52 = x50 + x51; - ℤ x53 = x49 + x52; - ℤ x54 = x42 * x41; - ℤ x55 = x41 * x42; - ℤ x56 = x54 + x55; - ℤ x57 = x40 * x40; - ℤ x58 = Const 5 * x57; - ℤ x59 = x56 + x58; - ℤ x60 = x42 * x42; - ℤ x61 = x41 * x40; - ℤ x62 = x40 * x41; - ℤ x63 = x61 + x62; - ℤ x64 = Const 5 * x63; - ℤ x65 = x60 + x64; - uint128_t x66 = x65 >> Const 85; - ℤ x67 = x66 + x59; - uint128_t x68 = x67 >> Const 85; - ℤ x69 = x68 + x53; - uint128_t x70 = x65 & Const 38685626227668133590597631; - uint128_t x71 = x69 >> Const 85; - uint128_t x72 = (uint128_t) Const 5 * x71; + uint256_t x49 = (uint256_t) x42 * (uint256_t) x40; + uint256_t x50 = (uint256_t) x41 * (uint256_t) x41; + uint256_t x51 = (uint256_t) x40 * (uint256_t) x42; + uint256_t x52 = x50 + x51; + uint256_t x53 = x49 + x52; + uint256_t x54 = (uint256_t) x42 * (uint256_t) x41; + uint256_t x55 = (uint256_t) x41 * (uint256_t) x42; + uint256_t x56 = x54 + x55; + uint256_t x57 = (uint256_t) x40 * (uint256_t) x40; + uint256_t x58 = (uint256_t) Const 5 * x57; + uint256_t x59 = x56 + x58; + uint256_t x60 = (uint256_t) x42 * (uint256_t) x42; + uint256_t x61 = (uint256_t) x41 * (uint256_t) x40; + uint256_t x62 = (uint256_t) x40 * (uint256_t) x41; + uint256_t x63 = x61 + x62; + uint256_t x64 = (uint256_t) Const 5 * x63; + uint256_t x65 = x60 + x64; + uint128_t x66 = (uint128_t) (x65 >> 0x55); + uint256_t x67 = (uint256_t) x66 + x59; + uint128_t x68 = (uint128_t) (x67 >> 0x55); + uint256_t x69 = (uint256_t) x68 + x53; + uint128_t x70 = (uint128_t) x65 & 0x1fffffffffffffffffffffL; + uint128_t x71 = (uint128_t) (x69 >> 0x55); + uint128_t x72 = Const 5 * x71; uint128_t x73 = x70 + x72; - uint64_t x74 = (uint64_t) (x73 >> Const 85); - uint128_t x75 = x67 & Const 38685626227668133590597631; - uint128_t x76 = (uint128_t) x74 + x75; - uint64_t x77 = (uint64_t) (x76 >> Const 85); - uint128_t x78 = x69 & Const 38685626227668133590597631; - uint128_t x79 = (uint128_t) x77 + x78; - uint128_t x80 = x76 & Const 38685626227668133590597631; - uint128_t x81 = x73 & Const 38685626227668133590597631; - ℤ x82 = x48 * x44; - ℤ x83 = x46 * x46; - ℤ x84 = x44 * x48; - ℤ x85 = x83 + x84; - ℤ x86 = x82 + x85; - ℤ x87 = x48 * x46; - ℤ x88 = x46 * x48; - ℤ x89 = x87 + x88; - ℤ x90 = x44 * x44; - ℤ x91 = Const 5 * x90; - ℤ x92 = x89 + x91; - ℤ x93 = x48 * x48; - ℤ x94 = x46 * x44; - ℤ x95 = x44 * x46; - ℤ x96 = x94 + x95; - ℤ x97 = Const 5 * x96; - ℤ x98 = x93 + x97; - uint128_t x99 = x98 >> Const 85; - ℤ x100 = x99 + x92; - uint128_t x101 = x100 >> Const 85; - ℤ x102 = x101 + x86; - uint128_t x103 = x98 & Const 38685626227668133590597631; - uint128_t x104 = x102 >> Const 85; - uint128_t x105 = (uint128_t) Const 5 * x104; + uint128_t x74 = (uint128_t) (x73 >> 0x55); + uint128_t x75 = (uint128_t) x67 & 0x1fffffffffffffffffffffL; + uint128_t x76 = x74 + x75; + uint128_t x77 = (uint128_t) (x76 >> 0x55); + uint128_t x78 = (uint128_t) x69 & 0x1fffffffffffffffffffffL; + uint128_t x79 = x77 + x78; + uint128_t x80 = x76 & 0x1fffffffffffffffffffffL; + uint128_t x81 = x73 & 0x1fffffffffffffffffffffL; + uint256_t x82 = (uint256_t) x48 * (uint256_t) x44; + uint256_t x83 = (uint256_t) x46 * (uint256_t) x46; + uint256_t x84 = (uint256_t) x44 * (uint256_t) x48; + uint256_t x85 = x83 + x84; + uint256_t x86 = x82 + x85; + uint256_t x87 = (uint256_t) x48 * (uint256_t) x46; + uint256_t x88 = (uint256_t) x46 * (uint256_t) x48; + uint256_t x89 = x87 + x88; + uint256_t x90 = (uint256_t) x44 * (uint256_t) x44; + uint256_t x91 = (uint256_t) Const 5 * x90; + uint256_t x92 = x89 + x91; + uint256_t x93 = (uint256_t) x48 * (uint256_t) x48; + uint256_t x94 = (uint256_t) x46 * (uint256_t) x44; + uint256_t x95 = (uint256_t) x44 * (uint256_t) x46; + uint256_t x96 = x94 + x95; + uint256_t x97 = (uint256_t) Const 5 * x96; + uint256_t x98 = x93 + x97; + uint128_t x99 = (uint128_t) (x98 >> 0x55); + uint256_t x100 = (uint256_t) x99 + x92; + uint128_t x101 = (uint128_t) (x100 >> 0x55); + uint256_t x102 = (uint256_t) x101 + x86; + uint128_t x103 = (uint128_t) x98 & 0x1fffffffffffffffffffffL; + uint128_t x104 = (uint128_t) (x102 >> 0x55); + uint128_t x105 = Const 5 * x104; uint128_t x106 = x103 + x105; - uint64_t x107 = (uint64_t) (x106 >> Const 85); - uint128_t x108 = x100 & Const 38685626227668133590597631; - uint128_t x109 = (uint128_t) x107 + x108; - uint64_t x110 = (uint64_t) (x109 >> Const 85); - uint128_t x111 = x102 & Const 38685626227668133590597631; - uint128_t x112 = (uint128_t) x110 + x111; - uint128_t x113 = x109 & Const 38685626227668133590597631; - uint128_t x114 = x106 & Const 38685626227668133590597631; - ℤ x115 = x81 * x112; - ℤ x116 = x80 * x113; - ℤ x117 = x79 * x114; - ℤ x118 = x116 + x117; - ℤ x119 = x115 + x118; - ℤ x120 = x81 * x113; - ℤ x121 = x80 * x114; - ℤ x122 = x120 + x121; - ℤ x123 = x79 * x112; - ℤ x124 = Const 5 * x123; - ℤ x125 = x122 + x124; - ℤ x126 = x81 * x114; - ℤ x127 = x80 * x112; - ℤ x128 = x79 * x113; - ℤ x129 = x127 + x128; - ℤ x130 = Const 5 * x129; - ℤ x131 = x126 + x130; - uint128_t x132 = x131 >> Const 85; - ℤ x133 = x132 + x125; - uint128_t x134 = x133 >> Const 85; - ℤ x135 = x134 + x119; - uint128_t x136 = x131 & Const 38685626227668133590597631; - uint128_t x137 = x135 >> Const 85; - uint128_t x138 = (uint128_t) Const 5 * x137; + uint128_t x107 = (uint128_t) (x106 >> 0x55); + uint128_t x108 = (uint128_t) x100 & 0x1fffffffffffffffffffffL; + uint128_t x109 = x107 + x108; + uint128_t x110 = (uint128_t) (x109 >> 0x55); + uint128_t x111 = (uint128_t) x102 & 0x1fffffffffffffffffffffL; + uint128_t x112 = x110 + x111; + uint128_t x113 = x109 & 0x1fffffffffffffffffffffL; + uint128_t x114 = x106 & 0x1fffffffffffffffffffffL; + uint256_t x115 = (uint256_t) x81 * (uint256_t) x112; + uint256_t x116 = (uint256_t) x80 * (uint256_t) x113; + uint256_t x117 = (uint256_t) x79 * (uint256_t) x114; + uint256_t x118 = x116 + x117; + uint256_t x119 = x115 + x118; + uint256_t x120 = (uint256_t) x81 * (uint256_t) x113; + uint256_t x121 = (uint256_t) x80 * (uint256_t) x114; + uint256_t x122 = x120 + x121; + uint256_t x123 = (uint256_t) x79 * (uint256_t) x112; + uint256_t x124 = (uint256_t) Const 5 * x123; + uint256_t x125 = x122 + x124; + uint256_t x126 = (uint256_t) x81 * (uint256_t) x114; + uint256_t x127 = (uint256_t) x80 * (uint256_t) x112; + uint256_t x128 = (uint256_t) x79 * (uint256_t) x113; + uint256_t x129 = x127 + x128; + uint256_t x130 = (uint256_t) Const 5 * x129; + uint256_t x131 = x126 + x130; + uint128_t x132 = (uint128_t) (x131 >> 0x55); + uint256_t x133 = (uint256_t) x132 + x125; + uint128_t x134 = (uint128_t) (x133 >> 0x55); + uint256_t x135 = (uint256_t) x134 + x119; + uint128_t x136 = (uint128_t) x131 & 0x1fffffffffffffffffffffL; + uint128_t x137 = (uint128_t) (x135 >> 0x55); + uint128_t x138 = Const 5 * x137; uint128_t x139 = x136 + x138; - uint64_t x140 = (uint64_t) (x139 >> Const 85); - uint128_t x141 = x133 & Const 38685626227668133590597631; - uint128_t x142 = (uint128_t) x140 + x141; - uint64_t x143 = (uint64_t) (x142 >> Const 85); - uint128_t x144 = x135 & Const 38685626227668133590597631; - uint128_t x145 = (uint128_t) x143 + x144; - uint128_t x146 = x142 & Const 38685626227668133590597631; - uint128_t x147 = x139 & Const 38685626227668133590597631; + uint128_t x140 = (uint128_t) (x139 >> 0x55); + uint128_t x141 = (uint128_t) x133 & 0x1fffffffffffffffffffffL; + uint128_t x142 = x140 + x141; + uint128_t x143 = (uint128_t) (x142 >> 0x55); + uint128_t x144 = (uint128_t) x135 & 0x1fffffffffffffffffffffL; + uint128_t x145 = x143 + x144; + uint128_t x146 = x142 & 0x1fffffffffffffffffffffL; + uint128_t x147 = x139 & 0x1fffffffffffffffffffffL; uint128_t x148 = Const 77371252455336267181195262 + x79; uint128_t x149 = x148 - x112; uint128_t x150 = Const 77371252455336267181195262 + x80; uint128_t x151 = x150 - x113; uint128_t x152 = Const 77371252455336267181195254 + x81; uint128_t x153 = x152 - x114; - ℤ x154 = x13 * x149; - ℤ x155 = x15 * x151; - ℤ x156 = x14 * x153; - ℤ x157 = x155 + x156; - ℤ x158 = x154 + x157; - ℤ x159 = x13 * x151; - ℤ x160 = x15 * x153; - ℤ x161 = x159 + x160; - ℤ x162 = x14 * x149; - ℤ x163 = Const 5 * x162; - ℤ x164 = x161 + x163; - ℤ x165 = x13 * x153; - ℤ x166 = x15 * x149; - ℤ x167 = x14 * x151; - ℤ x168 = x166 + x167; - ℤ x169 = Const 5 * x168; - ℤ x170 = x165 + x169; - uint128_t x171 = x170 >> Const 85; - ℤ x172 = x171 + x164; - uint128_t x173 = x172 >> Const 85; - ℤ x174 = x173 + x158; - uint128_t x175 = x170 & Const 38685626227668133590597631; - uint128_t x176 = x174 >> Const 85; - uint128_t x177 = (uint128_t) Const 5 * x176; + uint256_t x154 = (uint256_t) x13 * (uint256_t) x149; + uint256_t x155 = (uint256_t) x15 * (uint256_t) x151; + uint256_t x156 = (uint256_t) x14 * (uint256_t) x153; + uint256_t x157 = x155 + x156; + uint256_t x158 = x154 + x157; + uint256_t x159 = (uint256_t) x13 * (uint256_t) x151; + uint256_t x160 = (uint256_t) x15 * (uint256_t) x153; + uint256_t x161 = x159 + x160; + uint256_t x162 = (uint256_t) x14 * (uint256_t) x149; + uint256_t x163 = (uint256_t) Const 5 * x162; + uint256_t x164 = x161 + x163; + uint256_t x165 = (uint256_t) x13 * (uint256_t) x153; + uint256_t x166 = (uint256_t) x15 * (uint256_t) x149; + uint256_t x167 = (uint256_t) x14 * (uint256_t) x151; + uint256_t x168 = x166 + x167; + uint256_t x169 = (uint256_t) Const 5 * x168; + uint256_t x170 = x165 + x169; + uint128_t x171 = (uint128_t) (x170 >> 0x55); + uint256_t x172 = (uint256_t) x171 + x164; + uint128_t x173 = (uint128_t) (x172 >> 0x55); + uint256_t x174 = (uint256_t) x173 + x158; + uint128_t x175 = (uint128_t) x170 & 0x1fffffffffffffffffffffL; + uint128_t x176 = (uint128_t) (x174 >> 0x55); + uint128_t x177 = Const 5 * x176; uint128_t x178 = x175 + x177; - uint64_t x179 = (uint64_t) (x178 >> Const 85); - uint128_t x180 = x172 & Const 38685626227668133590597631; - uint128_t x181 = (uint128_t) x179 + x180; - uint64_t x182 = (uint64_t) (x181 >> Const 85); - uint128_t x183 = x174 & Const 38685626227668133590597631; - uint128_t x184 = (uint128_t) x182 + x183; - uint128_t x185 = x181 & Const 38685626227668133590597631; - uint128_t x186 = x178 & Const 38685626227668133590597631; + uint128_t x179 = (uint128_t) (x178 >> 0x55); + uint128_t x180 = (uint128_t) x172 & 0x1fffffffffffffffffffffL; + uint128_t x181 = x179 + x180; + uint128_t x182 = (uint128_t) (x181 >> 0x55); + uint128_t x183 = (uint128_t) x174 & 0x1fffffffffffffffffffffL; + uint128_t x184 = x182 + x183; + uint128_t x185 = x181 & 0x1fffffffffffffffffffffL; + uint128_t x186 = x178 & 0x1fffffffffffffffffffffL; uint128_t x187 = x79 + x184; uint128_t x188 = x80 + x185; uint128_t x189 = x81 + x186; - ℤ x190 = x153 * x187; - ℤ x191 = x151 * x188; - ℤ x192 = x149 * x189; - ℤ x193 = x191 + x192; - ℤ x194 = x190 + x193; - ℤ x195 = x153 * x188; - ℤ x196 = x151 * x189; - ℤ x197 = x195 + x196; - ℤ x198 = x149 * x187; - ℤ x199 = Const 5 * x198; - ℤ x200 = x197 + x199; - ℤ x201 = x153 * x189; - ℤ x202 = x151 * x187; - ℤ x203 = x149 * x188; - ℤ x204 = x202 + x203; - ℤ x205 = Const 5 * x204; - ℤ x206 = x201 + x205; - uint128_t x207 = x206 >> Const 85; - ℤ x208 = x207 + x200; - uint128_t x209 = x208 >> Const 85; - ℤ x210 = x209 + x194; - uint128_t x211 = x206 & Const 38685626227668133590597631; - uint128_t x212 = x210 >> Const 85; - uint128_t x213 = (uint128_t) Const 5 * x212; + uint256_t x190 = (uint256_t) x153 * (uint256_t) x187; + uint256_t x191 = (uint256_t) x151 * (uint256_t) x188; + uint256_t x192 = (uint256_t) x149 * (uint256_t) x189; + uint256_t x193 = x191 + x192; + uint256_t x194 = x190 + x193; + uint256_t x195 = (uint256_t) x153 * (uint256_t) x188; + uint256_t x196 = (uint256_t) x151 * (uint256_t) x189; + uint256_t x197 = x195 + x196; + uint256_t x198 = (uint256_t) x149 * (uint256_t) x187; + uint256_t x199 = (uint256_t) Const 5 * x198; + uint256_t x200 = x197 + x199; + uint256_t x201 = (uint256_t) x153 * (uint256_t) x189; + uint256_t x202 = (uint256_t) x151 * (uint256_t) x187; + uint256_t x203 = (uint256_t) x149 * (uint256_t) x188; + uint256_t x204 = x202 + x203; + uint256_t x205 = (uint256_t) Const 5 * x204; + uint256_t x206 = x201 + x205; + uint128_t x207 = (uint128_t) (x206 >> 0x55); + uint256_t x208 = (uint256_t) x207 + x200; + uint128_t x209 = (uint128_t) (x208 >> 0x55); + uint256_t x210 = (uint256_t) x209 + x194; + uint128_t x211 = (uint128_t) x206 & 0x1fffffffffffffffffffffL; + uint128_t x212 = (uint128_t) (x210 >> 0x55); + uint128_t x213 = Const 5 * x212; uint128_t x214 = x211 + x213; - uint64_t x215 = (uint64_t) (x214 >> Const 85); - uint128_t x216 = x208 & Const 38685626227668133590597631; - uint128_t x217 = (uint128_t) x215 + x216; - uint64_t x218 = (uint64_t) (x217 >> Const 85); - uint128_t x219 = x210 & Const 38685626227668133590597631; - uint128_t x220 = (uint128_t) x218 + x219; - uint128_t x221 = x217 & Const 38685626227668133590597631; - uint128_t x222 = x214 & Const 38685626227668133590597631; + uint128_t x215 = (uint128_t) (x214 >> 0x55); + uint128_t x216 = (uint128_t) x208 & 0x1fffffffffffffffffffffL; + uint128_t x217 = x215 + x216; + uint128_t x218 = (uint128_t) (x217 >> 0x55); + uint128_t x219 = (uint128_t) x210 & 0x1fffffffffffffffffffffL; + uint128_t x220 = x218 + x219; + uint128_t x221 = x217 & 0x1fffffffffffffffffffffL; + uint128_t x222 = x214 & 0x1fffffffffffffffffffffL; uint128_t x223 = x34 + x38; uint128_t x224 = x35 + x39; uint128_t x225 = x33 + x37; @@ -194,111 +194,111 @@ uint128_t x229 = x228 - x39; uint128_t x230 = Const 77371252455336267181195254 + x33; uint128_t x231 = x230 - x37; - ℤ x232 = x225 * x44; - ℤ x233 = x224 * x46; - ℤ x234 = x223 * x48; - ℤ x235 = x233 + x234; - ℤ x236 = x232 + x235; - ℤ x237 = x225 * x46; - ℤ x238 = x224 * x48; - ℤ x239 = x237 + x238; - ℤ x240 = x223 * x44; - ℤ x241 = Const 5 * x240; - ℤ x242 = x239 + x241; - ℤ x243 = x225 * x48; - ℤ x244 = x224 * x44; - ℤ x245 = x223 * x46; - ℤ x246 = x244 + x245; - ℤ x247 = Const 5 * x246; - ℤ x248 = x243 + x247; - uint128_t x249 = x248 >> Const 85; - ℤ x250 = x249 + x242; - uint128_t x251 = x250 >> Const 85; - ℤ x252 = x251 + x236; - uint128_t x253 = x248 & Const 38685626227668133590597631; - uint128_t x254 = x252 >> Const 85; - uint128_t x255 = (uint128_t) Const 5 * x254; + uint256_t x232 = (uint256_t) x225 * (uint256_t) x44; + uint256_t x233 = (uint256_t) x224 * (uint256_t) x46; + uint256_t x234 = (uint256_t) x223 * (uint256_t) x48; + uint256_t x235 = x233 + x234; + uint256_t x236 = x232 + x235; + uint256_t x237 = (uint256_t) x225 * (uint256_t) x46; + uint256_t x238 = (uint256_t) x224 * (uint256_t) x48; + uint256_t x239 = x237 + x238; + uint256_t x240 = (uint256_t) x223 * (uint256_t) x44; + uint256_t x241 = (uint256_t) Const 5 * x240; + uint256_t x242 = x239 + x241; + uint256_t x243 = (uint256_t) x225 * (uint256_t) x48; + uint256_t x244 = (uint256_t) x224 * (uint256_t) x44; + uint256_t x245 = (uint256_t) x223 * (uint256_t) x46; + uint256_t x246 = x244 + x245; + uint256_t x247 = (uint256_t) Const 5 * x246; + uint256_t x248 = x243 + x247; + uint128_t x249 = (uint128_t) (x248 >> 0x55); + uint256_t x250 = (uint256_t) x249 + x242; + uint128_t x251 = (uint128_t) (x250 >> 0x55); + uint256_t x252 = (uint256_t) x251 + x236; + uint128_t x253 = (uint128_t) x248 & 0x1fffffffffffffffffffffL; + uint128_t x254 = (uint128_t) (x252 >> 0x55); + uint128_t x255 = Const 5 * x254; uint128_t x256 = x253 + x255; - uint64_t x257 = (uint64_t) (x256 >> Const 85); - uint128_t x258 = x250 & Const 38685626227668133590597631; - uint128_t x259 = (uint128_t) x257 + x258; - uint64_t x260 = (uint64_t) (x259 >> Const 85); - uint128_t x261 = x252 & Const 38685626227668133590597631; - uint128_t x262 = (uint128_t) x260 + x261; - uint128_t x263 = x259 & Const 38685626227668133590597631; - uint128_t x264 = x256 & Const 38685626227668133590597631; - ℤ x265 = x231 * x40; - ℤ x266 = x229 * x41; - ℤ x267 = x227 * x42; - ℤ x268 = x266 + x267; - ℤ x269 = x265 + x268; - ℤ x270 = x231 * x41; - ℤ x271 = x229 * x42; - ℤ x272 = x270 + x271; - ℤ x273 = x227 * x40; - ℤ x274 = Const 5 * x273; - ℤ x275 = x272 + x274; - ℤ x276 = x231 * x42; - ℤ x277 = x229 * x40; - ℤ x278 = x227 * x41; - ℤ x279 = x277 + x278; - ℤ x280 = Const 5 * x279; - ℤ x281 = x276 + x280; - uint128_t x282 = x281 >> Const 85; - ℤ x283 = x282 + x275; - uint128_t x284 = x283 >> Const 85; - ℤ x285 = x284 + x269; - uint128_t x286 = x281 & Const 38685626227668133590597631; - uint128_t x287 = x285 >> Const 85; - uint128_t x288 = (uint128_t) Const 5 * x287; + uint128_t x257 = (uint128_t) (x256 >> 0x55); + uint128_t x258 = (uint128_t) x250 & 0x1fffffffffffffffffffffL; + uint128_t x259 = x257 + x258; + uint128_t x260 = (uint128_t) (x259 >> 0x55); + uint128_t x261 = (uint128_t) x252 & 0x1fffffffffffffffffffffL; + uint128_t x262 = x260 + x261; + uint128_t x263 = x259 & 0x1fffffffffffffffffffffL; + uint128_t x264 = x256 & 0x1fffffffffffffffffffffL; + uint256_t x265 = (uint256_t) x231 * (uint256_t) x40; + uint256_t x266 = (uint256_t) x229 * (uint256_t) x41; + uint256_t x267 = (uint256_t) x227 * (uint256_t) x42; + uint256_t x268 = x266 + x267; + uint256_t x269 = x265 + x268; + uint256_t x270 = (uint256_t) x231 * (uint256_t) x41; + uint256_t x271 = (uint256_t) x229 * (uint256_t) x42; + uint256_t x272 = x270 + x271; + uint256_t x273 = (uint256_t) x227 * (uint256_t) x40; + uint256_t x274 = (uint256_t) Const 5 * x273; + uint256_t x275 = x272 + x274; + uint256_t x276 = (uint256_t) x231 * (uint256_t) x42; + uint256_t x277 = (uint256_t) x229 * (uint256_t) x40; + uint256_t x278 = (uint256_t) x227 * (uint256_t) x41; + uint256_t x279 = x277 + x278; + uint256_t x280 = (uint256_t) Const 5 * x279; + uint256_t x281 = x276 + x280; + uint128_t x282 = (uint128_t) (x281 >> 0x55); + uint256_t x283 = (uint256_t) x282 + x275; + uint128_t x284 = (uint128_t) (x283 >> 0x55); + uint256_t x285 = (uint256_t) x284 + x269; + uint128_t x286 = (uint128_t) x281 & 0x1fffffffffffffffffffffL; + uint128_t x287 = (uint128_t) (x285 >> 0x55); + uint128_t x288 = Const 5 * x287; uint128_t x289 = x286 + x288; - uint64_t x290 = (uint64_t) (x289 >> Const 85); - uint128_t x291 = x283 & Const 38685626227668133590597631; - uint128_t x292 = (uint128_t) x290 + x291; - uint64_t x293 = (uint64_t) (x292 >> Const 85); - uint128_t x294 = x285 & Const 38685626227668133590597631; - uint128_t x295 = (uint128_t) x293 + x294; - uint128_t x296 = x292 & Const 38685626227668133590597631; - uint128_t x297 = x289 & Const 38685626227668133590597631; + uint128_t x290 = (uint128_t) (x289 >> 0x55); + uint128_t x291 = (uint128_t) x283 & 0x1fffffffffffffffffffffL; + uint128_t x292 = x290 + x291; + uint128_t x293 = (uint128_t) (x292 >> 0x55); + uint128_t x294 = (uint128_t) x285 & 0x1fffffffffffffffffffffL; + uint128_t x295 = x293 + x294; + uint128_t x296 = x292 & 0x1fffffffffffffffffffffL; + uint128_t x297 = x289 & 0x1fffffffffffffffffffffL; uint128_t x298 = x295 + x262; uint128_t x299 = x296 + x263; uint128_t x300 = x297 + x264; uint128_t x301 = x295 + x262; uint128_t x302 = x296 + x263; uint128_t x303 = x297 + x264; - ℤ x304 = x300 * x301; - ℤ x305 = x299 * x302; - ℤ x306 = x298 * x303; - ℤ x307 = x305 + x306; - ℤ x308 = x304 + x307; - ℤ x309 = x300 * x302; - ℤ x310 = x299 * x303; - ℤ x311 = x309 + x310; - ℤ x312 = x298 * x301; - ℤ x313 = Const 5 * x312; - ℤ x314 = x311 + x313; - ℤ x315 = x300 * x303; - ℤ x316 = x299 * x301; - ℤ x317 = x298 * x302; - ℤ x318 = x316 + x317; - ℤ x319 = Const 5 * x318; - ℤ x320 = x315 + x319; - uint128_t x321 = x320 >> Const 85; - ℤ x322 = x321 + x314; - uint128_t x323 = x322 >> Const 85; - ℤ x324 = x323 + x308; - uint128_t x325 = x320 & Const 38685626227668133590597631; - uint128_t x326 = x324 >> Const 85; - uint128_t x327 = (uint128_t) Const 5 * x326; + uint256_t x304 = (uint256_t) x300 * (uint256_t) x301; + uint256_t x305 = (uint256_t) x299 * (uint256_t) x302; + uint256_t x306 = (uint256_t) x298 * (uint256_t) x303; + uint256_t x307 = x305 + x306; + uint256_t x308 = x304 + x307; + uint256_t x309 = (uint256_t) x300 * (uint256_t) x302; + uint256_t x310 = (uint256_t) x299 * (uint256_t) x303; + uint256_t x311 = x309 + x310; + uint256_t x312 = (uint256_t) x298 * (uint256_t) x301; + uint256_t x313 = (uint256_t) Const 5 * x312; + uint256_t x314 = x311 + x313; + uint256_t x315 = (uint256_t) x300 * (uint256_t) x303; + uint256_t x316 = (uint256_t) x299 * (uint256_t) x301; + uint256_t x317 = (uint256_t) x298 * (uint256_t) x302; + uint256_t x318 = x316 + x317; + uint256_t x319 = (uint256_t) Const 5 * x318; + uint256_t x320 = x315 + x319; + uint128_t x321 = (uint128_t) (x320 >> 0x55); + uint256_t x322 = (uint256_t) x321 + x314; + uint128_t x323 = (uint128_t) (x322 >> 0x55); + uint256_t x324 = (uint256_t) x323 + x308; + uint128_t x325 = (uint128_t) x320 & 0x1fffffffffffffffffffffL; + uint128_t x326 = (uint128_t) (x324 >> 0x55); + uint128_t x327 = Const 5 * x326; uint128_t x328 = x325 + x327; - uint64_t x329 = (uint64_t) (x328 >> Const 85); - uint128_t x330 = x322 & Const 38685626227668133590597631; - uint128_t x331 = (uint128_t) x329 + x330; - uint64_t x332 = (uint64_t) (x331 >> Const 85); - uint128_t x333 = x324 & Const 38685626227668133590597631; - uint128_t x334 = (uint128_t) x332 + x333; - uint128_t x335 = x331 & Const 38685626227668133590597631; - uint128_t x336 = x328 & Const 38685626227668133590597631; + uint128_t x329 = (uint128_t) (x328 >> 0x55); + uint128_t x330 = (uint128_t) x322 & 0x1fffffffffffffffffffffL; + uint128_t x331 = x329 + x330; + uint128_t x332 = (uint128_t) (x331 >> 0x55); + uint128_t x333 = (uint128_t) x324 & 0x1fffffffffffffffffffffL; + uint128_t x334 = x332 + x333; + uint128_t x335 = x331 & 0x1fffffffffffffffffffffL; + uint128_t x336 = x328 & 0x1fffffffffffffffffffffL; uint128_t x337 = Const 77371252455336267181195262 + x295; uint128_t x338 = x337 - x262; uint128_t x339 = Const 77371252455336267181195262 + x296; @@ -311,1217 +311,75 @@ uint128_t x346 = x345 - x263; uint128_t x347 = Const 77371252455336267181195254 + x297; uint128_t x348 = x347 - x264; - ℤ x349 = x342 * x344; - ℤ x350 = x340 * x346; - ℤ x351 = x338 * x348; - ℤ x352 = x350 + x351; - ℤ x353 = x349 + x352; - ℤ x354 = x342 * x346; - ℤ x355 = x340 * x348; - ℤ x356 = x354 + x355; - ℤ x357 = x338 * x344; - ℤ x358 = Const 5 * x357; - ℤ x359 = x356 + x358; - ℤ x360 = x342 * x348; - ℤ x361 = x340 * x344; - ℤ x362 = x338 * x346; - ℤ x363 = x361 + x362; - ℤ x364 = Const 5 * x363; - ℤ x365 = x360 + x364; - uint128_t x366 = x365 >> Const 85; - ℤ x367 = x366 + x359; - uint128_t x368 = x367 >> Const 85; - ℤ x369 = x368 + x353; - uint128_t x370 = x365 & Const 38685626227668133590597631; - uint128_t x371 = x369 >> Const 85; - uint128_t x372 = (uint128_t) Const 5 * x371; + uint256_t x349 = (uint256_t) x342 * (uint256_t) x344; + uint256_t x350 = (uint256_t) x340 * (uint256_t) x346; + uint256_t x351 = (uint256_t) x338 * (uint256_t) x348; + uint256_t x352 = x350 + x351; + uint256_t x353 = x349 + x352; + uint256_t x354 = (uint256_t) x342 * (uint256_t) x346; + uint256_t x355 = (uint256_t) x340 * (uint256_t) x348; + uint256_t x356 = x354 + x355; + uint256_t x357 = (uint256_t) x338 * (uint256_t) x344; + uint256_t x358 = (uint256_t) Const 5 * x357; + uint256_t x359 = x356 + x358; + uint256_t x360 = (uint256_t) x342 * (uint256_t) x348; + uint256_t x361 = (uint256_t) x340 * (uint256_t) x344; + uint256_t x362 = (uint256_t) x338 * (uint256_t) x346; + uint256_t x363 = x361 + x362; + uint256_t x364 = (uint256_t) Const 5 * x363; + uint256_t x365 = x360 + x364; + uint128_t x366 = (uint128_t) (x365 >> 0x55); + uint256_t x367 = (uint256_t) x366 + x359; + uint128_t x368 = (uint128_t) (x367 >> 0x55); + uint256_t x369 = (uint256_t) x368 + x353; + uint128_t x370 = (uint128_t) x365 & 0x1fffffffffffffffffffffL; + uint128_t x371 = (uint128_t) (x369 >> 0x55); + uint128_t x372 = Const 5 * x371; uint128_t x373 = x370 + x372; - uint64_t x374 = (uint64_t) (x373 >> Const 85); - uint128_t x375 = x367 & Const 38685626227668133590597631; - uint128_t x376 = (uint128_t) x374 + x375; - uint64_t x377 = (uint64_t) (x376 >> Const 85); - uint128_t x378 = x369 & Const 38685626227668133590597631; - uint128_t x379 = (uint128_t) x377 + x378; - uint128_t x380 = x376 & Const 38685626227668133590597631; - uint128_t x381 = x373 & Const 38685626227668133590597631; - ℤ x382 = x17 * x379; - ℤ x383 = x19 * x380; - ℤ x384 = x18 * x381; - ℤ x385 = x383 + x384; - ℤ x386 = x382 + x385; - ℤ x387 = x17 * x380; - ℤ x388 = x19 * x381; - ℤ x389 = x387 + x388; - ℤ x390 = x18 * x379; - ℤ x391 = Const 5 * x390; - ℤ x392 = x389 + x391; - ℤ x393 = x17 * x381; - ℤ x394 = x19 * x379; - ℤ x395 = x18 * x380; - ℤ x396 = x394 + x395; - ℤ x397 = Const 5 * x396; - ℤ x398 = x393 + x397; - uint128_t x399 = x398 >> Const 85; - ℤ x400 = x399 + x392; - uint128_t x401 = x400 >> Const 85; - ℤ x402 = x401 + x386; - uint128_t x403 = x398 & Const 38685626227668133590597631; - uint128_t x404 = x402 >> Const 85; - uint128_t x405 = (uint128_t) Const 5 * x404; + uint128_t x374 = (uint128_t) (x373 >> 0x55); + uint128_t x375 = (uint128_t) x367 & 0x1fffffffffffffffffffffL; + uint128_t x376 = x374 + x375; + uint128_t x377 = (uint128_t) (x376 >> 0x55); + uint128_t x378 = (uint128_t) x369 & 0x1fffffffffffffffffffffL; + uint128_t x379 = x377 + x378; + uint128_t x380 = x376 & 0x1fffffffffffffffffffffL; + uint128_t x381 = x373 & 0x1fffffffffffffffffffffL; + uint256_t x382 = (uint256_t) x17 * (uint256_t) x379; + uint256_t x383 = (uint256_t) x19 * (uint256_t) x380; + uint256_t x384 = (uint256_t) x18 * (uint256_t) x381; + uint256_t x385 = x383 + x384; + uint256_t x386 = x382 + x385; + uint256_t x387 = (uint256_t) x17 * (uint256_t) x380; + uint256_t x388 = (uint256_t) x19 * (uint256_t) x381; + uint256_t x389 = x387 + x388; + uint256_t x390 = (uint256_t) x18 * (uint256_t) x379; + uint256_t x391 = (uint256_t) Const 5 * x390; + uint256_t x392 = x389 + x391; + uint256_t x393 = (uint256_t) x17 * (uint256_t) x381; + uint256_t x394 = (uint256_t) x19 * (uint256_t) x379; + uint256_t x395 = (uint256_t) x18 * (uint256_t) x380; + uint256_t x396 = x394 + x395; + uint256_t x397 = (uint256_t) Const 5 * x396; + uint256_t x398 = x393 + x397; + uint128_t x399 = (uint128_t) (x398 >> 0x55); + uint256_t x400 = (uint256_t) x399 + x392; + uint128_t x401 = (uint128_t) (x400 >> 0x55); + uint256_t x402 = (uint256_t) x401 + x386; + uint128_t x403 = (uint128_t) x398 & 0x1fffffffffffffffffffffL; + uint128_t x404 = (uint128_t) (x402 >> 0x55); + uint128_t x405 = Const 5 * x404; uint128_t x406 = x403 + x405; - uint64_t x407 = (uint64_t) (x406 >> Const 85); - uint128_t x408 = x400 & Const 38685626227668133590597631; - uint128_t x409 = (uint128_t) x407 + x408; - uint64_t x410 = (uint64_t) (x409 >> Const 85); - uint128_t x411 = x402 & Const 38685626227668133590597631; - uint128_t x412 = (uint128_t) x410 + x411; - uint128_t x413 = x409 & Const 38685626227668133590597631; - uint128_t x414 = x406 & Const 38685626227668133590597631; + uint128_t x407 = (uint128_t) (x406 >> 0x55); + uint128_t x408 = (uint128_t) x400 & 0x1fffffffffffffffffffffL; + uint128_t x409 = x407 + x408; + uint128_t x410 = (uint128_t) (x409 >> 0x55); + uint128_t x411 = (uint128_t) x402 & 0x1fffffffffffffffffffffL; + uint128_t x412 = x410 + x411; + uint128_t x413 = x409 & 0x1fffffffffffffffffffffL; + uint128_t x414 = x406 & 0x1fffffffffffffffffffffL; (Return x145, Return x146, Return x147, (Return x220, Return x221, Return x222), (Return x334, Return x335, Return x336, (Return x412, Return x413, Return x414)))) -(x, x0, (x1, x2), (x3, x4)) in -x5 in -x5, let (_, y) := let (x5, _) := Interp-η -(λ var : Syntax.base_type → Type, - λ '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), (x34, x35, x33, (x38, x39, x37)))%core, - uint128_t x40 = x24 + x28; - uint128_t x41 = x25 + x29; - uint128_t x42 = x23 + x27; - uint128_t x43 = Const 77371252455336267181195262 + x24; - uint128_t x44 = x43 - x28; - uint128_t x45 = Const 77371252455336267181195262 + x25; - uint128_t x46 = x45 - x29; - uint128_t x47 = Const 77371252455336267181195254 + x23; - uint128_t x48 = x47 - x27; - ℤ x49 = x42 * x40; - ℤ x50 = x41 * x41; - ℤ x51 = x40 * x42; - ℤ x52 = x50 + x51; - ℤ x53 = x49 + x52; - ℤ x54 = x42 * x41; - ℤ x55 = x41 * x42; - ℤ x56 = x54 + x55; - ℤ x57 = x40 * x40; - ℤ x58 = Const 5 * x57; - ℤ x59 = x56 + x58; - ℤ x60 = x42 * x42; - ℤ x61 = x41 * x40; - ℤ x62 = x40 * x41; - ℤ x63 = x61 + x62; - ℤ x64 = Const 5 * x63; - ℤ x65 = x60 + x64; - uint128_t x66 = x65 >> Const 85; - ℤ x67 = x66 + x59; - uint128_t x68 = x67 >> Const 85; - ℤ x69 = x68 + x53; - uint128_t x70 = x65 & Const 38685626227668133590597631; - uint128_t x71 = x69 >> Const 85; - uint128_t x72 = (uint128_t) Const 5 * x71; - uint128_t x73 = x70 + x72; - uint64_t x74 = (uint64_t) (x73 >> Const 85); - uint128_t x75 = x67 & Const 38685626227668133590597631; - uint128_t x76 = (uint128_t) x74 + x75; - uint64_t x77 = (uint64_t) (x76 >> Const 85); - uint128_t x78 = x69 & Const 38685626227668133590597631; - uint128_t x79 = (uint128_t) x77 + x78; - uint128_t x80 = x76 & Const 38685626227668133590597631; - uint128_t x81 = x73 & Const 38685626227668133590597631; - ℤ x82 = x48 * x44; - ℤ x83 = x46 * x46; - ℤ x84 = x44 * x48; - ℤ x85 = x83 + x84; - ℤ x86 = x82 + x85; - ℤ x87 = x48 * x46; - ℤ x88 = x46 * x48; - ℤ x89 = x87 + x88; - ℤ x90 = x44 * x44; - ℤ x91 = Const 5 * x90; - ℤ x92 = x89 + x91; - ℤ x93 = x48 * x48; - ℤ x94 = x46 * x44; - ℤ x95 = x44 * x46; - ℤ x96 = x94 + x95; - ℤ x97 = Const 5 * x96; - ℤ x98 = x93 + x97; - uint128_t x99 = x98 >> Const 85; - ℤ x100 = x99 + x92; - uint128_t x101 = x100 >> Const 85; - ℤ x102 = x101 + x86; - uint128_t x103 = x98 & Const 38685626227668133590597631; - uint128_t x104 = x102 >> Const 85; - uint128_t x105 = (uint128_t) Const 5 * x104; - uint128_t x106 = x103 + x105; - uint64_t x107 = (uint64_t) (x106 >> Const 85); - uint128_t x108 = x100 & Const 38685626227668133590597631; - uint128_t x109 = (uint128_t) x107 + x108; - uint64_t x110 = (uint64_t) (x109 >> Const 85); - uint128_t x111 = x102 & Const 38685626227668133590597631; - uint128_t x112 = (uint128_t) x110 + x111; - uint128_t x113 = x109 & Const 38685626227668133590597631; - uint128_t x114 = x106 & Const 38685626227668133590597631; - ℤ x115 = x81 * x112; - ℤ x116 = x80 * x113; - ℤ x117 = x79 * x114; - ℤ x118 = x116 + x117; - ℤ x119 = x115 + x118; - ℤ x120 = x81 * x113; - ℤ x121 = x80 * x114; - ℤ x122 = x120 + x121; - ℤ x123 = x79 * x112; - ℤ x124 = Const 5 * x123; - ℤ x125 = x122 + x124; - ℤ x126 = x81 * x114; - ℤ x127 = x80 * x112; - ℤ x128 = x79 * x113; - ℤ x129 = x127 + x128; - ℤ x130 = Const 5 * x129; - ℤ x131 = x126 + x130; - uint128_t x132 = x131 >> Const 85; - ℤ x133 = x132 + x125; - uint128_t x134 = x133 >> Const 85; - ℤ x135 = x134 + x119; - uint128_t x136 = x131 & Const 38685626227668133590597631; - uint128_t x137 = x135 >> Const 85; - uint128_t x138 = (uint128_t) Const 5 * x137; - uint128_t x139 = x136 + x138; - uint64_t x140 = (uint64_t) (x139 >> Const 85); - uint128_t x141 = x133 & Const 38685626227668133590597631; - uint128_t x142 = (uint128_t) x140 + x141; - uint64_t x143 = (uint64_t) (x142 >> Const 85); - uint128_t x144 = x135 & Const 38685626227668133590597631; - uint128_t x145 = (uint128_t) x143 + x144; - uint128_t x146 = x142 & Const 38685626227668133590597631; - uint128_t x147 = x139 & Const 38685626227668133590597631; - uint128_t x148 = Const 77371252455336267181195262 + x79; - uint128_t x149 = x148 - x112; - uint128_t x150 = Const 77371252455336267181195262 + x80; - uint128_t x151 = x150 - x113; - uint128_t x152 = Const 77371252455336267181195254 + x81; - uint128_t x153 = x152 - x114; - ℤ x154 = x13 * x149; - ℤ x155 = x15 * x151; - ℤ x156 = x14 * x153; - ℤ x157 = x155 + x156; - ℤ x158 = x154 + x157; - ℤ x159 = x13 * x151; - ℤ x160 = x15 * x153; - ℤ x161 = x159 + x160; - ℤ x162 = x14 * x149; - ℤ x163 = Const 5 * x162; - ℤ x164 = x161 + x163; - ℤ x165 = x13 * x153; - ℤ x166 = x15 * x149; - ℤ x167 = x14 * x151; - ℤ x168 = x166 + x167; - ℤ x169 = Const 5 * x168; - ℤ x170 = x165 + x169; - uint128_t x171 = x170 >> Const 85; - ℤ x172 = x171 + x164; - uint128_t x173 = x172 >> Const 85; - ℤ x174 = x173 + x158; - uint128_t x175 = x170 & Const 38685626227668133590597631; - uint128_t x176 = x174 >> Const 85; - uint128_t x177 = (uint128_t) Const 5 * x176; - uint128_t x178 = x175 + x177; - uint64_t x179 = (uint64_t) (x178 >> Const 85); - uint128_t x180 = x172 & Const 38685626227668133590597631; - uint128_t x181 = (uint128_t) x179 + x180; - uint64_t x182 = (uint64_t) (x181 >> Const 85); - uint128_t x183 = x174 & Const 38685626227668133590597631; - uint128_t x184 = (uint128_t) x182 + x183; - uint128_t x185 = x181 & Const 38685626227668133590597631; - uint128_t x186 = x178 & Const 38685626227668133590597631; - uint128_t x187 = x79 + x184; - uint128_t x188 = x80 + x185; - uint128_t x189 = x81 + x186; - ℤ x190 = x153 * x187; - ℤ x191 = x151 * x188; - ℤ x192 = x149 * x189; - ℤ x193 = x191 + x192; - ℤ x194 = x190 + x193; - ℤ x195 = x153 * x188; - ℤ x196 = x151 * x189; - ℤ x197 = x195 + x196; - ℤ x198 = x149 * x187; - ℤ x199 = Const 5 * x198; - ℤ x200 = x197 + x199; - ℤ x201 = x153 * x189; - ℤ x202 = x151 * x187; - ℤ x203 = x149 * x188; - ℤ x204 = x202 + x203; - ℤ x205 = Const 5 * x204; - ℤ x206 = x201 + x205; - uint128_t x207 = x206 >> Const 85; - ℤ x208 = x207 + x200; - uint128_t x209 = x208 >> Const 85; - ℤ x210 = x209 + x194; - uint128_t x211 = x206 & Const 38685626227668133590597631; - uint128_t x212 = x210 >> Const 85; - uint128_t x213 = (uint128_t) Const 5 * x212; - uint128_t x214 = x211 + x213; - uint64_t x215 = (uint64_t) (x214 >> Const 85); - uint128_t x216 = x208 & Const 38685626227668133590597631; - uint128_t x217 = (uint128_t) x215 + x216; - uint64_t x218 = (uint64_t) (x217 >> Const 85); - uint128_t x219 = x210 & Const 38685626227668133590597631; - uint128_t x220 = (uint128_t) x218 + x219; - uint128_t x221 = x217 & Const 38685626227668133590597631; - uint128_t x222 = x214 & Const 38685626227668133590597631; - uint128_t x223 = x34 + x38; - uint128_t x224 = x35 + x39; - uint128_t x225 = x33 + x37; - uint128_t x226 = Const 77371252455336267181195262 + x34; - uint128_t x227 = x226 - x38; - uint128_t x228 = Const 77371252455336267181195262 + x35; - uint128_t x229 = x228 - x39; - uint128_t x230 = Const 77371252455336267181195254 + x33; - uint128_t x231 = x230 - x37; - ℤ x232 = x225 * x44; - ℤ x233 = x224 * x46; - ℤ x234 = x223 * x48; - ℤ x235 = x233 + x234; - ℤ x236 = x232 + x235; - ℤ x237 = x225 * x46; - ℤ x238 = x224 * x48; - ℤ x239 = x237 + x238; - ℤ x240 = x223 * x44; - ℤ x241 = Const 5 * x240; - ℤ x242 = x239 + x241; - ℤ x243 = x225 * x48; - ℤ x244 = x224 * x44; - ℤ x245 = x223 * x46; - ℤ x246 = x244 + x245; - ℤ x247 = Const 5 * x246; - ℤ x248 = x243 + x247; - uint128_t x249 = x248 >> Const 85; - ℤ x250 = x249 + x242; - uint128_t x251 = x250 >> Const 85; - ℤ x252 = x251 + x236; - uint128_t x253 = x248 & Const 38685626227668133590597631; - uint128_t x254 = x252 >> Const 85; - uint128_t x255 = (uint128_t) Const 5 * x254; - uint128_t x256 = x253 + x255; - uint64_t x257 = (uint64_t) (x256 >> Const 85); - uint128_t x258 = x250 & Const 38685626227668133590597631; - uint128_t x259 = (uint128_t) x257 + x258; - uint64_t x260 = (uint64_t) (x259 >> Const 85); - uint128_t x261 = x252 & Const 38685626227668133590597631; - uint128_t x262 = (uint128_t) x260 + x261; - uint128_t x263 = x259 & Const 38685626227668133590597631; - uint128_t x264 = x256 & Const 38685626227668133590597631; - ℤ x265 = x231 * x40; - ℤ x266 = x229 * x41; - ℤ x267 = x227 * x42; - ℤ x268 = x266 + x267; - ℤ x269 = x265 + x268; - ℤ x270 = x231 * x41; - ℤ x271 = x229 * x42; - ℤ x272 = x270 + x271; - ℤ x273 = x227 * x40; - ℤ x274 = Const 5 * x273; - ℤ x275 = x272 + x274; - ℤ x276 = x231 * x42; - ℤ x277 = x229 * x40; - ℤ x278 = x227 * x41; - ℤ x279 = x277 + x278; - ℤ x280 = Const 5 * x279; - ℤ x281 = x276 + x280; - uint128_t x282 = x281 >> Const 85; - ℤ x283 = x282 + x275; - uint128_t x284 = x283 >> Const 85; - ℤ x285 = x284 + x269; - uint128_t x286 = x281 & Const 38685626227668133590597631; - uint128_t x287 = x285 >> Const 85; - uint128_t x288 = (uint128_t) Const 5 * x287; - uint128_t x289 = x286 + x288; - uint64_t x290 = (uint64_t) (x289 >> Const 85); - uint128_t x291 = x283 & Const 38685626227668133590597631; - uint128_t x292 = (uint128_t) x290 + x291; - uint64_t x293 = (uint64_t) (x292 >> Const 85); - uint128_t x294 = x285 & Const 38685626227668133590597631; - uint128_t x295 = (uint128_t) x293 + x294; - uint128_t x296 = x292 & Const 38685626227668133590597631; - uint128_t x297 = x289 & Const 38685626227668133590597631; - uint128_t x298 = x295 + x262; - uint128_t x299 = x296 + x263; - uint128_t x300 = x297 + x264; - uint128_t x301 = x295 + x262; - uint128_t x302 = x296 + x263; - uint128_t x303 = x297 + x264; - ℤ x304 = x300 * x301; - ℤ x305 = x299 * x302; - ℤ x306 = x298 * x303; - ℤ x307 = x305 + x306; - ℤ x308 = x304 + x307; - ℤ x309 = x300 * x302; - ℤ x310 = x299 * x303; - ℤ x311 = x309 + x310; - ℤ x312 = x298 * x301; - ℤ x313 = Const 5 * x312; - ℤ x314 = x311 + x313; - ℤ x315 = x300 * x303; - ℤ x316 = x299 * x301; - ℤ x317 = x298 * x302; - ℤ x318 = x316 + x317; - ℤ x319 = Const 5 * x318; - ℤ x320 = x315 + x319; - uint128_t x321 = x320 >> Const 85; - ℤ x322 = x321 + x314; - uint128_t x323 = x322 >> Const 85; - ℤ x324 = x323 + x308; - uint128_t x325 = x320 & Const 38685626227668133590597631; - uint128_t x326 = x324 >> Const 85; - uint128_t x327 = (uint128_t) Const 5 * x326; - uint128_t x328 = x325 + x327; - uint64_t x329 = (uint64_t) (x328 >> Const 85); - uint128_t x330 = x322 & Const 38685626227668133590597631; - uint128_t x331 = (uint128_t) x329 + x330; - uint64_t x332 = (uint64_t) (x331 >> Const 85); - uint128_t x333 = x324 & Const 38685626227668133590597631; - uint128_t x334 = (uint128_t) x332 + x333; - uint128_t x335 = x331 & Const 38685626227668133590597631; - uint128_t x336 = x328 & Const 38685626227668133590597631; - uint128_t x337 = Const 77371252455336267181195262 + x295; - uint128_t x338 = x337 - x262; - uint128_t x339 = Const 77371252455336267181195262 + x296; - uint128_t x340 = x339 - x263; - uint128_t x341 = Const 77371252455336267181195254 + x297; - uint128_t x342 = x341 - x264; - uint128_t x343 = Const 77371252455336267181195262 + x295; - uint128_t x344 = x343 - x262; - uint128_t x345 = Const 77371252455336267181195262 + x296; - uint128_t x346 = x345 - x263; - uint128_t x347 = Const 77371252455336267181195254 + x297; - uint128_t x348 = x347 - x264; - ℤ x349 = x342 * x344; - ℤ x350 = x340 * x346; - ℤ x351 = x338 * x348; - ℤ x352 = x350 + x351; - ℤ x353 = x349 + x352; - ℤ x354 = x342 * x346; - ℤ x355 = x340 * x348; - ℤ x356 = x354 + x355; - ℤ x357 = x338 * x344; - ℤ x358 = Const 5 * x357; - ℤ x359 = x356 + x358; - ℤ x360 = x342 * x348; - ℤ x361 = x340 * x344; - ℤ x362 = x338 * x346; - ℤ x363 = x361 + x362; - ℤ x364 = Const 5 * x363; - ℤ x365 = x360 + x364; - uint128_t x366 = x365 >> Const 85; - ℤ x367 = x366 + x359; - uint128_t x368 = x367 >> Const 85; - ℤ x369 = x368 + x353; - uint128_t x370 = x365 & Const 38685626227668133590597631; - uint128_t x371 = x369 >> Const 85; - uint128_t x372 = (uint128_t) Const 5 * x371; - uint128_t x373 = x370 + x372; - uint64_t x374 = (uint64_t) (x373 >> Const 85); - uint128_t x375 = x367 & Const 38685626227668133590597631; - uint128_t x376 = (uint128_t) x374 + x375; - uint64_t x377 = (uint64_t) (x376 >> Const 85); - uint128_t x378 = x369 & Const 38685626227668133590597631; - uint128_t x379 = (uint128_t) x377 + x378; - uint128_t x380 = x376 & Const 38685626227668133590597631; - uint128_t x381 = x373 & Const 38685626227668133590597631; - ℤ x382 = x17 * x379; - ℤ x383 = x19 * x380; - ℤ x384 = x18 * x381; - ℤ x385 = x383 + x384; - ℤ x386 = x382 + x385; - ℤ x387 = x17 * x380; - ℤ x388 = x19 * x381; - ℤ x389 = x387 + x388; - ℤ x390 = x18 * x379; - ℤ x391 = Const 5 * x390; - ℤ x392 = x389 + x391; - ℤ x393 = x17 * x381; - ℤ x394 = x19 * x379; - ℤ x395 = x18 * x380; - ℤ x396 = x394 + x395; - ℤ x397 = Const 5 * x396; - ℤ x398 = x393 + x397; - uint128_t x399 = x398 >> Const 85; - ℤ x400 = x399 + x392; - uint128_t x401 = x400 >> Const 85; - ℤ x402 = x401 + x386; - uint128_t x403 = x398 & Const 38685626227668133590597631; - uint128_t x404 = x402 >> Const 85; - uint128_t x405 = (uint128_t) Const 5 * x404; - uint128_t x406 = x403 + x405; - uint64_t x407 = (uint64_t) (x406 >> Const 85); - uint128_t x408 = x400 & Const 38685626227668133590597631; - uint128_t x409 = (uint128_t) x407 + x408; - uint64_t x410 = (uint64_t) (x409 >> Const 85); - uint128_t x411 = x402 & Const 38685626227668133590597631; - uint128_t x412 = (uint128_t) x410 + x411; - uint128_t x413 = x409 & Const 38685626227668133590597631; - uint128_t x414 = x406 & Const 38685626227668133590597631; - (Return x145, Return x146, Return x147, (Return x220, Return x221, Return x222), (Return x334, Return x335, Return x336, (Return x412, Return x413, Return x414)))) -(x, x0, (x1, x2), (x3, x4)) in -x5 in -y, (let (x5, _) := let (_, y) := Interp-η - (λ var : Syntax.base_type → Type, - λ '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), (x34, x35, x33, (x38, x39, x37)))%core, - uint128_t x40 = x24 + x28; - uint128_t x41 = x25 + x29; - uint128_t x42 = x23 + x27; - uint128_t x43 = Const 77371252455336267181195262 + x24; - uint128_t x44 = x43 - x28; - uint128_t x45 = Const 77371252455336267181195262 + x25; - uint128_t x46 = x45 - x29; - uint128_t x47 = Const 77371252455336267181195254 + x23; - uint128_t x48 = x47 - x27; - ℤ x49 = x42 * x40; - ℤ x50 = x41 * x41; - ℤ x51 = x40 * x42; - ℤ x52 = x50 + x51; - ℤ x53 = x49 + x52; - ℤ x54 = x42 * x41; - ℤ x55 = x41 * x42; - ℤ x56 = x54 + x55; - ℤ x57 = x40 * x40; - ℤ x58 = Const 5 * x57; - ℤ x59 = x56 + x58; - ℤ x60 = x42 * x42; - ℤ x61 = x41 * x40; - ℤ x62 = x40 * x41; - ℤ x63 = x61 + x62; - ℤ x64 = Const 5 * x63; - ℤ x65 = x60 + x64; - uint128_t x66 = x65 >> Const 85; - ℤ x67 = x66 + x59; - uint128_t x68 = x67 >> Const 85; - ℤ x69 = x68 + x53; - uint128_t x70 = x65 & Const 38685626227668133590597631; - uint128_t x71 = x69 >> Const 85; - uint128_t x72 = (uint128_t) Const 5 * x71; - uint128_t x73 = x70 + x72; - uint64_t x74 = (uint64_t) (x73 >> Const 85); - uint128_t x75 = x67 & Const 38685626227668133590597631; - uint128_t x76 = (uint128_t) x74 + x75; - uint64_t x77 = (uint64_t) (x76 >> Const 85); - uint128_t x78 = x69 & Const 38685626227668133590597631; - uint128_t x79 = (uint128_t) x77 + x78; - uint128_t x80 = x76 & Const 38685626227668133590597631; - uint128_t x81 = x73 & Const 38685626227668133590597631; - ℤ x82 = x48 * x44; - ℤ x83 = x46 * x46; - ℤ x84 = x44 * x48; - ℤ x85 = x83 + x84; - ℤ x86 = x82 + x85; - ℤ x87 = x48 * x46; - ℤ x88 = x46 * x48; - ℤ x89 = x87 + x88; - ℤ x90 = x44 * x44; - ℤ x91 = Const 5 * x90; - ℤ x92 = x89 + x91; - ℤ x93 = x48 * x48; - ℤ x94 = x46 * x44; - ℤ x95 = x44 * x46; - ℤ x96 = x94 + x95; - ℤ x97 = Const 5 * x96; - ℤ x98 = x93 + x97; - uint128_t x99 = x98 >> Const 85; - ℤ x100 = x99 + x92; - uint128_t x101 = x100 >> Const 85; - ℤ x102 = x101 + x86; - uint128_t x103 = x98 & Const 38685626227668133590597631; - uint128_t x104 = x102 >> Const 85; - uint128_t x105 = (uint128_t) Const 5 * x104; - uint128_t x106 = x103 + x105; - uint64_t x107 = (uint64_t) (x106 >> Const 85); - uint128_t x108 = x100 & Const 38685626227668133590597631; - uint128_t x109 = (uint128_t) x107 + x108; - uint64_t x110 = (uint64_t) (x109 >> Const 85); - uint128_t x111 = x102 & Const 38685626227668133590597631; - uint128_t x112 = (uint128_t) x110 + x111; - uint128_t x113 = x109 & Const 38685626227668133590597631; - uint128_t x114 = x106 & Const 38685626227668133590597631; - ℤ x115 = x81 * x112; - ℤ x116 = x80 * x113; - ℤ x117 = x79 * x114; - ℤ x118 = x116 + x117; - ℤ x119 = x115 + x118; - ℤ x120 = x81 * x113; - ℤ x121 = x80 * x114; - ℤ x122 = x120 + x121; - ℤ x123 = x79 * x112; - ℤ x124 = Const 5 * x123; - ℤ x125 = x122 + x124; - ℤ x126 = x81 * x114; - ℤ x127 = x80 * x112; - ℤ x128 = x79 * x113; - ℤ x129 = x127 + x128; - ℤ x130 = Const 5 * x129; - ℤ x131 = x126 + x130; - uint128_t x132 = x131 >> Const 85; - ℤ x133 = x132 + x125; - uint128_t x134 = x133 >> Const 85; - ℤ x135 = x134 + x119; - uint128_t x136 = x131 & Const 38685626227668133590597631; - uint128_t x137 = x135 >> Const 85; - uint128_t x138 = (uint128_t) Const 5 * x137; - uint128_t x139 = x136 + x138; - uint64_t x140 = (uint64_t) (x139 >> Const 85); - uint128_t x141 = x133 & Const 38685626227668133590597631; - uint128_t x142 = (uint128_t) x140 + x141; - uint64_t x143 = (uint64_t) (x142 >> Const 85); - uint128_t x144 = x135 & Const 38685626227668133590597631; - uint128_t x145 = (uint128_t) x143 + x144; - uint128_t x146 = x142 & Const 38685626227668133590597631; - uint128_t x147 = x139 & Const 38685626227668133590597631; - uint128_t x148 = Const 77371252455336267181195262 + x79; - uint128_t x149 = x148 - x112; - uint128_t x150 = Const 77371252455336267181195262 + x80; - uint128_t x151 = x150 - x113; - uint128_t x152 = Const 77371252455336267181195254 + x81; - uint128_t x153 = x152 - x114; - ℤ x154 = x13 * x149; - ℤ x155 = x15 * x151; - ℤ x156 = x14 * x153; - ℤ x157 = x155 + x156; - ℤ x158 = x154 + x157; - ℤ x159 = x13 * x151; - ℤ x160 = x15 * x153; - ℤ x161 = x159 + x160; - ℤ x162 = x14 * x149; - ℤ x163 = Const 5 * x162; - ℤ x164 = x161 + x163; - ℤ x165 = x13 * x153; - ℤ x166 = x15 * x149; - ℤ x167 = x14 * x151; - ℤ x168 = x166 + x167; - ℤ x169 = Const 5 * x168; - ℤ x170 = x165 + x169; - uint128_t x171 = x170 >> Const 85; - ℤ x172 = x171 + x164; - uint128_t x173 = x172 >> Const 85; - ℤ x174 = x173 + x158; - uint128_t x175 = x170 & Const 38685626227668133590597631; - uint128_t x176 = x174 >> Const 85; - uint128_t x177 = (uint128_t) Const 5 * x176; - uint128_t x178 = x175 + x177; - uint64_t x179 = (uint64_t) (x178 >> Const 85); - uint128_t x180 = x172 & Const 38685626227668133590597631; - uint128_t x181 = (uint128_t) x179 + x180; - uint64_t x182 = (uint64_t) (x181 >> Const 85); - uint128_t x183 = x174 & Const 38685626227668133590597631; - uint128_t x184 = (uint128_t) x182 + x183; - uint128_t x185 = x181 & Const 38685626227668133590597631; - uint128_t x186 = x178 & Const 38685626227668133590597631; - uint128_t x187 = x79 + x184; - uint128_t x188 = x80 + x185; - uint128_t x189 = x81 + x186; - ℤ x190 = x153 * x187; - ℤ x191 = x151 * x188; - ℤ x192 = x149 * x189; - ℤ x193 = x191 + x192; - ℤ x194 = x190 + x193; - ℤ x195 = x153 * x188; - ℤ x196 = x151 * x189; - ℤ x197 = x195 + x196; - ℤ x198 = x149 * x187; - ℤ x199 = Const 5 * x198; - ℤ x200 = x197 + x199; - ℤ x201 = x153 * x189; - ℤ x202 = x151 * x187; - ℤ x203 = x149 * x188; - ℤ x204 = x202 + x203; - ℤ x205 = Const 5 * x204; - ℤ x206 = x201 + x205; - uint128_t x207 = x206 >> Const 85; - ℤ x208 = x207 + x200; - uint128_t x209 = x208 >> Const 85; - ℤ x210 = x209 + x194; - uint128_t x211 = x206 & Const 38685626227668133590597631; - uint128_t x212 = x210 >> Const 85; - uint128_t x213 = (uint128_t) Const 5 * x212; - uint128_t x214 = x211 + x213; - uint64_t x215 = (uint64_t) (x214 >> Const 85); - uint128_t x216 = x208 & Const 38685626227668133590597631; - uint128_t x217 = (uint128_t) x215 + x216; - uint64_t x218 = (uint64_t) (x217 >> Const 85); - uint128_t x219 = x210 & Const 38685626227668133590597631; - uint128_t x220 = (uint128_t) x218 + x219; - uint128_t x221 = x217 & Const 38685626227668133590597631; - uint128_t x222 = x214 & Const 38685626227668133590597631; - uint128_t x223 = x34 + x38; - uint128_t x224 = x35 + x39; - uint128_t x225 = x33 + x37; - uint128_t x226 = Const 77371252455336267181195262 + x34; - uint128_t x227 = x226 - x38; - uint128_t x228 = Const 77371252455336267181195262 + x35; - uint128_t x229 = x228 - x39; - uint128_t x230 = Const 77371252455336267181195254 + x33; - uint128_t x231 = x230 - x37; - ℤ x232 = x225 * x44; - ℤ x233 = x224 * x46; - ℤ x234 = x223 * x48; - ℤ x235 = x233 + x234; - ℤ x236 = x232 + x235; - ℤ x237 = x225 * x46; - ℤ x238 = x224 * x48; - ℤ x239 = x237 + x238; - ℤ x240 = x223 * x44; - ℤ x241 = Const 5 * x240; - ℤ x242 = x239 + x241; - ℤ x243 = x225 * x48; - ℤ x244 = x224 * x44; - ℤ x245 = x223 * x46; - ℤ x246 = x244 + x245; - ℤ x247 = Const 5 * x246; - ℤ x248 = x243 + x247; - uint128_t x249 = x248 >> Const 85; - ℤ x250 = x249 + x242; - uint128_t x251 = x250 >> Const 85; - ℤ x252 = x251 + x236; - uint128_t x253 = x248 & Const 38685626227668133590597631; - uint128_t x254 = x252 >> Const 85; - uint128_t x255 = (uint128_t) Const 5 * x254; - uint128_t x256 = x253 + x255; - uint64_t x257 = (uint64_t) (x256 >> Const 85); - uint128_t x258 = x250 & Const 38685626227668133590597631; - uint128_t x259 = (uint128_t) x257 + x258; - uint64_t x260 = (uint64_t) (x259 >> Const 85); - uint128_t x261 = x252 & Const 38685626227668133590597631; - uint128_t x262 = (uint128_t) x260 + x261; - uint128_t x263 = x259 & Const 38685626227668133590597631; - uint128_t x264 = x256 & Const 38685626227668133590597631; - ℤ x265 = x231 * x40; - ℤ x266 = x229 * x41; - ℤ x267 = x227 * x42; - ℤ x268 = x266 + x267; - ℤ x269 = x265 + x268; - ℤ x270 = x231 * x41; - ℤ x271 = x229 * x42; - ℤ x272 = x270 + x271; - ℤ x273 = x227 * x40; - ℤ x274 = Const 5 * x273; - ℤ x275 = x272 + x274; - ℤ x276 = x231 * x42; - ℤ x277 = x229 * x40; - ℤ x278 = x227 * x41; - ℤ x279 = x277 + x278; - ℤ x280 = Const 5 * x279; - ℤ x281 = x276 + x280; - uint128_t x282 = x281 >> Const 85; - ℤ x283 = x282 + x275; - uint128_t x284 = x283 >> Const 85; - ℤ x285 = x284 + x269; - uint128_t x286 = x281 & Const 38685626227668133590597631; - uint128_t x287 = x285 >> Const 85; - uint128_t x288 = (uint128_t) Const 5 * x287; - uint128_t x289 = x286 + x288; - uint64_t x290 = (uint64_t) (x289 >> Const 85); - uint128_t x291 = x283 & Const 38685626227668133590597631; - uint128_t x292 = (uint128_t) x290 + x291; - uint64_t x293 = (uint64_t) (x292 >> Const 85); - uint128_t x294 = x285 & Const 38685626227668133590597631; - uint128_t x295 = (uint128_t) x293 + x294; - uint128_t x296 = x292 & Const 38685626227668133590597631; - uint128_t x297 = x289 & Const 38685626227668133590597631; - uint128_t x298 = x295 + x262; - uint128_t x299 = x296 + x263; - uint128_t x300 = x297 + x264; - uint128_t x301 = x295 + x262; - uint128_t x302 = x296 + x263; - uint128_t x303 = x297 + x264; - ℤ x304 = x300 * x301; - ℤ x305 = x299 * x302; - ℤ x306 = x298 * x303; - ℤ x307 = x305 + x306; - ℤ x308 = x304 + x307; - ℤ x309 = x300 * x302; - ℤ x310 = x299 * x303; - ℤ x311 = x309 + x310; - ℤ x312 = x298 * x301; - ℤ x313 = Const 5 * x312; - ℤ x314 = x311 + x313; - ℤ x315 = x300 * x303; - ℤ x316 = x299 * x301; - ℤ x317 = x298 * x302; - ℤ x318 = x316 + x317; - ℤ x319 = Const 5 * x318; - ℤ x320 = x315 + x319; - uint128_t x321 = x320 >> Const 85; - ℤ x322 = x321 + x314; - uint128_t x323 = x322 >> Const 85; - ℤ x324 = x323 + x308; - uint128_t x325 = x320 & Const 38685626227668133590597631; - uint128_t x326 = x324 >> Const 85; - uint128_t x327 = (uint128_t) Const 5 * x326; - uint128_t x328 = x325 + x327; - uint64_t x329 = (uint64_t) (x328 >> Const 85); - uint128_t x330 = x322 & Const 38685626227668133590597631; - uint128_t x331 = (uint128_t) x329 + x330; - uint64_t x332 = (uint64_t) (x331 >> Const 85); - uint128_t x333 = x324 & Const 38685626227668133590597631; - uint128_t x334 = (uint128_t) x332 + x333; - uint128_t x335 = x331 & Const 38685626227668133590597631; - uint128_t x336 = x328 & Const 38685626227668133590597631; - uint128_t x337 = Const 77371252455336267181195262 + x295; - uint128_t x338 = x337 - x262; - uint128_t x339 = Const 77371252455336267181195262 + x296; - uint128_t x340 = x339 - x263; - uint128_t x341 = Const 77371252455336267181195254 + x297; - uint128_t x342 = x341 - x264; - uint128_t x343 = Const 77371252455336267181195262 + x295; - uint128_t x344 = x343 - x262; - uint128_t x345 = Const 77371252455336267181195262 + x296; - uint128_t x346 = x345 - x263; - uint128_t x347 = Const 77371252455336267181195254 + x297; - uint128_t x348 = x347 - x264; - ℤ x349 = x342 * x344; - ℤ x350 = x340 * x346; - ℤ x351 = x338 * x348; - ℤ x352 = x350 + x351; - ℤ x353 = x349 + x352; - ℤ x354 = x342 * x346; - ℤ x355 = x340 * x348; - ℤ x356 = x354 + x355; - ℤ x357 = x338 * x344; - ℤ x358 = Const 5 * x357; - ℤ x359 = x356 + x358; - ℤ x360 = x342 * x348; - ℤ x361 = x340 * x344; - ℤ x362 = x338 * x346; - ℤ x363 = x361 + x362; - ℤ x364 = Const 5 * x363; - ℤ x365 = x360 + x364; - uint128_t x366 = x365 >> Const 85; - ℤ x367 = x366 + x359; - uint128_t x368 = x367 >> Const 85; - ℤ x369 = x368 + x353; - uint128_t x370 = x365 & Const 38685626227668133590597631; - uint128_t x371 = x369 >> Const 85; - uint128_t x372 = (uint128_t) Const 5 * x371; - uint128_t x373 = x370 + x372; - uint64_t x374 = (uint64_t) (x373 >> Const 85); - uint128_t x375 = x367 & Const 38685626227668133590597631; - uint128_t x376 = (uint128_t) x374 + x375; - uint64_t x377 = (uint64_t) (x376 >> Const 85); - uint128_t x378 = x369 & Const 38685626227668133590597631; - uint128_t x379 = (uint128_t) x377 + x378; - uint128_t x380 = x376 & Const 38685626227668133590597631; - uint128_t x381 = x373 & Const 38685626227668133590597631; - ℤ x382 = x17 * x379; - ℤ x383 = x19 * x380; - ℤ x384 = x18 * x381; - ℤ x385 = x383 + x384; - ℤ x386 = x382 + x385; - ℤ x387 = x17 * x380; - ℤ x388 = x19 * x381; - ℤ x389 = x387 + x388; - ℤ x390 = x18 * x379; - ℤ x391 = Const 5 * x390; - ℤ x392 = x389 + x391; - ℤ x393 = x17 * x381; - ℤ x394 = x19 * x379; - ℤ x395 = x18 * x380; - ℤ x396 = x394 + x395; - ℤ x397 = Const 5 * x396; - ℤ x398 = x393 + x397; - uint128_t x399 = x398 >> Const 85; - ℤ x400 = x399 + x392; - uint128_t x401 = x400 >> Const 85; - ℤ x402 = x401 + x386; - uint128_t x403 = x398 & Const 38685626227668133590597631; - uint128_t x404 = x402 >> Const 85; - uint128_t x405 = (uint128_t) Const 5 * x404; - uint128_t x406 = x403 + x405; - uint64_t x407 = (uint64_t) (x406 >> Const 85); - uint128_t x408 = x400 & Const 38685626227668133590597631; - uint128_t x409 = (uint128_t) x407 + x408; - uint64_t x410 = (uint64_t) (x409 >> Const 85); - uint128_t x411 = x402 & Const 38685626227668133590597631; - uint128_t x412 = (uint128_t) x410 + x411; - uint128_t x413 = x409 & Const 38685626227668133590597631; - uint128_t x414 = x406 & Const 38685626227668133590597631; - (Return x145, Return x146, Return x147, (Return x220, Return x221, Return x222), (Return x334, Return x335, Return x336, (Return x412, Return x413, Return x414)))) - (x, x0, (x1, x2), (x3, x4)) in - y in - x5, let (_, y) := let (_, y) := Interp-η - (λ var : Syntax.base_type → Type, - λ '(x14, x15, x13, (x18, x19, x17), (x24, x25, x23, (x28, x29, x27)), (x34, x35, x33, (x38, x39, x37)))%core, - uint128_t x40 = x24 + x28; - uint128_t x41 = x25 + x29; - uint128_t x42 = x23 + x27; - uint128_t x43 = Const 77371252455336267181195262 + x24; - uint128_t x44 = x43 - x28; - uint128_t x45 = Const 77371252455336267181195262 + x25; - uint128_t x46 = x45 - x29; - uint128_t x47 = Const 77371252455336267181195254 + x23; - uint128_t x48 = x47 - x27; - ℤ x49 = x42 * x40; - ℤ x50 = x41 * x41; - ℤ x51 = x40 * x42; - ℤ x52 = x50 + x51; - ℤ x53 = x49 + x52; - ℤ x54 = x42 * x41; - ℤ x55 = x41 * x42; - ℤ x56 = x54 + x55; - ℤ x57 = x40 * x40; - ℤ x58 = Const 5 * x57; - ℤ x59 = x56 + x58; - ℤ x60 = x42 * x42; - ℤ x61 = x41 * x40; - ℤ x62 = x40 * x41; - ℤ x63 = x61 + x62; - ℤ x64 = Const 5 * x63; - ℤ x65 = x60 + x64; - uint128_t x66 = x65 >> Const 85; - ℤ x67 = x66 + x59; - uint128_t x68 = x67 >> Const 85; - ℤ x69 = x68 + x53; - uint128_t x70 = x65 & Const 38685626227668133590597631; - uint128_t x71 = x69 >> Const 85; - uint128_t x72 = (uint128_t) Const 5 * x71; - uint128_t x73 = x70 + x72; - uint64_t x74 = (uint64_t) (x73 >> Const 85); - uint128_t x75 = x67 & Const 38685626227668133590597631; - uint128_t x76 = (uint128_t) x74 + x75; - uint64_t x77 = (uint64_t) (x76 >> Const 85); - uint128_t x78 = x69 & Const 38685626227668133590597631; - uint128_t x79 = (uint128_t) x77 + x78; - uint128_t x80 = x76 & Const 38685626227668133590597631; - uint128_t x81 = x73 & Const 38685626227668133590597631; - ℤ x82 = x48 * x44; - ℤ x83 = x46 * x46; - ℤ x84 = x44 * x48; - ℤ x85 = x83 + x84; - ℤ x86 = x82 + x85; - ℤ x87 = x48 * x46; - ℤ x88 = x46 * x48; - ℤ x89 = x87 + x88; - ℤ x90 = x44 * x44; - ℤ x91 = Const 5 * x90; - ℤ x92 = x89 + x91; - ℤ x93 = x48 * x48; - ℤ x94 = x46 * x44; - ℤ x95 = x44 * x46; - ℤ x96 = x94 + x95; - ℤ x97 = Const 5 * x96; - ℤ x98 = x93 + x97; - uint128_t x99 = x98 >> Const 85; - ℤ x100 = x99 + x92; - uint128_t x101 = x100 >> Const 85; - ℤ x102 = x101 + x86; - uint128_t x103 = x98 & Const 38685626227668133590597631; - uint128_t x104 = x102 >> Const 85; - uint128_t x105 = (uint128_t) Const 5 * x104; - uint128_t x106 = x103 + x105; - uint64_t x107 = (uint64_t) (x106 >> Const 85); - uint128_t x108 = x100 & Const 38685626227668133590597631; - uint128_t x109 = (uint128_t) x107 + x108; - uint64_t x110 = (uint64_t) (x109 >> Const 85); - uint128_t x111 = x102 & Const 38685626227668133590597631; - uint128_t x112 = (uint128_t) x110 + x111; - uint128_t x113 = x109 & Const 38685626227668133590597631; - uint128_t x114 = x106 & Const 38685626227668133590597631; - ℤ x115 = x81 * x112; - ℤ x116 = x80 * x113; - ℤ x117 = x79 * x114; - ℤ x118 = x116 + x117; - ℤ x119 = x115 + x118; - ℤ x120 = x81 * x113; - ℤ x121 = x80 * x114; - ℤ x122 = x120 + x121; - ℤ x123 = x79 * x112; - ℤ x124 = Const 5 * x123; - ℤ x125 = x122 + x124; - ℤ x126 = x81 * x114; - ℤ x127 = x80 * x112; - ℤ x128 = x79 * x113; - ℤ x129 = x127 + x128; - ℤ x130 = Const 5 * x129; - ℤ x131 = x126 + x130; - uint128_t x132 = x131 >> Const 85; - ℤ x133 = x132 + x125; - uint128_t x134 = x133 >> Const 85; - ℤ x135 = x134 + x119; - uint128_t x136 = x131 & Const 38685626227668133590597631; - uint128_t x137 = x135 >> Const 85; - uint128_t x138 = (uint128_t) Const 5 * x137; - uint128_t x139 = x136 + x138; - uint64_t x140 = (uint64_t) (x139 >> Const 85); - uint128_t x141 = x133 & Const 38685626227668133590597631; - uint128_t x142 = (uint128_t) x140 + x141; - uint64_t x143 = (uint64_t) (x142 >> Const 85); - uint128_t x144 = x135 & Const 38685626227668133590597631; - uint128_t x145 = (uint128_t) x143 + x144; - uint128_t x146 = x142 & Const 38685626227668133590597631; - uint128_t x147 = x139 & Const 38685626227668133590597631; - uint128_t x148 = Const 77371252455336267181195262 + x79; - uint128_t x149 = x148 - x112; - uint128_t x150 = Const 77371252455336267181195262 + x80; - uint128_t x151 = x150 - x113; - uint128_t x152 = Const 77371252455336267181195254 + x81; - uint128_t x153 = x152 - x114; - ℤ x154 = x13 * x149; - ℤ x155 = x15 * x151; - ℤ x156 = x14 * x153; - ℤ x157 = x155 + x156; - ℤ x158 = x154 + x157; - ℤ x159 = x13 * x151; - ℤ x160 = x15 * x153; - ℤ x161 = x159 + x160; - ℤ x162 = x14 * x149; - ℤ x163 = Const 5 * x162; - ℤ x164 = x161 + x163; - ℤ x165 = x13 * x153; - ℤ x166 = x15 * x149; - ℤ x167 = x14 * x151; - ℤ x168 = x166 + x167; - ℤ x169 = Const 5 * x168; - ℤ x170 = x165 + x169; - uint128_t x171 = x170 >> Const 85; - ℤ x172 = x171 + x164; - uint128_t x173 = x172 >> Const 85; - ℤ x174 = x173 + x158; - uint128_t x175 = x170 & Const 38685626227668133590597631; - uint128_t x176 = x174 >> Const 85; - uint128_t x177 = (uint128_t) Const 5 * x176; - uint128_t x178 = x175 + x177; - uint64_t x179 = (uint64_t) (x178 >> Const 85); - uint128_t x180 = x172 & Const 38685626227668133590597631; - uint128_t x181 = (uint128_t) x179 + x180; - uint64_t x182 = (uint64_t) (x181 >> Const 85); - uint128_t x183 = x174 & Const 38685626227668133590597631; - uint128_t x184 = (uint128_t) x182 + x183; - uint128_t x185 = x181 & Const 38685626227668133590597631; - uint128_t x186 = x178 & Const 38685626227668133590597631; - uint128_t x187 = x79 + x184; - uint128_t x188 = x80 + x185; - uint128_t x189 = x81 + x186; - ℤ x190 = x153 * x187; - ℤ x191 = x151 * x188; - ℤ x192 = x149 * x189; - ℤ x193 = x191 + x192; - ℤ x194 = x190 + x193; - ℤ x195 = x153 * x188; - ℤ x196 = x151 * x189; - ℤ x197 = x195 + x196; - ℤ x198 = x149 * x187; - ℤ x199 = Const 5 * x198; - ℤ x200 = x197 + x199; - ℤ x201 = x153 * x189; - ℤ x202 = x151 * x187; - ℤ x203 = x149 * x188; - ℤ x204 = x202 + x203; - ℤ x205 = Const 5 * x204; - ℤ x206 = x201 + x205; - uint128_t x207 = x206 >> Const 85; - ℤ x208 = x207 + x200; - uint128_t x209 = x208 >> Const 85; - ℤ x210 = x209 + x194; - uint128_t x211 = x206 & Const 38685626227668133590597631; - uint128_t x212 = x210 >> Const 85; - uint128_t x213 = (uint128_t) Const 5 * x212; - uint128_t x214 = x211 + x213; - uint64_t x215 = (uint64_t) (x214 >> Const 85); - uint128_t x216 = x208 & Const 38685626227668133590597631; - uint128_t x217 = (uint128_t) x215 + x216; - uint64_t x218 = (uint64_t) (x217 >> Const 85); - uint128_t x219 = x210 & Const 38685626227668133590597631; - uint128_t x220 = (uint128_t) x218 + x219; - uint128_t x221 = x217 & Const 38685626227668133590597631; - uint128_t x222 = x214 & Const 38685626227668133590597631; - uint128_t x223 = x34 + x38; - uint128_t x224 = x35 + x39; - uint128_t x225 = x33 + x37; - uint128_t x226 = Const 77371252455336267181195262 + x34; - uint128_t x227 = x226 - x38; - uint128_t x228 = Const 77371252455336267181195262 + x35; - uint128_t x229 = x228 - x39; - uint128_t x230 = Const 77371252455336267181195254 + x33; - uint128_t x231 = x230 - x37; - ℤ x232 = x225 * x44; - ℤ x233 = x224 * x46; - ℤ x234 = x223 * x48; - ℤ x235 = x233 + x234; - ℤ x236 = x232 + x235; - ℤ x237 = x225 * x46; - ℤ x238 = x224 * x48; - ℤ x239 = x237 + x238; - ℤ x240 = x223 * x44; - ℤ x241 = Const 5 * x240; - ℤ x242 = x239 + x241; - ℤ x243 = x225 * x48; - ℤ x244 = x224 * x44; - ℤ x245 = x223 * x46; - ℤ x246 = x244 + x245; - ℤ x247 = Const 5 * x246; - ℤ x248 = x243 + x247; - uint128_t x249 = x248 >> Const 85; - ℤ x250 = x249 + x242; - uint128_t x251 = x250 >> Const 85; - ℤ x252 = x251 + x236; - uint128_t x253 = x248 & Const 38685626227668133590597631; - uint128_t x254 = x252 >> Const 85; - uint128_t x255 = (uint128_t) Const 5 * x254; - uint128_t x256 = x253 + x255; - uint64_t x257 = (uint64_t) (x256 >> Const 85); - uint128_t x258 = x250 & Const 38685626227668133590597631; - uint128_t x259 = (uint128_t) x257 + x258; - uint64_t x260 = (uint64_t) (x259 >> Const 85); - uint128_t x261 = x252 & Const 38685626227668133590597631; - uint128_t x262 = (uint128_t) x260 + x261; - uint128_t x263 = x259 & Const 38685626227668133590597631; - uint128_t x264 = x256 & Const 38685626227668133590597631; - ℤ x265 = x231 * x40; - ℤ x266 = x229 * x41; - ℤ x267 = x227 * x42; - ℤ x268 = x266 + x267; - ℤ x269 = x265 + x268; - ℤ x270 = x231 * x41; - ℤ x271 = x229 * x42; - ℤ x272 = x270 + x271; - ℤ x273 = x227 * x40; - ℤ x274 = Const 5 * x273; - ℤ x275 = x272 + x274; - ℤ x276 = x231 * x42; - ℤ x277 = x229 * x40; - ℤ x278 = x227 * x41; - ℤ x279 = x277 + x278; - ℤ x280 = Const 5 * x279; - ℤ x281 = x276 + x280; - uint128_t x282 = x281 >> Const 85; - ℤ x283 = x282 + x275; - uint128_t x284 = x283 >> Const 85; - ℤ x285 = x284 + x269; - uint128_t x286 = x281 & Const 38685626227668133590597631; - uint128_t x287 = x285 >> Const 85; - uint128_t x288 = (uint128_t) Const 5 * x287; - uint128_t x289 = x286 + x288; - uint64_t x290 = (uint64_t) (x289 >> Const 85); - uint128_t x291 = x283 & Const 38685626227668133590597631; - uint128_t x292 = (uint128_t) x290 + x291; - uint64_t x293 = (uint64_t) (x292 >> Const 85); - uint128_t x294 = x285 & Const 38685626227668133590597631; - uint128_t x295 = (uint128_t) x293 + x294; - uint128_t x296 = x292 & Const 38685626227668133590597631; - uint128_t x297 = x289 & Const 38685626227668133590597631; - uint128_t x298 = x295 + x262; - uint128_t x299 = x296 + x263; - uint128_t x300 = x297 + x264; - uint128_t x301 = x295 + x262; - uint128_t x302 = x296 + x263; - uint128_t x303 = x297 + x264; - ℤ x304 = x300 * x301; - ℤ x305 = x299 * x302; - ℤ x306 = x298 * x303; - ℤ x307 = x305 + x306; - ℤ x308 = x304 + x307; - ℤ x309 = x300 * x302; - ℤ x310 = x299 * x303; - ℤ x311 = x309 + x310; - ℤ x312 = x298 * x301; - ℤ x313 = Const 5 * x312; - ℤ x314 = x311 + x313; - ℤ x315 = x300 * x303; - ℤ x316 = x299 * x301; - ℤ x317 = x298 * x302; - ℤ x318 = x316 + x317; - ℤ x319 = Const 5 * x318; - ℤ x320 = x315 + x319; - uint128_t x321 = x320 >> Const 85; - ℤ x322 = x321 + x314; - uint128_t x323 = x322 >> Const 85; - ℤ x324 = x323 + x308; - uint128_t x325 = x320 & Const 38685626227668133590597631; - uint128_t x326 = x324 >> Const 85; - uint128_t x327 = (uint128_t) Const 5 * x326; - uint128_t x328 = x325 + x327; - uint64_t x329 = (uint64_t) (x328 >> Const 85); - uint128_t x330 = x322 & Const 38685626227668133590597631; - uint128_t x331 = (uint128_t) x329 + x330; - uint64_t x332 = (uint64_t) (x331 >> Const 85); - uint128_t x333 = x324 & Const 38685626227668133590597631; - uint128_t x334 = (uint128_t) x332 + x333; - uint128_t x335 = x331 & Const 38685626227668133590597631; - uint128_t x336 = x328 & Const 38685626227668133590597631; - uint128_t x337 = Const 77371252455336267181195262 + x295; - uint128_t x338 = x337 - x262; - uint128_t x339 = Const 77371252455336267181195262 + x296; - uint128_t x340 = x339 - x263; - uint128_t x341 = Const 77371252455336267181195254 + x297; - uint128_t x342 = x341 - x264; - uint128_t x343 = Const 77371252455336267181195262 + x295; - uint128_t x344 = x343 - x262; - uint128_t x345 = Const 77371252455336267181195262 + x296; - uint128_t x346 = x345 - x263; - uint128_t x347 = Const 77371252455336267181195254 + x297; - uint128_t x348 = x347 - x264; - ℤ x349 = x342 * x344; - ℤ x350 = x340 * x346; - ℤ x351 = x338 * x348; - ℤ x352 = x350 + x351; - ℤ x353 = x349 + x352; - ℤ x354 = x342 * x346; - ℤ x355 = x340 * x348; - ℤ x356 = x354 + x355; - ℤ x357 = x338 * x344; - ℤ x358 = Const 5 * x357; - ℤ x359 = x356 + x358; - ℤ x360 = x342 * x348; - ℤ x361 = x340 * x344; - ℤ x362 = x338 * x346; - ℤ x363 = x361 + x362; - ℤ x364 = Const 5 * x363; - ℤ x365 = x360 + x364; - uint128_t x366 = x365 >> Const 85; - ℤ x367 = x366 + x359; - uint128_t x368 = x367 >> Const 85; - ℤ x369 = x368 + x353; - uint128_t x370 = x365 & Const 38685626227668133590597631; - uint128_t x371 = x369 >> Const 85; - uint128_t x372 = (uint128_t) Const 5 * x371; - uint128_t x373 = x370 + x372; - uint64_t x374 = (uint64_t) (x373 >> Const 85); - uint128_t x375 = x367 & Const 38685626227668133590597631; - uint128_t x376 = (uint128_t) x374 + x375; - uint64_t x377 = (uint64_t) (x376 >> Const 85); - uint128_t x378 = x369 & Const 38685626227668133590597631; - uint128_t x379 = (uint128_t) x377 + x378; - uint128_t x380 = x376 & Const 38685626227668133590597631; - uint128_t x381 = x373 & Const 38685626227668133590597631; - ℤ x382 = x17 * x379; - ℤ x383 = x19 * x380; - ℤ x384 = x18 * x381; - ℤ x385 = x383 + x384; - ℤ x386 = x382 + x385; - ℤ x387 = x17 * x380; - ℤ x388 = x19 * x381; - ℤ x389 = x387 + x388; - ℤ x390 = x18 * x379; - ℤ x391 = Const 5 * x390; - ℤ x392 = x389 + x391; - ℤ x393 = x17 * x381; - ℤ x394 = x19 * x379; - ℤ x395 = x18 * x380; - ℤ x396 = x394 + x395; - ℤ x397 = Const 5 * x396; - ℤ x398 = x393 + x397; - uint128_t x399 = x398 >> Const 85; - ℤ x400 = x399 + x392; - uint128_t x401 = x400 >> Const 85; - ℤ x402 = x401 + x386; - uint128_t x403 = x398 & Const 38685626227668133590597631; - uint128_t x404 = x402 >> Const 85; - uint128_t x405 = (uint128_t) Const 5 * x404; - uint128_t x406 = x403 + x405; - uint64_t x407 = (uint64_t) (x406 >> Const 85); - uint128_t x408 = x400 & Const 38685626227668133590597631; - uint128_t x409 = (uint128_t) x407 + x408; - uint64_t x410 = (uint64_t) (x409 >> Const 85); - uint128_t x411 = x402 & Const 38685626227668133590597631; - uint128_t x412 = (uint128_t) x410 + x411; - uint128_t x413 = x409 & Const 38685626227668133590597631; - uint128_t x414 = x406 & Const 38685626227668133590597631; - (Return x145, Return x146, Return x147, (Return x220, Return x221, Return x222), (Return x334, Return x335, Return x336, (Return x412, Return x413, Return x414)))) - (x, x0, (x1, x2), (x3, x4)) in - y in - y))%core +(x, x0, (x1, x2), (x3, x4))%core in +(let (a0, b0) := a in +(a0, b0), let (a0, b0) := b in +(a0, b0))%core : word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 * (word128 * word128 * word128) * (word128 * word128 * word128 * (word128 * word128 * word128)) |