refactor: rephrase the register frame-condition precondition as non-membership in a list of modified registers

Description:

We change the type of the non-effect hypothesis in AxEffects to

    ∀ (f : StateField), f ∉ [f₁, ⋯, fₙ] →
      r f <currentState> = r f <initialState>

where f₁, ⋯, fₙ are the modified registers, replacing the current sequence of pre-conditions f ≠ f₁ → f ≠ f₂ → … → f ≠ fₙ → ….

This change makes sym_aggregate slightly less powerful out of the box: it will no longer apply ∀ (f : StateField), f ∉ [a, b] → ... given an hypothesis like f ∉ [a, b, c] with more information in the local context. Note that applications of the non-effects theorem to concrete registers are unaffected.

We have to either break this hypothesis f ∉ [a, b, c], and each of the non-effect preconditions, back down in terms of non-equalities (which is doable with a single simp only [...] at * with the right lemmas, as I've done currently), or we could empower sym_aggregate to seed its simpset with the sublist hypotheses f ∉ [b, c] and f ∉ [c].

Upside, though, is that this PR gives a slight speedup:

e90accd (this PR)	Runtime (avg)	Runtime (geomean)
SHA512_150	2.9s	2.9s
SHA512_225	5.6s	5.6s
SHA512_400	15.2s	15.2s

Compared to main	a47a266 (main)	Runtime (avg)
SHA512_150	3.4s	3.4s
SHA512_225	6.7s	6.7s
SHA512_400	18.7s	18.7s

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine? Yes

Yes

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

leanprover / LNSym