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 May 24, 2024
1 parent 3a504f4 commit 6bfe6a9
Show file tree
Hide file tree
Showing 5 changed files with 41 additions and 44 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.

6 changes: 2 additions & 4 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,8 @@ type group_manager_key = {

[@@ with_bytes dy_bytes]
type group_manager_value = {
[@@@ with_parser #bytes ps_nat]
si_public: nat;
[@@@ with_parser #bytes ps_nat]
si_private: nat;
si_public: state_id;
si_private: state_id;
}

%splice [ps_group_manager_value] (gen_parser (`group_manager_value))
Expand Down
3 changes: 1 addition & 2 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,7 @@ open MLS.TreeSync.Symbolic.IsWellFormed

[@@ with_bytes dy_bytes]
type key_package_manager_value = {
[@@@ with_parser #bytes ps_nat]
si_private: nat;
si_private: state_id;
}

%splice [ps_key_package_manager_value] (gen_parser (`key_package_manager_value))
Expand Down
20 changes: 10 additions & 10 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ val new_public_treesync_state:
#tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes ->
principal ->
st:treesync_state dy_bytes tkt dy_as_token group_id ->
traceful nat
traceful state_id
let new_public_treesync_state #tkt #group_id prin st =
let* state_id = new_session_id prin in
set_state prin state_id (treesync_state_to_bare_treesync_state st);*
Expand Down Expand Up @@ -141,7 +141,7 @@ let new_public_treesync_state_proof #invs #tkt #group_id prin st tr = ()

val set_public_treesync_state:
#tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes ->
prin:principal -> state_id:nat ->
prin:principal -> state_id:state_id ->
st:treesync_state dy_bytes tkt dy_as_token group_id ->
traceful unit
let set_public_treesync_state #tkt #group_id prin state_id st =
Expand All @@ -150,7 +150,7 @@ let set_public_treesync_state #tkt #group_id prin state_id st =
val set_public_treesync_state_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes -> #group_id:mls_bytes dy_bytes ->
prin:principal -> state_id:nat ->
prin:principal -> state_id:state_id ->
st:treesync_state dy_bytes tkt dy_as_token group_id ->
tr:trace ->
Lemma
Expand All @@ -169,7 +169,7 @@ let set_public_treesync_state_proof #invs #tkt #group_id prin state_id st tr = (

val get_public_treesync_state:
#tkt:treekem_types dy_bytes ->
prin:principal -> state_id:nat ->
prin:principal -> state_id:state_id ->
traceful (option (dtuple2 (mls_bytes dy_bytes) (treesync_state dy_bytes tkt dy_as_token)))
let get_public_treesync_state #tkt prin state_id =
let*? bare_st: bare_treesync_state tkt = get_state prin state_id in
Expand All @@ -186,7 +186,7 @@ let get_public_treesync_state #tkt prin state_id =
val get_public_treesync_state_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
prin:principal -> state_id:nat ->
prin:principal -> state_id:state_id ->
tr:trace ->
Lemma
(requires
Expand Down Expand Up @@ -242,7 +242,7 @@ let treesync_private_state_tag_and_invariant #ci = (local_state_treesync_private

val new_private_treesync_state:
principal -> treesync_private_state ->
traceful nat
traceful state_id
let new_private_treesync_state prin st =
let* state_id = new_session_id prin in
set_state prin state_id st;*
Expand All @@ -265,14 +265,14 @@ val new_private_treesync_state_proof:
let new_private_treesync_state_proof #invs prin st tr = ()

val set_private_treesync_state:
principal -> nat -> treesync_private_state ->
principal -> state_id -> treesync_private_state ->
traceful unit
let set_private_treesync_state prin state_id st =
set_state prin state_id st

val set_private_treesync_state_proof:
{|invs:protocol_invariants|} ->
prin:principal -> state_id:nat -> st:treesync_private_state ->
prin:principal -> state_id:state_id -> st:treesync_private_state ->
tr:trace ->
Lemma
(requires
Expand All @@ -287,14 +287,14 @@ val set_private_treesync_state_proof:
let set_private_treesync_state_proof #invs prin state_id st tr = ()

val get_private_treesync_state:
principal -> nat ->
principal -> state_id ->
traceful (option treesync_private_state)
let get_private_treesync_state prin state_id =
get_state prin state_id

val get_private_treesync_state_proof:
{|invs:protocol_invariants|} ->
prin:principal -> state_id:nat ->
prin:principal -> state_id:state_id ->
tr:trace ->
Lemma
(requires
Expand Down
50 changes: 25 additions & 25 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ let has_treesync_invariants tkt invs =
has_leaf_node_tbs_invariant tkt invs.crypto_invs

val get_token_for:
p:principal -> as_session:nat ->
p:principal -> as_session:state_id ->
inp:as_input dy_bytes ->
traceful (option dy_as_token)
let get_token_for p as_session (verification_key, credential) =
Expand All @@ -64,7 +64,7 @@ let get_token_for p as_session (verification_key, credential) =

val get_token_for_proof:
{|invs:protocol_invariants|} ->
p:principal -> as_session:nat ->
p:principal -> as_session:state_id ->
inp:as_input dy_bytes ->
tr:trace ->
Lemma
Expand All @@ -88,7 +88,7 @@ let get_token_for_proof #invs p as_session (verification_key, credential) tr = (

#push-options "--fuel 1 --ifuel 1"
val get_tokens_for:
p:principal -> as_session:nat ->
p:principal -> as_session:state_id ->
inps:list (option (as_input dy_bytes)) ->
traceful (option (l:list (option dy_as_token){List.Tot.length l == List.Tot.length inps}))
let rec get_tokens_for p as_session inps =
Expand All @@ -110,7 +110,7 @@ let rec get_tokens_for p as_session inps =
#push-options "--fuel 1 --ifuel 1"
val get_tokens_for_proof:
{|invs:protocol_invariants|} ->
p:principal -> as_session:nat ->
p:principal -> as_session:state_id ->
inps:list (option (as_input dy_bytes)) ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -148,8 +148,8 @@ let rec get_tokens_for_proof #invs p as_session inps tr =

val create:
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:state_id ->
traceful (option unit)
let create #tkt p as_session gmgr_session group_id ln secret_session =
let*? create_pend = extract_result (prepare_create #dy_bytes #crypto_dy_bytes group_id ln) in
Expand All @@ -163,8 +163,8 @@ let create #tkt p as_session gmgr_session group_id ln secret_session =
val create_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> secret_session:state_id ->
tr:trace ->
Lemma
(requires
Expand Down Expand Up @@ -193,7 +193,7 @@ let create_proof #invs #tkt p as_session gmgr_session group_id ln secret_session

val welcome:
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat -> kpmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id -> kpmgr_session:state_id ->
my_key_package:key_package_nt dy_bytes tkt ->
group_id:mls_bytes dy_bytes -> l:nat -> t:treesync dy_bytes tkt l 0 ->
traceful (option unit)
Expand All @@ -210,7 +210,7 @@ let welcome #tkt p as_session gmgr_session kpmgr_session my_key_package group_id
val welcome_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat -> kpmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id -> kpmgr_session:state_id ->
my_key_package:key_package_nt dy_bytes tkt ->
group_id:mls_bytes dy_bytes -> l:nat -> t:treesync dy_bytes tkt l 0 ->
tr:trace ->
Expand Down Expand Up @@ -251,7 +251,7 @@ let welcome_proof #invs #tkt p as_session gmgr_session kpmgr_session my_key_pack

val add:
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt ->
traceful (option nat)
let add #tkt p as_session gmgr_session group_id ln =
Expand All @@ -266,7 +266,7 @@ let add #tkt p as_session gmgr_session group_id ln =
val add_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -310,7 +310,7 @@ let add_proof #invs #tkt p as_session gmgr_session group_id ln tr =

val update:
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat ->
traceful (option unit)
let update #tkt p as_session gmgr_session group_id ln li =
Expand All @@ -326,7 +326,7 @@ let update #tkt p as_session gmgr_session group_id ln li =
val update_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> ln:leaf_node_nt dy_bytes tkt -> li:nat ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -368,7 +368,7 @@ let update_proof #invs #tkt p as_session gmgr_session group_id ln li tr =

val remove:
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> li:nat ->
traceful (option unit)
let remove #tkt p as_session gmgr_session group_id li =
Expand All @@ -383,7 +383,7 @@ let remove #tkt p as_session gmgr_session group_id li =
val remove_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> li:nat ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -419,7 +419,7 @@ let remove_proof #invs #tkt p as_session gmgr_session group_id li tr =

val commit:
#tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li ->
traceful (option unit)
let commit #tkt #l #li p as_session gmgr_session group_id path =
Expand All @@ -436,7 +436,7 @@ let commit #tkt #l #li p as_session gmgr_session group_id path =
val commit_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->
p:principal -> as_session:nat -> gmgr_session:nat ->
p:principal -> as_session:state_id -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> path:pathsync dy_bytes tkt l 0 li ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -492,7 +492,7 @@ let commit_proof #invs #tkt #l #li p as_session gmgr_session group_id path tr =

val create_signature_keypair:
p:principal ->
traceful (option (nat & signature_public_key_nt dy_bytes))
traceful (option (state_id & signature_public_key_nt dy_bytes))
let create_signature_keypair p =
let* signature_key = mk_rand (SigKey "MLS.LeafSignKey") (principal_label p) 32 in
let verification_key = vk signature_key in
Expand Down Expand Up @@ -545,7 +545,7 @@ let external_path_has_event_later #tkt #l #li prin tr1 tr2 t p group_id =
#push-options "--z3rlimit 25"
val authenticate_path:
#tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->
p:principal -> gmgr_session:nat ->
p:principal -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> tree:treesync dy_bytes tkt l 0 -> path:external_pathsync dy_bytes tkt l 0 li{(get_path_leaf path).source == LNS_update} ->
traceful (option (pathsync dy_bytes tkt l 0 li))
let authenticate_path #tkt #l p gmgr_session group_id tree path =
Expand All @@ -566,7 +566,7 @@ let authenticate_path #tkt #l p gmgr_session group_id tree path =
val authenticate_path_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->
p:principal -> gmgr_session:nat ->
p:principal -> gmgr_session:state_id ->
group_id:mls_bytes dy_bytes -> tree:treesync dy_bytes tkt l 0 -> path:external_pathsync dy_bytes tkt l 0 li ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -625,7 +625,7 @@ let authenticate_path_proof #invs #tkt #l p gmgr_session group_id tree path tr =
val authenticate_leaf_node_data_from_key_package:
#tkt:treekem_types dy_bytes ->
p:principal ->
si_private:nat ->
si_private:state_id ->
ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_key_package} ->
traceful (option (leaf_node_nt dy_bytes tkt))
let authenticate_leaf_node_data_from_key_package #tkt p si_private ln_data =
Expand All @@ -638,7 +638,7 @@ val authenticate_leaf_node_data_from_key_package_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal ->
si_private:nat ->
si_private:state_id ->
ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_key_package} ->
tr:trace ->
Lemma
Expand Down Expand Up @@ -679,7 +679,7 @@ let authenticate_leaf_node_data_from_key_package_proof #invs #tkt p si_private
val authenticate_leaf_node_data_from_update:
#tkt:treekem_types dy_bytes ->
p:principal ->
si_private:nat ->
si_private:state_id ->
ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_update} -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 ->
traceful (option (leaf_node_nt dy_bytes tkt))
let authenticate_leaf_node_data_from_update #tkt p si_private ln_data group_id leaf_index =
Expand All @@ -692,7 +692,7 @@ val authenticate_leaf_node_data_from_update_proof:
{|invs:protocol_invariants|} ->
#tkt:treekem_types dy_bytes ->
p:principal ->
si_private:nat ->
si_private:state_id ->
ln_data:leaf_node_data_nt dy_bytes tkt{ln_data.source == LNS_update} -> group_id:mls_bytes dy_bytes -> leaf_index:nat_lbytes 4 ->
tr:trace ->
Lemma
Expand Down

0 comments on commit 6bfe6a9

Please sign in to comment.