Poly.addl_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 110-124 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=110&end_line=124

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/nat.bend as N
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

def addl_val(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +ys: List<&2, U32>, +a: Nat, +b: Nat, +hx: {LM.lea(xs, a) == True{} : Bool}, +hy: {LM.lea(ys, b) == True{} : Bool}, +hab: {Nat.is_lt(Nat.add(a, b), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.addl(xs, ys)) == Nat.add(FS.value(xs), FS.value(ys)) : Nat}:
  match xs ys:
    case Nil{} _:
      {==}
    case Con{+x, +xt} Nil{}:
      Equal.sym(Nat, Nat.add(FS.value(Con{x, xt}), 0n), FS.value(Con{x, xt}), N.add_zero(FS.value(Con{x, xt})))
    case Con{+x, +xt} Con{+y, +yt}:
      +ev = addl_v(one, h1, x, y, a, b, LM.lea_head(x, xt, a, hx), LM.lea_head(y, yt, b, hy), hab)
      +ih = addl_val(one, h1, xt, yt, a, b, LM.lea_tail(x, xt, a, hx), LM.lea_tail(y, yt, b, hy), hab)
      +X = FS.value(xt)
      +Y = FS.value(yt)
      +e1 = M.cong_add(v(U32.add(x, y)), Nat.add(v(x), v(y)), C.shift(8n, FS.value(F.addl(xt, yt))), C.shift(8n, Nat.add(X, Y)), ev, M.cong_sc(8n, FS.value(F.addl(xt, yt)), Nat.add(X, Y), ih))
      +e2 = M.cong_r(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y)), Nat.add(C.shift(8n, X), C.shift(8n, Y)), Equal.sym(Nat, Nat.add(C.shift(8n, X), C.shift(8n, Y)), C.shift(8n, Nat.add(X, Y)), M.sc_add(8n, X, Y)))
      Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(8n, FS.value(F.addl(xt, yt)))), Nat.add(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(y), C.shift(8n, Y))), e1,
        Equal.trans(Nat, Nat.add(Nat.add(v(x), v(y)), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(v(x), v(y)), Nat.add(C.shift(8n, X), C.shift(8n, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(y), C.shift(8n, Y))), e2, M.add4(v(x), v(y), C.shift(8n, X), C.shift(8n, Y))))

Uses (24):
  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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  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=add4
  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/num.bend&name=sc_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=addl_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/nat.bend&name=add_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=addl