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

not yet implemented in Rust #5871

Open
ajewellamz opened this issue Oct 29, 2024 · 0 comments
Open

not yet implemented in Rust #5871

ajewellamz opened this issue Oct 29, 2024 · 0 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@ajewellamz
Copy link
Collaborator

Dafny version

4.8.1

Code to produce this issue

Fro m the function this is from the function AwsKmsMrkAreUnique in MPL/src/Keyrings/AwsKms/AwsKmsMrkAreUnique.dfy


let mut duplicateMrkIds: Set<Sequence<DafnyCharUTF16>> = (&({
    let mut mrkKeyIds = mrkKeyIds.clone();
    Rc::new(move || -> Set<Sequence<DafnyCharUTF16>>{
        let mut _coll0: SetBuilder<Sequence<DafnyCharUTF16>> = SetBuilder::<Sequence<DafnyCharUTF16>>::new();
        for r#__compr_0 in (&mrkKeyIds).iter() {
          let mut x: Sequence<DafnyCharUTF16> = r#__compr_0.clone();
          if mrkKeyIds.contains(&x) && mrkKeyIds.as_dafny_multiset().get((&x)/*<i>Coercion from ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> to ::dafny_runtime::DafnyInt</i> not yet implemented*/) >= int!(1) {
            _coll0.add(&x)
          }
        }
        _coll0.build()
      })
  }))();


### Command to run and resulting output

```code
make transpile_rust

What happened?

if mrkKeyIds.contains(&x) && mrkKeyIds.as_dafny_multiset().get((&x)/Coercion from ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> to ::dafny_runtime::DafnyInt not yet implemented/) >= int!(1) {

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

Mac

@ajewellamz ajewellamz added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Oct 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Development

No branches or pull requests

1 participant