Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

C# Wrong Result: Multi-level Multisets #4011

Open
alex-usher opened this issue May 15, 2023 · 2 comments · Fixed by #5412 · May be fixed by #5497
Open

C# Wrong Result: Multi-level Multisets #4011

alex-usher opened this issue May 15, 2023 · 2 comments · Fixed by #5412 · May be fixed by #5497
Assignees
Labels
during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done

Comments

@alex-usher
Copy link

Dafny version

4.1.0

Code to produce this issue

method Main() {
	var a: multiset<bool> := multiset{false, true};
	var b: multiset<multiset<bool>> := multiset{a[true := 0]};

	print b == multiset{multiset{false}}, "\n";
}

Command to run and resulting output

$ dafny /compile:4 main.dfy

Dafny program verifier finished with 1 verified, 0 errors
Running...

false

$ dafny /compile:4 /compileTarget:js main.dfy

Dafny program verifier finished with 1 verified, 0 errors
Running...

true

What happened?

The above program verifies and compiles successfully to all backends, but the C# backend will print false while all others will print true (where true would be the expected case).

What type of operating system are you experiencing the problem on?

Linux, Mac

@alex-usher alex-usher added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label May 15, 2023
@alex-usher
Copy link
Author

Hi, just wanted to ping this issue as I believe it may be a soundness wrong result :)

@alex-usher alex-usher changed the title C# Miscompilation: Multi-level Multisets C# Wrong Result: Multi-level Multisets Oct 25, 2023
@keyboardDrummer keyboardDrummer added lang: c# Dafny's C# transpiler and its runtime during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly priority: next Will consider working on this after in progress work is done part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag labels Apr 25, 2024
@fabiomadge fabiomadge self-assigned this May 14, 2024
atomb added a commit that referenced this issue May 24, 2024
…5412)

Fixes #4011.

---------

Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
@robin-aws
Copy link
Member

Reopening because we had to revert the PR to fix nightly: #5492

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag priority: next Will consider working on this after in progress work is done
Projects
None yet
4 participants