Remaining Mary features/proofs

- Token Algebras
+ Function `scaledMinDeposit` (Figure 6) (together with replacing precondition on UTxO rule)
+ Function `serialize : TA -> Bytestring` ("The specific underlying TA is required to be serializable in
every era")
+ Function `anameLen : AssetName -> MemoryEstimate` (Figure 13)
+ Function `serSize` (Figure 13)
+ Function `numAssets : TA -> Nat` (Figure 13)
+ Function `sumALs` (derived from `anameLen`, figure 13)
+ Function `numPids` (Figure 13)
+ Function `size : TA -> MemoryEstimate` (instead of being taken as a primitive, figure 14)