let op_Greater_Greater_Greater (a:u32) (s:u32{0 < v s && v s < 32}) =
  let (m:u32{v m = 32}) = 32ul in
  (op_Greater_Greater_Hat a s) |^ (a <<^ (m -^ s))
let op_Greater_Greater_Greater (a: u32) (s: u32{0 < v s && v s < 32}) =
let m:m: u32{v m = 32} = 32ul in
(op_Greater_Greater_Hat a s) |^ (a <<^ (m -^ s))
Buffer.Utils.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Buffer.fst.checked C.Compat.Loops.fst.checked
Buffer.Utils.fst
Buffer.Utils.u32 Prims.b2t Prims.op_AmpAmp Prims.op_LessThan FStar.UInt32.v FStar.UInt32.op_Bar_Hat FStar.UInt32.op_Greater_Greater_Hat FStar.UInt32.op_Less_Less_Hat FStar.UInt32.op_Subtraction_Hat Prims.op_Equality Prims.int FStar.UInt32.__uint_to_t FStar.UInt32.t
module Buffer.Utils

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All

open FStar.Mul
open FStar.Ghost
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Int.Cast
open FStar.UInt8
open FStar.UInt32
open FStar.Buffer

open FStar.Math.Lemmas

module U8 = FStar.UInt8
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST

let u32 = FStar.UInt32.t
let u8 = FStar.UInt8.t
let uint32s = buffer u32
let bytes = buffer u8
val op_Greater_Greater_Greater : a: Buffer.Utils.u32 -> s: Buffer.Utils.u32{0 < FStar.UInt32.v s && FStar.UInt32.v s < 32}
  -> FStar.UInt32.t
a: Buffer.Utils.u32 -> s: Buffer.Utils.u32{0 < FStar.UInt32.v s && FStar.UInt32.v s < 32}
  -> FStar.UInt32.t