Blockchain.v 7.44 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
Record ChainInterface :=
57
  build_chain_interface {
58
59
60
61
    (* Would be nice to encapsulate ChainInterface somewhat here
       and avoid these ugly prefixed names *)
    ci_chain_type : Type;
    ci_chain_at : ci_chain_type -> BlockId -> option ci_chain_type;
62
63
64
    (* 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 *)
65
66
67
68
    ci_head_block : ci_chain_type -> Block;
    ci_incoming_txs : ci_chain_type -> Address -> list Tx;
    ci_outgoing_txs :  ci_chain_type -> Address -> list Tx;
    ci_contract_state : ci_chain_type -> Address -> option OakValue;
69
70
71
  }.

Record Chain :=
72
  build_chain {
73
74
    chain_ci : ChainInterface;
    chain_val : chain_ci.(ci_chain_type);
75
76
  }.

77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
Section ChainAccessors.
  Context (chain : Chain).

  Let g {A : Type} (p : forall chain : ChainInterface, ci_chain_type chain -> A)
      := 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.
102

103
Inductive ContractCallContext :=
104
  build_contract_call_ctx {
105
106
107
108
109
110
111
112
    (* 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;
113
  }.
114

115
Inductive ChainAction :=
116
117
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
  | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
with WeakContract :=
     | build_weak_contract
         (version : Version)
         (init : ContractCallContext -> OakValue -> option OakValue)
         (receive : ContractCallContext -> OakValue (* state *) ->
                    option OakValue (* message *) ->
                    option (OakValue * list ChainAction)).

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
146
147
148
149
150
           {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 :=
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
  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.
167

168
169
Coercion contract_to_weak_contract : Contract >-> WeakContract.

170
171
172
173
174
175
176
177
178
179
180
181
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).

Record ContractInterface {setup_ty msg_ty state_ty : Type} :=
182
  build_contract_interface {
183
    (* The address of the contract being interfaced with *)
184
    contract_address : Address;
185
186
    (* Version of the contract *)
    contract_version : Version;
187
    (* The setup that was passed when the contract was deployed *)
188
    contract_setup : setup_ty;
189
    (* Obtain the state at some point of time *)
190
    get_state : Chain -> option state_ty;
191
    (* Make an action transferring money to the contract without
192
       a message *)
193
    transfer : Amount -> ChainAction;
194
    (* Make an action calling the contract *)
195
    call : Amount -> msg_ty -> ChainAction;
196
197
  }.

198
199
200
Arguments ContractInterface _ _ _ : clear implicits.
Arguments build_contract_interface {_ _ _}.

201
202
203
Definition get_contract_interface
           (chain : Chain)
           (addr : Address)
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
           (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; |}.