use ::ghosts::vestibule::*;

type Nat = u64;

fn fibo (
    ghost_ctx: Ectoplasm,
    n: Ghost,
) -> Nat
{
    let n = ghost_ctx.materialize(n);
    ghost!(#[tag(decreases)] #[no_init] { n });
    match n {
        | 0 => 0,
        | 1 => 1,
        | _ => {
            fibo(ghost_ctx, ghost!(n - 1))
            +
            fibo(ghost_ctx, ghost!(n - 2))
        },
    }
}

fn lemma_fibo_is_monotonic (
    ghost_ctx: Ectoplasm,
    i: Ghost,
    j: Ghost,
)
{
    let i = ghost_ctx.materialize(i);
    let j = ghost_ctx.materialize(j);
    ghost!(#[tag(requires)] #[no_init] { i <= j });
    ghost!(#[tag(ensures)] #[no_init] { i <= j });
    ghost!(#[tag(ensures)] #[no_init] {
        fibo(ghost_ctx, ghost!(i)) <= fibo(ghost_ctx, ghost!(j))
    });
    ghost!(#[tag(decreases)] #[no_init] { j - 1 });

    match () {
        | _case if i < 2 && j < 2 => {},
        | _case if i == j => {},
        | _case if i == j - 1 => {
            // reveal_with_fuel(fibo, 2);
            lemma_fibo_is_monotonic(ghost_ctx, ghost!(i), ghost!(j - 1));
        },
        | _default => {
            lemma_fibo_is_monotonic(ghost_ctx, ghost!(i), ghost!(j - 1));
            lemma_fibo_is_monotonic(ghost_ctx, ghost!(i), ghost!(j - 2));
        },
    }
}

fn fibo_fits_u64 (
    ghost_ctx: Ectoplasm,
    n: Ghost,
) -> bool
{
    fibo(ghost_ctx, n) <= 0xffff_ffff_ffff_ffff
}

fn assume (
    _: bool
)
{}

fn fibo_impl (n: u64)
  -> u64
{
    ghost!(#[tag(requires)] #[no_init] |ectoplasm| {
        fibo_fits_u64(ectoplasm, ghost!(n))
    });
    ghost!(#[tag(ensures)] #[no_init] |ectoplasm| {
        materialize_return!() == fibo(ectoplasm, ghost!(n))
    });

    if n == 0 {
        return 0;
    }
    let mut prev: u64 = 0;
    let mut cur: u64 = 1;
    let mut i: u64 = 1;
    while i < n {
        ghost!(#[tag(invariant)] #[no_init] |ectoplasm| [
            i > 0,
            i <= n,
            fibo_fits_u64(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] n as Nat),
            ),
            fibo_fits_u64(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] i as Nat),
            ),
            cur == fibo(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] i),
            ),
            prev == fibo(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] { i as Nat - 1 }),
            ),
        ]);
        ghost!(#[tag(proof)] {
            assume(cur as Nat + prev <= 0xffff_ffff_ffff_ffff);
        });
        let new_cur = cur + prev;
        prev = cur;
        cur = new_cur;
        i += 1;
        ghost!(#[tag(proof)] |ectoplasm| {
            lemma_fibo_is_monotonic(ectoplasm,
                ghost!(#[tag(spec_expr)] #[no_init] { i }),
                ghost!(#[tag(spec_expr)] #[no_init] { n }),
            );
        });
    }
    cur
}