def rid

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:186

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E

186def rid(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}, id: Nat, +hid: {Nat.is_lt(id, 4n) == True{} : Bool}) -> {E.recover_ok(z, r, s, id, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), id, True{}) : Maybe<&2, List<&2, U32>>}:
187  match id:
188    case 0n:
189      rc0(one, h1, z, hz, r, hr, s, hs)
190    case 1n:
191      rc1(one, h1, z, hz, r, hr, s, hs)
192    case 2n:
193      rc2(one, h1, z, hz, r, hr, s, hs)
194    case 3n:
195      rc3(one, h1, z, hz, r, hr, s, hs)
196    case 4n+ +c:
197      Empty.absurd({E.recover_ok(z, r, s, 4n+c, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 4n+c, True{}) : Maybe<&2, List<&2, U32>>}, not4(c, hid))