Skip to main content

oxilean_std/coding_theory/
functions.rs

1//! Auto-generated module
2//!
3//! ๐Ÿค– Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::Node;
6use oxilean_kernel::{Declaration, Environment, Expr, Name};
7
8use super::types::{
9    BICMCapacityEstimator, BinaryVector, BurstErrorDetector, CSMeasurementMatrix, ChannelCapacity,
10    ConvolutionalEncoder, FountainCode, GF2m, HammingCode, HammingCode74, LinearCode, PolarCode,
11    PolarCodeBEC, ProductCode, ReedMullerCode, ReedSolomonCode, TurboCode,
12};
13
14pub fn app(f: Expr, a: Expr) -> Expr {
15    Expr::App(Node::new(f), Node::new(a))
16}
17pub fn cst(s: &str) -> Expr {
18    Expr::Const(Name::str(s), vec![])
19}
20pub fn prop() -> Expr {
21    Expr::Sort(oxilean_kernel::Level::zero())
22}
23pub fn type0() -> Expr {
24    Expr::Sort(oxilean_kernel::Level::succ(oxilean_kernel::Level::zero()))
25}
26pub fn nat_ty() -> Expr {
27    cst("Nat")
28}
29pub fn arrow(a: Expr, b: Expr) -> Expr {
30    Expr::Pi(
31        oxilean_kernel::BinderInfo::Default,
32        Name::str("_"),
33        Node::new(a),
34        Node::new(b),
35    )
36}
37/// `LinearCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€” an (n, k, d) linear code.
38pub fn linear_code_ty() -> Expr {
39    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
40}
41/// `GeneratorMatrix : Nat โ†’ Nat โ†’ Type` โ€” a kร—n generator matrix G.
42pub fn generator_matrix_ty() -> Expr {
43    arrow(nat_ty(), arrow(nat_ty(), type0()))
44}
45/// `ParityCheckMatrix : Nat โ†’ Nat โ†’ Type` โ€” an (n-k)ร—n parity-check matrix H.
46pub fn parity_check_matrix_ty() -> Expr {
47    arrow(nat_ty(), arrow(nat_ty(), type0()))
48}
49/// `HammingBound : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€” sphere-packing (Hamming) bound.
50pub fn hamming_bound_ty() -> Expr {
51    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
52}
53/// `SingletonBound : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€” Singleton bound d โ‰ค n - k + 1.
54pub fn singleton_bound_ty() -> Expr {
55    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
56}
57/// `PlotkinBound : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€” Plotkin bound on max codewords.
58pub fn plotkin_bound_ty() -> Expr {
59    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
60}
61/// `shannon_channel_coding : โˆ€ (R C : Real), R < C โ†’ ReliableComm R` โ€”
62/// reliable communication is possible for any rate below channel capacity.
63pub fn shannon_channel_coding_ty() -> Expr {
64    arrow(cst("Real"), arrow(cst("Real"), prop()))
65}
66/// `noisy_channel : โˆ€ (p : Real), BSCCapacity p = 1 - BinaryEntropy p` โ€”
67/// binary symmetric channel capacity is 1 - H(p).
68pub fn noisy_channel_ty() -> Expr {
69    arrow(cst("Real"), prop())
70}
71/// `hamming_perfect : โˆ€ (r : Nat), PerfectCode (HammingCode r)` โ€”
72/// Hamming codes (2^r-1, 2^r-r-1, 3) meet the Hamming bound exactly.
73pub fn hamming_perfect_ty() -> Expr {
74    arrow(nat_ty(), prop())
75}
76/// `reed_solomon_mds : โˆ€ (n k : Nat), MDS (ReedSolomon n k)` โ€”
77/// Reed-Solomon codes are maximum distance separable (meet the Singleton bound).
78pub fn reed_solomon_mds_ty() -> Expr {
79    arrow(nat_ty(), arrow(nat_ty(), prop()))
80}
81/// `SystematicCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€” an (n, k, d) code in systematic form [I_k | P].
82pub fn systematic_code_ty() -> Expr {
83    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
84}
85/// `dual_code_parity_check_is_generator : Nat โ†’ Nat โ†’ Prop` โ€”
86/// the parity-check matrix of C is the generator matrix of the dual code C^โŠฅ.
87pub fn dual_code_parity_check_is_generator_ty() -> Expr {
88    arrow(nat_ty(), arrow(nat_ty(), prop()))
89}
90/// `systematic_encoding : Nat โ†’ Nat โ†’ Prop` โ€”
91/// every linear code is equivalent to a code in systematic form.
92pub fn systematic_encoding_ty() -> Expr {
93    arrow(nat_ty(), arrow(nat_ty(), prop()))
94}
95/// `HammingCodeOptimal : Nat โ†’ Prop` โ€”
96/// Hamming codes are the unique perfect single-error-correcting codes (up to equivalence).
97pub fn hamming_code_optimal_ty() -> Expr {
98    arrow(nat_ty(), prop())
99}
100/// `ExtendedHammingCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
101/// extended Hamming code (2^r, 2^r - r - 1, 4) obtained by adding an overall parity bit.
102pub fn extended_hamming_code_ty() -> Expr {
103    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
104}
105/// `ReedSolomonMinDistance : Nat โ†’ Nat โ†’ Prop` โ€”
106/// minimum distance of RS(n, k) over GF(q) is n - k + 1.
107pub fn reed_solomon_min_distance_ty() -> Expr {
108    arrow(nat_ty(), arrow(nat_ty(), prop()))
109}
110/// `ReedSolomonEvalEncoding : Nat โ†’ Nat โ†’ Type` โ€”
111/// RS encoding: evaluate a degree-(k-1) polynomial at n distinct field points.
112pub fn reed_solomon_eval_encoding_ty() -> Expr {
113    arrow(nat_ty(), arrow(nat_ty(), type0()))
114}
115/// `BCHCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
116/// BCH code of length n, design distance ฮด, over GF(q^m).
117pub fn bch_code_ty() -> Expr {
118    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
119}
120/// `BCHDesignDistance : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
121/// BCH bound: minimum distance of BCH code with design distance ฮด is โ‰ฅ ฮด.
122pub fn bch_design_distance_ty() -> Expr {
123    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
124}
125/// `BCHRootsExtensionField : Nat โ†’ Nat โ†’ Prop` โ€”
126/// roots of BCH generator polynomial lie in an extension field GF(q^m).
127pub fn bch_roots_extension_field_ty() -> Expr {
128    arrow(nat_ty(), arrow(nat_ty(), prop()))
129}
130/// `LDPCCode : Nat โ†’ Nat โ†’ Type` โ€” LDPC code defined by sparse parity-check matrix.
131pub fn ldpc_code_ty() -> Expr {
132    arrow(nat_ty(), arrow(nat_ty(), type0()))
133}
134/// `GallagerLDPC : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
135/// Gallager-constructed LDPC code with column weight j and row weight k.
136pub fn gallager_ldpc_ty() -> Expr {
137    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
138}
139/// `BeliefPropagationDecoding : Nat โ†’ Nat โ†’ Prop` โ€”
140/// belief propagation on the Tanner graph of an LDPC code achieves capacity on BEC.
141pub fn belief_propagation_decoding_ty() -> Expr {
142    arrow(nat_ty(), arrow(nat_ty(), prop()))
143}
144/// `PolarCode : Nat โ†’ Type` โ€” polar code of block length N = 2^n.
145pub fn polar_code_ty() -> Expr {
146    arrow(nat_ty(), type0())
147}
148/// `PolarCodeCapacityAchieving : Nat โ†’ Prop` โ€”
149/// polar codes achieve the capacity of any binary-input memoryless symmetric channel.
150pub fn polar_code_capacity_achieving_ty() -> Expr {
151    arrow(nat_ty(), prop())
152}
153/// `ChannelPolarization : Nat โ†’ Prop` โ€”
154/// after N successive cancellation steps, synthetic channels polarize to noiseless or pure-noise.
155pub fn channel_polarization_ty() -> Expr {
156    arrow(nat_ty(), prop())
157}
158/// `TurboCode : Nat โ†’ Nat โ†’ Type` โ€” turbo code constructed from two recursive systematic codes.
159pub fn turbo_code_ty() -> Expr {
160    arrow(nat_ty(), arrow(nat_ty(), type0()))
161}
162/// `TurboCodeNearCapacity : Nat โ†’ Nat โ†’ Prop` โ€”
163/// turbo codes can operate within a small fraction of Shannon capacity.
164pub fn turbo_code_near_capacity_ty() -> Expr {
165    arrow(nat_ty(), arrow(nat_ty(), prop()))
166}
167/// `ConvolutionalCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
168/// convolutional code with rate k/n and constraint length K.
169pub fn convolutional_code_ty() -> Expr {
170    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
171}
172/// `ViterbiAlgorithm : Nat โ†’ Nat โ†’ Prop` โ€”
173/// Viterbi algorithm achieves maximum-likelihood decoding for convolutional codes.
174pub fn viterbi_algorithm_ty() -> Expr {
175    arrow(nat_ty(), arrow(nat_ty(), prop()))
176}
177/// `ExpanderCode : Nat โ†’ Nat โ†’ Type` โ€” code based on bipartite expander graph.
178pub fn expander_code_ty() -> Expr {
179    arrow(nat_ty(), arrow(nat_ty(), type0()))
180}
181/// `ExpanderCodeLinearTimeDecoding : Nat โ†’ Nat โ†’ Prop` โ€”
182/// expander codes admit linear-time decoding algorithms.
183pub fn expander_code_linear_time_decoding_ty() -> Expr {
184    arrow(nat_ty(), arrow(nat_ty(), prop()))
185}
186/// `FountainCode : Nat โ†’ Type` โ€” rateless erasure code (e.g., Luby Transform).
187pub fn fountain_code_ty() -> Expr {
188    arrow(nat_ty(), type0())
189}
190/// `LubyTransformCode : Nat โ†’ Type` โ€” LT (Luby Transform) fountain code.
191pub fn luby_transform_code_ty() -> Expr {
192    arrow(nat_ty(), type0())
193}
194/// `RaptorCode : Nat โ†’ Type` โ€” Raptor code: pre-coded LT code with linear encoding/decoding.
195pub fn raptor_code_ty() -> Expr {
196    arrow(nat_ty(), type0())
197}
198/// `NetworkCodingCapacity : Nat โ†’ Nat โ†’ Prop` โ€”
199/// max-flow min-cut theorem: multicast capacity equals minimum cut capacity.
200pub fn network_coding_capacity_ty() -> Expr {
201    arrow(nat_ty(), arrow(nat_ty(), prop()))
202}
203/// `LinearNetworkCoding : Nat โ†’ Nat โ†’ Prop` โ€”
204/// linear network coding suffices to achieve multicast capacity.
205pub fn linear_network_coding_ty() -> Expr {
206    arrow(nat_ty(), arrow(nat_ty(), prop()))
207}
208/// `SpaceTimeCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
209/// space-time block code with n_t transmit antennas, n_r receive antennas, rate R.
210pub fn space_time_code_ty() -> Expr {
211    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
212}
213/// `AlamoutiScheme : Prop` โ€”
214/// Alamouti scheme achieves full diversity order 2 with 2 transmit antennas, simple decoding.
215pub fn alamouti_scheme_ty() -> Expr {
216    prop()
217}
218/// `LatticeCode : Nat โ†’ Type` โ€” lattice code in R^n.
219pub fn lattice_code_ty() -> Expr {
220    arrow(nat_ty(), type0())
221}
222/// `MinkowskiLatticeTheorem : Nat โ†’ Prop` โ€”
223/// Minkowski's theorem: a convex body of volume > 2^n contains a nonzero lattice point.
224pub fn minkowski_lattice_theorem_ty() -> Expr {
225    arrow(nat_ty(), prop())
226}
227/// `ListDecoding : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
228/// list decoder that outputs a list of codewords within Hamming distance e.
229pub fn list_decoding_ty() -> Expr {
230    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
231}
232/// `GuruswamiSudanDecoding : Nat โ†’ Nat โ†’ Prop` โ€”
233/// Guruswami-Sudan algorithm list-decodes RS codes up to 1 - โˆš(k/n) fraction of errors.
234pub fn guruswami_sudan_decoding_ty() -> Expr {
235    arrow(nat_ty(), arrow(nat_ty(), prop()))
236}
237/// `ParvareshVardyDecoding : Nat โ†’ Nat โ†’ Prop` โ€”
238/// Parvaresh-Vardy codes improve GS list-decoding radius using correlated polynomials.
239pub fn parvaresh_vardy_decoding_ty() -> Expr {
240    arrow(nat_ty(), arrow(nat_ty(), prop()))
241}
242/// `AlgebraicGeometryCode : Nat โ†’ Nat โ†’ Type` โ€”
243/// AG code (Goppa code) constructed from an algebraic curve over GF(q).
244pub fn algebraic_geometry_code_ty() -> Expr {
245    arrow(nat_ty(), arrow(nat_ty(), type0()))
246}
247/// `GoppaCodeMinDistance : Nat โ†’ Nat โ†’ Prop` โ€”
248/// Goppa code minimum distance satisfies d โ‰ฅ n - k (Goppa bound).
249pub fn goppa_code_min_distance_ty() -> Expr {
250    arrow(nat_ty(), arrow(nat_ty(), prop()))
251}
252/// `TsfasmanVladutZink : Nat โ†’ Prop` โ€”
253/// Tsfasman-Vladut-Zink theorem: AG codes exceed Gilbert-Varshamov bound for large alphabet.
254pub fn tsfasman_vladut_zink_ty() -> Expr {
255    arrow(nat_ty(), prop())
256}
257/// `StabilizerCode : Nat โ†’ Nat โ†’ Type` โ€”
258/// quantum stabilizer code encoding k logical qubits into n physical qubits.
259pub fn stabilizer_code_ty() -> Expr {
260    arrow(nat_ty(), arrow(nat_ty(), type0()))
261}
262/// `CSSCode : Nat โ†’ Nat โ†’ Type` โ€”
263/// Calderbank-Shor-Steane (CSS) code constructed from two classical codes C1 โŠ‡ C2.
264pub fn css_code_ty() -> Expr {
265    arrow(nat_ty(), arrow(nat_ty(), type0()))
266}
267/// `ToricCode : Nat โ†’ Type` โ€”
268/// Kitaev toric code on an Lร—L torus: encodes 2 logical qubits, distance L.
269pub fn toric_code_ty() -> Expr {
270    arrow(nat_ty(), type0())
271}
272/// `QuantumHammingBound : Nat โ†’ Nat โ†’ Prop` โ€”
273/// quantum Hamming (sphere-packing) bound for non-degenerate codes.
274pub fn quantum_hamming_bound_ty() -> Expr {
275    arrow(nat_ty(), arrow(nat_ty(), prop()))
276}
277/// `QuantumSingleton : Nat โ†’ Nat โ†’ Prop` โ€”
278/// quantum Singleton (Knill-Laflamme) bound: d โ‰ค n/2 - k/2 + 1 for non-degenerate codes.
279pub fn quantum_singleton_ty() -> Expr {
280    arrow(nat_ty(), arrow(nat_ty(), prop()))
281}
282/// `EliasBassalygo : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
283/// Elias-Bassalygo bound on maximum code size A(n, d).
284pub fn elias_bassalygo_ty() -> Expr {
285    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
286}
287/// `MRRWBound : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
288/// McEliece-Rodemich-Rumsey-Welch (MRRW) linear-programming bound.
289pub fn mrrw_bound_ty() -> Expr {
290    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
291}
292/// `GilbertVarshamov : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
293/// Gilbert-Varshamov lower bound: there exists a linear code with d โ‰ฅ ฮด
294/// and rate โ‰ฅ 1 - H(ฮด/n).
295pub fn gilbert_varshamov_ty() -> Expr {
296    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
297}
298/// `GreismerBound : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
299/// Griesmer bound on minimum length of a binary linear code with given k and d.
300pub fn griesmer_bound_ty() -> Expr {
301    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
302}
303/// `CapacityAchievingSequence : Nat โ†’ Prop` โ€”
304/// a sequence of codes achieves capacity if rate โ†’ C and error probability โ†’ 0.
305pub fn capacity_achieving_sequence_ty() -> Expr {
306    arrow(nat_ty(), prop())
307}
308/// `ShannonEntropy : Nat โ†’ cst(Real)` โ€” `H : Nat โ†’ Real`, discrete Shannon entropy.
309pub fn shannon_entropy_ty() -> Expr {
310    arrow(nat_ty(), cst("Real"))
311}
312/// `MutualInformation : Nat โ†’ Nat โ†’ cst(Real)` โ€” `I(X;Y) : Nat โ†’ Nat โ†’ Real`.
313pub fn mutual_information_ty() -> Expr {
314    arrow(nat_ty(), arrow(nat_ty(), cst("Real")))
315}
316/// `RegeneratingCode : Nat โ†’ Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
317/// (n, k, d, ฮฒ) regenerating code for distributed storage.
318pub fn regenerating_code_ty() -> Expr {
319    arrow(
320        nat_ty(),
321        arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0()))),
322    )
323}
324/// `MinimumStorageRegenerating : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
325/// MSR point: minimizes storage per node subject to exact repair.
326pub fn minimum_storage_regenerating_ty() -> Expr {
327    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
328}
329/// `MinimumBandwidthRegenerating : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
330/// MBR point: minimizes repair bandwidth subject to exact repair.
331pub fn minimum_bandwidth_regenerating_ty() -> Expr {
332    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
333}
334/// `LocallyDecodableCode : Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
335/// LDC with codeword length N, message length K, query complexity q.
336pub fn locally_decodable_code_ty() -> Expr {
337    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0())))
338}
339/// `LocallyDecodableCodeBound : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
340/// lower bound on codeword length for q-query LDCs.
341pub fn locally_decodable_code_bound_ty() -> Expr {
342    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
343}
344/// `TrellisCodedModulation : Nat โ†’ Nat โ†’ Type` โ€”
345/// TCM scheme combining coding and modulation with bandwidth efficiency b bits/s/Hz.
346pub fn trellis_coded_modulation_ty() -> Expr {
347    arrow(nat_ty(), arrow(nat_ty(), type0()))
348}
349/// `UngerboeckCodedModulation : Nat โ†’ Prop` โ€”
350/// Ungerboeck's set-partitioning TCM achieves coding gain without bandwidth expansion.
351pub fn ungerboeck_coded_modulation_ty() -> Expr {
352    arrow(nat_ty(), prop())
353}
354/// `SurfaceCode : Nat โ†’ Type` โ€”
355/// Kitaev surface code on an Lร—L planar lattice with distance L.
356pub fn surface_code_ty() -> Expr {
357    arrow(nat_ty(), type0())
358}
359/// `SurfaceCodeThreshold : Prop` โ€”
360/// surface codes have a fault-tolerance threshold above which logical error rates
361/// decrease exponentially with code distance.
362pub fn surface_code_threshold_ty() -> Expr {
363    prop()
364}
365/// `ColorCode : Nat โ†’ Type` โ€”
366/// topological color code on a 2-colex (2-colorable complex) of size parameter n.
367pub fn color_code_ty() -> Expr {
368    arrow(nat_ty(), type0())
369}
370/// `ColorCodeTransversalGates : Nat โ†’ Prop` โ€”
371/// 2D color codes support transversal implementation of the full Clifford group.
372pub fn color_code_transversal_gates_ty() -> Expr {
373    arrow(nat_ty(), prop())
374}
375/// `QuantumLDPCCode : Nat โ†’ Nat โ†’ Type` โ€”
376/// quantum LDPC code with n physical qubits and k logical qubits,
377/// defined by sparse check matrices.
378pub fn quantum_ldpc_code_ty() -> Expr {
379    arrow(nat_ty(), arrow(nat_ty(), type0()))
380}
381/// `QuantumLDPCGoodCode : Nat โ†’ Prop` โ€”
382/// good quantum LDPC codes have linear distance and linear rate simultaneously.
383pub fn quantum_ldpc_good_code_ty() -> Expr {
384    arrow(nat_ty(), prop())
385}
386/// `SpatiallyCoupledCode : Nat โ†’ Nat โ†’ Type` โ€”
387/// spatially coupled ensemble of LDPC codes achieving MAP threshold.
388pub fn spatially_coupled_code_ty() -> Expr {
389    arrow(nat_ty(), arrow(nat_ty(), type0()))
390}
391/// `ThresholdSaturation : Nat โ†’ Prop` โ€”
392/// threshold saturation: BP threshold of spatially coupled codes equals MAP threshold.
393pub fn threshold_saturation_ty() -> Expr {
394    arrow(nat_ty(), prop())
395}
396/// `ReedMullerCode : Nat โ†’ Nat โ†’ Type` โ€”
397/// Reed-Muller code RM(r, m) of order r in m variables.
398pub fn reed_muller_code_ty() -> Expr {
399    arrow(nat_ty(), arrow(nat_ty(), type0()))
400}
401/// `ReedMullerDecoding : Nat โ†’ Nat โ†’ Prop` โ€”
402/// Reed-Muller codes of order 1 are first-order Reed-Muller codes
403/// decodable by majority logic.
404pub fn reed_muller_decoding_ty() -> Expr {
405    arrow(nat_ty(), arrow(nat_ty(), prop()))
406}
407/// `ReedMullerCapacityAchieving : Prop` โ€”
408/// Reed-Muller codes achieve capacity on the binary erasure channel.
409pub fn reed_muller_capacity_achieving_ty() -> Expr {
410    prop()
411}
412/// `UniversallyDecodableMatrix : Nat โ†’ Nat โ†’ Type` โ€”
413/// UDM of dimension nร—m: rows form a code universal for combinatorial channels.
414pub fn universally_decodable_matrix_ty() -> Expr {
415    arrow(nat_ty(), arrow(nat_ty(), type0()))
416}
417/// `UDMCapacityAchieving : Nat โ†’ Nat โ†’ Prop` โ€”
418/// UDMs achieve capacity of the compound channel.
419pub fn udm_capacity_achieving_ty() -> Expr {
420    arrow(nat_ty(), arrow(nat_ty(), prop()))
421}
422/// `CompressedSensingMatrix : Nat โ†’ Nat โ†’ Type` โ€”
423/// mร—n measurement matrix satisfying the restricted isometry property.
424pub fn compressed_sensing_matrix_ty() -> Expr {
425    arrow(nat_ty(), arrow(nat_ty(), type0()))
426}
427/// `RestrictedIsometryProperty : Nat โ†’ Nat โ†’ Prop` โ€”
428/// RIP: every set of s columns of the measurement matrix is nearly orthonormal.
429pub fn restricted_isometry_property_ty() -> Expr {
430    arrow(nat_ty(), arrow(nat_ty(), prop()))
431}
432/// `BasisPursuitRecovery : Nat โ†’ Nat โ†’ Prop` โ€”
433/// basis pursuit (L1 minimization) recovers k-sparse signals from m โ‰ฅ O(k log(n/k))
434/// measurements.
435pub fn basis_pursuit_recovery_ty() -> Expr {
436    arrow(nat_ty(), arrow(nat_ty(), prop()))
437}
438/// `MIMOCapacity : Nat โ†’ Nat โ†’ Prop` โ€”
439/// MIMO channel capacity: C = log det(I + (SNR/n_t) H H^โ€ ) for n_t transmit, n_r receive
440/// antennas.
441pub fn mimo_capacity_ty() -> Expr {
442    arrow(nat_ty(), arrow(nat_ty(), prop()))
443}
444/// `MIMOSpacetimeDiversity : Nat โ†’ Nat โ†’ Nat โ†’ Prop` โ€”
445/// diversity-multiplexing tradeoff: d(r) = (n_t - r)(n_r - r) for MIMO channel.
446pub fn mimo_spacetime_diversity_ty() -> Expr {
447    arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), prop())))
448}
449/// `ProductCode : Nat โ†’ Nat โ†’ Nat โ†’ Nat โ†’ Type` โ€”
450/// tensor product code C1 โŠ— C2 with parameters (n1*n2, k1*k2, d1*d2).
451pub fn product_code_ty() -> Expr {
452    arrow(
453        nat_ty(),
454        arrow(nat_ty(), arrow(nat_ty(), arrow(nat_ty(), type0()))),
455    )
456}
457/// `ConcatenatedCode : Nat โ†’ Nat โ†’ Type` โ€”
458/// Forney concatenated code with outer code of length n and inner code of length m.
459pub fn concatenated_code_ty() -> Expr {
460    arrow(nat_ty(), arrow(nat_ty(), type0()))
461}
462/// `ConcatenatedCodeDecoding : Nat โ†’ Nat โ†’ Prop` โ€”
463/// concatenated codes decoded by generalized minimum distance (GMD) decoding
464/// can correct a fraction of errors.
465pub fn concatenated_code_decoding_ty() -> Expr {
466    arrow(nat_ty(), arrow(nat_ty(), prop()))
467}
468/// `InterleavedCode : Nat โ†’ Nat โ†’ Type` โ€”
469/// interleaved code with interleaving depth d over block length n.
470pub fn interleaved_code_ty() -> Expr {
471    arrow(nat_ty(), arrow(nat_ty(), type0()))
472}
473/// `BurstErrorCorrectionInterleaving : Nat โ†’ Nat โ†’ Prop` โ€”
474/// interleaving converts burst errors into random errors correctable by inner code.
475pub fn burst_error_correction_interleaving_ty() -> Expr {
476    arrow(nat_ty(), arrow(nat_ty(), prop()))
477}
478/// `PolarCodeBECCapacity : Nat โ†’ Prop` โ€”
479/// polar codes achieve BEC capacity with block-error rate O(2^{-N^{0.5}}).
480pub fn polar_code_bec_capacity_ty() -> Expr {
481    arrow(nat_ty(), prop())
482}
483/// `LDPCCapacityBEC : Nat โ†’ Prop` โ€”
484/// degree-optimized LDPC codes achieve BEC capacity under belief propagation.
485pub fn ldpc_capacity_bec_ty() -> Expr {
486    arrow(nat_ty(), prop())
487}
488/// `SpaghettiCodeAwgn : Nat โ†’ Prop` โ€”
489/// LDPC codes with optimized degree distributions approach AWGN capacity.
490pub fn ldpc_capacity_awgn_ty() -> Expr {
491    arrow(nat_ty(), prop())
492}
493/// `CRCPolarCode : Nat โ†’ Nat โ†’ Type` โ€”
494/// CRC-aided polar code with CRC length r and block length N = 2^n.
495pub fn crc_polar_code_ty() -> Expr {
496    arrow(nat_ty(), arrow(nat_ty(), type0()))
497}
498/// `PolarCodeSuccessiveCancellation : Nat โ†’ Prop` โ€”
499/// successive cancellation (SC) decoding of polar codes achieves O(N log N) complexity.
500pub fn polar_code_successive_cancellation_ty() -> Expr {
501    arrow(nat_ty(), prop())
502}
503/// `PolarCodeSCL : Nat โ†’ Nat โ†’ Prop` โ€”
504/// successive cancellation list (SCL) decoding of polar codes with list size L.
505pub fn polar_code_scl_ty() -> Expr {
506    arrow(nat_ty(), arrow(nat_ty(), prop()))
507}
508/// `BitInterleavedCodedModulation : Nat โ†’ Nat โ†’ Type` โ€”
509/// BICM scheme with code rate R and modulation order M.
510pub fn bit_interleaved_coded_modulation_ty() -> Expr {
511    arrow(nat_ty(), arrow(nat_ty(), type0()))
512}
513/// `BICMCapacity : Nat โ†’ Nat โ†’ Prop` โ€”
514/// BICM capacity equals the sum of mutual informations of individual bit channels.
515pub fn bicm_capacity_ty() -> Expr {
516    arrow(nat_ty(), arrow(nat_ty(), prop()))
517}
518/// `NonbinaryLDPC : Nat โ†’ Nat โ†’ Type` โ€”
519/// LDPC code over GF(q) with block length n and q = 2^m.
520pub fn nonbinary_ldpc_ty() -> Expr {
521    arrow(nat_ty(), arrow(nat_ty(), type0()))
522}
523/// `NonbinaryTurboCode : Nat โ†’ Nat โ†’ Type` โ€”
524/// turbo code over GF(q): two RSC codes over GF(q) with interleaver.
525pub fn nonbinary_turbo_code_ty() -> Expr {
526    arrow(nat_ty(), arrow(nat_ty(), type0()))
527}
528/// `QaryPolarCode : Nat โ†’ Nat โ†’ Type` โ€”
529/// polar code for q-ary symmetric channel with block length N and alphabet size q.
530pub fn qary_polar_code_ty() -> Expr {
531    arrow(nat_ty(), arrow(nat_ty(), type0()))
532}
533/// `WozencraftEnsemble : Nat โ†’ Nat โ†’ Prop` โ€”
534/// Wozencraft ensemble of random linear codes: most codes achieve GV bound.
535pub fn wozencraft_ensemble_ty() -> Expr {
536    arrow(nat_ty(), arrow(nat_ty(), prop()))
537}
538/// `RandomLinearCodeGV : Nat โ†’ Nat โ†’ Prop` โ€”
539/// random linear codes over GF(q) achieve the Gilbert-Varshamov bound with high
540/// probability.
541pub fn random_linear_code_gv_ty() -> Expr {
542    arrow(nat_ty(), arrow(nat_ty(), prop()))
543}
544/// `MacWilliamsTransform : Nat โ†’ Nat โ†’ Prop` โ€”
545/// MacWilliams identity: weight enumerator of C^โŠฅ is the MacWilliams transform of
546/// weight enumerator of C.
547pub fn mac_williams_transform_ty() -> Expr {
548    arrow(nat_ty(), arrow(nat_ty(), prop()))
549}
550/// `WeightEnumerator : Nat โ†’ Nat โ†’ Type` โ€”
551/// weight enumerator polynomial W_C(x, y) = ฮฃ_{c โˆˆ C} x^{n-wt(c)} y^{wt(c)}.
552pub fn weight_enumerator_ty() -> Expr {
553    arrow(nat_ty(), arrow(nat_ty(), type0()))
554}
555/// `BlahutArimoto : Nat โ†’ Prop` โ€”
556/// Blahut-Arimoto algorithm computes channel capacity and rate-distortion function.
557pub fn blahut_arimoto_ty() -> Expr {
558    arrow(nat_ty(), prop())
559}
560/// `RateDistortionFunction : Nat โ†’ Nat โ†’ Prop` โ€”
561/// Shannon rate-distortion theorem: R(D) = min_{p(xฬ‚|x): E\[d(X,Xฬ‚)\]โ‰คD} I(X; Xฬ‚).
562pub fn rate_distortion_function_ty() -> Expr {
563    arrow(nat_ty(), arrow(nat_ty(), prop()))
564}
565/// `ChannelCapacityConverse : Nat โ†’ Prop` โ€”
566/// converse to channel coding theorem: no code with rate R > C and vanishing error.
567pub fn channel_capacity_converse_ty() -> Expr {
568    arrow(nat_ty(), prop())
569}
570/// Populate `env` with all coding theory axioms and theorems.
571pub fn build_coding_theory_env(env: &mut Environment) {
572    let axioms: &[(&str, Expr)] = &[
573        ("LinearCode", linear_code_ty()),
574        ("GeneratorMatrix", generator_matrix_ty()),
575        ("ParityCheckMatrix", parity_check_matrix_ty()),
576        ("HammingBound", hamming_bound_ty()),
577        ("SingletonBound", singleton_bound_ty()),
578        ("PlotkinBound", plotkin_bound_ty()),
579        ("shannon_channel_coding", shannon_channel_coding_ty()),
580        ("noisy_channel", noisy_channel_ty()),
581        ("hamming_perfect", hamming_perfect_ty()),
582        ("reed_solomon_mds", reed_solomon_mds_ty()),
583        ("BinaryEntropy", arrow(cst("Real"), cst("Real"))),
584        ("BSCCapacity", arrow(cst("Real"), cst("Real"))),
585        ("BECCapacity", arrow(cst("Real"), cst("Real"))),
586        ("AWGNCapacity", arrow(cst("Real"), cst("Real"))),
587        ("HammingCode", arrow(nat_ty(), type0())),
588        ("ReedSolomon", arrow(nat_ty(), arrow(nat_ty(), type0()))),
589        ("PerfectCode", arrow(type0(), prop())),
590        ("MDS", arrow(type0(), prop())),
591        ("ReliableComm", arrow(cst("Real"), prop())),
592        ("SystematicCode", systematic_code_ty()),
593        (
594            "dual_code_parity_check_is_generator",
595            dual_code_parity_check_is_generator_ty(),
596        ),
597        ("systematic_encoding", systematic_encoding_ty()),
598        ("HammingCodeOptimal", hamming_code_optimal_ty()),
599        ("ExtendedHammingCode", extended_hamming_code_ty()),
600        ("ReedSolomonMinDistance", reed_solomon_min_distance_ty()),
601        ("ReedSolomonEvalEncoding", reed_solomon_eval_encoding_ty()),
602        ("BCHCode", bch_code_ty()),
603        ("BCHDesignDistance", bch_design_distance_ty()),
604        ("BCHRootsExtensionField", bch_roots_extension_field_ty()),
605        ("LDPCCode", ldpc_code_ty()),
606        ("GallagerLDPC", gallager_ldpc_ty()),
607        (
608            "BeliefPropagationDecoding",
609            belief_propagation_decoding_ty(),
610        ),
611        ("PolarCode", polar_code_ty()),
612        (
613            "PolarCodeCapacityAchieving",
614            polar_code_capacity_achieving_ty(),
615        ),
616        ("ChannelPolarization", channel_polarization_ty()),
617        ("TurboCode", turbo_code_ty()),
618        ("TurboCodeNearCapacity", turbo_code_near_capacity_ty()),
619        ("ConvolutionalCode", convolutional_code_ty()),
620        ("ViterbiAlgorithm", viterbi_algorithm_ty()),
621        ("ExpanderCode", expander_code_ty()),
622        (
623            "ExpanderCodeLinearTimeDecoding",
624            expander_code_linear_time_decoding_ty(),
625        ),
626        ("FountainCode", fountain_code_ty()),
627        ("LubyTransformCode", luby_transform_code_ty()),
628        ("RaptorCode", raptor_code_ty()),
629        ("NetworkCodingCapacity", network_coding_capacity_ty()),
630        ("LinearNetworkCoding", linear_network_coding_ty()),
631        ("SpaceTimeCode", space_time_code_ty()),
632        ("AlamoutiScheme", alamouti_scheme_ty()),
633        ("LatticeCode", lattice_code_ty()),
634        ("MinkowskiLatticeTheorem", minkowski_lattice_theorem_ty()),
635        ("ListDecoding", list_decoding_ty()),
636        ("GuruswamiSudanDecoding", guruswami_sudan_decoding_ty()),
637        ("ParvareshVardyDecoding", parvaresh_vardy_decoding_ty()),
638        ("AlgebraicGeometryCode", algebraic_geometry_code_ty()),
639        ("GoppaCodeMinDistance", goppa_code_min_distance_ty()),
640        ("TsfasmanVladutZink", tsfasman_vladut_zink_ty()),
641        ("StabilizerCode", stabilizer_code_ty()),
642        ("CSSCode", css_code_ty()),
643        ("ToricCode", toric_code_ty()),
644        ("QuantumHammingBound", quantum_hamming_bound_ty()),
645        ("QuantumSingleton", quantum_singleton_ty()),
646        ("EliasBassalygo", elias_bassalygo_ty()),
647        ("MRRWBound", mrrw_bound_ty()),
648        ("GilbertVarshamov", gilbert_varshamov_ty()),
649        ("GreismerBound", griesmer_bound_ty()),
650        (
651            "CapacityAchievingSequence",
652            capacity_achieving_sequence_ty(),
653        ),
654        ("ShannonEntropy", shannon_entropy_ty()),
655        ("MutualInformation", mutual_information_ty()),
656        ("RegeneratingCode", regenerating_code_ty()),
657        (
658            "MinimumStorageRegenerating",
659            minimum_storage_regenerating_ty(),
660        ),
661        (
662            "MinimumBandwidthRegenerating",
663            minimum_bandwidth_regenerating_ty(),
664        ),
665        ("LocallyDecodableCode", locally_decodable_code_ty()),
666        (
667            "LocallyDecodableCodeBound",
668            locally_decodable_code_bound_ty(),
669        ),
670        ("TrellisCodedModulation", trellis_coded_modulation_ty()),
671        (
672            "UngerboeckCodedModulation",
673            ungerboeck_coded_modulation_ty(),
674        ),
675        ("SurfaceCode", surface_code_ty()),
676        ("SurfaceCodeThreshold", surface_code_threshold_ty()),
677        ("ColorCode", color_code_ty()),
678        (
679            "ColorCodeTransversalGates",
680            color_code_transversal_gates_ty(),
681        ),
682        ("QuantumLDPCCode", quantum_ldpc_code_ty()),
683        ("QuantumLDPCGoodCode", quantum_ldpc_good_code_ty()),
684        ("SpatiallyCoupledCode", spatially_coupled_code_ty()),
685        ("ThresholdSaturation", threshold_saturation_ty()),
686        ("ReedMullerCode", reed_muller_code_ty()),
687        ("ReedMullerDecoding", reed_muller_decoding_ty()),
688        (
689            "ReedMullerCapacityAchieving",
690            reed_muller_capacity_achieving_ty(),
691        ),
692        (
693            "UniversallyDecodableMatrix",
694            universally_decodable_matrix_ty(),
695        ),
696        ("UDMCapacityAchieving", udm_capacity_achieving_ty()),
697        ("CompressedSensingMatrix", compressed_sensing_matrix_ty()),
698        (
699            "RestrictedIsometryProperty",
700            restricted_isometry_property_ty(),
701        ),
702        ("BasisPursuitRecovery", basis_pursuit_recovery_ty()),
703        ("MIMOCapacity", mimo_capacity_ty()),
704        ("MIMOSpacetimeDiversity", mimo_spacetime_diversity_ty()),
705        ("ProductCode", product_code_ty()),
706        ("ConcatenatedCode", concatenated_code_ty()),
707        ("ConcatenatedCodeDecoding", concatenated_code_decoding_ty()),
708        ("InterleavedCode", interleaved_code_ty()),
709        (
710            "BurstErrorCorrectionInterleaving",
711            burst_error_correction_interleaving_ty(),
712        ),
713        ("PolarCodeBECCapacity", polar_code_bec_capacity_ty()),
714        ("LDPCCapacityBEC", ldpc_capacity_bec_ty()),
715        ("LDPCCapacityAWGN", ldpc_capacity_awgn_ty()),
716        ("CRCPolarCode", crc_polar_code_ty()),
717        (
718            "PolarCodeSuccessiveCancellation",
719            polar_code_successive_cancellation_ty(),
720        ),
721        ("PolarCodeSCL", polar_code_scl_ty()),
722        (
723            "BitInterleavedCodedModulation",
724            bit_interleaved_coded_modulation_ty(),
725        ),
726        ("BICMCapacity", bicm_capacity_ty()),
727        ("NonbinaryLDPC", nonbinary_ldpc_ty()),
728        ("NonbinaryTurboCode", nonbinary_turbo_code_ty()),
729        ("QaryPolarCode", qary_polar_code_ty()),
730        ("WozencraftEnsemble", wozencraft_ensemble_ty()),
731        ("RandomLinearCodeGV", random_linear_code_gv_ty()),
732        ("MacWilliamsTransform", mac_williams_transform_ty()),
733        ("WeightEnumerator", weight_enumerator_ty()),
734        ("BlahutArimoto", blahut_arimoto_ty()),
735        ("RateDistortionFunction", rate_distortion_function_ty()),
736        ("ChannelCapacityConverse", channel_capacity_converse_ty()),
737    ];
738    for (name, ty) in axioms {
739        env.add(Declaration::Axiom {
740            name: Name::str(*name),
741            univ_params: vec![],
742            ty: ty.clone(),
743        })
744        .ok();
745    }
746}
747/// Volume of a Hamming ball of radius `t` in `{0,1}^n`: ฮฃ_{i=0}^{t} C(n,i).
748pub fn hamming_ball_volume(n: usize, t: usize) -> usize {
749    let mut vol = 0usize;
750    let mut binom = 1usize;
751    for i in 0..=t {
752        vol = vol.saturating_add(binom);
753        if i < t {
754            binom = binom.saturating_mul(n - i) / (i + 1);
755        }
756    }
757    vol
758}
759/// Approximation of erfc(x) = (2/โˆšฯ€) โˆซ_x^โˆž e^{-tยฒ} dt.
760///
761/// Uses the rational approximation from Abramowitz & Stegun ยง7.1.26
762/// with maximum absolute error < 1.5 ร— 10^{-7}.
763pub fn erfc_approx(x: f64) -> f64 {
764    if x < 0.0 {
765        return 2.0 - erfc_approx(-x);
766    }
767    let t = 1.0 / (1.0 + 0.3275911 * x);
768    let poly = t
769        * (0.254829592
770            + t * (-0.284496736 + t * (1.421413741 + t * (-1.453152027 + t * 1.061405429))));
771    poly * (-x * x).exp()
772}
773#[cfg(test)]
774mod tests {
775    use super::*;
776    #[test]
777    fn test_binary_vector_hamming_weight() {
778        let v = BinaryVector::from_bits(vec![true, false, true, true, false]);
779        assert_eq!(v.hamming_weight(), 3);
780        let z = BinaryVector::new(4);
781        assert_eq!(z.hamming_weight(), 0);
782    }
783    #[test]
784    fn test_binary_vector_xor_dot() {
785        let a = BinaryVector::from_bits(vec![true, false, true]);
786        let b = BinaryVector::from_bits(vec![true, true, false]);
787        let c = a.xor(&b);
788        assert_eq!(c.bits, vec![false, true, true]);
789        assert!(a.dot(&b));
790        let x = BinaryVector::from_bits(vec![true, false, false]);
791        let y = BinaryVector::from_bits(vec![false, true, false]);
792        assert!(!x.dot(&y));
793    }
794    #[test]
795    fn test_binary_vector_hamming_distance() {
796        let a = BinaryVector::from_bits(vec![true, false, true, false]);
797        let b = BinaryVector::from_bits(vec![false, false, true, true]);
798        assert_eq!(a.hamming_distance(&b), 2);
799    }
800    #[test]
801    fn test_linear_code_rate_redundancy() {
802        let code = LinearCode::new(7, 4, 3);
803        assert!((code.rate() - 4.0 / 7.0).abs() < 1e-10);
804        assert_eq!(code.redundancy(), 3);
805        assert_eq!(code.corrects_errors(), 1);
806        assert_eq!(code.detects_errors(), 2);
807    }
808    #[test]
809    fn test_singleton_bound_mds() {
810        let mds = LinearCode::new(7, 4, 4);
811        assert!(mds.meets_singleton_bound());
812        let not_mds = LinearCode::new(7, 4, 3);
813        assert!(!not_mds.meets_singleton_bound());
814    }
815    #[test]
816    fn test_hamming_code_parameters() {
817        let ham = HammingCode::new(3);
818        let lc = ham.to_linear_code();
819        assert_eq!(lc.n, 7);
820        assert_eq!(lc.k, 4);
821        assert_eq!(lc.d_min, 3);
822        assert_eq!(lc.corrects_errors(), 1);
823    }
824    #[test]
825    fn test_hamming_code_is_perfect() {
826        let ham = HammingCode::new(3);
827        let lc = ham.to_linear_code();
828        assert!(lc.meets_hamming_bound());
829    }
830    #[test]
831    fn test_hamming_74_encode_is_codeword() {
832        let ham = HammingCode74::new();
833        let msg = BinaryVector::from_bits(vec![true, false, true, true]);
834        let cw = ham.encode(&msg);
835        assert_eq!(cw.bits.len(), 7);
836        assert!(ham.inner.is_codeword(&cw));
837    }
838    #[test]
839    fn test_hamming_74_single_error_correction() {
840        let ham = HammingCode74::new();
841        let msg = BinaryVector::from_bits(vec![true, false, true, false]);
842        let cw = ham.encode(&msg);
843        let mut received = cw.clone();
844        received.bits[2] ^= true;
845        let corrected = ham.correct(&received);
846        assert_eq!(corrected.bits, cw.bits);
847    }
848    #[test]
849    fn test_linear_code_matrix_encode_syndrome() {
850        let ham = HammingCode74::new();
851        let msg = BinaryVector::from_bits(vec![false, true, false, true]);
852        let cw = ham.encode(&msg);
853        let syn = ham.syndrome(&cw);
854        assert_eq!(syn.hamming_weight(), 0);
855    }
856    #[test]
857    fn test_reed_solomon_encode() {
858        let rs = ReedSolomonCode::new(7, 3, 11);
859        let cw = rs.encode(&[1, 2, 3]);
860        assert_eq!(cw.len(), 7);
861        assert!(cw.iter().all(|&v| v < 11));
862        assert_eq!(rs.min_distance(), 5);
863        assert_eq!(rs.error_correction_capability(), 2);
864    }
865    #[test]
866    fn test_reed_solomon_zero_message() {
867        let rs = ReedSolomonCode::new(5, 3, 7);
868        let cw = rs.encode(&[0, 0, 0]);
869        assert!(cw.iter().all(|&v| v == 0));
870    }
871    #[test]
872    fn test_convolutional_encoder_basic() {
873        let mut enc = ConvolutionalEncoder::new(1, 2, 3, vec![0b111, 0b101]);
874        enc.reset();
875        let out = enc.encode_bit(true);
876        assert_eq!(out.len(), 2);
877        assert_eq!(out, vec![true, true]);
878    }
879    #[test]
880    fn test_convolutional_encoder_flush() {
881        let mut enc = ConvolutionalEncoder::new(1, 2, 3, vec![0b111, 0b101]);
882        enc.reset();
883        let _ = enc.encode(&[true, false, true]);
884        let tail = enc.flush();
885        assert_eq!(tail.len(), 4);
886    }
887    #[test]
888    fn test_channel_capacity_bsc() {
889        assert!((ChannelCapacity::bsc_capacity(0.0) - 1.0).abs() < 1e-10);
890        assert!(ChannelCapacity::bsc_capacity(0.5).abs() < 1e-10);
891        assert!((ChannelCapacity::bsc_capacity(1.0) - 1.0).abs() < 1e-10);
892    }
893    #[test]
894    fn test_channel_capacity_bec_awgn() {
895        assert!((ChannelCapacity::bec_capacity(0.5) - 0.5).abs() < 1e-10);
896        assert!(ChannelCapacity::awgn_capacity(0.0).abs() < 1e-10);
897        assert!((ChannelCapacity::awgn_capacity(1.0) - 0.5).abs() < 1e-10);
898    }
899    #[test]
900    fn test_q_ary_entropy() {
901        assert!(ChannelCapacity::q_ary_entropy(0.0, 4).abs() < 1e-10);
902        assert!(ChannelCapacity::q_ary_entropy(1.0, 4).abs() < 1e-10);
903        let p = 0.3;
904        let bh = ChannelCapacity::binary_entropy(p);
905        let qh = ChannelCapacity::q_ary_entropy(p, 2);
906        assert!((bh - qh).abs() < 1e-8, "bh={bh} qh={qh}");
907    }
908    #[test]
909    fn test_gf2m_arithmetic() {
910        let gf = GF2m::new(3, 11);
911        assert_eq!(gf.size, 8);
912        assert_eq!(gf.pow(0), 1);
913        assert_eq!(gf.pow(1), 2);
914        assert_eq!(gf.pow(2), 4);
915        assert_eq!(gf.pow(7), gf.pow(0));
916        assert_eq!(gf.mul(1, 1), 1);
917        assert_eq!(gf.add(3, 5), 6);
918        assert_eq!(gf.mul(gf.inv(2), 2), 1);
919    }
920    #[test]
921    fn test_burst_error_detector() {
922        let det = BurstErrorDetector::new(7, 2, vec![true, true, true]);
923        let zero_cw = BinaryVector::new(7);
924        assert!(det.is_valid(&zero_cw));
925        let mut errored = BinaryVector::new(7);
926        errored.bits[3] = true;
927        let syn = det.compute_syndrome(&errored);
928        assert_ne!(syn.hamming_weight(), 0);
929    }
930    #[test]
931    fn test_build_coding_theory_env() {
932        let mut env = Environment::new();
933        build_coding_theory_env(&mut env);
934        assert!(env.get(&Name::str("LinearCode")).is_some());
935        assert!(env.get(&Name::str("shannon_channel_coding")).is_some());
936        assert!(env.get(&Name::str("hamming_perfect")).is_some());
937        assert!(env.get(&Name::str("reed_solomon_mds")).is_some());
938        assert!(env.get(&Name::str("BCHCode")).is_some());
939        assert!(env.get(&Name::str("PolarCode")).is_some());
940        assert!(env.get(&Name::str("TurboCode")).is_some());
941        assert!(env.get(&Name::str("LDPCCode")).is_some());
942        assert!(env.get(&Name::str("StabilizerCode")).is_some());
943        assert!(env.get(&Name::str("CSSCode")).is_some());
944        assert!(env.get(&Name::str("ToricCode")).is_some());
945        assert!(env.get(&Name::str("EliasBassalygo")).is_some());
946        assert!(env.get(&Name::str("MRRWBound")).is_some());
947        assert!(env.get(&Name::str("GilbertVarshamov")).is_some());
948        assert!(env.get(&Name::str("GuruswamiSudanDecoding")).is_some());
949        assert!(env.get(&Name::str("RegeneratingCode")).is_some());
950        assert!(env.get(&Name::str("LocallyDecodableCode")).is_some());
951        assert!(env.get(&Name::str("AlamoutiScheme")).is_some());
952        assert!(env.get(&Name::str("TrellisCodedModulation")).is_some());
953        assert!(env.get(&Name::str("SurfaceCode")).is_some());
954        assert!(env.get(&Name::str("ColorCode")).is_some());
955        assert!(env.get(&Name::str("QuantumLDPCCode")).is_some());
956        assert!(env.get(&Name::str("ReedMullerCode")).is_some());
957        assert!(env.get(&Name::str("CompressedSensingMatrix")).is_some());
958        assert!(env.get(&Name::str("RestrictedIsometryProperty")).is_some());
959        assert!(env.get(&Name::str("MIMOCapacity")).is_some());
960        assert!(env.get(&Name::str("ProductCode")).is_some());
961        assert!(env.get(&Name::str("WeightEnumerator")).is_some());
962        assert!(env.get(&Name::str("BlahutArimoto")).is_some());
963        assert!(env.get(&Name::str("RateDistortionFunction")).is_some());
964        assert!(env.get(&Name::str("ChannelCapacityConverse")).is_some());
965    }
966    #[test]
967    fn test_reed_muller_code_parameters() {
968        let rm = ReedMullerCode::new(1, 3);
969        assert_eq!(rm.block_length(), 8);
970        assert_eq!(rm.min_distance(), 4);
971        assert_eq!(rm.dimension(), 4);
972        assert!(rm.is_first_order());
973        assert_eq!(rm.error_correction_capability(), 1);
974        let rm2 = ReedMullerCode::new(2, 4);
975        assert_eq!(rm2.block_length(), 16);
976        assert_eq!(rm2.min_distance(), 4);
977        assert_eq!(rm2.dimension(), 11);
978        assert!(!rm2.is_first_order());
979    }
980    #[test]
981    fn test_product_code_parameters() {
982        let c1 = LinearCode::new(7, 4, 3);
983        let c2 = LinearCode::new(5, 3, 3);
984        let pc = ProductCode::new(c1, c2);
985        assert_eq!(pc.block_length(), 35);
986        assert_eq!(pc.dimension(), 12);
987        assert_eq!(pc.min_distance(), 9);
988        let rate = pc.rate();
989        assert!((rate - 12.0 / 35.0).abs() < 1e-10);
990    }
991    #[test]
992    fn test_polar_code_bec_construction() {
993        let polar = PolarCodeBEC::new(4, 8, 0.5);
994        assert_eq!(polar.block_length(), 16);
995        assert_eq!(polar.dimension(), 8);
996        let rate = polar.rate();
997        assert!((rate - 0.5).abs() < 1e-10);
998        for &z in &polar.erasure_probs {
999            assert!(z >= 0.0 && z <= 1.0 + 1e-12);
1000        }
1001        let frac = polar.fraction_good(0.01);
1002        assert!(frac >= 0.0 && frac <= 1.0);
1003    }
1004    #[test]
1005    fn test_cs_measurement_matrix() {
1006        let data = vec![1.0, 0.0, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0, 1.0];
1007        let phi = CSMeasurementMatrix::from_data(3, 3, data);
1008        assert!(phi.mutual_coherence() < 1e-10);
1009        let y = phi.apply(&[1.0, 2.0, 3.0]);
1010        assert!((y[0] - 1.0).abs() < 1e-10);
1011        assert!((y[1] - 2.0).abs() < 1e-10);
1012        assert!((y[2] - 3.0).abs() < 1e-10);
1013    }
1014    #[test]
1015    fn test_bicm_capacity_bpsk() {
1016        let bpsk = BICMCapacityEstimator::new(2);
1017        assert_eq!(bpsk.bits_per_symbol, 1);
1018        assert_eq!(bpsk.spectral_efficiency_upper_bound(), 1.0);
1019        let cap = bpsk.approximate_capacity_db(30.0);
1020        assert!(cap > 0.99 && cap <= 1.0);
1021        let cap_low = bpsk.approximate_capacity_db(-10.0);
1022        assert!(cap_low >= 0.0 && cap_low < 0.5);
1023    }
1024    #[test]
1025    fn test_bicm_capacity_qam() {
1026        let qam16 = BICMCapacityEstimator::new(16);
1027        assert_eq!(qam16.bits_per_symbol, 4);
1028        assert_eq!(qam16.spectral_efficiency_upper_bound(), 4.0);
1029        let cap = qam16.approximate_capacity_db(20.0);
1030        assert!(cap > 0.0 && cap <= 4.0);
1031    }
1032}
1033#[allow(dead_code)]
1034pub fn binomial(n: usize, k: usize) -> usize {
1035    if k > n {
1036        return 0;
1037    }
1038    let mut result = 1usize;
1039    for i in 0..k.min(n - k) {
1040        result = result.saturating_mul(n - i);
1041        result /= i + 1;
1042    }
1043    result
1044}
1045#[cfg(test)]
1046mod tests_coding_extra {
1047    use super::*;
1048    #[test]
1049    fn test_reed_solomon() {
1050        let rs = ReedSolomonCode::new(7, 4, 8);
1051        assert_eq!(rs.distance(), 4);
1052        assert!(rs.is_mds());
1053        assert_eq!(rs.error_correction_capacity(), 1);
1054        assert_eq!(rs.erasure_correction_capacity(), 3);
1055        assert!((rs.rate() - 4.0 / 7.0).abs() < 1e-9);
1056    }
1057    #[test]
1058    fn test_turbo_code() {
1059        let tc = TurboCode::standard_3gpp(1024);
1060        assert!(tc.overall_rate() > 0.0 && tc.overall_rate() < 1.0);
1061    }
1062    #[test]
1063    fn test_polar_code() {
1064        let pc = PolarCode::new(1024, 512);
1065        assert!((pc.rate() - 0.5).abs() < 1e-9);
1066        assert!(pc.is_capacity_achieving());
1067        assert!(pc.successive_cancellation_complexity() > 0);
1068    }
1069    #[test]
1070    fn test_fountain_code() {
1071        let lt = FountainCode::lt_code(1000);
1072        assert!(lt.is_rateless());
1073        let needed = lt.n_symbols_to_decode();
1074        assert!(needed > 1000);
1075        let raptor = FountainCode::raptor_code(1000);
1076        assert!(raptor.decoding_complexity() < lt.decoding_complexity());
1077    }
1078    #[test]
1079    fn test_linear_code() {
1080        let hamming = LinearCode::new(7, 4, 3);
1081        assert!(hamming.satisfies_singleton_bound());
1082        assert!(hamming.satisfies_hamming_bound());
1083        assert!(hamming.is_perfect());
1084    }
1085}