From ce1fa7a944fecb8d737ea32587cd6020c032d8de Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Thu, 19 Feb 2026 16:36:36 -0500 Subject: [PATCH 1/2] Fix an unstable proof (thanks to a patch from Chris), so that Vest works with a recent Verus + vstd pair --- vest/Cargo.toml | 4 +--- vest/src/regular/variant.rs | 1 + 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/vest/Cargo.toml b/vest/Cargo.toml index d92f236..6f14296 100644 --- a/vest/Cargo.toml +++ b/vest/Cargo.toml @@ -17,9 +17,7 @@ default = ["std"] std = [] [dependencies] -vstd = "=0.0.0-2026-01-11-0057" -#verus_builtin = "0.0.0-2025-08-12-1837" -#verus_builtin_macros = "0.0.0-2025-12-07-0054" +vstd = "=0.0.0-2026-02-19-1634" #vstd = { git = "https://github.com/verus-lang/verus", branch = "main" } #verus_builtin = { git = "https://github.com/verus-lang/verus", branch = "main" } diff --git a/vest/src/regular/variant.rs b/vest/src/regular/variant.rs index 94d82f7..cb52a8f 100644 --- a/vest/src/regular/variant.rs +++ b/vest/src/regular/variant.rs @@ -508,6 +508,7 @@ impl SecureSpecCombinator for OptThen where } proof fn lemma_prefix_secure(&self, s1: Seq, s2: Seq) { + vstd::slice::axiom_slice_ext_equal(&[true], &[true]); if Fst::is_prefix_secure() && Snd::is_prefix_secure() { self.0.0.0.lemma_prefix_secure(s1, s2); self.0.0.lemma_parse_length(s1); From 02b700cba9259d2d2007abbce7e3628758d03c28 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Thu, 19 Feb 2026 16:42:59 -0500 Subject: [PATCH 2/2] We don't actually need to bump the vstd version up; the proof still works with the old version as well. --- vest/Cargo.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/vest/Cargo.toml b/vest/Cargo.toml index 6f14296..9f04fa3 100644 --- a/vest/Cargo.toml +++ b/vest/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "vest_lib" -version = "0.0.1" +version = "0.0.2" edition = "2021" license = "MIT" description = "VestLib: A library of formally verified parser and serializer combinators" @@ -17,7 +17,7 @@ default = ["std"] std = [] [dependencies] -vstd = "=0.0.0-2026-02-19-1634" +vstd = "=0.0.0-2026-01-11-0057" #vstd = { git = "https://github.com/verus-lang/verus", branch = "main" } #verus_builtin = { git = "https://github.com/verus-lang/verus", branch = "main" }