def le_split

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/random/bytes.bend:64

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

64def le_split(+x: W.U64) -> {SCR.le_bytes(x) == Con{b0(x), b7(x)} : List<&2, U32>}:
65  match x:
66    case W.U64{+l, +h}:
67      {==}