Add fibonacci example to the Guide to illustrate how spec, proof, and exec code work together #1354
Conversation
|
When talking with some folks learning Verus, they said that Section 3 of the guide gave them some understanding of the mode system, but they were still confused about how you were supposed to use the different modes, and (despite the table in opening section), which modes call which other modes. I thought this might help with some of that confusion. I'm open to suggestions for other examples, however. |
| if i < 2 && j < 2 { | ||
| } else if i == j { | ||
| } else if i == j - 1 { | ||
| assert(fib(j) == fib((j - 2) as nat) + fib((j - 1) as nat)); | ||
| lemma_fib_is_monotonic(i, (j - 1) as nat); | ||
| } else { | ||
| lemma_fib_is_monotonic(i, (j - 1) as nat); | ||
| lemma_fib_is_monotonic(i, (j - 2) as nat); | ||
| } |
There was a problem hiding this comment.
There's a simpler proof for this, that we found during the tutorial proof debugging session:
| if i < 2 && j < 2 { | |
| } else if i == j { | |
| } else if i == j - 1 { | |
| assert(fib(j) == fib((j - 2) as nat) + fib((j - 1) as nat)); | |
| lemma_fib_is_monotonic(i, (j - 1) as nat); | |
| } else { | |
| lemma_fib_is_monotonic(i, (j - 1) as nat); | |
| lemma_fib_is_monotonic(i, (j - 2) as nat); | |
| } | |
| if i < 2 && j < 2 { | |
| } else if i == j { | |
| } else if i == j - 1 { | |
| reveal_with_fuel(fibo_spec, 2); | |
| } else { | |
| reveal_with_fuel(fibo_spec, 2); | |
| lemma_fib_is_monotonic(i, (j - 1) as nat); | |
| } |
| exec fn fib_impl(n: u64) -> (result: u64) | ||
| requires | ||
| fib_fits_u64(n as nat), | ||
| ensures | ||
| result == fib(n as nat), |
There was a problem hiding this comment.
This version of the fibonacci demo is a bit more compact, but sort-of unrealistic, due to the fact that the caller needs to prove that the result will fit in a u64. I have a more realistic version that returns an Option that's None if the result doesn't fit: what do you think, shall I replace it on this branch?
No description provided.