f.rs

#![feature(register_tool)]
#![register_tool(flux)]

#[flux::refined_by(fin: int, fout: int)]
#[flux::invariant(fin >= 0)]
#[flux::invariant(fout > 0)]
#[flux::invariant(fout >= fin)]
#[derive(Debug)]
enum Fact {
    #[flux::variant(Fact[0, 1])]
    Zero,
    #[flux::variant((Box<Fact[@fi2, @fo2]>) -> Fact[fi2 + 1, (fi2 + 1)*fo2])]
    N(Box<Fact>),
}

#[flux::refined_by(fin: int, fout: int)]
#[derive(Debug)]
struct FactAns {
    #[flux::field(i32[@fout])]
    ans: i32,
    #[flux::field(Fact[@fin, @fout])]
    proof: Fact,
}

impl FactAns {
    #[flux::sig(fn(ans: i32, Fact[@fin, ans]) -> FactAns{v : v.fin == fin && v.fout == ans})]
    fn new(ans: i32, proof: Fact) -> FactAns {
        FactAns { ans, proof }
    }
}

#[flux::sig(fn(n: i32{m : m >= 0}) -> FactAns{v : v.fin == n})]
fn fact(n: i32) -> FactAns {
    let mut p = Fact::Zero;
    let mut f = 1;
    let mut m = 0;
    while m < n {
        p = Fact::N(Box::new(p));
        m = m + 1;
        f = f * m;
    }
    FactAns::new(f, p)
}