Document provers

[Aurel300]

No description provided.

[Aurel300]

@marcoeilers Maybe the tutorial should have a section on configuration in general? I think there should be a section to list all the configuration flags (even though we would have to keep that in sync with the Scala definitions), which would also be a good place to discuss the options at greater length? E.g.: what sorts of timeouts/resources you can use for the backends, how you can enable portfolio mode, counterexamples (still not documented I just noticed)...

[marcoeilers]

Yes, I agree with the configuration section.

But the explanation for the @prover annotation (from the PR that isn't merged yet) is not correct; that annotation is not equivalent to --prover. If, via --prover, you've selected a portfolio of multiple provers, then the @prover annotation on a member allows you to select a subset of those provers to select this member. Silicon starts prover instances once at the beginning, so it's not so easy to start up new ones when verifying a specific member, that's the reason. Maybe this is a sign that I should rename the @prover annotation then though, it really does suggest that it's equivalent to the command line option.