Add large example at the end of the manual

[atomb]

The current version of the manual ends rather abruptly, and doesn't show examples of some of the more advanced features. It would be nice to conclude it with a large-ish example of compositional verification of some Java or C program to tie all of the previous sections together.

[ChrisEPhifer]

@atomb Do you have any ideas on what you might like this larger example to be? I'd be happy to both work on the verification task & document my process to supplement the manual, but I can't say I have any super good ideas on what that verification task should actually be :)

[atomb]

I don't have any really good ideas. To take an example that already exists, it could be reasonable to use examples/salsa20. It's a case where, if you want to prove it for just one size, doing things monolithically is faster (at least last time I tried; this sort of thing changes all the time) but if you want to prove multiple sizes then proving all the fixed-size functions first and then just iterating over the top-level function for multiple sizes is faster. So it's a sort of interesting demonstration of where it can be useful (but it's not an example of the case where monolithic verification is infeasible, even though such examples exist).