Fix unsound record contract deduplication #2042
Merged
Conversation
This file contains 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
Contract equality code used to flat out ignore all of the metadata of a
fields, including contract annotations, which is obviously entirely
wrong. This means that `{foo | String}` and `{foo | Number}` was deemed
equal and deduplicated as the same contract.
This commit fixes the issue by comparing the metadata as well. Contract
labels are a subtle matter, and they are the only part that is ignored
by the contract equality code.
|
TODO:
|
jneem
approved these changes
Sep 16, 2024
Co-authored-by: jneem <[email protected]>
|
Bencher Report| Branch | 2042/merge |
| Testbed | ubuntu-latest |
⚠️ WARNING: The following Measure does not have a Threshold. Without a Threshold, no Alerts will ever be generated!Click here to create a new Threshold
For more information, see the Threshold documentation.
To only post results if a Threshold exists, set the--ci-only-thresholdsCLI flag.
Click to view all benchmark results
| Benchmark | Latency | nanoseconds (ns) |
|---|---|---|
| fibonacci 10 | 📈 view plot | 498,230.00 |
| pidigits 100 | 📈 view plot | 3,281,100.00 |
| product 30 | 📈 view plot | 820,750.00 |
| scalar 10 | 📈 view plot | 1,495,100.00 |
| sum 30 | 📈 view plot | 824,090.00 |
yannham
added a commit
that referenced
this pull request
Sep 17, 2024
* Fix contract equality unsound on records
Contract equality code used to flat out ignore all of the metadata of a
fields, including contract annotations, which is obviously entirely
wrong. This means that `{foo | String}` and `{foo | Number}` was deemed
equal and deduplicated as the same contract.
This commit fixes the issue by comparing the metadata as well. Contract
labels are a subtle matter, and they are the only part that is ignored
by the contract equality code.
* Add comparison of label's type_environment for safety
* Update core/src/typecheck/eq.rs
Co-authored-by: jneem <[email protected]>
* Add integration test for contract dedup unsoundness
---------
Co-authored-by: jneem <[email protected]>
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.
Closes #2041.
As hinted in the original issue, the culprit is indeed the contract deduplication optimization, and more specifically the contract equality checker. The checker only looks at the fields' values to establish equality without looking at the metadata, which is obviously wrong, as it would equate most contracts with the same structures such as
{foo | Number}and{foo | String}, since the distinction is in the metadata.This commit fixes the issue by comparing the field metadata as well.