proofs/crypto/curve25519/mulw.bend checks

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

17 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 ../../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
import ./fieldops.bend as FO

Definitions

def v source · line 24 · raw

@+x:U32 -> Nat

def cbn_add source · line 29 · raw

@+a:Nat -> @+b:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cbn(Nat.add(a, b), k) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cbn(a, k), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cbn(b, k)) : Nat}

def cbn_pow source · line 36 · raw

@+j:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cbn(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, 1n), k) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, k) : Nat}

def cb_okb source · line 47 · raw

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

def mm8 source · line 58 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(16n, one) : Nat}

def cb32 source · line 61 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:Nat -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cb(a, Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one))) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one) : Nat}

def lea8 source · line 68 · raw

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

def conv_ge source · line 71 · raw

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

def conv_hc source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cb(a, Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def conv_lea21 source · line 81 · 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.lea(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(a, b), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool}

def conv_val source · line 86 · 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/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(a, b)) == Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b)) : Nat}

def m38_27 source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.mul(38n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(27n, one)) == True{} : Bool}

def wsum_le source · line 95 · raw

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

def wsum_lt source · line 99 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one), Nat.mul(38n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def m38_lt source · line 102 · raw

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

def wide_okb source · line 105 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+zs:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(zs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> @+hge:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.len_ge(32n, zs) == True{} : Bool} -> @+hle:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.len_le(64n, zs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.wide(zs), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool}

def wide_mod source · line 117 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+zs:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(zs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> @+hge:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.len_ge(32n, zs) == True{} : Bool} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.wide(zs)), 1n+pp) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(zs), 1n+pp) : Nat}

def wide_in source · line 137 · 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.wide(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.conv(a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool}

def mul_okb source · line 143 · 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.mul(a, b), 255n) == True{} : Bool}

def mul_mod source · line 146 · 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.mul(a, b)), 1n+pp) == Nat.mod(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b)), 1n+pp) : Nat}

def sq_okb source · line 154 · raw

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

def sq_mod source · line 157 · 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> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sq(a)), 1n+pp) == Nat.mod(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a)), 1n+pp) : Nat}

def ms_lt source · line 162 · raw

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

def ms_le source · line 167 · raw

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

def scal_in source · line 172 · raw

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

def mul_small_okb source · line 176 · raw

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

def mul_small_mod source · line 179 · 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> -> @+k:U32 -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hk:{Nat.is_le(v(k), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(17n, one)) == True{} : Bool} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.mul_small(a, k)), 1n+pp) == Nat.mod(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), v(k)), 1n+pp) : Nat}