More general mint cheat code (#884)

* may or may not be initialized (was always uninitialized before)
* may or may not have an authorisation key (Option)
* may or may not have a freeze authorisation key (Option)

The options are now modeled by a variable in the `variantIdx` field. The
payload data for `None` would be `.List` but the payload data (`Pubkey`)
is set nevertheless, assuming that it will never be read if the variant
index is `0` for `None`.

Author: jberthold

kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md

@@ -418,16 +418,14 @@ module KMIR-SPL-TOKEN
                     ),
                     SPLDataBuffer(
                       Aggregate(variantIdx(0),
-                        // Model COption<Pubkey> as
-                        // Some(pubkey); None is not represented here.
-                        ListItem(Aggregate(variantIdx(1),
+                        // optional key. The model always carries a payload key (never to be read if None)
+                        ListItem(Aggregate(variantIdx(?SplMintHasAuthKey),
                           ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintAuthorityKey:List))))))
                         ListItem(Integer(?SplMintSupply:Int, 64, false))
                         ListItem(Integer(?SplMintDecimals:Int, 8, false))
-                        ListItem(BoolVal(false))
-                        // Model COption<Pubkey> as
-                        // Some(pubkey); None is not represented here.
-                        ListItem(Aggregate(variantIdx(1),
+                        ListItem(BoolVal(?_SplMintInitialised))
+                        // optional key. The model always carries a payload key (never to be read if None)
+                        ListItem(Aggregate(variantIdx(?SplMintHasFreezeKey),
                           ListItem(Aggregate(variantIdx(0), ListItem(Range(?SplMintFreezeAuthorityKey:List))))))
                       )
                     )
@@ -447,7 +445,9 @@ module KMIR-SPL-TOKEN
       orBool #functionName(lookupFunction(#tyOfCall(FUNC))) ==String "cheatcode_is_spl_mint"
     ensures #isSplPubkey(?SplMintAccountKey)
       andBool #isSplPubkey(?SplMintOwnerKey)
+      andBool 0 <=Int ?SplMintHasAuthKey andBool ?SplMintHasAuthKey <=Int 1
       andBool #isSplPubkey(?SplMintAuthorityKey)
+      andBool 0 <=Int ?SplMintHasFreezeKey andBool ?SplMintHasFreezeKey <=Int 1
       andBool #isSplPubkey(?SplMintFreezeAuthorityKey)
       andBool 0 <=Int ?SplMintLamports andBool ?SplMintLamports <Int 18446744073709551616
       andBool 0 <=Int ?SplMintRentEpoch andBool ?SplMintRentEpoch <Int 18446744073709551616