proofs/crypto/ed25519/adc.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as Adc

12 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../curve25519/num.bend as M
import ../curve25519/limbs.bend as LM
import ../curve25519/poly.bend as PL
import ../curve25519/consts.bend as K

Definitions

def v source · line 19 · raw

@+x:U32 -> Nat

def adc_ok source · line 22 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> @zs:List<&2, U32> -> @+c:Nat -> @+co:Nat -> Bool

def digit source · line 33 · raw

@+one:Nat -> @+x:Nat -> @+y:Nat -> @+c:Nat -> @+z:Nat -> @+hz:{Nat.mod(Nat.add(Nat.add(x, y), c), 256n) == z : Nat} -> {Nat.add(Nat.add(Nat.mul(one, x), Nat.mul(one, y)), Nat.mul(one, c)) == Nat.add(Nat.mul(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, Nat.mul(one, Nat.div(Nat.add(Nat.add(x, y), c), 256n)))) : Nat}

one digit: x + y + c == z + 256 c' scaled by one

def swap5 source · line 43 · raw

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

(a + A') + (b + B') + c == (a + b + c) + (A' + B') rearranged

def adc_val source · line 48 · raw

@+one:Nat -> @+xs:List<&2, U32> -> @+ys:List<&2, U32> -> @+zs:List<&2, U32> -> @+c:Nat -> @+co:Nat -> @+h:{adc_ok(xs, ys, zs, c, co) == True{} : Bool} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, xs), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, ys)), Nat.mul(one, c)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, zs), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.sh(xs, Nat.mul(one, co))) : Nat}

def digs_eq source · line 83 · raw

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

a limb list and a digit list agree

def valo_digits source · line 92 · raw

@+one:Nat -> @+xs:List<&2, U32> -> @+ds:List<&2, Nat> -> @+h:{digs_eq(xs, ds) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.digits(one, ds) : Nat}

def valo_u source · line 105 · raw

@+one:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.valo(one, xs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.uvalue(one, xs) : Nat}