(I'd have to figure out how to do the code equation stuff to make this
type actually usable the way nat is, but it should behave correctly in
proofs)

(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)

* Fix an issue in a proof of the hashmap

* Improve scalar_decr_tac

* Improve the error message of scalar_tac and add the missing Termination.lean

* Make progress on the proofs of the hashmap

* Make a minor modification to the hashmap

* Make progress on the hashmap

* Make progress on the proofs

* Make progress on the proofs

* Make progress on the proof of the hashmap

* Progress on the proofs of the hashmap

* Update a proof

* Update the Charon pin

* Make minor modifications to the hashmap

* Regenerate the tests

* Regenerate the hashmap

* Add lemmas to the Lean backend

* Make progress on the proofs of the hashmap

* Make a minor fix

* Finish the proof about the hashmap

* Update scalar_tac

* Make a minor modification in the hashmap

* Update the proofs of the hashmap

---------

Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local>
Co-authored-by: Son Ho <sonho@Sons-MBP.lan>