~/bend-docscommunity

proofs/crypto/curve25519/ladder.bend checks

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

19 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 S
import ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/curve25519/x25519.bend as X
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ./limbs.bend as LM
import ./consts.bend as K
import ./fieldops.bend as FO
import ./canon.bend as CN
import ./cong.bend as G
import ./rel.bend as RL
import ./mulw.bend as MW
import ./pow.bend as PW
import ./xbits.bend as XB
import ./prime.bend as PR

Definitions

def v source · line 26 · raw

@+x:U32 -> Nat

def DP source · line 29 · raw

@-A:Data -> @-B:Data -> Data

def Rst source · line 32 · raw

@+pp:Nat -> @st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.St -> @sst:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.LSt -> Data

def o_sel source · line 39 · raw

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

def c_fst source · line 52 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+sw:U32 -> @+s:Nat -> @+hs:{v(sw) == s : Nat} -> @+hb:{Nat.is_le(s, 1n) == True{} : Bool} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+A:Nat -> @+B:Nat -> @+oa:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+ca:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), A) -> @+ob:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> @+cb:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b), B) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.select(sw, a, b)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.cs_fst(s, A, B))

def c_snd source · line 65 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+sw:U32 -> @+s:Nat -> @+hs:{v(sw) == s : Nat} -> @+hb:{Nat.is_le(s, 1n) == True{} : Bool} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+A:Nat -> @+B:Nat -> @+oa:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+ca:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), A) -> @+ob:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> @+cb:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b), B) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.select(sw, b, a)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.cs_snd(s, A, B))

def a24_c source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+c24:List<&2, U32> -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, c24) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.a24(one) : Nat} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(c24), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.a24(one))

def step_rel source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+c24:List<&2, U32> -> @+oc:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, c24, 255n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, c24) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.a24(one) : Nat} -> @+x1:List<&2, U32> -> @+X1:Nat -> @+o1:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x1, 255n) == True{} : Bool} -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x1), X1) -> @+x2:List<&2, U32> -> @+X2:Nat -> @+o2:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x2, 255n) == True{} : Bool} -> @+c2:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x2), X2) -> @+z2:List<&2, U32> -> @+Z2:Nat -> @+oz2:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, z2, 255n) == True{} : Bool} -> @+cz2:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(z2), Z2) -> @+x3:List<&2, U32> -> @+X3:Nat -> @+o3:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x3, 255n) == True{} : Bool} -> @+c3:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x3), X3) -> @+z3:List<&2, U32> -> @+Z3:Nat -> @+oz3:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, z3, 255n) == True{} : Bool} -> @+cz3:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(z3), Z3) -> @+kt:U32 -> @+KT:Nat -> @+hk:{v(kt) == KT : Nat} -> @+hkb:{Nat.is_le(KT, 1n) == True{} : Bool} -> Rst(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.step(c24, x1, x2, z2, x3, z3, kt), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.step(one, 1n+pp, X1, X2, Z2, X3, Z3, KT))

def rung_rel source · line 153 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+c24:List<&2, U32> -> @+oc:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, c24, 255n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, c24) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.a24(one) : Nat} -> @+x1:List<&2, U32> -> @+X1:Nat -> @+o1:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x1, 255n) == True{} : Bool} -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x1), X1) -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.St -> @+sst:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.LSt -> @+h:Rst(pp, st, sst) -> @+kt:U32 -> @+KT:Nat -> @+hk:{v(kt) == KT : Nat} -> @+hkb:{Nat.is_le(KT, 1n) == True{} : Bool} -> Rst(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.rung(c24, x1, st, kt), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.rung(one, 1n+pp, X1, sst, KT))

def ladder_rel source · line 177 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+n:Nat -> @+c24:List<&2, U32> -> @+oc:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, c24, 255n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, c24) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.a24(one) : Nat} -> @+kc:List<&2, U32> -> @+hkc:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(kc, 255n) == True{} : Bool} -> @+x1:List<&2, U32> -> @+X1:Nat -> @+o1:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x1, 255n) == True{} : Bool} -> @+c1:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x1), X1) -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.St -> @+sst:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.LSt -> @+h:Rst(pp, st, sst) -> Rst(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.ladder(n, c24, kc, x1, st), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.ladder(one, 1n+pp, n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(kc), X1, sst))

def finish_rel source · line 188 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.St -> @+sst:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.LSt -> @+h:Rst(pp, st, sst) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.finish(st) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.finish(1n+pp, sst) : List<&2, U32>}

def a24_shape source · line 227 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.a24 == 65 <> 219 <> 1 <> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.rep(29n, 0, []) : List<&2, U32>}

def a24_valo source · line 230 · raw

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

def x25519_rel source · line 235 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, u, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.x25519_raw(k, u) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.finish(1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.ladder(one, 1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.nbits(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.clamp(k)), Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.decode_u(u), 1n+pp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.LSt{1n, 0n, Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.decode_u(u), 1n+pp), 1n, 0n})) : List<&2, U32>}

def x25519_value source · line 246 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(k) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(u) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.X25519.value(one, h1, k, u, hk, hu)