[libra framework][move-prover] Abstraction of auth key construction in LibraAccount
[libra framework][move-prover] Abstraction of auth key construction in LibraAccount

This pulls auth key construction from make_account into its own private function, which can then be abstracted for verification. This avoids the use of vector concatenation of `LCS:to_bytes(x)` results in verification conditions, which appear to be a source of butterflies.

This doesn't enable new verifications (everything in LibraAccount was verified already before), but hardens for future critical changes to avoid timeouts.

aptos-labs/aptos-core,aptos-labs/aptos-core,libra/libra,aptos-labs/aptos-core,aptos-labs/aptos-core,aptos-labs/aptos-core,libra/libra,aptos-labs/aptos-core,libra/libra,aptos-labs/aptos-core,libra/libra,libra/libra