Skip to content

Commit 322f6d5

Browse files
msprotzmsprotz
authored
Merge pull request #1025 from hacl-star/protz_abstract_struct
Enable more instances of the C Abstract Struct pattern
2 parents e23aff3 + 7ff930c commit 322f6d5

230 files changed

Lines changed: 5641 additions & 4620 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Makefile‎

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -738,32 +738,40 @@ TARGET_H_INCLUDE = -add-early-include '"krml/internal/target.h"'
738738
# Note: due to backwards-compat, the syntax for the option is not super great...
739739
# it's `-add-include 'Foo:"bar.h"'` (include added to Foo.h) and
740740
# `-add-include 'Foo.c:"bar.h"'` (include added to Foo.c). Note how the former
741-
# doesn't have the extension while the latter does.
741+
# doesn't have the file extension while the latter does.
742+
# Note: the syntax got worse, now Foo.h:"bar.h" means the INTERNAL header internal/Foo.h includes
743+
# bar.h
744+
# Note: we would like to maintain the invariant (as of Feb 2025) that we NEVER include libintvector.h from a
745+
# public header. See https://github.com/python/cpython/issues/130213
746+
# FIXME: Sha3_Simd256 does *not* have an internal header so we can't enforce the invariant here
742747
INTRINSIC_FLAGS = \
743748
-add-include 'Hacl_P256.c:"lib_intrinsics.h"' \
744749
\
745750
-add-include 'Hacl_AEAD_Chacha20Poly1305_Simd128.c:"libintvector.h"' \
746751
-add-include 'Hacl_Chacha20_Vec128.c:"libintvector.h"' \
747752
-add-include 'Hacl_SHA2_Vec128.c:"libintvector.h"' \
748753
\
749-
-add-include 'Hacl_Hash_Blake2s_Simd128:"libintvector.h"' \
750-
-add-include 'Hacl_MAC_Poly1305_Simd128:"libintvector.h"' \
754+
-add-include 'Hacl_Hash_Blake2s_Simd128.h:"libintvector.h"' \
755+
-add-include 'Hacl_MAC_Poly1305_Simd128.h:"libintvector.h"' \
751756
\
752757
-add-include 'Hacl_AEAD_Chacha20Poly1305_Simd256.c:"libintvector.h"' \
753758
-add-include 'Hacl_Chacha20_Vec256.c:"libintvector.h"' \
754759
-add-include 'Hacl_SHA2_Vec256.c:"libintvector.h"' \
755760
\
756-
-add-include 'Hacl_Hash_Blake2b_Simd256:"libintvector.h"' \
757-
-add-include 'Hacl_MAC_Poly1305_Simd256:"libintvector.h"' \
761+
-add-include 'Hacl_Hash_Blake2b_Simd256.h:"libintvector.h"' \
762+
-add-include 'Hacl_MAC_Poly1305_Simd256.h:"libintvector.h"' \
758763
\
759764
-add-include 'Hacl_Hash_SHA3_Simd256:"libintvector.h"' \
760-
-add-include 'Hacl_Streaming_Types:"libintvector.h"'
765+
-add-include 'Vale.h:"libintvector.h"' \
766+
-add-include 'Vale.h:<inttypes.h>' \
767+
-add-include 'EverCrypt_Hash.h:"libintvector.h"' \
768+
-add-include 'Hacl_Streaming_HMAC.h:"libintvector-shim.h"'
761769

762770
# Disabled for distributions that don't include code based on intrinsics.
763771
INTRINSIC_INT_FLAGS = \
764772
-add-include 'Hacl_P256:"lib_intrinsics.h"' \
765773
-add-include 'Hacl_Bignum:"lib_intrinsics.h"' \
766-
-add-include 'Hacl_Bignum_Base:"lib_intrinsics.h"' \
774+
-add-include 'Hacl_Bignum_Base.h:"lib_intrinsics.h"' \
767775
-add-include 'Hacl_K256_ECDSA:"lib_intrinsics.h"'
768776

769777
# Disables tests; overriden in Wasm where tests indicate what can be compiled.

‎Makefile.common‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ HMAC_BUNDLE=-bundle Hacl.HMAC= \
194194
# Note: Hacl_Hash_SHA2 is legacy SHA2 here, will eventually go away, there's a proper
195195
# bundle in STREAMING_BUNDLE, below
196196
HASH_BUNDLE= \
197-
-bundle Hacl.Streaming.Blake2.Types+Hacl.Streaming.Types=Hacl.Streaming.MD,Spec.Hash.Definitions[rename=Hacl_Streaming_Types] \
197+
-bundle Hacl.Streaming.Types+Hacl.Streaming.MD=Spec.Hash.Definitions[rename=Hacl_Streaming_Types] \
198198
-bundle Hacl.Streaming.MD5=Hacl.Hash.MD5,Hacl.Hash.Core.MD5[rename=Hacl_Hash_MD5,rename-prefix] \
199199
-bundle Hacl.Streaming.SHA1=Hacl.Hash.SHA1,Hacl.Hash.Core.SHA1[rename=Hacl_Hash_SHA1,rename-prefix] \
200200
-bundle Hacl.Impl.SHA2.Types=[rename=Hacl_SHA2_Types] \

‎code/blake2/Hacl.Blake2b_256.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,5 +46,5 @@ let load_state256b_from_state32: Core.load_state_st Spec.Blake2B Core.M256 =
4646
let store_state256b_to_state32: Core.store_state_st Spec.Blake2B Core.M256 =
4747
Core.store_state_to_state32 #Spec.Blake2B #Core.M256
4848

49-
let malloc_with_key : Impl.blake2_malloc_st Spec.Blake2B Core.M256 =
49+
let malloc_internal_state_with_key : Impl.blake2_malloc_st Spec.Blake2B Core.M256 =
5050
Impl.blake2_malloc Spec.Blake2B Core.M256

‎code/blake2/Hacl.Blake2b_32.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,5 +39,5 @@ let update : Impl.blake2_update_st Spec.Blake2B Core.M32 =
3939
let finish : Impl.blake2_finish_st Spec.Blake2B Core.M32 =
4040
Impl.blake2_finish #Spec.Blake2B #Core.M32
4141

42-
let malloc_with_key : Impl.blake2_malloc_st Spec.Blake2B Core.M32 =
42+
let malloc_internal_state_with_key : Impl.blake2_malloc_st Spec.Blake2B Core.M32 =
4343
Impl.blake2_malloc Spec.Blake2B Core.M32

‎code/blake2/Hacl.Blake2s_128.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,5 +46,5 @@ let store_state128s_to_state32: Core.store_state_st Spec.Blake2S Core.M128 =
4646
let load_state128s_from_state32: Core.load_state_st Spec.Blake2S Core.M128 =
4747
Core.load_state_from_state32 #Spec.Blake2S #Core.M128
4848

49-
let malloc_with_key : Impl.blake2_malloc_st Spec.Blake2S Core.M128 =
49+
let malloc_internal_state_with_key : Impl.blake2_malloc_st Spec.Blake2S Core.M128 =
5050
Impl.blake2_malloc Spec.Blake2S Core.M128

‎code/blake2/Hacl.Blake2s_32.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,5 +40,5 @@ let update : Impl.blake2_update_st Spec.Blake2S Core.M32 =
4040
let finish : Impl.blake2_finish_st Spec.Blake2S Core.M32 =
4141
Impl.blake2_finish #Spec.Blake2S #Core.M32
4242

43-
let malloc_with_key : Impl.blake2_malloc_st Spec.Blake2S Core.M32 =
43+
let malloc_internal_state_with_key : Impl.blake2_malloc_st Spec.Blake2S Core.M32 =
4444
Impl.blake2_malloc Spec.Blake2S Core.M32

‎code/hash/Hacl.Hash.Blake2b_256.fst‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open Lib.Buffer
1010

1111
friend Spec.Agile.Hash
1212

13-
let malloc = BlB256.malloc_with_key
13+
let malloc = BlB256.malloc_internal_state_with_key
1414

1515
let alloca () =
1616
let h0 = ST.get() in
@@ -38,3 +38,17 @@ let update_last s prev input input_len =
3838
let finish s dst = BlB256.finish (hash_len Blake2B) dst s
3939

4040
let hash output input input_len = Hacl.Streaming.Blake2b_256.hash_with_key output 64ul input input_len (null #MUT uint8) 0ul
41+
42+
let copy_internal_state src dst =
43+
calc (==) {
44+
B.length src;
45+
(==) {}
46+
impl_state_length (| Spec.Agile.Hash.Blake2B, Hacl.Impl.Blake2.Core.M256 |);
47+
(==) {}
48+
UInt32.v (4ul *. row_len Spec.Blake2.Definitions.Blake2B Hacl.Impl.Blake2.Core.M256);
49+
(==) {}
50+
UInt32.v (4ul *. 1ul);
51+
(==) { Lib.IntTypes.mul_mod_lemma 4ul 1ul; assert_norm (4 < pow2 32) }
52+
UInt32.v 4ul;
53+
};
54+
B.blit src 0ul dst 0ul 4ul

‎code/hash/Hacl.Hash.Blake2b_256.fsti‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,23 @@ val init: init_st (|Blake2B, M256|)
2626
inline_for_extraction noextract
2727
val update_multi: update_multi_st (|Blake2B, M256|)
2828

29+
let update_multi_no_inline: update_multi_st (|Blake2B, M256|) = update_multi
30+
2931
inline_for_extraction noextract
3032
val update_last: update_last_st (|Blake2B, M256|)
3133

34+
let update_last_no_inline: update_last_st (|Blake2B, M256|) = update_last
35+
3236
inline_for_extraction noextract
3337
val finish: finish_st (|Blake2B, M256|)
3438

3539
inline_for_extraction noextract
3640
val hash: hash_st Blake2B
41+
42+
module B = LowStar.Buffer
43+
open FStar.HyperStack.ST
44+
45+
val copy_internal_state (src dst: state (| Spec.Agile.Hash.Blake2B, Hacl.Impl.Blake2.Core.M256 |)): Stack unit
46+
(requires (fun h0 -> B.(live h0 src /\ live h0 dst /\ loc_disjoint (loc_buffer src) (loc_buffer dst))))
47+
(ensures (fun h0 _ h1 ->
48+
B.(modifies (loc_buffer dst) h0 h1 /\ as_seq h1 dst `Seq.equal` as_seq h0 src)))

‎code/hash/Hacl.Hash.Blake2b_32.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open Lib.Buffer
1010

1111
friend Spec.Agile.Hash
1212

13-
let malloc = BlB32.malloc_with_key
13+
let malloc = BlB32.malloc_internal_state_with_key
1414

1515
let alloca () =
1616
let h0 = ST.get() in

‎code/hash/Hacl.Hash.Blake2s_128.fst‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open Lib.Buffer
1010

1111
friend Spec.Agile.Hash
1212

13-
let malloc = BlS128.malloc_with_key
13+
let malloc = BlS128.malloc_internal_state_with_key
1414

1515
let alloca () =
1616
let h0 = ST.get() in
@@ -38,3 +38,7 @@ let update_last s prev input input_len =
3838
let finish s dst = BlS128.finish (hash_len Blake2S) dst s
3939

4040
let hash output input input_len = Hacl.Streaming.Blake2s_128.hash_with_key output 32ul input input_len (null #MUT uint8) 0ul
41+
42+
let copy_internal_state src dst =
43+
Lib.IntTypes.mul_mod_lemma 4ul 1ul; assert_norm (4 < pow2 32);
44+
B.blit src 0ul dst 0ul 4ul

0 commit comments

Comments
 (0)