Miles with expiration

Search…
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!
Miles
Next - Contract library
Escrow
Last modified 1yr ago
Export as PDF
Copy link