…#883 review)

Skip-changelog: comment-only edit; the PR already carries its CHANGELOG bullet

Co-Authored-By: Claude <[email protected]>

Co-Authored-By: Claude <[email protected]>

…onger collide (#884)

The verifier named Z3 datatype sorts with the old lossy sanitize
(`key.replace("<", "_").replace(">", "").replace(", ", "_")`), so a
monomorphized `Box<Int>` and a flat ADT literally named `Box_Int` both
became the Z3 name `Box_Int`. Z3's per-context datatype cache conflates
same-named sorts (the last `create()` wins and earlier same-named sorts
silently adopt its structure), so `Box<Int>`'s sort acquired the flat
ADT's `MkBoxInt(Bool)` constructor — a false E500 counterexample
(`@Box<Int>.0 = MkBoxInt(False)`) on trivially-true valid code.

Both Z3 sort-name sites (`_get_or_create_adt_sort` and
`_get_or_create_tuple_sort` in `vera/smt.py`) now route through the
injective `mangle_type_name` mangler #775 introduced for WAT symbols, so
distinct type keys can never share a Z3 sort name. The full-type-string
sort cache and the #871 nested-Float64 fpEQ walk are unaffected (the cache
is keyed by the type string, not the Z3-visible name).

Soundness-safe: the conflation only freed field constraints, producing
conservative false negatives, never a false Tier-1 — a genuinely-false
ensures over the colliding pair is still disproved after the fix, now with
the correct `MkBox` constructor.

Both sort-name sites are independently pinned, one collision per site, so
neither `mangle_type_name` call can be reverted without flipping a test:

- ADT site (`_get_or_create_adt_sort`): the `Box<Int>` / flat `Box_Int`
  collision. Reverting it re-collides the sorts and flips the three
  `Box`-collision tests (verifies-clean, correct-constructor, and the
  false-prove probe) back to the false E500.
- Tuple site (`_get_or_create_tuple_sort`): a `Tuple<Tuple<Int>, Int>` vs
  `Tuple<Tuple<Int, Int>>` collision. Both keys lossy-sanitize to
  `Tuple_Tuple_Int_Int`; under the lossy name the two synthesised tuple
  sorts share one Z3 datatype, and a match arm projecting a field index
  the conflated sort does not carry crashes the verifier with
  `z3.z3types.Z3Exception: Invalid accessor index` at `sort.accessor`
  (in `_bind_pattern`). Reverting it flips the new tuple-collision test.
  Confirmed load-bearing: reverting this site with only the `Box`
  collision test present flipped nothing.

The rename also broke the verifier's Array-element reverse lookup, fixed
here since #884 caused it. `_get_element_sort_for_array`'s tier-3 fallback
reconstructed the `_z3_sorts` key by string surgery
(`elt_key.replace("_", "<", 1) + ">"`) that assumed the old lossy naming,
so after the rename a generic-ADT element (`Array<Box<Int>>` → sort
`Array_Box_LInt_R`) produced the non-matching candidate `Box<LInt_R>` and
the lookup silently returned None. Latent — tier 1's creation-time direct
map (`_array_element_sorts`) fires for every live path, and no corpus
program indexes an `Array<Generic<T>>` in a contract this way — but
dead-on-arrival for that shape. A new injective inverse
`unmangle_type_name` (a left-to-right prefix-code decode, round-trip-tested
against `mangle_type_name`) recovers the key correctly, and the stale
tier-3 comment is corrected.

Pinned by tests/test_verifier_sort_name_collision_884.py (ADT + tuple
collisions, rename-control, false-prove disproved for the right reason),
the ch06_adt_sort_disambiguation conformance program,
TestSmtContextDirect.test_element_sort_reverse_lookup_tier3_generic_adt
(the Array-element unit pin), and the unmangle round-trip / non-range-input
tests in TestMangleInjectivity. Mutation-validated: reverting either
sort-name site to the lossy sanitize flips its collision test RED, and
reverting the Array-element lookup to the old string surgery flips the
reverse-lookup unit test RED.

Pre-existing on main; found by the PR #883 adversarial panel.

Co-Authored-By: Claude <[email protected]>

…onger collide (#884)

The verifier named Z3 datatype sorts with the old lossy sanitize
(`key.replace("<", "_").replace(">", "").replace(", ", "_")`), so a
monomorphized `Box<Int>` and a flat ADT literally named `Box_Int` both
became the Z3 name `Box_Int`. Z3's per-context datatype cache conflates
same-named sorts (the last `create()` wins and earlier same-named sorts
silently adopt its structure), so `Box<Int>`'s sort acquired the flat
ADT's `MkBoxInt(Bool)` constructor — a false E500 counterexample
(`@Box<Int>.0 = MkBoxInt(False)`) on trivially-true valid code.

Both Z3 sort-name sites (`_get_or_create_adt_sort` and
`_get_or_create_tuple_sort` in `vera/smt.py`) now route through the
injective `mangle_type_name` mangler #775 introduced for WAT symbols, so
distinct type keys can never share a Z3 sort name. The full-type-string
sort cache and the #871 nested-Float64 fpEQ walk are unaffected (the cache
is keyed by the type string, not the Z3-visible name).

Soundness-safe: the conflation only freed field constraints, producing
conservative false negatives, never a false Tier-1 — a genuinely-false
ensures over the colliding pair is still disproved after the fix, now with
the correct `MkBox` constructor.

Both sort-name sites are independently pinned, one collision per site, so
neither `mangle_type_name` call can be reverted without flipping a test:

- ADT site (`_get_or_create_adt_sort`): the `Box<Int>` / flat `Box_Int`
  collision. Reverting it re-collides the sorts and flips the three
  `Box`-collision tests (verifies-clean, correct-constructor, and the
  false-prove probe) back to the false E500.
- Tuple site (`_get_or_create_tuple_sort`): a `Tuple<Tuple<Int>, Int>` vs
  `Tuple<Tuple<Int, Int>>` collision. Both keys lossy-sanitize to
  `Tuple_Tuple_Int_Int`; under the lossy name the two synthesised tuple
  sorts share one Z3 datatype, and a match arm projecting a field index
  the conflated sort does not carry crashes the verifier with
  `z3.z3types.Z3Exception: Invalid accessor index` at `sort.accessor`
  (in `_bind_pattern`). Reverting it flips the new tuple-collision test.
  Confirmed load-bearing: reverting this site with only the `Box`
  collision test present flipped nothing.

The rename also broke the verifier's Array-element reverse lookup, fixed
here since #884 caused it. `_get_element_sort_for_array`'s tier-3 fallback
reconstructed the `_z3_sorts` key by string surgery
(`elt_key.replace("_", "<", 1) + ">"`) that assumed the old lossy naming,
so after the rename a generic-ADT element (`Array<Box<Int>>` → sort
`Array_Box_LInt_R`) produced the non-matching candidate `Box<LInt_R>` and
the lookup silently returned None. Latent — tier 1's creation-time direct
map (`_array_element_sorts`) fires for every live path, and no corpus
program indexes an `Array<Generic<T>>` in a contract this way — but
dead-on-arrival for that shape. A new injective inverse
`unmangle_type_name` (a left-to-right prefix-code decode, round-trip-tested
against `mangle_type_name`) recovers the key correctly, and the stale
tier-3 comment is corrected.

Pinned by tests/test_verifier_sort_name_collision_884.py (ADT + tuple
collisions, rename-control, false-prove disproved for the right reason),
the ch06_adt_sort_disambiguation conformance program,
TestSmtContextDirect.test_element_sort_reverse_lookup_tier3_generic_adt
(the Array-element unit pin), and the unmangle round-trip / non-range-input
tests in TestMangleInjectivity. Mutation-validated: reverting either
sort-name site to the lossy sanitize flips its collision test RED, and
reverting the Array-element lookup to the old string surgery flips the
reverse-lookup unit test RED.

Pre-existing on main; found by the PR #883 adversarial panel.

Co-Authored-By: Claude <[email protected]>