Adc.valo_digits: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as Adc
Lines 92-103 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend&start_line=92&end_line=103

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/proofs/lib/nat.bend as N
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/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K

def valo_digits(+one: Nat, +xs: List<&2, U32>, +ds: List<&2, Nat>, +h: {digs_eq(xs, ds) == True{} : Bool}) -> {K.valo(one, xs) == FS.digits(one, ds) : Nat}:
  match xs ds:
    case Nil{} Nil{}:
      {==}
    case Con{+x, +xt} Con{+d, +dt}:
      +e1 = N.eq_from_is_eq(v(x), d, L.and_left(Nat.is_eq(v(x), d), digs_eq(xt, dt), h))
      +e2 = valo_digits(one, xt, dt, L.and_right(Nat.is_eq(v(x), d), digs_eq(xt, dt), h))
      M.cong_add(Nat.mul(one, v(x)), Nat.mul(one, d), C.shift(8n, K.valo(one, xt)), C.shift(8n, FS.digits(one, dt)), Equal.cong(Nat, Nat, z => Nat.mul(one, z), v(x), d, e1), M.cong_sc(8n, K.valo(one, xt), FS.digits(one, dt), e2))
    case Nil{} Con{d, dt}:
      Empty.absurd({0n == FS.digits(one, Con{d, dt}) : Nat}, L.false_true(h))
    case Con{x, xt} Nil{}:
      Empty.absurd({K.valo(one, Con{x, xt}) == 0n : Nat}, L.false_true(h))

Uses (19):
  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=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.is_eq
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend&name=valo
  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_sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend&name=digs_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right
  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/nat.bend&name=eq_from_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift