AlphaVerus

Advanced Proof: String Manipulation Lemma

Shows complex string reasoning with detailed verification steps

Specification

proof fn lemma_step_subrange(substring: Seq, string: Seq)
    requires
        substring.len() > 0,
        string.len() >= substring.len(),
    ensures
        (substring[0] == string.subrange(0, substring.len() as int)[0] && (substring.skip(1)
            =~= string.skip(1).subrange(0, substring.skip(1).len() as int))) ==> (substring
            =~= string.subrange(0, substring.len() as int)),
    decreases substring.len(),

Code + Proof (Generated by AlphaVerus)

let m = substring.len();
let n = string.len();
assert(m > 0);
assert(m <= n);
let h = string.subrange(0, m as int);
assert(h.len() == m);
assert(substring.len() == h.len());
if substring[0] == h[0] {
    let k = substring.skip(1).len();
    assert(k == h.skip(1).len());
    let g = string.skip(1).subrange(0, k as int);
    assert(g.len() == k);
    assert(k == substring.len() - 1);
    assert(k == h.len() - 1);
    if m > 1 {
        if substring.skip(1) =~= g {
            assert(substring[0] == h[0]);
            assert(substring.len() == g.len() + 1);
            assert(substring.len() == h.len());
            assert(forall|i: nat| 0 <= i && i < m ==> substring[i as int] == h[i as int]) by {
                assert(substring[0] == h[0]);
                assert(substring.skip(1) =~= g);
                assert(forall|i: nat| 1 <= i && i < m ==> substring[i as int] == g[i as int - 1]);
                assert(substring =~= h);
            }
            assert(substring =~= h);
        } else {
            assert(!(substring =~= h));
        }
    } else {
        assert(substring =~= h);
    }
} else {
    assert(!(substring =~= h));
}

Translation Example: Dafny to Verus

All Code is AlphaVerus-Generated

Translation of Recursive Implementation

use vstd::prelude::*;

verus! {
fn search_recursive(a: &Vec, i: usize, j: usize, x: i32) -> (k: i32)
    requires
        0 <= i && i <= j && j <= a.len(),
        j - i < 100000,
        j <= i32::MAX as usize,
    ensures
        i <= k && k < j || k == -1,
        k != -1 ==> a[k as int] == x,
        k != -1 ==> forall|r: nat| k < r && r < j ==> a[r as int] != x,
        k == -1 ==> forall|r: nat| i <= r && r < j ==> a[r as int] != x,
    decreases
        j - i,
{
    if j == i {
        -1
    } else if a[j - 1] == x {
        assert(j - 1 <= i32::MAX as usize);
        if j - 1 <= i32::MAX as usize {
            (j - 1) as i32
        } else {
            -1
        }
    } else {
        search_recursive(a, i, j - 1, x)
    }
}

Translation of Iterative Implementation

fn search_loop(a: &Vec, i: usize, j: usize, x: i32) -> (k: i32)
    requires
        0 <= i && i <= j && j <= a.len(),
        j - i < 100000,
        j <= i32::MAX as usize,
    ensures
        i <= k && k < j || k == -1,
        k != -1 ==> a[k as int] == x,
        k != -1 ==> forall|r: nat| k < r && r < j ==> a[r as int] != x,
        k == -1 ==> forall|r: nat| i <= r && r < j ==> a[r as int] != x,
{
    if i == j {
        return -1;
    }
    let mut t: usize = j;
    while t > i
        invariant
            0 <= i <= t && t <= j,
            t <= a.len(),
            forall|p: nat| t <= p && p < j ==> a[p as int] != x,
            t <= i32::MAX as usize,
        decreases
            t,
    {
        assert(t <= a.len());
        if a[t - 1] == x {
            if t - 1 <= i32::MAX as usize {
                return (t - 1) as i32;
            } else {
                return -1;
            }
        } else {
            assert(t > i);
            t = t - 1;
        }
    }
    -1
}