**Verified fast formulas for control bits for permutation networks**

*Daniel J. Bernstein*

**Abstract: **This paper presents detailed and computer-verified proofs of formulas that, given a permutation pi of 2^m indices with m>=1, produce control bits for a standard permutation network that uses 2^m(m-1/2) swaps to apply pi to a list. The formulas match the control bits computed by a serial algorithm of Stone (1968) and a parallel algorithm of Nassimi–Sahni (1982). The proofs are a step towards computer-verified correctness proofs for efficient implementations of these algorithms.

**Category / Keywords: **implementation / sorting networks, permutation networks, Beneš networks, Clos networks, Stone's algorithm, Nassimi–Sahni algorithm, constant-time algorithms, parallelization, vectorization

**Date: **received 29 Nov 2020, last revised 29 Nov 2020

**Contact author: **authorcontact-controlbits at box cr yp to

**Available format(s): **PDF | BibTeX Citation

**Version: **20201129:191826 (All versions of this report)

**Short URL: **ia.cr/2020/1493

[ Cryptology ePrint archive ]