chore: update DY*

fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst

@@ -15,18 +15,17 @@ open MLS.Result
 
 noeq
 type signwithlabel_crypto_pred {|crypto_usages|} = {
-  pred: trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes -> prop;
+  pred: trace -> sk_usg:usage{SigKey? sk_usg} -> msg:bytes -> prop;
   pred_later:
     tr1:trace -> tr2:trace ->
-    vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
+    sk_usg:usage{SigKey? sk_usg} -> msg:bytes ->
     Lemma
     (requires
-      pred tr1 vk msg /\
-      bytes_well_formed tr1 vk /\
+      pred tr1 sk_usg msg /\
       bytes_well_formed tr1 msg /\
       tr1 <$ tr2
     )
-    (ensures pred tr2 vk msg)
+    (ensures pred tr2 sk_usg msg)
   ;
 }
 
@@ -41,8 +40,8 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
     FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2
   );
 
-  tagged_data_t = (trace & (vk:bytes{SigKey? (get_signkey_usage vk)}) & bytes);
-  raw_data_t = (trace & (vk:bytes{SigKey? (get_signkey_usage vk)}) & bytes);
+  tagged_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes);
+  raw_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes);
   output_t = prop;
 
   decode_tagged_data = (fun (tr, vk, data) -> (
@@ -52,7 +51,7 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
   ));
 
   local_fun_t = mk_dependent_type signwithlabel_crypto_pred;
-  global_fun_t = trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> bytes -> prop;
+  global_fun_t = trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> prop;
 
   default_global_fun = (fun tr vk content -> False);
 
@@ -102,7 +101,7 @@ let intro_has_signwithlabel_pred #cusgs sign_pred tag local_pred =
 val mk_global_mls_sign_pred:
   {|crypto_usages|} ->
   list (valid_label & signwithlabel_crypto_pred) ->
-  trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> bytes ->
+  trace -> sk_usg:usage{SigKey? sk_usg} -> bytes ->
   prop
 let mk_global_mls_sign_pred tagged_local_preds vk msg =
   mk_global_fun split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) vk msg
@@ -112,22 +111,21 @@ val mk_global_mls_sign_pred_later:
   {|crypto_usages|} ->
   tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
   tr1:trace -> tr2:trace ->
-  vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
+  sk_usg:usage{SigKey? sk_usg} -> msg:bytes ->
   Lemma
   (requires
-    mk_global_mls_sign_pred tagged_local_preds tr1 vk msg /\
-    bytes_well_formed tr1 vk /\
+    mk_global_mls_sign_pred tagged_local_preds tr1 sk_usg msg /\
     bytes_well_formed tr1 msg /\
     tr1 <$ tr2
   )
-  (ensures mk_global_mls_sign_pred tagged_local_preds tr2 vk msg)
-let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 vk msg =
-  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, vk, msg);
-  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, vk, msg);
+  (ensures mk_global_mls_sign_pred tagged_local_preds tr2 sk_usg msg)
+let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 sk_usg msg =
+  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, sk_usg, msg);
+  mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, sk_usg, msg);
   FStar.Classical.move_requires (parse_wf_lemma (sign_content_nt bytes) (bytes_well_formed tr1)) msg;
-  introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, vk, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, vk, content) with (
+  introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, sk_usg, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, sk_usg, content) with (
     introduce _ ==> _ with _. (
-      lpred.pred_later tr1 tr2 vk content
+      lpred.pred_later tr1 tr2 sk_usg content
     )
   )
 #pop-options
@@ -179,10 +177,13 @@ val bytes_invariant_sign_with_label:
     bytes_invariant tr sk /\
     bytes_invariant tr nonce /\
     bytes_invariant tr msg /\
-    get_usage sk == mk_mls_sigkey_usage prin /\
-    SigNonce? (get_usage nonce) /\
-    (get_label tr sk) `can_flow tr` (get_label tr nonce) /\
-    spred.pred tr (vk sk) msg /\
+    sk `has_usage tr` mk_mls_sigkey_usage prin /\
+    nonce `has_usage tr` SigNonce /\
+    (get_label tr sk) `can_flow tr` (get_label tr nonce) /\ (
+      spred.pred tr (mk_mls_sigkey_usage prin) msg
+      \/
+      get_label tr sk `can_flow tr` public
+    ) /\
     has_mls_signwithlabel_pred (lab, spred)
   )
   (ensures
@@ -206,13 +207,13 @@ val bytes_invariant_verify_with_label:
     bytes_invariant tr vk /\
     bytes_invariant tr content /\
     bytes_invariant tr signature /\
+    vk `has_signkey_usage tr` mk_mls_sigkey_usage prin /\
     verify_with_label vk lab content signature /\
     has_mls_signwithlabel_pred (lab, spred)
   )
   (ensures
     (
-      get_signkey_usage vk == mk_mls_sigkey_usage prin ==>
-      spred.pred tr vk content
+      spred.pred tr (mk_mls_sigkey_usage prin) content
     ) \/ (
       (get_signkey_label tr vk) `can_flow tr` public
     )

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst

@@ -48,8 +48,8 @@ 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))
+val group_manager_tag_and_invariant: {|crypto_invariants|} -> dtuple2 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)|)
 
 (*** Group manager API ***)
 

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst

@@ -31,16 +31,16 @@ let key_package_manager_pred #ci tkt = {
   );
   pred_later = (fun tr1 tr2 prin state_id key_package value -> ());
   pred_knowable = (fun tr prin state_id key_package value ->
-    assert(is_well_formed _ (is_knowable_by (principal_state_label prin state_id) tr) key_package)
+    assert(is_well_formed _ (is_knowable_by (principal_tag_state_label prin (key_package_manager_types tkt).tag state_id) tr) key_package)
   );
 }
 
 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)))
+val key_package_manager_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> dtuple2 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))|)
 
 (*** KeyPackage manager API ***)
 

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst

@@ -64,6 +64,9 @@ type bare_treesync_state (tkt:treekem_types dy_bytes) =
 
 instance parseable_serializeable_bare_treesync_state (tkt:treekem_types dy_bytes): parseable_serializeable dy_bytes (bare_treesync_state tkt) = mk_parseable_serializeable (ps_bare_treesync_state_ tkt dy_as_token ps_dy_as_token)
 
+instance local_state_bare_treesync_state (tkt:treekem_types dy_bytes): local_state (bare_treesync_state tkt) =
+  mk_local_state_instance "MLS.TreeSync.PublicState"
+
 #push-options "--fuel 1 --ifuel 1 --z3rlimit 25"
 val treesync_public_state_pred: {|crypto_invariants|} -> tkt:treekem_types dy_bytes -> local_state_predicate (bare_treesync_state tkt)
 let treesync_public_state_pred #ci tkt = {
@@ -79,22 +82,19 @@ let treesync_public_state_pred #ci tkt = {
     wf_weaken_lemma _ (is_publishable tr1) (is_publishable tr2) st.tree
   );
   pred_knowable = (fun tr prin state_id st ->
-    let pre = is_knowable_by (principal_state_label prin state_id) tr in
+    let pre = is_knowable_by (principal_typed_state_content_label prin (local_state_bare_treesync_state tkt).tag state_id st) tr in
     wf_weaken_lemma _ (is_publishable tr) pre st.tree;
     ps_dy_as_tokens_is_well_formed pre st.tokens
   );
 }
 #pop-options
 
-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 (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))
+val treesync_public_state_tag_and_invariant: {|crypto_invariants|} -> treekem_types dy_bytes -> dtuple2 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)|)
 
 (*** Traceful API for public state ***)
 
@@ -219,6 +219,9 @@ type treesync_private_state = treesync_private_state_ dy_bytes
 
 instance parseable_serializeable_treesync_private_state: parseable_serializeable dy_bytes treesync_private_state = mk_parseable_serializeable ps_treesync_private_state_
 
+instance local_state_treesync_private_state: local_state treesync_private_state =
+  mk_local_state_instance "MLS.TreeSync.PrivateState"
+
 val treesync_private_state_pred: {|crypto_invariants|} -> local_state_predicate treesync_private_state
 let treesync_private_state_pred #ci = {
   pred = (fun tr prin state_id st ->
@@ -228,15 +231,12 @@ let treesync_private_state_pred #ci = {
   pred_knowable = (fun tr prin state_id st -> ());
 }
 
-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 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)
+val treesync_private_state_tag_and_invariant: {|crypto_invariants|} -> dtuple2 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|)
 
 (*** Traceful API for private state ***)
 

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst

@@ -159,6 +159,7 @@ let create #tkt p as_session gmgr_session group_id ln secret_session =
   add_new_group_sessions p gmgr_session { group_id } group_sessions;*?
   return (Some ())
 
+#push-options "--z3rlimit 25"
 val create_proof:
   {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes ->
@@ -189,6 +190,7 @@ let create_proof #invs #tkt p as_session gmgr_session group_id ln secret_session
       finalize_create_valid #_ #_ #_ #(dy_asp tr) create_pend token
     )
   )
+#pop-options
 
 val welcome:
   #tkt:treekem_types dy_bytes ->

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst

@@ -41,21 +41,21 @@ let as_cache_pred #ci = {
     value.time <= DY.Core.Trace.Base.length tr /\
     is_publishable (prefix tr value.time) key.verification_key /\
     get_signkey_label tr key.verification_key == principal_label value.who /\
-    get_signkey_usage key.verification_key == mk_mls_sigkey_usage value.who /\
+    key.verification_key `has_signkey_usage tr` mk_mls_sigkey_usage value.who /\
     is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable (prefix tr value.time)) key.credential
   );
   pred_later = (fun tr1 tr2 prin state_id key value -> ());
   pred_knowable = (fun tr prin state_id key value ->
-    assert(is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_knowable_by (principal_state_label prin state_id) tr) key.credential)
+    assert(is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_knowable_by (principal_tag_state_label prin as_cache_types.tag state_id) tr) key.credential)
   );
 }
 
 val has_as_cache_invariant: {|protocol_invariants|} -> prop
 let has_as_cache_invariant #invs =
   has_map_session_invariant as_cache_pred
 
-val as_cache_tag_and_invariant: {|crypto_invariants|} -> string & local_bytes_state_predicate
-let as_cache_tag_and_invariant #ci = (as_cache_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant as_cache_pred))
+val as_cache_tag_and_invariant: {|crypto_invariants|} -> dtuple2 string local_bytes_state_predicate
+let as_cache_tag_and_invariant #ci = (|as_cache_types.tag, local_state_predicate_to_local_bytes_state_predicate (map_session_invariant as_cache_pred)|)
 
 (*** AS cache API ***)
 

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst

@@ -46,7 +46,7 @@ instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invaria
   preds = treesync_crypto_predicates tkt;
 }
 
-val all_state_predicates: tkt:treekem_types dy_bytes -> list (string & local_bytes_state_predicate)
+val all_state_predicates: tkt:treekem_types dy_bytes -> list (dtuple2 string local_bytes_state_predicate)
 let all_state_predicates tkt = [
   as_cache_tag_and_invariant;
   group_manager_tag_and_invariant;
@@ -86,7 +86,7 @@ let all_sign_preds_has_all_sign_preds tkt =
 
 val all_state_predicates_has_all_state_predicates: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt)))
 let all_state_predicates_has_all_state_predicates tkt =
-  assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_state_predicates tkt)));
+  assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (all_state_predicates tkt)));
   mk_state_pred_correct (all_state_predicates tkt);
   norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt))