As part of the Marlowe audit, a discrepancy was found regarding the MoneyPreservation.thy theory. We state in plain English that when we compute a transaction the money is preserved. This means that no assets are created or destroyed during a transaction. The problem is that the theorems inside MoneyPreservation.thyonly refers about the quantity of tokens and don't guarantee that the same token is preserved. This means that the proofs don't guarantee us that if we deposit 15 ada and 20 djed we won't get 15 djed and 20 ada back.
To address this I created the AssetsPreservation.thy theory, which introduces a new typedef Assets that represents Multi-token assets. I've added multiple class instances to allow arithmetic on the new type and completed proving that reduceContractStep preserves assets.
Before going further and proving that computeTransaction and playTrace preserves assets (with all the intermediate functions), I wanted to take a small sanity check to see that the proofs are going in the right direction.
Most of my concerns are expressed as TODO: comments in the code, but I explain the most important one here:
Account representation
The Semantics.thy theory, which is the subject of the proofs, works with accounts represented as an associative list
and it uses the functions insert, delete and lookup defined in the MList.thy theory. This is well suited for an executable definition, as Plutus also works with associative lists, but is harder to reason about.
In the second section of AssetsPreservation.thy I defined another type synonym for Accounts as a Map.
type_synonym Accounts = "AccountId ⇀ Assets"
My main issue here is that in order to prove stuff for the executable definition I still need to make lemmas around the associative list representation, which are harder to do (look for example at assetsInAccounts_distrib_on_update). I tried to map the list version to Map version in lemmas like moneyInAccountFromSemantic, but for the moment I wasn't able to prove them. Another thing I did to aleviate this problem was to add a MList_induct lemma in MList, to be able to do induction in lists the same way I do it for Maps.
Another issue that I have is that I need to propagate assumptions like valid_map acc and allAccountsPositive acc when I'm using the List representation, and finite (dom acc) when I'm using the Map representation. I though of creating a typedef with the finite restriction, but I'm wondering if that won't involve in also having to re-define/transfer a lot of the Map lemmas. The question here would be, what is the rule of thumb for using a type_synonym vs typedef, and is there any way to easily expose the underlying lemmas of Map if I use a typedef?
A side note on the List representation using an int and the allAccountsPositive restriction: I found it a little bit harder to work with nat rather than int as they form a semiring instead of a ring, so in order to simplify something like a + (b - a) = b I first need to prove than a ≤ b (a and b being Multi-token Assets).
A final note on this section, the audit also pointed out that MList implementation differs from the Plutus AssocMap implementation. For example:
We could easily change MList to behave the same as AssocMap, but that is not ideal as the Marlowe specification should be blockchain agnostic. I wonder what is the best solution for this problem. My intuition tells me that if I define a typedef around Isabelle Map with the finite restriction, I should probably use that in the Semantics.thy code as well, then investigate on how to use code equations to use a particular implementation (like MList). If we do this, we should also add some property based tests in the marlowe-spec-test tool to check properties likeinsert k v1 (insert k v2 m) = insert k v1 m, but don't rely on the order of entries.
hrajchert
commented
1 year ago
As part of the Marlowe audit, a discrepancy was found regarding the
MoneyPreservation.thytheory. We state in plain English that when we compute a transaction the money is preserved. This means that no assets are created or destroyed during a transaction. The problem is that the theorems insideMoneyPreservation.thyonly refers about the quantity of tokens and don't guarantee that the same token is preserved. This means that the proofs don't guarantee us that if we deposit15 adaand20 djedwe won't get15 djedand20 adaback.To address this I created the
AssetsPreservation.thytheory, which introduces a newtypedef Assetsthat represents Multi-token assets. I've added multiple class instances to allow arithmetic on the new type and completed proving thatreduceContractSteppreserves assets.Before going further and proving that
computeTransactionandplayTracepreserves assets (with all the intermediate functions), I wanted to take a small sanity check to see that the proofs are going in the right direction.Most of my concerns are expressed as
TODO:comments in the code, but I explain the most important one here:Account representation
The
Semantics.thytheory, which is the subject of the proofs, works with accounts represented as an associative listand it uses the functions
insert,deleteandlookupdefined in theMList.thytheory. This is well suited for an executable definition, as Plutus also works with associative lists, but is harder to reason about.In the second section of
AssetsPreservation.thyI defined another type synonym for Accounts as a Map.My main issue here is that in order to prove stuff for the executable definition I still need to make lemmas around the associative list representation, which are harder to do (look for example at
assetsInAccounts_distrib_on_update). I tried to map the list version to Map version in lemmas likemoneyInAccountFromSemantic, but for the moment I wasn't able to prove them. Another thing I did to aleviate this problem was to add aMList_inductlemma in MList, to be able to do induction in lists the same way I do it for Maps.Another issue that I have is that I need to propagate assumptions like
valid_map accandallAccountsPositive accwhen I'm using the List representation, andfinite (dom acc)when I'm using the Map representation. I though of creating atypedefwith thefiniterestriction, but I'm wondering if that won't involve in also having to re-define/transfer a lot of the Map lemmas. The question here would be, what is the rule of thumb for using atype_synonymvstypedef, and is there any way to easily expose the underlying lemmas of Map if I use atypedef?A side note on the List representation using an
intand theallAccountsPositiverestriction: I found it a little bit harder to work withnatrather thanintas they form a semiring instead of a ring, so in order to simplify something likea + (b - a) = bI first need to prove thana ≤ b(aandbbeing Multi-token Assets).A final note on this section, the audit also pointed out that
MListimplementation differs from the PlutusAssocMapimplementation. For example:We could easily change
MListto behave the same asAssocMap, but that is not ideal as the Marlowe specification should be blockchain agnostic. I wonder what is the best solution for this problem. My intuition tells me that if I define atypedefaround IsabelleMapwith thefiniterestriction, I should probably use that in theSemantics.thycode as well, then investigate on how to use code equations to use a particular implementation (like MList). If we do this, we should also add some property based tests in the marlowe-spec-test tool to check properties likeinsert k v1 (insert k v2 m) = insert k v1 m, but don't rely on the order of entries.