E0116: contract

E0116 contract — a face contract (requires / ensures) says something a caller could not evaluate, or sits on a handler that cannot carry one.

A compile-time error of soma check, the checker of the Soma programming language (soma explain E0116).

The rule

A face contract (requires / ensures on a signal) is evaluated on every call and is part of the caller's proof, so it may only compare the signal's parameters (and result, in ensures) with literals, constants and pure builtins. A clause that reads a memory slot, calls a handler or uses a non-pure builtin, or a contract on a [native] handler, is refused with E0116. Keep the part about the parameters in the face (requires cents > 0) and move the check against stored data into the handler as a require ... else Tag.

A program that triggers it

cell Wallet {
    face {
        signal withdraw(owner: String, cents: Int) -> Int
            requires cents > 0 && cents <= balances.get(owner)
    }
    memory {
        balances: Map<String, Int> [persistent]
    }
    on withdraw(owner: String, cents: Int) {
        let left = (balances.get(owner) ?? 0) - cents
        balances.set(owner, left)
        return left
    }
}

What soma check prints:

$ soma check wrong.cell
error: `requires cents > 0 && cents <= balances.get(owner)` on signal 'withdraw' reads `balances`: a clause names the signal's parameters (owner, cents) — a slot or a local belongs in the handler, as a `require`
  --> wrong.cell:4:22
  |
4 |             requires cents > 0 && cents <= balances.get(owner)
  |                      ^
  = code: E0116
✗ 1 error(s), 0 warning(s).

The fix field of soma check --json: a slot or a local belongs in the handler, as a `require`

The fix

On line 4, requires cents > 0 && cents <= balances.get(owner) becomes requires cents > 0; line 10 is rewritten.

--- wrong.cell
+++ right.cell
@@ -2,5 +2,5 @@
     face {
         signal withdraw(owner: String, cents: Int) -> Int
-            requires cents > 0 && cents <= balances.get(owner)
+            requires cents > 0
     }
     memory {
@@ -8,5 +8,7 @@
     }
     on withdraw(owner: String, cents: Int) {
-        let left = (balances.get(owner) ?? 0) - cents
+        let balance = balances.get(owner) ?? 0
+        require cents <= balance else InsufficientFunds "{owner} has {balance}"
+        let left = balance - cents
         balances.set(owner, left)
         return left

With the fix, soma check accepts the program:

$ soma check right.cell
✓ All checks passed.