val op_Greater_Greater_Greater : a: MiTLS.Buffer.Utils.u32 ->
    s: MiTLS.Buffer.Utils.u32{0 < FStar.UInt32.v s && FStar.UInt32.v s < 32}
  -> FStar.UInt32.t
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))
module MiTLS.Buffer.Utils
open MiTLS

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
/
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
MiTLS.Buffer.Utils.fst

    a: MiTLS.Buffer.Utils.u32 ->
    s: MiTLS.Buffer.Utils.u32{0 < FStar.UInt32.v s && FStar.UInt32.v s < 32}
  -> FStar.UInt32.t
MiTLS.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
let ( >>> ) (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))