~/bend-docscommunity

proofs/crypto/curve25519/fieldops.bend checks

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

19 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/u32.bend as U
import ../../lib/u32alg.bend as A
import ../../lib/u32div.bend as UD
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ./num.bend as M
import ./limbs.bend as LM
import ./poly.bend as PL
import ./fold.bend as FD
import ./reduce.bend as RD
import ./consts.bend as K

Definitions

def v source · line 25 · raw

@+x:U32 -> Nat

def gea source · line 29 · raw

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

every limb at least b

def le_small source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+hx:{Nat.is_le(x, 4096n) == True{} : Bool} -> {Nat.is_le(x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool}

255 + 255 and 255 + 2040 are below 2^28

def lt32_small source · line 41 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+hx:{Nat.is_le(x, 4096n) == True{} : Bool} -> {Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def addl_okb source · line 46 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool}

def add_okb source · line 50 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add(a, b), 255n) == True{} : Bool}

def add_mod source · line 53 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add(a, b)), 1n+pp) == Nat.mod(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b)), 1n+pp) : Nat}

def gea_head source · line 60 · raw

@+h:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+e:{gea(h <> t, b) == True{} : Bool} -> {Nat.is_le(b, v(h)) == True{} : Bool}

def gea_tail source · line 63 · raw

@+h:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+e:{gea(h <> t, b) == True{} : Bool} -> {gea(t, b) == True{} : Bool}

def subl_v source · line 67 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+k:U32 -> @+bx:Nat -> @+by:Nat -> @+bk:Nat -> @+hx:{Nat.is_le(v(x), bx) == True{} : Bool} -> @+hy:{Nat.is_le(v(y), by) == True{} : Bool} -> @+hk:{Nat.is_le(v(k), bk) == True{} : Bool} -> @+hg:{Nat.is_le(by, v(k)) == True{} : Bool} -> @+hb:{Nat.is_lt(Nat.add(bx, bk), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {Nat.add(v(U32.sub(U32.add(x, k), y)), v(y)) == Nat.add(v(x), v(k)) : Nat}

one limb: (x + k) - y with y <= k, no wrap

def subl_val source · line 77 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+ks:List<&2, U32> -> @+bx:Nat -> @+by:Nat -> @+bk:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, bx) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ys, by) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ks, bk) == True{} : Bool} -> @+hg:{gea(ks, by) == True{} : Bool} -> @+hb:{Nat.is_lt(Nat.add(bx, bk), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.subl(xs, ys, ks)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ys)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ks)) : Nat}

def subl_okb source · line 106 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+ks:List<&2, U32> -> @+bx:Nat -> @+by:Nat -> @+bk:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, bx) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ys, by) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ks, bk) == True{} : Bool} -> @+hg:{gea(ks, by) == True{} : Bool} -> @+hb:{Nat.is_lt(Nat.add(bx, bk), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.subl(xs, ys, ks), Nat.add(bx, bk)) == True{} : Bool}

def sub_core source · line 128 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+S:Nat -> @+hS:{Nat.add(S, B) == Nat.add(A, Nat.mul(8n, 1n+pp)) : Nat} -> {Nat.mod(S, 1n+pp) == Nat.mod(Nat.sub(Nat.add(A, 1n+pp), Nat.mod(B, 1n+pp)), 1n+pp) : Nat}

S + B == A + 8 P gives S == (A + P - (B mod P)) mod P, mod P

def subg_okb source · line 151 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ks:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, ks, 2040n) == True{} : Bool} -> @+hg:{gea(ks, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.subl(a, b, ks), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool}

sub with its 8p constant as a parameter

def subg_mod source · line 155 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ks:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, ks, 2040n) == True{} : Bool} -> @+hg:{gea(ks, 255n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, ks) == Nat.mul(8n, 1n+pp) : Nat} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.subl(a, b, ks))), 1n+pp) == Nat.mod(Nat.sub(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 1n+pp), Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b), 1n+pp)), 1n+pp) : Nat}

def eight_p_okb source · line 162 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.eight_p, 2040n) == True{} : Bool}

def eight_p_gea source · line 165 · raw

{gea(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.eight_p, 255n) == True{} : Bool}

def sub_okb source · line 168 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sub(a, b), 255n) == True{} : Bool}

def sub_mod source · line 171 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sub(a, b)), 1n+pp) == Nat.mod(Nat.sub(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 1n+pp), Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b), 1n+pp)), 1n+pp) : Nat}

def mul1 source · line 176 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> {U32.mul(x, 1) == x : U32}

def mul0 source · line 180 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> {U32.mul(x, 0) == 0 : U32}

def select0 source · line 184 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, 255n) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ys, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.select(0, xs, ys) == xs : List<&2, U32>}

def select1 source · line 199 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, 255n) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ys, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.select(1, xs, ys) == ys : List<&2, U32>}