decodePoint ∘ encodePoint = some

Ed25519's 32-byte point compression (y in the low 255 bits, the parity of x in the top bit) round-trips on every curve point. Decoding recovers x from y by the p ≡ 5 (mod 8) square-root recipe of RFC 8032, x₀ = xx^((p+3)/8) corrected by √-1, then fixes the sign by parity; sqrt_step shows the recipe always lands on ±x, and parity_fix that the parity rule picks x.

theorem Cryptlib.Primitives.Sign.Ed25519Codec.ofDigits_range (k n : ℕ) : Nat.ofDigits 256 (List.map (fun (i : ℕ) => n >>> (8 * i) % 256) (List.range k)) = n % 256 ^ k

theorem Cryptlib.Primitives.Sign.Ed25519Codec.bytesToNat_natToBytes (n : ℕ) (h : n < 256 ^ 32) : Ed25519Math.bytesToNat (Ed25519Math.natToBytes 32 n) = n

theorem Cryptlib.Primitives.Sign.Ed25519Codec.powAux_eq (b : Ed25519Facts.F) (e : ℕ) : Ed25519Math.powAux b e = b ^ e

theorem Cryptlib.Primitives.Sign.Ed25519Codec.sqrtMinusOne_eq : Ed25519Math.sqrtMinusOne = Ed25519Facts.i

theorem Cryptlib.Primitives.Sign.Ed25519Codec.sqrtMinusOne_sq : Ed25519Math.sqrtMinusOne ^ 2 = -1

theorem Cryptlib.Primitives.Sign.Ed25519Codec.sqrt_step {x y : Ed25519Facts.F} (hq : -x ^ 2 + y ^ 2 = 1 + Ed25519Facts.d * x ^ 2 * y ^ 2) : (if Ed25519Math.powAux ((y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1)) ((NIKE.X25519Common.p + 3) / 8) ^ 2 = (y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1) then Ed25519Math.powAux ((y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1)) ((NIKE.X25519Common.p + 3) / 8) else Ed25519Math.powAux ((y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1)) ((NIKE.X25519Common.p + 3) / 8) * Ed25519Math.sqrtMinusOne) = x ∨ (if Ed25519Math.powAux ((y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1)) ((NIKE.X25519Common.p + 3) / 8) ^ 2 = (y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1) then Ed25519Math.powAux ((y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1)) ((NIKE.X25519Common.p + 3) / 8) else Ed25519Math.powAux ((y ^ 2 - 1) / (Ed25519Facts.d * y ^ 2 + 1)) ((NIKE.X25519Common.p + 3) / 8) * Ed25519Math.sqrtMinusOne) = -x

theorem Cryptlib.Primitives.Sign.Ed25519Codec.ofFn_range (k : ℕ) (g : ℕ → ℕ) : (List.ofFn fun (i : Fin k) => g ↑i) = List.map g (List.range k)

theorem Cryptlib.Primitives.Sign.Ed25519Codec.bytesToNat_ofFn (k n : ℕ) : Ed25519Math.bytesToNat (Vector.ofFn fun (i : Fin k) => (n >>> (8 * ↑i)).toUInt8).toList = n % 256 ^ k

theorem Cryptlib.Primitives.Sign.Ed25519Codec.val_lt_pow {z : Ed25519Facts.F} : ZMod.val z < 2 ^ 255

theorem Cryptlib.Primitives.Sign.Ed25519Codec.raw_encode (q : Ed25519Math.Point) : Ed25519Math.bytesToNat (Ed25519Math.encodePoint q).toList = ZMod.val q.y + 2 ^ 255 * (ZMod.val q.x % 2)

theorem Cryptlib.Primitives.Sign.Ed25519Codec.parity_fix {x xc : Ed25519Facts.F} (h : xc = x ∨ xc = -x) : (if ZMod.val xc % 2 = ZMod.val x % 2 then xc else -xc) = x

theorem Cryptlib.Primitives.Sign.Ed25519Codec.decode_encode (q : Ed25519Math.Point) (hq : Ed25519Math.onCurve q) : Ed25519Math.decodePoint (Ed25519Math.encodePoint q) = some q