~/bend-docscommunity

proofs/crypto/ed25519/top.bend checks

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

24 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 ../../../spec/crypto/sha512.bend as SHA
import ../../../src/crypto/hash.bend as H
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 ../../../src/crypto/ed25519/scalar.bend as ESC
import ../../../src/crypto/ed25519/ed25519.bend as E
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../curve25519/limbs.bend as LM
import ../curve25519/cong.bend as G
import ../curve25519/rel.bend as RL
import ../curve25519/xbits.bend as XB
import ./scalar.bend as SC
import ./scalar3.bend as S3
import ./prel.bend as PR
import ./pcodec.bend as PC
import ./pdec.bend as PD
import ./bytes.bend as BY

Definitions

def bits_eq source · line 31 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.bitlen(k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, one) : Nat}

def mul_rel 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} -> @+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)) -> @+k:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> @+p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sp:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hp:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, p, sp) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.mul(cs, k, p), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.mul(one, 1n+pp, D, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(k), sp))

[k] p, k 32 bytes: the implementation runs over bitlen(k) = 256 bits, the spec over 2^8 one

def enc_rel source · line 41 · 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(one, 1n+pp, sp) : List<&2, U32>}

encode, the spec's byte count 2^5 one

def rh_val source · line 46 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(bs))) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.sha512_bytes(bs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) : Nat}

def rh_eq source · line 55 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+sbs:List<&2, U32> -> @+e:{bs == sbs : List<&2, U32>} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(bs))) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.sha512_bytes(sbs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) : Nat}

def hram_s source · line 58 · raw

@+one:Nat -> @+rb:List<&2, U32> -> @+a:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.hram(one, rb, a, msg) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.sha512_bytes(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(rb, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(a, msg)))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)) : Nat}

def hram_i source · line 65 · raw

@+rb:List<&2, U32> -> @+a:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.hram(rb, a, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.sha512(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(rb, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(a, msg)))) : List<&2, U32>}

def red_lt source · line 72 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(bs)), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar3.mmL(one)) == True{} : Bool}

def secret_eq source · line 76 · raw

@+h:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.clamp(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.take(32n, h))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.secret(h) : Nat}

def cat2_eq source · line 81 · raw

@+x:List<&2, U32> -> @+sx:List<&2, U32> -> @+y:List<&2, U32> -> @+sy:List<&2, U32> -> @+m:List<&2, U32> -> @+ex:{x == sx : List<&2, U32>} -> @+ey:{y == sy : List<&2, U32>} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(x, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(y, m)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(sx, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(sy, m)) : List<&2, U32>}

def hk_okb source · line 88 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+rb:List<&2, U32> -> @+a:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.hram(rb, a, msg), 255n) == True{} : Bool}

def hk_val source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+rb:List<&2, U32> -> @+srb:List<&2, U32> -> @+erb:{rb == srb : List<&2, U32>} -> @+a:List<&2, U32> -> @+sa:List<&2, U32> -> @+ea:{a == sa : List<&2, U32>} -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.hram(rb, a, msg)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.hram(one, srb, sa, msg) : Nat}

def ma_eq source · line 102 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+r:List<&2, U32> -> @+sk:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, r, 255n) == True{} : Bool} -> @+lr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar3.mmL(one)) == True{} : Bool} -> @+hsk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, sk, 255n) == True{} : Bool} -> @+Rs:Nat -> @+Ks:Nat -> @+Ss:Nat -> @+eR:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r) == Rs : Nat} -> @+eK:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(k) == Ks : Nat} -> @+eS:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(sk) == Ss : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.mul_add(k, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(sk), r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.le_bytes(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(5n, one), Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one))) : List<&2, U32>}

S = (r + k s) mod L, as 32 bytes: s reduced first (the implementation's reduce(secret)), the same residue

def public_body_rel source · line 137 · 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> -> @+D:Nat -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), D) -> @+rd2: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, D, D)) -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(64n, h, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.public_of(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs), xs, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.public_body(one, 1n+pp, D, h) : List<&2, U32>}

def pub_guard source · line 149 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+h:List<&2, U32> -> @+x:List<&2, U32> -> @+e:{x == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.public_body(one, p, d, h) : List<&2, U32>} -> {x == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.public_of(one, p, d, h) : List<&2, U32>}

def public_rel source · line 156 · 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> -> @+D:Nat -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), D) -> @+rd2: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, D, D)) -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(64n, h, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.public_of(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs), xs, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.public_of(one, 1n+pp, D, h) : List<&2, U32>}

def rb_eq source · line 159 · 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)) -> @+B:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+SB:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hB:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, B, SB) -> @+r:List<&2, U32> -> @+okr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, r, 255n) == True{} : Bool} -> @+Rs:Nat -> @+eR:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r) == Rs : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.encode(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.mul(cs, r, B)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.encode(one, 1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.mul(one, 1n+pp, D, Rs, SB)) : List<&2, U32>}

def sig_eq source · line 164 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+RB:List<&2, U32> -> @+SRB:List<&2, U32> -> @+eRB:{RB == SRB : List<&2, U32>} -> @+k:List<&2, U32> -> @+okk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> @+Ks:Nat -> @+eK:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(k) == Ks : Nat} -> @+r:List<&2, U32> -> @+okr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, r, 255n) == True{} : Bool} -> @+lr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar3.mmL(one)) == True{} : Bool} -> @+Rs:Nat -> @+eR:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(r) == Rs : Nat} -> @+sk:List<&2, U32> -> @+hsk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, sk, 255n) == True{} : Bool} -> @+Ss:Nat -> @+eS:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(sk) == Ss : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(RB, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.mul_add(k, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.reduce(sk), r)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(SRB, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.le_bytes(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(5n, one), Nat.mod(Nat.add(Rs, Nat.mul(Ks, Ss)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.ell(one)))) : List<&2, U32>}

R || S

def prefix_eq source · line 170 · raw

@+h:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.cat(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.drop(32n, h), msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.cat(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.rest(32n, h), msg) : List<&2, U32>}

def sign_body_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} -> @+xs:List<&2, U32> -> @+D:Nat -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), D) -> @+rd2: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, D, D)) -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(64n, h, 255n) == True{} : Bool} -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.sign_with(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs), xs, h, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sign_body(one, 1n+pp, D, h, msg) : List<&2, U32>}

def sign_guard source · line 198 · raw

@+one:Nat -> @+p:Nat -> @+d:Nat -> @+h:List<&2, U32> -> @+msg:List<&2, U32> -> @+x:List<&2, U32> -> @+e:{x == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sign_body(one, p, d, h, msg) : List<&2, U32>} -> {x == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sign_with(one, p, d, h, msg) : List<&2, U32>}

def sign_rel source · line 205 · 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> -> @+D:Nat -> @+rd:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.cs_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs)), D) -> @+rd2: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, D, D)) -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(64n, h, 255n) == True{} : Bool} -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.sign_with(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(xs), xs, h, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.sign_with(one, 1n+pp, D, h, msg) : List<&2, U32>}

def check_some source · line 210 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+rb:List<&2, U32> -> @+sb:List<&2, U32> -> @+hsb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, sb, 255n) == True{} : Bool} -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sr:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hr:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, r, sr) -> @+a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sa:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+ha:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, a, sa) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.check(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(pk), sb, rb, pk, msg, Some{r}, Some{a}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.check(one, 1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(sb), rb, pk, msg, Some{sr}, Some{sa}) : Bool}

def check_a source · line 231 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+rb:List<&2, U32> -> @+sb:List<&2, U32> -> @+hsb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, sb, 255n) == True{} : Bool} -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt -> @+sr:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt -> @+hr:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.Rp(pp, r, sr) -> @+aa:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt> -> @+saa:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt> -> @+haa:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, aa, saa) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.check(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(pk), sb, rb, pk, msg, Some{r}, aa) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.check(one, 1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(sb), rb, pk, msg, Some{sr}, saa) : Bool}

def check_rel source · line 242 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+pk:List<&2, U32> -> @+msg:List<&2, U32> -> @+rb:List<&2, U32> -> @+sb:List<&2, U32> -> @+hsb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, sb, 255n) == True{} : Bool} -> @+ra:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt> -> @+sra:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt> -> @+hra:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, ra, sra) -> @+aa:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.Pt> -> @+saa:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.EPt> -> @+haa:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.MR(pp, aa, saa) -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.check(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(pk), sb, rb, pk, msg, ra, aa) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.check(one, 1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(sb), rb, pk, msg, sra, saa) : Bool}

def verify_with_rel source · line 253 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+pk:List<&2, U32> -> @+hpk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, pk, 255n) == True{} : Bool} -> @+msg:List<&2, U32> -> @+rb:List<&2, U32> -> @+hrb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, rb, 255n) == True{} : Bool} -> @+sb:List<&2, U32> -> @+hsb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, sb, 255n) == True{} : Bool} -> @+s_ok:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.verify_with(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.consts(pk), pk, msg, rb, sb, s_ok) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.verify_with(one, 1n+pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.dconst(one, 1n+pp), pk, msg, rb, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(sb), s_ok) : Bool}