Limbs.carry_val: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs Lines 232-261 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&start_line=232&end_line=261 import Base import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS 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 import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M # value(limbs) + 2^(8 n) carry_out == value(xs) + carry_in def carry_val(+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.add(FS.value(cl(F.carry(xs, c))), sh(xs, v(cc(F.carry(xs, c))))) == Nat.add(FS.value(xs), v(c)) : Nat}: match xs: case Nil{}: {==} case Con{+h, +t}: +hh = lea_head(h, t, WD.sc(28n, one), hx) +ht = lea_tail(h, t, WD.sc(28n, one), hx) +s = U32.add(h, c) +lo = U32.mod(s, 256) +hi = U32.div(s, 256) +r = F.carry(t, hi) +ih = carry_val(one, h1, t, hi, ht, c_next(one, h1, h, c, hh, hc)) %Equal.sym(List<&2, U32>, cl(F.carry_con(lo, r)), Con{lo, cl(r)}, cl_con(lo, r)) : {Nat.add(FS.value(_), C.shift(8n, sh(t, v(cc(F.carry_con(lo, r)))))) == Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)) : Nat} %Equal.sym(U32, cc(F.carry_con(lo, r)), cc(r), cc_con(lo, r)) : {Nat.add(FS.value(Con{lo, cl(r)}), C.shift(8n, sh(t, v(_)))) == Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)) : Nat} +A = FS.value(cl(r)) +B = sh(t, v(cc(r))) +e1 = Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, A)), C.shift(8n, B)), Nat.add(v(lo), Nat.add(C.shift(8n, A), C.shift(8n, B))), Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), NA.add_assoc(v(lo), C.shift(8n, A), C.shift(8n, B)), M.cong_r(v(lo), Nat.add(C.shift(8n, A), C.shift(8n, B)), C.shift(8n, Nat.add(A, B)), M.sc_add(8n, A, B))) +e2 = M.cong_r(v(lo), C.shift(8n, Nat.add(A, B)), C.shift(8n, Nat.add(FS.value(t), v(hi))), M.cong_sc(8n, Nat.add(A, B), Nat.add(FS.value(t), v(hi)), ih)) +e3 = Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), M.cong_r(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi))), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), Equal.sym(Nat, Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), C.shift(8n, Nat.add(FS.value(t), v(hi))), M.sc_add(8n, FS.value(t), v(hi)))), Equal.trans(Nat, Nat.add(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Nat.add(v(lo), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), M.cong_r(v(lo), Nat.add(C.shift(8n, FS.value(t)), C.shift(8n, v(hi))), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t))), NA.add_comm(C.shift(8n, FS.value(t)), C.shift(8n, v(hi)))), Equal.sym(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(v(lo), Nat.add(C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))), NA.add_assoc(v(lo), C.shift(8n, v(hi)), C.shift(8n, FS.value(t)))))) +e4 = M.cong_l(Nat.add(v(lo), C.shift(8n, v(hi))), v(s), C.shift(8n, FS.value(t)), split_v(s)) +e5 = M.cong_l(v(s), Nat.add(v(h), v(c)), C.shift(8n, FS.value(t)), s_v(one, h1, h, c, hh, hc)) +e6 = Equal.trans(Nat, Nat.add(Nat.add(v(h), v(c)), C.shift(8n, FS.value(t))), Nat.add(v(h), Nat.add(v(c), C.shift(8n, FS.value(t)))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), NA.add_assoc(v(h), v(c), C.shift(8n, FS.value(t))), Equal.trans(Nat, Nat.add(v(h), Nat.add(v(c), C.shift(8n, FS.value(t)))), Nat.add(v(h), Nat.add(C.shift(8n, FS.value(t)), v(c))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), M.cong_r(v(h), Nat.add(v(c), C.shift(8n, FS.value(t))), Nat.add(C.shift(8n, FS.value(t)), v(c)), NA.add_comm(v(c), C.shift(8n, FS.value(t)))), Equal.sym(Nat, Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), Nat.add(v(h), Nat.add(C.shift(8n, FS.value(t)), v(c))), NA.add_assoc(v(h), C.shift(8n, FS.value(t)), v(c))))) Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, A)), C.shift(8n, B)), Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e1, Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(A, B))), Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e2, Equal.trans(Nat, Nat.add(v(lo), C.shift(8n, Nat.add(FS.value(t), v(hi)))), Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e3, Equal.trans(Nat, Nat.add(Nat.add(v(lo), C.shift(8n, v(hi))), C.shift(8n, FS.value(t))), Nat.add(v(s), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e4, Equal.trans(Nat, Nat.add(v(s), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), v(c)), C.shift(8n, FS.value(t))), Nat.add(Nat.add(v(h), C.shift(8n, FS.value(t))), v(c)), e5, e6))))) Uses (34): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans 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=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=c_next https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=cc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=cc_con https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=cl https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=cl_con https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_head https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_tail https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=s_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=sh https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=split_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=carry https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=carry_con