[move-prover] Specified Offer.move.
[move-prover] Specified Offer.move.

Wrote functional specifications for all four functions and
two global specifications to restrict creation and removal of
Offer.T resources to the create and remove functions.

Additional notes: In an earlier implementation, I was able to write
a more general property that states that only the sender or the intended
recipient (i.e. Offer<T<Offered>>.for) of an Offer could receive the
offered struct (refer to the properties below). This would allow
for additional functions that change the Offer to be implemented without
changing the specification (e.g. if an update offer function is
implemented).

```
/// **Informally:** If the Offer is removed from an address, then the sender
///                 must be the intended recipient
ensures all(domain<address>(), |addr|
  (old(exists<T<Offered>>(addr)) && !exists<T<Offered>>(addr)) ==>
  (old(sender_is_offer_recipient<Offered>(addr))));
/// **Informally:** An offer under an account is unchanged if it is not the sender's
///                 account or if the sender is not the recipient
ensures all(domain<address>(), |addr|
  (old(exists<T<Offered>>(addr)) && old(!sender_is_offer_recipient<Offered>(addr))) ==>
  (exists<T<Offered>>(addr) && old(global<T<Offered>>(addr)) == global<T<Offered>>(addr)));
/// **Informally:** An offer under an account is unchanged if the intended
///                 recipient does not redeem it
ensures all(domain<address>(), |addr|
  (old(exists<T<Offered>>(addr)) && exists<T<Offered>>(addr)) ==>
  (old(global<T<Offered>>(addr)) == global<T<Offered>>(addr)));
```

However, with the introduction of signers the property is false
without the precondition / assumption that the signer is the sender,

Closes: #4315
Approved by: DavidLDill

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