Adc.adc_ok: 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 22-30 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=22&end_line=30

import Base

def adc_ok(xs: List<&2, U32>, ys: List<&2, U32>, zs: List<&2, U32>, +c: Nat, +co: Nat) -> Bool:
  match xs ys zs:
    case Nil{} Nil{} Nil{}:
      Nat.is_eq(c, co)
    case Con{x, xt} Con{y, yt} Con{z, zt}:
      +s = Nat.add(Nat.add(U32.to_nat(x), U32.to_nat(y)), c)
      Bool.and(Nat.is_eq(Nat.mod(s, 256n), U32.to_nat(z)), adc_ok(xt, yt, zt, Nat.div(s, 256n), co))
    case _ _ _:
      False{}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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.div
  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.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat