Skip to content

fix: compare extern references by pointer identity in the Go runtime - #6497

Open
fabiomadge wants to merge 8 commits into
dafny-lang:masterfrom
fabiomadge:fix/6491-go-ref-identity
Open

fix: compare extern references by pointer identity in the Go runtime#6497
fabiomadge wants to merge 8 commits into
dafny-lang:masterfrom
fabiomadge:fix/6491-go-ref-identity

Conversation

@fabiomadge

@fabiomadge fabiomadge commented Jul 28, 2026

Copy link
Copy Markdown
Collaborator

Part of #6491, Go variant. Dafny gives class types identity equality, and every Dafny-generated reference type implements the runtime's EqualsGeneric interface accordingly (pointer equality for classes and arrays). Extern classes that do not implement EqualsGeneric fell through AreEqual's reflect.DeepEqual fallback, which follows pointers and compares structurally:

var a := new Box();  // extern class, plain Go struct
var b := new Box();
assert a != b;       // verified
var s := {a, b};
assert |s| == 2;     // verified — but the compiled set had 1 element

Unlike the equals()/__eq__ variants of #6491 on the other backends, no override is needed on the extern's part — any ordinary Go struct is affected, because DeepEqual on two pointers compares the pointees. This hits everywhere the runtime compares generically: set/multiset/map construction and membership, seq membership, and equality at type parameters.

Fix. In AreEqual, pointer-kind values that do not implement EqualsGeneric are compared by pointer identity instead of DeepEqual. Non-pointer values — the value representations that legitimately rely on the DeepEqual fallback — are unaffected, as is every EqualsGeneric implementor (all Dafny-generated types and the runtime's own collections). Applied to both runtime copies (DafnyRuntimeGo, DafnyRuntimeGo-gomod).

Non-regression checked: datatype structural equality, set-of-datatype dedup, generic equality at datatypes/sets/arrays, and the equality-sensitive comp/dafny0 lit tests across all targets; the Go runtime's own test suite passes. The lit regression test uses an extern Go struct with no methods at all, and a runtime unit test pins all three AreEqual regimes (extern pointers by identity, non-pointer values by DeepEqual, EqualsGeneric implementors by their method) plus cross-type pointer comparison.

Survey of in-repo Go externs (9 files: 7 test fixtures, 2 stdlib): none rely on structural DeepEqual equality. The standard library's own extern classes (Std.Concurrent's MutableMap et al.) hand-implement EqualsGeneric as pointer identity — the semantics this PR makes the default — and the one extern class implementing neither (ExternCtors-externs/Library.go) was a latent instance of the bug that its test never triggers. EqualsGeneric remains the opt-in for externs that want structural equality, now documented on the interface.

Notes for review: non-comparable dynamic types (funcs, maps, slices) cannot reach the new identity branch — their reflection kinds are not Ptr, so they keep the DeepEqual path and Go's ==-panic-on-non-comparable is unreachable; typed-nil pointers are intercepted earlier by IsDafnyNull. An extern class can still opt in to structural equality by implementing EqualsGeneric, which is matched before the pointer check. The identity branch is also ~6x faster than the DeepEqual call it replaces (8.5ns vs 55ns measured). docs/Compilation/Go.md and AreEqual's doc comment now state the identity rule.

Scope note: direct == on class types was already sound on Go (compiled to pointer comparison); this fixes the generic-comparison path. The remaining #6491 work on other backends (Java/C# collections honoring overridden equals) is tracked in the issue.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Dafny gives class types identity equality, and every Dafny-generated
reference type implements EqualsGeneric accordingly (pointer equality
for classes and arrays). Extern classes that do not implement
EqualsGeneric fell through AreEqual's reflect.DeepEqual fallback, which
follows pointers and compares structurally — so two distinct extern
objects with equal contents were 'equal' wherever the runtime compares
generically (set/multiset/map construction and membership, seq
membership, equality at type parameters), contradicting verified facts
like |{a, b}| == 2. Unlike the equals()/__eq__ variants of dafny-lang#6491 on
other backends, this needs no override on the extern's part: any plain
Go struct is affected.

In AreEqual, compare pointer-kind values that do not implement
EqualsGeneric by pointer identity instead of handing them to DeepEqual.
Non-pointer values (the value types that legitimately rely on the
DeepEqual fallback) are unaffected, as is every EqualsGeneric
implementor. Applied to both runtime copies.

Part of dafny-lang#6491.
The function-level doc comment still described DeepEqual as the
unconditional last resort; it now states the identity rule for
non-EqualsGeneric pointers, as does docs/Compilation/Go.md. The new
runtime test pins all three AreEqual regimes: extern references by
identity, non-pointer values by DeepEqual, EqualsGeneric implementors
by their own method.
State the contract where extern authors implement it: EqualsGeneric is
how an extern class chooses its equality (Std_Concurrent's MutableMap
is the conventional identity implementation), and the identity fallback
in AreEqual only governs pointers that did not opt in.
Cross-reference the EqualsGeneric opt-in documented in Compilation/Go.md and
point to the datatype / type {:extern} T(==) alternatives.

Relates to dafny-lang#6491.
The prior wording presented implementing EqualsGeneric as a plain 'opt in to
structural equality'; doing so on a reference type actually reintroduces the
collection-vs-identity divergence (the built-in collections then compare
structurally while the verifier and direct == use identity). State that it is
only appropriate for value-semantics externs.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant