From 842e0ddbe01ff6346483ea7955b9af6febc9857a Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Tue, 6 Feb 2024 15:50:47 +0100
Subject: [PATCH] feat(hax): add `extract-handshake` to the driver

---
 hax-driver.py | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/hax-driver.py b/hax-driver.py
index b21ddeb9..dcaff432 100755
--- 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,