Show counterexample values in the final expected refinement

[CatarinaGamboa]

Summary

Carry the expanded expected predicate used by the SMT check into refinement errors. Substitute every displayed counterexample value that can safely be parsed as a literal, using expression variable identities. Preserve the original expected predicate and counterexample assignments.

For an alias mismatch, the verifier can now show:

Refinement Error: ... is not a subtype of Positive(buffered)
Final expected: buffered > 0
Counterexample: buffered == 0
With witness: 0 > 0 ✗

The CLI error displays the final expected predicate and witness. RefinementError also exposes both as predicates for a future server DTO and VS Code presentation change. Verification results are unchanged.

Closes #296.

Verification

• Full verifier test suite passed: 340 tests, zero failures.
• Focused tests cover alias expansion, multiple assignments, repeated variables, negative values, unsafe values left unchanged, and a real verifier counterexample.
• git diff --check passed.

Integration note

The current VS Code server DTO does not serialize these new fields, so they will not appear in the extension until a separate server/client update consumes them.

[rcosta358]

A while back I thought about adding a simplification pass specifically for expected types that could also be applied to counterexamples, and I think that would address this issue in a better way.

This simplification would expand aliases and static final constants, for example:

• ∀x. true => x == Byte.MAX_VALUE → ∀x. true => x == 127
• ∀x. x == -1 => Positive(x) → ∀x. x == -1 => x > 0 → -1 > 0

Then we could have navigate the simplification history just like we are doing for the found types.
What do you think?

[CatarinaGamboa]

Yeah we could extend the simplification here, but also do the substitution of values with the counter-examples in the expected type

[rcosta358]

Yes, I also had thought about that possibility. We can plug them in the expected type and then perform the same simplification to see how they make the expected type false.