Blockchain.v 11.5 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
57
58
59
(* The ChainInterface is an interface that allows different implementations
   of chains. This represents the view of the blockchain that a contract
   can access and interact with. This is separate from
*)
60
Record ChainInterface :=
61
  build_chain_interface {
62
63
    (* Would be nice to encapsulate ChainInterface somewhat here
       and avoid these ugly prefixed names *)
64
65
    ci_type : Type;
    ci_chain_at : ci_type -> BlockId -> option ci_type;
66
67
68
    (* 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 *)
69
70
71
72
    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;
73
74
  }.

75
76
77
78
79
80
81
82
(* An actual chain interface together with a value of the chain.
   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. *)
83
Record Chain :=
84
  build_chain {
85
    chain_ci : ChainInterface;
86
    chain_val : chain_ci.(ci_type);
87
88
  }.

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

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

115
Inductive ContractCallContext :=
116
  build_contract_call_ctx {
117
118
119
120
121
122
123
124
    (* 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;
125
  }.
126

127
128
(* Operations that a contract can return that allows it to perform
   different actions as a result of its execution. *)
129
Inductive ChainAction :=
130
131
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
132
  | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
133
134
135
136
137
138
139
140
141
142
143
144
145
(* Since one operation is the possibility to deploy a new contract,
   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
with WeakContract :=
     | build_weak_contract
         (version : Version)
         (init : ContractCallContext -> OakValue -> option OakValue)
         (receive : ContractCallContext -> OakValue (* state *) ->
                    option OakValue (* message *) ->
                    option (OakValue * list ChainAction)).

154
155
156
157
(* Represents a strongly-typed contract. This is what user's will primarily
   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 *)
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
Record Contract
       (setup_ty msg_ty state_ty : Type)
       {eq_setup : OakTypeEquivalence setup_ty}
       {eq_msg : OakTypeEquivalence msg_ty}
       {eq_state : OakTypeEquivalence state_ty} :=
  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
177
178
179
180
181
           {setup_ty msg_ty state_ty : Type}
           {_ : OakTypeEquivalence setup_ty}
           {_ : OakTypeEquivalence msg_ty}
           {_ : OakTypeEquivalence state_ty}
           (c : Contract setup_ty msg_ty state_ty) : WeakContract :=
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
  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.
198

199
200
Coercion contract_to_weak_contract : Contract >-> WeakContract.

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

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

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

236
237
238
Definition get_contract_interface
           (chain : Chain)
           (addr : Address)
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
           (setup_ty msg_ty state_ty : Type)
           {_ : OakTypeEquivalence setup_ty}
           {_ : OakTypeEquivalence msg_ty}
           {_ : OakTypeEquivalence state_ty}
  : 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; |}.
255
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
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302

(* A ChainBuilder represents the additional state, operations and specifications
   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 contains 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. *)
(* 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;
  }.

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.