In the aim to use the SplitPredicate module for KDF invariants, that are functions outputting usage or label, I first generalized the module to support functions (noting that predicates are functions to prop).
I also generalized the tag encoding mechanism so that local functions are associated with a set of tags. I hoped it would be useful to split the invariants of KDF.Extract, but now I'm not convinced it would be useful toward that goal. Anyway, I feel this is still an improvement to the encode_tag mechanism that felt quite ad-hoc (because it was), this mechanism is strictly more generic, by using the following translation:
let tag_set_t = old.tag_t
let tag_t = old.encoded_tag_t
let tag_belong_to tag tag_set =
tag = old.encode_tag tag_set
let cant_belong_to_disjoint_sets tag tag_set_1 tag_set_2 =
FStar.Classical.move_requires_3 old.encode_tag_inj tag_set_1 tag_set_2
meaning that the encode_tag mechanism can only be used to represent single-element tag sets.
In the process, I also greatly simplified the proofs of the SplitFunction module!
In the aim to use the SplitPredicate module for KDF invariants, that are functions outputting
usageorlabel, I first generalized the module to support functions (noting that predicates are functions toprop).I also generalized the tag encoding mechanism so that local functions are associated with a set of tags. I hoped it would be useful to split the invariants of KDF.Extract, but now I'm not convinced it would be useful toward that goal. Anyway, I feel this is still an improvement to the
encode_tagmechanism that felt quite ad-hoc (because it was), this mechanism is strictly more generic, by using the following translation:meaning that the
encode_tagmechanism can only be used to represent single-element tag sets.In the process, I also greatly simplified the proofs of the SplitFunction module!