Re: [isabelle] bit vs. bool in HOL-Word

On 08/18/2013 07:35 PM, Brian Huffman wrote:
I created Library/Bit.thy in February 2009 as a theory of the field of
integers mod 2. One motivation was to be able to have polynomials with
integers mod 2 as coefficients, which have applications in
cryptography. (I had also been working on Library/Polynomial.thy
around the same time.) As a field, it is possible to use type "bit"
with polynomial operations like div, mod, and gcd.

Hi Brian,

could you describe in a bit more detail which aspects of finite fields
you have formalized? In particular, have you formalized the concept of
an irreducible polynomial, together with specific irreducibility criteria?
When I started a formalization of AES a while ago, I used a brute-force
approach to prove that the polynomial in the AES specification is actually
irreducible. More precisely, to prove that p is irreducible I proved that
no polynomial q with degree q \in { p div 2} divides p, but I was
wondering whether there are more clever ways of doing this.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.