val quad32_shift_left_1 (q: quad32) : quad32
let quad32_shift_left_1 (q:quad32) : quad32 =
  let l = four_map (fun (i:nat32) -> ishl i 1) q in
  let r = four_map (fun (i:nat32) -> ishr i 31) q in
  let Mkfour r0 r1 r2 r3 = r in
  quad32_xor l (Mkfour 0 r0 r1 r2)
val quad32_shift_left_1 (q: quad32) : quad32
let quad32_shift_left_1 (q: quad32) : quad32 =
let l = four_map (fun (i: nat32) -> ishl i 1) q in
let r = four_map (fun (i: nat32) -> ishr i 31) q in
let Mkfour r0 r1 r2 r3 = r in
quad32_xor l (Mkfour 0 r0 r1 r2)
Vale.AES.GF128.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Math.Poly2.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.GF128_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.GF128.fsti
Vale.Def.Types_s.quad32 Vale.Def.Words_s.natN Vale.Def.Words_s.pow2_32 Vale.Def.Types_s.quad32_xor Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 Vale.Def.Words_s.four Vale.Def.Words.Four_s.four_map Vale.Def.Types_s.ishr Vale.Def.Types_s.ishl
module Vale.AES.GF128
open FStar.Seq
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.AES.GF128_s
open Vale.Math.Poly2_s
open Vale.Math.Poly2.Bits_s
open Vale.Math.Poly2
open Vale.Math.Poly2.Lemmas
val quad32_shift_left_1 (q: quad32) : quad32
q: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32