def adc_val

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/adc.bend:48

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/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/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/consts.bend as K

48def adc_val(+one: Nat, +xs: List<&2, U32>, +ys: List<&2, U32>, +zs: List<&2, U32>, +c: Nat, +co: Nat, +h: {adc_ok(xs, ys, zs, c, co) == True{} : Bool}) -> {Nat.add(Nat.add(K.valo(one, xs), K.valo(one, ys)), Nat.mul(one, c)) == Nat.add(K.valo(one, zs), LM.sh(xs, Nat.mul(one, co))) : Nat}:
49  match xs ys zs:
50    case Nil{} Nil{} Nil{}:
51      %N.eq_from_is_eq(c, co, h) : {Nat.add(Nat.add(0n, 0n), Nat.mul(one, c)) == Nat.add(0n, Nat.mul(one, _)) : Nat}
52      {==}
53    case Con{+x, +xt} Con{+y, +yt} Con{+z, +zt}:
54      +s = Nat.add(Nat.add(v(x), v(y)), c)
55      +q = Nat.div(s, 256n)
56      +hz = N.eq_from_is_eq(Nat.mod(s, 256n), v(z), L.and_left(Nat.is_eq(Nat.mod(s, 256n), v(z)), adc_ok(xt, yt, zt, q, co), h))
57      +ih = adc_val(one, xt, yt, zt, q, co, L.and_right(Nat.is_eq(Nat.mod(s, 256n), v(z)), adc_ok(xt, yt, zt, q, co), h))
58      +X = K.valo(one, xt)
59      +Y = K.valo(one, yt)
60      +Z = K.valo(one, zt)
61      +a = Nat.mul(one, v(x))
62      +b = Nat.mul(one, v(y))
63      +cc = Nat.mul(one, c)
64      +e1 = swap5(a, b, cc, C.shift(8n, X), C.shift(8n, Y))
65      +e2 = M.cong_add(Nat.add(Nat.add(a, b), cc), Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.mul(one, q))), Nat.add(C.shift(8n, X), C.shift(8n, Y)), C.shift(8n, Nat.add(X, Y)), digit(one, v(x), v(y), c, v(z), hz), M.sc_add(8n, X, Y))
66      +e3 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.mul(one, q))), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.mul(one, v(z)), Nat.add(C.shift(8n, Nat.mul(one, q)), C.shift(8n, Nat.add(X, Y)))), Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q)))), NA.add_assoc(Nat.mul(one, v(z)), C.shift(8n, Nat.mul(one, q)), C.shift(8n, Nat.add(X, Y))), M.cong_r(Nat.mul(one, v(z)), Nat.add(C.shift(8n, Nat.mul(one, q)), C.shift(8n, Nat.add(X, Y))), C.shift(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q))), Equal.trans(Nat, Nat.add(C.shift(8n, Nat.mul(one, q)), C.shift(8n, Nat.add(X, Y))), C.shift(8n, Nat.add(Nat.mul(one, q), Nat.add(X, Y))), C.shift(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q))), M.sc_add(8n, Nat.mul(one, q), Nat.add(X, Y)), M.cong_sc(8n, Nat.add(Nat.mul(one, q), Nat.add(X, Y)), Nat.add(Nat.add(X, Y), Nat.mul(one, q)), NA.add_comm(Nat.mul(one, q), Nat.add(X, Y))))))
67      +e4 = M.cong_r(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q))), C.shift(8n, Nat.add(Z, LM.sh(xt, Nat.mul(one, co)))), M.cong_sc(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q)), Nat.add(Z, LM.sh(xt, Nat.mul(one, co))), ih))
68      +e5 = Equal.trans(Nat, Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Z, LM.sh(xt, Nat.mul(one, co))))), Nat.add(Nat.mul(one, v(z)), Nat.add(C.shift(8n, Z), C.shift(8n, LM.sh(xt, Nat.mul(one, co))))), Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Z)), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), M.cong_r(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Z, LM.sh(xt, Nat.mul(one, co)))), Nat.add(C.shift(8n, Z), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), Equal.sym(Nat, Nat.add(C.shift(8n, Z), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), C.shift(8n, Nat.add(Z, LM.sh(xt, Nat.mul(one, co)))), M.sc_add(8n, Z, LM.sh(xt, Nat.mul(one, co))))), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Z)), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), Nat.add(Nat.mul(one, v(z)), Nat.add(C.shift(8n, Z), C.shift(8n, LM.sh(xt, Nat.mul(one, co))))), NA.add_assoc(Nat.mul(one, v(z)), C.shift(8n, Z), C.shift(8n, LM.sh(xt, Nat.mul(one, co))))))
69      Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, C.shift(8n, X)), Nat.add(b, C.shift(8n, Y))), cc), Nat.add(Nat.add(Nat.add(a, b), cc), Nat.add(C.shift(8n, X), C.shift(8n, Y))), Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Z)), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), e1,
70        Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, b), cc), Nat.add(C.shift(8n, X), C.shift(8n, Y))), Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.mul(one, q))), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Z)), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), e2,
71          Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.mul(one, q))), C.shift(8n, Nat.add(X, Y))), Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q)))), Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Z)), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), e3,
72            Equal.trans(Nat, Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Nat.add(X, Y), Nat.mul(one, q)))), Nat.add(Nat.mul(one, v(z)), C.shift(8n, Nat.add(Z, LM.sh(xt, Nat.mul(one, co))))), Nat.add(Nat.add(Nat.mul(one, v(z)), C.shift(8n, Z)), C.shift(8n, LM.sh(xt, Nat.mul(one, co)))), e4, e5))))
73    case Nil{} Nil{} Con{z, zt}:
74      Empty.absurd({Nat.add(Nat.add(0n, 0n), Nat.mul(one, c)) == Nat.add(K.valo(one, Con{z, zt}), Nat.mul(one, co)) : Nat}, L.false_true(h))
75    case Nil{} Con{y, yt} _:
76      Empty.absurd({Nat.add(Nat.add(0n, K.valo(one, Con{y, yt})), Nat.mul(one, c)) == Nat.add(K.valo(one, zs), Nat.mul(one, co)) : Nat}, L.false_true(h))
77    case Con{x, xt} Nil{} _:
78      Empty.absurd({Nat.add(Nat.add(K.valo(one, Con{x, xt}), 0n), Nat.mul(one, c)) == Nat.add(K.valo(one, zs), LM.sh(Con{x, xt}, Nat.mul(one, co))) : Nat}, L.false_true(h))
79    case Con{x, xt} Con{y, yt} Nil{}:
80      Empty.absurd({Nat.add(Nat.add(K.valo(one, Con{x, xt}), K.valo(one, Con{y, yt})), Nat.mul(one, c)) == Nat.add(0n, LM.sh(Con{x, xt}, Nat.mul(one, co))) : Nat}, L.false_true(h))