Bertie Lax Typechecking

.envrc

@@ -0,0 +1,5 @@
+use nix
+export HACL_HOME="/home/lucas/repos/hacl-star"
+export HAX_PROOF_LIBS_HOME="/home/lucas/repos/hax/latest-core/proof-libs/fstar"
+export HAX_LIBS_HOME="/home/lucas/repos/hax/latest-core/hax-lib/proofs/fstar/extraction"
+export FSTAR_HOME="/home/lucas/repos/hax/latest-core/proof-libs/fstar"

.github/workflows/hax.yml

@@ -47,4 +47,4 @@ jobs:
       - name: 🏃🏻‍♀️ Run hax extraction
         run: |
           eval $(opam env)
-          ./hax-driver.py extract
+          ./hax-driver.py extract-fstar

Cargo.toml

@@ -18,14 +18,15 @@ rand = "0.8.0"
 hex = "0.4.3"
 tracing = "0.1"
 libcrux = { version = "0.0.2-pre.2", features = ["rand"] }
-hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
-
+hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true}
+hax-lib = { git = "https://github.com/hacspec/hax" }
 
 [features]
 default = ["api"]
 test_utils = []
 secret_integers = []
 api = []             # The streaming Rust API that everyone should use but is not hacspec.
+hax-fstar = ["dep:hax-lib-macros"]
 hax-pv = ["dep:hax-lib-macros"]
 
 [dev-dependencies]

default.nix

@@ -0,0 +1,14 @@
+let
+  pkgs = import <nixpkgs> {};
+in
+  pkgs.mkShell {
+    packages = with pkgs; [
+      python3
+      rustup
+    ];
+
+    HACL_HOME = "/home/lucas/repos/hacl-star";
+    HAX_PROOF_LIBS_HOME = "/home/lucas/repos/hax/latest-core/proof-libs/fstar";
+    HAX_LIBS_HOME = "/home/lucas/repos/hax/latest-core/hax-lib/proofs/fstar/extraction";
+    FSTAR_HOME = "/home/lucas/repos/hax/latest-core/proof-libs/fstar";
+  }

hax-driver.py

@@ -34,7 +34,7 @@ def shell(command, expect=0, cwd=None, env={}):
     dest="sub",
     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-fstar")
 extract_proverif_parser = sub_parser.add_parser("extract-proverif")
 typecheck_parser = sub_parser.add_parser("typecheck")
 patch_proverif_parser = sub_parser.add_parser("patch-proverif")
@@ -67,13 +67,16 @@ def shell(command, expect=0, cwd=None, env={}):
     "-C",
     "-p",
     "bertie",
+    "-p",
+    "rand_core",
     "--no-default-features",
     ";",
     "into",
 ]
+
 hax_env = {}
 
-if options.sub == "extract":
+if options.sub == "extract-fstar":
     # The extract sub command.
     shell(
         cargo_hax_into
@@ -82,7 +85,7 @@ def shell(command, expect=0, cwd=None, env={}):
             "-**::non_hax::** -bertie::stream::**",
             "fstar",
             "--interfaces",
-            "+**"
+            "+** +!bertie::tls13crypto::** +!bertie::tls13utils::**"
         ],
         cwd=".",
         env=hax_env,

proofs/fstar/README.md

@@ -0,0 +1,19 @@
+This directory holds the extracted F* code for the Bertie protocol layer.
+
+The `extraction` folder is generated by running `hax-driver.py extract-fstar`
+
+We then apply a patch to this folder for lax checking to obtain `extraction-lax`.
+
+This patch mainly performs the following fixes which will become unnecessary with future hax fixes:
+
+* Recursive functions are not produced with `let rec` in F*
+* IndexMut implementations need to implemented by hand in F*
+* Empty lists need type annotations in F*
+
+Finally, we edit the code in `extraction-lax` by hand to obtain panic-freedom proofs in `extraction-panic-free`.
+Eventually these hand-edits will be backported into Rust as pre- and post-conditions.
+
+
+
+
+