Canonical Byte-String Encoding for Finite-Ring Cryptosystems
Kyrylo Riabov, Serhii Kryvyi
cs.CR
Mar 24, 2026 · v1
TL;DR
Provides a Lean 4 formalization of an rANS-based byte-to-residue codec with machine-checked roundtrip proofs.
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.
Problem
Ring-mapping cryptographic protocols need a canonical byte-to-residue layer before any algebraic encryption step can begin. Existing approaches use hand-built alphabets and small fixed symbol tables, leaving open the general problem of encoding arbitrary binary data as finite-ring elements.
Approach
The paper presents the base-m length codec, a canonical map from byte strings of length less than 2^64 to lists of residues modulo m, adapting an rANS-based system. Decoding is exact for all moduli satisfying stated parameter bounds, and tolerant to appended suffix digits because the encoding carries the byte length in a fixed-width header. A Lean 4 formalization verifies the core round-trip correctness properties, while a Rust implementation provides the practical codec.
Results
The codec achieves exact round-trip encoding and decoding for all moduli m >= 2 satisfying the parameter bound 256 <= decoderLowerBound(w, m). The Lean 4 proofs cover the core correctness theorems. A Rust implementation demonstrates practical performance.
