Skip to content

Commit

Permalink
update ocaml
Browse files Browse the repository at this point in the history
  • Loading branch information
@franziskuskiefer
franziskuskiefer committed Sep 6, 2022
1 parent 15b23fd commit fa26749
Show file tree
Hide file tree
Showing 24 changed files with 263 additions and 231 deletions.
85 changes: 41 additions & 44 deletions ocaml/ctypes.depend
View file

Large diffs are not rendered by default.

22 changes: 0 additions & 22 deletions ocaml/lib/EverCrypt_AutoConfig2_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,6 @@ module Bindings(F:Cstubs.FOREIGN) =
foreign "EverCrypt_AutoConfig2_has_rdrand" (void @-> (returning bool))
let everCrypt_AutoConfig2_has_avx512 =
foreign "EverCrypt_AutoConfig2_has_avx512" (void @-> (returning bool))
let everCrypt_AutoConfig2_wants_vale =
foreign "EverCrypt_AutoConfig2_wants_vale" (void @-> (returning bool))
let everCrypt_AutoConfig2_wants_hacl =
foreign "EverCrypt_AutoConfig2_wants_hacl" (void @-> (returning bool))
let everCrypt_AutoConfig2_wants_openssl =
foreign "EverCrypt_AutoConfig2_wants_openssl"
(void @-> (returning bool))
let everCrypt_AutoConfig2_wants_bcrypt =
foreign "EverCrypt_AutoConfig2_wants_bcrypt"
(void @-> (returning bool))
let everCrypt_AutoConfig2_recall =
foreign "EverCrypt_AutoConfig2_recall" (void @-> (returning void))
let everCrypt_AutoConfig2_init =
Expand Down Expand Up @@ -69,18 +59,6 @@ module Bindings(F:Cstubs.FOREIGN) =
let everCrypt_AutoConfig2_disable_avx512 =
foreign "EverCrypt_AutoConfig2_disable_avx512"
(void @-> (returning void))
let everCrypt_AutoConfig2_disable_vale =
foreign "EverCrypt_AutoConfig2_disable_vale"
(void @-> (returning void))
let everCrypt_AutoConfig2_disable_hacl =
foreign "EverCrypt_AutoConfig2_disable_hacl"
(void @-> (returning void))
let everCrypt_AutoConfig2_disable_openssl =
foreign "EverCrypt_AutoConfig2_disable_openssl"
(void @-> (returning void))
let everCrypt_AutoConfig2_disable_bcrypt =
foreign "EverCrypt_AutoConfig2_disable_bcrypt"
(void @-> (returning void))
let everCrypt_AutoConfig2_has_vec128 =
foreign "EverCrypt_AutoConfig2_has_vec128" (void @-> (returning bool))
let everCrypt_AutoConfig2_has_vec256 =
Expand Down
55 changes: 12 additions & 43 deletions ocaml/lib/EverCrypt_Hash_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,52 +16,21 @@ module Bindings(F:Cstubs.FOREIGN) =
type everCrypt_Hash_alg13 = spec_Hash_Definitions_hash_alg
let everCrypt_Hash_alg13 =
typedef spec_Hash_Definitions_hash_alg "EverCrypt_Hash_alg13"
type everCrypt_Hash_state_s_tags = Unsigned.UInt8.t
let everCrypt_Hash_state_s_tags =
typedef uint8_t "EverCrypt_Hash_state_s_tags"
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_MD5_s =
Unsigned.UInt8.of_int 0
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_SHA1_s =
Unsigned.UInt8.of_int 1
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_SHA2_224_s =
Unsigned.UInt8.of_int 2
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_SHA2_256_s =
Unsigned.UInt8.of_int 3
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_SHA2_384_s =
Unsigned.UInt8.of_int 4
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_SHA2_512_s =
Unsigned.UInt8.of_int 5
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_Blake2S_s =
Unsigned.UInt8.of_int 6
let everCrypt_Hash_state_s_tags_EverCrypt_Hash_Blake2B_s =
Unsigned.UInt8.of_int 7
type state_s_tags = Unsigned.UInt8.t
let state_s_tags = typedef uint8_t "state_s_tags"
let state_s_tags_MD5_s = Unsigned.UInt8.of_int 0
let state_s_tags_SHA1_s = Unsigned.UInt8.of_int 1
let state_s_tags_SHA2_224_s = Unsigned.UInt8.of_int 2
let state_s_tags_SHA2_256_s = Unsigned.UInt8.of_int 3
let state_s_tags_SHA2_384_s = Unsigned.UInt8.of_int 4
let state_s_tags_SHA2_512_s = Unsigned.UInt8.of_int 5
let state_s_tags_Blake2S_s = Unsigned.UInt8.of_int 6
let state_s_tags_Blake2S_128_s = Unsigned.UInt8.of_int 7
let state_s_tags_Blake2B_s = Unsigned.UInt8.of_int 8
let state_s_tags_Blake2B_256_s = Unsigned.UInt8.of_int 9
type everCrypt_Hash_state_s = [ `everCrypt_Hash_state_s ] structure
let (everCrypt_Hash_state_s : [ `everCrypt_Hash_state_s ] structure typ)
= structure "EverCrypt_Hash_state_s_s"
let everCrypt_Hash_state_s_tag =
field everCrypt_Hash_state_s "tag" everCrypt_Hash_state_s_tags
type everCrypt_Hash_state_s_val = [ `anonymous ] union
let (everCrypt_Hash_state_s_val : [ `anonymous ] union typ) = union ""
let everCrypt_Hash_state_s_val_case_MD5_s =
field everCrypt_Hash_state_s_val "case_MD5_s" (ptr uint32_t)
let everCrypt_Hash_state_s_val_case_SHA1_s =
field everCrypt_Hash_state_s_val "case_SHA1_s" (ptr uint32_t)
let everCrypt_Hash_state_s_val_case_SHA2_224_s =
field everCrypt_Hash_state_s_val "case_SHA2_224_s" (ptr uint32_t)
let everCrypt_Hash_state_s_val_case_SHA2_256_s =
field everCrypt_Hash_state_s_val "case_SHA2_256_s" (ptr uint32_t)
let everCrypt_Hash_state_s_val_case_SHA2_384_s =
field everCrypt_Hash_state_s_val "case_SHA2_384_s" (ptr uint64_t)
let everCrypt_Hash_state_s_val_case_SHA2_512_s =
field everCrypt_Hash_state_s_val "case_SHA2_512_s" (ptr uint64_t)
let everCrypt_Hash_state_s_val_case_Blake2S_s =
field everCrypt_Hash_state_s_val "case_Blake2S_s" (ptr uint32_t)
let everCrypt_Hash_state_s_val_case_Blake2B_s =
field everCrypt_Hash_state_s_val "case_Blake2B_s" (ptr uint64_t)
let _ = seal everCrypt_Hash_state_s_val
let everCrypt_Hash_state_s_u =
field everCrypt_Hash_state_s "" everCrypt_Hash_state_s_val
let _ = seal everCrypt_Hash_state_s
let everCrypt_Hash_alg_of_state =
foreign "EverCrypt_Hash_alg_of_state"
((ptr everCrypt_Hash_state_s) @->
Expand Down
13 changes: 0 additions & 13 deletions ocaml/lib/EverCrypt_StaticConfig_bindings.ml
View file

This file was deleted.

16 changes: 0 additions & 16 deletions ocaml/lib/EverCrypt_Vale_bindings.ml
View file

This file was deleted.

6 changes: 3 additions & 3 deletions ocaml/lib/Hacl_Bignum256_32_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_GenericField32_applied =
(Hacl_GenericField32_bindings.Bindings)(Hacl_GenericField32_stubs)
open Hacl_GenericField32_applied
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_Bignum256_32_add =
foreign "Hacl_Bignum256_32_add"
((ptr uint32_t) @->
Expand Down
17 changes: 3 additions & 14 deletions ocaml/lib/Hacl_Bignum256_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_Bignum256_add =
foreign "Hacl_Bignum256_add"
((ptr uint64_t) @->
Expand Down Expand Up @@ -47,20 +50,6 @@ module Bindings(F:Cstubs.FOREIGN) =
foreign "Hacl_Bignum256_mod_inv_prime_vartime"
((ptr uint64_t) @->
((ptr uint64_t) @-> ((ptr uint64_t) @-> (returning bool))))
type hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 =
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 ] structure
let (hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 :
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 ] structure typ) =
structure "Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_s"
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_len =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "len" uint32_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_n =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "n" (ptr uint64_t)
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_mu =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "mu" uint64_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_r2 =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "r2" (ptr uint64_t)
let _ = seal hacl_Bignum_MontArithmetic_bn_mont_ctx_u64
let hacl_Bignum256_mont_ctx_init =
foreign "Hacl_Bignum256_mont_ctx_init"
((ptr uint64_t) @->
Expand Down
6 changes: 3 additions & 3 deletions ocaml/lib/Hacl_Bignum32_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_GenericField32_applied =
(Hacl_GenericField32_bindings.Bindings)(Hacl_GenericField32_stubs)
open Hacl_GenericField32_applied
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_Bignum32_add =
foreign "Hacl_Bignum32_add"
(uint32_t @->
Expand Down
6 changes: 3 additions & 3 deletions ocaml/lib/Hacl_Bignum4096_32_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_GenericField32_applied =
(Hacl_GenericField32_bindings.Bindings)(Hacl_GenericField32_stubs)
open Hacl_GenericField32_applied
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_Bignum4096_32_add =
foreign "Hacl_Bignum4096_32_add"
((ptr uint32_t) @->
Expand Down
6 changes: 3 additions & 3 deletions ocaml/lib/Hacl_Bignum4096_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_Bignum256_applied =
(Hacl_Bignum256_bindings.Bindings)(Hacl_Bignum256_stubs)
open Hacl_Bignum256_applied
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_Bignum4096_add =
foreign "Hacl_Bignum4096_add"
((ptr uint64_t) @->
Expand Down
6 changes: 3 additions & 3 deletions ocaml/lib/Hacl_Bignum64_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_Bignum256_applied =
(Hacl_Bignum256_bindings.Bindings)(Hacl_Bignum256_stubs)
open Hacl_Bignum256_applied
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_Bignum64_add =
foreign "Hacl_Bignum64_add"
(uint32_t @->
Expand Down
28 changes: 28 additions & 0 deletions ocaml/lib/Hacl_Bignum_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,4 +254,32 @@ module Bindings(F:Cstubs.FOREIGN) =
(uint32_t @->
((ptr uint64_t) @->
((ptr uint64_t) @-> (returning void))))))))
type hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 =
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 ] structure
let (hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 :
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 ] structure typ) =
structure "Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_s"
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_len =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "len" uint32_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_n =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "n" (ptr uint32_t)
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_mu =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "mu" uint32_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_r2 =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "r2" (ptr uint32_t)
let _ = seal hacl_Bignum_MontArithmetic_bn_mont_ctx_u32
type hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 =
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 ] structure
let (hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 :
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 ] structure typ) =
structure "Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_s"
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_len =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "len" uint32_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_n =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "n" (ptr uint64_t)
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_mu =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "mu" uint64_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_r2 =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 "r2" (ptr uint64_t)
let _ = seal hacl_Bignum_MontArithmetic_bn_mont_ctx_u64
end
17 changes: 3 additions & 14 deletions ocaml/lib/Hacl_GenericField32_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
type hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 =
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 ] structure
let (hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 :
[ `hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 ] structure typ) =
structure "Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_s"
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_len =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "len" uint32_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_n =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "n" (ptr uint32_t)
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_mu =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "mu" uint32_t
let hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_r2 =
field hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 "r2" (ptr uint32_t)
let _ = seal hacl_Bignum_MontArithmetic_bn_mont_ctx_u32
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_GenericField32_field_modulus_check =
foreign "Hacl_GenericField32_field_modulus_check"
(uint32_t @-> ((ptr uint32_t) @-> (returning bool)))
Expand Down
6 changes: 3 additions & 3 deletions ocaml/lib/Hacl_GenericField64_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ open Ctypes
module Bindings(F:Cstubs.FOREIGN) =
struct
open F
module Hacl_Bignum256_applied =
(Hacl_Bignum256_bindings.Bindings)(Hacl_Bignum256_stubs)
open Hacl_Bignum256_applied
module Hacl_Bignum_applied =
(Hacl_Bignum_bindings.Bindings)(Hacl_Bignum_stubs)
open Hacl_Bignum_applied
let hacl_GenericField64_field_modulus_check =
foreign "Hacl_GenericField64_field_modulus_check"
(uint32_t @-> ((ptr uint64_t) @-> (returning bool)))
Expand Down
3 changes: 3 additions & 0 deletions ocaml/lib/Hacl_Hash_Blake2_bindings.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,9 @@ module Bindings(F:Cstubs.FOREIGN) =
Unsigned.UInt8.of_int 1
let hacl_Impl_Blake2_Core_m_spec_Hacl_Impl_Blake2_Core_M256 =
Unsigned.UInt8.of_int 2
let hacl_Hash_Core_Blake2_init_blake2s_32 =
foreign "Hacl_Hash_Core_Blake2_init_blake2s_32"
((ptr uint32_t) @-> (returning uint64_t))
let hacl_Hash_Core_Blake2_update_blake2s_32 =
foreign "Hacl_Hash_Core_Blake2_update_blake2s_32"
((ptr uint32_t) @->
Expand Down
Loading

0 comments on commit fa26749

Please sign in to comment.