fix mulx argument order using sed, test feadd, femul (fails due to #234)

5 files changed, 108 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 133737812..c684d4243 100644
--- a/Makefile
+++ b/Makefile
@@ -177,6 +177,12 @@ third_party/openssl-nistp256c64/measure:  third_party/openssl-nistp256c64/compil
 third_party/openssl-nistp256c64/measurements.txt: third_party/openssl-nistp256c64/measure
 	./capture.sh third_party/openssl-nistp256c64 65535
 
+src/Specific/NISTP256/AMD64/test/feadd_test: src/Specific/NISTP256/AMD64/compiler.sh src/Specific/NISTP256/AMD64/feadd.c liblow/cmovznz.c src/Specific/NISTP256/AMD64/test/feadd_test.c liblow/cmovznz.c
+	src/Specific/NISTP256/AMD64/compiler.sh -o src/Specific/NISTP256/AMD64/test/feadd_test src/Specific/NISTP256/AMD64/feadd.c -I liblow -I src/Specific/NISTP256/AMD64/ src/Specific/NISTP256/AMD64/test/feadd_test.c liblow/cmovznz.c
+
+src/Specific/NISTP256/AMD64/test/femul_test: src/Specific/NISTP256/AMD64/compiler.sh src/Specific/NISTP256/AMD64/femul.c liblow/cmovznz.c src/Specific/NISTP256/AMD64/test/femul_test.c liblow/cmovznz.c
+	src/Specific/NISTP256/AMD64/compiler.sh -o src/Specific/NISTP256/AMD64/test/femul_test src/Specific/NISTP256/AMD64/femul.c -I liblow -I src/Specific/NISTP256/AMD64/ src/Specific/NISTP256/AMD64/test/femul_test.c liblow/cmovznz.c
+
 src/Specific/NISTP256/AMD64/measure:  src/Specific/NISTP256/AMD64/bench_madd.c src/Specific/NISTP256/AMD64/feadd.c src/Specific/NISTP256/AMD64/femul.c src/Specific/NISTP256/AMD64/fenz.c src/Specific/NISTP256/AMD64/feopp.c src/Specific/NISTP256/AMD64/fesub.c src/Specific/NISTP256/AMD64/p256_jacobian_add_affine.c liblow/cmovznz.c measure.c src/Specific/NISTP256/AMD64/compiler.sh measure.c
 	src/Specific/NISTP256/AMD64/compiler.sh -o src/Specific/NISTP256/AMD64/measure src/Specific/NISTP256/AMD64/*.c -I src/Specific/NISTP256/AMD64/ measure.c -D UUT=bench_madd -I liblow liblow/*.c
 
@@ -192,8 +198,10 @@ src/Specific/NISTP256/AMD64/icc/measurements.txt: src/Specific/NISTP256/AMD64/ic
 bench: src/Specific/X25519/C64/measurements.txt third_party/openssl-curve25519/measurements.txt src/Specific/NISTP256/AMD64/measurements.txt src/Specific/NISTP256/AMD64/icc/measurements.txt third_party/openssl-nistz256/measurements.txt third_party/openssl-nistp256c64/measurements.txt
 	head -999999 $?
 
-test: src/Specific/X25519/C64/test
+test: src/Specific/X25519/C64/test src/Specific/NISTP256/AMD64/test/feadd_test src/Specific/NISTP256/AMD64/test/femul_test
 	src/Specific/X25519/C64/test
+	src/Specific/NISTP256/AMD64/test/feadd_test
+	src/Specific/NISTP256/AMD64/test/femul_test
 
 clean::
 	rm -f Makefile.coq
diff --git a/extract-function.sh b/extract-function.sh
index c4345674f..c00ae274b 100755
--- a/extract-function.sh
+++ b/extract-function.sh
@@ -62,10 +62,11 @@ while IFS= read -r line; do
       case "$show" in
         true)
           lines=$((lines+1))
-          echo "{ $line" | \
-            sed s':^\([^,]*\) \([^, ]*\)\(\s*\),\(.*\)\(mulx.*\))\([; ]*\)$:\1 \2\3;\4_\5, \&\2)\6:' | \
+          line="$(echo "$line" | \
+            sed s':^\([^,]*\),\(\s*\)\([^ ]*\) \([^ ]*\)\(.*\)\(mulx.*\))\([; ]*\)$: \3 \4;\2\1\5_\6, \&\4)\7:' | \
             sed s':^\([^,]*\) \([^, ]*\)\(\s*\),\(.*\)\(addcarryx.*\))\([; ]*\)$:\1 \2\3;\4_\5, \&\2)\6:' | \
-            sed s':^\([^,]*\) \([^, ]*\)\(\s*\),\(.*\)\(subborrow.*\))\([; ]*\)$:\1 \2\3;\4_\5, \&\2)\6:'
+            sed s':^\([^,]*\) \([^, ]*\)\(\s*\),\(.*\)\(subborrow.*\))\([; ]*\)$:\1 \2\3;\4_\5, \&\2)\6:')"
+          echo "{ $line"
           ;;
       esac
       ;;
diff --git a/src/Specific/NISTP256/AMD64/measurements.txt b/src/Specific/NISTP256/AMD64/measurements.txt
index 1ec583018..d4dca8e54 100644
--- a/src/Specific/NISTP256/AMD64/measurements.txt
+++ b/src/Specific/NISTP256/AMD64/measurements.txt
@@ -1,2 +1,2 @@
 1576	ashryn-noht-notb-noac-broadwell	2.60ghz	7.1.1	cac291e0
-1688	ashryn-noht-notb-ac-broadwell	2.50ghz	7.1.1	d7ad9528
+1640	ashryn-noht-notb-ac-broadwell	2.50ghz	7.1.1	6c558bd2
diff --git a/src/Specific/NISTP256/AMD64/test/feadd_test.c b/src/Specific/NISTP256/AMD64/test/feadd_test.c
new file mode 100644
index 000000000..3cdd1fd60
--- /dev/null
+++ b/src/Specific/NISTP256/AMD64/test/feadd_test.c
@@ -0,0 +1,46 @@
+#include <stdint.h>
+#include <inttypes.h>
+#include <stdio.h>
+#include "feadd.h"
+
+static int check(uint64_t out[4], uint64_t ref[4]) {
+  return out[0] == ref[0] && out[1] == ref[1] && out[2] == ref[2] && out[3] == ref[3];
+}
+
+int main() {
+  {
+    uint64_t out[4] = {0};
+    uint64_t in1[4] = {0, 0, 0, 1};
+    uint64_t in2[4] = {0, 0, 0, 1};
+    uint64_t ref[4] = {0, 0, 0, 2};
+    feadd(out, in1[0], in1[1], in1[2], in1[3], in2[0], in2[1], in2[2], in2[3]);
+    if (!check(out, ref)) return 1;
+  }
+  {
+    uint64_t out[4] = {0};
+    uint64_t in1[4] = {0, 0, 0, 0};
+    uint64_t in2[4] = {0, 0, 0, 0};
+    uint64_t ref[4] = {0, 0, 0, 0};
+    feadd(out, in1[0], in1[1], in1[2], in1[3], in2[0], in2[1], in2[2], in2[3]);
+    if (!check(out, ref)) return 2;
+  }
+  {
+    uint64_t out[4] = {0};
+    uint64_t in1[4] = {0xffffffff00000001, 0x0000000000000000, 0x00000000ffffffff, 0xfffffffffffffffe}; // p256-1
+    uint64_t in2[4] = {0, 0, 0, 1};
+    uint64_t ref[4] = {0, 0, 0, 0};
+    feadd(out, in1[0], in1[1], in1[2], in1[3], in2[0], in2[1], in2[2], in2[3]);
+    if (!check(out, ref)) return 3;
+  }
+  {
+    uint64_t out[4] = {0};
+    uint64_t in1[4] = {0xffffffff00000001, 0x0000000000000000, 0x00000000ffffffff, 0xfffffffffffffffe}; // p256-1
+    uint64_t in2[4] = {0, 0, 0, 7};
+    uint64_t ref[4] = {0, 0, 0, 6};
+    feadd(out, in1[0], in1[1], in1[2], in1[3], in2[0], in2[1], in2[2], in2[3]);
+    if (!check(out, ref)) return 4;
+  }
+  
+  //printf("0x%016" PRIx64 " 0x%016" PRIx64 " 0x%016" PRIx64 " 0x%016" PRIx64 "\n", out[0], out[1], out[2], out[3]);
+  //printf("((((((0x%016" PRIx64 "<<64)+ 0x%016" PRIx64 ")<<64)+ 0x%016" PRIx64 ")<<64)+ 0x%016" PRIx64 ")\n", out[0], out[1], out[2], out[3]);
+}
diff --git a/src/Specific/NISTP256/AMD64/test/femul_test.c b/src/Specific/NISTP256/AMD64/test/femul_test.c
new file mode 100644
index 000000000..9519399e0
--- /dev/null
+++ b/src/Specific/NISTP256/AMD64/test/femul_test.c
@@ -0,0 +1,48 @@
+#include <stdint.h>
+#include <inttypes.h>
+#include <stdio.h>
+#include "femul.h"
+
+// all arrays big-endian
+static uint64_t Rmodm[4] = {0xfffffffe, 0xffffffffffffffff, 0xffffffff00000000, 0x0000000000000001};
+
+int main() {
+  uint64_t out[4] = {0};
+  if ( femul(out,
+        Rmodm[0], Rmodm[1], Rmodm[2], Rmodm[3],
+        Rmodm[0], Rmodm[1], Rmodm[2], Rmodm[3]), 
+      ! (out[0]   == Rmodm[0]
+        && out[1] == Rmodm[1]
+        && out[2] == Rmodm[2]
+        && out[3] == Rmodm[3]
+        )) { return 1; }
+  if ( femul(out,
+        0, 0, 0, 0,
+        Rmodm[0], Rmodm[1], Rmodm[2], Rmodm[3]), 
+      ! (out[0]   == 0
+        && out[1] == 0
+        && out[2] == 0
+        && out[3] == 0
+        )) { return 2; }
+  if ( femul(out,
+        0, 0, 0, 1,
+        0, 0, 0, 1), 
+      ! (out[0]   == 0xfffffffe00000003 // R^-1
+        && out[1] == 0xfffffffd00000002
+        && out[2] == 0x00000001fffffffe
+        && out[3] == 0x0000000300000000
+        )) { return 3; }
+  if ( femul(out,
+        0, 0, 0, 1,
+        0x4fffffffd, 0xfffffffffffffffe, 0xfffffffbffffffff, 0x0000000000000003),  // R^2
+      ! (out[0]   == Rmodm[0]
+        && out[1] == Rmodm[1]
+        && out[2] == Rmodm[2]
+        && out[3] == Rmodm[3]
+        )) { return 4; }
+
+
+  //printf("0x%016" PRIx64 " 0x%016" PRIx64 " 0x%016" PRIx64 " 0x%016" PRIx64 "\n", out[0], out[1], out[2], out[3]);
+  //printf("((((((0x%016" PRIx64 "<<64)+ 0x%016" PRIx64 ")<<64)+ 0x%016" PRIx64 ")<<64)+ 0x%016" PRIx64 ")\n", out[0], out[1], out[2], out[3]);
+  return 0;
+}