~/bend-docscommunity

proofs/crypto/curve25519/limbs.bend checks

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

13 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/u32div.bend as UD
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 ../../math/u64/u64div.bend as PD
import ./num.bend as M

Definitions

def v source · line 22 · raw

@+x:U32 -> Nat

def sh source · line 26 · raw

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

2^(8 len(xs)) x

def shn source · line 34 · raw

@n:Nat -> @+x:Nat -> Nat

2^(8 n) x

def okb source · line 42 · raw

@n:Nat -> @xs:List<&2, U32> -> @+b:Nat -> Bool

exactly n limbs, each at most b

def lea source · line 58 · raw

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

every limb at most b

def cl source · line 65 · raw

@r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.Cr -> List<&2, U32>

def cc source · line 68 · raw

@r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.Cr -> U32

def okb_head source · line 73 · raw

@+n:Nat -> @+h:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+e:{okb(1n+n, h <> t, b) == True{} : Bool} -> {Nat.is_le(v(h), b) == True{} : Bool}

def okb_tail source · line 76 · raw

@+n:Nat -> @+h:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+e:{okb(1n+n, h <> t, b) == True{} : Bool} -> {okb(n, t, b) == True{} : Bool}

def okb_lea source · line 79 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+e:{okb(n, xs, b) == True{} : Bool} -> {lea(xs, b) == True{} : Bool}

def lea_head source · line 90 · raw

@+h:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+e:{lea(h <> t, b) == True{} : Bool} -> {Nat.is_le(v(h), b) == True{} : Bool}

def lea_tail source · line 93 · raw

@+h:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+e:{lea(h <> t, b) == True{} : Bool} -> {lea(t, b) == True{} : Bool}

def lea_mono source · line 97 · raw

@+xs:List<&2, U32> -> @+b:Nat -> @+c:Nat -> @+hb:{Nat.is_le(b, c) == True{} : Bool} -> @+e:{lea(xs, b) == True{} : Bool} -> {lea(xs, c) == True{} : Bool}

a weaker bound

def sh_okb source · line 104 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+x:Nat -> @+e:{okb(n, xs, b) == True{} : Bool} -> {sh(xs, x) == shn(n, x) : Nat}

def bytes_okb source · line 116 · raw

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

the spec's tight (bytes_ok 32: limbs below 256) is okb 32 with bound 255

def okb_bytes source · line 129 · raw

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

def k256 source · line 142 · raw

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

def sc_pos1 source · line 145 · raw

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

def sc_lt_succ source · line 149 · raw

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

2^k < 2^(k+1)

def sc_lt source · line 157 · raw

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

2^a < 2^(d + 1 + a)

def add_v source · line 162 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+h:{Nat.is_lt(Nat.add(v(x), v(y)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}

def mul_v source · line 165 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+h:{Nat.is_lt(Nat.mul(v(x), v(y)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(32n, one)) == True{} : Bool} -> {v(U32.mul(x, y)) == Nat.mul(v(x), v(y)) : Nat}

def mod256 source · line 168 · raw

@+x:U32 -> {v(U32.mod(x, 256)) == Nat.mod(v(x), 256n) : Nat}

def div256 source · line 171 · raw

@+x:U32 -> {v(U32.div(x, 256)) == Nat.div(v(x), 256n) : Nat}

def m256 source · line 174 · raw

@+x:Nat -> {Nat.mul(x, 256n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, x) : Nat}

def dm256 source · line 178 · raw

@+n:Nat -> {Nat.add(Nat.mod(n, 256n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, Nat.div(n, 256n))) == n : Nat}

n == (n mod 256) + 2^8 (n div 256)

def split_v source · line 184 · raw

@+s:U32 -> {Nat.add(v(U32.mod(s, 256)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, v(U32.div(s, 256)))) == v(s) : Nat}

a U32 split into its low byte and the rest

def lo_le source · line 189 · raw

@+s:U32 -> {Nat.is_le(v(U32.mod(s, 256)), 255n) == True{} : Bool}

def hi_lt source · line 194 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+h:{Nat.is_lt(v(s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(Nat.add(k, 8n), one)) == True{} : Bool} -> {Nat.is_lt(v(U32.div(s, 256)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one)) == True{} : Bool}

(s div 256) < 2^k when s < 2^(k + 8)

def cl_con source · line 207 · raw

@+l:U32 -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.Cr -> {cl(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry_con(l, r)) == l <> cl(r) : List<&2, U32>}

def cc_con source · line 212 · raw

@+l:U32 -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.Cr -> {cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry_con(l, r)) == cc(r) : U32}

def s_lt source · line 218 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+c:U32 -> @+hx:{Nat.is_le(v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {Nat.is_lt(Nat.add(v(x), v(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(29n, one)) == True{} : Bool}

carry-in at most 2^21 and a limb at most 2^28: their sum is below 2^29

def s_v source · line 224 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+c:U32 -> @+hx:{Nat.is_le(v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {v(U32.add(x, c)) == Nat.add(v(x), v(c)) : Nat}

def c_next source · line 227 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+c:U32 -> @+hx:{Nat.is_le(v(x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {Nat.is_le(v(U32.div(U32.add(x, c), 256)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool}

def carry_val source · line 233 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+c:U32 -> @+hx:{lea(xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(cl(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, c))), sh(xs, v(cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, c))))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(xs), v(c)) : Nat}

value(limbs) + 2^(8 n) carry_out == value(xs) + carry_in

def carry_ok source · line 264 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+n:Nat -> @+xs:List<&2, U32> -> @+c:U32 -> @+hn:{okb(n, xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {okb(n, cl(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, c)), 255n) == True{} : Bool}

every output limb below 2^8, the same count

def carry_cb source · line 282 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, U32> -> @+c:U32 -> @+hx:{lea(xs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(28n, one)) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool} -> {Nat.is_le(v(cc(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.carry(xs, c))), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(21n, one)) == True{} : Bool}

the carry out is at most 2^21