proofs/crypto/curve25519/poly.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as Poly

11 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../src/crypto/curve25519/field.bend as F
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./num.bend as M
import ./limbs.bend as LM

Definitions

def v source · line 19 · raw

@+x:U32 -> Nat

def len_le source · line 24 · raw

@n:Nat -> @xs:List<&2, U32> -> Bool

def len_ge source · line 39 · raw

@n:Nat -> @xs:List<&2, U32> -> Bool

def len_le_nil source · line 50 · raw

@+n:Nat -> {len_le(n, []) == True{} : Bool}

def len_le_mono source · line 57 · raw

@+k:Nat -> @+d:Nat -> @+xs:List<&2, U32> -> @+e:{len_le(k, xs) == True{} : Bool} -> {len_le(Nat.add(k, d), xs) == True{} : Bool}

def okb_len_le source · line 68 · raw

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

def okb_len_ge source · line 79 · raw

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

def okb_mono source · line 90 · raw

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

def le_add_l source · line 101 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}

def addl_v source · line 107 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_le(v(x), a) == True{} : Bool} -> @+hy:{Nat.is_le(v(y), b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.add(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}

def addl_val source · line 110 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(xs, a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.add(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(xs, ys)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ys)) : Nat}

def addl_lea source · line 126 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(xs, a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.add(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(xs, ys), Nat.add(a, b)) == True{} : Bool}

def addl_okb source · line 138 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hl:{len_le(n, ys) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.add(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(xs, ys), Nat.add(a, b)) == True{} : Bool}

n limbs and at most n limbs give n limbs

def addl_len_ge source · line 157 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+e:{len_ge(n, xs) == True{} : Bool} -> {len_ge(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(xs, ys)) == True{} : Bool}

def addl_len_le source · line 168 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+ex:{len_le(n, xs) == True{} : Bool} -> @+ey:{len_le(n, ys) == True{} : Bool} -> {len_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(xs, ys)) == True{} : Bool}

def sc_mul_l source · line 183 · raw

@+k:Nat -> @+a:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, Nat.mul(a, x)) == Nat.mul(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x)) : Nat}

def scal_v source · line 189 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_le(v(x), a) == True{} : Bool} -> @+hy:{Nat.is_le(v(y), b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}

def scal_val source · line 192 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_le(v(x), a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.scal(x, ys)) == Nat.mul(v(x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ys)) : Nat}

def scal_lea source · line 206 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_le(v(x), a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}

def scal_okb source · line 216 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+x:U32 -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_le(v(x), a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ys, b) == True{} : Bool} -> @+hab:{Nat.is_lt(Nat.mul(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}

def scal_len_ge source · line 230 · raw

@+n:Nat -> @+x:U32 -> @+ys:List<&2, U32> -> @+e:{len_ge(n, ys) == True{} : Bool} -> {len_ge(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.scal(x, ys)) == True{} : Bool}

def scal_len_le source · line 239 · raw

@+n:Nat -> @+x:U32 -> @+ys:List<&2, U32> -> @+e:{len_le(n, ys) == True{} : Bool} -> {len_le(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.scal(x, ys)) == True{} : Bool}

def cb source · line 253 · raw

@xs:List<&2, U32> -> @+k:Nat -> Nat

len(xs) * k

def cbn source · line 260 · raw

@n:Nat -> @+k:Nat -> Nat

def conv_lea source · line 267 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(xs, a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hc:{Nat.is_lt(cb(xs, Nat.mul(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(xs, ys), cb(xs, Nat.mul(a, b))) == True{} : Bool}

def conv_val source · line 280 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(xs, a) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(ys, b) == True{} : Bool} -> @+hc:{Nat.is_lt(cb(xs, Nat.mul(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(xs, ys)) == Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ys)) : Nat}

def conv_len_ge source · line 303 · raw

@+n:Nat -> @+x:U32 -> @+xt:List<&2, U32> -> @+ys:List<&2, U32> -> @+e:{len_ge(n, ys) == True{} : Bool} -> {len_ge(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(x <> xt, ys)) == True{} : Bool}

def conv_len_le source · line 307 · raw

@+j:Nat -> @+k:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+ex:{len_le(j, xs) == True{} : Bool} -> @+ey:{len_le(k, ys) == True{} : Bool} -> {len_le(Nat.add(j, k), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(xs, ys)) == True{} : Bool}

len(conv(xs, ys)) <= j + k when len(xs) <= j and len(ys) <= k

def take_drop_val source · line 323 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.take(n, xs)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.sh(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.take(n, xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.drop(n, xs)))) : Nat}

def take_okb source · line 339 · raw

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

def drop_lea source · line 348 · raw

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

def drop_len_le source · line 357 · raw

@+n:Nat -> @+k:Nat -> @+xs:List<&2, U32> -> @+hl:{len_le(Nat.add(n, k), xs) == True{} : Bool} -> {len_le(k, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.drop(n, xs)) == True{} : Bool}