Panic freedom with F*

Cargo.toml

@@ -21,16 +21,14 @@ libcrux-kem = {version = "0.0.2-alpha.1", features = ["pre-verification", "kyber
 libcrux = { version = "0.0.2-alpha.1", features = [
     "rand",
 ]}
-hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
-hax-lib = { git = "https://github.com/hacspec/hax" }
+hax-lib = { git = "https://github.com/hacspec/hax/", branch= "pq11-fstar-libs" }
+
 
 [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]
 bertie = { path = ".", features = ["test_utils"] }

hax-driver.py

@@ -97,7 +97,7 @@ def shell(command, expect=0, cwd=None, env={}):
             "-**::non_hax::** -bertie::stream::**",
             "fstar",
             "--interfaces",
-            "+** +!bertie::tls13crypto::** +!bertie::tls13utils::**"
+            "+** +!bertie::tls13crypto::** +!bertie::tls13utils::** +!bertie::tls13cert::**"
         ],
         cwd=".",
         env=hax_env,

proofs/fstar/extraction/Bertie.Server.fst

@@ -3,11 +3,35 @@ module Bertie.Server
 open Core
 open FStar.Mul
 
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Bertie.Tls13utils in
+  ()
+
 let impl__ServerDB__new
       (server_name cert sk: Bertie.Tls13utils.t_Bytes)
       (psk_opt: Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
      = { f_server_name = server_name; f_cert = cert; f_sk = sk; f_psk_opt = psk_opt } <: t_ServerDB
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_1': Core.Fmt.t_Debug t_ServerDB
+
+let impl_1 = impl_1'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_2': Core.Clone.t_Clone t_ServerDB
+
+let impl_2 = impl_2'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_3': Core.Default.t_Default t_ServerDB
+
+let impl_3 = impl_3'
+
 let lookup_db
       (ciphersuite: Bertie.Tls13crypto.t_Algorithms)
       (db: t_ServerDB)
@@ -25,15 +49,22 @@ let lookup_db
         Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
     with
     | true, Core.Option.Option_Some ctkt, Core.Option.Option_Some (stkt, psk) ->
-      (match Bertie.Tls13utils.check_eq ctkt stkt with
+      (match Bertie.Tls13utils.check_eq ctkt stkt <: Core.Result.t_Result Prims.unit u8 with
         | Core.Result.Result_Ok _ ->
           let server:t_ServerInfo =
             {
-              f_cert = Core.Clone.f_clone db.f_cert;
-              f_sk = Core.Clone.f_clone db.f_sk;
+              f_cert
+              =
+              Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes
+                #FStar.Tactics.Typeclasses.solve
+                db.f_cert;
+              f_sk
+              =
+              Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve db.f_sk;
               f_psk_opt
               =
-              Core.Option.Option_Some (Core.Clone.f_clone psk)
+              Core.Option.Option_Some
+              (Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve psk)
               <:
               Core.Option.t_Option Bertie.Tls13utils.t_Bytes
             }
@@ -46,8 +77,12 @@ let lookup_db
     | false, _, _ ->
       let server:t_ServerInfo =
         {
-          f_cert = Core.Clone.f_clone db.f_cert;
-          f_sk = Core.Clone.f_clone db.f_sk;
+          f_cert
+          =
+          Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve db.f_cert;
+          f_sk
+          =
+          Core.Clone.f_clone #Bertie.Tls13utils.t_Bytes #FStar.Tactics.Typeclasses.solve db.f_sk;
           f_psk_opt = Core.Option.Option_None <: Core.Option.t_Option Bertie.Tls13utils.t_Bytes
         }
         <:

proofs/fstar/extraction/Bertie.Server.fsti

@@ -3,24 +3,45 @@ module Bertie.Server
 open Core
 open FStar.Mul
 
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Bertie.Tls13utils in
+  ()
+
+/// The Server Database
 type t_ServerDB = {
   f_server_name:Bertie.Tls13utils.t_Bytes;
   f_cert:Bertie.Tls13utils.t_Bytes;
   f_sk:Bertie.Tls13utils.t_Bytes;
   f_psk_opt:Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes)
 }
 
+/// Create a new server database.
+/// Note that this only holds one value at a time right now. #51
 val impl__ServerDB__new
       (server_name cert sk: Bertie.Tls13utils.t_Bytes)
       (psk_opt: Core.Option.t_Option (Bertie.Tls13utils.t_Bytes & Bertie.Tls13utils.t_Bytes))
     : Prims.Pure t_ServerDB Prims.l_True (fun _ -> Prims.l_True)
 
+/// Global server information.
 type t_ServerInfo = {
   f_cert:Bertie.Tls13utils.t_Bytes;
   f_sk:Bertie.Tls13utils.t_Bytes;
   f_psk_opt:Core.Option.t_Option Bertie.Tls13utils.t_Bytes
 }
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_1:Core.Fmt.t_Debug t_ServerDB
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_2:Core.Clone.t_Clone t_ServerDB
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+val impl_3:Core.Default.t_Default t_ServerDB
+
+/// Look up a server for the given `ciphersuite`.
+/// The function returns a server with the first algorithm it finds.
 val lookup_db
       (ciphersuite: Bertie.Tls13crypto.t_Algorithms)
       (db: t_ServerDB)