Derive Developer Facing States

[rcosta358]

Description

This PR improves error messages by deriving developer-facing states from internal state equalities.
When an error contains an internal equality like state1(new) == state1(old) plus a known developer state for old, the diagnostic now displays the corresponding developer state for new and omits the internal equality once it has served that purpose.

This is for error messages only and does not change SMT verification behavior.

Example

Before

startCompression(param⁷¹) &&
state1(param⁷¹) == state1(param⁶⁹) &&
startTiling(param⁶⁹) &&
startCompression(param⁶⁹)

After

startCompression(param⁷¹) &&
startTiling(param⁶⁹) &&
startCompression(param⁶⁹) &&
startTiling(param⁷¹)

Related Issue

Closes #206.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests under liquidjava-example/src/main/java/testSuite/ (Correct* / Error*)
• mvn test passes locally
• Updated docs/README if behavior or API changed

[alcides]

Exactly how do state1 and startTiling relate? It seems startTiling(x) is equals to state1(x) == SOME_CONSTANT_FOR_StartTiling. Is that the case?

[CatarinaGamboa]

Exactly how do state1 and startTiling relate? It seems startTiling(x) is equals to state1(x) == SOME_CONSTANT_FOR_StartTiling. Is that the case?

Internally, the states are encoded as an uninterpreted function with integer values

@StateSet("startTiling, explicitTiling, setTiling")
// internally, create state1( _ )
//                                == 0 : startTiling
//                                == 1 : explicitTiling
//                                == 2 : setTiling

Then this is very helpful when the state does not change in a function invocation we add to the context something like

state1(x1) == state1(x2)

but this means nothing to the user, so we want to show this using the developer facing states. So we need to apply the equality resolution before we do the state changes from state1( _ ) == 0 : startTiling
Does that make sense?

[alcides]

Yes, it does!

I think my concern is whether knowing that the state of x1 and x2 must be the same is important to understand the error message (instead of x1 being in state A and x2 also need to be in state A), since the error would persist even if it was state B.

[CatarinaGamboa]

I think we can maybe just simplify when both sides are instances of the same variable.
Also, we should probably allow the click expand for these cases as well

[CatarinaGamboa]

@rcosta358 when running the cli with the ImageWriteParam case I still get the previous error, can you check it?

[rcosta358]

We need to merge main first