Fold.fold_id: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as Fold
Lines 32-47 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend&start_line=32&end_line=47

import Base
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

# A + 2^256 c == 2 c p + (A + 38 c)
def fold_id(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +a: Nat, +c: Nat) -> {Nat.add(a, LM.shn(32n, c)) == Nat.add(Nat.mul(Nat.add(c, c), 1n+pp), Nat.add(a, Nat.mul(38n, c))) : Nat}:
  +P = {1n+pp : Nat}
  +e1 = Equal.sym(Nat, Nat.mul(c, WD.sc(256n, one)), WD.sc(256n, c), M.mul_sc_r(256n, one, h1, c))
  +e2 = Equal.trans(Nat, WD.sc(256n, one), Nat.add(WD.sc(255n, one), WD.sc(255n, one)), Nat.add(Nat.add(P, 19n), Nat.add(P, 19n)), Equal.sym(Nat, Nat.add(WD.sc(255n, one), WD.sc(255n, one)), WD.sc(256n, one), M.sc_dbl(255n, one)), M.cong_add(WD.sc(255n, one), Nat.add(P, 19n), WD.sc(255n, one), Nat.add(P, 19n), Equal.sym(Nat, Nat.add(P, 19n), WD.sc(255n, one), hP), Equal.sym(Nat, Nat.add(P, 19n), WD.sc(255n, one), hP)))
  +e3 = M.add4(P, 19n, P, 19n)
  +e4 = Equal.trans(Nat, WD.sc(256n, one), Nat.add(Nat.add(P, 19n), Nat.add(P, 19n)), Nat.add(Nat.add(P, P), 38n), e2, e3)
  +e5 = Equal.trans(Nat, Nat.mul(c, WD.sc(256n, one)), Nat.mul(c, Nat.add(Nat.add(P, P), 38n)), Nat.add(Nat.mul(c, Nat.add(P, P)), Nat.mul(c, 38n)), Equal.cong(Nat, Nat, t => Nat.mul(c, t), WD.sc(256n, one), Nat.add(Nat.add(P, P), 38n), e4), NA.mul_add_left(c, Nat.add(P, P), 38n))
  +e6 = Equal.trans(Nat, Nat.mul(c, Nat.add(P, P)), Nat.add(Nat.mul(c, P), Nat.mul(c, P)), Nat.mul(Nat.add(c, c), P), NA.mul_add_left(c, P, P), Equal.sym(Nat, Nat.mul(Nat.add(c, c), P), Nat.add(Nat.mul(c, P), Nat.mul(c, P)), NA.mul_add_right(c, c, P)))
  +e7 = M.cong_add(Nat.mul(c, Nat.add(P, P)), Nat.mul(Nat.add(c, c), P), Nat.mul(c, 38n), Nat.mul(38n, c), e6, NA.mul_comm(c, 38n))
  +q = Nat.mul(Nat.add(c, c), P)
  +r = Nat.mul(38n, c)
  +e8 = Equal.trans(Nat, WD.sc(256n, c), Nat.mul(c, WD.sc(256n, one)), Nat.add(q, r), e1, Equal.trans(Nat, Nat.mul(c, WD.sc(256n, one)), Nat.add(Nat.mul(c, Nat.add(P, P)), Nat.mul(c, 38n)), Nat.add(q, r), e5, e7))
  +e9 = M.cong_r(a, WD.sc(256n, c), Nat.add(q, r), e8)
  +e10 = Equal.trans(Nat, Nat.add(a, Nat.add(q, r)), Nat.add(q, Nat.add(a, r)), Nat.add(q, Nat.add(a, r)), NA.add_swap(a, q, r), {==})
  Equal.trans(Nat, Nat.add(a, WD.sc(256n, c)), Nat.add(a, Nat.add(q, r)), Nat.add(q, Nat.add(a, r)), e9, e10)

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=shn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=add4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_add
  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=mul_sc_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc