~/bend-docscommunity

proofs/crypto/curve25519/pow.bend checks

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

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/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ./num.bend as M
import ./limbs.bend as LM
import ./consts.bend as K
import ./mulw.bend as MW
import ./cong.bend as G

Definitions

def v source · line 23 · raw

@+x:U32 -> Nat

def Fo source · line 27 · raw

@+one:Nat -> @+n:Nat -> Nat

2^n - 1

def one_le_sc source · line 30 · raw

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

def fo_sum source · line 34 · raw

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

def sub_add_r source · line 38 · raw

@+a:Nat -> @+c:Nat -> @+b:Nat -> @+h:{Nat.is_le(b, c) == True{} : Bool} -> {Nat.sub(Nat.add(a, c), b) == Nat.add(a, Nat.sub(c, b)) : Nat}

(a + c) - b == a + (c - b) for b <= c

def fo_step source · line 45 · raw

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

2^m + (2^m - 1) == 2^(m+1) - 1

def bexp source · line 50 · raw

@b:Bool -> Nat

def blen source · line 57 · raw

@bs:List<&2, Bool> -> Nat

def eb source · line 65 · raw

@+one:Nat -> @bs:List<&2, Bool> -> Nat

the exponent of x contributed by the bits

def po_zero source · line 74 · raw

@+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_ones(x, 0n, acc) == acc : List<&2, U32>}

def po_step source · line 81 · raw

@+x:List<&2, U32> -> @+m:Nat -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_ones(x, 1n+m, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_ones(x, m, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sq(acc), x)) : List<&2, U32>}

def pbs_nil source · line 88 · raw

@+x:List<&2, U32> -> @+acc:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bits(x, [], acc) == acc : List<&2, U32>}

def pbs_con source · line 95 · raw

@+x:List<&2, U32> -> @+b:Bool -> @+bt:List<&2, Bool> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bits(x, b <> bt, acc) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bits(x, bt, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bit(b, x, acc)) : List<&2, U32>}

def po_okb source · line 104 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_ones(x, n, acc), 255n) == True{} : Bool}

def pb_okb source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+b:Bool -> @+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bit(b, x, acc), 255n) == True{} : Bool}

def pbs_okb source · line 120 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, Bool> -> @+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bits(x, bs, acc), 255n) == True{} : Bool}

def step_c source · line 132 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+acc:List<&2, U32> -> @+x:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> @+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.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.sq(acc), x)), Nat.mul(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x)))

acc^2 x

def pow_one_one source · line 140 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:Nat -> {Nat.mul(Nat.pow(a, one), 1n) == a : Nat}

a^one * 1 == a

def sq_pow source · line 145 · raw

@+a:Nat -> @+y:Nat -> @+s:Nat -> @+z:Nat -> @+s2:Nat -> @+hs:{Nat.add(s, s) == s2 : Nat} -> {Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), y), s), z) == Nat.mul(Nat.pow(a, s2), Nat.mul(Nat.pow(y, s), z)) : Nat}

(a^2 y)^(2^m) z == a^(2^(m+1)) (y^(2^m) z)

def po_val source · line 152 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+n:Nat -> @+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_ones(x, n, acc)), Nat.mul(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(n, one)), Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), Fo(one, n))))

def pb_val source · line 176 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+b:Bool -> @+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bit(b, x, acc)), Nat.mul(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc)), Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), bexp(b))))

def bit_pow source · line 187 · raw

@+a:Nat -> @+x:Nat -> @+e:Nat -> @+s:Nat -> @+z:Nat -> @+s2:Nat -> @+hs:{Nat.add(s, s) == s2 : Nat} -> {Nat.mul(Nat.pow(Nat.mul(Nat.mul(a, a), Nat.pow(x, e)), s), Nat.pow(x, z)) == Nat.mul(Nat.pow(a, s2), Nat.pow(x, Nat.add(Nat.mul(e, s), z))) : Nat}

(a^2 x^e)^s y == a^(2 s) x^(e s) y

def pbs_val source · line 193 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+bs:List<&2, Bool> -> @+x:List<&2, U32> -> @+acc:List<&2, U32> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, x, 255n) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, acc, 255n) == True{} : Bool} -> 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.ceq(pp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_bits(x, bs, acc)), Nat.mul(Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(acc), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(blen(bs), one)), Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), eb(one, bs))))

def chain_val source · line 215 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+n:Nat -> @+bs:List<&2, Bool> -> @+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.pow_bits(x, bs, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.pow_ones(x, n, x))), Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), Nat.add(Nat.mul(Fo(one, 1n+n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(blen(bs), one)), eb(one, bs))))

pow_bits(x, bs, pow_ones(x, n, x)) == x^(Fo(n + 1) 2^len + eb)

def cancel_r source · line 231 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e:{Nat.add(a, c) == Nat.add(b, c) : Nat} -> {a == b : Nat}

def f32 source · line 235 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> {Nat.add(Nat.mul(Fo(one, 250n), 32n), 32n) == Nat.add(1n+pp, 19n) : Nat}

32 Fo(250) + 32 == p + 19

def small_one source · line 242 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+a:Nat -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, 1n) == a : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one) == a : Nat}

def inv_bits source · line 245 · raw

List<&2, Bool>

def p58_bits source · line 248 · raw

List<&2, Bool>

def eb_inv source · line 251 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {eb(one, inv_bits) == 11n : Nat}

def eb_p58 source · line 254 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {eb(one, p58_bits) == 1n : Nat}

def inv_exp source · line 258 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> {Nat.add(Nat.mul(Fo(one, 250n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(blen(inv_bits), one)), eb(one, inv_bits)) == Nat.sub(1n+pp, 2n) : Nat}

32 Fo(250) + 11 == p - 2

def p58_exp source · line 271 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> {Nat.add(Nat.mul(Fo(one, 250n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(blen(p58_bits), one)), eb(one, p58_bits)) == Nat.div(Nat.sub(1n+pp, 5n), 8n) : Nat}

4 Fo(250) + 1 == (p - 5) / 8

def inv_okb source · line 289 · raw

@+one:Nat -> @+h1:{one == 1n : 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.inv(x), 255n) == True{} : Bool}

def p58_okb source · line 292 · raw

@+one:Nat -> @+h1:{one == 1n : 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.pow_p58(x), 255n) == True{} : Bool}

def inv_val source · line 295 · 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.inv(x)), Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), Nat.sub(1n+pp, 2n)))

def p58_val source · line 299 · 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.pow_p58(x)), Nat.pow(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(x), Nat.div(Nat.sub(1n+pp, 5n), 8n)))