From 09b57fd84e858359e5ee1e8d6a2abae928719ca9 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 12:00:56 -0300 Subject: [PATCH 01/24] Add clarification to choices --- isabelle/Core/SemanticsTypes.thy | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/isabelle/Core/SemanticsTypes.thy b/isabelle/Core/SemanticsTypes.thy index ad503aac..9ec87f6f 100644 --- a/isabelle/Core/SemanticsTypes.thy +++ b/isabelle/Core/SemanticsTypes.thy @@ -119,6 +119,8 @@ data type is a tuple of integers that represents an \<^bold>\inclusive\A \<^emph>\Choice\ is an external action \secref{sec:actions-and-inputs}, so it can only be made as part +of a \<^emph>\When\ contract \secref{sec:contracts}\ subsection \Values and Observations\label{sec:values-and-observations} \ @@ -194,14 +196,13 @@ and @{term "x = y"} are represented by @{term "ValueLT x y"}, @{term "ValueLE x subsection \Actions and inputs\label{sec:actions-and-inputs}\ text \ -@{term "Action"}s and @{term "Input"}s are closely related. An @{term "Action"} can be added in a list -of @{term "Case"}s \secref{sec:contracts} as a way to declare the possible external @{term "Input"}s a -@{term "Party"} can include in a @{term "Transaction"} at a certain time. - +@{term "Action"}s and @{term "Input"}s are closely related. When we design the contract we +can declare that an external @{term "Action"} is needed to advance to a particular path. +These actions can only be present in a @{term "Case"} of the @{term "When"} contract \secref{sec:contracts} \ text \ -The different types of actions are: +The different types of external actions are: \ datatype Action = Deposit AccountId Party Token Value From 8f66d393158a98657b2282a6a59df08b0025ccac Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 17:17:07 -0300 Subject: [PATCH 02/24] Fix note around division --- isabelle/Doc/Specification/Core.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/isabelle/Doc/Specification/Core.thy b/isabelle/Doc/Specification/Core.thy index b6765287..570e7489 100644 --- a/isabelle/Doc/Specification/Core.thy +++ b/isabelle/Doc/Specification/Core.thy @@ -165,7 +165,7 @@ text \@{thm evalValue_MulValue}\ subsubsection \Division\ -text \Division is a special case because we only evaluate to natural numbers: +text \Division is a special case because we only evaluate to integers: \<^item> If the denominator is 0, the result is also 0. Other languages uses NaN or Infinity to represent this case \<^item> The result will be rounded towards zero.\ From 009c42b444a106047319a663734d86a24e30e307 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 17:39:23 -0300 Subject: [PATCH 03/24] Show maximum time lemma without inference rule --- isabelle/Doc/Specification/Guarantees.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/isabelle/Doc/Specification/Guarantees.thy b/isabelle/Doc/Specification/Guarantees.thy index 7df91576..fd11b27b 100644 --- a/isabelle/Doc/Specification/Guarantees.thy +++ b/isabelle/Doc/Specification/Guarantees.thy @@ -138,7 +138,7 @@ subsection \All Contracts Have a Maximum Time\label{sec:max-time-guarantee text \If one sends an empty transaction with time equal to @{const maxTimeContract}, then the contract will close.\ -text \@{thm [mode=Rule,names_short] timedOutTransaction_closes_contract}\ +text \@{thm [display,names_short, margin=40] timedOutTransaction_closes_contract}\ subsection \Contract Does Not Hold Funds After it Closes\ From b194dc6022a7d27b650eb3719e22db030d3c817a Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 17:40:53 -0300 Subject: [PATCH 04/24] Remove duplicate reference of IntervalResult --- isabelle/Doc/Specification/Core.thy | 4 ---- 1 file changed, 4 deletions(-) diff --git a/isabelle/Doc/Specification/Core.thy b/isabelle/Doc/Specification/Core.thy index 570e7489..3b2f6707 100644 --- a/isabelle/Doc/Specification/Core.thy +++ b/isabelle/Doc/Specification/Core.thy @@ -51,10 +51,6 @@ with the time interval of @{term Environment} \secref{sec:state-and-env} to yiel time for the new state that will result from applying the transaction. It throws an error if the interval is nonsensical or in the past.\ -text \ -@{datatype [display,names_short, margin=40]IntervalResult} -\ - (* FIXME: synonim are expanding *) text \@{code_stmts fixInterval constant: fixInterval (Haskell)}\ From 06a95af6434cf56800518d1275821dc8024f082c Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 17:46:54 -0300 Subject: [PATCH 05/24] Removed undefined reference --- isabelle/Core/SemanticsTypes.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/isabelle/Core/SemanticsTypes.thy b/isabelle/Core/SemanticsTypes.thy index 9ec87f6f..884ebf65 100644 --- a/isabelle/Core/SemanticsTypes.thy +++ b/isabelle/Core/SemanticsTypes.thy @@ -259,7 +259,7 @@ and Contract = Close | Assert Observation Contract text \@{term Close} is the simplest contract, when we evaluate it, the execution is completed and we -generate \<^term>\Payment\s \secref{TODO} for the assets in the internal accounts to their default owners +generate \<^term>\Payment\s for the assets in the internal accounts to their default owners \<^footnote>\Even if the payments are generated one at a time (per account and per Token), the cardano implementation generates a single transaction\. \ From 2a51a804c96200ede86ad43aedc37187902134f9 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 18:09:15 -0300 Subject: [PATCH 06/24] Clarify the utilities functions --- isabelle/Doc/Specification/Core.thy | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/isabelle/Doc/Specification/Core.thy b/isabelle/Doc/Specification/Core.thy index 3b2f6707..cb666b32 100644 --- a/isabelle/Doc/Specification/Core.thy +++ b/isabelle/Doc/Specification/Core.thy @@ -104,12 +104,21 @@ subsection \Utilities\label{sec:accountutilities}\ text \The @{const moneyInAccount}, @{const updateMoneyInAccount}, and @{const addMoneyToAccount} functions read, write, and increment the funds in a particular account of the @{term State}, -respectively. The @{const giveMoney} function transfer funds internally between accounts. The -@{const refundOne} function finds the first account with funds in it.\ +respectively.\ text \@{code_stmts moneyInAccount constant: moneyInAccount (Haskell)}\ text \@{code_stmts updateMoneyInAccount constant: updateMoneyInAccount (Haskell)}\ text \@{code_stmts addMoneyToAccount constant: addMoneyToAccount (Haskell)}\ + +(* TODO: This will become clearer after refactoring the semantics as literal programming PLT-3761 *) +text \The @{const giveMoney} function is used in @{const reduceContractStep} to execute a Payment. +It takes as arguments the Party to remove funds from, the Payee to pay to, the amount and token to pay +and the state accounts. It returns the Payment as a Reduce effect and the new state accounts. + +\ text \@{code_stmts giveMoney constant: giveMoney (Haskell)}\ + +text \The @{const refundOne} function is also used inside @{const reduceContractStep}. It receives +the state accounts, and returns the first account with funds and the rest of the accounts.\ text \@{code_stmts refundOne constant: refundOne (Haskell)}\ subsection \Evaluate Value\label{sec:evalvalue}\ From 0c1a6426132546c584592748626a75ac310ea03d Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 18:28:28 -0300 Subject: [PATCH 07/24] Improved definition for NegValue --- isabelle/Doc/Specification/Core.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/isabelle/Doc/Specification/Core.thy b/isabelle/Doc/Specification/Core.thy index cb666b32..cf5468aa 100644 --- a/isabelle/Doc/Specification/Core.thy +++ b/isabelle/Doc/Specification/Core.thy @@ -158,9 +158,9 @@ text \@{thm evalValue_SubValue}\ subsubsection \Negation\ -text \For every value \<^emph>\x\ there is the complement \<^emph>\NegValue x\ so that\ +text \For the \<^emph>\NegValue\ case, @{const evalValue} will evaluate the inner value and negate it\ -text \@{thm evalNegValue}\ +text \@{thm evalValue_NegValue}\ subsubsection \Multiplication\ From e846d3ba2e9edd864ed606c8e6b3b7259738b195 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Wed, 15 Mar 2023 18:34:45 -0300 Subject: [PATCH 08/24] Fix typos --- isabelle/Core/OptBoundTimeInterval.thy | 4 ++-- isabelle/Doc/Specification/Core.thy | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/isabelle/Core/OptBoundTimeInterval.thy b/isabelle/Core/OptBoundTimeInterval.thy index 6c2ff027..e05b78d4 100644 --- a/isabelle/Core/OptBoundTimeInterval.thy +++ b/isabelle/Core/OptBoundTimeInterval.thy @@ -34,12 +34,12 @@ fun bToSet :: "OptBoundTimeInterval => POSIXTime set" where | "bToSet (Bounded l, Bounded r) = {l..r}" -section "Interval intesection" +section "Interval intersection" text \ The interval intersection is achieved by calculating the maximum lower bound and the minimum -higher bound, favouring Bounded to Unbounded endpoits. +higher bound, favouring Bounded to Unbounded endpoints. \ fun maxLow :: "BEndpoint \ BEndpoint \ BEndpoint" where "maxLow Unbounded y = y" diff --git a/isabelle/Doc/Specification/Core.thy b/isabelle/Doc/Specification/Core.thy index cf5468aa..b5c3f892 100644 --- a/isabelle/Doc/Specification/Core.thy +++ b/isabelle/Doc/Specification/Core.thy @@ -198,7 +198,7 @@ text \@{thm evalValue_TimeIntervalEnd}\ subsubsection \Use Value\ -text \For the \<^emph>\TimeIntervalEnd\ case, @{const evalValue} will look in its state for a bound @{typ ValueId}. +text \For the \<^emph>\UseValue\ case, @{const evalValue} will look in its state for a bound @{typ ValueId}. It will default to zero if it doesn't find it.\ text \@{thm evalValue_UseValue}\ From 09b802022001c30b543131c7708de691f34c798f Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 10:42:06 -0300 Subject: [PATCH 09/24] Fix party in ApplyNonPositiveDeposit warning --- isabelle/Core/Semantics.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/isabelle/Core/Semantics.thy b/isabelle/Core/Semantics.thy index fa858d14..70023760 100644 --- a/isabelle/Core/Semantics.thy +++ b/isabelle/Core/Semantics.thy @@ -510,7 +510,7 @@ fun applyCases :: "Environment \ State \ Input \ amount = evalValue env state val) then let warning = if amount > 0 then ApplyNoWarning - else ApplyNonPositiveDeposit party1 accId2 tok2 amount in + else ApplyNonPositiveDeposit party2 accId2 tok2 amount in let newState = state \ accounts := addMoneyToAccount accId1 tok1 amount (accounts state) \ in Applied warning newState cont else applyCases env state (IDeposit accId1 party1 tok1 amount) rest)" | From f42ae9daf3b4ea9f9bbe5d09b2ebb0b65a5c3f31 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 10:48:05 -0300 Subject: [PATCH 10/24] Avoid shadowing in Applied case --- isabelle/Core/Semantics.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/isabelle/Core/Semantics.thy b/isabelle/Core/Semantics.thy index 70023760..6bb3eb51 100644 --- a/isabelle/Core/Semantics.thy +++ b/isabelle/Core/Semantics.thy @@ -580,8 +580,8 @@ fun applyAllLoop :: "bool \ Environment \ State \ (case applyInput env curState input cont of - Applied applyWarn newState cont \ - applyAllLoop True env newState cont rest + Applied applyWarn newState appliedCont \ + applyAllLoop True env newState appliedCont rest (warnings @ (convertReduceWarnings reduceWarns) @ (convertApplyWarning applyWarn)) (payments @ pays) From 738550947ef948bdd6d1a873758f887a2d735b0d Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 16:46:45 -0300 Subject: [PATCH 11/24] Add comments to calculateNonAmbiguousInterval --- isabelle/Core/Semantics.thy | 60 ++++++++++++++++++++++++++++++++----- 1 file changed, 53 insertions(+), 7 deletions(-) diff --git a/isabelle/Core/Semantics.thy b/isabelle/Core/Semantics.thy index 6bb3eb51..1bdcd444 100644 --- a/isabelle/Core/Semantics.thy +++ b/isabelle/Core/Semantics.thy @@ -721,34 +721,80 @@ and maxTimeCase :: "Case \ int" where subsection "calculateNonAmbiguousInterval" +text "Helper functions for \<^emph>\calculateNonAmbiguousInterval\" fun gtIfNone :: "int option \ int \ bool" where "gtIfNone None _ = True" | "gtIfNone (Some x) y = (x > y)" fun geIfNone :: "int option \ int \ bool" where "geIfNone None _ = True" | -"geIfNone (Some x) y = (x \ y)" +"geIfNone (Some x) y = (x \ y) " fun subIfSome :: "int option \ int \ int option" where "subIfSome None _ = None" | "subIfSome (Some x) y = Some (x - y)" +text \ +A TimeInterval (startTime, endTime) can be ambiguous wrt a When's timeout if startTime < timeout \ endTime + +\ + +text \The \<^emph>\calculateNonAmbiguousInterval\ function can help a user to calculate a TimeInterval that +won't be ambiguous for the next \<^emph>\n\ inputs of a contract.\ + +text \The only Contract constructor that can yield a \<^term>\TEAmbiguousTimeIntervalError\ is the \<^term>\When\ case. +Computing a transaction of a contract that starts in a non quiescent state (\<^term>\Let\, \<^term>\Pay\, \<^term>\If\, \<^term>\Assert\) +can end in a \<^term>\TEAmbiguousTimeIntervalError\ iff there is a \<^term>\When\ case that makes it ambiguous. +\ + +text \A TimeInterval expressed as the tuple \<^term>\(startTime \ endTime)\ can be ambiguous wrt a \<^term>\When\'s timeout +iff \<^emph>\startTime < timeout \ endTime\ +\ + +text +\ It parameters of \<^emph>\calculateNonAmbiguousInterval\ are: +\<^item> An optional number of Inputs to check. The number of inputs corresponds to the number of "When". +If None is passed, it means that we should check for transactions of any number of inputs. +\<^item> A lower bound (normally the current time). +\<^item> The Contract to check. + +The function returns an Optionally Bound Time Interval, as defined in the \<^emph>\OptBoundTimeInterval.thy\ theory. +In the \<^emph>\TimeRange.thy\ theory we prove that computing a transaction with these bounds doesn't end with an ambiguous error. +\ +\ \TODO: The intersectInterval can produce an invalid time interval, which would mean that not suitable TimeInterval was found\ fun calculateNonAmbiguousInterval :: "int option \ POSIXTime \ Contract \ OptBoundTimeInterval" -where + where +\ \A Close contract can't be ambiguous, so an Unbounded interval is returned \ "calculateNonAmbiguousInterval _ _ Close = (Unbounded, Unbounded)" | +\ \A Pay contract isn't ambiguous by itself, so we calculate for the continuation\ "calculateNonAmbiguousInterval n t (Pay _ _ _ _ c) = calculateNonAmbiguousInterval n t c" | -"calculateNonAmbiguousInterval n t (If _ ct cf) = intersectInterval (calculateNonAmbiguousInterval n t ct) +\ \If we branch, we intersect the result of both possibilites. \ +\ \TODO: Note that not knowing which branch can be selected beforehand means that we return a smaller TimeInterval than +possible. Maybe we could improve this by using the actual Input instead of the number of inputs\ +"calculateNonAmbiguousInterval n t (If _ ct cf) = intersectInterval + (calculateNonAmbiguousInterval n t ct) (calculateNonAmbiguousInterval n t cf)" | -"calculateNonAmbiguousInterval n t (When Nil timeout tcont) = +\ \We treat the When contract in two parts. The base case (when no actions are available) and a recursive +case, when we have a particular action \ +"calculateNonAmbiguousInterval n t (When [] timeout tcont) = (if t < timeout + \ \If the When's timeout is in the future, we can generate a non-ambiguous time interval + by restricting the endTime to be strictly lower than the timeout\ then (Unbounded, Bounded (timeout - 1)) + \ \If the timeout is in the past, we need to restrict the startTime to be larger or equal than + the timeout\ else intersectInterval (Bounded timeout, Unbounded) (calculateNonAmbiguousInterval n t tcont))" | -"calculateNonAmbiguousInterval n t (When (Cons (Case _ cont ) tail) timeout tcont) = + +"calculateNonAmbiguousInterval n t (When (Case _ cont # restCases) timeout tcont) = (if gtIfNone n 0 +\ \If n is none (check all) or n > 0 we recursively calculate the intersection for all the continuations\ then intersectInterval (calculateNonAmbiguousInterval (subIfSome n 1) t cont) - (calculateNonAmbiguousInterval n t (When tail timeout tcont)) - else calculateNonAmbiguousInterval n t (When tail timeout tcont))" | + (calculateNonAmbiguousInterval n t (When restCases timeout tcont)) +\ \If n \ 0 we don't calculate for the current case and we iterate until we reach the base case\ +\ \TODO: we should be able to change restCases for [] to check the base case directly\ + else calculateNonAmbiguousInterval n t (When restCases timeout tcont))" | +\ \A Let or Assert contracts aren't ambiguous by themselves, so we calculate for the continuation\ "calculateNonAmbiguousInterval n t (Let _ _ c) = calculateNonAmbiguousInterval n t c" | "calculateNonAmbiguousInterval n t (Assert _ c) = calculateNonAmbiguousInterval n t c" From e64cfcbedbee7652169288339e9c76f4f78fcbc4 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 17:07:08 -0300 Subject: [PATCH 12/24] Promote some lemmas to theorems --- isabelle/Core/ValidState.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/isabelle/Core/ValidState.thy b/isabelle/Core/ValidState.thy index ad3daba5..20afada7 100644 --- a/isabelle/Core/ValidState.thy +++ b/isabelle/Core/ValidState.thy @@ -173,7 +173,7 @@ lemma computeTransaction_preserves_valid_state_aux : by simp by simp -lemma computeTransaction_preserves_valid_state : +theorem computeTransaction_preserves_valid_state : "valid_state state \ computeTransaction tran state cont = TransactionOutput out \ valid_state (txOutState out) " by (metis (full_types) Transaction.surjective TransactionOutputRecord.surjective computeTransaction_preserves_valid_state_aux old.unit.exhaust) @@ -191,7 +191,7 @@ lemma empty_state_valid_state : "valid_state (emptyState sl)" by (metis MList.valid_empty State.select_convs(1) State.select_convs(2) State.select_convs(3) emptyState.elims valid_state.simps) -lemma playTrace_preserves_valid_state : +theorem playTrace_preserves_valid_state : "playTrace sl c transList = TransactionOutput txOut \ valid_state (txOutState txOut)" apply (simp only:playTrace.simps) From bc4803d22adbeca149b6f5379ab93e1b147150e3 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 17:07:34 -0300 Subject: [PATCH 13/24] Fix typo --- isabelle/Core/SingleInputTransactions.thy | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/isabelle/Core/SingleInputTransactions.thy b/isabelle/Core/SingleInputTransactions.thy index 94b40a4c..b51d85f2 100644 --- a/isabelle/Core/SingleInputTransactions.thy +++ b/isabelle/Core/SingleInputTransactions.thy @@ -35,11 +35,11 @@ lemma reductionLoopIdempotent : by simp done -lemma reduceContractUntilQuiescentIdempotent : +lemma reduceContractUntilQuiescentIdempotent : "reduceContractUntilQuiescent env state contract = ContractQuiescent reducedAfter wa pa nsta ncont \ reduceContractUntilQuiescent env nsta ncont = ContractQuiescent False [] [] nsta ncont" apply (simp only:reduceContractUntilQuiescent.simps) - using reductionLoopIdempotent by blast + using reductionLoopIdempotent by blast lemma applyAllLoopEmptyIdempotent : "applyAllLoop reducedBefore env sta cont [] a b = ApplyAllSuccess reducedAfter wa pa nsta ncont \ @@ -124,7 +124,7 @@ lemma applyLoopIdempotent : using applyLoopIdempotent_base_case by auto by simp by simp - + lemma applyLoopIdempotent_base_case2 : "applyAllLoop reducedBefore env sta cont [] twa tef = ApplyAllSuccess reducedAfter wa pa nsta ncont \ applyAllLoop reducedAfter env nsta ncont t [] [] = ApplyAllSuccess reducedAfter2 nwa npa fsta fcont \ @@ -650,7 +650,7 @@ lemma applyAllLoop_longer_doesnt_grow : subgoal for reducedBefore env sta cont t wa pa reducedAfter1 cwa1 pa1 sta1 cont1 reducedAfter2 cwa2 pa2 sta2 cont2 apply (subst (asm) applyAllLoop.simps) apply (subst (asm) applyAllLoop.simps[of reducedBefore env sta cont "[] @ t"]) - apply (cases "reduceContractUntilQuiescent env sta cont") + apply (cases "reduceContractUntilQuiescent env sta cont") apply (simp only:ReduceResult.case) apply (simp only:list.case append_Nil) subgoal for reducedAfter wa pa nsta ncont @@ -659,7 +659,7 @@ lemma applyAllLoop_longer_doesnt_grow : apply blast apply (simp only:list.case) subgoal for head tail - apply (cases "applyInput env nsta head ncont") + apply (cases "applyInput env nsta head ncont") apply (simp only:ApplyResult.case) apply (metis ApplyAllResult.inject applyAllLoop_only_makes_smaller applyInput_only_makes_smaller less_le_trans not_le_imp_less order.asym) by simp @@ -858,7 +858,7 @@ lemma computeTransactionStepEquivalence : apply (simp only:IntervalResult.case Let_def) subgoal for fIenv3 fIsta3 apply (cases "applyAllInputs fIenv3 fIsta3 icont rest") - apply (simp only:ApplyAllResult.case) + apply (simp only:ApplyAllResult.case) subgoal for reducedAfter3 cwa3 pa3 sta3 con3 apply (cases "\ reducedAfter3 \ (icont \ Close \ accounts ista = [])") apply (simp del:fixInterval.simps computeTransaction.simps applyAllInputs.simps only:refl if_False) @@ -974,7 +974,7 @@ lemma fixInterval_idemp_after_computeTransaction : fixInterval interv ista = IntervalTrimmed env ista" by (simp add: applyInput_preserves_minTime fixInterval_idemp_on_same_minTime reductionLoop_preserves_minTime) -lemma applyAllLoop_independet_of_acc_error1 : +lemma applyAllLoop_independent_of_acc_error1 : "applyAllLoop reducedBefore env sta cont htail wa pa = ApplyAllNoMatchError \ applyAllLoop reducedBefore env sta cont htail wa2 pa2 = ApplyAllNoMatchError" apply (induction htail arbitrary: reducedBefore env sta cont wa pa wa2 pa2) @@ -984,7 +984,7 @@ lemma applyAllLoop_independet_of_acc_error1 : by (auto split:ReduceResult.split ApplyResult.split simp del:applyAllLoop.simps) done -lemma applyAllLoop_independet_of_acc_error2 : +lemma applyAllLoop_independent_of_acc_error2 : "applyAllLoop reducedBefore env sta cont htail wa pa = ApplyAllAmbiguousTimeIntervalError \ applyAllLoop reducedBefore env sta cont htail wa2 pa2 = ApplyAllAmbiguousTimeIntervalError" apply (induction htail arbitrary: reducedBefore env sta cont wa pa wa2 pa2) @@ -1051,8 +1051,8 @@ lemma computeTransactionStepEquivalence_error : apply (smt ApplyAllResult.simps(8) ApplyResult.distinct(1) ApplyResult.simps(4) ReduceResult.simps(4) append.assoc append_self_conv applyAllInputsPrefix1 applyAllInputsPrefix2 applyAllLoop.simps applyAllLoopJustAppendsWarningsAndEffects applyInput.simps(2) list.simps(5) reduceContractUntilQuiescentIdempotent) apply simp by auto - apply (metis (no_types, lifting) ApplyAllResult.simps(9) ApplyResult.simps(4) ReduceResult.simps(4) applyAllLoop.simps applyAllLoop_independet_of_acc_error1 list.simps(5) reduceContractUntilQuiescentIdempotent) - by (metis (no_types, lifting) ApplyAllResult.simps(10) ApplyResult.simps(4) ReduceResult.simps(4) applyAllLoop.simps applyAllLoop_independet_of_acc_error2 list.simps(5) reduceContractUntilQuiescentIdempotent) + apply (metis (no_types, lifting) ApplyAllResult.simps(9) ApplyResult.simps(4) ReduceResult.simps(4) applyAllLoop.simps applyAllLoop_independent_of_acc_error1 list.simps(5) reduceContractUntilQuiescentIdempotent) + by (metis (no_types, lifting) ApplyAllResult.simps(10) ApplyResult.simps(4) ReduceResult.simps(4) applyAllLoop.simps applyAllLoop_independent_of_acc_error2 list.simps(5) reduceContractUntilQuiescentIdempotent) using reduceContractUntilQuiescentIdempotent by auto by simp by simp @@ -1234,5 +1234,5 @@ lemma inputToTransactions_isSingleInput : "isSingleInput (inputsToTransactions s lemma traceListToSingleInput_isSingleInput2 : "isSingleInput (traceListToSingleInput t)" apply (induction t rule:traceListToSingleInput.induct) by (simp_all add: inputToTransactions_isSingleInput isSingleInput_dist_with_append) - + end From 8596198c7fc956df0d9ecdc20bce3e5d1df899d1 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 17:07:51 -0300 Subject: [PATCH 14/24] Removed duplicate isValidInterval --- isabelle/Core/TimeRange.thy | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/isabelle/Core/TimeRange.thy b/isabelle/Core/TimeRange.thy index 925fd40c..9dfa4850 100644 --- a/isabelle/Core/TimeRange.thy +++ b/isabelle/Core/TimeRange.thy @@ -227,8 +227,6 @@ lemma geIfNone_redListSize : "geIfNone n (int (length (h # t))) \ geIfNone (subIfSome n 1) (int (length t))" by (smt (verit, ccfv_threshold) Semantics.geIfNone.elims(1) Semantics.geIfNone.simps(2) Semantics.subIfSome.elims impossible_Cons of_nat_le_iff) -fun isValidInterval :: "POSIXTime \ POSIXTime \ bool" where -"isValidInterval (a, b) = (a \ b)" lemma reduceStep_ifCaseLtCt_aux : "inInterval (a, b) (calculateNonAmbiguousInterval n ct (When x41 x42 x43)) \ a \ b \ env = \timeInterval = (a, b)\ \ b < x42 \ ct < x42" @@ -243,7 +241,7 @@ lemma reduceStep_ifCaseLtCt_aux : "inInterval (a, b) (calculateNonAmbiguousInter done lemma reduceStep_ifCaseLtCt : "inInterval (timeInterval env) (calculateNonAmbiguousInterval n ct (When x41 x42 x43)) \ - reduceContractStep env state (When x41 x42 x43) = NotReduced \ isValidInterval (timeInterval env) \ ct < x42" + reduceContractStep env state (When x41 x42 x43) = NotReduced \ validTimeInterval (timeInterval env) \ ct < x42" apply (cases env) subgoal for timeInterv apply (cases timeInterv) @@ -257,7 +255,7 @@ lemma reduceStep_ifCaseLtCt : "inInterval (timeInterval env) (calculateNonAmbigu done lemma reduceLoop_ifCaseLtCt : "inInterval (timeInterval env) (calculateNonAmbiguousInterval n ct cont) \ - reductionLoop b env state cont wa ef = ContractQuiescent x11 x12 x13 x14 x15 \ isValidInterval (timeInterval env) \ ifCaseLt ct x15" + reductionLoop b env state cont wa ef = ContractQuiescent x11 x12 x13 x14 x15 \ validTimeInterval (timeInterval env) \ ifCaseLt ct x15" apply (induction b env state cont wa ef rule:reductionLoop.induct) subgoal for reduced env state contract warnings payments apply (cases "x15 = Close") @@ -279,14 +277,14 @@ lemma reduceLoop_ifCaseLtCt : "inInterval (timeInterval env) (calculateNonAmbigu lemma reduceContractUntilQuiescent_ifCaseLtCt : "inInterval (timeInterval env) (calculateNonAmbiguousInterval n ct cont) \ reduceContractUntilQuiescent env state cont = ContractQuiescent x11 x12 x13 x14 x15 \ - isValidInterval (timeInterval env) \ ifCaseLt ct x15" + validTimeInterval (timeInterval env) \ ifCaseLt ct x15" apply (simp only:reduceContractUntilQuiescent.simps) by (simp add: reduceLoop_ifCaseLtCt) lemma calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllLoop : "geIfNone n (int (length inps)) \ inInterval (timeInterval env) (calculateNonAmbiguousInterval n ct c) \ - isValidInterval (timeInterval env) \ + validTimeInterval (timeInterval env) \ applyAllLoop b env s c inps wa ef \ ApplyAllAmbiguousTimeIntervalError" apply (induction b env s c inps wa ef arbitrary: n ct rule:applyAllLoop.induct) @@ -320,7 +318,7 @@ lemma calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllLoop : lemma calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllInputs : "geIfNone n (int (length inps)) \ inInterval (minInterv, maxInterv) (calculateNonAmbiguousInterval n ct c) \ - isValidInterval (minInterv, maxInterv) \ + validTimeInterval (minInterv, maxInterv) \ applyAllInputs \ timeInterval = (minInterv, maxInterv) \ s c inps \ ApplyAllAmbiguousTimeIntervalError" apply (simp only:applyAllInputs.simps) @@ -346,8 +344,8 @@ theorem calculateNonAmbiguousIntervalAvoidsAmbiguousInterval : subgoal for accounts choices boundValues minTime apply (cases "minInterv \ minTime") apply (simp del:applyAllInputs.simps) - apply (smt (verit, ccfv_threshold) OptBoundTimeInterval.inInterval.elims(3) OptBoundTimeInterval.inInterval.simps(2) OptBoundTimeInterval.inInterval.simps(3) OptBoundTimeInterval.inInterval.simps(4) TimeRange.isValidInterval.simps calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllInputs) - by (metis Lattices.linorder_class.max.absorb4 Lattices.linorder_class.max.commute TimeRange.isValidInterval.simps calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllInputs linorder_not_le) + apply (smt (verit, ccfv_threshold) OptBoundTimeInterval.inInterval.elims(3) OptBoundTimeInterval.inInterval.simps(2) OptBoundTimeInterval.inInterval.simps(3) OptBoundTimeInterval.inInterval.simps(4) validTimeInterval.simps calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllInputs) + by (metis Lattices.linorder_class.max.absorb4 Lattices.linorder_class.max.commute OptBoundTimeInterval.validTimeInterval.simps calculateNonAmbiguousIntervalAvoidsAmbiguousInterval_applyAllInputs linorder_not_le) done done done From 2ccfcaa919dad6420d08d0185c320a17bfecc5dd Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 17:18:29 -0300 Subject: [PATCH 15/24] Simplified computeTransaction_preserves_valid_state --- isabelle/Core/ValidState.thy | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/isabelle/Core/ValidState.thy b/isabelle/Core/ValidState.thy index 20afada7..0d689df8 100644 --- a/isabelle/Core/ValidState.thy +++ b/isabelle/Core/ValidState.thy @@ -157,26 +157,19 @@ lemma fixInterval_preserves_valid_state : apply (simp del:valid_state.simps add:Let_def) by auto -lemma computeTransaction_preserves_valid_state_aux : - "valid_state state \ - computeTransaction \interval = intervalI, inputs = inputsI\ state cont - = TransactionOutput \txOutWarnings = txOutWarningsO, txOutPayments = txOutPaymentsO, txOutState = txOutStateO, txOutContract = txOutContractO\ \ - valid_state (txOutStateO)" +theorem computeTransaction_preserves_valid_state : + "valid_state state \ computeTransaction tran state cont = TransactionOutput out \ valid_state (txOutState out)" apply (simp only:computeTransaction.simps Let_def) - apply (cases "fixInterval (interval \interval = intervalI, inputs = inputsI\) state") + apply (cases "fixInterval (interval tran) state") apply (simp only:IntervalResult.case) subgoal for env sta - apply (cases "applyAllInputs env sta cont (inputs \interval = intervalI, inputs = inputsI\)") + apply (cases "applyAllInputs env sta cont (inputs tran)") apply (simp only:ApplyAllResult.case) apply (metis TransactionOutput.distinct(1) TransactionOutput.inject(1) TransactionOutputRecord.select_convs(3) applyAllInputs.simps applyAllLoop_preserves_valid_state fixInterval_preserves_valid_state small_lazy'.cases) apply simp by simp by simp -theorem computeTransaction_preserves_valid_state : - "valid_state state \ computeTransaction tran state cont = TransactionOutput out \ valid_state (txOutState out) " - by (metis (full_types) Transaction.surjective TransactionOutputRecord.surjective computeTransaction_preserves_valid_state_aux old.unit.exhaust) - lemma playTraceAux_preserves_valid_state : "valid_state (txOutState txIn) \ playTraceAux txIn transList = TransactionOutput txOut \ From 08aab8fdcf590e92a76022e5350505688ae5bd46 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 17:36:15 -0300 Subject: [PATCH 16/24] Applied suggestions to TimeRange --- isabelle/Core/TimeRange.thy | 58 ++++++++++++++----------------------- 1 file changed, 21 insertions(+), 37 deletions(-) diff --git a/isabelle/Core/TimeRange.thy b/isabelle/Core/TimeRange.thy index 9dfa4850..5df9212e 100644 --- a/isabelle/Core/TimeRange.thy +++ b/isabelle/Core/TimeRange.thy @@ -5,47 +5,31 @@ begin theorem inIntervalIdempotentToIntersectInterval : "inInterval (min1, max1) (min2, max2) = (intersectInterval (Bounded min1, Bounded max1) (min2, max2) = (Bounded min1, Bounded max1))" - apply (cases min2) - apply (cases max2) - apply simp - subgoal for a - by auto[1] - apply (cases max2) - subgoal for a - by auto - subgoal for a b - by auto - done + by (cases min2;cases max2;auto) lemma inIntervalIdempotency1 : - "inInterval (x, y) (intersectInterval b c) \ inInterval (x, y) b" - apply (cases b) - apply (cases c) - subgoal for b1 b2 c1 c2 - apply (simp only:inInterval.simps) - apply (cases b1) - apply (cases c1) - apply (smt (verit, best) OptBoundTimeInterval.intersectInterval.simps OptBoundTimeInterval.maxLow.simps(1) OptBoundTimeInterval.minHigh.elims assoc commute inIntervalIdempotentToIntersectInterval) - apply (smt (verit, ccfv_threshold) OptBoundTimeInterval.inInterval.simps(2) OptBoundTimeInterval.inInterval.simps(4) OptBoundTimeInterval.intersectInterval.simps OptBoundTimeInterval.maxLow.simps(2) OptBoundTimeInterval.minHigh.elims OptBoundTimeInterval.minHigh.simps(2) inIntervalIdempotentToIntersectInterval maxLow_comm) - apply (cases c1) - apply simp - apply (smt (verit, ccfv_threshold) OptBoundTimeInterval.inInterval.simps(3) OptBoundTimeInterval.inInterval.simps(4) OptBoundTimeInterval.minHigh.elims) - by (smt (verit) Groups.abel_semigroup.commute Groups.semigroup.assoc OptBoundTimeInterval.intersectInterval.simps OptBoundTimeInterval.maxLow.simps(3) OptBoundTimeInterval.minHigh.elims abel_semigroup_axioms inIntervalIdempotentToIntersectInterval semigroup_axioms) - done + assumes "inInterval (x, y) (intersectInterval b c)" + shows "inInterval (x, y) b" +proof (cases b) + case [simp]: (Pair b1 b2) + thus ?thesis proof (cases c) + case (Pair c1 c2) + thus ?thesis using assms by (cases c1; cases c2; cases b1; cases b2; simp) + qed +qed + lemma inIntervalIdempotency2 : - "inInterval (x, y) (intersectInterval b c) \ inInterval (x, y) c" - apply (cases b) - apply (cases c) - subgoal for b1 b2 c1 c2 - apply (simp only:intersectInterval.simps) - apply (cases b1) - apply (cases c1) - apply (metis OptBoundTimeInterval.intersectInterval.simps commute inIntervalIdempotency1) - apply (metis OptBoundTimeInterval.intersectInterval.simps commute inIntervalIdempotency1) - apply simp - by (metis OptBoundTimeInterval.intersectInterval.simps inIntervalIdempotency1 minHigh_comm) - done + assumes "inInterval (x, y) (intersectInterval b c)" + shows "inInterval (x, y) c" +proof (cases b) + case [simp]: (Pair b1 b2) + thus ?thesis proof (cases c) + case (Pair c1 c2) + thus ?thesis using assms by (cases c1; cases c2; cases b1; cases b2; simp) + qed +qed + lemma compatibleIdempotencyWhen : "b \ a2 \ b \ a1 \ From 8c33cb15d2545a50bae6873ce9152783764c19b5 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 17:53:41 -0300 Subject: [PATCH 17/24] Simplified linorder instances --- isabelle/Core/SemanticsGuarantees.thy | 107 +++++++++++--------------- 1 file changed, 43 insertions(+), 64 deletions(-) diff --git a/isabelle/Core/SemanticsGuarantees.thy b/isabelle/Core/SemanticsGuarantees.thy index 5bbeb130..d84ab370 100644 --- a/isabelle/Core/SemanticsGuarantees.thy +++ b/isabelle/Core/SemanticsGuarantees.thy @@ -47,17 +47,15 @@ instantiation "Party" :: linorder begin instance proof - fix x y - have "(x < y) = (x \ y \ \ y \ (x :: Party))" + fix x y :: Party + show "x < y \ x \ y \ \ y \ x" by (meson less_Party.simps less_Party_def less_eq_Party_def linearParty) - thus "(x < y) = (x \ y \ \ y \ x)" by simp next - fix x - have "x \ (x :: Party)" by (meson linearParty) - thus "x \ x" by simp + fix x :: Party + show "x \ x" by (meson linearParty) next - fix x y z - have "x \ y \ y \ z \ x \ (z :: Party)" + fix x y z :: Party + show "x \ y \ y \ z \ x \ z" apply (auto simp add:less_eq_Party_def) apply (cases x) apply (cases y) @@ -69,19 +67,14 @@ next apply (cases y) apply (cases z) apply simp_all - by (metis (full_types) SemanticsGuarantees.less_eq_Party.elims(2) SemanticsGuarantees.less_eq_Party.simps(4) SemanticsTypes.Party.simps(4) less_eq_BS_trans less_eq_ByteString_def) - - thus "x \ y \ y \ z \ x \ z" by simp + by (metis (full_types) SemanticsGuarantees.less_eq_Party.elims(2) SemanticsGuarantees.less_eq_Party.simps(4) SemanticsTypes.Party.simps(4) less_eq_BS_trans less_eq_ByteString_def) next - fix x y z - have "x \ y \ y \ x \ x = (y :: Party)" - by (smt (verit) SemanticsGuarantees.less_eq_Party.elims(2) SemanticsGuarantees.less_eq_Party.simps(3) SemanticsTypes.Party.inject(2) SemanticsTypes.Party.simps(4) byteStringLessEqTwiceEq less_eq_ByteString_def less_eq_Party_def) - - thus "x \ y \ y \ x \ x = (y :: Party)" by simp + fix x y z :: Party + show "x \ y \ y \ x \ x = y" + by (smt (verit) SemanticsGuarantees.less_eq_Party.elims(2) SemanticsGuarantees.less_eq_Party.simps(3) SemanticsTypes.Party.inject(2) SemanticsTypes.Party.simps(4) byteStringLessEqTwiceEq less_eq_ByteString_def less_eq_Party_def) next - fix x y - from linearParty have "x \ y \ y \ (x :: Party)" by simp - thus "x \ y \ y \ x" by simp + fix x y :: Party + from linearParty show "x \ y \ y \ x " by simp qed end @@ -113,28 +106,23 @@ instantiation "Token" :: linorder begin instance proof - fix x y - have "(x < y) = (x \ y \ \ y \ (x :: Token))" + fix x y :: Token + show "x < y \ x \ y \ \ y \ x" by (meson less_Tok.simps less_Token_def less_eq_Token_def linearToken) - thus "(x < y) = (x \ y \ \ y \ x)" by simp next - fix x - have "x \ (x :: Token)" by (meson linearToken) - thus "x \ x" by simp + fix x :: Token + show "x \ x" by (meson linearToken) next - fix x y z - have "x \ y \ y \ z \ x \ (z :: Token)" + fix x y z :: Token + show "x \ y \ y \ z \ x \ z" by (smt less_eq_BS_trans less_BS.simps less_eq_Tok.elims(2) less_eq_Tok.simps less_eq_Token_def oneLessEqBS) - thus "x \ y \ y \ z \ x \ z" by simp next - fix x y z - have "x \ y \ y \ x \ x = (y :: Token)" + fix x y z :: Token + show "x \ y \ y \ x \ x = y" by (smt Token.simps(1) byteStringLessEqTwiceEq less_BS.simps less_eq_Tok.elims(2) less_eq_Token_def oneLessEqBS) - thus "x \ y \ y \ x \ x = (y :: Token)" by simp next - fix x y - from linearToken have "x \ y \ y \ (x :: Token)" by simp - thus "x \ y \ y \ x" by simp + fix x y :: Token + from linearToken show "x \ y \ y \ x" by simp qed end (* END Proof of linorder for Token *) @@ -166,32 +154,28 @@ instantiation "ChoiceId" :: linorder begin instance proof - fix x y - have "(x < y) = (x \ y \ \ y \ (x :: ChoiceId))" + fix x y :: ChoiceId + show "x < y \ x \ y \ \ y \ x" by (meson less_ChoId.elims(2) less_ChoId.elims(3) less_ChoiceId_def less_eq_ChoiceId_def linearChoiceId) - thus "(x < y) = (x \ y \ \ y \ x)" by simp next - fix x - have "x \ (x :: ChoiceId)" by (meson linearChoiceId) - thus "x \ x" by simp + fix x :: ChoiceId + show "x \ x" by (meson linearChoiceId) + next - fix x y z - have "x \ y \ y \ z \ x \ (z :: ChoiceId)" + fix x y z :: ChoiceId + show "x \ y \ y \ z \ x \ z" apply (cases x) apply (cases y) apply (cases z) apply (simp only:less_eq_ChoiceId_def) by (smt less_eq_BS_trans less_BS.simps less_eq_ChoId.simps oneLessEqBS order.trans) - thus "x \ y \ y \ z \ x \ z" by simp next - fix x y z - have "x \ y \ y \ x \ x = (y :: ChoiceId)" + fix x y z :: ChoiceId + show "x \ y \ y \ x \ x = y" by (smt byteStringLessEqTwiceEq eq_iff less_BS.simps less_eq_ChoId.elims(2) less_eq_ChoId.simps less_eq_ChoiceId_def oneLessEqBS) - thus "x \ y \ y \ x \ x = (y :: ChoiceId)" by simp next - fix x y - from linearChoiceId have "x \ y \ y \ (x :: ChoiceId)" by simp - thus "x \ y \ y \ x" by simp + fix x y :: ChoiceId + from linearChoiceId show "x \ y \ y \ x" by simp qed end (* END Proof of linorder for ChoiceId *) @@ -221,28 +205,23 @@ instantiation "ValueId" :: linorder begin instance proof - fix x y - have "(x < y) = (x \ y \ \ y \ (x :: ValueId))" + fix x y :: ValueId + show "x < y \ x \ y \ \ y \ x" by (metis ValueId.exhaust less_BS.simps less_ValId.simps less_ValueId_def less_eq_ValId.simps less_eq_ValueId_def linearValueId) - thus "(x < y) = (x \ y \ \ y \ x)" by simp next - fix x - have "x \ (x :: ValueId)" by (meson linearValueId) - thus "x \ x" by simp + fix x :: ValueId + show "x \ x" by (meson linearValueId) next - fix x y z - have "x \ y \ y \ z \ x \ (z :: ValueId)" + fix x y z :: ValueId + show "x \ y \ y \ z \ x \ z" by (smt ValueId.simps(1) less_eq_BS_trans less_eq_ValId.elims(2) less_eq_ValId.elims(3) less_eq_ValueId_def) - thus "x \ y \ y \ z \ x \ z" by simp next - fix x y z - have "x \ y \ y \ x \ x = (y :: ValueId)" + fix x y z :: ValueId + show "x \ y \ y \ x \ x = y" by (metis ValueId.simps(1) byteStringLessEqTwiceEq less_eq_ValId.elims(2) less_eq_ValueId_def) - thus "x \ y \ y \ x \ x = (y :: ValueId)" by simp next - fix x y - from linearValueId have "x \ y \ y \ (x :: ValueId)" by simp - thus "x \ y \ y \ x" by simp + fix x y :: ValueId + from linearValueId show "x \ y \ y \ x" by simp qed end (* END Proof of linorder for ValueId *) From b7069ff815cfebec4c190bda0e421859aaf0cb8c Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 16 Mar 2023 18:02:07 -0300 Subject: [PATCH 18/24] Remove unused assumptions in PositiveAccounts --- isabelle/Core/PositiveAccounts.thy | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/isabelle/Core/PositiveAccounts.thy b/isabelle/Core/PositiveAccounts.thy index 37fc88fb..f712d1a8 100644 --- a/isabelle/Core/PositiveAccounts.thy +++ b/isabelle/Core/PositiveAccounts.thy @@ -9,8 +9,7 @@ fun positiveMoneyInAccountOrNoAccount :: "AccountId \ Token \ x > 0)" lemma addMoneyToAccountPositve_match : - "\x tok. positiveMoneyInAccountOrNoAccount x tok accs \ - money > 0 \ + "money > 0 \ newBalance > 0 \ positiveMoneyInAccountOrNoAccount y tok2 (MList.insert (y, tok2) newBalance accs)" apply simp @@ -18,7 +17,6 @@ lemma addMoneyToAccountPositve_match : lemma addMoneyToAccountPositive_noMatch : "\x tok. positiveMoneyInAccountOrNoAccount x tok accs \ - money > 0 \ (accId, tok) \ (y, tok2) \ newBalance > 0 \ positiveMoneyInAccountOrNoAccount y tok2 (MList.insert (accId, tok2) newBalance accs)" From 9f0938cdfa0266488df4885f3eed1e5755e8336a Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Fri, 17 Mar 2023 10:47:09 -0300 Subject: [PATCH 19/24] Removed unused assumptions --- isabelle/Core/QuiescentResult.thy | 3 +-- isabelle/Core/TimeRange.thy | 2 +- isabelle/Core/Timeout.thy | 18 +++++++++--------- isabelle/Core/ValidState.thy | 3 +-- 4 files changed, 12 insertions(+), 14 deletions(-) diff --git a/isabelle/Core/QuiescentResult.thy b/isabelle/Core/QuiescentResult.thy index 65fadf54..51c9c162 100644 --- a/isabelle/Core/QuiescentResult.thy +++ b/isabelle/Core/QuiescentResult.thy @@ -13,8 +13,7 @@ lemma reduceContractStepPayIsQuiescent : warning = if paidMoney < moneyToPay then ReducePartialPay x21 x22 tok paidMoney moneyToPay else ReduceNoWarning; (payment, finalAccs) = giveMoney x21 x22 tok paidMoney newAccs in Reduced warning payment (sta\accounts := finalAccs\) x24) = - NotReduced \ - cont = Pay x21 x22 tok x23 x24 \ False" + NotReduced \ False" apply (cases "evalValue env sta x23 \ 0") apply simp apply (cases "min (moneyInAccount x21 tok (accounts sta)) (evalValue env sta x23) < (evalValue env sta x23)") diff --git a/isabelle/Core/TimeRange.thy b/isabelle/Core/TimeRange.thy index 5df9212e..7c3b03a5 100644 --- a/isabelle/Core/TimeRange.thy +++ b/isabelle/Core/TimeRange.thy @@ -213,7 +213,7 @@ lemma geIfNone_redListSize : lemma reduceStep_ifCaseLtCt_aux : "inInterval (a, b) (calculateNonAmbiguousInterval n ct (When x41 x42 x43)) \ - a \ b \ env = \timeInterval = (a, b)\ \ b < x42 \ ct < x42" + a \ b \ b < x42 \ ct < x42" apply (induction x41) apply simp apply (smt (verit, best) OptBoundTimeInterval.inInterval.simps(3) inIntervalIdempotency1) diff --git a/isabelle/Core/Timeout.thy b/isabelle/Core/Timeout.thy index a4fc1afb..d5917e41 100644 --- a/isabelle/Core/Timeout.thy +++ b/isabelle/Core/Timeout.thy @@ -40,8 +40,7 @@ lemma reduceClose_is_Close : "reduceContractUntilQuiescent env sta Close = Contr using reductionLoopClose_is_Close by blast lemma timedOutReduce_only_quiescent_in_close_When : - "minTime sta \ iniTime \ - maxTimeContract (When x41 x42 x43) \ iniTime \ + "maxTimeContract (When x41 x42 x43) \ iniTime \ iniTime \ endTime \ reduceContractStep \timeInterval = (iniTime, endTime)\ (sta\minTime := iniTime\) (When x41 x42 x43) \ NotReduced" apply (induction x41) @@ -119,7 +118,7 @@ lemma maxTimeNotAmbiguous : "maxTimeContract cont \ iniTime \ iniTime \ + " maxTimeContract c \ iniTime \ iniTime \ endTime \ reduceContractStep \timeInterval = (iniTime, endTime)\ (sta\minTime := iniTime\) c = NotReduced \ c = Close" @@ -167,7 +166,7 @@ lemma timedOutReduceStep_does_not_modify_minTime : apply (smt ReduceStepResult.inject State.ext_inject State.surjective State.update_convs(3) State.update_convs(4) reduceContractStep.simps(5)) by simp -lemma timedOutReduceContractLoop_closes_contract : "minTime sta \ iniTime \ +lemma timedOutReduceContractLoop_closes_contract : " maxTimeContract cont \ iniTime \ iniTime \ endTime \ minTime sta = iniTime \ @@ -187,13 +186,14 @@ lemma timedOutReduceContractLoop_closes_contract : "minTime sta \ iniTime \< apply simp apply simp apply simp + + using facts maxTimeOnlyDecreases_reduceStep apply fastforce apply simp - using facts(3) facts(7) maxTimeOnlyDecreases_reduceStep apply fastforce - apply simp - using facts(5) facts(7) timedOutReduceStep_does_not_modify_minTime apply blast - by (metis (no_types, lifting) ReduceStepResult.simps(8) facts(6) facts(7) reductionLoop.simps) + using facts timedOutReduceStep_does_not_modify_minTime apply meson + using facts by (metis (no_types, lifting) ReduceStepResult.simps(8) reductionLoop.simps) done - using timedOutReduce_only_quiescent_in_close apply fastforce + using timedOutReduce_only_quiescent_in_close + apply (metis SemanticsTypes.State.cases SemanticsTypes.State.select_convs(4) SemanticsTypes.State.update_convs(4) reductionLoopClose_is_Close) using maxTimeNotAmbiguous_reduceStep by blast done diff --git a/isabelle/Core/ValidState.thy b/isabelle/Core/ValidState.thy index 0d689df8..8db6439a 100644 --- a/isabelle/Core/ValidState.thy +++ b/isabelle/Core/ValidState.thy @@ -25,8 +25,7 @@ lemma refundOne_preserves_valid_map_accounts : lemma reductionStep_preserves_valid_state_Refund : "valid_state state \ reduceContractStep env state Close = Reduced wa ef newState newCont \ - state = \accounts = oldAccounts, choices = oldChoices, boundValues = oldBoundValues, minTime = oldMinTime\ \ - newState = \accounts = newAccounts, choices = newChoices, boundValues = newBoundValues, minTime = newMinTime\ \ + state = \accounts = oldAccounts, choices = oldChoices, boundValues = oldBoundValues, minTime = oldMinTime\ \ valid_state newState" apply (cases "refundOne oldAccounts") using refundOne_preserves_valid_map_accounts by auto From 27ccf99d7abf976d33106afba54606bb58f8a2c5 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Fri, 17 Mar 2023 10:59:04 -0300 Subject: [PATCH 20/24] Removed duplicate lemmas --- isabelle/Core/PositiveAccounts.thy | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/isabelle/Core/PositiveAccounts.thy b/isabelle/Core/PositiveAccounts.thy index f712d1a8..35836ec2 100644 --- a/isabelle/Core/PositiveAccounts.thy +++ b/isabelle/Core/PositiveAccounts.thy @@ -364,20 +364,11 @@ lemma positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive : apply simp using positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive_aux2 by auto -theorem accountsArePositive : - "valid_state state \ (\x tok. positiveMoneyInAccountOrNoAccount x tok (accounts state)) \ - computeTransaction txIn state cont = TransactionOutput txOut \ - positiveMoneyInAccountOrNoAccount y tok2 (accounts (txOutState txOut))" - using computeTransaction_gtZero by blast - theorem accountsArePositive2 : "valid_state state \ allAccountsPositiveState state \ computeTransaction txIn state cont = TransactionOutput txOut - \ allAccountsPositiveState (txOutState txOut)" - by (meson accountsArePositive allAccountsPositiveImpliesPositiveMoneyInAccountOrNoAccount allAccountsPositiveState.elims(2) allAccountsPositiveState.elims(3) computeTransaction_preserves_valid_state positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive valid_state.elims(2)) - -lemma valid_state_valid_accounts : "valid_state state \ valid_map (accounts state)" - by simp + \ allAccountsPositiveState (txOutState txOut)" + by (meson computeTransaction_gtZero allAccountsPositiveImpliesPositiveMoneyInAccountOrNoAccount allAccountsPositiveState.elims(2) allAccountsPositiveState.elims(3) computeTransaction_preserves_valid_state positiveMoneyInAccountOrNoAccountImpliesAllAccountsPositive valid_state.elims(2)) theorem accountsArePositive2_trace : "valid_state (txOutState txIn) \ allAccountsPositiveState (txOutState txIn) From 9c258478a4264ad3aff2a20ea6b577beba21ffed Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Fri, 17 Mar 2023 11:44:49 -0300 Subject: [PATCH 21/24] Removed unused lemmas --- isabelle/Core/PositiveAccounts.thy | 8 -------- isabelle/Core/QuiescentResult.thy | 6 ++---- isabelle/Core/SingleInputTransactions.thy | 8 -------- isabelle/Core/ValidState.thy | 8 -------- 4 files changed, 2 insertions(+), 28 deletions(-) diff --git a/isabelle/Core/PositiveAccounts.thy b/isabelle/Core/PositiveAccounts.thy index 35836ec2..29402149 100644 --- a/isabelle/Core/PositiveAccounts.thy +++ b/isabelle/Core/PositiveAccounts.thy @@ -61,14 +61,6 @@ lemma positiveMoneyInAccountOrNoAccount_sublist_gtZero_different : apply (simp only:positiveMoneyInAccountOrNoAccount.simps findWithDefault.simps) by (metis MList.delete.simps(2) MList.different_delete_lookup) -lemma positiveMoneyInAccountOrNoAccount_sublist_gtZero : - "valid_map ((accIdTok, money) # rest) \ - money > 0 \ - (\x tok. positiveMoneyInAccountOrNoAccount x tok ((accIdTok, money) # rest)) \ positiveMoneyInAccountOrNoAccount y tok2 rest" - apply (cases "accIdTok = (y, tok2)") - using positiveMoneyInAccountOrNoAccount_valid_zero apply auto[1] - using positiveMoneyInAccountOrNoAccount_sublist_gtZero_different by blast - lemma positiveMoneyInAccountOrNoAccount_gtZero_preservation : "valid_map ((accIdTok, money) # rest) \ (\x tok. positiveMoneyInAccountOrNoAccount x tok ((accIdTok, money) # rest)) \ positiveMoneyInAccountOrNoAccount y tok2 rest" diff --git a/isabelle/Core/QuiescentResult.thy b/isabelle/Core/QuiescentResult.thy index 51c9c162..c8bd6f0e 100644 --- a/isabelle/Core/QuiescentResult.thy +++ b/isabelle/Core/QuiescentResult.thy @@ -2,9 +2,6 @@ theory QuiescentResult imports Semantics PositiveAccounts begin -lemma reduceOne_onlyIfNonEmptyState : "refundOne acc = Some c \ acc \ []" - by auto - lemma reduceContractStepPayIsQuiescent : "(let moneyToPay = evalValue env sta x23 in if moneyToPay \ 0 then Reduced (ReduceNonPositivePay x21 x22 tok moneyToPay) ReduceNoPayment sta x24 @@ -149,7 +146,8 @@ lemma reductionLoop_reduce_monotonic : "reductionLoop True env sta cont wa ef = by simp done -lemma reduceContractUntilQuiescent_ifDifferentReduced : "reduceContractUntilQuiescent si sta cont = ContractQuiescent reduce wa ef sta newCont \ cont \ newCont \ reduce" +text "If we reduce the contract and the continuation has changed, then the reduced flag should be true" +theorem reduceContractUntilQuiescent_ifDifferentReduced : "reduceContractUntilQuiescent si sta cont = ContractQuiescent reduce wa ef sta newCont \ cont \ newCont \ reduce" apply (simp only:reduceContractUntilQuiescent.simps) apply (simp only:reductionLoop.simps) apply (cases "reduceContractStep si sta cont") diff --git a/isabelle/Core/SingleInputTransactions.thy b/isabelle/Core/SingleInputTransactions.thy index b51d85f2..c4100d22 100644 --- a/isabelle/Core/SingleInputTransactions.thy +++ b/isabelle/Core/SingleInputTransactions.thy @@ -1211,14 +1211,6 @@ lemma transactionPrefixForSingleInput : "h # t = traceListToSingleInput nt \interval = inte, inputs = inp_h # inp_t\ # t = traceListToSingleInput t2 \ inp_t \ [] \ False" - apply (induction t2 rule:traceListToSingleInput.induct) - apply simp_all - subgoal for si inps rest - apply (induction si inps rule:inputsToTransactions.induct) - by simp_all - done - fun isSingleInput :: "Transaction list \ bool" where "isSingleInput [] = True" | "isSingleInput (h # t) = (length (inputs h) \ 1 \ isSingleInput t)" diff --git a/isabelle/Core/ValidState.thy b/isabelle/Core/ValidState.thy index 8db6439a..c3cc45e5 100644 --- a/isabelle/Core/ValidState.thy +++ b/isabelle/Core/ValidState.thy @@ -6,14 +6,6 @@ lemma valid_state_valid_accounts : "valid_state state \ valid_ma apply (cases state) by simp -lemma valid_state_valid_choices : "valid_state state \ valid_map (choices state)" - apply (cases state) - by simp - -lemma valid_state_valid_boundValues : "valid_state state \ valid_map (boundValues state)" - apply (cases state) - by simp - lemma refundOne_preserves_valid_map_accounts : "valid_map oldAccounts \ refundOne oldAccounts = Some ((party, money), newAccounts) From 9b71e21c513d9e1fc0664a7cd2f95ad03da618c6 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Fri, 17 Mar 2023 11:51:33 -0300 Subject: [PATCH 22/24] Add changelog --- CHANGELOG.md | 21 +++++++++++++++++++++ isabelle/generated/Semantics.hs | 22 +++++++++++----------- 2 files changed, 32 insertions(+), 11 deletions(-) create mode 100644 CHANGELOG.md diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 00000000..b22ecb14 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,21 @@ +# Changelog + +# XXX 2023 - Marlowe specification version 3, (RC2 or final?) + +## Specification +- [PLT-4195](https://github.com/input-output-hk/marlowe/pull/161) - Change MoneyPreservation for AssetPreservation +- [PLT-3505](https://github.com/input-output-hk/marlowe/pull/168) - Several small fixes to the specification from the audit report +- [SCP-4869](https://github.com/input-output-hk/marlowe/pull/164) - Add lemma for DivValue rounding to zero +- [SCP-4908](https://github.com/input-output-hk/marlowe/pull/163) - Add Escrow to the contract examples + +## Test Spec +- [SCP-4860](https://github.com/input-output-hk/marlowe/pull/158) - Make tests reproducible +- [SCP-4698](https://github.com/input-output-hk/marlowe/pull/154) - Implement roundtrip test for all serialized types +- [SCP-4901](https://github.com/input-output-hk/marlowe/pull/160) - Add tests to EvalValue + +## General +- [SCP-4748](https://github.com/input-output-hk/marlowe/pull/155) - Fixed cabal packages. +- [SCP-4848](https://github.com/input-output-hk/marlowe/pull/156) - Fix problem with `edit-marlowe-proofs` command. + +# Dec 2022 - Marlowe specification version 3, RC1 +Version `v3-rc1` was tagged on commit `c8c67ad6892ec68842461d2e66b02ca87f93f70c` on 19 Dec 2022 and submitted to the auditors. This marks the begining of the changelog. \ No newline at end of file diff --git a/isabelle/generated/Semantics.hs b/isabelle/generated/Semantics.hs index a4417f64..506c8b21 100644 --- a/isabelle/generated/Semantics.hs +++ b/isabelle/generated/Semantics.hs @@ -544,7 +544,7 @@ applyCases env state (SemanticsTypes.IDeposit accId1 party1 tok1 amount) then let { warning = (if Arith.less_int Arith.zero_int amount then ApplyNoWarning - else ApplyNonPositiveDeposit party1 accId2 tok2 amount); + else ApplyNonPositiveDeposit party2 accId2 tok2 amount); newState = SemanticsTypes.accounts_update (\ _ -> @@ -618,8 +618,8 @@ applyAllLoop contractChanged env state contract inputs warnings payments = (payments ++ pays) curState cont; input : rest -> (case applyInput env curState input cont of { - Applied applyWarn newState conta -> - applyAllLoop True env newState conta rest + Applied applyWarn newState appliedCont -> + applyAllLoop True env newState appliedCont rest (warnings ++ convertReduceWarnings reduceWarns ++ convertApplyWarning applyWarn) @@ -806,14 +806,14 @@ calculateNonAmbiguousInterval n t (SemanticsTypes.When [] timeout tcont) = OptBoundTimeInterval.Unbounded) (calculateNonAmbiguousInterval n t tcont)); calculateNonAmbiguousInterval n t - (SemanticsTypes.When (SemanticsTypes.Case vb cont : tail) timeout tcont) = - (if gtIfNone n Arith.zero_int - then OptBoundTimeInterval.intersectInterval - (calculateNonAmbiguousInterval (subIfSome n Arith.one_int) t cont) - (calculateNonAmbiguousInterval n t - (SemanticsTypes.When tail timeout tcont)) - else calculateNonAmbiguousInterval n t - (SemanticsTypes.When tail timeout tcont)); + (SemanticsTypes.When (SemanticsTypes.Case vb cont : restCases) timeout tcont) + = (if gtIfNone n Arith.zero_int + then OptBoundTimeInterval.intersectInterval + (calculateNonAmbiguousInterval (subIfSome n Arith.one_int) t cont) + (calculateNonAmbiguousInterval n t + (SemanticsTypes.When restCases timeout tcont)) + else calculateNonAmbiguousInterval n t + (SemanticsTypes.When restCases timeout tcont)); calculateNonAmbiguousInterval n t (SemanticsTypes.Let vc vd c) = calculateNonAmbiguousInterval n t c; calculateNonAmbiguousInterval n t (SemanticsTypes.Assert ve c) = From 97fac7de1fd1fb285a82fb3803ab8017f7c23b92 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Thu, 23 Mar 2023 11:11:45 -0300 Subject: [PATCH 23/24] Update changelog --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index b22ecb14..c8c32ede 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ - [SCP-4860](https://github.com/input-output-hk/marlowe/pull/158) - Make tests reproducible - [SCP-4698](https://github.com/input-output-hk/marlowe/pull/154) - Implement roundtrip test for all serialized types - [SCP-4901](https://github.com/input-output-hk/marlowe/pull/160) - Add tests to EvalValue +- [PLT-4250](https://github.com/input-output-hk/marlowe/pull/170) - Add tests to EvalObservation ## General - [SCP-4748](https://github.com/input-output-hk/marlowe/pull/155) - Fixed cabal packages. From 0b0a1affdb1ba6cfcb0b4b85ae417670181c3ed3 Mon Sep 17 00:00:00 2001 From: Hernan Rajchert Date: Fri, 7 Apr 2023 11:58:10 -0300 Subject: [PATCH 24/24] Update changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index c8c32ede..4df9cf66 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,10 +13,12 @@ - [SCP-4698](https://github.com/input-output-hk/marlowe/pull/154) - Implement roundtrip test for all serialized types - [SCP-4901](https://github.com/input-output-hk/marlowe/pull/160) - Add tests to EvalValue - [PLT-4250](https://github.com/input-output-hk/marlowe/pull/170) - Add tests to EvalObservation +- [PLT-3313](https://github.com/input-output-hk/marlowe/pull/167) - Add Semiarbitrary instances and property based tests for some of Isabelle theorems ## General - [SCP-4748](https://github.com/input-output-hk/marlowe/pull/155) - Fixed cabal packages. - [SCP-4848](https://github.com/input-output-hk/marlowe/pull/156) - Fix problem with `edit-marlowe-proofs` command. +- [PR 175](https://github.com/input-output-hk/marlowe/pull/175) - Add version bounds to all libraries # Dec 2022 - Marlowe specification version 3, RC1 Version `v3-rc1` was tagged on commit `c8c67ad6892ec68842461d2e66b02ca87f93f70c` on 19 Dec 2022 and submitted to the auditors. This marks the begining of the changelog. \ No newline at end of file