chore: update F* and fix regressions

Inria-Prosecco · Mar 20, 2024 · 44e03a2 · 44e03a2
1 parent ac6175f
commit 44e03a2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/fstar/treesync/proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst b/fstar/treesync/proofs/MLS.TreeSync.Invariants.ParentHash.Proofs.fst
@@ -251,6 +251,7 @@ let rec filtered_resolution_are_leaves_imply_are_sorted #bytes #bl #tkt #l #i p
   match t with
   | TLeaf _ -> ()
   | TNode None left right -> (
+    assert(forall (x:node_index) l. List.Tot.mem x l <==> List.Tot.memP x l);
     filter_append p (resolution left) (resolution right);
     FStar.Classical.forall_intro (List.Tot.append_mem (List.Tot.filter p (resolution left)) (List.Tot.filter p (resolution right)));
     filtered_resolution_are_leaves_imply_are_sorted p left;