Blockchain.v 12.6 KB
Newer Older
1
From Coq Require Import List.
2
3
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
4
From SmartContracts Require Import Extras.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
5

6
Definition Address := nat.
7
Delimit Scope address_scope with address.
8
Bind Scope address_scope with Address.
9
10
11
12
13
14
15

Module Address.
  Definition eqb := Nat.eqb.
End Address.

Infix "=?" := Address.eqb (at level 70) : address_scope.

16
17
18
Definition Amount := nat.
Definition BlockId := nat.
Definition Version := nat.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
19

20
Record ContractDeployment :=
21
  build_contract_deployment {
22
    deployment_version : Version;
23
24
25
26
    (* todo: model any type/constraints so we can have this. Right now the
       problem is that Congress messages can contain _any_ oak value (for
       the congress to send out), so there is no bijection from its message type
       to oak type.
27
    deployment_msg_ty : OakType;
28
    deployment_state_ty : OakType; *)
29
    deployment_setup : OakValue;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
30
31
  }.

32
33
34
35
Inductive TxBody :=
  | tx_empty
  | tx_deploy (deployment : ContractDeployment)
  | tx_call (message : OakValue).
36

37
38
39
40
41
42
Record Tx :=
  build_tx {
    tx_from : Address;
    tx_to : Address;
    tx_amount : Amount;
    tx_body : TxBody;
43
44
  }.

45
46
47
Record BlockHeader :=
  build_block_header {
    block_number : BlockId;
48
49
  }.

50
51
52
53
54
55
Record Block :=
  build_block {
    block_header : BlockHeader;
    block_txs : list Tx;
  }.

56
(* The ChainInterface is an interface that allows different implementations
57
58
59
of chains. This represents the view of the blockchain that a contract
can access and interact with. This does not contain all information of
the chain (and it can't for positivity reasons).
60
*)
61
Record ChainInterface :=
62
  build_chain_interface {
63
64
    (* Would be nice to encapsulate ChainInterface somewhat here
       and avoid these ugly prefixed names *)
65
66
    ci_type : Type;
    ci_chain_at : ci_type -> BlockId -> option ci_type;
67
68
69
    (* Last finished block. During contract execution, this is the previous
       block, i.e. this block does _not_ contain the transaction that caused
       the contract to be called *)
70
71
72
73
    ci_head_block : ci_type -> Block;
    ci_incoming_txs : ci_type -> Address -> list Tx;
    ci_outgoing_txs :  ci_type -> Address -> list Tx;
    ci_contract_state : ci_type -> Address -> option OakValue;
74
75
  }.

76
(* An actual chain interface together with a value of the chain.
77
78
79
80
81
82
83
For example, one obvious chain implementation could be as a list
of blocks and some operations on such a list. Then, the value is
simply the list of blocks.
This avoids having to either
1. Import an actual instance of ChainInterface when taking a chain, or
2. Abstracting over any implementation of ChainInterface when taking
a chain. *)
84
Record Chain :=
85
  build_chain {
86
    chain_ci : ChainInterface;
87
    chain_val : chain_ci.(ci_type);
88
89
  }.

90
91
92
Section ChainAccessors.
  Context (chain : Chain).

93
  Let g {A : Type} (p : forall chain : ChainInterface, ci_type chain -> A)
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
      := p chain.(chain_ci) chain.(chain_val).

  Definition chain_at (bid : BlockId) : option Chain :=
    do x <- chain.(chain_ci).(ci_chain_at) chain.(chain_val) bid;
      Some {| chain_val := x |}.

  Definition head_block := g ci_head_block.
  Definition incoming_txs := g ci_incoming_txs.
  Definition outgoing_txs := g ci_outgoing_txs.
  Definition contract_state := g ci_contract_state.
  Definition account_balance (addr : Address) : Amount :=
    let sum := fold_right Nat.add 0 in
    let sum_amounts txs := sum (map tx_amount txs) in
    sum_amounts (incoming_txs addr) - sum_amounts (outgoing_txs addr).
  Definition contract_deployment (addr : Address) : option ContractDeployment :=
    let to_dep tx := match tx.(tx_body) with
                     | tx_deploy dep => Some dep
                     | _ => None
                     end in
    find_first to_dep (incoming_txs addr).
End ChainAccessors.
115

116
Inductive ContractCallContext :=
117
  build_contract_call_ctx {
118
119
120
121
122
123
124
125
    (* Chain *)
    ctx_chain : Chain;
    (* Address sending the funds *)
    ctx_from : Address;
    (* Address of the contract being called *)
    ctx_contract_address : Address;
    (* Amount of GTU passed in call *)
    ctx_amount : Amount;
126
  }.
127

128
(* Operations that a contract can return that allows it to perform
129
different actions as a result of its execution. *)
130
Inductive ChainAction :=
131
132
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
133
  | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
134
(* Since one operation is the possibility to deploy a new contract,
135
136
137
138
139
140
141
142
143
144
145
this represents an instance of a contract. Note that the act of deploying
a contract has to be a separate thing to the contract deployment a contract
can access during its execution due to positivity constraints. That is,
we would like to allow contracts to obtain information about what another
contract was deployed with (its setup, version and amount transferred). An obvious
way to model this would be to simply store a WeakContract in the chain.
But this is already a non-strict positive occurence, since we dumbed down then
end up with
Record WeakContract := { receive : (Address -> WeakContract) -> State -> State }.
where Address -> WeakContract would be some operation that the chain provides
to allow access to contracts in deployments.
146
*)
147
148
149
150
151
152
153
154
with WeakContract :=
     | build_weak_contract
         (version : Version)
         (init : ContractCallContext -> OakValue -> option OakValue)
         (receive : ContractCallContext -> OakValue (* state *) ->
                    option OakValue (* message *) ->
                    option (OakValue * list ChainAction)).

155
(* Represents a strongly-typed contract. This is what user's will primarily
156
157
158
use and interact with when they want deployment. We keep the weak contract
only "internally" for blockchains, while any strongly-typed contract can
be converted to and from *)
159
160
Record Contract
       (setup_ty msg_ty state_ty : Type)
161
162
163
       `{OakTypeEquivalence setup_ty}
       `{OakTypeEquivalence msg_ty}
       `{OakTypeEquivalence state_ty} :=
164
165
166
167
168
169
170
171
172
173
174
175
176
177
  build_contract {
    version : Version;
    init : ContractCallContext -> setup_ty -> option state_ty;
    receive :
      ContractCallContext -> state_ty ->
      option msg_ty -> option (state_ty * list ChainAction);
  }.

Arguments version {_ _ _ _ _ _} contract : rename.
Arguments init {_ _ _ _ _ _} contract ctx setup : rename.
Arguments receive {_ _ _ _ _ _} contract ctx state msg : rename.
Arguments build_contract {_ _ _ _ _ _}.

Definition contract_to_weak_contract
178
           {setup_ty msg_ty state_ty : Type}
179
180
181
           `{OakTypeEquivalence setup_ty}
           `{OakTypeEquivalence msg_ty}
           `{OakTypeEquivalence state_ty}
182
           (c : Contract setup_ty msg_ty state_ty) : WeakContract :=
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
  let weak_init ctx oak_setup :=
      do setup <- deserialize oak_setup;
      do state <- c.(init) ctx setup;
      Some (serialize state) in
  let weak_recv ctx oak_state oak_msg_opt :=
      do state <- deserialize oak_state;
      match oak_msg_opt with
      | Some oak_msg =>
        do msg <- deserialize oak_msg;
        do '(new_state, acts) <- c.(receive) ctx state (Some msg);
        Some (serialize new_state, acts)
      | None =>
        do '(new_state, acts) <- c.(receive)  ctx state None;
        Some (serialize new_state, acts)
      end in
  build_weak_contract c.(version) weak_init weak_recv.
199

200
201
Coercion contract_to_weak_contract : Contract >-> WeakContract.

202
(* Deploy a strongly typed contract with some amount and setup *)
203
204
Definition create_deployment
           {setup_ty msg_ty state_ty : Type}
205
206
207
           `{OakTypeEquivalence setup_ty}
           `{OakTypeEquivalence msg_ty}
           `{OakTypeEquivalence state_ty}
208
209
210
211
212
213
           (amount : Amount)
           (contract : Contract setup_ty msg_ty state_ty)
           (setup : setup_ty)
  : ChainAction :=
  act_deploy amount contract (serialize setup).

214
(* The contract interface is the main mechanism allowing a deployed
215
216
contract to interact with another deployed contract. This hides
the ugly details everything being OakValue away from contracts. *)
217
Record ContractInterface {setup_ty msg_ty state_ty : Type} :=
218
  build_contract_interface {
219
    (* The address of the contract being interfaced with *)
220
    contract_address : Address;
221
222
    (* Version of the contract *)
    contract_version : Version;
223
    (* The setup that was passed when the contract was deployed *)
224
    contract_setup : setup_ty;
225
    (* Obtain the state at some point of time *)
226
    get_state : Chain -> option state_ty;
227
    (* Make an action transferring money to the contract without
228
       a message *)
229
    transfer : Amount -> ChainAction;
230
    (* Make an action calling the contract *)
231
    call : Amount -> msg_ty -> ChainAction;
232
233
  }.

234
235
236
Arguments ContractInterface _ _ _ : clear implicits.
Arguments build_contract_interface {_ _ _}.

237
238
239
Definition get_contract_interface
           (chain : Chain)
           (addr : Address)
240
           (setup_ty msg_ty state_ty : Type)
241
242
243
           `{OakTypeEquivalence setup_ty}
           `{OakTypeEquivalence msg_ty}
           `{OakTypeEquivalence state_ty}
244
245
246
247
248
249
250
251
252
253
254
255
  : option (ContractInterface setup_ty msg_ty state_ty) :=
  do 'build_contract_deployment ver ov_setup <- contract_deployment chain addr;
  do setup <- deserialize ov_setup;
  let ifc_get_state chain := deserialize =<< (contract_state chain addr) in
  let ifc_transfer := act_transfer addr in
  let ifc_call amount msg := act_call addr amount (serialize msg) in
  Some {| contract_address := addr;
          contract_version := ver;
          contract_setup := setup;
          get_state := ifc_get_state;
          transfer := ifc_transfer;
          call := ifc_call; |}.
256

257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
(* TODO: Is there a more organic way of doing this than duplicating the
structures? Maybe by abstracting over the details or something? This is
super ugly.*)
Inductive FullTxBody :=
  | ftx_empty
  | ftx_deploy (contract : WeakContract) (setup : OakValue)
  | ftx_call (message : OakValue).

Record FullTx :=
  build_ftx {
    ftx_from : Address;
    ftx_to : Address;
    ftx_amount : Amount;
    ftx_body : FullTxBody;
    ftx_is_internal : bool;
  }.

Definition full_tx_to_tx (ftx : FullTx) : Tx :=
  let (from, to, amount, fbody, _) := ftx in
  let body :=
      match fbody with
      | ftx_empty => tx_empty
      | ftx_deploy (build_weak_contract ver _ _) setup =>
        tx_deploy (build_contract_deployment ver setup)
      | ftx_call msg => tx_call msg
      end in
  build_tx from to amount body.

Coercion full_tx_to_tx : FullTx >-> Tx.

287
(* A ChainBuilder represents the additional state, operations and specifications
288
289
290
291
292
293
294
295
296
that a concrete implementation of a block chain needs to support. In contrast
to Chain and ChainInterface, this contains the _full_ blockchain information.
Thus, a ChainBuilder should be convertible into a Chain but not vice-versa.
As an example, the builder needs to contain information about all contracts
(including their receive functions) to be able to properly call into contracts
when receiving messages. The ChainBuilder is what supports the actual
"progression of time" induced by new blocks being added. Such a ChainBuilder is
what contracts will reason over when proving interesting temporal properties
of their behavior. *)
297
298
299
300
301
302
303
304
305
306
307
308
(* TODO: Naming of this is kind of bad. It is somewhat descriptive, but not really.
   Maybe something like ChainEnvironment or ChainContext could be better. *)
Record ChainBuilderInterface :=
  build_chain_builder_interface {
    cbi_chain_interface :> ChainInterface;
    cbi_type : Type;
    cbi_chain : cbi_type -> cbi_chain_interface.(ci_type);
    cbi_initial : cbi_type;
    cbi_add_block : cbi_type -> (* cur *)
                    Address (* coinbase *) ->
                    list (Address * ChainAction) (* actions *) ->
                    option cbi_type;
309
310
311
312
    (* List of transactions that have been executed on the chain, in order.
That is, the head of the list corresponds to actions in the very first block.
This includes "internal" transactions (txs resulting from contract execution) *)
    cbi_all_txs : cbi_type -> list FullTx;
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
  }.

Record ChainBuilder :=
  build_chain_builder {
    chain_builder_cbi : ChainBuilderInterface;
    chain_builder_val : chain_builder_cbi.(cbi_type);
  }.

Definition chain_builder_chain (cb : ChainBuilder) : Chain :=
  let (cbi, val) := cb in
  build_chain cbi (cbi.(cbi_chain) val).

Coercion chain_builder_chain : ChainBuilder >-> Chain.

Definition initial_chain_builder (cbi : ChainBuilderInterface) : ChainBuilder :=
  build_chain_builder cbi cbi.(cbi_initial).

Definition add_block
           (cur : ChainBuilder)
           (coinbase : Address)
           (actions : list (Address * ChainAction))
           : option ChainBuilder :=
  let (ifc, val) := cur in
  let new_val := ifc.(cbi_add_block) val coinbase actions in
  option_map (build_chain_builder ifc) new_val.
338
339
340
341

Definition all_txs (cb : ChainBuilder) :=
  let (ifc, val) := cb in
  ifc.(cbi_all_txs) val.