Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
concordium
smartcontractinteractions
Commits
4e862e5a
Commit
4e862e5a
authored
Apr 26, 2019
by
Jakob Botsch Nielsen
Browse files
Prove an auxiliary lemma and clean up circulation proof
parent
b09772ad
Pipeline
#12147
passed with stage
in 5 minutes and 16 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
src/Blockchain.v
View file @
4e862e5a
...
...
@@ 42,7 +42,8 @@ Infix "=?" := address_eqb (at level 70) : address_scope.
Global
Ltac
destruct_address_eq
:=
repeat
match
goal
with

[

context
[(
?
a
=?
?
b
)
%
address
]]
=>
destruct
(
address_eqb_spec
a
b
)

[
H
:
context
[
address_eqb
?
a
?
b
]

_
]
=>
destruct
(
address_eqb_spec
a
b
)

[

context
[
address_eqb
?
a
?
b
]]
=>
destruct
(
address_eqb_spec
a
b
)
end
.
Section
Blockchain
.
...
...
@@ 819,6 +820,33 @@ Proof.

[
IH
:
_

_
]
=>
now
rewrite
IH
end
.
Qed
.
Ltac
rewrite_environment_equiv
:=
match
goal
with

[
H
:
EnvironmentEquiv
_
_

_
]
=>
rewrite
H
in
*
end
.
Ltac
destruct_step
:=
match
goal
with

[
H
:
ChainStep
_
_
_
_
_

_
]
=>
destruct
H
end
.
Lemma
contract_addr_format
{
to
to_queue
}
(
trace
:
ChainTrace
empty_env
[]
to
to_queue
)
(
addr
:
Address
)
(
wc
:
WeakContract
)
:
env_contracts
to
addr
=
Some
wc
>
address_is_contract
addr
=
true
.
Proof
.
intros
contract_at_addr
.
remember
empty_env
eqn
:
eq
.
induction
trace
;
rewrite
eq
in
*
;
clear
eq
;
try
rewrite_environment_equiv
;
cbn
in
*
;
auto
.

congruence
.

destruct_step
;
rewrite_environment_equiv
;
cbn
in
*
;
auto
.
destruct_address_eq
;
subst
;
auto
.
Qed
.
End
Theories
.
End
Trace
.
End
Semantics
.
...
...
src/Circulation.v
View file @
4e862e5a
...
...
@@ 42,7 +42,7 @@ Proof.
unfold
circulation
.
induction
(
elements
Address
)
as
[

x
xs
IH
].

reflexivity
.

simpl
in
*
.

cbn
in
*
.
rewrite
IH
,
(
account_balance_post
step
),
from_eq_to
.
lia
.
Qed
.
...
...
@@ 100,21 +100,20 @@ Proof.
pose
proof
(
Permutation_NoDup
perm
(
elements_set
Address
))
as
perm_set
.
unfold
circulation
.
rewrite
perm
.
simpl
.
cbn
.
unfold
constructor
,
set
,
account_balance
.
simpl
.
cbn
.
destruct
(
address_eqb_spec
baker
baker
);
try
congruence
.
simpl
.
pose
proof
(
in_NoDup_app
baker
[
baker
]
suf
ltac
:
(
prove
)
perm_set
)
as
not_in_suf
.
repeat
rewrite
<
Z
.
add_assoc
.
f_equal
.
rewrite
<
Z
.
add_comm
.
repeat
rewrite
<
Z
.
add_assoc
.
f_equal
.
cbn
.
match
goal
with

[

((
?
a

?
b
+
(
?
c
+
?
d
))
+
?
e
=
(
?
a

?
b
+
?
d
+
?
f
+
?
c
))
%
Z
]
=>
enough
(
e
=
f
)
by
lia
end
.
pose
proof
(
in_NoDup_app
baker
[
baker
]
suf
ltac
:
(
prove
)
perm_set
)
as
not_in_suf
.
clear
perm
perm_set
e
.
induction
suf
as
[

x
xs
IH
];
auto
.
simpl
in
*
.
cbn
in
*
.
apply
Decidable
.
not_or
in
not_in_suf
.
destruct
(
address_eqb_spec
x
baker
);
try
tauto
.
specialize
(
IH
(
proj2
not_in_suf
)).
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment