Blockchain.v 793 Bytes
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
From Coq Require Import String.
2
From Coq Require OrderedTypeEx.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
3

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

Module Address.
  Definition eqb := Nat.eqb.
  Module as_modern_OT := PeanoNat.Nat.
  Module as_old_OT := OrderedTypeEx.Nat_as_OT.
End Address.

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

16
17
18
19
Definition amount := nat.
Definition block_id := nat.
Definition block_hash := string.
Definition version := nat.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
20

21
22
Inductive tx_body :=
| Empty : tx_body.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
23

24
Record contract_call_details :=
25
26
  {
    from : address ;
27
28
    to : address ;
    value : amount
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
29
30
  }.

31
32
33
34
35
36
37
38
39
40
41
42
43
44
Record block_header :=
  {
    blockNumber : block_id
  }.

Record block :=
  {
    header : block_header
  }.

Record chain :=
  {
    headBlock : block
  }.