1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pdec.src; edit the .src 2 import Base 3 import ./sel.bend as SL 4 import ../../../spec/crypto/secp256k1/field.bend as FS 5 import ../../../spec/crypto/secp256k1/curve.bend as CV 6 import ../../../src/crypto/secp256k1/field.bend as F 7 import ../../../src/crypto/secp256k1/bytes.bend as B 8 import ../../../src/crypto/secp256k1/point.bend as P 9 import ./fwrap.bend as FW 10 import ./bytes.bend as BY 11 import ./point.bend as PT 12 import ./penc.bend as PE 13 import ./blist.bend as BL 14 15 # SEC 1 decoding of src/crypto/secp256k1/point.bend (decode: compressed 16 # and uncompressed public keys) against spec/crypto/secp256k1/curve.bend, 17 # and the decoded points are reduced. 18 19 # ---- byte lists ---- 20 21 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>}: 22 match a b: 23 case True{} True{}: 24 PE.decompress_v(one, h1, x, U32.to_nat(U32.and(pre, 1)), SL.red_of(one, x, hl, hb), BL.par01(pre)) 25 case True{} False{}: 26 {==} 27 case False{} _: 28 {==} 29 30 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}: 31 match a b: 32 case True{} True{}: 33 PE.decompress_r(one, h1, x, U32.to_nat(U32.and(pre, 1)), SL.red_of(one, x, hl, hb), BL.par01(pre)) 34 case True{} False{}: 35 {==} 36 case False{} _: 37 {==} 38 39 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>}: 40 %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>} 41 %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>} 42 %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>} 43 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)), {==}) 44 45 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}: 46 %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} 47 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)), {==}) 48 49 # ---- uncompressed ---- 50 51 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>}: 52 match ok: 53 case True{}: 54 %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>} 55 {==} 56 case False{}: 57 {==} 58 59 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>}: 60 match a bx by: 61 case True{} True{} True{}: 62 %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>} 63 duv(one, h1, x, y, CV.on_curve(FS.prime(one), FS.value(one, x), FS.value(one, y))) 64 case True{} True{} False{}: 65 {==} 66 case True{} False{} _: 67 {==} 68 case False{} _ _: 69 {==} 70 71 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}: 72 match ok: 73 case True{}: 74 PT.pr3(one, x, y, F.one(), hx, hy, PE.one_r(one, h1)) 75 case False{}: 76 {==} 77 78 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}: 79 match a bx by: 80 case True{} True{} True{}: 81 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)) 82 case True{} True{} False{}: 83 {==} 84 case True{} False{} _: 85 {==} 86 case False{} _ _: 87 {==} 88 89 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>}: 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)), {==}, {==}) 107 108 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}: 109 +hlx = BY.of_be_limbs(one, h1, B.prefix(32n, rest), BL.pl32(rest, hl)) 110 +hly = BY.of_be_limbs(one, h1, B.suffix(32n, rest), BL.sl32(rest, hl)) 111 %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} 112 %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} 113 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)), {==}, {==}) 114 115 # ---- decode ---- 116 117 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>}: 118 match c33 c65: 119 case True{} _: 120 %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>} 121 %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>} 122 d33(one, h1, CV.head(bs), CV.after(1n, bs), BL.len_tail(32n, bs, h33)) 123 case False{} True{}: 124 %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>} 125 %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>} 126 %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>} 127 d65(one, h1, CV.head(bs), CV.after(1n, bs), BL.len_tail(64n, bs, h65)) 128 case False{} False{}: 129 {==} 130 131 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}: 132 match c33 c65: 133 case True{} _: 134 %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} 135 d33r(one, h1, B.head(bs), CV.after(1n, bs), BL.len_tail(32n, bs, h33)) 136 case False{} True{}: 137 %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} 138 d65r(one, h1, B.head(bs), CV.after(1n, bs), BL.len_tail(64n, bs, h65)) 139 case False{} False{}: 140 {==} 141 142 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>}: 143 %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>} 144 %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>} 145 dl(one, h1, bs, CV.length_is(33n, bs), CV.length_is(65n, bs), BL.hl_is(33n, bs), BL.hl_is(65n, bs)) 146 147 def decode_r(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>) -> {PE.mpred(one, P.decode(bs)) == True{} : Bool}: 148 dlr(one, h1, bs, B.has_len(33n, bs), B.has_len(65n, bs), {==}, {==})