~/bend-docscommunity

proofs/crypto/secp256k1/pdec.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend as Pdec

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pdec.src; edit the .src

12 imports
import Base
import ./sel.bend as SL
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/point.bend as P
import ./fwrap.bend as FW
import ./bytes.bend as BY
import ./point.bend as PT
import ./penc.bend as PE
import ./blist.bend as BL

Definitions

def dc source · line 21 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pre:U32 -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @a:Bool -> @b:Bool -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_c(x, U32.to_nat(U32.and(pre, 1)), Bool.and(a, b))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decode_c_if(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), pre, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), Bool.and(a, b)) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def dcr source · line 30 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pre:U32 -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @a:Bool -> @b:Bool -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_c(x, U32.to_nat(U32.and(pre, 1)), Bool.and(a, b))) == True{} : Bool}

def d33 source · line 39 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pre:U32 -> @+rest:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, rest) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_33(pre, rest)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decode_c(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), pre, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(rest)) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def d33r source · line 45 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pre:U32 -> @+rest:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, rest) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_33(pre, rest)) == True{} : Bool}

def duv source · line 51 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @ok:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_u(x, y, ok)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decompress_if(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), ok) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def du source · line 59 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+hlx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @+hly:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, y) == True{} : Bool} -> @a:Bool -> @bx:Bool -> @by:Bool -> @+hbx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == bx : Bool} -> @+hby:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == by : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_u(x, y, Bool.and(Bool.and(a, Bool.and(bx, by)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.on_curve(x, y)))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decompress_if(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), Bool.and(Bool.and(a, Bool.and(bx, by)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.on_curve(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y)))) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def dur_ok source · line 71 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> @ok:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_u(x, y, ok)) == True{} : Bool}

def dur source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+hlx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @+hly:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, y) == True{} : Bool} -> @a:Bool -> @bx:Bool -> @by:Bool -> @+hbx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == bx : Bool} -> @+hby:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == by : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_u(x, y, Bool.and(Bool.and(a, Bool.and(bx, by)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.on_curve(x, y)))) == True{} : Bool}

def d65 source · line 89 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pre:U32 -> @+rest:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(64n, rest) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_65(pre, rest)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decode_u(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), pre, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.first(32n, rest)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(32n, rest))) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def d65r source · line 108 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pre:U32 -> @+rest:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(64n, rest) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_65(pre, rest)) == True{} : Bool}

def dl source · line 117 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @c33:Bool -> @c65:Bool -> @+h33:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(33n, bs) == c33 : Bool} -> @+h65:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(65n, bs) == c65 : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_len(bs, c33, c65)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decode_len(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), bs, c33, c65) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def dlr source · line 131 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @c33:Bool -> @c65:Bool -> @+h33:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(33n, bs) == c33 : Bool} -> @+h65:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(65n, bs) == c65 : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode_len(bs, c33, c65)) == True{} : Bool}

def decode_v source · line 142 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode(bs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decode(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), bs) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def decode_r source · line 147 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decode(bs)) == True{} : Bool}