Mini DAO

archetype mini_dao
asset shares identified by addr {
addr : address;
value : tez
}
entry withdraw () {
specification {
postcondition p1 {
let some s = shares[caller] in
balance = before.balance - s.value
otherwise true
}
}
require {
r0 : shares.contains(caller);
r1 : shares[caller].value > 0tz;
r2 : balance >= shares[caller].value;
}
effect {
var v = shares[caller].value;
transfer v to caller;
shares.update (caller, { value = 0tz })
}
}
Edit on GitHub