search

tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

Find a more idiomatic way of handling Plutus `Value` #13

Closed VictorCMiraldo closed 2 years ago

VictorCMiraldo commented 3 years ago

Cardano EUTxO contracts manipulate Value transfers between addresses.

newtype Value = Value { getValue :: Map.Map CurrencySymbol (Map.Map TokenName Integer) }

This datatype gets translated to [(ByteString, [(ByteString, Integer)])], which is a little too permissive for most of our TLA+ models. I can imagine that many contracts will not require this degree of generality, in fact, I think we could be better off translating it to [PlutusToken -> Integer] where PlutusToken is a set of model values.

VictorCMiraldo commented 2 years ago

We are likely not coming back to TLA+, this issue is out of scope.