Skip to content

Commit

Permalink
hacspec: add feature needed for fstar generation
Browse files Browse the repository at this point in the history
  • Loading branch information
geonnave committed Aug 2, 2023
1 parent 90a63d3 commit 0791e44
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 12 deletions.
2 changes: 2 additions & 0 deletions crypto/edhoc-crypto-hacspec/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,10 +94,12 @@ pub fn p256_ecdh(
secret
}

#[cfg(not(feature = "hacspec-pure"))]
pub fn get_random_byte() -> U8 {
U8(rand::thread_rng().gen::<u8>())
}

#[cfg(not(feature = "hacspec-pure"))]
pub fn p256_generate_key_pair() -> (BytesP256ElemLen, BytesP256ElemLen) {
// generate a private key
let mut private_key = BytesP256ElemLen::new();
Expand Down
12 changes: 0 additions & 12 deletions hacspec/adjust_features_for_hax.patch
Original file line number Diff line number Diff line change
Expand Up @@ -32,18 +32,6 @@ index e59a361..14f606e 100644
+[features]
+hacspec-pure = []
\ No newline at end of file
diff --git a/crypto/edhoc-crypto-hacspec/src/lib.rs b/crypto/edhoc-crypto-hacspec/src/lib.rs
index a9c7064..a9e2a7e 100644
--- a/crypto/edhoc-crypto-hacspec/src/lib.rs
+++ b/crypto/edhoc-crypto-hacspec/src/lib.rs
@@ -94,6 +94,7 @@ pub fn p256_ecdh(
secret
}

+#[cfg(not(feature = "hacspec-pure"))]
pub fn p256_generate_key_pair() -> (BytesP256ElemLen, BytesP256ElemLen) {
// generate a private key
let mut private_key = BytesP256ElemLen::new();
diff --git a/hacspec/Cargo.toml b/hacspec/Cargo.toml
index 94b80ae..51dbeb2 100644
--- a/hacspec/Cargo.toml
Expand Down

0 comments on commit 0791e44

Please sign in to comment.