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.

翻译：在代数加密步骤开始前，环映射协议需要一个规范的字节到剩余层的转换。本文将这一层独立出来，并提出了基-m长度编解码器，这是一种从长度小于2^64的字节串到模m剩余类列表的规范映射。该编码器基于并适配了Duda提出的rANS系统。在满足本文参数界限的所有模数条件下，解码是精确的。由于编码在其定宽头部携带字节长度，解码也能容忍附加的有效后缀数字。本文还提供了所描述协议的Rust实现、带机器校验证明的抽象编解码器的Lean 4形式化，以及性能基准测试。Lean 4形式化确立了定宽前缀反转和小于2^64的载荷状态界限、流级往返正确性，以及每个输出符号都是模m的有效剩余类。最后，我们进行了复杂性分析，并讨论了编解码器在实际使用中遇到的实际问题。