~/bend-docscommunity

proofs/crypto/curve25519/fold.bend checks

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

15 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/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

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def fold_id source · line 33 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+a:Nat -> @+c:Nat -> {Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, c)) == Nat.add(Nat.mul(Nat.add(c, c), 1n+pp), Nat.add(a, Nat.mul(38n, c))) : Nat}

A + 2^256 c == 2 c p + (A + 38 c)

def m38 source · line 52 · raw

@+x:Nat -> {Nat.is_le(Nat.mul(38n, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(6n, x)) == True{} : Bool}

38 x <= 2^6 x

def le255 source · line 58 · raw

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

255 <= 2^27 (= 2^8 2^19)

def head_le source · line 65 · raw

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

255 + 38 c <= 2^28 for c <= 2^21

def add0_val source · line 73 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+xt:List<&2, U32> -> @+k:U32 -> @+h:{Nat.is_lt(Nat.add(v(x), v(k)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add0(x <> xt, k)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x <> xt), v(k)) : Nat}

def add0_zero source · line 79 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add0(xs, 0) == xs : List<&2, U32>}

def m38_v source · line 88 · raw

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

def pass_fin_eta source · line 92 · raw

@+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.Cr -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pass_fin(r) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add0(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cl(r), U32.mul(38, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(r))) : List<&2, U32>}

def fin_val source · line 97 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:Nat -> @+a:List<&2, U32> -> @+c:U32 -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(1n+m, a, 255n) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add0(a, U32.mul(38, c))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), Nat.mul(38n, v(c))) : Nat}

def fin_okb source · line 106 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+m:Nat -> @+a:List<&2, U32> -> @+c:U32 -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(1n+m, a, 255n) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(1n+m, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add0(a, U32.mul(38, c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool}

def cr_okb source · line 119 · raw

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

the carry of a 32-limb input: its limbs, value and carry out

def cr_cb source · line 122 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> {Nat.is_le(v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool}

def cr_val source · line 125 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cl(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs) : Nat}

def pass_val source · line 131 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pass(xs)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cl(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0))), Nat.mul(38n, v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0))))) : Nat}

def pass_okb source · line 136 · raw

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

def pass_fold source · line 142 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+xs:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs) == Nat.add(Nat.mul(Nat.add(v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0))), v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, 0)))), 1n+pp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pass(xs))) : Nat}

value(xs) == 2 c p + value(pass(xs))

def pass_mod source · line 151 · raw

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