Canon.sum_v: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as Canon Lines 109-125 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&start_line=109&end_line=125 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/nat.bend as N 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 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 import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD def sum_v(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +acc: U32, +e: {LM.okb(n, xs, 255n) == True{} : Bool}, +ha: {Nat.is_lt(Nat.add(v(acc), PL.cbn(n, WD.sc(8n, one))), WD.sc(32n, one)) == True{} : Bool}) -> {v(F.sum_all(xs, acc)) == Nat.add(v(acc), sumv(xs)) : Nat}: match n xs: case 0n Nil{}: Equal.sym(Nat, Nat.add(v(acc), 0n), v(acc), N.add_zero(v(acc))) case 0n Con{y, yt}: Empty.absurd({v(F.sum_all(Con{y, yt}, acc)) == Nat.add(v(acc), sumv(Con{y, yt})) : Nat}, L.false_true(e)) case 1n+m Nil{}: Empty.absurd({v(acc) == Nat.add(v(acc), 0n) : Nat}, L.false_true(e)) case 1n+ +m Con{+y, +yt}: +hy = N.le_trans(v(y), 255n, WD.sc(8n, one), LM.okb_head(m, y, yt, 255n, e), FD.le255(one, h1, 0n)) +b1 = N.le_lt_trans(Nat.add(v(acc), v(y)), Nat.add(v(acc), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one)))), WD.sc(32n, one), N.le_add_left(v(y), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))), v(acc), N.le_trans(v(y), WD.sc(8n, one), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))), hy, N.le_add_right(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))))), ha) +ea = LM.add_v(one, h1, acc, y, b1) +b2a = M.le_add_r(Nat.add(v(acc), v(y)), Nat.add(v(acc), WD.sc(8n, one)), PL.cbn(m, WD.sc(8n, one)), N.le_add_left(v(y), WD.sc(8n, one), v(acc), hy)) +b2b = L.subst(Nat, z => {Nat.is_le(Nat.add(Nat.add(v(acc), v(y)), PL.cbn(m, WD.sc(8n, one))), z) == True{} : Bool}, Nat.add(Nat.add(v(acc), WD.sc(8n, one)), PL.cbn(m, WD.sc(8n, one))), Nat.add(v(acc), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one)))), NA.add_assoc(v(acc), WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one))), b2a) +b2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(z, PL.cbn(m, WD.sc(8n, one))), WD.sc(32n, one)) == True{} : Bool}, Nat.add(v(acc), v(y)), v(U32.add(acc, y)), Equal.sym(Nat, v(U32.add(acc, y)), Nat.add(v(acc), v(y)), ea), N.le_lt_trans(Nat.add(Nat.add(v(acc), v(y)), PL.cbn(m, WD.sc(8n, one))), Nat.add(v(acc), Nat.add(WD.sc(8n, one), PL.cbn(m, WD.sc(8n, one)))), WD.sc(32n, one), b2b, ha)) +ih = sum_v(one, h1, m, yt, U32.add(acc, y), LM.okb_tail(m, y, yt, 255n, e), b2) Equal.trans(Nat, v(F.sum_all(yt, U32.add(acc, y))), Nat.add(v(U32.add(acc, y)), sumv(yt)), Nat.add(v(acc), Nat.add(v(y), sumv(yt))), ih, Equal.trans(Nat, Nat.add(v(U32.add(acc, y)), sumv(yt)), Nat.add(Nat.add(v(acc), v(y)), sumv(yt)), Nat.add(v(acc), Nat.add(v(y), sumv(yt))), M.cong_l(v(U32.add(acc, y)), Nat.add(v(acc), v(y)), sumv(yt), ea), NA.add_assoc(v(acc), v(y), sumv(yt)))) Uses (31): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd 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=Nat.is_lt 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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=sumv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend&name=le255 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=add_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb_head https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb_tail 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=le_add_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=cbn 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/logic.bend&name=false_true https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_left https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans 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/src/crypto/curve25519/field.bend&name=sum_all