completed programs roughly from 70 to 80

[edwin1729]

No description provided.

[parno]

Thanks for making so much progress on so many tasks! This is great to see.

As a minor suggestion, inside the Verus code base, we typically topologically sort our files, so that the leaf functions are at the top, and the entrypoint is at the bottom. Doing that here might make things a bit easier to review in some cases (like for Task 70).

[parno]

This spec says that anything that we return contains the substring and was in the original strings list. To match the English description's intention, I think it might need to be strengthened to say that if there is a string in strings that contains the substring, then it will appear in res.

I wonder if this spec might be expressed using a filter, e.g., res@ == strings@.filter(|s| s.has_substring(substring), for a suitable definition of has_substring.

[edwin1729]

I've rewritten the the spec to capture the prompt

[parno]

I think this version captures the property I mentioned above, but I think it might have lost the property your previous version included. In other words, I think your current spec would allow the function to return the entire input list.

Perhaps you could show that combining your two versions of the spec imply the filter-based spec above.

[parno]

Is it possible to show that this is equivalent to this?

ret <==> exists|i: int| x == #[trigger] (i * i * i),

That's what I was initially expecting to see, given the English prompt.

[WeetHet]

@parno is it okay if a program verifies with cvc5 and doesn't with z3?

At the moment, cvc5 support is still pretty experimental, so I think we should aim to get everything to verify with Z3.

Could you help me with 034? I can't get it to work with z3

This should work.

fn unique_sorted(s: Vec<i32>) -> (result: Vec<i32>)
    requires
        forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j],
    ensures
        forall|i: int, j: int| 0 <= i < j < result.len() ==> result[i] < result[j],
        forall|i: int| #![auto] 0 <= i < result.len() ==> s@.contains(result[i]),
        forall|i: int| #![trigger s[i]] 0 <= i < s.len() ==> result@.contains(s[i]),
{
    let mut result: Vec<i32> = vec![];
    for i in 0..s.len()
        invariant
            forall|i: int, j: int| 0 <= i < j < s.len() ==> s[i] <= s[j],
            forall|k: int, l: int| 0 <= k < l < result.len() ==> result[k] < result[l],
            forall|k: int|
                #![trigger result[k]]
                0 <= k < result.len() ==> (exists|m: int| 0 <= m < i && result[k] == s[m]),
            forall|m: int| #![trigger s[m]] 0 <= m < i ==> result@.contains(s[m]),
    {
        let ghost pre = result;
        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(result@.contains(s[i as int])) by {
            assert(result[result.len() - 1] == s[i as int]);
        }
    }
    result
}

Also include

use vstd::seq_lib::lemma_seq_contains_after_push;

in the front.

PS: I ran your 034 with CVC5 but it did not pass. Did you use verus -V cvc5 human_eval_034.rs ? Or am I missing a flag?

PS2: Another way to do 034 is probably creating a HashSet from Vec, but it probably involves extending vstd.

Weird, maybe it's because I have cvc5 1.2.0 and not 1.1.2?

[ahuoguo]

PS: I ran your 034 with CVC5 but it did not pass. Did you use verus -V cvc5 human_eval_034.rs ? Or am I missing a flag?

Weird, maybe it's because I have cvc5 1.2.0 and not 1.1.2?

Huh! It was indeed a version issue (it passed on my end after using cvc5 1.20 instead of 1.12). That's interesting.

[parno]

I added a few responses to the latest edits. It looks like you also added some new files? If so, I haven't looked at them yet; I wasn't sure if they were ready for review. It might be easier to do them in a separate PR (or at least do any new tasks on a separate PR).

[parno]

I think this version captures the property I mentioned above, but I think it might have lost the property your previous version included. In other words, I think your current spec would allow the function to return the entire input list.

Perhaps you could show that combining your two versions of the spec imply the filter-based spec above.

[edwin1729]

Hi sorry for the prolonged silence. I intend to complete these programs slowly over weekends now that term has started for me. Thanks as always for the feedback

[parno]

No problem -- we totally understand you have other demands on your time!

[parno]

Just wanted to check in on the status of this PR. If it seems unlikely you'll be able to work on them, could we split off the completed tasks into a separate PR, so that we can merge them into main?

[edwin1729]

@parno I've made a new PR with all programs with no unresolved threads or admits copied to a new PR.

#34

It ci seems to be broken