Email Gateway (Aug 18 2022 at 12:51): Email Gateway (Aug 18 2022 at 12:51):From: "Janney, Mark-P26816" <Mark.Janney@gdc4s.com>
Greetings -
I am working on a formal development of an efficient software algorithm
to calculate a proprietary cyclic redundancy check (CRC). This CRC
itself is defined in the usual fashion in terms of polynomials over
GF(2).
Rather than re-invent the wheel, I'd like to re-use existing Isabelle
theories as much as possible. I'm interested in theories in any of the
following areas:
-- polynomials over a field
-- GF(2)
-- CRC specifications and algorithms
If anyone can point me towards such material, I would be grateful.
Thanks - Mark Janney
Email Gateway (Aug 18 2022 at 12:52):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Mark,
The Isabelle distribution contains two different formalizations of
polynomials, each with its own tradeoffs.
First, there is Univ_Poly.thy, created by Amine Chaieb for use in his
proof of the fundamental theorem of algebra. This theory is
automatically included if your theory imports Complex_Main. It does
not define a type constructor for polynomials, but rather implements
all operations in terms of lists.
Second, there is the collection of theories in HOL/Algebra/poly,
created by Clemens Ballarin. These theories define an actual type
constructor for polynomials, and they also include a formalization of
long division for polynomials, which I expect you would need for your
application. Unfortunately, the theories are rather out of date, and
do not use the same hierarchy of algebraic classes as the rest of
Isabelle/HOL. If you use them, you might have to provide some extra
instance proofs for the duplicated axclasses, and the proof automation
is not as good as it could be (since many simprocs in Isabelle/HOL are
specific to the type classes defined in Ring_and_Field.thy).
It would be nice to eventually merge these two theories, so that we
could have a type constructor for polynomials that supports all of the
usual operations, and is also integrated with the current type class
hierarchy. I have already done a bit of tinkering with these theories,
so if there is enough interest I would probably be willing to work on
this some more.
For GF(2), you could just import the HOL-Word image and use 1-bit
words. However, the Word library does not provide a field class
instance for this type. It probably wouldn't be too much work to just
define the type yourself.
Hope this helps,
Quoting "Janney, Mark-P26816" <Mark.Janney@gdc4s.com>:
Last updated: May 03 2024 at 04:19 UTC