val quad32_shr32 (q: quad32) : quad32
val quad32_shr32 (q: quad32) : quad32
let quad32_shr32 (q:quad32) : quad32 =
  let Mkfour v0 v1 v2 v3 = q in
  Mkfour v1 v2 v3 0
module Vale.AES.AES_helpers_BE

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.AES.AES_BE_s
open FStar.Mul
open Vale.Arch.Types
open Vale.Def.Words.Seq_s

// syntax for seq accesses, s.[index] and s.[index] <- value
unfold let (.[]) (#a:Type) (s:seq a) (i:nat{ i < length s}) : Tot a = index s i
unfold let (.[]<-) = Seq.upd

unfold let ( *^ ) = nat32_xor
unfold let ( *^^ ) = quad32_xor

unfold let be_quad32_to_seq (q:quad32) : seq nat32 = four_to_seq_BE q
/
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_BE_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.AES_helpers_BE.fsti
q: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32
Vale.Def.Types_s.quad32 Vale.Def.Types_s.nat32 Vale.Def.Words_s.Mkfour
let quad32_shr32 (q: quad32) : quad32 =
  
let Mkfour v0 v1 v2 v3 = q in
Mkfour v1 v2 v3 0