Fix code-gen by unrolling loops and getting rid of empty for-loops

hacl-star · Apr 18, 2024 · e8bdd9e · e8bdd9e
1 parent 462c12c
commit e8bdd9e
Show file tree

Hide file tree

Showing 30 changed files with 177 additions and 37,302 deletions.
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-l: test
+all: test
 
 # Boilerplate
 # -----------
@@ -71,11 +71,12 @@ dist/Makefile.basic: $(filter-out %prims.krml,$(ALL_KRML_FILES))
 	  -add-include '<stdbool.h>' \
 	  -add-include '<string.h>' \
 	  -fparentheses \
+	  -funroll-loops 16 \
 	  -o libmerkletree.a \
 	  $(VALE_FLAGS) \
 	  -no-prefix 'MerkleTree' \
 	  -no-prefix 'MerkleTree.EverCrypt' \
-	  -bundle EverCrypt.Hash=EverCrypt,EverCrypt.*,Meta.*,Hacl.*,Vale.*,Spec.*,Lib.* \
+	  -bundle EverCrypt.Hash,EverCrypt,EverCrypt.*,Meta.*,Hacl.*,Vale.*,Spec.*,Lib.*[rename=EverCrypt_Hash] \
 	  -library EverCrypt.AutoConfig2 \
 	  -bundle 'MerkleTree+MerkleTree.Init+MerkleTree.EverCrypt+MerkleTree.Low+MerkleTree.Low.Serialization+MerkleTree.Low.Hashfunctions=MerkleTree.*[rename=MerkleTree]' \
 	  -bundle LowStar.* \

diff --git a/dist/EverCrypt_Hash.c b/dist/EverCrypt_Hash.c
diff --git a/dist/EverCrypt_Hash.h b/dist/EverCrypt_Hash.h
diff --git a/dist/LowStar.c b/dist/LowStar.c
diff --git a/dist/Makefile.include b/dist/Makefile.include
@@ -2,4 +2,4 @@ USER_TARGET=libmerkletree.a
 USER_CFLAGS=-DLib_IntVector_Intrinsics_vec256=void* -DLib_IntVector_Intrinsics_vec128=void*
 USER_C_FILES=
 ALL_C_FILES=EverCrypt_Hash.c LowStar.c MerkleTree.c
-ALL_H_FILES=EverCrypt_Hash.h MerkleTree.h internal/EverCrypt_Hash.h internal/LowStar.h internal/MerkleTree.h internal/Merkle_Krmllib.h
+ALL_H_FILES=MerkleTree.h internal/EverCrypt_Hash.h internal/LowStar.h internal/MerkleTree.h internal/Merkle_Krmllib.h
diff --git a/dist/MerkleTree.c b/dist/MerkleTree.c
diff --git a/dist/MerkleTree.h b/dist/MerkleTree.h
diff --git a/dist/internal/EverCrypt_Hash.h b/dist/internal/EverCrypt_Hash.h
diff --git a/dist/internal/LowStar.h b/dist/internal/LowStar.h
diff --git a/dist/internal/MerkleTree.h b/dist/internal/MerkleTree.h
diff --git a/dist/internal/Merkle_Krmllib.h b/dist/internal/Merkle_Krmllib.h
diff --git a/dist/libmerkletree.def b/dist/libmerkletree.def
@@ -2,31 +2,11 @@ LIBRARY libmerkletree
 
 EXPORTS
   LowStar_Vector_new_capacity
-  EverCrypt_Hash_string_of_alg
-  EverCrypt_Hash_uu___is_MD5_s
-  EverCrypt_Hash_uu___is_SHA1_s
-  EverCrypt_Hash_uu___is_SHA2_224_s
-  EverCrypt_Hash_uu___is_SHA2_256_s
-  EverCrypt_Hash_uu___is_SHA2_384_s
-  EverCrypt_Hash_uu___is_SHA2_512_s
-  EverCrypt_Hash_uu___is_SHA3_224_s
-  EverCrypt_Hash_uu___is_SHA3_256_s
-  EverCrypt_Hash_uu___is_SHA3_384_s
-  EverCrypt_Hash_uu___is_SHA3_512_s
-  EverCrypt_Hash_uu___is_Blake2S_s
-  EverCrypt_Hash_uu___is_Blake2S_128_s
-  EverCrypt_Hash_uu___is_Blake2B_s
-  EverCrypt_Hash_uu___is_Blake2B_256_s
-  EverCrypt_Hash_alg_of_state
   EverCrypt_Hash_create_in
-  EverCrypt_Hash_create
   EverCrypt_Hash_init
-  EverCrypt_Hash_update_multi_256
   EverCrypt_Hash_update_multi
-  EverCrypt_Hash_update_last
   EverCrypt_Hash_finish
   EverCrypt_Hash_free_
-  EverCrypt_Hash_copy
   LowStar_RVector_free_elems___uint8_t__uint32_t
   mt_init_hash
   mt_free_hash

diff --git a/hints/Lib.RawBuffer.fst.hints b/hints/Lib.RawBuffer.fst.hints
@@ -1,159 +1 @@
-[
-  "9��~�\u001bW<�nHQd�\f�",
-  [
-    [
-      "Lib.RawBuffer.blit",
-      1,
-      2,
-      1,
-      [
-        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
-        "equation_FStar.Monotonic.HyperStack.live_region",
-        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
-        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
-        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
-        "equation_LowStar.Buffer.trivial_preorder",
-        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
-        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8",
-        "int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
-        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
-        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
-        "primitive_Prims.op_LessThanOrEqual",
-        "projection_inverse_BoxBool_proj_0",
-        "projection_inverse_BoxInt_proj_0",
-        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
-        "refinement_interpretation_Tm_refine_45714303651d17b17626bf17b59ae2a7",
-        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
-        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
-        "typing_FStar.Monotonic.HyperStack.live_region",
-        "typing_FStar.UInt32.v", "typing_FStar.UInt8.t",
-        "typing_LowStar.Buffer.trivial_preorder",
-        "typing_LowStar.Monotonic.Buffer.frameOf"
-      ],
-      0,
-      "d28cccdbc7c64a05068a9a57758d9a1a"
-    ],
-    [
-      "Lib.RawBuffer.blit",
-      2,
-      2,
-      1,
-      [
-        "@MaxIFuel_assumption", "@query", "b2t_def",
-        "constructor_distinct_Lib.IntTypes.PUB",
-        "constructor_distinct_Lib.IntTypes.SEC",
-        "constructor_distinct_Lib.IntTypes.U8",
-        "equality_tok_Lib.IntTypes.PUB@tok",
-        "equality_tok_Lib.IntTypes.SEC@tok",
-        "equality_tok_Lib.IntTypes.U8@tok",
-        "equation_FStar.HyperStack.ST.equal_domains",
-        "equation_FStar.HyperStack.ST.equal_stack_domains",
-        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
-        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
-        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
-        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
-        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
-        "equation_LowStar.Buffer.buffer",
-        "equation_LowStar.Buffer.trivial_preorder",
-        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
-        "function_token_typing_Lib.IntTypes.byte_t",
-        "function_token_typing_Lib.IntTypes.uint8",
-        "function_token_typing_LowStar.Buffer.trivial_preorder",
-        "int_inversion", "int_typing",
-        "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
-        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
-        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
-        "lemma_FStar.Seq.Base.lemma_index_slice",
-        "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt8.uv_inv",
-        "lemma_Lib.IntTypes.v_injective",
-        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
-        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
-        "primitive_Prims.op_LessThanOrEqual",
-        "primitive_Prims.op_Subtraction",
-        "projection_inverse_BoxBool_proj_0",
-        "projection_inverse_BoxInt_proj_0",
-        "refinement_interpretation_Tm_refine_321725eb4d16bdb848c74e3894f7a159",
-        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
-        "refinement_interpretation_Tm_refine_45714303651d17b17626bf17b59ae2a7",
-        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
-        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
-        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
-        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
-        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
-        "refinement_interpretation_Tm_refine_f68569b7912e33ebde47e50e220f67a5",
-        "true_interp", "typing_FStar.Seq.Base.index",
-        "typing_FStar.UInt32.v", "typing_Lib.RawIntTypes.u8_from_UInt8",
-        "typing_LowStar.Buffer.trivial_preorder",
-        "typing_LowStar.Monotonic.Buffer.as_seq",
-        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
-      ],
-      0,
-      "c0b5c7c75bff63b448bfdce043269d53"
-    ],
-    [
-      "Lib.RawBuffer.lbytes_eq",
-      1,
-      2,
-      1,
-      [
-        "@MaxIFuel_assumption", "@query",
-        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
-        "bool_inversion", "bool_typing",
-        "constructor_distinct_Lib.IntTypes.PUB",
-        "constructor_distinct_Lib.IntTypes.SEC",
-        "constructor_distinct_Lib.IntTypes.U32",
-        "constructor_distinct_Lib.IntTypes.U8",
-        "equality_tok_Lib.IntTypes.PUB@tok",
-        "equality_tok_Lib.IntTypes.SEC@tok",
-        "equality_tok_Lib.IntTypes.U32@tok",
-        "equality_tok_Lib.IntTypes.U8@tok",
-        "equation_FStar.Monotonic.HyperStack.live_region",
-        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
-        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
-        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
-        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
-        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
-        "equation_LowStar.Buffer.trivial_preorder",
-        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
-        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.byte_t",
-        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
-        "lemma_FStar.Seq.Base.lemma_eq_elim",
-        "lemma_FStar.Seq.Base.lemma_eq_intro",
-        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
-        "lemma_LowStar.Monotonic.Buffer.length_null_1",
-        "lemma_LowStar.Monotonic.Buffer.length_null_2",
-        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
-        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
-        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
-        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
-        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
-        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
-        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
-        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
-        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
-        "projection_inverse_BoxBool_proj_0",
-        "projection_inverse_BoxInt_proj_0",
-        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
-        "refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086",
-        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
-        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
-        "refinement_interpretation_Tm_refine_699abca7bab73696ae075e9bacac2b7d",
-        "refinement_interpretation_Tm_refine_69ec46e0fdc9cd5ed2ef9c60fdc7f6e4",
-        "refinement_interpretation_Tm_refine_c1fb9a388e64d6307daf25ff6fa12df2",
-        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
-        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
-        "typing_FStar.Monotonic.HyperStack.live_region",
-        "typing_FStar.UInt32.v", "typing_FStar.UInt8.t",
-        "typing_LowStar.Buffer.trivial_preorder",
-        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
-        "typing_LowStar.Monotonic.Buffer.as_seq",
-        "typing_LowStar.Monotonic.Buffer.frameOf",
-        "typing_LowStar.Monotonic.Buffer.len",
-        "typing_LowStar.Monotonic.Buffer.loc_buffer",
-        "typing_LowStar.Monotonic.Buffer.loc_none"
-      ],
-      0,
-      "5c3583298d62e0e589cb3c418fe52d21"
-    ]
-  ]
-]
+[ "9��~�\u001bW<�nHQd�\f�", [] ]
diff --git a/hints/Lib.RawBuffer.fsti.hints b/hints/Lib.RawBuffer.fsti.hints
@@ -1,37 +1 @@
-[
-  "ÍN��Y\u0002\u007f��5�/{R\u001d",
-  [
-    [
-      "Lib.RawBuffer.blit",
-      1,
-      2,
-      1,
-      [
-        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
-        "equation_FStar.Monotonic.HyperStack.live_region",
-        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
-        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
-        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
-        "equation_LowStar.Buffer.trivial_preorder",
-        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
-        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8",
-        "int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
-        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
-        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
-        "primitive_Prims.op_LessThanOrEqual",
-        "projection_inverse_BoxBool_proj_0",
-        "projection_inverse_BoxInt_proj_0",
-        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
-        "refinement_interpretation_Tm_refine_45714303651d17b17626bf17b59ae2a7",
-        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
-        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
-        "typing_FStar.Monotonic.HyperStack.live_region",
-        "typing_FStar.UInt32.v", "typing_FStar.UInt8.t",
-        "typing_LowStar.Buffer.trivial_preorder",
-        "typing_LowStar.Monotonic.Buffer.frameOf"
-      ],
-      0,
-      "1b3d0a8546b11f8b209e7d23ac899427"
-    ]
-  ]
-]
+[ "ÍN��Y\u0002\u007f��5�/{R\u001d", [] ]