From 4beb781995c4f629b4d26f8e0c0c694c35c9333f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Thu, 21 Nov 2024 20:13:28 +0100 Subject: [PATCH] cleanup: make `tree_create` create a non-blank node --- fstar/common/code/MLS.TreeCommon.fst | 4 ++-- fstar/treekem/code/MLS.TreeKEM.API.Tree.fst | 2 +- fstar/treesync/code/MLS.TreeSync.API.fst | 2 +- fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst | 2 +- .../proofs/MLS.TreeSync.Invariants.AuthService.Proofs.fst | 2 +- .../proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst | 2 +- .../proofs/MLS.TreeSync.Invariants.UnmergedLeaves.Proofs.fst | 2 +- .../proofs/MLS.TreeSync.Invariants.ValidLeaves.Proofs.fst | 2 +- 8 files changed, 9 insertions(+), 9 deletions(-) diff --git a/fstar/common/code/MLS.TreeCommon.fst b/fstar/common/code/MLS.TreeCommon.fst index 727b459..f0e0425 100644 --- a/fstar/common/code/MLS.TreeCommon.fst +++ b/fstar/common/code/MLS.TreeCommon.fst @@ -9,9 +9,9 @@ open MLS.Tree val tree_create: #leaf_t:Type -> #node_t:Type -> leaf_t -> - tree leaf_t node_t 0 0 + tree (option leaf_t) node_t 0 0 let tree_create lp = - TLeaf lp + TLeaf (Some lp) (*** Common tree operations ***) diff --git a/fstar/treekem/code/MLS.TreeKEM.API.Tree.fst b/fstar/treekem/code/MLS.TreeKEM.API.Tree.fst index 54ac29c..b86504c 100644 --- a/fstar/treekem/code/MLS.TreeKEM.API.Tree.fst +++ b/fstar/treekem/code/MLS.TreeKEM.API.Tree.fst @@ -23,7 +23,7 @@ val create: let create #bytes #cb dec_key enc_key = { levels = 0; - tree = TLeaf (Some ({public_key = enc_key} <: treekem_leaf bytes)); + tree = tree_create ({public_key = enc_key} <: treekem_leaf bytes); priv = PLeaf dec_key } diff --git a/fstar/treesync/code/MLS.TreeSync.API.fst b/fstar/treesync/code/MLS.TreeSync.API.fst index a0e96ec..10969fc 100644 --- a/fstar/treesync/code/MLS.TreeSync.API.fst +++ b/fstar/treesync/code/MLS.TreeSync.API.fst @@ -94,7 +94,7 @@ let finalize_create #bytes #cb #tkt #asp #group_id #ln pend token = ({ levels = 0; tree = tree_create ln; - tokens = MLS.TreeCommon.tree_create (Some token); + tokens = MLS.TreeCommon.tree_create token; }) val finalize_create_valid: diff --git a/fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst b/fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst index afcdd24..5b90b4e 100644 --- a/fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst +++ b/fstar/treesync/code/MLS.TreeSync.Refined.Operations.fst @@ -27,7 +27,7 @@ let tree_create #bytes #cb #tkt #group_id ln = unmerged_leaves_ok_tree_create ln; parent_hash_invariant_tree_create ln; valid_leaves_invariant_tree_create group_id ln; - tree_create (Some ln) + tree_create ln val tree_add: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> diff --git a/fstar/treesync/proofs/MLS.TreeSync.Invariants.AuthService.Proofs.fst b/fstar/treesync/proofs/MLS.TreeSync.Invariants.AuthService.Proofs.fst index 59ddcc4..fa644a0 100644 --- a/fstar/treesync/proofs/MLS.TreeSync.Invariants.AuthService.Proofs.fst +++ b/fstar/treesync/proofs/MLS.TreeSync.Invariants.AuthService.Proofs.fst @@ -30,7 +30,7 @@ val all_credentials_ok_tree_create: ln:leaf_node_nt bytes tkt -> token:asp.token_t -> Lemma (requires asp.credential_ok (ln.data.signature_key, ln.data.credential) token) - (ensures all_credentials_ok (tree_create (Some ln)) (tree_create (Some token))) + (ensures all_credentials_ok (tree_create ln) (tree_create token)) let all_credentials_ok_tree_create #bytes #bl #tkt ln token = () val all_credentials_ok_tree_add: diff --git a/fstar/treesync/proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst b/fstar/treesync/proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst index 50bcf94..fdaf481 100644 --- a/fstar/treesync/proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst +++ b/fstar/treesync/proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst @@ -570,7 +570,7 @@ val parent_hash_invariant_tree_create: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> ln:leaf_node_nt bytes tkt -> Lemma - (parent_hash_invariant (tree_create (Some ln))) + (parent_hash_invariant (tree_create ln)) let parent_hash_invariant_tree_create #bytes #cb #tkt ln = () val parent_hash_invariant_mk_blank_tree: #bytes:Type0 -> {|crypto_bytes bytes|} -> #tkt:treekem_types bytes -> l:nat -> i:tree_index l -> Lemma (parent_hash_invariant (mk_blank_tree l i <: treesync bytes tkt l i)) diff --git a/fstar/treesync/proofs/MLS.TreeSync.Invariants.UnmergedLeaves.Proofs.fst b/fstar/treesync/proofs/MLS.TreeSync.Invariants.UnmergedLeaves.Proofs.fst index 8fe907b..a4170a6 100644 --- a/fstar/treesync/proofs/MLS.TreeSync.Invariants.UnmergedLeaves.Proofs.fst +++ b/fstar/treesync/proofs/MLS.TreeSync.Invariants.UnmergedLeaves.Proofs.fst @@ -22,7 +22,7 @@ val unmerged_leaves_ok_tree_create: #bytes:Type0 -> {|bytes_like bytes|} -> #tkt:treekem_types bytes -> ln:leaf_node_nt bytes tkt -> Lemma - (unmerged_leaves_ok (tree_create (Some ln))) + (unmerged_leaves_ok (tree_create ln)) let unmerged_leaves_ok_tree_create #bytes #bl #tkt ln = () (*** Update/Remove ***) diff --git a/fstar/treesync/proofs/MLS.TreeSync.Invariants.ValidLeaves.Proofs.fst b/fstar/treesync/proofs/MLS.TreeSync.Invariants.ValidLeaves.Proofs.fst index d5f095b..14dbcf1 100644 --- a/fstar/treesync/proofs/MLS.TreeSync.Invariants.ValidLeaves.Proofs.fst +++ b/fstar/treesync/proofs/MLS.TreeSync.Invariants.ValidLeaves.Proofs.fst @@ -19,7 +19,7 @@ val valid_leaves_invariant_tree_create: group_id:mls_bytes bytes -> ln:leaf_node_nt bytes tkt -> Lemma (requires leaf_is_valid ln group_id 0) - (ensures valid_leaves_invariant group_id (tree_create (Some ln))) + (ensures valid_leaves_invariant group_id (tree_create ln)) let valid_leaves_invariant_tree_create #bytes #cb #tkt group_id ln = () val valid_leaves_invariant_tree_add: