# 13. Rules and proofs

> Chapter 13: state what your program must never do as rules in RULES.al, prove them for every input with alice prove, read counterexamples, prove whole Int32 ranges with --smt, and keep PROOF.al honest in CI.

Canonical: https://alice-lang.org/documentation/learn/proofs/

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

A test checks a few examples you thought of. Bugs live in the inputs you did not think of: the zero, the negative number, the value at the very edge of a range. This chapter shows how to state a **rule** that must hold for *every* input in a range, and have the compiler check all of them.

It is the most useful chapter for anyone who changes code they did not write, and that includes AI coding agents. A rule says what must stay true. A proof shows it still is.

## 13.1 A first rule

Here is a small method that keeps a value inside a range, and a rule about it:

```alice cmd="prove" ignore="last-column"
def clamp(x : Int32, lo : Int32, hi : Int32) : Int32
  return lo if x < lo
  return hi if x > 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
```

```text title="Output"
╭──────────────────────┬─────────┬────────┬────╮
│ rule                 │   cases │ result │ ms │
├──────────────────────┼─────────┼────────┼────┤
│ clamp_stays_in_range │ 202,101 │ proven │  9 │
╰──────────────────────┴─────────┴────────┴────╯
```

Let's read the rule:

- `rule name(...) ... end` looks like a method. Its last expression is the verdict: `true` means the rule holds for these inputs.
- `x in -1000..1000` gives `x` a **domain**: every integer from -1000 to 1000. `lo in -50..50` does the same for `lo`.
- `alice prove` runs the rule for **every combination**: 2001 values of `x` times 101 values of `lo`, which is 202,101 cases. They run in parallel, so it takes milliseconds. The last column is the time; yours will differ.

Every case returned `true`, so the result is **proven**. Not "tested": a rule must be pure (it may not print, write files, or change state), so it gives the same answer every time, and checking every case of the domain is a proof for that domain.

## 13.2 When a rule fails

Now a rule that is wrong, or rather a method that is. A midpoint function, the kind used in binary search:

```alice cmd="prove" exit="1" ignore="last-column"
def midpoint(a : Int32, b : Int32) : Int32
  (a + b) / 2
end

rule midpoint_is_between(a in -100..100, b in -100..100)
  return true if a > b
  m = midpoint(a, b)
  m >= a && m <= b
end

rule midpoint_is_symmetric(a in -100..100, b in -100..100)
  midpoint(a, b) == midpoint(b, a)
end

rule halves_add_up(n in -100..100)
  midpoint(0, n) * 2 == n
end
```

```text title="Output"
╭───────────────────────┬────────┬──────────────────┬────╮
│ rule                  │  cases │ result           │ ms │
├───────────────────────┼────────┼──────────────────┼────┤
│ halves_add_up         │    201 │ fails at n = -99 │  0 │
│ midpoint_is_between   │ 40,401 │ proven           │  4 │
│ midpoint_is_symmetric │ 40,401 │ proven           │  4 │
╰───────────────────────┴────────┴──────────────────┴────╯
error: some rules fail: fix the code (or the rule) and run `alice prove` again
```

Rules are listed in alphabetical order. `halves_add_up` fails, and Alice prints a **counterexample**: the exact input that breaks it, the first one in domain order, the same on every run. `midpoint(0, -99)` is `-50`, because division rounds down, and `-50 * 2` is `-100`, not `-99`.

Here the rule is what is wrong: it only holds for even `n`. When a rule fails, ask which one is wrong, the code or the rule. Fix the code unless the rule states something that was never required. Here we fix the rule with `return true if n.odd?`.

An exception counts as a failure too. If the code overflows or divides by zero for some input, the result names the exception and the input.

## 13.3 PROOF.al: a certificate

`alice prove` writes a file `PROOF.al` next to the code:

```text
# PROOF.al: written by `alice prove`. Do not edit; run `alice prove` after changing the code or RULES.al.
# Every rule marked proven returned true on every case of its domain. Rules are pure, so this is a proof by
# exhaustion of the program as Alice compiles it. `alice prove --check` fails when the sources change.
#
# alice 0.14.0
# sources sha256 0a71df4ab1d21d83b0d6c9e283d12e848ade57ef70ba1d23a49ad7295c7dc343
# rule discount_never_negative: proven over 2110211 cases
# rule discount_never_raises_the_price: proven over 2110211 cases
```

It records the Alice version, a SHA-256 hash of every source file, and each rule's result. Commit it with the code.

`alice prove --check` proves everything again and also compares with `PROOF.al`. It fails when any rule fails, **or** when the sources changed since `PROOF.al` was written, or a rule was added or removed. So a green `--check` means: the code you are looking at is the code that was proven.

## 13.4 A change that breaks a rule

Here is the situation this tool is built for. The tea shop keeps its pricing in `src/pricing.al`. The discount is capped at 50 percent:

```alice file="src/pricing.al"
def discounted(total : Int64, percent : Int32) : Int64
  return total if percent <= 0
  total - total * Math.Min(percent, 50) / 100
end
```

The shop's rules live in `RULES.al`:

```alice cmd="prove" target="." ignore="last-column"
rule discount_never_negative(total in 0..10_000, percent in -10..200)
  discounted(total.to_i64, percent) >= 0
end

rule discount_never_raises_the_price(total in 0..10_000, percent in -10..200)
  discounted(total.to_i64, percent) <= total
end
```

```text title="Output"
╭─────────────────────────────────┬───────────┬────────┬────╮
│ rule                            │     cases │ result │ ms │
├─────────────────────────────────┼───────────┼────────┼────┤
│ discount_never_negative         │ 2,110,211 │ proven │  6 │
│ discount_never_raises_the_price │ 2,110,211 │ proven │  6 │
╰─────────────────────────────────┴───────────┴────────┴────╯
```

Both rules hold for every total up to 100.00 and every percentage from -10 to 200: over four million cases. The project commits `PROOF.al`.

Now someone, a colleague or an AI agent asked to "simplify the pricing code", notices that `Math.Min(percent, 50)` looks redundant, and removes it:

```alice file="src/pricing.al"
def discounted(total : Int64, percent : Int32) : Int64
  return total if percent <= 0
  total - total * percent / 100
end
```

The tests still pass: the test suite only tried 10 and 15 percent. But the pre-commit check runs `alice prove --check`:

```alice cmd="prove --check" target="." exit="1" ignore="last-column"
rule discount_never_negative(total in 0..10_000, percent in -10..200)
  discounted(total.to_i64, percent) >= 0
end

rule discount_never_raises_the_price(total in 0..10_000, percent in -10..200)
  discounted(total.to_i64, percent) <= total
end
```

```text title="Output"
╭──────────────────────────────┬───────────┬──────────────────────────────┬────╮
│ rule                         │     cases │ result                       │ ms │
├──────────────────────────────┼───────────┼──────────────────────────────┼────┤
│ discount_never_negative      │ 2,110,211 │ fails at total = 1, percent  │  5 │
│                              │           │ = 200                        │    │
│ discount_never_raises_the_pr │ 2,110,211 │ proven                       │  4 │
│ ice                          │           │                              │    │
╰──────────────────────────────┴───────────┴──────────────────────────────┴────╯
error: PROOF.al is missing or stale: the code or RULES.al changed since it was 
written; run `alice prove` and commit PROOF.al
```

The counterexample is concrete: a total of 1 cent with a 200 percent discount gives a price of -1 cent. The shop would pay customers to drink tea. The commit is blocked, and whoever made the change, person or agent, gets the exact input to look at. The cap was not redundant; it was the requirement. Restore it, run `alice prove`, and commit the new `PROOF.al`.

## 13.5 Whole ranges with `--smt`

Enumeration has a limit: at most 2^32 cases per rule. A rule over all `Int32` values for two variables would be 2^64 cases, far too many. For such rules, `alice prove --smt` uses Z3, an **SMT solver**: a program that reasons about formulas instead of trying values. It translates the rule and the methods it calls into logic with Alice's exact semantics, including checked overflow and rounding-down division, and either proves the rule for every input or finds a counterexample.

Write the variable's type instead of a domain:

```alice cmd="prove --smt" exit="1" ignore="last-column"
def magnitude(x : Int32) : Int32
  x < 0 ? -x : x
end

def midpoint(a : Int32, b : Int32) : Int32
  a + (b - a) / 2
end

rule magnitude_is_not_negative(x : Int32)
  magnitude(x) >= 0
end

rule midpoint_is_between(a : Int32, b : Int32)
  return true if a > b
  m = midpoint(a, b)
  m >= a && m <= b
end
```

```text title="Output"
╭───────────────────────────┬───────┬─────────────────────────────────────┬────╮
│ rule                      │ cases │ result                              │ ms │
├───────────────────────────┼───────┼─────────────────────────────────────┼────┤
│ magnitude_is_not_negative │   all │ fails at x = -2147483648            │  0 │
│ midpoint_is_between       │   all │ fails at a = -1594602484, b =       │  0 │
│                           │       │ 1061940235                          │    │
╰───────────────────────────┴───────┴─────────────────────────────────────┴────╯
error: some rules fail: fix the code (or the rule) and run `alice prove` again
```

Both failures are real bugs that sampling would almost never find:

- `-x` for `x = Int32::MIN` does not fit in an `Int32`. In Alice it raises `OverflowException`, which fails the rule; in C it would silently stay negative.
- `b - a` overflows when `a` is very negative and `b` very positive. The written-out midpoint `a + (b - a) / 2` is a well-known way to avoid overflow of `a + b`, and it still overflows here.

The fix computes in 64 bits, where the sum cannot overflow:

```alice cmd="prove --smt" ignore="last-column"
def midpoint(a : Int32, b : Int32) : Int32
  ((a.to_i64 + b) / 2).to_i32
end

rule midpoint_is_between(a : Int32, b : Int32)
  return true if a > b
  m = midpoint(a, b)
  m >= a && m <= b
end
```

```text title="Output"
╭─────────────────────┬───────┬────────┬────╮
│ rule                │ cases │ result │ ms │
├─────────────────────┼───────┼────────┼────┤
│ midpoint_is_between │   all │ proven │  0 │
╰─────────────────────┴───────┴────────┴────╯
```

"all" means every one of the 2^64 input pairs. `PROOF.al` marks such results `(smt)`.

`--smt` handles integer arithmetic, `if` and ternaries, early `return`, locals, `Math.Min`/`Math.Max` and calls to non-recursive pure methods. A rule with loops, recursion, objects or floats is enumerated over its domains instead, never half-proven. Z3 is an optional system library: install `libz3` (`pacman -S z3`, `apt install libz3-4`, `brew install z3`) or set `ALICE_Z3` to its path.

## 13.6 Rules in CI

Make the check automatic, so that no change can merge with a failing or stale proof. In GitHub Actions:

```yaml
name: proofs
on: [push, pull_request]
jobs:
  prove:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install Alice
        run: |
          curl -fsSL https://alice-lang.org/install.sh | sh
          echo "$HOME/.alice/bin" >> "$GITHUB_PATH"
      - name: Prove the rules
        run: alice prove --check
```

`alice prove --check` exits with status 1 on any failure, which fails the job. Add `sudo apt-get install -y libz3-4` and `--smt` if your rules use whole ranges. Locally, the same command fits in a Git pre-commit hook.

## 13.7 What a proof does and does not tell you

Be precise about the guarantee:

- **Proven:** for every input in the stated domains, the rule returned `true`, for the program as this Alice version compiles it.
- **Not covered:** inputs outside the domains. Choose domains that include the edges: zero, negatives, and the limits your code branches on.
- **Trusted, not proven:** the Alice compiler, the .NET compiler and runtime, and Z3.
- **A rule is only as good as what it states.** A proven rule that says the wrong thing proves the wrong thing. Write rules from the requirements, not from the current code.

Rules complement tests. Tests show examples and document behavior; rules close the gaps between the examples.

:::caution\[Common mistakes]

- **A domain that is too large.** More than 2^32 cases is `AL0214`. Narrow the ranges, split the rule, or use `--smt`.
- **A rule that is not pure.** Printing or writing state inside a rule is `AL0210`.
- **Changing the rule to make it pass.** Fix the code, unless the rule itself states something that was never required, and then say so in the commit.
- **Forgetting to commit `PROOF.al`.** `--check` then reports it as missing or stale.
- **Domains without edges.** `x in 1..100` never tries 0 or a negative number.
  :::

## Exercises

1. Write `percent_of(total : Int32, p : Int32) : Int32` as `total * p / 100` and a rule that the result never exceeds `total` for `total in 0..1000` and `p in 0..100`. Prove it.
2. Extend the domain of exercise 1 to `p in 0..200`. What does `alice prove` say, and is the code or the rule wrong?
3. Write `sign(x : Int32) : Int32` (-1, 0 or 1) and prove with `--smt` that `sign(x) * magnitude` is `x`, using `x.abs`. What does the solver find?

<details>
<summary>Answers</summary>

1. Answer:

   ```alice cmd="prove" ignore="last-column"
   def percent_of(total : Int32, p : Int32) : Int32
     total * p / 100
   end

   rule percent_never_exceeds_total(total in 0..1000, p in 0..100)
     percent_of(total, p) <= total
   end
   ```

   ```text title="Output"
   ╭─────────────────────────────┬─────────┬────────┬────╮
   │ rule                        │   cases │ result │ ms │
   ├─────────────────────────────┼─────────┼────────┼────┤
   │ percent_never_exceeds_total │ 101,101 │ proven │  2 │
   ╰─────────────────────────────┴─────────┴────────┴────╯
   ```

2. It fails, for example at `total = 1, p = 200`: 200 percent of a total is more than the total. The code is right; the rule only holds for `p` up to 100, so the rule must say so.

3. It fails at `x = -2147483648`: `x.abs` overflows for the smallest `Int32`, which raises an exception, and an exception fails the rule.

   ```alice cmd="prove --smt" exit="1" ignore="last-column"
   def sign(x : Int32) : Int32
     return -1 if x < 0
     return 1 if x > 0
     0
   end

   rule sign_times_abs(x : Int32)
     sign(x) * x.abs == x
   end
   ```

   ```text title="Output"
   ╭────────────────┬───────┬──────────────────────────┬────╮
   │ rule           │ cases │ result                   │ ms │
   ├────────────────┼───────┼──────────────────────────┼────┤
   │ sign_times_abs │   all │ fails at x = -2147483648 │  0 │
   ╰────────────────┴───────┴──────────────────────────┴────╯
   error: some rules fail: fix the code (or the rule) and run `alice prove` again
   ```

</details>

## Summary

- A `rule` is a pure Boolean method over finite domains (`x in lo..hi`, `b : Bool`). `alice prove` checks every case and writes `PROOF.al`.
- A failure prints the first counterexample. An exception is a failure.
- `alice prove --check` fails on a failing rule or on stale sources. Run it before every commit and in CI, and commit `PROOF.al`.
- `alice prove --smt` proves integer rules over whole `Int32`/`Int64` ranges with Z3.
- A proof covers the stated domains for the program as compiled; it is only as good as the rule.

[Chapter 14](https://alice-lang.org/documentation/learn/dotnet.md) opens the door to the rest of the .NET world.

## Continue reading

- Previous: [12. Performance](https://alice-lang.org/documentation/learn/performance.md)
- Next: [14. Using .NET](https://alice-lang.org/documentation/learn/dotnet.md)