def h2L

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar3.bend:79

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as AD
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC

79# 2 L <= 2^256
80def h2L(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(Nat.add(1n+mmL(one), 1n+mmL(one)), SC.T(one)) == True{} : Bool}:
81  +l = K.valo(one, ESC.ell())
82  +d = K.valo(one, dlist())
83  +c = K.valo(one, ESC.comp_l())
84  +m = {1n+mmL(one) : Nat}
85  +e = AD.adc_val(one, ESC.ell(), dlist(), ESC.comp_l(), 0n, 0n, adc1())
86  +s0 = Equal.trans(Nat, LM.sh(ESC.ell(), Nat.mul(one, 0n)), LM.shn(32n, Nat.mul(one, 0n)), 0n, LM.sh_okb(32n, ESC.ell(), 255n, Nat.mul(one, 0n), {==}), Equal.cong(Nat, Nat, z => LM.shn(32n, z), Nat.mul(one, 0n), 0n, NA.mul_zero(one)))
87  +e1 = Equal.trans(Nat, Nat.add(l, d), Nat.add(Nat.add(l, d), Nat.mul(one, 0n)), c, Equal.trans(Nat, Nat.add(l, d), Nat.add(Nat.add(l, d), 0n), Nat.add(Nat.add(l, d), Nat.mul(one, 0n)), Equal.sym(Nat, Nat.add(Nat.add(l, d), 0n), Nat.add(l, d), N.add_zero(Nat.add(l, d))), M.cong_r(Nat.add(l, d), 0n, Nat.mul(one, 0n), Equal.sym(Nat, Nat.mul(one, 0n), 0n, NA.mul_zero(one)))), Equal.trans(Nat, Nat.add(Nat.add(l, d), Nat.mul(one, 0n)), Nat.add(c, LM.sh(ESC.ell(), Nat.mul(one, 0n))), c, e, Equal.trans(Nat, Nat.add(c, LM.sh(ESC.ell(), Nat.mul(one, 0n))), Nat.add(c, 0n), c, M.cong_r(c, LM.sh(ESC.ell(), Nat.mul(one, 0n)), 0n, s0), N.add_zero(c))))
88  +lm = Equal.trans(Nat, l, SE.ell(one), m, ell_valo(one), Equal.sym(Nat, m, SE.ell(one), ell_eq(one, h1)))
89  +e2 = Equal.trans(Nat, Nat.add(Nat.add(m, m), d), Nat.add(m, Nat.add(l, d)), SC.T(one), Equal.trans(Nat, Nat.add(Nat.add(m, m), d), Nat.add(m, Nat.add(m, d)), Nat.add(m, Nat.add(l, d)), NA.add_assoc(m, m, d), M.cong_r(m, Nat.add(m, d), Nat.add(l, d), M.cong_l(m, l, d, Equal.sym(Nat, l, m, lm)))), Equal.trans(Nat, Nat.add(m, Nat.add(l, d)), Nat.add(m, c), SC.T(one), M.cong_r(m, Nat.add(l, d), c, e1), Equal.trans(Nat, Nat.add(m, c), Nat.add(c, m), SC.T(one), NA.add_comm(m, c), hvL(one, h1))))
90  L.subst(Nat, z => {Nat.is_le(Nat.add(m, m), z) == True{} : Bool}, Nat.add(Nat.add(m, m), d), SC.T(one), e2, N.le_add_right(Nat.add(m, m), d))