~/bend-docscommunity

proofs/crypto/curve25519/proof.bend checks

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

23 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 S
import ../../../spec/crypto/kex.bend as SK
import ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/curve25519/x25519.bend as X
import ../../../src/crypto/kex.bend as K
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 ../../math/natural/arith.bend as NR
import ./limbs.bend as LM
import ./fieldops.bend as FO
import ./mulw.bend as MW
import ./pow.bend as PW
import ./canon.bend as CN
import ./eqf.bend as EQ
import ./xbits.bend as XB
import ./ladder.bend as LD
import ./prime.bend as PR
import ./cong.bend as G

Definitions

def v source · line 30 · raw

@+x:U32 -> Nat

def pp1 source · line 33 · raw

@+one:Nat -> Nat

def ok source · line 36 · raw

@+a:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool}

def tight_of source · line 39 · raw

@+a:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool}

def at_p source · line 43 · raw

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

a statement about p = 1 + pp, restated about FS.prime(one)

def add_value source · line 48 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Add.value(one, h1, a, b, ha, hb)

def add_tight source · line 51 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Add.tight(one, h1, a, b, ha, hb)

def sub_value source · line 54 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Sub.value(one, h1, a, b, ha, hb)

def sub_tight source · line 57 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Sub.tight(one, h1, a, b, ha, hb)

def mul_value source · line 60 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Mul.value(one, h1, a, b, ha, hb)

def mul_tight source · line 63 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Mul.tight(one, h1, a, b, ha, hb)

def sq_value source · line 66 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Sq.value(one, h1, a, ha)

def sq_tight source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Sq.tight(one, h1, a, ha)

def mul_small_value source · line 72 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+k:U32 -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hk:{Nat.is_lt(U32.to_nat(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(17n, one)) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.MulSmall.value(one, h1, a, k, ha, hk)

def mul_small_tight source · line 75 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+k:U32 -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hk:{Nat.is_lt(U32.to_nat(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(17n, one)) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.MulSmall.tight(one, h1, a, k, ha, hk)

def select_zero source · line 78 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Select.zero(one, h1, a, b, ha, hb)

def select_one source · line 81 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Select.one(one, h1, a, b, ha, hb)

def inv_value source · line 84 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Inv.value(one, h1, a, ha)

def inv_tight source · line 89 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Inv.tight(one, h1, a, ha)

def p58_value source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.PowP58.value(one, h1, a, ha)

def p58_tight source · line 98 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.PowP58.tight(one, h1, a, ha)

def freeze_value source · line 101 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Freeze.value(one, h1, a, ha)

def freeze_tight source · line 104 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Freeze.tight(one, h1, a, ha)

def of_bytes_tight source · line 107 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(bs) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.OfBytes.tight(one, h1, bs, hb)

def eq_value source · line 110 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(b) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Eq.value(one, h1, a, b, ha, hb)

def is_zero_value source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.IsZero.value(one, h1, a, ha)

def parity_value source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(a) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.Parity.value(one, h1, a, ha)

def x25519_value source · line 121 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(k) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(u) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.X25519.value(one, h1, k, u, hk, hu)

def valid_eq source · line 124 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.valid_bytes(n, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bytes_ok(n, xs) : Bool}

def checked_by source · line 137 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> @+b1:Bool -> @+e1:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(k) == b1 : Bool} -> @+b2:Bool -> @+e2:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(u) == b2 : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.x25519_if(Bool.and(b1, b2), k, u) == Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(b1, b2), Some{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.x25519(one, k, u)}, None{}) : Maybe<&2, List<&2, U32>>}

def x25519_checked source · line 146 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.X25519.checked(one, h1, k, u)

def le_bytes_ok source · line 153 · raw

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

def finish_tight source · line 164 · raw

@+p:Nat -> @+st:0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.LSt -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.finish(p, st)) == True{} : Bool}

def spec_tight source · line 169 · raw

@+one:Nat -> @+k:List<&2, U32> -> @+u:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.x25519(one, k, u)) == True{} : Bool}

def zero_eq source · line 174 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ss:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, ss, 255n) == True{} : Bool} -> {U32.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sum_all(ss, 0), 0) == Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ss), 0n) : Bool}

def base_eq source · line 179 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.base == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.base : List<&2, U32>}

def base_tight source · line 182 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.base) == True{} : Bool}

def kex_public source · line 185 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+seed:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(seed) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.Kex.public(one, h1, seed, hs)

def nz_eq source · line 191 · raw

@+ss:List<&2, U32> -> @+z:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kex.nonzero(ss, z) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.unless_zero(ss, z) : Maybe<&2, List<&2, U32>>}

def shared_by source · line 198 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ss:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(ss) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kex.shared_of(Some{ss}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.unless_zero(ss, Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ss), 0n)) : Maybe<&2, List<&2, U32>>}

def kex_shared source · line 203 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+pk:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(sk) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(pk) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.Kex.shared(one, h1, sk, pk, hs, hp)

def kex_reject source · line 210 · raw

@+sk:List<&2, U32> -> @+pk:List<&2, U32> -> @+h:{Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(sk), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.tight(pk)) == False{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.Kex.reject(sk, pk, h)