Commit 86c3f6dd authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Some updates to Blockchain.v

* Add =? operator for addresses
* Add rudimentary block chain info (block number, needed by Congress.v)
parent 6fa52472
......@@ -2,6 +2,17 @@ From Coq Require Import String.
From Coq Require OrderedTypeEx.
Definition address := nat.
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.
Definition amount := nat.
Definition block_id := nat.
Definition block_hash := string.
......@@ -11,13 +22,23 @@ Inductive tx_body :=
| Empty : tx_body.
Record contract_call_details :=
{ from : address ;
{
from : address ;
to : address ;
value : amount
}.
Module Address.
Definition eqb := Nat.eqb.
Module as_modern_OT := PeanoNat.Nat.
Module as_old_OT := OrderedTypeEx.Nat_as_OT.
End Address.
\ No newline at end of file
Record block_header :=
{
blockNumber : block_id
}.
Record block :=
{
header : block_header
}.
Record chain :=
{
headBlock : block
}.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment