Stream: Is there code for X?

Topic: Efficient code generator setup for binary operations

Manuel Eberl (Jun 06 2024 at 14:54):

I'm wondering if there is any code generator setup on type int/nat for bit operations like AND, OR, XOR, NOT as well as bit shifts, bitlen, etc. Even when I include HOL-Library.Code_Target_Numeral these get translated to horribly inefficient integer arithmetic involving multiplication/division.

I am aware of the word library, which does these things for fixed-width integers, but I need it for arbitrary-precision integers.

I do have a proof-of-concept code generator setup for SML and Haskell that I could put in the distribution, but I want to make sure I'm not reinventing the wheel here.

Manuel Eberl (Jun 06 2024 at 14:58):

I just found this: https://www.isa-afp.org/entries/Native_Word.html

That does include some of the things I want, but not all of them; in particular no support for things like bitlen or floorlog2.

In any case I think this should really go into the distribution.

Wenda Li (Jun 07 2024 at 09:25):

Agreed. On the other hand, I am always curious why many other more dedicated projects like 'MicroJava' and several protocol verifications are in the distribution. Not sure if they are re-used that often these days.

Manuel Eberl (Jun 07 2024 at 09:28):

Historic reasons. These predate the AFP, I think. The last time I suggested that they be moved to the AFP I think I was told that these are not interesting enough or not "nice" enough to be moved there.

Wenda Li (Jun 07 2024 at 09:50):

I see. Probably something we can do in the future. I do think the standard library should ideally be more actively maintained/reused than an 'archive'~

Manuel Eberl (Jun 07 2024 at 09:52):

I would definitely second that.

Manuel Eberl (Jun 07 2024 at 09:52):

But generally there is the problem that the barrier between the distribution and the AFP is not very well-defined

Manuel Eberl (Jun 07 2024 at 09:53):

There's also all these "ex"/"examples" theories in the distribution, but I think I don't really mind those.

Manuel Eberl (Jun 07 2024 at 09:53):

I did e.g. move Bernoulli from there to the AFP once though because I needed it.

Manuel Eberl (Jun 07 2024 at 09:53):

(and significantly extended it in the process)

Last updated: Dec 21 2024 at 16:20 UTC