Miles with expiration
This contract archetype manages the expiration date of a mile. An expired mile cannot be consumed and may be cleared out by the administrator.
A mille owner is identified by an address and possesses some miles. A mile is identified by a string id and has an expiration date. Every mile is possessed by one and only one owner:
basic model
A mile can be added and consumed if its expiration date is in the future.
A storage optimisation is added to the above model. A mile is augmented with a quantity value to gather several miles with the same expiration date. For example, 3 miles with the same expiration date are merged into one mile with the quantity value set to 3:
3 miles with same expiration date ...
... modeled as one mile with a quantity value
This optimisation comes with a cost of algorithmic complexity in the consume entry (line 74).
All entries are called by the admin role, which is ensured by security predicate g1 (line 120).
miles_with_expiration.arl
1
archetype miles_with_expiration
2
3
variable admin : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
4
5
(* id is a string because it is generated off-chain *)
6
asset mile identified by id {
7
id : string;
8
amount : int;
9
expiration : date
10
} with {
11
m1 : amount > 0;
12
}
13
14
(* a partition ensures there is no direct access to mile collection *)
15
asset owner identified by addr {
16
addr : role;
17
miles : partition<mile> = [] (* injective (owner x mile) *)
18
}
19
20
entry add (ow : address, newmile_id : string, newmile_amount : int, newmile_expiration : date) {
21
called by admin
22
23
require {
24
c1 : newmile_amount > 0;
25
}
26
27
failif {
28
c2 : mile.contains(newmile_id);
29
}
30
31
effect {
32
owner.addupdate (ow, { miles += [{id = newmile_id; amount = newmile_amount; expiration = newmile_expiration} ] })
33
}
34
}
35
36
entry consume (a : address, quantity : int) {
37
38
specification {
39
40
assert p1 {
41
remainder = 0
42
}
43
44
postcondition p2 {
45
mile.sum(the.amount) = before.mile.sum(the.amount) - quantity
46
invariant for loop {
47
0 <= remainder <= toiterate.sum(the.amount);
48
before.mile.sum(the.amount) = mile.sum(the.amount) + quantity - remainder
49
}
50
}
51
52
postcondition p3 {
53
forall m in removed.mile, m.expiration >= now
54
invariant for loop {
55
removed.mile.subsetof(by_expiration)
56
}
57
}
58
59
postcondition p4 {
60
added.mile.isempty()
61
invariant for loop {
62
added.mile.isempty()
63
}
64
}
65
}
66
67
called by admin
68
69
require {
70
r2 : quantity >= 0;
71
}
72
73
effect {
74
var by_expiration = owner[a].miles.sort(expiration).select(the.expiration > now);
75
dorequire (by_expiration.sum(the.amount) >= quantity);
76
var remainder = quantity;
77
for : loop m in by_expiration do
78
if remainder > 0
79
then (
80
if mile[m].amount > remainder
81
then (
82
mile.update(m, { amount -= remainder });
83
remainder := 0
84
)
85
else if mile[m].amount = remainder
86
then (
87
remainder := 0;
88
owner[a].miles.remove(m)
89
) else (
90
remainder -= mile[m].amount;
91
owner[a].miles.remove(m)
92
)
93
)
94
done;
95
assert p1
96
}
97
}
98
99
entry clear_expired () {
100
specification {
101
postcondition s3 {
102
forall m in removed.mile, m.expiration < now
103
invariant for loop2 {
104
forall m in removed.mile, m.expiration < now
105
}
106
}
107
}
108
109
called by admin
110
111
effect {
112
for : loop2 o in owner do
113
owner[o].miles.removeif(the.expiration < now)
114
done
115
}
116
}
117
118
security {
119
(* this ensures that any mile was added with the 'add' entry *)
120
g1 : only_by_role (anyentry, admin);
121
g2 : only_in_entry (remove (mile), [consume or clear_expired]);
122
g3 : not_in_entry (add (mile), consume);
123
g4 : no_storage_fail (add)
124
}
125
Copied!
Last modified 1yr ago
Export as PDF
Copy link