val related_zero_u64: Prims.unit
  -> Lemma ((UInt.to_vec (U64.v 0uL)) `Seq.equal` (FStar.BitVector.zero_vec #64))
val related_zero_u64: Prims.unit
  -> Lemma ((UInt.to_vec (U64.v 0uL)) `Seq.equal` (FStar.BitVector.zero_vec #64))
let related_zero_u64 ()
  : Lemma (UInt.to_vec (U64.v 0uL) `Seq.equal`
           FStar.BitVector.zero_vec #64)
  = assert (U64.v 0uL == UInt.zero 64)
module Zeta.Steel.BitUtils

module T = Zeta.Steel.FormatsManual
module L = FStar.List.Tot
module U64 = FStar.UInt64
module BV = FStar.BV

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

let bitvec_of_u64_inj  (i j:U64.t)
  : Lemma
    (ensures
      UInt.to_vec (U64.v i) == UInt.to_vec (U64.v j) ==>
      i == j)
  = UInt.inverse_num_lemma (U64.v i);
    UInt.inverse_num_lemma (U64.v j)

let bitvec_of_u256_inj (i j:_)
  : Lemma
    (ensures bitvec_of_u256 i == bitvec_of_u256 j ==>
             i == j)
  = bitvec_of_u64_inj i.v0 j.v0;
    bitvec_of_u64_inj i.v1 j.v1;
    bitvec_of_u64_inj i.v2 j.v2;
    bitvec_of_u64_inj i.v3 j.v3;
    if bitvec_of_u256 i = bitvec_of_u256 j
    then (
    Seq.lemma_append_inj
      (UInt.to_vec (U64.v i.v0))
      ((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)))))
      (UInt.to_vec (U64.v j.v0))
      ((UInt.to_vec (U64.v j.v1)) `Seq.append` (
       (UInt.to_vec (U64.v j.v2)) `Seq.append` (
       (UInt.to_vec (U64.v j.v3)))));
    Seq.lemma_append_inj
      (UInt.to_vec (U64.v i.v1))
      ((UInt.to_vec (U64.v i.v2)) `Seq.append` (
       (UInt.to_vec (U64.v i.v3))))
      (UInt.to_vec (U64.v j.v1))
       ((UInt.to_vec (U64.v j.v2)) `Seq.append` (
       (UInt.to_vec (U64.v j.v3))));
    Seq.lemma_append_inj
      (UInt.to_vec (U64.v i.v2))
      (UInt.to_vec (U64.v i.v3))
      (UInt.to_vec (U64.v j.v2))
      (UInt.to_vec (U64.v j.v3))
    )
/
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
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures FStar.Seq.Base.equal (FStar.UInt.to_vec (FStar.UInt64.v 0uL)) FStar.BitVector.zero_vec)
Prims.unit Prims._assert Prims.eq2 FStar.UInt.uint_t FStar.UInt64.n FStar.UInt64.v FStar.UInt64.__uint_to_t FStar.UInt.zero Prims.l_True Prims.squash FStar.Seq.Base.equal Prims.bool FStar.UInt.to_vec FStar.BitVector.zero_vec Prims.Nil FStar.Pervasives.pattern
let related_zero_u64 ()
    : Lemma ((UInt.to_vec (U64.v 0uL)) `Seq.equal` (FStar.BitVector.zero_vec #64)) =
  
assert (U64.v 0uL == UInt.zero 64)