def run0

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/consts.bend:67

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/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

67# a run of zeros shifts
68def run0(+one: Nat, +n: Nat, +tl: List<&2, U32>) -> {valo(one, rep(n, 0, tl)) == LM.shn(n, valo(one, tl)) : Nat}:
69  match n:
70    case 0n:
71      {==}
72    case 1n+ +m:
73      +R = valo(one, rep(m, 0, tl))
74      +e1 = M.cong_l(Nat.mul(one, 0n), 0n, C.shift(8n, R), NA.mul_zero(one))
75      Equal.trans(Nat, Nat.add(Nat.mul(one, 0n), C.shift(8n, R)), C.shift(8n, R), C.shift(8n, LM.shn(m, valo(one, tl))), e1, M.cong_sc(8n, R, LM.shn(m, valo(one, tl)), run0(one, m, tl)))