Blockchain.v 4.28 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
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
105
106
107
108
109
110
111
112
113
114
115
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

Inductive Contract : Type -> Type -> Type -> Type :=
  | build_contract :
      forall (setup_ty msg_ty state_ty : Type),
        Version ->
        (setup_ty -> ContractCallContext -> option state_ty) -> (* init *)
        (state_ty -> ContractCallContext ->
         option msg_ty -> option (state_ty * list ChainAction)) -> (* receive *)
        Contract setup_ty msg_ty state_ty
with ChainAction :=
  | act_transfer (to : Address) (amount : Amount)
  | act_deploy :
      forall setup_ty msg_ty state_ty,
        Contract setup_ty msg_ty state_ty ->
        setup_ty ->
        ChainAction
  | act_call (to : Address) (amount : Amount) (msg : OakValue).

Definition contract_version {A B C : Type} (c : Contract A B C) :=
  let 'build_contract _ _ _ ver _ _ := c in ver.

Definition contract_init {A B C : Type} (c : Contract A B C) :=
  let 'build_contract _ _ _ _ init _ := c in init.

Definition contract_receive {A B C : Type} (c : Contract A B C) :=
  let 'build_contract _ _ _ _ _ recv := c in recv.

Record ContractInterface (setup_ty msg_ty state_ty : Type) :=
  build_contract_interface {
    contract_address : Address;
    setup : setup_ty;
    get_state : Chain -> option state_ty;
    transfer : Amount -> ChainAction;
    call : Amount -> msg_ty -> ChainAction;
  }.

(* 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
  end.