PLT-5370 - Merkleization formalization #171
Conversation
| fun evalSize :: "State \<Rightarrow> MContract \<Rightarrow> nat" where | ||
| "evalSize sta cont = length (accounts sta) + 2 * (size cont)" | ||
|
|
||
| lemma reduceMContractStepReducesSize : | ||
| "reduceMContractStep env sta c = Reduced twa tef nsta nc \<Longrightarrow> | ||
| (evalSize nsta nc) < (evalSize sta c)" | ||
| sorry |
There was a problem hiding this comment.
This was copy pasted and adapted from the evalBound in the Semantic module. This should later be modified to use the mcontract_size function, currently defined in the Unmerkleize module
There was a problem hiding this comment.
We shouldn't have any sorrys in main, we should change it to oops and comment out code that depends on it. I guess CI is passing because this is not added to CI yet, otherwise it shouldn't pass
There was a problem hiding this comment.
I left this as sorry on purpose because it is a draft PR, not intended to be merged on main, rather to start the discussion on the direction we should take to formalize merkleization. The most important thing to assess in this PR is which approach of the ones stated in the Readme should be used (or maybe one that I didn't thought of)
There was a problem hiding this comment.
On another note, I think the CI tests are only firing when we make a change in a haskell file, we should check this with the help of @shlevy
| | NotReduced | ||
| | AmbiguousTimeIntervalReductionError | ||
|
|
||
| fun reduceMContractStep :: "Environment \<Rightarrow> State \<Rightarrow> MContract \<Rightarrow> ReduceStepMResult" where |
There was a problem hiding this comment.
To improve readability in the future I might rename the functions and type to be the same as the Semantic module, and whenever we need to disambiguate we use the qualified name
hrajchert
force-pushed
the
hrajchert/linorder-simplification
branch
from
ee8c6a7 to
4f4d5f5
Compare
isabelle/Core/PositiveAccounts.thy
Outdated
| theorem accountsArePositive : | ||
| "valid_state state \<Longrightarrow> (\<forall>x tok. positiveMoneyInAccountOrNoAccount x tok (accounts state)) \<Longrightarrow> | ||
| computeTransaction txIn state cont = TransactionOutput txOut \<Longrightarrow> | ||
| positiveMoneyInAccountOrNoAccount y tok2 (accounts (txOutState txOut))" | ||
| using computeTransaction_gtZero by blast |
There was a problem hiding this comment.
A couple of notes... Sadly, this change does not belong to the merkleization PR. I had the following dependency
Merkleization PR --depends--> Simplification of some linorder instances --depends--> PLT-3505 small fixes to the isabelle specification --depends--> PLT-4195 - Asset preservation theory
This change actually belongs to PLT-3505 small fixes to the isabelle specification. When I merged the Asset preservation theory I rebased the small fixes and the linorder PR but I forgot to update this one 🤦🏻 .
Regarding the change itself, it was due to this audit observation
The theorem is a duplicate of computeTransaction_gtZero (and actually is "automatically" solved using that)
isabelle/Core/QuiescentResult.thy
Outdated
| @@ -2,9 +2,6 @@ theory QuiescentResult | |||
| imports Semantics PositiveAccounts | |||
| begin | |||
|
|
|||
| lemma reduceOne_onlyIfNonEmptyState : "refundOne acc = Some c \<Longrightarrow> acc \<noteq> []" | |||
| by auto | |||
There was a problem hiding this comment.
Also, this is a good theorem to have, not sure why remove it
There was a problem hiding this comment.
The lemma wasn't actually being used and it is trivially solved, so probably any lemma that needs to know that the account isn't empty can use the simplifier directly
| fun evalSize :: "State \<Rightarrow> MContract \<Rightarrow> nat" where | ||
| "evalSize sta cont = length (accounts sta) + 2 * (size cont)" | ||
|
|
||
| lemma reduceMContractStepReducesSize : | ||
| "reduceMContractStep env sta c = Reduced twa tef nsta nc \<Longrightarrow> | ||
| (evalSize nsta nc) < (evalSize sta c)" | ||
| sorry |
There was a problem hiding this comment.
We shouldn't have any sorrys in main, we should change it to oops and comment out code that depends on it. I guess CI is passing because this is not added to CI yet, otherwise it shouldn't pass
hrajchert
force-pushed
the
hrajchert/linorder-simplification
branch
from
4f4d5f5 to
22e262d
Compare
hrajchert
force-pushed
the
hrajchert/merkleization
branch
from
bf97569 to
7290d26
Compare
hrajchert
force-pushed
the
hrajchert/merkleization
branch
from
7290d26 to
d1c19fa
Compare
palas
changed the title
hrajchert
force-pushed
the
hrajchert/merkleization
branch
from
e6a8b7a to
d1c19fa
Compare
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: