Define Scalars, anybytes using $@ without tuples or ptsto_bytes

[andres-erbsen]

Cc @miriampolzer @lukaszobernig This is the refactor I was talking about. It's not ready to land quite yet, but Fiat-crypto should build (but untested from clean build). You probably don't want to build on top of this branch, but perhaps it can be useful as a glimpse of things to come.

Key changes;

• Scalars are defined using le_split
• Memory.v rewritten, including definition of anybytes for stackalloc
• Array.v has stronger lemmas

Dependencies

• Develop theory about $@ coqutil#136
• Limit tuples to MachineWidth intetrface, remove from Memory riscv-coq#42
• absolutize some imports kami#43
• Semantics and Scalars without tuples bedrock2#474
• Replace tuples with $@ in Semantics, Scalars rupicola#162