~/jendhub

def pos16

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bounds.bend:38

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as Bounds
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/crypto/secp256k1/limbs.bend as LV

38# 2^256 y
39def pos16(+y: Nat) -> {LV.pos(16n, y) == C.shift(256n, y) : Nat}:
40  pos_shift(16n, y)

Uses (4)

Used by (8)