# Formal Algebraic Law Specs
`formal_spec.rs` turns every `AlgebraicLaw` variant into a structural
mathematical statement. The output is an AST, not a restated law name, so later
exporters can target theorem provers such as TLA+, Coq, Kani, or SMT-LIB.
The core types are:
- `FormalLaw`: a quantified statement, currently `ForAll` or `Exists`.
- `Predicate`: equality, order, implication, conjunction, disjunction,
negation, exact-one, and custom predicates.
- `Expr`: variables, constants, and operation calls.
- `AlgebraicLawFormalSpec`: extension trait that provides
`law.formal_spec()` for `AlgebraicLaw`.
## Adding A Law
1. Add the new `AlgebraicLaw` variant in `vyre-spec`.
2. Add the variant to `ALL_ALGEBRAIC_LAWS` and `LAW_CATALOG`.
3. Add a `match` arm in `AlgebraicLawFormalSpec::formal_spec`.
4. Encode the actual mathematical shape with `FormalLaw`, `Predicate`, and
`Expr`. Do not encode the variant name as a string-only placeholder.
5. Add or update the inline snapshot test in `conform/tests/formal_spec.rs`.
6. Add a doc example on the variant that shows standard notation and a Rust
construction example.
The formal spec must be domain-valid. For example, an absorbing element carried
as `u32` is a domain constant, so one-sided absorbing laws must use that same
constant on both the argument and result side:
```text
forall a . f(a, z) = z
```
not:
```text
forall a . f(a, z) = 0
```
unless `z` is explicitly the constant `0`.