JAR: Join-Accumulate Refine

18.3. Encoding and Recovery🔗

🔗def
Jar.Erasure.nextPowerOfTwo (n : Nat) : Nat
Jar.Erasure.nextPowerOfTwo (n : Nat) : Nat

Next power of 2 that is >= n.

🔗def
Jar.Erasure.nextMultipleOf (n m : Nat) : Nat
Jar.Erasure.nextMultipleOf (n m : Nat) :
  Nat

Round n up to the nearest multiple of m.

🔗def
Jar.Erasure.encodeRS (originalCount recoveryCount : Nat)
  (dataSymbols : Array UInt16) : Array UInt16
Jar.Erasure.encodeRS
  (originalCount recoveryCount : Nat)
  (dataSymbols : Array UInt16) :
  Array UInt16

Encode originalCount data GF(2^16) symbols into recoveryCount parity symbols using the Leopard-RS additive FFT approach. Returns an array of recoveryCount parity GF elements.

🔗def
Jar.Erasure.dataShards [Jar.JarConfig] : Nat
Jar.Erasure.dataShards [Jar.JarConfig] :
  Nat

Number of data shards: 3 * W_E / W_P. For full config (W_P=6): 3 * 684 / 6 = 342. For tiny config (W_P=1026): 3 * 684 / 1026 = 2.

🔗def
Jar.Erasure.recoveryShards [Jar.JarConfig] : Nat
Jar.Erasure.recoveryShards
  [Jar.JarConfig] : Nat

Number of recovery shards: V - dataShards.

🔗def
Jar.Erasure.pieceSize [Jar.JarConfig] : Nat
Jar.Erasure.pieceSize [Jar.JarConfig] :
  Nat

Piece size in bytes: dataShards * 2.

🔗def
Jar.Erasure.erasureCode [Jar.JarConfig] (_k : Nat) (data : ByteArray) :
  Array ByteArray
Jar.Erasure.erasureCode [Jar.JarConfig]
  (_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.JarConfig] (_k : Nat)
  (chunks : Array (ByteArray × Nat)) : Option ByteArray
Jar.Erasure.erasureRecover [Jar.JarConfig]
  (_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.)