### Abstract

We give a verified implementation of the Schönhage-Strassen Multiplication on Integers based on the original paper by Schönhage and Strassen and verify its asymptotic complexity of $\mathcal{O}\left(n \log n \log \log n\right)$ bit operations. Integers are represented as LSBF (least significant bit first) boolean lists. The running time is verified using the Time Monad defined in Root-Balanced Trees by Nipkow. For verifying correctness, we adapt the formalization of Number Theoretic Transforms (NTTs) by Ammer and Kreuzer to the context of rings that need not be fields.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical
- Mathematics/Algebra

### Related publications

- https://mediatum.ub.tum.de/1717658

### Session Schoenhage_Strassen

- Schoenhage_Strassen_Preliminaries
- Schoenhage_Strassen_Runtime_Preliminaries
- Schoenhage_Strassen_Ring_Lemmas
- NTT_Rings
- FNTT_Rings
- Z_mod_power_of_2
- Z_mod_power_of_2_TM
- Z_mod_Fermat
- Z_mod_Fermat_TM
- Schoenhage_Strassen
- Schoenhage_Strassen_TM

### Depends on

- The Akra-Bazzi theorem and the Master theorem
- Karatsuba Multiplication on Integers
- Number Theoretic Transform
- Root-Balanced Tree
- Universal Hash Families
- Finite Machine Word Library

## Cite

×

Schoenhage_Strassen-AFP

    @article{Schoenhage_Strassen-AFP,
      author  = {Jakob Schulz},
      title   = {Schönhage-Strassen Multiplication},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Schoenhage_Strassen.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest