Skip to content

Commit

Permalink
refactor: have ref_hash return an mls_bytes
Browse files Browse the repository at this point in the history
  • Loading branch information
TWal committed Jun 5, 2024
1 parent da09832 commit 9d90394
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 7 deletions.
3 changes: 1 addition & 2 deletions fstar/bootstrap/MLS.Bootstrap.KeyPackageRef.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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
11 changes: 6 additions & 5 deletions fstar/common/code/MLS.Crypto.Derived.fst
Original file line number Diff line number Diff line change
Expand Up @@ -308,24 +308,25 @@ 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

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
Expand Down

0 comments on commit 9d90394

Please sign in to comment.