Miles

miles.arl
archetype miles
​
variable[%transferable%] validator : role = @fake_validator
​
asset account identified by owner {
  owner  : role;
  amount : int;
}
​
action 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 })
  }
}
​
action consume (ow : role, value : int) {
  specification {
    postcondition s1 {
      let some ba = before.account.get(ow) in
      let some a = account.get(ow) in
      ba.amount = a.amount + value
      otherwise true
      otherwise true
    }
  }
​
  called by validator
​
  require {
    c1 : account.get(ow).amount >= value;
  }
​
  effect {
    account.update (ow, { amount -= value })
  }
}
​