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:
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:
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).
archetype miles_with_expirationvariable 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 adminrequire {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) - quantityinvariant 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 >= nowinvariant for loop {removed.mile.subsetof(by_expiration)}}postcondition p4 {added.mile.isempty()invariant for loop {added.mile.isempty()}}}called by adminrequire {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 doif remainder > 0then (if mile[m].amount > remainderthen (mile.update(m, { amount -= remainder });remainder := 0)else if mile[m].amount = remainderthen (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 < nowinvariant for loop2 {forall m in removed.mile, m.expiration < now}}}called by admineffect {for : loop2 o in owner doowner[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)}