Finished task 139

[amarshah1]

No description provided.

[parno]

Thanks for tackling this! Looks like there was some tricky math involved in your proof.

[parno]

It's a bit tricky to map this spec to the one in the prompt. Could we instead use something like this?

    spec fn factorial(n: int) -> int 
        decreases n,
    {
        if n <= 1 {
            0
        } else {
            n * factorial(n - 1)
        }
    }

    spec fn brazilian_factorial(n: int) -> int 
        decreases n,
    {
        if n <= 1 {
            factorial(1)
        } else {
            factorial(n) * brazilian_factorial(n - 1)
        }
    }

[parno]

Can you replace 4294967295 with u32::MAX to make the intent clearer?

I also suspect that the next requirement is a strictly stronger requirement, no?

I'm also a bit reluctant to have a requirement that asks that you already know something about the thing you're about to compute. Could we instead use a strategy similar to this version of fib?

[amarshah1]

The changes have been made. Thanks for the suggestion! This way is much simpler. I also changed 255 to u8::MAX in task025 (everything else stays the same)

[parno]

Great, thanks for the changes!