proofs/crypto/ed25519/scalar2.bend checks

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

23 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../spec/crypto/curve25519/x25519.bend as SX
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/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 ../../math/typed/width.bend as WI
import ../curve25519/num.bend as M
import ../curve25519/limbs.bend as LM
import ../curve25519/consts.bend as K
import ../curve25519/fieldops.bend as FO
import ../curve25519/cong.bend as G
import ../curve25519/xbits.bend as XB
import ./scalar.bend as SC

Definitions

def v source · line 30 · raw

@+x:U32 -> Nat

def shift_sc source · line 33 · raw

@+k:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x) : Nat}

def low_step source · line 41 · raw

@+t:Nat -> @+V:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(1n+t, V) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(t, V), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(t, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.bit(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(t, V)))) : Nat}

bit t joins the low t bits

def byte_fits source · line 56 · raw

@+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.bitlen(bs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs)) == 0n : Nat}

a byte string's value fits its bit count

def low_all source · line 67 · raw

@+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.bitlen(bs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs) : Nat}

def macg source · line 72 · raw

@n:Nat -> @+bs:List<&2, U32> -> @+s:List<&2, U32> -> @+acc:List<&2, U32> -> @+cp:List<&2, U32> -> List<&2, U32>

def mac_eq source · line 80 · raw

@+n:Nat -> @+bs:List<&2, U32> -> @+s:List<&2, U32> -> @+acc:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.mac(n, bs, s, acc) == macg(n, bs, s, acc, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.comp_l) : List<&2, U32>}

def sel_okb source · line 88 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kb:U32 -> @+b:Nat -> @+hk:{v(kb) == b : Nat} -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> @+s:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.select(kb, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.zero, s), 255n) == True{} : Bool}

the selected addend: bit * s

def sel_val source · line 101 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+kb:U32 -> @+b:Nat -> @+hk:{v(kb) == b : Nat} -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> @+s:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.select(kb, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.zero, s)) == Nat.mul(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s)) : Nat}

def sel_lt source · line 114 · raw

@+mm:Nat -> @+b:Nat -> @+S:Nat -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> @+ls:{Nat.is_lt(S, 1n+mm) == True{} : Bool} -> {Nat.is_lt(Nat.mul(b, S), 1n+mm) == True{} : Bool}

def mac_okb source · line 123 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mm:Nat -> @+cp:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 255n) == True{} : Bool} -> @+hv:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp), 1n+mm) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one) : Nat} -> @+n:Nat -> @+bs:List<&2, U32> -> @+s:List<&2, U32> -> @+acc:List<&2, U32> -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, macg(n, bs, s, acc, cp), 255n) == True{} : Bool}

def mac_lt source · line 134 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mm:Nat -> @+h2:{Nat.is_le(Nat.add(1n+mm, 1n+mm), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one)) == True{} : Bool} -> @+cp:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 255n) == True{} : Bool} -> @+hv:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp), 1n+mm) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one) : Nat} -> @+n:Nat -> @+bs:List<&2, U32> -> @+s:List<&2, U32> -> @+acc:List<&2, U32> -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> @+ls:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s), 1n+mm) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> @+la:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 1n+mm) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(mm, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(macg(n, bs, s, acc, cp)), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc)), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s))))

def mac_below source · line 172 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mm:Nat -> @+h2:{Nat.is_le(Nat.add(1n+mm, 1n+mm), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one)) == True{} : Bool} -> @+cp:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 255n) == True{} : Bool} -> @+hv:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp), 1n+mm) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one) : Nat} -> @+n:Nat -> @+bs:List<&2, U32> -> @+s:List<&2, U32> -> @+acc:List<&2, U32> -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> @+ls:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s), 1n+mm) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> @+la:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 1n+mm) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(macg(n, bs, s, acc, cp)), 1n+mm) == True{} : Bool}

def mac_val source · line 194 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mm:Nat -> @+h2:{Nat.is_le(Nat.add(1n+mm, 1n+mm), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one)) == True{} : Bool} -> @+cp:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 255n) == True{} : Bool} -> @+hv:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp), 1n+mm) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one) : Nat} -> @+n:Nat -> @+bs:List<&2, U32> -> @+s:List<&2, U32> -> @+acc:List<&2, U32> -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, s, 255n) == True{} : Bool} -> @+ls:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s), 1n+mm) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> @+la:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 1n+mm) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(macg(n, bs, s, acc, cp)) == Nat.mod(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc)), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(s))), 1n+mm) : Nat}

the exact value: the loop result is reduced