forked from mit-plv/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update .log.expected files with checked-in generated ones
- Loading branch information
1 parent
6e3b84d
commit 048d025
Showing
121 changed files
with
11,414 additions
and
974 deletions.
There are no files selected for viewing
439 changes: 439 additions & 0 deletions
439
src/Specific/montgomery32_2e226m5_8limbs/femulDisplay.log.expected
Large diffs are not rendered by default.
Oops, something went wrong.
32 changes: 32 additions & 0 deletions
32
src/Specific/montgomery32_2e226m5_8limbs/feoppDisplay.log.expected
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, | ||
| Interp-η | ||
| (λ var : Syntax.base_type → Type, | ||
| λ '(x13, x14, x12, x10, x8, x6, x4, x2)%core, | ||
| uint32_t x16, uint8_t/*bool*/ x17 = subborrow_u32(0x0, 0x0, x2); | ||
| uint32_t x19, uint8_t/*bool*/ x20 = subborrow_u32(x17, 0x0, x4); | ||
| uint32_t x22, uint8_t/*bool*/ x23 = subborrow_u32(x20, 0x0, x6); | ||
| uint32_t x25, uint8_t/*bool*/ x26 = subborrow_u32(x23, 0x0, x8); | ||
| uint32_t x28, uint8_t/*bool*/ x29 = subborrow_u32(x26, 0x0, x10); | ||
| uint32_t x31, uint8_t/*bool*/ x32 = subborrow_u32(x29, 0x0, x12); | ||
| uint32_t x34, uint8_t/*bool*/ x35 = subborrow_u32(x32, 0x0, x14); | ||
| uint32_t x37, uint8_t/*bool*/ x38 = subborrow_u32(x35, 0x0, x13); | ||
| uint32_t x39 = cmovznz32(x38, 0x0, 0xffffffff); | ||
| uint32_t x40 = (x39 & 0xfffffffb); | ||
| uint32_t x42, uint8_t/*bool*/ x43 = addcarryx_u32(0x0, x16, x40); | ||
| uint32_t x44 = (x39 & 0xffffffff); | ||
| uint32_t x46, uint8_t/*bool*/ x47 = addcarryx_u32(x43, x19, x44); | ||
| uint32_t x48 = (x39 & 0xffffffff); | ||
| uint32_t x50, uint8_t/*bool*/ x51 = addcarryx_u32(x47, x22, x48); | ||
| uint32_t x52 = (x39 & 0xffffffff); | ||
| uint32_t x54, uint8_t/*bool*/ x55 = addcarryx_u32(x51, x25, x52); | ||
| uint32_t x56 = (x39 & 0xffffffff); | ||
| uint32_t x58, uint8_t/*bool*/ x59 = addcarryx_u32(x55, x28, x56); | ||
| uint32_t x60 = (x39 & 0xffffffff); | ||
| uint32_t x62, uint8_t/*bool*/ x63 = addcarryx_u32(x59, x31, x60); | ||
| uint32_t x64 = (x39 & 0xffffffff); | ||
| uint32_t x66, uint8_t/*bool*/ x67 = addcarryx_u32(x63, x34, x64); | ||
| uint8_t x68 = ((uint8_t)x39 & 0x3); | ||
| uint32_t x70, uint8_t/*bool*/ _ = addcarryx_u32(x67, x37, x68); | ||
| (Return x70, Return x66, Return x62, Return x58, Return x54, Return x50, Return x46, Return x42)) | ||
| x | ||
| : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) |
32 changes: 32 additions & 0 deletions
32
src/Specific/montgomery32_2e226m5_8limbs/fesubDisplay.log.expected
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, | ||
| Interp-η | ||
| (λ var : Syntax.base_type → Type, | ||
| λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, | ||
| uint32_t x33, uint8_t/*bool*/ x34 = subborrow_u32(0x0, x5, x19); | ||
| uint32_t x36, uint8_t/*bool*/ x37 = subborrow_u32(x34, x7, x21); | ||
| uint32_t x39, uint8_t/*bool*/ x40 = subborrow_u32(x37, x9, x23); | ||
| uint32_t x42, uint8_t/*bool*/ x43 = subborrow_u32(x40, x11, x25); | ||
| uint32_t x45, uint8_t/*bool*/ x46 = subborrow_u32(x43, x13, x27); | ||
| uint32_t x48, uint8_t/*bool*/ x49 = subborrow_u32(x46, x15, x29); | ||
| uint32_t x51, uint8_t/*bool*/ x52 = subborrow_u32(x49, x17, x31); | ||
| uint32_t x54, uint8_t/*bool*/ x55 = subborrow_u32(x52, x16, x30); | ||
| uint32_t x56 = cmovznz32(x55, 0x0, 0xffffffff); | ||
| uint32_t x57 = (x56 & 0xfffffffb); | ||
| uint32_t x59, uint8_t/*bool*/ x60 = addcarryx_u32(0x0, x33, x57); | ||
| uint32_t x61 = (x56 & 0xffffffff); | ||
| uint32_t x63, uint8_t/*bool*/ x64 = addcarryx_u32(x60, x36, x61); | ||
| uint32_t x65 = (x56 & 0xffffffff); | ||
| uint32_t x67, uint8_t/*bool*/ x68 = addcarryx_u32(x64, x39, x65); | ||
| uint32_t x69 = (x56 & 0xffffffff); | ||
| uint32_t x71, uint8_t/*bool*/ x72 = addcarryx_u32(x68, x42, x69); | ||
| uint32_t x73 = (x56 & 0xffffffff); | ||
| uint32_t x75, uint8_t/*bool*/ x76 = addcarryx_u32(x72, x45, x73); | ||
| uint32_t x77 = (x56 & 0xffffffff); | ||
| uint32_t x79, uint8_t/*bool*/ x80 = addcarryx_u32(x76, x48, x77); | ||
| uint32_t x81 = (x56 & 0xffffffff); | ||
| uint32_t x83, uint8_t/*bool*/ x84 = addcarryx_u32(x80, x51, x81); | ||
| uint8_t x85 = ((uint8_t)x56 & 0x3); | ||
| uint32_t x87, uint8_t/*bool*/ _ = addcarryx_u32(x84, x54, x85); | ||
| (Return x87, Return x83, Return x79, Return x75, Return x71, Return x67, Return x63, Return x59)) | ||
| (x, x0)%core | ||
| : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) |
439 changes: 439 additions & 0 deletions
439
src/Specific/montgomery32_2e230m27_8limbs/femulDisplay.log.expected
Large diffs are not rendered by default.
Oops, something went wrong.
32 changes: 32 additions & 0 deletions
32
src/Specific/montgomery32_2e230m27_8limbs/feoppDisplay.log.expected
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, | ||
| Interp-η | ||
| (λ var : Syntax.base_type → Type, | ||
| λ '(x13, x14, x12, x10, x8, x6, x4, x2)%core, | ||
| uint32_t x16, uint8_t/*bool*/ x17 = subborrow_u32(0x0, 0x0, x2); | ||
| uint32_t x19, uint8_t/*bool*/ x20 = subborrow_u32(x17, 0x0, x4); | ||
| uint32_t x22, uint8_t/*bool*/ x23 = subborrow_u32(x20, 0x0, x6); | ||
| uint32_t x25, uint8_t/*bool*/ x26 = subborrow_u32(x23, 0x0, x8); | ||
| uint32_t x28, uint8_t/*bool*/ x29 = subborrow_u32(x26, 0x0, x10); | ||
| uint32_t x31, uint8_t/*bool*/ x32 = subborrow_u32(x29, 0x0, x12); | ||
| uint32_t x34, uint8_t/*bool*/ x35 = subborrow_u32(x32, 0x0, x14); | ||
| uint32_t x37, uint8_t/*bool*/ x38 = subborrow_u32(x35, 0x0, x13); | ||
| uint32_t x39 = cmovznz32(x38, 0x0, 0xffffffff); | ||
| uint32_t x40 = (x39 & 0xffffffe5); | ||
| uint32_t x42, uint8_t/*bool*/ x43 = addcarryx_u32(0x0, x16, x40); | ||
| uint32_t x44 = (x39 & 0xffffffff); | ||
| uint32_t x46, uint8_t/*bool*/ x47 = addcarryx_u32(x43, x19, x44); | ||
| uint32_t x48 = (x39 & 0xffffffff); | ||
| uint32_t x50, uint8_t/*bool*/ x51 = addcarryx_u32(x47, x22, x48); | ||
| uint32_t x52 = (x39 & 0xffffffff); | ||
| uint32_t x54, uint8_t/*bool*/ x55 = addcarryx_u32(x51, x25, x52); | ||
| uint32_t x56 = (x39 & 0xffffffff); | ||
| uint32_t x58, uint8_t/*bool*/ x59 = addcarryx_u32(x55, x28, x56); | ||
| uint32_t x60 = (x39 & 0xffffffff); | ||
| uint32_t x62, uint8_t/*bool*/ x63 = addcarryx_u32(x59, x31, x60); | ||
| uint32_t x64 = (x39 & 0xffffffff); | ||
| uint32_t x66, uint8_t/*bool*/ x67 = addcarryx_u32(x63, x34, x64); | ||
| uint8_t x68 = ((uint8_t)x39 & 0x3f); | ||
| uint32_t x70, uint8_t/*bool*/ _ = addcarryx_u32(x67, x37, x68); | ||
| (Return x70, Return x66, Return x62, Return x58, Return x54, Return x50, Return x46, Return x42)) | ||
| x | ||
| : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) |
32 changes: 32 additions & 0 deletions
32
src/Specific/montgomery32_2e230m27_8limbs/fesubDisplay.log.expected
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32, | ||
| Interp-η | ||
| (λ var : Syntax.base_type → Type, | ||
| λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, | ||
| uint32_t x33, uint8_t/*bool*/ x34 = subborrow_u32(0x0, x5, x19); | ||
| uint32_t x36, uint8_t/*bool*/ x37 = subborrow_u32(x34, x7, x21); | ||
| uint32_t x39, uint8_t/*bool*/ x40 = subborrow_u32(x37, x9, x23); | ||
| uint32_t x42, uint8_t/*bool*/ x43 = subborrow_u32(x40, x11, x25); | ||
| uint32_t x45, uint8_t/*bool*/ x46 = subborrow_u32(x43, x13, x27); | ||
| uint32_t x48, uint8_t/*bool*/ x49 = subborrow_u32(x46, x15, x29); | ||
| uint32_t x51, uint8_t/*bool*/ x52 = subborrow_u32(x49, x17, x31); | ||
| uint32_t x54, uint8_t/*bool*/ x55 = subborrow_u32(x52, x16, x30); | ||
| uint32_t x56 = cmovznz32(x55, 0x0, 0xffffffff); | ||
| uint32_t x57 = (x56 & 0xffffffe5); | ||
| uint32_t x59, uint8_t/*bool*/ x60 = addcarryx_u32(0x0, x33, x57); | ||
| uint32_t x61 = (x56 & 0xffffffff); | ||
| uint32_t x63, uint8_t/*bool*/ x64 = addcarryx_u32(x60, x36, x61); | ||
| uint32_t x65 = (x56 & 0xffffffff); | ||
| uint32_t x67, uint8_t/*bool*/ x68 = addcarryx_u32(x64, x39, x65); | ||
| uint32_t x69 = (x56 & 0xffffffff); | ||
| uint32_t x71, uint8_t/*bool*/ x72 = addcarryx_u32(x68, x42, x69); | ||
| uint32_t x73 = (x56 & 0xffffffff); | ||
| uint32_t x75, uint8_t/*bool*/ x76 = addcarryx_u32(x72, x45, x73); | ||
| uint32_t x77 = (x56 & 0xffffffff); | ||
| uint32_t x79, uint8_t/*bool*/ x80 = addcarryx_u32(x76, x48, x77); | ||
| uint32_t x81 = (x56 & 0xffffffff); | ||
| uint32_t x83, uint8_t/*bool*/ x84 = addcarryx_u32(x80, x51, x81); | ||
| uint8_t x85 = ((uint8_t)x56 & 0x3f); | ||
| uint32_t x87, uint8_t/*bool*/ _ = addcarryx_u32(x84, x54, x85); | ||
| (Return x87, Return x83, Return x79, Return x75, Return x71, Return x67, Return x63, Return x59)) | ||
| (x, x0)%core | ||
| : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) |
Oops, something went wrong.