WIP: Add FIPS-aligned AES specification

[hanno-becker]

This is a work-in-progress attempt add adding an alternative model AESSpec.lean of the AES specification that's closely aligned to the FIPS specification. The existing model in AESArm.lean and AESCommon.lean is more aligned to the Arm ASL for AES instructions.

Status: So far I merely added various interpretations of AES state as (a) bitvector, (b) byte sequence, (c) 4x4 byte grid, and conversions between them.

This is my first attempt at doing anything with Lean, and I'm sure there's a lot to improve. I'm grateful about any comments 🙏