~/bend-docscommunity

proofs/crypto/curve25519/consts.bend checks

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

13 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

Definitions

def v source · line 20 · raw

@+x:U32 -> Nat

def valo source · line 24 · raw

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

the value of xs times one, digit by digit

def valo_value source · line 31 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> {valo(one, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs) : Nat}

def rep source · line 40 · raw

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

n copies of k, then tl

def run8 source · line 48 · raw

@+one:Nat -> @+n:Nat -> @+tl:List<&2, U32> -> {Nat.add(valo(one, rep(n, 2040, tl)), Nat.mul(one, 8n)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(n, Nat.add(valo(one, tl), Nat.mul(one, 8n))) : Nat}

a run of 2040 = 8 * 255 absorbs a carry of 8

def run0 source · line 68 · raw

@+one:Nat -> @+n:Nat -> @+tl:List<&2, U32> -> {valo(one, rep(n, 0, tl)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.shn(n, valo(one, tl)) : Nat}

a run of zeros shifts

def one_k source · line 77 · raw

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

def s258 source · line 81 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(258n, one) == Nat.add(Nat.mul(8n, 1n+pp), 152n) : Nat}

2^258 == 8 p + 152

def eight_p_shape source · line 89 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.eight_p == 1896 <> rep(30n, 2040, [1016]) : List<&2, U32>}

def eight_p_val source · line 93 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> {valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.eight_p) == Nat.mul(8n, 1n+pp) : Nat}

value(8p limbs) == 8 p

def vg source · line 120 · raw

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

valo guarded on one: kept folded by the checker (see FS.gdigits)

def vg_valo source · line 127 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> {vg(one, xs) == valo(one, xs) : Nat}