As part of the Marlowe audit, the following concern was found
This DRAFT PR is an attempt to formalize merkleized contracts.
Two approaches were considered for this task: modify the contract type in the Core session to include the merkleized case, or create a new Merkle session that reuses everything it can from the Core session and prove that both versions are equivalent. We chose the latter approach for the following reasons.
Modifying the Core session would invalidate all current theories, while adding a new Merkle session does not invalidate anything but adds some duplication. For example, the Merkleized and Unmerkleized versions of reduceContractStep are the same, but we need to have both versions since the types are different.
If we modify the Core session, we would have the Merkleized and Unmerkleized versions under the same type, which can make the lemmas for equivalence harder to express. We would probably need to add an isMerkleized proposition and include it as an assumption in the lemmas, while having separate versions, the proposition is implied by the type.
If we decide to keep this approach, the following tasks need to be accomplished:
For all the functions in the MerkleInterpreter theory, we need to prove that if we can unmerkleize the contract then the payments, state, and warnings obtained from the unmerkleized function are equivalent to their merkleized counterpart.
Provide a merkleize algorithm (given a hash function with some assumptions).
Prove that merkleizing and unmerkleizing a contract yields back the original contract.
As part of the Marlowe audit, the following concern was found
This DRAFT PR is an attempt to formalize merkleized contracts.
Two approaches were considered for this task: modify the contract type in the
Core sessionto include the merkleized case, or create a newMerkle sessionthat reuses everything it can from theCore sessionand prove that both versions are equivalent. We chose the latter approach for the following reasons.Modifying the
Core sessionwould invalidate all current theories, while adding a newMerkle sessiondoes not invalidate anything but adds some duplication. For example, the Merkleized and Unmerkleized versions of reduceContractStep are the same, but we need to have both versions since the types are different.If we modify the Core session, we would have the Merkleized and Unmerkleized versions under the same type, which can make the lemmas for equivalence harder to express. We would probably need to add an
isMerkleizedproposition and include it as an assumption in the lemmas, while having separate versions, the proposition is implied by the type.If we decide to keep this approach, the following tasks need to be accomplished: