From 7290d2692e74097f4ae128dce750aec5e5902dc4 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Mon, 20 Mar 2023 17:35:16 -0300 Subject: [PATCH] Initial version of merkleization theory --- isabelle/Merkle/MerkleInterpreter.thy | 255 ++++++++++++++++++++++++++ isabelle/Merkle/MerkleTypes.thy | 20 ++ isabelle/Merkle/Unmerkleize.thy | 147 +++++++++++++++ isabelle/ROOT | 11 ++ 4 files changed, 433 insertions(+) create mode 100644 isabelle/Merkle/MerkleInterpreter.thy create mode 100644 isabelle/Merkle/MerkleTypes.thy create mode 100644 isabelle/Merkle/Unmerkleize.thy diff --git a/isabelle/Merkle/MerkleInterpreter.thy b/isabelle/Merkle/MerkleInterpreter.thy new file mode 100644 index 00000000..3a4af580 --- /dev/null +++ b/isabelle/Merkle/MerkleInterpreter.thy @@ -0,0 +1,255 @@ +theory MerkleInterpreter + +imports MerkleTypes Core.Semantics +begin + +section "Interpreter" + +fun getAction :: "MCase \ Action" where + "getAction (Case action _) = action" +| "getAction (MerkleizedCase action _) = action" + +fun getInputContent :: "MInput \ Input" where + "getInputContent (NormalInput i) = i" +| "getInputContent (MerkleizedInput i _ _) = i" + +fun getContinuation :: "MInput \ MCase \ MContract option" where + "getContinuation (NormalInput _) (Case _ continuation) = Some continuation" +| "getContinuation (MerkleizedInput _ inputContinuationHash continuation) (MerkleizedCase _ continuationHash) + = (if inputContinuationHash = continuationHash + then Some continuation + else None + )" +| "getContinuation _ _ = None" + +subsection "Reduce contract Step" + +\ \The only difference with ReduceStepResult is the MContract instead of Contract\ +datatype ReduceStepMResult = Reduced ReduceWarning ReduceEffect State MContract + | NotReduced + | AmbiguousTimeIntervalReductionError + +fun reduceMContractStep :: "Environment \ State \ MContract \ ReduceStepMResult" where +"reduceMContractStep _ state Close = + (case refundOne (accounts state) of + Some ((party, token, money), newAccount) \ + let newState = state \ accounts := newAccount \ in + Reduced ReduceNoWarning (ReduceWithPayment (Payment party (Party party) token money)) newState Close + | None \ NotReduced)" | +"reduceMContractStep env state (Pay accId payee token val cont) = + (let amountToPay = evalValue env state val in + if amountToPay \ 0 + then (let warning = ReduceNonPositivePay accId payee token amountToPay in + Reduced warning ReduceNoPayment state cont) + else (let balance = moneyInAccount accId token (accounts state); + paidAmount = min balance amountToPay; + newBalance = balance - paidAmount; + newAccs = updateMoneyInAccount accId token newBalance (accounts state); + warning = (if paidAmount < amountToPay + then ReducePartialPay accId payee token paidAmount amountToPay + else ReduceNoWarning) ; + (payment, finalAccs) = giveMoney accId payee token paidAmount newAccs + in + Reduced warning payment (state \ accounts := finalAccs \) cont))" | +"reduceMContractStep env state (If obs cont1 cont2) = + (let cont = (if evalObservation env state obs + then cont1 + else cont2) in + Reduced ReduceNoWarning ReduceNoPayment state cont)" | +"reduceMContractStep env state (When _ timeout cont) = + (let (startTime, endTime) = timeInterval env in + \ \if timeout in future – do not reduce\ + if endTime < timeout then NotReduced + \ \if timeout in the past – reduce to timeout continuation\ + else if timeout \ startTime then Reduced ReduceNoWarning ReduceNoPayment state cont + \ \ if timeout in the time range – issue an ambiguity error\ + else AmbiguousTimeIntervalReductionError)" | +"reduceMContractStep env state (Let valId val cont) = + (let evaluatedValue = evalValue env state val; + boundVals = boundValues state; + newState = state \ boundValues := MList.insert valId evaluatedValue boundVals \; + warn = case lookup valId boundVals of + Some oldVal \ ReduceShadowing valId oldVal evaluatedValue + | None \ ReduceNoWarning + in Reduced warn ReduceNoPayment newState cont)" | +"reduceMContractStep env state (Assert obs cont) = + (let warning = if evalObservation env state obs + then ReduceNoWarning + else ReduceAssertionFailed + in Reduced warning ReduceNoPayment state cont)" + +subsection "Evaluation size" + +text \This function gives the notion of size for an evaluation. It is used to show that reductionMLoop +terminates.\ +fun evalSize :: "State \ MContract \ nat" where +"evalSize sta cont = length (accounts sta) + 2 * (size cont)" + +lemma reduceMContractStepReducesSize : + "reduceMContractStep env sta c = Reduced twa tef nsta nc \ + (evalSize nsta nc) < (evalSize sta c)" + sorry + + +subsection "Reduce contract until quiescent" + + +\ \The only difference with ReduceResult is the MContract instead of Contract\ + +datatype ReduceMResult + = ContractQuiescent bool "ReduceWarning list" "Payment list" State MContract + | RRAmbiguousTimeIntervalError + + +function (sequential) reductionMLoop :: "bool \ Environment \ State \ MContract \ ReduceWarning list \ + Payment list \ ReduceMResult" where +"reductionMLoop reduced env state contract warnings payments = + (case reduceMContractStep env state contract of + Reduced warning effect newState ncontract \ + let newWarnings = (if warning = ReduceNoWarning + then warnings + else warning # warnings) in + let newPayments = (case effect of + ReduceWithPayment payment \ payment # payments + | ReduceNoPayment \ payments) in + reductionMLoop True env newState ncontract newWarnings newPayments + | AmbiguousTimeIntervalReductionError \ RRAmbiguousTimeIntervalError + | NotReduced \ ContractQuiescent reduced (rev warnings) (rev payments) state contract)" + by pat_completeness auto +termination reductionMLoop + apply (relation "measure (\(_, (_, (state, (contract, _)))) . evalSize state contract)") + using reduceMContractStepReducesSize by auto + + +fun reduceMContractUntilQuiescent :: "Environment \ State \ MContract \ ReduceMResult" where +"reduceMContractUntilQuiescent env state contract = reductionMLoop False env state contract [] []" + +subsection "Apply input" + +datatype ApplyAction = AppliedAction ApplyWarning State + | NotAppliedAction + +datatype ApplyMResult = Applied ApplyWarning State MContract + | ApplyNoMatchError + +fun applyAction :: "Environment \ State \ Input \ Action \ ApplyAction" where + "applyAction env state (IDeposit accId1 party1 tok1 amount) (Deposit accId2 party2 tok2 val) = + (if accId1 = accId2 & party1 = party2 & tok1 = tok2 & amount = evalValue env state val + then let warning = if amount > 0 then ApplyNoWarning + else ApplyNonPositiveDeposit party2 accId2 tok2 amount; + newAccounts = addMoneyToAccount accId1 tok1 amount (accounts state); + newState = state \ accounts := newAccounts\ + in AppliedAction warning newState + else NotAppliedAction + )" +|"applyAction _ state (IChoice choId1 choice) (Choice choId2 bounds) = + (if choId1 = choId2 & inBounds choice bounds + then let newState = state \ choices := MList.insert choId1 choice (choices state) \ + in AppliedAction ApplyNoWarning newState + else NotAppliedAction + )" +|"applyAction env state INotify (Notify obs) = + (if evalObservation env state obs + then AppliedAction ApplyNoWarning state + else NotAppliedAction + )" +|"applyAction _ _ (IChoice _ _) (Deposit _ _ _ _) = NotAppliedAction" +|"applyAction _ _ (IChoice _ _) (Notify _) = NotAppliedAction" +|"applyAction _ _ INotify (Deposit _ _ _ _) = NotAppliedAction" +|"applyAction _ _ INotify (Choice _ _) = NotAppliedAction" +|"applyAction _ _ (IDeposit _ _ _ _) (Choice _ _) = NotAppliedAction" +|"applyAction _ _ (IDeposit _ _ _ _) (Notify _) = NotAppliedAction" + + +fun applyMCases :: "Environment \ State \ MInput \ MCase list \ ApplyMResult" where +"applyMCases _ _ _ [] = ApplyNoMatchError" | +"applyMCases env state input (headCase # tailCases) = ( + let inputContent = getInputContent input; + action = getAction headCase; + maybeContinuation = getContinuation input headCase + in (case applyAction env state inputContent action of + AppliedAction warning newState \ ApplyNoMatchError + | NotAppliedAction \ applyMCases env state input tailCases) + ) +" + +fun applyMInput :: "Environment \ State \ MInput \ MContract \ ApplyMResult" where +"applyMInput env state input (When cases _ _) = applyMCases env state input cases" | +"applyMInput env state input c = ApplyNoMatchError" + + +subsection "Apply all inputs" + +datatype ApplyAllMResult = + ApplyAllSuccess bool "TransactionWarning list" "Payment list" State MContract +| ApplyAllNoMatchError +| ApplyAllAmbiguousTimeIntervalError +| ApplyAllHashMismatch + + +fun applyAllMLoop :: "bool \ Environment \ State \ MContract \ MInput list \ + TransactionWarning list \ Payment list \ + ApplyAllMResult" where +"applyAllMLoop contractChanged env state contract inpts warnings payments = + (case reduceMContractUntilQuiescent env state contract of + RRAmbiguousTimeIntervalError \ ApplyAllAmbiguousTimeIntervalError + | ContractQuiescent reduced reduceWarns pays curState cont \ + (case inpts of + Nil \ ApplyAllSuccess (contractChanged \ reduced) (warnings @ (convertReduceWarnings reduceWarns)) + (payments @ pays) curState cont + | Cons input rest \ + (case applyMInput env curState input cont of + Applied applyWarn newState appliedCont \ + applyAllMLoop True env newState appliedCont rest + (warnings @ (convertReduceWarnings reduceWarns) + @ (convertApplyWarning applyWarn)) + (payments @ pays) + | ApplyNoMatchError \ ApplyAllNoMatchError)))" + + +fun applyAllMInputs :: "Environment \ State \ MContract \ MInput list \ + ApplyAllMResult" where +"applyAllMInputs env state contract inps = applyAllMLoop False env state contract inps Nil Nil" + +subsection "Compute transaction" + + +record MTransaction = interval :: TimeInterval + inputs :: "MInput list" + + +datatype TransactionError = TEAmbiguousTimeIntervalError + | TEApplyNoMatchError + | TEIntervalError IntervalError + | TEUselessTransaction + | TEHashMismatch + +record TransactionOutputRecord = txOutWarnings :: "TransactionWarning list" + txOutPayments :: "Payment list" + txOutState :: State + txOutContract :: MContract + + +datatype TransactionOutput + = TransactionOutput TransactionOutputRecord + | TransactionError TransactionError + +fun computeMTransaction :: "MTransaction \ State \ MContract \ TransactionOutput" where +"computeMTransaction tx state contract = + (let inps = inputs tx in + case fixInterval (interval tx) state of + IntervalTrimmed env fixSta \ + (case applyAllMInputs env fixSta contract inps of + ApplyAllSuccess reduced warnings payments newState cont \ + if ((\ reduced) \ ((contract \ Close) \ (accounts state = []))) + then TransactionError TEUselessTransaction + else TransactionOutput \ txOutWarnings = warnings + , txOutPayments = payments + , txOutState = newState + , txOutContract = cont \ + | ApplyAllNoMatchError \ TransactionError TEApplyNoMatchError + | ApplyAllAmbiguousTimeIntervalError \ TransactionError TEAmbiguousTimeIntervalError + | ApplyAllHashMismatch => TransactionError TEHashMismatch + ) + | IntervalError error \ TransactionError (TEIntervalError error))" +end \ No newline at end of file diff --git a/isabelle/Merkle/MerkleTypes.thy b/isabelle/Merkle/MerkleTypes.thy new file mode 100644 index 00000000..f6138a5e --- /dev/null +++ b/isabelle/Merkle/MerkleTypes.thy @@ -0,0 +1,20 @@ +theory MerkleTypes + +imports Core.SemanticsTypes +begin + +section "Types" + +datatype MCase = Case Action MContract + | MerkleizedCase Action ByteString +and MContract = Close + | Pay AccountId Payee Token Value MContract + | If Observation MContract MContract + | When "MCase list" Timeout MContract + | Let ValueId Value MContract + | Assert Observation MContract + +datatype MInput = NormalInput Input + | MerkleizedInput Input ByteString MContract + +end \ No newline at end of file diff --git a/isabelle/Merkle/Unmerkleize.thy b/isabelle/Merkle/Unmerkleize.thy new file mode 100644 index 00000000..b60aa3c3 --- /dev/null +++ b/isabelle/Merkle/Unmerkleize.thy @@ -0,0 +1,147 @@ +theory Unmerkleize + imports MerkleTypes "HOL-Library.Finite_Map" "HOL-Library.Monad_Syntax" +begin + +section "MerkleMap" +text \The Unmerkleize theory is responsible for reversing the process of contract merkleization. +Its implementation involves looking up each sub-contract's continuation from a Merkle map. \ + +type_synonym MerkleMap = "(ByteString, MContract) fmap" + +subsection "Size" + +text "The following functions provide the notion of size to a Merkleized Contract, Case and MerkleMap. +They are used to prove the termination of the unmerkleize function " +fun mcontract_size :: "MContract \ nat" +and mcase_size :: "MCase \ nat" +where + "mcontract_size Close = 1" +|"mcontract_size (Pay _ _ _ _ cont) = 1 + mcontract_size cont" +|"mcontract_size (Let _ _ cont) = 1 + mcontract_size cont" +|"mcontract_size (Assert _ cont) = 1 + mcontract_size cont" +|"mcontract_size (If _ trueCont falseCont) = 1 + mcontract_size trueCont + mcontract_size falseCont" +|"mcontract_size (When [] _ cont) = 1 + mcontract_size cont" +|"mcontract_size (When (c#cs) t cont) = mcase_size c + mcontract_size ((When cs t cont))" +|"mcase_size (Case _ cont) = 1 + mcontract_size cont " +|"mcase_size (MerkleizedCase _ _) = 1 " + +fun addMerkleMapSize :: "(ByteString \ MContract) \ nat \ nat" where +"addMerkleMapSize e a = mcontract_size (snd e) + a" + + +fun merkleMap_size :: "MerkleMap \ nat" where +"merkleMap_size m = ffold addMerkleMapSize 0 (fset_of_fmap m)" + +lemma cont_size_lt_when [simp] : "mcontract_size cont < mcontract_size (When cases timeout cont)" + by (induction cases) simp_all + +lemma case_size_lt_when [simp]: "c \ set cases \ mcase_size c < mcontract_size (When cases timeout cont)" +proof (induction cases) + case Nil + then show ?case by simp +next + case (Cons a cases) + then show ?case + by (smt (verit, del_insts) Groups.ab_semigroup_add_class.add.commute Unmerkleize.mcontract_size.simps(7) cont_size_lt_when add_lessD1 nat_add_left_cancel_less set_ConsD) +qed + +interpretation comp_fun_commute "addMerkleMapSize" + by unfold_locales auto + +lemma merkleMap_size_distrib_drop: + assumes "fmlookup m k = Some c" + shows "merkleMap_size m = mcontract_size c + merkleMap_size (fmdrop k m)" +proof - + note assms + moreover obtain m' where "fmdrop k m = m'" + by simp + moreover have "\v. (k, v) |\| fset_of_fmap m'" + using calculation by fastforce + + moreover have "m = fmupd k c m'" + using calculation fmlookup_inject by fastforce + + moreover have "fset_of_fmap m = finsert (k,c) (fset_of_fmap m')" + using calculation + apply auto + by presburger (metis Option.option.inject) + + ultimately show ?thesis + by auto +qed + +subsection "Unmerkleize" + +text "We define the unmerkleize function for contract and case together as they are mutually recursive. +Each function takes as input a map of continuations and the merkleized contract or case, and may return + the unmerkleized version if all the continuations are present in the map +" +term those +function (sequential) unmerkleize :: "MerkleMap \ MContract \ Contract option" +and unmerkleizeCase :: "MerkleMap \ MCase \ Case option" +where +\ \Close is the base case\ + "unmerkleize _ MContract.Close = Some Contract.Close" +\ \Pay, Let, Assert and If recursively unmerkleize the continuations\ +|"unmerkleize merkleConts (MContract.Pay accId payee tok val cont) = + map_option (Contract.Pay accId payee tok val) (unmerkleize merkleConts cont)" +|"unmerkleize merkleConts (MContract.Let valId val cont) = + map_option (Contract.Let valId val) (unmerkleize merkleConts cont)" +|"unmerkleize merkleConts (MContract.Assert obs cont) = + map_option (Contract.Assert obs) (unmerkleize merkleConts cont)" +|"unmerkleize merkleConts (MContract.If obs contTrue contFalse) = + (let + mContTrue = unmerkleize merkleConts contTrue; + mContFalse = unmerkleize merkleConts contFalse + in + case (mContTrue, mContFalse) of + (Some t, Some f) \ Some (Contract.If obs t f) + |(_, _) \ None + ) + " +\ \For the \<^emph>\When\ contract we unmerkleize the timeout continuation and the cases\ +|"unmerkleize merkleConts (MContract.When cases timeout cont) = + (let + mCont = unmerkleize merkleConts cont; + \ \\<^emph>\those:: a option list \ 'a list option\ makes sure that all the cases succeed\ + mCases = those (map (unmerkleizeCase merkleConts) cases) + + in + case (mCases, mCont) of + (Some cs, Some c) \ Some (Contract.When cs timeout c) + |(_, _) \ None + ) + " +\ \For the normal case we just unmerkleize the continuation\ +|"unmerkleizeCase merkleConts (MCase.Case action cont) = + map_option (Case.Case action) (unmerkleize merkleConts cont)" +\ \For the merkleized case, we check if the continuation hash is present in the map of continuations. + If it is, we continue the unmerkleization process by dropping the case from the map. + Removing contHash from the map ensures that there are no loops (which is needed to prove termination). + Note that we are not verifying that the contract continuation hashes to contHash. + That would provide a higher level of assurance since it not only prevents loops but also + ensures authenticity. Eventually, when we execute the merkleized contract on the blockchain, + it is necessary to perform this authenticity check. However, in this context, relaxing the + assumption that contHash corresponds to the contract continuation allows for greater flexibility + in the unmerkleization process and contract creation\ +|"unmerkleizeCase merkleConts (MCase.MerkleizedCase action contHash) = + ( let + cont' = fmlookup merkleConts contHash >>= unmerkleize (fmdrop contHash merkleConts) + in + map_option (Case.Case action) cont' + ) + " + by pat_completeness auto +termination +\ \To prove that the function terminates we use a measure related to the number of continuations. +At each recursive call, either the measure of the continuation gets smaller, or the measure of all +possible continuations (from the map) get smaller\ + apply (relation "measure + (\t. case t of + Inl (dict, cont) \ merkleMap_size dict + mcontract_size cont + |Inr (dict, case') \ merkleMap_size dict + mcase_size case' + )") + using merkleMap_size_distrib_drop by auto + + +end \ No newline at end of file diff --git a/isabelle/ROOT b/isabelle/ROOT index d91390e4..c2d04b6d 100644 --- a/isabelle/ROOT +++ b/isabelle/ROOT @@ -67,6 +67,17 @@ session CodeExports in "CodeExports" = HOL + CodeExports export_files (in "../generated") [3] "*:code/**" +session Merkle in "Merkle" = HOL + + description "Alternative version of Marlowe with Merkleization" + options [document = false, system_heaps = false] + sessions + "HOL-Library" + "Core" + theories + MerkleTypes + MerkleInterpreter + Unmerkleize + chapter Doc session Cheatsheet in "Doc/Cheatsheet" = HOL +