WIP: Add FIPS-aligned AES specification #29
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is a minimal attempt at providing a elimination tactic `elim`. Elimination rules are a unified and principled way to destruct various kinds of premises, and ubiquituous in Isabelle. While std and mathlib have custom destruction tactics, we try to avoid external dependencies as much as possible here. Signed-off-by: Hanno Becker <[email protected]>
This commit adds definition and basic constructions and lemmas for a type `Vec t n` of length-n lists of type `t`. This exists in Mathlib, but in the interest of keeping dependencies down (and as a useful learning exercise), we re-implement the required material here. Signed-off-by: Hanno Becker <[email protected]>
`simp` rules for `extractLsb'` and `cast` / `append` Signed-off-by: Hanno Becker <[email protected]>
This commit adds `AESSpec.lean` which aims to model the AES specification in a way that's as close to the FIPS specification as possible (the existing specification in `AESArm.lean` is more aligned to the Arm ASL). This is work in progress. For the moment, we only have definitions of the AES state as a bitvector, byte vector, or byte array, as well as conversions between them. Signed-off-by: Hanno Becker <[email protected]>
shigoel
reviewed
May 2, 2024
| def example_bitvec' := byte_seq_to_bitvec example_byteseq | ||
| def example_byteseq' := bitvec_to_byte_seq 16 example_bitvec' | ||
|
|
||
| #eval example_bitvec |
There was a problem hiding this comment.
I'd recommend using example to test these out instead of using #eval. E.g., see
Line 165 in bdfadd5
|
I don't have the bandwidth to push this at the moment. I'll close for now and reopen if things change. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a work-in-progress attempt add adding an alternative model
AESSpec.leanof the AES specification that's closely aligned to the FIPS specification. The existing model inAESArm.leanandAESCommon.leanis 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 🙏