~/bend-docscommunity

proofs/crypto/secp256k1/bytes.bend checks

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

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

14 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WW
import ./u32and.bend as FB
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./ineq.bend as I

Definitions

def le_val source · line 21 · raw

@bs:List<&2, U32> -> Nat

the little-endian value of bytes

def pw8 source · line 26 · raw

@n:Nat -> @+y:Nat -> Nat

def pw8_add source · line 31 · raw

@n:Nat -> @+x:Nat -> @+y:Nat -> {pw8(n, Nat.add(x, y)) == Nat.add(pw8(n, x), pw8(n, y)) : Nat}

def pw8_zero source · line 40 · raw

@n:Nat -> {pw8(n, 0n) == 0n : Nat}

def pw8_shift source · line 49 · raw

@n:Nat -> @+y:Nat -> {pw8(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, y)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, pw8(n, y)) : Nat}

def le_app source · line 57 · raw

@xs:List<&2, U32> -> @+ys:List<&2, U32> -> {le_val(List.append(&2, U32, xs, ys)) == Nat.add(le_val(xs), pw8(List.length(&2, U32, xs), le_val(ys))) : Nat}

def app_assoc source · line 69 · raw

@xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+zs:List<&2, U32> -> {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}

def rev_go source · line 76 · raw

@xs:List<&2, U32> -> @+acc:List<&2, U32> -> {List.reverse.go(&2, U32, xs, acc) == List.append(&2, U32, List.reverse.go(&2, U32, xs, []), acc) : List<&2, U32>}

def rev_cons source · line 86 · raw

@+x:U32 -> @+t:List<&2, U32> -> {List.reverse(&2, U32, x <> t) == List.append(&2, U32, List.reverse(&2, U32, t), [x]) : List<&2, U32>}

def len_app source · line 89 · raw

@xs:List<&2, U32> -> @+ys:List<&2, U32> -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}

def len_rev source · line 96 · raw

@xs:List<&2, U32> -> {List.length(&2, U32, List.reverse(&2, U32, xs)) == List.length(&2, U32, xs) : Nat}

def os2ip_go_v source · line 109 · raw

@bs:List<&2, U32> -> @+acc:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip_go(bs, acc) == Nat.add(pw8(List.length(&2, U32, bs), acc), le_val(List.reverse(&2, U32, bs))) : Nat}

def os2ip_v source · line 131 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(bs) == le_val(List.reverse(&2, U32, bs)) : Nat}

def limbs_le_v source · line 138 · raw

@cs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.limbs_le(cs)) == le_val(cs) : Nat}

def of_be_v source · line 157 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(bs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(bs) : Nat}

def of_be_value source · line 162 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(bs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(bs) : Nat}

def byte_lt source · line 168 · raw

@+b:U32 -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.byte(b), 256n) == True{} : Bool}

def byte_lt1 source · line 172 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:U32 -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.byte(b), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, one)) == True{} : Bool}

def limb_lt source · line 177 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> {Nat.is_lt(Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.byte(y), 256n), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.byte(x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool}

y 256 + x < 2^16 for bytes x, y

def limbs_le_ok source · line 183 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @k:Nat -> @cs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(Nat.double(k), cs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, k, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.limbs_le(cs)) == True{} : Bool}

def has_len_v source · line 196 · raw

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

def has_len_rev source · line 207 · raw

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

def of_be_limbs source · line 213 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, bs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(bs)) == True{} : Bool}

def low8 source · line 218 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(8n, n) == Nat.mod(n, 256n) : Nat}

def high8 source · line 225 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(8n, n) == Nat.div(n, 256n) : Nat}

def fits_one source · line 233 · raw

@k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, x) == True{} : Bool}

x < 2^k (2^k with a symbolic one): x fits k bits

def low_v source · line 245 · raw

@+x:Nat -> @+r:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(8n, Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, r))) == Nat.mod(x, 256n) : Nat}

low 8 bits of x + 2^16 r: those of x

def fh8 source · line 250 · raw

@+x:Nat -> @+f16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(8n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(8n, x)) == True{} : Bool}

def mid_v source · line 255 · raw

@+x:Nat -> @+r:Nat -> @+f16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(8n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(8n, Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, r)))) == Nat.div(x, 256n) : Nat}

the next 8 bits: x div 256 (x < 2^16)

def top_v source · line 263 · raw

@+x:Nat -> @+r:Nat -> @+f16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(8n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(8n, Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, r)))) == r : Nat}

the rest: r

def bytes_le_v source · line 269 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @k:Nat -> @xs:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, k, xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.bytes_le(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp_le(Nat.double(k), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs)) : List<&2, U32>}

def i2_is source · line 291 · raw

@+n:Nat -> @x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp(n, x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp_go(n, x) : List<&2, U32>}

def to_be_v source · line 298 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.to_be(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp(32n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs)) : List<&2, U32>}