chore: update DY*

Inria-Prosecco · Jul 24, 2024 · b3e4f94 · b3e4f94
1 parent f57dc7d
commit b3e4f94
Show file tree

Hide file tree

Showing 8 changed files with 25 additions and 23 deletions.
diff --git a/Makefile b/Makefile
@@ -11,7 +11,7 @@ INNER_SOURCE_DIRS = api bootstrap common/code common/proofs glue/code glue/proof
 HACL_SNAPSHOT_DIR = $(MLS_HOME)/hacl-star-snapshot
 SOURCE_DIRS = $(addprefix $(MLS_HOME)/fstar/, $(INNER_SOURCE_DIRS))
 
-DY_INCLUDE_DIRS = core lib lib/comparse lib/event lib/state lib/utils
+DY_INCLUDE_DIRS = core lib lib/comparse lib/crypto lib/event lib/state lib/utils
 INCLUDE_DIRS = $(SOURCE_DIRS) $(HACL_SNAPSHOT_DIR)/lib $(HACL_SNAPSHOT_DIR)/specs $(COMPARSE_HOME)/src $(if $(USE_DY), $(addprefix $(DY_HOME)/src/, $(DY_INCLUDE_DIRS)))
 FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS))
 

diff --git a/flake.lock b/flake.lock
diff --git a/fstar/symbolic/MLS.Symbolic.fst b/fstar/symbolic/MLS.Symbolic.fst
@@ -159,7 +159,7 @@ let split_sign_pred_params {|crypto_usages|}: split_function_parameters = {
 
 val has_sign_pred: crypto_invariants -> (valid_label & mls_sign_pred) -> prop
 let has_sign_pred ci (lab, spred) =
-  has_local_fun split_sign_pred_params (sign_pred #ci) (lab, spred)
+  has_local_fun split_sign_pred_params ((sign_pred #ci).pred) (lab, spred)
 
 #push-options "--z3rlimit 25"
 val bytes_invariant_sign_with_label:
@@ -258,7 +258,7 @@ val mk_sign_pred_correct:
   ci:crypto_invariants -> lspred:list (valid_label & mls_sign_pred) ->
   Lemma
   (requires
-    sign_pred == mk_sign_pred lspred /\
+    sign_pred.pred == mk_sign_pred lspred /\
     List.Tot.no_repeats_p (List.Tot.map fst lspred)
   )
   (ensures for_allP (has_sign_pred ci) lspred)

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
@@ -222,7 +222,7 @@ instance parseable_serializeable_treesync_private_state: parseable_serializeable
 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 ->
-    is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key
+    is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key
   );
   pred_later = (fun tr1 tr2 prin state_id st -> ());
   pred_knowable = (fun tr prin state_id st -> ());
@@ -254,7 +254,7 @@ val new_private_treesync_state_proof:
   tr:trace ->
   Lemma
   (requires
-    is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key /\
+    is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
     trace_invariant tr /\
     has_treesync_private_state_invariant invs
   )
@@ -276,7 +276,7 @@ val set_private_treesync_state_proof:
   tr:trace ->
   Lemma
   (requires
-    is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key /\
+    is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key /\
     trace_invariant tr /\
     has_treesync_private_state_invariant invs
   )
@@ -307,7 +307,7 @@ val get_private_treesync_state_proof:
       match opt_result with
       | None -> True
       | Some st ->
-        is_signature_key "MLS.LeafSignKey" (principal_label prin) tr st.signature_key
+        is_signature_key (SigKey "MLS.LeafSignKey" empty) (principal_label prin) tr st.signature_key
     )
   ))
 let get_private_treesync_state_proof #invs prin state_id tr = ()
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
@@ -494,7 +494,7 @@ val create_signature_keypair:
   p:principal ->
   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* signature_key = mk_rand (SigKey "MLS.LeafSignKey" empty) (principal_label p) 32 in
   let verification_key = vk signature_key in
   guard (length (signature_key <: dy_bytes) < pow2 30);*?
   guard (length (verification_key <: dy_bytes) < pow2 30);*?
@@ -517,7 +517,7 @@ val create_signature_keypair_proof:
       match opt_res with
       | None -> True
       | Some (private_si, verification_key) ->
-        is_verification_key "MLS.LeafSignKey" (principal_label p) tr_out verification_key
+        is_verification_key (SigKey "MLS.LeafSignKey" empty) (principal_label p) tr_out verification_key
     )
   ))
 let create_signature_keypair_proof #invs p tr = ()

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
@@ -43,7 +43,7 @@ let as_cache_pred #ci = {
     value.time <= DY.Core.Trace.Type.length tr /\
     is_publishable (prefix tr value.time) key.verification_key /\
     get_signkey_label key.verification_key == principal_label value.who /\
-    get_signkey_usage key.verification_key == SigKey value.usg /\
+    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
   );
   pred_later = (fun tr1 tr2 prin state_id key value -> ());

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
@@ -27,10 +27,12 @@ let all_sign_preds tkt = [
 val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates treesync_crypto_usages
 let treesync_crypto_predicates tkt = {
   default_crypto_predicates treesync_crypto_usages with
-  sign_pred = mk_sign_pred (all_sign_preds tkt);
-  sign_pred_later = (fun tr1 tr2 vk msg ->
-    mk_sign_pred_later (all_sign_preds tkt) tr1 tr2 vk msg
-  );
+  sign_pred = {
+    pred = mk_sign_pred (all_sign_preds tkt);
+    pred_later = (fun tr1 tr2 vk msg ->
+      mk_sign_pred_later (all_sign_preds tkt) tr1 tr2 vk msg
+    );
+  }
 }
 
 instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invariants = {
@@ -49,7 +51,7 @@ let all_state_predicates tkt = [
 
 val treesync_trace_invariants: tkt:treekem_types dy_bytes -> trace_invariants (treesync_crypto_invariants tkt)
 let treesync_trace_invariants tkt = {
-  state_pred = mk_state_predicate (treesync_crypto_invariants tkt) (all_state_predicates tkt);
+  state_pred = mk_state_pred (treesync_crypto_invariants tkt) (all_state_predicates tkt);
   event_pred = mk_event_pred [];
 }
 
@@ -78,7 +80,7 @@ let treesync_global_usage_has_leaf_node_tbs_invariant 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 (treesync_protocol_invariants tkt)) (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)));
-  mk_global_local_bytes_state_predicate_correct (treesync_protocol_invariants tkt) (all_state_predicates tkt);
+  mk_state_pred_correct (treesync_protocol_invariants tkt) (all_state_predicates tkt);
   norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP (has_local_bytes_state_predicate (treesync_protocol_invariants tkt)) (all_state_predicates tkt))
 
 val treesync_protocol_invariants_has_as_cache_invariant: tkt:treekem_types dy_bytes -> Lemma

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -46,7 +46,7 @@ let dy_asp #ci tr = {
   credential_ok = (fun (vk, cred) token ->
     token.time <= (DY.Core.Trace.Type.length tr) /\
     bytes_invariant (prefix tr token.time) vk /\
-    get_signkey_usage vk == SigKey "MLS.LeafSignKey" /\
+    get_signkey_usage vk == SigKey "MLS.LeafSignKey" empty /\
     get_signkey_label vk == principal_label token.who
   );
   valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->
@@ -657,7 +657,7 @@ val is_msg_external_path_to_path:
     is_well_formed _ (is_knowable_by label tr) t /\
     is_well_formed _ (is_knowable_by label tr) p /\
     is_knowable_by label tr group_id /\
-    bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" /\
+    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 /\
@@ -713,7 +713,7 @@ val is_msg_sign_leaf_node_data_key_package:
     Success? (sign_leaf_node_data_key_package ln_data sk nonce) /\
     leaf_node_has_event prin tr ({data = ln_data; group_id = (); leaf_index = ();}) /\
     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" /\
+    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 /\
@@ -743,7 +743,7 @@ val is_msg_sign_leaf_node_data_update:
     tree_has_event prin tr group_id (|0, (leaf_index <: nat), TLeaf (Some ({data = ln_data; signature = empty #dy_bytes;} <: leaf_node_nt dy_bytes tkt))|) /\
     is_well_formed_prefix (ps_leaf_node_data_nt tkt) (is_knowable_by label tr) ln_data /\
     is_knowable_by label tr group_id /\
-    bytes_invariant tr sk /\ get_usage sk == SigKey "MLS.LeafSignKey" /\
+    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 /\