fix: compile Python reference-type equality to identity comparison - #6496
Open
fabiomadge wants to merge 6 commits into
Open
fix: compile Python reference-type equality to identity comparison#6496fabiomadge wants to merge 6 commits into
fabiomadge wants to merge 6 commits into
Conversation
Dafny gives class types identity equality, and the verifier reasons about them accordingly. The Python backend compiled == and != on reference types to Python's ==/!=, which dispatch to the overridable __eq__ hook — so an extern class overriding __eq__ (or a future generated override) made verified reference (in)equalities evaluate incorrectly at run time. Datatype __eq__ methods compared class-typed fields the same way. Emit 'is'/'is not' for EqCommon/NeqCommon at reference types, and identity comparisons for reference-typed fields in generated datatype __eq__ methods, mirroring how the Java and C# backends already special- case IsRefType at the same decision point (JavaCodeGenerator EqCommon emits '== (Object)'). Part of dafny-lang#6491 (the collection-level unsoundness on other backends is tracked there).
Following the ExternCtors.dfy convention removes the axiomatized factory method and its BigInteger handling from the extern; the structural __eq__ needs no state at all to subvert identity.
…ation The generic-datatype field case (G<T> instantiated at a reference type) and equality at abstract type parameters still compile to ==, matching the universal-equality fallbacks of the other backends; the helper's doc comment records this boundary explicitly.
This was referenced Jul 28, 2026
Document that reference-type == now compiles to identity (this PR), while the
built-in collections still consult __eq__/__hash__, so an extern overriding
those can still diverge from verified facts; point to datatype and
type {:extern} T(==) as the structural alternatives.
Relates to dafny-lang#6491.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of #6491. Dafny gives class types identity equality and the verifier reasons about them accordingly, but the Python backend compiled
==/!=on reference types to Python's==/!=, which dispatch to the overridable__eq__hook. An extern class overriding__eq__therefore made verified reference (in)equalities evaluate incorrectly at run time:Generated datatype
__eq__methods compared class-typed fields the same way, soD(a, 0) != D(b, 0)was also verified-true but runtime-false.Fix. Emit
is/is notforEqCommon/NeqCommonat reference types (afterDatatypeWrapperEraser.SimplifyType, as elsewhere), and identity comparisons for reference-typed fields in generated datatype__eq__methods. This mirrors the discrimination the Java and C# backends already make at the same decision point (JavaCodeGeneratoremits== (Object)for ref types;CsharpCodeGeneratoremits== (object)). Python was the only backend where even direct equality was affected.Non-regression checked:
x == null, trait-typed comparisons, array identity, and the equality-sensitivecomp/dafny0compile tests across all targets. The regression test uses an extern with a structural__eq__override, asserting both direct and datatype-field inequality survive compilation.Known boundary, documented on the new
EqualityOperatorhelper: equality at an abstract type parameter (e.g. insidemethod Eq<T(==)>(x: T, y: T), or a generic datatype'sT-typed field) still compiles to==— the static type is not a reference type there. This matches the other backends, whose universal-equality fallbacks (java.util.Objects.equals,object.Equals) have the same hole; closing it needs runtime type information (the TypeDescriptor discussion in #6491).Scope note: this intentionally does not address the collection-level unsoundness of #6491 (
set<Box>collapsing etc.), which exists on several backends and needs the runtime collections to key on identity for reference types — a larger, cross-backend design discussed in the issue.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.