defproperty

[joelburget]

We should add the ability to abstract over properties. Two motivating examples:

(defproperty pure
  [ (forall (table:table) (not (or (table-read table) (table-write table))))
    (not abort)
  ])

(defproperty (conserves-mass (table:table column:column)
  (= (column-delta table column) 0.0))

Notes:

• Both examples assume abstraction over table and column names (Table quantification #122)
• The first example assumes a more powerful property language which can speak of failure.
• The second example is hardcoded to work over decimal columns. Though column-delta works over either decimal or integer columns, 0.0 is a decimal (and 0 is only an integer). We don't currently have any language feature which would allow us to specify a 0 that could be either.
• Pact has a distinction between constants (defconst) and functions (defun). Do we want the equivalent for properties? My first example is a constant whereas the second is a function.
• It's likely we'd also want abstraction for schema invariants, but this seems less useful, so my plan is to punt on this for now.
• defined properties will be brought into scope via a use, like defined functions and constants.

[joelburget]

@slpopejoy I want to write out the design we discussed over the phone to make sure we all agree on how it should look concretely.

We introduce a model form, which can occur as a module top-level:

(module accounts 'accounts-admin-keyset
  "accounts module"
  (model
    ; TODO: abstract over table / column
    (defproperty conserves-mass
      (= (column-delta 'accounts 'balance) 0.0))

    (defproperty correct-auth
      (when
        (not (authorized-by 'accounts-admin-keyset))
        abort))
  )

  ...)

What's the syntax for function level properties? This doesn't read right:

  (defun transfer (src:string dest:string amount:decimal)
    "transfer AMOUNT from SRC to DEST"
    (model (property conserves-mass))
    (debit src amount)
    (credit dest amount))

Should it look like this?

  (defun transfer (src:string dest:string amount:decimal)
    (meta 
      "transfer AMOUNT from SRC to DEST"
      (model (property conserves-mass)))
    (debit src amount)
    (credit dest amount))

Additionally you can import properties only via (use properties 'properties). I think I like use model better. Thoughts?