Rule Syntax

Rules express temporal constraints using modal mu-calculus.

Submitting Rules

When adding a rule to a contract, you must include a model that witnesses satisfiability:

modal c commit \
  --method rule \
  --rule 'rule my_rule { formula { always(<+signed_by(/members/alice.id)> true) } }' \
  --model 'model witness { initial s; s -> s [] }' \
  --sign key.pem

The model proves the rule can be satisfied. Without a satisfying model, the rule commit is rejected. This prevents adding unsatisfiable rules that would deadlock the contract.

Basic Structure

rule <name> {
  starting_at <commit_ref>
  formula {
    <modal_formula>
  }
}

// Or as default export
export default rule {
  starting_at $PARENT
  formula {
    <modal_formula>
  }
}

Anchoring (starting_at)

starting_at $PARENT           // Parent of this commit
starting_at $ROOT             // Genesis commit
starting_at abc123...         // Specific commit hash

Modal Operators

Operator	Meaning
[ACTION] φ	After ALL ACTION transitions, φ holds
<ACTION> φ	After SOME ACTION transition, φ holds
[-ACTION] φ	If ACTION is refused/impossible, φ holds
[<+ACTION>] φ	Committed: CAN do ACTION and CANNOT refuse

Commitment Versus Enabledness

Use the operator that matches the claim you want the contract to make:

<+PAY> true

PAY is enabled from the current witness state.

[<+PAY>] true

PAY is committed: it is enabled and its refusal edge is unavailable.

[+PAY] +signed_by(/parties/alice.id)

Every matching PAY transition must carry Alice's signature predicate.

Avoid [+PAY] true as a guard. A box formula with inner true is satisfied even when there is no matching PAY transition, so it does not prove PAY happened or that PAY is committed. Run modality model lint <file> before signing rules; it reports this as modality/vacuous-box-guard.

Temporal Operators (Syntactic Sugar)

always(φ)           // φ holds forever (invariant)
                    // = gfp(X, φ & []X)

eventually(φ)       // φ holds now or sometime later
                    // = lfp(X, φ | <>X)

until(p, q)         // p holds until q becomes true
                    // = lfp(X, q | (p & <>X))

Fixed Points

// Greatest fixed point (νX) - invariants, safety
gfp(X, property & []X)

// Least fixed point (μX) - reachability, liveness
lfp(X, target | <>X)

// Unicode alternatives
νX. (property & []X)
μX. (target | <>X)

Boolean Connectives

φ & ψ           // Conjunction (and)
φ | ψ           // Disjunction (or)
!φ              // Negation (not)
true            // Always true
false           // Always false

Prefer explicit boolean form for conditional rules:

!+modifies(/members) | +all_signed(/members)

The parser still accepts implication syntax in some contexts, but docs and onboarding examples avoid it so temporal steps and proof implication are not conflated. modality model lint <file> reports signed-rule uses as modality/implication-sugar; rewrite them to explicit Boolean form before signing.