Merge pull request #108 from cryspen/jonas/update-model

Reflect code / backend changes in PV handshake model
cryspen · Apr 4, 2024 · 00d6718 · 00d6718
2 parents f612a59 + 46e6c32
commit 00d6718
Show file tree

Hide file tree

Showing 3 changed files with 231 additions and 2,398 deletions.
diff --git a/hax-driver.py b/hax-driver.py
@@ -74,6 +74,18 @@ def shell(command, expect=0, cwd=None, env={}):
     "into",
 ]
 
+cargo_hax_into_pv = [
+    "cargo",
+    "hax",
+    "-C",
+    "-p",
+    "bertie",
+    "--no-default-features",
+    "--features",
+    "hax-pv",
+    ";",
+    "into",
+]
 hax_env = {}
 
 if options.sub == "extract-fstar":
@@ -107,7 +119,7 @@ def shell(command, expect=0, cwd=None, env={}):
 elif options.sub == "extract-proverif":
     # The extract sub command.
     shell(
-        cargo_hax_into
+        cargo_hax_into_pv
         + [
             "-i",
             " ".join([