proofs/crypto/curve25519/rel.bend checks

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

15 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../src/crypto/curve25519/field.bend as F
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 ../../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 ./cong.bend as G

Definitions

def R source · line 22 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+a:Nat -> Data

def rc_add source · line 25 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> @+oy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+cy:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), b) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add(x, y)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fadd(1n+pp, a, b))

def r_add source · line 29 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> @+oy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+cy:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), b) -> R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.add(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fadd(1n+pp, a, b))

def rc_sub source · line 32 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> @+oy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+cy:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), b) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sub(x, y)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fsub(1n+pp, a, b))

def r_sub 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} -> @+x:List<&2, U32> -> @+y:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> @+oy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+cy:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), b) -> R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sub(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fsub(1n+pp, a, b))

def rc_mul source · line 45 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> @+oy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+cy:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), b) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.mul(x, y)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fmul(1n+pp, a, b))

def r_mul source · line 49 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> @+oy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, y, 255n) == True{} : Bool} -> @+cy:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(y), b) -> R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.mul(x, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fmul(1n+pp, a, b))

def rc_sq source · line 52 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sq(x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fmul(1n+pp, a, a))

def r_sq source · line 55 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sq(x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fmul(1n+pp, a, a))

def rc_inv source · line 58 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.inv(x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.finv(1n+pp, a))

def r_inv source · line 64 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.inv(x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.finv(1n+pp, a))

def rc_p58 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_p58(x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fpow(1n+pp, a, Nat.div(Nat.sub(1n+pp, 5n), 8n)))

def r_p58 source · line 73 · 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 -> @+ox:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+cx:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> R(pp, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_p58(x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.fpow(1n+pp, a, Nat.div(Nat.sub(1n+pp, 5n), 8n)))

def r_o source · line 76 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+a:Nat -> @+r:R(pp, x, a) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool}

def r_c source · line 81 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+a:Nat -> @+r:R(pp, x, a) -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a)

def mkR source · line 86 · raw

@+pp:Nat -> @+x:List<&2, U32> -> @+a:Nat -> @+o:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+c:0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), a) -> R(pp, x, a)