~/bend-docscommunity

proofs/crypto/curve25519/prime.bend checks

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

8 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./num.bend as M

Definitions

def pp_of source · line 13 · raw

@+one:Nat -> Nat

def p20 source · line 16 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(20n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one)) == True{} : Bool}

def pp_sum source · line 21 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(20n, pp_of(one)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat}

20 + pp == 2^255

def hP source · line 24 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(1n+pp_of(one), 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat}

def prime_eq source · line 29 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.prime(one) == 1n+pp_of(one) : Nat}