Skip to content

Commit

Permalink
cleanup: add and use parseable_serializeable instances when needed
Browse files Browse the repository at this point in the history
  • Loading branch information
@TWal
TWal committed Jun 5, 2024
1 parent b25f0ca commit da09832
Show file tree
Hide file tree
Showing 5 changed files with 23 additions and 13 deletions.
22 changes: 11 additions & 11 deletions fstar/api/MLS.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ let state_to_group_context st =

val hash_leaf_package: leaf_node_nt bytes tkt -> result bytes
let hash_leaf_package leaf_package =
let leaf_package = (ps_prefix_to_ps_whole (ps_leaf_node_nt _)).serialize leaf_package in
let leaf_package = serialize _ leaf_package in
hash_hash leaf_package

val process_proposal: nat -> (state & list (key_package_nt bytes tkt & nat)) -> proposal_nt bytes -> result (state & list (key_package_nt bytes tkt & nat))
Expand Down Expand Up @@ -325,7 +325,7 @@ let fresh_key_package_internal e { identity; signature_key } private_sign_key =
extensions;
} in
let? signature = (
let tbs = (ps_prefix_to_ps_whole (ps_leaf_node_tbs_nt _)).serialize ({
let tbs = serialize (leaf_node_tbs_nt bytes tkt) ({
data = leaf_data;
group_id = ();
leaf_index = ();
Expand All @@ -346,7 +346,7 @@ let fresh_key_package_internal e { identity; signature_key } private_sign_key =
extensions = [];
} <: key_package_tbs_nt bytes tkt) in
let? nonce = universal_sign_nonce in
let tbs: bytes = (ps_prefix_to_ps_whole (ps_key_package_tbs_nt _)).serialize kp_tbs in
let tbs: bytes = serialize _ kp_tbs in
let? signature: bytes = sign_with_label private_sign_key "KeyPackageTBS" tbs nonce in
let? signature = mk_mls_bytes signature "fresh_key_package_internal" "signature" in
return (({
Expand All @@ -356,7 +356,7 @@ let fresh_key_package_internal e { identity; signature_key } private_sign_key =

let fresh_key_package e cred private_sign_key =
let? key_package, leaf_secret = fresh_key_package_internal e cred private_sign_key in
let key_package_bytes = (ps_prefix_to_ps_whole (ps_key_package_nt _)).serialize key_package in
let key_package_bytes = serialize _ key_package in
let? hash = compute_key_package_ref key_package in
return (key_package_bytes, (hash <: bytes), (leaf_secret <: bytes))

Expand Down Expand Up @@ -426,7 +426,7 @@ let rec unsafe_mk_randomness #l e =
val generate_welcome_message: state -> ratchet_tree_nt bytes tkt -> group_context_nt bytes -> mac_nt bytes -> bytes -> new_key_packages:list (key_package_nt bytes tkt & bytes) -> bytes -> result (welcome_nt bytes)
let generate_welcome_message st ratchet_tree new_group_context confirmation_tag joiner_secret new_key_packages e =
let? joiner_secret = mk_mls_bytes joiner_secret "generate_welcome_message" "joiner_secret" in
let? ratchet_tree_bytes = mk_mls_bytes ((ps_prefix_to_ps_whole (ps_ratchet_tree_nt tkt)).serialize ratchet_tree) "generate_welcome_message" "ratchet_tree" in
let? ratchet_tree_bytes = mk_mls_bytes (serialize _ ratchet_tree) "generate_welcome_message" "ratchet_tree" in
let? leaf_index = mk_nat_lbytes st.leaf_index "generate_welcome_message" "leaf_index" in
let? extensions = mk_mls_list [{extension_type = ET_ratchet_tree; extension_data = ratchet_tree_bytes;}] "generate_welcome_message" "extensions" in
let group_info_tbs: group_info_tbs_nt bytes = {
Expand Down Expand Up @@ -591,14 +591,14 @@ let generate_commit state e proposals =
#pop-options

let add state key_package e =
let? key_package = from_option "error message if it is malformed" ((ps_prefix_to_ps_whole (ps_key_package_nt tkt)).parse key_package) in
let? key_package = from_option "error message if it is malformed" (parse _ key_package) in
let proposals = [ (P_add {key_package}) ] in
let? (state, {group_msg; path_secrets; joiner_secret; ratchet_tree; new_group_context; confirmation_tag}, e) = generate_commit state e proposals in
let? fresh, e = chop_entropy e 32 in
let rand = fresh in
assume (hpke_private_key_length #bytes == 32);
let? welcome_msg = generate_welcome_message state ratchet_tree new_group_context confirmation_tag joiner_secret path_secrets rand in
let w:welcome_message = (empty #bytes, (ps_prefix_to_ps_whole ps_welcome_nt).serialize welcome_msg) in
let w:welcome_message = (empty #bytes, serialize _ welcome_msg) in
return (state, (group_msg,w))

let remove state p e =
Expand Down Expand Up @@ -654,7 +654,7 @@ let find_my_index #l t sign_pk =
#push-options "--z3rlimit 50"
let process_welcome_message w (sign_pk, sign_sk) lookup =
let (_, welcome_bytes) = w in
let? welcome = from_option "process_welcome_message: can't parse welcome message" ((ps_prefix_to_ps_whole ps_welcome_nt).parse welcome_bytes) in
let? welcome = from_option "process_welcome_message: can't parse welcome message" (parse _ welcome_bytes) in
let extract_hpke_sk (x:bytes): result (hpke_private_key bytes) =
if not (length x = hpke_private_key_length #bytes) then
internal_failure "process_welcome_message: bad HPKE private key length"
Expand All @@ -666,7 +666,7 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =
let? ratchet_tree = (
match group_info.tbs.extensions with
| [{extension_type = ET_ratchet_tree; extension_data}] ->
from_option "bad ratchet tree" ((ps_prefix_to_ps_whole #bytes (ps_ratchet_tree_nt tkt)).parse extension_data)
from_option "bad ratchet tree" (parse _ (extension_data <: bytes))
| _ -> error "process_welcome_message: invalid extensions"
) in
let? treesync_state = (
Expand Down Expand Up @@ -696,7 +696,7 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =
let? interim_transcript_hash = MLS.TreeDEM.Message.Transcript.compute_interim_transcript_hash #bytes group_info.tbs.confirmation_tag group_info.tbs.group_context.confirmed_transcript_hash in
let? tree_hash = MLS.TreeSync.API.compute_tree_hash treesync_state in
let? group_context = compute_group_context group_info.tbs.group_context.group_id group_info.tbs.group_context.epoch tree_hash group_info.tbs.group_context.confirmed_transcript_hash in
let? epoch_secret = MLS.TreeKEM.KeySchedule.secret_joiner_to_epoch secrets.joiner_secret None ((ps_prefix_to_ps_whole ps_group_context_nt).serialize group_context) in
let? epoch_secret = MLS.TreeKEM.KeySchedule.secret_joiner_to_epoch (secrets.joiner_secret <: bytes) None (serialize _ group_context) in
let? (treekem_state, encryption_secret) = MLS.TreeKEM.API.welcome treekem leaf_decryption_key opt_path_secret_and_inviter_ind leaf_index epoch_secret in

let? tree_hash = MLS.TreeSync.API.compute_tree_hash treesync_state in
Expand Down Expand Up @@ -739,7 +739,7 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =

let process_group_message state msg =
let? msg = from_option "process_group_message: can't parse group message"
((ps_prefix_to_ps_whole ps_mls_message_nt).parse msg) in
(parse _ msg) in
let? (wire_format, message) = (
match msg with
| M_mls10 (M_public_message msg) ->
Expand Down
3 changes: 3 additions & 0 deletions fstar/bootstrap/MLS.Bootstrap.NetworkTypes.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,7 @@ type encrypted_group_secrets_nt (bytes:Type0) {|bytes_like bytes|} = {
}

%splice [ps_encrypted_group_secrets_nt] (gen_parser (`encrypted_group_secrets_nt))
%splice [ps_encrypted_group_secrets_nt_is_well_formed] (gen_is_well_formed_lemma (`encrypted_group_secrets_nt))

/// struct {
/// CipherSuite cipher_suite;
Expand All @@ -147,4 +148,6 @@ type welcome_nt (bytes:Type0) {|bytes_like bytes|} = {
}

%splice [ps_welcome_nt] (gen_parser (`welcome_nt))
%splice [ps_welcome_nt_is_well_formed] (gen_is_well_formed_lemma (`welcome_nt))

instance parseable_serializeable_welcome_nt (bytes:Type0) {|bytes_like bytes|}: parseable_serializeable bytes (welcome_nt bytes) = mk_parseable_serializeable ps_welcome_nt
8 changes: 6 additions & 2 deletions fstar/common/code/MLS.Crypto.Derived.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -177,7 +177,7 @@ val get_sign_content:
label:valid_label -> content:mls_bytes bytes ->
bytes
let get_sign_content #bytes #cb label content =
((ps_prefix_to_ps_whole ps_sign_content_nt).serialize ({
(serialize _ ({
label = get_mls_label label;
content = content;
}))
Expand Down Expand Up @@ -217,6 +217,10 @@ type kdf_label_nt (bytes:Type0) {|bytes_like bytes|} = {
}

%splice [ps_kdf_label_nt] (gen_parser (`kdf_label_nt))
%splice [ps_kdf_label_nt_is_well_formed] (gen_is_well_formed_lemma (`kdf_label_nt))

instance parseable_serializeable_kdf_label_nt (bytes:Type0) {|bytes_like bytes|}: parseable_serializeable bytes (kdf_label_nt bytes) =
mk_parseable_serializeable ps_kdf_label_nt

val expand_with_label:
#bytes:Type0 -> {|crypto_bytes bytes|} ->
Expand All @@ -226,7 +230,7 @@ let expand_with_label #bytes #cb secret label context len =
normalize_term_spec ((pow2 30) - 8);
let? length = mk_nat_lbytes len "expand_with_label" "len" in
let? context = mk_mls_bytes context "expand_with_label" "context" in
let kdf_label = (ps_prefix_to_ps_whole ps_kdf_label_nt).serialize ({
let kdf_label = serialize _ ({
length;
label = get_mls_label label;
context;
Expand Down
1 change: 1 addition & 0 deletions fstar/treekem/code/MLS.TreeKEM.NetworkTypes.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ type hpke_ciphertext_nt (bytes:Type0) {|bytes_like bytes|} = {
}

%splice [ps_hpke_ciphertext_nt] (gen_parser (`hpke_ciphertext_nt))
%splice [ps_hpke_ciphertext_nt_is_well_formed] (gen_is_well_formed_lemma (`hpke_ciphertext_nt))

/// struct {
/// HPKEPublicKey encryption_key;
Expand Down
2 changes: 2 additions & 0 deletions fstar/treesync/code/MLS.TreeSync.NetworkTypes.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,3 +206,5 @@ type node_nt (bytes:Type0) {|bytes_like bytes|} (tkt:treekem_types bytes) =
type ratchet_tree_nt (bytes:Type0) {|bytes_like bytes|} (tkt:treekem_types bytes) = mls_list bytes (ps_option (ps_node_nt tkt))

%splice [ps_ratchet_tree_nt] (gen_parser (`ratchet_tree_nt))

instance parseable_serializeable_ratchet_tree_nt (bytes:Type0) {|bytes_like bytes|} (tkt:treekem_types bytes): parseable_serializeable bytes (ratchet_tree_nt bytes tkt) = mk_parseable_serializeable (ps_ratchet_tree_nt tkt)

0 comments on commit da09832

Please sign in to comment.