val bitvec_of_u256 (i: T.u256)
  : bv_t 256
val bitvec_of_u256 (i: T.u256)
  : bv_t 256
let bitvec_of_u256 (i:T.u256) : FStar.BitVector.bv_t 256 =
  (UInt.to_vec (U64.v i.v0)) `Seq.append` (
  (UInt.to_vec (U64.v i.v1)) `Seq.append` (
  (UInt.to_vec (U64.v i.v2)) `Seq.append` (
  (UInt.to_vec (U64.v i.v3)))))
module Zeta.Steel.BitUtils

module T = Zeta.Steel.FormatsManual
module L = FStar.List.Tot
module U64 = FStar.UInt64
module BV = FStar.BV
/
Zeta.Steel.FormatsManual.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.BV.fsti.checked FStar.BitVector.fst.checked
Zeta.Steel.BitUtils.fst
i: Zeta.Steel.KeyUtils.u256 -> Zeta.Steel.BitUtils.bv_t 256
Zeta.Steel.KeyUtils.u256 FStar.Seq.Base.append Prims.bool FStar.UInt.to_vec FStar.UInt64.n FStar.UInt64.v Zeta.Steel.KeyUtils.__proj__Mku256__item__v0 Zeta.Steel.KeyUtils.__proj__Mku256__item__v1 Zeta.Steel.KeyUtils.__proj__Mku256__item__v2 Zeta.Steel.KeyUtils.__proj__Mku256__item__v3 FStar.BitVector.bv_t Zeta.Steel.BitUtils.bv_t
let bitvec_of_u256 (i: T.u256) : FStar.BitVector.bv_t 256 =
  
(UInt.to_vec (U64.v i.v0))
`Seq.append`
((UInt.to_vec (U64.v i.v1))
  `Seq.append`
  ((UInt.to_vec (U64.v i.v2)) `Seq.append` ((UInt.to_vec (U64.v i.v3)))))