Crypto Primitives Abstraction Layer

engine/backends/proverif/proverif_backend.ml

@@ -10,6 +10,7 @@ include
       include On.Macro
       include On.Question_mark
       include On.Early_exit
+      include On.Slice
     end)
     (struct
       let backend = Diagnostics.Backend.ProVerif
@@ -30,6 +31,7 @@ module SubtypeToInputLanguage
           (* and type slice = Features.Off.slice *)
           (* and type raw_pointer = Features.Off.raw_pointer *)
             with type early_exit = Features.On.early_exit
+             and type slice = Features.On.slice
              and type question_mark = Features.On.question_mark
              and type macro = Features.On.macro
     (* and type as_pattern = Features.Off.as_pattern *)
@@ -61,7 +63,6 @@ struct
         let mutable_reference = reject
         let mutable_pointer = reject
         let reference = reject
-        let slice = reject
         let raw_pointer = reject
         let as_pattern = reject
         let nontrivial_lhs = reject
@@ -286,17 +287,6 @@ module Print = struct
           | TApp _ -> super#ty ctx ty
           | _ -> string "bitstring"
 
-      method! expr_app : expr -> expr list -> generic_value list fn =
-        fun f args _generic_args ->
-          let args =
-            separate_map
-              (comma ^^ break 1)
-              (print#expr_at Expr_App_arg >> group)
-              args
-          in
-          let f = print#expr_at Expr_App_f f |> group in
-          f ^^ iblock parens args
-
       method! literal : Generic_printer_base.literal_ctx -> literal fn =
         fun _ctx -> function
           | Int { value; negative; _ } ->

hax-lib-protocol/Cargo.toml

@@ -11,3 +11,4 @@ readme.workspace = true
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
+libcrux = "0.0.2-pre.2"

hax-lib-protocol/README.md

@@ -0,0 +1,19 @@
+# Hax Protocol Library
+This crate provides tools for protocol developers to write protcol
+specifications for hax.
+
+## Protocol Traits
+To hax, a protocol is a collection of communicating state
+machines. This module provides traits that describe parts of a state
+machine's behaviour, specifically it provides traits for creating an
+initial state, and for state transition behaviour when reading or
+writing a message.
+
+## Cryptographic Abstractions
+Beside message passing and state transitions, a protocol of course
+includes operations on the sent and received messages. For
+cryptographic protocols, these will be of a fairly restricted set of
+cryptoraphic primitive operations, which are provided in these
+cryptographic abstractions. This allows protocol authors to specify
+protocol party internal operations in a way that is easily accessible
+to hax.