Currently, List type is used when we refer to a list of BitVec in functional specification of AES-GCM. This means information on the length of the list of BitVecs are lost. This can cause trouble when type inference requires knowing the length of the lists -- theorems would have to be defined manually for the length of lists. Rework the AES-GCM specification to use Vector type to see if it can simplify definitions.
Currently,
Listtype is used when we refer to a list ofBitVecin functional specification of AES-GCM. This means information on the length of the list ofBitVecs are lost. This can cause trouble when type inference requires knowing the length of the lists -- theorems would have to be defined manually for the length of lists. Rework the AES-GCM specification to use Vector type to see if it can simplify definitions.