Fieldops.subl_val: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as Fieldops Lines 77-104 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&start_line=77&end_line=104 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/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/crypto/curve25519/num.bend as M import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM def subl_val(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +ks: List<&2, U32>, +bx: Nat, +by: Nat, +bk: Nat, +hx: {LM.okb(n, xs, bx) == True{} : Bool}, +hy: {LM.okb(n, ys, by) == True{} : Bool}, +hk: {LM.okb(n, ks, bk) == True{} : Bool}, +hg: {gea(ks, by) == True{} : Bool}, +hb: {Nat.is_lt(Nat.add(bx, bk), WD.sc(32n, one)) == True{} : Bool}) -> {Nat.add(FS.value(F.subl(xs, ys, ks)), FS.value(ys)) == Nat.add(FS.value(xs), FS.value(ks)) : Nat}: match n xs ys ks: case 0n Nil{} Nil{} Nil{}: {==} case 0n Nil{} Nil{} Con{k, kt}: Empty.absurd({Nat.add(0n, 0n) == Nat.add(0n, FS.value(Con{k, kt})) : Nat}, L.false_true(hk)) case 0n Nil{} Con{y, yt} _: Empty.absurd({Nat.add(0n, FS.value(Con{y, yt})) == Nat.add(0n, FS.value(ks)) : Nat}, L.false_true(hy)) case 0n Con{x, xt} _ _: Empty.absurd({Nat.add(FS.value(F.subl(Con{x, xt}, ys, ks)), FS.value(ys)) == Nat.add(FS.value(Con{x, xt}), FS.value(ks)) : Nat}, L.false_true(hx)) case 1n+m Nil{} _ _: Empty.absurd({Nat.add(0n, FS.value(ys)) == Nat.add(0n, FS.value(ks)) : Nat}, L.false_true(hx)) case 1n+m Con{x, xt} Nil{} _: Empty.absurd({Nat.add(0n, 0n) == Nat.add(FS.value(Con{x, xt}), FS.value(ks)) : Nat}, L.false_true(hy)) case 1n+m Con{x, xt} Con{y, yt} Nil{}: Empty.absurd({Nat.add(0n, FS.value(Con{y, yt})) == Nat.add(FS.value(Con{x, xt}), 0n) : Nat}, L.false_true(hk)) case 1n+ +m Con{+x, +xt} Con{+y, +yt} Con{+k, +kt}: +s = U32.sub(U32.add(x, k), y) +S = FS.value(F.subl(xt, yt, kt)) +Y = FS.value(yt) +X = FS.value(xt) +KK = FS.value(kt) +el = subl_v(one, h1, x, y, k, bx, by, bk, LM.okb_head(m, x, xt, bx, hx), LM.okb_head(m, y, yt, by, hy), LM.okb_head(m, k, kt, bk, hk), gea_head(k, kt, by, hg), hb) +ih = subl_val(one, h1, m, xt, yt, kt, bx, by, bk, LM.okb_tail(m, x, xt, bx, hx), LM.okb_tail(m, y, yt, by, hy), LM.okb_tail(m, k, kt, bk, hk), gea_tail(k, kt, by, hg), hb) +e1 = M.add4(v(s), C.shift(8n, S), v(y), C.shift(8n, Y)) +e2 = M.cong_add(Nat.add(v(s), v(y)), Nat.add(v(x), v(k)), Nat.add(C.shift(8n, S), C.shift(8n, Y)), C.shift(8n, Nat.add(X, KK)), el, Equal.trans(Nat, Nat.add(C.shift(8n, S), C.shift(8n, Y)), C.shift(8n, Nat.add(S, Y)), C.shift(8n, Nat.add(X, KK)), M.sc_add(8n, S, Y), M.cong_sc(8n, Nat.add(S, Y), Nat.add(X, KK), ih))) +e3 = Equal.trans(Nat, Nat.add(Nat.add(v(x), v(k)), C.shift(8n, Nat.add(X, KK))), Nat.add(Nat.add(v(x), v(k)), Nat.add(C.shift(8n, X), C.shift(8n, KK))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(k), C.shift(8n, KK))), M.cong_r(Nat.add(v(x), v(k)), C.shift(8n, Nat.add(X, KK)), Nat.add(C.shift(8n, X), C.shift(8n, KK)), Equal.sym(Nat, Nat.add(C.shift(8n, X), C.shift(8n, KK)), C.shift(8n, Nat.add(X, KK)), M.sc_add(8n, X, KK))), M.add4(v(x), v(k), C.shift(8n, X), C.shift(8n, KK))) Equal.trans(Nat, Nat.add(Nat.add(v(s), C.shift(8n, S)), Nat.add(v(y), C.shift(8n, Y))), Nat.add(Nat.add(v(s), v(y)), Nat.add(C.shift(8n, S), C.shift(8n, Y))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(k), C.shift(8n, KK))), e1, Equal.trans(Nat, Nat.add(Nat.add(v(s), v(y)), Nat.add(C.shift(8n, S), C.shift(8n, Y))), Nat.add(Nat.add(v(x), v(k)), C.shift(8n, Nat.add(X, KK))), Nat.add(Nat.add(v(x), C.shift(8n, X)), Nat.add(v(k), C.shift(8n, KK))), e2, e3)) Uses (29): 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_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=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=gea https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=gea_head https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=gea_tail https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=subl_v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=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=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=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/logic.bend&name=false_true 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=subl