proofs/crypto/secp256k1/blist.bend checks

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

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

8 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../lib/logic.bend as Lg
import ../../math/typed/width.bend as WW
import ./u32and.bend as FB
import ./bytes.bend as BY

Definitions

def head_eq source · line 15 · raw

@bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.head(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.head(bs) : U32}

def tail_after source · line 22 · raw

@bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.tail(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(1n, bs) : List<&2, U32>}

def suffix_after source · line 29 · raw

@n:Nat -> @bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.suffix(n, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(n, bs) : List<&2, U32>}

def prefix_first source · line 38 · raw

@n:Nat -> @bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.prefix(n, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.first(n, bs) : List<&2, U32>}

def after33 source · line 47 · raw

@bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(33n, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(1n, bs)) : List<&2, U32>}

def len_tail source · line 54 · raw

@+n:Nat -> @bs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(1n+n, bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(1n, bs)) == True{} : Bool}

def pre_len source · line 61 · raw

@a:Nat -> @+b:Nat -> @xs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(Nat.add(a, b), xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.first(a, xs)) == True{} : Bool}

def suf_len source · line 70 · raw

@a:Nat -> @+b:Nat -> @xs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(Nat.add(a, b), xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.after(a, xs)) == True{} : Bool}

def hl_is source · line 79 · raw

@+n:Nat -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(n, bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.length_is(n, bs) : Bool}

def par01 source · line 83 · raw

@+pre:U32 -> {Nat.is_lt(U32.to_nat(U32.and(pre, 1)), 2n) == True{} : Bool}

the parity bit of the prefix byte

def pl32 source · line 87 · raw

@+rest:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(64n, rest) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.prefix(32n, rest)) == True{} : Bool}

def sl32 source · line 91 · raw

@+rest:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(64n, rest) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.suffix(32n, rest)) == True{} : Bool}