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

Reply via email to