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