As part of the Marlowe audit, the following problem was found
Basically, the proof didn't guarantee us that if we deposit 15 ada and 20 djed we won't get 15 djed and 20 ada back, only that we'd get 35 tokens.
The new theory AssetsPreservation solves this by working with a new MultiAsset data type, defined in MultiAssets.thy. The new type defines some type classes for working with MultiAssets as if they were natural numbers.
The lemmas were restructured, removing the need of auxiliary functions to solve the following issues
The function moneyInPayment was renamed to assetsInExternalPayment as suggested by the auditors, to mark that we are talking about money transferred from the contract to an external party and not from internal account to internal account.
I've attached a version of the specification-v3.pdf with a modified section 3.1 and 3.2
As part of the Marlowe audit, the following problem was found
Basically, the proof didn't guarantee us that if we deposit
15 adaand20 djedwe won't get15 djedand20 adaback, only that we'd get 35 tokens.The new theory AssetsPreservation solves this by working with a new MultiAsset data type, defined in
MultiAssets.thy. The new type defines some type classes for working with MultiAssets as if they were natural numbers.The lemmas were restructured, removing the need of auxiliary functions to solve the following issues
The function
moneyInPaymentwas renamed toassetsInExternalPaymentas suggested by the auditors, to mark that we are talking about money transferred from the contract to an external party and not from internal account to internal account.I've attached a version of the specification-v3.pdf with a modified section 3.1 and 3.2