def secp256k1n : ℕ

Equations

• secp256k1n = 115792089237316195423570985008687907852837564279074904382605163141518161494337

def blobECDSARECOVER (e v r s : String) : String

Equations

• blobECDSARECOVER e v r s = (totallySafePerformIO ∘ IO.Process.run) (blobECDSARECOVER.pythonCommandOfInput e v r s)

def blobECDSARECOVER.pythonCommandOfInput (e v r s : String) : IO.Process.SpawnArgs

Equations

• One or more equations did not get rendered due to their size.

def blobSign (e pᵣ : String) : List String

Equations

• blobSign e pᵣ = ((fun (x : String) => x.split Char.isWhitespace) ∘ totallySafePerformIO ∘ IO.Process.run) (blobSign.pythonCommandOfInput e pᵣ)

def blobSign.pythonCommandOfInput (e pᵣ : String) : IO.Process.SpawnArgs

Equations

• One or more equations did not get rendered due to their size.

def ECDSASIGN (e pᵣ : ByteArray) : Except String (ByteArray × ByteArray × ByteArray)

Equations

• One or more equations did not get rendered due to their size.

def ECDSARECOVER (e v r s : ByteArray) : Except String ByteArray

Equations

• ECDSARECOVER e v r s = match blobECDSARECOVER (toHex e) (toHex v) (toHex r) (toHex s) with | "error" => Except.error "ECDSARECOVER failed" | s => ByteArray.ofBlob (padLeft 128 s)