I’m working on a demonstration of a Dafny proof that an operation takes constant time, or at least a fairly constant number of machine cycles. It’s the kind of thing you need when you’re trying to prevent side-channel-attacks. Here’s what I have so far:

method IndexOf( s: seq<int>, value: int) returns (index: int)
    // Answers the index of value in s:
    requires value in s
    ensures 0 <= index < |s|
    ensures s[index] == value
    ensures value !in s[0..index]
{
    ghost var numIterations := 0;
    ghost var numFirstBranch := 0;

    var result := -1;
    for i := 0 to |s|
        invariant result == -1 ==> value !in s[0..i]
        invariant result < |s|
        invariant result >= 0 ==> value !in s[0..result]
        invariant result >= 0 ==> s[result] == value
        invariant numIterations == i
        invariant result != -1 ==> numFirstBranch==1
        invariant result == -1 ==> numFirstBranch==0
        { numIterations := numIterations + 1;
            if (s[i] == value) && (result == -1) 
            { numFirstBranch := numFirstBranch + 1;
                result := i;
            }
        }
    assert numIterations == |s|;
    assert numFirstBranch == 1;
    return result;
}

Sorry about the huge number of loop invariants – they’re all necessary. But this does satisfies the timing constraints – for a given length of sequence s, the number of executions of each different path is constant.

Alas, though, that’s not correct, because the test (s[i] == value) && (result == -1) actually involves two different execution paths, since the RHS will not be evaluated if the LHS is false.

The C programming solution, replacing && with &, doesn’t work – Dafny won’t accept & between two booleans (why???). Casting the booleans to integers isn’t allowed either.

I’m stuck. How can I test two expressions together without involving multiple execution paths?