Commit ed136fc6 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Lots of refactoring and progress on proving LocalBlockchain

parent cccf3368
......@@ -184,3 +184,9 @@ Ltac simplify_perm :=
repeat simplify_perm_round;
simpl;
try apply Permutation_refl.
Ltac case_match :=
match goal with
| [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
| [|- context [ match ?x with _ => _ end ]] => destruct x eqn:?
end.
This diff is collapsed.
From Coq Require Import NArith ZArith.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Finite.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From Coq Require Import Eqdep_dec.
From Coq Require Import List.
From Coq Require Import Psatz.
From stdpp Require countable.
Import ListNotations.
Local Open Scope N.
Definition BoundedN (bound : N) := { n : N | n < bound }.
Module BoundedN.
Definition eqb {bound : N} (a b : BoundedN bound) : bool :=
N.eqb (proj1_sig a) (proj1_sig b).
Definition eq_dec {bound : N} (a b : BoundedN bound) :
{a = b} + {a <> b}.
Proof.
destruct a as [a alt], b as [b blt].
destruct (N.eq_dec a b).
- left. subst. f_equal.
apply UIP_dec.
decide equality.
- right.
intros H.
inversion H.
contradiction.
Defined.
Local Lemma N_lt_dec (a b : N) : {a < b} + {~(a < b)}.
Proof. unfold "<". decide equality. Defined.
Local Lemma Z_lt_dec (a b : Z) : ({a < b} + {~(a < b)})%Z.
Proof. unfold "<"%Z. decide equality. Defined.
Definition to_N {bound : N} (n : BoundedN bound) : N :=
proj1_sig n.
Definition of_N {bound : N} (n : N) : option (BoundedN bound).
Proof.
destruct (N_lt_dec n bound).
- exact (Some (exist _ n l)).
- exact None.
Defined.
Definition to_nat {bound : N} (n : BoundedN bound) : nat :=
N.to_nat (to_N n).
Definition of_nat {bound : N} (n : nat) : option (BoundedN bound) :=
of_N (N.of_nat n).
Definition to_Z {bound : N} (n : BoundedN bound) : Z :=
Z.of_N (to_N n).
Definition of_Z {bound : N} (z : Z) : option (BoundedN bound) :=
if (z <? 0)%Z then None else of_N (Z.to_N z).
Definition of_Z_const (bound : N) (z : Z) :=
let ofz := @of_Z bound z in
match ofz return (match ofz with
| Some _ => BoundedN bound
| None => unit
end) with
| Some x => x
| None => tt
end.
Lemma to_N_inj {bound : N} {a b : BoundedN bound} :
to_N a = to_N b -> a = b.
Proof.
intros eq.
destruct a, b.
simpl in *.
subst.
f_equal.
apply UIP_dec.
decide equality.
Qed.
Hint Resolve to_N_inj.
Lemma eqb_spec {bound : N} (a b : BoundedN bound) :
Bool.reflect (a = b) (eqb a b).
Proof.
unfold eqb.
destruct (N.eqb_spec (proj1_sig a) (proj1_sig b)) as [eq | neq].
- constructor.
auto.
- constructor.
intros H; rewrite H in neq; tauto.
Qed.
Lemma eqb_refl {bound : N} (n : BoundedN bound) :
eqb n n = true.
Proof. destruct (eqb_spec n n); tauto. Qed.
Lemma to_nat_inj {bound : N} (a b : BoundedN bound) :
to_nat a = to_nat b -> a = b.
Proof.
intros eq.
apply to_N_inj.
unfold to_nat in eq.
now apply N2Nat.inj.
Qed.
Lemma to_Z_inj {bound : N} (a b : BoundedN bound) :
to_Z a = to_Z b -> a = b.
Proof.
intros eq.
apply to_N_inj.
unfold to_Z in eq.
now apply N2Z.inj.
Qed.
Lemma of_to_N {bound : N} (n : BoundedN bound) :
of_N (to_N n) = Some n.
Proof.
destruct n as [n lt]; simpl.
unfold of_N.
destruct (N_lt_dec n bound).
- f_equal.
now apply to_N_inj.
- tauto.
Qed.
Lemma of_to_nat {bound : N} (n : BoundedN bound) :
of_nat (to_nat n) = Some n.
Proof.
unfold to_nat, of_nat.
rewrite N2Nat.id.
apply of_to_N.
Qed.
Lemma of_n_not_lt_0 (n : N) :
(Z.of_N n <? 0)%Z = false.
Proof.
destruct (Z.ltb_spec (Z.of_N n) 0).
- apply Zlt_not_le in H.
destruct (H (N2Z.is_nonneg n)).
- reflexivity.
Qed.
Lemma of_to_Z {bound : N} (n : BoundedN bound) :
of_Z (to_Z n) = Some n.
Proof.
unfold to_Z, of_Z.
rewrite of_n_not_lt_0.
rewrite N2Z.id.
apply of_to_N.
Qed.
Lemma of_N_some {bound : N} {m : N} {n : BoundedN bound} :
of_N m = Some n -> to_N n = m.
Proof.
intros H.
unfold of_N in H.
destruct (N_lt_dec m bound); prove.
Qed.
Lemma of_N_none {bound : N} {m : N} :
@of_N bound m = None -> m >= bound.
Proof.
intros H.
unfold of_N in H.
destruct (N_lt_dec m bound).
- inversion H.
- assumption.
Qed.
Lemma of_nat_some {bound : N} {m : nat} {n : BoundedN bound} :
of_nat m = Some n -> to_nat n = m.
Proof.
intros H.
unfold to_nat.
rewrite (of_N_some H).
apply Nat2N.id.
Qed.
Lemma of_nat_none {bound : N} {m : nat} :
@of_nat bound m = None -> N.of_nat m >= bound.
Proof. apply of_N_none. Qed.
Lemma in_map_of_nat (bound : N) (n : BoundedN bound) (xs : list nat) :
In n (map_option (@of_nat bound) xs) <-> In (to_nat n) xs.
Proof.
induction xs as [|x xs IH].
- split; intros H; inversion H.
- simpl.
destruct (of_nat x) eqn:of_nat_x; split; intros H.
+ destruct H.
* subst.
left.
symmetry.
now apply of_nat_some.
* tauto.
+ destruct H as [eq | Hin].
* left.
rewrite eq in of_nat_x.
rewrite of_to_nat in of_nat_x; prove.
* prove.
+ tauto.
+ destruct H as [eq | Hin].
* rewrite eq, of_to_nat in of_nat_x; inversion of_nat_x.
* prove.
Qed.
Module Stdpp.
Import countable.
Global Instance BoundedNEqDec {bound : N} : EqDecision (BoundedN bound) :=
eq_dec.
Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound).
Proof.
refine {| encode n := encode (proj1_sig n);
decode n := do n' <- (decode n : option N); _; |}.
Unshelve. all: cycle 1.
- destruct (N_lt_dec n' bound).
+ exact (Some (exist _ n' l)).
+ exact None.
- intros [x lt].
rewrite decode_encode.
simpl.
destruct (N_lt_dec x bound).
+ assert (lt = l) by (apply UIP_dec; decide equality).
now subst.
+ tauto.
Qed.
End Stdpp.
Program Instance BoundedN_equivalence {bound : N}
: OakTypeEquivalence (BoundedN bound) :=
{| serialize bn := serialize (countable.encode bn);
deserialize v :=
do p <- (deserialize v : option positive);
countable.decode p |}.
Next Obligation.
intros bound x.
simpl.
rewrite deserialize_serialize.
simpl.
now rewrite countable.decode_encode.
Qed.
Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
{| elements := map_option of_nat (List.seq 0 (N.to_nat bound)) |}.
Proof.
- pose proof (seq_NoDup (N.to_nat bound) 0) as nodup.
pose proof (in_seq (N.to_nat bound) 0) as in_seq'.
pose proof (fun n => proj1 (in_seq' n)) as in_seq; clear in_seq'.
induction nodup; try constructor.
simpl.
pose proof (in_seq x) as x_bound.
specialize (x_bound (or_introl eq_refl)).
destruct x_bound as [useless x_bound]; clear useless.
simpl in x_bound.
destruct (of_nat x) eqn:ofnatx. all: cycle 1.
apply of_nat_none in ofnatx.
lia.
constructor.
+ intros Hin.
apply in_map_of_nat in Hin.
apply of_nat_some in ofnatx.
rewrite <- ofnatx in H.
tauto.
+ apply IHnodup.
intros n in_n_l.
apply (in_seq n (or_intror in_n_l)).
- intros t.
apply in_map_of_nat.
apply in_seq.
unfold to_nat.
destruct t as [t lt].
simpl.
split; auto with *.
Qed.
End BoundedN.
Delimit Scope BoundedN_scope with BoundedN.
Bind Scope BoundedN_scope with BoundedN.
......@@ -2,76 +2,91 @@
chain implementing a chain type. More specifically, we show that the circulation
does not change during execution of blocks. This is proven under the (implicit)
assumption that the address space is finite. *)
From Coq Require Import List Permutation ZArith.
From SmartContracts Require Import Automation Blockchain Extras.
From Coq Require Import List Permutation ZArith Psatz.
From SmartContracts Require Import Automation Blockchain Extras Finite.
Import ListNotations.
Section Circulation.
Context {ChainBaseTypes : ChainBaseTypes}.
Context {Chain : ChainType}.
Context `{!FiniteAddressSpace Chain}.
Context `{Finite Address}.
Definition circulation (chain : Chain) :=
sumZ (account_balance chain) valid_addresses.
sumZ (account_balance chain) (elements Address).
(* We then prove that over any single step, the circulation is preserved.
The idea behind this proof is that addrs contain from and to so
we can move them to the beginning of the sum and it easily follows that
the sum of their balances is the same as before. For the rest of the
list the total balance will then not be affected which follows by induction. *)
Lemma transfer_reorganize
{pre post : Environment}
{act : InternalAction}
(transfer : Transfer act pre post)
: exists suf, Permutation ([iact_from act; iact_to act] ++ suf) valid_addresses.
Lemma address_reorganize {a b : Address} :
a <> b ->
exists suf, Permutation ([a; b] ++ suf) (elements Address).
Proof.
pose proof (valid_address_from transfer).
pose proof (valid_address_to transfer).
pose proof (from_neq_to transfer).
apply (NoDup_incl_reorganize _ [iact_from act; iact_to act]);
intros a_neq_b.
apply (NoDup_incl_reorganize _ [a; b]);
repeat constructor; unfold incl; prove.
Qed.
Lemma act_circulation_unchanged
Lemma step_from_to_same
{pre post : Environment}
{act : InternalAction}
(transfer : Transfer act pre post) :
{act : ExternalAction}
{new_acts : list ExternalAction}
(step : ChainStep pre post act new_acts) :
step_from step = step_to step ->
circulation post = circulation pre.
Proof.
intros from_eq_to.
unfold circulation.
destruct (transfer_reorganize transfer) as [suf perm].
induction (elements Address) as [| x xs IH].
- reflexivity.
- simpl.
rewrite IH, (account_balance_post step), from_eq_to.
lia.
Qed.
Hint Resolve step_from_to_same.
Lemma step_circulation_unchanged
{pre post : Environment}
{act : ExternalAction}
{new_acts : list ExternalAction}
(step : ChainStep pre post act new_acts) :
circulation post = circulation pre.
Proof.
destruct (address_eqb_spec (step_from step) (step_to step))
as [from_eq_to | from_neq_to]; eauto.
destruct (address_reorganize from_neq_to) as [suf perm].
apply Permutation_sym in perm.
unfold circulation.
rewrite 2!(sumZ_permutation perm); prove.
rewrite (account_balance_from_pre_post transfer).
rewrite (account_balance_to_pre_post transfer).
rewrite (account_balance_post_to step from_neq_to).
rewrite (account_balance_post_from step from_neq_to).
enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
pose proof (Permutation_NoDup perm valid_addresses_set) as perm_set.
assert (from_not_in_suf: ~In (iact_from act) suf).
{ apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
assert (to_not_in_suf: ~In (iact_to act) suf).
{ apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
pose proof (Permutation_NoDup perm) as perm_set.
assert (from_not_in_suf: ~In (step_from step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
assert (to_not_in_suf: ~In (step_to step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
clear perm perm_set.
pose proof (account_balance_unrelated_pre_post transfer).
pose proof (account_balance_post_irrelevant step).
induction suf as [| x xs IH]; prove.
Qed.
Hint Resolve act_circulation_unchanged.
Lemma step_circulation_unchanged
{pre post : Environment}
{x y : list InternalAction}
(step : ChainStep pre post x y) :
circulation post = circulation pre.
Proof. destruct step; eauto. Qed.
Hint Resolve step_circulation_unchanged.
(* Finally, we get the result over block traces by a simple induction. *)
Lemma block_trace_circulation_unchanged
{pre post : Environment}
{x y : list InternalAction}
{x y : list ExternalAction}
(trace : BlockTrace pre post x y)
: circulation post = circulation pre.
Proof. induction trace; prove; eauto. Qed.
Proof.
induction trace;
match goal with
| [IH: _ |- _] => try rewrite <- IH; eauto
end.
Qed.
End Circulation.
......@@ -13,7 +13,7 @@ Import ListNotations.
Import RecordSetNotations.
Section Congress.
Context {Chain : ChainType}.
Context {BaseTypes : ChainBaseTypes} {Chain : ChainType}.
Local Open Scope Z.
Set Primitive Projections.
......@@ -348,3 +348,5 @@ Theorem congress_no_unmatched_actions
(chain : Chain)
(
*)
End Congress.
......@@ -93,21 +93,3 @@ Proof.
rewrite app_assoc in nodup_l_app_m.
generalize in_or_app; prove.
Qed.
Section N.
Local Open Scope N.
Lemma N_lt_dec (p1 p2 : N) :
{p1 < p2} + {~(p1 < p2)}.
Proof.
unfold "<".
decide equality.
Qed.
Lemma N_lt_proofirrelevant (p1 p2 : N) (pf1 pf2 : p1 < p2) :
pf1 = pf2.
Proof.
apply UIP_dec.
decide equality.
Qed.
End N.
From Coq Require Import List.
Import ListNotations.
Class Finite (T : Type) :=
build_finite {
elements : list T;
elements_set : NoDup elements;
elements_all : forall (t : T), In t elements;
}.
Arguments elements _ {_}.
Arguments elements_set _ {_}.
Arguments elements_all _ {_}.
Hint Resolve elements_set elements_all.
......@@ -5,6 +5,7 @@ From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
From stdpp Require countable.
......@@ -12,43 +13,19 @@ From stdpp Require countable.
Import RecordSetNotations.
Import ListNotations.
(*
(* Very important we use < here because it is defined as a decidable equality. *)
Definition LCAddress := { n : N | n < 2^128 }%N.
Local Open Scope bool.
Module LCAddressCountable.
Import countable.
Section LocalBlockchain.
Let AddrSize : N := 2^128.
Instance LCAddress_countable : Countable LCAddress.
Proof.
refine {| encode n := encode (proj1_sig n);
decode n :=
do n' <- (decode n : option N);
_; |}.
Unshelve. all: cycle 1.
- destruct (N_lt_dec n' (2^128)%N).
+ exact (Some (exist _ n' l)).
+ exact None.
- intros x.
rewrite decode_encode.
destruct x as [x lt].
simpl.
destruct (N_lt_dec x (N.pos (2^128))).
+ rewrite (N_lt_proofirrelevant _ _ lt l).
reflexivity.
+ contradiction.
Qed.
End LCAddressCountable.
Definition lc_addr (n : N) : (if (n <? 2^128)%N then LCAddress else unit).
Proof.
unfold "<?"%N.
destruct (n ?= 2^128)%N eqn:n_comp.
- exact tt.
- exact (exist _ n n_comp).
- exact tt.
Qed.
*)
Instance LocalChainBaseTypes : ChainBaseTypes :=
{| Address := BoundedN AddrSize;
address_eqb := BoundedN.eqb;
address_eqb_spec := BoundedN.eqb_spec;
address_encode := countable.encode;
address_decode := countable.decode;
address_decode_encode := countable.decode_encode;
|}.
Record ChainUpdate :=
build_chain_update {
......@@ -78,7 +55,7 @@ Record LocalChain :=
Definition genesis_block : Block :=
{| block_header := {| block_number := 0;
block_coinbase := 0%N; |};
block_coinbase := BoundedN.of_Z_const AddrSize 0; |};
block_txs := [] |}.
Instance eta_local_chain : Settable _ :=
......@@ -128,9 +105,7 @@ Instance lc_type : ChainType :=
head_block := lc_head_block;
incoming_txs := lc_incoming_txs;
outgoing_txs := lc_outgoing_txs;
contract_state := lc_contract_state;
valid_address a := True;
|}.
contract_state := lc_contract_state; |}.
Definition lc_initial_chain : LocalChain :=
{| lc_blocks := [genesis_block];
......@@ -150,33 +125,42 @@ Record LocalChainBuilder :=
*)
}.
Definition initial_chain_builder : LocalChainBuilder :=
{| lcb_lc := lc_initial_chain;
lcb_contracts := FMap.empty |}.
Instance eta_local_chain_builder : Settable _ :=
mkSettable
((constructor build_local_chain_builder) <*> lcb_lc
<*> lcb_contracts)%settable.
Definition initial_chain_builder : LocalChainBuilder :=
{| lcb_lc := lc_initial_chain;
lcb_contracts := FMap.empty |}.
Definition lcb_env (lcb : LocalChainBuilder) : Environment :=
build_env lcb.(lcb_lc) (fun a => FMap.find a lcb.(lcb_contracts)).
Section ExecuteActions.
Context (initial_lcb : LocalChainBuilder).
Context (initial_lcb : LocalChainBuilder)
(initial_acts : list ExternalAction).
Local Coercion lcb_lc : LocalChainBuilder >-> LocalChain.
Local Coercion lcb_env : LocalChainBuilder >-> Environment.
Record ExecutionContext :=
build_execution_context {
new_iacts : list InternalAction;
block_txs : list Tx;
new_update : ChainUpdate;
recorded_iacts : list InternalAction;
cur_env : Environment;
acts_stack : list ExternalAction;
trace : BlockTrace initial_lcb cur_env initial_acts acts_stack;
}.
Instance eta_execution_context : Settable _ :=
mkSettable
((constructor build_execution_context) <*> new_iacts
((constructor build_execution_context) <*> block_txs
<*> new_update
<*> recorded_iacts)%settable.