How to prove the finite property for the type GF2pow8
 Prove that for a fixed
n
,GF2powN
is finite by induction on the degree. Case
0
, trivial.  Case
(Suc N)
. Case
(Suc 0)
, trivial.  Case
(Suc (Suc M))
, the set can be generated from the degree(Suc M)
.
 Case
 Case
 Automatically for case
8
, the set is finite.
How to implement the inverse using the extended Euclidean algorithm
 Refer to the
bezw
term.  Using a new userdefined induct rule:
 Assumes \(\bigwedge m.~P~m~0\) and \(\bigwedge m.~P~m~1\) and \(\bigwedge m~n.~0 ≠ n ⟹ 1 ≠ n ⟹ P~n (m \mod n) ⟹ P ~m~n\)
 Shows \(P~m~n\)
How to prove the irreduciblity?
 Basic idea, by brute force all the polys whose degrees less that 9.
 Also a new induct rule?
 How to apply the calculation process?
 Prove each degree seperately, along with some obvious lemmas. (For example, degree (8  m) and degree m can be taken together.)
 Maybe there is no automatic way to prove this. (What if the degree is larger?)
How to model the representations?
Like bit lists, natural numbers range from 0–256.
Use bin_to_bl
and bl_to_bin
functions to convert between naturals and \(\text{GF}_2^8\). But be cautious about the sequence of the bits in this representation. It may be reversed.
About the computation of the conversion between numbers and \(\text{GF}_2^8\) elements, we will talk about it in the Code Generation Part.
Failed attempts:
 To instantiate the
countable
class: it providesfrom_nat
andto_nat
functions, but it seems that the constants related lemma can’t be proved by simply applyingeval
(some basic problems with the code gen part).  To instantiate the
numeral
class: it will comprehend terms like0x08
as \(\text{GF}_2^8\) type, but in an “addone” way, thus the results can be only 1 or zero since add is actually binary XOR.
How to formalize the computation between the matrices?
Using Jordan_Normal_Form.Matrix
from AFP for now.
Use HOLAnalysis.Finite_Cartesian_Product
. Build the matrices from vectors, and build the vectors from vec_lambda
constructor.
Implement the numeral type four
to formalize the index of the matrices.
We can just use the numeral type predefined in theory HOLLibrary.Numeral_Type
. More concretly, use HOLLibrary.Typed_length
.
About the computations, this theory provides many useful functions:
map_matrix
 the inherited plus, multiply or something else.
Proofs about the Cipher itself

Round Ops can be inversed.
 SubBytes, skipped for now, it is also related to the codegen part.
 MixColumns, assert that the used two matrices are indeed inversed to each other. (This assertion need to be proved further).
 ShiftRows. The \((+1)\) operation for numeral types can help.
 AddRoundKey. The add for \(\text{GF}_2^8\) is actually XOR. Thus this can be proved simply.

Ciphers that using these Round Ops
 The key_schedule part is straightforward. (\( \forall k, f(k) = f(k) \))
 Unfolding all the definitions and former lemmas.
Code Generation
Three problems. (Comments from Albert)

No constructor for the type
('a, 'b) vec
Note that
vec
is a typedefed type and it usually means that the code generation technology does not know how to represent this in code. Luckily, we can simply solve this problem by declaringvec_lambda
as the code_datatype andvec_lambda_beta
as a code equation (for evaluatingvec_nth
). 
Handling UNIV set in code
We still have problem with the code representation of UNIV. If you type
code_thms "(**)"
you will see that matrixmatrix multiplication involves the UNIV set and its representation isUNIV = List.coset []
. If you access the element of matrixmatrix multiplication via vec_nth, you will have aMatch
exception raised. 
Matrix equality in code
Previous solutions still would not allow you to evaluate whether two matrices are equal or not. If you try it immediately, it will keep (possibly) forever. The culprit is the equality definition of two matrices: two matrices are equal if their function representation is equal. This means that you have to evaluate for all domain that two functions are equal
f1 = f2 <> ∀x. f1 x = f2 x
and our domain here is unfortunately naturals. But we don’t actually have to do that if we monomorphise our matrices equality toGF2pow8^4^4
; we only need to check forset [0, 1, 2, 3]
or any four consecutive numbers.
What’s more, I need to read the related Isabelle refs to get a better understanding of codegen.
Lessons
 Use predefined lemmas and functions as much as possible. (use
find_consts
andfind_theorems
)  Tear the big problems apart into very very small pieces.
 Use class based other than locale based when possible.
(T.B.A)