proofs/crypto/secp256k1/pdec.bend source
proofs/crypto/secp256k1/pdec.bend on the hub · documented module
# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pdec.src; edit the .srcimport Baseimport ./sel.bend as SLimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../spec/crypto/secp256k1/curve.bend as CVimport ../../../src/crypto/secp256k1/field.bend as Fimport ../../../src/crypto/secp256k1/bytes.bend as Bimport ../../../src/crypto/secp256k1/point.bend as Pimport ./fwrap.bend as FWimport ./bytes.bend as BYimport ./point.bend as PTimport ./penc.bend as PEimport ./blist.bend as BL# SEC 1 decoding of src/crypto/secp256k1/point.bend (decode: compressed# and uncompressed public keys) against spec/crypto/secp256k1/curve.bend,# and the decoded points are reduced.# ---- byte lists ----def dc(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, a: Bool, b: Bool, +hb: {Nat.is_lt(FS.value(one, x), FS.prime(one)) == b : Bool}) -> {PE.mpv(one, P.decode_c(x, U32.to_nat(U32.and(pre, 1)), Bool.and(a, b))) == CV.decode_c_if(FS.prime(one), pre, FS.value(one, x), Bool.and(a, b)) : Maybe<&2, CV.SPoint>}: match a b: case True{} True{}: PE.decompress_v(one, h1, x, U32.to_nat(U32.and(pre, 1)), SL.red_of(one, x, hl, hb), BL.par01(pre)) case True{} False{}: {==} case False{} _: {==}def dcr(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +x: List<&2, Nat>, +hl: {FS.limbs16(one, 16n, x) == True{} : Bool}, a: Bool, b: Bool, +hb: {Nat.is_lt(FS.value(one, x), FS.prime(one)) == b : Bool}) -> {PE.mpred(one, P.decode_c(x, U32.to_nat(U32.and(pre, 1)), Bool.and(a, b))) == True{} : Bool}: match a b: case True{} True{}: PE.decompress_r(one, h1, x, U32.to_nat(U32.and(pre, 1)), SL.red_of(one, x, hl, hb), BL.par01(pre)) case True{} False{}: {==} case False{} _: {==}def d33(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +rest: List<&2, U32>, +hl: {B.has_len(32n, rest) == True{} : Bool}) -> {PE.mpv(one, P.decode_33(pre, rest)) == CV.decode_c(FS.prime(one), pre, CV.os2ip(rest)) : Maybe<&2, CV.SPoint>}: %Equal.sym(Bool, F.lt_p(B.of_be(rest)), Nat.is_lt(FS.value(one, B.of_be(rest)), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(rest))) : {PE.mpv(one, P.decode_c(B.of_be(rest), U32.to_nat(U32.and(pre, 1)), Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), _))) == CV.decode_c_if(FS.prime(one), pre, CV.os2ip(rest), Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(CV.os2ip(rest), FS.prime(one)))) : Maybe<&2, CV.SPoint>} %Equal.sym(Nat, CV.os2ip(rest), FS.value(one, B.of_be(rest)), Equal.sym(Nat, FS.value(one, B.of_be(rest)), CV.os2ip(rest), BY.of_be_value(one, h1, rest))) : {PE.mpv(one, P.decode_c(B.of_be(rest), U32.to_nat(U32.and(pre, 1)), Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(FS.value(one, B.of_be(rest)), FS.prime(one))))) == CV.decode_c_if(FS.prime(one), pre, _, Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(CV.os2ip(rest), FS.prime(one)))) : Maybe<&2, CV.SPoint>} %Equal.sym(Nat, CV.os2ip(rest), FS.value(one, B.of_be(rest)), Equal.sym(Nat, FS.value(one, B.of_be(rest)), CV.os2ip(rest), BY.of_be_value(one, h1, rest))) : {PE.mpv(one, P.decode_c(B.of_be(rest), U32.to_nat(U32.and(pre, 1)), Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(FS.value(one, B.of_be(rest)), FS.prime(one))))) == CV.decode_c_if(FS.prime(one), pre, FS.value(one, B.of_be(rest)), Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(_, FS.prime(one)))) : Maybe<&2, CV.SPoint>} dc(one, h1, pre, B.of_be(rest), BY.of_be_limbs(one, h1, rest, hl), Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(FS.value(one, B.of_be(rest)), FS.prime(one)), {==})def d33r(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +rest: List<&2, U32>, +hl: {B.has_len(32n, rest) == True{} : Bool}) -> {PE.mpred(one, P.decode_33(pre, rest)) == True{} : Bool}: %Equal.sym(Bool, F.lt_p(B.of_be(rest)), Nat.is_lt(FS.value(one, B.of_be(rest)), FS.prime(one)), FW.lt_p_f(one, h1, B.of_be(rest))) : {PE.mpred(one, P.decode_c(B.of_be(rest), U32.to_nat(U32.and(pre, 1)), Bool.and(Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), _))) == True{} : Bool} dcr(one, h1, pre, B.of_be(rest), BY.of_be_limbs(one, h1, rest, hl), Bool.or(U32.is_eq(pre, 2), U32.is_eq(pre, 3)), Nat.is_lt(FS.value(one, B.of_be(rest)), FS.prime(one)), {==})# ---- uncompressed ----def duv(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, ok: Bool) -> {PE.mpv(one, P.decode_u(x, y, ok)) == CV.decompress_if(FS.value(one, x), FS.value(one, y), ok) : Maybe<&2, CV.SPoint>}: match ok: case True{}: %Equal.sym(Nat, FS.value(one, F.one()), 1n, PE.one_v(one, h1)) : {Some{CV.SPoint{FS.value(one, x), FS.value(one, y), _}} == Some{CV.SPoint{FS.value(one, x), FS.value(one, y), 1n}} : Maybe<&2, CV.SPoint>} {==} case False{}: {==}def du(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +hlx: {FS.limbs16(one, 16n, x) == True{} : Bool}, +hly: {FS.limbs16(one, 16n, y) == True{} : Bool}, a: Bool, bx: Bool, by: Bool, +hbx: {Nat.is_lt(FS.value(one, x), FS.prime(one)) == bx : Bool}, +hby: {Nat.is_lt(FS.value(one, y), FS.prime(one)) == by : Bool}) -> {PE.mpv(one, P.decode_u(x, y, Bool.and(Bool.and(a, Bool.and(bx, by)), P.on_curve(x, y)))) == CV.decompress_if(FS.value(one, x), FS.value(one, y), Bool.and(Bool.and(a, Bool.and(bx, by)), CV.on_curve(FS.prime(one), FS.value(one, x), FS.value(one, y)))) : Maybe<&2, CV.SPoint>}: match a bx by: case True{} True{} True{}: %Equal.sym(Bool, P.on_curve(x, y), CV.on_curve(FS.prime(one), FS.value(one, x), FS.value(one, y)), PE.on_curve_v(one, h1, x, y, SL.red_of(one, x, hlx, hbx), SL.red_of(one, y, hly, hby))) : {PE.mpv(one, P.decode_u(x, y, Bool.and(Bool.and(a, Bool.and(bx, by)), _))) == CV.decompress_if(FS.value(one, x), FS.value(one, y), Bool.and(Bool.and(a, Bool.and(bx, by)), CV.on_curve(FS.prime(one), FS.value(one, x), FS.value(one, y)))) : Maybe<&2, CV.SPoint>} duv(one, h1, x, y, CV.on_curve(FS.prime(one), FS.value(one, x), FS.value(one, y))) case True{} True{} False{}: {==} case True{} False{} _: {==} case False{} _ _: {==}def dur_ok(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +hx: {PT.red(one, x) == True{} : Bool}, +hy: {PT.red(one, y) == True{} : Bool}, ok: Bool) -> {PE.mpred(one, P.decode_u(x, y, ok)) == True{} : Bool}: match ok: case True{}: PT.pr3(one, x, y, F.one(), hx, hy, PE.one_r(one, h1)) case False{}: {==}def dur(+one: Nat, +h1: {one == 1n : Nat}, +x: List<&2, Nat>, +y: List<&2, Nat>, +hlx: {FS.limbs16(one, 16n, x) == True{} : Bool}, +hly: {FS.limbs16(one, 16n, y) == True{} : Bool}, a: Bool, bx: Bool, by: Bool, +hbx: {Nat.is_lt(FS.value(one, x), FS.prime(one)) == bx : Bool}, +hby: {Nat.is_lt(FS.value(one, y), FS.prime(one)) == by : Bool}) -> {PE.mpred(one, P.decode_u(x, y, Bool.and(Bool.and(a, Bool.and(bx, by)), P.on_curve(x, y)))) == True{} : Bool}: match a bx by: case True{} True{} True{}: dur_ok(one, h1, x, y, SL.red_of(one, x, hlx, hbx), SL.red_of(one, y, hly, hby), P.on_curve(x, y)) case True{} True{} False{}: {==} case True{} False{} _: {==} case False{} _ _: {==}def 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>}: +hlx = BY.of_be_limbs(one, h1, B.prefix(32n, rest), BL.pl32(rest, hl)) +hly = BY.of_be_limbs(one, h1, B.suffix(32n, rest), BL.sl32(rest, hl)) %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} %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>} 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)), {==}, {==})def d65r(+one: Nat, +h1: {one == 1n : Nat}, +pre: U32, +rest: List<&2, U32>, +hl: {B.has_len(64n, rest) == True{} : Bool}) -> {PE.mpred(one, P.decode_65(pre, rest)) == True{} : Bool}: +hlx = BY.of_be_limbs(one, h1, B.prefix(32n, rest), BL.pl32(rest, hl)) +hly = BY.of_be_limbs(one, h1, B.suffix(32n, rest), BL.sl32(rest, hl)) %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.mpred(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)))))) == True{} : Bool} %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.mpred(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)))))) == True{} : Bool} dur(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)), {==}, {==})# ---- decode ----def dl(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, c33: Bool, c65: Bool, +h33: {B.has_len(33n, bs) == c33 : Bool}, +h65: {B.has_len(65n, bs) == c65 : Bool}) -> {PE.mpv(one, P.decode_len(bs, c33, c65)) == CV.decode_len(FS.prime(one), bs, c33, c65) : Maybe<&2, CV.SPoint>}: match c33 c65: case True{} _: %Equal.sym(U32, B.head(bs), CV.head(bs), BL.head_eq(bs)) : {PE.mpv(one, P.decode_33(_, B.tail(bs))) == CV.decode_c(FS.prime(one), CV.head(bs), CV.os2ip(CV.after(1n, bs))) : Maybe<&2, CV.SPoint>} %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {PE.mpv(one, P.decode_33(CV.head(bs), _)) == CV.decode_c(FS.prime(one), CV.head(bs), CV.os2ip(CV.after(1n, bs))) : Maybe<&2, CV.SPoint>} d33(one, h1, CV.head(bs), CV.after(1n, bs), BL.len_tail(32n, bs, h33)) case False{} True{}: %Equal.sym(U32, B.head(bs), CV.head(bs), BL.head_eq(bs)) : {PE.mpv(one, P.decode_65(_, B.tail(bs))) == CV.decode_u(FS.prime(one), CV.head(bs), CV.os2ip(CV.first(32n, CV.after(1n, bs))), CV.os2ip(CV.after(33n, bs))) : Maybe<&2, CV.SPoint>} %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {PE.mpv(one, P.decode_65(CV.head(bs), _)) == CV.decode_u(FS.prime(one), CV.head(bs), CV.os2ip(CV.first(32n, CV.after(1n, bs))), CV.os2ip(CV.after(33n, bs))) : Maybe<&2, CV.SPoint>} %Equal.sym(List<&2, U32>, CV.after(33n, bs), CV.after(32n, CV.after(1n, bs)), BL.after33(bs)) : {PE.mpv(one, P.decode_65(CV.head(bs), CV.after(1n, bs))) == CV.decode_u(FS.prime(one), CV.head(bs), CV.os2ip(CV.first(32n, CV.after(1n, bs))), CV.os2ip(_)) : Maybe<&2, CV.SPoint>} d65(one, h1, CV.head(bs), CV.after(1n, bs), BL.len_tail(64n, bs, h65)) case False{} False{}: {==}def dlr(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, c33: Bool, c65: Bool, +h33: {B.has_len(33n, bs) == c33 : Bool}, +h65: {B.has_len(65n, bs) == c65 : Bool}) -> {PE.mpred(one, P.decode_len(bs, c33, c65)) == True{} : Bool}: match c33 c65: case True{} _: %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {PE.mpred(one, P.decode_33(B.head(bs), _)) == True{} : Bool} d33r(one, h1, B.head(bs), CV.after(1n, bs), BL.len_tail(32n, bs, h33)) case False{} True{}: %Equal.sym(List<&2, U32>, B.tail(bs), CV.after(1n, bs), BL.tail_after(bs)) : {PE.mpred(one, P.decode_65(B.head(bs), _)) == True{} : Bool} d65r(one, h1, B.head(bs), CV.after(1n, bs), BL.len_tail(64n, bs, h65)) case False{} False{}: {==}def decode_v(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {PE.mpv(one, P.decode(bs)) == CV.decode(FS.prime(one), bs) : Maybe<&2, CV.SPoint>}: %Equal.sym(Bool, B.has_len(33n, bs), CV.length_is(33n, bs), BL.hl_is(33n, bs)) : {PE.mpv(one, P.decode_len(bs, _, B.has_len(65n, bs))) == CV.decode_len(FS.prime(one), bs, CV.length_is(33n, bs), CV.length_is(65n, bs)) : Maybe<&2, CV.SPoint>} %Equal.sym(Bool, B.has_len(65n, bs), CV.length_is(65n, bs), BL.hl_is(65n, bs)) : {PE.mpv(one, P.decode_len(bs, CV.length_is(33n, bs), _)) == CV.decode_len(FS.prime(one), bs, CV.length_is(33n, bs), CV.length_is(65n, bs)) : Maybe<&2, CV.SPoint>} dl(one, h1, bs, CV.length_is(33n, bs), CV.length_is(65n, bs), BL.hl_is(33n, bs), BL.hl_is(65n, bs))def decode_r(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {PE.mpred(one, P.decode(bs)) == True{} : Bool}: dlr(one, h1, bs, B.has_len(33n, bs), B.has_len(65n, bs), {==}, {==})