# Rules and proofs

> Declare what your program must never do in RULES.al and let alice prove check every case, with a PROOF.al certificate for CI.

Canonical: https://alice-lang.org/documentation/guides/rules-and-proofs/

[Documentation index](https://alice-lang.org/documentation/llms.txt) · [Complete book](https://alice-lang.org/llms-full.txt)

Alice's take on Bend's `LAWS.bend`: you write the properties your program must never break, and the compiler
checks them on every input of a finite domain. A failure prints the exact inputs that break the rule.

## Write a rule

```alice
def clamp(x : Int32, lo : Int32, hi : Int32) : Int32
  x < lo ? lo : (x > hi ? hi : x)
end

rule clamp_stays_in_range(x in -1000..1000, lo in -50..50)
  c = clamp(x, lo, lo + 10)
  c >= lo && c <= lo + 10
end
```

- `rule name(vars) ... end` returns `Bool`; the last expression is the verdict.
- Each variable ranges over `lo..hi` (inclusive), `lo...hi` (exclusive) with integer literals, or `Bool`.
- A rule must be pure (AL0210). Pure code gives the same answer for the same inputs, so checking every input
  is a proof by exhaustion, not a random test.
- At most 2^32 cases per rule (AL0214).

Keep rules in `RULES.al` at the project root. They can call any pure function of the program.

## Prove

```text
$ alice prove
╭───────────────────────┬─────────┬────────╮
│ rule                  │   cases │ result │
├───────────────────────┼─────────┼────────┤
│ clamp_stays_in_range  │ 202,101 │ proven │
╰───────────────────────┴─────────┴────────╯
```

`alice prove` compiles the project, runs every rule over its whole domain in parallel, and writes `PROOF.al`:
each rule's result and a SHA-256 of every source file. A broken rule prints
`fails at x = 1001, lo = 0`; an exception during a case (overflow, division by zero) is a failure too.

## In CI and before committing

`alice prove --check` proves again and compares with `PROOF.al`. It fails if a rule fails or if the code
changed since `PROOF.al` was written. Commit `PROOF.al` with the code. AI agents working on an Alice project
are told to run it before every commit (see [AI agents and the guide](https://alice-lang.org/documentation/tools/ai-agents.md)).

## When rules are worth it

| Good fit                                                                        | Poor fit                                          |
| ------------------------------------------------------------------------------- | ------------------------------------------------- |
| invariants that must never break: balances, game rules, parsers, state machines | properties over huge or unbounded inputs          |
| numeric edge cases (rounding, overflow, ranges)                                 | behaviour that depends on I/O, time or randomness |
| code that people or agents edit often                                           | one-off scripts                                   |

## What is guaranteed

The rule holds on every listed input for the program as this Alice version compiles it. Inputs outside the
domains are not covered, so include the edges (`0`, negatives, limits). The compiler and the .NET runtime are
trusted, not proven. Alice proves its own numeric semantics (floored division, `divmod`, wrapping) the same way
on every release.

## Continue reading

- Previous: [Build games and desktop programs](https://alice-lang.org/documentation/guides/games.md)
- Next: [Test Alice programs](https://alice-lang.org/documentation/guides/testing.md)