Commit 931f7691 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Attempts with PackedCursorList

parent 391ccde6
Pipeline #12191 failed with stage
in 1 minute and 48 seconds
......@@ -12,6 +12,7 @@ src/LocalBlockchain.v
src/LocalBlockchainTests.v
src/Monads.v
src/Oak.v
src/Transport.v
-R vendor/record-update RecordUpdate
vendor/record-update/RecordSet.v
vendor/record-update/RecordUpdate.v
......@@ -185,3 +185,8 @@ Ltac solve_by_rewrite :=
match goal with
| [H: _ |- _] => now rewrite H
end.
Ltac solve_by_inversion :=
match goal with
| [H: _ |- _] => solve [inversion H]
end.
......@@ -4,11 +4,14 @@ From Coq Require Import Psatz.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
From Coq Require Import JMeq.
From Coq Require Import Program.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From SmartContracts Require Import CursorList.
From SmartContracts Require Import Transport.
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.
......@@ -802,6 +805,191 @@ Proof.
+ intuition.
Qed.
Definition ends_with_tx_from
(address : Address)
{from to}
(trace : ChainTrace from to) : Prop :=
match trace with
| clnil => False
| snoc _ evt =>
match evt with
| evt_step _ step _ =>
step_from step = address
| _ => False
end
end.
Definition ends_with_tx_to
(address : Address)
{from to}
(trace : ChainTrace from to) : Prop :=
match trace with
| clnil => False
| snoc _ evt =>
match evt with
| evt_step _ step _ =>
step_to step = address
| _ => False
end
end.
(*
Lemma exists_map_back state (trace : ChainTrace empty_state state) :
exists f,
match trace with
|
forall
*)
Ltac super_subst := repeat (subst; cbn in *).
(* With these definitions we can prove that if an outgoing transaction from a contract
appears in a trace, then there is a prefix that ended in a call to this contract.*)
Local Open Scope clist.
Lemma no_unprovoked_contract_txs state address (trace : PackedCursorList) :
packed_from trace = empty_state ->
packed_to trace = state ->
address_is_contract address = true ->
forall out_state (out_t : PackedCursorList),
out_t `prefix_of` trace /\ ends_with_tx_from address out_t ->
exists in_state (in_t : ChainTrace empty_state in_state),
in_t `prefix_of` out_t /\ ends_with_tx_to address in_t.
Proof.
intros addr_is_contract out_state out_t [out_prefix out_is_out].
remember empty_state eqn:eq.
induction trace; cbn in *; [|destruct_event].
- (* empty trace cannot end with address *)
destruct out_prefix as [suffix suffix_eq].
destruct out_t; try inversion out_is_out.
destruct suffix; inversion suffix_eq.
- (* block event so nothing relevant changed since previous. *)
apply prefix_of_snoc in out_prefix.
destruct out_prefix as [[]|[]]; super_subst; auto; solve_by_inversion.
- (* step event *)
match goal with
| [step: ChainStep _ _ _ _ |- _] => dependent destruction step
end.
+ (* step_empty, cannot be to contract, but can be from contract. *)
match goal with
| [tx : Tx |- _] => destruct (address_eqb_spec (tx_from tx) address); subst tx
end; super_subst.
* (* from = address, so out_t can potentially be entire trace. *)
apply prefix_of_snoc in out_prefix.
destruct out_prefix as [[]|[]]; [|super_subst; auto].
(* solved case where out_t is not full trace, so case where *)
(* it is remains. *)
apply IHtrace; try solve [super_subst; auto].
Show Proof.
destruct (address_eqb_spec from0 address).
*
destruct H; subst; cbn in *; subst.
dependent rewrite H in out_is_out.
dependent destruction out_t.
* inversion H.
dependent destruction H0.
subst.
rewrite H in out_is_out.
destruct out_t; cbn in *.
* tauto.
*
destruct out_prefix as [suffix suffix_eq].
destruct suffix; cbn in *.
+ rewrite <- suffix_eq in out_is_out; cbn in *; tauto.
+ apply prefix_of_snoc
*
(* trace is ctrace_block, cannot end with tx from contract so just apply IH *)
apply IHtrace; auto.
(* out_t must be a prefix of trace since it ends with TX from contract *)
destruct out_prefix as [suffix suffix_eq].
destruct suffix; cbn in *.
+ rewrite <- suffix_eq in out_is_out; cbn in *; tauto.
+ inversion suffix_eq.
match goal with
| [H: context[ctrace_block ?trace ?a ?b ?c] |- _] =>
change (ctrace_block trace a b c) with (trace ++ ctrace_block ctrace_refl a b c) in *
end.
destruct suffix.
change (ctrace_block trace _ _ _
debug auto.
Lemma no_unprovoked_contract_txs state address (trace : ChainTrace empty_state state) :
address_is_contract address = true ->
forall out_state (out_t : ChainTrace empty_state out_state),
out_t `prefix_of` trace /\ ends_with_tx_from address out_t ->
exists in_state (in_t : ChainTrace empty_state in_state),
in_t `prefix_of` out_t /\ ends_with_tx_to address in_t.
Proof.
intros addr_is_contract out_state out_t [out_prefix out_is_out].
remember empty_state eqn:eq.
induction trace; cbn in *; [|destruct_event].
- (* empty trace cannot end with address *)
destruct out_prefix as [suffix suffix_eq].
destruct out_t; try inversion out_is_out.
destruct suffix; inversion suffix_eq.
- (* block event so nothing relevant changed since previous. *)
apply prefix_of_snoc in out_prefix.
destruct out_prefix as [[]|[]]; super_subst; auto; solve_by_inversion.
- (* step event *)
match goal with
| [step: ChainStep _ _ _ _ |- _] => dependent destruction step
end.
+ (* step_empty, cannot be to contract, but can be from contract. *)
match goal with
| [tx : Tx |- _] => destruct (address_eqb_spec (tx_from tx) address); subst tx
end; super_subst.
* (* from = address, so out_t can potentially be entire trace. *)
apply prefix_of_snoc in out_prefix.
destruct out_prefix as [[]|[]]; [|super_subst; auto].
(* solved case where out_t is not full trace, so case where *)
(* it is remains. *)
apply IHtrace; try solve [super_subst; auto].
Show Proof.
destruct (address_eqb_spec from0 address).
*
destruct H; subst; cbn in *; subst.
dependent rewrite H in out_is_out.
dependent destruction out_t.
* inversion H.
dependent destruction H0.
subst.
rewrite H in out_is_out.
destruct out_t; cbn in *.
* tauto.
*
destruct out_prefix as [suffix suffix_eq].
destruct suffix; cbn in *.
+ rewrite <- suffix_eq in out_is_out; cbn in *; tauto.
+ apply prefix_of_snoc
*
(* trace is ctrace_block, cannot end with tx from contract so just apply IH *)
apply IHtrace; auto.
(* out_t must be a prefix of trace since it ends with TX from contract *)
destruct out_prefix as [suffix suffix_eq].
destruct suffix; cbn in *.
+ rewrite <- suffix_eq in out_is_out; cbn in *; tauto.
+ inversion suffix_eq.
match goal with
| [H: context[ctrace_block ?trace ?a ?b ?c] |- _] =>
change (ctrace_block trace a b c) with (trace ++ ctrace_block ctrace_refl a b c) in *
end.
destruct suffix.
change (ctrace_block trace _ _ _
debug auto.
End Theories.
End Trace.
End Semantics.
......
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
From Coq Require Import Morphisms.
From Coq Require Import Program.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Containers.
From SmartContracts Require Import Automation.
From SmartContracts Require Import Extras.
From RecordUpdate Require Import RecordUpdate.
From Coq Require Import List.
......@@ -360,14 +361,157 @@ Proof. repeat intro; solve_contract_proper. Qed.
Definition contract : Contract Setup Msg State :=
build_contract version init init_proper receive receive_proper.
End Congress.
(*
(* This first property states that the Congress will only send out actions
to be performed if there is a matching CreateProposal somewhere in the
past. That is, no CreateProposal can lead to two batches of actions being
sent out, and the actions correspond to the ones passed in CreateProposal. *)
Theorem congress_no_unmatched_actions
(chain : Chain)
(
Section Theories.
Local Open Scope nat.
Definition num_proposed_congress_actions chain address :=
let extract tx :=
match tx_body tx with
| tx_call msg =>
match deserialize msg with
| Some (create_proposal acts) => length acts
| _ => 0
end
| _ => 0
end in
fold_right (fun tx n => n + extract tx) 0 (incoming_txs chain address).
Definition num_proposed_congress_actions_in_state chain address :=
match contract_state chain address >>= deserialize with
| Some state =>
fold_right (fun proposal n => n + length (actions proposal)) 0 (FMap.values (proposals state))
| None => 0
end.
Instance num_proposed_congress_actions_proper :
Proper (ChainEquiv ==> eq ==> eq) num_proposed_congress_actions.
Proof.
now repeat intro; subst; unfold num_proposed_congress_actions;
match goal with
| [H: ChainEquiv _ _ |- _] => rewrite H
end.
Qed.
Instance num_proposed_congress_actions_in_state_proper :
Proper (ChainEquiv ==> eq ==> eq) num_proposed_congress_actions_in_state.
Proof.
now repeat intro; subst; unfold num_proposed_congress_actions_in_state;
match goal with
| [H: ChainEquiv _ _ |- _] => rewrite H
end.
Qed.
Lemma num_proposed_congress_actions_unchanged c1 c2 address :
incoming_txs c1 address = incoming_txs c2 address ->
num_proposed_congress_actions c1 address = num_proposed_congress_actions c2 address.
Proof.
Admitted.
Lemma num_proposed_congress_actions_in_state_unchanged c1 c2 address :
incoming_txs c1 address = incoming_txs c2 address ->
num_proposed_congress_actions_in_state c1 address =
num_proposed_congress_actions_in_state c2 address.
Proof.
Admitted.
Local Open Scope trace.
Lemma trace_prefix_refl {e1 q1 e2 q2} {trace : ChainTrace e1 q1 e2 q2} :
trace `prefix_of` ctrace_refl -> trace ~= @ctrace_refl _ e1 q1.
Proof.
intros [suffix app_eq].
dependent destruction suffix; cbn in *; inversion app_eq; auto.
Qed.
Definition ends_with_tx_from
(address : Address)
{from from_queue to to_queue}
(trace : ChainTrace from from_queue to to_queue) : Prop :=
match trace with
| ctrace_step _ step => step_from step = address
| _ => False
end.
Definition ends_with_tx_to
(address : Address)
{from from_queue to to_queue}
(trace : ChainTrace from from_queue to to_queue) : Prop :=
match trace with
| ctrace_step _ step => step_to step = address
| _ => False
end.
Lemma matching_proposals env l address (trace : ChainTrace empty_env [] env l) :
forall out_env out_q (out_t : ChainTrace empty_env [] out_env out_q),
out_t `prefix_of` trace /\ ends_with_tx_from address out_t ->
exists in_env in_q (in_t : ChainTrace empty_env [] in_env in_q),
in_t `prefix_of` out_t /\ ends_with_tx_to address in_t.
Proof.
remember empty_env eqn:eq.
induction trace; intros out_env out_q out_t [out_prefix out_is_out].
- destruct out_prefix as [suffix suffix_eq].
destruct out_t; try inversion out_is_out.
dependent destruction suffix; inversion suffix_eq.
-
specialize (IHtrace eq).
dependent destruction out_t;
dependent destruction suffix; try inversion suffix_eq.
inversion out_is_out.
- Show Proof.
dependent destruction out_t; unfold EndsWithTxFrom in *;
try solve [inversion out_is_out].
destruct out_prefix.
+
pose proof (trace_prefix_refl out_prefix).
inversion H.
rewrite H in out_is_out.
{ dependent destruction out_t; auto.
rewrite (trace_prefix_refl out_prefix) in out_is_out.
inversion contract_out_prefix.
ChainTrace env l ->
env_contracts env address = Some (Congress.contract : WeakContract) ->
num_proposed_congress_actions_in_state env address +
length (outgoing_txs env address) <= num_proposed_congress_actions env address.
Proof.
intros trace congress_deployed.
Hint Resolve contract_addr_format.
assert (address_is_contract address = true) as addr_format
by eauto.
induction trace.
- now rewrite H.
- rewrite H1 in *; auto.
- destruct H.
+ rewrite H3 in *.
assert (incoming_txs (add_tx tx pre) address = incoming_txs pre address).
{
cbn.
unfold add_tx_to_map; destruct_address_eq; subst; cbn in *; congruence.
}
erewrite num_proposed_congress_actions_unchanged,
num_proposed_congress_actions_in_state_unchanged; try eassumption.
unfold num_proposed_congress_actions.
assert (incoming_txs (add_tx tx pre
unfold num_proposed_congress_actions, num_proposed_congress_actions_in_state.
unfold contract_state.
cbn.
unfold add_tx_to_map.
subst tx; cbn.
assert (address <> to) by (destruct (address_eqb_spec address to); congruence).
subst tx.
cbn in *.
subst tx.
cbn in *.
apply IHc.
- auto.
End Theories.
*)
End Congress.
......@@ -26,6 +26,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}.
......
......@@ -5,11 +5,24 @@ which must match with the previous element. For that reason this is
also a snoc list. Note that this is not unlike fhlist from CPDT,
except we place further restrictions on it. *)
From SmartContracts Require Import Automation.
From SmartContracts Require Import Transport.
From Coq Require Import JMeq.
From Coq Require Import Program.
From Coq Require Import List.
Import ListNotations.
Section List.
Definition list_prefix {A : Type} (prefix full : list A) :=
exists suffix, full = suffix ++ prefix.
End List.
Infix "`prefix_of`" := list_prefix (at level 70) : list_scope.
Section CursorList.
Context {cursor_type : Type} {elm_type : cursor_type -> cursor_type -> Type}.
Inductive CursorList : cursor_type -> cursor_type -> Type :=
| nil : forall {elm}, CursorList elm elm
| clnil : forall {elm}, CursorList elm elm
| snoc : forall {from mid to}, CursorList from mid -> elm_type mid to -> CursorList from to.
Definition snoc_eq
......@@ -25,30 +38,113 @@ Fixpoint clist_app
(xs : CursorList from mid)
(ys : CursorList mid to) : CursorList from to :=
match ys with
| nil => fun xs => xs
| clnil => fun xs => xs
| snoc ys' y => fun xs => snoc (clist_app xs ys') y
end xs.
Infix "++" := clist_app (right associativity, at level 60).
Definition clist_prefix
Definition clist_prefix_dep
{from mid to}
(prefix : CursorList from mid)
(full : CursorList from to) : Prop :=
exists suffix, full = prefix ++ suffix.
Definition clist_suffix
Definition clist_suffix_dep
{from mid to}
(suffix : CursorList mid to)
(full : CursorList from to) : Prop :=
exists prefix, full = prefix ++ suffix.
Infix "`prefix_of`" := clist_prefix (at level 70).
Infix "`suffix_of`" := clist_suffix (at level 70).
Infix "`prefix_of_dep`" := clist_prefix_dep (at level 70).
Infix "`suffix_of_dep`" := clist_suffix_dep (at level 70).
Section Packed.
Record PackedElement :=
build_packed_element {
pelm_from : cursor_type;
pelm_to : cursor_type;
pelm : elm_type pelm_from pelm_to;
}.
Arguments build_packed_element {_ _}.
Fixpoint is_chained (prev_from : cursor_type) (xs : list PackedElement) (from : cursor_type) : Prop :=
match xs with
| [] => prev_from = from
| x :: xs => prev_from = pelm_to x /\ is_chained (pelm_from x) xs from
end.
Fixpoint clist_to_packed_aux {from to} (xs : CursorList from to) : list PackedElement :=
match xs with
| clnil => []
| snoc xs x => build_packed_element x :: clist_to_packed_aux xs
end.
Lemma clist_to_packed_aux_wf {from to} (xs : CursorList from to) l :
clist_to_packed_aux xs = l -> is_chained to l from.
Proof.
revert from to xs.
induction l as [|p ps IH]; intros from to xs eq; cbn in *.
- destruct xs; auto; solve_by_inversion.
- destruct xs; inversion eq.
cbn in *.
split; auto.
match goal with
| [H: _ |- _] => now rewrite H; eauto
end.
Defined.
Record PackedCursorList :=
build_packed_clist {
packed_from : cursor_type;
packed_to : cursor_type;
packed_list : list PackedElement;
packed_list_wf : is_chained packed_to packed_list packed_from;
}.
Definition clist_to_packed
{from to}
(xs : CursorList from to) : PackedCursorList :=
{| packed_from := from;
packed_to := to;
packed_list := clist_to_packed_aux xs;
packed_list_wf := clist_to_packed_aux_wf xs _ eq_refl;
|}.
Fixpoint packed_to_clist_aux {from to ps} (wf : is_chained to ps from) {struct ps}
: CursorList from to.
Proof.
destruct ps as [|p ps']; cbn in *.
- subst; apply clnil.
- destruct wf as [wf_to_eq wf_prefix].
destruct p as [p_from p_to p].
cbn in *.
subst.
exact (snoc (packed_to_clist_aux _ _ _ wf_prefix) p).
Defined.
Definition packed_to_clist (ps : PackedCursorList)
: CursorList (packed_from ps) (packed_to ps) :=
packed_to_clist_aux (packed_list_wf ps).
Lemma clist_packed_iff {from to} :
inhabited (CursorList from to) <->
exists (ps : PackedCursorList), packed_from ps = from /\ packed_to ps = to.
Proof.
split.
- intros [xs].
exists (clist_to_packed xs).
auto.
- intros [ps [from_eq to_eq]]; subst.
constructor.
apply (packed_to_clist ps).
Qed.
End Packed.
Section Theories.
Lemma clist_app_nil_l {from to} (xs : CursorList from to) :
nil ++ xs = xs.
Lemma clist_app_clnil_l {from to} (xs : CursorList from to) :
clnil ++ xs = xs.
Proof. induction xs; auto; cbn; solve_by_rewrite. Qed.
Lemma clist_app_assoc
......@@ -58,27 +154,52 @@ Lemma clist_app_assoc
(zs : CursorList c3 c4) :
xs ++ ys ++ zs = (xs ++ ys) ++ zs.
Proof. induction zs; intros; auto; cbn; solve_by_rewrite. Qed.
End Theories.
Lemma prefix_of_app
Lemma prefix_of_dep_refl {from to} (xs : CursorList from to) :
xs `prefix_of_dep` xs.
Proof. now exists clnil. Qed.
Lemma prefix_of_dep_app
{from mid to to'}
{prefix : CursorList from mid}
{xs : CursorList from to}
{suffix : CursorList to to'} :
prefix `prefix_of` xs ->
prefix `prefix_of` xs ++ suffix.
prefix `prefix_of_dep` xs ->
prefix `prefix_of_dep` xs ++ suffix.
Proof.
intros [ex_suffix ex_suffix_eq_app].
exists (ex_suffix ++ suffix).
rewrite clist_app_assoc; congruence.
Qed.
Lemma prefix_of_snoc
{from mid mid' to}
(xs : CursorList from mid)
(ys : CursorList from mid')
(y : elm_type mid' to) :
xs `prefix_of_dep` snoc ys y ->
{ pf : mid = to & pf # xs = snoc ys y } \/
xs `prefix_of_dep` ys.
Proof.
intros is_prefix.
destruct is_prefix as [suffix suffix_app_eq].
destruct suffix; cbn in *.
- left. refine (existT _ eq_refl _); auto.
- right.
dependent destruction suffix_app_eq.
now exists suffix.
Qed.
End Theories.
End CursorList.
Delimit Scope clist_scope with trace.
Delimit Scope clist_scope with clist.
Bind Scope clist_scope with CursorList.
Infix "++" := clist_app (right associativity, at level 60) : clist_scope.
Infix "`prefix_of`" := clist_prefix (at level 70) : clist_scope.
Infix "`suffix_of`" := clist_suffix (at level 70) : clist_scope.
Infix "`prefix_of_dep`" := clist_prefix_dep (at level 70) : clist_scope.
Infix "`suffix_of_dep`" := clist_suffix_dep (at level 70) : clist_scope.
Arguments CursorList : clear implicits.
Hint Resolve prefix_of_dep_refl prefix_of_dep_app : core.
Definition transport {A : Type} {P : A -> Type} {a b : A} (p : a = b) : P a -> P b
:= fun a => match p with eq_refl => a end.
Notation "p # x" := (transport p x) (right associativity, at level 65).
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