Valid, satisfiable, explicit transaction abort / success

[joelburget]

Currently properties assume success. When you write (>= result 0), we translate this to (when success (>= result 0)). The assumption here is that 90% of the time you don't care to speak about failure. Why is that?

(defun transfer (from:string to:string amount:integer)
  ("Transfer money between accounts"
    (properties [
      (row-enforced 'accounts 'ks from)
      (= (column-delta 'accounts 'balance) 0)
      ]))

  (let ((from-bal (at 'balance (read accounts from)))
        (from-ks  (at 'ks      (read accounts from)))
        (to-bal   (at 'balance (read accounts to))))
    (enforce-keyset from-ks)
    (enforce (> amount 0))
    (enforce (>= from-bal amount) "Insufficient Funds")
    (enforce (!= to from))
    (update accounts from { "balance": (- from-bal amount) })
    (update accounts to   { "balance": (+ to-bal amount) }))))

Failure is acknowledged as a good thing. We enforce four times to fail when the input is invalid and we only care about the case when the transaction succeeds, because that's the only case when this function has an effect.

However, it is useful to speak about success in at least one case. It's useful to be able to declare a function pure if it can't fail (not abort / success) (or read or write).

For this we envision a more powerful property language that can speak of failure and success.

Relatedly, our property language currently only checks that properties are valid, meaning "this is true in all cases". But it might also be useful to express satisfiability, meaning "this is possible". I'm not sure whether (a) we definitely want to add this feature, and (b) if it's part of this work.

It's an open question how we denote this more powerful property language:

1. We could default to the weaker language, but switch to the more powerful one for any property mentioning success / abort. This is not a good idea. It's both confusing and easy to get wrong.

2. The current property language we could denote with transaction-property / transaction-properties, for properties of a successful transaction. Is the more powerful language then property / properties?

[bts]

In the past we've also talked about the possibility of calling these powerful/advanced modes valid and satisfiable (vs property, properties)

[sirlensalot]

Why isn't something like (abort-when (not (row-exists accounts from))) acceptable? Ie, "always succeed" continues to be the default, requiring additional specification only for abort.