Poly.scal_val: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as Poly
Lines 192-204 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&start_line=192&end_line=204

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
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/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
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

def scal_val(+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}) -> {FS.value(F.scal(x, ys)) == Nat.mul(v(x), FS.value(ys)) : Nat}:
  match ys:
    case Nil{}:
      Equal.sym(Nat, Nat.mul(v(x), 0n), 0n, NA.mul_zero(v(x)))
    case Con{+y, +yt}:
      +ev = scal_v(one, h1, x, y, a, b, hx, LM.lea_head(y, yt, b, hy), hab)
      +ih = scal_val(one, h1, x, yt, a, b, hx, LM.lea_tail(y, yt, b, hy), hab)
      +Y = FS.value(yt)
      +e1 = M.cong_add(v(U32.mul(x, y)), Nat.mul(v(x), v(y)), C.shift(8n, FS.value(F.scal(x, yt))), C.shift(8n, Nat.mul(v(x), Y)), ev, M.cong_sc(8n, FS.value(F.scal(x, yt)), Nat.mul(v(x), Y), ih))
      +e2 = M.cong_r(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y)), Nat.mul(v(x), C.shift(8n, Y)), sc_mul_l(8n, v(x), Y))
      +e3 = Equal.sym(Nat, Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), Nat.add(Nat.mul(v(x), v(y)), Nat.mul(v(x), C.shift(8n, Y))), NA.mul_add_left(v(x), v(y), C.shift(8n, Y)))
      Equal.trans(Nat, Nat.add(v(U32.mul(x, y)), C.shift(8n, FS.value(F.scal(x, yt)))), Nat.add(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y))), Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), e1,
        Equal.trans(Nat, Nat.add(Nat.mul(v(x), v(y)), C.shift(8n, Nat.mul(v(x), Y))), Nat.add(Nat.mul(v(x), v(y)), Nat.mul(v(x), C.shift(8n, Y))), Nat.mul(v(x), Nat.add(v(y), C.shift(8n, Y))), e2, e3))

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=sc_mul_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=scal_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=scal