In Rust, `constant` returns different values.

[ajewellamz]

Dafny version

4.9.1 (b998ed949)

Code to produce this issue

// const SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext := ...
method {:test} RunManifestTests() {
  var orig := SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext;
  for i := 0 to 100 {
    expect orig == SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext;
  }
}

Command to run and resulting output

git clone --recurse-submodules git@github.com:aws/aws-cryptographic-material-providers-library.git
cd aws-cryptographic-material-providers-library
git checkout ajewell/test-fail
cd TestVectorsAwsCryptographicMaterialProviders
make polymorph_rust transpile_rust test_rust

You should see a single test failure, in the test shown above.

What happened?

A constant should be constant. In Rust, this constant is variable.

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

Mac

[RitvikKapila]

The constant SuccessTestingRequiredEncryptionContextKeysReproducedEncryptionContext is defined here. It is a set composition and should output a set of 5 values every-time, but this constant computation is flaky.

A heads up, you will have to comment out the line inside the main function of implementation_from_dafny.rs to make the above configuration work every time you transpile code in Rust.

[ajewellamz]

This can be worked around n the Dafny code, so closing.

[robin-aws]

This turned out to be because of an invalid extern in the definition of the constant: a function that did not necessarily return the same output for the same input (because it depended on HashSet ordering).

Closing this, but also considering it a +1 on #5861