~/bend-docscommunity

proofs/crypto/curve25519/reduce.bend checks

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

16 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
import ./fold.bend as FD

Definitions

def v source · line 21 · raw

@+x:U32 -> Nat

def val_lt source · line 25 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, 255n) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(n, one)) == True{} : Bool}

value(xs) < 2^(8 n) for n limbs below 2^8

def lt_cancel_r source · line 42 · raw

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

a + t < b + t -> a < b

def shn_ge source · line 51 · raw

@+one:Nat -> @+c:Nat -> @+h:{Nat.is_le(one, c) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, c)) == True{} : Bool}

2^256 c >= 2^256 when c >= 1

def shn_lt_cancel source · line 55 · raw

@+c:Nat -> @+d:Nat -> @+h:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, d)) == True{} : Bool} -> {Nat.is_lt(c, d) == True{} : Bool}

2^256 c < 2^256 2 -> c < 2

def k_le_t source · line 59 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(27n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool}

K = 2^27; K + 38 <= 2^256 and K < 2^256

def k38_le_t source · line 62 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(27n, one), 38n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool}

def small_zero source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Nat -> @+c:Nat -> @+ha:{Nat.is_lt(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool} -> @+hc:{Nat.is_lt(c, one) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool}

case c < 1 (so c == 0): a + 38 c == a < T

def small_one source · line 76 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Nat -> @+c:Nat -> @+V:Nat -> @+hv:{Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, c)) == V : Nat} -> @+hV:{Nat.is_lt(V, Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(27n, one))) == True{} : Bool} -> @+hc:{Nat.is_le(one, c) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool}

case c >= 1: then a < K and c == 1, so a + 38 < K + 38 <= T

def small_by source · line 97 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Nat -> @+c:Nat -> @+V:Nat -> @+b:Bool -> @+hb:{Nat.is_lt(c, one) == b : Bool} -> @+ha:{Nat.is_lt(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool} -> @+hv:{Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, c)) == V : Nat} -> @+hV:{Nat.is_lt(V, Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(27n, one))) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, Nat.mul(38n, c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool}

def two_lt source · line 105 · 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_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pass(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pass(xs))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool}

after two passes the value is below 2^256

def last_zero source · line 125 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Nat -> @+c:Nat -> @+V:Nat -> @+hv:{Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, c)) == V : Nat} -> @+hV:{Nat.is_lt(V, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(32n, one)) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(c, one) == b : Bool} -> {c == 0n : Nat}

a pass of a value below 2^256 carries out 0: the output is the carry's limbs

def pass_exact source · line 134 · raw

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

def reduce_okb source · line 140 · 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.reduce(xs), 255n) == True{} : Bool}

reduce gives 32 limbs below 2^8

def reduce_mod source · line 150 · 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.reduce(xs)), 1n+pp) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs), 1n+pp) : Nat}