# `ExTLA.Fingerprint`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/fingerprint.ex#L1)

Canonical, collision-resistant state identity.

A fingerprint is the truncated SHA-256 of the state's canonical binary encoding.

This module decides whether the checker's answers can be trusted. A fingerprint
collision silently drops an unexplored state, and the run then reports success
over a state space it never visited — the worst failure mode a verification tool
has. That is why `:erlang.phash2/1` is not used despite its speed: its default range is
2^27, and by the birthday bound a million distinct states would already collide
thousands of times (over a hundred even at 2^32, the most it allows). At 64 bits ten million states expect about 3 x 10^-6 collisions.

# `t`

```elixir
@type t() :: <<_::64>> | <<_::128>>
```

# `canonical`

Canonical binary encoding of a state.

Uses `:erlang.term_to_binary/2` with the `:deterministic` option, which fixes map
and MapSet key ordering in the external term format. The plain 1-arity call is NOT
used: its output for maps is not a guaranteed canonical encoding across OTP
versions, so two equal states could encode differently and be explored twice — or,
worse, a stored fingerprint could stop matching after an OTP upgrade.

# `collision_estimate`

Expected number of distinct states silently lost to collisions, by the birthday
bound: `n^2 / 2^(bits+1)`. Reported in every `ExTLA.ModelChecker.result()` so a run's
soundness margin is visible rather than assumed.

The number is an expectation, not a bound: it is well below 1 for every run a
64-bit fingerprint is appropriate for, and reporting `0.0000000271` rather than
"no collisions" is the point — it says the answer is probabilistic and how
probable, instead of implying a guarantee the method does not provide.

    iex> ExTLA.Fingerprint.collision_estimate(10_000_000, 64)
    2.710505431213761e-6

# `compute`

Fingerprint a state. 64 bits by default; `bits: 128` for very large runs.

    iex> ExTLA.Fingerprint.compute(%{x: 1}) == ExTLA.Fingerprint.compute(%{x: 1})
    true

    iex> byte_size(ExTLA.Fingerprint.compute(%{x: 1}, bits: 128))
    16

# `of_encoding`

Fingerprint an encoding that has already been produced.

Symmetry reduction (`ExTLA.Symmetry`) picks the smallest encoding of a state over every
permutation of its interchangeable constants, and that encoding — not the state it came
from — is what identity is then defined by. Re-encoding the winner would be work already
done, and re-deriving it a chance for the two to disagree.

# `permitted_bits`

The widths a fingerprint may be computed at.

Asked for rather than restated by callers. `mix extla.check --fingerprint-bits`
validates its flag against this, so a second list cannot fall out of step with the one
`compute/2` actually enforces.

---

*Consult [api-reference.md](api-reference.md) for complete listing*