13.2. Encoding and Recovery🔗

def

Jar.Erasure.erasureCode [Jar.JamConfig] (_k : Nat) (data : ByteArray) :
  Array ByteArray
Jar.Erasure.erasureCode [Jar.JamConfig]
  (_k : Nat) (data : ByteArray) :
  Array ByteArray

C_k(data) : Erasure-code a blob into V chunks. GP Appendix H eq (H.4). Input: data blob. Output: V chunks of 2k octets each. The first dataShards chunks are the original data (systematic). The remaining recoveryShards chunks are RS parity.

def

Jar.Erasure.erasureRecover [Jar.JamConfig] (_k : Nat)
  (chunks : Array (ByteArray × Nat)) : Option ByteArray
Jar.Erasure.erasureRecover [Jar.JamConfig]
  (_k : Nat)
  (chunks : Array (ByteArray × Nat)) :
  Option ByteArray

R_k(chunks) : Recover original data from any dataShards chunks. GP Appendix H eq (H.5). Input: at least dataShards (chunk, index) pairs. Output: reconstructed data of original length. (Not yet implemented — recovery requires IFFT-based decoding.)