Emit Rust code

[johnterickson]

Rust is a particularly interesting language to interop with Dafny because of it's strong types, anti-aliasing guarantees, memory safety, and performance optimizations.

An example of how this could light up well is if Dafny could turn expect #547 expressions into compiler optimization hints. Here's the a Rust version of the binary search example that I wrote by hand:

pub extern fn binary_search(a: &[i32], key: i32) -> Option<usize> {
    let mut lo = 0;
    let mut hi = a.len();
    while lo < hi {
        let mid = lo + (hi - lo) / 2;

        // expect mid < |len|;
        if !(mid < a.len()) { unsafe { unreachable_unchecked(); } }

        if key < a[mid] {
            hi = mid;
        } else if a[mid] < key {
            lo = mid + 1;
        } else {
            return Some(mid);
        }
    }

    return None;
}

The resulting code (at least via MSVC) contains no bounds checks for a[mid] when the (faked) expect clause is included - cool!

[robin-aws]

I responded on #547, but then realized we can actually do better than your example!

Because the Dafny verifier requires all array indexes to be provably safe, we should be able to compile all Dafny array operations to unsafe Rust array operations, since Dafny is already responsible for the bounds checking. There's a version of binary search in the Dafny test suite here that doesn't need expect to verify and therefore wouldn't have the indirect bounds check either:

dafny/Test/dafny4/BinarySearch.dfy

Lines 55 to 76 in 14c5be9

	method BinarySearchInt32_good(a: array<int>, key: int) returns (r: int32)
	requires a.Length < 0x8000_0000
	requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
	ensures 0 <= r ==> r < a.Length as int32 && a[r] == key
	ensures r < 0 ==> key !in a[..]
	{
	var lo, hi := 0, a.Length as int32;
	while lo < hi
	invariant 0 <= lo <= hi <= a.Length as int32
	invariant key !in a[..lo] && key !in a[hi..]
	{
	var mid := lo + (hi - lo) / 2; // this is how to do it
	if key < a[mid] {
	hi := mid;
	} else if a[mid] < key {
	lo := mid + 1;
	} else {
	return mid;
	}
	}
	return -1;
	}

expect is useful for situations where you can't or don't want to statically guarantee an assertion holds, but in most cases like this one it's not necessary.

[MikaelMayer]

In the current development of the Dafny to Rust code generator, arrays will be encoding using slices and accesses will be using unchecked access. So I'm happy to close this issue !
Note that we might want a debugging mode in which we encode arrays using vec just in case the code does not pass verification, to remain somehow memory safe, but it's not planned as of today.

[MikaelMayer]

Let me leave it open until the branch is merged into master