Skip to content

Commit 0a7d342

Browse files
clarusclarus
committed
Split the Erc20.v file
1 parent 583cf30 commit 0a7d342

File tree

2 files changed

+188
-188
lines changed

2 files changed

+188
-188
lines changed

Diff for: ‎erc20.v renamed to ‎Common.v

+2-188
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
Require Import Coq.Lists.List.
2-
Require Import Coq.Strings.String.
1+
Require Export Coq.Lists.List.
2+
Require Export Coq.Strings.String.
33

44
Import ListNotations.
55

@@ -220,88 +220,6 @@ Module SmartContract.
220220
Arguments t : clear implicits.
221221
End SmartContract.
222222

223-
(** Here we give an application of our DSL above with a representation of a simplified version of
224-
an [ERC-20] smart contract. *)
225-
Module Erc20.
226-
(** The init parameters are a name and a symbol for the token we are creating. They do not play
227-
any role in the computations, but are there in the ERC-20 of OpenZeppelin that we study. *)
228-
Definition InitInput : Set :=
229-
string * string.
230-
231-
(** The init outputs a new token kind *)
232-
Definition InitOutput : Set :=
233-
TokenKind.
234-
235-
(** The state of the contract is just the name and the symbol of its token. The token balance for
236-
each user is stored in the global world and we do not have to handle it here. *)
237-
Module State.
238-
Record t : Set := {
239-
name : string;
240-
symbol : string;
241-
}.
242-
End State.
243-
244-
(** The commands representing the entrypoints of our smart contract, with the type of their
245-
output. *)
246-
Module Command.
247-
Inductive t {token_kind : InitOutput} : Set -> Set :=
248-
| BalanceOf : User -> t (TokenQuantity token_kind)
249-
| GetAllowance : User -> User -> t (TokenQuantity token_kind)
250-
| Transfer : User -> TokenQuantity token_kind -> t unit
251-
| Approve (spender : User) (quantity : TokenQuantity token_kind) : t unit
252-
| Mint (account : User) (value : TokenQuantity token_kind) : t unit.
253-
Arguments t : clear implicits.
254-
End Command.
255-
256-
(** The definition of our ERC-20 smart contract *)
257-
Definition smart_contract :
258-
SmartContract.t
259-
InitInput
260-
InitOutput
261-
Command.t
262-
State.t :=
263-
{|
264-
(* The constructor function *)
265-
SmartContract.init _sender '(name, symbol) :=
266-
let! token_kind := M.MakeAction Action.CreateTokenKind in
267-
let state := {|
268-
State.name := name;
269-
State.symbol := symbol;
270-
|} in
271-
M.Pure (Some (token_kind, state));
272-
SmartContract.call A token_kind sender command state :=
273-
match command in Command.t _ A return M.t (option (A * _)) with
274-
(* The "balanceOf" entrypoint *)
275-
| Command.BalanceOf user =>
276-
(* We run the action to get the balance *)
277-
let! balance := M.MakeAction (Action.GetBalance token_kind user) in
278-
M.Pure (Some (balance, state))
279-
(* The "allowance" entrypoint *)
280-
| Command.GetAllowance user spender =>
281-
let! allowance := M.MakeAction (Action.GetAllowance token_kind user spender) in
282-
M.Pure (Some (allowance, state))
283-
(* The "transfer" entrypoint *)
284-
| Command.Transfer to value =>
285-
(* We run the action to make the transfer and to know if it succeeded *)
286-
let! is_success := M.MakeAction (Action.Transfer token_kind sender to value) in
287-
if is_success then
288-
M.Pure (Some (tt, state))
289-
else
290-
M.Pure None
291-
(* The "approve" entrypoint *)
292-
| Command.Approve spender value =>
293-
let! _ := M.MakeAction (Action.Approve token_kind sender spender value) in
294-
M.Pure (Some (tt, state))
295-
| Command.Mint account value =>
296-
let! is_success := M.MakeAction (Action.Mint token_kind account value) in
297-
if is_success then
298-
M.Pure (Some (tt, state))
299-
else
300-
M.Pure None
301-
end;
302-
|}.
303-
End Erc20.
304-
305223
(** Here we will define what it means for a smart contract defined in our DSL to be safe, in the
306224
sense that no one can steal money from others. *)
307225
Module NoStealing.
@@ -353,107 +271,3 @@ Module NoStealing.
353271
}.
354272
End InSmartContract.
355273
End NoStealing.
356-
357-
(** Now we will verify that our ERC-20 smart contract is safe *)
358-
Module Erc20IsSafe.
359-
(** Here is the specification saying that our smart contract is safe. It applies the predicate
360-
saying that a smart contract is safe to our definition of ERC-20. *)
361-
Lemma is_safe : NoStealing.InSmartContract.t Erc20.smart_contract.
362-
(** Here is the proof that the specification is correct. It should be executed in an IDE to see
363-
the proof state as we progress line by line.
364-
365-
The general idea is to go over all the possible execution scenarios of the smart contract,
366-
with the init, the "balanceOf", and the "transfer" entrypoints, and to prove that they are all
367-
safe.
368-
*)
369-
Proof.
370-
constructor; intros; cbn.
371-
{ (* init *)
372-
destruct init_input as [name symbol].
373-
unfold NoStealing.InRun.t; cbn.
374-
destruct Primitives.create_token_kind.
375-
apply ActionTree.Forall.Let. {
376-
(* The init is safe because the action we make to create a new token kind is safe *)
377-
apply ActionTree.Forall.MakeAction.
378-
cbn.
379-
trivial.
380-
}
381-
apply ActionTree.Forall.Pure.
382-
}
383-
{ (* call *)
384-
destruct command.
385-
{ (* BalanceOf *)
386-
unfold NoStealing.InRun.t; cbn.
387-
apply ActionTree.Forall.Let. {
388-
(* The "balanceOf" entrypoint is safe because the action we make to get the balance of a
389-
user is safe *)
390-
apply ActionTree.Forall.MakeAction.
391-
cbn.
392-
trivial.
393-
}
394-
apply ActionTree.Forall.Pure.
395-
}
396-
{ (* GetAllowance *)
397-
cbn.
398-
unfold NoStealing.InActionTree.t.
399-
apply ActionTree.Forall.Let. {
400-
apply ActionTree.Forall.MakeAction.
401-
cbn.
402-
trivial.
403-
}
404-
apply ActionTree.Forall.Pure.
405-
}
406-
{ (* Transfer *)
407-
unfold NoStealing.InRun.t; cbn.
408-
(* We have two cases, depending on whether the transfer succeeded or not. In both cases we
409-
make a single transfer (or transfer attempt) with the right user for the source account,
410-
so this is safe.
411-
*)
412-
destruct Primitives.transfer; cbn.
413-
{ apply ActionTree.Forall.Let. {
414-
apply ActionTree.Forall.MakeAction.
415-
cbn.
416-
reflexivity.
417-
}
418-
apply ActionTree.Forall.Pure.
419-
}
420-
{ apply ActionTree.Forall.Let. {
421-
apply ActionTree.Forall.MakeAction.
422-
cbn.
423-
reflexivity.
424-
}
425-
apply ActionTree.Forall.Pure.
426-
}
427-
}
428-
{ (* Approve *)
429-
cbn.
430-
apply ActionTree.Forall.Let. {
431-
apply ActionTree.Forall.MakeAction.
432-
cbn.
433-
trivial.
434-
}
435-
apply ActionTree.Forall.Pure.
436-
}
437-
{ (* Mint *)
438-
unfold NoStealing.InRun.t; cbn.
439-
destruct Primitives.mint.
440-
{ cbn.
441-
apply ActionTree.Forall.Let. {
442-
apply ActionTree.Forall.MakeAction.
443-
cbn.
444-
trivial.
445-
}
446-
apply ActionTree.Forall.Pure.
447-
}
448-
{ cbn.
449-
apply ActionTree.Forall.Let. {
450-
apply ActionTree.Forall.MakeAction.
451-
cbn.
452-
trivial.
453-
}
454-
apply ActionTree.Forall.Pure.
455-
}
456-
}
457-
}
458-
Qed.
459-
End Erc20IsSafe.

Diff for: ‎Erc20.v

+186
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,186 @@
1+
Require Import FullSpecificationSmartContracts.Common.
2+
3+
(** Here we give an application of our DSL above with a representation of a simplified version of
4+
an [ERC-20] smart contract. *)
5+
6+
(** The init parameters are a name and a symbol for the token we are creating. They do not play
7+
any role in the computations, but are there in the ERC-20 of OpenZeppelin that we study. *)
8+
Definition InitInput : Set :=
9+
string * string.
10+
11+
(** The init outputs a new token kind *)
12+
Definition InitOutput : Set :=
13+
TokenKind.
14+
15+
(** The state of the contract is just the name and the symbol of its token. The token balance for
16+
each user is stored in the global world and we do not have to handle it here. *)
17+
Module State.
18+
Record t : Set := {
19+
name : string;
20+
symbol : string;
21+
}.
22+
End State.
23+
24+
(** The commands representing the entrypoints of our smart contract, with the type of their
25+
output. *)
26+
Module Command.
27+
Inductive t {token_kind : InitOutput} : Set -> Set :=
28+
| BalanceOf : User -> t (TokenQuantity token_kind)
29+
| GetAllowance : User -> User -> t (TokenQuantity token_kind)
30+
| Transfer : User -> TokenQuantity token_kind -> t unit
31+
| Approve (spender : User) (quantity : TokenQuantity token_kind) : t unit
32+
| Mint (account : User) (value : TokenQuantity token_kind) : t unit.
33+
Arguments t : clear implicits.
34+
End Command.
35+
36+
(** The definition of our ERC-20 smart contract *)
37+
Definition smart_contract :
38+
SmartContract.t
39+
InitInput
40+
InitOutput
41+
Command.t
42+
State.t :=
43+
{|
44+
(* The constructor function *)
45+
SmartContract.init _sender '(name, symbol) :=
46+
let! token_kind := M.MakeAction Action.CreateTokenKind in
47+
let state := {|
48+
State.name := name;
49+
State.symbol := symbol;
50+
|} in
51+
M.Pure (Some (token_kind, state));
52+
SmartContract.call A token_kind sender command state :=
53+
match command in Command.t _ A return M.t (option (A * _)) with
54+
(* The "balanceOf" entrypoint *)
55+
| Command.BalanceOf user =>
56+
(* We run the action to get the balance *)
57+
let! balance := M.MakeAction (Action.GetBalance token_kind user) in
58+
M.Pure (Some (balance, state))
59+
(* The "allowance" entrypoint *)
60+
| Command.GetAllowance user spender =>
61+
let! allowance := M.MakeAction (Action.GetAllowance token_kind user spender) in
62+
M.Pure (Some (allowance, state))
63+
(* The "transfer" entrypoint *)
64+
| Command.Transfer to value =>
65+
(* We run the action to make the transfer and to know if it succeeded *)
66+
let! is_success := M.MakeAction (Action.Transfer token_kind sender to value) in
67+
if is_success then
68+
M.Pure (Some (tt, state))
69+
else
70+
M.Pure None
71+
(* The "approve" entrypoint *)
72+
| Command.Approve spender value =>
73+
let! _ := M.MakeAction (Action.Approve token_kind sender spender value) in
74+
M.Pure (Some (tt, state))
75+
| Command.Mint account value =>
76+
let! is_success := M.MakeAction (Action.Mint token_kind account value) in
77+
if is_success then
78+
M.Pure (Some (tt, state))
79+
else
80+
M.Pure None
81+
end;
82+
|}.
83+
84+
(** Now we will verify that our ERC-20 smart contract is safe *)
85+
Module IsSafe.
86+
(** Here is the specification saying that our smart contract is safe. It applies the predicate
87+
saying that a smart contract is safe to our definition of ERC-20. *)
88+
Lemma is_safe : NoStealing.InSmartContract.t Erc20.smart_contract.
89+
(** Here is the proof that the specification is correct. It should be executed in an IDE to see
90+
the proof state as we progress line by line.
91+
92+
The general idea is to go over all the possible execution scenarios of the smart contract,
93+
with the init, the "balanceOf", and the "transfer" entrypoints, and to prove that they are all
94+
safe.
95+
*)
96+
Proof.
97+
constructor; intros; cbn.
98+
{ (* init *)
99+
destruct init_input as [name symbol].
100+
unfold NoStealing.InRun.t; cbn.
101+
destruct Primitives.create_token_kind.
102+
apply ActionTree.Forall.Let. {
103+
(* The init is safe because the action we make to create a new token kind is safe *)
104+
apply ActionTree.Forall.MakeAction.
105+
cbn.
106+
trivial.
107+
}
108+
apply ActionTree.Forall.Pure.
109+
}
110+
{ (* call *)
111+
destruct command.
112+
{ (* BalanceOf *)
113+
unfold NoStealing.InRun.t; cbn.
114+
apply ActionTree.Forall.Let. {
115+
(* The "balanceOf" entrypoint is safe because the action we make to get the balance of a
116+
user is safe *)
117+
apply ActionTree.Forall.MakeAction.
118+
cbn.
119+
trivial.
120+
}
121+
apply ActionTree.Forall.Pure.
122+
}
123+
{ (* GetAllowance *)
124+
cbn.
125+
unfold NoStealing.InActionTree.t.
126+
apply ActionTree.Forall.Let. {
127+
apply ActionTree.Forall.MakeAction.
128+
cbn.
129+
trivial.
130+
}
131+
apply ActionTree.Forall.Pure.
132+
}
133+
{ (* Transfer *)
134+
unfold NoStealing.InRun.t; cbn.
135+
(* We have two cases, depending on whether the transfer succeeded or not. In both cases we
136+
make a single transfer (or transfer attempt) with the right user for the source account,
137+
so this is safe.
138+
*)
139+
destruct Primitives.transfer; cbn.
140+
{ apply ActionTree.Forall.Let. {
141+
apply ActionTree.Forall.MakeAction.
142+
cbn.
143+
reflexivity.
144+
}
145+
apply ActionTree.Forall.Pure.
146+
}
147+
{ apply ActionTree.Forall.Let. {
148+
apply ActionTree.Forall.MakeAction.
149+
cbn.
150+
reflexivity.
151+
}
152+
apply ActionTree.Forall.Pure.
153+
}
154+
}
155+
{ (* Approve *)
156+
cbn.
157+
apply ActionTree.Forall.Let. {
158+
apply ActionTree.Forall.MakeAction.
159+
cbn.
160+
trivial.
161+
}
162+
apply ActionTree.Forall.Pure.
163+
}
164+
{ (* Mint *)
165+
unfold NoStealing.InRun.t; cbn.
166+
destruct Primitives.mint.
167+
{ cbn.
168+
apply ActionTree.Forall.Let. {
169+
apply ActionTree.Forall.MakeAction.
170+
cbn.
171+
trivial.
172+
}
173+
apply ActionTree.Forall.Pure.
174+
}
175+
{ cbn.
176+
apply ActionTree.Forall.Let. {
177+
apply ActionTree.Forall.MakeAction.
178+
cbn.
179+
trivial.
180+
}
181+
apply ActionTree.Forall.Pure.
182+
}
183+
}
184+
}
185+
Qed.
186+
End IsSafe.

0 commit comments

Comments
 (0)