Fibonacci (proofs + loop)

staload _ = "prelude/DATS/integer.dats"

dataprop FIB (int, int) =
| FIB0 (0, 0) | FIB1 (1, 1)
| {n: nat} {r0, r1: int} FIB2 (n + 2, r0 + r1) of (FIB (n, r0), FIB (n + 1, r1))

fun fibver {n: nat} .<>. (n: int n) : [r: int] (FIB (n, r) | int r) =
let
    var r0: int = 0
    var r1: int = 1
    var i : int = 0

    prvar pf0 = FIB0 ()
    prvar pf1 = FIB1 ()

    val () =
    while* {i: nat; r0, r1: int | i <= n} .<n - i>. (pf0: FIB (i, r0), pf1: FIB (i + 1, r1), i: int(i), r0: int r0, r1: int r1) : [r: int] (pf0 : FIB (n, r), r0: int r) => (i < n)
    {
        val () = i := i + 1
        val tmp = r0 + r1
        val () = r0 := r1
        val () = r1 := tmp
    
        prval pf1_ = pf1
        prval pf0_ = pf0
        prval pftmp = FIB2 (pf0_, pf1_)
        prval () = pf0 := pf1_
        prval () = pf1 := pftmp
    }
in
    (pf0 | r0)
end

implement main0 () = () where
{
    val () = println! ((fibver(10)).1)
    val () = println! ((fibver(20)).1)
}