def subl_val

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fieldops.bend:77

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

77def 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}:
78  match n xs ys ks:
79    case 0n Nil{} Nil{} Nil{}:
80      {==}
81    case 0n Nil{} Nil{} Con{k, kt}:
82      Empty.absurd({Nat.add(0n, 0n) == Nat.add(0n, FS.value(Con{k, kt})) : Nat}, L.false_true(hk))
83    case 0n Nil{} Con{y, yt} _:
84      Empty.absurd({Nat.add(0n, FS.value(Con{y, yt})) == Nat.add(0n, FS.value(ks)) : Nat}, L.false_true(hy))
85    case 0n Con{x, xt} _ _:
86      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))
87    case 1n+m Nil{} _ _:
88      Empty.absurd({Nat.add(0n, FS.value(ys)) == Nat.add(0n, FS.value(ks)) : Nat}, L.false_true(hx))
89    case 1n+m Con{x, xt} Nil{} _:
90      Empty.absurd({Nat.add(0n, 0n) == Nat.add(FS.value(Con{x, xt}), FS.value(ks)) : Nat}, L.false_true(hy))
91    case 1n+m Con{x, xt} Con{y, yt} Nil{}:
92      Empty.absurd({Nat.add(0n, FS.value(Con{y, yt})) == Nat.add(FS.value(Con{x, xt}), 0n) : Nat}, L.false_true(hk))
93    case 1n+ +m Con{+x, +xt} Con{+y, +yt} Con{+k, +kt}:
94      +s = U32.sub(U32.add(x, k), y)
95      +S = FS.value(F.subl(xt, yt, kt))
96      +Y = FS.value(yt)
97      +X = FS.value(xt)
98      +KK = FS.value(kt)
99      +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)
100      +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)
101      +e1 = M.add4(v(s), C.shift(8n, S), v(y), C.shift(8n, Y))
102      +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)))
103      +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)))
104      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))