Hello everyone,
I've got two questions:
1. Can anyone point me to a theory in HOL formalizing matrx multiplication?
2. I need to formalize a linear-feedback shift register. They are
usually expressed in finite field arithmetic as a polynomial mod 2. So
far I've only found a theory for polynomials over \mathbb{R}. Am I right
that modelling the LSFR via wordslib is the easiest way?
Cheers, Robert
--
Robert Künnemann, Ph.D.
Security in Information Technology, TU Darmstadt
Mornewegstraße 30, Room 4.1.05, D64293 Darmstadt
Phone: +49 6151 16 75532
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
