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.
Summary
Functions
Canonical binary encoding of a state.
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.
Fingerprint a state. 64 bits by default; bits: 128 for very large runs.
Fingerprint an encoding that has already been produced.
The widths a fingerprint may be computed at.
Types
Functions
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.
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-6Fingerprint 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))
16Fingerprint 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.
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.