Blockchain.v 5.44 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
From Coq Require Import String.
2
From Coq Require OrderedTypeEx.
3
4
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
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
19
Definition Amount := nat.
Definition BlockId := nat.
Definition BlockHash := string.
Definition Version := nat.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
20

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

29
30
31
32
33
34
35
36
37
38
39
Inductive TxBody :=
  | tx_empty
  | tx_deploy (deployment : ContractDeployment)
  | tx_call (message : OakValue).
      
Record Tx :=
  build_tx {
    tx_from : Address;
    tx_to : Address;
    tx_amount : Amount;
    tx_body : TxBody;
40
41
  }.

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

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

53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
(* 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 {
    ifc_chain_type : Type;
    ifc_chain_at : ifc_chain_type -> BlockId -> option ifc_chain_type;
    ifc_head_block : ifc_chain_type -> Block;
    ifc_incoming_txs : ifc_chain_type -> Address -> list Tx;
    ifc_outgoing_txs :  ifc_chain_type -> Address -> list Tx;
    ifc_contract_deployment :  ifc_chain_type -> Address -> option ContractDeployment;
    ifc_contract_state : ifc_chain_type -> Address -> option OakValue;
  }.

Record Chain :=
85
  build_chain {
86
87
    chain_ifc : ChainInterface;
    chain_val : ifc_chain_type chain_ifc
88
89
  }.

90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
Definition chain_at (c : Chain) (bid : BlockId) : option Chain :=
  do x <- c.(chain_ifc).(ifc_chain_at) c.(chain_val) bid;
     Some {| chain_val := x |}.

Definition head_block (c : Chain) :=
  c.(chain_ifc).(ifc_head_block) c.(chain_val).

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

Definition incoming_txs (c : Chain) :=
  c.(chain_ifc).(ifc_incoming_txs) c.(chain_val).

Definition outgoing_txs (c : Chain) :=
  c.(chain_ifc).(ifc_outgoing_txs) c.(chain_val).

Definition contract_deployment (c : Chain) :=
  c.(chain_ifc).(ifc_contract_deployment) c.(chain_val).

Definition contract_state (c : Chain) :=
  c.(chain_ifc).(ifc_contract_state) c.(chain_val).

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

124
Inductive ChainAction :=
125
126
127
128
129
130
131
132
| 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)).
133

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

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