Limbs.carry: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend as Limbs
Lines 96-110 of bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend&start_line=96&end_line=110

import Base

# A carry pass: n limbs, each below 2^16, then one limb holding the carry u
# out of them plus the value of whatever is left of xs past n limbs (on
# every call below xs has at most n limbs, so that is the carry alone).
# Every function here looks at its list before producing anything, so that
# on a symbolic argument the proof checker stops at once.
def carry(n: Nat, xs: List<&2, Nat>, u: Nat) -> List<&2, Nat>:
  match n xs:
    case 0n Nil{}: [u]
    case 0n x <> t: [Nat.add(u, horner(x <> t))]
    case 1n+k Nil{}:
      +s = Nat.add(u, 0n)
      lo16(s) <> carry(k, Nil{}, hi16(s))
    case 1n+k x <> t:
      +s = Nat.add(u, x)
      lo16(s) <> carry(k, t, hi16(s))

Uses (6):
  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=bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=hi16
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=horner
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=lo16