Merge pull request #92 from cryspen/lucas/driver-extract-handshake

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

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,