Dafny to Rust transpiled code issue

[RitvikKapila]

Hi,
I am working on the ESDK for Rust and am facing some issues in transpiling Rust from Dafny. There is an Unsupported Error in the implementation_from_dafny.rs generated file. It is from this predicate method in the ESDK Dafny source code:

const ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH := UINT16_LIMIT - 2;

predicate method IsESDKEncryptionContext(ec: MPL.EncryptionContext) {
  && |ec| < UINT16_LIMIT
  && Length(ec) < ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH
  && forall element
  | element in (multiset(ec.Keys) + multiset(ec.Values))
  ::
    && HasUint16Len(element)
    && ValidUTF8Seq(element)
}

This is the erroneous transpiled code in implementation_from_dafny.rs:

    pub fn IsESDKEncryptionContext(ec: &Map<ValidUTF8Bytes, ValidUTF8Bytes>) -> bool {
      set!{r#_<i>Unsupported: DAST_dBinOp_dAnd with not 2 elements</i>.clone(), ec.cardinality() < crate::r#_StandardLibrary_Compile::r#_UInt_Compile::_default::UINT16_LIMIT() && _default::Length(ec) < _default::ESDK_CANONICAL_ENCRYPTION_CONTEXT_MAX_LENGTH(), set!{<i>Unsupported: quantifier with not 2 elements</i>.clone(), {
            let mut ec = ec.clone();
            Rc::new(move |r#__forall_var_0: &ValidUTF8Bytes| -> bool{
                let mut element: ValidUTF8Bytes = r#__forall_var_0.clone();
                if {
                    let i: Sequence<u8> = element.clone();
                    crate::UTF8::_default::ValidUTF8Seq(&i)
                  } {
                  !ec.keys().as_dafny_multiset().merge(&ec.values().as_dafny_multiset()).contains(&element) || crate::r#_StandardLibrary_Compile::r#_UInt_Compile::_default::HasUint16Len::<u8>(&element) && crate::UTF8::_default::ValidUTF8Seq(&element)
                } else {
                  true
                }
              })
          }}, <i>Unsupported: <i>EmitMultiSetBoundedPool</i></i>.clone()}
    }

The stacktrace when I run cargo test is as follows. This catches the issue in transpile rust:

Compiling aws-esdk v0.1.0 (<path to the directory redacted>)
error: `_` cannot be a raw identifier
     --> src/implementation_from_dafny.rs:86826:12
      |
86826 |       set!{r#_<i>Unsupported: DAST_dBinOp_dAnd with not 2 elements</i>.clone(), ec.cardinality() < crate::r#_StandardLibrary_Compile::r...
      |            ^^^

error: comparison operators cannot be chained
     --> src/implementation_from_dafny.rs:86826:15
      |
86826 |       set!{r#_<i>Unsupported: DAST_dBinOp_dAnd with not 2 elements</i>.clone(), ec.cardinality() < crate::r#_StandardLibrary_Compile::r...
      |               ^ ^
      |
     ::: /Users/rkapila/Documents/projects/esdk-rust/aws-encryption-sdk-dafny/AwsEncryptionSDK/runtimes/rust/dafny_runtime_rust/src/lib.rs:2469:8
      |
2469  |     ($($x:expr), *) => {
      |        ------- while parsing argument for this `expr` macro fragment
      |
      = help: use `::<...>` instead of `<...>` to specify lifetime, type, or const arguments
      = help: or use `(...)` if you meant to specify fn arguments

error: could not compile `aws-esdk` (lib) due to 2 previous errors
warning: build failed, waiting for other jobs to finish...
error: could not compile `aws-esdk` (lib test) due to 2 previous errors

[MikaelMayer]

Looks like the enumeration for multisets hasn't been implemented I'll work on that.