~/bend-docscommunity

proofs/crypto/ed25519/pcodec.bend checks

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

29 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 ../../../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 ../../lib/u32.bend as U
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../curve25519/limbs.bend as LM
import ../curve25519/consts.bend as K
import ../curve25519/fieldops.bend as FO
import ../curve25519/mulw.bend as MW
import ../curve25519/pow.bend as PW
import ../curve25519/canon.bend as CN
import ../curve25519/eqf.bend as EQ
import ../curve25519/freeze.bend as FZ
import ../curve25519/cong.bend as G
import ../curve25519/rel.bend as RL
import ../curve25519/xbits.bend as XB
import ../curve25519/ladder.bend as LD
import ./scalar.bend as SC
import ./prel.bend as PR
import ../curve25519/num.bend as M2

Definitions

def v source · line 34 · raw

@+x:U32 -> Nat

def MR source · line 38 · raw

@+pp:Nat -> @+m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt> -> @+sm:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt> -> Data

decoding results: both None, or both Some of related points

def r_zero source · line 51 · raw

@+pp:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.zero, 0n)

def r_one source · line 54 · raw

@+pp:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.one, 1n)

def r_small source · line 57 · raw

@+pp:Nat -> @+k:U32 -> @+hk:{Nat.is_le(v(k), 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.small(k), v(k))

def c65_shape source · line 60 · raw

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

def c66_shape source · line 63 · raw

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

def c65_valo source · line 66 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.c121665) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.digits(one, [65n, 219n, 1n]) : Nat}

def c66_valo source · line 71 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.c121666) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.digits(one, [66n, 219n, 1n]) : Nat}

def r_valo source · line 77 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+ks:List<&2, U32> -> @+D:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, ks) == D : Nat} -> @+ho:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, ks, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, ks, D)

a constant given through its valo, the list kept a variable

def lit_valo source · line 80 · raw

@+one:Nat -> @+xs:List<&2, U32> -> @+k:List<&2, U32> -> @+D:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, k) == D : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.lit(xs, k)) == D : Nat}

def lit_okb source · line 87 · raw

@+xs:List<&2, U32> -> @+k:List<&2, U32> -> @+ho:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.lit(xs, k), 255n) == True{} : Bool}

def r_lit_small source · line 94 · raw

@+pp:Nat -> @+xs:List<&2, U32> -> @+k:U32 -> @+hk:{Nat.is_le(v(k), 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.lit(xs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.small(k)), v(k))

def r_c65 source · line 101 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+xs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.lit(xs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.c121665), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.digits(one, [65n, 219n, 1n]))

def r_c66 source · line 104 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+xs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.lit(xs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.c121666), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.digits(one, [66n, 219n, 1n]))

def dval source · line 109 · raw

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

def r_d source · line 112 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+xs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp))

def r_d2 source · line 119 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+xs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d2(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fadd(1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp)))

def p14_bits source · line 122 · raw

List<&2, Bool>

def eb_p14 source · line 125 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/pow.eb(one, p14_bits) == 3n : Nat}

def p14_exp source · line 129 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> {Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/pow.Fo(one, 250n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/pow.blen(p14_bits), one)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/pow.eb(one, p14_bits)) == Nat.div(Nat.sub(1n+pp, 1n), 4n) : Nat}

8 Fo(250) + 3 == (p - 1) / 4

def r_sqm1 source · line 145 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+xs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp))

def red source · line 160 · raw

@+pp:Nat -> @+a:Nat -> {Nat.mod(Nat.mod(a, 1n+pp), 1n+pp) == Nat.mod(a, 1n+pp) : Nat}

def eq_rel source · line 163 · 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) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> @+hb:{Nat.mod(b, 1n+pp) == b : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.eq(x, y) == Nat.is_eq(a, b) : Bool}

def iz_rel source · line 169 · 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) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.is_zero(x) == Nat.is_eq(a, 0n) : Bool}

def par_rel source · line 173 · 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) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> {v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.parity(x)) == Nat.mod(a, 2n) : Nat}

def u32_eq_nat source · line 176 · raw

@+a:U32 -> @+b:U32 -> {U32.is_eq(a, b) == Nat.is_eq(v(a), v(b)) : Bool}

def mod2_le source · line 179 · raw

@+a:Nat -> {Nat.is_le(Nat.mod(a, 2n), 1n) == True{} : Bool}

def equal_rel source · line 184 · 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 -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+sq:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hp:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, p, sp) -> @+hq:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, q, sq) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.equal(p, q) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.equal(1n+pp, sp, sq) : Bool}

def set_eq source · line 200 · raw

@+xs:List<&2, U32> -> @+b:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.set_top(xs, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.set_msb(xs, b) : List<&2, U32>}

def bytes_rel source · line 212 · 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) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.to_bytes(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.le_bytes(32n, a) : List<&2, U32>}

the canonical bytes of an element related to a reduced a

def par_u32 source · line 218 · 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) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.parity(x) == U32.from_nat(Nat.mod(a, 2n)) : U32}

def encode_rel source · line 223 · 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:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, p, sp) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.encode(p) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.encode_n(32n, 1n+pp, sp) : List<&2, U32>}