Fieldops.select1: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as Fieldops
Lines 199-214 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&start_line=199&end_line=214

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/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

def select1(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +hx: {LM.okb(n, xs, 255n) == True{} : Bool}, +hy: {LM.okb(n, ys, 255n) == True{} : Bool}) -> {F.select(1, xs, ys) == ys : List<&2, U32>}:
  match n xs ys:
    case 0n Nil{} Nil{}:
      {==}
    case 0n Nil{} Con{y, yt}:
      Empty.absurd({F.select(1, Nil{}, Con{y, yt}) == Con{y, yt} : List<&2, U32>}, L.false_true(hy))
    case 0n Con{x, xt} _:
      Empty.absurd({F.select(1, Con{x, xt}, ys) == ys : List<&2, U32>}, L.false_true(hx))
    case 1n+m Nil{} _:
      Empty.absurd({Nil{} == ys : List<&2, U32>}, L.false_true(hx))
    case 1n+m Con{x, xt} Nil{}:
      {==}
    case 1n+ +m Con{+x, +xt} Con{+y, +yt}:
      +e1 = Equal.trans(U32, U32.add(U32.mul(x, 0), U32.mul(y, 1)), U32.add(0, y), y, Equal.trans(U32, U32.add(U32.mul(x, 0), U32.mul(y, 1)), U32.add(0, U32.mul(y, 1)), U32.add(0, y), Equal.cong(U32, U32, z => U32.add(z, U32.mul(y, 1)), U32.mul(x, 0), 0, mul0(one, h1, x)), Equal.cong(U32, U32, z => U32.add(0, z), U32.mul(y, 1), y, mul1(one, h1, y))), A.zero_add(y))
      +e2 = select1(one, h1, m, xt, yt, LM.okb_tail(m, x, xt, 255n, hx), LM.okb_tail(m, y, yt, 255n, hy))
      Equal.trans(List<&2, U32>, Con{U32.add(U32.mul(x, 0), U32.mul(y, 1)), F.select(1, xt, yt)}, Con{y, F.select(1, xt, yt)}, Con{y, yt}, Equal.cong(U32, List<&2, U32>, z => Con{z, F.select(1, xt, yt)}, U32.add(U32.mul(x, 0), U32.mul(y, 1)), y, e1), Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{y, z}, F.select(1, xt, yt), yt, e2))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  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/fieldops.bend&name=mul0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=mul1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb_tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=zero_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=select