Object oriented smart contracts for UTXO-based blockchains

Abstract

Disclosed is method and system for turning existing object-oriented programming languages into smart contract languages without introducing new syntactic features. The invented method and system provide a protocol that enables storing a history of computations on a decentralized computer network, such as UTXO-based blockchain system, for any object-oriented computer language. The invented method and system further provide for storing and updating data on blockchains, where such blockchains may be used in cryptocurrency applications and for smart contracts.

Claims

1. A method comprising: generating, by a processor, an instruction in a first object-oriented computer language for operating in a decentralized computer network from an instruction in a second object-oriented computer language that can operate on a local computer, where a semantic of the second object-oriented computer language can be expressed by a rule so, S, E, ├e: v, S′ with - denoting a semantic relation, the rule meaning that in a context where a variable self refers to an object so, where a data store on the local computer is S, and where an execution environment is E, an expression e evaluates to an object v at a second data store S′ in the local computer; and replacing, by the processor, a local storage update command S[v/l], which updates at least one location l by the object v, by a command to broadcast to the decentralized computer network at least one transaction that spends at least one unspent-transaction-output corresponding to the location 1 into a new output that stores at least one of (i) the object v and (ii) information enabling the object v to be determined; wherein the generated instruction in the first object-oriented computer language enables operation of a smart contract.

2. The method of claim 1, wherein the generated instruction in the first object-oriented computer language is a storage-update instruction, and wherein the storage-update instruction either immediately precedes a recursive call to a first semantic relation or is located at an end of a body of the rule expressed in the second object-oriented computer language.

3. The method of claim 1, wherein the generated instruction in the first object-oriented computer language is an instruction for storing a data structure D at an unspent memory location OUT on the decentralized computer network, the data structure D further including a data structure D, where the data structure D′ further includes a data structure D′ the method further comprising: (a) receiving, at the local computer, a request to store the data structure D at an unspent memory location OUT on the decentralized computer network; (b) creating, at the local computer, a request TX to the decentralized computer network, to spend the unspent memory location OUT and to generate a new unspent memory location OUT′ on the decentralized computer network; (c) using the local computer to sign and broadcast the request TX to the decentralized computer network; (d) receiving the request TX at the decentralized computer network; (e) using the decentralized computer network to determine validity of the request TX according to a protocol of the decentralized computer network; and (f) if the request TX is determined to be valid, performing the steps of (i) spending the unspent memory location OUT on the decentralized computer network and generating the new unspent memory locations OUT′ on the decentralized computer network; and (ii) repeating steps (a) through (f)(i) above while using the data structure D′ in place of the data structure D and while using the memory location OUT′ in place of the memory location OUT.

4. The method of claim 1, wherein the decentralized computer network is an unspent-transaction-outputs blockchain.

5. The method of claim 1, wherein a source code of a program written in one of the first computer language and the second computer language is stored in a transaction.

6. The method of claim 5, where the transaction represents object creation.

7. A computer system comprising a local computer, the local computer comprising: a) a memory for storing computer instructions and data; and b) a processor operatively coupled to the memory, the processor executes the instructions to cause the local computer performing: generating an instruction in a first object-oriented computer language for operating in a decentralized computer network from an instruction in a second object-oriented computer language that can operate on the local computer, where a semantic of the second object-oriented computer language can be expressed by a rule so, S, E, ├e: v, S′, with - denoting a semantic relation, the rule meaning that in a context where a variable self refers to an object so, where a data store on the local computer is S, and where an execution environment is E, an expression e evaluates to an object v at a second data store S′ in the local computer; and replacing a centralized storage update command S[v/l], which updates at least one location l by the object v, by a command to broadcast to the decentralized computer network at least one transaction that spends at least one unspent-transaction-output corresponding to the location l into a new output that stores at least one of (i) the object v and (ii) information enabling the object v to be determined; wherein the generated instruction in the first object-oriented computer language enables operation of a smart contract.

8. The computer system of claim 7, wherein the decentralized computer network is an unspent-transaction-outputs blockchain.

9. The computer system of claim 7, wherein the generated instruction in the first object-oriented computer language is an instruction for storing a data structure D at an unspent memory location OUT on the decentralized computer network, the data structure D further including a data structure D′, wherein the data structure D′ further includes a data structure D″; and (a) wherein the local computer is configured to receive a request to store the data structure D at the unspent memory location OUT on the decentralized computer network; (b) wherein the local computer is configured to create a request TX to spend the unspent memory location OUT and to generate a new unspent memory location OUT′ on the decentralized computer network; (c) wherein the local computer is configured to enable signing and broadcasting the request TX to the decentralized computer network; (d) wherein the decentralized computer network is configured to receive the request TX; (e) wherein the decentralized computer network is configured to enable determining validity of the request TX according to a protocol of the decentralized computer network; and (f) if said request TX is determined to be valid, (i) the decentralized computer network further configured to spend the unspent memory location OUT on the decentralized computer network and to generate the new unspent memory location OUT′ on the decentralized computer network; and (ii) wherein the computer system is configured to repeat operations (a) through (f)(i) above while using the data structure D′ in place of the data structure D and while using the memory location OUT′ in place of the memory location OUT.

10. The computer system of claim 7, wherein a source code of a program written in one of the first computer language and the second computer language is stored in a transaction that represents object creation.

Description

BRIEF DESCRIPTION OF THE FIGURES

(1) The accompanying figures, where like reference numerals refer to identical or functionally similar elements throughout the separate views, together with the detailed description below, are incorporated in and form part of the specification, and serve to further illustrate embodiments of concepts that include the claimed invention and explain various principles and advantages of those embodiments.

(2) FIG. 1 is a computer system in accordance with some embodiments of the present invention.

(3) FIG. 2 shows a computer on a decentralized computer network in accordance with some embodiments of the present invention.

(4) FIG. 3 is a diagram of the transactions that are broadcast when a location in the store of the decentralized computer is updated.

(5) FIG. 4 is a diagram of the transactions that are broadcast when a variable assignment Id<−e is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(6) FIG. 5 is a diagram of the transactions that are broadcast when an expression of the form let Id: T<−e in e′ is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(7) FIG. 6 is a diagram of the transactions that are broadcast when an expression of the form new A is evaluated in semantics in accordance with some embodiments of the present invention.

(8) FIG. 7 is a diagram of the transactions that are broadcast when an expression of the form e.sub.0, f(e.sub.1, . . . , e.sub.n) is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(9) FIG. 8 is a diagram of the transactions that are broadcast when an expression let x<−1 in y<−2 in x<−y is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(10) FIG. 9 is a diagram of the transactions that are broadcast when an expression new A is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(11) FIG. 10 is a diagram of the transactions that are broadcast when an expression new B is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(12) FIG. 11 is a diagram of the transactions that are broadcast when an expression let c<−new Counter in a.inc(1) is evaluated in a blockchain semantics in accordance with some embodiments of the present invention.

(13) FIG. 12 is a diagram of a transaction context in accordance with some embodiments of the present invention.

(14) FIG. 13 is a diagram of a process of plugging a context into a hole in accordance with some embodiments of the present invention.

(15) FIG. 14 is a diagram of a process of plugging an empty context into a hole in accordance with some embodiments of the present invention.

(16) FIG. 15 is a diagram of context [Ctx-Assign] for semantic rule [B-Assign] of a blockchain semantics in accordance with some embodiments of the present invention.

(17) FIG. 16 is a diagram of context [Ctx-New] for semantic rule [B-New] of a blockchain semantics in accordance with some embodiments of the present invention.

(18) FIG. 17 is a diagram of context [Ctx-Let] for semantic rule [B-Let] of a blockchain semantics in accordance with some embodiments of the present invention.

(19) FIG. 18 is a diagram of context [Ctx-Dispatch] for semantic rule [B-Dispatch] of a blockchain semantics in accordance with some embodiments of the present invention.

(20) Skilled artisans will appreciate that elements in the figures are illustrated for simplicity and clarity. The apparatus and method components have been represented where appropriate by conventional symbols in the drawings, showing only those specific details that are pertinent to understanding the embodiments of the present invention so as not to obscure the disclosure with details that will be readily apparent to those of ordinary skill in the art having the benefit of the description herein.

DETAILED DESCRIPTION

(21) The following detailed description discloses some embodiments of the present invention. A person skilled in the art, however, will understand that the present invention in not limited to the specific disclosed embodiments, and that other embodiments are within the scope of the present invention.

(22) Although the present invention can work with any object-oriented programing language, one exemplary embodiment implements the invention using a UXTO-type blockchain and a simple object-oriented language called Classroom Object-Oriented Language (“COOL”).

(23) A UXTO-based cryptocurrency has two elements: a data structure called a blockchain and a consensus algorithm that is used to update the blockchain. The present invention is independent of the consensus algorithm used and can operate on all UTXO-based blockchains regardless of the consensus protocol used.

(24) In one embodiment of the present invention, a blockchain B includes a set of transactions (requests issued to a distributed computer network), where a transaction consists of a list of inputs ins and a list of outputs outs. Each transaction (request) tx and each output out in a blockchain B has a unique identifier denoted by Id(tx, B) and Id(out, B), respectively. Given an identifier id of an object, B(id) denotes the object in the blockchain B, therefore B(Id(tx, B))=tx and B(Id(out, B))=out.

(25) Below is an exemplary expression for a transaction tx having a number of inputs ins and outputs outs.

(26) TABLE-US-00001 tx = {  ins: [ { old.sub.1, ?params.sub.1 }, ..., { old.sub.n, ?params.sub.n } ]  outs [ { condition.sub.1, amount.sub.1, ?data.sub.1 }, ... { condition.sub.m, amount.sub.m, ?data.sub.m } ] }

(27) An input in B stores the id of an output in B in a field called old.sub.i and may also store an array of parameters in a filed called params. A transaction tx is considered signed if each one of its inputs contains an array of parameters; considered partially signed if some inputs have parameters; and considered unsigned if no input contains parameters. Given a transaction tx, copy(tx) denotes the unsigned transaction that is obtained from tx by removing all parameters from the transaction's inputs.

(28) An output includes a function condition that maps parameters to a Boolean, a number of coins called amount, and optionally some data.

(29) A partial function that maps a transaction and an n-ary spending condition to an array of n−1 parameters may be referred to as a wallet W. W can sign an input {old: B(out)} of a transaction tx if copy(tx) and the condition c.sub.out of the output out that is being spent are in the domain of W. For example, sign.sub.W(tx) denotes the transaction obtained from tx by replacing every unsigned input {old: B(out)} that W can sign by {old: B(out), params: W(copy(tx), c.sub.out)}.

(30) For example, the expression below describes the process of signing a transaction tx, in which a wallet W can sign the first but not the second input of tx. The first input of tx references an output out.sub.0 with spending condition c. The unsigned transaction copy(tx) is obtained from tx by removing a parameter sig from the second input. sign.sub.W(tx) has sig added back as the parameter of the second input and W(copy(tx), c) is added as the parameter of the first input.

(31) TABLE-US-00002 out.sub.0 = { amount: . . . , condition: c } tx.sub.0 = { ins: . . . , outs: [out.sub.0] } tx = { ins: [ { old: Id(out.sub.0, B) }, { old: . . . , params: [sig] } ], outs: . . . } copy(tx) = { ins: [ { old: Id(out.sub.0, B) }, { old: . . . } ], outs: . . . } signw(tx) = {  ins: [ { outId: Id(out.sub.0, B), params: W(copy(tx), c) },  { old: . . . , params: [sig] } ],  outs: . . . }

(32) We can say that input in “spends” output out if in includes a reference to out. We can also say that a transaction tx “spends” an output out if the out is spent by an input of tx. We can say that a wallet W can “spend” from an output out with condition c if there is a transaction tx such that

(33) $c\left(\mathrm{copy}\left(\mathrm{tx}\right),W\left(\mathrm{copy}\left(\mathrm{tx}\right),c\right)\right)=\mathrm{true}$

(34) A blockchain B is valid if: 1. Every transaction tx in B is fully signed and has a unique id Id(tx, B). 2. If {old: o, params: p} is an input in B, then B contains an output out such that B(o)=out. 3. If {old: o.sub.1, params: p.sub.1} and {old.: o.sub.2, params: p.sub.2} are distinct inputs in B, then o.sub.1≠o.sub.2. 4. If {old: o, params: p} is an input in B, then copy(tx) and p satisfy the condition B(o). 5. If a transaction tx in B has at least one input, then the sum of coins in the outputs of tx is not greater than the sum of coins in the outputs spent by tx.

(35) A wallet can broadcast a unsigned transaction tx to a blockchain B if the expression B∪{sign.sub.W(TX)} is valid.

(36) A transaction with no inputs is called a coinbase transaction. Such a transaction creates new coins. Note that according to the definition in one preferred embodiment, any coinbase transaction is valid in any blockchain.

(37) In real world blockchains, only distinguished users called miners are permitted to broadcast coinbase transactions.

(38) In addition, the consensus protocol may impose further constraints on how frequently coinbase transactions can occur and how many coins they can create. Below is an example of a payment system that can be implemented using a blockchain of the present invention.

(39) Let (gen, sign, verify) be a digital signature scheme. Let (pubKey, privKey) be a private-public key pair generated by gen( ). A transaction TX.sub.0 that has one output out with a condition c that maps (x, y) to verify(x, pubKey, y). Let W be a wallet that maps (copy(tx), c) to [privkey, sign(privKey, copy(tx))] for every transaction tx.

(40) $ou{t}_0=\left\{\mathrm{condition}\text{:}\left(x,y\right)=\text{>}\mathrm{verify}\left(x,\mathrm{pubKey},y\right),\mathrm{amount}\text{:}a\right\}$${\mathrm{tx}}_0=\left\{\mathrm{ins}\text{:}\mathrm{.Math.},\mathrm{outs}\text{:}\left[\mathrm{ou}{t}_0\right]\right\}$$\mathrm{tx}=\{\mathrm{ins}\text{:}\left[\left\{\mathrm{outId}\text{:}{\mathrm{Id}}_B\left(ou{t}_0\right)\right\}\right],\mathrm{outs}\text{:}\mathrm{.Math.}\}$$\mathrm{copy}\left(\mathrm{tx}\right)=\mathrm{tx}$${\mathrm{sign}}_w\left(\mathrm{tx}\right)=\{\mathrm{ins}\text{:}\left[\left\{\mathrm{outId}\text{:}\mathrm{Id}\left({\mathrm{out}}_{0}B\right),\mathrm{params}\text{:}\left[\mathrm{privKey},\mathrm{sign}\left(\mathrm{privKey},\mathrm{copy}\left(\mathrm{tx}\right)\right)\right]\right\}\right],\mathrm{outs}\text{:}\mathrm{.Math.}\}$

(41) Because the expression below is true, tx is a witness that W can spend the output tx.sub.0. c(copy(tx), W(copy(tx), c))=c(copy(tx), sign(privKey, copy(tx)))=verify(copy(tx), pubKey, sign(privKey, copy(tx)))=true

(42) Although the present invention can operate with any object-oriented programming language, in one preferred embodiment, the present invention will be described in the context of the COOL programming language. COOL is a statically typed object-oriented language with a formally defined syntax and semantics that are described in “The Cool Reference Manual,” which was authored by Alex Aiken in 1995, and the contents of which are hereby incorporated in full by reference. The syntax of Cool is similar to the syntax of existing object-oriented programming languages like Java or Javascript.

(43) Cool programs are sets of classes written is a syntax that is similar to existing object-oriented programming languages like Java or Javascript. For every program P, there are two functions that can be computed from the source code of P: the function class returns the attributes, types and initializations for a given class:

(44) $\begin{array}{cc}\mathrm{class}\left(X\right)=\left(a_i\text{:}{T}_1\leftarrow e_i,\mathrm{.Math.},a_n\text{:}{T}_n\leftarrow e_n\right)& \end{array}$
The function implementation returns the parameters and body of a given method in a class:

(45) $\mathrm{implementation}\left(X,m\right)=\left(x_1,...,x_n,e_{body}\right)$

(46) Most constructs in Cool are expressions and every expression has a value. The basic expressions in Cool are integer constants like 1, 2, 3, strings like ‘hello’, and the Boolean values true and false. All values are objects in Cool. Values are defined with respect to a set of identifiers Ids and a set of locations Loc. Identifiers are atomic syntactic objects that can be used as variables. There are also special identifiers, like self. The values with identifiers Ids and locations in Loc (denoted Val.sub.lds, Loc) is the set containing void, Bool(b) for b∈{true, false}, Int(n) for integer n, String(l, s) for string s of length l, and elements of the form C(a.sub.1=loc.sub.1, . . . , a.sub.n=loc.sub.n) where C is a class name, a.sub.1, . . . , a.sub.n∈Ids, and loc.sub.1, . . . , loc.sub.n∈Loc.

(47) Each value in Cool has a type. The type of integer constant x in Int and its value in Int(x), and the same notion is used to strings and Booleans. The type of object C(a=1) is C. Each type has a default value: the default Dint of Int is 0, and the default of D.sub.string is String is the empty string”, the default of D.sub.Bool of Bool is false, and the default of any other type is void.

(48) As mentioned above, the set of Ids of identifies in a program always incudes a special variable self that refers to the object on which a method was dispatched. We write Val instead of Val.sub.ids, Loc when the set of ids and the set of locations are clear from the context.

(49) The semantics of Cool is defined with respect to a partial function called environment E: Ids->Loc and a partial function called store S: Loc->Val. The operational semantics of Cool is defined by rules of the form so, S, E, e: v, S′
where so is an object, E is an environment, S and S′ are stores, e is an expression, and v is value. The rule reads: In the context where the special variable self refers to the object so, the store is S, and the environment is E, the expression e evaluates to value v and the new store is S′.

(50) Changes to the store and environment will be denoted using the following notations: Given a function F: D->R and elements d, d′∈D and r∈R, we provide F[r/d] to be a function such that R[r/d](d′)=r if d=d′ and F[r/d](d′)=F(d′) otherwise. To allocate memory, we need a way to obtain a new location from a store. Thus, we provide newloc(S) to be a function that returns a location l∈Loc for a given store S, such that l is not in the domain of S.

(51) The semantic rules of Cool that are relevant here are discussed below (the other rules can be found in Section 13 of the Cool manual, which is incorporated herein in its entirety). For the examples below, we fix an environment E and a store S1.

Variable Assignment

(52) The first step when evaluating Id←e in so, S.sub.1, E, as disclosed above is to evaluate expression e to obtain its value v. The side effect of the evaluation is that the store S.sub.1 is updated to a store S.sub.2, however, S.sub.2 might be identical to S.sub.1. Next, the location E(Id) of Id is looked up in the environment. Finally, the store S.sub.2 is updated to store value vat location l. The semantics rule [Assign] of the Cool semantics is shown below.

(53) TABLE-US-00003 [Assign] so, S.sub.1, E ├ e: v, S.sub.2 E(Id) = I S.sub.3 = S.sub.2[v/I]  −−−−−−−−−- so, S.sub.1, E ├ Id ← e: v, S.sub.3

Variable Definition

(54) When an assignment let Id: T1←e.sub.1 in e.sub.2 is evaluated in so, S.sub.1, E, the expression e.sub.1 is evaluated to value v.sub.1. Then a new location l is obtained S.sub.2, and the value v.sub.1 is stored at location l. Finally, the expression e.sub.2 is evaluated in the environment E′=E[l/id].

(55) TABLE-US-00004 [Let] so, S.sub.1, E ├ e: v, S.sub.2 I= newloc (S.sub.2) S.sub.3 = S.sub.2[v/I] E′ = E[I/Id] so, S.sub.3, E′ ├ e′: v′, S.sub.4  ------------------------------------ so, S1, E ├ let Id: T ← e in e′: v′, S.sub.4

Object Construction

(56) When an expression new A is evaluated, the class A.sub.o to be constructed is determined (details of SELF_TYPE can be found in section 4.1 of the Cool manual, which is incorporated herein in its entirety). Next, distinct new locations li are obtained from S.sub.1 for every attribute a.sub.i: T.sub.i of A and l<=i<=n. Location l.sub.i in initialized to the default for type A.sub.i. Finally, the expression a.sub.1←e.sub.1; . . . ;a.sub.n←e.sub.n; is evaluated in an environment that contains the locations that store the attributes of A.sub.o.

(57) TABLE-US-00005 [New] A.sub.0= X if A = SELF_TYPE and so=X(. . .); and A.sub.0 = A otherwise class (A.sub.0) = (a.sub.1: A.sub.1 ← e.sub.1, . . . , a.sub.n: A.sub.n ← e.sub.n) I.sub.i= newloc(S.sub.1), for i = 1 . . . , n and each I.sub.i is distinct V.sub.1 = A.sub.0(a.sub.1 = I.sub.1, . . . , a.sub.n= I.sub.n) S.sub.2 = S.sub.1[D.sub.A_.sub.1/I.sub.1, . . . , D.sub.A_.sub.n/I.sub.n] v.sub.1, S.sub.2, [a.sub.1: I.sub.1, . . . , a.sub.n: I.sub.n] ├ {a.sub.1 ← e.sub.1; . . . ; a.sub.n ← e.sub.n;}: v.sub.2, S.sub.3  — — — — — — — — — -   ---------------  ----------- so, S.sub.1, E ├ new A: v.sub.1, S.sub.3

Method Dispatch

(58) When an expression e.sub.o.Math.f(e.sub.1, . . . , e.sub.n) is evaluated in the Cool semantics, the expressions e.sub.1, . . . , e.sub.n that are passed as parameters are evaluated to the values v.sub.1, . . . , v.sub.n, respectively. Then expression e.sub.o is evaluated to value v.sub.o. Then one new location l.sub.x_i is created and initialized to store v.sub.i for l<=i<=n. Then the body e.sub.n+1 of the method f is evaluated in an environment that contains the locations storing the attributes of the object v.sub.o on which the function was called, as well as the locations l.sub.x_1, . . . , l.sub.x_n that store the values of the parameters.

(59) TABLE-US-00006 [Dispatch] so, S.sub.1, E ├ e.sub.1: v.sub.1, S.sub.2 so, S.sub.2, E ├ e.sub.2: v.sub.2, S.sub.3 . . . so, S.sub.n, E ├ e.sub.n: v.sub.n, S.sub.n+1 so, S.sub.n+1, E ├ e.sub.0: v.sub.0, S.sub.n+2 A(a.sub.1 = I.sub.a_1, . . . a.sub.m = I.sub.a_m) = V.sub.0 (x.sub.1, . . . , x.sub.n, e.sub.n+1) = implementation(A, f) I.sub.x_i = newloc(S.sub.n+2), for i=1 . . . n and each I.sub.x_i is distinct S.sub.n+3 = S.sub.n+2[v.sub.1/I.sub.x_1, . . . v.sub.n/I.sub.x_n] v.sub.0, S.sub.n+3, [a.sub.1: I.sub.a_1, . . . a.sub.m: I.sub.a_m, x.sub.1: I.sub.x_1, . . . , x.sub.n: I.sub.x_n] ├ e.sub.n+1: v.sub.n+1, S.sub.n+4 so, S.sub.1, E ├ e.sub.0.f(e.sub.1, . . . ,e.sub.n): v.sub.n+1, S.sub.n+4

(60) As mentioned above, the present invention can convert any object-oriented programming language into a smart contract version of that language. One embodiment of the invention described below converts the Cool programming language into a smart contract version of Cool, which will be referred to BCool programming language.

BCool

(61) The syntax of an exemplary programming language, BCool, is identical to the syntax of Cool. Before we disclose the semantics for BCool, however, we fix some notation. Let tx be a transaction with inputs [in.sub.1, . . . , in.sub.n] and outputs [out.sub.1, . . . , out.sub.n]. An output out, for which n<l<=m is called a b-location. If i<min(n, m), then out; is a successor of the output out and is spent by in.sub.i. In this case, out is a predecessor of out.sub.i. An output out is a revision if its predecessor is a b-location or a revision. Output out is the latest revision of output out′ if there are outputs out.sub.1, . . . , out.sub.n such that out′=out.sub.1, out.sub.i is the predecessor of out.sub.i+1 for all l<=i<n, out.sub.n=out, and out is unspent.

(62) We provide two functions that compute the revision and genesis for a given output.

(63) $\mathrm{rev}\left(\mathrm{out},B\right)=\mathrm{out}\mathrm{if}\mathrm{out}\mathrm{is}\mathrm{unspent}$$\mathrm{rev}\left(\mathrm{out},B\right)=\mathrm{rev}\left({\mathrm{out}}^{\prime },B\right)\mathrm{if}\mathrm{out}\mathrm{has}a\mathrm{successor}{\mathrm{out}}^{\prime }$$\mathrm{rev}\left(\mathrm{out},B\right)=\mathrm{undefined}\mathrm{otherwise}$$\mathrm{loc}\left(\mathrm{out},B\right)=\mathrm{out}\mathrm{if}\mathrm{out}\mathrm{is}ab\text{-}\mathrm{location}$$\mathrm{loc}\left(\mathrm{out},B\right)=\mathrm{loc}\left({\mathrm{out}}^{\prime },B\right)\mathrm{if}\mathrm{out}\mathrm{has}a\mathrm{predecessor}{\mathrm{out}}^{\prime }$$\mathrm{loc}\left(\mathrm{out},B\right)=\mathrm{undefined}\mathrm{otherwise}$

(64) This process is shown in FIG. 3. Specifically FIG. 3 is a diagram of the transactions that are broadcast when a location in the store of the decentralized computer is updated.

(65) Values in BCool, analogous to Cool, are either of a basic type (String, Number, Boolean), void, or of the form C(a.sub.1=l.sub.1, . . . , a.sub.n=l.sub.n) where C is a class name, a.sub.1, . . . , a.sub.n are the attributes of C and l.sub.1, . . . , l.sub.n are b-locations.

Semantics of Bcool

(66) Let B be a blockchain. A blockchain environment E for B is a mapping from identifiers to b-locations in B. The semantic rules of BCool are of the form so, B, E e: v, B′

(67) where so is a value, B and B′ are blockchains such that B⊂B′, E is a blockchain environment, e is an expression, and v is a value with b-locations in B.

(68) One key distinguishing feature of the present invention, reflected in the exemplary language, BCool, is that it uses a blockchain instead of a store. Whenever and expression e is evaluated, a (possibly empty) set Te of transactions is broadcast to the blockchain. The BCool semantics uses distinguished outputs called b-locations that correspond to the locations in the Cool semantics. When a location loc is uploaded in Cool, the BCool semantics broadcast a transaction that spends the latest revision of the corresponding b-location into a successor that stores the new value.

(69) We fix some notations for denoting reads from and writes to a blockchain. Let B be a blockchain and out an output in B. We provide B(out) to be the value stored at the latest revision of output out, that is B(out)=v if rev(out) is of the form {data: {val: v}} and B(out) is undefined otherwise.

(70) Writes are facilitated as follows. Let B be a blockchain, R={l.sub.1, . . . , l.sub.n} a set of b-locations in B, and U={l′.sub.1->v.sub.1, . . . , l′.sub.m->v.sub.m} a mapping from b-locations in B to values such that {l.sub.1, . . . l.sub.n} and {l′.sub.1, . . . , l′.sub.m} are disjoint. We provide tx(B, U, R) to be a transaction that spends each location l′.sub.i with l<=i<=m into a successor that stores the value v.sub.i; tx(B, U, R) also spends the latest revision of each b-location l.sub.i with 1<=i 21 =n into a successor that stores the value stored at b-location l.sub.i in B:

(71) TABLE-US-00007 tx(B,U,R) = {  ins: [   { old: rev(I.sub.1, B) }, . . . , { old: rev(I.sub.n, B) },   { old: rev(I′.sub.1, B) }, . . . , { old: rev(I′.sub.m, B) },  ]  outs: [   { data: { val: B(I.sub.1) } }, . . . , { data: { val: B(I.sub.n) } },   { data: { val: v.sub.1 }}, . . . ,{ data: { val: v.sub.m } },  ] }

(72) Given tx(B, U, R), an expression e, we provide tx(B, U, R, e) to be the transactions obtained from tx(B, U, R) by adding expression e to the data of the first output.

(73) Given blockchain B we provide b-newloc(B) to be a function that returns an unspent b-location from B. An unspent b-location can be generated by broadcasting a transaction with more outputs than inputs, so we assume that B contains sufficiently many unspent b-locations to perform a computation.

(74) Given a blockchain environment E=[a.sub.1: l.sub.1, . . . , a.sub.n: l.sub.n] we denote by loc(E) the set of b-locations {l.sub.1, . . . , l.sub.n} that occur in E. Similarly, given value v=(a.sub.1=l.sub.1, . . . , a.sub.n: l.sub.n) we denote by loc(E) the set {l.sub.1, . . . , l.sub.n}.

Semantic Rules

(75) Given a store S and a set of locations L we provide inset(S, L) to be the set of locations in S that can reach a location in L in the object graph. Note that L is contained in inset(S, L).

(76) The semantic rules of BCool can be obtained from the semantic rules of Cool in a mechanical way. BCool has one rule [B-R] that is obtained from the rule [R] of Cool as follows: Replace every symbol ├ for semantic relation of Cool with for semantic relation of BCool Replace every symbol Si denoting a centralized storage with a symbol Bi denoting a decentralized storage (blockchain) Either before or after the store-update replacing step below, ensure that store updates always immediately precede recursive calls or are at the end of a rule body Replace every store update Si[v.sub.1/I.sub.1, . . . , v.sub.n/l.sub.n] in the body of a rule for so, S, E, ├e: v, S′ by an update that adds a transaction tx(B.sub.i, [v.sub.1/l.sub.1 . . . v.sub.n/l.sub.n], loc(E)∪loc(so)∪inset(Si, {l.sub.1 . . . l.sub.n})\{l.sub.1 . . . l.sub.n}, {e, E, loc(so)}). In other words, replace every store update S.sub.i[v/l] that updates at least one location l in S.sub.i by value v, by the instruction to broadcast one or more transactions to the blockchain that spend at least one unspent-transaction-output (“utxo”) corresponding to location l into a new output that stores a value v (or stores other meta information that allow v to be computed) and spend at least one additional utxo corresponding to a location in the current execution environment E (also referred to as stack frames) into a new output that stores the same value as its predecessor. In another embodiment, every store update Si[v.sub.1/l.sub.1, . . . v.sub.n/l.sub.n] in the body of the rule for so, S, E ├e: v, S′ by a blockchain update that adds a transaction tx(B.sub.i, [v.sub.1/l.sub.1 . . . v.sub.n/l.sub.n], loc(E)∪loc(so) ∪inset(Si, {l.sub.1 . . . l.sub.n})\{l.sub.1 . . . l.sub.n}, {e, E, loc(so)}). Note, the first to bullets merely rewrite the symbols for notation convenience, as the symbol B.sub.i in the added transaction could be written as S.sub.i.

(77) The rewriting is trivial for rules that do not change the store. Therefore we omit the BCool rules that correspond (letter for letter) to the following Cool rules that do not change the store: [Var], [self], [True], [False], [Int], [String], [If-True], [If-False], [Sequence], [Loop-True], [Loop-False], [IsVoid-True], [IsVoid-False], [Not], [Comp], [Neg], [Arith].

(78) The rules of the Cool semantics that change the store are [Assign], [Let], [New], [Dispatch], and [StaticDispatch]. Below we explain the rewritings of the first four rules in detail. We omit the rewriting of the rule [StaticDispatch] because it is almost exactly like the rule [Dispatch].

B-Assign

(79) The semantic rule for variable assignment in BCool is as follows:

(80) TABLE-US-00008 so, B.sub.1, E  e: v, B.sub.2 E(Id) = I B.sub.3 = B.sub.2 ∪ { tx(B.sub.2, [v/I], loc(E) ∪ loc(so) \ { I }, Id ← e) } ----------------------------------------------------------- so, B.sub.1, E  Id ← e: v, B.sub.3

(81) FIG. 4 shows the evaluation of Id←e with respect to object so, blockchain B.sub.1, and environment E. In the figure, innermost boxes are either outputs or locations. Outputs are designated as out.sub.i, out′.sub.i, or out″.sub.i for some number i. Locations are designated with the letter l. The top most box labelled B1 represents a set of transactions containing the outputs inside the box labelled B.sub.1. Assume that l.sub.1, . . . , ln, l are the b-locations that occur in either E or so, and that out.sub.1, . . . , out.sub.n, out are the revisions of l.sub.1, . . . , ln, l in B.sub.1 respectively. Like in the semantics of Cool, the first step in the evaluation of Id←e is to recursively evaluate e. FIG. 4 shows the set of transactions in T.sub.e that is broadcast when e is evaluated. Transactions in Te spend the outputs out.sub.1, . . . , out.sub.n, out, thereby creating new revisions out′.sub.1, . . . , out′.sub.n, out′. Then the transaction tx=tx(B.sub.2, [v/l], loc(E)Uloc(so)\{I}, Id←e) is broadcast. This transaction spends the b-locations loc(E)Uloc(so)\{l}={l.sub.1, . . . , l.sub.n} into outputs that store the same values as their predecessor. Transaction tx has one additional input-output pair that spends output out′ into an output out″ which in turn stores the value v obtained from evaluating e. The first output of tx also stores the expression Id←e.

B-Let

(82) The semantic rule for defining variables via let is as follows:

(83) TABLE-US-00009 so, B.sub.1, E  e: v, B.sub.2 I = b-newloc(S.sub.2) E′ = E[I/Id] B.sub.3 = B.sub.2 U {tx(B.sub.2, [v/I], loc(E′) U loc(so), let Id: T ← e in e′)} so, B.sub.3, E′  e′: v′, B.sub.4  — — — — — — — — — - so, B.sub.1, E  let Id: T ← e in e′: v′, B.sub.4

(84) The evaluation of let Id: T←e in e′ with respect to a value so, blockchain B.sub.1, and environment E is shown in FIG. 5. Assume that loc(E)Uloc(so)=l.sub.1, . . . , l.sub.n are b-locations in B.sub.1 and that out.sub.i, . . . , out.sub.n are their revisions in B.sub.1. When the evaluation starts in the first line of the rule of [B-Let], the expression e is evaluated and transactions Te are broadcast that create new revisions out′.sub.1: . . . , out′.sub.n for the l.sub.1, . . . , l.sub.n.

(85) Next, a b-location l is obtained from B.sub.2=B.sub.1UTe. A blockchain environment E′ is defined to be E[l/Id]. Then the transaction tx(B.sub.2, [v/l], loc(E′)U loc(so), let Id: T.sub.1←e.sub.1 in e.sub.2) is broadcast. The transaction spends the latest revisions of l.sub.1, . . . , l.sub.n into outputs out″.sub.1, . . . , out″.sub.n that store the same values as their predecessors. The transaction has one more input-output pair that spends b-location l into a successor that stores the value v.

(86) In the last step, e′ is evaluated in the environment E′ that contains l.sub.i, . . . , l.sub.n form E but also the new location l. The value v′ returned from evaluating e′ is also returned from the evaluation of let Id: T←e in e′.

B-New

(87) Next, we consider object creation in BCool.

(88) TABLE-US-00010 A.sub.0 = X if A = SELF_TYPE and so = X(. . .); and A.sub.0 = A otherwise class(A.sub.0) = (a.sub.1: A.sub.1 ← e.sub.1, . . . , a.sub.n: A.sub.n ← e.sub.n) I.sub.1 = b-newloc(B.sub.1), for i = 1, . . . , n and each I.sub.1 is distinct v = A.sub.0(a.sub.1 = I.sub.1, . . . , a.sub.n = I.sub.n) B.sub.2 = B.sub.1 ∪ { tx(B.sub.1, [D.sub.A_1/I.sub.1, . . . , D.sub.A_n/I.sub.n], loc(E) ∪ loc(so) \ {I.sub.1, . . . , I.sub.n }, new A) } v.sub.1, B.sub.2, [a.sub.1: I.sub.1, . . . , a.sub.n: I.sub.n]  {a.sub.1 ← e.sub.1; . . . ; a.sub.n ← e.sub.n;}: v′, B.sub.3 so, B.sub.1, E  new T: v, B.sub.3

(89) Let A be a class identifier such that class(A)=(a.sub.1: A.sub.1←e.sub.1, . . . , a.sub.n:A.sub.n←e.sub.n). The evaluation of new A with respect to object so, blockchain B.sub.1, and environment E is visualized in FIG. 6. When new A is evaluated, n unspent b-locations l.sub.i, . . . , l.sub.n are obtained from B.sub.1. Assume that loc(E)Uloc(so)\{l.sub.1, . . . , l.sub.n}={l′.sub.1, . . . , l′.sub.m} and that {out′.sub.1, . . . , out′.sub.m} are their revisions in B.sub.1. When the transaction

(90) $tx=\mathrm{tx}\left(B_1,\left[D_{A\_1}/l_1,\mathrm{.Math.},D_{\mathrm{A\_n}}/l_n\right],\mathrm{loc}\left(E\right).Math.\mathrm{loc}\left(\mathrm{so}\right)\setminus \left\{l_1,\mathrm{.Math.},l_n\right\},\mathrm{new}A\right)$
is broadcast, the outputs out′.sub.i, . . . , out′.sub.m are spent into new outputs that store the same values as their predecessors. The fresh b-locations l.sub.1, . . . , l.sub.n are spent into outputs that store the defaults D.sub.A_1, . . . , D.sub.A_n of the types A.sub.1, . . . , A.sub.n of the attributes of A. Finally, each b-locations li with l<=i<=n is initialized to the value of e.sub.i. First e.sub.1 is evaluated in an environment that contains only the b-locations l.sub.1, . . . , l.sub.n. This returns a value v.sub.1 that is assigned to b-location l.sub.1 as described in the section on [B-Assign]. This process is then repeated for each b-location l.sub.2 . . . , l.sub.n and expression e.sub.2, . . . , e.sub.n. The value A(a.sub.1=l.sub.1, . . . , a.sub.n=l.sub.n) is returned from the evaluation of new A.

B-Dispatch

(91) Finally, the semantics of method dispatch is provided as follows:

(92) TABLE-US-00011 so, B.sub.1, E  e1: v.sub.1, B.sub.2 so, B.sub.2, E  e2: v.sub.2, B.sub.3 . . . so, B.sub.n, E  en: v.sub.n, B.sub.n+1 so, B.sub.n+1, E  e.sub.0: v.sub.0, B.sub.n+2 A(a.sub.1 = I.sub.a_1 , . . . , a.sub.m = I.sub.a_m) = v.sub.0 (x.sub.1, . . . , x.sub.n, e.sub.n+1) = implementation(A, f) I.sub.x_I = b-newloc(B.sub.n+2), for i = 1, . . . , n and each I.sub.x_I is distinct B.sub.n+3 = B.sub.n+2 ∪ { tx(B.sub.1, [v.sub.1/I.sub.x_1 , . . . , v.sub.n/I.sub.x_n], loc(E) ∪ loc(so), e.sub.0.f(e.sub.1, . . . , e.sub.n)) } v.sub.0, B.sub.n+3, [a.sub.1: I.sub.a_1 , . . . , a.sub.m: I.sub.a_m, x.sub.1: I.sub.x_1 , . . . , x.sub.n: I.sub.x_n]  e.sub.n+1: v.sub.n+1, B.sub.n+4 ---------------------------------------------------------------------- so, B.sub.1, E  e.sub.0.f(e.sub.1, . . . , e.sub.n): v.sub.n+1, B.sub.n+4

(93) FIG. 7 shows the evaluation of an expression e.sub.0.Math.f(e.sub.1, . . . , e.sub.n). As before, we consider the evaluation with respect to a blockchain B.sub.1, environment E, and object so. We assume that loc(E)∪loc(so)={l′.sub.1, . . . , l′.sub.k} are b-locations and that {out′.sub.1, . . . , out′.sub.k} are their revisions in B.sub.1. First, the expressions e.sub.1, . . . , e.sub.n are evaluated to values v.sub.1, . . . , v.sub.n in the environment E. Transactions T.sub.e_1∪ . . . ∪T.sub.e_n are broadcast which updates the blockchain to B.sub.n+1=B.sub.1∪T.sub.e_1∪ . . . ∪T.sub.e_n. Then, expression e.sub.0 is evaluated in B.sub.n+1 which returns a value v.sub.0=A(a.sub.1=l.sub.a_1, . . . , a.sub.m=l.sub.a_m) and might broadcast further transactions T.sub.e_0. Next, n unspent b-locations l.sub.x_1, . . . , l.sub.x_n are obtained from B.sub.n+2=B.sub.n+1∪T.sub.e_0. Then the transaction

(94) $\mathrm{tx}=\mathrm{tx}\left(B_1,\left[v_1/l_{x\_1},\mathrm{.Math.},v_n/l_{x\_n}\right],\mathrm{loc}\left(E\right).Math.\mathrm{loc}\left(\mathrm{so}\right),e_0.Math.f\left(e_1,\mathrm{.Math.},e_n\right)\right)$
is broadcast. It spends the latest revisions of loc(E)∪loc(so) (that is l′.sub.1, . . . , l′.sub.k) into outputs that store the same value as their predecessor. The transaction also spends the unspent b-locations l.sub.x_1, . . . , l.sub.x_n into revisions that store the values v.sub.1, . . . , v.sub.n. This first output of tx also stores the expression e.sub.0.Math.f(e.sub.1, . . . , e.sub.n).

(95) Finally, the body e.sub.n+1 of the function f is evaluated to v.sub.n+1 in a blockchain environment that contains the b-locations l.sub.x_1, . . . , l.sub.x_n and l.sub.a_1, . . . , l.sub.a_m. The value v.sub.n+1 is returned from the evaluation of e.sub.0.Math.f(e.sub.1, . . . , e.sub.n

B-Static-Dispatch

(96) The rule for static method dispatch is almost entirely like the rule [B-Dispatch] as shown below. The only difference is that in a normal dispatch, the class of this expression is used to determine the method to invoke; in static dispatch the class is specified in the dispatch itself

(97) TABLE-US-00012 so, B.sub.1, E  e1: v.sub.1, B.sub.2 so, B.sub.2, E  e2: v.sub.2, B.sub.3 . . . so, B.sub.n, E  en: v.sub.n, B.sub.n+1 so, B.sub.n+1, E  e.sub.0: v.sub.0, B.sub.n+2 A(a.sub.1 = I.sub.a_1 , . . . , a.sub.m = I.sub.a_m) = v.sub.0 (x.sub.1, . . . , x.sub.n, e.sub.n+1) = implementation(T, f) I.sub.x_I = b-newloc(B.sub.n+2), for i = 1, . . . , n and each I.sub.x_I is distinct B.sub.n+3 = B.sub.n+2 ∪ { tx(B.sub.n+2, [v.sub.1/I.sub.x_1 , . . . , v.sub.n/I.sub.x_n], loc(E) ∪ loc(so), e.sub.0.f(e.sub.1, . . . , e.sub.n)) } v.sub.0, B.sub.n+3, [a.sub.1: I.sub.a_1 , . . . , a.sub.m: I.sub.a_m, x.sub.1: I.sub.x_1 , . . . , x.sub.n: I.sub.x_n]  e.sub.n+1: v.sub.n+1, B.sub.n+4 ---------------------------------------------------------------------------- so, B.sub.1, E  e.sub.0@T.f(e.sub.1, . . . , e.sub.n): v.sub.n+1, B.sub.n+4

Examples

(98) Following are several examples of the evaluation of BCool expressions.

Variable Definition and Assignment

(99) Consider the expression e below consisting of two nested let expressions and an assignment.

(100) TABLE-US-00013 let x ← 1  in let y ← 2   in x ← y

(101) The evaluation is shown in FIG. 8. The first step is to evaluate the expression 1. This evaluation broadcasts no transactions and returns the value Int(1). Then an unspent b-locations lx is obtained and a transaction is a broadcast that spends lx into an output that stores the value Int(1). The first output of this transaction stores the expression e.

(102) Then the expression e′=let y←2 in x←y is evaluated in an environment that maps identifier x to location lx. In this evaluation, the first step is to evaluate the expression 2, which returns the value Int(2). A fresh location ly is obtained from the current blockchain. Then a transaction is broadcast that stores e′ inits first output. This transaction spends lx because it is in the current environment and pends l.sub.x because it is the location created in e′.

(103) In the final step, the assignment x←y is evaluated in the environment E=[x: l.sub.y, y: l.sub.y]. According to the rule for assignments, the expression y is evaluated first. As y is an identifier, no transactions are broadcast. Instead, the b-location l.sub.y for y is looked up in E and the value Int(2) that is stored in the latest revision of l.sub.y is returned. Control returns to the evaluation of x<-y and a transaction is broadcast that spends the latest revisions of the b-locations in the current environment E. The outputs of this transaction update the value stored in l.sub.x to Int(2) and keep all other locations (only l.sub.y in this case) unchanged. This transactions stores x<-y in its first output.

Object Creation

(104) Consider the program P below

(105) TABLE-US-00014 class A {  num: Int }

(106) FIG. 9 shows the evaluation of new A. The first step is to obtain unspent b-locations for each attribute. In this example, there is only one attribute, num, and we denote its unspent b-location by l.sub.num. Next, the location l.sub.num is initialized to the default value Int(0) for integers. This is achieved by broadcasting a transaction tx that spends l.sub.num into an output that stores the value Int(0) and the expression new A. Next, consider the class B in the listing below.

(107) TABLE-US-00015 class B {  a1: A ← new A  a2: A ← new A }

(108) The evaluation of new B is shown in FIG. 10. In the first step, two unspent b-locations la_.sub.1 and la_.sub.2 are obtained from the blockchain. Both are initialized to void in the transaction that also stores the expression new B. The value returned is the object B(a.sub.1=la_.sub.1, a.sub.2=la_.sub.2).

(109) Next, the attributes a.sub.1 and a.sub.2 are assigned values. Both assignments are performed in an environment that contains l.sub.a_1 and l.sub.a_2. To assign a value to a.sub.1 a new object of class A is created as described in the last example. As this object is constructed in an environment that contains other locations (l.sub.a_1 and l.sub.a_2 in this case), the latest revisions of l.sub.a_1 and l.sub.a_2 are spent as well. Next, the value A(num=l.sub.num_1) is assigned to the b-location l.sub.a_1 by the transaction that stores the expression a.sub.1←new A.

(110) Finally, the second attribute a.sub.2 is initialized in the same way. The return value of the entire expression is B(a.sub.1=l.sub.a_1, a.sub.2=l.sub.a_2)

Method Invocation

(111) This final example shows how all four rules [B-Let], [B-Assign], [B-New], and [B-Dispatch] work together. Consider the following program:

(112) TABLE-US-00016 class Counter {  num: Int  inc(x: Int): Int {   num ← x  } }

(113) The evaluation of the expression e below can be explained as follows

(114) let c←new Counter

(115) in c.inc(1)

(116) The first step in the evaluation of e is to evaluate new Counter. In the process transactions tx.sub.1 and tx.sub.2 are broadcast as shown in the FIG. 11. The value Counter(num=l.sub.num) is returned and assigned to the counter variable as follows: a new location l.sub.c is obtained from the blockchain and transaction tx.sub.3 is broadcast that updates the value stored in l.sub.c to Counter(num=l.sub.num).

(117) Finally, c.inc(1) is evaluated in the environment E=[c: l.sub.c]. First, parameter l is evaluated to the value Int(1). Then a new unspent b-location l.sub.x is obtained and is initialized to Int(1) by transaction tx.sub.4. Finally, the body num←x of the inc function is evaluated in the environment E=[num: l.sub.num, x: l.sub.x]. This broadcasts the transaction tx.sub.5 that updates the value stored in l.sub.num to Int(1). The value returned from the entire expression e is Int(1).

Completeness of BCool

(118) We associate a store S.sub.B with every blockchain B as follows. Let L be the set of b-locations in B and let Val.sub.L be the set of Cool values with locations in L. The store of B is a mapping S.sub.B: L->Val.sub.L such that S.sub.B(l) is the value stored at the latest revision of l∈L.

(119) Lemma 1. Let B be a blockchain with b-locations L. Let so ∈Val.sub.L, blockchain environment E, blockchain B, and expression e be given and let S=S.sub.B. Then so, S, E ├e: v, S′ and so, B, E s: v, B′ implies that S′=S.sub.B′.

(120) Proof. By induction on e. If e does not change the store in the Cool semantics, then e does not change the blockchain under the BCool semantics and hence the statement is trivial.

(121) Let so, E, B, and S be as in the assumption. Let v.sub.1, . . . , v.sub.n be values and let l.sub.1, . . . , l.sub.n be locations. Let S′=[v.sub.1/l.sub.1, . . . , v.sub.n/l.sub.n], tx=tx(B, [v.sub.1/l.sub.1, . . . , v.sub.n/l.sub.n], loc(E) ∪loc(so)\{l.sub.1, . . . , l.sub.n}, e), and B′=B∪{tx}. We show that S′=S.sub.B′. The Lemma follows by a straightforward induction over e.

(122) There are two cases. If l=l.sub.i for some l>=l>=n, then by definition S′(l)=v.sub.i. Note that tx(B.sub.i[v.sub.1/l.sub.1, . . . , v.sub.n/l.sub.n], loc(E)∪loc(so)\{l.sub.1, . . . , l.sub.n}, e) spends the latest revision of l into a successor labelled v.sub.i. Hence B′(l)=v.sub.i.

(123) If l.Math.{l.sub.1, . . . , l.sub.n} then S′(l)=S(l). If l∈loc(E)∪loc(so) then tx spends the latest revision of l into a successor that stores the value B(1), and hence B′(1)=B(1)=S(1)=S′(1). Otherwise tx does not spend the latest revision of l and the result follows trivially.

(124) BCool semantics can be optimized further by, for example, using the following two techniques. The goal of the optimizations is to save costs when running a smart contract. To goal of the first optimization is to reduce the size of each transaction broadcast by not storing the values. The goal of the second optimization is to reduce the number of transactions broadcast. The result of applying both optimizations is a smart contract system that can run programs of arbitrary computational (time and space) complexity at a fixed cost.

Decreasing Size of Transactions

(125) We disclose an alternative semantics for BCool expressions called the BC2 that broadcasts transactions that store only expressions and no values. The values, nevertheless, can be computed from the expressions stored on the blockchain. Below, we will refer to the BCool semantics provided above as BC1. We use a new semantic relation for BC2 that has one semantic rule [B2-R] for every rule [B-R] in BC1. The rule [B2-R] is obtained from [B-R] by replacing every occurrence of by 2 and every line of the form

(126) $B^{\prime }=B.Math.\left\{\mathrm{tx}\left(B,\left[v_1/l_1,\mathrm{.Math.},v_n/l_n\right],\mathrm{loc}\left(E\right).Math.\mathrm{loc}\left(so\right),e\right)\right\}$
by a line of the form

(127) $B^{\prime }=B.Math.\left\{\mathrm{tx}\left(B,\left[\right],\left\{l_1,\mathrm{.Math.},l_n\right\}.Math.\mathrm{loc}\left(E\right).Math.\mathrm{loc}\left(\mathrm{so}\right),e\right)\right\}$

(128) Note that the BC2 stores only expressions in the blockchain and no values. Therefore, using BC2 has the advantage that the size of a transaction is reduced and hence transaction fees are saved.

(129) We provide the notion of a valid set of transactions for BC2. Valid transactions are built up from patterns called contexts. A context consists of a sequence of transactions and holes. Every context contains one distinguished transaction called the root of the context. Every hole contains a list of positions and every transaction contains a list of outputs. Holes and transactions are labeled by an expression. A node is either a position or an output and there is a binary relation called spend on nodes. FIG. 12 is a diagram of a transaction context in accordance with some embodiments of the present invention.

(130) FIGS. 15 through 18 show four contexts labelled [Ctx-Assign], [Ctx-Let], [Ctx-New], [Ctx-Dispatch], respectively, the relation spend is indicated by the arrows. Nested boxes with solid lines represent transactions and outputs and arrows represent spending relations. Rectangles with a dashed border represent holes that contain positions. Each context has one transaction with a thicker border that is called the root of the context. In each context, a set of outputs is shown in backslash crosshatches. The locations of these outputs are called the connectors of the context.

(131) FIG. 13 shows context C with n connectors. This context can be plugged into a hole h of a context C′ with n positions if the hole and the context are labeled by the same expression. We denote the resulting context by C′[h<-C]. The root of C′[h<-C] is the root of C′.

(132) An empty context can be plugged into any hole. This process is shown in FIG. 14.

(133) The contexts in FIGS. 15-18 correspond to the derivation rules [Ctx-Assign], [Ctx-New], [Ctx-Let], [Ctx-Dispatch] of the [BC2] semantics. The context for expression e contains a hole for each evaluation of a subexpression of e. The holes are ordered according to the order of evaluation of the subexpressions of e. The root of the context c is labelled by e. The connectors of a context correspond to the set of store locations that are (a) updated by the evaluation of e and (b) accessible after the evaluation of e. The positions of a hole for sub-expression e′ of e correspond to the connectors of the context of e′.

(134) FIGS. 15-18 show the contexts that correspond to evaluation rules of the Cool semantics that update the store. For all other evaluation rules [R] for expression e we provide [R]'s context to be a sequence of holes that are labelled by the sub-expressions of e in the order of their evaluation. Evaluation rules that do not evaluate subexpressions via ├ are the empty context with no holes or transactions. The empty context can be plugged into any hole, closing it as shown in FIG. 14.

(135) Just as derivation rules can be used to build a derivation trees, contexts can be used to build a graphs of Bitcoin transactions. We provide for each expression e it transaction graph by structural recursion on nesting depth of the derivation tree of e: For the base case consider an expression whose derivation tree consists of a single node. The context of all of these expressions is the empty context. The transaction graph of an expression whose context is empty is the empty graph with no transactions. The transaction graph of a context C with holes h1 . . . hn is obtained by plugging the transaction graphs G.sub.1 . . . G.sub.n of the (lower level) expressions of the holes h.sub.1 . . . h.sub.n into the context C as described in FIG. 13.

(136) The size of a transaction graph for expression e is proportional to the number of derivation steps required to evaluate e. As Bitcoin miners charge per transaction size the cost of evaluating an expression would be proportional to the number of derivation steps as well. This is also the cost of evaluating smart contracts on Ethereum where transaction fees are charged per step in the Ethereum Virtual Machine.

(137) A set of transactions T satisfies a transaction pattern P if there is a one to one mapping iso: T->P between the transactions in P and the transactions in T, such that t in T has n inputs and m outputs if and only if iso(t) has n outputs with in-degree>0 and m outputs with out-degree>0, and the i-th input of t spends by the j-th out of t′ if and only if there is an edge from iso(t) to iso(t′) the expression on the first inputs of t is the expression on the label of iso(t). A set of transactions T is valid if it satisfies some transaction pattern that can be obtained from the contexts shown in FIGS. 15-18.

(138) The following lemma allows multiple users to read the expressions in transactions that are broadcast by BC2 and all perform the same computations on their own devices using the Cool semantics. This way, users can gain consensus over the state of a system that they can modify according to predefined rules.

(139) Lemma 2: For every blockchain B, there is a store S.sub.B such that if T is a valid set of transactions, then one can compute a value so.sub.T, B, an environment E.sub.B, T, and an expression e.sub.B, T, such that so.sub.B, T, S.sub.B, E.sub.B, T├e.sub.B, T: v, S′ for some v and S′=S.sub.B∪T.

(140) Proof. Let B and T be given. The proof is by induction on the size of B∪T. As T is valid it satisfies a transaction pattern P=[ct.sub.1, . . . , ct.sub.n] obtained from the contexts in FIGS. 15-18. Then P can be parsed into one of the contexts [h.sub.1, . . . , h.sub.n, r, h′.sub.1, . . . , h′.sub.m] of FIGS. 15-18 where r is the root of P.

(141) Let T.sub.1, . . . , T.sub.n, be the subsets of T that correspond to the holes h.sub.1, . . . , h.sub.n of the pattern P under the mapping iso from T to P. Let B.sub.i=B∪T.sub.1∪ . . . ∪T.sub.i, for 1<=i<=n. We apply the induction hypothesis sequentially to B.sub.1 . . . , B.sub.n. By induction, we compute a values so.sub.i, environments E.sub.i, and expressions e.sub.i such that so.sub.i, S.sub.i, E.sub.i├e.sub.i: v.sub.i, S.sub.i+1 where S.sub.i=S.sub.B_i for 1<=i<=n.

(142) Next, given S.sub.n, we computer the store S.sub.n+1 for the blockchain B.sub.n∪{r}. Let e.sub.0 be the expression on the first output of r.

(143) If the e.sub.0 is of the form Id<-e, then n=1 and we lookup Id in the environment E.sub.1 to determine its location l. We provide S.sub.3=S.sub.2[v.sub.1/l], where v.sub.1 is the value we computed from the transactions for e in step 1.

(144) We next provide the self-object so.sub.n+1. We first determine the locations of so.sub.n+1. Let Outs.sub.so be the sequence outputs of r that have the self-object bit set. For each output out in Outs.sub.so let l.sub.out be its location. We next determine an identifier Id.sub.out for each out∈Outs.sub.so. Consider the expression e.sub.gen stored in the transaction t.sub.gen that spends l.sub.out. One can determine from FIGS. 15-18 that e.sub.gen must be a let-expression, a new-expression, or a dispatch-expression. If e.sub.gen=Id<-e, then we provide Id.sub.out=Id. If e.sub.gen is new A such that class(A)=(a.sub.1: T.sub.1<-e.sub.1, . . . , a.sub.i: T.sub.i<-e.sub.i) and out is the j-th output of r, then Id.sub.out=a.sub.j. If e.sub.gen=e′.sub.0.Math.f(e′.sub.1, . . . , e′.sub.n), A is the type of e′.sub.0, implementation(A, f)=(x.sub.1, . . . , x.sub.n, e.sub.body), and out is the j-th output of r, then we provide Id.sub.out=x.sub.j. We provide so.sub.i+1 to be (Id.sub.out_1=I.sub.out_t, . . . , Id.sub.out_k=l.sub.out_k) such that Outs.sub.so=[out.sub.1, . . . , out.sub.k]. The environment E.sub.n+1 can be constructed from the outputs Outs.sub.E of r that have the environment bit set in the same way. Let e.sub.n+1 be the expression e.sub.0=Id<-e stored in the first output of r. One can check that so.sub.n+1, S.sub.n+1, E.sub.n+1├e.sub.n+1: v.sub.n+1, S.sub.n+2 for some v.sub.n+1 and S.sub.n+2.

(145) The case where e.sub.0 is of the for let Id<-e in e′ is similar: Again, by inspecting the patters [Ctx-Let], one can verify that so.sub.1, S.sub.1, E.sub.1 were computed in step 1 such that so.sub.1, S.sub.1, E.sub.1├e.sub.1: v.sub.1, S.sub.2. Also, we can tell that r must have k′+1 outputs and k′ inputs for some number k′. Let out be the last output of r and let l.sub.out be its location. We provide S.sub.3=S.sub.2[v.sub.1\l.sub.out] and e.sub.n+1 to be let Id<-e in e′. Again, it is easy to check that so.sub.n+1, S.sub.n+1, E.sub.n+1├e.sub.n+1: v.sub.n+1, S.sub.n+2 for some v.sub.n+1 and S.sub.n+2.

(146) The cases for e.sub.0=new A is based on the same ideas. The object so and the environment can be obtained as in the cases for assignment and let expressions. We apply the induction hypothesis and update the store locations l.sub.a_1, . . . , l.sub.a_n with the default values D.sub.T_1, . . . , D.sub.T_n for their types t.sub.1, . . . , t.sub.n as indicated in FIG. 14.

(147) The case of a method dispatch e.sub.0=e.Math.f(e.sub.1, . . . , e.sub.n) is also similar. The value so and the environment E are determined as in the cases before. We apply the induction hypothesis and update the store locations l.sub.x_1, . . . , l.sub.x_n with the default values v.sub.1, . . . , v.sub.n computed in the recursive calls as above.

(148) In the third step we apply the induction hypothesis to the transactions T′.sub.1, . . . , T′.sub.m that correspond to the holes h′.sub.1, . . . , h′.sub.m after r. The lemma follows for the last self-object, environment, and store computed.

(149) Decreasing the Number of Transactions: We disclose a third semantics BC3 for BCool expressions. Given an expression, this semantics first builds the transaction graph described in the section on [BC2]. Instead of broadcasting all transactions in the graph, the graph is first “batched” into a single transaction. This can be accomplished by collapsing all outputs that are connected by one or more “spend” relations. The inputs of this single transaction are the inputs of the transaction graph that spend outputs outside of the transaction graph. The single transaction can be further compacted by removing all input output pairs that correspond to locations in the store that can be garbage collected.

(150) The big advantage of this semantics is that only one transaction is broadcast per evaluated expression. The cost of evaluating an expression under this semantics is fixed and independent of the number of steps required to evaluate the transaction. This means that algorithms of arbitrary computational complexity can be evaluated as smart contracts at a constant cost.

Read Write Conflicts

(151) The order in which transactions are written to the blockchain is not necessarily the same order in which transactions are read by another user. A writer's transactions will not necessarily be included in a block ordered by the time they were sent. However a slightly weaker condition holds: the transactions in the order of writing are included in some topological order of the transaction graph. The sequence of transactions that is read by the readers might therefore be a different topological order. In order to guarantee that all users compute the same value one must show that the values that are read are invariant under topological re-orderings.

(152) To see why the encoding we disclose in paragraph [000121] is invariant under topological reordering, it is helpful to first consider a transaction encoding scheme in which all b-locations are spent that correspond to locations of the store that are either read from or written to during the evaluation of an expression: tx(Bi, [v.sub.1/l.sub.1 . . . v.sub.n/l.sub.n], loc(E)∪loc(so)∪readSet(S, E, e)\{l.sub.1 . . . l.sub.n}, {e, E, loc(so)})

(153) It follows from results in serializability theory that this encoding is invariant under topological re-orderings. The disadvantage of such scheme is that expressions that read a lot of values become expensive to evaluate because they are encoded as large transactions with many inputs. The encoding disclosed in this invention, see, e.g, paragraph [000121], avoids having to spend all locations that are read and stores the inset of locations that are changed instead. This set is often much smaller. One can show that the encoding disclosed in paragraph [000121] is invariant under topological re-orderings.

(154) The invention has been disclosed in at least three smart contract semantics for existing object-oriented programming language. The semantics BC2 and BC3 are more practical than BC1 in some applications.

(155) BC2 makes it very hard for a user to cheat. All a user can do is broadcast a transaction with an invalid expression. In this case, the evaluation just throws an error. Under BC2 it is impossible for a user to broadcast a transaction that leads to a state in the store that is not reachable in the program.

(156) BC3 has practical relevance because of the low cost that it permits users to run a smart contract. This makes it possible to run smart contracts of arbitrary complexity at a fixed cost.

(157) While the foregoing descriptions disclose specific examples, other examples may be used to achieve similar results. Further, the various features of the foregoing embodiments may be selected and combined to produce numerous variations of improved systems.

(158) In the foregoing specification, specific embodiments have been described. However, one of ordinary skill in the art appreciates that various modifications and changes can be made without departing from the scope of the invention as set forth in the claims below. Accordingly, the specification and figures are to be regarded in an illustrative rather than a restrictive sense, and all such modifications are intended to be included within the scope of present teachings.

(159) Moreover, in this document, relational terms such as first and second, and the like may be used solely to distinguish one entity or action from another entity or action without necessarily requiring or implying any actual such relationship or order between such entities or actions. The terms “comprises,” “comprising,” “has”, “having,” “includes”, “including,” “contains”, “containing” or any other variation thereof, are intended to cover a non-exclusive inclusion, such that a process, method, article, or apparatus that comprises, has, includes, contains a list of elements does not include only those elements but may include other elements not expressly listed or inherent to such process, method, article, or apparatus. An element proceeded by “comprises . . . a”, “has . . . a”, “includes . . . a”, “contains . . . a” does not, without more constraints, preclude the existence of additional identical elements in the process, method, article, or apparatus that comprises, has, includes, contains the element. The terms “a” and “an” are defined as one or more unless explicitly stated otherwise herein. The terms “substantially”, “essentially”, “approximately”, “about” or any other version thereof, are defined as being close to as understood by one of ordinary skill in the art. The term “coupled” as used herein is defined as connected, although not necessarily directly and not necessarily mechanically. A device or structure that is “configured” in a certain way is configured in at least that way but may also be configured in ways that are not listed.

(160) The Abstract of the Disclosure is provided to allow the reader to quickly ascertain the nature of the technical disclosure. It is submitted with the understanding that it will not be used to interpret or limit the scope or meaning of the claims. In addition, in the foregoing Detailed Description, it can be seen that various features are grouped together in various embodiments for the purpose of streamlining the disclosure. This method of disclosure is not to be interpreted as reflecting an intention that the claimed embodiments require more features than are expressly recited in each claim. Rather, as the following claims reflect, inventive subject matter lies in less than all features of a single disclosed embodiment. Thus, the following claims are hereby incorporated into the Detailed Description, with each claim standing on its own as a separately claimed subject matter.