Skip to content

Commit

Permalink
chore: update DY*
Browse files Browse the repository at this point in the history
  • Loading branch information
@TWal
TWal committed Aug 14, 2024
1 parent 3c3f146 commit 9d8ed31
Show file tree
Hide file tree
Showing 9 changed files with 104 additions and 105 deletions.
6 changes: 3 additions & 3 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

18 changes: 9 additions & 9 deletions fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
}

#push-options "--ifuel 1"
val has_signwithlabel_pred: {|cusgs:crypto_usages|} -> sign_crypto_predicate cusgs -> (valid_label & signwithlabel_crypto_pred) -> prop
val has_signwithlabel_pred: {|crypto_usages|} -> sign_crypto_predicate -> (valid_label & signwithlabel_crypto_pred) -> prop
let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) =
forall tr vk msg.
{:pattern sign_pred.pred tr vk msg}
Expand All @@ -74,8 +74,8 @@ let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) =
#pop-options

val intro_has_signwithlabel_pred:
{|cusgs:crypto_usages|} ->
sign_pred:sign_crypto_predicate cusgs -> tagged_local_pred:(valid_label & signwithlabel_crypto_pred) ->
{|crypto_usages|} ->
sign_pred:sign_crypto_predicate -> tagged_local_pred:(valid_label & signwithlabel_crypto_pred) ->
Lemma
(requires has_local_fun split_signwithlabel_crypto_pred_params sign_pred.pred tagged_local_pred)
(ensures has_signwithlabel_pred sign_pred tagged_local_pred)
Expand Down Expand Up @@ -123,25 +123,25 @@ let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 vk msg =
#pop-options

val mk_mls_sign_pred:
{|cusgs:crypto_usages|} ->
{|crypto_usages|} ->
list (valid_label & signwithlabel_crypto_pred) ->
sign_crypto_predicate cusgs
sign_crypto_predicate
let mk_mls_sign_pred #cusgs tagged_local_preds = {
pred = mk_global_mls_sign_pred tagged_local_preds;
pred_later = mk_global_mls_sign_pred_later tagged_local_preds;
}

#push-options "--ifuel 1"
val mk_mls_sign_pred_correct:
{|cusgs:crypto_usages|} ->
sign_pred:sign_crypto_predicate cusgs -> tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
{|crypto_usages|} ->
sign_pred:sign_crypto_predicate -> tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
Lemma
(requires
sign_pred == mk_mls_sign_pred tagged_local_preds /\
List.Tot.no_repeats_p (List.Tot.map fst tagged_local_preds)
)
(ensures for_allP (has_signwithlabel_pred sign_pred) tagged_local_preds)
let mk_mls_sign_pred_correct sign_pred tagged_local_preds =
let mk_mls_sign_pred_correct #cusgs sign_pred tagged_local_preds =
for_allP_eq (has_signwithlabel_pred sign_pred) tagged_local_preds;
no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_preds);
FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_signwithlabel_crypto_pred_params tagged_local_preds));
Expand All @@ -153,7 +153,7 @@ let mk_mls_sign_pred_correct sign_pred tagged_local_preds =
val has_mls_signwithlabel_pred: {|crypto_invariants|} -> (valid_label & signwithlabel_crypto_pred) -> prop
let has_mls_signwithlabel_pred #cinvs tagged_local_pred =
exists mls_sign_pred.
has_sign_predicate cinvs ("MLS.LeafSignKey", mls_sign_pred) /\
has_sign_predicate ("MLS.LeafSignKey", mls_sign_pred) /\
has_signwithlabel_pred mls_sign_pred tagged_local_pred

(*** Lemmas on SignWithLabel and VerifyWithLabel ***)
Expand Down
6 changes: 3 additions & 3 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,9 @@ let group_manager_pred #ci = {
pred_knowable = (fun tr prin state_id key value -> ());
}

val has_group_manager_invariant: protocol_invariants -> prop
let has_group_manager_invariant invs =
has_map_session_invariant invs group_manager_pred
val has_group_manager_invariant: {|protocol_invariants|} -> prop
let has_group_manager_invariant #invs =
has_map_session_invariant group_manager_pred

val group_manager_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
let group_manager_tag_and_invariant #ci = (group_manager_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant group_manager_pred))
Expand Down
6 changes: 3 additions & 3 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,9 +35,9 @@ let key_package_manager_pred #ci tkt = {
);
}

val has_key_package_manager_invariant: treekem_types dy_bytes -> protocol_invariants -> prop
let has_key_package_manager_invariant tkt invs =
has_map_session_invariant invs (key_package_manager_pred tkt)
val has_key_package_manager_invariant: treekem_types dy_bytes -> {|protocol_invariants|} -> prop
let has_key_package_manager_invariant tkt #invs =
has_map_session_invariant (key_package_manager_pred tkt)

val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> string & local_bytes_state_predicate
let key_package_manager_tag_and_invariant #ci tkt = ((key_package_manager_types tkt).tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant (key_package_manager_pred tkt)))
Expand Down
36 changes: 18 additions & 18 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,9 +89,9 @@ let treesync_public_state_pred #ci tkt = {
instance local_state_bare_treesync_state (tkt:treekem_types dy_bytes): local_state (bare_treesync_state tkt) =
mk_local_state_instance "MLS.TreeSync.PublicState"

val has_treesync_public_state_invariant: treekem_types dy_bytes -> protocol_invariants -> prop
let has_treesync_public_state_invariant tkt invs =
has_local_state_predicate invs (treesync_public_state_pred tkt)
val has_treesync_public_state_invariant: treekem_types dy_bytes -> {|protocol_invariants|} -> prop
let has_treesync_public_state_invariant tkt #invs =
has_local_state_predicate (treesync_public_state_pred tkt)

val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> string & local_bytes_state_predicate
let treesync_public_state_tag_and_invariant #ci tkt = ((local_state_bare_treesync_state tkt).tag, local_state_predicate_to_local_bytes_state_predicate (treesync_public_state_pred tkt))
Expand Down Expand Up @@ -120,7 +120,7 @@ let new_public_treesync_state #tkt #group_id prin st =
return state_id

val new_public_treesync_state_proof:
{|invs:protocol_invariants|} ->
{|protocol_invariants|} ->
#tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes ->
prin:principal ->
st:treesync_state dy_bytes tkt dy_as_token group_id ->
Expand All @@ -131,7 +131,7 @@ val new_public_treesync_state_proof:
is_well_formed _ (is_publishable tr) (st.tree <: treesync _ _ _ _) /\
treesync_state_valid (dy_asp tr) st /\
trace_invariant tr /\
has_treesync_public_state_invariant tkt invs
has_treesync_public_state_invariant tkt
)
(ensures (
let (_, tr_out) = new_public_treesync_state prin st tr in
Expand All @@ -148,7 +148,7 @@ let set_public_treesync_state #tkt #group_id prin state_id st =
set_state prin state_id (treesync_state_to_bare_treesync_state st)

val set_public_treesync_state_proof:
{|invs:protocol_invariants|} ->
{|protocol_invariants|} ->
#tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes ->
prin:principal -> state_id:state_id ->
st:treesync_state dy_bytes tkt dy_as_token group_id ->
Expand All @@ -159,7 +159,7 @@ val set_public_treesync_state_proof:
is_well_formed _ (is_publishable tr) (st.tree <: treesync _ _ _ _) /\
treesync_state_valid (dy_asp tr) st /\
trace_invariant tr /\
has_treesync_public_state_invariant tkt invs
has_treesync_public_state_invariant tkt
)
(ensures (
let ((), tr_out) = set_public_treesync_state prin state_id st tr in
Expand All @@ -184,14 +184,14 @@ let get_public_treesync_state #tkt prin state_id =
} <: treesync_state dy_bytes tkt dy_as_token bare_st.group_id)|))

val get_public_treesync_state_proof:
{|invs:protocol_invariants|} ->
{|protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
prin:principal -> state_id:state_id ->
tr:trace ->
Lemma
(requires
trace_invariant tr /\
has_treesync_public_state_invariant tkt invs
has_treesync_public_state_invariant tkt
)
(ensures (
let (opt_result, tr_out) = get_public_treesync_state prin state_id tr in
Expand Down Expand Up @@ -231,9 +231,9 @@ let treesync_private_state_pred #ci = {
instance local_state_treesync_private_state: local_state treesync_private_state =
mk_local_state_instance "MLS.TreeSync.PrivateState"

val has_treesync_private_state_invariant: protocol_invariants -> prop
let has_treesync_private_state_invariant invs =
has_local_state_predicate invs treesync_private_state_pred
val has_treesync_private_state_invariant: {|protocol_invariants|} -> prop
let has_treesync_private_state_invariant #invs =
has_local_state_predicate treesync_private_state_pred

val treesync_private_state_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
let treesync_private_state_tag_and_invariant #ci = (local_state_treesync_private_state.tag, local_state_predicate_to_local_bytes_state_predicate treesync_private_state_pred)
Expand All @@ -249,14 +249,14 @@ let new_private_treesync_state prin st =
return state_id

val new_private_treesync_state_proof:
{|invs:protocol_invariants|} ->
{|protocol_invariants|} ->
prin:principal -> st:treesync_private_state ->
tr:trace ->
Lemma
(requires
is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
trace_invariant tr /\
has_treesync_private_state_invariant invs
has_treesync_private_state_invariant
)
(ensures (
let (_, tr_out) = new_private_treesync_state prin st tr in
Expand All @@ -271,14 +271,14 @@ let set_private_treesync_state prin state_id st =
set_state prin state_id st

val set_private_treesync_state_proof:
{|invs:protocol_invariants|} ->
{|protocol_invariants|} ->
prin:principal -> state_id:state_id -> st:treesync_private_state ->
tr:trace ->
Lemma
(requires
is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
trace_invariant tr /\
has_treesync_private_state_invariant invs
has_treesync_private_state_invariant
)
(ensures (
let ((), tr_out) = set_private_treesync_state prin state_id st tr in
Expand All @@ -293,13 +293,13 @@ let get_private_treesync_state prin state_id =
get_state prin state_id

val get_private_treesync_state_proof:
{|invs:protocol_invariants|} ->
{|protocol_invariants|} ->
prin:principal -> state_id:state_id ->
tr:trace ->
Lemma
(requires
trace_invariant tr /\
has_treesync_private_state_invariant invs
has_treesync_private_state_invariant
)
(ensures (
let (opt_result, tr_out) = get_private_treesync_state prin state_id tr in
Expand Down
Loading

0 comments on commit 9d8ed31

Please sign in to comment.