spec/crypto/curve25519/field.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as Field

3 imports

import Base
import ../../lib/common.bend as C
import ../../../src/crypto/curve25519/field.bend as F

Definitions

def value source · line 34 · raw

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

decodeLittleEndian (RFC 7748 section 5): sum of b_i 2^(8 i)

def bytes_ok source · line 42 · raw

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

n values, each below 2^8

def tight source · line 57 · raw

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

def digits source · line 63 · raw

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

a constant from its little-endian base-256 digits, each scaled by the symbolic one (so the checker never unfolds it): digits(one, [65n, 219n, 1n]) is 121665 for one == 1

def uvalue source · line 72 · raw

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

a constant from its little-endian bytes (U32 values), each scaled by the symbolic one: uvalue(one, bs) is value(bs) for one == 1

def prime source · line 80 · raw

@+one:Nat -> Nat

p = 2^255 - 19

def fadd source · line 84 · raw

@+p:Nat -> @a:Nat -> @b:Nat -> Nat

arithmetic mod p (every result reduced)

def fsub source · line 87 · raw

@+p:Nat -> @a:Nat -> @b:Nat -> Nat

def fmul source · line 90 · raw

@+p:Nat -> @a:Nat -> @b:Nat -> Nat

def fpow source · line 93 · raw

@+p:Nat -> @a:Nat -> @e:Nat -> Nat

def finv source · line 97 · raw

@+p:Nat -> @a:Nat -> Nat

a^(p - 2): the inverse of a nonzero a (Fermat), 0 for 0 (RFC 7748 section 5)

def Add.value source · line 102 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Add.tight source · line 105 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Sub.value source · line 108 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Sub.tight source · line 111 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Mul.value source · line 114 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Mul.tight source · line 117 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Sq.value source · line 120 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def Sq.tight source · line 123 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def MulSmall.value source · line 127 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+k:U32 -> @+ha:{tight(a) == True{} : Bool} -> @+hk:{Nat.is_lt(U32.to_nat(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(17n, one)) == True{} : Bool} -> Type

k below 2^17

def MulSmall.tight source · line 130 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+k:U32 -> @+ha:{tight(a) == True{} : Bool} -> @+hk:{Nat.is_lt(U32.to_nat(k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(17n, one)) == True{} : Bool} -> Type

def Select.zero source · line 133 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Select.one source · line 136 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def Inv.value source · line 139 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def Inv.tight source · line 142 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def PowP58.value source · line 146 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

a^((p - 5) / 8), RFC 8032 section 5.1.3

def PowP58.tight source · line 149 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def Freeze.value source · line 153 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

the canonical representative, which is the 32-byte encoding

def Freeze.tight source · line 156 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def OfBytes.tight source · line 159 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, U32> -> @+hb:{tight(bs) == True{} : Bool} -> Type

def Eq.value source · line 162 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> @+hb:{tight(b) == True{} : Bool} -> Type

def IsZero.value source · line 165 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type

def Parity.value source · line 168 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+a:List<&2, U32> -> @+ha:{tight(a) == True{} : Bool} -> Type