Hi Makarius, On 08/11/17 14:13, Makarius wrote:

On 08/11/17 12:35, Tobias Nipkow wrote:On 07/11/2017 23:13, Makarius wrote:For Flyspeck-Tame a small performance loss remains. It might be worth trying to configure the Isabelle/HOL codegen to use FixedInt instead of regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1 than with 5.6.Just as for Isabelle itself, I don't want generated code to abort with overflow or even worse to overflow silently.I also don't want to see FixedInt used routinely instead of proper mathematical Int. The idea above is to provide an option for the HOL codegen that is used specifically for applications like Flyspeck-Tame. It is mainly a question to codegen experts, if that can be done easily.

`My AFP entry Native_Word basically provides the setup for unsigned fixed-size integers,`

`but as a separate type uintXX. The same could be done for signed fixed-size integers. The`

`problem is how to get from int to uintXX. There are basically two options:`

1. Just axiomatize that int are implemented with uintXX. This is potentially unsound.

`2. Prove that actually no overflow occurs in the computations. The AFP entry`

`Berlekamp-Zassenhaus does that for factoring polynomials over finite fields. The basic`

`setup is there, but applying it to a particular instance requires quite some work.`

`FixedInt has the additional challenge that the width is implementation dependent, so this`

`requires a few tricks similar to the formalisation of uint in the AFP entry.`

`In summary: In principle it could be possible to use FixedInt in Flyspec-Tame in a sound`

`way, but it would be quite a bit of work.`

Andreas _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev