def carry_ok

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

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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

263# every output limb below 2^8, the same count
264def carry_ok(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +c: U32, +hn: {okb(n, xs, WD.sc(28n, one)) == True{} : Bool}, +hc: {Nat.is_le(v(c), WD.sc(21n, one)) == True{} : Bool}) -> {okb(n, cl(F.carry(xs, c)), 255n) == True{} : Bool}:
265  match n xs:
266    case 0n Nil{}:
267      {==}
268    case 0n Con{y, yt}:
269      Empty.absurd({okb(0n, cl(F.carry(Con{y, yt}, c)), 255n) == True{} : Bool}, L.false_true(hn))
270    case 1n+m Nil{}:
271      Empty.absurd({okb(1n+m, cl(F.carry(Nil{}, c)), 255n) == True{} : Bool}, L.false_true(hn))
272    case 1n+ +m Con{+h, +t}:
273      +hh = okb_head(m, h, t, WD.sc(28n, one), hn)
274      +ht = okb_tail(m, h, t, WD.sc(28n, one), hn)
275      +s = U32.add(h, c)
276      +lo = U32.mod(s, 256)
277      +r = F.carry(t, U32.div(s, 256))
278      %Equal.sym(List<&2, U32>, cl(F.carry_con(lo, r)), Con{lo, cl(r)}, cl_con(lo, r)) : {okb(1n+m, _, 255n) == True{} : Bool}
279      L.and_intro(Nat.is_le(v(lo), 255n), okb(m, cl(r), 255n), lo_le(s), carry_ok(one, h1, m, t, U32.div(s, 256), ht, c_next(one, h1, h, c, hh, hc)))