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 action (line 39).
All actions are called by the admin role, which is ensured by security predicate s1 (line 109).
miles:with:expiration.arl
miles:with:expiration.mlw
miles:with:expiration.md
1
archetype miles_with_expiration
2
3
variable[%transferable%] admin : role = @tz1aazS5ms5cbGkb6FN1wvWmN7yrMTTcr6wB
4
5
(* id is a string because it is generated off-chain *)
6
asset mile identified by id sorted by expiration {
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 : mile partition = [] (* injective (owner x mile) *)
18
}
19
20
action add (ow : address, newmile : mile) {
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
action 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 mile.removed(), m.expiration >= now
54
invariant for loop {
55
mile.removed().subsetof(by_expiration)
56
}
57
}
58
59
postcondition p4 {
60
mile.added().isempty()
61
invariant for loop {
62
mile.added().isempty()
63
}
64
}
65
}
66
67
called by admin
68
69
require {
70
r2 : quantity >= 0;
71
}
72
73
effect {
74
let ow = owner.get(a) in
75
let by_expiration = ow.miles.select(the.expiration > now) in
76
require (by_expiration.sum(the.amount) >= quantity);
77
let remainder = quantity in
78
for : loop m in by_expiration do
79
if remainder > 0
80
then (
81
if m.amount > remainder
82
then (
83
mile.update(m.id, { amount -= remainder });
84
remainder := 0
85
)
86
else if m.amount = remainder
87
then (
88
remainder := 0;
89
ow.miles.remove(m.id)
90
) else (
91
remainder -= m.amount;
92
ow.miles.remove(m.id)
93
)
94
)
95
done;
96
assert p1
97
}
98
}
99
100
action clear_expired () {
101
specification {
102
postcondition s3 {
103
forall m in mile.removed(), m.expiration < now
104
invariant for loop2 {
105
forall m in mile.removed(), m.expiration < now
106
}
107
}
108
}
109
110
called by admin
111
112
effect {
113
for : loop2 o in owner do
114
o.miles.removeif (the.expiration < now)
115
done
116
}
117
}
118
119
security {
120
(* this ensures that any mile was added with the 'add' action *)
121
g1 : only_by_role (anyaction, admin);
122
g2 : only_in_action (remove (mile), [consume or clear_expired]);
123
g3 : not_in_action (add (mile), consume);
124
g4 : no_storage_fail (add)
125
}
Copied!
1
module Miles
2
3
use archetype.Lib
4
5
(* TRACES *)
6
7
type asset =
8
| Mile
9
| Owner
10
11
type entry =
12
| Add
13
| Consume
14
| ClearExpired
15
16
type field =
17
| Amount
18
| Expiration
19
| Miles
20
21
clone archetype.Trace as Tr with type asset = asset,
22
type entry = entry,
23
type field = field
24
25
(* for storage invariant initialisation *)
26
val function empty_mile_amounts : map int
27
val function empty_mile_expirations : map date
28
val function empty_owner_miles : map acol
29
axiom def_mile_amounts : forall m : key. empty_mile_amounts m > 0
30
31
type storage = {
32
mutable admin : role;
33
mutable miles : acol;
34
mutable mile_amounts : map int;
35
mutable mile_expirations : map date;
36
mutable owners : acol;
37
mutable owner_miles : map acol;
38
(* contract *)
39
mutable ops : transfers;
40
(* diff sets *)
41
mutable miles_added : acol;
42
mutable miles_removed : acol;
43
mutable owner_added : acol;
44
mutable owner_removed : acol;
45
(* traces *)
46
mutable tr : Tr.log;
47
mutable ename : option entry;
48
} invariant {
49
forall m : key. get mile_amounts m > 0
50
} by {
51
admin = 0;
52
miles = Nil;
53
mile_amounts = empty_mile_amounts;
54
mile_expirations = empty_mile_expirations;
55
owners = Nil;
56
owner_miles = empty_owner_miles;
57
ops = Nil;
58
miles_added = Nil;
59
miles_removed = Nil;
60
owner_added = Nil;
61
owner_removed = Nil;
62
tr = Nil;
63
ename = None;
64
}
65
66
(* getters *)
67
let get_mile (s : storage) (k : key) : key
68
raises { NotFound }
69
ensures { mem result s.miles }
70
= if not (mem k s.miles) then raise NotFound else k
71
72
let function get_amount (s : storage) (k : key) : int = get s.mile_amounts k
73
74
let function get_expiration (s : storage) (k : key) : date = get s.mile_expirations k
75
76
let get_owner (s : storage) (o : key) : key
77
raises { NotFound }
78
ensures { mem result s.owners }
79
= if not (mem o s.owners) then raise NotFound else o
80
81
(* Owner.miles is a partition of s.miles *)
82
axiom subset_miles : forall s : storage, o : key.
83
subset (get s.owner_miles o) s.miles
84
85
let function get_miles (s : storage) (o : key) : acol
86
ensures { subset result s.miles }
87
= get s.owner_miles o
88
89
90
clone archetype.Sum as Amounts with type storage = storage,
91
val f = get_amount
92
93
let remove_miles (o : key) (m : key) (s:storage) : unit
94
raises { NotFound }
95
requires { mem m s.miles }
96
requires { mem o s.owners }
97
ensures { forall x:key. mem x s.miles <-> (mem x (old s).miles /\ x <> m) }
98
ensures { forall x:key. mem x s.miles_removed <-> (mem x (old s).miles_removed \/ x = m) }
99
ensures { forall x:key. mem x (get_miles s o) <-> (mem x (get_miles (old s) o) /\ x <> m) }
100
ensures { Amounts.sum (old s) (old s).miles = Amounts.sum s s.miles + get_amount (old s) m }
101
=
102
s.miles <- remove m s.miles;
103
s.miles_removed <- add m s.miles_removed;
104
let miles = get_miles s o in
105
let new_owner_miles = remove m miles in
106
s.owner_miles <- set s.owner_miles o new_owner_miles
107
108
let add_miles (o : key) (m : key) (a : int) (e : date) (s : storage) : unit
109
raises { NotFound }
110
requires { mem o s.owners }
111
requires { not (mem m s.miles) }
112
requires { a > 0 }
113
ensures { forall x:key. mem x s.miles <-> (mem x (old s).miles \/ x = m) }
114
ensures { forall x:key. mem x s.miles_added <-> (mem x (old s).miles_added \/ x = m) }
115
ensures { Amounts.sum (old s) (old s).miles + a = Amounts.sum s s.miles }
116
=
117
s.miles <- add m s.miles;
118
s.miles_added <- add m s.miles_added;
119
s.mile_amounts <- set s.mile_amounts m a;
120
s.mile_expirations <- set s.mile_expirations m e;
121
let miles = get_miles s o in
122
let new_owner_miles = add m miles in
123
s.owner_miles <- set s.owner_miles o new_owner_miles
124
125
let set_amount (m : key) (a : int) (s : storage) : unit
126
requires { mem m s.miles }
127
requires { a > 0 }
128
ensures { Amounts.sum (old s) (old s).miles = Amounts.sum s s.miles - a + get_amount (old s) m }
129
ensures { (old s).miles = s.miles }
130
= s.mile_amounts <- set s.mile_amounts m a
131
132
let update_owner (o : key) (new_miles : acol) (s : storage) : unit
133
raises { NotFound }
134
=
135
if not (mem o s.owners) then raise NotFound;
136
s.owner_miles <- set s.owner_miles o new_miles
137
138
let addifnotexist (o : key) (new_miles : acol) (s : storage) : unit
139
raises { NotFound }
140
ensures { mem o s.owners }
141
=
142
if not (mem o s.owners)
143
then (
144
s.owners <- add o s.owners;
145
update_owner o new_miles s
146
)
147
148
(* Actions *****************************************************************)
149
150
let add (e : env) (s : storage) (ow : key) (m : key) (a : int) (ex : date) : transfers
151
raises { InvalidCaller, InvalidCondition, NotFound }
152
requires { not (mem m s.miles) }
153
=
154
if caller e <> s.admin then raise InvalidCaller;
155
if not (a > 0) then raise InvalidCondition;
156
addifnotexist ow Nil s;
157
add_miles ow m a ex s;
158
Contract.empty
159
160
(*let function test_consume (e : env) (s : storage) (a : key) : bool = get_expiration s a > now e
161
meta "rewrite_def" function test_consume
162
axiom tauto_test_consume: forall e : env, s : storage, a : key.
163
now e < get_expiration s a <-> test_consume e s a = true
164
165
clone archetype.Filter as FConsume with type storage = storage,
166
val test = test_consume*)
167
168
let rec function filter_consume (e : env) (s : storage) (c : acol) : acol
169
variant { c }
170
ensures { forall a : key. mem a result -> get_expiration s a > now e }
171
ensures { subset result c }
172
=
173
match c with
174
| Nil -> Nil
175
| Cons a tl ->
176
if get_expiration s a > now e
177
then Cons a (filter_consume e s tl)
178
else filter_consume e s tl
179
end
180
181
let consume (e : env) (s : storage) (owner : address) (nbmiles : int) : transfers
182
raises { NotFound, InvalidCaller, InvalidCondition }
183
requires { is_empty s.miles_removed }
184
requires { is_empty s.miles_added }
185
(* forall m : removed miles, m.expiration > now *)
186
ensures { forall m : key.
187
(*mem m (diff (old s).miles s.miles) -> get_expiration s m > (now e)*)
188
mem m s.miles_removed -> get_expiration s m > (now e)
189
}
190
(* mile.sum(quantity) = before miles.sum(quantity) - nbmiles *)
191
ensures { Amounts.sum (old s) (old s).miles = Amounts.sum s s.miles + nbmiles }
192
(* is_emtpy add.miles *)
193
ensures { is_empty s.miles_added }
194
= if caller e <> s.admin then raise InvalidCaller;
195
if nbmiles <= 0 then raise InvalidCondition;
196
let o = get_owner s owner in
197
let miles = get_miles s o in
198
let l = filter_consume e s miles in
199
(*let l = FConsume.filter e s miles in*)
200
if not (nbmiles <= Amounts.sum s l) then raise InvalidCondition;
201
let remainder = ref nbmiles in
202
try
203
for i = 0 to (length l) - 1 do
204
(* helps for the membership precondition of set_amount: *)
205
invariant { forall k : int. i <= k < length l -> mem (nth k l) s.miles }
206
(* removed miles are in l: *)
207
(*invariant { subset (diff (old s).miles s.miles) l }*)
208
invariant { subset s.miles_removed l }
209
(* remainder bounds: *)
210
invariant { 0 <= !remainder <= Amounts.part_sum s l i (length l) }
211
(* right amount spent invariant *)
212
invariant { Amounts.sum (old s) (old s).miles = Amounts.sum s s.miles + nbmiles - !remainder }
213
let m = nth i l in
214
if get_amount s m > !remainder
215
then
216
(set_amount m (get_amount s m - !remainder) s;
217
remainder := 0;
218
raise Break)
219
else if get_amount s m = !remainder
220
then
221
(remainder := 0;
222
remove_miles o m s;
223
raise Break)
224
else
225
(remainder := !remainder - get_amount s m;
226
remove_miles o m s)
227
done;
228
with Break -> assert { !remainder = 0 }; ()
229
end;
230
assert { !remainder = 0 };
231
Contract.empty
232
233
(* let function test_clear_expired (e : env) (s : storage) (a : key) : bool = get_expiration s a < now e
234
235
clone archetype.Filter as FClearexpired with type storage = storage,
236
val test = test_clear_expired*)
237
238
let rec function filter_clear_expired (e : env) (s : storage) (c : acol) : acol
239
variant { c }
240
ensures { forall a : key. mem a result -> get_expiration s a < now e }
241
ensures { subset result c }
242
=
243
match c with
244
| Nil -> Nil
245
| Cons a tl ->
246
if get_expiration s a < now e
247
then Cons a (filter_clear_expired e s tl)
248
else filter_clear_expired e s tl
249
end
250
251
let clear_expired (e : env) (s : storage) : transfers
252
raises { NotFound, InvalidCaller }
253
requires { is_empty s.miles_added }
254
requires { is_empty s.miles_removed }
255
ensures { forall m : key. mem m s.miles_removed -> get_expiration s m < now e }
256
= if caller e <> s.admin then raise InvalidCaller;
257
for i = 0 to (length s.owners)-1 do
258
invariant { forall m : key. mem m s.miles_removed -> get_expiration s m < now e }
259
let o = nth i s.owners in
260
let miles = get_miles s o in
261
let l = filter_clear_expired e s miles in
262
label Internal_loop in
263
for j = 0 to (length l) - 1 do
264
invariant { forall k : int. j <= k < length l -> mem (nth k l) s.miles }
265
invariant { forall m : key. mem m s.miles_removed <->
266
(mem m (s at Internal_loop).miles_removed \/ (exists k : int. 0 <= k < j /\ m = nth k l)) }
267
let m = nth j l in
268
remove_miles o m s;
269
done;
270
271
done;
272
Contract.empty
273
274
let all_entries (e : env) (s : storage)
275
(* add *)
276
(ow : key) (m : key) (a : int) (ex : date)
277
(* consume *)
278
(owner : address) (nbmiles : int)
279
(* clear expired *)
280
raises { NotFound, InvalidCaller, InvalidCondition }
281
requires { s.tr = Nil }
282
requires { s.ops = Nil }
283
(* any action is performed only by rome admin *)
284
ensures { forall ac : Tr.action, a : asset. Tr.performed_only_by_role e s.tr (Cons ac Nil) (Cons a Nil) (Cons s.admin Nil) }
285
(* remove miles is performed only by action (consome or clear_expired)*)
286
ensures { Tr.performed_only_by_action e s.tr (Cons Tr.Rm Nil) (Cons Mile Nil) (Cons Consume (Cons ClearExpired Nil)) }
287
(* add is not permformed by consume *)
288
=
289
match s.ename with
290
| Some Add ->
291
if caller e <> s.admin then raise InvalidCaller;
292
if not (a > 0) then raise InvalidCondition;
293
s.tr <- s.tr ++ Tr.mk_trace Add Owner Tr.Add;
294
s.tr <- s.tr ++ Tr.mk_trace Add Mile Tr.Add;
295
Contract.empty
296
| Some Consume ->
297
if caller e <> s.admin then raise InvalidCaller;
298
if nbmiles <= 0 then raise InvalidCondition;
299
let o = get_owner s owner in
300
let miles = get_miles s o in
301
let l = filter_consume e s miles in
302
if not (nbmiles <= Amounts.sum s l) then raise InvalidCondition;
303
let remainder = ref nbmiles in
304
try
305
for i = 0 to (length l) - 1 do
306
invariant { forall ac : Tr.action, a : asset. Tr.performed_only_by_role e s.tr (Cons ac Nil) (Cons a Nil) (Cons s.admin Nil) }
307
invariant { Tr.performed_only_by_action e s.tr (Cons Tr.Rm Nil) (Cons Mile Nil) (Cons Consume (Cons ClearExpired Nil)) }
308
let m = nth i l in
309
if get_amount s m > !remainder
310
then
311
(s.tr <- s.tr ++ Tr.mk_trace Consume Mile (Tr.Update Amount);
312
remainder := 0;
313
raise Break)
314
else if get_amount s m = !remainder
315
then
316
(remainder := 0;
317
s.tr <- s.tr ++ Tr.mk_trace Consume Mile Tr.Rm;
318
raise Break)
319
else
320
(remainder := !remainder - get_amount s m;
321
s.tr <- s.tr ++ Tr.mk_trace Consume Mile Tr.Rm)
322
done;
323
with Break -> ()
324
end;
325
Contract.empty
326
| Some ClearExpired ->
327
if caller e <> s.admin then raise InvalidCaller;
328
for i = 0 to (length s.owners)-1 do
329
invariant { forall ac : Tr.action, a : asset. Tr.performed_only_by_role e s.tr (Cons ac Nil) (Cons a Nil) (Cons s.admin Nil) }
330
invariant { Tr.performed_only_by_action e s.tr (Cons Tr.Rm Nil) (Cons Mile Nil) (Cons Consume (Cons ClearExpired Nil)) }
331
let o = nth i s.owners in
332
let miles = get_miles s o in
333
let l = filter_clear_expired e s miles in
334
for j = 0 to (length l) - 1 do
335
invariant { forall ac : Tr.action, a : asset. Tr.performed_only_by_role e s.tr (Cons ac Nil) (Cons a Nil) (Cons s.admin Nil) }
336
invariant { Tr.performed_only_by_action e s.tr (Cons Tr.Rm Nil) (Cons Mile Nil) (Cons Consume (Cons ClearExpired Nil)) }
337
let m = nth j l in
338
s.tr <- s.tr ++ Tr.mk_trace Consume Mile Tr.Rm
339
done;
340
341
done;
342
Contract.empty
343
| None -> Contract.empty
344
end
345
end
Copied!
1
# Miles with Expiration
2
> Genrated with [Archetype](https://archetype-lang.org/) v0.1 (2019-04-09)
3
## Roles
4
5
### Admin
6
7
| | |
8
|----------------|---|---|
9
|Address | |
10
|Extension | |
11
12
## Assets
13
### Mile
14
15
| Field | Desc | Type | Attribute |
16
|--|--|--|--|
17
| id | | string | __key__, order
18
| quantity | | integer |
19
| expiration | | date |
20
### Owner
21
22
| Field | Desc | Type | Attribute |
23
|--|--|--|--|
24
| addr | | string | __key__, order
25
| miles | | partition |
26
27
## Actions
28
29
### add
30
`called by` admin
31
| Name | Desc | Type |
32
|--|--|--|
33
|ow||string
34
|newmile||mile asset
35
36
### consume
37
`called by` admin
38
| Name | Desc | Type |
39
|--|--|--|
40
|ow||string
41
|val||integer
42
#### Formal Specification
43
##### p1
44
`let o = owner.get owner in o.miles.sum(quantity) = before o.miles.sum(quantity) - val`
45
##### p2
46
`forall m : removed miles, m.expiration >= now`
47
##### p3
48
`is_empty (added miles)`
49
### clear
50
`called by` admin
51
52
## Formal properties
53
54
##### m1
55
`forall m : mile, m.amount > 0`
56
##### s1
57
`anyaction may be performed only by role admin`
58
##### s2
59
`(remove mile) may be performed only by tx consume`
60
##### s3
61
`transfers_by_tx anytx = 0`
Copied!
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub