The `#WB` simplification rule with `requires` is not total and may cause stuck states**

[Stevengre]

Issue:

Description

To fix a soundness issue where writes to the same index could be reordered incorrectly, the following requires clause was added to the #WB simplification rule:

rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) 
  => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification]
  requires I0 =/=Int I1

This change successfully prevents the unsound reordering.

Problem

The introduction of requires I0 =/=Int I1 has created a new problem related to non-totality. When the prover encounters symbolic indices (i.e., I0 and I1 are symbolic variables whose equality cannot be decided at simplification time), the condition I0 =/=Int I1 cannot be proven true.

Because simplification rules do not generate branches for different outcomes of a condition, the rule fails to apply in these symbolic cases. This results in a "stuck" configuration where an uncompleted write #WB(false, ...) can never be processed past a completed one, effectively stalling the execution.

The original intent was for this rule to handle all remaining cases (similar to an owise behavior), but the requires clause now prevents this.

Example Scenario

A configuration might get stuck in a state similar to this:

// Where I and J are symbolic integers from input
...
#WB(false, I:Int, V0, NUM0, #WB(true, J:Int, V1, NUM1, ...))
...

In this case, I =/=Int J is undecidable, so the rule will not fire.

Goal

We need to find a way to make the #WB simplification process total while preserving soundness. The current implementation prioritizes soundness at the cost of termination in symbolic cases.

Possible questions to address:

1. How can we correctly handle the case where I0 and I1 are symbolic?
2. Is there a mechanism other than a standard requires clause that can handle this, perhaps by creating a side condition?
3. Could we split this into multiple rules to explicitly handle the I0 ==Int I1 case and the I0 =/=Int I1 case, ensuring that one of them applies? This would still need a way to deal with the undecidable case.

The primary objective is to develop a solution that is both sound and total for all inputs, including symbolic ones.