def d65
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/pdec.bend:89
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend as Pdec
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/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as FW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as PE
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as BL
89def d65(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {PE.mpv(one, P.decode_65(pre, rest)) == CV.decode_u(FS.prime(one), pre, CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))) : Maybe<&2, CV.SPoint>}:
90 +hlx = BY.of_be_limbs(one, h1, B.prefix(32n, rest), BL.pl32(rest, hl))
91 +hly = BY.of_be_limbs(one, h1, B.suffix(32n, rest), BL.sl32(rest, hl))
92 %Equal.sym(Bool, F.lt_p(B.of_be(B.prefix(32n, rest))), Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(_, F.lt_p(B.of_be(B.suffix(32n, rest))))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
93 %Equal.sym(Bool, F.lt_p(B.of_be(B.suffix(32n, rest))), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), _)), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
94 %Equal.sym(List<&2, U32>, CV.first(32n, rest), B.prefix(32n, rest), Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), BL.prefix_first(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(_), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(CV.first(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
95 %Equal.sym(List<&2, U32>, CV.first(32n, rest), B.prefix(32n, rest), Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), BL.prefix_first(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(_), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(CV.first(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
96 %Equal.sym(List<&2, U32>, CV.first(32n, rest), B.prefix(32n, rest), Equal.sym(List<&2, U32>, B.prefix(32n, rest), CV.first(32n, rest), BL.prefix_first(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(_), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
97 %Equal.sym(List<&2, U32>, CV.after(32n, rest), B.suffix(32n, rest), Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), BL.suffix_after(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(_), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(CV.after(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
98 %Equal.sym(List<&2, U32>, CV.after(32n, rest), B.suffix(32n, rest), Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), BL.suffix_after(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(_), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(CV.after(32n, rest))))) : Maybe<&2, CV.SPoint>}
99 %Equal.sym(List<&2, U32>, CV.after(32n, rest), B.suffix(32n, rest), Equal.sym(List<&2, U32>, B.suffix(32n, rest), CV.after(32n, rest), BL.suffix_after(32n, rest))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(_)))) : Maybe<&2, CV.SPoint>}
100 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, rest)), FS.value(one, B.of_be(B.prefix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.prefix(32n, rest)), BY.of_be_value(one, h1, B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(_, CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(CV.os2ip(B.prefix(32n, rest)), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
101 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, rest)), FS.value(one, B.of_be(B.prefix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.prefix(32n, rest)), BY.of_be_value(one, h1, B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(_, FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), CV.os2ip(B.prefix(32n, rest)), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
102 %Equal.sym(Nat, CV.os2ip(B.prefix(32n, rest)), FS.value(one, B.of_be(B.prefix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.prefix(32n, rest)), BY.of_be_value(one, h1, B.prefix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), _, CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
103 %Equal.sym(Nat, CV.os2ip(B.suffix(32n, rest)), FS.value(one, B.of_be(B.suffix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), BY.of_be_value(one, h1, B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), _, Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(CV.os2ip(B.suffix(32n, rest)), FS.prime(one)))), CV.on_curve(FS.prime(one), FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
104 %Equal.sym(Nat, CV.os2ip(B.suffix(32n, rest)), FS.value(one, B.of_be(B.suffix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), BY.of_be_value(one, h1, B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.value(one, B.of_be(B.suffix(32n, rest))), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(_, FS.prime(one)))), CV.on_curve(FS.prime(one), FS.value(one, B.of_be(B.prefix(32n, rest))), CV.os2ip(B.suffix(32n, rest))))) : Maybe<&2, CV.SPoint>}
105 %Equal.sym(Nat, CV.os2ip(B.suffix(32n, rest)), FS.value(one, B.of_be(B.suffix(32n, rest))), Equal.sym(Nat, FS.value(one, B.of_be(B.suffix(32n, rest))), CV.os2ip(B.suffix(32n, rest)), BY.of_be_value(one, h1, B.suffix(32n, rest)))) : {PE.mpv(one, P.decode_u(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), P.on_curve(B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)))))) == CV.decompress_if(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.value(one, B.of_be(B.suffix(32n, rest))), Bool.and(Bool.and(U32.is_eq(pre, 4), Bool.and(Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)))), CV.on_curve(FS.prime(one), FS.value(one, B.of_be(B.prefix(32n, rest))), _))) : Maybe<&2, CV.SPoint>}
106 du(one, h1, B.of_be(B.prefix(32n, rest)), B.of_be(B.suffix(32n, rest)), hlx, hly, U32.is_eq(pre, 4), Nat.is_lt(FS.value(one, B.of_be(B.prefix(32n, rest))), FS.prime(one)), Nat.is_lt(FS.value(one, B.of_be(B.suffix(32n, rest))), FS.prime(one)), {==}, {==})