Refinement types for pre-checks

[obycode]

A common pattern we see in smart contracts is where a trait is passed in to a function, and then inside the function, this trait is checked to make sure that it matches some principal defined in a data-var or map. This check is then needed in many functions and can be easily forgotten. In place of this error-prone behavior, we could allow developers to define refinement types, which enforce a check as a sort of pre-check before executing the function body.

I'm picturing something like this:

(define-refined-type (CheckedToken <sip-010>)
  (if (is-eq (contract-of CheckedToken) (var-get expected-token))
    (ok true)
    (err u1)
  ))

(define-public (do-something (token CheckedToken))
  ...
)

When do-something is called directly by a transaction or a contract-call?, the check is performed and will exit immediately if it returns an error. Otherwise, the function body is executed as usual. In this example, token could be passed into another local function specifying the CheckedToken type and the check does not need to be repeated.

What I don't like about it:

• The error type needs to match all functions that use this type

[obycode]

Alternative syntax would be to reuse the <> for these types, similar to traits:

(define-refined-type (checked-token <sip-010>)
  (if (is-eq (contract-of checked-token) (var-get expected-token))
    (ok true)
    (err u1)
  ))

(define-public (do-something (token <checked-token>))
  ...
)

[obycode]

I just remembered that we have some similar refinement type ideas already in these issues:

• Integer refinement type #13
• String refinement types #19
• Principal refinement types #24

[kantai]

Something to keep in mind with this kind of application of refinement types is that the check's semantics end up being important. In your examples, I think they're basically pre-conditions for the function arguments, so the semantic is that the check is executed on every invocation of the function. But we'd also need to make some decisions about whether or not they can be used other places where types are supplied (e.g., trait definitions, deserialization), and if so, what it means in those places too (i.e., do those also apply the check at deserialization?). I'm not sure that this description captures exactly my point, but I think that the system needs to have an opinion on something like this:

define-refined-type (checked-token <sip-010>)
  (if (is-eq (contract-of checked-token) (var-get expected-token))
    (ok true)
    (err u1)
  ))

(define-public (do-something (token <checked-token>))
   ;; token passes the check here
  (begin
     (var-set expected-token something-else)
     ;; token wouldn't pass the check here
     (contract-call? token ...)))

Is that something that should error? I think we'd want the answer to be "no", but it's definitely something that needs to be specified.

[jcnelson]

I think we'd want to be very, very careful about the side-effects of code that can go into the type predicate. Are any of these legal?

(define-constant TRUSTED_PRINCIPAL_CONST 'SPV7FQJ1W9VJA2CGZ31HDTZF2QNVYTTQ3EX16RQV)
(define-data-var trusted-principal-var principal 'SP1EW26WKNS7Y73B2ES0WBNH19QJHGQF93P71M6JJ)

(define-public (change-trusted-principal (new-principal principal))
   (ok (var-set trusted-principal-var new-principal))

;; Case #0: The predicate evaluates to nonsensical outputs.
;; Does this even type-check?
(define-refined-type (checked-token-0 <sip-010>)
    "w00t!")

;; Case #1: This type is dependent on runtime state, since
;; `change-trusted-principal` can put whatever it wants into
;; `trusted-principal-var`
(define-refined-type (checked-token-1 <sip-010>)
   (if (is-eq (contract-of checked-token-1) (var-get trusted-principal-var))
      true
      false))

;; Case 2: This type's predicate can panic at runtime. What happens now?
(define-refined-type (checked-token-2 <sip-010>)
   (if (is-eq (contract-of checked-token-2) TRUSTED_PRINCIPAL_CONST)
      true
      (unwrap-panic (err u1))))

;; Case 3: Every time this type is checked at runtime, it mutates contract state.
;; Is this allowed?
(define-refined-type (checked-token-3 <sip-010>)
   (if (is-eq (contract-of checked-token-3) (var-get trusted-principal-var))
      (begin
         (var-set trusted-principal-var tx-sender)  ;; tx-sender could be a contract address!
         true)
      false))

I think, at a minimum, we'd want the following:

• The type predicate must evaluate to bool.
• The type predicate must be read-only. No state mutations in type-checking.
• Runtime panics in the type predicate cause the transaction to abort.
• The type predicate is valuated lazily, meaning that it would be affected by (and compose with) as-contract or at-block

Also, I'm not sure I'd call this a refinement type anymore, since it's basically impossible to check a refined type statically. This, to me, looks more like a "type decorator" -- like a function decorator, but for a type. The key difference is that type decorators are evaluated at runtime, and the type-checker only verifies that type decorator's code body is read-only and evaluates to bool.

What do you think?

[obycode]

@kantai

I think they're basically pre-conditions for the function arguments, so the semantic is that the check is executed on every invocation of the function.

I was thinking of it a bit differently. What I was attempting to describe was that the check is only executed at contract call boundaries, so if that function is called directly in a transaction, then it passes the token to another local function which takes a <checked-token>, the check is not performed again. I would not expect your example to raise an error.

[obycode]

@jcnelson

The type predicate must evaluate to bool.

I guess that means that a failure would result in some new kind of runtime panic? I think that would work. I had it returning a response, whose result is ignored if ok and error value would be returned to the caller. But the problem I pointed out with that then is that the error type needs to match the error type of all functions that use it. Making it a runtime panic instead solves that problem.

The type predicate must be read-only. No state mutations in type-checking.

Yes, I think that is a good idea.

Runtime panics in the type predicate cause the transaction to abort.

Agreed.

The type predicate is valuated lazily, meaning that it would be affected by (and compose with) as-contract or at-block

Agreed.

Also, I'm not sure I'd call this a refinement type anymore, since it's basically impossible to check a refined type statically.

I believe there are other languages that enforce refinements at runtime, so it wouldn't be a totally new usage of the term. I guess we'd have to talk to some devs to see what terms make sense to most.

[jcnelson]

@obycode

What I was attempting to describe was that the check is only executed at contract call boundaries, so if that function is called directly in a transaction, then it passes the token to another local function which takes a , the check is not performed again.

Isn't that a bit surprising? What if the type predicate depends on contract-local state, which could change between the contract-call boundary and the function call?

For example:

(define-data-var allowed bool true)
(define-refined-type (thing <thing-trait>)
   (var-get allowed))

(define-public (do-public-thing (thing <checked-thing>))
   (begin
      (var-set allowed false)
      (do-private-thing thing)
      (var-set allowed true)
      (ok true)))

(define-private (do-private-thing (thing <checked-thing>))
   ;; What happens here? Should this panic since the type predicate for
   ;; `checked-thing` is now demonstrably false?