Skip to content

SCP-4387 Re organize isabelle semantic types to become literal programming #134

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Sep 21, 2022
Merged

SCP-4387 Re organize isabelle semantic types to become literal programming #134

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
ff9b2ee
SCP-4388 replace PK for Address
hrajchert Sep 1, 2022
a77d83a
SCP-4387 re organize isabelle semantics types to become literate prog…
hrajchert Sep 3, 2022
0d1a15b
SCP-4387 Suggested changes to #134.
bwbush Sep 12, 2022
1c001cd
Merge pull request #136 from input-output-hk/bwbush/PR134-comments
hrajchert Sep 12, 2022
7668ce1
Applied Pablos PR feedback
hrajchert Sep 21, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 54 additions & 0 deletions isabelle/Core/BlockchainTypes.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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>
Copy link
Collaborator

@palas palas Sep 20, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is meant to be inclusive on both sides. Not sure about ledger or plutus, which last time I heard was inclusive on min and exclusive on max

Copy link
Collaborator Author

@hrajchert hrajchert Sep 21, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@bwbush do you know the answer to this?

type_synonym TimeInterval = "POSIXTime \<times> POSIXTime"

(*<*)
end
(*>*)
6 changes: 3 additions & 3 deletions isabelle/Core/MoneyPreservation.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down Expand Up @@ -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 :
Expand Down Expand Up @@ -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)
Expand Down
37 changes: 20 additions & 17 deletions isabelle/Core/Semantics.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 *)
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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"
Expand All @@ -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 =
Expand All @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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) =
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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)"

Expand All @@ -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
Expand All @@ -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" |
Expand Down
Loading