Merge pull request #134 from input-output-hk/hrajchert/scp-4387-liter…

…ate-programming

isabelle/Core/BlockchainTypes.thy

@@ -0,0 +1,54 @@
+(*<*)
+\<comment> \<open>This module defines the types we abstract from Blockchain specific implementation\<close>
+theory BlockchainTypes
+imports Main Util.Serialisation
+begin
+(*>*)
+
+section \<open>Blockchain agnostic \label{sec:blockchain-agnostic}\<close>
+
+text \<open>
+Marlowe is currently implemented on the Cardano Blockchain, but it is designed to be Blockchain agnostic.
+\<close>
+
+text \<open>
+Programs written in languages like Java and Python can be run on different architectures, like amd64 or arm64, because they have
+ interpreters and runtimes for them. In the same way, the Marlowe interpreter could be implemented to run on other blockchains,
+ like Ethereum, Solana for example.
+\<close>
+
+text \<open>
+We make the following assumptions on the underlying Blockchain that allow Marlowe Semantics to serve
+as a common abstraction:
+\<close>
+
+text \<open>
+In order to define the different \<^term>\<open>Token\<close>s that are used as currency in the participants accounts
+\secref{sec:internal-accounts}, deposits, and payments,
+ we need to be able to express a \<^term>\<open>TokenName\<close> and \<^term>\<open>CurrencySymbol\<close>.
+\<close>
+type_synonym TokenName = ByteString
+type_synonym CurrencySymbol = ByteString
+
+
+text \<open>To define a fixed participant in the contract \secref{sec:participants-roles-and-addresses}
+and to make payouts to them, we need to express an \<^term>\<open>Address\<close>.\<close>
+type_synonym Address = ByteString
+
+text \<open>In the context of this specification, these string types are opaque, and we don't enforce
+a particular encoding or format.\<close>
+
+text \<open>The \<^term>\<open>Timeout\<close>s that prevent us from waiting forever for external \<^term>\<open>Input\<close>s are represented
+by the number of milliseconds from the Unix Epoch \<^footnote>\<open>January 1st, 1970 at 00:00:00 UTC\<close>. \<close>
+type_synonym POSIXTime = int
+
+type_synonym Timeout = POSIXTime
+
+text \<open>The \<^term>\<open>TimeInterval\<close> that defines the validity of a transaction is a tuple of exclusive start
+and end time. \<close>
+\<comment> \<open>TODO: Check if exclusive or inclusive\<close>
+type_synonym TimeInterval = "POSIXTime \<times> POSIXTime"
+
+(*<*)
+end
+(*>*)

isabelle/Core/MoneyPreservation.thy

@@ -24,7 +24,7 @@ fun moneyInReduceStepResult :: "State \<Rightarrow> ReduceStepResult \<Rightarro
 "moneyInReduceStepResult state AmbiguousTimeIntervalReductionError = moneyInState state"
 
 fun moneyInRefundOneResult :: "Accounts \<Rightarrow>
-                               ((Party \<times> Token \<times> Money) \<times> Accounts) option \<Rightarrow> int" where
+                               ((Party \<times> Token \<times> int) \<times> Accounts) option \<Rightarrow> int" where
 "moneyInRefundOneResult accs None = moneyInAccounts accs" |
 "moneyInRefundOneResult _ (Some ((_, _, m), newAccs)) = m + moneyInAccounts newAccs"
 
@@ -419,7 +419,7 @@ lemma applyCases_preserves_money :
 lemma applyInput_preserves_money :
   "validAndPositive_state state \<Longrightarrow>
    moneyInState state + moneyInInput inp = moneyInApplyResult state inp (applyInput env state inp cont)"
-  apply (cases cont)                                                        
+  apply (cases cont)
   by (simp_all add:applyCases_preserves_money del:validAndPositive_state.simps moneyInState.simps)
 
 lemma reductionLoop_preserves_money_NoPayment_not_ReduceNoWarning :
@@ -566,7 +566,7 @@ lemma fixInterval_preserves_money :
 lemma computeTransaction_preserves_money :
   "validAndPositive_state state \<Longrightarrow>
    moneyInState state + moneyInInputs (inputs tra) = moneyInTransactionOutput state (inputs tra) (computeTransaction tra state contract)"
-  apply (simp only:computeTransaction.simps)    
+  apply (simp only:computeTransaction.simps)
   apply (cases "fixInterval (interval tra) state")
   subgoal for env fixSta
     apply (simp only:IntervalResult.simps Let_def)

isabelle/Core/Semantics.thy

@@ -1,5 +1,5 @@
 theory Semantics
-imports Main Util.MList Util.SList ListTools "HOL-Library.Product_Lexorder" SemanticsTypes
+imports Main Util.MList Util.SList ListTools "HOL-Library.Product_Lexorder" SemanticsTypes SemanticsGuarantees
 begin
 
 (* EVALUATION *)
@@ -84,10 +84,10 @@ lemma evalNegValue :
   by auto
 
 lemma evalAddCommutative :
-  "evalValue env sta (AddValue x y) = evalValue env sta (AddValue y x)" 
-  by auto 
+  "evalValue env sta (AddValue x y) = evalValue env sta (AddValue y x)"
+  by auto
 
-lemma evalAddAssoc : 
+lemma evalAddAssoc :
   "evalValue env sta (AddValue x (AddValue y z)) = evalValue env sta (AddValue (AddValue x y) z)"
   by auto
 
@@ -212,7 +212,7 @@ lemma evalDivCommutesWithNeg2 :
   by (smt (verit) div_minus_right)
 
 fun refundOne :: "Accounts \<Rightarrow>
-                  ((Party \<times> Token \<times> Money) \<times> Accounts) option" where
+                  ((Party \<times> Token \<times> int) \<times> Accounts) option" where
 "refundOne (((accId, tok), money)#rest) =
    (if money > 0 then Some ((accId, tok, money), rest) else refundOne rest)" |
 "refundOne [] = None"
@@ -224,23 +224,23 @@ lemma refundOneShortens : "refundOne acc = Some (c, nacc) \<Longrightarrow>
   by (metis Pair_inject length_Cons less_Suc_eq list.distinct(1)
             list.inject option.inject refundOne.elims)
 
-datatype Payment = Payment AccountId Payee Token Money
+datatype Payment = Payment AccountId Payee Token int
 
 datatype ReduceEffect = ReduceNoPayment
                       | ReduceWithPayment Payment
 
-fun moneyInAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> Accounts \<Rightarrow> Money" where
+fun moneyInAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> Accounts \<Rightarrow> int" where
 "moneyInAccount accId token accountsV = findWithDefault 0 (accId, token) accountsV"
 
-fun updateMoneyInAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> Money \<Rightarrow>
+fun updateMoneyInAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> int \<Rightarrow>
                              Accounts \<Rightarrow>
                              Accounts" where
 "updateMoneyInAccount accId token money accountsV =
   (if money \<le> 0
    then MList.delete (accId, token) accountsV
    else MList.insert (accId, token) money accountsV)"
 
-fun addMoneyToAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> Money \<Rightarrow>
+fun addMoneyToAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> int \<Rightarrow>
                           Accounts \<Rightarrow>
                           Accounts" where
 "addMoneyToAccount accId token money accountsV =
@@ -250,7 +250,7 @@ fun addMoneyToAccount :: "AccountId \<Rightarrow> Token \<Rightarrow> Money \<Ri
    then accountsV
    else updateMoneyInAccount accId token newBalance accountsV)"
 
-fun giveMoney :: "AccountId \<Rightarrow> Payee \<Rightarrow> Token \<Rightarrow> Money \<Rightarrow> Accounts \<Rightarrow>
+fun giveMoney :: "AccountId \<Rightarrow> Payee \<Rightarrow> Token \<Rightarrow> int \<Rightarrow> Accounts \<Rightarrow>
                   (ReduceEffect \<times> Accounts)" where
 "giveMoney accountId payee token money accountsV =
   (let newAccounts = case payee of
@@ -267,8 +267,8 @@ lemma giveMoneyIncOne : "giveMoney sa p t m a = (e, na) \<Longrightarrow> length
 (* REDUCE *)
 
 datatype ReduceWarning = ReduceNoWarning
-                       | ReduceNonPositivePay AccountId Payee Token Money
-                       | ReducePartialPay AccountId Payee Token Money Money
+                       | ReduceNonPositivePay AccountId Payee Token int
+                       | ReducePartialPay AccountId Payee Token int int
                        | ReduceShadowing ValueId int int
                        | ReduceAssertionFailed
 
@@ -492,6 +492,9 @@ datatype ApplyWarning = ApplyNoWarning
 datatype ApplyResult = Applied ApplyWarning State Contract
                      | ApplyNoMatchError
 
+fun inBounds :: "ChosenNum \<Rightarrow> Bound list \<Rightarrow> bool" where
+"inBounds num = any (\<lambda> (l, u) \<Rightarrow> num \<ge> l \<and> num \<le> u)"
+
 fun applyCases :: "Environment \<Rightarrow> State \<Rightarrow> Input \<Rightarrow> Case list \<Rightarrow> ApplyResult" where
 "applyCases env state (IDeposit accId1 party1 tok1 amount)
             (Cons (Case (Deposit accId2 party2 tok2 val) cont) rest) =
@@ -527,7 +530,7 @@ fun applyInput :: "Environment \<Rightarrow> State \<Rightarrow> Input \<Rightar
 
 datatype TransactionWarning = TransactionNonPositiveDeposit Party AccountId Token int
                             | TransactionNonPositivePay AccountId Payee Token int
-                            | TransactionPartialPay AccountId Payee Token Money Money
+                            | TransactionPartialPay AccountId Payee Token int int
                             | TransactionShadowing ValueId int int
                             | TransactionAssertionFailed
 
@@ -641,7 +644,7 @@ fun playTrace :: "POSIXTime \<Rightarrow> Contract \<Rightarrow> Transaction lis
 
 (* Extra functions *)
 
-type_synonym TransactionOutcomes = "(Party \<times> Money) list"
+type_synonym TransactionOutcomes = "(Party \<times> int) list"
 
 definition "emptyOutcome = (MList.empty :: TransactionOutcomes)"
 
@@ -651,7 +654,7 @@ lemma emptyOutcomeValid : "valid_map emptyOutcome"
 fun isEmptyOutcome :: "TransactionOutcomes \<Rightarrow> bool" where
 "isEmptyOutcome trOut = all (\<lambda> (x, y) \<Rightarrow> y = 0) trOut"
 
-fun addOutcome :: "Party \<Rightarrow> Money \<Rightarrow> TransactionOutcomes \<Rightarrow> TransactionOutcomes" where
+fun addOutcome :: "Party \<Rightarrow> int \<Rightarrow> TransactionOutcomes \<Rightarrow> TransactionOutcomes" where
 "addOutcome party diffValue trOut =
    (let newValue = case MList.lookup party trOut of
                      Some value \<Rightarrow> value + diffValue
@@ -661,13 +664,13 @@ fun addOutcome :: "Party \<Rightarrow> Money \<Rightarrow> TransactionOutcomes \
 fun combineOutcomes :: "TransactionOutcomes \<Rightarrow> TransactionOutcomes \<Rightarrow> TransactionOutcomes" where
 "combineOutcomes x y = MList.unionWith plus x y"
 
-fun getPartiesFromReduceEffect :: "ReduceEffect list \<Rightarrow> (Party \<times> Token \<times> Money) list" where
+fun getPartiesFromReduceEffect :: "ReduceEffect list \<Rightarrow> (Party \<times> Token \<times> int) list" where
 "getPartiesFromReduceEffect (Cons (ReduceWithPayment (Payment src (Party p) tok m)) t) =
    Cons (p, tok, -m) (getPartiesFromReduceEffect t)" |
 "getPartiesFromReduceEffect (Cons x t) = getPartiesFromReduceEffect t" |
 "getPartiesFromReduceEffect Nil = Nil"
 
-fun getPartiesFromInput :: "Input list \<Rightarrow> (Party \<times> Token \<times> Money) list" where
+fun getPartiesFromInput :: "Input list \<Rightarrow> (Party \<times> Token \<times> int) list" where
 "getPartiesFromInput (Cons (IDeposit _ p tok m) t) =
    Cons (p, tok, m) (getPartiesFromInput t)" |
 "getPartiesFromInput (Cons x t) = getPartiesFromInput t" |