Commit 478221dd authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Update for dev Coq

parent ad6bc95a
Pipeline #12079 passed with stage
in 5 minutes and 21 seconds
......@@ -467,10 +467,11 @@ Inductive ChainStep :
incoming_txs pre to = [] ->
act = build_act from (act_deploy amount wc setup) ->
tx = build_tx from to amount (tx_deploy (build_contract_deployment (wc_version wc) setup)) ->
wc.(wc_init)
(add_tx tx pre)
(build_ctx from to amount)
setup = Some state ->
wc_init
wc
(add_tx tx pre)
(build_ctx from to amount)
setup = Some state ->
EnvironmentEquiv
new_env
(set_contract_state to state (add_contract to wc (add_tx tx pre))) ->
......@@ -492,11 +493,12 @@ Inductive ChainStep :
contract_state pre to = Some prev_state ->
act = build_act from (act_transfer to amount) ->
tx = build_tx from to amount tx_empty ->
wc.(wc_receive)
(add_tx tx pre)
(build_ctx from to amount)
prev_state
None = Some (new_state, resp_acts) ->
wc_receive
wc
(add_tx tx pre)
(build_ctx from to amount)
prev_state
None = Some (new_state, resp_acts) ->
new_acts = map (build_act to) resp_acts ->
EnvironmentEquiv
new_env
......@@ -520,11 +522,12 @@ Inductive ChainStep :
contract_state pre to = Some prev_state ->
act = build_act from (act_call to amount msg) ->
tx = build_tx from to amount (tx_call msg) ->
wc.(wc_receive)
(add_tx tx pre)
(build_ctx from to amount)
prev_state
(Some msg) = Some (new_state, resp_acts) ->
wc_receive
wc
(add_tx tx pre)
(build_ctx from to amount)
prev_state
(Some msg) = Some (new_state, resp_acts) ->
new_acts = map (build_act to) resp_acts ->
EnvironmentEquiv
new_env
......
......@@ -70,7 +70,7 @@ Module BoundedN.
decide equality.
Qed.
Hint Resolve to_N_inj.
Hint Resolve to_N_inj : core.
Lemma eqb_spec {bound : N} (a b : BoundedN bound) :
Bool.reflect (a = b) (eqb a b).
......@@ -229,39 +229,54 @@ Module BoundedN.
decode_encode := decode_encode_bounded; |}.
End Stdpp.
Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
{| elements := map_option of_nat (List.seq 0 (N.to_nat bound)) |}.
Definition bounded_elements (bound : N) : list (BoundedN bound) :=
map_option of_nat (List.seq 0 (N.to_nat bound)).
Lemma bounded_elements_set (bound : N) :
NoDup (bounded_elements 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.
change ((bound ?= t) = Gt) with (bound > t) in lt.
lia.
unfold bounded_elements.
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)).
Qed.
Lemma bounded_elements_all (bound : N) :
forall a, In a (bounded_elements bound).
Proof.
unfold bounded_elements.
intros t.
apply in_map_of_nat.
apply in_seq.
unfold to_nat.
destruct t as [t lt].
simpl.
change ((bound ?= t) = Gt) with (bound > t) in lt.
lia.
Qed.
Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
{| elements := bounded_elements bound;
elements_set := bounded_elements_set bound;
elements_all := bounded_elements_all bound; |}.
End BoundedN.
Delimit Scope BoundedN_scope with BoundedN.
......
......@@ -50,7 +50,7 @@ Proof.
lia.
Qed.
Hint Resolve step_from_to_same.
Hint Resolve step_from_to_same : core.
Lemma step_circulation_unchanged
{pre : Environment}
......@@ -82,7 +82,7 @@ Proof.
induction suf as [| x xs IH]; prove.
Qed.
Hint Resolve step_circulation_unchanged.
Hint Resolve step_circulation_unchanged : core.
(* Finally, we get the result over block traces by a simple induction. *)
Lemma block_trace_circulation_unchanged
......@@ -98,7 +98,7 @@ Proof.
end.
Qed.
Hint Resolve block_trace_circulation_unchanged.
Hint Resolve block_trace_circulation_unchanged : core.
Lemma circulation_equal (c1 c2 : Chain) :
ChainEquiv c1 c2 -> circulation c1 = circulation c2.
......
......@@ -66,10 +66,11 @@ Module FMap.
End Theories.
End FMap.
Hint Resolve FMap.find_union_None.
Hint Resolve FMap.find_union_Some_l.
Hint Resolve FMap.find_add.
Hint Resolve FMap.find_add_ne.
Hint Resolve
FMap.find_union_None
FMap.find_union_Some_l
FMap.find_add
FMap.find_add_ne : core.
Instance empty_set_eq_dec : stdpp.base.EqDecision Empty_set.
Proof. decidable.solve_decision. Defined.
......
......@@ -12,4 +12,4 @@ Arguments elements _ {_}.
Arguments elements_set _ {_}.
Arguments elements_all _ {_}.
Hint Resolve elements_set elements_all.
Hint Resolve elements_set elements_all : core.
......@@ -27,8 +27,6 @@ Global Instance LocalChainBaseTypes : ChainBaseTypes :=
compute_block_reward n := 50%Z;
|}.
Compute LocalChainBaseTypes.
Record LocalChain :=
build_local_chain {
lc_header : BlockHeader;
......@@ -297,8 +295,7 @@ Section ExecuteActions.
intros exec.
unfold execute_action in exec.
destruct act as [from body].
Hint Resolve send_or_call_step.
Hint Resolve deploy_contract_step.
Hint Resolve send_or_call_step deploy_contract_step : core.
destruct body as [to amount|to amount msg|amount wc setup]; eauto.
Qed.
......@@ -310,7 +307,7 @@ Section ExecuteActions.
induction gas as [|gas IH]; intros acts lc lc_after exec.
- unfold execute_steps in exec.
destruct acts as [|x xs]; [|congruence].
Hint Constructors BlockTrace.
Hint Constructors BlockTrace : core.
replace lc_after with lc by congruence; auto.
- destruct acts as [|x xs]; simpl in *.
+ replace lc_after with lc by congruence; auto.
......@@ -416,7 +413,7 @@ Proof.
match goal with
| [H: context[execute_steps _ _ ?a] |- _] => remember a as lc_block_start
end.
Hint Resolve validate_header_valid execute_steps_trace.
Hint Resolve validate_header_valid execute_steps_trace : core.
apply (ctrace_block lc_initial prev_lc_end new_header baker actions lc_block_start lc);
eauto; clear validate.
......
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