Merge branch 'main' into twal/more_trace_

src/lib/crypto/DY.Lib.Crypto.KdfExpand.Split.fst

@@ -16,7 +16,7 @@ let split_kdf_expand_usage_get_usage_params: split_function_parameters = {
     Some (tag, (prk_usage, info))
   );
 
-  local_fun_t = kdf_expand_crypto_usage;
+  local_fun_t = mk_dependent_type kdf_expand_crypto_usage;
   global_fun_t = prk_usage:usage{KdfExpandKey? prk_usage} -> info:bytes -> usage;
 
   default_global_fun = (fun prk_usage info -> NoUsage);
@@ -45,7 +45,7 @@ let split_kdf_expand_usage_get_label_params = {
     Some (tag, (prk_usage, prk_label, info))
   );
 
-  local_fun_t = kdf_expand_crypto_usage;
+  local_fun_t = mk_dependent_type kdf_expand_crypto_usage;
   global_fun_t = prk_usage:usage{KdfExpandKey? prk_usage} -> prk_label:label -> info:bytes -> label;
 
   default_global_fun = (fun prk_usage prk_label info -> prk_label);
@@ -88,7 +88,7 @@ let has_kdf_expand_usage #cusgs (tag, local_invariant) =
 val intro_has_kdf_expand_usage_get_usage:
   {|crypto_usages|} -> tagged_local_invariant:(string & kdf_expand_crypto_usage) ->
   Lemma
-  (requires has_local_fun split_kdf_expand_usage_get_usage_params kdf_expand_usage.get_usage tagged_local_invariant)
+  (requires has_local_fun split_kdf_expand_usage_get_usage_params kdf_expand_usage.get_usage (mk_dependent_tagged_local_fun tagged_local_invariant))
   (ensures has_kdf_expand_usage_get_usage tagged_local_invariant)
 let intro_has_kdf_expand_usage_get_usage #cusgs (tag, local_invariant) =
   introduce
@@ -107,7 +107,7 @@ let intro_has_kdf_expand_usage_get_usage #cusgs (tag, local_invariant) =
 val intro_has_kdf_expand_usage_get_label:
   {|crypto_usages|} -> tagged_local_invariant:(string & kdf_expand_crypto_usage) ->
   Lemma
-  (requires has_local_fun split_kdf_expand_usage_get_label_params kdf_expand_usage.get_label tagged_local_invariant)
+  (requires has_local_fun split_kdf_expand_usage_get_label_params kdf_expand_usage.get_label (mk_dependent_tagged_local_fun tagged_local_invariant))
   (ensures has_kdf_expand_usage_get_label tagged_local_invariant)
 let intro_has_kdf_expand_usage_get_label #cusgs (tag, local_invariant) =
   introduce
@@ -130,23 +130,23 @@ val mk_global_kdf_expand_usage_get_usage:
   prk_usage:usage{KdfExpandKey? prk_usage} -> info:bytes ->
   usage
 let mk_global_kdf_expand_usage_get_usage tagged_local_invariants =
-  mk_global_fun (split_kdf_expand_usage_get_usage_params) tagged_local_invariants
+  mk_global_fun (split_kdf_expand_usage_get_usage_params) (mk_dependent_tagged_local_funs tagged_local_invariants)
 
 val mk_global_kdf_expand_usage_get_label:
   list (string & kdf_expand_crypto_usage) ->
   prk_usage:usage{KdfExpandKey? prk_usage} -> prk_label:label -> info:bytes ->
   label
 let mk_global_kdf_expand_usage_get_label tagged_local_invariants =
-  mk_global_fun (split_kdf_expand_usage_get_label_params) tagged_local_invariants
+  mk_global_fun (split_kdf_expand_usage_get_label_params) (mk_dependent_tagged_local_funs tagged_local_invariants)
 
 val mk_global_kdf_expand_usage_get_label_lemma:
   tagged_local_invariants:list (string & kdf_expand_crypto_usage) ->
   tr:trace ->
   prk_usage:usage{KdfExpandKey? prk_usage} -> prk_label:label -> info:bytes ->
   Lemma ((mk_global_kdf_expand_usage_get_label tagged_local_invariants prk_usage prk_label info) `can_flow tr` prk_label)
 let mk_global_kdf_expand_usage_get_label_lemma tagged_local_invariants tr prk_usage prk_label info =
-  mk_global_fun_eq split_kdf_expand_usage_get_label_params tagged_local_invariants (prk_usage, prk_label, info);
-  introduce forall tagged_local_invariants. split_kdf_expand_usage_get_label_params.apply_local_fun tagged_local_invariants (prk_usage, prk_label, info) `can_flow tr` prk_label with (
+  mk_global_fun_eq split_kdf_expand_usage_get_label_params (mk_dependent_tagged_local_funs tagged_local_invariants) (prk_usage, prk_label, info);
+  introduce forall tag_set tagged_local_invariants. split_kdf_expand_usage_get_label_params.apply_local_fun #tag_set tagged_local_invariants (prk_usage, prk_label, info) `can_flow tr` prk_label with (
     tagged_local_invariants.get_label_lemma tr prk_usage prk_label info
   )
 
@@ -168,7 +168,9 @@ val mk_kdf_expand_usage_correct:
 let mk_kdf_expand_usage_correct #cusgs tagged_local_invariants =
   no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_invariants);
   for_allP_eq has_kdf_expand_usage tagged_local_invariants;
-  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_kdf_expand_usage_get_usage_params tagged_local_invariants));
-  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_kdf_expand_usage_get_label_params tagged_local_invariants));
+  map_dfst_mk_dependent_tagged_local_funs tagged_local_invariants;
+  FStar.Classical.forall_intro_2 (memP_mk_dependent_tagged_local_funs tagged_local_invariants);
+  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_kdf_expand_usage_get_usage_params (mk_dependent_tagged_local_funs tagged_local_invariants)));
+  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_kdf_expand_usage_get_label_params (mk_dependent_tagged_local_funs tagged_local_invariants)));
   FStar.Classical.forall_intro (FStar.Classical.move_requires intro_has_kdf_expand_usage_get_usage);
   FStar.Classical.forall_intro (FStar.Classical.move_requires intro_has_kdf_expand_usage_get_label)

src/lib/crypto/DY.Lib.Crypto.SplitPredicate.fst

@@ -55,12 +55,12 @@ let split_crypto_predicate_parameters_to_split_function_parameters (params:split
     Some (tag, (tr, key, data))
   );
 
-  local_fun_t = params.local_pred_t;
+  local_fun_t = mk_dependent_type params.local_pred_t;
   global_fun_t = params.global_pred_t;
 
   default_global_fun = params.mk_global_pred always_false;
 
-  apply_local_fun = params.apply_local_pred;
+  apply_local_fun = (fun #tag_set -> params.apply_local_pred);
   apply_global_fun = params.apply_global_pred;
   mk_global_fun = params.mk_global_pred;
   apply_mk_global_fun = params.apply_mk_global_pred;
@@ -71,7 +71,7 @@ val has_local_crypto_predicate:
   params.global_pred_t -> (string & params.local_pred_t) ->
   prop
 let has_local_crypto_predicate params global_pred (tag, local_pred) =
-  has_local_fun (split_crypto_predicate_parameters_to_split_function_parameters params) global_pred (tag, local_pred)
+  has_local_fun (split_crypto_predicate_parameters_to_split_function_parameters params) global_pred (|tag, local_pred|)
 
 val has_local_crypto_predicate_elim:
   params:split_crypto_predicate_parameters ->
@@ -90,7 +90,7 @@ val mk_global_crypto_predicate:
   list (string & params.local_pred_t) ->
   params.global_pred_t
 let mk_global_crypto_predicate params tagged_local_preds =
-  mk_global_fun (split_crypto_predicate_parameters_to_split_function_parameters params) tagged_local_preds
+  mk_global_fun (split_crypto_predicate_parameters_to_split_function_parameters params) (mk_dependent_tagged_local_funs tagged_local_preds)
 
 val mk_global_crypto_predicate_later:
   params:split_crypto_predicate_parameters ->
@@ -107,9 +107,9 @@ val mk_global_crypto_predicate_later:
 let mk_global_crypto_predicate_later params tagged_local_preds tr1 tr2 key data =
   let fparams = split_crypto_predicate_parameters_to_split_function_parameters params in
   params.apply_mk_global_pred always_false (tr1, key, data);
-  mk_global_fun_eq fparams tagged_local_preds (tr1, key, data);
-  mk_global_fun_eq fparams tagged_local_preds (tr2, key, data);
-  introduce forall lpred. fparams.apply_local_fun lpred (tr1, key, data) ==> fparams.apply_local_fun lpred (tr2, key, data) with (
+  mk_global_fun_eq fparams (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, key, data);
+  mk_global_fun_eq fparams (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, key, data);
+  introduce forall tag_set lpred. fparams.apply_local_fun lpred (tr1, key, data) ==> fparams.apply_local_fun #tag_set lpred (tr2, key, data) with (
     introduce _ ==> _ with _. params.apply_local_pred_later lpred tr1 tr2 key data
   )
 
@@ -125,5 +125,6 @@ val mk_global_crypto_predicate_correct:
   (ensures has_local_crypto_predicate params (mk_global_crypto_predicate params tagged_local_preds) (tag, local_pred))
 let mk_global_crypto_predicate_correct params tagged_local_preds tag local_pred =
   no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_preds);
-  mk_global_fun_correct (split_crypto_predicate_parameters_to_split_function_parameters params) tagged_local_preds tag local_pred
-
+  map_dfst_mk_dependent_tagged_local_funs tagged_local_preds;
+  memP_mk_dependent_tagged_local_funs tagged_local_preds tag local_pred;
+  mk_global_fun_correct (split_crypto_predicate_parameters_to_split_function_parameters params) (mk_dependent_tagged_local_funs tagged_local_preds) tag local_pred

src/lib/event/DY.Lib.Event.Typed.fst

@@ -52,7 +52,7 @@ let split_event_pred_params: split_function_parameters = {
     Some (tag, (tr, prin, content))
   ));
 
-  local_fun_t = trace -> principal -> bytes -> prop;
+  local_fun_t = mk_dependent_type (trace -> principal -> bytes -> prop);
   global_fun_t = trace -> principal -> string -> bytes -> prop;
 
   default_global_fun = (fun tr prin tag content -> False);
@@ -69,7 +69,7 @@ let split_event_pred_params: split_function_parameters = {
   apply_mk_global_fun = (fun spred x -> ());
 }
 
-type compiled_event_predicate = split_event_pred_params.local_fun_t
+type compiled_event_predicate = trace -> principal -> bytes -> prop
 
 val compile_event_pred:
   #a:Type0 -> {|event a|} ->
@@ -84,7 +84,7 @@ let compile_event_pred #a #ev epred tr prin content_bytes =
 val has_compiled_event_pred:
   {|protocol_invariants|} -> (string & compiled_event_predicate) -> prop
 let has_compiled_event_pred #invs (tag, epred) =
-  has_local_fun split_event_pred_params event_pred (tag, epred)
+  has_local_fun split_event_pred_params event_pred (|tag, epred|)
 
 val has_event_pred:
   #a:Type0 -> {|event a|} ->
@@ -96,7 +96,7 @@ let has_event_pred #a #ev #invs epred =
 
 val mk_event_pred: {|crypto_invariants|} -> list (string & compiled_event_predicate) -> trace -> principal -> string -> bytes -> prop
 let mk_event_pred #cinvs tagged_local_preds =
-  mk_global_fun split_event_pred_params tagged_local_preds
+  mk_global_fun split_event_pred_params (mk_dependent_tagged_local_funs tagged_local_preds)
 
 val mk_event_pred_correct: {|protocol_invariants|} -> tagged_local_preds:list (string & compiled_event_predicate) -> Lemma
   (requires
@@ -108,7 +108,9 @@ let mk_event_pred_correct #invs tagged_local_preds =
   reveal_opaque (`%has_compiled_event_pred) (has_compiled_event_pred);
   no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_preds);
   for_allP_eq has_compiled_event_pred tagged_local_preds;
-  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_event_pred_params tagged_local_preds))
+  map_dfst_mk_dependent_tagged_local_funs tagged_local_preds;
+  FStar.Classical.forall_intro_2 (memP_mk_dependent_tagged_local_funs tagged_local_preds);
+  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_event_pred_params (mk_dependent_tagged_local_funs tagged_local_preds)))
 
 (*** Monadic functions ***)
 

src/lib/state/DY.Lib.State.Tagged.fst

@@ -53,7 +53,7 @@ let split_local_bytes_state_predicate_params {|crypto_invariants|} : split_funct
     | None -> None
   ));
 
-  local_fun_t = local_bytes_state_predicate;
+  local_fun_t = mk_dependent_type local_bytes_state_predicate;
   global_fun_t = trace -> principal -> state_id -> bytes -> prop;
 
   default_global_fun = (fun tr prin sess_id sess_content -> False);
@@ -73,13 +73,13 @@ let split_local_bytes_state_predicate_params {|crypto_invariants|} : split_funct
 [@@ "opaque_to_smt"]
 val has_local_bytes_state_predicate: {|protocol_invariants|} -> (string & local_bytes_state_predicate) -> prop
 let has_local_bytes_state_predicate #invs (tag, spred) =
-  has_local_fun split_local_bytes_state_predicate_params state_pred.pred (tag, spred)
+  has_local_fun split_local_bytes_state_predicate_params state_pred.pred (|tag, spred|)
 
 (*** Global tagged state predicate builder ***)
 
 val mk_global_local_bytes_state_predicate: {|crypto_invariants|} -> list (string & local_bytes_state_predicate) -> trace -> principal -> state_id -> bytes -> prop
 let mk_global_local_bytes_state_predicate #cinvs tagged_local_preds =
-  mk_global_fun split_local_bytes_state_predicate_params tagged_local_preds
+  mk_global_fun split_local_bytes_state_predicate_params (mk_dependent_tagged_local_funs tagged_local_preds)
 
 #push-options "--ifuel 2" // to deconstruct nested tuples
 val mk_global_local_bytes_state_predicate_later:
@@ -88,9 +88,9 @@ val mk_global_local_bytes_state_predicate_later:
   (requires mk_global_local_bytes_state_predicate tagged_local_preds tr1 prin sess_id full_content /\ tr1 <$ tr2)
   (ensures mk_global_local_bytes_state_predicate tagged_local_preds tr2 prin sess_id full_content)
 let mk_global_local_bytes_state_predicate_later #cinvs tagged_local_preds tr1 tr2 prin sess_id full_content =
-  mk_global_fun_eq split_local_bytes_state_predicate_params tagged_local_preds (tr1, prin, sess_id, full_content);
-  mk_global_fun_eq split_local_bytes_state_predicate_params tagged_local_preds (tr2, prin, sess_id, full_content);
-  introduce forall lpred content. split_local_bytes_state_predicate_params.apply_local_fun lpred (tr1, prin, sess_id, content) ==> split_local_bytes_state_predicate_params.apply_local_fun lpred (tr2, prin, sess_id, content) with (
+  mk_global_fun_eq split_local_bytes_state_predicate_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, prin, sess_id, full_content);
+  mk_global_fun_eq split_local_bytes_state_predicate_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, prin, sess_id, full_content);
+  introduce forall tag_set lpred content. split_local_bytes_state_predicate_params.apply_local_fun #tag_set lpred (tr1, prin, sess_id, content) ==> split_local_bytes_state_predicate_params.apply_local_fun lpred (tr2, prin, sess_id, content) with (
     introduce _ ==> _ with _. lpred.pred_later tr1 tr2 prin sess_id content
   )
 #pop-options
@@ -102,11 +102,11 @@ val mk_global_local_bytes_state_predicate_knowable:
   (requires mk_global_local_bytes_state_predicate tagged_local_preds tr prin sess_id full_content)
   (ensures is_knowable_by (principal_state_label prin sess_id) tr full_content)
 let mk_global_local_bytes_state_predicate_knowable #cinvs tagged_local_preds tr prin sess_id full_content =
-  mk_global_fun_eq split_local_bytes_state_predicate_params tagged_local_preds (tr, prin, sess_id, full_content);
+  mk_global_fun_eq split_local_bytes_state_predicate_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr, prin, sess_id, full_content);
   match split_local_bytes_state_predicate_params.decode_tagged_data (tr, prin, sess_id, full_content) with
   | Some (tag, (_, _, _, content)) -> (
-    match find_local_fun split_local_bytes_state_predicate_params tagged_local_preds tag with
-    | Some lpred -> (
+    match find_local_fun split_local_bytes_state_predicate_params (mk_dependent_tagged_local_funs tagged_local_preds) tag with
+    | Some (|_, lpred|) -> (
       lpred.pred_knowable tr prin sess_id content;
       serialize_parse_inv_lemma tagged_state full_content;
       serialize_wf_lemma tagged_state (is_knowable_by (principal_state_label prin sess_id) tr) ({tag; content})
@@ -133,7 +133,9 @@ let mk_state_pred_correct #invs tagged_local_preds =
   reveal_opaque (`%has_local_bytes_state_predicate) (has_local_bytes_state_predicate);
   no_repeats_p_implies_for_all_pairsP_unequal (List.Tot.map fst tagged_local_preds);
   for_allP_eq has_local_bytes_state_predicate tagged_local_preds;
-  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_local_bytes_state_predicate_params tagged_local_preds))
+  map_dfst_mk_dependent_tagged_local_funs tagged_local_preds;
+  FStar.Classical.forall_intro_2 (FStar.Classical.move_requires_2 (mk_global_fun_correct split_local_bytes_state_predicate_params (mk_dependent_tagged_local_funs tagged_local_preds)));
+  FStar.Classical.forall_intro_2 (memP_mk_dependent_tagged_local_funs tagged_local_preds)
 
 (*** Predicates on trace ***)