diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-03 16:16:54 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-03 16:16:54 -0400 |
| commit | ace8e78b301f99fea24c01c3f322cf1a98f9e03b (patch) | |
| tree | c08212c0850df897b8dee3dd63b2dc8888663e6c /src/Specific/NISTP256/AMD64 | |
| parent | 0d21d15d37e5aabae6c9430b37b665743ed47b02 (diff) | |
Fix display target
Diffstat (limited to 'src/Specific/NISTP256/AMD64')
| -rw-r--r-- | src/Specific/NISTP256/AMD64/feoppDisplay.log | 19 | ||||
| -rw-r--r-- | src/Specific/NISTP256/AMD64/feoppDisplay.v | 2 |
2 files changed, 20 insertions, 1 deletions
diff --git a/src/Specific/NISTP256/AMD64/feoppDisplay.log b/src/Specific/NISTP256/AMD64/feoppDisplay.log index e69de29bb..211b2b863 100644 --- a/src/Specific/NISTP256/AMD64/feoppDisplay.log +++ b/src/Specific/NISTP256/AMD64/feoppDisplay.log @@ -0,0 +1,19 @@ +λ x : word64 * word64 * word64 * word64, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x5, x6, x4, x2)%core, + uint64_t x8, uint8_t x9 = subborrow_u64(0x0, 0x0, x2); + uint64_t x11, uint8_t x12 = subborrow_u64(x9, 0x0, x4); + uint64_t x14, uint8_t x15 = subborrow_u64(x12, 0x0, x6); + uint64_t x17, uint8_t x18 = subborrow_u64(x15, 0x0, x5); + uint64_t x19 = (uint64_t)cmovznz(x18, 0x0, 0xffffffffffffffffL); + uint64_t x20 = x19 & 0xffffffffffffffffL; + uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x8, x20); + uint64_t x24 = x19 & 0xffffffff; + uint64_t x26, uint8_t x27 = addcarryx_u64(x23, x11, x24); + uint64_t x29, uint8_t x30 = addcarryx_u64(x27, x14, 0x0); + uint64_t x31 = x19 & 0xffffffff00000001L; + uint64_t x33, uint8_t _ = addcarryx_u64(x30, x17, x31); + (Return x33, Return x29, Return x26, Return x22)) +x + : word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/feoppDisplay.v b/src/Specific/NISTP256/AMD64/feoppDisplay.v index af0987565..9075af2f2 100644 --- a/src/Specific/NISTP256/AMD64/feoppDisplay.v +++ b/src/Specific/NISTP256/AMD64/feoppDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.NISTP256.AMD64.IntegrationTestMontgomeryP256_Opp. +Require Import Crypto.Specific.NISTP256.AMD64.feopp. Require Import Crypto.Specific.IntegrationTestDisplayCommon. Check display opp. |