From f82f804bde7674e325c4a8426e525e856708aba5 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Wed, 17 May 2017 13:26:43 -0400
Subject: [PATCH] Experimenting with extracting code

---
 .../OpenSSL/poly1305/x64/Makefile             | 37 +++++++++++++++++++
 .../OpenSSL/poly1305/x64/poly1305.vaf         | 21 ++++++++++-
 2 files changed, 56 insertions(+), 2 deletions(-)
 create mode 100644 src/thirdPartyPorts/OpenSSL/poly1305/x64/Makefile

diff --git a/src/thirdPartyPorts/OpenSSL/poly1305/x64/Makefile b/src/thirdPartyPorts/OpenSSL/poly1305/x64/Makefile
new file mode 100644
index 00000000..91ed46ff
--- /dev/null
+++ b/src/thirdPartyPorts/OpenSSL/poly1305/x64/Makefile
@@ -0,0 +1,37 @@
+REPO_BASE=../../../../../
+ARCH=$(REPO_BASE)/tools/Vale/test
+
+INCLUDE=--include $(ARCH) --include $(REPO_BASE)/src/crypto/poly1305/x64/
+Z3_OPTIONS=--z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 --z3cliopt smt.arith.nl=false
+FSTAR_OPTIONS=$(INCLUDE) $(Z3_OPTIONS) --hint_info --lax
+VALE=mono $(REPO_BASE)/bin/vale.exe 
+
+# For simplified Makefiles, define FSTAR_HOME, then include the file below.
+include $(FSTAR_HOME)/examples/Makefile.include
+
+all: ocaml
+
+include $(FSTAR_HOME)/ulib/ml/Makefile.include
+
+$(ARCH)/decls.fst: $(ARCH)/decls.vaf
+	$(VALE) -in $(ARCH)/decls.vaf -fstarText -out $(ARCH)/decls.fst
+
+poly1305.fst: poly1305.vaf $(ARCH)/decls.vaf
+	$(VALE) -in poly1305.vaf -fstarText -out poly1305.fst
+
+poly1305.v: poly1305.fst $(ARCH)/decls.fst
+	fstar $(FSTAR_OPTIONS) poly1305.fst
+
+ocaml: out poly1305.fst
+	$(MAKE) -C $(ULIB_ML)
+	$(FSTAR) $(FSTAR_DEFAULT_ARGS) $(INCLUDE) --lax --odir out --codegen OCaml poly1305.fst
+	$(OCAMLOPT) out/Semantics.ml out/Decls.ml out/Vale.ml out/Poly1305.ml -o poly1305.exe
+	./poly1305.exe
+
+out:
+	mkdir -p out
+
+clean:
+	make -C $(ULIB_ML) clean
+	rm -rf out
+	rm -f *~
diff --git a/src/thirdPartyPorts/OpenSSL/poly1305/x64/poly1305.vaf b/src/thirdPartyPorts/OpenSSL/poly1305/x64/poly1305.vaf
index 92c63820..1b3dd44b 100644
--- a/src/thirdPartyPorts/OpenSSL/poly1305/x64/poly1305.vaf
+++ b/src/thirdPartyPorts/OpenSSL/poly1305/x64/poly1305.vaf
@@ -832,8 +832,7 @@ procedure{:timeLimitMultiplier 2} poly1305(
     Store64(ctx, r15, 128, Public, ctx_id);
 
     h := poly1305_impl(ctx, inp, len, r0, r1, h0, h1, h2, key_r, key_s, n, p, ctx_id, inp_id);
-
-    Store64(ctx, h0,  0, Public, ctx_id);
+Store64(ctx, h0,  0, Public, ctx_id);
     Store64(ctx, h1,  8, Public, ctx_id);
 
     Load64(h1,  ctx, 72, Public, ctx_id);
@@ -848,3 +847,21 @@ procedure{:timeLimitMultiplier 2} poly1305(
 }
 
 */
+
+#verbatim
+
+open Print
+open FStar.IO
+
+let print_poly1305 (p:printer) =
+  let poly_code = va_code_poly1305_multiply (OReg R8) (OReg R9) (OReg R10) (OReg R11) (OReg R13) (OReg R14) (OReg Rbx) (OReg Rbp) in
+  print_header p;
+  print_proc "poly1305" poly_code 0 p;
+  print_footer p
+
+let main =
+  print_poly1305 masm;
+  print_string "\n\n";
+  print_poly1305 gcc
+
+#endverbatim