Blockchain.v 4.55 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
45
Record BlockHeader :=
  build_block_header {
    block_number : BlockId;
    block_hash : BlockHash;
46
47
  }.

48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
Record Block :=
  build_block {
    block_header : BlockHeader;
    block_txs : list Tx;
  }.

Inductive Chain :=
  build_chain {
    get_chain_at : BlockId -> option Chain;
    get_block_at : BlockId -> option Block;
    head_block : Block;
    get_incoming_txs : Address -> list unit;
    get_outgoing_txs : Address -> list unit;
    get_contract_deployment : Address -> option ContractDeployment;
    get_contract_state : Address -> option OakValue;
  }.

Inductive ContractCallContext :=
  build_contract_call_ctx {
    (* 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;
75
  }.
76

77
Inductive ChainAction :=
78
  | act_transfer (to : Address) (amount : Amount)
79
80
81
  (* todo: Should we use mutual inductives and store a Contract here?
     It does not allow contracts to store chain actions in their state,
     but that may be preferable. *)
82
83
  | act_deploy :
      forall setup_ty msg_ty state_ty,
84
85
86
87
        Version ->
        (ContractCallContext -> setup_ty -> option state_ty) -> (* init *)
        (ContractCallContext -> state_ty ->
         option msg_ty -> option (state_ty * list ChainAction)) -> (* receive *)
88
89
90
        ChainAction
  | act_call (to : Address) (amount : Amount) (msg : OakValue).

91
92
93
94
95
96
97
Record Contract (setup_ty msg_ty state_ty : Type) :=
  build_contract {
    contract_version : Version;
    contract_init : ContractCallContext -> setup_ty -> option state_ty;
    contract_receive : ContractCallContext -> state_ty ->
                       option msg_ty -> option (state_ty * list ChainAction);
    }.
98

99
Arguments build_contract {_ _ _}.
100
101
102

Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
  build_contract_interface {
103
    (* The address of the contract being interfaced with *)
104
    contract_address : Address;
105
    (* The setup that was passed when the contract was deployed *)
106
    setup : setup_ty;
107
    (* Obtain the state at some point of time *)
108
    get_state : Chain -> option state_ty;
109
110
    (* Make an action transferirng money to the contract without
       a message *)
111
    transfer : Amount -> ChainAction;
112
    (* Make an action calling the contract *)
113
114
115
    call : Amount -> msg_ty -> ChainAction;
  }.

116
(*
117
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
(* 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
   only to interact with a contrat using interpreted types. *)
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
145
146
  end.
*)