Support multiple return values in SST

[Chris-Hawblitzel]

This allows multiple return values for SST proof/exec functions and StmX::Call statements, similar to multiple return values in Boogie. I used this to implement the upcoming verifier::shadow_data feature. It might also be useful for #1301 and #2436 . For #2436 , for example, we could keep the StmX::Call destinations aligned with the ens_args extra return-value arguments, rather than having to match a tuple destination in StmX::Call to non-tuple ens_args extra return-value arguments.

It remains to be seen what we do with call_requires/call_ensures when there are implicit extra ghost/tracked arguments and return values not present in the original Rust types as seen by the Rust type checker. In some places, we could use existential quantification over the extra arguments and return values. More generally, we might have something like call_requires_with/call_ensures_with to talk about the extra values. For now, though, I just assert that the call_requires/call_ensures axioms are removed whenever extra arguments and return values are added that aren't part of the original Rust types.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.