~/bend-docscommunity

proofs/crypto/curve25519/canon.bend checks

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

22 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/arith.bend as AR
import ../../lib/u32.bend as U
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/u64/u64div.bend as PD
import ./num.bend as M
import ./limbs.bend as LM
import ./poly.bend as PL
import ./fold.bend as FD
import ./reduce.bend as RD
import ./consts.bend as K
import ./fieldops.bend as FO
import ./cong.bend as G
import ./freeze.bend as FZ
import ./mulw.bend as MW

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def by_okb 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> -> @+cp:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 128n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat} -> @+b:Bool -> @+hb:{Nat.is_lt(v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(x, cp), 0))), one) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/freeze.csg(x, cp), 255n) == True{} : Bool}

def by_ceq 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} -> @+x:List<&2, U32> -> @+cp:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 128n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat} -> @+b:Bool -> @+hb:{Nat.is_lt(v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(x, cp), 0))), one) == b : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/freeze.csg(x, cp)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x))

def by_lt source · line 54 · 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> -> @+cp:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, cp, 128n) == True{} : Bool} -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat} -> @+bB:Nat -> @+q:Nat -> @+hxB:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), Nat.add(1n+pp, bB)) == True{} : Bool} -> @+hPQ:{Nat.is_le(1n+pp, q) == True{} : Bool} -> @+hBQ:{Nat.is_le(bB, q) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_lt(v(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.addl(x, cp), 0))), one) == b : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/freeze.csg(x, cp)), q) == True{} : Bool}

def cs_c source · line 67 · raw

@+one:Nat -> @+x:List<&2, U32> -> @+cp:List<&2, U32> -> Nat

def csub_okb source · line 72 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.csub(x), 255n) == True{} : Bool}

def csub_ceq source · line 75 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.csub(x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x))

def csub_lt 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} -> @+x:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+bB:Nat -> @+q:Nat -> @+hxB:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), Nat.add(1n+pp, bB)) == True{} : Bool} -> @+hPQ:{Nat.is_le(1n+pp, q) == True{} : Bool} -> @+hBQ:{Nat.is_le(bB, q) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.csub(x)), q) == True{} : Bool}

def freeze_okb source · line 81 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.freeze(x), 255n) == True{} : Bool}

def freeze_ceq source · line 84 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.freeze(x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x))

def freeze_lt source · line 87 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.freeze(x)), 1n+pp) == True{} : Bool}

def freeze_val source · line 95 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.freeze(x)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), 1n+pp) : Nat}

value(freeze(x)) == value(x) mod p

def sumv source · line 102 · raw

@xs:List<&2, U32> -> Nat

def sum_v source · line 109 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+acc:U32 -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, xs, 255n) == True{} : Bool} -> @+ha:{Nat.is_lt(Nat.add(v(acc), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cbn(n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sum_all(xs, acc)) == Nat.add(v(acc), sumv(xs)) : Nat}

def iz_add source · line 127 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}

def iz_dbl source · line 134 · raw

@+x:Nat -> {Nat.is_eq(Nat.double(x), 0n) == Nat.is_eq(x, 0n) : Bool}

def iz_sc source · line 141 · raw

@+k:Nat -> @+x:Nat -> {Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x), 0n) == Nat.is_eq(x, 0n) : Bool}

def iz_sum source · line 148 · raw

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

def u32_iz source · line 158 · raw

@+a:U32 -> {U32.is_eq(a, 0) == Nat.is_eq(v(a), 0n) : Bool}

def cb32_lt source · line 161 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(Nat.add(v(0), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.cbn(32n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(8n, one))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool}

def is_zero_val source · line 165 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.is_zero(x) == Nat.is_eq(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), 1n+pp), 0n) : Bool}

def and1 source · line 176 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> {v(U32.and(l, 1)) == Nat.mod(v(l), 2n) : Nat}

def low_bit_val source · line 185 · raw

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

the value mod 2 is the low limb mod 2

def parity_val source · line 196 · 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> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.parity(x)) == Nat.mod(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), 1n+pp), 2n) : Nat}