chore: update mutable maps

[rishav-karanjit]

updating mutable maps based on: dafny-lang/dafny#5999

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[ssomayyajula]

Because MutableMap is the only extern in libraries, I suppose it's OK for it to be out of sync with DafnyStandardLibraries until we figure out what's going on with dafny-lang/dafny#6333, but I'll let the other reviewer decide.

[rishav-karanjit]

Because MutableMap is the only extern in libraries, I suppose it's OK for it to be out of sync with DafnyStandardLibraries until we figure out what's going on with dafny-lang/dafny#6333, but I'll let the other reviewer decide.

Yes. We (from crypto tools) just update it as we need it.

[ssomayyajula]

Since inv is now part of MutableMap, is there any reason why it's not part of the specs as in https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy? Do you not need it?

[MikaelMayer]

Works for me

[rishav-karanjit]

Since inv is now part of MutableMap, is there any reason why it's not part of the specs as in dafny-lang/dafny@master/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy? Do you not need it?

Its not part of spec in this PR because I did not needed that in MPL. You can add a suggestion if you recommend it or add it in a different PR. I am fine with either.

[ssomayyajula]

Oh got it, since it's ghost I don't have a problem. Approved