  In this work, we verify the mutable LongMap from the Scala standard library,
a hash table using open addressing within a single array, using the Stainless
program verifier. As a reference implementation, we write an immutable map
based on a list of tuples. We then show that LongMap's operations correspond to
operations of this association list. To express the resizing of the hash table
array, we introduce a new reference swapping construct in Stainless. This
allows us to apply the decorator pattern without introducing aliasing. Our
verification effort led us to find and fix a bug in the original implementation
that manifests for large hash tables. Our performance analysis shows the
verified version to be within a 1.5 factor of the original data structure.
