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
miles_with_expiration.arl
archetype miles_with_expiration
variable admin : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
(* id is a string because it is generated off-chain *)
asset mile identified by id {
id : string;
amount : int;
expiration : date
} with {
m1 : amount > 0;
}
(* a partition ensures there is no direct access to mile collection *)
asset owner identified by addr {
addr : role;
miles : partition<mile> = [] (* injective (owner x mile) *)
}
entry add (ow : address, newmile_id : string, newmile_amount : int, newmile_expiration : date) {
called by admin
require {
c1 : newmile_amount > 0;
}
failif {
c2 : mile.contains(newmile_id);
}
effect {
owner.addupdate (ow, { miles += [{id = newmile_id; amount = newmile_amount; expiration = newmile_expiration} ] })
}
}
entry consume (a : address, quantity : int) {
specification {
assert p1 {
remainder = 0
}
postcondition p2 {
mile.sum(the.amount) = before.mile.sum(the.amount) - quantity
invariant for loop {
0 <= remainder <= toiterate.sum(the.amount);
before.mile.sum(the.amount) = mile.sum(the.amount) + quantity - remainder
}
}
postcondition p3 {
forall m in removed.mile, m.expiration >= now
invariant for loop {
removed.mile.subsetof(by_expiration)
}
}
postcondition p4 {
added.mile.isempty()
invariant for loop {
added.mile.isempty()
}
}
}
called by admin
require {
r2 : quantity >= 0;
}
effect {
var by_expiration = owner[a].miles.sort(expiration).select(the.expiration > now);
dorequire (by_expiration.sum(the.amount) >= quantity);
var remainder = quantity;
for : loop m in by_expiration do
if remainder > 0
then (
if mile[m].amount > remainder
then (
mile.update(m, { amount -= remainder });
remainder := 0
)
else if mile[m].amount = remainder
then (
remainder := 0;
owner[a].miles.remove(m)
) else (
remainder -= mile[m].amount;
owner[a].miles.remove(m)
)
)
done;
assert p1
}
}
entry clear_expired () {
specification {
postcondition s3 {
forall m in removed.mile, m.expiration < now
invariant for loop2 {
forall m in removed.mile, m.expiration < now
}
}
}
called by admin
effect {
for : loop2 o in owner do
owner[o].miles.removeif(the.expiration < now)
done
}
}
security {
(* this ensures that any mile was added with the 'add' entry *)
g1 : only_by_role (anyentry, admin);
g2 : only_in_entry (remove (mile), [consume or clear_expired]);
g3 : not_in_entry (add (mile), consume);
g4 : no_storage_fail (add)
}
Edit on GitHub