Skip to content

Commit

Permalink
feat(split fun): make local_pred_t dependent on tag_set_t (#59)
Browse files Browse the repository at this point in the history 
* feat(split fun): make `local_pred_t` dependent on `tag_set_t`

* update F*

* apply Clara's remark
  • Loading branch information
@TWal
TWal authored Oct 14, 2024
1 parent ac82925 commit 4fe16e8
Show file tree
Hide file tree
Showing 5 changed files with 118 additions and 65 deletions.
22 changes: 12 additions & 10 deletions src/lib/crypto/DY.Lib.Crypto.KdfExpand.Split.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
)

Expand All @@ -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)
19 changes: 10 additions & 9 deletions src/lib/crypto/DY.Lib.Crypto.SplitPredicate.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 ->
Expand All @@ -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 ->
Expand All @@ -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
)

Expand All @@ -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
12 changes: 7 additions & 5 deletions src/lib/event/DY.Lib.Event.Typed.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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|} ->
Expand All @@ -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|} ->
Expand All @@ -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
Expand All @@ -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 ***)

Expand Down
22 changes: 12 additions & 10 deletions src/lib/state/DY.Lib.State.Tagged.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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:
Expand All @@ -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
Expand All @@ -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})
Expand All @@ -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 ***)

Expand Down
Loading

2 comments on commit 4fe16e8

@mtzguido
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi @TWal , looks like this broke mls-star?

* Error 189 at fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst(54,16-54,41):
  - Expected expression of type _: MLS.Crypto.Derived.valid_label -> Type
    got expression signwithlabel_crypto_pred
    of type Type

1 error was reported (see above)

Ran into it here https://github.com/mtzguido/FStar/actions/runs/11333532252

@TWal
Copy link
Collaborator Author

@TWal TWal commented on 4fe16e8 Oct 15, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes indeed, will fix it!
Probably the check-world action shouldn't update DY*, I will investigate the nix invocation to do that. F* developers shouldn't worry about the dependencies MLS* - DY*.

Please sign in to comment.