~/bend-docscommunity

proofs/crypto/curve25519/xbits.bend checks

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

21 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 ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/curve25519/x25519.bend as X
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/u32div.bend as UD
import ../../lib/lemmas/spec/numeric.bend as SN
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WI
import ../../math/typed/shrn.bend as SR
import ../../math/hash/hash.bend as HH
import ./num.bend as M
import ./limbs.bend as LM
import ./canon.bend as CN

Definitions

def v source · line 27 · raw

@+x:U32 -> Nat

def high_zero source · line 32 · raw

@+t:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(t, 0n) == 0n : Nat}

def low_bit source · line 40 · raw

@+t:Nat -> @+b:U32 -> @+w:Nat -> {v(U32.and(U32.shrn(b, t), 1)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.bit(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(t, Nat.add(v(b), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(t, Nat.double(w))))) : Nat}

bit t (t < 8) of b + 2^8 V is bit t of b

def kbit_val source · line 49 · raw

@+bs:List<&2, U32> -> @+t:Nat -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.kbit(bs, t)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.kbit(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs), t) : Nat}

X.kbit(bs, t) is bit t of the value of the bytes

def kbit_le source · line 77 · raw

@+bs:List<&2, U32> -> @+t:Nat -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.lea(bs, 255n) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.kbit(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(bs), t), 1n) == True{} : Bool}

def clamp_top_eq source · line 82 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.clamp_top(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.clamp_last(xs) : List<&2, U32>}

def clamp_eq source · line 93 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.clamp(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.clamp(bs) : List<&2, U32>}

def len_eq source · line 100 · raw

@+bs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.len(bs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.length(U32, bs) : Nat}

def nbits_eq source · line 107 · raw

@+k:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.nbits(k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.bits(k) : Nat}

def bit_or_le source · line 111 · raw

@+a:Bool -> @+b:Bool -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(Bool.or(a, b)), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(a), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b))) == True{} : Bool}

or never exceeds the sum

def or_le source · line 122 · raw

@+n:Nat -> @+x:Word(n) -> @+m:Word(n) -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(n, Word.or(n, x, m)), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(n, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.uw(n, m))) == True{} : Bool}

def or_le32 source · line 134 · raw

@+x:U32 -> @+m:U32 -> {Nat.is_le(v(U32.or(x, m)), Nat.add(v(x), v(m))) == True{} : Bool}

def clamp_top_okb source · line 142 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(1n+n, xs, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(1n+n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.clamp_top(xs), 255n) == True{} : Bool}

def clamp_okb source · line 158 · raw

@+k:List<&2, U32> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, k, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.clamp(k), 255n) == True{} : Bool}

def u0 source · line 168 · raw

@+a:U32 -> @+e:{v(a) == 0n : Nat} -> {a == 0 : U32}

def u1 source · line 171 · raw

@+a:U32 -> @+e:{v(a) == 1n : Nat} -> {a == 1 : U32}

def xor_bits source · line 175 · raw

@+a:U32 -> @+b:U32 -> @+na:Nat -> @+nb:Nat -> @+ea:{v(a) == na : Nat} -> @+eb:{v(b) == nb : Nat} -> @+ha:{Nat.is_le(na, 1n) == True{} : Bool} -> @+hb:{Nat.is_le(nb, 1n) == True{} : Bool} -> {v(U32.xor(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.bxor(na, nb) : Nat}

swap ^= k_t on bits

def bxor_le source · line 198 · raw

@+a:Nat -> @+b:Nat -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.bxor(a, b), 1n) == True{} : Bool}

def byte_rt source · line 207 · raw

@+y:U32 -> @+hy:{Nat.is_le(v(y), 255n) == True{} : Bool} -> {U32.from_nat(v(y)) == y : U32}

def bytes_le source · line 211 · raw

@+n:Nat -> @+ys:List<&2, U32> -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(n, ys, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.le_bytes(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(ys)) == ys : List<&2, U32>}

n tight bytes are the little-endian encoding of their value

def mask_eq source · line 233 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.mask_top(xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.mask_last(xs) : List<&2, U32>}

def mask_okb source · line 244 · raw

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