A law is a property of a function that the compiler can check. You state one with @law, and the compiler rejects the function if it can't show the law holds:

@law(:pure, :deterministic)
public function double(x: Int) :: Int -> x * 2

The laws:

• pure: changes nothing outside itself. It may read the clock or draw a random number, but not write, send or spawn.
• deterministic: the same input always gives the same output. Includes pure.
• total: always returns.
• idempotent: applying it twice gives the same result as applying it once, f(f(x)) == f(x). Includes deterministic.
• monotone: more information in never gives less back. Includes deterministic.

Each law includes the ones below it. total is separate.

When you write no @law, the compiler works the laws out itself from the function body; that is how it knows a function is safe to call from a rule guard. When the compiler can't prove a law you know holds, @law(pure: :hint) records it without the check.

Laws are worked out from a function's capabilities: what it may do beyond computing its result.