Data independent memcmp

My try at validating the memcmp function from this Tor diff using Frama-C. The loop_precondition is what I'm stuck on.

/*@ predicate IsValidRange( unsigned char *a, integer n ) =   @     ( 0 <= n ) && \valid_range( a, 0, n - 1 );
  @*/
/*@ requires \valid(x) && \valid(y);
  @ assigns nothing;
  @ 
  @ behavior zero_length:
  @  assumes len == 0;
  @  ensures \result == 0;
  @
  @ behavior equal:
  @  assumes len > 0;
  @  assumes x_y_equal : \forall integer n;
  @     0 <= n < len ==> x[n] == y[n];
  @  requires IsValidRange(x, len);
  @  requires IsValidRange(y, len);
  @  ensures \result == 0;
  @
  @ behavior not_equal:
  @  assumes len > 0;
  @  assumes x_y_not_equal : \exists integer n;
  @    0 <= n < len ==> x[n] != y[n];
  @  requires IsValidRange(x, len);
  @  requires IsValidRange(y, len);
  @  ensures \result != 0;
  @
  @ complete behaviors zero_length, equal, not_equal;
  @ disjoint behaviors zero_length, equal, not_equal;
  @*/
int
tor_memcmp(const unsigned char *x, const unsigned char *y, unsigned int len)
{
    unsigned int i = len;
    int retval = 0, newval;
    if (len == 0) return 0;
    while (i--) {
        //@ assert loop_precondition: (retval == 0) || (\exists integer n; i < n < len && x[i] != y[i]);
        int v1 = x[i];
        int v2 = y[i];
        int equal_p = v1 ^ v2;
        //@ assert (x[i] == y[i] && equal_p == 0) || (x[i] != y[i] && 0 < equal_p <= 255);
        // relies on two's complement!
        --equal_p;
        //@ assert (x[i] == y[i] && equal_p == -1) || (x[i] != y[i] && 0 <= equal_p < 255);
        // relies on signed right shift!
        equal_p >>= 8;
        //@ assert (x[i] == y[i] && equal_p == -1) || (x[i] != y[i] && equal_p =>= 0);
        newval = retval & equal_p;
        //@ assert (x[i] == y[i] && retval == newval) || (x[i] != y[i] && newval == 0);
        retval = newval;
        newval = retval + (v1 - v2);
        //@ assert (x[i] == y[i] && newval == retval) || (x[i] != y[i] && newval == (v1 - v2));
        retval = newval;
    }   
    return retval;
}