def carry

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

import Base

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