proofs/crypto/ed25519/scalar3.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as Scalar3

21 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../spec/crypto/ed25519.bend as SE
import ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/curve25519/x25519.bend as X
import ../../../src/crypto/ed25519/scalar.bend as ESC
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/u32alg.bend as A
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../curve25519/num.bend as M
import ../curve25519/limbs.bend as LM
import ../curve25519/consts.bend as K
import ../curve25519/cong.bend as G
import ./adc.bend as AD
import ./scalar.bend as SC
import ./scalar2.bend as S2

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def dlist source · line 31 · raw

List<&2, U32>

2^256 - 2 L

def zeros source · line 35 · raw

List<&2, U32>

def adc1 source · line 38 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/adc.adc_ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.ell, dlist, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.comp_l, 0n, 0n) == True{} : Bool}

def adc2 source · line 41 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/adc.adc_ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.comp_l, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.ell, zeros, 0n, 1n) == True{} : Bool}

def ell_valo source · line 44 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.ell) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one) : Nat}

def mmL source · line 47 · raw

@+one:Nat -> Nat

def ell_ge source · line 50 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(2n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) == True{} : Bool}

def ell_eq source · line 56 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {1n+mmL(one) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one) : Nat}

def one_lt source · line 59 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(1n, 1n+mmL(one)) == True{} : Bool}

def cp_okb source · line 62 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.comp_l, 255n) == True{} : Bool}

def zero_vg source · line 65 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, zeros) == 0n : Nat}

def hvL source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.comp_l), 1n+mmL(one)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one) : Nat}

(2^256 - L) + L == 2^256

def h2L source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(1n+mmL(one), 1n+mmL(one)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one)) == True{} : Bool}

2 L <= 2^256

def reduce_m source · line 94 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(bs)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs), 1n+mmL(one)) : Nat}

def mul_add_m source · line 103 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+s:List<&2, U32> -> @+r:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(k, 255n) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, r, 255n) == True{} : Bool} -> @+ls:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s), 1n+mmL(one)) == True{} : Bool} -> @+lr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), 1n+mmL(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.mul_add(k, s, r)) == Nat.mod(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s))), 1n+mmL(one)) : Nat}

def mul_add_lt source · line 123 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+s:List<&2, U32> -> @+r:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(k, 255n) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, r, 255n) == True{} : Bool} -> @+ls:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s), 1n+mmL(one)) == True{} : Bool} -> @+lr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), 1n+mmL(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.mul_add(k, s, r), 255n) == True{} : Bool}

def reduce_okb source · line 131 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(bs), 255n) == True{} : Bool}

def lt_l_m source · line 135 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.lt_l(x) == Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), 1n+mmL(one)) : Bool}