Commit 1b1c9908 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Prove a property for the Congress contract

This proves a concrete property about any Congress contract deployed to
a blockchain. More specifically, we show that the count of transactions
sent out by any Congress contract will always be less than or equal to
the total number of actions it has receive in "create proposal"
messages.
Thus, this property is stated only over the transactions going in and
out to the Congress contract.
To prove this, we reason over incoming and outgoing transactions, the
internal state of the congress and also the actions in the blockchain
queue.
parent 778c39f1
Pipeline #12212 failed with stage
in 22 seconds
......@@ -185,3 +185,14 @@ Ltac solve_by_rewrite :=
match goal with
| [H: _ |- _] => now rewrite H
end.
Ltac solve_by_inversion :=
match goal with
| [H: _ |- _] => solve [inversion H]
end.
Ltac specialize_hypotheses :=
repeat
match goal with
| [H: _ -> _ |- _] => specialize (H ltac:(auto))
end.
......@@ -661,6 +661,18 @@ Proof.
| [H: EnvironmentEquiv _ _ |- _] => now rewrite H
end.
Qed.
Lemma contracts_post_pre_none contract :
env_contracts post contract = None ->
env_contracts pre contract = None.
Proof.
intros H.
destruct step;
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
end; cbn in *; auto.
destruct_address_eq; congruence.
Qed.
End Theories.
End Step.
......@@ -778,6 +790,132 @@ Proof.
+ destruct_step; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
+ intuition.
Qed.
Lemma new_acts_no_out_queue addr1 addr2 new_acts resp_acts :
addr1 <> addr2 ->
new_acts = map (build_act addr2) resp_acts ->
Forall (fun a => (act_from a =? addr1)%address = false) new_acts.
Proof.
intros neq ?; subst.
induction resp_acts; cbn; auto.
constructor; destruct_address_eq; cbn in *; congruence.
Qed.
Ltac destruct_chain_event :=
match goal with
| [evt: ChainEvent _ _ |- _] => destruct evt
end.
Ltac destruct_chain_step :=
match goal with
| [step: ChainStep _ _ _ _ |- _] => destruct step
end.
Local Open Scope address.
(* This next lemma shows that any for a full chain trace,
the ending state will not have any queued actions from
undeployed contracts. *)
Lemma undeployed_contract_no_out_queue contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
address_is_contract contract = true ->
env_contracts state contract = None ->
Forall (fun act => (act_from act =? contract) = false) (chain_state_queue state).
Proof.
intros [trace] is_contract.
remember empty_state eqn:eq.
induction trace;
intros undeployed; rewrite eq in *; clear eq; cbn; auto.
destruct_chain_event; [|destruct_chain_step|];
try rewrite_environment_equiv;
repeat
match goal with
| [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
end;
cbn in *.
- (* New block *)
match goal with
| [H: Forall _ _ |- _] => induction H
end; constructor; auto.
destruct_address_eq; congruence.
- (* Transfer step, just use IH *)
eapply list.Forall_cons; eauto.
- (* Deploy step. First show that it is not to contract and then use IH. *)
destruct_address_eq; try congruence.
eapply list.Forall_cons; eauto.
- (* Call. Show that it holds for new actions as it is from *)
(* another contract, and use IH for remaining. *)
apply list.Forall_app.
assert (contract <> to) by congruence.
split; [eapply new_acts_no_out_queue|eapply list.Forall_cons]; eauto.
- (* Permutation *)
subst.
specialize_hypotheses.
match goal with
| [prev_eq_new: _ = _, perm: Permutation _ _ |- _] =>
now rewrite prev_eq_new in *; rewrite <- perm; auto
end.
Qed.
(* With this lemma proven, we can show that the (perhaps seemingly stronger)
fact, that an undeployed contract has no outgoing txs, holds. *)
Lemma undeployed_contract_no_out_txs contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
address_is_contract contract = true ->
env_contracts state contract = None ->
outgoing_txs state contract = [].
Proof.
intros [trace] is_contract.
remember empty_state eqn:eq.
induction trace;
intros undeployed; rewrite eq in *; clear eq; cbn; auto.
destruct_chain_event.
- (* New block *)
rewrite_environment_equiv; auto.
- (* In these steps we will use that the queue did not contain txs to the contract. *)
Hint Resolve contracts_post_pre_none : core.
pose proof
(undeployed_contract_no_out_queue
contract prev
ltac:(auto) ltac:(auto) ltac:(eauto)) as Hqueue.
destruct_chain_step; rewrite_environment_equiv;
repeat
match goal with
| [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
end;
subst;
subst tx;
inversion Hqueue;
cbn in *;
unfold add_tx_to_map;
inversion Hqueue;
subst;
cbn in *;
destruct_address_eq;
subst; try tauto; congruence.
- match goal with
| [H: _ = _ |- _] => rewrite H in *; auto
end.
Qed.
Lemma undeployed_contract_no_in_txs contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
address_is_contract contract = true ->
env_contracts state contract = None ->
incoming_txs state contract = [].
Proof.
intros [trace] is_contract.
remember empty_state eqn:eq.
induction trace; intros undeployed; rewrite eq in *; clear eq; cbn; auto.
destruct_chain_event.
- (* New block *)
rewrite_environment_equiv; auto.
- destruct_chain_step; rewrite_environment_equiv;
cbn in *;
unfold add_tx_to_map;
destruct_address_eq; auto; subst; congruence.
- match goal with
| [H: _ = _ |- _] => rewrite H in *; auto
end.
Qed.
End Theories.
End Trace.
......@@ -804,6 +942,7 @@ Class ChainBuilderType :=
}.
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
Global Coercion builder_env : builder_type >-> Environment.
End Blockchain.
Arguments version {_ _ _ _ _ _ _}.
......@@ -812,3 +951,23 @@ Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}.
Arguments ContractInterface {_} _ _ _.
Arguments build_contract_interface {_ _ _ _}.
Ltac destruct_chain_event :=
match goal with
| [evt: ChainEvent _ _ |- _] => destruct evt
end.
Ltac destruct_chain_step :=
match goal with
| [step: ChainStep _ _ _ _ |- _] => destruct step
end.
Ltac invert_chain_step :=
match goal with
| [step: ChainStep _ _ _ _ |- _] => inversion step
end.
Ltac rewrite_environment_equiv :=
match goal with
| [eq: EnvironmentEquiv _ _ |- _] => rewrite eq in *
end.
This diff is collapsed.
From Coq Require Import List.
From Coq Require Import ZArith.
From Coq Require Import Permutation.
From stdpp Require gmap.
From SmartContracts Require Import Monads.
From SmartContracts Require Import BoundedN.
From SmartContracts Require Import Automation.
Import ListNotations.
Notation FMap := gmap.gmap.
......@@ -26,6 +28,9 @@ Module FMap.
Notation alter := stdpp.base.alter.
Notation partial_alter := stdpp.base.partial_alter.
Definition values {K V : Type} `{countable.Countable K} (m : FMap K V) : list V :=
map snd (elements m).
Section Theories.
Context {K V : Type} `{countable.Countable K}.
......@@ -63,6 +68,45 @@ Module FMap.
k <> k' ->
find k' (partial_alter f k m) = find k' m.
Proof. apply fin_maps.lookup_partial_alter_ne. Qed.
Lemma find_empty k :
FMap.find k (FMap.empty : FMap K V) = None.
Proof. apply fin_maps.lookup_empty. Qed.
Lemma elements_add (m : FMap K V) k v :
find k m = None ->
Permutation (elements (add k v m)) ((k, v) :: elements m).
Proof. apply fin_maps.map_to_list_insert. Qed.
Lemma elements_empty : (elements empty : list (K * V)) = [].
Proof. now rewrite fin_maps.map_to_list_empty. Qed.
Lemma elements_add_empty (k : K) (v : V) :
FMap.elements (FMap.add k v FMap.empty) = [(k, v)].
Proof. now rewrite fin_maps.insert_empty, fin_maps.map_to_list_singleton. Qed.
Lemma add_remove (m : FMap K V) k v :
add k v (remove k m) = add k v m.
Proof. apply fin_maps.insert_delete. Qed.
Lemma remove_add (m : FMap K V) k v :
find k m = None ->
remove k (add k v m) = m.
Proof. apply fin_maps.delete_insert. Qed.
Lemma find_remove (m : FMap K V) k :
find k (remove k m) = None.
Proof. apply fin_maps.lookup_delete. Qed.
Lemma add_commute (m : FMap K V) (k k' : K) (v v' : V) :
k <> k' ->
FMap.add k v (FMap.add k' v' m) = FMap.add k' v' (FMap.add k v m).
Proof. apply fin_maps.insert_commute. Qed.
Lemma add_id (m : FMap K V) k v :
find k m = Some v ->
add k v m = m.
Proof. apply fin_maps.insert_id. Qed.
End Theories.
End FMap.
......
......@@ -33,18 +33,44 @@ Definition with_default {A : Type} (a : A) (o : option A) : A :=
| None => a
end.
Fixpoint sumZ {A : Type} (f : A -> Z) (xs : list A) : Z :=
match xs with
| [] => 0
| x :: xs' => f x + sumZ f xs'
end.
Fixpoint sumnat {A : Type} (f : A -> nat) (xs : list A) : nat :=
match xs with
| [] => 0
| x :: xs' => f x + sumnat f xs'
end.
Lemma sumnat_app
{A : Type} {f : A -> nat} {xs ys : list A} :
sumnat f (xs ++ ys) = sumnat f xs + sumnat f ys.
Proof.
revert ys.
induction xs as [| x xs IH]; intros ys; auto.
simpl.
rewrite IH.
lia.
Qed.
Lemma sumnat_permutation
{A : Type} {f : A -> nat} {xs ys : list A}
(perm_eq : Permutation xs ys) :
sumnat f xs = sumnat f ys.
Proof. induction perm_eq; perm_simplify; lia. Qed.
Instance sumnat_perm_proper {A : Type} {f : A -> nat} :
Proper (Permutation (A:=A) ==> eq) (sumnat f).
Proof. intros x y perm. now apply sumnat_permutation. Qed.
Lemma sumZ_permutation
{A : Type} {f : A -> Z} {xs ys : list A}
(perm_eq : Permutation xs ys) :
sumZ f xs = sumZ f ys.
Proof. induction perm_eq; prove. Qed.
Proof. induction perm_eq; perm_simplify; lia. Qed.
Instance sumZ_perm_proper {A : Type} {f : A -> Z} :
Proper (Permutation (A:=A) ==> eq) (sumZ f).
......@@ -138,3 +164,22 @@ Proof.
simpl.
lia.
Qed.
Lemma forall_respects_permutation {A} (xs ys : list A) P :
Permutation xs ys -> Forall P xs -> Forall P ys.
Proof.
intros perm all.
apply Forall_forall.
intros y y_in.
pose proof (proj1 (Forall_forall P xs) all).
apply H.
apply Permutation_in with ys; symmetry in perm; auto.
Qed.
Instance Forall_Permutation_proper {A} :
Proper (eq ==> @Permutation A ==> iff) (@Forall A).
Proof.
intros f f' ? xs ys perm.
subst f'.
split; apply forall_respects_permutation; auto; symmetry; auto.
Qed.
......@@ -506,14 +506,14 @@ Proof.
reflexivity.
Defined.
Global Instance lcb_chain_builder_type : ChainBuilderType :=
Global Instance LocalChainBuilderDepthFirst : ChainBuilderType :=
{| builder_type := LocalChainBuilder;
builder_initial := lcb_initial;
builder_env lcb := lcb_lc lcb;
builder_add_block := add_block true;
builder_trace := lcb_trace; |}.
Definition lcb_chain_builder_type_breadth_first : ChainBuilderType :=
Definition LocalChainBuilderBreadthFirst : ChainBuilderType :=
{| builder_type := LocalChainBuilder;
builder_initial := lcb_initial;
builder_env lcb := lcb_lc lcb;
......
......@@ -23,7 +23,7 @@ Section LocalBlockchainTests.
Definition person_3 : Address :=
BoundedN.of_Z_const AddrSize 13.
Definition ChainBuilder := builder_type.
Definition ChainBuilder := LocalChainBuilderDepthFirst.
Definition chain1 : ChainBuilder := builder_initial.
......@@ -36,9 +36,6 @@ Section LocalBlockchainTests.
| None => tt
end.
Local Coercion to_env (cb : ChainBuilder) : Environment :=
builder_env cb.
Compute (block_header chain1).
(* Baker mines an empty block (and gets some coins) *)
......@@ -180,3 +177,21 @@ Section LocalBlockchainTests.
Compute (account_balance chain8 person_3).
Print Assumptions chain8.
End LocalBlockchainTests.
Hint Resolve congress_txs_after_block.
(* The congress satisfies a property specialized to the local blockchain DFS: *)
Lemma congress_txs_after_local_chain_block
(prev new : LocalChainBuilderDepthFirst) baker acts slot finalization_height :
builder_add_block prev baker acts slot finalization_height = Some new ->
forall addr,
env_contracts new addr = Some (Congress.contract : WeakContract) ->
length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr.
Proof. eauto. Qed.
(* And of course, it is satisfied for the breadth first chain as well. *)
Lemma congress_txs_after_local_chain_bf_block
(prev new : LocalChainBuilderBreadthFirst) baker acts slot finalization_height :
builder_add_block prev baker acts slot finalization_height = Some new ->
forall addr,
env_contracts new addr = Some (Congress.contract : WeakContract) ->
length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr.
Proof. eauto. Qed.
Markdown is supported
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