Skip to content

Commit

Permalink
chore: update F* and DY*
Browse files Browse the repository at this point in the history
  • Loading branch information
@TWal
TWal committed Jan 6, 2025
1 parent 35a1775 commit 81ce141
Show file tree
Hide file tree
Showing 4 changed files with 49 additions and 43 deletions.
12 changes: 6 additions & 6 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

70 changes: 36 additions & 34 deletions fstar/common/symbolic/MLS.Crypto.Derived.Symbolic.SignWithLabel.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,17 +15,18 @@ open MLS.Result

noeq
type signwithlabel_crypto_pred {|crypto_usages|} = {
pred: trace -> sk_usg:usage{SigKey? sk_usg} -> msg:bytes -> prop;
pred: trace -> sk_usg:usage{SigKey? sk_usg} -> vk:bytes -> msg:bytes -> prop;
pred_later:
tr1:trace -> tr2:trace ->
sk_usg:usage{SigKey? sk_usg} -> msg:bytes ->
sk_usg:usage{SigKey? sk_usg} -> vk:bytes -> msg:bytes ->
Lemma
(requires
pred tr1 sk_usg msg /\
pred tr1 sk_usg vk msg /\
bytes_well_formed tr1 vk /\
bytes_well_formed tr1 msg /\
tr1 <$ tr2
)
(ensures pred tr2 sk_usg msg)
(ensures pred tr2 sk_usg vk msg)
;
}

Expand All @@ -40,38 +41,38 @@ let split_signwithlabel_crypto_pred_params {|crypto_usages|}: split_function_par
FStar.Classical.move_requires_2 get_mls_label_inj tag_set_1 tag_set_2
);

tagged_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes);
raw_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes);
tagged_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes & bytes);
raw_data_t = (trace & (sk_usg:usage{SigKey? sk_usg}) & bytes & bytes);
output_t = prop;

decode_tagged_data = (fun (tr, vk, data) -> (
decode_tagged_data = (fun (tr, sk_usage, vk, data) -> (
match parse (sign_content_nt bytes) data with
| Some ({label; content}) -> Some (label, (tr, vk, content))
| Some ({label; content}) -> Some (label, (tr, sk_usage, vk, content))
| None -> None
));

local_fun_t = mk_dependent_type signwithlabel_crypto_pred;
global_fun_t = trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> prop;
global_fun_t = trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> bytes -> prop;

default_global_fun = (fun tr vk content -> False);
default_global_fun = (fun tr sk_usage vk content -> False);


apply_local_fun = (fun pred (tr, vk, content) -> pred.pred tr vk content);
apply_global_fun = (fun pred (tr, vk, msg) -> pred tr vk msg);
mk_global_fun = (fun pred tr vk msg -> pred (tr, vk, msg));
apply_local_fun = (fun pred (tr, sk_usage, vk, content) -> pred.pred tr sk_usage vk content);
apply_global_fun = (fun pred (tr, sk_usage, vk, msg) -> pred tr sk_usage vk msg);
mk_global_fun = (fun pred tr sk_usage vk msg -> pred (tr, sk_usage, vk, msg));
apply_mk_global_fun = (fun _ _ -> ());
}

#push-options "--ifuel 1"
val has_signwithlabel_pred: {|crypto_usages|} -> sign_crypto_predicate -> (valid_label & signwithlabel_crypto_pred) -> prop
let has_signwithlabel_pred #cusgs sign_pred (lab, local_pred) =
forall tr vk msg.
{:pattern sign_pred.pred tr vk msg}
forall tr sk_usage vk msg.
{:pattern sign_pred.pred tr sk_usage vk msg}
match parse (sign_content_nt bytes) msg with
| Some {label; content} -> (
label == get_mls_label lab ==> (
sign_pred.pred tr vk msg ==
local_pred.pred tr vk content
sign_pred.pred tr sk_usage vk msg ==
local_pred.pred tr sk_usage vk content
)
)
| _ -> True
Expand All @@ -85,47 +86,48 @@ val intro_has_signwithlabel_pred:
(ensures has_signwithlabel_pred sign_pred (tag, local_pred))
let intro_has_signwithlabel_pred #cusgs sign_pred tag local_pred =
introduce
forall tr vk msg.
forall tr sk_usage vk msg.
match parse (sign_content_nt bytes) msg with
| Some {label; content} -> (
label == get_mls_label tag ==> (
sign_pred.pred tr vk msg ==
local_pred.pred tr vk content
sign_pred.pred tr sk_usage vk msg ==
local_pred.pred tr sk_usage vk content
)
)
| _ -> True
with (
has_local_fun_elim split_signwithlabel_crypto_pred_params sign_pred.pred tag local_pred (tr, vk, msg)
has_local_fun_elim split_signwithlabel_crypto_pred_params sign_pred.pred tag local_pred (tr, sk_usage, vk, msg)
)

val mk_global_mls_sign_pred:
{|crypto_usages|} ->
list (valid_label & signwithlabel_crypto_pred) ->
trace -> sk_usg:usage{SigKey? sk_usg} -> bytes ->
trace -> sk_usg:usage{SigKey? sk_usg} -> bytes -> bytes ->
prop
let mk_global_mls_sign_pred tagged_local_preds vk msg =
mk_global_fun split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) vk msg
let mk_global_mls_sign_pred tagged_local_preds sk_usage vk msg =
mk_global_fun split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) sk_usage vk msg

#push-options "--ifuel 2"
val mk_global_mls_sign_pred_later:
{|crypto_usages|} ->
tagged_local_preds:list (valid_label & signwithlabel_crypto_pred) ->
tr1:trace -> tr2:trace ->
sk_usg:usage{SigKey? sk_usg} -> msg:bytes ->
sk_usg:usage{SigKey? sk_usg} -> vk:bytes -> msg:bytes ->
Lemma
(requires
mk_global_mls_sign_pred tagged_local_preds tr1 sk_usg msg /\
mk_global_mls_sign_pred tagged_local_preds tr1 sk_usg vk msg /\
bytes_well_formed tr1 vk /\
bytes_well_formed tr1 msg /\
tr1 <$ tr2
)
(ensures mk_global_mls_sign_pred tagged_local_preds tr2 sk_usg msg)
let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 sk_usg msg =
mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, sk_usg, msg);
mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, sk_usg, msg);
(ensures mk_global_mls_sign_pred tagged_local_preds tr2 sk_usg vk msg)
let mk_global_mls_sign_pred_later tagged_local_preds tr1 tr2 sk_usg vk msg =
mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr1, sk_usg, vk, msg);
mk_global_fun_eq split_signwithlabel_crypto_pred_params (mk_dependent_tagged_local_funs tagged_local_preds) (tr2, sk_usg, vk, msg);
FStar.Classical.move_requires (parse_wf_lemma (sign_content_nt bytes) (bytes_well_formed tr1)) msg;
introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, sk_usg, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, sk_usg, content) with (
introduce forall tag_set lpred content. bytes_well_formed tr1 content /\ split_signwithlabel_crypto_pred_params.apply_local_fun lpred (tr1, sk_usg, vk, content) ==> split_signwithlabel_crypto_pred_params.apply_local_fun #tag_set lpred (tr2, sk_usg, vk, content) with (
introduce _ ==> _ with _. (
lpred.pred_later tr1 tr2 sk_usg content
lpred.pred_later tr1 tr2 sk_usg vk content
)
)
#pop-options
Expand Down Expand Up @@ -180,7 +182,7 @@ val bytes_invariant_sign_with_label:
sk `has_usage tr` mk_mls_sigkey_usage prin /\
nonce `has_usage tr` SigNonce /\
(get_label tr sk) `can_flow tr` (get_label tr nonce) /\ (
spred.pred tr (mk_mls_sigkey_usage prin) msg
spred.pred tr (mk_mls_sigkey_usage prin) (vk sk) msg
\/
get_label tr sk `can_flow tr` public
) /\
Expand Down Expand Up @@ -213,7 +215,7 @@ val bytes_invariant_verify_with_label:
)
(ensures
(
spred.pred tr (mk_mls_sigkey_usage prin) content
spred.pred tr (mk_mls_sigkey_usage prin) vk content
) \/ (
(get_signkey_label tr vk) `can_flow tr` public
)
Expand Down
4 changes: 4 additions & 0 deletions fstar/treemath/MLS.TreeMath.Internal.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,7 @@ let get_bit_lemma x k =
lemma_lemma q k;
FStar.Math.Lemmas.small_mod (((q%2)*(pow2 k)) + (x%(pow2 k))) (pow2 (k+1))

#push-options "--z3rlimit 500"
val is_left_node_left: x:nat{level x <> 0} -> Lemma (is_left_node (left x) == true)
let is_left_node_left x =
//Z3 really has troube proving this inside the proof, hence this separate lemma
Expand All @@ -312,7 +313,9 @@ let is_left_node_left x =
is_left_node_lemma x xl q k;
FStar.Math.Lemmas.small_div (x % (pow2 (k-1))) (pow2 k);
FStar.Math.Lemmas.cancel_mul_mod q 2
#pop-options

#push-options "--z3rlimit 500"
val is_right_node_right: x:nat{level x <> 0} -> Lemma (is_left_node (right x) == false)
let is_right_node_right x =
//Z3 really has troube proving this inside the proof, hence this separate lemma
Expand All @@ -334,6 +337,7 @@ let is_right_node_right x =
assert (xr/(pow2 k) == 1 + 2*q);
FStar.Math.Lemmas.lemma_mod_plus_distr_r 1 (2*q) 2;
FStar.Math.Lemmas.cancel_mul_mod q 2
#pop-options

(*** Proofs: parent of left/right node ***)

Expand Down
6 changes: 3 additions & 3 deletions fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ val leaf_node_sign_pred:
{|crypto_usages|} -> treekem_types bytes ->
signwithlabel_crypto_pred
let leaf_node_sign_pred #cu tkt = {
pred = (fun tr sk_usg ln_tbs_bytes ->
pred = (fun tr sk_usg vk ln_tbs_bytes ->
match (parse (leaf_node_tbs_nt bytes tkt) ln_tbs_bytes) with
| None -> False
| Some ln_tbs -> (
Expand All @@ -137,7 +137,7 @@ let leaf_node_sign_pred #cu tkt = {
)
)
);
pred_later = (fun tr1 tr2 vk ln_tbs_bytes ->
pred_later = (fun tr1 tr2 sk_usg vk ln_tbs_bytes ->
parse_wf_lemma (leaf_node_tbs_nt bytes tkt) (bytes_well_formed tr1) ln_tbs_bytes;
introduce forall prin tr group_id (tl:tree_list 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 (
Expand Down Expand Up @@ -329,7 +329,7 @@ let parent_hash_implies_event #ci #tkt #l #i tr group_id t ast =
serialize_wf_lemma (leaf_node_tbs_nt bytes tkt) (bytes_invariant tr) ln_tbs;
bytes_invariant_verify_with_label (leaf_node_sign_pred tkt) tr authentifier ln.data.signature_key "LeafNodeTBS" ln_tbs_bytes ln.signature;

introduce ((leaf_node_sign_pred tkt).pred tr (mk_mls_sigkey_usage authentifier) ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
introduce ((leaf_node_sign_pred tkt).pred tr (mk_mls_sigkey_usage authentifier) ln.data.signature_key ln_tbs_bytes) ==> tree_has_event authentifier tr group_id (|l, i, (canonicalize t authentifier_li)|)
with _. (
(
parse_serialize_inv_lemma #bytes (leaf_node_tbs_nt bytes tkt) ln_tbs;
Expand Down

0 comments on commit 81ce141

Please sign in to comment.