diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-15 16:07:17 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-15 16:07:17 -0500 |
| commit | 27b1da9e942db23e82c092c5c131ee755557b42c (patch) | |
| tree | da360f16636e455f11fecd5212fbd5c5462d8ec1 | |
| parent | 316358ce914dbcc93eac3ede6ac5916bf36101e7 (diff) | |
Add more display logs
18 files changed, 4240 insertions, 0 deletions
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddDisplay.log b/src/SpecificGen/GF2213_32Reflective/Reified/AddDisplay.log new file mode 100644 index 000000000..4e361cd8d --- /dev/null +++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddDisplay.log @@ -0,0 +1,36 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : var Syntax.TZ, +Tbase Syntax.TZ x15 = x + x7; +Tbase Syntax.TZ x16 = x0 + x8; +Tbase Syntax.TZ x17 = x1 + x9; +Tbase Syntax.TZ x18 = x2 + x10; +Tbase Syntax.TZ x19 = x3 + x11; +Tbase Syntax.TZ x20 = x4 + x12; +Tbase Syntax.TZ x21 = x5 + x13; +Tbase Syntax.TZ x22 = x6 + x14; +(Return x15, Return x16, Return x17, Return x18, Return x19, +Return x20, Return x21, Return x22) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddJavaDisplay.log b/src/SpecificGen/GF2213_32Reflective/Reified/AddJavaDisplay.log new file mode 100644 index 000000000..4e361cd8d --- /dev/null +++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddJavaDisplay.log @@ -0,0 +1,36 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : var Syntax.TZ, +Tbase Syntax.TZ x15 = x + x7; +Tbase Syntax.TZ x16 = x0 + x8; +Tbase Syntax.TZ x17 = x1 + x9; +Tbase Syntax.TZ x18 = x2 + x10; +Tbase Syntax.TZ x19 = x3 + x11; +Tbase Syntax.TZ x20 = x4 + x12; +Tbase Syntax.TZ x21 = x5 + x13; +Tbase Syntax.TZ x22 = x6 + x14; +(Return x15, Return x16, Return x17, Return x18, Return x19, +Return x20, Return x21, Return x22) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/MulDisplay.log b/src/SpecificGen/GF2213_32Reflective/Reified/MulDisplay.log new file mode 100644 index 000000000..e4af15465 --- /dev/null +++ b/src/SpecificGen/GF2213_32Reflective/Reified/MulDisplay.log @@ -0,0 +1,214 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : var Syntax.TZ, +Tbase Syntax.TZ x15 = x6 * x14; +Tbase Syntax.TZ x16 = x13 * 0x2; +Tbase Syntax.TZ x17 = x * x16; +Tbase Syntax.TZ x18 = x12 * 0x2; +Tbase Syntax.TZ x19 = x0 * x18; +Tbase Syntax.TZ x20 = x11 * 0x2; +Tbase Syntax.TZ x21 = x1 * x20; +Tbase Syntax.TZ x22 = x10 * 0x2; +Tbase Syntax.TZ x23 = x2 * x22; +Tbase Syntax.TZ x24 = x9 * 0x2; +Tbase Syntax.TZ x25 = x3 * x24; +Tbase Syntax.TZ x26 = x8 * 0x2; +Tbase Syntax.TZ x27 = x4 * x26; +Tbase Syntax.TZ x28 = x7 * 0x2; +Tbase Syntax.TZ x29 = x5 * x28; +Tbase Syntax.TZ x30 = x27 + x29; +Tbase Syntax.TZ x31 = x25 + x30; +Tbase Syntax.TZ x32 = x23 + x31; +Tbase Syntax.TZ x33 = x21 + x32; +Tbase Syntax.TZ x34 = x19 + x33; +Tbase Syntax.TZ x35 = x17 + x34; +Tbase Syntax.TZ x36 = 0x3 * x35; +Tbase Syntax.TZ x37 = x15 + x36; +Tbase Syntax.TZ x38 = x37 >> 0x1c; +Tbase Syntax.TZ x39 = x5 * x14; +Tbase Syntax.TZ x40 = x6 * x13; +Tbase Syntax.TZ x41 = x39 + x40; +Tbase Syntax.TZ x42 = x12 * 0x2; +Tbase Syntax.TZ x43 = x * x42; +Tbase Syntax.TZ x44 = x0 * x11; +Tbase Syntax.TZ x45 = x10 * 0x2; +Tbase Syntax.TZ x46 = x1 * x45; +Tbase Syntax.TZ x47 = x9 * 0x2; +Tbase Syntax.TZ x48 = x2 * x47; +Tbase Syntax.TZ x49 = x3 * x8; +Tbase Syntax.TZ x50 = x7 * 0x2; +Tbase Syntax.TZ x51 = x4 * x50; +Tbase Syntax.TZ x52 = x49 + x51; +Tbase Syntax.TZ x53 = x48 + x52; +Tbase Syntax.TZ x54 = x46 + x53; +Tbase Syntax.TZ x55 = x44 + x54; +Tbase Syntax.TZ x56 = x43 + x55; +Tbase Syntax.TZ x57 = 0x3 * x56; +Tbase Syntax.TZ x58 = x41 + x57; +Tbase Syntax.TZ x59 = x38 + x58; +Tbase Syntax.TZ x60 = x59 >> 0x1c; +Tbase Syntax.TZ x61 = x4 * x14; +Tbase Syntax.TZ x62 = x5 * x13; +Tbase Syntax.TZ x63 = x6 * x12; +Tbase Syntax.TZ x64 = x62 + x63; +Tbase Syntax.TZ x65 = x61 + x64; +Tbase Syntax.TZ x66 = x * x11; +Tbase Syntax.TZ x67 = x0 * x10; +Tbase Syntax.TZ x68 = x9 * 0x2; +Tbase Syntax.TZ x69 = x1 * x68; +Tbase Syntax.TZ x70 = x2 * x8; +Tbase Syntax.TZ x71 = x3 * x7; +Tbase Syntax.TZ x72 = x70 + x71; +Tbase Syntax.TZ x73 = x69 + x72; +Tbase Syntax.TZ x74 = x67 + x73; +Tbase Syntax.TZ x75 = x66 + x74; +Tbase Syntax.TZ x76 = 0x3 * x75; +Tbase Syntax.TZ x77 = x65 + x76; +Tbase Syntax.TZ x78 = x60 + x77; +Tbase Syntax.TZ x79 = x78 >> 0x1b; +Tbase Syntax.TZ x80 = x3 * x14; +Tbase Syntax.TZ x81 = x13 * 0x2; +Tbase Syntax.TZ x82 = x4 * x81; +Tbase Syntax.TZ x83 = x12 * 0x2; +Tbase Syntax.TZ x84 = x5 * x83; +Tbase Syntax.TZ x85 = x6 * x11; +Tbase Syntax.TZ x86 = x84 + x85; +Tbase Syntax.TZ x87 = x82 + x86; +Tbase Syntax.TZ x88 = x80 + x87; +Tbase Syntax.TZ x89 = x10 * 0x2; +Tbase Syntax.TZ x90 = x * x89; +Tbase Syntax.TZ x91 = x9 * 0x2; +Tbase Syntax.TZ x92 = x0 * x91; +Tbase Syntax.TZ x93 = x8 * 0x2; +Tbase Syntax.TZ x94 = x1 * x93; +Tbase Syntax.TZ x95 = x7 * 0x2; +Tbase Syntax.TZ x96 = x2 * x95; +Tbase Syntax.TZ x97 = x94 + x96; +Tbase Syntax.TZ x98 = x92 + x97; +Tbase Syntax.TZ x99 = x90 + x98; +Tbase Syntax.TZ x100 = 0x3 * x99; +Tbase Syntax.TZ x101 = x88 + x100; +Tbase Syntax.TZ x102 = x79 + x101; +Tbase Syntax.TZ x103 = x102 >> 0x1c; +Tbase Syntax.TZ x104 = x2 * x14; +Tbase Syntax.TZ x105 = x3 * x13; +Tbase Syntax.TZ x106 = x12 * 0x2; +Tbase Syntax.TZ x107 = x4 * x106; +Tbase Syntax.TZ x108 = x5 * x11; +Tbase Syntax.TZ x109 = x6 * x10; +Tbase Syntax.TZ x110 = x108 + x109; +Tbase Syntax.TZ x111 = x107 + x110; +Tbase Syntax.TZ x112 = x105 + x111; +Tbase Syntax.TZ x113 = x104 + x112; +Tbase Syntax.TZ x114 = x9 * 0x2; +Tbase Syntax.TZ x115 = x * x114; +Tbase Syntax.TZ x116 = x0 * x8; +Tbase Syntax.TZ x117 = x7 * 0x2; +Tbase Syntax.TZ x118 = x1 * x117; +Tbase Syntax.TZ x119 = x116 + x118; +Tbase Syntax.TZ x120 = x115 + x119; +Tbase Syntax.TZ x121 = 0x3 * x120; +Tbase Syntax.TZ x122 = x113 + x121; +Tbase Syntax.TZ x123 = x103 + x122; +Tbase Syntax.TZ x124 = x123 >> 0x1c; +Tbase Syntax.TZ x125 = x1 * x14; +Tbase Syntax.TZ x126 = x2 * x13; +Tbase Syntax.TZ x127 = x3 * x12; +Tbase Syntax.TZ x128 = x4 * x11; +Tbase Syntax.TZ x129 = x5 * x10; +Tbase Syntax.TZ x130 = x6 * x9; +Tbase Syntax.TZ x131 = x129 + x130; +Tbase Syntax.TZ x132 = x128 + x131; +Tbase Syntax.TZ x133 = x127 + x132; +Tbase Syntax.TZ x134 = x126 + x133; +Tbase Syntax.TZ x135 = x125 + x134; +Tbase Syntax.TZ x136 = x * x8; +Tbase Syntax.TZ x137 = x0 * x7; +Tbase Syntax.TZ x138 = x136 + x137; +Tbase Syntax.TZ x139 = 0x3 * x138; +Tbase Syntax.TZ x140 = x135 + x139; +Tbase Syntax.TZ x141 = x124 + x140; +Tbase Syntax.TZ x142 = x141 >> 0x1b; +Tbase Syntax.TZ x143 = x0 * x14; +Tbase Syntax.TZ x144 = x13 * 0x2; +Tbase Syntax.TZ x145 = x1 * x144; +Tbase Syntax.TZ x146 = x12 * 0x2; +Tbase Syntax.TZ x147 = x2 * x146; +Tbase Syntax.TZ x148 = x3 * x11; +Tbase Syntax.TZ x149 = x10 * 0x2; +Tbase Syntax.TZ x150 = x4 * x149; +Tbase Syntax.TZ x151 = x9 * 0x2; +Tbase Syntax.TZ x152 = x5 * x151; +Tbase Syntax.TZ x153 = x6 * x8; +Tbase Syntax.TZ x154 = x152 + x153; +Tbase Syntax.TZ x155 = x150 + x154; +Tbase Syntax.TZ x156 = x148 + x155; +Tbase Syntax.TZ x157 = x147 + x156; +Tbase Syntax.TZ x158 = x145 + x157; +Tbase Syntax.TZ x159 = x143 + x158; +Tbase Syntax.TZ x160 = x7 * 0x2; +Tbase Syntax.TZ x161 = x * x160; +Tbase Syntax.TZ x162 = 0x3 * x161; +Tbase Syntax.TZ x163 = x159 + x162; +Tbase Syntax.TZ x164 = x142 + x163; +Tbase Syntax.TZ x165 = x164 >> 0x1c; +Tbase Syntax.TZ x166 = x * x14; +Tbase Syntax.TZ x167 = x0 * x13; +Tbase Syntax.TZ x168 = x12 * 0x2; +Tbase Syntax.TZ x169 = x1 * x168; +Tbase Syntax.TZ x170 = x2 * x11; +Tbase Syntax.TZ x171 = x3 * x10; +Tbase Syntax.TZ x172 = x9 * 0x2; +Tbase Syntax.TZ x173 = x4 * x172; +Tbase Syntax.TZ x174 = x5 * x8; +Tbase Syntax.TZ x175 = x6 * x7; +Tbase Syntax.TZ x176 = x174 + x175; +Tbase Syntax.TZ x177 = x173 + x176; +Tbase Syntax.TZ x178 = x171 + x177; +Tbase Syntax.TZ x179 = x170 + x178; +Tbase Syntax.TZ x180 = x169 + x179; +Tbase Syntax.TZ x181 = x167 + x180; +Tbase Syntax.TZ x182 = x166 + x181; +Tbase Syntax.TZ x183 = x165 + x182; +Tbase Syntax.TZ x184 = x183 >> 0x1b; +Tbase Syntax.TZ x185 = 0x3 * x184; +Tbase Syntax.TZ x186 = x37 & 0xfffffff; +Tbase Syntax.TZ x187 = x185 + x186; +Tbase Syntax.TZ x188 = x187 >> 0x1c; +Tbase Syntax.TZ x189 = x59 & 0xfffffff; +Tbase Syntax.TZ x190 = x188 + x189; +Tbase Syntax.TZ x191 = x183 & 0x7ffffff; +Tbase Syntax.TZ x192 = x164 & 0xfffffff; +Tbase Syntax.TZ x193 = x141 & 0x7ffffff; +Tbase Syntax.TZ x194 = x123 & 0xfffffff; +Tbase Syntax.TZ x195 = x102 & 0xfffffff; +Tbase Syntax.TZ x196 = x190 >> 0x1c; +Tbase Syntax.TZ x197 = x78 & 0x7ffffff; +Tbase Syntax.TZ x198 = x196 + x197; +Tbase Syntax.TZ x199 = x190 & 0xfffffff; +Tbase Syntax.TZ x200 = x187 & 0xfffffff; +(Return x191, Return x192, Return x193, Return x194, +Return x195, Return x198, Return x199, Return x200) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/MulJavaDisplay.log b/src/SpecificGen/GF2213_32Reflective/Reified/MulJavaDisplay.log new file mode 100644 index 000000000..0c4efc86c --- /dev/null +++ b/src/SpecificGen/GF2213_32Reflective/Reified/MulJavaDisplay.log @@ -0,0 +1,214 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : var Syntax.TZ, +Tbase Syntax.TZ x15 = x6 * x14; +Tbase Syntax.TZ x16 = x13 * 0x2; +Tbase Syntax.TZ x17 = x * x16; +Tbase Syntax.TZ x18 = x12 * 0x2; +Tbase Syntax.TZ x19 = x0 * x18; +Tbase Syntax.TZ x20 = x11 * 0x2; +Tbase Syntax.TZ x21 = x1 * x20; +Tbase Syntax.TZ x22 = x10 * 0x2; +Tbase Syntax.TZ x23 = x2 * x22; +Tbase Syntax.TZ x24 = x9 * 0x2; +Tbase Syntax.TZ x25 = x3 * x24; +Tbase Syntax.TZ x26 = x8 * 0x2; +Tbase Syntax.TZ x27 = x4 * x26; +Tbase Syntax.TZ x28 = x7 * 0x2; +Tbase Syntax.TZ x29 = x5 * x28; +Tbase Syntax.TZ x30 = x27 + x29; +Tbase Syntax.TZ x31 = x25 + x30; +Tbase Syntax.TZ x32 = x23 + x31; +Tbase Syntax.TZ x33 = x21 + x32; +Tbase Syntax.TZ x34 = x19 + x33; +Tbase Syntax.TZ x35 = x17 + x34; +Tbase Syntax.TZ x36 = 0x3 * x35; +Tbase Syntax.TZ x37 = x15 + x36; +Tbase Syntax.TZ x38 = x37 >>> 0x1c; +Tbase Syntax.TZ x39 = x5 * x14; +Tbase Syntax.TZ x40 = x6 * x13; +Tbase Syntax.TZ x41 = x39 + x40; +Tbase Syntax.TZ x42 = x12 * 0x2; +Tbase Syntax.TZ x43 = x * x42; +Tbase Syntax.TZ x44 = x0 * x11; +Tbase Syntax.TZ x45 = x10 * 0x2; +Tbase Syntax.TZ x46 = x1 * x45; +Tbase Syntax.TZ x47 = x9 * 0x2; +Tbase Syntax.TZ x48 = x2 * x47; +Tbase Syntax.TZ x49 = x3 * x8; +Tbase Syntax.TZ x50 = x7 * 0x2; +Tbase Syntax.TZ x51 = x4 * x50; +Tbase Syntax.TZ x52 = x49 + x51; +Tbase Syntax.TZ x53 = x48 + x52; +Tbase Syntax.TZ x54 = x46 + x53; +Tbase Syntax.TZ x55 = x44 + x54; +Tbase Syntax.TZ x56 = x43 + x55; +Tbase Syntax.TZ x57 = 0x3 * x56; +Tbase Syntax.TZ x58 = x41 + x57; +Tbase Syntax.TZ x59 = x38 + x58; +Tbase Syntax.TZ x60 = x59 >>> 0x1c; +Tbase Syntax.TZ x61 = x4 * x14; +Tbase Syntax.TZ x62 = x5 * x13; +Tbase Syntax.TZ x63 = x6 * x12; +Tbase Syntax.TZ x64 = x62 + x63; +Tbase Syntax.TZ x65 = x61 + x64; +Tbase Syntax.TZ x66 = x * x11; +Tbase Syntax.TZ x67 = x0 * x10; +Tbase Syntax.TZ x68 = x9 * 0x2; +Tbase Syntax.TZ x69 = x1 * x68; +Tbase Syntax.TZ x70 = x2 * x8; +Tbase Syntax.TZ x71 = x3 * x7; +Tbase Syntax.TZ x72 = x70 + x71; +Tbase Syntax.TZ x73 = x69 + x72; +Tbase Syntax.TZ x74 = x67 + x73; +Tbase Syntax.TZ x75 = x66 + x74; +Tbase Syntax.TZ x76 = 0x3 * x75; +Tbase Syntax.TZ x77 = x65 + x76; +Tbase Syntax.TZ x78 = x60 + x77; +Tbase Syntax.TZ x79 = x78 >>> 0x1b; +Tbase Syntax.TZ x80 = x3 * x14; +Tbase Syntax.TZ x81 = x13 * 0x2; +Tbase Syntax.TZ x82 = x4 * x81; +Tbase Syntax.TZ x83 = x12 * 0x2; +Tbase Syntax.TZ x84 = x5 * x83; +Tbase Syntax.TZ x85 = x6 * x11; +Tbase Syntax.TZ x86 = x84 + x85; +Tbase Syntax.TZ x87 = x82 + x86; +Tbase Syntax.TZ x88 = x80 + x87; +Tbase Syntax.TZ x89 = x10 * 0x2; +Tbase Syntax.TZ x90 = x * x89; +Tbase Syntax.TZ x91 = x9 * 0x2; +Tbase Syntax.TZ x92 = x0 * x91; +Tbase Syntax.TZ x93 = x8 * 0x2; +Tbase Syntax.TZ x94 = x1 * x93; +Tbase Syntax.TZ x95 = x7 * 0x2; +Tbase Syntax.TZ x96 = x2 * x95; +Tbase Syntax.TZ x97 = x94 + x96; +Tbase Syntax.TZ x98 = x92 + x97; +Tbase Syntax.TZ x99 = x90 + x98; +Tbase Syntax.TZ x100 = 0x3 * x99; +Tbase Syntax.TZ x101 = x88 + x100; +Tbase Syntax.TZ x102 = x79 + x101; +Tbase Syntax.TZ x103 = x102 >>> 0x1c; +Tbase Syntax.TZ x104 = x2 * x14; +Tbase Syntax.TZ x105 = x3 * x13; +Tbase Syntax.TZ x106 = x12 * 0x2; +Tbase Syntax.TZ x107 = x4 * x106; +Tbase Syntax.TZ x108 = x5 * x11; +Tbase Syntax.TZ x109 = x6 * x10; +Tbase Syntax.TZ x110 = x108 + x109; +Tbase Syntax.TZ x111 = x107 + x110; +Tbase Syntax.TZ x112 = x105 + x111; +Tbase Syntax.TZ x113 = x104 + x112; +Tbase Syntax.TZ x114 = x9 * 0x2; +Tbase Syntax.TZ x115 = x * x114; +Tbase Syntax.TZ x116 = x0 * x8; +Tbase Syntax.TZ x117 = x7 * 0x2; +Tbase Syntax.TZ x118 = x1 * x117; +Tbase Syntax.TZ x119 = x116 + x118; +Tbase Syntax.TZ x120 = x115 + x119; +Tbase Syntax.TZ x121 = 0x3 * x120; +Tbase Syntax.TZ x122 = x113 + x121; +Tbase Syntax.TZ x123 = x103 + x122; +Tbase Syntax.TZ x124 = x123 >>> 0x1c; +Tbase Syntax.TZ x125 = x1 * x14; +Tbase Syntax.TZ x126 = x2 * x13; +Tbase Syntax.TZ x127 = x3 * x12; +Tbase Syntax.TZ x128 = x4 * x11; +Tbase Syntax.TZ x129 = x5 * x10; +Tbase Syntax.TZ x130 = x6 * x9; +Tbase Syntax.TZ x131 = x129 + x130; +Tbase Syntax.TZ x132 = x128 + x131; +Tbase Syntax.TZ x133 = x127 + x132; +Tbase Syntax.TZ x134 = x126 + x133; +Tbase Syntax.TZ x135 = x125 + x134; +Tbase Syntax.TZ x136 = x * x8; +Tbase Syntax.TZ x137 = x0 * x7; +Tbase Syntax.TZ x138 = x136 + x137; +Tbase Syntax.TZ x139 = 0x3 * x138; +Tbase Syntax.TZ x140 = x135 + x139; +Tbase Syntax.TZ x141 = x124 + x140; +Tbase Syntax.TZ x142 = x141 >>> 0x1b; +Tbase Syntax.TZ x143 = x0 * x14; +Tbase Syntax.TZ x144 = x13 * 0x2; +Tbase Syntax.TZ x145 = x1 * x144; +Tbase Syntax.TZ x146 = x12 * 0x2; +Tbase Syntax.TZ x147 = x2 * x146; +Tbase Syntax.TZ x148 = x3 * x11; +Tbase Syntax.TZ x149 = x10 * 0x2; +Tbase Syntax.TZ x150 = x4 * x149; +Tbase Syntax.TZ x151 = x9 * 0x2; +Tbase Syntax.TZ x152 = x5 * x151; +Tbase Syntax.TZ x153 = x6 * x8; +Tbase Syntax.TZ x154 = x152 + x153; +Tbase Syntax.TZ x155 = x150 + x154; +Tbase Syntax.TZ x156 = x148 + x155; +Tbase Syntax.TZ x157 = x147 + x156; +Tbase Syntax.TZ x158 = x145 + x157; +Tbase Syntax.TZ x159 = x143 + x158; +Tbase Syntax.TZ x160 = x7 * 0x2; +Tbase Syntax.TZ x161 = x * x160; +Tbase Syntax.TZ x162 = 0x3 * x161; +Tbase Syntax.TZ x163 = x159 + x162; +Tbase Syntax.TZ x164 = x142 + x163; +Tbase Syntax.TZ x165 = x164 >>> 0x1c; +Tbase Syntax.TZ x166 = x * x14; +Tbase Syntax.TZ x167 = x0 * x13; +Tbase Syntax.TZ x168 = x12 * 0x2; +Tbase Syntax.TZ x169 = x1 * x168; +Tbase Syntax.TZ x170 = x2 * x11; +Tbase Syntax.TZ x171 = x3 * x10; +Tbase Syntax.TZ x172 = x9 * 0x2; +Tbase Syntax.TZ x173 = x4 * x172; +Tbase Syntax.TZ x174 = x5 * x8; +Tbase Syntax.TZ x175 = x6 * x7; +Tbase Syntax.TZ x176 = x174 + x175; +Tbase Syntax.TZ x177 = x173 + x176; +Tbase Syntax.TZ x178 = x171 + x177; +Tbase Syntax.TZ x179 = x170 + x178; +Tbase Syntax.TZ x180 = x169 + x179; +Tbase Syntax.TZ x181 = x167 + x180; +Tbase Syntax.TZ x182 = x166 + x181; +Tbase Syntax.TZ x183 = x165 + x182; +Tbase Syntax.TZ x184 = x183 >>> 0x1b; +Tbase Syntax.TZ x185 = 0x3 * x184; +Tbase Syntax.TZ x186 = x37 & 0xfffffff; +Tbase Syntax.TZ x187 = x185 + x186; +Tbase Syntax.TZ x188 = x187 >>> 0x1c; +Tbase Syntax.TZ x189 = x59 & 0xfffffff; +Tbase Syntax.TZ x190 = x188 + x189; +Tbase Syntax.TZ x191 = x183 & 0x7ffffff; +Tbase Syntax.TZ x192 = x164 & 0xfffffff; +Tbase Syntax.TZ x193 = x141 & 0x7ffffff; +Tbase Syntax.TZ x194 = x123 & 0xfffffff; +Tbase Syntax.TZ x195 = x102 & 0xfffffff; +Tbase Syntax.TZ x196 = x190 >>> 0x1c; +Tbase Syntax.TZ x197 = x78 & 0x7ffffff; +Tbase Syntax.TZ x198 = x196 + x197; +Tbase Syntax.TZ x199 = x190 & 0xfffffff; +Tbase Syntax.TZ x200 = x187 & 0xfffffff; +(Return x191, Return x192, Return x193, Return x194, +Return x195, Return x198, Return x199, Return x200) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddDisplay.log b/src/SpecificGen/GF2519_32Reflective/Reified/AddDisplay.log new file mode 100644 index 000000000..156f0286e --- /dev/null +++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddDisplay.log @@ -0,0 +1,45 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x + x9; +Tbase Syntax.TZ x20 = x0 + x10; +Tbase Syntax.TZ x21 = x1 + x11; +Tbase Syntax.TZ x22 = x2 + x12; +Tbase Syntax.TZ x23 = x3 + x13; +Tbase Syntax.TZ x24 = x4 + x14; +Tbase Syntax.TZ x25 = x5 + x15; +Tbase Syntax.TZ x26 = x6 + x16; +Tbase Syntax.TZ x27 = x7 + x17; +Tbase Syntax.TZ x28 = x8 + x18; +(Return x19, Return x20, Return x21, Return x22, Return x23, +Return x24, Return x25, Return x26, Return x27, Return x28) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddJavaDisplay.log b/src/SpecificGen/GF2519_32Reflective/Reified/AddJavaDisplay.log new file mode 100644 index 000000000..156f0286e --- /dev/null +++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddJavaDisplay.log @@ -0,0 +1,45 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x + x9; +Tbase Syntax.TZ x20 = x0 + x10; +Tbase Syntax.TZ x21 = x1 + x11; +Tbase Syntax.TZ x22 = x2 + x12; +Tbase Syntax.TZ x23 = x3 + x13; +Tbase Syntax.TZ x24 = x4 + x14; +Tbase Syntax.TZ x25 = x5 + x15; +Tbase Syntax.TZ x26 = x6 + x16; +Tbase Syntax.TZ x27 = x7 + x17; +Tbase Syntax.TZ x28 = x8 + x18; +(Return x19, Return x20, Return x21, Return x22, Return x23, +Return x24, Return x25, Return x26, Return x27, Return x28) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/MulDisplay.log b/src/SpecificGen/GF2519_32Reflective/Reified/MulDisplay.log new file mode 100644 index 000000000..37db43d02 --- /dev/null +++ b/src/SpecificGen/GF2519_32Reflective/Reified/MulDisplay.log @@ -0,0 +1,317 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x8 * x18; +Tbase Syntax.TZ x20 = x17 * 0x2; +Tbase Syntax.TZ x21 = x * x20; +Tbase Syntax.TZ x22 = x16 * 0x2; +Tbase Syntax.TZ x23 = x0 * x22; +Tbase Syntax.TZ x24 = x15 * 0x2; +Tbase Syntax.TZ x25 = x1 * x24; +Tbase Syntax.TZ x26 = x14 * 0x2; +Tbase Syntax.TZ x27 = x2 * x26; +Tbase Syntax.TZ x28 = x13 * 0x2; +Tbase Syntax.TZ x29 = x3 * x28; +Tbase Syntax.TZ x30 = x12 * 0x2; +Tbase Syntax.TZ x31 = x4 * x30; +Tbase Syntax.TZ x32 = x11 * 0x2; +Tbase Syntax.TZ x33 = x5 * x32; +Tbase Syntax.TZ x34 = x10 * 0x2; +Tbase Syntax.TZ x35 = x6 * x34; +Tbase Syntax.TZ x36 = x9 * 0x2; +Tbase Syntax.TZ x37 = x7 * x36; +Tbase Syntax.TZ x38 = x35 + x37; +Tbase Syntax.TZ x39 = x33 + x38; +Tbase Syntax.TZ x40 = x31 + x39; +Tbase Syntax.TZ x41 = x29 + x40; +Tbase Syntax.TZ x42 = x27 + x41; +Tbase Syntax.TZ x43 = x25 + x42; +Tbase Syntax.TZ x44 = x23 + x43; +Tbase Syntax.TZ x45 = x21 + x44; +Tbase Syntax.TZ x46 = 0x9 * x45; +Tbase Syntax.TZ x47 = x19 + x46; +Tbase Syntax.TZ x48 = x47 >> 0x1a; +Tbase Syntax.TZ x49 = x7 * x18; +Tbase Syntax.TZ x50 = x8 * x17; +Tbase Syntax.TZ x51 = x49 + x50; +Tbase Syntax.TZ x52 = x * x16; +Tbase Syntax.TZ x53 = x0 * x15; +Tbase Syntax.TZ x54 = x1 * x14; +Tbase Syntax.TZ x55 = x2 * x13; +Tbase Syntax.TZ x56 = x3 * x12; +Tbase Syntax.TZ x57 = x4 * x11; +Tbase Syntax.TZ x58 = x5 * x10; +Tbase Syntax.TZ x59 = x6 * x9; +Tbase Syntax.TZ x60 = x58 + x59; +Tbase Syntax.TZ x61 = x57 + x60; +Tbase Syntax.TZ x62 = x56 + x61; +Tbase Syntax.TZ x63 = x55 + x62; +Tbase Syntax.TZ x64 = x54 + x63; +Tbase Syntax.TZ x65 = x53 + x64; +Tbase Syntax.TZ x66 = x52 + x65; +Tbase Syntax.TZ x67 = 0x9 * x66; +Tbase Syntax.TZ x68 = x51 + x67; +Tbase Syntax.TZ x69 = x48 + x68; +Tbase Syntax.TZ x70 = x69 >> 0x19; +Tbase Syntax.TZ x71 = x6 * x18; +Tbase Syntax.TZ x72 = x17 * 0x2; +Tbase Syntax.TZ x73 = x7 * x72; +Tbase Syntax.TZ x74 = x8 * x16; +Tbase Syntax.TZ x75 = x73 + x74; +Tbase Syntax.TZ x76 = x71 + x75; +Tbase Syntax.TZ x77 = x * x15; +Tbase Syntax.TZ x78 = x0 * x14; +Tbase Syntax.TZ x79 = x1 * x13; +Tbase Syntax.TZ x80 = x2 * x12; +Tbase Syntax.TZ x81 = x3 * x11; +Tbase Syntax.TZ x82 = x4 * x10; +Tbase Syntax.TZ x83 = x5 * x9; +Tbase Syntax.TZ x84 = x82 + x83; +Tbase Syntax.TZ x85 = x81 + x84; +Tbase Syntax.TZ x86 = x80 + x85; +Tbase Syntax.TZ x87 = x79 + x86; +Tbase Syntax.TZ x88 = x78 + x87; +Tbase Syntax.TZ x89 = x77 + x88; +Tbase Syntax.TZ x90 = 0x9 * x89; +Tbase Syntax.TZ x91 = x76 + x90; +Tbase Syntax.TZ x92 = x70 + x91; +Tbase Syntax.TZ x93 = x92 >> 0x19; +Tbase Syntax.TZ x94 = x5 * x18; +Tbase Syntax.TZ x95 = x17 * 0x2; +Tbase Syntax.TZ x96 = x6 * x95; +Tbase Syntax.TZ x97 = x16 * 0x2; +Tbase Syntax.TZ x98 = x7 * x97; +Tbase Syntax.TZ x99 = x8 * x15; +Tbase Syntax.TZ x100 = x98 + x99; +Tbase Syntax.TZ x101 = x96 + x100; +Tbase Syntax.TZ x102 = x94 + x101; +Tbase Syntax.TZ x103 = x * x14; +Tbase Syntax.TZ x104 = x0 * x13; +Tbase Syntax.TZ x105 = x1 * x12; +Tbase Syntax.TZ x106 = x2 * x11; +Tbase Syntax.TZ x107 = x3 * x10; +Tbase Syntax.TZ x108 = x4 * x9; +Tbase Syntax.TZ x109 = x107 + x108; +Tbase Syntax.TZ x110 = x106 + x109; +Tbase Syntax.TZ x111 = x105 + x110; +Tbase Syntax.TZ x112 = x104 + x111; +Tbase Syntax.TZ x113 = x103 + x112; +Tbase Syntax.TZ x114 = 0x9 * x113; +Tbase Syntax.TZ x115 = x102 + x114; +Tbase Syntax.TZ x116 = x93 + x115; +Tbase Syntax.TZ x117 = x116 >> 0x19; +Tbase Syntax.TZ x118 = x4 * x18; +Tbase Syntax.TZ x119 = x17 * 0x2; +Tbase Syntax.TZ x120 = x5 * x119; +Tbase Syntax.TZ x121 = x16 * 0x2; +Tbase Syntax.TZ x122 = x6 * x121; +Tbase Syntax.TZ x123 = x15 * 0x2; +Tbase Syntax.TZ x124 = x7 * x123; +Tbase Syntax.TZ x125 = x8 * x14; +Tbase Syntax.TZ x126 = x124 + x125; +Tbase Syntax.TZ x127 = x122 + x126; +Tbase Syntax.TZ x128 = x120 + x127; +Tbase Syntax.TZ x129 = x118 + x128; +Tbase Syntax.TZ x130 = x * x13; +Tbase Syntax.TZ x131 = x0 * x12; +Tbase Syntax.TZ x132 = x1 * x11; +Tbase Syntax.TZ x133 = x2 * x10; +Tbase Syntax.TZ x134 = x3 * x9; +Tbase Syntax.TZ x135 = x133 + x134; +Tbase Syntax.TZ x136 = x132 + x135; +Tbase Syntax.TZ x137 = x131 + x136; +Tbase Syntax.TZ x138 = x130 + x137; +Tbase Syntax.TZ x139 = 0x9 * x138; +Tbase Syntax.TZ x140 = x129 + x139; +Tbase Syntax.TZ x141 = x117 + x140; +Tbase Syntax.TZ x142 = x141 >> 0x19; +Tbase Syntax.TZ x143 = x3 * x18; +Tbase Syntax.TZ x144 = x17 * 0x2; +Tbase Syntax.TZ x145 = x4 * x144; +Tbase Syntax.TZ x146 = x16 * 0x2; +Tbase Syntax.TZ x147 = x5 * x146; +Tbase Syntax.TZ x148 = x15 * 0x2; +Tbase Syntax.TZ x149 = x6 * x148; +Tbase Syntax.TZ x150 = x14 * 0x2; +Tbase Syntax.TZ x151 = x7 * x150; +Tbase Syntax.TZ x152 = x8 * x13; +Tbase Syntax.TZ x153 = x151 + x152; +Tbase Syntax.TZ x154 = x149 + x153; +Tbase Syntax.TZ x155 = x147 + x154; +Tbase Syntax.TZ x156 = x145 + x155; +Tbase Syntax.TZ x157 = x143 + x156; +Tbase Syntax.TZ x158 = x * x12; +Tbase Syntax.TZ x159 = x0 * x11; +Tbase Syntax.TZ x160 = x1 * x10; +Tbase Syntax.TZ x161 = x2 * x9; +Tbase Syntax.TZ x162 = x160 + x161; +Tbase Syntax.TZ x163 = x159 + x162; +Tbase Syntax.TZ x164 = x158 + x163; +Tbase Syntax.TZ x165 = 0x9 * x164; +Tbase Syntax.TZ x166 = x157 + x165; +Tbase Syntax.TZ x167 = x142 + x166; +Tbase Syntax.TZ x168 = x167 >> 0x19; +Tbase Syntax.TZ x169 = x2 * x18; +Tbase Syntax.TZ x170 = x17 * 0x2; +Tbase Syntax.TZ x171 = x3 * x170; +Tbase Syntax.TZ x172 = x16 * 0x2; +Tbase Syntax.TZ x173 = x4 * x172; +Tbase Syntax.TZ x174 = x15 * 0x2; +Tbase Syntax.TZ x175 = x5 * x174; +Tbase Syntax.TZ x176 = x14 * 0x2; +Tbase Syntax.TZ x177 = x6 * x176; +Tbase Syntax.TZ x178 = x13 * 0x2; +Tbase Syntax.TZ x179 = x7 * x178; +Tbase Syntax.TZ x180 = x8 * x12; +Tbase Syntax.TZ x181 = x179 + x180; +Tbase Syntax.TZ x182 = x177 + x181; +Tbase Syntax.TZ x183 = x175 + x182; +Tbase Syntax.TZ x184 = x173 + x183; +Tbase Syntax.TZ x185 = x171 + x184; +Tbase Syntax.TZ x186 = x169 + x185; +Tbase Syntax.TZ x187 = x * x11; +Tbase Syntax.TZ x188 = x0 * x10; +Tbase Syntax.TZ x189 = x1 * x9; +Tbase Syntax.TZ x190 = x188 + x189; +Tbase Syntax.TZ x191 = x187 + x190; +Tbase Syntax.TZ x192 = 0x9 * x191; +Tbase Syntax.TZ x193 = x186 + x192; +Tbase Syntax.TZ x194 = x168 + x193; +Tbase Syntax.TZ x195 = x194 >> 0x19; +Tbase Syntax.TZ x196 = x1 * x18; +Tbase Syntax.TZ x197 = x17 * 0x2; +Tbase Syntax.TZ x198 = x2 * x197; +Tbase Syntax.TZ x199 = x16 * 0x2; +Tbase Syntax.TZ x200 = x3 * x199; +Tbase Syntax.TZ x201 = x15 * 0x2; +Tbase Syntax.TZ x202 = x4 * x201; +Tbase Syntax.TZ x203 = x14 * 0x2; +Tbase Syntax.TZ x204 = x5 * x203; +Tbase Syntax.TZ x205 = x13 * 0x2; +Tbase Syntax.TZ x206 = x6 * x205; +Tbase Syntax.TZ x207 = x12 * 0x2; +Tbase Syntax.TZ x208 = x7 * x207; +Tbase Syntax.TZ x209 = x8 * x11; +Tbase Syntax.TZ x210 = x208 + x209; +Tbase Syntax.TZ x211 = x206 + x210; +Tbase Syntax.TZ x212 = x204 + x211; +Tbase Syntax.TZ x213 = x202 + x212; +Tbase Syntax.TZ x214 = x200 + x213; +Tbase Syntax.TZ x215 = x198 + x214; +Tbase Syntax.TZ x216 = x196 + x215; +Tbase Syntax.TZ x217 = x * x10; +Tbase Syntax.TZ x218 = x0 * x9; +Tbase Syntax.TZ x219 = x217 + x218; +Tbase Syntax.TZ x220 = 0x9 * x219; +Tbase Syntax.TZ x221 = x216 + x220; +Tbase Syntax.TZ x222 = x195 + x221; +Tbase Syntax.TZ x223 = x222 >> 0x19; +Tbase Syntax.TZ x224 = x0 * x18; +Tbase Syntax.TZ x225 = x17 * 0x2; +Tbase Syntax.TZ x226 = x1 * x225; +Tbase Syntax.TZ x227 = x16 * 0x2; +Tbase Syntax.TZ x228 = x2 * x227; +Tbase Syntax.TZ x229 = x15 * 0x2; +Tbase Syntax.TZ x230 = x3 * x229; +Tbase Syntax.TZ x231 = x14 * 0x2; +Tbase Syntax.TZ x232 = x4 * x231; +Tbase Syntax.TZ x233 = x13 * 0x2; +Tbase Syntax.TZ x234 = x5 * x233; +Tbase Syntax.TZ x235 = x12 * 0x2; +Tbase Syntax.TZ x236 = x6 * x235; +Tbase Syntax.TZ x237 = x11 * 0x2; +Tbase Syntax.TZ x238 = x7 * x237; +Tbase Syntax.TZ x239 = x8 * x10; +Tbase Syntax.TZ x240 = x238 + x239; +Tbase Syntax.TZ x241 = x236 + x240; +Tbase Syntax.TZ x242 = x234 + x241; +Tbase Syntax.TZ x243 = x232 + x242; +Tbase Syntax.TZ x244 = x230 + x243; +Tbase Syntax.TZ x245 = x228 + x244; +Tbase Syntax.TZ x246 = x226 + x245; +Tbase Syntax.TZ x247 = x224 + x246; +Tbase Syntax.TZ x248 = x * x9; +Tbase Syntax.TZ x249 = 0x9 * x248; +Tbase Syntax.TZ x250 = x247 + x249; +Tbase Syntax.TZ x251 = x223 + x250; +Tbase Syntax.TZ x252 = x251 >> 0x19; +Tbase Syntax.TZ x253 = x * x18; +Tbase Syntax.TZ x254 = x17 * 0x2; +Tbase Syntax.TZ x255 = x0 * x254; +Tbase Syntax.TZ x256 = x16 * 0x2; +Tbase Syntax.TZ x257 = x1 * x256; +Tbase Syntax.TZ x258 = x15 * 0x2; +Tbase Syntax.TZ x259 = x2 * x258; +Tbase Syntax.TZ x260 = x14 * 0x2; +Tbase Syntax.TZ x261 = x3 * x260; +Tbase Syntax.TZ x262 = x13 * 0x2; +Tbase Syntax.TZ x263 = x4 * x262; +Tbase Syntax.TZ x264 = x12 * 0x2; +Tbase Syntax.TZ x265 = x5 * x264; +Tbase Syntax.TZ x266 = x11 * 0x2; +Tbase Syntax.TZ x267 = x6 * x266; +Tbase Syntax.TZ x268 = x10 * 0x2; +Tbase Syntax.TZ x269 = x7 * x268; +Tbase Syntax.TZ x270 = x8 * x9; +Tbase Syntax.TZ x271 = x269 + x270; +Tbase Syntax.TZ x272 = x267 + x271; +Tbase Syntax.TZ x273 = x265 + x272; +Tbase Syntax.TZ x274 = x263 + x273; +Tbase Syntax.TZ x275 = x261 + x274; +Tbase Syntax.TZ x276 = x259 + x275; +Tbase Syntax.TZ x277 = x257 + x276; +Tbase Syntax.TZ x278 = x255 + x277; +Tbase Syntax.TZ x279 = x253 + x278; +Tbase Syntax.TZ x280 = x252 + x279; +Tbase Syntax.TZ x281 = x280 >> 0x19; +Tbase Syntax.TZ x282 = 0x9 * x281; +Tbase Syntax.TZ x283 = x47 & 0x3ffffff; +Tbase Syntax.TZ x284 = x282 + x283; +Tbase Syntax.TZ x285 = x284 >> 0x1a; +Tbase Syntax.TZ x286 = x69 & 0x1ffffff; +Tbase Syntax.TZ x287 = x285 + x286; +Tbase Syntax.TZ x288 = x280 & 0x1ffffff; +Tbase Syntax.TZ x289 = x251 & 0x1ffffff; +Tbase Syntax.TZ x290 = x222 & 0x1ffffff; +Tbase Syntax.TZ x291 = x194 & 0x1ffffff; +Tbase Syntax.TZ x292 = x167 & 0x1ffffff; +Tbase Syntax.TZ x293 = x141 & 0x1ffffff; +Tbase Syntax.TZ x294 = x116 & 0x1ffffff; +Tbase Syntax.TZ x295 = x287 >> 0x19; +Tbase Syntax.TZ x296 = x92 & 0x1ffffff; +Tbase Syntax.TZ x297 = x295 + x296; +Tbase Syntax.TZ x298 = x287 & 0x1ffffff; +Tbase Syntax.TZ x299 = x284 & 0x3ffffff; +(Return x288, Return x289, Return x290, Return x291, +Return x292, Return x293, Return x294, Return x297, +Return x298, Return x299) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/MulJavaDisplay.log b/src/SpecificGen/GF2519_32Reflective/Reified/MulJavaDisplay.log new file mode 100644 index 000000000..edcc8bbd0 --- /dev/null +++ b/src/SpecificGen/GF2519_32Reflective/Reified/MulJavaDisplay.log @@ -0,0 +1,317 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x8 * x18; +Tbase Syntax.TZ x20 = x17 * 0x2; +Tbase Syntax.TZ x21 = x * x20; +Tbase Syntax.TZ x22 = x16 * 0x2; +Tbase Syntax.TZ x23 = x0 * x22; +Tbase Syntax.TZ x24 = x15 * 0x2; +Tbase Syntax.TZ x25 = x1 * x24; +Tbase Syntax.TZ x26 = x14 * 0x2; +Tbase Syntax.TZ x27 = x2 * x26; +Tbase Syntax.TZ x28 = x13 * 0x2; +Tbase Syntax.TZ x29 = x3 * x28; +Tbase Syntax.TZ x30 = x12 * 0x2; +Tbase Syntax.TZ x31 = x4 * x30; +Tbase Syntax.TZ x32 = x11 * 0x2; +Tbase Syntax.TZ x33 = x5 * x32; +Tbase Syntax.TZ x34 = x10 * 0x2; +Tbase Syntax.TZ x35 = x6 * x34; +Tbase Syntax.TZ x36 = x9 * 0x2; +Tbase Syntax.TZ x37 = x7 * x36; +Tbase Syntax.TZ x38 = x35 + x37; +Tbase Syntax.TZ x39 = x33 + x38; +Tbase Syntax.TZ x40 = x31 + x39; +Tbase Syntax.TZ x41 = x29 + x40; +Tbase Syntax.TZ x42 = x27 + x41; +Tbase Syntax.TZ x43 = x25 + x42; +Tbase Syntax.TZ x44 = x23 + x43; +Tbase Syntax.TZ x45 = x21 + x44; +Tbase Syntax.TZ x46 = 0x9 * x45; +Tbase Syntax.TZ x47 = x19 + x46; +Tbase Syntax.TZ x48 = x47 >>> 0x1a; +Tbase Syntax.TZ x49 = x7 * x18; +Tbase Syntax.TZ x50 = x8 * x17; +Tbase Syntax.TZ x51 = x49 + x50; +Tbase Syntax.TZ x52 = x * x16; +Tbase Syntax.TZ x53 = x0 * x15; +Tbase Syntax.TZ x54 = x1 * x14; +Tbase Syntax.TZ x55 = x2 * x13; +Tbase Syntax.TZ x56 = x3 * x12; +Tbase Syntax.TZ x57 = x4 * x11; +Tbase Syntax.TZ x58 = x5 * x10; +Tbase Syntax.TZ x59 = x6 * x9; +Tbase Syntax.TZ x60 = x58 + x59; +Tbase Syntax.TZ x61 = x57 + x60; +Tbase Syntax.TZ x62 = x56 + x61; +Tbase Syntax.TZ x63 = x55 + x62; +Tbase Syntax.TZ x64 = x54 + x63; +Tbase Syntax.TZ x65 = x53 + x64; +Tbase Syntax.TZ x66 = x52 + x65; +Tbase Syntax.TZ x67 = 0x9 * x66; +Tbase Syntax.TZ x68 = x51 + x67; +Tbase Syntax.TZ x69 = x48 + x68; +Tbase Syntax.TZ x70 = x69 >>> 0x19; +Tbase Syntax.TZ x71 = x6 * x18; +Tbase Syntax.TZ x72 = x17 * 0x2; +Tbase Syntax.TZ x73 = x7 * x72; +Tbase Syntax.TZ x74 = x8 * x16; +Tbase Syntax.TZ x75 = x73 + x74; +Tbase Syntax.TZ x76 = x71 + x75; +Tbase Syntax.TZ x77 = x * x15; +Tbase Syntax.TZ x78 = x0 * x14; +Tbase Syntax.TZ x79 = x1 * x13; +Tbase Syntax.TZ x80 = x2 * x12; +Tbase Syntax.TZ x81 = x3 * x11; +Tbase Syntax.TZ x82 = x4 * x10; +Tbase Syntax.TZ x83 = x5 * x9; +Tbase Syntax.TZ x84 = x82 + x83; +Tbase Syntax.TZ x85 = x81 + x84; +Tbase Syntax.TZ x86 = x80 + x85; +Tbase Syntax.TZ x87 = x79 + x86; +Tbase Syntax.TZ x88 = x78 + x87; +Tbase Syntax.TZ x89 = x77 + x88; +Tbase Syntax.TZ x90 = 0x9 * x89; +Tbase Syntax.TZ x91 = x76 + x90; +Tbase Syntax.TZ x92 = x70 + x91; +Tbase Syntax.TZ x93 = x92 >>> 0x19; +Tbase Syntax.TZ x94 = x5 * x18; +Tbase Syntax.TZ x95 = x17 * 0x2; +Tbase Syntax.TZ x96 = x6 * x95; +Tbase Syntax.TZ x97 = x16 * 0x2; +Tbase Syntax.TZ x98 = x7 * x97; +Tbase Syntax.TZ x99 = x8 * x15; +Tbase Syntax.TZ x100 = x98 + x99; +Tbase Syntax.TZ x101 = x96 + x100; +Tbase Syntax.TZ x102 = x94 + x101; +Tbase Syntax.TZ x103 = x * x14; +Tbase Syntax.TZ x104 = x0 * x13; +Tbase Syntax.TZ x105 = x1 * x12; +Tbase Syntax.TZ x106 = x2 * x11; +Tbase Syntax.TZ x107 = x3 * x10; +Tbase Syntax.TZ x108 = x4 * x9; +Tbase Syntax.TZ x109 = x107 + x108; +Tbase Syntax.TZ x110 = x106 + x109; +Tbase Syntax.TZ x111 = x105 + x110; +Tbase Syntax.TZ x112 = x104 + x111; +Tbase Syntax.TZ x113 = x103 + x112; +Tbase Syntax.TZ x114 = 0x9 * x113; +Tbase Syntax.TZ x115 = x102 + x114; +Tbase Syntax.TZ x116 = x93 + x115; +Tbase Syntax.TZ x117 = x116 >>> 0x19; +Tbase Syntax.TZ x118 = x4 * x18; +Tbase Syntax.TZ x119 = x17 * 0x2; +Tbase Syntax.TZ x120 = x5 * x119; +Tbase Syntax.TZ x121 = x16 * 0x2; +Tbase Syntax.TZ x122 = x6 * x121; +Tbase Syntax.TZ x123 = x15 * 0x2; +Tbase Syntax.TZ x124 = x7 * x123; +Tbase Syntax.TZ x125 = x8 * x14; +Tbase Syntax.TZ x126 = x124 + x125; +Tbase Syntax.TZ x127 = x122 + x126; +Tbase Syntax.TZ x128 = x120 + x127; +Tbase Syntax.TZ x129 = x118 + x128; +Tbase Syntax.TZ x130 = x * x13; +Tbase Syntax.TZ x131 = x0 * x12; +Tbase Syntax.TZ x132 = x1 * x11; +Tbase Syntax.TZ x133 = x2 * x10; +Tbase Syntax.TZ x134 = x3 * x9; +Tbase Syntax.TZ x135 = x133 + x134; +Tbase Syntax.TZ x136 = x132 + x135; +Tbase Syntax.TZ x137 = x131 + x136; +Tbase Syntax.TZ x138 = x130 + x137; +Tbase Syntax.TZ x139 = 0x9 * x138; +Tbase Syntax.TZ x140 = x129 + x139; +Tbase Syntax.TZ x141 = x117 + x140; +Tbase Syntax.TZ x142 = x141 >>> 0x19; +Tbase Syntax.TZ x143 = x3 * x18; +Tbase Syntax.TZ x144 = x17 * 0x2; +Tbase Syntax.TZ x145 = x4 * x144; +Tbase Syntax.TZ x146 = x16 * 0x2; +Tbase Syntax.TZ x147 = x5 * x146; +Tbase Syntax.TZ x148 = x15 * 0x2; +Tbase Syntax.TZ x149 = x6 * x148; +Tbase Syntax.TZ x150 = x14 * 0x2; +Tbase Syntax.TZ x151 = x7 * x150; +Tbase Syntax.TZ x152 = x8 * x13; +Tbase Syntax.TZ x153 = x151 + x152; +Tbase Syntax.TZ x154 = x149 + x153; +Tbase Syntax.TZ x155 = x147 + x154; +Tbase Syntax.TZ x156 = x145 + x155; +Tbase Syntax.TZ x157 = x143 + x156; +Tbase Syntax.TZ x158 = x * x12; +Tbase Syntax.TZ x159 = x0 * x11; +Tbase Syntax.TZ x160 = x1 * x10; +Tbase Syntax.TZ x161 = x2 * x9; +Tbase Syntax.TZ x162 = x160 + x161; +Tbase Syntax.TZ x163 = x159 + x162; +Tbase Syntax.TZ x164 = x158 + x163; +Tbase Syntax.TZ x165 = 0x9 * x164; +Tbase Syntax.TZ x166 = x157 + x165; +Tbase Syntax.TZ x167 = x142 + x166; +Tbase Syntax.TZ x168 = x167 >>> 0x19; +Tbase Syntax.TZ x169 = x2 * x18; +Tbase Syntax.TZ x170 = x17 * 0x2; +Tbase Syntax.TZ x171 = x3 * x170; +Tbase Syntax.TZ x172 = x16 * 0x2; +Tbase Syntax.TZ x173 = x4 * x172; +Tbase Syntax.TZ x174 = x15 * 0x2; +Tbase Syntax.TZ x175 = x5 * x174; +Tbase Syntax.TZ x176 = x14 * 0x2; +Tbase Syntax.TZ x177 = x6 * x176; +Tbase Syntax.TZ x178 = x13 * 0x2; +Tbase Syntax.TZ x179 = x7 * x178; +Tbase Syntax.TZ x180 = x8 * x12; +Tbase Syntax.TZ x181 = x179 + x180; +Tbase Syntax.TZ x182 = x177 + x181; +Tbase Syntax.TZ x183 = x175 + x182; +Tbase Syntax.TZ x184 = x173 + x183; +Tbase Syntax.TZ x185 = x171 + x184; +Tbase Syntax.TZ x186 = x169 + x185; +Tbase Syntax.TZ x187 = x * x11; +Tbase Syntax.TZ x188 = x0 * x10; +Tbase Syntax.TZ x189 = x1 * x9; +Tbase Syntax.TZ x190 = x188 + x189; +Tbase Syntax.TZ x191 = x187 + x190; +Tbase Syntax.TZ x192 = 0x9 * x191; +Tbase Syntax.TZ x193 = x186 + x192; +Tbase Syntax.TZ x194 = x168 + x193; +Tbase Syntax.TZ x195 = x194 >>> 0x19; +Tbase Syntax.TZ x196 = x1 * x18; +Tbase Syntax.TZ x197 = x17 * 0x2; +Tbase Syntax.TZ x198 = x2 * x197; +Tbase Syntax.TZ x199 = x16 * 0x2; +Tbase Syntax.TZ x200 = x3 * x199; +Tbase Syntax.TZ x201 = x15 * 0x2; +Tbase Syntax.TZ x202 = x4 * x201; +Tbase Syntax.TZ x203 = x14 * 0x2; +Tbase Syntax.TZ x204 = x5 * x203; +Tbase Syntax.TZ x205 = x13 * 0x2; +Tbase Syntax.TZ x206 = x6 * x205; +Tbase Syntax.TZ x207 = x12 * 0x2; +Tbase Syntax.TZ x208 = x7 * x207; +Tbase Syntax.TZ x209 = x8 * x11; +Tbase Syntax.TZ x210 = x208 + x209; +Tbase Syntax.TZ x211 = x206 + x210; +Tbase Syntax.TZ x212 = x204 + x211; +Tbase Syntax.TZ x213 = x202 + x212; +Tbase Syntax.TZ x214 = x200 + x213; +Tbase Syntax.TZ x215 = x198 + x214; +Tbase Syntax.TZ x216 = x196 + x215; +Tbase Syntax.TZ x217 = x * x10; +Tbase Syntax.TZ x218 = x0 * x9; +Tbase Syntax.TZ x219 = x217 + x218; +Tbase Syntax.TZ x220 = 0x9 * x219; +Tbase Syntax.TZ x221 = x216 + x220; +Tbase Syntax.TZ x222 = x195 + x221; +Tbase Syntax.TZ x223 = x222 >>> 0x19; +Tbase Syntax.TZ x224 = x0 * x18; +Tbase Syntax.TZ x225 = x17 * 0x2; +Tbase Syntax.TZ x226 = x1 * x225; +Tbase Syntax.TZ x227 = x16 * 0x2; +Tbase Syntax.TZ x228 = x2 * x227; +Tbase Syntax.TZ x229 = x15 * 0x2; +Tbase Syntax.TZ x230 = x3 * x229; +Tbase Syntax.TZ x231 = x14 * 0x2; +Tbase Syntax.TZ x232 = x4 * x231; +Tbase Syntax.TZ x233 = x13 * 0x2; +Tbase Syntax.TZ x234 = x5 * x233; +Tbase Syntax.TZ x235 = x12 * 0x2; +Tbase Syntax.TZ x236 = x6 * x235; +Tbase Syntax.TZ x237 = x11 * 0x2; +Tbase Syntax.TZ x238 = x7 * x237; +Tbase Syntax.TZ x239 = x8 * x10; +Tbase Syntax.TZ x240 = x238 + x239; +Tbase Syntax.TZ x241 = x236 + x240; +Tbase Syntax.TZ x242 = x234 + x241; +Tbase Syntax.TZ x243 = x232 + x242; +Tbase Syntax.TZ x244 = x230 + x243; +Tbase Syntax.TZ x245 = x228 + x244; +Tbase Syntax.TZ x246 = x226 + x245; +Tbase Syntax.TZ x247 = x224 + x246; +Tbase Syntax.TZ x248 = x * x9; +Tbase Syntax.TZ x249 = 0x9 * x248; +Tbase Syntax.TZ x250 = x247 + x249; +Tbase Syntax.TZ x251 = x223 + x250; +Tbase Syntax.TZ x252 = x251 >>> 0x19; +Tbase Syntax.TZ x253 = x * x18; +Tbase Syntax.TZ x254 = x17 * 0x2; +Tbase Syntax.TZ x255 = x0 * x254; +Tbase Syntax.TZ x256 = x16 * 0x2; +Tbase Syntax.TZ x257 = x1 * x256; +Tbase Syntax.TZ x258 = x15 * 0x2; +Tbase Syntax.TZ x259 = x2 * x258; +Tbase Syntax.TZ x260 = x14 * 0x2; +Tbase Syntax.TZ x261 = x3 * x260; +Tbase Syntax.TZ x262 = x13 * 0x2; +Tbase Syntax.TZ x263 = x4 * x262; +Tbase Syntax.TZ x264 = x12 * 0x2; +Tbase Syntax.TZ x265 = x5 * x264; +Tbase Syntax.TZ x266 = x11 * 0x2; +Tbase Syntax.TZ x267 = x6 * x266; +Tbase Syntax.TZ x268 = x10 * 0x2; +Tbase Syntax.TZ x269 = x7 * x268; +Tbase Syntax.TZ x270 = x8 * x9; +Tbase Syntax.TZ x271 = x269 + x270; +Tbase Syntax.TZ x272 = x267 + x271; +Tbase Syntax.TZ x273 = x265 + x272; +Tbase Syntax.TZ x274 = x263 + x273; +Tbase Syntax.TZ x275 = x261 + x274; +Tbase Syntax.TZ x276 = x259 + x275; +Tbase Syntax.TZ x277 = x257 + x276; +Tbase Syntax.TZ x278 = x255 + x277; +Tbase Syntax.TZ x279 = x253 + x278; +Tbase Syntax.TZ x280 = x252 + x279; +Tbase Syntax.TZ x281 = x280 >>> 0x19; +Tbase Syntax.TZ x282 = 0x9 * x281; +Tbase Syntax.TZ x283 = x47 & 0x3ffffff; +Tbase Syntax.TZ x284 = x282 + x283; +Tbase Syntax.TZ x285 = x284 >>> 0x1a; +Tbase Syntax.TZ x286 = x69 & 0x1ffffff; +Tbase Syntax.TZ x287 = x285 + x286; +Tbase Syntax.TZ x288 = x280 & 0x1ffffff; +Tbase Syntax.TZ x289 = x251 & 0x1ffffff; +Tbase Syntax.TZ x290 = x222 & 0x1ffffff; +Tbase Syntax.TZ x291 = x194 & 0x1ffffff; +Tbase Syntax.TZ x292 = x167 & 0x1ffffff; +Tbase Syntax.TZ x293 = x141 & 0x1ffffff; +Tbase Syntax.TZ x294 = x116 & 0x1ffffff; +Tbase Syntax.TZ x295 = x287 >>> 0x19; +Tbase Syntax.TZ x296 = x92 & 0x1ffffff; +Tbase Syntax.TZ x297 = x295 + x296; +Tbase Syntax.TZ x298 = x287 & 0x1ffffff; +Tbase Syntax.TZ x299 = x284 & 0x3ffffff; +(Return x288, Return x289, Return x290, Return x291, +Return x292, Return x293, Return x294, Return x297, +Return x298, Return x299) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddDisplay.log b/src/SpecificGen/GF25519_32Reflective/Reified/AddDisplay.log new file mode 100644 index 000000000..156f0286e --- /dev/null +++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddDisplay.log @@ -0,0 +1,45 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x + x9; +Tbase Syntax.TZ x20 = x0 + x10; +Tbase Syntax.TZ x21 = x1 + x11; +Tbase Syntax.TZ x22 = x2 + x12; +Tbase Syntax.TZ x23 = x3 + x13; +Tbase Syntax.TZ x24 = x4 + x14; +Tbase Syntax.TZ x25 = x5 + x15; +Tbase Syntax.TZ x26 = x6 + x16; +Tbase Syntax.TZ x27 = x7 + x17; +Tbase Syntax.TZ x28 = x8 + x18; +(Return x19, Return x20, Return x21, Return x22, Return x23, +Return x24, Return x25, Return x26, Return x27, Return x28) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddJavaDisplay.log b/src/SpecificGen/GF25519_32Reflective/Reified/AddJavaDisplay.log new file mode 100644 index 000000000..156f0286e --- /dev/null +++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddJavaDisplay.log @@ -0,0 +1,45 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x + x9; +Tbase Syntax.TZ x20 = x0 + x10; +Tbase Syntax.TZ x21 = x1 + x11; +Tbase Syntax.TZ x22 = x2 + x12; +Tbase Syntax.TZ x23 = x3 + x13; +Tbase Syntax.TZ x24 = x4 + x14; +Tbase Syntax.TZ x25 = x5 + x15; +Tbase Syntax.TZ x26 = x6 + x16; +Tbase Syntax.TZ x27 = x7 + x17; +Tbase Syntax.TZ x28 = x8 + x18; +(Return x19, Return x20, Return x21, Return x22, Return x23, +Return x24, Return x25, Return x26, Return x27, Return x28) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/MulDisplay.log b/src/SpecificGen/GF25519_32Reflective/Reified/MulDisplay.log new file mode 100644 index 000000000..30f70a7a2 --- /dev/null +++ b/src/SpecificGen/GF25519_32Reflective/Reified/MulDisplay.log @@ -0,0 +1,297 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x8 * x18; +Tbase Syntax.TZ x20 = x17 * 0x2; +Tbase Syntax.TZ x21 = x * x20; +Tbase Syntax.TZ x22 = x0 * x16; +Tbase Syntax.TZ x23 = x15 * 0x2; +Tbase Syntax.TZ x24 = x1 * x23; +Tbase Syntax.TZ x25 = x2 * x14; +Tbase Syntax.TZ x26 = x13 * 0x2; +Tbase Syntax.TZ x27 = x3 * x26; +Tbase Syntax.TZ x28 = x4 * x12; +Tbase Syntax.TZ x29 = x11 * 0x2; +Tbase Syntax.TZ x30 = x5 * x29; +Tbase Syntax.TZ x31 = x6 * x10; +Tbase Syntax.TZ x32 = x9 * 0x2; +Tbase Syntax.TZ x33 = x7 * x32; +Tbase Syntax.TZ x34 = x31 + x33; +Tbase Syntax.TZ x35 = x30 + x34; +Tbase Syntax.TZ x36 = x28 + x35; +Tbase Syntax.TZ x37 = x27 + x36; +Tbase Syntax.TZ x38 = x25 + x37; +Tbase Syntax.TZ x39 = x24 + x38; +Tbase Syntax.TZ x40 = x22 + x39; +Tbase Syntax.TZ x41 = x21 + x40; +Tbase Syntax.TZ x42 = 0x13 * x41; +Tbase Syntax.TZ x43 = x19 + x42; +Tbase Syntax.TZ x44 = x43 >> 0x1a; +Tbase Syntax.TZ x45 = x7 * x18; +Tbase Syntax.TZ x46 = x8 * x17; +Tbase Syntax.TZ x47 = x45 + x46; +Tbase Syntax.TZ x48 = x * x16; +Tbase Syntax.TZ x49 = x0 * x15; +Tbase Syntax.TZ x50 = x1 * x14; +Tbase Syntax.TZ x51 = x2 * x13; +Tbase Syntax.TZ x52 = x3 * x12; +Tbase Syntax.TZ x53 = x4 * x11; +Tbase Syntax.TZ x54 = x5 * x10; +Tbase Syntax.TZ x55 = x6 * x9; +Tbase Syntax.TZ x56 = x54 + x55; +Tbase Syntax.TZ x57 = x53 + x56; +Tbase Syntax.TZ x58 = x52 + x57; +Tbase Syntax.TZ x59 = x51 + x58; +Tbase Syntax.TZ x60 = x50 + x59; +Tbase Syntax.TZ x61 = x49 + x60; +Tbase Syntax.TZ x62 = x48 + x61; +Tbase Syntax.TZ x63 = 0x13 * x62; +Tbase Syntax.TZ x64 = x47 + x63; +Tbase Syntax.TZ x65 = x44 + x64; +Tbase Syntax.TZ x66 = x65 >> 0x19; +Tbase Syntax.TZ x67 = x6 * x18; +Tbase Syntax.TZ x68 = x17 * 0x2; +Tbase Syntax.TZ x69 = x7 * x68; +Tbase Syntax.TZ x70 = x8 * x16; +Tbase Syntax.TZ x71 = x69 + x70; +Tbase Syntax.TZ x72 = x67 + x71; +Tbase Syntax.TZ x73 = x15 * 0x2; +Tbase Syntax.TZ x74 = x * x73; +Tbase Syntax.TZ x75 = x0 * x14; +Tbase Syntax.TZ x76 = x13 * 0x2; +Tbase Syntax.TZ x77 = x1 * x76; +Tbase Syntax.TZ x78 = x2 * x12; +Tbase Syntax.TZ x79 = x11 * 0x2; +Tbase Syntax.TZ x80 = x3 * x79; +Tbase Syntax.TZ x81 = x4 * x10; +Tbase Syntax.TZ x82 = x9 * 0x2; +Tbase Syntax.TZ x83 = x5 * x82; +Tbase Syntax.TZ x84 = x81 + x83; +Tbase Syntax.TZ x85 = x80 + x84; +Tbase Syntax.TZ x86 = x78 + x85; +Tbase Syntax.TZ x87 = x77 + x86; +Tbase Syntax.TZ x88 = x75 + x87; +Tbase Syntax.TZ x89 = x74 + x88; +Tbase Syntax.TZ x90 = 0x13 * x89; +Tbase Syntax.TZ x91 = x72 + x90; +Tbase Syntax.TZ x92 = x66 + x91; +Tbase Syntax.TZ x93 = x92 >> 0x1a; +Tbase Syntax.TZ x94 = x5 * x18; +Tbase Syntax.TZ x95 = x6 * x17; +Tbase Syntax.TZ x96 = x7 * x16; +Tbase Syntax.TZ x97 = x8 * x15; +Tbase Syntax.TZ x98 = x96 + x97; +Tbase Syntax.TZ x99 = x95 + x98; +Tbase Syntax.TZ x100 = x94 + x99; +Tbase Syntax.TZ x101 = x * x14; +Tbase Syntax.TZ x102 = x0 * x13; +Tbase Syntax.TZ x103 = x1 * x12; +Tbase Syntax.TZ x104 = x2 * x11; +Tbase Syntax.TZ x105 = x3 * x10; +Tbase Syntax.TZ x106 = x4 * x9; +Tbase Syntax.TZ x107 = x105 + x106; +Tbase Syntax.TZ x108 = x104 + x107; +Tbase Syntax.TZ x109 = x103 + x108; +Tbase Syntax.TZ x110 = x102 + x109; +Tbase Syntax.TZ x111 = x101 + x110; +Tbase Syntax.TZ x112 = 0x13 * x111; +Tbase Syntax.TZ x113 = x100 + x112; +Tbase Syntax.TZ x114 = x93 + x113; +Tbase Syntax.TZ x115 = x114 >> 0x19; +Tbase Syntax.TZ x116 = x4 * x18; +Tbase Syntax.TZ x117 = x17 * 0x2; +Tbase Syntax.TZ x118 = x5 * x117; +Tbase Syntax.TZ x119 = x6 * x16; +Tbase Syntax.TZ x120 = x15 * 0x2; +Tbase Syntax.TZ x121 = x7 * x120; +Tbase Syntax.TZ x122 = x8 * x14; +Tbase Syntax.TZ x123 = x121 + x122; +Tbase Syntax.TZ x124 = x119 + x123; +Tbase Syntax.TZ x125 = x118 + x124; +Tbase Syntax.TZ x126 = x116 + x125; +Tbase Syntax.TZ x127 = x13 * 0x2; +Tbase Syntax.TZ x128 = x * x127; +Tbase Syntax.TZ x129 = x0 * x12; +Tbase Syntax.TZ x130 = x11 * 0x2; +Tbase Syntax.TZ x131 = x1 * x130; +Tbase Syntax.TZ x132 = x2 * x10; +Tbase Syntax.TZ x133 = x9 * 0x2; +Tbase Syntax.TZ x134 = x3 * x133; +Tbase Syntax.TZ x135 = x132 + x134; +Tbase Syntax.TZ x136 = x131 + x135; +Tbase Syntax.TZ x137 = x129 + x136; +Tbase Syntax.TZ x138 = x128 + x137; +Tbase Syntax.TZ x139 = 0x13 * x138; +Tbase Syntax.TZ x140 = x126 + x139; +Tbase Syntax.TZ x141 = x115 + x140; +Tbase Syntax.TZ x142 = x141 >> 0x1a; +Tbase Syntax.TZ x143 = x3 * x18; +Tbase Syntax.TZ x144 = x4 * x17; +Tbase Syntax.TZ x145 = x5 * x16; +Tbase Syntax.TZ x146 = x6 * x15; +Tbase Syntax.TZ x147 = x7 * x14; +Tbase Syntax.TZ x148 = x8 * x13; +Tbase Syntax.TZ x149 = x147 + x148; +Tbase Syntax.TZ x150 = x146 + x149; +Tbase Syntax.TZ x151 = x145 + x150; +Tbase Syntax.TZ x152 = x144 + x151; +Tbase Syntax.TZ x153 = x143 + x152; +Tbase Syntax.TZ x154 = x * x12; +Tbase Syntax.TZ x155 = x0 * x11; +Tbase Syntax.TZ x156 = x1 * x10; +Tbase Syntax.TZ x157 = x2 * x9; +Tbase Syntax.TZ x158 = x156 + x157; +Tbase Syntax.TZ x159 = x155 + x158; +Tbase Syntax.TZ x160 = x154 + x159; +Tbase Syntax.TZ x161 = 0x13 * x160; +Tbase Syntax.TZ x162 = x153 + x161; +Tbase Syntax.TZ x163 = x142 + x162; +Tbase Syntax.TZ x164 = x163 >> 0x19; +Tbase Syntax.TZ x165 = x2 * x18; +Tbase Syntax.TZ x166 = x17 * 0x2; +Tbase Syntax.TZ x167 = x3 * x166; +Tbase Syntax.TZ x168 = x4 * x16; +Tbase Syntax.TZ x169 = x15 * 0x2; +Tbase Syntax.TZ x170 = x5 * x169; +Tbase Syntax.TZ x171 = x6 * x14; +Tbase Syntax.TZ x172 = x13 * 0x2; +Tbase Syntax.TZ x173 = x7 * x172; +Tbase Syntax.TZ x174 = x8 * x12; +Tbase Syntax.TZ x175 = x173 + x174; +Tbase Syntax.TZ x176 = x171 + x175; +Tbase Syntax.TZ x177 = x170 + x176; +Tbase Syntax.TZ x178 = x168 + x177; +Tbase Syntax.TZ x179 = x167 + x178; +Tbase Syntax.TZ x180 = x165 + x179; +Tbase Syntax.TZ x181 = x11 * 0x2; +Tbase Syntax.TZ x182 = x * x181; +Tbase Syntax.TZ x183 = x0 * x10; +Tbase Syntax.TZ x184 = x9 * 0x2; +Tbase Syntax.TZ x185 = x1 * x184; +Tbase Syntax.TZ x186 = x183 + x185; +Tbase Syntax.TZ x187 = x182 + x186; +Tbase Syntax.TZ x188 = 0x13 * x187; +Tbase Syntax.TZ x189 = x180 + x188; +Tbase Syntax.TZ x190 = x164 + x189; +Tbase Syntax.TZ x191 = x190 >> 0x1a; +Tbase Syntax.TZ x192 = x1 * x18; +Tbase Syntax.TZ x193 = x2 * x17; +Tbase Syntax.TZ x194 = x3 * x16; +Tbase Syntax.TZ x195 = x4 * x15; +Tbase Syntax.TZ x196 = x5 * x14; +Tbase Syntax.TZ x197 = x6 * x13; +Tbase Syntax.TZ x198 = x7 * x12; +Tbase Syntax.TZ x199 = x8 * x11; +Tbase Syntax.TZ x200 = x198 + x199; +Tbase Syntax.TZ x201 = x197 + x200; +Tbase Syntax.TZ x202 = x196 + x201; +Tbase Syntax.TZ x203 = x195 + x202; +Tbase Syntax.TZ x204 = x194 + x203; +Tbase Syntax.TZ x205 = x193 + x204; +Tbase Syntax.TZ x206 = x192 + x205; +Tbase Syntax.TZ x207 = x * x10; +Tbase Syntax.TZ x208 = x0 * x9; +Tbase Syntax.TZ x209 = x207 + x208; +Tbase Syntax.TZ x210 = 0x13 * x209; +Tbase Syntax.TZ x211 = x206 + x210; +Tbase Syntax.TZ x212 = x191 + x211; +Tbase Syntax.TZ x213 = x212 >> 0x19; +Tbase Syntax.TZ x214 = x0 * x18; +Tbase Syntax.TZ x215 = x17 * 0x2; +Tbase Syntax.TZ x216 = x1 * x215; +Tbase Syntax.TZ x217 = x2 * x16; +Tbase Syntax.TZ x218 = x15 * 0x2; +Tbase Syntax.TZ x219 = x3 * x218; +Tbase Syntax.TZ x220 = x4 * x14; +Tbase Syntax.TZ x221 = x13 * 0x2; +Tbase Syntax.TZ x222 = x5 * x221; +Tbase Syntax.TZ x223 = x6 * x12; +Tbase Syntax.TZ x224 = x11 * 0x2; +Tbase Syntax.TZ x225 = x7 * x224; +Tbase Syntax.TZ x226 = x8 * x10; +Tbase Syntax.TZ x227 = x225 + x226; +Tbase Syntax.TZ x228 = x223 + x227; +Tbase Syntax.TZ x229 = x222 + x228; +Tbase Syntax.TZ x230 = x220 + x229; +Tbase Syntax.TZ x231 = x219 + x230; +Tbase Syntax.TZ x232 = x217 + x231; +Tbase Syntax.TZ x233 = x216 + x232; +Tbase Syntax.TZ x234 = x214 + x233; +Tbase Syntax.TZ x235 = x9 * 0x2; +Tbase Syntax.TZ x236 = x * x235; +Tbase Syntax.TZ x237 = 0x13 * x236; +Tbase Syntax.TZ x238 = x234 + x237; +Tbase Syntax.TZ x239 = x213 + x238; +Tbase Syntax.TZ x240 = x239 >> 0x1a; +Tbase Syntax.TZ x241 = x * x18; +Tbase Syntax.TZ x242 = x0 * x17; +Tbase Syntax.TZ x243 = x1 * x16; +Tbase Syntax.TZ x244 = x2 * x15; +Tbase Syntax.TZ x245 = x3 * x14; +Tbase Syntax.TZ x246 = x4 * x13; +Tbase Syntax.TZ x247 = x5 * x12; +Tbase Syntax.TZ x248 = x6 * x11; +Tbase Syntax.TZ x249 = x7 * x10; +Tbase Syntax.TZ x250 = x8 * x9; +Tbase Syntax.TZ x251 = x249 + x250; +Tbase Syntax.TZ x252 = x248 + x251; +Tbase Syntax.TZ x253 = x247 + x252; +Tbase Syntax.TZ x254 = x246 + x253; +Tbase Syntax.TZ x255 = x245 + x254; +Tbase Syntax.TZ x256 = x244 + x255; +Tbase Syntax.TZ x257 = x243 + x256; +Tbase Syntax.TZ x258 = x242 + x257; +Tbase Syntax.TZ x259 = x241 + x258; +Tbase Syntax.TZ x260 = x240 + x259; +Tbase Syntax.TZ x261 = x260 >> 0x19; +Tbase Syntax.TZ x262 = 0x13 * x261; +Tbase Syntax.TZ x263 = x43 & 0x3ffffff; +Tbase Syntax.TZ x264 = x262 + x263; +Tbase Syntax.TZ x265 = x264 >> 0x1a; +Tbase Syntax.TZ x266 = x65 & 0x1ffffff; +Tbase Syntax.TZ x267 = x265 + x266; +Tbase Syntax.TZ x268 = x260 & 0x1ffffff; +Tbase Syntax.TZ x269 = x239 & 0x3ffffff; +Tbase Syntax.TZ x270 = x212 & 0x1ffffff; +Tbase Syntax.TZ x271 = x190 & 0x3ffffff; +Tbase Syntax.TZ x272 = x163 & 0x1ffffff; +Tbase Syntax.TZ x273 = x141 & 0x3ffffff; +Tbase Syntax.TZ x274 = x114 & 0x1ffffff; +Tbase Syntax.TZ x275 = x267 >> 0x19; +Tbase Syntax.TZ x276 = x92 & 0x3ffffff; +Tbase Syntax.TZ x277 = x275 + x276; +Tbase Syntax.TZ x278 = x267 & 0x1ffffff; +Tbase Syntax.TZ x279 = x264 & 0x3ffffff; +(Return x268, Return x269, Return x270, Return x271, +Return x272, Return x273, Return x274, Return x277, +Return x278, Return x279) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/MulJavaDisplay.log b/src/SpecificGen/GF25519_32Reflective/Reified/MulJavaDisplay.log new file mode 100644 index 000000000..d0d6c01b1 --- /dev/null +++ b/src/SpecificGen/GF25519_32Reflective/Reified/MulJavaDisplay.log @@ -0,0 +1,297 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ +x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 + x18 : var Syntax.TZ, +Tbase Syntax.TZ x19 = x8 * x18; +Tbase Syntax.TZ x20 = x17 * 0x2; +Tbase Syntax.TZ x21 = x * x20; +Tbase Syntax.TZ x22 = x0 * x16; +Tbase Syntax.TZ x23 = x15 * 0x2; +Tbase Syntax.TZ x24 = x1 * x23; +Tbase Syntax.TZ x25 = x2 * x14; +Tbase Syntax.TZ x26 = x13 * 0x2; +Tbase Syntax.TZ x27 = x3 * x26; +Tbase Syntax.TZ x28 = x4 * x12; +Tbase Syntax.TZ x29 = x11 * 0x2; +Tbase Syntax.TZ x30 = x5 * x29; +Tbase Syntax.TZ x31 = x6 * x10; +Tbase Syntax.TZ x32 = x9 * 0x2; +Tbase Syntax.TZ x33 = x7 * x32; +Tbase Syntax.TZ x34 = x31 + x33; +Tbase Syntax.TZ x35 = x30 + x34; +Tbase Syntax.TZ x36 = x28 + x35; +Tbase Syntax.TZ x37 = x27 + x36; +Tbase Syntax.TZ x38 = x25 + x37; +Tbase Syntax.TZ x39 = x24 + x38; +Tbase Syntax.TZ x40 = x22 + x39; +Tbase Syntax.TZ x41 = x21 + x40; +Tbase Syntax.TZ x42 = 0x13 * x41; +Tbase Syntax.TZ x43 = x19 + x42; +Tbase Syntax.TZ x44 = x43 >>> 0x1a; +Tbase Syntax.TZ x45 = x7 * x18; +Tbase Syntax.TZ x46 = x8 * x17; +Tbase Syntax.TZ x47 = x45 + x46; +Tbase Syntax.TZ x48 = x * x16; +Tbase Syntax.TZ x49 = x0 * x15; +Tbase Syntax.TZ x50 = x1 * x14; +Tbase Syntax.TZ x51 = x2 * x13; +Tbase Syntax.TZ x52 = x3 * x12; +Tbase Syntax.TZ x53 = x4 * x11; +Tbase Syntax.TZ x54 = x5 * x10; +Tbase Syntax.TZ x55 = x6 * x9; +Tbase Syntax.TZ x56 = x54 + x55; +Tbase Syntax.TZ x57 = x53 + x56; +Tbase Syntax.TZ x58 = x52 + x57; +Tbase Syntax.TZ x59 = x51 + x58; +Tbase Syntax.TZ x60 = x50 + x59; +Tbase Syntax.TZ x61 = x49 + x60; +Tbase Syntax.TZ x62 = x48 + x61; +Tbase Syntax.TZ x63 = 0x13 * x62; +Tbase Syntax.TZ x64 = x47 + x63; +Tbase Syntax.TZ x65 = x44 + x64; +Tbase Syntax.TZ x66 = x65 >>> 0x19; +Tbase Syntax.TZ x67 = x6 * x18; +Tbase Syntax.TZ x68 = x17 * 0x2; +Tbase Syntax.TZ x69 = x7 * x68; +Tbase Syntax.TZ x70 = x8 * x16; +Tbase Syntax.TZ x71 = x69 + x70; +Tbase Syntax.TZ x72 = x67 + x71; +Tbase Syntax.TZ x73 = x15 * 0x2; +Tbase Syntax.TZ x74 = x * x73; +Tbase Syntax.TZ x75 = x0 * x14; +Tbase Syntax.TZ x76 = x13 * 0x2; +Tbase Syntax.TZ x77 = x1 * x76; +Tbase Syntax.TZ x78 = x2 * x12; +Tbase Syntax.TZ x79 = x11 * 0x2; +Tbase Syntax.TZ x80 = x3 * x79; +Tbase Syntax.TZ x81 = x4 * x10; +Tbase Syntax.TZ x82 = x9 * 0x2; +Tbase Syntax.TZ x83 = x5 * x82; +Tbase Syntax.TZ x84 = x81 + x83; +Tbase Syntax.TZ x85 = x80 + x84; +Tbase Syntax.TZ x86 = x78 + x85; +Tbase Syntax.TZ x87 = x77 + x86; +Tbase Syntax.TZ x88 = x75 + x87; +Tbase Syntax.TZ x89 = x74 + x88; +Tbase Syntax.TZ x90 = 0x13 * x89; +Tbase Syntax.TZ x91 = x72 + x90; +Tbase Syntax.TZ x92 = x66 + x91; +Tbase Syntax.TZ x93 = x92 >>> 0x1a; +Tbase Syntax.TZ x94 = x5 * x18; +Tbase Syntax.TZ x95 = x6 * x17; +Tbase Syntax.TZ x96 = x7 * x16; +Tbase Syntax.TZ x97 = x8 * x15; +Tbase Syntax.TZ x98 = x96 + x97; +Tbase Syntax.TZ x99 = x95 + x98; +Tbase Syntax.TZ x100 = x94 + x99; +Tbase Syntax.TZ x101 = x * x14; +Tbase Syntax.TZ x102 = x0 * x13; +Tbase Syntax.TZ x103 = x1 * x12; +Tbase Syntax.TZ x104 = x2 * x11; +Tbase Syntax.TZ x105 = x3 * x10; +Tbase Syntax.TZ x106 = x4 * x9; +Tbase Syntax.TZ x107 = x105 + x106; +Tbase Syntax.TZ x108 = x104 + x107; +Tbase Syntax.TZ x109 = x103 + x108; +Tbase Syntax.TZ x110 = x102 + x109; +Tbase Syntax.TZ x111 = x101 + x110; +Tbase Syntax.TZ x112 = 0x13 * x111; +Tbase Syntax.TZ x113 = x100 + x112; +Tbase Syntax.TZ x114 = x93 + x113; +Tbase Syntax.TZ x115 = x114 >>> 0x19; +Tbase Syntax.TZ x116 = x4 * x18; +Tbase Syntax.TZ x117 = x17 * 0x2; +Tbase Syntax.TZ x118 = x5 * x117; +Tbase Syntax.TZ x119 = x6 * x16; +Tbase Syntax.TZ x120 = x15 * 0x2; +Tbase Syntax.TZ x121 = x7 * x120; +Tbase Syntax.TZ x122 = x8 * x14; +Tbase Syntax.TZ x123 = x121 + x122; +Tbase Syntax.TZ x124 = x119 + x123; +Tbase Syntax.TZ x125 = x118 + x124; +Tbase Syntax.TZ x126 = x116 + x125; +Tbase Syntax.TZ x127 = x13 * 0x2; +Tbase Syntax.TZ x128 = x * x127; +Tbase Syntax.TZ x129 = x0 * x12; +Tbase Syntax.TZ x130 = x11 * 0x2; +Tbase Syntax.TZ x131 = x1 * x130; +Tbase Syntax.TZ x132 = x2 * x10; +Tbase Syntax.TZ x133 = x9 * 0x2; +Tbase Syntax.TZ x134 = x3 * x133; +Tbase Syntax.TZ x135 = x132 + x134; +Tbase Syntax.TZ x136 = x131 + x135; +Tbase Syntax.TZ x137 = x129 + x136; +Tbase Syntax.TZ x138 = x128 + x137; +Tbase Syntax.TZ x139 = 0x13 * x138; +Tbase Syntax.TZ x140 = x126 + x139; +Tbase Syntax.TZ x141 = x115 + x140; +Tbase Syntax.TZ x142 = x141 >>> 0x1a; +Tbase Syntax.TZ x143 = x3 * x18; +Tbase Syntax.TZ x144 = x4 * x17; +Tbase Syntax.TZ x145 = x5 * x16; +Tbase Syntax.TZ x146 = x6 * x15; +Tbase Syntax.TZ x147 = x7 * x14; +Tbase Syntax.TZ x148 = x8 * x13; +Tbase Syntax.TZ x149 = x147 + x148; +Tbase Syntax.TZ x150 = x146 + x149; +Tbase Syntax.TZ x151 = x145 + x150; +Tbase Syntax.TZ x152 = x144 + x151; +Tbase Syntax.TZ x153 = x143 + x152; +Tbase Syntax.TZ x154 = x * x12; +Tbase Syntax.TZ x155 = x0 * x11; +Tbase Syntax.TZ x156 = x1 * x10; +Tbase Syntax.TZ x157 = x2 * x9; +Tbase Syntax.TZ x158 = x156 + x157; +Tbase Syntax.TZ x159 = x155 + x158; +Tbase Syntax.TZ x160 = x154 + x159; +Tbase Syntax.TZ x161 = 0x13 * x160; +Tbase Syntax.TZ x162 = x153 + x161; +Tbase Syntax.TZ x163 = x142 + x162; +Tbase Syntax.TZ x164 = x163 >>> 0x19; +Tbase Syntax.TZ x165 = x2 * x18; +Tbase Syntax.TZ x166 = x17 * 0x2; +Tbase Syntax.TZ x167 = x3 * x166; +Tbase Syntax.TZ x168 = x4 * x16; +Tbase Syntax.TZ x169 = x15 * 0x2; +Tbase Syntax.TZ x170 = x5 * x169; +Tbase Syntax.TZ x171 = x6 * x14; +Tbase Syntax.TZ x172 = x13 * 0x2; +Tbase Syntax.TZ x173 = x7 * x172; +Tbase Syntax.TZ x174 = x8 * x12; +Tbase Syntax.TZ x175 = x173 + x174; +Tbase Syntax.TZ x176 = x171 + x175; +Tbase Syntax.TZ x177 = x170 + x176; +Tbase Syntax.TZ x178 = x168 + x177; +Tbase Syntax.TZ x179 = x167 + x178; +Tbase Syntax.TZ x180 = x165 + x179; +Tbase Syntax.TZ x181 = x11 * 0x2; +Tbase Syntax.TZ x182 = x * x181; +Tbase Syntax.TZ x183 = x0 * x10; +Tbase Syntax.TZ x184 = x9 * 0x2; +Tbase Syntax.TZ x185 = x1 * x184; +Tbase Syntax.TZ x186 = x183 + x185; +Tbase Syntax.TZ x187 = x182 + x186; +Tbase Syntax.TZ x188 = 0x13 * x187; +Tbase Syntax.TZ x189 = x180 + x188; +Tbase Syntax.TZ x190 = x164 + x189; +Tbase Syntax.TZ x191 = x190 >>> 0x1a; +Tbase Syntax.TZ x192 = x1 * x18; +Tbase Syntax.TZ x193 = x2 * x17; +Tbase Syntax.TZ x194 = x3 * x16; +Tbase Syntax.TZ x195 = x4 * x15; +Tbase Syntax.TZ x196 = x5 * x14; +Tbase Syntax.TZ x197 = x6 * x13; +Tbase Syntax.TZ x198 = x7 * x12; +Tbase Syntax.TZ x199 = x8 * x11; +Tbase Syntax.TZ x200 = x198 + x199; +Tbase Syntax.TZ x201 = x197 + x200; +Tbase Syntax.TZ x202 = x196 + x201; +Tbase Syntax.TZ x203 = x195 + x202; +Tbase Syntax.TZ x204 = x194 + x203; +Tbase Syntax.TZ x205 = x193 + x204; +Tbase Syntax.TZ x206 = x192 + x205; +Tbase Syntax.TZ x207 = x * x10; +Tbase Syntax.TZ x208 = x0 * x9; +Tbase Syntax.TZ x209 = x207 + x208; +Tbase Syntax.TZ x210 = 0x13 * x209; +Tbase Syntax.TZ x211 = x206 + x210; +Tbase Syntax.TZ x212 = x191 + x211; +Tbase Syntax.TZ x213 = x212 >>> 0x19; +Tbase Syntax.TZ x214 = x0 * x18; +Tbase Syntax.TZ x215 = x17 * 0x2; +Tbase Syntax.TZ x216 = x1 * x215; +Tbase Syntax.TZ x217 = x2 * x16; +Tbase Syntax.TZ x218 = x15 * 0x2; +Tbase Syntax.TZ x219 = x3 * x218; +Tbase Syntax.TZ x220 = x4 * x14; +Tbase Syntax.TZ x221 = x13 * 0x2; +Tbase Syntax.TZ x222 = x5 * x221; +Tbase Syntax.TZ x223 = x6 * x12; +Tbase Syntax.TZ x224 = x11 * 0x2; +Tbase Syntax.TZ x225 = x7 * x224; +Tbase Syntax.TZ x226 = x8 * x10; +Tbase Syntax.TZ x227 = x225 + x226; +Tbase Syntax.TZ x228 = x223 + x227; +Tbase Syntax.TZ x229 = x222 + x228; +Tbase Syntax.TZ x230 = x220 + x229; +Tbase Syntax.TZ x231 = x219 + x230; +Tbase Syntax.TZ x232 = x217 + x231; +Tbase Syntax.TZ x233 = x216 + x232; +Tbase Syntax.TZ x234 = x214 + x233; +Tbase Syntax.TZ x235 = x9 * 0x2; +Tbase Syntax.TZ x236 = x * x235; +Tbase Syntax.TZ x237 = 0x13 * x236; +Tbase Syntax.TZ x238 = x234 + x237; +Tbase Syntax.TZ x239 = x213 + x238; +Tbase Syntax.TZ x240 = x239 >>> 0x1a; +Tbase Syntax.TZ x241 = x * x18; +Tbase Syntax.TZ x242 = x0 * x17; +Tbase Syntax.TZ x243 = x1 * x16; +Tbase Syntax.TZ x244 = x2 * x15; +Tbase Syntax.TZ x245 = x3 * x14; +Tbase Syntax.TZ x246 = x4 * x13; +Tbase Syntax.TZ x247 = x5 * x12; +Tbase Syntax.TZ x248 = x6 * x11; +Tbase Syntax.TZ x249 = x7 * x10; +Tbase Syntax.TZ x250 = x8 * x9; +Tbase Syntax.TZ x251 = x249 + x250; +Tbase Syntax.TZ x252 = x248 + x251; +Tbase Syntax.TZ x253 = x247 + x252; +Tbase Syntax.TZ x254 = x246 + x253; +Tbase Syntax.TZ x255 = x245 + x254; +Tbase Syntax.TZ x256 = x244 + x255; +Tbase Syntax.TZ x257 = x243 + x256; +Tbase Syntax.TZ x258 = x242 + x257; +Tbase Syntax.TZ x259 = x241 + x258; +Tbase Syntax.TZ x260 = x240 + x259; +Tbase Syntax.TZ x261 = x260 >>> 0x19; +Tbase Syntax.TZ x262 = 0x13 * x261; +Tbase Syntax.TZ x263 = x43 & 0x3ffffff; +Tbase Syntax.TZ x264 = x262 + x263; +Tbase Syntax.TZ x265 = x264 >>> 0x1a; +Tbase Syntax.TZ x266 = x65 & 0x1ffffff; +Tbase Syntax.TZ x267 = x265 + x266; +Tbase Syntax.TZ x268 = x260 & 0x1ffffff; +Tbase Syntax.TZ x269 = x239 & 0x3ffffff; +Tbase Syntax.TZ x270 = x212 & 0x1ffffff; +Tbase Syntax.TZ x271 = x190 & 0x3ffffff; +Tbase Syntax.TZ x272 = x163 & 0x1ffffff; +Tbase Syntax.TZ x273 = x141 & 0x3ffffff; +Tbase Syntax.TZ x274 = x114 & 0x1ffffff; +Tbase Syntax.TZ x275 = x267 >>> 0x19; +Tbase Syntax.TZ x276 = x92 & 0x3ffffff; +Tbase Syntax.TZ x277 = x275 + x276; +Tbase Syntax.TZ x278 = x267 & 0x1ffffff; +Tbase Syntax.TZ x279 = x264 & 0x3ffffff; +(Return x268, Return x269, Return x270, Return x271, +Return x272, Return x273, Return x274, Return x277, +Return x278, Return x279) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log new file mode 100644 index 000000000..c1012d128 --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddDisplay.log @@ -0,0 +1,25 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ, +Tbase Syntax.TZ x9 = x + x4; +Tbase Syntax.TZ x10 = x0 + x5; +Tbase Syntax.TZ x11 = x1 + x6; +Tbase Syntax.TZ x12 = x2 + x7; +Tbase Syntax.TZ x13 = x3 + x8; +(Return x9, Return x10, Return x11, Return x12, Return x13) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddJavaDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/AddJavaDisplay.log new file mode 100644 index 000000000..c1012d128 --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddJavaDisplay.log @@ -0,0 +1,25 @@ +raddW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ, +Tbase Syntax.TZ x9 = x + x4; +Tbase Syntax.TZ x10 = x0 + x5; +Tbase Syntax.TZ x11 = x1 + x6; +Tbase Syntax.TZ x12 = x2 + x7; +Tbase Syntax.TZ x13 = x3 + x8; +(Return x9, Return x10, Return x11, Return x12, Return x13) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepDisplay.log new file mode 100644 index 000000000..d826efaab --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepDisplay.log @@ -0,0 +1,1050 @@ +rladderstepW = +fun var : base_type -> Type => +λ +_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 + x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 + x43 : var TZ, +Tbase TZ x44 = x24 + x29; +Tbase TZ x45 = x25 + x30; +Tbase TZ x46 = x26 + x31; +Tbase TZ x47 = x27 + x32; +Tbase TZ x48 = x28 + x33; +Tbase TZ x49 = x48 * x48; +Tbase TZ x50 = x44 * x47; +Tbase TZ x51 = x45 * x46; +Tbase TZ x52 = x46 * x45; +Tbase TZ x53 = x47 * x44; +Tbase TZ x54 = x52 + x53; +Tbase TZ x55 = x51 + x54; +Tbase TZ x56 = x50 + x55; +Tbase TZ x57 = 0x13; +Tbase TZ x58 = x57 * x56; +Tbase TZ x59 = x49 + x58; +Tbase TZ x60 = 0x33; +Tbase TZ x61 = x59 >> x60; +Tbase TZ x62 = x47 * x48; +Tbase TZ x63 = x48 * x47; +Tbase TZ x64 = x62 + x63; +Tbase TZ x65 = x44 * x46; +Tbase TZ x66 = x45 * x45; +Tbase TZ x67 = x46 * x44; +Tbase TZ x68 = x66 + x67; +Tbase TZ x69 = x65 + x68; +Tbase TZ x70 = 0x13; +Tbase TZ x71 = x70 * x69; +Tbase TZ x72 = x64 + x71; +Tbase TZ x73 = x61 + x72; +Tbase TZ x74 = 0x33; +Tbase TZ x75 = x73 >> x74; +Tbase TZ x76 = x46 * x48; +Tbase TZ x77 = x47 * x47; +Tbase TZ x78 = x48 * x46; +Tbase TZ x79 = x77 + x78; +Tbase TZ x80 = x76 + x79; +Tbase TZ x81 = x44 * x45; +Tbase TZ x82 = x45 * x44; +Tbase TZ x83 = x81 + x82; +Tbase TZ x84 = 0x13; +Tbase TZ x85 = x84 * x83; +Tbase TZ x86 = x80 + x85; +Tbase TZ x87 = x75 + x86; +Tbase TZ x88 = 0x33; +Tbase TZ x89 = x87 >> x88; +Tbase TZ x90 = x45 * x48; +Tbase TZ x91 = x46 * x47; +Tbase TZ x92 = x47 * x46; +Tbase TZ x93 = x48 * x45; +Tbase TZ x94 = x92 + x93; +Tbase TZ x95 = x91 + x94; +Tbase TZ x96 = x90 + x95; +Tbase TZ x97 = x44 * x44; +Tbase TZ x98 = 0x13; +Tbase TZ x99 = x98 * x97; +Tbase TZ x100 = x96 + x99; +Tbase TZ x101 = x89 + x100; +Tbase TZ x102 = 0x33; +Tbase TZ x103 = x101 >> x102; +Tbase TZ x104 = x44 * x48; +Tbase TZ x105 = x45 * x47; +Tbase TZ x106 = x46 * x46; +Tbase TZ x107 = x47 * x45; +Tbase TZ x108 = x48 * x44; +Tbase TZ x109 = x107 + x108; +Tbase TZ x110 = x106 + x109; +Tbase TZ x111 = x105 + x110; +Tbase TZ x112 = x104 + x111; +Tbase TZ x113 = x103 + x112; +Tbase TZ x114 = 0x33; +Tbase TZ x115 = x113 >> x114; +Tbase TZ x116 = 0x13; +Tbase TZ x117 = x116 * x115; +Tbase TZ x118 = 0x7ffffffffffff; +Tbase TZ x119 = x59 & x118; +Tbase TZ x120 = x117 + x119; +Tbase TZ x121 = 0x33; +Tbase TZ x122 = x120 >> x121; +Tbase TZ x123 = 0x7ffffffffffff; +Tbase TZ x124 = x73 & x123; +Tbase TZ x125 = x122 + x124; +Tbase TZ x126 = 0x7ffffffffffff; +Tbase TZ x127 = x113 & x126; +Tbase TZ x128 = 0x7ffffffffffff; +Tbase TZ x129 = x101 & x128; +Tbase TZ x130 = 0x33; +Tbase TZ x131 = x125 >> x130; +Tbase TZ x132 = 0x7ffffffffffff; +Tbase TZ x133 = x87 & x132; +Tbase TZ x134 = x131 + x133; +Tbase TZ x135 = 0x7ffffffffffff; +Tbase TZ x136 = x125 & x135; +Tbase TZ x137 = 0x7ffffffffffff; +Tbase TZ x138 = x120 & x137; +Tbase TZ x139 = 0xffffffffffffe; +Tbase TZ x140 = x139 + x24; +Tbase TZ x141 = x140 - x29; +Tbase TZ x142 = 0xffffffffffffe; +Tbase TZ x143 = x142 + x25; +Tbase TZ x144 = x143 - x30; +Tbase TZ x145 = 0xffffffffffffe; +Tbase TZ x146 = x145 + x26; +Tbase TZ x147 = x146 - x31; +Tbase TZ x148 = 0xffffffffffffe; +Tbase TZ x149 = x148 + x27; +Tbase TZ x150 = x149 - x32; +Tbase TZ x151 = 0xfffffffffffda; +Tbase TZ x152 = x151 + x28; +Tbase TZ x153 = x152 - x33; +Tbase TZ x154 = x153 * x153; +Tbase TZ x155 = x141 * x150; +Tbase TZ x156 = x144 * x147; +Tbase TZ x157 = x147 * x144; +Tbase TZ x158 = x150 * x141; +Tbase TZ x159 = x157 + x158; +Tbase TZ x160 = x156 + x159; +Tbase TZ x161 = x155 + x160; +Tbase TZ x162 = 0x13; +Tbase TZ x163 = x162 * x161; +Tbase TZ x164 = x154 + x163; +Tbase TZ x165 = 0x33; +Tbase TZ x166 = x164 >> x165; +Tbase TZ x167 = x150 * x153; +Tbase TZ x168 = x153 * x150; +Tbase TZ x169 = x167 + x168; +Tbase TZ x170 = x141 * x147; +Tbase TZ x171 = x144 * x144; +Tbase TZ x172 = x147 * x141; +Tbase TZ x173 = x171 + x172; +Tbase TZ x174 = x170 + x173; +Tbase TZ x175 = 0x13; +Tbase TZ x176 = x175 * x174; +Tbase TZ x177 = x169 + x176; +Tbase TZ x178 = x166 + x177; +Tbase TZ x179 = 0x33; +Tbase TZ x180 = x178 >> x179; +Tbase TZ x181 = x147 * x153; +Tbase TZ x182 = x150 * x150; +Tbase TZ x183 = x153 * x147; +Tbase TZ x184 = x182 + x183; +Tbase TZ x185 = x181 + x184; +Tbase TZ x186 = x141 * x144; +Tbase TZ x187 = x144 * x141; +Tbase TZ x188 = x186 + x187; +Tbase TZ x189 = 0x13; +Tbase TZ x190 = x189 * x188; +Tbase TZ x191 = x185 + x190; +Tbase TZ x192 = x180 + x191; +Tbase TZ x193 = 0x33; +Tbase TZ x194 = x192 >> x193; +Tbase TZ x195 = x144 * x153; +Tbase TZ x196 = x147 * x150; +Tbase TZ x197 = x150 * x147; +Tbase TZ x198 = x153 * x144; +Tbase TZ x199 = x197 + x198; +Tbase TZ x200 = x196 + x199; +Tbase TZ x201 = x195 + x200; +Tbase TZ x202 = x141 * x141; +Tbase TZ x203 = 0x13; +Tbase TZ x204 = x203 * x202; +Tbase TZ x205 = x201 + x204; +Tbase TZ x206 = x194 + x205; +Tbase TZ x207 = 0x33; +Tbase TZ x208 = x206 >> x207; +Tbase TZ x209 = x141 * x153; +Tbase TZ x210 = x144 * x150; +Tbase TZ x211 = x147 * x147; +Tbase TZ x212 = x150 * x144; +Tbase TZ x213 = x153 * x141; +Tbase TZ x214 = x212 + x213; +Tbase TZ x215 = x211 + x214; +Tbase TZ x216 = x210 + x215; +Tbase TZ x217 = x209 + x216; +Tbase TZ x218 = x208 + x217; +Tbase TZ x219 = 0x33; +Tbase TZ x220 = x218 >> x219; +Tbase TZ x221 = 0x13; +Tbase TZ x222 = x221 * x220; +Tbase TZ x223 = 0x7ffffffffffff; +Tbase TZ x224 = x164 & x223; +Tbase TZ x225 = x222 + x224; +Tbase TZ x226 = 0x33; +Tbase TZ x227 = x225 >> x226; +Tbase TZ x228 = 0x7ffffffffffff; +Tbase TZ x229 = x178 & x228; +Tbase TZ x230 = x227 + x229; +Tbase TZ x231 = 0x7ffffffffffff; +Tbase TZ x232 = x218 & x231; +Tbase TZ x233 = 0x7ffffffffffff; +Tbase TZ x234 = x206 & x233; +Tbase TZ x235 = 0x33; +Tbase TZ x236 = x230 >> x235; +Tbase TZ x237 = 0x7ffffffffffff; +Tbase TZ x238 = x192 & x237; +Tbase TZ x239 = x236 + x238; +Tbase TZ x240 = 0x7ffffffffffff; +Tbase TZ x241 = x230 & x240; +Tbase TZ x242 = 0x7ffffffffffff; +Tbase TZ x243 = x225 & x242; +Tbase TZ x244 = 0xffffffffffffe; +Tbase TZ x245 = x244 + x127; +Tbase TZ x246 = x245 - x232; +Tbase TZ x247 = 0xffffffffffffe; +Tbase TZ x248 = x247 + x129; +Tbase TZ x249 = x248 - x234; +Tbase TZ x250 = 0xffffffffffffe; +Tbase TZ x251 = x250 + x134; +Tbase TZ x252 = x251 - x239; +Tbase TZ x253 = 0xffffffffffffe; +Tbase TZ x254 = x253 + x136; +Tbase TZ x255 = x254 - x241; +Tbase TZ x256 = 0xfffffffffffda; +Tbase TZ x257 = x256 + x138; +Tbase TZ x258 = x257 - x243; +Tbase TZ x259 = x34 + x39; +Tbase TZ x260 = x35 + x40; +Tbase TZ x261 = x36 + x41; +Tbase TZ x262 = x37 + x42; +Tbase TZ x263 = x38 + x43; +Tbase TZ x264 = 0xffffffffffffe; +Tbase TZ x265 = x264 + x34; +Tbase TZ x266 = x265 - x39; +Tbase TZ x267 = 0xffffffffffffe; +Tbase TZ x268 = x267 + x35; +Tbase TZ x269 = x268 - x40; +Tbase TZ x270 = 0xffffffffffffe; +Tbase TZ x271 = x270 + x36; +Tbase TZ x272 = x271 - x41; +Tbase TZ x273 = 0xffffffffffffe; +Tbase TZ x274 = x273 + x37; +Tbase TZ x275 = x274 - x42; +Tbase TZ x276 = 0xfffffffffffda; +Tbase TZ x277 = x276 + x38; +Tbase TZ x278 = x277 - x43; +Tbase TZ x279 = x278 * x48; +Tbase TZ x280 = x266 * x47; +Tbase TZ x281 = x269 * x46; +Tbase TZ x282 = x272 * x45; +Tbase TZ x283 = x275 * x44; +Tbase TZ x284 = x282 + x283; +Tbase TZ x285 = x281 + x284; +Tbase TZ x286 = x280 + x285; +Tbase TZ x287 = 0x13; +Tbase TZ x288 = x287 * x286; +Tbase TZ x289 = x279 + x288; +Tbase TZ x290 = 0x33; +Tbase TZ x291 = x289 >> x290; +Tbase TZ x292 = x275 * x48; +Tbase TZ x293 = x278 * x47; +Tbase TZ x294 = x292 + x293; +Tbase TZ x295 = x266 * x46; +Tbase TZ x296 = x269 * x45; +Tbase TZ x297 = x272 * x44; +Tbase TZ x298 = x296 + x297; +Tbase TZ x299 = x295 + x298; +Tbase TZ x300 = 0x13; +Tbase TZ x301 = x300 * x299; +Tbase TZ x302 = x294 + x301; +Tbase TZ x303 = x291 + x302; +Tbase TZ x304 = 0x33; +Tbase TZ x305 = x303 >> x304; +Tbase TZ x306 = x272 * x48; +Tbase TZ x307 = x275 * x47; +Tbase TZ x308 = x278 * x46; +Tbase TZ x309 = x307 + x308; +Tbase TZ x310 = x306 + x309; +Tbase TZ x311 = x266 * x45; +Tbase TZ x312 = x269 * x44; +Tbase TZ x313 = x311 + x312; +Tbase TZ x314 = 0x13; +Tbase TZ x315 = x314 * x313; +Tbase TZ x316 = x310 + x315; +Tbase TZ x317 = x305 + x316; +Tbase TZ x318 = 0x33; +Tbase TZ x319 = x317 >> x318; +Tbase TZ x320 = x269 * x48; +Tbase TZ x321 = x272 * x47; +Tbase TZ x322 = x275 * x46; +Tbase TZ x323 = x278 * x45; +Tbase TZ x324 = x322 + x323; +Tbase TZ x325 = x321 + x324; +Tbase TZ x326 = x320 + x325; +Tbase TZ x327 = x266 * x44; +Tbase TZ x328 = 0x13; +Tbase TZ x329 = x328 * x327; +Tbase TZ x330 = x326 + x329; +Tbase TZ x331 = x319 + x330; +Tbase TZ x332 = 0x33; +Tbase TZ x333 = x331 >> x332; +Tbase TZ x334 = x266 * x48; +Tbase TZ x335 = x269 * x47; +Tbase TZ x336 = x272 * x46; +Tbase TZ x337 = x275 * x45; +Tbase TZ x338 = x278 * x44; +Tbase TZ x339 = x337 + x338; +Tbase TZ x340 = x336 + x339; +Tbase TZ x341 = x335 + x340; +Tbase TZ x342 = x334 + x341; +Tbase TZ x343 = x333 + x342; +Tbase TZ x344 = 0x33; +Tbase TZ x345 = x343 >> x344; +Tbase TZ x346 = 0x13; +Tbase TZ x347 = x346 * x345; +Tbase TZ x348 = 0x7ffffffffffff; +Tbase TZ x349 = x289 & x348; +Tbase TZ x350 = x347 + x349; +Tbase TZ x351 = 0x33; +Tbase TZ x352 = x350 >> x351; +Tbase TZ x353 = 0x7ffffffffffff; +Tbase TZ x354 = x303 & x353; +Tbase TZ x355 = x352 + x354; +Tbase TZ x356 = 0x7ffffffffffff; +Tbase TZ x357 = x343 & x356; +Tbase TZ x358 = 0x7ffffffffffff; +Tbase TZ x359 = x331 & x358; +Tbase TZ x360 = 0x33; +Tbase TZ x361 = x355 >> x360; +Tbase TZ x362 = 0x7ffffffffffff; +Tbase TZ x363 = x317 & x362; +Tbase TZ x364 = x361 + x363; +Tbase TZ x365 = 0x7ffffffffffff; +Tbase TZ x366 = x355 & x365; +Tbase TZ x367 = 0x7ffffffffffff; +Tbase TZ x368 = x350 & x367; +Tbase TZ x369 = x263 * x153; +Tbase TZ x370 = x259 * x150; +Tbase TZ x371 = x260 * x147; +Tbase TZ x372 = x261 * x144; +Tbase TZ x373 = x262 * x141; +Tbase TZ x374 = x372 + x373; +Tbase TZ x375 = x371 + x374; +Tbase TZ x376 = x370 + x375; +Tbase TZ x377 = 0x13; +Tbase TZ x378 = x377 * x376; +Tbase TZ x379 = x369 + x378; +Tbase TZ x380 = 0x33; +Tbase TZ x381 = x379 >> x380; +Tbase TZ x382 = x262 * x153; +Tbase TZ x383 = x263 * x150; +Tbase TZ x384 = x382 + x383; +Tbase TZ x385 = x259 * x147; +Tbase TZ x386 = x260 * x144; +Tbase TZ x387 = x261 * x141; +Tbase TZ x388 = x386 + x387; +Tbase TZ x389 = x385 + x388; +Tbase TZ x390 = 0x13; +Tbase TZ x391 = x390 * x389; +Tbase TZ x392 = x384 + x391; +Tbase TZ x393 = x381 + x392; +Tbase TZ x394 = 0x33; +Tbase TZ x395 = x393 >> x394; +Tbase TZ x396 = x261 * x153; +Tbase TZ x397 = x262 * x150; +Tbase TZ x398 = x263 * x147; +Tbase TZ x399 = x397 + x398; +Tbase TZ x400 = x396 + x399; +Tbase TZ x401 = x259 * x144; +Tbase TZ x402 = x260 * x141; +Tbase TZ x403 = x401 + x402; +Tbase TZ x404 = 0x13; +Tbase TZ x405 = x404 * x403; +Tbase TZ x406 = x400 + x405; +Tbase TZ x407 = x395 + x406; +Tbase TZ x408 = 0x33; +Tbase TZ x409 = x407 >> x408; +Tbase TZ x410 = x260 * x153; +Tbase TZ x411 = x261 * x150; +Tbase TZ x412 = x262 * x147; +Tbase TZ x413 = x263 * x144; +Tbase TZ x414 = x412 + x413; +Tbase TZ x415 = x411 + x414; +Tbase TZ x416 = x410 + x415; +Tbase TZ x417 = x259 * x141; +Tbase TZ x418 = 0x13; +Tbase TZ x419 = x418 * x417; +Tbase TZ x420 = x416 + x419; +Tbase TZ x421 = x409 + x420; +Tbase TZ x422 = 0x33; +Tbase TZ x423 = x421 >> x422; +Tbase TZ x424 = x259 * x153; +Tbase TZ x425 = x260 * x150; +Tbase TZ x426 = x261 * x147; +Tbase TZ x427 = x262 * x144; +Tbase TZ x428 = x263 * x141; +Tbase TZ x429 = x427 + x428; +Tbase TZ x430 = x426 + x429; +Tbase TZ x431 = x425 + x430; +Tbase TZ x432 = x424 + x431; +Tbase TZ x433 = x423 + x432; +Tbase TZ x434 = 0x33; +Tbase TZ x435 = x433 >> x434; +Tbase TZ x436 = 0x13; +Tbase TZ x437 = x436 * x435; +Tbase TZ x438 = 0x7ffffffffffff; +Tbase TZ x439 = x379 & x438; +Tbase TZ x440 = x437 + x439; +Tbase TZ x441 = 0x33; +Tbase TZ x442 = x440 >> x441; +Tbase TZ x443 = 0x7ffffffffffff; +Tbase TZ x444 = x393 & x443; +Tbase TZ x445 = x442 + x444; +Tbase TZ x446 = 0x7ffffffffffff; +Tbase TZ x447 = x433 & x446; +Tbase TZ x448 = 0x7ffffffffffff; +Tbase TZ x449 = x421 & x448; +Tbase TZ x450 = 0x33; +Tbase TZ x451 = x445 >> x450; +Tbase TZ x452 = 0x7ffffffffffff; +Tbase TZ x453 = x407 & x452; +Tbase TZ x454 = x451 + x453; +Tbase TZ x455 = 0x7ffffffffffff; +Tbase TZ x456 = x445 & x455; +Tbase TZ x457 = 0x7ffffffffffff; +Tbase TZ x458 = x440 & x457; +Tbase TZ x459 = x357 + x447; +Tbase TZ x460 = x359 + x449; +Tbase TZ x461 = x364 + x454; +Tbase TZ x462 = x366 + x456; +Tbase TZ x463 = x368 + x458; +Tbase TZ x464 = x357 + x447; +Tbase TZ x465 = x359 + x449; +Tbase TZ x466 = x364 + x454; +Tbase TZ x467 = x366 + x456; +Tbase TZ x468 = x368 + x458; +Tbase TZ x469 = x463 * x468; +Tbase TZ x470 = x459 * x467; +Tbase TZ x471 = x460 * x466; +Tbase TZ x472 = x461 * x465; +Tbase TZ x473 = x462 * x464; +Tbase TZ x474 = x472 + x473; +Tbase TZ x475 = x471 + x474; +Tbase TZ x476 = x470 + x475; +Tbase TZ x477 = 0x13; +Tbase TZ x478 = x477 * x476; +Tbase TZ x479 = x469 + x478; +Tbase TZ x480 = 0x33; +Tbase TZ x481 = x479 >> x480; +Tbase TZ x482 = x462 * x468; +Tbase TZ x483 = x463 * x467; +Tbase TZ x484 = x482 + x483; +Tbase TZ x485 = x459 * x466; +Tbase TZ x486 = x460 * x465; +Tbase TZ x487 = x461 * x464; +Tbase TZ x488 = x486 + x487; +Tbase TZ x489 = x485 + x488; +Tbase TZ x490 = 0x13; +Tbase TZ x491 = x490 * x489; +Tbase TZ x492 = x484 + x491; +Tbase TZ x493 = x481 + x492; +Tbase TZ x494 = 0x33; +Tbase TZ x495 = x493 >> x494; +Tbase TZ x496 = x461 * x468; +Tbase TZ x497 = x462 * x467; +Tbase TZ x498 = x463 * x466; +Tbase TZ x499 = x497 + x498; +Tbase TZ x500 = x496 + x499; +Tbase TZ x501 = x459 * x465; +Tbase TZ x502 = x460 * x464; +Tbase TZ x503 = x501 + x502; +Tbase TZ x504 = 0x13; +Tbase TZ x505 = x504 * x503; +Tbase TZ x506 = x500 + x505; +Tbase TZ x507 = x495 + x506; +Tbase TZ x508 = 0x33; +Tbase TZ x509 = x507 >> x508; +Tbase TZ x510 = x460 * x468; +Tbase TZ x511 = x461 * x467; +Tbase TZ x512 = x462 * x466; +Tbase TZ x513 = x463 * x465; +Tbase TZ x514 = x512 + x513; +Tbase TZ x515 = x511 + x514; +Tbase TZ x516 = x510 + x515; +Tbase TZ x517 = x459 * x464; +Tbase TZ x518 = 0x13; +Tbase TZ x519 = x518 * x517; +Tbase TZ x520 = x516 + x519; +Tbase TZ x521 = x509 + x520; +Tbase TZ x522 = 0x33; +Tbase TZ x523 = x521 >> x522; +Tbase TZ x524 = x459 * x468; +Tbase TZ x525 = x460 * x467; +Tbase TZ x526 = x461 * x466; +Tbase TZ x527 = x462 * x465; +Tbase TZ x528 = x463 * x464; +Tbase TZ x529 = x527 + x528; +Tbase TZ x530 = x526 + x529; +Tbase TZ x531 = x525 + x530; +Tbase TZ x532 = x524 + x531; +Tbase TZ x533 = x523 + x532; +Tbase TZ x534 = 0x33; +Tbase TZ x535 = x533 >> x534; +Tbase TZ x536 = 0x13; +Tbase TZ x537 = x536 * x535; +Tbase TZ x538 = 0x7ffffffffffff; +Tbase TZ x539 = x479 & x538; +Tbase TZ x540 = x537 + x539; +Tbase TZ x541 = 0x33; +Tbase TZ x542 = x540 >> x541; +Tbase TZ x543 = 0x7ffffffffffff; +Tbase TZ x544 = x493 & x543; +Tbase TZ x545 = x542 + x544; +Tbase TZ x546 = 0x7ffffffffffff; +Tbase TZ x547 = x533 & x546; +Tbase TZ x548 = 0x7ffffffffffff; +Tbase TZ x549 = x521 & x548; +Tbase TZ x550 = 0x33; +Tbase TZ x551 = x545 >> x550; +Tbase TZ x552 = 0x7ffffffffffff; +Tbase TZ x553 = x507 & x552; +Tbase TZ x554 = x551 + x553; +Tbase TZ x555 = 0x7ffffffffffff; +Tbase TZ x556 = x545 & x555; +Tbase TZ x557 = 0x7ffffffffffff; +Tbase TZ x558 = x540 & x557; +Tbase TZ x559 = 0xffffffffffffe; +Tbase TZ x560 = x559 + x357; +Tbase TZ x561 = x560 - x447; +Tbase TZ x562 = 0xffffffffffffe; +Tbase TZ x563 = x562 + x359; +Tbase TZ x564 = x563 - x449; +Tbase TZ x565 = 0xffffffffffffe; +Tbase TZ x566 = x565 + x364; +Tbase TZ x567 = x566 - x454; +Tbase TZ x568 = 0xffffffffffffe; +Tbase TZ x569 = x568 + x366; +Tbase TZ x570 = x569 - x456; +Tbase TZ x571 = 0xfffffffffffda; +Tbase TZ x572 = x571 + x368; +Tbase TZ x573 = x572 - x458; +Tbase TZ x574 = 0xffffffffffffe; +Tbase TZ x575 = x574 + x357; +Tbase TZ x576 = x575 - x447; +Tbase TZ x577 = 0xffffffffffffe; +Tbase TZ x578 = x577 + x359; +Tbase TZ x579 = x578 - x449; +Tbase TZ x580 = 0xffffffffffffe; +Tbase TZ x581 = x580 + x364; +Tbase TZ x582 = x581 - x454; +Tbase TZ x583 = 0xffffffffffffe; +Tbase TZ x584 = x583 + x366; +Tbase TZ x585 = x584 - x456; +Tbase TZ x586 = 0xfffffffffffda; +Tbase TZ x587 = x586 + x368; +Tbase TZ x588 = x587 - x458; +Tbase TZ x589 = x573 * x588; +Tbase TZ x590 = x561 * x585; +Tbase TZ x591 = x564 * x582; +Tbase TZ x592 = x567 * x579; +Tbase TZ x593 = x570 * x576; +Tbase TZ x594 = x592 + x593; +Tbase TZ x595 = x591 + x594; +Tbase TZ x596 = x590 + x595; +Tbase TZ x597 = 0x13; +Tbase TZ x598 = x597 * x596; +Tbase TZ x599 = x589 + x598; +Tbase TZ x600 = 0x33; +Tbase TZ x601 = x599 >> x600; +Tbase TZ x602 = x570 * x588; +Tbase TZ x603 = x573 * x585; +Tbase TZ x604 = x602 + x603; +Tbase TZ x605 = x561 * x582; +Tbase TZ x606 = x564 * x579; +Tbase TZ x607 = x567 * x576; +Tbase TZ x608 = x606 + x607; +Tbase TZ x609 = x605 + x608; +Tbase TZ x610 = 0x13; +Tbase TZ x611 = x610 * x609; +Tbase TZ x612 = x604 + x611; +Tbase TZ x613 = x601 + x612; +Tbase TZ x614 = 0x33; +Tbase TZ x615 = x613 >> x614; +Tbase TZ x616 = x567 * x588; +Tbase TZ x617 = x570 * x585; +Tbase TZ x618 = x573 * x582; +Tbase TZ x619 = x617 + x618; +Tbase TZ x620 = x616 + x619; +Tbase TZ x621 = x561 * x579; +Tbase TZ x622 = x564 * x576; +Tbase TZ x623 = x621 + x622; +Tbase TZ x624 = 0x13; +Tbase TZ x625 = x624 * x623; +Tbase TZ x626 = x620 + x625; +Tbase TZ x627 = x615 + x626; +Tbase TZ x628 = 0x33; +Tbase TZ x629 = x627 >> x628; +Tbase TZ x630 = x564 * x588; +Tbase TZ x631 = x567 * x585; +Tbase TZ x632 = x570 * x582; +Tbase TZ x633 = x573 * x579; +Tbase TZ x634 = x632 + x633; +Tbase TZ x635 = x631 + x634; +Tbase TZ x636 = x630 + x635; +Tbase TZ x637 = x561 * x576; +Tbase TZ x638 = 0x13; +Tbase TZ x639 = x638 * x637; +Tbase TZ x640 = x636 + x639; +Tbase TZ x641 = x629 + x640; +Tbase TZ x642 = 0x33; +Tbase TZ x643 = x641 >> x642; +Tbase TZ x644 = x561 * x588; +Tbase TZ x645 = x564 * x585; +Tbase TZ x646 = x567 * x582; +Tbase TZ x647 = x570 * x579; +Tbase TZ x648 = x573 * x576; +Tbase TZ x649 = x647 + x648; +Tbase TZ x650 = x646 + x649; +Tbase TZ x651 = x645 + x650; +Tbase TZ x652 = x644 + x651; +Tbase TZ x653 = x643 + x652; +Tbase TZ x654 = 0x33; +Tbase TZ x655 = x653 >> x654; +Tbase TZ x656 = 0x13; +Tbase TZ x657 = x656 * x655; +Tbase TZ x658 = 0x7ffffffffffff; +Tbase TZ x659 = x599 & x658; +Tbase TZ x660 = x657 + x659; +Tbase TZ x661 = 0x33; +Tbase TZ x662 = x660 >> x661; +Tbase TZ x663 = 0x7ffffffffffff; +Tbase TZ x664 = x613 & x663; +Tbase TZ x665 = x662 + x664; +Tbase TZ x666 = 0x7ffffffffffff; +Tbase TZ x667 = x653 & x666; +Tbase TZ x668 = 0x7ffffffffffff; +Tbase TZ x669 = x641 & x668; +Tbase TZ x670 = 0x33; +Tbase TZ x671 = x665 >> x670; +Tbase TZ x672 = 0x7ffffffffffff; +Tbase TZ x673 = x627 & x672; +Tbase TZ x674 = x671 + x673; +Tbase TZ x675 = 0x7ffffffffffff; +Tbase TZ x676 = x665 & x675; +Tbase TZ x677 = 0x7ffffffffffff; +Tbase TZ x678 = x660 & x677; +Tbase TZ x679 = x23 * x678; +Tbase TZ x680 = x19 * x676; +Tbase TZ x681 = x20 * x674; +Tbase TZ x682 = x21 * x669; +Tbase TZ x683 = x22 * x667; +Tbase TZ x684 = x682 + x683; +Tbase TZ x685 = x681 + x684; +Tbase TZ x686 = x680 + x685; +Tbase TZ x687 = 0x13; +Tbase TZ x688 = x687 * x686; +Tbase TZ x689 = x679 + x688; +Tbase TZ x690 = 0x33; +Tbase TZ x691 = x689 >> x690; +Tbase TZ x692 = x22 * x678; +Tbase TZ x693 = x23 * x676; +Tbase TZ x694 = x692 + x693; +Tbase TZ x695 = x19 * x674; +Tbase TZ x696 = x20 * x669; +Tbase TZ x697 = x21 * x667; +Tbase TZ x698 = x696 + x697; +Tbase TZ x699 = x695 + x698; +Tbase TZ x700 = 0x13; +Tbase TZ x701 = x700 * x699; +Tbase TZ x702 = x694 + x701; +Tbase TZ x703 = x691 + x702; +Tbase TZ x704 = 0x33; +Tbase TZ x705 = x703 >> x704; +Tbase TZ x706 = x21 * x678; +Tbase TZ x707 = x22 * x676; +Tbase TZ x708 = x23 * x674; +Tbase TZ x709 = x707 + x708; +Tbase TZ x710 = x706 + x709; +Tbase TZ x711 = x19 * x669; +Tbase TZ x712 = x20 * x667; +Tbase TZ x713 = x711 + x712; +Tbase TZ x714 = 0x13; +Tbase TZ x715 = x714 * x713; +Tbase TZ x716 = x710 + x715; +Tbase TZ x717 = x705 + x716; +Tbase TZ x718 = 0x33; +Tbase TZ x719 = x717 >> x718; +Tbase TZ x720 = x20 * x678; +Tbase TZ x721 = x21 * x676; +Tbase TZ x722 = x22 * x674; +Tbase TZ x723 = x23 * x669; +Tbase TZ x724 = x722 + x723; +Tbase TZ x725 = x721 + x724; +Tbase TZ x726 = x720 + x725; +Tbase TZ x727 = x19 * x667; +Tbase TZ x728 = 0x13; +Tbase TZ x729 = x728 * x727; +Tbase TZ x730 = x726 + x729; +Tbase TZ x731 = x719 + x730; +Tbase TZ x732 = 0x33; +Tbase TZ x733 = x731 >> x732; +Tbase TZ x734 = x19 * x678; +Tbase TZ x735 = x20 * x676; +Tbase TZ x736 = x21 * x674; +Tbase TZ x737 = x22 * x669; +Tbase TZ x738 = x23 * x667; +Tbase TZ x739 = x737 + x738; +Tbase TZ x740 = x736 + x739; +Tbase TZ x741 = x735 + x740; +Tbase TZ x742 = x734 + x741; +Tbase TZ x743 = x733 + x742; +Tbase TZ x744 = 0x33; +Tbase TZ x745 = x743 >> x744; +Tbase TZ x746 = 0x13; +Tbase TZ x747 = x746 * x745; +Tbase TZ x748 = 0x7ffffffffffff; +Tbase TZ x749 = x689 & x748; +Tbase TZ x750 = x747 + x749; +Tbase TZ x751 = 0x33; +Tbase TZ x752 = x750 >> x751; +Tbase TZ x753 = 0x7ffffffffffff; +Tbase TZ x754 = x703 & x753; +Tbase TZ x755 = x752 + x754; +Tbase TZ x756 = 0x7ffffffffffff; +Tbase TZ x757 = x743 & x756; +Tbase TZ x758 = 0x7ffffffffffff; +Tbase TZ x759 = x731 & x758; +Tbase TZ x760 = 0x33; +Tbase TZ x761 = x755 >> x760; +Tbase TZ x762 = 0x7ffffffffffff; +Tbase TZ x763 = x717 & x762; +Tbase TZ x764 = x761 + x763; +Tbase TZ x765 = 0x7ffffffffffff; +Tbase TZ x766 = x755 & x765; +Tbase TZ x767 = 0x7ffffffffffff; +Tbase TZ x768 = x750 & x767; +Tbase TZ x769 = x138 * x243; +Tbase TZ x770 = x127 * x241; +Tbase TZ x771 = x129 * x239; +Tbase TZ x772 = x134 * x234; +Tbase TZ x773 = x136 * x232; +Tbase TZ x774 = x772 + x773; +Tbase TZ x775 = x771 + x774; +Tbase TZ x776 = x770 + x775; +Tbase TZ x777 = 0x13; +Tbase TZ x778 = x777 * x776; +Tbase TZ x779 = x769 + x778; +Tbase TZ x780 = 0x33; +Tbase TZ x781 = x779 >> x780; +Tbase TZ x782 = x136 * x243; +Tbase TZ x783 = x138 * x241; +Tbase TZ x784 = x782 + x783; +Tbase TZ x785 = x127 * x239; +Tbase TZ x786 = x129 * x234; +Tbase TZ x787 = x134 * x232; +Tbase TZ x788 = x786 + x787; +Tbase TZ x789 = x785 + x788; +Tbase TZ x790 = 0x13; +Tbase TZ x791 = x790 * x789; +Tbase TZ x792 = x784 + x791; +Tbase TZ x793 = x781 + x792; +Tbase TZ x794 = 0x33; +Tbase TZ x795 = x793 >> x794; +Tbase TZ x796 = x134 * x243; +Tbase TZ x797 = x136 * x241; +Tbase TZ x798 = x138 * x239; +Tbase TZ x799 = x797 + x798; +Tbase TZ x800 = x796 + x799; +Tbase TZ x801 = x127 * x234; +Tbase TZ x802 = x129 * x232; +Tbase TZ x803 = x801 + x802; +Tbase TZ x804 = 0x13; +Tbase TZ x805 = x804 * x803; +Tbase TZ x806 = x800 + x805; +Tbase TZ x807 = x795 + x806; +Tbase TZ x808 = 0x33; +Tbase TZ x809 = x807 >> x808; +Tbase TZ x810 = x129 * x243; +Tbase TZ x811 = x134 * x241; +Tbase TZ x812 = x136 * x239; +Tbase TZ x813 = x138 * x234; +Tbase TZ x814 = x812 + x813; +Tbase TZ x815 = x811 + x814; +Tbase TZ x816 = x810 + x815; +Tbase TZ x817 = x127 * x232; +Tbase TZ x818 = 0x13; +Tbase TZ x819 = x818 * x817; +Tbase TZ x820 = x816 + x819; +Tbase TZ x821 = x809 + x820; +Tbase TZ x822 = 0x33; +Tbase TZ x823 = x821 >> x822; +Tbase TZ x824 = x127 * x243; +Tbase TZ x825 = x129 * x241; +Tbase TZ x826 = x134 * x239; +Tbase TZ x827 = x136 * x234; +Tbase TZ x828 = x138 * x232; +Tbase TZ x829 = x827 + x828; +Tbase TZ x830 = x826 + x829; +Tbase TZ x831 = x825 + x830; +Tbase TZ x832 = x824 + x831; +Tbase TZ x833 = x823 + x832; +Tbase TZ x834 = 0x33; +Tbase TZ x835 = x833 >> x834; +Tbase TZ x836 = 0x13; +Tbase TZ x837 = x836 * x835; +Tbase TZ x838 = 0x7ffffffffffff; +Tbase TZ x839 = x779 & x838; +Tbase TZ x840 = x837 + x839; +Tbase TZ x841 = 0x33; +Tbase TZ x842 = x840 >> x841; +Tbase TZ x843 = 0x7ffffffffffff; +Tbase TZ x844 = x793 & x843; +Tbase TZ x845 = x842 + x844; +Tbase TZ x846 = 0x7ffffffffffff; +Tbase TZ x847 = x833 & x846; +Tbase TZ x848 = 0x7ffffffffffff; +Tbase TZ x849 = x821 & x848; +Tbase TZ x850 = 0x33; +Tbase TZ x851 = x845 >> x850; +Tbase TZ x852 = 0x7ffffffffffff; +Tbase TZ x853 = x807 & x852; +Tbase TZ x854 = x851 + x853; +Tbase TZ x855 = 0x7ffffffffffff; +Tbase TZ x856 = x845 & x855; +Tbase TZ x857 = 0x7ffffffffffff; +Tbase TZ x858 = x840 & x857; +Tbase TZ x859 = x18 * x258; +Tbase TZ x860 = x14 * x255; +Tbase TZ x861 = x15 * x252; +Tbase TZ x862 = x16 * x249; +Tbase TZ x863 = x17 * x246; +Tbase TZ x864 = x862 + x863; +Tbase TZ x865 = x861 + x864; +Tbase TZ x866 = x860 + x865; +Tbase TZ x867 = 0x13; +Tbase TZ x868 = x867 * x866; +Tbase TZ x869 = x859 + x868; +Tbase TZ x870 = 0x33; +Tbase TZ x871 = x869 >> x870; +Tbase TZ x872 = x17 * x258; +Tbase TZ x873 = x18 * x255; +Tbase TZ x874 = x872 + x873; +Tbase TZ x875 = x14 * x252; +Tbase TZ x876 = x15 * x249; +Tbase TZ x877 = x16 * x246; +Tbase TZ x878 = x876 + x877; +Tbase TZ x879 = x875 + x878; +Tbase TZ x880 = 0x13; +Tbase TZ x881 = x880 * x879; +Tbase TZ x882 = x874 + x881; +Tbase TZ x883 = x871 + x882; +Tbase TZ x884 = 0x33; +Tbase TZ x885 = x883 >> x884; +Tbase TZ x886 = x16 * x258; +Tbase TZ x887 = x17 * x255; +Tbase TZ x888 = x18 * x252; +Tbase TZ x889 = x887 + x888; +Tbase TZ x890 = x886 + x889; +Tbase TZ x891 = x14 * x249; +Tbase TZ x892 = x15 * x246; +Tbase TZ x893 = x891 + x892; +Tbase TZ x894 = 0x13; +Tbase TZ x895 = x894 * x893; +Tbase TZ x896 = x890 + x895; +Tbase TZ x897 = x885 + x896; +Tbase TZ x898 = 0x33; +Tbase TZ x899 = x897 >> x898; +Tbase TZ x900 = x15 * x258; +Tbase TZ x901 = x16 * x255; +Tbase TZ x902 = x17 * x252; +Tbase TZ x903 = x18 * x249; +Tbase TZ x904 = x902 + x903; +Tbase TZ x905 = x901 + x904; +Tbase TZ x906 = x900 + x905; +Tbase TZ x907 = x14 * x246; +Tbase TZ x908 = 0x13; +Tbase TZ x909 = x908 * x907; +Tbase TZ x910 = x906 + x909; +Tbase TZ x911 = x899 + x910; +Tbase TZ x912 = 0x33; +Tbase TZ x913 = x911 >> x912; +Tbase TZ x914 = x14 * x258; +Tbase TZ x915 = x15 * x255; +Tbase TZ x916 = x16 * x252; +Tbase TZ x917 = x17 * x249; +Tbase TZ x918 = x18 * x246; +Tbase TZ x919 = x917 + x918; +Tbase TZ x920 = x916 + x919; +Tbase TZ x921 = x915 + x920; +Tbase TZ x922 = x914 + x921; +Tbase TZ x923 = x913 + x922; +Tbase TZ x924 = 0x33; +Tbase TZ x925 = x923 >> x924; +Tbase TZ x926 = 0x13; +Tbase TZ x927 = x926 * x925; +Tbase TZ x928 = 0x7ffffffffffff; +Tbase TZ x929 = x869 & x928; +Tbase TZ x930 = x927 + x929; +Tbase TZ x931 = 0x33; +Tbase TZ x932 = x930 >> x931; +Tbase TZ x933 = 0x7ffffffffffff; +Tbase TZ x934 = x883 & x933; +Tbase TZ x935 = x932 + x934; +Tbase TZ x936 = 0x7ffffffffffff; +Tbase TZ x937 = x923 & x936; +Tbase TZ x938 = 0x7ffffffffffff; +Tbase TZ x939 = x911 & x938; +Tbase TZ x940 = 0x33; +Tbase TZ x941 = x935 >> x940; +Tbase TZ x942 = 0x7ffffffffffff; +Tbase TZ x943 = x897 & x942; +Tbase TZ x944 = x941 + x943; +Tbase TZ x945 = 0x7ffffffffffff; +Tbase TZ x946 = x935 & x945; +Tbase TZ x947 = 0x7ffffffffffff; +Tbase TZ x948 = x930 & x947; +Tbase TZ x949 = x127 + x937; +Tbase TZ x950 = x129 + x939; +Tbase TZ x951 = x134 + x944; +Tbase TZ x952 = x136 + x946; +Tbase TZ x953 = x138 + x948; +Tbase TZ x954 = x258 * x953; +Tbase TZ x955 = x246 * x952; +Tbase TZ x956 = x249 * x951; +Tbase TZ x957 = x252 * x950; +Tbase TZ x958 = x255 * x949; +Tbase TZ x959 = x957 + x958; +Tbase TZ x960 = x956 + x959; +Tbase TZ x961 = x955 + x960; +Tbase TZ x962 = 0x13; +Tbase TZ x963 = x962 * x961; +Tbase TZ x964 = x954 + x963; +Tbase TZ x965 = 0x33; +Tbase TZ x966 = x964 >> x965; +Tbase TZ x967 = x255 * x953; +Tbase TZ x968 = x258 * x952; +Tbase TZ x969 = x967 + x968; +Tbase TZ x970 = x246 * x951; +Tbase TZ x971 = x249 * x950; +Tbase TZ x972 = x252 * x949; +Tbase TZ x973 = x971 + x972; +Tbase TZ x974 = x970 + x973; +Tbase TZ x975 = 0x13; +Tbase TZ x976 = x975 * x974; +Tbase TZ x977 = x969 + x976; +Tbase TZ x978 = x966 + x977; +Tbase TZ x979 = 0x33; +Tbase TZ x980 = x978 >> x979; +Tbase TZ x981 = x252 * x953; +Tbase TZ x982 = x255 * x952; +Tbase TZ x983 = x258 * x951; +Tbase TZ x984 = x982 + x983; +Tbase TZ x985 = x981 + x984; +Tbase TZ x986 = x246 * x950; +Tbase TZ x987 = x249 * x949; +Tbase TZ x988 = x986 + x987; +Tbase TZ x989 = 0x13; +Tbase TZ x990 = x989 * x988; +Tbase TZ x991 = x985 + x990; +Tbase TZ x992 = x980 + x991; +Tbase TZ x993 = 0x33; +Tbase TZ x994 = x992 >> x993; +Tbase TZ x995 = x249 * x953; +Tbase TZ x996 = x252 * x952; +Tbase TZ x997 = x255 * x951; +Tbase TZ x998 = x258 * x950; +Tbase TZ x999 = x997 + x998; +Tbase TZ x1000 = x996 + x999; +Tbase TZ x1001 = x995 + x1000; +Tbase TZ x1002 = x246 * x949; +Tbase TZ x1003 = 0x13; +Tbase TZ x1004 = x1003 * x1002; +Tbase TZ x1005 = x1001 + x1004; +Tbase TZ x1006 = x994 + x1005; +Tbase TZ x1007 = 0x33; +Tbase TZ x1008 = x1006 >> x1007; +Tbase TZ x1009 = x246 * x953; +Tbase TZ x1010 = x249 * x952; +Tbase TZ x1011 = x252 * x951; +Tbase TZ x1012 = x255 * x950; +Tbase TZ x1013 = x258 * x949; +Tbase TZ x1014 = x1012 + x1013; +Tbase TZ x1015 = x1011 + x1014; +Tbase TZ x1016 = x1010 + x1015; +Tbase TZ x1017 = x1009 + x1016; +Tbase TZ x1018 = x1008 + x1017; +Tbase TZ x1019 = 0x33; +Tbase TZ x1020 = x1018 >> x1019; +Tbase TZ x1021 = 0x13; +Tbase TZ x1022 = x1021 * x1020; +Tbase TZ x1023 = 0x7ffffffffffff; +Tbase TZ x1024 = x964 & x1023; +Tbase TZ x1025 = x1022 + x1024; +Tbase TZ x1026 = 0x33; +Tbase TZ x1027 = x1025 >> x1026; +Tbase TZ x1028 = 0x7ffffffffffff; +Tbase TZ x1029 = x978 & x1028; +Tbase TZ x1030 = x1027 + x1029; +Tbase TZ x1031 = 0x7ffffffffffff; +Tbase TZ x1032 = x1018 & x1031; +Tbase TZ x1033 = 0x7ffffffffffff; +Tbase TZ x1034 = x1006 & x1033; +Tbase TZ x1035 = 0x33; +Tbase TZ x1036 = x1030 >> x1035; +Tbase TZ x1037 = 0x7ffffffffffff; +Tbase TZ x1038 = x992 & x1037; +Tbase TZ x1039 = x1036 + x1038; +Tbase TZ x1040 = 0x7ffffffffffff; +Tbase TZ x1041 = x1030 & x1040; +Tbase TZ x1042 = 0x7ffffffffffff; +Tbase TZ x1043 = x1025 & x1042; +(Return x847, Return x849, Return x854, Return x856, +Return x858, +(Return x1032, Return x1034, Return x1039, Return x1041, Return x1043), +(Return x547, Return x549, Return x554, Return x556, Return x558), +(Return x757, Return x759, Return x764, Return x766, Return x768)) + : forall var : base_type -> Type, + expr base_type op + (TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> ...) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepJavaDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepJavaDisplay.log new file mode 100644 index 000000000..86c86f426 --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStepJavaDisplay.log @@ -0,0 +1,1050 @@ +rladderstepW = +fun var : base_type -> Type => +λ +_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 + x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 + x43 : var TZ, +Tbase TZ x44 = x24 + x29; +Tbase TZ x45 = x25 + x30; +Tbase TZ x46 = x26 + x31; +Tbase TZ x47 = x27 + x32; +Tbase TZ x48 = x28 + x33; +Tbase TZ x49 = x48 * x48; +Tbase TZ x50 = x44 * x47; +Tbase TZ x51 = x45 * x46; +Tbase TZ x52 = x46 * x45; +Tbase TZ x53 = x47 * x44; +Tbase TZ x54 = x52 + x53; +Tbase TZ x55 = x51 + x54; +Tbase TZ x56 = x50 + x55; +Tbase TZ x57 = 0x13; +Tbase TZ x58 = x57 * x56; +Tbase TZ x59 = x49 + x58; +Tbase TZ x60 = 0x33; +Tbase TZ x61 = x59 >>> x60; +Tbase TZ x62 = x47 * x48; +Tbase TZ x63 = x48 * x47; +Tbase TZ x64 = x62 + x63; +Tbase TZ x65 = x44 * x46; +Tbase TZ x66 = x45 * x45; +Tbase TZ x67 = x46 * x44; +Tbase TZ x68 = x66 + x67; +Tbase TZ x69 = x65 + x68; +Tbase TZ x70 = 0x13; +Tbase TZ x71 = x70 * x69; +Tbase TZ x72 = x64 + x71; +Tbase TZ x73 = x61 + x72; +Tbase TZ x74 = 0x33; +Tbase TZ x75 = x73 >>> x74; +Tbase TZ x76 = x46 * x48; +Tbase TZ x77 = x47 * x47; +Tbase TZ x78 = x48 * x46; +Tbase TZ x79 = x77 + x78; +Tbase TZ x80 = x76 + x79; +Tbase TZ x81 = x44 * x45; +Tbase TZ x82 = x45 * x44; +Tbase TZ x83 = x81 + x82; +Tbase TZ x84 = 0x13; +Tbase TZ x85 = x84 * x83; +Tbase TZ x86 = x80 + x85; +Tbase TZ x87 = x75 + x86; +Tbase TZ x88 = 0x33; +Tbase TZ x89 = x87 >>> x88; +Tbase TZ x90 = x45 * x48; +Tbase TZ x91 = x46 * x47; +Tbase TZ x92 = x47 * x46; +Tbase TZ x93 = x48 * x45; +Tbase TZ x94 = x92 + x93; +Tbase TZ x95 = x91 + x94; +Tbase TZ x96 = x90 + x95; +Tbase TZ x97 = x44 * x44; +Tbase TZ x98 = 0x13; +Tbase TZ x99 = x98 * x97; +Tbase TZ x100 = x96 + x99; +Tbase TZ x101 = x89 + x100; +Tbase TZ x102 = 0x33; +Tbase TZ x103 = x101 >>> x102; +Tbase TZ x104 = x44 * x48; +Tbase TZ x105 = x45 * x47; +Tbase TZ x106 = x46 * x46; +Tbase TZ x107 = x47 * x45; +Tbase TZ x108 = x48 * x44; +Tbase TZ x109 = x107 + x108; +Tbase TZ x110 = x106 + x109; +Tbase TZ x111 = x105 + x110; +Tbase TZ x112 = x104 + x111; +Tbase TZ x113 = x103 + x112; +Tbase TZ x114 = 0x33; +Tbase TZ x115 = x113 >>> x114; +Tbase TZ x116 = 0x13; +Tbase TZ x117 = x116 * x115; +Tbase TZ x118 = 0x7ffffffffffff; +Tbase TZ x119 = x59 & x118; +Tbase TZ x120 = x117 + x119; +Tbase TZ x121 = 0x33; +Tbase TZ x122 = x120 >>> x121; +Tbase TZ x123 = 0x7ffffffffffff; +Tbase TZ x124 = x73 & x123; +Tbase TZ x125 = x122 + x124; +Tbase TZ x126 = 0x7ffffffffffff; +Tbase TZ x127 = x113 & x126; +Tbase TZ x128 = 0x7ffffffffffff; +Tbase TZ x129 = x101 & x128; +Tbase TZ x130 = 0x33; +Tbase TZ x131 = x125 >>> x130; +Tbase TZ x132 = 0x7ffffffffffff; +Tbase TZ x133 = x87 & x132; +Tbase TZ x134 = x131 + x133; +Tbase TZ x135 = 0x7ffffffffffff; +Tbase TZ x136 = x125 & x135; +Tbase TZ x137 = 0x7ffffffffffff; +Tbase TZ x138 = x120 & x137; +Tbase TZ x139 = 0xffffffffffffe; +Tbase TZ x140 = x139 + x24; +Tbase TZ x141 = x140 - x29; +Tbase TZ x142 = 0xffffffffffffe; +Tbase TZ x143 = x142 + x25; +Tbase TZ x144 = x143 - x30; +Tbase TZ x145 = 0xffffffffffffe; +Tbase TZ x146 = x145 + x26; +Tbase TZ x147 = x146 - x31; +Tbase TZ x148 = 0xffffffffffffe; +Tbase TZ x149 = x148 + x27; +Tbase TZ x150 = x149 - x32; +Tbase TZ x151 = 0xfffffffffffda; +Tbase TZ x152 = x151 + x28; +Tbase TZ x153 = x152 - x33; +Tbase TZ x154 = x153 * x153; +Tbase TZ x155 = x141 * x150; +Tbase TZ x156 = x144 * x147; +Tbase TZ x157 = x147 * x144; +Tbase TZ x158 = x150 * x141; +Tbase TZ x159 = x157 + x158; +Tbase TZ x160 = x156 + x159; +Tbase TZ x161 = x155 + x160; +Tbase TZ x162 = 0x13; +Tbase TZ x163 = x162 * x161; +Tbase TZ x164 = x154 + x163; +Tbase TZ x165 = 0x33; +Tbase TZ x166 = x164 >>> x165; +Tbase TZ x167 = x150 * x153; +Tbase TZ x168 = x153 * x150; +Tbase TZ x169 = x167 + x168; +Tbase TZ x170 = x141 * x147; +Tbase TZ x171 = x144 * x144; +Tbase TZ x172 = x147 * x141; +Tbase TZ x173 = x171 + x172; +Tbase TZ x174 = x170 + x173; +Tbase TZ x175 = 0x13; +Tbase TZ x176 = x175 * x174; +Tbase TZ x177 = x169 + x176; +Tbase TZ x178 = x166 + x177; +Tbase TZ x179 = 0x33; +Tbase TZ x180 = x178 >>> x179; +Tbase TZ x181 = x147 * x153; +Tbase TZ x182 = x150 * x150; +Tbase TZ x183 = x153 * x147; +Tbase TZ x184 = x182 + x183; +Tbase TZ x185 = x181 + x184; +Tbase TZ x186 = x141 * x144; +Tbase TZ x187 = x144 * x141; +Tbase TZ x188 = x186 + x187; +Tbase TZ x189 = 0x13; +Tbase TZ x190 = x189 * x188; +Tbase TZ x191 = x185 + x190; +Tbase TZ x192 = x180 + x191; +Tbase TZ x193 = 0x33; +Tbase TZ x194 = x192 >>> x193; +Tbase TZ x195 = x144 * x153; +Tbase TZ x196 = x147 * x150; +Tbase TZ x197 = x150 * x147; +Tbase TZ x198 = x153 * x144; +Tbase TZ x199 = x197 + x198; +Tbase TZ x200 = x196 + x199; +Tbase TZ x201 = x195 + x200; +Tbase TZ x202 = x141 * x141; +Tbase TZ x203 = 0x13; +Tbase TZ x204 = x203 * x202; +Tbase TZ x205 = x201 + x204; +Tbase TZ x206 = x194 + x205; +Tbase TZ x207 = 0x33; +Tbase TZ x208 = x206 >>> x207; +Tbase TZ x209 = x141 * x153; +Tbase TZ x210 = x144 * x150; +Tbase TZ x211 = x147 * x147; +Tbase TZ x212 = x150 * x144; +Tbase TZ x213 = x153 * x141; +Tbase TZ x214 = x212 + x213; +Tbase TZ x215 = x211 + x214; +Tbase TZ x216 = x210 + x215; +Tbase TZ x217 = x209 + x216; +Tbase TZ x218 = x208 + x217; +Tbase TZ x219 = 0x33; +Tbase TZ x220 = x218 >>> x219; +Tbase TZ x221 = 0x13; +Tbase TZ x222 = x221 * x220; +Tbase TZ x223 = 0x7ffffffffffff; +Tbase TZ x224 = x164 & x223; +Tbase TZ x225 = x222 + x224; +Tbase TZ x226 = 0x33; +Tbase TZ x227 = x225 >>> x226; +Tbase TZ x228 = 0x7ffffffffffff; +Tbase TZ x229 = x178 & x228; +Tbase TZ x230 = x227 + x229; +Tbase TZ x231 = 0x7ffffffffffff; +Tbase TZ x232 = x218 & x231; +Tbase TZ x233 = 0x7ffffffffffff; +Tbase TZ x234 = x206 & x233; +Tbase TZ x235 = 0x33; +Tbase TZ x236 = x230 >>> x235; +Tbase TZ x237 = 0x7ffffffffffff; +Tbase TZ x238 = x192 & x237; +Tbase TZ x239 = x236 + x238; +Tbase TZ x240 = 0x7ffffffffffff; +Tbase TZ x241 = x230 & x240; +Tbase TZ x242 = 0x7ffffffffffff; +Tbase TZ x243 = x225 & x242; +Tbase TZ x244 = 0xffffffffffffe; +Tbase TZ x245 = x244 + x127; +Tbase TZ x246 = x245 - x232; +Tbase TZ x247 = 0xffffffffffffe; +Tbase TZ x248 = x247 + x129; +Tbase TZ x249 = x248 - x234; +Tbase TZ x250 = 0xffffffffffffe; +Tbase TZ x251 = x250 + x134; +Tbase TZ x252 = x251 - x239; +Tbase TZ x253 = 0xffffffffffffe; +Tbase TZ x254 = x253 + x136; +Tbase TZ x255 = x254 - x241; +Tbase TZ x256 = 0xfffffffffffda; +Tbase TZ x257 = x256 + x138; +Tbase TZ x258 = x257 - x243; +Tbase TZ x259 = x34 + x39; +Tbase TZ x260 = x35 + x40; +Tbase TZ x261 = x36 + x41; +Tbase TZ x262 = x37 + x42; +Tbase TZ x263 = x38 + x43; +Tbase TZ x264 = 0xffffffffffffe; +Tbase TZ x265 = x264 + x34; +Tbase TZ x266 = x265 - x39; +Tbase TZ x267 = 0xffffffffffffe; +Tbase TZ x268 = x267 + x35; +Tbase TZ x269 = x268 - x40; +Tbase TZ x270 = 0xffffffffffffe; +Tbase TZ x271 = x270 + x36; +Tbase TZ x272 = x271 - x41; +Tbase TZ x273 = 0xffffffffffffe; +Tbase TZ x274 = x273 + x37; +Tbase TZ x275 = x274 - x42; +Tbase TZ x276 = 0xfffffffffffda; +Tbase TZ x277 = x276 + x38; +Tbase TZ x278 = x277 - x43; +Tbase TZ x279 = x278 * x48; +Tbase TZ x280 = x266 * x47; +Tbase TZ x281 = x269 * x46; +Tbase TZ x282 = x272 * x45; +Tbase TZ x283 = x275 * x44; +Tbase TZ x284 = x282 + x283; +Tbase TZ x285 = x281 + x284; +Tbase TZ x286 = x280 + x285; +Tbase TZ x287 = 0x13; +Tbase TZ x288 = x287 * x286; +Tbase TZ x289 = x279 + x288; +Tbase TZ x290 = 0x33; +Tbase TZ x291 = x289 >>> x290; +Tbase TZ x292 = x275 * x48; +Tbase TZ x293 = x278 * x47; +Tbase TZ x294 = x292 + x293; +Tbase TZ x295 = x266 * x46; +Tbase TZ x296 = x269 * x45; +Tbase TZ x297 = x272 * x44; +Tbase TZ x298 = x296 + x297; +Tbase TZ x299 = x295 + x298; +Tbase TZ x300 = 0x13; +Tbase TZ x301 = x300 * x299; +Tbase TZ x302 = x294 + x301; +Tbase TZ x303 = x291 + x302; +Tbase TZ x304 = 0x33; +Tbase TZ x305 = x303 >>> x304; +Tbase TZ x306 = x272 * x48; +Tbase TZ x307 = x275 * x47; +Tbase TZ x308 = x278 * x46; +Tbase TZ x309 = x307 + x308; +Tbase TZ x310 = x306 + x309; +Tbase TZ x311 = x266 * x45; +Tbase TZ x312 = x269 * x44; +Tbase TZ x313 = x311 + x312; +Tbase TZ x314 = 0x13; +Tbase TZ x315 = x314 * x313; +Tbase TZ x316 = x310 + x315; +Tbase TZ x317 = x305 + x316; +Tbase TZ x318 = 0x33; +Tbase TZ x319 = x317 >>> x318; +Tbase TZ x320 = x269 * x48; +Tbase TZ x321 = x272 * x47; +Tbase TZ x322 = x275 * x46; +Tbase TZ x323 = x278 * x45; +Tbase TZ x324 = x322 + x323; +Tbase TZ x325 = x321 + x324; +Tbase TZ x326 = x320 + x325; +Tbase TZ x327 = x266 * x44; +Tbase TZ x328 = 0x13; +Tbase TZ x329 = x328 * x327; +Tbase TZ x330 = x326 + x329; +Tbase TZ x331 = x319 + x330; +Tbase TZ x332 = 0x33; +Tbase TZ x333 = x331 >>> x332; +Tbase TZ x334 = x266 * x48; +Tbase TZ x335 = x269 * x47; +Tbase TZ x336 = x272 * x46; +Tbase TZ x337 = x275 * x45; +Tbase TZ x338 = x278 * x44; +Tbase TZ x339 = x337 + x338; +Tbase TZ x340 = x336 + x339; +Tbase TZ x341 = x335 + x340; +Tbase TZ x342 = x334 + x341; +Tbase TZ x343 = x333 + x342; +Tbase TZ x344 = 0x33; +Tbase TZ x345 = x343 >>> x344; +Tbase TZ x346 = 0x13; +Tbase TZ x347 = x346 * x345; +Tbase TZ x348 = 0x7ffffffffffff; +Tbase TZ x349 = x289 & x348; +Tbase TZ x350 = x347 + x349; +Tbase TZ x351 = 0x33; +Tbase TZ x352 = x350 >>> x351; +Tbase TZ x353 = 0x7ffffffffffff; +Tbase TZ x354 = x303 & x353; +Tbase TZ x355 = x352 + x354; +Tbase TZ x356 = 0x7ffffffffffff; +Tbase TZ x357 = x343 & x356; +Tbase TZ x358 = 0x7ffffffffffff; +Tbase TZ x359 = x331 & x358; +Tbase TZ x360 = 0x33; +Tbase TZ x361 = x355 >>> x360; +Tbase TZ x362 = 0x7ffffffffffff; +Tbase TZ x363 = x317 & x362; +Tbase TZ x364 = x361 + x363; +Tbase TZ x365 = 0x7ffffffffffff; +Tbase TZ x366 = x355 & x365; +Tbase TZ x367 = 0x7ffffffffffff; +Tbase TZ x368 = x350 & x367; +Tbase TZ x369 = x263 * x153; +Tbase TZ x370 = x259 * x150; +Tbase TZ x371 = x260 * x147; +Tbase TZ x372 = x261 * x144; +Tbase TZ x373 = x262 * x141; +Tbase TZ x374 = x372 + x373; +Tbase TZ x375 = x371 + x374; +Tbase TZ x376 = x370 + x375; +Tbase TZ x377 = 0x13; +Tbase TZ x378 = x377 * x376; +Tbase TZ x379 = x369 + x378; +Tbase TZ x380 = 0x33; +Tbase TZ x381 = x379 >>> x380; +Tbase TZ x382 = x262 * x153; +Tbase TZ x383 = x263 * x150; +Tbase TZ x384 = x382 + x383; +Tbase TZ x385 = x259 * x147; +Tbase TZ x386 = x260 * x144; +Tbase TZ x387 = x261 * x141; +Tbase TZ x388 = x386 + x387; +Tbase TZ x389 = x385 + x388; +Tbase TZ x390 = 0x13; +Tbase TZ x391 = x390 * x389; +Tbase TZ x392 = x384 + x391; +Tbase TZ x393 = x381 + x392; +Tbase TZ x394 = 0x33; +Tbase TZ x395 = x393 >>> x394; +Tbase TZ x396 = x261 * x153; +Tbase TZ x397 = x262 * x150; +Tbase TZ x398 = x263 * x147; +Tbase TZ x399 = x397 + x398; +Tbase TZ x400 = x396 + x399; +Tbase TZ x401 = x259 * x144; +Tbase TZ x402 = x260 * x141; +Tbase TZ x403 = x401 + x402; +Tbase TZ x404 = 0x13; +Tbase TZ x405 = x404 * x403; +Tbase TZ x406 = x400 + x405; +Tbase TZ x407 = x395 + x406; +Tbase TZ x408 = 0x33; +Tbase TZ x409 = x407 >>> x408; +Tbase TZ x410 = x260 * x153; +Tbase TZ x411 = x261 * x150; +Tbase TZ x412 = x262 * x147; +Tbase TZ x413 = x263 * x144; +Tbase TZ x414 = x412 + x413; +Tbase TZ x415 = x411 + x414; +Tbase TZ x416 = x410 + x415; +Tbase TZ x417 = x259 * x141; +Tbase TZ x418 = 0x13; +Tbase TZ x419 = x418 * x417; +Tbase TZ x420 = x416 + x419; +Tbase TZ x421 = x409 + x420; +Tbase TZ x422 = 0x33; +Tbase TZ x423 = x421 >>> x422; +Tbase TZ x424 = x259 * x153; +Tbase TZ x425 = x260 * x150; +Tbase TZ x426 = x261 * x147; +Tbase TZ x427 = x262 * x144; +Tbase TZ x428 = x263 * x141; +Tbase TZ x429 = x427 + x428; +Tbase TZ x430 = x426 + x429; +Tbase TZ x431 = x425 + x430; +Tbase TZ x432 = x424 + x431; +Tbase TZ x433 = x423 + x432; +Tbase TZ x434 = 0x33; +Tbase TZ x435 = x433 >>> x434; +Tbase TZ x436 = 0x13; +Tbase TZ x437 = x436 * x435; +Tbase TZ x438 = 0x7ffffffffffff; +Tbase TZ x439 = x379 & x438; +Tbase TZ x440 = x437 + x439; +Tbase TZ x441 = 0x33; +Tbase TZ x442 = x440 >>> x441; +Tbase TZ x443 = 0x7ffffffffffff; +Tbase TZ x444 = x393 & x443; +Tbase TZ x445 = x442 + x444; +Tbase TZ x446 = 0x7ffffffffffff; +Tbase TZ x447 = x433 & x446; +Tbase TZ x448 = 0x7ffffffffffff; +Tbase TZ x449 = x421 & x448; +Tbase TZ x450 = 0x33; +Tbase TZ x451 = x445 >>> x450; +Tbase TZ x452 = 0x7ffffffffffff; +Tbase TZ x453 = x407 & x452; +Tbase TZ x454 = x451 + x453; +Tbase TZ x455 = 0x7ffffffffffff; +Tbase TZ x456 = x445 & x455; +Tbase TZ x457 = 0x7ffffffffffff; +Tbase TZ x458 = x440 & x457; +Tbase TZ x459 = x357 + x447; +Tbase TZ x460 = x359 + x449; +Tbase TZ x461 = x364 + x454; +Tbase TZ x462 = x366 + x456; +Tbase TZ x463 = x368 + x458; +Tbase TZ x464 = x357 + x447; +Tbase TZ x465 = x359 + x449; +Tbase TZ x466 = x364 + x454; +Tbase TZ x467 = x366 + x456; +Tbase TZ x468 = x368 + x458; +Tbase TZ x469 = x463 * x468; +Tbase TZ x470 = x459 * x467; +Tbase TZ x471 = x460 * x466; +Tbase TZ x472 = x461 * x465; +Tbase TZ x473 = x462 * x464; +Tbase TZ x474 = x472 + x473; +Tbase TZ x475 = x471 + x474; +Tbase TZ x476 = x470 + x475; +Tbase TZ x477 = 0x13; +Tbase TZ x478 = x477 * x476; +Tbase TZ x479 = x469 + x478; +Tbase TZ x480 = 0x33; +Tbase TZ x481 = x479 >>> x480; +Tbase TZ x482 = x462 * x468; +Tbase TZ x483 = x463 * x467; +Tbase TZ x484 = x482 + x483; +Tbase TZ x485 = x459 * x466; +Tbase TZ x486 = x460 * x465; +Tbase TZ x487 = x461 * x464; +Tbase TZ x488 = x486 + x487; +Tbase TZ x489 = x485 + x488; +Tbase TZ x490 = 0x13; +Tbase TZ x491 = x490 * x489; +Tbase TZ x492 = x484 + x491; +Tbase TZ x493 = x481 + x492; +Tbase TZ x494 = 0x33; +Tbase TZ x495 = x493 >>> x494; +Tbase TZ x496 = x461 * x468; +Tbase TZ x497 = x462 * x467; +Tbase TZ x498 = x463 * x466; +Tbase TZ x499 = x497 + x498; +Tbase TZ x500 = x496 + x499; +Tbase TZ x501 = x459 * x465; +Tbase TZ x502 = x460 * x464; +Tbase TZ x503 = x501 + x502; +Tbase TZ x504 = 0x13; +Tbase TZ x505 = x504 * x503; +Tbase TZ x506 = x500 + x505; +Tbase TZ x507 = x495 + x506; +Tbase TZ x508 = 0x33; +Tbase TZ x509 = x507 >>> x508; +Tbase TZ x510 = x460 * x468; +Tbase TZ x511 = x461 * x467; +Tbase TZ x512 = x462 * x466; +Tbase TZ x513 = x463 * x465; +Tbase TZ x514 = x512 + x513; +Tbase TZ x515 = x511 + x514; +Tbase TZ x516 = x510 + x515; +Tbase TZ x517 = x459 * x464; +Tbase TZ x518 = 0x13; +Tbase TZ x519 = x518 * x517; +Tbase TZ x520 = x516 + x519; +Tbase TZ x521 = x509 + x520; +Tbase TZ x522 = 0x33; +Tbase TZ x523 = x521 >>> x522; +Tbase TZ x524 = x459 * x468; +Tbase TZ x525 = x460 * x467; +Tbase TZ x526 = x461 * x466; +Tbase TZ x527 = x462 * x465; +Tbase TZ x528 = x463 * x464; +Tbase TZ x529 = x527 + x528; +Tbase TZ x530 = x526 + x529; +Tbase TZ x531 = x525 + x530; +Tbase TZ x532 = x524 + x531; +Tbase TZ x533 = x523 + x532; +Tbase TZ x534 = 0x33; +Tbase TZ x535 = x533 >>> x534; +Tbase TZ x536 = 0x13; +Tbase TZ x537 = x536 * x535; +Tbase TZ x538 = 0x7ffffffffffff; +Tbase TZ x539 = x479 & x538; +Tbase TZ x540 = x537 + x539; +Tbase TZ x541 = 0x33; +Tbase TZ x542 = x540 >>> x541; +Tbase TZ x543 = 0x7ffffffffffff; +Tbase TZ x544 = x493 & x543; +Tbase TZ x545 = x542 + x544; +Tbase TZ x546 = 0x7ffffffffffff; +Tbase TZ x547 = x533 & x546; +Tbase TZ x548 = 0x7ffffffffffff; +Tbase TZ x549 = x521 & x548; +Tbase TZ x550 = 0x33; +Tbase TZ x551 = x545 >>> x550; +Tbase TZ x552 = 0x7ffffffffffff; +Tbase TZ x553 = x507 & x552; +Tbase TZ x554 = x551 + x553; +Tbase TZ x555 = 0x7ffffffffffff; +Tbase TZ x556 = x545 & x555; +Tbase TZ x557 = 0x7ffffffffffff; +Tbase TZ x558 = x540 & x557; +Tbase TZ x559 = 0xffffffffffffe; +Tbase TZ x560 = x559 + x357; +Tbase TZ x561 = x560 - x447; +Tbase TZ x562 = 0xffffffffffffe; +Tbase TZ x563 = x562 + x359; +Tbase TZ x564 = x563 - x449; +Tbase TZ x565 = 0xffffffffffffe; +Tbase TZ x566 = x565 + x364; +Tbase TZ x567 = x566 - x454; +Tbase TZ x568 = 0xffffffffffffe; +Tbase TZ x569 = x568 + x366; +Tbase TZ x570 = x569 - x456; +Tbase TZ x571 = 0xfffffffffffda; +Tbase TZ x572 = x571 + x368; +Tbase TZ x573 = x572 - x458; +Tbase TZ x574 = 0xffffffffffffe; +Tbase TZ x575 = x574 + x357; +Tbase TZ x576 = x575 - x447; +Tbase TZ x577 = 0xffffffffffffe; +Tbase TZ x578 = x577 + x359; +Tbase TZ x579 = x578 - x449; +Tbase TZ x580 = 0xffffffffffffe; +Tbase TZ x581 = x580 + x364; +Tbase TZ x582 = x581 - x454; +Tbase TZ x583 = 0xffffffffffffe; +Tbase TZ x584 = x583 + x366; +Tbase TZ x585 = x584 - x456; +Tbase TZ x586 = 0xfffffffffffda; +Tbase TZ x587 = x586 + x368; +Tbase TZ x588 = x587 - x458; +Tbase TZ x589 = x573 * x588; +Tbase TZ x590 = x561 * x585; +Tbase TZ x591 = x564 * x582; +Tbase TZ x592 = x567 * x579; +Tbase TZ x593 = x570 * x576; +Tbase TZ x594 = x592 + x593; +Tbase TZ x595 = x591 + x594; +Tbase TZ x596 = x590 + x595; +Tbase TZ x597 = 0x13; +Tbase TZ x598 = x597 * x596; +Tbase TZ x599 = x589 + x598; +Tbase TZ x600 = 0x33; +Tbase TZ x601 = x599 >>> x600; +Tbase TZ x602 = x570 * x588; +Tbase TZ x603 = x573 * x585; +Tbase TZ x604 = x602 + x603; +Tbase TZ x605 = x561 * x582; +Tbase TZ x606 = x564 * x579; +Tbase TZ x607 = x567 * x576; +Tbase TZ x608 = x606 + x607; +Tbase TZ x609 = x605 + x608; +Tbase TZ x610 = 0x13; +Tbase TZ x611 = x610 * x609; +Tbase TZ x612 = x604 + x611; +Tbase TZ x613 = x601 + x612; +Tbase TZ x614 = 0x33; +Tbase TZ x615 = x613 >>> x614; +Tbase TZ x616 = x567 * x588; +Tbase TZ x617 = x570 * x585; +Tbase TZ x618 = x573 * x582; +Tbase TZ x619 = x617 + x618; +Tbase TZ x620 = x616 + x619; +Tbase TZ x621 = x561 * x579; +Tbase TZ x622 = x564 * x576; +Tbase TZ x623 = x621 + x622; +Tbase TZ x624 = 0x13; +Tbase TZ x625 = x624 * x623; +Tbase TZ x626 = x620 + x625; +Tbase TZ x627 = x615 + x626; +Tbase TZ x628 = 0x33; +Tbase TZ x629 = x627 >>> x628; +Tbase TZ x630 = x564 * x588; +Tbase TZ x631 = x567 * x585; +Tbase TZ x632 = x570 * x582; +Tbase TZ x633 = x573 * x579; +Tbase TZ x634 = x632 + x633; +Tbase TZ x635 = x631 + x634; +Tbase TZ x636 = x630 + x635; +Tbase TZ x637 = x561 * x576; +Tbase TZ x638 = 0x13; +Tbase TZ x639 = x638 * x637; +Tbase TZ x640 = x636 + x639; +Tbase TZ x641 = x629 + x640; +Tbase TZ x642 = 0x33; +Tbase TZ x643 = x641 >>> x642; +Tbase TZ x644 = x561 * x588; +Tbase TZ x645 = x564 * x585; +Tbase TZ x646 = x567 * x582; +Tbase TZ x647 = x570 * x579; +Tbase TZ x648 = x573 * x576; +Tbase TZ x649 = x647 + x648; +Tbase TZ x650 = x646 + x649; +Tbase TZ x651 = x645 + x650; +Tbase TZ x652 = x644 + x651; +Tbase TZ x653 = x643 + x652; +Tbase TZ x654 = 0x33; +Tbase TZ x655 = x653 >>> x654; +Tbase TZ x656 = 0x13; +Tbase TZ x657 = x656 * x655; +Tbase TZ x658 = 0x7ffffffffffff; +Tbase TZ x659 = x599 & x658; +Tbase TZ x660 = x657 + x659; +Tbase TZ x661 = 0x33; +Tbase TZ x662 = x660 >>> x661; +Tbase TZ x663 = 0x7ffffffffffff; +Tbase TZ x664 = x613 & x663; +Tbase TZ x665 = x662 + x664; +Tbase TZ x666 = 0x7ffffffffffff; +Tbase TZ x667 = x653 & x666; +Tbase TZ x668 = 0x7ffffffffffff; +Tbase TZ x669 = x641 & x668; +Tbase TZ x670 = 0x33; +Tbase TZ x671 = x665 >>> x670; +Tbase TZ x672 = 0x7ffffffffffff; +Tbase TZ x673 = x627 & x672; +Tbase TZ x674 = x671 + x673; +Tbase TZ x675 = 0x7ffffffffffff; +Tbase TZ x676 = x665 & x675; +Tbase TZ x677 = 0x7ffffffffffff; +Tbase TZ x678 = x660 & x677; +Tbase TZ x679 = x23 * x678; +Tbase TZ x680 = x19 * x676; +Tbase TZ x681 = x20 * x674; +Tbase TZ x682 = x21 * x669; +Tbase TZ x683 = x22 * x667; +Tbase TZ x684 = x682 + x683; +Tbase TZ x685 = x681 + x684; +Tbase TZ x686 = x680 + x685; +Tbase TZ x687 = 0x13; +Tbase TZ x688 = x687 * x686; +Tbase TZ x689 = x679 + x688; +Tbase TZ x690 = 0x33; +Tbase TZ x691 = x689 >>> x690; +Tbase TZ x692 = x22 * x678; +Tbase TZ x693 = x23 * x676; +Tbase TZ x694 = x692 + x693; +Tbase TZ x695 = x19 * x674; +Tbase TZ x696 = x20 * x669; +Tbase TZ x697 = x21 * x667; +Tbase TZ x698 = x696 + x697; +Tbase TZ x699 = x695 + x698; +Tbase TZ x700 = 0x13; +Tbase TZ x701 = x700 * x699; +Tbase TZ x702 = x694 + x701; +Tbase TZ x703 = x691 + x702; +Tbase TZ x704 = 0x33; +Tbase TZ x705 = x703 >>> x704; +Tbase TZ x706 = x21 * x678; +Tbase TZ x707 = x22 * x676; +Tbase TZ x708 = x23 * x674; +Tbase TZ x709 = x707 + x708; +Tbase TZ x710 = x706 + x709; +Tbase TZ x711 = x19 * x669; +Tbase TZ x712 = x20 * x667; +Tbase TZ x713 = x711 + x712; +Tbase TZ x714 = 0x13; +Tbase TZ x715 = x714 * x713; +Tbase TZ x716 = x710 + x715; +Tbase TZ x717 = x705 + x716; +Tbase TZ x718 = 0x33; +Tbase TZ x719 = x717 >>> x718; +Tbase TZ x720 = x20 * x678; +Tbase TZ x721 = x21 * x676; +Tbase TZ x722 = x22 * x674; +Tbase TZ x723 = x23 * x669; +Tbase TZ x724 = x722 + x723; +Tbase TZ x725 = x721 + x724; +Tbase TZ x726 = x720 + x725; +Tbase TZ x727 = x19 * x667; +Tbase TZ x728 = 0x13; +Tbase TZ x729 = x728 * x727; +Tbase TZ x730 = x726 + x729; +Tbase TZ x731 = x719 + x730; +Tbase TZ x732 = 0x33; +Tbase TZ x733 = x731 >>> x732; +Tbase TZ x734 = x19 * x678; +Tbase TZ x735 = x20 * x676; +Tbase TZ x736 = x21 * x674; +Tbase TZ x737 = x22 * x669; +Tbase TZ x738 = x23 * x667; +Tbase TZ x739 = x737 + x738; +Tbase TZ x740 = x736 + x739; +Tbase TZ x741 = x735 + x740; +Tbase TZ x742 = x734 + x741; +Tbase TZ x743 = x733 + x742; +Tbase TZ x744 = 0x33; +Tbase TZ x745 = x743 >>> x744; +Tbase TZ x746 = 0x13; +Tbase TZ x747 = x746 * x745; +Tbase TZ x748 = 0x7ffffffffffff; +Tbase TZ x749 = x689 & x748; +Tbase TZ x750 = x747 + x749; +Tbase TZ x751 = 0x33; +Tbase TZ x752 = x750 >>> x751; +Tbase TZ x753 = 0x7ffffffffffff; +Tbase TZ x754 = x703 & x753; +Tbase TZ x755 = x752 + x754; +Tbase TZ x756 = 0x7ffffffffffff; +Tbase TZ x757 = x743 & x756; +Tbase TZ x758 = 0x7ffffffffffff; +Tbase TZ x759 = x731 & x758; +Tbase TZ x760 = 0x33; +Tbase TZ x761 = x755 >>> x760; +Tbase TZ x762 = 0x7ffffffffffff; +Tbase TZ x763 = x717 & x762; +Tbase TZ x764 = x761 + x763; +Tbase TZ x765 = 0x7ffffffffffff; +Tbase TZ x766 = x755 & x765; +Tbase TZ x767 = 0x7ffffffffffff; +Tbase TZ x768 = x750 & x767; +Tbase TZ x769 = x138 * x243; +Tbase TZ x770 = x127 * x241; +Tbase TZ x771 = x129 * x239; +Tbase TZ x772 = x134 * x234; +Tbase TZ x773 = x136 * x232; +Tbase TZ x774 = x772 + x773; +Tbase TZ x775 = x771 + x774; +Tbase TZ x776 = x770 + x775; +Tbase TZ x777 = 0x13; +Tbase TZ x778 = x777 * x776; +Tbase TZ x779 = x769 + x778; +Tbase TZ x780 = 0x33; +Tbase TZ x781 = x779 >>> x780; +Tbase TZ x782 = x136 * x243; +Tbase TZ x783 = x138 * x241; +Tbase TZ x784 = x782 + x783; +Tbase TZ x785 = x127 * x239; +Tbase TZ x786 = x129 * x234; +Tbase TZ x787 = x134 * x232; +Tbase TZ x788 = x786 + x787; +Tbase TZ x789 = x785 + x788; +Tbase TZ x790 = 0x13; +Tbase TZ x791 = x790 * x789; +Tbase TZ x792 = x784 + x791; +Tbase TZ x793 = x781 + x792; +Tbase TZ x794 = 0x33; +Tbase TZ x795 = x793 >>> x794; +Tbase TZ x796 = x134 * x243; +Tbase TZ x797 = x136 * x241; +Tbase TZ x798 = x138 * x239; +Tbase TZ x799 = x797 + x798; +Tbase TZ x800 = x796 + x799; +Tbase TZ x801 = x127 * x234; +Tbase TZ x802 = x129 * x232; +Tbase TZ x803 = x801 + x802; +Tbase TZ x804 = 0x13; +Tbase TZ x805 = x804 * x803; +Tbase TZ x806 = x800 + x805; +Tbase TZ x807 = x795 + x806; +Tbase TZ x808 = 0x33; +Tbase TZ x809 = x807 >>> x808; +Tbase TZ x810 = x129 * x243; +Tbase TZ x811 = x134 * x241; +Tbase TZ x812 = x136 * x239; +Tbase TZ x813 = x138 * x234; +Tbase TZ x814 = x812 + x813; +Tbase TZ x815 = x811 + x814; +Tbase TZ x816 = x810 + x815; +Tbase TZ x817 = x127 * x232; +Tbase TZ x818 = 0x13; +Tbase TZ x819 = x818 * x817; +Tbase TZ x820 = x816 + x819; +Tbase TZ x821 = x809 + x820; +Tbase TZ x822 = 0x33; +Tbase TZ x823 = x821 >>> x822; +Tbase TZ x824 = x127 * x243; +Tbase TZ x825 = x129 * x241; +Tbase TZ x826 = x134 * x239; +Tbase TZ x827 = x136 * x234; +Tbase TZ x828 = x138 * x232; +Tbase TZ x829 = x827 + x828; +Tbase TZ x830 = x826 + x829; +Tbase TZ x831 = x825 + x830; +Tbase TZ x832 = x824 + x831; +Tbase TZ x833 = x823 + x832; +Tbase TZ x834 = 0x33; +Tbase TZ x835 = x833 >>> x834; +Tbase TZ x836 = 0x13; +Tbase TZ x837 = x836 * x835; +Tbase TZ x838 = 0x7ffffffffffff; +Tbase TZ x839 = x779 & x838; +Tbase TZ x840 = x837 + x839; +Tbase TZ x841 = 0x33; +Tbase TZ x842 = x840 >>> x841; +Tbase TZ x843 = 0x7ffffffffffff; +Tbase TZ x844 = x793 & x843; +Tbase TZ x845 = x842 + x844; +Tbase TZ x846 = 0x7ffffffffffff; +Tbase TZ x847 = x833 & x846; +Tbase TZ x848 = 0x7ffffffffffff; +Tbase TZ x849 = x821 & x848; +Tbase TZ x850 = 0x33; +Tbase TZ x851 = x845 >>> x850; +Tbase TZ x852 = 0x7ffffffffffff; +Tbase TZ x853 = x807 & x852; +Tbase TZ x854 = x851 + x853; +Tbase TZ x855 = 0x7ffffffffffff; +Tbase TZ x856 = x845 & x855; +Tbase TZ x857 = 0x7ffffffffffff; +Tbase TZ x858 = x840 & x857; +Tbase TZ x859 = x18 * x258; +Tbase TZ x860 = x14 * x255; +Tbase TZ x861 = x15 * x252; +Tbase TZ x862 = x16 * x249; +Tbase TZ x863 = x17 * x246; +Tbase TZ x864 = x862 + x863; +Tbase TZ x865 = x861 + x864; +Tbase TZ x866 = x860 + x865; +Tbase TZ x867 = 0x13; +Tbase TZ x868 = x867 * x866; +Tbase TZ x869 = x859 + x868; +Tbase TZ x870 = 0x33; +Tbase TZ x871 = x869 >>> x870; +Tbase TZ x872 = x17 * x258; +Tbase TZ x873 = x18 * x255; +Tbase TZ x874 = x872 + x873; +Tbase TZ x875 = x14 * x252; +Tbase TZ x876 = x15 * x249; +Tbase TZ x877 = x16 * x246; +Tbase TZ x878 = x876 + x877; +Tbase TZ x879 = x875 + x878; +Tbase TZ x880 = 0x13; +Tbase TZ x881 = x880 * x879; +Tbase TZ x882 = x874 + x881; +Tbase TZ x883 = x871 + x882; +Tbase TZ x884 = 0x33; +Tbase TZ x885 = x883 >>> x884; +Tbase TZ x886 = x16 * x258; +Tbase TZ x887 = x17 * x255; +Tbase TZ x888 = x18 * x252; +Tbase TZ x889 = x887 + x888; +Tbase TZ x890 = x886 + x889; +Tbase TZ x891 = x14 * x249; +Tbase TZ x892 = x15 * x246; +Tbase TZ x893 = x891 + x892; +Tbase TZ x894 = 0x13; +Tbase TZ x895 = x894 * x893; +Tbase TZ x896 = x890 + x895; +Tbase TZ x897 = x885 + x896; +Tbase TZ x898 = 0x33; +Tbase TZ x899 = x897 >>> x898; +Tbase TZ x900 = x15 * x258; +Tbase TZ x901 = x16 * x255; +Tbase TZ x902 = x17 * x252; +Tbase TZ x903 = x18 * x249; +Tbase TZ x904 = x902 + x903; +Tbase TZ x905 = x901 + x904; +Tbase TZ x906 = x900 + x905; +Tbase TZ x907 = x14 * x246; +Tbase TZ x908 = 0x13; +Tbase TZ x909 = x908 * x907; +Tbase TZ x910 = x906 + x909; +Tbase TZ x911 = x899 + x910; +Tbase TZ x912 = 0x33; +Tbase TZ x913 = x911 >>> x912; +Tbase TZ x914 = x14 * x258; +Tbase TZ x915 = x15 * x255; +Tbase TZ x916 = x16 * x252; +Tbase TZ x917 = x17 * x249; +Tbase TZ x918 = x18 * x246; +Tbase TZ x919 = x917 + x918; +Tbase TZ x920 = x916 + x919; +Tbase TZ x921 = x915 + x920; +Tbase TZ x922 = x914 + x921; +Tbase TZ x923 = x913 + x922; +Tbase TZ x924 = 0x33; +Tbase TZ x925 = x923 >>> x924; +Tbase TZ x926 = 0x13; +Tbase TZ x927 = x926 * x925; +Tbase TZ x928 = 0x7ffffffffffff; +Tbase TZ x929 = x869 & x928; +Tbase TZ x930 = x927 + x929; +Tbase TZ x931 = 0x33; +Tbase TZ x932 = x930 >>> x931; +Tbase TZ x933 = 0x7ffffffffffff; +Tbase TZ x934 = x883 & x933; +Tbase TZ x935 = x932 + x934; +Tbase TZ x936 = 0x7ffffffffffff; +Tbase TZ x937 = x923 & x936; +Tbase TZ x938 = 0x7ffffffffffff; +Tbase TZ x939 = x911 & x938; +Tbase TZ x940 = 0x33; +Tbase TZ x941 = x935 >>> x940; +Tbase TZ x942 = 0x7ffffffffffff; +Tbase TZ x943 = x897 & x942; +Tbase TZ x944 = x941 + x943; +Tbase TZ x945 = 0x7ffffffffffff; +Tbase TZ x946 = x935 & x945; +Tbase TZ x947 = 0x7ffffffffffff; +Tbase TZ x948 = x930 & x947; +Tbase TZ x949 = x127 + x937; +Tbase TZ x950 = x129 + x939; +Tbase TZ x951 = x134 + x944; +Tbase TZ x952 = x136 + x946; +Tbase TZ x953 = x138 + x948; +Tbase TZ x954 = x258 * x953; +Tbase TZ x955 = x246 * x952; +Tbase TZ x956 = x249 * x951; +Tbase TZ x957 = x252 * x950; +Tbase TZ x958 = x255 * x949; +Tbase TZ x959 = x957 + x958; +Tbase TZ x960 = x956 + x959; +Tbase TZ x961 = x955 + x960; +Tbase TZ x962 = 0x13; +Tbase TZ x963 = x962 * x961; +Tbase TZ x964 = x954 + x963; +Tbase TZ x965 = 0x33; +Tbase TZ x966 = x964 >>> x965; +Tbase TZ x967 = x255 * x953; +Tbase TZ x968 = x258 * x952; +Tbase TZ x969 = x967 + x968; +Tbase TZ x970 = x246 * x951; +Tbase TZ x971 = x249 * x950; +Tbase TZ x972 = x252 * x949; +Tbase TZ x973 = x971 + x972; +Tbase TZ x974 = x970 + x973; +Tbase TZ x975 = 0x13; +Tbase TZ x976 = x975 * x974; +Tbase TZ x977 = x969 + x976; +Tbase TZ x978 = x966 + x977; +Tbase TZ x979 = 0x33; +Tbase TZ x980 = x978 >>> x979; +Tbase TZ x981 = x252 * x953; +Tbase TZ x982 = x255 * x952; +Tbase TZ x983 = x258 * x951; +Tbase TZ x984 = x982 + x983; +Tbase TZ x985 = x981 + x984; +Tbase TZ x986 = x246 * x950; +Tbase TZ x987 = x249 * x949; +Tbase TZ x988 = x986 + x987; +Tbase TZ x989 = 0x13; +Tbase TZ x990 = x989 * x988; +Tbase TZ x991 = x985 + x990; +Tbase TZ x992 = x980 + x991; +Tbase TZ x993 = 0x33; +Tbase TZ x994 = x992 >>> x993; +Tbase TZ x995 = x249 * x953; +Tbase TZ x996 = x252 * x952; +Tbase TZ x997 = x255 * x951; +Tbase TZ x998 = x258 * x950; +Tbase TZ x999 = x997 + x998; +Tbase TZ x1000 = x996 + x999; +Tbase TZ x1001 = x995 + x1000; +Tbase TZ x1002 = x246 * x949; +Tbase TZ x1003 = 0x13; +Tbase TZ x1004 = x1003 * x1002; +Tbase TZ x1005 = x1001 + x1004; +Tbase TZ x1006 = x994 + x1005; +Tbase TZ x1007 = 0x33; +Tbase TZ x1008 = x1006 >>> x1007; +Tbase TZ x1009 = x246 * x953; +Tbase TZ x1010 = x249 * x952; +Tbase TZ x1011 = x252 * x951; +Tbase TZ x1012 = x255 * x950; +Tbase TZ x1013 = x258 * x949; +Tbase TZ x1014 = x1012 + x1013; +Tbase TZ x1015 = x1011 + x1014; +Tbase TZ x1016 = x1010 + x1015; +Tbase TZ x1017 = x1009 + x1016; +Tbase TZ x1018 = x1008 + x1017; +Tbase TZ x1019 = 0x33; +Tbase TZ x1020 = x1018 >>> x1019; +Tbase TZ x1021 = 0x13; +Tbase TZ x1022 = x1021 * x1020; +Tbase TZ x1023 = 0x7ffffffffffff; +Tbase TZ x1024 = x964 & x1023; +Tbase TZ x1025 = x1022 + x1024; +Tbase TZ x1026 = 0x33; +Tbase TZ x1027 = x1025 >>> x1026; +Tbase TZ x1028 = 0x7ffffffffffff; +Tbase TZ x1029 = x978 & x1028; +Tbase TZ x1030 = x1027 + x1029; +Tbase TZ x1031 = 0x7ffffffffffff; +Tbase TZ x1032 = x1018 & x1031; +Tbase TZ x1033 = 0x7ffffffffffff; +Tbase TZ x1034 = x1006 & x1033; +Tbase TZ x1035 = 0x33; +Tbase TZ x1036 = x1030 >>> x1035; +Tbase TZ x1037 = 0x7ffffffffffff; +Tbase TZ x1038 = x992 & x1037; +Tbase TZ x1039 = x1036 + x1038; +Tbase TZ x1040 = 0x7ffffffffffff; +Tbase TZ x1041 = x1030 & x1040; +Tbase TZ x1042 = 0x7ffffffffffff; +Tbase TZ x1043 = x1025 & x1042; +(Return x847, Return x849, Return x854, Return x856, +Return x858, +(Return x1032, Return x1034, Return x1039, Return x1041, Return x1043), +(Return x547, Return x549, Return x554, Return x556, Return x558), +(Return x757, Return x759, Return x764, Return x766, Return x768)) + : forall var : base_type -> Type, + expr base_type op + (TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> + TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> TZ -> ...) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/MulDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/MulDisplay.log new file mode 100644 index 000000000..47536ebbf --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/MulDisplay.log @@ -0,0 +1,91 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ, +Tbase Syntax.TZ x9 = x3 * x8; +Tbase Syntax.TZ x10 = x * x7; +Tbase Syntax.TZ x11 = x0 * x6; +Tbase Syntax.TZ x12 = x1 * x5; +Tbase Syntax.TZ x13 = x2 * x4; +Tbase Syntax.TZ x14 = x12 + x13; +Tbase Syntax.TZ x15 = x11 + x14; +Tbase Syntax.TZ x16 = x10 + x15; +Tbase Syntax.TZ x17 = 0x13 * x16; +Tbase Syntax.TZ x18 = x9 + x17; +Tbase Syntax.TZ x19 = x18 >> 0x33; +Tbase Syntax.TZ x20 = x2 * x8; +Tbase Syntax.TZ x21 = x3 * x7; +Tbase Syntax.TZ x22 = x20 + x21; +Tbase Syntax.TZ x23 = x * x6; +Tbase Syntax.TZ x24 = x0 * x5; +Tbase Syntax.TZ x25 = x1 * x4; +Tbase Syntax.TZ x26 = x24 + x25; +Tbase Syntax.TZ x27 = x23 + x26; +Tbase Syntax.TZ x28 = 0x13 * x27; +Tbase Syntax.TZ x29 = x22 + x28; +Tbase Syntax.TZ x30 = x19 + x29; +Tbase Syntax.TZ x31 = x30 >> 0x33; +Tbase Syntax.TZ x32 = x1 * x8; +Tbase Syntax.TZ x33 = x2 * x7; +Tbase Syntax.TZ x34 = x3 * x6; +Tbase Syntax.TZ x35 = x33 + x34; +Tbase Syntax.TZ x36 = x32 + x35; +Tbase Syntax.TZ x37 = x * x5; +Tbase Syntax.TZ x38 = x0 * x4; +Tbase Syntax.TZ x39 = x37 + x38; +Tbase Syntax.TZ x40 = 0x13 * x39; +Tbase Syntax.TZ x41 = x36 + x40; +Tbase Syntax.TZ x42 = x31 + x41; +Tbase Syntax.TZ x43 = x42 >> 0x33; +Tbase Syntax.TZ x44 = x0 * x8; +Tbase Syntax.TZ x45 = x1 * x7; +Tbase Syntax.TZ x46 = x2 * x6; +Tbase Syntax.TZ x47 = x3 * x5; +Tbase Syntax.TZ x48 = x46 + x47; +Tbase Syntax.TZ x49 = x45 + x48; +Tbase Syntax.TZ x50 = x44 + x49; +Tbase Syntax.TZ x51 = x * x4; +Tbase Syntax.TZ x52 = 0x13 * x51; +Tbase Syntax.TZ x53 = x50 + x52; +Tbase Syntax.TZ x54 = x43 + x53; +Tbase Syntax.TZ x55 = x54 >> 0x33; +Tbase Syntax.TZ x56 = x * x8; +Tbase Syntax.TZ x57 = x0 * x7; +Tbase Syntax.TZ x58 = x1 * x6; +Tbase Syntax.TZ x59 = x2 * x5; +Tbase Syntax.TZ x60 = x3 * x4; +Tbase Syntax.TZ x61 = x59 + x60; +Tbase Syntax.TZ x62 = x58 + x61; +Tbase Syntax.TZ x63 = x57 + x62; +Tbase Syntax.TZ x64 = x56 + x63; +Tbase Syntax.TZ x65 = x55 + x64; +Tbase Syntax.TZ x66 = x65 >> 0x33; +Tbase Syntax.TZ x67 = 0x13 * x66; +Tbase Syntax.TZ x68 = x18 & 0x7ffffffffffff; +Tbase Syntax.TZ x69 = x67 + x68; +Tbase Syntax.TZ x70 = x69 >> 0x33; +Tbase Syntax.TZ x71 = x30 & 0x7ffffffffffff; +Tbase Syntax.TZ x72 = x70 + x71; +Tbase Syntax.TZ x73 = x65 & 0x7ffffffffffff; +Tbase Syntax.TZ x74 = x54 & 0x7ffffffffffff; +Tbase Syntax.TZ x75 = x72 >> 0x33; +Tbase Syntax.TZ x76 = x42 & 0x7ffffffffffff; +Tbase Syntax.TZ x77 = x75 + x76; +Tbase Syntax.TZ x78 = x72 & 0x7ffffffffffff; +Tbase Syntax.TZ x79 = x69 & 0x7ffffffffffff; +(Return x73, Return x74, Return x77, Return x78, Return x79) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/MulJavaDisplay.log b/src/SpecificGen/GF25519_64Reflective/Reified/MulJavaDisplay.log new file mode 100644 index 000000000..9e5e4069a --- /dev/null +++ b/src/SpecificGen/GF25519_64Reflective/Reified/MulJavaDisplay.log @@ -0,0 +1,91 @@ +rmulW = +fun var : Syntax.base_type -> Type => +λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ, +Tbase Syntax.TZ x9 = x3 * x8; +Tbase Syntax.TZ x10 = x * x7; +Tbase Syntax.TZ x11 = x0 * x6; +Tbase Syntax.TZ x12 = x1 * x5; +Tbase Syntax.TZ x13 = x2 * x4; +Tbase Syntax.TZ x14 = x12 + x13; +Tbase Syntax.TZ x15 = x11 + x14; +Tbase Syntax.TZ x16 = x10 + x15; +Tbase Syntax.TZ x17 = 0x13 * x16; +Tbase Syntax.TZ x18 = x9 + x17; +Tbase Syntax.TZ x19 = x18 >>> 0x33; +Tbase Syntax.TZ x20 = x2 * x8; +Tbase Syntax.TZ x21 = x3 * x7; +Tbase Syntax.TZ x22 = x20 + x21; +Tbase Syntax.TZ x23 = x * x6; +Tbase Syntax.TZ x24 = x0 * x5; +Tbase Syntax.TZ x25 = x1 * x4; +Tbase Syntax.TZ x26 = x24 + x25; +Tbase Syntax.TZ x27 = x23 + x26; +Tbase Syntax.TZ x28 = 0x13 * x27; +Tbase Syntax.TZ x29 = x22 + x28; +Tbase Syntax.TZ x30 = x19 + x29; +Tbase Syntax.TZ x31 = x30 >>> 0x33; +Tbase Syntax.TZ x32 = x1 * x8; +Tbase Syntax.TZ x33 = x2 * x7; +Tbase Syntax.TZ x34 = x3 * x6; +Tbase Syntax.TZ x35 = x33 + x34; +Tbase Syntax.TZ x36 = x32 + x35; +Tbase Syntax.TZ x37 = x * x5; +Tbase Syntax.TZ x38 = x0 * x4; +Tbase Syntax.TZ x39 = x37 + x38; +Tbase Syntax.TZ x40 = 0x13 * x39; +Tbase Syntax.TZ x41 = x36 + x40; +Tbase Syntax.TZ x42 = x31 + x41; +Tbase Syntax.TZ x43 = x42 >>> 0x33; +Tbase Syntax.TZ x44 = x0 * x8; +Tbase Syntax.TZ x45 = x1 * x7; +Tbase Syntax.TZ x46 = x2 * x6; +Tbase Syntax.TZ x47 = x3 * x5; +Tbase Syntax.TZ x48 = x46 + x47; +Tbase Syntax.TZ x49 = x45 + x48; +Tbase Syntax.TZ x50 = x44 + x49; +Tbase Syntax.TZ x51 = x * x4; +Tbase Syntax.TZ x52 = 0x13 * x51; +Tbase Syntax.TZ x53 = x50 + x52; +Tbase Syntax.TZ x54 = x43 + x53; +Tbase Syntax.TZ x55 = x54 >>> 0x33; +Tbase Syntax.TZ x56 = x * x8; +Tbase Syntax.TZ x57 = x0 * x7; +Tbase Syntax.TZ x58 = x1 * x6; +Tbase Syntax.TZ x59 = x2 * x5; +Tbase Syntax.TZ x60 = x3 * x4; +Tbase Syntax.TZ x61 = x59 + x60; +Tbase Syntax.TZ x62 = x58 + x61; +Tbase Syntax.TZ x63 = x57 + x62; +Tbase Syntax.TZ x64 = x56 + x63; +Tbase Syntax.TZ x65 = x55 + x64; +Tbase Syntax.TZ x66 = x65 >>> 0x33; +Tbase Syntax.TZ x67 = 0x13 * x66; +Tbase Syntax.TZ x68 = x18 & 0x7ffffffffffff; +Tbase Syntax.TZ x69 = x67 + x68; +Tbase Syntax.TZ x70 = x69 >>> 0x33; +Tbase Syntax.TZ x71 = x30 & 0x7ffffffffffff; +Tbase Syntax.TZ x72 = x70 + x71; +Tbase Syntax.TZ x73 = x65 & 0x7ffffffffffff; +Tbase Syntax.TZ x74 = x54 & 0x7ffffffffffff; +Tbase Syntax.TZ x75 = x72 >>> 0x33; +Tbase Syntax.TZ x76 = x42 & 0x7ffffffffffff; +Tbase Syntax.TZ x77 = x75 + x76; +Tbase Syntax.TZ x78 = x72 & 0x7ffffffffffff; +Tbase Syntax.TZ x79 = x69 & 0x7ffffffffffff; +(Return x73, Return x74, Return x77, Return x78, Return x79) + : forall var : Syntax.base_type -> Type, + expr Syntax.base_type Syntax.op + (Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Syntax.TZ -> + Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ * + Tbase Syntax.TZ * Tbase Syntax.TZ) + +Argument scope is [function_scope] |