Miles

miles.arl
archetype miles
​
variable validator : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
​
asset account identified by owner {
  owner  : role;
  amount : int;
}
​
entry add (ow : role, value : int) {
  called by validator
  effect {
    if account.contains(ow) then
      account.update (ow, { amount += value })
    else
      account.add({ owner = ow; amount = 0 })
  }
}
​
entry consume (ow : role, value : int) {
  specification {
    postcondition s1 {
      let some ba = before.account[ow] in
      let some a = account[ow] in
      ba.amount = a.amount + value
      otherwise true
      otherwise true
    }
  }
​
  called by validator
​
  require {
    c1 : account[ow].amount >= value;
  }
​
  effect {
    account.update (ow, { amount -= value })
  }
}
​