val va_wp_ShiftLeft128_1 (a: poly) (va_s0: va_state) (va_k: (va_state -> unit -> Type0)) : Type0
let va_wp_ShiftLeft128_1 (a:poly) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree a < 128 /\ va_get_vec 1 va_s0 ==
    Vale.Math.Poly2.Bits_s.to_quad32 a /\ (forall (va_x_v1:quad32) (va_x_v2:quad32) . let va_sM =
    va_upd_vec 2 va_x_v2 (va_upd_vec 1 va_x_v1 va_s0) in va_get_ok va_sM /\ va_get_vec 1 va_sM ==
    Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.shift a 1) ==> va_k va_sM (())))
val va_wp_ShiftLeft128_1 (a: poly) (va_s0: va_state) (va_k: (va_state -> unit -> Type0)) : Type0
let va_wp_ShiftLeft128_1 (a: poly) (va_s0: va_state) (va_k: (va_state -> unit -> Type0)) : Type0 =
(va_get_ok va_s0 /\ Vale.Math.Poly2_s.degree a < 128 /\
  va_get_vec 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 a /\
  (forall (va_x_v1: quad32) (va_x_v2: quad32).
      let va_sM = va_upd_vec 2 va_x_v2 (va_upd_vec 1 va_x_v1 va_s0) in
      va_get_ok va_sM /\
      va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.shift a 1) ==>
      va_k va_sM (())))
Vale.AES.PPC64LE.GF128_Mul.fsti.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.QuickCodes.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsVector.fsti.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Math.Poly2.Bits.fsti.checked Vale.Math.Poly2.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.Types_helpers.fsti.checked Vale.AES.PPC64LE.PolyOps.fsti.checked Vale.AES.GHash_BE.fsti.checked Vale.AES.GF128_s.fsti.checked Vale.AES.GF128.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.PPC64LE.GF128_Mul.fsti
Vale.Math.Poly2_s.poly Vale.PPC64LE.Decls.va_state Prims.unit Prims.l_and Prims.b2t Vale.PPC64LE.Decls.va_get_ok Prims.op_LessThan Vale.Math.Poly2_s.degree Prims.eq2 Vale.Def.Types_s.quad32 Vale.PPC64LE.Decls.va_get_vec Vale.Math.Poly2.Bits_s.to_quad32 Prims.l_Forall Vale.PPC64LE.Machine_s.quad32 Prims.l_imp Vale.Math.Poly2_s.shift Vale.PPC64LE.Machine_s.state Vale.PPC64LE.Decls.va_upd_vec
module Vale.AES.PPC64LE.GF128_Mul
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.TypesNative
open Vale.Math.Poly2_s
open Vale.Math.Poly2
open Vale.Math.Poly2.Bits_s
open Vale.Math.Poly2.Bits
open Vale.Math.Poly2.Lemmas
open Vale.AES.GF128_s
open Vale.AES.GF128
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.InsVector
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.QuickCodes
open Vale.AES.PPC64LE.PolyOps
open Vale.AES.Types_helpers
open Vale.AES.GHash_BE
//-- ShiftLeft128_1

val va_code_ShiftLeft128_1 : va_dummy:unit -> Tot va_code

val va_codegen_success_ShiftLeft128_1 : va_dummy:unit -> Tot va_pbool

val va_lemma_ShiftLeft128_1 : va_b0:va_code -> va_s0:va_state -> a:poly
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_ShiftLeft128_1 ()) va_s0 /\ va_get_ok va_s0 /\
    Vale.Math.Poly2_s.degree a < 128 /\ va_get_vec 1 va_s0 == Vale.Math.Poly2.Bits_s.to_quad32 a))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    va_get_vec 1 va_sM == Vale.Math.Poly2.Bits_s.to_quad32 (Vale.Math.Poly2_s.shift a 1) /\
    va_state_eq va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM (va_update_ok va_sM va_s0)))))
[@ va_qattr]
val va_wp_ShiftLeft128_1 (a: poly) (va_s0: va_state) (va_k: (va_state -> unit -> Type0)) : Type0

    a: Vale.Math.Poly2_s.poly ->
    va_s0: Vale.PPC64LE.Decls.va_state ->
    va_k: (_: Vale.PPC64LE.Decls.va_state -> _: Prims.unit -> Type0)
  -> Type0