From a590c14f17f1e36699e9b5d31d859a07e2f9599c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Tue, 13 Feb 2024 10:06:45 +0100 Subject: [PATCH] chore: update F* & fix regressions --- flake.lock | 12 ++++++------ fstar/test/MLS.Test.FromExt.TreeOperations.fst | 1 + 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/flake.lock b/flake.lock index 11616cf..ec4c926 100644 --- a/flake.lock +++ b/flake.lock @@ -62,11 +62,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1706891748, - "narHash": "sha256-oqWC0SCGyFQ/qaVOHE5qB24G8xYEJFQo8fTwADUO4Ow=", + "lastModified": 1707789277, + "narHash": "sha256-mIF1jQia02Lz9okv/ElmzVKe82+YxIFuVZSdPOn/dLw=", "owner": "FStarLang", "repo": "FStar", - "rev": "58c915a86a2c07c8eca8d9deafd76cb7a91f0eb7", + "rev": "7579c2df5849cea38190be6994a7acaf9109f0b9", "type": "github" }, "original": { @@ -94,11 +94,11 @@ "hacl-star-src": { "flake": false, "locked": { - "lastModified": 1706898309, - "narHash": "sha256-n6KYj60fdu8ZzCkI9BYM7ylxLjKpGYW5/83rzDwyG7E=", + "lastModified": 1707754589, + "narHash": "sha256-nNrS5LqYTU0i0uwCFLLEQH94FujZB3KVvXB0ZAzENbY=", "owner": "hacl-star", "repo": "hacl-star", - "rev": "2f5f95bc0ced5f51b3a9ecf59b870722749ec8a1", + "rev": "eb1badfa34c70b0bbe0fe24fe0f49fb1295c7872", "type": "github" }, "original": { diff --git a/fstar/test/MLS.Test.FromExt.TreeOperations.fst b/fstar/test/MLS.Test.FromExt.TreeOperations.fst index 580c098..100fc56 100644 --- a/fstar/test/MLS.Test.FromExt.TreeOperations.fst +++ b/fstar/test/MLS.Test.FromExt.TreeOperations.fst @@ -40,6 +40,7 @@ let test_tree_operations_one t = let bl = bytes_like_bytes in let tree_before = extract_option "tree_before" (((ps_prefix_to_ps_whole (ps_ratchet_tree_nt tkt))).parse (hex_string_to_bytes t.tree_before)) in let (|l, treesync_before|) = extract_result (ratchet_tree_to_treesync tree_before) in + assert((pow2 l) `divides` 0); let proposal = extract_option "proposal" (((ps_prefix_to_ps_whole (ps_proposal_nt))).parse (hex_string_to_bytes t.proposal)) in let proposal_sender = FStar.UInt32.v t.proposal_sender in let (|_, treesync_after|): l:nat & treesync bytes tkt l 0 =