Email Gateway (Aug 19 2022 at 11:39): Email Gateway (Aug 19 2022 at 11:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hello all,
I have been revisiting the HOL-Word theories, and a central question
which has come to my mind is how bits are to be represented. Some
theories are just using bool, but some use a dedicated but also
two-valued type bit. This mixture is awkward. Further, it seems to me
that the use of the bit type (in connection with the pseudo infix
constructor _ BIT _, which is the seed of almost all further usages of
type bit) goes back to the ancient numeral representation as signed bit
strings, which is now gone.
So, I would call for feedback from users of the HOL-Word theories:
Is there a reason to prefer bit over bool or the other way round, and
if yes, in which situations? Or does that just appear as accident?
If bool would be the preferred type, is it feasible (wrt. to existing
applications »outside there«) to replace bit by bool entirely? This
could also include input syntax 0 and 1 for False and True respectively,
a conversion of_bool :: bool => 'a::zero_neq_one etc.
Suggestions welcome,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:40):From: Brian Huffman <huffman.brian.c@gmail.com>
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.
The connections between Bit.thy and the ancient numeral representation
using _ BIT _ are accidental (see rev. 8e33b9d04a82); it is just a
coincidence that the new type is also named "bit". The other uses of
Bit.thy in HOL-Word are also likely due to my choice of the name of
the type "bit" more than anything else. Perhaps "Z2" or "z2" would
have been a better name for the new type; I just thought that an
English word would fit better with Isabelle's naming conventions.
In summary: I never meant for Library/Bit.thy to have any connection
whatsoever to HOL-Word; I'd be in favor of converting HOL-Word to use
type bool instead. Also, I'm open to renaming Library/Bit.thy to more
accurately describe its contents and intended use.
Email Gateway (Aug 19 2022 at 11:40):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
I'll try to give you my understanding of the situation.
As users, we mostly use these n-bit machine word representations:
- as lists of booleans of length n (to_bl/of_bl)
- as functions from a domain of cardinality n to bool (test_bit)
- as naturals modulo 2^n (unat/of_nat)
- as nonnegative integers modulo 2 ^ n (uint/word_of_int)
- as a integers - 2 ^ (n - 1) <= x < 2 ^ (n - 1) (sint/word_of_int)
The word type could also have been defined as any of these
representations, and the strength of the library is that the user
doesn't need to care much what the underlying type definition is.
I think that HOL-Word has a lot of history in it. It was created around
the time of an earlier change in the numeral representation, which
annoyed its author somewhat and resulted in some compatibility layers.
As a user, seeing these layers, types and definitions is a strong
indication that you've dug too deep. The same goes for the "_ BIT _"
representation. I suspect that these representations only get used in
user proofs in evaluating concrete n-bit arithmetic (that is, the
simpset introduces them then removes them again).
So, in short, go ahead and reconcile. I don't think users will have too
much work to do if the key representations and theorems about them are
preserved.
Final comment, the word_bitwise representation Sascha and I worked on in
2010 uses the boolean list representation (to_bl/of_bl) or, more
precisely, its reverse (rev o to_bl/of_bl o rev). In hindsight, the HOL4
group's approach based on the function-to-bool representation (test-bit
in Isabelle) is probably smarter, since it caches better, though it
involves lots of natural inequalities which require simprocs to resolve
in Isabelle and are a bit of a nuisance. I'm not sure if that is even
slightly relevant.
Sincerely,
Thomas.
Email Gateway (Aug 19 2022 at 11:40):From: Stefan Berghofer <berghofe@in.tum.de>
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 {1..degree p div 2} divides p, but I was
wondering whether there are more clever ways of doing this.
Greetings,
Stefan
Email Gateway (Aug 19 2022 at 11:40):From: Brian Huffman <huffman.brian.c@gmail.com>
On Wed, Aug 21, 2013 at 8:57 AM, Stefan Berghofer <berghofe@in.tum.de> wrote:
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?
I haven't formalized very much: Polynomial.thy defines div, mod, and
gcd on univariate polynomials over a field, but I haven't formalized
irreducibility or proved any related theorems.
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 {1..degree p div 2} divides p, but I was
wondering whether there are more clever ways of doing this.
I guess there are ([1] suggests a few methods), but I don't know of
any formalizations of such methods in Isabelle.
[1] http://en.wikipedia.org/wiki/Factorization_of_polynomials_over_finite_fields
Email Gateway (Aug 19 2022 at 11:43):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
thanks for the replies. I will give a short summary and give some clues
what I am actually aiming for. Note that this is just a roadmap for
future work, not anything I see for the near future (~ 3 months).
Concerning Bit.thy – this is something separate, a formalisation of
the Z2 field actually. It stand aparat, and references of the Word
theories to bit should be replaced by bool.
Concerning bit operations – these should use bool uniformly. Both
explicit list conversions and implicit structural operation like
test_bit and set_bit are relevant for user space. _ BIT _ is a historic
accident. The idea is to clearly separate the bit operations into
separate HOL-Library theories, to make them properly available for
applications which do not need words but bits.
This suggests a few refinements, which then lead to naming questions,
e.g. for bin_nth :: int => nat => bool the name does not really make
sense ;-). Maybe its best to have the bit operations in a theory named
Bit, to have qualified names like Bit.test :: 'a => nat => bool or
Bit.map :: nat => (bool => bool) => ('a => 'a) and such. Then the
existing Z2 theory should maybe really be named Z2. (Just rough
thoughts at the moment, not clear suggestions).
It is uncertain when I will come back to that issue, but the basic
landmarks are now far clearer than before.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/bit_bool/
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/bit_bool_afp/
where bool replaces bit as digit type throughout.
I invite users with heavy applications of the Word library to check this
first before bringing it upstream.
Happy proving,
Florian
signature.asc
Last updated: Apr 20 2024 at 08:16 UTC