def reduce

bend-collections-laws-crypto@1.0.0.0 · src/crypto/secp256k1/limbs.bend:155

import Base

155# x mod m for x below 2^512, in k folds (x is looked at first, so that the
156# proof checker keeps an unknown reduction folded)
157def reduce(+c: List<&2, Nat>, k: Nat, xs: List<&2, Nat>) -> List<&2, Nat>:
158  match xs:
159    case Nil{}: reduce_go(c, k, Nil{})
160    case x <> t: reduce_go(c, k, x <> t)