From 61d0f6a3cca9849fe9ce415b653dae8c691b3326 Mon Sep 17 00:00:00 2001 From: WeetHet Date: Thu, 19 Sep 2024 09:35:42 +0300 Subject: [PATCH] Make 034 verify without cvc5 Co-authored-by: Bryan Parno --- tasks/human_eval_034.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tasks/human_eval_034.rs b/tasks/human_eval_034.rs index efa889d..4a5fe3e 100644 --- a/tasks/human_eval_034.rs +++ b/tasks/human_eval_034.rs @@ -8,6 +8,7 @@ HumanEval/34 use vstd::calc; use vstd::prelude::*; use vstd::seq_lib::lemma_multiset_commutative; +use vstd::seq_lib::lemma_seq_contains_after_push; verus! { @@ -142,15 +143,16 @@ fn unique_sorted(s: Vec) -> (result: Vec) if result.len() == 0 || result[result.len() - 1] != s[i] { assert(result.len() == 0 || result[result.len() - 1] < s[i as int]); result.push(s[i]); + assert forall|m: int| #![trigger s[m]] 0 <= m < i implies result@.contains(s[m]) by { + assert(pre@.contains(s@[m])); + lemma_seq_contains_after_push(pre@, s@[i as int], s@[m]); + }; } assert(forall|m: int| #![trigger result@[m], pre@[m]] 0 <= m < pre.len() ==> pre@.contains(result@[m]) ==> result@.contains(pre@[m])) by { assert(forall|m: int| 0 <= m < pre.len() ==> result@[m] == pre@[m]); } - assert(forall|m: int| - #![trigger s@[m]] - 0 <= m < i ==> pre@.contains(s[m]) && result@.contains(s[m])); assert(result@.contains(s[i as int])) by { assert(result[result.len() - 1] == s[i as int]); }