Tweaking rlimits for new F*

[mtzguido]

Hi, I needed to bump some rlimits to get an everest green for a change that's coming to F* (FStarLang/FStar@fc1b447, FStarLang/FStar#2894, FStarLang/FStar#2915).

The F* change should be rather innocuous as far as SMT changes go, but some proofs here seem to be close to their rlimit. If these changes don't look too crazy I'd like to merge them so I can merge the F* PR.

[msprotz]

These changes all look good. Two questions:

• what is assert_spinoff, and why is it helping better than a regular assert? is this a general pattern, should other pieces of Low* code start using assert_spinoff?
• why is it that a proof needs fuel 4 and ifuel 4? did something regress?
  thanks!

[mtzguido]

Thanks for reviewing!

• assert_spinoff p is similar to assert, except that the obligation to prove p is done in a separate Z3 query from the "main" one, which can help with stability (e.g. each query has their own rlimit). I am not sure it's actually needed here, I just tend to use it when proofs get hairy. I could try without it, but it also doesn't hurt IMO.
• I am actually decreasing the fuel, most of the file is under this:

#push-options "--z3rlimit 32 --max_fuel 8 --max_ifuel 8 --initial_fuel 8 --initial_ifuel 8"        

[msprotz]

I am actually decreasing the fuel, most of the file is under this:

😱

assert_spinoff p is similar to assert

thanks for clarifying... this might come in handy in some of the trickier proofs in HACL*

all looks good to me, merging