-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcrowdfunding.v
1369 lines (1300 loc) · 50.5 KB
/
crowdfunding.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From mathcomp Require Import all_ssreflect.
From Michocoq Require Import semantics util macros.
Import syntax comparable error.
Require Import ccgen_util.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module crowdfunding(C : ContractContext).
Module semantics := Semantics C. Import semantics.
Require Import String.
Open Scope string_scope.
Open Scope michelson_scope.
Definition parameter_ty :=
or key_hash None
(or address None address None) None.
Definition storage_ty :=
(pair
(pair (set (* %raisers *) address) (map (* %refund_table *) address mutez))
(pair (pair (bool (* %withdrawn *)) (timestamp (* %funding_start *)))
(pair (timestamp (* %funding_end *)) (timestamp (* %unconditional_refund_start *))))).
Definition funding_start {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(timestamp ::: storage_ty ::: S) :=
{DUP; UNPAIR; DROP1; UNPAIR; UNPAIR; DROP1; DIP1 {DROP1}}.
Definition funding_end {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(timestamp ::: storage_ty ::: S) :=
{DUP; UNPAIR; DROP1; UNPAIR; DROP1; UNPAIR; DIP1 {DROP1}}.
Definition refund_table {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(map address mutez::: storage_ty ::: S) :=
{DUP; UNPAIR; DIP1 {DROP1}; UNPAIR; DROP1}.
Definition update_refund_table {self_type S} :
instruction_seq self_type false
(map address mutez::: storage_ty ::: S)
(storage_ty ::: S) :=
{SWAP; UNPAIR; UNPAIR; DIP1 {DROP1; SWAP}; PAIR; PAIR}.
Definition validate_contribute {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(storage_ty ::: S) :=
funding_start;;; {NOW; COMPARE; GE;
DIP1 funding_end; DIP1 {NOW; SWAP; COMPARE; GE}; AND; NOT;
IF_TRUE {FAILWITH} { }}.
Definition unconditional_refund_start {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(timestamp ::: storage_ty ::: S) :=
{DUP; UNPAIR; DROP1; UNPAIR; DROP1; UNPAIR; DROP1}.
Definition raisers {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(set address::: storage_ty ::: S) :=
{DUP; UNPAIR; DIP1 {DROP1}; UNPAIR; DIP1 {DROP1}}.
Definition withdrawn {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(bool ::: storage_ty ::: S) :=
{DUP; UNPAIR; DROP1; UNPAIR; DIP1 {DROP1}; UNPAIR; DIP1 {DROP1}}.
Definition set_withdrawn {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(storage_ty ::: S) :=
{UNPAIR; DIP1 {UNPAIR; UNPAIR; DROP1; PUSH bool True; PAIR; PAIR}; PAIR}.
Definition validate_withdraw {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(storage_ty ::: S) :=
funding_start;;; NOW;; SWAP;; COMPARE;; GE;;
{DIP1 funding_end; DIP1 {NOW; COMPARE; GE}; AND; NOT};;;
DIP1 {NOW; DIP1 unconditional_refund_start; SWAP; COMPARE; LE};;
@OR _ _ bitwise_bool _;; IF_TRUE {FAILWITH} { };;
withdrawn;;; IF_TRUE {FAILWITH} { };;
raisers;;; {SOURCE; @MEM _ _ _ (mem_set address) _;
NOT; IF_TRUE {FAILWITH} { }}.
Definition create_transfer {self_type S} :
instruction_seq self_type false
(mutez ::: address ::: storage_ty ::: S)
(operation ::: storage_ty ::: S) :=
{DIP1 {CONTRACT None unit}; SWAP;
IF_NONE {FAILWITH}
{SWAP; UNIT; TRANSFER_TOKENS}}.
Definition validate_refund {self_type S} :
instruction_seq self_type false
(storage_ty ::: S)
(storage_ty ::: S) :=
{NOW; DIP1 unconditional_refund_start; SWAP; COMPARE; GT};;;
IF_TRUE {FAILWITH} { };; withdrawn;;; {IF_TRUE {FAILWITH} { }}.
Definition crowdfunding : full_contract false parameter_ty None storage_ty :=
{DUP; CAR; DIP1 {CDR};
IF_LEFT
(IMPLICIT_ACCOUNT;;
ADDRESS;;
DUP;;
DIIP refund_table;;
DIP1 {@GET _ _ _ (get_map address mutez) _};;
DIP1 {IF_SOME {AMOUNT; @ADD _ _ _ add_tez_tez _} {AMOUNT}};;
DIP1 {SOME};;
DIIP refund_table;;
@UPDATE _ _ _ _ (update_map address mutez) _;;
DIP1 validate_contribute;; update_refund_table;;; {NIL operation; PAIR})
{IF_LEFT
(DIP1 validate_withdraw;;
BALANCE;;
create_transfer;;;
{NIL operation; SWAP; CONS; DIP1 set_withdrawn; PAIR})
{DIP1 refund_table; DUP; DIP1 {@GET _ _ _ (get_map address mutez) _}; SWAP;
IF_NONE {FAILWITH}
(SWAP;;
DIP1 {SWAP};;
NONE mutez;;
DIIP refund_table;;
SWAP;;
DUP;;
DIP1 {@UPDATE _ _ _ _ (update_map address mutez) _};;
DIIP validate_refund;;
DIP1 update_refund_table;;
DIP1 {SWAP};;
SWAP;;
create_transfer;;;
{NIL operation; SWAP; CONS; PAIR})}}}.
Local Definition geq a b :=
match BinInt.Z.compare a b with
| Gt | Eq => true
| _ => false
end.
Local Definition gt a b :=
match BinInt.Z.compare a b with
| Gt => true
| _ => false
end.
Import Notations.
Lemma crowdfunding_correct_contribute
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(refund_address : data key_hash)
(raisers : data (set address))
(refund_table : data (map address mutez))
(funding_start : data timestamp)
(funding_end : data timestamp)
(unconditional_refund_start : data timestamp)
(withdrawn : data bool)
(psi : stack (pair (list operation) storage_ty ::: [::]) -> Prop) :
let refund_amount x := map.get _ _ _
(address_ _ (implicit_account x)) in
let insert := map.insert address_constant tez.mutez address_compare
(compare_eq_iff address) (gt_trans address)
(Implicit refund_address) in
fuel > 5 ->
precond (eval_seq env crowdfunding fuel
(inl refund_address,
((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)) psi <->
let changed_refund_table :=
match refund_amount refund_address refund_table with
| Some x =>
let! z := tez.of_Z (BinInt.Z.add (tez.to_Z (amount env)) (tez.to_Z x)) in
Return (insert z refund_table)
| None =>
Return (insert (amount env) refund_table)
end in
precond changed_refund_table (fun t =>
geq (now env) funding_start /\ geq funding_end (now env)
/\ psi ([::],
((raisers, t),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)).
Proof.
move=> ra ins F; have<-: 6 + (fuel - 6) = fuel by rewrite addnC subnK.
rewrite /geq; subst ra ins; split.
+ rewrite eval_seq_precond_correct /eval_seq_precond /=.
set H := map.get _ _ _ _ _.
case: H => [a|].
- set T := tez.of_Z _.
case: T => //= T [] /negP/negP /andP[].
case: (BinInt.Z.compare (now env) funding_start) => //;
case: (BinInt.Z.compare funding_end (now env)) => //; auto.
- case=> [] /negP/negP /andP[] /=.
case: (BinInt.Z.compare (now env) funding_start) => //;
case: (BinInt.Z.compare funding_end (now env)) => //; auto.
+ rewrite eval_seq_precond_correct /eval_seq_precond /=.
set H := map.get _ _ _ _ _.
case: H => [a|/=].
- set T := tez.of_Z _.
case: T => //= T [] + [].
case: (BinInt.Z.compare (now env) funding_start) => //;
case: (BinInt.Z.compare funding_end (now env)) => //; auto;
(try by case);
(try by move=> + []).
- case => + [].
case: (BinInt.Z.compare (now env) funding_start) => //;
case: (BinInt.Z.compare funding_end (now env)) => //; auto;
(try by case);
(try by move=> + []).
Qed.
Lemma crowdfunding_fail_contribute
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(refund_address : data key_hash)
(raisers : data (set address))
(refund_table : data (big_map address mutez))
(funding_start : data timestamp)
(funding_end : data timestamp)
(unconditional_refund_start : data timestamp)
(withdrawn : data bool) :
fuel <= 5 ->
~~ success (eval_seq env crowdfunding fuel
(inl refund_address,
((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)).
Proof.
case: fuel => //.
repeat case => //.
rewrite /eval_seq /=.
case: (map.get _ _ _ _ ) => // a.
case: (tez.of_Z _) => //.
Qed.
Lemma crowdfunding_correct_withdraw
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(beneficiary : data address)
(raisers : data (set address))
(refund_table : data (big_map address mutez))
(funding_start : data timestamp)
(funding_end : data timestamp)
(unconditional_refund_start : data timestamp)
(withdrawn : data bool)
(psi : stack (pair (list operation) storage_ty ::: [::]) -> Prop) :
fuel > 7 ->
precond (eval_seq env crowdfunding fuel
(inr (inl beneficiary),
((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)) psi <->
geq funding_start (now env) /\ geq (now env) funding_end
/\ gt unconditional_refund_start (now env)
/\ withdrawn = false
/\ set.mem address_constant address_compare (source env) raisers
/\ exists y, contract_ None unit beneficiary = Some y
/\ psi ([:: transfer_tokens env unit tt (balance env) y],
(raisers, refund_table,
(true, funding_start, (funding_end, unconditional_refund_start))), tt).
Proof.
move=> F; have<-: 8 + (fuel - 8) = fuel by rewrite addnC subnK.
rewrite eval_seq_precond_correct /eval_seq_precond /=.
rewrite /gt /geq; split.
+ case => + [] + [].
case: (BinInt.Z.compare funding_start (now env)) => //;
case: (BinInt.Z.compare (now env) funding_end) => //;
by (rewrite /= BinInt.Z.compare_antisym;
case: (BinInt.Z.compare (now env) unconditional_refund_start) => // + + a *;
repeat split => //; auto; by move/negP/negP: a).
+ case=> + [] + [] + [] + [].
case: (BinInt.Z.compare funding_start (now env)) => // _;
case: (BinInt.Z.compare (now env) funding_end) => // _;
case: (BinInt.Z.compare unconditional_refund_start (now env)) => // _ *;
repeat split => //; auto; by apply/negP/negP.
Qed.
Lemma crowdfunding_fail_withdraw
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(beneficiary : data address)
(raisers : data (set address))
(refund_table : data (big_map address mutez))
(funding_start : data timestamp)
(funding_end : data timestamp)
(unconditional_refund_start : data timestamp)
(withdrawn : data bool) :
fuel <= 7 ->
~~ success (eval_seq env crowdfunding fuel
(inr (inl beneficiary),
((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)).
Proof.
case: fuel => //.
repeat case => //.
Qed.
Lemma crowdfunding_correct_refund
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(eligible_address : data address)
(raisers : data (set address))
(refund_table : data (big_map address mutez))
(funding_start : data timestamp)
(funding_end : data timestamp)
(unconditional_refund_start : data timestamp)
(withdrawn : data bool)
(psi : stack (pair (list operation) storage_ty ::: [::]) -> Prop) :
let remove := map.remove address_constant tez.mutez address_compare
(compare_eq_iff address) (lt_trans address) (gt_trans address) in
let get := map.get address_constant tez.mutez address_compare in
fuel > 7 ->
precond (eval_seq env crowdfunding fuel
(inr (inr eligible_address),
((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)) psi <->
exists y, get eligible_address refund_table = Some y
/\ geq (now env) unconditional_refund_start
/\ withdrawn = false
/\ (exists y0, contract_ None unit eligible_address = Some y0
/\ psi ([:: transfer_tokens env unit tt y y0],
(raisers, remove eligible_address refund_table,
(withdrawn, funding_start, (funding_end, unconditional_refund_start))), tt)).
Proof.
move=> rm get F; have<-: 8 + (fuel - 8) = fuel by rewrite addnC subnK.
rewrite eval_seq_precond_correct /eval_seq_precond /=.
subst rm get; rewrite /gt /geq; split.
+ case=> y [] H1 [] H2 [] H3 H4; exists y.
repeat split; auto.
rewrite /= BinInt.Z.compare_antisym.
by case: H2; case: (BinInt.Z.compare unconditional_refund_start (now env)); auto.
+ case=> y [] H1 [] H2 [] H3 H4; exists y.
repeat split; auto.
rewrite /= BinInt.Z.compare_antisym.
by case: H2; case: (BinInt.Z.compare (now env) unconditional_refund_start); auto.
Qed.
Lemma crowdfunding_fail_refund
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(eligible_address : data address)
(raisers : data (set address))
(refund_table : data (big_map address mutez))
(funding_start : data timestamp)
(funding_end : data timestamp)
(unconditional_refund_start : data timestamp)
(withdrawn : data bool) :
fuel <= 7 ->
~~ success (eval_seq env crowdfunding fuel
(inr (inr eligible_address),
((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)).
Proof.
case: fuel => //.
repeat case => //;
rewrite /eval_seq /=;
case: (map.get _ _ _ _ ) => //.
Qed.
(* 90 days = (60*60*24*90) seconds *)
Definition funding_start_latest :=
Comparable_constant _ (BinInt.Z_of_nat [Num of 7776000]
: simple_comparable_data int).
(* 270 days = (60*60*24*270) seconds *)
Definition funding_period_longest :=
Comparable_constant _ (BinInt.Z_of_nat [Num of 23328000]
: simple_comparable_data int).
(* 90 days = (60*60*24*90) seconds *)
Definition redeem_period_longest :=
Comparable_constant _ (BinInt.Z_of_nat [Num of 7776000]
: simple_comparable_data int).
Local Notation SUB := (@SUB _ _ _ sub_timestamp_timestamp _).
Local Notation OR := (@OR _ _ bitwise_bool _).
Definition validation_snippet :
instruction_seq None false (storage_ty ::: mutez ::: [::]) [::] :=
DIP1 {DROP1};;
raisers;;;
@SIZE _ _ (size_set _) _;;
PUSH _ (Comparable_constant _ (BinNums.N0 : simple_comparable_data nat));;
COMPARE;;
EQ;;
IF_TRUE {PUSH _ (Comparable_constant syntax_type.string "there must be at least one registered raiser"); FAILWITH} { };;
funding_start;;;
DIP1 {NOW};;
COMPARE;;
LT;;
DIP1 funding_end;;
DIIP funding_start;;
DIP1 {COMPARE; LT};;
OR;;
DIP1 unconditional_refund_start;;
DIIP funding_end;;
DIP1 {COMPARE; LT};;
OR;;
IF_TRUE {PUSH syntax_type.string (Comparable_constant syntax_type.string "timestamp parameters given in wrong order"); FAILWITH} { };;
funding_start;;;
NOW;;
SWAP;;
SUB;;
PUSH int funding_start_latest;;
SWAP;;
COMPARE;;
GT;;
IF_TRUE {PUSH syntax_type.string (Comparable_constant syntax_type.string "funding_start too late"); FAILWITH} { };;
funding_end;;;
DIP1 funding_start;;
SUB;;
PUSH int funding_period_longest;;
SWAP;;
COMPARE;;
GT;;
IF_TRUE {PUSH syntax_type.string (Comparable_constant syntax_type.string "funding period too long"); FAILWITH} { };;
unconditional_refund_start;;;
{DIP1 funding_end; SUB; PUSH int redeem_period_longest; SWAP; COMPARE; GT;
IF_TRUE {PUSH _ (Comparable_constant syntax_type.string "redeem period too long"); FAILWITH} { }; DROP1}.
Definition crowdfunding_genprog_validation_snippet :=
make_typed_validation_snippet validation_snippet.
Hypothesis new_env :
forall {N : self_info},
@proto_env N -> data (list operation) -> @proto_env N.
Hypothesis now_geq :
forall N env ops,
geq (now (@new_env N env ops)) (now env).
Section Composition.
Definition comp {tffB T U}
(N : self_info)
(env : @proto_env N)
(A : stack (pair (list operation) U ::: [::]))
(paramB : data T)
fuelB
(B : instruction_seq N tffB (pair T U :: [::])
(pair (list operation) U :: [::])) :=
let '(opsA, storage, tt) := A in
match eval_seq env B fuelB (paramB, storage, tt) with
| Return (opsB, storage, tt) =>
(new_env env opsB, (cat opsA opsB, storage, tt))
| Failed _ =>
(env, (opsA, storage, tt))
end.
Definition compN {tff T U N}
(I : instruction_seq N tff (pair T U :: [::])
(pair (list operation) U :: [::]))
xs env storage :=
foldr (fun b a => comp a.1 a.2 b.1 b.2 I) (env, ([::], storage, tt)) xs.
End Composition.
Inductive operation' :=
| TransferTokens : forall
(env : @proto_env (Some (parameter_ty, None)))
(m : tez.mutez)
(d : data (contract unit))
(da : data address), operation'.
Definition eval_seq_another
(env : @proto_env (Some (parameter_ty, None)))
(fuel : Datatypes.nat)
(A : stack (pair parameter_ty storage_ty ::: [::])) :=
let refund_amount x := map.get _ _ _
(address_ _ (implicit_account x)) in
let remove := map.remove address_constant tez.mutez address_compare
(compare_eq_iff address) (lt_trans address) (gt_trans address) in
let get := map.get address_constant tez.mutez address_compare in
let '((raisers, refund_table),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))) := A.1.2 in
match A.1.1 with
| inr (inr eligible_address) =>
match get eligible_address refund_table with
| Some y =>
match contract_ None unit eligible_address with
| Some y0 =>
if (7 < fuel) && geq (now env) unconditional_refund_start && (withdrawn == false)
then Return ([:: TransferTokens env y y0 eligible_address],
(raisers, remove eligible_address refund_table,
(withdrawn, funding_start, (funding_end, unconditional_refund_start))), tt)
else Failed _ Overflow
| None => Failed _ Overflow
end
| None => Failed _ Overflow
end
| inr (inl beneficiary) =>
match contract_ None unit beneficiary with
| None => Failed _ Overflow
| Some y =>
if (7 < fuel) && geq funding_start (now env) && geq (now env) funding_end
&& gt unconditional_refund_start (now env)
&& (set.mem address_constant address_compare (source env) raisers)
&& (withdrawn == false)
then Return ([:: TransferTokens env (balance env) y beneficiary],
(raisers, refund_table,
(true, funding_start, (funding_end, unconditional_refund_start))), tt)
else Failed _ Overflow
end
| inl refund_address =>
let insert := map.insert address_constant tez.mutez address_compare
(compare_eq_iff address) (gt_trans address)
(Implicit refund_address) in
let! t :=
match refund_amount refund_address refund_table with
| Some x =>
let! z := tez.of_Z (BinInt.Z.add (tez.to_Z (amount env)) (tez.to_Z x)) in
Return (insert z refund_table)
| None =>
Return (insert (amount env) refund_table)
end in
if (5 < fuel) && geq (now env) funding_start && geq funding_end (now env)
then Return ([::],
((raisers, t),
((withdrawn, funding_start),
(funding_end, unconditional_refund_start))), tt)
else Failed _ Overflow
end.
Local Definition conv (o : operation') :=
match o with
| TransferTokens env m d _ =>
transfer_tokens env unit tt m d
end.
Local Definition destination (o : operation') :=
match o with
| TransferTokens env m d da => da
end.
Lemma eval_seq_eq env fuel A :
success (eval_seq env crowdfunding fuel A) ->
eval_seq env crowdfunding fuel A =
let! (ops, storage, tt) := eval_seq_another env fuel A in
Return (seq.map conv ops, storage, tt).
Proof.
case: A => [][] op st [].
case: st => [][] raisers refund_table [][] withdrawn funding_start
[] funding_end unconditional_refund_start.
case: op => [refund_address|[beneficiary|eligible_address]] s.
+ have f5 : 5 < fuel.
rewrite ltnNge.
apply/negP => /(crowdfunding_fail_contribute
env refund_address raisers refund_table funding_start funding_end unconditional_refund_start withdrawn).
by rewrite s.
have: is_true (success (eval_seq env crowdfunding fuel (inl refund_address, (raisers, refund_table, (withdrawn, funding_start, (funding_end, unconditional_refund_start))), tt)))
by rewrite s.
rewrite success_precond crowdfunding_correct_contribute //= /eval_seq_another /=.
set B := match _ with | Some _ => _ | None => _ end .
case Beq : B => //= [][] Ha [] Hb _.
rewrite Ha Hb f5 return_precond crowdfunding_correct_contribute //.
subst B; rewrite Beq /=.
by auto.
+ have f7 : 7 < fuel.
rewrite ltnNge.
apply/negP => /(crowdfunding_fail_withdraw
env beneficiary raisers refund_table funding_start funding_end unconditional_refund_start withdrawn).
by rewrite s.
have: is_true (success (eval_seq env crowdfunding fuel (inr (inl beneficiary), (raisers, refund_table, (withdrawn, funding_start, (funding_end, unconditional_refund_start))), tt)))
by rewrite s.
rewrite success_precond crowdfunding_correct_withdraw //= /eval_seq_another /=.
case=> []a1 []a2 []a3 []a4 []a5 []y [] Hy _.
rewrite a1 a2 a3 a4 a5 f7 Hy return_precond crowdfunding_correct_withdraw //.
repeat split => //.
by exists y; auto.
+ have f7 : 7 < fuel.
rewrite ltnNge.
apply/negP => /(crowdfunding_fail_refund
env eligible_address raisers refund_table funding_start funding_end unconditional_refund_start withdrawn).
by rewrite s.
have: is_true (success (eval_seq env crowdfunding fuel (inr (inr eligible_address), (raisers, refund_table, (withdrawn, funding_start, (funding_end, unconditional_refund_start))), tt)))
by rewrite s.
rewrite success_precond crowdfunding_correct_refund //= /eval_seq_another /=.
case=> []y []Hy []a1 []a2 []y0 []Hy0 _.
rewrite Hy Hy0 a1 a2 f7 return_precond crowdfunding_correct_refund //.
exists y; repeat split => //.
exists y0; by auto.
Qed.
Lemma eval_seq_fail env fuel A :
~~ success (eval_seq env crowdfunding fuel A) <->
~~ success (eval_seq_another env fuel A).
Proof.
case: A => [][] op st [].
case: st => [][] raisers refund_table [][] withdrawn funding_start
[] funding_end unconditional_refund_start.
case: op => [refund_address|[beneficiary|eligible_address]];
split; apply/contra => s.
+ apply/Bool.Is_true_eq_true.
rewrite -/Is_true -/is_true success_precond.
have f5: 5 < fuel.
rewrite ltnNge.
apply/negP => f5.
move: s.
rewrite /eval_seq_another /= ltnNge f5 /=.
by case: (match _ with | Some _ => _ | None => _ end).
rewrite crowdfunding_correct_contribute //=.
move: s.
rewrite /eval_seq_another /=.
set B := (match _ with | Some _ => _ | None => _ end).
case Beq : B => //.
rewrite f5 /=.
case: (geq (now env) funding_start) => //.
by case: (geq funding_end (now env)).
+ apply/Bool.Is_true_eq_true.
rewrite -/Is_true -/is_true success_precond.
have f5: 5 < fuel.
rewrite ltnNge.
apply/negP => /(crowdfunding_fail_contribute
env refund_address raisers refund_table funding_start funding_end unconditional_refund_start withdrawn).
by rewrite s.
rewrite /eval_seq_another /= f5 /=.
move/Bool.Is_true_eq_left: s.
rewrite -/Is_true -/is_true success_precond crowdfunding_correct_contribute //=.
set B := (match _ with | Some _ => _ | None => _ end).
case Beq : B => //=.
case: (geq (now env) funding_start) => [|[]//].
by case: (geq funding_end (now env)) => [|[] _ []].
+ apply/Bool.Is_true_eq_true.
rewrite -/Is_true -/is_true success_precond.
have f7: 7 < fuel.
rewrite ltnNge.
apply/negP => f7.
move: s.
rewrite /eval_seq_another /= ltnNge f7 /=.
by case: (contract_ None unit beneficiary).
rewrite crowdfunding_correct_withdraw //=.
move: s.
rewrite /eval_seq_another /=.
case Ceq: (contract_ _ _ _) => [a|//].
rewrite f7 /=.
case: (geq funding_start (now env)) => //.
case: (geq (now env) funding_end) => //.
case: (gt unconditional_refund_start (now env)) => //.
case: (set.mem address_constant address_compare (source env) raisers) => //.
case: withdrawn => //= _.
repeat split => //.
by exists a.
+ apply/Bool.Is_true_eq_true.
rewrite -/Is_true -/is_true success_precond.
have f7: 7 < fuel.
rewrite ltnNge.
apply/negP => /(crowdfunding_fail_withdraw
env beneficiary raisers refund_table funding_start funding_end unconditional_refund_start withdrawn).
by rewrite s.
rewrite /eval_seq_another /= f7 /=.
move/Bool.Is_true_eq_left: s.
rewrite -/Is_true -/is_true success_precond crowdfunding_correct_withdraw //=.
by case=> []-> []-> []-> []-> []-> []y []-> _ /=.
+ apply/Bool.Is_true_eq_true.
rewrite -/Is_true -/is_true success_precond.
have f7: 7 < fuel.
rewrite ltnNge.
apply/negP => f7.
move: s.
rewrite /eval_seq_another /= ltnNge f7 /=.
case: (map.get _ _ _ _ _) => //.
by case: (contract_ _ _ _).
rewrite crowdfunding_correct_refund //=.
move: s.
rewrite /eval_seq_another /= f7 /=.
case Teq: (map.get _ _ _ _ _) => [t|//].
case Ceq: (contract_ _ _ _) => [a|//].
case: (geq (now env) unconditional_refund_start) => //.
case: withdrawn => //= _.
exists t; repeat split => //.
by exists a.
+ apply/Bool.Is_true_eq_true.
rewrite -/Is_true -/is_true success_precond.
have f7: 7 < fuel.
rewrite ltnNge.
apply/negP => /(crowdfunding_fail_refund
env eligible_address raisers refund_table funding_start funding_end unconditional_refund_start withdrawn).
by rewrite s.
rewrite /eval_seq_another /= f7 /=.
move/Bool.Is_true_eq_left: s.
rewrite -/Is_true -/is_true success_precond crowdfunding_correct_refund //=.
by case=> []x []-> []-> []-> []x0 []-> _.
Qed.
Definition comp_another
(env : @proto_env (Some (parameter_ty, None)))
(A : seq operation' * data storage_ty * Datatypes.unit)
(paramB : data parameter_ty)
fuelB :=
match eval_seq_another env fuelB (paramB, A.1.2, tt) with
| Return (opsB, storage, tt) =>
(new_env env (seq.map conv opsB), (cat A.1.1 opsB, storage, tt))
| Failed _ =>
(env, (A.1.1, A.1.2, tt))
end.
Definition compN_another xs env storage :=
foldr (fun b a => comp_another a.1 a.2 b.1 b.2) (env, ([::], storage, tt)) xs.
Lemma comp_eq env ops st paramB fuelB :
comp env (seq.map conv ops, st, tt) paramB fuelB crowdfunding
= let '(env, (ops, st, tt)) := comp_another env (ops, st, tt) paramB fuelB in
(env, (seq.map conv ops, st, tt)).
Proof.
rewrite /comp /comp_another.
set A := eval_seq_another _ _ _.
case Aeq : A => [|a].
have/eval_seq_fail: ~~ success A by rewrite Aeq.
by case: (eval_seq env crowdfunding fuelB (paramB, st, tt)).
set C := eval_seq env crowdfunding fuelB (paramB, st, tt).
have/eval_seq_eq: success C.
apply/negP => /negP /eval_seq_fail.
by subst A; rewrite Aeq.
subst C => ->.
subst A; rewrite Aeq.
case: a Aeq => [][] opsA st0 [] /= ?.
by rewrite map_cat.
Qed.
Lemma compN_eq env xs storage :
compN crowdfunding xs env storage
= let '(env, (ops, st, tt)) := compN_another xs env storage in
(env, (seq.map conv ops, st, tt)).
Proof.
elim: xs env storage => // x xs IH env storage.
rewrite /= !IH //=.
case: (compN_another xs env storage) => [] env0 [][] ops st [].
case s: (success (eval_seq env0 crowdfunding x.2 (x.1, st, tt))).
+ rewrite /= eval_seq_eq // /comp_another.
case: (eval_seq_another env0 x.2 (x.1, st, tt)) s => [//|] [][]? ? [].
by rewrite map_cat.
+ have: ~~ success (eval_seq_another env0 x.2 (x.1, st, tt))
by rewrite -eval_seq_fail s.
move: s => /=; rewrite /comp_another.
case: (eval_seq env0 crowdfunding x.2 (x.1, st, tt)) => //.
by case: (eval_seq_another env0 x.2 (x.1, st, tt)).
Qed.
Definition address_constant_eq a b :=
match a, b with
| Implicit (Mk_key_hash x), Implicit (Mk_key_hash y) => eqb x y
| Originated (Mk_smart_contract_address x),
Originated (Mk_smart_contract_address y) => eqb x y
| _, _ => false
end.
Lemma comparable_data_eqP :
Equality.axiom (address_constant_eq).
Proof.
case=> [][]x [][]y; apply/(iffP idP) => //= [];
(try by move/eqb_spec => ->);
by case=> ->; apply/eqb_spec.
Qed.
Canonical comparable_data_eqMixin := EqMixin comparable_data_eqP.
Canonical comparable_data_eqType :=
Eval hnf in EqType _ comparable_data_eqMixin.
Definition operation_constant_eq a b :=
match a, b with
| Mk_operation x, Mk_operation y => eqb x y
end.
Lemma operation_constant_eqP :
Equality.axiom operation_constant_eq.
Proof.
case=> []x []y; apply/(iffP idP) => /= [/eqb_spec -> //|[]->].
by apply/eqb_spec.
Qed.
Canonical operation_constant_eqMixin := EqMixin operation_constant_eqP.
Canonical operation_constant_eqType :=
Eval hnf in EqType (data operation) operation_constant_eqMixin.
Lemma size_crowdfunding_operations env x y z a b:
eval_seq_another env x (y, z, tt) = Return (a, b, tt) ->
seq.size a <= 1.
Proof.
rewrite /eval_seq_another.
case: y => [refund_address|[beneficiary|eligible_address]] /=.
+ case: z => [] [] ? ? [] [] ? ? [] ? ?.
case: (match _ with | Some _ => _ | None => _ end) => //= ?.
by case: ifP => // ? [] <-.
+ case: z => [] [] ? ? [] [] ? ? [] ? ?.
case: (contract_ None unit beneficiary) => // ?.
by case: ifP => // ? [] <-.
+ case: z => [] [] ? ? [] [] ? ? [] ? ?.
case: (map.get address_constant tez.mutez address_compare eligible_address _) => // ?.
case: (contract_ None unit _) => // ?.
by case: ifP => // ? [] <-.
Qed.
Lemma gt_geq_trans' a b c :
gt a b -> geq b c -> gt a c.
Proof.
move=> ab bc.
rewrite /gt.
case eq: (BinInt.Z.compare a c) => //.
+ move: eq.
rewrite BinInt.Z.compare_eq_iff => bceq.
rewrite {}bceq in ab, bc.
move: ab bc.
rewrite /gt /geq BinInt.Z.compare_antisym.
by case: (BinInt.Z.compare b c).
+ move: ab bc.
rewrite /gt /geq BinInt.Z.compare_antisym.
case eqab: (BinInt.Z.compare b a) => //.
rewrite BinInt.Z.compare_antisym.
case eqac: (BinInt.Z.compare c b) => //.
- move: eqac.
rewrite BinInt.Z.compare_eq_iff => eqcb.
rewrite eqcb in eq.
move: eq eqab.
rewrite BinInt.Z.compare_antisym.
by case: (BinInt.Z.compare b a).
- move: eq eqab eqac.
rewrite !BinInt.Z.compare_lt_iff => bc ab.
move: (BinInt.Z.lt_trans _ _ _ ab bc).
rewrite -!BinInt.Z.compare_lt_iff BinInt.Z.compare_antisym.
by case: (BinInt.Z.compare c b).
Qed.
Lemma geq_refl a : geq a a.
Proof.
rewrite /geq.
by rewrite BinInt.Z.compare_refl.
Qed.
Lemma pres_unconditional_refund_start xs env storage :
storage.2.2.2 = (compN_another xs env storage).2.1.2.2.2.2.
Proof.
elim: xs env storage => // x xs IH env storage.
rewrite /= /comp_another /=.
case eq: (eval_seq_another _ _ _) => [/=|[][] ops st []]; first by apply/IH.
have->: st.2.2.2 = (compN_another xs env storage).2.1.2.2.2.2.
case: x eq => [][|[]] x f.
+ rewrite /eval_seq_another /=.
case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (map.get address_constant tez.mutez address_compare _ _) => /= [z|].
case: (tez.of_Z _) => [//|a]/=.
by case: ifP => // ? [] ? <-.
by case: ifP => // ? [] ? [] <-.
+ rewrite /eval_seq_another /=.
case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (contract_ None unit _) => // ?.
by case: ifP => // ? [] ? <-.
+ rewrite /eval_seq_another /=.
case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (map.get _ _ _ _ _) => // ?.
case: (contract_ _ _ _) => // ?.
by case: ifP => // ? [] ? <-.
by apply/IH.
Qed.
Lemma pres_funding_end xs env storage :
storage.2.2.1 = (compN_another xs env storage).2.1.2.2.2.1.
Proof.
elim: xs env storage => // x xs IH env storage.
rewrite /= /comp_another /=.
case eq: (eval_seq_another _ _ _) => [/=|[][] ops st []]; first by apply/IH.
have->: st.2.2.1 = (compN_another xs env storage).2.1.2.2.2.1.
case: x eq => [][|[]] x f.
+ rewrite /eval_seq_another /=.
case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (map.get address_constant tez.mutez address_compare _ _) => /= [z|].
case: (tez.of_Z _) => [//|a]/=.
by case: ifP => // ? [] ? <-.
by case: ifP => // ? [] ? [] <-.
+ rewrite /eval_seq_another /=.
case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (contract_ None unit _) => // ?.
by case: ifP => // ? [] ? <-.
+ rewrite /eval_seq_another /=.
case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (map.get _ _ _ _ _) => // ?.
case: (contract_ _ _ _) => // ?.
by case: ifP => // ? [] ? <-.
by apply/IH.
Qed.
Lemma geq_gt a b :
geq a b -> ~~ gt b a.
Proof.
rewrite /geq /gt /= BinInt.Z.compare_antisym.
by case: (BinInt.Z.compare b a).
Qed.
Lemma geq_trans' : transitive geq.
Proof.
move=> a b c.
rewrite /geq /= BinInt.Z.compare_antisym.
case ab: (BinInt.Z.compare a b) => //.
move: ab.
by rewrite BinInt.Z.compare_eq_iff => ->.
rewrite BinInt.Z.compare_antisym.
case ac: (BinInt.Z.compare c a) => //.
move: ac.
rewrite BinInt.Z.compare_eq_iff => ->.
by rewrite BinInt.Z.compare_antisym ab.
move: ab ac.
rewrite !BinInt.Z.compare_lt_iff => ab bc.
move: (BinInt.Z.lt_trans _ _ _ bc ab).
by rewrite BinInt.Z.compare_antisym -BinInt.Z.compare_lt_iff => ->.
Qed.
Lemma compN_unconditional_refund_start xs env storage :
gt storage.2.2.2 (now (compN_another xs env storage).1) ->
(compN_another xs env storage).2.1.2.2.1.1 = false ->
(compN_another xs env storage).2.1.1 = [::].
Proof.
elim: xs env storage => // x xs IH env storage.
rewrite /= /comp_another /=.
case: x => [][refund_address|[beneficiary|eligible_address]] fuel;
rewrite /eval_seq_another /=.
+ case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (map.get address_constant tez.mutez address_compare _ _) => /= [z|].
case: (tez.of_Z _) => [e H1 H2|a]/=.
apply/IH => //.
by rewrite eq.
case: ifP => ? /= H1 H2; last
by apply/IH => //; rewrite eq.
rewrite IH ?eq //.
by apply/(gt_geq_trans' H1)/now_geq.
case: ifP => ? /= H1 H2; last
by apply/IH => //; rewrite eq.
rewrite /= cats0 IH ?eq //.
by apply/(gt_geq_trans' H1)/now_geq.
+ case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (contract_ None unit beneficiary) => [a H1 H2|??]; last
by apply/IH => //; rewrite eq.
case: ifP => H0; last first.
rewrite IH ?eq //.
apply/(gt_geq_trans' H1).
by rewrite H0 geq_refl.
by rewrite H0 /= in H2.
by rewrite H0 /= in H2.
+ case eq : (compN_another xs env storage).2.1.2 =>
[[]raisers refund_table
[][]withdrawn funding_start []
funding_end unconditional_refund_start].
case: (map.get _ _ _ _ _) => [|??]; last by apply/IH => //; rewrite eq.
case: (contract_ None unit eligible_address) => [??|???];
last by apply/IH => //; rewrite eq.
case: ifP => [H0|???]; last by apply/IH => //; rewrite eq.
have->: storage.2.2.2 = unconditional_refund_start
by rewrite (pres_unconditional_refund_start xs env storage) eq.
case/andP: H0 => [] /andP[] ? /geq_gt C1 ? C2.
by rewrite (gt_geq_trans' C2 (now_geq _ _)) in C1.
Qed.
Lemma mem_insert a b c d e f x y z:
Relations_1.Transitive (fun a0 b0 => c a0 b0 = Lt) ->
map.mem a b c x (map.insert a b c d e y f z) <->
c y x = Eq \/ map.mem a b c x z.
Proof.
move=> h; split => H1.
+ have H1' : is_true (map.mem a b c x (map.insert a b c d e y f z))
by rewrite H1.
case: (map.map_memget _ _ _ _ _ H1') => ? H2.
case cxy: (c y x); auto.
- rewrite map.get_insert_other // in H2.
* move: (map.map_getmem _ _ _ _ _ _ H2).
by case: (map.mem _ _ _ _ _); auto.
* by rewrite -d cxy.