feat(hax): add extract-handshake to the driver

cryspen · Mar 4, 2024 · 842e0dd · 842e0dd
1 parent 99726ee
commit 842e0dd
Showing 1 changed file with 17 additions and 0 deletions.
diff --git a/hax-driver.py b/hax-driver.py
@@ -35,6 +35,7 @@ def shell(command, expect=0, cwd=None, env={}):
     help="Extract and typecheck F* etc. from the Bertie Rust code.",
 )
 extract_parser = sub_parser.add_parser("extract")
+extract_parser = sub_parser.add_parser("extract-handshake")
 
 typecheck_parser = sub_parser.add_parser("typecheck")
 typecheck_parser.add_argument(
@@ -78,6 +79,22 @@ def shell(command, expect=0, cwd=None, env={}):
             "-i",
             "-**::non_hax::** -bertie::stream::**",
             "fstar",
+            "--interfaces",
+            "+**"
+        ],
+        cwd=".",
+        env=hax_env,
+    )
+elif options.sub == "extract-handshake":
+    # The extract sub command.
+    shell(
+        cargo_hax_into
+        + [
+            "-i",
+            "-** +~bertie::tls13handshake::**",
+            "fstar",
+            "--interfaces",
+            "+!** +bertie::tls13handshake::**"
         ],
         cwd=".",
         env=hax_env,