E0031: unknown_promise

E0031 unknown_promise — a promise no checker implements.

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

The rule

A promise in a face must name one of the structural promises that soma check can test (all_persistent, all_encrypted, all_consistent, has_memory, has_face, has_signals, has_auth), combined with &&, || and !. Anything else, such as a comparison on stored values, is refused because a promise that no check backs would prove nothing. Move a bound on stored values into the cell's memory as an invariant, which is checked before every write; to keep a sentence as documentation only, quote it: promise "balances never go negative".

A program that triggers it

cell Wallet {
    face {
        signal deposit(owner: String, cents: Int) -> Int
        promise all_persistent
        promise balances >= 0
    }
    memory {
        balances: Map<String, Int> [persistent, consistent]
    }
    on deposit(owner: String, cents: Int) {
        let next = (balances.get(owner) ?? 0) + cents
        balances.set(owner, next)
        return next
    }
}

What soma check prints:

$ soma check wrong.cell
error: cell 'Wallet' promises `balances >= 0`, which nothing checks — a face promise is structural (all_persistent, all_encrypted, all_consistent, has_memory, has_face, has_signals, has_auth), combined with &&, || and !. A bound on stored values is an `invariant` in `memory`, a latency bound goes in `cost { latency: … }`; for a note, quote it: `promise "balances >= 0"`
  --> wrong.cell:5:17
  |
5 |         promise balances >= 0
  |                 ^
  = code: E0031
✗ 1 error(s), 0 warning(s).

The fix field of soma check --json: a face promise is structural (all_persistent, all_encrypted, all_consistent, has_memory, has_face, has_signals, has_auth), combined with &&, || and !. A bound on stored values is an `invariant` in `memory`, a latency bound goes in `cost { latency: … }`; for a note, quote it: `promise "balances >= 0"`

The fix

Line 5 is removed; 1 line is added after line 8.

--- wrong.cell
+++ right.cell
@@ -3,8 +3,8 @@
         signal deposit(owner: String, cents: Int) -> Int
         promise all_persistent
-        promise balances >= 0
     }
     memory {
         balances: Map<String, Int> [persistent, consistent]
+        invariant balances >= 0
     }
     on deposit(owner: String, cents: Int) {

With the fix, soma check accepts the program:

$ soma check right.cell
✓ All checks passed.