From 9d9039470014168d3239386226049e7c2b6931f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Wed, 5 Jun 2024 18:06:26 +0200 Subject: [PATCH] refactor: have `ref_hash` return an `mls_bytes` --- fstar/bootstrap/MLS.Bootstrap.KeyPackageRef.fst | 3 +-- fstar/common/code/MLS.Crypto.Derived.fst | 11 ++++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/fstar/bootstrap/MLS.Bootstrap.KeyPackageRef.fst b/fstar/bootstrap/MLS.Bootstrap.KeyPackageRef.fst index 574ccc2..3202acd 100644 --- a/fstar/bootstrap/MLS.Bootstrap.KeyPackageRef.fst +++ b/fstar/bootstrap/MLS.Bootstrap.KeyPackageRef.fst @@ -12,5 +12,4 @@ val compute_key_package_ref: result (key_package_ref_nt bytes) let compute_key_package_ref #bytes #cb kp = let kp_bytes: bytes = serialize (key_package_nt bytes tkt) kp in - let? res = make_keypackage_ref kp_bytes in - mk_mls_bytes res "compute_key_package_ref" "res" + make_keypackage_ref kp_bytes diff --git a/fstar/common/code/MLS.Crypto.Derived.fst b/fstar/common/code/MLS.Crypto.Derived.fst index 6dbb09a..3723d10 100644 --- a/fstar/common/code/MLS.Crypto.Derived.fst +++ b/fstar/common/code/MLS.Crypto.Derived.fst @@ -308,16 +308,17 @@ instance parseable_serializeable_ref_hash_input_nt (bytes:Type0) {|bytes_like by val ref_hash: #bytes:Type0 -> {|crypto_bytes bytes|} -> mls_ascii_string -> bytes -> - result bytes + result (mls_bytes bytes) let ref_hash #bytes #cb label value = let? value = mk_mls_bytes value "ref_hash" "value" in - let hash_content = (serialize (ref_hash_input_nt bytes) ({label; value;})) in - hash_hash hash_content + let hash_content: bytes = (serialize (ref_hash_input_nt bytes) ({label; value;})) in + let? ref = hash_hash hash_content in + mk_mls_bytes ref "ref_hash" "ref" val make_keypackage_ref: #bytes:Type0 -> {|crypto_bytes bytes|} -> bytes -> - result bytes + result (mls_bytes bytes) let make_keypackage_ref #bytes #cb buf = normalize_term_spec (String.strlen "MLS 1.0 KeyPackage Reference"); ref_hash "MLS 1.0 KeyPackage Reference" buf @@ -325,7 +326,7 @@ let make_keypackage_ref #bytes #cb buf = val make_proposal_ref: #bytes:Type0 -> {|crypto_bytes bytes|} -> bytes -> - result bytes + result (mls_bytes bytes) let make_proposal_ref #bytes #cb buf = normalize_term_spec (String.strlen "MLS 1.0 Proposal Reference"); ref_hash "MLS 1.0 Proposal Reference" buf