Rewrite the AES parameterized example to show off the new module system

[m-yac]

Currently the examples/param_modules/AES and cryptol-specs AES examples heavily rely on backticked module imports, as they were likely designed to show off this feature. With this feature removed, we should rewrite these examples to show off the new module system, instead of directly adapting them. This would get rid of the clunky code which results from directly adapting these examples, and would add a good larger example of using interface modules to the repo.

[m-yac]

Once #1373 is incorporated, we should just use that feature instead of rewriting the whole example.