def bits_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/top.bend:31

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/src/crypto/curve25519/x25519.bend as X
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/ed25519/bytes.bend as BY

31def bits_eq(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +hk: {LM.okb(32n, k, 255n) == True{} : Bool}) -> {X.bitlen(k) == C.shift(8n, one) : Nat}:
32  Equal.trans(Nat, X.bitlen(k), 256n, C.shift(8n, one), BY.bitlen_256(k, hk), Equal.cong(Nat, Nat, z => C.shift(8n, z), 1n, one, Equal.sym(Nat, one, 1n, h1)))