val quad32_shift_2_left_1 (qa qb: quad32) : quad32 & quad32
let quad32_shift_2_left_1 (qa qb:quad32) : quad32 & quad32 =
  let la = four_map (fun (i:nat32) -> ishl i 1) qa in
  let lb = four_map (fun (i:nat32) -> ishl i 1) qb in
  let ra = four_map (fun (i:nat32) -> ishr i 31) qa in
  let rb = four_map (fun (i:nat32) -> ishr i 31) qb in
  let Mkfour ra0 ra1 ra2 ra3 = ra in
  let Mkfour rb0 rb1 rb2 rb3 = rb in
  let qa' = quad32_xor la (Mkfour 0 ra0 ra1 ra2) in
  let qb' = quad32_xor lb (quad32_xor (Mkfour ra3 0 0 0) (Mkfour 0 rb0 rb1 rb2)) in
  (qa', qb')
val quad32_shift_2_left_1 (qa qb: quad32) : quad32 & quad32
let quad32_shift_2_left_1 (qa qb: quad32) : quad32 & quad32 =
let la = four_map (fun (i: nat32) -> ishl i 1) qa in
let lb = four_map (fun (i: nat32) -> ishl i 1) qb in
let ra = four_map (fun (i: nat32) -> ishr i 31) qa in
let rb = four_map (fun (i: nat32) -> ishr i 31) qb in
let Mkfour ra0 ra1 ra2 ra3 = ra in
let Mkfour rb0 rb1 rb2 rb3 = rb in
let qa' = quad32_xor la (Mkfour 0 ra0 ra1 ra2) in
let qb' = quad32_xor lb (quad32_xor (Mkfour ra3 0 0 0) (Mkfour 0 rb0 rb1 rb2)) in
(qa', qb')
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 FStar.Pervasives.Native.Mktuple2 Vale.Def.Types_s.quad32_xor Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 FStar.Pervasives.Native.tuple2 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

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_2_left_1 (qa qb: quad32) : quad32 & quad32
qa: Vale.Def.Types_s.quad32 -> qb: Vale.Def.Types_s.quad32
  -> Vale.Def.Types_s.quad32 * Vale.Def.Types_s.quad32