val va_code_Gctr_blocks128_body_1way : alg:algorithm -> Tot va_code
let va_code_Gctr_blocks128_body_1way alg =
  (va_Block (va_CCons (va_Block (va_CNil ())) (va_CCons (va_code_Vmr (va_op_vec_opr_vec 0)
    (va_op_vec_opr_vec 7)) (va_CCons (va_code_AESEncryptBlock alg) (va_CCons
    (va_code_Load128_byte16_buffer_index (va_op_heaplet_mem_heaplet 1) (va_op_vec_opr_vec 2)
    (va_op_reg_opr_reg 3) (va_op_reg_opr_reg 9) Secret) (va_CCons (va_code_Vxor (va_op_vec_opr_vec
    2) (va_op_vec_opr_vec 2) (va_op_vec_opr_vec 0)) (va_CCons (va_code_Store128_byte16_buffer_index
    (va_op_heaplet_mem_heaplet 1) (va_op_vec_opr_vec 2) (va_op_reg_opr_reg 7) (va_op_reg_opr_reg 9)
    Secret) (va_CNil ()))))))))
val va_code_Gctr_blocks128_body_1way : alg:algorithm -> Tot va_code
let va_code_Gctr_blocks128_body_1way alg =
(va_Block (va_CCons (va_Block (va_CNil ()))
        (va_CCons (va_code_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7))
            (va_CCons (va_code_AESEncryptBlock alg)
                (va_CCons (va_code_Load128_byte16_buffer_index (va_op_heaplet_mem_heaplet 1)
                        (va_op_vec_opr_vec 2)
                        (va_op_reg_opr_reg 3)
                        (va_op_reg_opr_reg 9)
                        Secret)
                    (va_CCons (va_code_Vxor (va_op_vec_opr_vec 2)
                            (va_op_vec_opr_vec 2)
                            (va_op_vec_opr_vec 0))
                        (va_CCons (va_code_Store128_byte16_buffer_index (va_op_heaplet_mem_heaplet 1
                                )
                                (va_op_vec_opr_vec 2)
                                (va_op_reg_opr_reg 7)
                                (va_op_reg_opr_reg 9)
                                Secret)
                            (va_CNil ()))))))))
Vale.AES.PPC64LE.GCTR.fst.checked
Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.QuickCodes.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsVector.fsti.checked Vale.PPC64LE.InsStack.fsti.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Poly1305.Math.fsti.checked Vale.Lib.Basic.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.Types_helpers.fsti.checked Vale.AES.PPC64LE.AES.fsti.checked Vale.AES.GCTR_BE_s.fst.checked Vale.AES.GCTR_BE.fsti.checked Vale.AES.GCM_helpers_BE.fsti.checked Vale.AES.AES_common_s.fst.checked Vale.AES.AES_BE_s.fst.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.PPC64LE.GCTR.fst
Vale.AES.AES_common_s.algorithm Vale.PPC64LE.Decls.va_Block Vale.PPC64LE.Decls.va_CCons Vale.PPC64LE.Decls.va_CNil Vale.PPC64LE.InsVector.va_code_Vmr Vale.PPC64LE.Decls.va_op_vec_opr_vec Vale.AES.PPC64LE.AES.va_code_AESEncryptBlock Vale.PPC64LE.InsVector.va_code_Load128_byte16_buffer_index Vale.PPC64LE.Decls.va_op_heaplet_mem_heaplet Vale.PPC64LE.Decls.va_op_reg_opr_reg Vale.Arch.HeapTypes_s.Secret Vale.PPC64LE.InsVector.va_code_Vxor Vale.PPC64LE.InsVector.va_code_Store128_byte16_buffer_index Vale.PPC64LE.Decls.va_code
module Vale.AES.PPC64LE.GCTR
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open FStar.Seq
open Vale.AES.AES_BE_s
open Vale.AES.PPC64LE.AES
open Vale.AES.GCTR_BE_s
open Vale.AES.GCTR_BE
open Vale.AES.GCM_helpers_BE
open Vale.Poly1305.Math
open Vale.Def.Words.Two_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.InsVector
open Vale.PPC64LE.InsStack
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.QuickCodes
open Vale.AES.Types_helpers
#reset-options "--z3rlimit 30"
open Vale.Lib.Basic
#reset-options "--z3rlimit 20"
//-- Gctr_register

[@ "opaque_to_smt" va_qattr]
let va_code_Gctr_register alg =
  (va_Block (va_CCons (va_code_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7)) (va_CCons
    (va_code_AESEncryptBlock alg) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_code_Vxor
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (va_CNil ()))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Gctr_register alg =
  (va_pbool_and (va_codegen_success_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7)) (va_pbool_and
    (va_codegen_success_AESEncryptBlock alg) (va_pbool_and (va_codegen_success_Vxor
    (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (va_ttrue ()))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Gctr_register (va_mods:va_mods_t) (alg:algorithm) (key:(seq nat32)) (round_keys:(seq
  quad32)) (keys_b:buffer128) : (va_quickCode unit (va_code_Gctr_register alg)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 99 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (Vale.AES.GCTR_BE_s.inc32 (va_get_vec 7 va_s) 0 == va_get_vec 7 va_s) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 100 column 8 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_quick_Vmr (va_op_vec_opr_vec 0) (va_op_vec_opr_vec 7)) (fun (va_s:va_state) _ -> va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 101 column 20 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_quick_AESEncryptBlock alg (va_get_vec 7 va_s) key round_keys keys_b) (fun (va_s:va_state) _
    -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    ((fun (alg_10536:Vale.AES.AES_common_s.algorithm) (key_10537:(FStar.Seq.Base.seq
    Vale.Def.Types_s.nat32)) (input_10538:Vale.Def.Types_s.quad32) ->
    Vale.AES.AES_BE_s.is_aes_key_word alg_10536 key_10537) alg key (va_get_vec 7 va_s)) (fun _ ->
    va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 102 column 5 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_get_vec 0 va_s == Vale.AES.AES_BE_s.aes_encrypt_word alg key (va_get_vec 7 va_s)) (va_QBind
    va_range1
    "***** PRECONDITION NOT MET AT line 104 column 9 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_quick_Vxor (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 1) (va_op_vec_opr_vec 0)) (fun
    (va_s:va_state) _ -> let (va_arg15:(FStar.Seq.Base.seq Vale.Def.Types_s.nat32)) = key in let
    (va_arg14:Vale.AES.AES_common_s.algorithm) = alg in let (va_arg13:Vale.Def.Types_s.quad32) =
    va_get_vec 1 va_old_s in let (va_arg12:Vale.Def.Types_s.quad32) = va_get_vec 7 va_s in va_qPURE
    va_range1
    "***** PRECONDITION NOT MET AT line 107 column 27 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.GCTR_BE.gctr_encrypt_one_block va_arg12 va_arg13 va_arg14 va_arg15)
    (va_QEmpty (()))))))))))

[@"opaque_to_smt"]
let va_lemma_Gctr_register va_b0 va_s0 alg key round_keys keys_b =
  let (va_mods:va_mods_t) = [va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10; va_Mod_ok] in
  let va_qc = va_qcode_Gctr_register va_mods alg key round_keys keys_b in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Gctr_register alg) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 80 column 1 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 96 column 142 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE (Vale.Def.Words.Seq_s.seq_four_to_seq_BE
    #Vale.Def.Words_s.nat32 (FStar.Seq.Base.create #quad32 1 (va_get_vec 1 va_sM))) ==
    Vale.AES.GCTR_BE_s.gctr_encrypt (va_get_vec 7 va_sM) (Vale.Arch.Types.be_quad32_to_bytes
    (va_get_vec 1 va_s0)) alg key) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 97 column 60 of file /home/gebner/everest/hacl-star/vale/code/crypto/aes/ppc64le/Vale.AES.PPC64LE.GCTR.vaf *****"
    (va_get_vec 1 va_sM == Vale.AES.GCTR_BE_s.gctr_encrypt_block (va_get_vec 7 va_sM) (va_get_vec 1
    va_s0) alg key 0))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10; va_Mod_ok]) va_sM
    va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Gctr_register alg key round_keys keys_b va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Gctr_register (va_code_Gctr_register alg) va_s0 alg key round_keys
    keys_b in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_vec 2 va_sM (va_update_vec 1 va_sM (va_update_vec 0 va_sM
    (va_update_reg 10 va_sM (va_update_ok va_sM va_s0))))));
  va_lemma_norm_mods ([va_Mod_vec 2; va_Mod_vec 1; va_Mod_vec 0; va_Mod_reg 10]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Gctr_blocks128_body_1way

val va_code_Gctr_blocks128_body_1way : alg:algorithm -> Tot va_code
[@ "opaque_to_smt" va_qattr]
val va_code_Gctr_blocks128_body_1way : alg:algorithm -> Tot va_code
alg: Vale.AES.AES_common_s.algorithm -> Vale.PPC64LE.Decls.va_code