cleanup: make tree_create create a non-blank node

Inria-Prosecco · Nov 21, 2024 · 4beb781 · 4beb781
1 parent 6f93999
commit 4beb781
Show file tree

Hide file tree

Showing 8 changed files with 9 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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: