Canonical Byte-String Encoding for Finite-Ring Cryptosystems

TL;DR

This paper introduces a canonical byte-string encoding for finite-ring cryptosystems, providing a formal, efficient, and verified method for byte-to-residue mapping with practical implementation and proofs.

Contribution

It presents the base-m length codec, a canonical byte-to-residue map with formal verification, implementation, and performance analysis for cryptographic applications.

Findings

Exact decoding for moduli within parameter bounds.

Encoding carries byte length, enabling suffix tolerance.

Formal proofs ensure correctness and bounds.

Abstract

Ring-mapping protocols need a canonical byte-to-residue layer before any algebraic encryption step can begin. This paper isolates that layer and presents the base-m length codec, a canonical map from byte strings of length less than 2^64 to lists of residues modulo m. The encoder builds on and adapts an rANS-based system proposed by Duda. Decoding is exact for all moduli satisfying the paper's parameter bounds. Because the encoding carries the byte length in its fixed-width header, decoding is also tolerant to appended valid suffix digits. The paper is accompanied by a Rust implementation of the described protocol, a Lean 4 formalization of the abstract codec with machine-checked proofs, and performance benchmarks. The Lean 4 formalization establishes fixed-width prefix inversion and payload-state bounds below 2^64, stream-level roundtrip correctness, and that every emitted symbol is a valid residue modulo m. We conclude with a complexity analysis and a discussion of practical considerations arising in real-world use of the codec.