From ace8e78b301f99fea24c01c3f322cf1a98f9e03b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 3 Jul 2017 16:16:54 -0400 Subject: Fix display target --- src/Specific/NISTP256/AMD64/feoppDisplay.log | 19 +++++++++++++++++++ src/Specific/NISTP256/AMD64/feoppDisplay.v | 2 +- 2 files changed, 20 insertions(+), 1 deletion(-) (limited to 'src/Specific/NISTP256/AMD64') 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. -- cgit v1.2.3