chore: update F* and DY*

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

@@ -20,7 +20,12 @@ type signwithlabel_crypto_pred {|crypto_usages|} = {
     tr1:trace -> tr2:trace ->
     vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
     Lemma
-    (requires pred tr1 vk msg /\ tr1 <$ tr2)
+    (requires
+      pred tr1 vk msg /\
+      bytes_well_formed tr1 vk /\
+      bytes_well_formed tr1 msg /\
+      tr1 <$ tr2
+    )
     (ensures pred tr2 vk msg)
   ;
 }
@@ -111,14 +116,19 @@ val mk_global_mls_sign_pred_later:
   Lemma
   (requires
     mk_global_mls_sign_pred tagged_local_preds tr1 vk msg /\
+    bytes_well_formed tr1 vk /\
+    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 tagged_local_preds (tr1, vk, msg);
   mk_global_fun_eq split_signwithlabel_crypto_pred_params tagged_local_preds (tr2, vk, msg);
-  introduce forall lpred content. split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, vk, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr2, vk, content) with (
-    introduce _ ==> _ with _. lpred.pred_later tr1 tr2 vk content
+  FStar.Classical.move_requires (parse_wf_lemma (sign_content_nt bytes) (bytes_well_formed tr1)) msg;
+  introduce forall 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 lpred (tr2, vk, content) with (
+    introduce _ ==> _ with _. (
+      lpred.pred_later tr1 tr2 vk content
+    )
   )
 #pop-options
 
@@ -168,21 +178,21 @@ val bytes_invariant_sign_with_label:
     bytes_invariant tr msg /\
     get_usage sk == SigKey "MLS.LeafSignKey" empty /\
     SigNonce? (get_usage nonce) /\
-    (get_label sk) `can_flow tr` (get_label nonce) /\
+    (get_label tr sk) `can_flow tr` (get_label tr nonce) /\
     spred.pred tr (vk sk) msg /\
     has_mls_signwithlabel_pred (lab, spred)
   )
   (ensures
     bytes_invariant tr (Success?.v (sign_with_label sk lab msg nonce)) /\
-    (get_label (Success?.v (sign_with_label sk lab msg nonce))) `can_flow tr` (get_label msg)
+    (get_label tr (Success?.v (sign_with_label sk lab msg nonce))) `can_flow tr` (get_label tr msg)
   )
 let bytes_invariant_sign_with_label #ci spred tr sk lab msg nonce =
   let sign_content: sign_content_nt bytes = {
     label = get_mls_label lab;
     content = msg;
   } in
   serialize_wf_lemma (sign_content_nt bytes) (bytes_invariant tr) sign_content;
-  serialize_wf_lemma (sign_content_nt bytes) (is_knowable_by (get_label msg) tr) sign_content
+  serialize_wf_lemma (sign_content_nt bytes) (is_knowable_by (get_label tr msg) tr) sign_content
 
 val bytes_invariant_verify_with_label:
   {|ci:crypto_invariants|} -> spred:signwithlabel_crypto_pred -> tr:trace ->
@@ -200,7 +210,7 @@ val bytes_invariant_verify_with_label:
       get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty ==>
       spred.pred tr vk content
     ) \/ (
-      (get_signkey_label vk) `can_flow tr` public 
+      (get_signkey_label tr vk) `can_flow tr` public
     )
   )
 let bytes_invariant_verify_with_label #ci spred tr vk lab content signature =

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

@@ -6,6 +6,8 @@ open DY.Lib
 open MLS.NetworkTypes
 open MLS.Symbolic
 
+#set-options "--fuel 0 --ifuel 0"
+
 (*** Group manager types & invariants ***)
 
 [@@ with_bytes dy_bytes]
@@ -31,6 +33,7 @@ instance group_manager_types: map_types group_manager_key group_manager_value =
   ps_value_t = ps_group_manager_value;
 }
 
+#push-options "--ifuel 1"
 val group_manager_pred: {|crypto_invariants|} -> map_predicate group_manager_key group_manager_value #_
 let group_manager_pred #ci = {
   pred = (fun tr prin state_id key value ->
@@ -39,6 +42,7 @@ let group_manager_pred #ci = {
   pred_later = (fun tr1 tr2 prin state_id key value -> ());
   pred_knowable = (fun tr prin state_id key value -> ());
 }
+#pop-options
 
 val has_group_manager_invariant: {|protocol_invariants|} -> prop
 let has_group_manager_invariant #invs =

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

@@ -432,7 +432,7 @@ let commit #tkt #l #li p as_session gmgr_session group_id path =
   set_public_treesync_state p group_session.si_public new_st;*
   return (Some ())
 
-#push-options "--z3rlimit 50"
+#push-options "--z3rlimit 100"
 val commit_proof:
   {|protocol_invariants|} ->
   #tkt:treekem_types dy_bytes -> #l:nat -> #li:leaf_index l 0 ->

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

@@ -40,9 +40,9 @@ instance as_cache_types: map_types as_cache_key as_cache_value = {
 val as_cache_pred: {|crypto_invariants|} -> map_predicate as_cache_key as_cache_value #_
 let as_cache_pred #ci = {
   pred = (fun tr prin state_id key value ->
-    value.time <= DY.Core.Trace.Type.length tr /\
+    value.time <= DY.Core.Trace.Base.length tr /\
     is_publishable (prefix tr value.time) key.verification_key /\
-    get_signkey_label key.verification_key == principal_label value.who /\
+    get_signkey_label tr key.verification_key == principal_label value.who /\
     get_signkey_usage key.verification_key == SigKey value.usg empty /\
     is_well_formed_whole (ps_prefix_to_ps_whole ps_credential_nt) (is_publishable (prefix tr value.time)) key.credential
   );

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

@@ -45,10 +45,10 @@ val dy_asp: {|crypto_invariants|} -> trace -> as_parameters dy_bytes
 let dy_asp #ci tr = {
   token_t = dy_as_token;
   credential_ok = (fun (vk, cred) token ->
-    token.time <= (DY.Core.Trace.Type.length tr) /\
+    token.time <= (DY.Core.Trace.Base.length tr) /\
     bytes_invariant (prefix tr token.time) vk /\
     get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty /\
-    get_signkey_label vk == principal_label token.who
+    get_signkey_label tr vk == principal_label token.who
   );
   valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
     True
@@ -146,22 +146,23 @@ let leaf_node_sign_pred #cu tkt = {
         match ln_tbs.data.source with
         | LNS_commit -> (
           exists (tl: tree_list dy_bytes tkt).
-            get_signkey_label vk == principal_label prin /\
+            get_signkey_label tr vk == principal_label prin /\
             tree_list_starts_with_tbs tl ln_tbs_bytes /\
             tree_list_is_parent_hash_linkedP tl /\
             tree_list_ends_at_root tl /\
             tree_list_is_canonicalized ln_tbs.leaf_index tl /\
             tree_list_has_event prin tr ln_tbs.group_id tl
         )
         | LNS_update -> (
-          get_signkey_label vk == principal_label prin /\
+          get_signkey_label tr vk == principal_label prin /\
           tree_has_event prin tr ln_tbs.group_id (|0, ln_tbs.leaf_index, TLeaf (Some ({data = ln_tbs.data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|)
         )
         | LNS_key_package -> True
         )
     )
   );
   pred_later = (fun tr1 tr2 vk ln_tbs_bytes ->
+    parse_wf_lemma (leaf_node_tbs_nt dy_bytes tkt) (bytes_well_formed tr1) ln_tbs_bytes;
     introduce forall prin tr group_id (tl:tree_list dy_bytes tkt). tree_list_has_event prin tr group_id tl <==> (forall x. List.Tot.memP x tl ==> tree_has_event prin tr group_id x)
     with (
       for_allP_eq (tree_has_event prin tr group_id) tl
@@ -357,7 +358,7 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
       parse_serialize_inv_lemma #dy_bytes (leaf_node_tbs_nt dy_bytes tkt) ln_tbs;
 
       eliminate exists (prin:principal) (leaf_tl: tree_list dy_bytes tkt).
-        get_signkey_label ln.data.signature_key == principal_label prin /\
+        get_signkey_label tr ln.data.signature_key == principal_label prin /\
         tree_list_starts_with_tbs leaf_tl ln_tbs_bytes /\
         tree_list_is_parent_hash_linkedP leaf_tl /\
         tree_list_ends_at_root leaf_tl /\
@@ -660,8 +661,8 @@ val is_msg_external_path_to_path:
     is_knowable_by label tr group_id /\
     bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\
     bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
-    get_label sk == principal_label prin /\
-    get_label nonce == principal_label prin /\
+    get_label tr sk == principal_label prin /\
+    get_label tr nonce == principal_label prin /\
     has_leaf_node_tbs_invariant tkt
   )
   (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (external_path_to_path t p group_id sk nonce)))
@@ -686,7 +687,7 @@ let is_msg_external_path_to_path #ci #tkt #l #li prin label tr t p group_id sk n
   let tl = path_to_tree_list t unsigned_path in
   path_to_tree_list_lemma t unsigned_path;
   introduce exists prin tl.
-    get_signkey_label (vk sk) == principal_label prin /\
+    get_signkey_label tr (vk sk) == principal_label prin /\
     tree_list_starts_with_tbs tl new_ln_tbs_bytes /\
     tree_list_is_parent_hash_linkedP tl /\
     tree_list_ends_at_root tl /\
@@ -716,8 +717,8 @@ val is_msg_sign_leaf_node_data_key_package:
     is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\
     bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\
     bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
-    get_label sk == principal_label prin /\
-    get_label nonce == principal_label prin /\
+    get_label tr sk == principal_label prin /\
+    get_label tr nonce == principal_label prin /\
     has_leaf_node_tbs_invariant tkt
   )
   (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (sign_leaf_node_data_key_package ln_data sk nonce)))
@@ -746,8 +747,8 @@ val is_msg_sign_leaf_node_data_update:
     is_knowable_by label tr group_id /\
     bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" empty /\
     bytes_invariant tr nonce /\ get_usage nonce == SigNonce /\
-    get_label sk == principal_label prin /\
-    get_label nonce == principal_label prin /\
+    get_label tr sk == principal_label prin /\
+    get_label tr nonce == principal_label prin /\
     has_leaf_node_tbs_invariant tkt
   )
   (ensures is_well_formed _ (is_knowable_by label tr) (Success?.v (sign_leaf_node_data_update ln_data group_id leaf_index sk nonce)))