Retain snapshot commit evidence after installation

[jeregrine]

Problem

The snapshot model's no-terminal-commit invariant checks only outstanding staging. Installation clears staging, making the invariant vacuously true precisely when it should reject an installation that never received a commit.

Fix

Retain the last installation's actual commit evidence independently of staging and assert that evidence. Ordinary model transitions and the finite state space are unchanged when projected onto the original variables.

The formal matrix also runs a negative qualification: remove the terminal-commit guard in an isolated model copy and require a safety violation specifically from NoCommitMeansNoInstall. Mutant survival and parser/runtime failures fail qualification instead of receiving credit.

Supporting information

The matrix now also requires Elixir to construct the isolated mutation and classify TLC's stable exit status. Individual model runs through check.sh still need only Java and tla2tools.jar. Qualification artifacts remain under ignored tmp/formal/ for inspection.