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
c3f21e1b
Commit
c3f21e1b
authored
Apr 25, 2019
by
Jakob Botsch Nielsen
Browse files
Prove that ChainStep and ChainTrace respect EnvironmentEquiv
parent
fa633115
Changes
2
Hide whitespace changes
Inline
Sidebyside
src/Blockchain.v
View file @
c3f21e1b
...
...
@@ 114,22 +114,6 @@ Next Obligation.
intros
x
y
z
[]
[];
apply
build_chain_equiv
;
congruence
.
Qed
.
Global
Instance
chain_equiv_header_proper
:
Proper
(
ChainEquiv
==>
eq
)
block_header
.
Proof
.
intros
x
y
.
apply
header_eq
.
Qed
.
Global
Instance
chain_equiv_incoming_txs_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
incoming_txs
.
Proof
.
intros
x
y
eq
a
b
eq
'
;
subst
;
apply
incoming_txs_eq
;
assumption
.
Qed
.
Global
Instance
chain_equiv_outgoing_txs_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
outgoing_txs
.
Proof
.
intros
x
y
eq
a
b
eq
'
;
subst
;
apply
outgoing_txs_eq
;
assumption
.
Qed
.
Global
Instance
chain_equiv_blocks_backes_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
blocks_baked
.
Proof
.
intros
x
y
eq
a
b
eq
'
;
subst
;
apply
blocks_baked_eq
;
assumption
.
Qed
.
Global
Instance
chain_equiv_contract_state_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
contract_state
.
Proof
.
intros
x
y
eq
a
b
eq
'
;
subst
;
apply
contract_state_eq
;
assumption
.
Qed
.
Section
Accessors
.
Local
Open
Scope
Z
.
...
...
@@ 147,6 +131,35 @@ Definition contract_deployment (chain : Chain) (addr : Address)
find_first
to_dep
(
incoming_txs
chain
addr
).
End
Accessors
.
Section
Theories
.
Ltac
rewrite_chain_equiv
:=
match
goal
with

[
H
:
ChainEquiv
_
_

_
]
=>
rewrite
H
end
.
Global
Instance
chain_equiv_header_proper
:
Proper
(
ChainEquiv
==>
eq
)
block_header
.
Proof
.
repeat
intro
;
auto
using
header_eq
.
Qed
.
Global
Instance
chain_equiv_incoming_txs_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
incoming_txs
.
Proof
.
repeat
intro
;
subst
;
auto
using
incoming_txs_eq
.
Qed
.
Global
Instance
chain_equiv_outgoing_txs_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
outgoing_txs
.
Proof
.
repeat
intro
;
subst
;
auto
using
outgoing_txs_eq
.
Qed
.
Global
Instance
chain_equiv_blocks_backes_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
blocks_baked
.
Proof
.
repeat
intro
;
subst
;
auto
using
blocks_baked_eq
.
Qed
.
Global
Instance
chain_equiv_contract_state_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
contract_state
.
Proof
.
repeat
intro
;
subst
;
auto
using
contract_state_eq
.
Qed
.
Global
Instance
chain_equiv_account_balance_proper
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
account_balance
.
Proof
.
repeat
intro
;
subst
;
unfold
account_balance
;
now
rewrite_chain_equiv
.
Qed
.
Global
Instance
chain_equiv_contract_deployment
:
Proper
(
ChainEquiv
==>
eq
==>
eq
)
contract_deployment
.
Proof
.
repeat
intro
;
subst
;
unfold
contract_deployment
;
now
rewrite_chain_equiv
.
Qed
.
End
Theories
.
Record
ContractCallContext
:=
build_ctx
{
(
*
Address
sending
the
funds
*
)
...
...
@@ 203,20 +216,30 @@ Definition wc_version (wc : WeakContract) : Version :=
Definition
wc_init
(
wc
:
WeakContract
)
:=
let
(
_
,
i
,
_
,
_
,
_
)
:=
wc
in
i
.
Definition
wc_init_proper
(
wc
:
WeakContract
)
:=
match
wc
return
Proper
(
ChainEquiv
==>
eq
==>
eq
==>
eq
)
(
wc_init
wc
)
with

build_weak_contract
_
_
ip
_
_
=>
ip
end
.
Global
Instance
wc_init_proper
:
Proper
(
eq
==>
ChainEquiv
==>
eq
==>
eq
==>
eq
)
wc_init
.
Proof
.
intros
wc
wc
'
eq
;
subst
wc
'
.
exact
(
match
wc
return
Proper
(
ChainEquiv
==>
eq
==>
eq
==>
eq
)
(
wc_init
wc
)
with

build_weak_contract
_
_
ip
_
_
=>
ip
end
).
Qed
.
Definition
wc_receive
(
wc
:
WeakContract
)
:=
let
(
_
,
_
,
_
,
r
,
_
)
:=
wc
in
r
.
Definition
wc_receive_proper
(
wc
:
WeakContract
)
:=
match
wc
return
Proper
(
ChainEquiv
==>
eq
==>
eq
==>
eq
==>
eq
)
(
wc_receive
wc
)
with

build_weak_contract
_
_
_
_
rp
=>
rp
end
.
Global
Instance
wc_receive_proper
:
Proper
(
eq
==>
ChainEquiv
==>
eq
==>
eq
==>
eq
==>
eq
)
wc_receive
.
Proof
.
intros
wc
wc
'
eq
;
subst
wc
'
.
exact
(
match
wc
return
Proper
(
ChainEquiv
==>
eq
==>
eq
==>
eq
==>
eq
)
(
wc_receive
wc
)
with

build_weak_contract
_
_
_
_
rp
=>
rp
end
).
Qed
.
Record
Action
:=
build_act
{
...
...
@@ 437,6 +460,42 @@ Definition set_contract_state (addr : Address) (state : OakValue) :=
update_chain
(
fun
c
=>
c
<
contract_state
::=
set_chain_contract_state
addr
state
>
).
Section
Theories
.
Ltac
solve_proper
:=
apply
build_env_equiv
;
[
apply
build_chain_equiv

];
cbn
;
repeat
intro
;
repeat
match
goal
with

[
H
:
EnvironmentEquiv
_
_

_
]
=>
rewrite
H
end
;
auto
.
Global
Instance
add_tx_proper
:
Proper
(
eq
==>
EnvironmentEquiv
==>
EnvironmentEquiv
)
add_tx
.
Proof
.
repeat
intro
;
subst
.
unfold
add_tx
,
add_tx_to_map
.
solve_proper
.
Qed
.
Global
Instance
add_contract_proper
:
Proper
(
eq
==>
eq
==>
EnvironmentEquiv
==>
EnvironmentEquiv
)
add_contract
.
Proof
.
repeat
intro
;
subst
.
unfold
add_contract
.
solve_proper
.
Qed
.
Global
Instance
set_contract_state_proper
:
Proper
(
eq
==>
eq
==>
EnvironmentEquiv
==>
EnvironmentEquiv
)
set_contract_state
.
Proof
.
repeat
intro
;
subst
.
unfold
set_contract_state
,
update_chain
,
set_chain_contract_state
.
solve_proper
.
Qed
.
Section
Step
.
Local
Open
Scope
Z
.
(
*
Next
we
define
a
single
step
.
It
specifies
how
an
external
action
...
...
@@ 632,7 +691,8 @@ Definition initial_env :=
contract_state
a
:=
None
;
}
;
env_contracts
a
:=
None
;
}
.
(
*
The
chain
captures
that
an
environment
can
be
reached
with
some
current
actions
.
*
)
(
*
The
chain
captures
that
an
environment
can
be
reached
with
some
current
actions
queued
.
*
)
Inductive
ChainTrace
:
Environment
>
list
Action
>
Prop
:=

ctrace_initial
:
forall
(
env
:
Environment
),
...
...
@@ 670,6 +730,34 @@ Inductive ChainTrace : Environment > list Action > Prop :=
ChainTrace
env
acts
>
Permutation
acts
acts
'
>
ChainTrace
env
acts
'
.
Lemma
chain_step_respects_equiv
e1
e2
act
tx
e1
'
e2
'
new_acts
:
EnvironmentEquiv
e1
e2
>
EnvironmentEquiv
e1
'
e2
'
>
ChainStep
e1
act
tx
e1
'
new_acts
>
ChainStep
e2
act
tx
e2
'
new_acts
.
Proof
.
Hint
Constructors
ChainStep
:
core
.
intros
eq
eq
'
step
.
destruct
step
;
rewrite
eq
,
eq
'
in
*
;
eauto
.
Qed
.
Lemma
chain_trace_respects_equiv
e1
e2
l
:
EnvironmentEquiv
e1
e2
>
ChainTrace
e1
l
>
ChainTrace
e2
l
.
Proof
.
intros
eq
trace
.
Hint
Resolve
ctrace_initial
ctrace_block
ctrace_step
:
core
.
Hint
Resolve
chain_step_respects_equiv
.
Hint
Extern
1
(
ChainTrace
?
env
_
)
=>
match
goal
with

[
H
:
Permutation
?
a
?
b

_
]
=>
apply
(
ctrace_permute
env
a
b
)
end
.
Hint
Extern
1
(
EnvironmentEquiv
_
_
)
=>
reflexivity
.
induction
trace
;
eauto
;
rewrite
eq
in
*
;
eauto
.
Qed
.
End
Theories
.
End
Semantics
.
Class
ChainBuilderType
:=
...
...
src/LocalBlockchain.v
View file @
c3f21e1b
...
...
@@ 484,10 +484,9 @@ Proof.
Hint
Resolve
validate_header_valid
validate_actions_valid
execute_steps_trace
add_new_block_header_equiv
ctrace_block
:
core
.
(
*
It
is
strange
that
this
is
necessary
..
*
)
Hint
Extern
1
(
EnvironmentEquiv
_
_
)
=>
reflexivity
.
ctrace_block
:
core
.
(
*
auto
does
not
pick
up
reflexivity
for
reflexive
relations
.
*
)
Hint
Extern
1
(
EnvironmentEquiv
_
_
)
=>
reflexivity
:
core
.
eauto
6.
Defined
.
...
...
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