def scal_lea

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/poly.bend:206

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

206def scal_lea(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {Nat.is_le(v(x), a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {LM.lea(F.scal(x, ys), Nat.mul(a, b)) == True{} : Bool}:
207  match ys:
208    case Nil{}:
209      {==}
210    case Con{+y, +yt}:
211      +hyh = LM.lea_head(y, yt, b, hy)
212      +ev = scal_v(one, h1, x, y, a, b, hx, hyh, hab)
213      +hd = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(v(x), v(y)), v(U32.mul(x, y)), Equal.sym(Nat, v(U32.mul(x, y)), Nat.mul(v(x), v(y)), ev), M.le_mul2(v(x), v(y), a, b, hx, hyh))
214      L.and_intro(Nat.is_le(v(U32.mul(x, y)), Nat.mul(a, b)), LM.lea(F.scal(x, yt), Nat.mul(a, b)), hd, scal_lea(one, h1, x, yt, a, b, hx, LM.lea_tail(y, yt, b, hy), hab))