Blockchain.v 5.54 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
From Coq Require Import String.
2

3
From Coq Require OrderedTypeEx.
4
5
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
6

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

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

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

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

22
Record ContractDeployment :=
23
  {
24
25
26
27
    deployment_version : Version;
    deployment_msg_ty : OakType;
    deployment_state_ty : OakType;
    deployment_setup : OakValue;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
28
29
  }.

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

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

43
44
45
Record BlockHeader :=
  build_block_header {
    block_number : BlockId;
46
47
  }.

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

54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
(* This needs to be polymorphic because ... for reasons. LocalChain does not
   work if not. A smaller repro is:
Class interface :=
  { ty : Type;
    func : ty -> ty;
  }.

(* the problem is that the implementation contains functions taking the
   interface *)
Record impl :=
  {
    callback : interface -> nat;
  }.

Definition func_concrete (i : impl) : impl := i.

Instance impl_interface : interface :=
  {| ty := impl; func := func_concrete |}.

   todo: come back to this and understand universe polymorphism in depth. *)
Polymorphic Record ChainInterface :=
  build_chain_interface {
76
77
78
79
80
81
82
83
84
    (* 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;
    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_deployment :  ci_chain_type -> Address -> option ContractDeployment;
    ci_contract_state : ci_chain_type -> Address -> option OakValue;
85
86
87
  }.

Record Chain :=
88
  build_chain {
89
90
    chain_ci : ChainInterface;
    chain_val : chain_ci.(ci_chain_type);
91
92
  }.

93
Definition chain_at (c : Chain) (bid : BlockId) : option Chain :=
94
95
  do x <- c.(chain_ci).(ci_chain_at) c.(chain_val) bid;
    Some {| chain_val := x |}.
96
97

Definition head_block (c : Chain) :=
98
  c.(chain_ci).(ci_head_block) c.(chain_val).
99
100
101
102
103

Definition block_at (c : Chain) (bid : BlockId) : option Block :=
  do c <- chain_at c bid; Some (head_block c).

Definition incoming_txs (c : Chain) :=
104
  c.(chain_ci).(ci_incoming_txs) c.(chain_val).
105
106

Definition outgoing_txs (c : Chain) :=
107
  c.(chain_ci).(ci_outgoing_txs) c.(chain_val).
108
109

Definition contract_deployment (c : Chain) :=
110
  c.(chain_ci).(ci_contract_deployment) c.(chain_val).
111
112

Definition contract_state (c : Chain) :=
113
  c.(chain_ci).(ci_contract_state) c.(chain_val).
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
Inductive ChainAction :=
128
129
130
131
132
133
134
135
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
  | act_deploy
      {setup_ty msg_ty state_ty : Type}
      (version : Version)
      (init : ContractCallContext -> setup_ty -> option state_ty)
      (receive : ContractCallContext -> state_ty ->
                 option msg_ty -> option (state_ty * list ChainAction)).
136

137
(*
138
139
Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
  build_contract_interface {
140
    (* The address of the contract being interfaced with *)
141
    contract_address : Address;
142
    (* The setup that was passed when the contract was deployed *)
143
    setup : setup_ty;
144
    (* Obtain the state at some point of time *)
145
    get_state : Chain -> option state_ty;
146
    (* Make an action transferring money to the contract without
147
       a message *)
148
    transfer : Amount -> ContractAction;
149
    (* Make an action calling the contract *)
150
    call : Amount -> msg_ty -> ContractAction;
151
  }.
152
*)
153

154
(*
155
156
157
(* 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
158
   only to interact with a contract using interpreted types. *)
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
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
183
  end.
184
*)