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

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

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

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

18
19
20
21
Definition Amount := nat.
Definition BlockId := nat.
Definition BlockHash := string.
Definition Version := nat.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
22

23
Record ContractDeployment :=
24
  {
25
    deployment_version : Version;
26
27
28
29
    (* 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.
30
    deployment_msg_ty : OakType;
31
    deployment_state_ty : OakType; *)
32
    deployment_setup : OakValue;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
33
34
  }.

35
36
37
38
Inductive TxBody :=
  | tx_empty
  | tx_deploy (deployment : ContractDeployment)
  | tx_call (message : OakValue).
39

40
41
42
43
44
45
Record Tx :=
  build_tx {
    tx_from : Address;
    tx_to : Address;
    tx_amount : Amount;
    tx_body : TxBody;
46
47
  }.

48
49
50
Record BlockHeader :=
  build_block_header {
    block_number : BlockId;
51
52
  }.

53
54
55
56
57
58
Record Block :=
  build_block {
    block_header : BlockHeader;
    block_txs : list Tx;
  }.

59
Record ChainInterface :=
60
  build_chain_interface {
61
62
63
64
    (* 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;
65
66
67
    (* 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 *)
68
69
70
71
    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;
72
73
74
  }.

Record Chain :=
75
  build_chain {
76
77
    chain_ci : ChainInterface;
    chain_val : chain_ci.(ci_chain_type);
78
79
  }.

80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
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.
105

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

118
Inductive ChainAction :=
119
120
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
  | 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
           {A B C : Type}
           {eq_a : OakTypeEquivalence A}
           {eq_b : OakTypeEquivalence B}
           {eq_c : OakTypeEquivalence C}
           (c : Contract A B C) : WeakContract :=
  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.
170

171
(*
172
173
Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
  build_contract_interface {
174
    (* The address of the contract being interfaced with *)
175
    contract_address : Address;
176
    (* The setup that was passed when the contract was deployed *)
177
    setup : setup_ty;
178
    (* Obtain the state at some point of time *)
179
    get_state : Chain -> option state_ty;
180
    (* Make an action transferring money to the contract without
181
       a message *)
182
    transfer : Amount -> ContractAction;
183
    (* Make an action calling the contract *)
184
    call : Amount -> msg_ty -> ContractAction;
185
  }.
186
*)
187

188
(*
189
190
191
(* todo: this should be easier -- we want actual strong typed
   interface by equivalence of oak type (iterated product, for instance)
   to types in contracts. Right now the interface received allows you
192
   only to interact with a contract using interpreted types. *)
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
Definition get_contract_interface
           (setup_oty msg_oty state_oty : OakType)
           (chain : Chain)
           (addr : Address)
  : option (ContractInterface
              (interp_type setup_oty)
              (interp_type msg_oty)
              (interp_type state_oty)) :=
  do deployment <- chain.(get_contract_deployment) addr;
  let (deploy_setup_oty, deploy_setup) := deployment.(deployment_setup) in
  match eq_oak_type_dec setup_oty deploy_setup_oty,
        eq_oak_type_dec msg_oty deployment.(deployment_msg_ty),
        eq_oak_type_dec state_oty deployment.(deployment_state_ty)
  with
  | left _, left _, left _ =>
    Some {|
        contract_address := addr;
        setup := let x : interp_type setup_oty := ltac:(subst; exact deploy_setup) in x;
        get_state futureChain :=
          do val <- futureChain.(get_contract_state) addr;
          extract_oak_value state_oty val;
        transfer := act_transfer addr;
        call amt msg := act_call addr amt (build_oak_value msg_oty msg) |}
  | _, _, _ => None
217
  end.
218
*)