Verified fast formulas for control bits for permutation networks

Daniel J.  Bernstein

Paper 2020/1493

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.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint. MINOR revision.
Keywords: sorting networks permutation networks Beneš networks Clos networks Stone's algorithm Nassimi–Sahni algorithm constant-time algorithms parallelization vectorization
Contact author(s): authorcontact-controlbits @ box cr yp to
History: 2020-11-29: received
Short URL: https://ia.cr/2020/1493
License: CC BY

BibTeX

@misc{cryptoeprint:2020/1493,
      author = {Daniel J.  Bernstein},
      title = {Verified fast formulas for control bits for permutation networks},
      howpublished = {Cryptology {ePrint} Archive, Paper 2020/1493},
      year = {2020},
      url = {https://eprint.iacr.org/2020/1493}
}