val div256 (x: U32.t) : Tot (y: U32.t{U32.v y == U32.v x / 256})
let div256 (x: U32.t) : Tot (y: U32.t { U32.v y == U32.v x / 256 }) =
  assert_norm (pow2 8 == 256);
  FStar.UInt.shift_right_value_lemma #32 (U32.v x) 8;
  x `U32.shift_right` 8ul
val div256 (x: U32.t) : Tot (y: U32.t{U32.v y == U32.v x / 256})
let div256 (x: U32.t) : Tot (y: U32.t{U32.v y == U32.v x / 256}) =
assert_norm (pow2 8 == 256);
FStar.UInt.shift_right_value_lemma #32 (U32.v x) 8;
x `U32.shift_right` 8ul
LowParse.Low.BoundedInt.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.BoundedInt.fst.checked LowParse.Low.Endianness.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Endianness.BitFields.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
LowParse.Low.BoundedInt.fst
FStar.UInt32.t FStar.UInt32.shift_right FStar.UInt32.__uint_to_t Prims.unit FStar.UInt.shift_right_value_lemma FStar.UInt32.v FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2 Prims.op_Division
module LowParse.Low.BoundedInt
open LowParse.Low.Combinators
module Seq = FStar.Seq
module U8  = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module E = LowParse.Endianness.BitFields
module BF = LowParse.BitFields
module LE = LowParse.Low.Endianness
module Cast = FStar.Int.Cast

friend LowParse.Spec.BoundedInt

inline_for_extraction
let mul256 (x: U16.t) : Tot (y: U32.t { U32.v y == 256 `Prims.op_Multiply` U16.v x }) =
  assert_norm (pow2 8 == 256);
  FStar.Math.Lemmas.pow2_lt_compat 32 24;
  FStar.Math.Lemmas.pow2_lt_compat 24 16;
  FStar.Math.Lemmas.pow2_lt_compat 16 8;
  FStar.Math.Lemmas.pow2_plus 8 16;
  FStar.Math.Lemmas.small_mod (U16.v x `Prims.op_Multiply` 256) (pow2 32);
  FStar.UInt.shift_left_value_lemma #32 (U16.v x) 8;
  Cast.uint16_to_uint32 x `U32.shift_left` 8ul

inline_for_extraction
val div256 (x: U32.t) : Tot (y: U32.t{U32.v y == U32.v x / 256})
x: FStar.UInt32.t -> y: FStar.UInt32.t{FStar.UInt32.v y == FStar.UInt32.v x / 256}