~/bend-docscommunity

proofs/crypto/ed25519/prel.bend checks

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

16 imports
import Base
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../spec/crypto/curve25519/x25519.bend as SX
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/point.bend as PT
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../curve25519/limbs.bend as LM
import ../curve25519/fieldops.bend as FO
import ../curve25519/mulw.bend as MW
import ../curve25519/cong.bend as G
import ../curve25519/rel.bend as RL
import ../curve25519/xbits.bend as XB

Definitions

def v source · line 23 · raw

@+x:U32 -> Nat

def DP source · line 26 · raw

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

def fst source · line 29 · raw

@-A:Data -> @-B:Data -> @+p:DP(A, B) -> A

def snd source · line 34 · raw

@-A:Data -> @-B:Data -> @+p:DP(A, B) -> B

def Rp source · line 39 · raw

@+pp:Nat -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> Data

def mk source · line 44 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+z:List<&2, U32> -> @+t:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> @+rz:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, z, c) -> @+rt:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, t, d) -> Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt{x, y, z, t}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt{a, b, c, d})

def rX source · line 47 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+z:List<&2, U32> -> @+t:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h:Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt{x, y, z, t}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt{a, b, c, d}) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a)

def rY source · line 50 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+z:List<&2, U32> -> @+t:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h:Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt{x, y, z, t}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt{a, b, c, d}) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b)

def rZ source · line 53 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+z:List<&2, U32> -> @+t:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h:Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt{x, y, z, t}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt{a, b, c, d}) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, z, c)

def rT source · line 56 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+z:List<&2, U32> -> @+t:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h:Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt{x, y, z, t}, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt{a, b, c, d}) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, t, d)

def o source · line 60 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+a:Nat -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool}

relation-level field operations

def c source · line 63 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+a:Nat -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a)

def radd source · line 66 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fadd(1n+pp, a, b))

def rsub source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sub(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fsub(1n+pp, a, b))

def rmul source · line 72 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.mul(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fmul(1n+pp, a, b))

def rsq source · line 75 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+x:List<&2, U32> -> @+a:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sq(x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fmul(1n+pp, a, a))

def add_rel source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+cs:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Cs -> @+D:Nat -> @+rd2:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d2(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fadd(1n+pp, D, D)) -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+sq:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hp:Rp(pp, p, sp) -> @+hq:Rp(pp, q, sq) -> Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.add(cs, p, q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.add(1n+pp, D, sp, sq))

def double_rel source · line 120 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hp:Rp(pp, p, sp) -> Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.double(p), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.double(1n+pp, sp))

def sel_eq0 source · line 158 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+sq:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+pp:Nat -> @+hp:Rp(pp, p, sp) -> @+hq:Rp(pp, q, sq) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.select(0, p, q) == p : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt}

def sel_eq1 source · line 175 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+sq:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+pp:Nat -> @+hp:Rp(pp, p, sp) -> @+hq:Rp(pp, q, sq) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.select(1, p, q) == q : 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt}

def sel_rel source · line 192 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+s:U32 -> @+b:Nat -> @+hs:{v(s) == b : Nat} -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+sq:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hp:Rp(pp, p, sp) -> @+hq:Rp(pp, q, sq) -> Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.select(s, p, q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.pick(b, sp, sq))

def smul_rel source · line 207 · 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 -> @+cs:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Cs -> @+D:Nat -> @+rd2:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d2(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fadd(1n+pp, D, D)) -> @+bs:List<&2, U32> -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hp:Rp(pp, p, sp) -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sq:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hq:Rp(pp, q, sq) -> Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.smul(n, cs, bs, p, q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.smul(1n+pp, D, n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs), sp, sq))