~/bend-docscommunity

proofs/crypto/ed25519/pdec.bend checks

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

26 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/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 ./pcodec.bend as PC
import ../curve25519/num.bend as M3

Definitions

def v source · line 32 · raw

@+x:U32 -> Nat

def hv_p source · line 36 · 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(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.comp_p), 1n+pp) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.T(one) : Nat}

y >= p exactly when the carry of y + 2^256 - p is not 0

def ge_p_eq source · line 42 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+y:List<&2, U32> -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.ge_p(y) == Bool.not(Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), 1n+pp)) : Bool}

def dec_fin_rel_core source · line 47 · 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} -> @+y:List<&2, U32> -> @+b:Nat -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> @+hb0:{Nat.is_le(b0, 1n) == True{} : Bool} -> @+fs:Bool -> @+hf:{Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.is_zero(x), U32.is_eq(x0, 1)) == fs : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.dec_fin(x, y, x0, fs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dec_fin(1n+pp, a, b, b0, fs))

def dec_fin_rel source · line 67 · 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} -> @+y:List<&2, U32> -> @+b:Nat -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> @+hb0:{Nat.is_le(b0, 1n) == True{} : Bool} -> @+fs:Bool -> @+hf:{Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.is_zero(x), U32.is_eq(x0, 1)) == fs : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.dec_fin(x, y, x0, Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.is_zero(x), U32.is_eq(x0, 1))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dec_fin(1n+pp, a, b, b0, fs))

def fail_eq source · line 71 · 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} -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> {Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.is_zero(x), U32.is_eq(x0, 1)) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b0, 1n)) : Bool}

def dec_root_rel_core source · line 78 · 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 -> @+rs:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp)) -> @+x:List<&2, U32> -> @+a:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> @+y:List<&2, U32> -> @+b:Nat -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> @+hb0:{Nat.is_le(b0, 1n) == True{} : Bool} -> @+u:List<&2, U32> -> @+vxx:List<&2, U32> -> @+iu:Bool -> @+inu:Bool -> @+su:Bool -> @+snu:Bool -> @+hu:{iu == su : Bool} -> @+hnu:{inu == snu : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.dec_root(cs, x, y, x0, u, vxx, su, snu), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dec_root(1n+pp, a, b, b0, su, snu))

def dec_root_rel source · line 94 · 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 -> @+rs:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp)) -> @+x:List<&2, U32> -> @+a:Nat -> @+rx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, x, a) -> @+ha:{Nat.mod(a, 1n+pp) == a : Nat} -> @+y:List<&2, U32> -> @+b:Nat -> @+ry:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, y, b) -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> @+hb0:{Nat.is_le(b0, 1n) == True{} : Bool} -> @+u:List<&2, U32> -> @+vxx:List<&2, U32> -> @+iu:Bool -> @+inu:Bool -> @+su:Bool -> @+snu:Bool -> @+hu:{iu == su : Bool} -> @+hnu:{inu == snu : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.dec_root(cs, x, y, x0, u, vxx, iu, inu), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dec_root(1n+pp, a, b, b0, su, snu))

def nf source · line 99 · raw

@+b:Bool -> @+h:{Bool.not(b) == False{} : Bool} -> {b == True{} : Bool}

def dec_y_rel_core source · line 106 · 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 -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(cs), D) -> @+rs:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp)) -> @+y:List<&2, U32> -> @+Y:Nat -> @+hyv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y) == Y : Nat} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> @+hb0:{Nat.is_le(b0, 1n) == True{} : Bool} -> @+bad:Bool -> @+hbad:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.ge_p(y) == bad : Bool} -> @+hlt:{Bool.not(Nat.is_lt(Y, 1n+pp)) == bad : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.dec_y(cs, y, x0, bad), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dec_y(1n+pp, D, Y, b0, bad))

def dec_y_rel source · line 148 · 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 -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(cs), D) -> @+rs:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp)) -> @+y:List<&2, U32> -> @+Y:Nat -> @+hyv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y) == Y : Nat} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+x0:U32 -> @+b0:Nat -> @+hx0:{v(x0) == b0 : Nat} -> @+hb0:{Nat.is_le(b0, 1n) == True{} : Bool} -> @+bad:Bool -> @+hbad:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.ge_p(y) == bad : Bool} -> @+hlt:{Bool.not(Nat.is_lt(Y, 1n+pp)) == bad : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.dec_y(cs, y, x0, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.ge_p(y)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dec_y(1n+pp, D, Y, b0, bad))

def decode_rel source · line 152 · 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 -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(cs), D) -> @+rs:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp)) -> @+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, bs, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.decode(cs, bs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.decode(1n+pp, D, bs))

def le_bytes_ok source · line 163 · raw

@+n:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.le_bytes(n, x), 255n) == True{} : Bool}

def identity_rel source · line 174 · raw

@+pp:Nat -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.identity, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.identity)

def base_of_rel source · line 177 · raw

@+pp:Nat -> @+m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt> -> @+sm:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt> -> @+h:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, m, sm) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.base_of(m), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.base_of(sm))

def base_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} -> @+cs:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Cs -> @+D:Nat -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(cs), D) -> @+rs:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_s(cs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sqm1(1n+pp)) -> @+xs:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.base(cs, xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.base(1n+pp, D))