~/bend-docscommunity

proofs/crypto/ed25519/bytes.bend checks

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

14 imports
import Base
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../spec/crypto/ed25519.bend as SE
import ../../../spec/crypto/sha512.bend as SHA
import ../../../src/crypto/hash.bend as H
import ../../../src/crypto/sha512/types.bend as T512
import ../../../src/crypto/sha512/core.bend as C512
import ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/curve25519/x25519.bend as X
import ../../../src/crypto/ed25519/ed25519.bend as E
import ../../lib/logic.bend as L
import ../../math/hash/hash.bend as HH
import ../sha512/conformance.bend as S512
import ../curve25519/limbs.bend as LM

Definitions

def v source · line 20 · raw

@+x:U32 -> Nat

def take_eq source · line 25 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.take(n, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.first(n, xs) : List<&2, U32>}

def drop_eq source · line 36 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.drop(n, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.rest(n, xs) : List<&2, U32>}

def cat_eq source · line 47 · raw

@+xs:List<&2, U32> -> @+ys:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(xs, ys) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(xs, ys) : List<&2, U32>}

def pl source · line 55 · raw

@n:Nat -> @+m:Nat -> Nat

n + m, by recursion on n

def take_okb source · line 62 · raw

@+n:Nat -> @+m:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(pl(n, m), xs, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.take(n, xs), b) == True{} : Bool}

def drop_okb source · line 73 · raw

@+n:Nat -> @+m:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(pl(n, m), xs, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(m, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.drop(n, xs), b) == True{} : Bool}

def e8 source · line 85 · raw

@n:Nat -> Nat

8 n

def bitlen_okb source · line 92 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.bitlen(xs) == e8(n) : Nat}

def bitlen_256 source · line 103 · raw

@+xs:List<&2, U32> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, xs, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.bitlen(xs) == 256n : Nat}

def sha_eq source · line 108 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(bytes) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.sha512_bytes(bytes) : List<&2, U32>}

def byte_and source · line 111 · raw

@+x:U32 -> {Nat.is_le(v(U32.and(x, 255)), 255n) == True{} : Bool}

def okb_con source · line 114 · raw

@+n:Nat -> @+x:U32 -> @+t:List<&2, U32> -> @+hx:{Nat.is_le(v(x), 255n) == True{} : Bool} -> @+ht:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, t, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(1n+n, x <> t, 255n) == True{} : Bool}

def octets_okb source · line 117 · raw

@+n:Nat -> @+x:U32 -> @+t:List<&2, U32> -> @+ht:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, t, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(4n+n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.octets(x, t), 255n) == True{} : Bool}

def lane_okb source · line 127 · raw

@+n:Nat -> @+l:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.Lane -> @+t:List<&2, U32> -> @+ht:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, t, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(8n+n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.lane_octets(l, t), 255n) == True{} : Bool}

def digest_okb source · line 132 · raw

@+s:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.State -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(64n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.digest_bytes(s), 255n) == True{} : Bool}

def sha_okb source · line 145 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(64n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(bytes), 255n) == True{} : Bool}

a digest: 64 bytes, each below 256

def sha_lea source · line 148 · raw

@+bytes:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(bytes), 255n) == True{} : Bool}