Use Seq drop_last in recursive definitions

[Chris-Hawblitzel]

I noticed that some recursive functions in seq_lib.rs (e.g. max, min, max_via, min_via) are defined in terms of drop_first or subrange(1, ...). If we used drop_last instead, the Seq indices would line up and proofs should require less manual work, especially if we add the following axiom (which Dafny uses for seq take):

#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_seq_subrange_index_zero<A>(s: Seq<A>, k: int, i: int)
    requires
        0 <= i < k <= s.len(),
    ensures
        (#[trigger] s.subrange(0, k))[i] == #[trigger] s[i],
{
}

[parno]

If we used drop_last instead, the Seq indices would line up

I'm not sure which set of indices you have in mind here.

proofs should require less manual work

I'm all for less manual work, and the axiom you have above (which hopefully one day would be proven) seems reasonable. In Dafny, however, it seemed like the style of "operate on the head of a sequence and recurse on the tail" generally provided better automation than your proposed "operate on the tail and recurse on the prefix". Related to the above, can you expand on why the latter is likely to automate better in Verus?

[Chris-Hawblitzel]

Sorry, I should have written more detail. I have in mind proofs like the following in Dafny:

function first<A>(s: seq<A>): A requires |s| > 0 { s[0] }
function last<A>(s: seq<A>): A requires |s| > 0 { s[|s| - 1] }
function drop_first<A>(s: seq<A>): seq<A> requires |s| > 0 { s[1..] }
function drop_last<A>(s: seq<A>): seq<A> requires |s| > 0 { s[0..|s| - 1] }

type t
predicate P(x: t)
predicate Q(x: t)

lemma l(x: t)
    requires P(x)
    ensures Q(x)

lemma test_drop_first(s: seq<t>)
    requires forall i: int :: 0 <= i < |s| ==> P(s[i])
    ensures  forall i: int :: 0 <= i < |s| ==> Q(s[i])
{
    if |s| > 0 {
        l(first(s));
        test_drop_first(drop_first(s));
    }
}

lemma test_drop_last(s: seq<t>)
    requires forall i: int :: 0 <= i < |s| ==> P(s[i])
    ensures  forall i: int :: 0 <= i < |s| ==> Q(s[i])
{
    if |s| > 0 {
        l(last(s));
        test_drop_last(drop_last(s));
    }
}

Both work as-is in Dafny. The relevant Dafny axioms for drop_first are:

axiom (forall<T> s: Seq T, n: int, j: int :: 
  {:weight 25} { Seq#Index(Seq#Drop(s, n), j) } 
  0 <= n && 0 <= j && j < Seq#Length(s) - n
     ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n));

axiom (forall<T> s: Seq T, n: int, k: int :: 
  {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) } 
  0 <= n && n <= k && k < Seq#Length(s)
     ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k));

The relevant Dafny axiom for drop_last is:

axiom (forall<T> s: Seq T, n: int, j: int :: 
  {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) } 
  0 <= j && j < n && j < Seq#Length(s)
     ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j));

Notice that there's an asymmetry in these axioms, with the single axiom for drop_last ("Take") and the two axioms for drop_first (Drop). This is because Drop has to perform arithmetic (j + n and k - n) to adjust the indices, whereas Take simply keeps the indices as is. As pointed out in dafny-lang/dafny@0d19591 , the arithmetic has the potential to lead to matching loops ("To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results."). (Also see dafny-lang/dafny@c766cf3 .)

For the drop_last style (Take), this matching loop doesn't occur, and I don't think any weight-based mitigation should be necessary.

I don't think this is specific to Verus; I think the issues are the same as in Dafny. In both Verus and Dafny, I would expect the drop_last style to provide at least as good automation as drop_first, and possibly better because no weights need to be used to suppress quantifier instantiations, and without the issue of the matching loops arising.

[parno]

Ahh, I see -- thanks for the clarification! I hadn't realized how much tweaking Dafny was doing to those axioms.

For trusted specs, I think I find algorithms that pull off the head slightly easier to read, but if the spec uses last and drop_last, it should still be pretty readable, and if it provides better automation, that seems like it's probably a net win.