def carry_cb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:281

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

281# the carry out is at most 2^21
282def carry_cb(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +c: U32, +hx: {lea(xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {Nat.is_le(v(cc(F.carry(xs, c))), WD.sc(21n, one)) == True{} : Bool}:
283  match xs:
284    case Nil{}:
285      hc
286    case Con{+h, +t}:
287      +hh = lea_head(h, t, WD.sc(28n, one), hx)
288      +ht = lea_tail(h, t, WD.sc(28n, one), hx)
289      +s = U32.add(h, c)
290      +lo = U32.mod(s, 256)
291      +r = F.carry(t, U32.div(s, 256))
292      %Equal.sym(U32, cc(F.carry_con(lo, r)), cc(r), cc_con(lo, r)) : {Nat.is_le(v(_), WD.sc(21n, one)) == True{} : Bool}
293      carry_cb(one, h1, t, U32.div(s, 256), ht, c_next(one, h1, h, c, hh, hc))