val va_qcode_Aes_ctr_encrypt
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
      (in1 in2 in3 in4: quad32)
    : (va_quickCode unit (va_code_Aes_ctr_encrypt alg))
val va_qcode_Aes_ctr_encrypt
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
      (in1 in2 in3 in4: quad32)
    : (va_quickCode unit (va_code_Aes_ctr_encrypt alg))
let va_qcode_Aes_ctr_encrypt (va_mods:va_mods_t) (alg:algorithm) (key:(seq nat32)) (round_keys:(seq
  quad32)) (keys_b:buffer128) (in1:quad32) (in2:quad32) (in3:quad32) (in4:quad32) : (va_quickCode
  unit (va_code_Aes_ctr_encrypt alg)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in let
    (va_arg89:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg88:Vale.Def.Types_s.quad32) = va_get_xmm 2 va_old_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 286 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg88 va_arg89) (let
    (va_arg87:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg86:Vale.Def.Types_s.quad32) = va_get_xmm 12 va_old_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 287 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg86 va_arg87) (let
    (va_arg85:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg84:Vale.Def.Types_s.quad32) = va_get_xmm 13 va_old_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 288 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg84 va_arg85) (let
    (va_arg83:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg82:Vale.Def.Types_s.quad32) = va_get_xmm 14 va_old_s in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 289 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg82 va_arg83) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 291 column 21 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_3rounds_4way alg 1 (va_get_xmm 2 va_old_s) (va_get_xmm 12 va_old_s) (va_get_xmm
    13 va_old_s) (va_get_xmm 14 va_old_s) round_keys) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 294 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64
    rR8) 64 Secret keys_b 4) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 295 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64
    rR8) 80 Secret keys_b 5) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 296 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR8) 96 Secret keys_b 6) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 297 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 6) (va_op_reg_opr64_reg64
    rR8) 112 Secret keys_b 7) (fun (va_s:va_state) _ -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 298 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 4) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 298 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 3 va_s == FStar.Seq.Base.index #quad32 round_keys 4) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 299 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 5) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 299 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 4 va_s == FStar.Seq.Base.index #quad32 round_keys 5) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 300 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 6) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 300 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 5 va_s == FStar.Seq.Base.index #quad32 round_keys 6) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 301 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 7) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 301 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 6 va_s == FStar.Seq.Base.index #quad32 round_keys 7) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 304 column 21 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_4rounds_4way alg 4 (va_get_xmm 2 va_old_s) (va_get_xmm 12 va_old_s) (va_get_xmm
    13 va_old_s) (va_get_xmm 14 va_old_s) round_keys) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 307 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64
    rR8) 128 Secret keys_b 8) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 308 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64
    rR8) 144 Secret keys_b 9) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 309 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR8) 160 Secret keys_b 10) (fun (va_s:va_state) _ -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 310 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 8) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 310 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 3 va_s == FStar.Seq.Base.index #quad32 round_keys 8) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 311 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 9) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 311 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 4 va_s == FStar.Seq.Base.index #quad32 round_keys 9) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 312 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 10) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 312 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 5 va_s == FStar.Seq.Base.index #quad32 round_keys 10) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 315 column 21 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_2rounds_4way alg 8 (va_get_xmm 2 va_old_s) (va_get_xmm 12 va_old_s) (va_get_xmm
    13 va_old_s) (va_get_xmm 14 va_old_s) round_keys) (fun (va_s:va_state) _ -> va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 318 column 15 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_qInlineIf va_mods (alg = AES_256) (qblock va_mods (fun (va_s:va_state) -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 320 column 15 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Mov128 (va_op_xmm_xmm 3) (va_op_xmm_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 321 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64
    rR8) 176 Secret keys_b 11) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 322 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR8) 192 Secret keys_b 12) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 323 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 6) (va_op_reg_opr64_reg64
    rR8) 208 Secret keys_b 13) (fun (va_s:va_state) _ -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 324 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 10) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 324 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 3 va_s == FStar.Seq.Base.index #quad32 round_keys 10) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 325 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 11) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 325 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 4 va_s == FStar.Seq.Base.index #quad32 round_keys 11) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 326 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 12) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 326 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 5 va_s == FStar.Seq.Base.index #quad32 round_keys 12) (va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 327 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 13) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 327 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 6 va_s == FStar.Seq.Base.index #quad32 round_keys 13) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 330 column 25 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_4rounds_4way alg 10 (va_get_xmm 2 va_old_s) (va_get_xmm 12 va_old_s) (va_get_xmm
    13 va_old_s) (va_get_xmm 14 va_old_s) round_keys) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 333 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64
    rR8) 224 Secret keys_b 14) (fun (va_s:va_state) _ -> va_qAssertSquash va_range1
    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 334 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun a_539 (s_540:(FStar.Seq.Base.seq a_539)) (i_541:Prims.nat) -> let (i_515:Prims.nat) =
    i_541 in Prims.b2t (Prims.op_LessThan i_515 (FStar.Seq.Base.length #a_539 s_540))) quad32
    round_keys 14) (fun _ -> va_qAssert va_range1
    "***** PRECONDITION NOT MET AT line 334 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 5 va_s == FStar.Seq.Base.index #quad32 round_keys 14) (va_QEmpty
    (()))))))))))))))))))) (qblock va_mods (fun (va_s:va_state) -> va_QEmpty (())))) (fun
    (va_s:va_state) va_g -> va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 341 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_AESNI_enc_last (va_op_xmm_xmm 2) (va_op_xmm_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 342 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_AESNI_enc_last (va_op_xmm_xmm 12) (va_op_xmm_xmm 5)) (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 343 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_AESNI_enc_last (va_op_xmm_xmm 13) (va_op_xmm_xmm 5)) (va_QBind va_range1
    "***** PRECONDITION NOT MET AT line 344 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_AESNI_enc_last (va_op_xmm_xmm 14) (va_op_xmm_xmm 5)) (fun (va_s:va_state) _ -> let
    (va_arg81:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg80:Vale.Def.Types_s.quad32) = in1 in let (va_arg79:Vale.AES.AES_common_s.algorithm) =
    alg in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 346 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.finish_cipher va_arg79 va_arg80 va_arg81) (let
    (va_arg78:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg77:Vale.Def.Types_s.quad32) = in2 in let (va_arg76:Vale.AES.AES_common_s.algorithm) =
    alg in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 347 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.finish_cipher va_arg76 va_arg77 va_arg78) (let
    (va_arg75:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg74:Vale.Def.Types_s.quad32) = in3 in let (va_arg73:Vale.AES.AES_common_s.algorithm) =
    alg in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 348 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.finish_cipher va_arg73 va_arg74 va_arg75) (let
    (va_arg72:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32)) = round_keys in let
    (va_arg71:Vale.Def.Types_s.quad32) = in4 in let (va_arg70:Vale.AES.AES_common_s.algorithm) =
    alg in va_qPURE va_range1
    "***** PRECONDITION NOT MET AT line 349 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (fun (_:unit) -> Vale.AES.AES_helpers.finish_cipher va_arg70 va_arg71 va_arg72) (va_QLemma
    va_range1
    "***** PRECONDITION NOT MET AT line 350 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) -> Vale.AES.AES_s.is_aes_key_LE alg
    key) alg in1 key) (fun _ -> (fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) ->
    Vale.AES.AES_s.aes_encrypt_LE alg key input_LE == Vale.AES.AES_s.eval_cipher alg input_LE
    (Vale.AES.AES_s.key_to_round_keys_LE alg key)) alg in1 key) (fun (_:unit) ->
    finish_aes_encrypt_le alg in1 key) (va_QLemma va_range1
    "***** PRECONDITION NOT MET AT line 351 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) -> Vale.AES.AES_s.is_aes_key_LE alg
    key) alg in2 key) (fun _ -> (fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) ->
    Vale.AES.AES_s.aes_encrypt_LE alg key input_LE == Vale.AES.AES_s.eval_cipher alg input_LE
    (Vale.AES.AES_s.key_to_round_keys_LE alg key)) alg in2 key) (fun (_:unit) ->
    finish_aes_encrypt_le alg in2 key) (va_QLemma va_range1
    "***** PRECONDITION NOT MET AT line 352 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) -> Vale.AES.AES_s.is_aes_key_LE alg
    key) alg in3 key) (fun _ -> (fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) ->
    Vale.AES.AES_s.aes_encrypt_LE alg key input_LE == Vale.AES.AES_s.eval_cipher alg input_LE
    (Vale.AES.AES_s.key_to_round_keys_LE alg key)) alg in3 key) (fun (_:unit) ->
    finish_aes_encrypt_le alg in3 key) (va_QLemma va_range1
    "***** PRECONDITION NOT MET AT line 353 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    ((fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) -> Vale.AES.AES_s.is_aes_key_LE alg
    key) alg in4 key) (fun _ -> (fun (alg:algorithm) (input_LE:quad32) (key:(seq nat32)) ->
    Vale.AES.AES_s.aes_encrypt_LE alg key input_LE == Vale.AES.AES_s.eval_cipher alg input_LE
    (Vale.AES.AES_s.key_to_round_keys_LE alg key)) alg in4 key) (fun (_:unit) ->
    finish_aes_encrypt_le alg in4 key) (va_QEmpty (()))))))))))))))))))))))))))))))))))))))))))))
module Vale.AES.X64.AESCTR
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Seq
open Vale.Arch.Types
open Vale.Arch.HeapImpl
open Vale.AES.AES_s
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsVector
open Vale.X64.InsAes
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.AES.AES_helpers
open Vale.Poly1305.Math    // For lemma_poly_bits64()
open Vale.AES.GCM_helpers
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.Arch.TypesNative
open Vale.AES.X64.GHash
open Vale.AES.GHash
open Vale.X64.CPU_Features_s
//-- finish_aes_encrypt_le


val finish_aes_encrypt_le : alg:algorithm -> input_LE:quad32 -> key:(seq nat32)
  -> Lemma
  (requires (Vale.AES.AES_s.is_aes_key_LE alg key))
  (ensures (Vale.AES.AES_s.aes_encrypt_LE alg key input_LE == Vale.AES.AES_s.eval_cipher alg
    input_LE (Vale.AES.AES_s.key_to_round_keys_LE alg key)))
let finish_aes_encrypt_le alg input_LE key =
  Vale.AES.AES_s.aes_encrypt_LE_reveal ();
  Vale.AES.AES_s.eval_cipher_reveal ();
  ()
//--
//-- Aes_round_4way

val va_code_Aes_round_4way : round_key:va_operand_xmm -> Tot va_code
[@ "opaque_to_smt"]
let va_code_Aes_round_4way round_key =
  (va_Block (va_CCons (va_code_AESNI_enc (va_op_xmm_xmm 2) round_key) (va_CCons (va_code_AESNI_enc
    (va_op_xmm_xmm 12) round_key) (va_CCons (va_code_AESNI_enc (va_op_xmm_xmm 13) round_key)
    (va_CCons (va_code_AESNI_enc (va_op_xmm_xmm 14) round_key) (va_CNil ()))))))

val va_codegen_success_Aes_round_4way : round_key:va_operand_xmm -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_Aes_round_4way round_key =
  (va_pbool_and (va_codegen_success_AESNI_enc (va_op_xmm_xmm 2) round_key) (va_pbool_and
    (va_codegen_success_AESNI_enc (va_op_xmm_xmm 12) round_key) (va_pbool_and
    (va_codegen_success_AESNI_enc (va_op_xmm_xmm 13) round_key) (va_pbool_and
    (va_codegen_success_AESNI_enc (va_op_xmm_xmm 14) round_key) (va_ttrue ())))))


val va_lemma_Aes_round_4way : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> n:pos ->
  round_key:va_operand_xmm -> init1:quad32 -> init2:quad32 -> init3:quad32 -> init4:quad32 ->
  round_keys:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Aes_round_4way round_key) va_s0 /\ va_is_src_xmm
    round_key va_s0 /\ va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr
    alg /\ Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm
    2 va_s0 == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_eval_xmm va_s0 round_key ==
    FStar.Seq.Base.index #quad32 round_keys n /\ 2 =!= round_key /\ 12 =!= round_key /\ 13 =!=
    round_key /\ 14 =!= round_key)))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys n /\ va_get_xmm 12 va_sM ==
    Vale.AES.AES_s.eval_rounds init2 round_keys n /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys n /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys n) /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM
    (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Aes_round_4way va_b0 va_s0 alg n round_key init1 init2 init3 init4 round_keys =
  va_reveal_opaque (`%va_code_Aes_round_4way) (va_code_Aes_round_4way round_key);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  Vale.AES.AES_s.eval_rounds_reveal ();
  Vale.AES.AES_helpers.commute_sub_bytes_shift_rows_forall ();
  let (va_s8, va_fc8) = va_lemma_AESNI_enc (va_hd va_b1) va_s0 (va_op_xmm_xmm 2) round_key in
  let va_b8 = va_tl va_b1 in
  let (va_s9, va_fc9) = va_lemma_AESNI_enc (va_hd va_b8) va_s8 (va_op_xmm_xmm 12) round_key in
  let va_b9 = va_tl va_b8 in
  let (va_s10, va_fc10) = va_lemma_AESNI_enc (va_hd va_b9) va_s9 (va_op_xmm_xmm 13) round_key in
  let va_b10 = va_tl va_b9 in
  let (va_s11, va_fc11) = va_lemma_AESNI_enc (va_hd va_b10) va_s10 (va_op_xmm_xmm 14) round_key in
  let va_b11 = va_tl va_b10 in
  let (va_sM, va_f11) = va_lemma_empty_total va_s11 va_b11 in
  let va_f10 = va_lemma_merge_total va_b10 va_s10 va_fc11 va_s11 va_f11 va_sM in
  let va_f9 = va_lemma_merge_total va_b9 va_s9 va_fc10 va_s10 va_f10 va_sM in
  let va_f8 = va_lemma_merge_total va_b8 va_s8 va_fc9 va_s9 va_f9 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc8 va_s8 va_f8 va_sM in
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Aes_round_4way (alg:algorithm) (n:pos) (round_key:va_operand_xmm) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) (va_s0:va_state)
  (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_is_src_xmm round_key va_s0 /\ va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n <
    Vale.AES.AES_common_s.nr alg /\ Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32
    round_keys) /\ va_get_xmm 2 va_s0 == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\
    va_get_xmm 12 va_s0 == Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13
    va_s0 == Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_eval_xmm va_s0 round_key ==
    FStar.Seq.Base.index #quad32 round_keys n /\ 2 =!= round_key /\ 12 =!= round_key /\ 13 =!=
    round_key /\ 14 =!= round_key) /\ (forall (va_x_xmm2:quad32) (va_x_xmm12:quad32)
    (va_x_xmm13:quad32) (va_x_xmm14:quad32) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags
    va_x_efl (va_upd_xmm 14 va_x_xmm14 (va_upd_xmm 13 va_x_xmm13 (va_upd_xmm 12 va_x_xmm12
    (va_upd_xmm 2 va_x_xmm2 va_s0)))) in va_get_ok va_sM /\ (va_get_xmm 2 va_sM ==
    Vale.AES.AES_s.eval_rounds init1 round_keys n /\ va_get_xmm 12 va_sM ==
    Vale.AES.AES_s.eval_rounds init2 round_keys n /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys n /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys n) ==> va_k va_sM (())))


val va_wpProof_Aes_round_4way : alg:algorithm -> n:pos -> round_key:va_operand_xmm -> init1:quad32
  -> init2:quad32 -> init3:quad32 -> init4:quad32 -> round_keys:(seq quad32) -> va_s0:va_state ->
  va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Aes_round_4way alg n round_key init1 init2 init3 init4
    round_keys va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Aes_round_4way round_key)
    ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2]) va_s0 va_k ((va_sM,
    va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Aes_round_4way alg n round_key init1 init2 init3 init4 round_keys va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Aes_round_4way (va_code_Aes_round_4way round_key) va_s0 alg n
    round_key init1 init2 init3 init4 round_keys in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM
    (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Aes_round_4way (alg:algorithm) (n:pos) (round_key:va_operand_xmm) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit
  (va_code_Aes_round_4way round_key)) =
  (va_QProc (va_code_Aes_round_4way round_key) ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13;
    va_Mod_xmm 12; va_Mod_xmm 2]) (va_wp_Aes_round_4way alg n round_key init1 init2 init3 init4
    round_keys) (va_wpProof_Aes_round_4way alg n round_key init1 init2 init3 init4 round_keys))
//--
//-- Aes_2rounds_4way

val va_code_Aes_2rounds_4way : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Aes_2rounds_4way () =
  (va_Block (va_CCons (va_code_Aes_round_4way (va_op_xmm_xmm 3)) (va_CCons (va_code_Aes_round_4way
    (va_op_xmm_xmm 4)) (va_CNil ()))))

val va_codegen_success_Aes_2rounds_4way : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Aes_2rounds_4way () =
  (va_pbool_and (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 3)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 4)) (va_ttrue ())))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Aes_2rounds_4way (va_mods:va_mods_t) (alg:algorithm) (n:pos) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit
  (va_code_Aes_2rounds_4way ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 162 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg n (va_op_xmm_xmm 3) init1 init2 init3 init4 round_keys) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 163 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 1) (va_op_xmm_xmm 4) init1 init2 init3 init4 round_keys)
    (va_QEmpty (())))))


val va_lemma_Aes_2rounds_4way : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> n:pos ->
  init1:quad32 -> init2:quad32 -> init3:quad32 -> init4:quad32 -> round_keys:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Aes_2rounds_4way ()) va_s0 /\ va_get_ok va_s0 /\
    (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 1 /\ Vale.AES.AES_common_s.nr
    alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0 ==
    Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 3 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys n /\ va_get_xmm 4 va_s0 == FStar.Seq.Base.index #quad32
    round_keys (n + 1))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 1) /\ va_get_xmm 12
    va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 1) /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n + 1) /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n + 1)) /\ va_state_eq va_sM (va_update_flags
    va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM (va_update_xmm 12 va_sM (va_update_xmm 2
    va_sM (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Aes_2rounds_4way va_b0 va_s0 alg n init1 init2 init3 init4 round_keys =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm
    2; va_Mod_ok] in
  let va_qc = va_qcode_Aes_2rounds_4way va_mods alg n init1 init2 init3 init4 round_keys in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Aes_2rounds_4way ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 130 column 1 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 157 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 158 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 159 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 13 va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 1)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 160 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 14 va_sM == Vale.AES.AES_s.eval_rounds init4 round_keys (n + 1)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Aes_2rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 1 /\
    Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0
    == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 3 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys n /\ va_get_xmm 4 va_s0 == FStar.Seq.Base.index #quad32
    round_keys (n + 1)) /\ (forall (va_x_xmm2:quad32) (va_x_xmm12:quad32) (va_x_xmm13:quad32)
    (va_x_xmm14:quad32) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_xmm
    14 va_x_xmm14 (va_upd_xmm 13 va_x_xmm13 (va_upd_xmm 12 va_x_xmm12 (va_upd_xmm 2 va_x_xmm2
    va_s0)))) in va_get_ok va_sM /\ (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1
    round_keys (n + 1) /\ va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n +
    1) /\ va_get_xmm 13 va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 1) /\ va_get_xmm
    14 va_sM == Vale.AES.AES_s.eval_rounds init4 round_keys (n + 1)) ==> va_k va_sM (())))


val va_wpProof_Aes_2rounds_4way : alg:algorithm -> n:pos -> init1:quad32 -> init2:quad32 ->
  init3:quad32 -> init4:quad32 -> round_keys:(seq quad32) -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Aes_2rounds_4way ()) ([va_Mod_flags;
    va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Aes_2rounds_4way (va_code_Aes_2rounds_4way ()) va_s0 alg n init1
    init2 init3 init4 round_keys in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM
    (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Aes_2rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit (va_code_Aes_2rounds_4way ())) =
  (va_QProc (va_code_Aes_2rounds_4way ()) ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm
    12; va_Mod_xmm 2]) (va_wp_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys)
    (va_wpProof_Aes_2rounds_4way alg n init1 init2 init3 init4 round_keys))
//--
//-- Aes_3rounds_4way

val va_code_Aes_3rounds_4way : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Aes_3rounds_4way () =
  (va_Block (va_CCons (va_code_Aes_round_4way (va_op_xmm_xmm 4)) (va_CCons (va_code_Aes_round_4way
    (va_op_xmm_xmm 5)) (va_CCons (va_code_Aes_round_4way (va_op_xmm_xmm 6)) (va_CNil ())))))

val va_codegen_success_Aes_3rounds_4way : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Aes_3rounds_4way () =
  (va_pbool_and (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 4)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 5)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 6)) (va_ttrue ()))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Aes_3rounds_4way (va_mods:va_mods_t) (alg:algorithm) (n:pos) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit
  (va_code_Aes_3rounds_4way ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 199 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 0) (va_op_xmm_xmm 4) init1 init2 init3 init4 round_keys)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 200 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 1) (va_op_xmm_xmm 5) init1 init2 init3 init4 round_keys)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 201 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 2) (va_op_xmm_xmm 6) init1 init2 init3 init4 round_keys)
    (va_QEmpty (()))))))


val va_lemma_Aes_3rounds_4way : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> n:pos ->
  init1:quad32 -> init2:quad32 -> init3:quad32 -> init4:quad32 -> round_keys:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Aes_3rounds_4way ()) va_s0 /\ va_get_ok va_s0 /\
    (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 2 /\ Vale.AES.AES_common_s.nr
    alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0 ==
    Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 4 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys (n + 0) /\ va_get_xmm 5 va_s0 == FStar.Seq.Base.index
    #quad32 round_keys (n + 1) /\ va_get_xmm 6 va_s0 == FStar.Seq.Base.index #quad32 round_keys (n
    + 2))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 2) /\ va_get_xmm 12
    va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 2) /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n + 2) /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n + 2)) /\ va_state_eq va_sM (va_update_flags
    va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM (va_update_xmm 12 va_sM (va_update_xmm 2
    va_sM (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Aes_3rounds_4way va_b0 va_s0 alg n init1 init2 init3 init4 round_keys =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm
    2; va_Mod_ok] in
  let va_qc = va_qcode_Aes_3rounds_4way va_mods alg n init1 init2 init3 init4 round_keys in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Aes_3rounds_4way ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 166 column 1 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 194 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 2)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 195 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 2)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 196 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 13 va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 2)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 197 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 14 va_sM == Vale.AES.AES_s.eval_rounds init4 round_keys (n + 2)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Aes_3rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 2 /\
    Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0
    == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 4 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys (n + 0) /\ va_get_xmm 5 va_s0 == FStar.Seq.Base.index
    #quad32 round_keys (n + 1) /\ va_get_xmm 6 va_s0 == FStar.Seq.Base.index #quad32 round_keys (n
    + 2)) /\ (forall (va_x_xmm2:quad32) (va_x_xmm12:quad32) (va_x_xmm13:quad32) (va_x_xmm14:quad32)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_xmm 14 va_x_xmm14
    (va_upd_xmm 13 va_x_xmm13 (va_upd_xmm 12 va_x_xmm12 (va_upd_xmm 2 va_x_xmm2 va_s0)))) in
    va_get_ok va_sM /\ (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 2)
    /\ va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 2) /\ va_get_xmm 13
    va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 2) /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n + 2)) ==> va_k va_sM (())))


val va_wpProof_Aes_3rounds_4way : alg:algorithm -> n:pos -> init1:quad32 -> init2:quad32 ->
  init3:quad32 -> init4:quad32 -> round_keys:(seq quad32) -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Aes_3rounds_4way alg n init1 init2 init3 init4 round_keys
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Aes_3rounds_4way ()) ([va_Mod_flags;
    va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Aes_3rounds_4way alg n init1 init2 init3 init4 round_keys va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Aes_3rounds_4way (va_code_Aes_3rounds_4way ()) va_s0 alg n init1
    init2 init3 init4 round_keys in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM
    (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Aes_3rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit (va_code_Aes_3rounds_4way ())) =
  (va_QProc (va_code_Aes_3rounds_4way ()) ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm
    12; va_Mod_xmm 2]) (va_wp_Aes_3rounds_4way alg n init1 init2 init3 init4 round_keys)
    (va_wpProof_Aes_3rounds_4way alg n init1 init2 init3 init4 round_keys))
//--
//-- Aes_4rounds_4way

val va_code_Aes_4rounds_4way : va_dummy:unit -> Tot va_code
[@ "opaque_to_smt" va_qattr]
let va_code_Aes_4rounds_4way () =
  (va_Block (va_CCons (va_code_Aes_round_4way (va_op_xmm_xmm 3)) (va_CCons (va_code_Aes_round_4way
    (va_op_xmm_xmm 4)) (va_CCons (va_code_Aes_round_4way (va_op_xmm_xmm 5)) (va_CCons
    (va_code_Aes_round_4way (va_op_xmm_xmm 6)) (va_CNil ()))))))

val va_codegen_success_Aes_4rounds_4way : va_dummy:unit -> Tot va_pbool
[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Aes_4rounds_4way () =
  (va_pbool_and (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 3)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 4)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 5)) (va_pbool_and
    (va_codegen_success_Aes_round_4way (va_op_xmm_xmm 6)) (va_ttrue ())))))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Aes_4rounds_4way (va_mods:va_mods_t) (alg:algorithm) (n:pos) (init1:quad32)
  (init2:quad32) (init3:quad32) (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit
  (va_code_Aes_4rounds_4way ())) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 238 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg n (va_op_xmm_xmm 3) init1 init2 init3 init4 round_keys) (va_QSeq
    va_range1
    "***** PRECONDITION NOT MET AT line 239 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 1) (va_op_xmm_xmm 4) init1 init2 init3 init4 round_keys)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 240 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 2) (va_op_xmm_xmm 5) init1 init2 init3 init4 round_keys)
    (va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 241 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_quick_Aes_round_4way alg (n + 3) (va_op_xmm_xmm 6) init1 init2 init3 init4 round_keys)
    (va_QEmpty (())))))))


val va_lemma_Aes_4rounds_4way : va_b0:va_code -> va_s0:va_state -> alg:algorithm -> n:pos ->
  init1:quad32 -> init2:quad32 -> init3:quad32 -> init4:quad32 -> round_keys:(seq quad32)
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Aes_4rounds_4way ()) va_s0 /\ va_get_ok va_s0 /\
    (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 3 /\ Vale.AES.AES_common_s.nr
    alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0 ==
    Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 3 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys n /\ va_get_xmm 4 va_s0 == FStar.Seq.Base.index #quad32
    round_keys (n + 1) /\ va_get_xmm 5 va_s0 == FStar.Seq.Base.index #quad32 round_keys (n + 2) /\
    va_get_xmm 6 va_s0 == FStar.Seq.Base.index #quad32 round_keys (n + 3))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 3) /\ va_get_xmm 12
    va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 3) /\ va_get_xmm 13 va_sM ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n + 3) /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n + 3)) /\ va_state_eq va_sM (va_update_flags
    va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM (va_update_xmm 12 va_sM (va_update_xmm 2
    va_sM (va_update_ok va_sM va_s0))))))))
[@"opaque_to_smt"]
let va_lemma_Aes_4rounds_4way va_b0 va_s0 alg n init1 init2 init3 init4 round_keys =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm
    2; va_Mod_ok] in
  let va_qc = va_qcode_Aes_4rounds_4way va_mods alg n init1 init2 init3 init4 round_keys in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Aes_4rounds_4way ()) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 204 column 1 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_ok va_sM) /\ (label va_range1
    "***** POSTCONDITION NOT MET AT line 233 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 3)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 234 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 3)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 235 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 13 va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 3)) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 236 column 54 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
    (va_get_xmm 14 va_sM == Vale.AES.AES_s.eval_rounds init4 round_keys (n + 3)))) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2;
    va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)

[@ va_qattr]
let va_wp_Aes_4rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (aesni_enabled /\ (1 <= n /\ n < Vale.AES.AES_common_s.nr alg - 3 /\
    Vale.AES.AES_common_s.nr alg <= FStar.Seq.Base.length #quad32 round_keys) /\ va_get_xmm 2 va_s0
    == Vale.AES.AES_s.eval_rounds init1 round_keys (n - 1) /\ va_get_xmm 12 va_s0 ==
    Vale.AES.AES_s.eval_rounds init2 round_keys (n - 1) /\ va_get_xmm 13 va_s0 ==
    Vale.AES.AES_s.eval_rounds init3 round_keys (n - 1) /\ va_get_xmm 14 va_s0 ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n - 1) /\ va_get_xmm 3 va_s0 ==
    FStar.Seq.Base.index #quad32 round_keys n /\ va_get_xmm 4 va_s0 == FStar.Seq.Base.index #quad32
    round_keys (n + 1) /\ va_get_xmm 5 va_s0 == FStar.Seq.Base.index #quad32 round_keys (n + 2) /\
    va_get_xmm 6 va_s0 == FStar.Seq.Base.index #quad32 round_keys (n + 3)) /\ (forall
    (va_x_xmm2:quad32) (va_x_xmm12:quad32) (va_x_xmm13:quad32) (va_x_xmm14:quad32)
    (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_xmm 14 va_x_xmm14
    (va_upd_xmm 13 va_x_xmm13 (va_upd_xmm 12 va_x_xmm12 (va_upd_xmm 2 va_x_xmm2 va_s0)))) in
    va_get_ok va_sM /\ (va_get_xmm 2 va_sM == Vale.AES.AES_s.eval_rounds init1 round_keys (n + 3)
    /\ va_get_xmm 12 va_sM == Vale.AES.AES_s.eval_rounds init2 round_keys (n + 3) /\ va_get_xmm 13
    va_sM == Vale.AES.AES_s.eval_rounds init3 round_keys (n + 3) /\ va_get_xmm 14 va_sM ==
    Vale.AES.AES_s.eval_rounds init4 round_keys (n + 3)) ==> va_k va_sM (())))


val va_wpProof_Aes_4rounds_4way : alg:algorithm -> n:pos -> init1:quad32 -> init2:quad32 ->
  init3:quad32 -> init4:quad32 -> round_keys:(seq quad32) -> va_s0:va_state -> va_k:(va_state ->
  unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Aes_4rounds_4way alg n init1 init2 init3 init4 round_keys
    va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Aes_4rounds_4way ()) ([va_Mod_flags;
    va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@"opaque_to_smt"]
let va_wpProof_Aes_4rounds_4way alg n init1 init2 init3 init4 round_keys va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Aes_4rounds_4way (va_code_Aes_4rounds_4way ()) va_s0 alg n init1
    init2 init3 init4 round_keys in
  va_lemma_upd_update va_sM;
  assert (va_state_eq va_sM (va_update_flags va_sM (va_update_xmm 14 va_sM (va_update_xmm 13 va_sM
    (va_update_xmm 12 va_sM (va_update_xmm 2 va_sM (va_update_ok va_sM va_s0)))))));
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm 12; va_Mod_xmm 2])
    va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

[@ "opaque_to_smt" va_qattr]
let va_quick_Aes_4rounds_4way (alg:algorithm) (n:pos) (init1:quad32) (init2:quad32) (init3:quad32)
  (init4:quad32) (round_keys:(seq quad32)) : (va_quickCode unit (va_code_Aes_4rounds_4way ())) =
  (va_QProc (va_code_Aes_4rounds_4way ()) ([va_Mod_flags; va_Mod_xmm 14; va_Mod_xmm 13; va_Mod_xmm
    12; va_Mod_xmm 2]) (va_wp_Aes_4rounds_4way alg n init1 init2 init3 init4 round_keys)
    (va_wpProof_Aes_4rounds_4way alg n init1 init2 init3 init4 round_keys))
//--
//-- Aes_ctr_encrypt

[@ "opaque_to_smt" va_qattr]
let va_code_Aes_ctr_encrypt alg =
  (va_Block (va_CCons (va_code_Aes_3rounds_4way ()) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64 rR8) 64 Secret)
    (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4)
    (va_op_reg_opr64_reg64 rR8) 80 Secret) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64 rR8) 96 Secret)
    (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 6)
    (va_op_reg_opr64_reg64 rR8) 112 Secret) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_Block
    (va_CNil ())) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (va_code_Aes_4rounds_4way ()) (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_xmm_xmm 3) (va_op_reg_opr64_reg64 rR8) 128 Secret) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64 rR8) 144 Secret)
    (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5)
    (va_op_reg_opr64_reg64 rR8) 160 Secret) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_Block
    (va_CNil ())) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_code_Aes_2rounds_4way ())
    (va_CCons (if (alg = AES_256) then va_Block (va_CCons (va_code_Mov128 (va_op_xmm_xmm 3)
    (va_op_xmm_xmm 5)) (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64 rR8) 176 Secret) (va_CCons (va_code_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64 rR8) 192 Secret)
    (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 6)
    (va_op_reg_opr64_reg64 rR8) 208 Secret) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_Block
    (va_CNil ())) (va_CCons (va_Block (va_CNil ())) (va_CCons (va_Block (va_CNil ())) (va_CCons
    (va_code_Aes_4rounds_4way ()) (va_CCons (va_code_Load128_buffer (va_op_heaplet_mem_heaplet 0)
    (va_op_xmm_xmm 5) (va_op_reg_opr64_reg64 rR8) 224 Secret) (va_CCons (va_Block (va_CNil ()))
    (va_CNil ())))))))))))) else va_Block (va_CNil ())) (va_CCons (va_code_AESNI_enc_last
    (va_op_xmm_xmm 2) (va_op_xmm_xmm 5)) (va_CCons (va_code_AESNI_enc_last (va_op_xmm_xmm 12)
    (va_op_xmm_xmm 5)) (va_CCons (va_code_AESNI_enc_last (va_op_xmm_xmm 13) (va_op_xmm_xmm 5))
    (va_CCons (va_code_AESNI_enc_last (va_op_xmm_xmm 14) (va_op_xmm_xmm 5)) (va_CNil
    ()))))))))))))))))))))))))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Aes_ctr_encrypt alg =
  (va_pbool_and (va_codegen_success_Aes_3rounds_4way ()) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3)
    (va_op_reg_opr64_reg64 rR8) 64 Secret) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64 rR8) 80 Secret)
    (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm
    5) (va_op_reg_opr64_reg64 rR8) 96 Secret) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 6) (va_op_reg_opr64_reg64 rR8) 112 Secret)
    (va_pbool_and (va_codegen_success_Aes_4rounds_4way ()) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 3)
    (va_op_reg_opr64_reg64 rR8) 128 Secret) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64 rR8) 144 Secret)
    (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm
    5) (va_op_reg_opr64_reg64 rR8) 160 Secret) (va_pbool_and (va_codegen_success_Aes_2rounds_4way
    ()) (va_pbool_and (if (alg = AES_256) then va_pbool_and (va_codegen_success_Mov128
    (va_op_xmm_xmm 3) (va_op_xmm_xmm 5)) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 4) (va_op_reg_opr64_reg64 rR8) 176 Secret)
    (va_pbool_and (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm
    5) (va_op_reg_opr64_reg64 rR8) 192 Secret) (va_pbool_and (va_codegen_success_Load128_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 6) (va_op_reg_opr64_reg64 rR8) 208 Secret)
    (va_pbool_and (va_codegen_success_Aes_4rounds_4way ()) (va_pbool_and
    (va_codegen_success_Load128_buffer (va_op_heaplet_mem_heaplet 0) (va_op_xmm_xmm 5)
    (va_op_reg_opr64_reg64 rR8) 224 Secret) (va_ttrue ())))))) else va_ttrue ()) (va_pbool_and
    (va_codegen_success_AESNI_enc_last (va_op_xmm_xmm 2) (va_op_xmm_xmm 5)) (va_pbool_and
    (va_codegen_success_AESNI_enc_last (va_op_xmm_xmm 12) (va_op_xmm_xmm 5)) (va_pbool_and
    (va_codegen_success_AESNI_enc_last (va_op_xmm_xmm 13) (va_op_xmm_xmm 5)) (va_pbool_and
    (va_codegen_success_AESNI_enc_last (va_op_xmm_xmm 14) (va_op_xmm_xmm 5)) (va_ttrue
    ()))))))))))))))))
/
Vale.X64.State.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsVector.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.InsAes.fsti.checked Vale.X64.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Poly1305.Math.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.AES.X64.GHash.fsti.checked Vale.AES.GHash.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked Vale.AES.AES_helpers.fsti.checked Vale.AES.AES_common_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.X64.AESCTR.fst

    va_mods: Vale.X64.QuickCode.va_mods_t ->
    alg: Vale.AES.AES_common_s.algorithm ->
    key: FStar.Seq.Base.seq Vale.X64.Memory.nat32 ->
    round_keys: FStar.Seq.Base.seq Vale.X64.Decls.quad32 ->
    keys_b: Vale.X64.Memory.buffer128 ->
    in1: Vale.X64.Decls.quad32 ->
    in2: Vale.X64.Decls.quad32 ->
    in3: Vale.X64.Decls.quad32 ->
    in4: Vale.X64.Decls.quad32
  -> Vale.X64.QuickCode.va_quickCode Prims.unit (Vale.AES.X64.AESCTR.va_code_Aes_ctr_encrypt alg)
Vale.X64.QuickCode.va_mods_t Vale.AES.AES_common_s.algorithm FStar.Seq.Base.seq Vale.X64.Memory.nat32 Vale.X64.Decls.quad32 Vale.X64.Memory.buffer128 Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.AES.X64.AESCTR.va_code_Aes_3rounds_4way Vale.X64.InsVector.va_code_Load128_buffer Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_xmm_xmm Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rR8 Vale.Arch.HeapTypes_s.Secret Vale.X64.Machine_s.Block Vale.X64.Decls.ins Vale.X64.Decls.ocmp Prims.Nil Vale.X64.Machine_s.precode Vale.AES.X64.AESCTR.va_code_Aes_4rounds_4way Vale.AES.X64.AESCTR.va_code_Aes_2rounds_4way Vale.X64.QuickCodes.if_code Prims.op_Equality Vale.AES.AES_common_s.AES_256 Vale.X64.QuickCodes.block Vale.X64.InsVector.va_code_Mov128 Vale.X64.InsAes.va_code_AESNI_enc_last Vale.X64.Decls.va_state Vale.X64.QuickCodes.va_qPURE Prims.pure_post Prims.l_and Prims.l_True Prims.l_Forall Prims.l_imp Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length Vale.Def.Types_s.quad32 Prims.eq2 Vale.AES.AES_s.eval_rounds Vale.X64.QuickCodes.va_range1 Vale.AES.AES_helpers.init_rounds_opaque Vale.X64.QuickCodes.va_QSeq Vale.AES.X64.AESCTR.va_quick_Aes_3rounds_4way Vale.X64.Decls.va_get_xmm Vale.X64.InsVector.va_quick_Load128_buffer Vale.X64.QuickCodes.va_QBind Vale.X64.QuickCodes.va_qAssertSquash Prims.op_LessThan Prims.nat Prims.squash Vale.X64.QuickCodes.va_qAssert FStar.Seq.Base.index Vale.AES.X64.AESCTR.va_quick_Aes_4rounds_4way Vale.AES.X64.AESCTR.va_quick_Aes_2rounds_4way Vale.X64.QuickCodes.va_qInlineIf Vale.X64.InsVector.va_quick_Mov128 Vale.X64.QuickCodes.va_QEmpty Vale.X64.QuickCodes.quickCodes Vale.X64.InsAes.va_quick_AESNI_enc_last Prims.int Prims.op_Addition Vale.Def.Types_s.quad32_xor Vale.AES.AES_common_s.sub_bytes Vale.AES.AES_s.shift_rows_LE Prims.op_Subtraction Vale.AES.AES_s.eval_cipher Vale.AES.AES_helpers.finish_cipher Vale.X64.QuickCodes.va_QLemma Vale.AES.AES_s.is_aes_key_LE Vale.AES.AES_s.aes_encrypt_LE Vale.AES.AES_s.key_to_round_keys_LE Vale.AES.X64.AESCTR.finish_aes_encrypt_le Vale.X64.State.vale_state Vale.X64.QuickCode.va_quickCode Vale.AES.X64.AESCTR.va_code_Aes_ctr_encrypt
let va_qcode_Aes_ctr_encrypt
      (va_mods: va_mods_t)
      (alg: algorithm)
      (key: (seq nat32))
      (round_keys: (seq quad32))
      (keys_b: buffer128)
      (in1 in2 in3 in4: quad32)
    : (va_quickCode unit (va_code_Aes_ctr_encrypt alg)) =
  
(qblock va_mods
    (fun (va_s: va_state) ->
        let va_old_s:va_state = va_s in
        let va_arg89:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32) = round_keys in
        let va_arg88:Vale.Def.Types_s.quad32 = va_get_xmm 2 va_old_s in
        va_qPURE va_range1
          "***** PRECONDITION NOT MET AT line 286 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
          (fun (_: unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg88 va_arg89)
          (let va_arg87:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32) = round_keys in
            let va_arg86:Vale.Def.Types_s.quad32 = va_get_xmm 12 va_old_s in
            va_qPURE va_range1
              "***** PRECONDITION NOT MET AT line 287 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
              (fun (_: unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg86 va_arg87)
              (let va_arg85:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32) = round_keys in
                let va_arg84:Vale.Def.Types_s.quad32 = va_get_xmm 13 va_old_s in
                va_qPURE va_range1
                  "***** PRECONDITION NOT MET AT line 288 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                  (fun (_: unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg84 va_arg85)
                  (let va_arg83:(FStar.Seq.Base.seq Vale.Def.Types_s.quad32) = round_keys in
                    let va_arg82:Vale.Def.Types_s.quad32 = va_get_xmm 14 va_old_s in
                    va_qPURE va_range1
                      "***** PRECONDITION NOT MET AT line 289 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                      (fun (_: unit) -> Vale.AES.AES_helpers.init_rounds_opaque va_arg82 va_arg83)
                      (va_QSeq va_range1
                          "***** PRECONDITION NOT MET AT line 291 column 21 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                          (va_quick_Aes_3rounds_4way alg
                              1
                              (va_get_xmm 2 va_old_s)
                              (va_get_xmm 12 va_old_s)
                              (va_get_xmm 13 va_old_s)
                              (va_get_xmm 14 va_old_s)
                              round_keys)
                          (va_QSeq va_range1
                              "***** PRECONDITION NOT MET AT line 294 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                              (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0)
                                  (va_op_xmm_xmm 3)
                                  (va_op_reg_opr64_reg64 rR8)
                                  64
                                  Secret
                                  keys_b
                                  4)
                              (va_QSeq va_range1
                                  "***** PRECONDITION NOT MET AT line 295 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                  (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0)
                                      (va_op_xmm_xmm 4)
                                      (va_op_reg_opr64_reg64 rR8)
                                      80
                                      Secret
                                      keys_b
                                      5)
                                  (va_QSeq va_range1
                                      "***** PRECONDITION NOT MET AT line 296 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                      (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0)
                                          (va_op_xmm_xmm 5)
                                          (va_op_reg_opr64_reg64 rR8)
                                          96
                                          Secret
                                          keys_b
                                          6)
                                      (va_QBind va_range1
                                          "***** PRECONDITION NOT MET AT line 297 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                          (va_quick_Load128_buffer (va_op_heaplet_mem_heaplet 0)
                                              (va_op_xmm_xmm 6)
                                              (va_op_reg_opr64_reg64 rR8)
                                              112
                                              Secret
                                              keys_b
                                              7)
                                          (fun (va_s: va_state) _ ->
                                              va_qAssertSquash va_range1
                                                "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 298 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                ((fun
                                                      a_539
                                                      (s_540: (FStar.Seq.Base.seq a_539))
                                                      (i_541: Prims.nat)
                                                      ->
                                                      let i_515:Prims.nat = i_541 in
                                                      Prims.b2t (Prims.op_LessThan i_515
                                                            (FStar.Seq.Base.length #a_539 s_540))) quad32
                                                    round_keys
                                                    4)
                                                (fun _ ->
                                                    va_qAssert va_range1
                                                      "***** PRECONDITION NOT MET AT line 298 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                      (va_get_xmm 3 va_s ==
                                                        FStar.Seq.Base.index #quad32 round_keys 4)
                                                      (va_qAssertSquash va_range1
                                                          "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 299 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                          ((fun
                                                                a_539
                                                                (s_540: (FStar.Seq.Base.seq a_539))
                                                                (i_541: Prims.nat)
                                                                ->
                                                                let i_515:Prims.nat = i_541 in
                                                                Prims.b2t (Prims.op_LessThan i_515
                                                                      (FStar.Seq.Base.length #a_539
                                                                          s_540))) quad32
                                                              round_keys
                                                              5)
                                                          (fun _ ->
                                                              va_qAssert va_range1
                                                                "***** PRECONDITION NOT MET AT line 299 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                (va_get_xmm 4 va_s ==
                                                                  FStar.Seq.Base.index #quad32
                                                                    round_keys
                                                                    5)
                                                                (va_qAssertSquash va_range1
                                                                    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 300 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                    ((fun
                                                                          a_539
                                                                          (s_540:
                                                                            (FStar.Seq.Base.seq a_539
                                                                              ))
                                                                          (i_541: Prims.nat)
                                                                          ->
                                                                          let i_515:Prims.nat =
                                                                            i_541
                                                                          in
                                                                          Prims.b2t (Prims.op_LessThan
                                                                                i_515
                                                                                (FStar.Seq.Base.length
                                                                                    #a_539
                                                                                    s_540))) quad32
                                                                        round_keys
                                                                        6)
                                                                    (fun _ ->
                                                                        va_qAssert va_range1
                                                                          "***** PRECONDITION NOT MET AT line 300 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                          (va_get_xmm 5 va_s ==
                                                                            FStar.Seq.Base.index #quad32
                                                                              round_keys
                                                                              6)
                                                                          (va_qAssertSquash va_range1
                                                                              "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 301 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                              ((fun
                                                                                    a_539
                                                                                    (s_540:
                                                                                      (FStar.Seq.Base.seq
                                                                                          a_539))
                                                                                    (i_541:
                                                                                      Prims.nat)
                                                                                    ->
                                                                                    let i_515:Prims.nat
                                                                                    =
                                                                                      i_541
                                                                                    in
                                                                                    Prims.b2t (Prims.op_LessThan
                                                                                          i_515
                                                                                          (FStar.Seq.Base.length
                                                                                              #a_539
                                                                                              s_540)
                                                                                      )) quad32
                                                                                  round_keys
                                                                                  7)
                                                                              (fun _ ->
                                                                                  va_qAssert va_range1
                                                                                    "***** PRECONDITION NOT MET AT line 301 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                    (va_get_xmm 6
                                                                                        va_s ==
                                                                                      FStar.Seq.Base.index
                                                                                        #quad32
                                                                                        round_keys
                                                                                        7)
                                                                                    (va_QSeq va_range1
                                                                                        "***** PRECONDITION NOT MET AT line 304 column 21 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                        (va_quick_Aes_4rounds_4way
                                                                                            alg
                                                                                            4
                                                                                            (va_get_xmm
                                                                                                2
                                                                                                va_old_s
                                                                                              )
                                                                                            (va_get_xmm
                                                                                                12
                                                                                                va_old_s
                                                                                              )
                                                                                            (va_get_xmm
                                                                                                13
                                                                                                va_old_s
                                                                                              )
                                                                                            (va_get_xmm
                                                                                                14
                                                                                                va_old_s
                                                                                              )
                                                                                            round_keys
                                                                                          )
                                                                                        (va_QSeq va_range1
                                                                                            "***** PRECONDITION NOT MET AT line 307 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                            (va_quick_Load128_buffer
                                                                                                (va_op_heaplet_mem_heaplet
                                                                                                    0
                                                                                                  )
                                                                                                (va_op_xmm_xmm
                                                                                                    3
                                                                                                  )
                                                                                                (va_op_reg_opr64_reg64
                                                                                                    rR8
                                                                                                  )
                                                                                                128
                                                                                                Secret
                                                                                                keys_b
                                                                                                8)
                                                                                            (va_QSeq
                                                                                                va_range1
                                                                                                "***** PRECONDITION NOT MET AT line 308 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                (va_quick_Load128_buffer
                                                                                                    (
                                                                                                      va_op_heaplet_mem_heaplet
                                                                                                        0

                                                                                                    )
                                                                                                    (
                                                                                                      va_op_xmm_xmm
                                                                                                        4

                                                                                                    )
                                                                                                    (
                                                                                                      va_op_reg_opr64_reg64
                                                                                                        rR8

                                                                                                    )
                                                                                                    144
                                                                                                    Secret
                                                                                                    keys_b
                                                                                                    9
                                                                                                  )
                                                                                                (va_QBind
                                                                                                    va_range1
                                                                                                    "***** PRECONDITION NOT MET AT line 309 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                    (
                                                                                                      va_quick_Load128_buffer
                                                                                                        (
                                                                                                          va_op_heaplet_mem_heaplet
                                                                                                            0

                                                                                                        )
                                                                                                        (
                                                                                                          va_op_xmm_xmm
                                                                                                            5

                                                                                                        )
                                                                                                        (
                                                                                                          va_op_reg_opr64_reg64
                                                                                                            rR8

                                                                                                        )
                                                                                                        160
                                                                                                        Secret
                                                                                                        keys_b
                                                                                                        10

                                                                                                    )
                                                                                                    (
                                                                                                      fun
                                                                                                        (
                                                                                                          va_s:
                                                                                                          va_state
                                                                                                        )
                                                                                                        _
                                                                                                        ->
                                                                                                        va_qAssertSquash
                                                                                                          va_range1
                                                                                                          "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 310 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                          (
                                                                                                            (
                                                                                                              fun
                                                                                                                a_539
                                                                                                                (
                                                                                                                  s_540:
                                                                                                                  (
                                                                                                                    FStar.Seq.Base.seq
                                                                                                                      a_539

                                                                                                                  )
                                                                                                                )
                                                                                                                (
                                                                                                                  i_541:
                                                                                                                  Prims.nat
                                                                                                                )
                                                                                                                ->
                                                                                                                let
                                                                                                                i_515:Prims.nat
                                                                                                                =
                                                                                                                  i_541
                                                                                                                in
                                                                                                                Prims.b2t
                                                                                                                  (
                                                                                                                    Prims.op_LessThan
                                                                                                                      i_515
                                                                                                                      (
                                                                                                                        FStar.Seq.Base.length
                                                                                                                          #a_539
                                                                                                                          s_540

                                                                                                                      )

                                                                                                                  )

                                                                                                            )
                                                                                                              quad32
                                                                                                              round_keys
                                                                                                              8

                                                                                                          )
                                                                                                          (
                                                                                                            fun
                                                                                                              _
                                                                                                              ->
                                                                                                              va_qAssert
                                                                                                                va_range1
                                                                                                                "***** PRECONDITION NOT MET AT line 310 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                (
                                                                                                                  va_get_xmm
                                                                                                                    3
                                                                                                                    va_s
                                                                                                                   ==
                                                                                                                  FStar.Seq.Base.index
                                                                                                                    #quad32
                                                                                                                    round_keys
                                                                                                                    8

                                                                                                                )
                                                                                                                (
                                                                                                                  va_qAssertSquash
                                                                                                                    va_range1
                                                                                                                    "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 311 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                    (
                                                                                                                      (
                                                                                                                        fun
                                                                                                                          a_539
                                                                                                                          (
                                                                                                                            s_540:
                                                                                                                            (
                                                                                                                              FStar.Seq.Base.seq
                                                                                                                                a_539

                                                                                                                            )
                                                                                                                          )
                                                                                                                          (
                                                                                                                            i_541:
                                                                                                                            Prims.nat
                                                                                                                          )
                                                                                                                          ->
                                                                                                                          let
                                                                                                                          i_515:Prims.nat
                                                                                                                          =
                                                                                                                            i_541
                                                                                                                          in
                                                                                                                          Prims.b2t
                                                                                                                            (
                                                                                                                              Prims.op_LessThan
                                                                                                                                i_515
                                                                                                                                (
                                                                                                                                  FStar.Seq.Base.length
                                                                                                                                    #a_539
                                                                                                                                    s_540

                                                                                                                                )

                                                                                                                            )

                                                                                                                      )
                                                                                                                        quad32
                                                                                                                        round_keys
                                                                                                                        9

                                                                                                                    )
                                                                                                                    (
                                                                                                                      fun
                                                                                                                        _
                                                                                                                        ->
                                                                                                                        va_qAssert
                                                                                                                          va_range1
                                                                                                                          "***** PRECONDITION NOT MET AT line 311 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                          (
                                                                                                                            va_get_xmm
                                                                                                                              4
                                                                                                                              va_s
                                                                                                                             ==
                                                                                                                            FStar.Seq.Base.index
                                                                                                                              #quad32
                                                                                                                              round_keys
                                                                                                                              9

                                                                                                                          )
                                                                                                                          (
                                                                                                                            va_qAssertSquash
                                                                                                                              va_range1
                                                                                                                              "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 312 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                              (
                                                                                                                                (
                                                                                                                                  fun
                                                                                                                                    a_539
                                                                                                                                    (
                                                                                                                                      s_540:
                                                                                                                                      (
                                                                                                                                        FStar.Seq.Base.seq
                                                                                                                                          a_539

                                                                                                                                      )
                                                                                                                                    )
                                                                                                                                    (
                                                                                                                                      i_541:
                                                                                                                                      Prims.nat
                                                                                                                                    )
                                                                                                                                    ->
                                                                                                                                    let
                                                                                                                                    i_515:Prims.nat
                                                                                                                                    =
                                                                                                                                      i_541
                                                                                                                                    in
                                                                                                                                    Prims.b2t
                                                                                                                                      (
                                                                                                                                        Prims.op_LessThan
                                                                                                                                          i_515
                                                                                                                                          (
                                                                                                                                            FStar.Seq.Base.length
                                                                                                                                              #a_539
                                                                                                                                              s_540

                                                                                                                                          )

                                                                                                                                      )

                                                                                                                                )
                                                                                                                                  quad32
                                                                                                                                  round_keys
                                                                                                                                  10

                                                                                                                              )
                                                                                                                              (
                                                                                                                                fun
                                                                                                                                  _
                                                                                                                                  ->
                                                                                                                                  va_qAssert
                                                                                                                                    va_range1
                                                                                                                                    "***** PRECONDITION NOT MET AT line 312 column 5 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                    (
                                                                                                                                      va_get_xmm
                                                                                                                                        5
                                                                                                                                        va_s
                                                                                                                                       ==
                                                                                                                                      FStar.Seq.Base.index
                                                                                                                                        #quad32
                                                                                                                                        round_keys
                                                                                                                                        10

                                                                                                                                    )
                                                                                                                                    (
                                                                                                                                      va_QBind
                                                                                                                                        va_range1
                                                                                                                                        "***** PRECONDITION NOT MET AT line 315 column 21 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                        (
                                                                                                                                          va_quick_Aes_2rounds_4way
                                                                                                                                            alg
                                                                                                                                            8
                                                                                                                                            (
                                                                                                                                              va_get_xmm
                                                                                                                                                2
                                                                                                                                                va_old_s

                                                                                                                                            )
                                                                                                                                            (
                                                                                                                                              va_get_xmm
                                                                                                                                                12
                                                                                                                                                va_old_s

                                                                                                                                            )
                                                                                                                                            (
                                                                                                                                              va_get_xmm
                                                                                                                                                13
                                                                                                                                                va_old_s

                                                                                                                                            )
                                                                                                                                            (
                                                                                                                                              va_get_xmm
                                                                                                                                                14
                                                                                                                                                va_old_s

                                                                                                                                            )
                                                                                                                                            round_keys

                                                                                                                                        )
                                                                                                                                        (
                                                                                                                                          fun
                                                                                                                                            (
                                                                                                                                              va_s:
                                                                                                                                              va_state
                                                                                                                                            )
                                                                                                                                            _
                                                                                                                                            ->
                                                                                                                                            va_QBind
                                                                                                                                              va_range1
                                                                                                                                              "***** PRECONDITION NOT MET AT line 318 column 15 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                              (
                                                                                                                                                va_qInlineIf
                                                                                                                                                  va_mods
                                                                                                                                                  (
                                                                                                                                                    alg =
                                                                                                                                                    AES_256
                                                                                                                                                  )
                                                                                                                                                  (
                                                                                                                                                    qblock
                                                                                                                                                      va_mods
                                                                                                                                                      (
                                                                                                                                                        fun
                                                                                                                                                          (
                                                                                                                                                            va_s:
                                                                                                                                                            va_state
                                                                                                                                                          )
                                                                                                                                                          ->
                                                                                                                                                          va_QSeq
                                                                                                                                                            va_range1
                                                                                                                                                            "***** PRECONDITION NOT MET AT line 320 column 15 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                            (
                                                                                                                                                              va_quick_Mov128
                                                                                                                                                                (
                                                                                                                                                                  va_op_xmm_xmm
                                                                                                                                                                    3

                                                                                                                                                                )
                                                                                                                                                                (
                                                                                                                                                                  va_op_xmm_xmm
                                                                                                                                                                    5

                                                                                                                                                                )

                                                                                                                                                            )
                                                                                                                                                            (
                                                                                                                                                              va_QSeq
                                                                                                                                                                va_range1
                                                                                                                                                                "***** PRECONDITION NOT MET AT line 321 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                (
                                                                                                                                                                  va_quick_Load128_buffer
                                                                                                                                                                    (
                                                                                                                                                                      va_op_heaplet_mem_heaplet
                                                                                                                                                                        0

                                                                                                                                                                    )
                                                                                                                                                                    (
                                                                                                                                                                      va_op_xmm_xmm
                                                                                                                                                                        4

                                                                                                                                                                    )
                                                                                                                                                                    (
                                                                                                                                                                      va_op_reg_opr64_reg64
                                                                                                                                                                        rR8

                                                                                                                                                                    )
                                                                                                                                                                    176
                                                                                                                                                                    Secret
                                                                                                                                                                    keys_b
                                                                                                                                                                    11

                                                                                                                                                                )
                                                                                                                                                                (
                                                                                                                                                                  va_QSeq
                                                                                                                                                                    va_range1
                                                                                                                                                                    "***** PRECONDITION NOT MET AT line 322 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                    (
                                                                                                                                                                      va_quick_Load128_buffer
                                                                                                                                                                        (
                                                                                                                                                                          va_op_heaplet_mem_heaplet
                                                                                                                                                                            0

                                                                                                                                                                        )
                                                                                                                                                                        (
                                                                                                                                                                          va_op_xmm_xmm
                                                                                                                                                                            5

                                                                                                                                                                        )
                                                                                                                                                                        (
                                                                                                                                                                          va_op_reg_opr64_reg64
                                                                                                                                                                            rR8

                                                                                                                                                                        )
                                                                                                                                                                        192
                                                                                                                                                                        Secret
                                                                                                                                                                        keys_b
                                                                                                                                                                        12

                                                                                                                                                                    )
                                                                                                                                                                    (
                                                                                                                                                                      va_QBind
                                                                                                                                                                        va_range1
                                                                                                                                                                        "***** PRECONDITION NOT MET AT line 323 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                        (
                                                                                                                                                                          va_quick_Load128_buffer
                                                                                                                                                                            (
                                                                                                                                                                              va_op_heaplet_mem_heaplet
                                                                                                                                                                                0

                                                                                                                                                                            )
                                                                                                                                                                            (
                                                                                                                                                                              va_op_xmm_xmm
                                                                                                                                                                                6

                                                                                                                                                                            )
                                                                                                                                                                            (
                                                                                                                                                                              va_op_reg_opr64_reg64
                                                                                                                                                                                rR8

                                                                                                                                                                            )
                                                                                                                                                                            208
                                                                                                                                                                            Secret
                                                                                                                                                                            keys_b
                                                                                                                                                                            13

                                                                                                                                                                        )
                                                                                                                                                                        (
                                                                                                                                                                          fun
                                                                                                                                                                            (
                                                                                                                                                                              va_s:
                                                                                                                                                                              va_state
                                                                                                                                                                            )
                                                                                                                                                                            _
                                                                                                                                                                            ->
                                                                                                                                                                            va_qAssertSquash
                                                                                                                                                                              va_range1
                                                                                                                                                                              "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 324 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                              (
                                                                                                                                                                                (
                                                                                                                                                                                  fun
                                                                                                                                                                                    a_539
                                                                                                                                                                                    (
                                                                                                                                                                                      s_540:
                                                                                                                                                                                      (
                                                                                                                                                                                        FStar.Seq.Base.seq
                                                                                                                                                                                          a_539

                                                                                                                                                                                      )
                                                                                                                                                                                    )
                                                                                                                                                                                    (
                                                                                                                                                                                      i_541:
                                                                                                                                                                                      Prims.nat
                                                                                                                                                                                    )
                                                                                                                                                                                    ->
                                                                                                                                                                                    let
                                                                                                                                                                                    i_515:Prims.nat
                                                                                                                                                                                    =
                                                                                                                                                                                      i_541
                                                                                                                                                                                    in
                                                                                                                                                                                    Prims.b2t
                                                                                                                                                                                      (
                                                                                                                                                                                        Prims.op_LessThan
                                                                                                                                                                                          i_515
                                                                                                                                                                                          (
                                                                                                                                                                                            FStar.Seq.Base.length
                                                                                                                                                                                              #a_539
                                                                                                                                                                                              s_540

                                                                                                                                                                                          )

                                                                                                                                                                                      )

                                                                                                                                                                                )
                                                                                                                                                                                  quad32
                                                                                                                                                                                  round_keys
                                                                                                                                                                                  10

                                                                                                                                                                              )
                                                                                                                                                                              (
                                                                                                                                                                                fun
                                                                                                                                                                                  _
                                                                                                                                                                                  ->
                                                                                                                                                                                  va_qAssert
                                                                                                                                                                                    va_range1
                                                                                                                                                                                    "***** PRECONDITION NOT MET AT line 324 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                    (
                                                                                                                                                                                      va_get_xmm
                                                                                                                                                                                        3
                                                                                                                                                                                        va_s
                                                                                                                                                                                       ==
                                                                                                                                                                                      FStar.Seq.Base.index
                                                                                                                                                                                        #quad32
                                                                                                                                                                                        round_keys
                                                                                                                                                                                        10

                                                                                                                                                                                    )
                                                                                                                                                                                    (
                                                                                                                                                                                      va_qAssertSquash
                                                                                                                                                                                        va_range1
                                                                                                                                                                                        "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 325 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                        (
                                                                                                                                                                                          (
                                                                                                                                                                                            fun
                                                                                                                                                                                              a_539
                                                                                                                                                                                              (
                                                                                                                                                                                                s_540:
                                                                                                                                                                                                (
                                                                                                                                                                                                  FStar.Seq.Base.seq
                                                                                                                                                                                                    a_539

                                                                                                                                                                                                )
                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                i_541:
                                                                                                                                                                                                Prims.nat
                                                                                                                                                                                              )
                                                                                                                                                                                              ->
                                                                                                                                                                                              let
                                                                                                                                                                                              i_515:Prims.nat
                                                                                                                                                                                              =
                                                                                                                                                                                                i_541
                                                                                                                                                                                              in
                                                                                                                                                                                              Prims.b2t
                                                                                                                                                                                                (
                                                                                                                                                                                                  Prims.op_LessThan
                                                                                                                                                                                                    i_515
                                                                                                                                                                                                    (
                                                                                                                                                                                                      FStar.Seq.Base.length
                                                                                                                                                                                                        #a_539
                                                                                                                                                                                                        s_540

                                                                                                                                                                                                    )

                                                                                                                                                                                                )

                                                                                                                                                                                          )
                                                                                                                                                                                            quad32
                                                                                                                                                                                            round_keys
                                                                                                                                                                                            11

                                                                                                                                                                                        )
                                                                                                                                                                                        (
                                                                                                                                                                                          fun
                                                                                                                                                                                            _
                                                                                                                                                                                            ->
                                                                                                                                                                                            va_qAssert
                                                                                                                                                                                              va_range1
                                                                                                                                                                                              "***** PRECONDITION NOT MET AT line 325 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                              (
                                                                                                                                                                                                va_get_xmm
                                                                                                                                                                                                  4
                                                                                                                                                                                                  va_s
                                                                                                                                                                                                 ==
                                                                                                                                                                                                FStar.Seq.Base.index
                                                                                                                                                                                                  #quad32
                                                                                                                                                                                                  round_keys
                                                                                                                                                                                                  11

                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                va_qAssertSquash
                                                                                                                                                                                                  va_range1
                                                                                                                                                                                                  "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 326 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                  (
                                                                                                                                                                                                    (
                                                                                                                                                                                                      fun
                                                                                                                                                                                                        a_539
                                                                                                                                                                                                        (
                                                                                                                                                                                                          s_540:
                                                                                                                                                                                                          (
                                                                                                                                                                                                            FStar.Seq.Base.seq
                                                                                                                                                                                                              a_539

                                                                                                                                                                                                          )
                                                                                                                                                                                                        )
                                                                                                                                                                                                        (
                                                                                                                                                                                                          i_541:
                                                                                                                                                                                                          Prims.nat
                                                                                                                                                                                                        )
                                                                                                                                                                                                        ->
                                                                                                                                                                                                        let
                                                                                                                                                                                                        i_515:Prims.nat
                                                                                                                                                                                                        =
                                                                                                                                                                                                          i_541
                                                                                                                                                                                                        in
                                                                                                                                                                                                        Prims.b2t
                                                                                                                                                                                                          (
                                                                                                                                                                                                            Prims.op_LessThan
                                                                                                                                                                                                              i_515
                                                                                                                                                                                                              (
                                                                                                                                                                                                                FStar.Seq.Base.length
                                                                                                                                                                                                                  #a_539
                                                                                                                                                                                                                  s_540

                                                                                                                                                                                                              )

                                                                                                                                                                                                          )

                                                                                                                                                                                                    )
                                                                                                                                                                                                      quad32
                                                                                                                                                                                                      round_keys
                                                                                                                                                                                                      12

                                                                                                                                                                                                  )
                                                                                                                                                                                                  (
                                                                                                                                                                                                    fun
                                                                                                                                                                                                      _
                                                                                                                                                                                                      ->
                                                                                                                                                                                                      va_qAssert
                                                                                                                                                                                                        va_range1
                                                                                                                                                                                                        "***** PRECONDITION NOT MET AT line 326 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                        (
                                                                                                                                                                                                          va_get_xmm
                                                                                                                                                                                                            5
                                                                                                                                                                                                            va_s
                                                                                                                                                                                                           ==
                                                                                                                                                                                                          FStar.Seq.Base.index
                                                                                                                                                                                                            #quad32
                                                                                                                                                                                                            round_keys
                                                                                                                                                                                                            12

                                                                                                                                                                                                        )
                                                                                                                                                                                                        (
                                                                                                                                                                                                          va_qAssertSquash
                                                                                                                                                                                                            va_range1
                                                                                                                                                                                                            "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 327 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                            (
                                                                                                                                                                                                              (
                                                                                                                                                                                                                fun
                                                                                                                                                                                                                  a_539
                                                                                                                                                                                                                  (
                                                                                                                                                                                                                    s_540:
                                                                                                                                                                                                                    (
                                                                                                                                                                                                                      FStar.Seq.Base.seq
                                                                                                                                                                                                                        a_539

                                                                                                                                                                                                                    )
                                                                                                                                                                                                                  )
                                                                                                                                                                                                                  (
                                                                                                                                                                                                                    i_541:
                                                                                                                                                                                                                    Prims.nat
                                                                                                                                                                                                                  )
                                                                                                                                                                                                                  ->
                                                                                                                                                                                                                  let
                                                                                                                                                                                                                  i_515:Prims.nat
                                                                                                                                                                                                                  =
                                                                                                                                                                                                                    i_541
                                                                                                                                                                                                                  in
                                                                                                                                                                                                                  Prims.b2t
                                                                                                                                                                                                                    (
                                                                                                                                                                                                                      Prims.op_LessThan
                                                                                                                                                                                                                        i_515
                                                                                                                                                                                                                        (
                                                                                                                                                                                                                          FStar.Seq.Base.length
                                                                                                                                                                                                                            #a_539
                                                                                                                                                                                                                            s_540

                                                                                                                                                                                                                        )

                                                                                                                                                                                                                    )

                                                                                                                                                                                                              )
                                                                                                                                                                                                                quad32
                                                                                                                                                                                                                round_keys
                                                                                                                                                                                                                13

                                                                                                                                                                                                            )
                                                                                                                                                                                                            (
                                                                                                                                                                                                              fun
                                                                                                                                                                                                                _
                                                                                                                                                                                                                ->
                                                                                                                                                                                                                va_qAssert
                                                                                                                                                                                                                  va_range1
                                                                                                                                                                                                                  "***** PRECONDITION NOT MET AT line 327 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                                  (
                                                                                                                                                                                                                    va_get_xmm
                                                                                                                                                                                                                      6
                                                                                                                                                                                                                      va_s
                                                                                                                                                                                                                     ==
                                                                                                                                                                                                                    FStar.Seq.Base.index
                                                                                                                                                                                                                      #quad32
                                                                                                                                                                                                                      round_keys
                                                                                                                                                                                                                      13

                                                                                                                                                                                                                  )
                                                                                                                                                                                                                  (
                                                                                                                                                                                                                    va_QSeq
                                                                                                                                                                                                                      va_range1
                                                                                                                                                                                                                      "***** PRECONDITION NOT MET AT line 330 column 25 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                                      (
                                                                                                                                                                                                                        va_quick_Aes_4rounds_4way
                                                                                                                                                                                                                          alg
                                                                                                                                                                                                                          10
                                                                                                                                                                                                                          (
                                                                                                                                                                                                                            va_get_xmm
                                                                                                                                                                                                                              2
                                                                                                                                                                                                                              va_old_s

                                                                                                                                                                                                                          )
                                                                                                                                                                                                                          (
                                                                                                                                                                                                                            va_get_xmm
                                                                                                                                                                                                                              12
                                                                                                                                                                                                                              va_old_s

                                                                                                                                                                                                                          )
                                                                                                                                                                                                                          (
                                                                                                                                                                                                                            va_get_xmm
                                                                                                                                                                                                                              13
                                                                                                                                                                                                                              va_old_s

                                                                                                                                                                                                                          )
                                                                                                                                                                                                                          (
                                                                                                                                                                                                                            va_get_xmm
                                                                                                                                                                                                                              14
                                                                                                                                                                                                                              va_old_s

                                                                                                                                                                                                                          )
                                                                                                                                                                                                                          round_keys

                                                                                                                                                                                                                      )
                                                                                                                                                                                                                      (
                                                                                                                                                                                                                        va_QBind
                                                                                                                                                                                                                          va_range1
                                                                                                                                                                                                                          "***** PRECONDITION NOT MET AT line 333 column 23 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                                          (
                                                                                                                                                                                                                            va_quick_Load128_buffer
                                                                                                                                                                                                                              (
                                                                                                                                                                                                                                va_op_heaplet_mem_heaplet
                                                                                                                                                                                                                                  0

                                                                                                                                                                                                                              )
                                                                                                                                                                                                                              (
                                                                                                                                                                                                                                va_op_xmm_xmm
                                                                                                                                                                                                                                  5

                                                                                                                                                                                                                              )
                                                                                                                                                                                                                              (
                                                                                                                                                                                                                                va_op_reg_opr64_reg64
                                                                                                                                                                                                                                  rR8

                                                                                                                                                                                                                              )
                                                                                                                                                                                                                              224
                                                                                                                                                                                                                              Secret
                                                                                                                                                                                                                              keys_b
                                                                                                                                                                                                                              14

                                                                                                                                                                                                                          )
                                                                                                                                                                                                                          (
                                                                                                                                                                                                                            fun
                                                                                                                                                                                                                              (
                                                                                                                                                                                                                                va_s:
                                                                                                                                                                                                                                va_state
                                                                                                                                                                                                                              )
                                                                                                                                                                                                                              _
                                                                                                                                                                                                                              ->
                                                                                                                                                                                                                              va_qAssertSquash
                                                                                                                                                                                                                                va_range1
                                                                                                                                                                                                                                "***** EXPRESSION PRECONDITIONS NOT MET WITHIN line 334 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                                                (
                                                                                                                                                                                                                                  (
                                                                                                                                                                                                                                    fun
                                                                                                                                                                                                                                      a_539
                                                                                                                                                                                                                                      (
                                                                                                                                                                                                                                        s_540:
                                                                                                                                                                                                                                        (
                                                                                                                                                                                                                                          FStar.Seq.Base.seq
                                                                                                                                                                                                                                            a_539

                                                                                                                                                                                                                                        )
                                                                                                                                                                                                                                      )
                                                                                                                                                                                                                                      (
                                                                                                                                                                                                                                        i_541:
                                                                                                                                                                                                                                        Prims.nat
                                                                                                                                                                                                                                      )
                                                                                                                                                                                                                                      ->
                                                                                                                                                                                                                                      let
                                                                                                                                                                                                                                      i_515:Prims.nat
                                                                                                                                                                                                                                      =
                                                                                                                                                                                                                                        i_541
                                                                                                                                                                                                                                      in
                                                                                                                                                                                                                                      Prims.b2t
                                                                                                                                                                                                                                        (
                                                                                                                                                                                                                                          Prims.op_LessThan
                                                                                                                                                                                                                                            i_515
                                                                                                                                                                                                                                            (
                                                                                                                                                                                                                                              FStar.Seq.Base.length
                                                                                                                                                                                                                                                #a_539
                                                                                                                                                                                                                                                s_540

                                                                                                                                                                                                                                            )

                                                                                                                                                                                                                                        )

                                                                                                                                                                                                                                  )
                                                                                                                                                                                                                                    quad32
                                                                                                                                                                                                                                    round_keys
                                                                                                                                                                                                                                    14

                                                                                                                                                                                                                                )
                                                                                                                                                                                                                                (
                                                                                                                                                                                                                                  fun
                                                                                                                                                                                                                                    _
                                                                                                                                                                                                                                    ->
                                                                                                                                                                                                                                    va_qAssert
                                                                                                                                                                                                                                      va_range1
                                                                                                                                                                                                                                      "***** PRECONDITION NOT MET AT line 334 column 9 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                                                      (
                                                                                                                                                                                                                                        va_get_xmm
                                                                                                                                                                                                                                          5
                                                                                                                                                                                                                                          va_s
                                                                                                                                                                                                                                         ==
                                                                                                                                                                                                                                        FStar.Seq.Base.index
                                                                                                                                                                                                                                          #quad32
                                                                                                                                                                                                                                          round_keys
                                                                                                                                                                                                                                          14

                                                                                                                                                                                                                                      )
                                                                                                                                                                                                                                      (
                                                                                                                                                                                                                                        va_QEmpty
                                                                                                                                                                                                                                          (
                                                                                                                                                                                                                                            ()
                                                                                                                                                                                                                                          )

                                                                                                                                                                                                                                      )

                                                                                                                                                                                                                                )

                                                                                                                                                                                                                          )

                                                                                                                                                                                                                      )

                                                                                                                                                                                                                  )

                                                                                                                                                                                                            )

                                                                                                                                                                                                        )

                                                                                                                                                                                                  )

                                                                                                                                                                                              )

                                                                                                                                                                                        )

                                                                                                                                                                                    )

                                                                                                                                                                              )

                                                                                                                                                                        )

                                                                                                                                                                    )

                                                                                                                                                                )

                                                                                                                                                            )

                                                                                                                                                      )

                                                                                                                                                  )
                                                                                                                                                  (
                                                                                                                                                    qblock
                                                                                                                                                      va_mods
                                                                                                                                                      (
                                                                                                                                                        fun
                                                                                                                                                          (
                                                                                                                                                            va_s:
                                                                                                                                                            va_state
                                                                                                                                                          )
                                                                                                                                                          ->
                                                                                                                                                          va_QEmpty
                                                                                                                                                            (
                                                                                                                                                              ()
                                                                                                                                                            )

                                                                                                                                                      )

                                                                                                                                                  )

                                                                                                                                              )
                                                                                                                                              (
                                                                                                                                                fun
                                                                                                                                                  (
                                                                                                                                                    va_s:
                                                                                                                                                    va_state
                                                                                                                                                  )
                                                                                                                                                  va_g
                                                                                                                                                  ->
                                                                                                                                                  va_QSeq
                                                                                                                                                    va_range1
                                                                                                                                                    "***** PRECONDITION NOT MET AT line 341 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                    (
                                                                                                                                                      va_quick_AESNI_enc_last
                                                                                                                                                        (
                                                                                                                                                          va_op_xmm_xmm
                                                                                                                                                            2

                                                                                                                                                        )
                                                                                                                                                        (
                                                                                                                                                          va_op_xmm_xmm
                                                                                                                                                            5

                                                                                                                                                        )

                                                                                                                                                    )
                                                                                                                                                    (
                                                                                                                                                      va_QSeq
                                                                                                                                                        va_range1
                                                                                                                                                        "***** PRECONDITION NOT MET AT line 342 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                        (
                                                                                                                                                          va_quick_AESNI_enc_last
                                                                                                                                                            (
                                                                                                                                                              va_op_xmm_xmm
                                                                                                                                                                12

                                                                                                                                                            )
                                                                                                                                                            (
                                                                                                                                                              va_op_xmm_xmm
                                                                                                                                                                5

                                                                                                                                                            )

                                                                                                                                                        )
                                                                                                                                                        (
                                                                                                                                                          va_QSeq
                                                                                                                                                            va_range1
                                                                                                                                                            "***** PRECONDITION NOT MET AT line 343 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                            (
                                                                                                                                                              va_quick_AESNI_enc_last
                                                                                                                                                                (
                                                                                                                                                                  va_op_xmm_xmm
                                                                                                                                                                    13

                                                                                                                                                                )
                                                                                                                                                                (
                                                                                                                                                                  va_op_xmm_xmm
                                                                                                                                                                    5

                                                                                                                                                                )

                                                                                                                                                            )
                                                                                                                                                            (
                                                                                                                                                              va_QBind
                                                                                                                                                                va_range1
                                                                                                                                                                "***** PRECONDITION NOT MET AT line 344 column 19 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                (
                                                                                                                                                                  va_quick_AESNI_enc_last
                                                                                                                                                                    (
                                                                                                                                                                      va_op_xmm_xmm
                                                                                                                                                                        14

                                                                                                                                                                    )
                                                                                                                                                                    (
                                                                                                                                                                      va_op_xmm_xmm
                                                                                                                                                                        5

                                                                                                                                                                    )

                                                                                                                                                                )
                                                                                                                                                                (
                                                                                                                                                                  fun
                                                                                                                                                                    (
                                                                                                                                                                      va_s:
                                                                                                                                                                      va_state
                                                                                                                                                                    )
                                                                                                                                                                    _
                                                                                                                                                                    ->
                                                                                                                                                                    let
                                                                                                                                                                    va_arg81:(
                                                                                                                                                                      FStar.Seq.Base.seq
                                                                                                                                                                        Vale.Def.Types_s.quad32

                                                                                                                                                                    )
                                                                                                                                                                    =
                                                                                                                                                                      round_keys
                                                                                                                                                                    in
                                                                                                                                                                    let
                                                                                                                                                                    va_arg80:Vale.Def.Types_s.quad32
                                                                                                                                                                    =
                                                                                                                                                                      in1
                                                                                                                                                                    in
                                                                                                                                                                    let
                                                                                                                                                                    va_arg79:Vale.AES.AES_common_s.algorithm
                                                                                                                                                                    =
                                                                                                                                                                      alg
                                                                                                                                                                    in
                                                                                                                                                                    va_qPURE
                                                                                                                                                                      va_range1
                                                                                                                                                                      "***** PRECONDITION NOT MET AT line 346 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                      (
                                                                                                                                                                        fun
                                                                                                                                                                          (
                                                                                                                                                                            _:
                                                                                                                                                                            unit
                                                                                                                                                                          )
                                                                                                                                                                          ->
                                                                                                                                                                          Vale.AES.AES_helpers.finish_cipher
                                                                                                                                                                            va_arg79
                                                                                                                                                                            va_arg80
                                                                                                                                                                            va_arg81

                                                                                                                                                                      )
                                                                                                                                                                      (
                                                                                                                                                                        let
                                                                                                                                                                        va_arg78:(
                                                                                                                                                                          FStar.Seq.Base.seq
                                                                                                                                                                            Vale.Def.Types_s.quad32

                                                                                                                                                                        )
                                                                                                                                                                        =
                                                                                                                                                                          round_keys
                                                                                                                                                                        in
                                                                                                                                                                        let
                                                                                                                                                                        va_arg77:Vale.Def.Types_s.quad32
                                                                                                                                                                        =
                                                                                                                                                                          in2
                                                                                                                                                                        in
                                                                                                                                                                        let
                                                                                                                                                                        va_arg76:Vale.AES.AES_common_s.algorithm
                                                                                                                                                                        =
                                                                                                                                                                          alg
                                                                                                                                                                        in
                                                                                                                                                                        va_qPURE
                                                                                                                                                                          va_range1
                                                                                                                                                                          "***** PRECONDITION NOT MET AT line 347 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                          (
                                                                                                                                                                            fun
                                                                                                                                                                              (
                                                                                                                                                                                _:
                                                                                                                                                                                unit
                                                                                                                                                                              )
                                                                                                                                                                              ->
                                                                                                                                                                              Vale.AES.AES_helpers.finish_cipher
                                                                                                                                                                                va_arg76
                                                                                                                                                                                va_arg77
                                                                                                                                                                                va_arg78

                                                                                                                                                                          )
                                                                                                                                                                          (
                                                                                                                                                                            let
                                                                                                                                                                            va_arg75:(
                                                                                                                                                                              FStar.Seq.Base.seq
                                                                                                                                                                                Vale.Def.Types_s.quad32

                                                                                                                                                                            )
                                                                                                                                                                            =
                                                                                                                                                                              round_keys
                                                                                                                                                                            in
                                                                                                                                                                            let
                                                                                                                                                                            va_arg74:Vale.Def.Types_s.quad32
                                                                                                                                                                            =
                                                                                                                                                                              in3
                                                                                                                                                                            in
                                                                                                                                                                            let
                                                                                                                                                                            va_arg73:Vale.AES.AES_common_s.algorithm
                                                                                                                                                                            =
                                                                                                                                                                              alg
                                                                                                                                                                            in
                                                                                                                                                                            va_qPURE
                                                                                                                                                                              va_range1
                                                                                                                                                                              "***** PRECONDITION NOT MET AT line 348 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                              (
                                                                                                                                                                                fun
                                                                                                                                                                                  (
                                                                                                                                                                                    _:
                                                                                                                                                                                    unit
                                                                                                                                                                                  )
                                                                                                                                                                                  ->
                                                                                                                                                                                  Vale.AES.AES_helpers.finish_cipher
                                                                                                                                                                                    va_arg73
                                                                                                                                                                                    va_arg74
                                                                                                                                                                                    va_arg75

                                                                                                                                                                              )
                                                                                                                                                                              (
                                                                                                                                                                                let
                                                                                                                                                                                va_arg72:(
                                                                                                                                                                                  FStar.Seq.Base.seq
                                                                                                                                                                                    Vale.Def.Types_s.quad32

                                                                                                                                                                                )
                                                                                                                                                                                =
                                                                                                                                                                                  round_keys
                                                                                                                                                                                in
                                                                                                                                                                                let
                                                                                                                                                                                va_arg71:Vale.Def.Types_s.quad32
                                                                                                                                                                                =
                                                                                                                                                                                  in4
                                                                                                                                                                                in
                                                                                                                                                                                let
                                                                                                                                                                                va_arg70:Vale.AES.AES_common_s.algorithm
                                                                                                                                                                                =
                                                                                                                                                                                  alg
                                                                                                                                                                                in
                                                                                                                                                                                va_qPURE
                                                                                                                                                                                  va_range1
                                                                                                                                                                                  "***** PRECONDITION NOT MET AT line 349 column 18 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                  (
                                                                                                                                                                                    fun
                                                                                                                                                                                      (
                                                                                                                                                                                        _:
                                                                                                                                                                                        unit
                                                                                                                                                                                      )
                                                                                                                                                                                      ->
                                                                                                                                                                                      Vale.AES.AES_helpers.finish_cipher
                                                                                                                                                                                        va_arg70
                                                                                                                                                                                        va_arg71
                                                                                                                                                                                        va_arg72

                                                                                                                                                                                  )
                                                                                                                                                                                  (
                                                                                                                                                                                    va_QLemma
                                                                                                                                                                                      va_range1
                                                                                                                                                                                      "***** PRECONDITION NOT MET AT line 350 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                      (
                                                                                                                                                                                        (
                                                                                                                                                                                          fun
                                                                                                                                                                                            (
                                                                                                                                                                                              alg:
                                                                                                                                                                                              algorithm
                                                                                                                                                                                            )
                                                                                                                                                                                            (
                                                                                                                                                                                              input_LE:
                                                                                                                                                                                              quad32
                                                                                                                                                                                            )
                                                                                                                                                                                            (
                                                                                                                                                                                              key:
                                                                                                                                                                                              (
                                                                                                                                                                                                seq
                                                                                                                                                                                                  nat32

                                                                                                                                                                                              )
                                                                                                                                                                                            )
                                                                                                                                                                                            ->
                                                                                                                                                                                            Vale.AES.AES_s.is_aes_key_LE
                                                                                                                                                                                              alg
                                                                                                                                                                                              key

                                                                                                                                                                                        )
                                                                                                                                                                                          alg
                                                                                                                                                                                          in1
                                                                                                                                                                                          key

                                                                                                                                                                                      )
                                                                                                                                                                                      (
                                                                                                                                                                                        fun
                                                                                                                                                                                          _
                                                                                                                                                                                          ->
                                                                                                                                                                                          (
                                                                                                                                                                                            fun
                                                                                                                                                                                              (
                                                                                                                                                                                                alg:
                                                                                                                                                                                                algorithm
                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                input_LE:
                                                                                                                                                                                                quad32
                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                key:
                                                                                                                                                                                                (
                                                                                                                                                                                                  seq
                                                                                                                                                                                                    nat32

                                                                                                                                                                                                )
                                                                                                                                                                                              )
                                                                                                                                                                                              ->
                                                                                                                                                                                              Vale.AES.AES_s.aes_encrypt_LE
                                                                                                                                                                                                alg
                                                                                                                                                                                                key
                                                                                                                                                                                                input_LE
                                                                                                                                                                                               ==
                                                                                                                                                                                              Vale.AES.AES_s.eval_cipher
                                                                                                                                                                                                alg
                                                                                                                                                                                                input_LE
                                                                                                                                                                                                (
                                                                                                                                                                                                  Vale.AES.AES_s.key_to_round_keys_LE
                                                                                                                                                                                                    alg
                                                                                                                                                                                                    key

                                                                                                                                                                                                )

                                                                                                                                                                                          )
                                                                                                                                                                                            alg
                                                                                                                                                                                            in1
                                                                                                                                                                                            key

                                                                                                                                                                                      )
                                                                                                                                                                                      (
                                                                                                                                                                                        fun
                                                                                                                                                                                          (
                                                                                                                                                                                            _:
                                                                                                                                                                                            unit
                                                                                                                                                                                          )
                                                                                                                                                                                          ->
                                                                                                                                                                                          finish_aes_encrypt_le
                                                                                                                                                                                            alg
                                                                                                                                                                                            in1
                                                                                                                                                                                            key

                                                                                                                                                                                      )
                                                                                                                                                                                      (
                                                                                                                                                                                        va_QLemma
                                                                                                                                                                                          va_range1
                                                                                                                                                                                          "***** PRECONDITION NOT MET AT line 351 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                          (
                                                                                                                                                                                            (
                                                                                                                                                                                              fun
                                                                                                                                                                                                (
                                                                                                                                                                                                  alg:
                                                                                                                                                                                                  algorithm
                                                                                                                                                                                                )
                                                                                                                                                                                                (
                                                                                                                                                                                                  input_LE:
                                                                                                                                                                                                  quad32
                                                                                                                                                                                                )
                                                                                                                                                                                                (
                                                                                                                                                                                                  key:
                                                                                                                                                                                                  (
                                                                                                                                                                                                    seq
                                                                                                                                                                                                      nat32

                                                                                                                                                                                                  )
                                                                                                                                                                                                )
                                                                                                                                                                                                ->
                                                                                                                                                                                                Vale.AES.AES_s.is_aes_key_LE
                                                                                                                                                                                                  alg
                                                                                                                                                                                                  key

                                                                                                                                                                                            )
                                                                                                                                                                                              alg
                                                                                                                                                                                              in2
                                                                                                                                                                                              key

                                                                                                                                                                                          )
                                                                                                                                                                                          (
                                                                                                                                                                                            fun
                                                                                                                                                                                              _
                                                                                                                                                                                              ->
                                                                                                                                                                                              (
                                                                                                                                                                                                fun
                                                                                                                                                                                                  (
                                                                                                                                                                                                    alg:
                                                                                                                                                                                                    algorithm
                                                                                                                                                                                                  )
                                                                                                                                                                                                  (
                                                                                                                                                                                                    input_LE:
                                                                                                                                                                                                    quad32
                                                                                                                                                                                                  )
                                                                                                                                                                                                  (
                                                                                                                                                                                                    key:
                                                                                                                                                                                                    (
                                                                                                                                                                                                      seq
                                                                                                                                                                                                        nat32

                                                                                                                                                                                                    )
                                                                                                                                                                                                  )
                                                                                                                                                                                                  ->
                                                                                                                                                                                                  Vale.AES.AES_s.aes_encrypt_LE
                                                                                                                                                                                                    alg
                                                                                                                                                                                                    key
                                                                                                                                                                                                    input_LE
                                                                                                                                                                                                   ==
                                                                                                                                                                                                  Vale.AES.AES_s.eval_cipher
                                                                                                                                                                                                    alg
                                                                                                                                                                                                    input_LE
                                                                                                                                                                                                    (
                                                                                                                                                                                                      Vale.AES.AES_s.key_to_round_keys_LE
                                                                                                                                                                                                        alg
                                                                                                                                                                                                        key

                                                                                                                                                                                                    )

                                                                                                                                                                                              )
                                                                                                                                                                                                alg
                                                                                                                                                                                                in2
                                                                                                                                                                                                key

                                                                                                                                                                                          )
                                                                                                                                                                                          (
                                                                                                                                                                                            fun
                                                                                                                                                                                              (
                                                                                                                                                                                                _:
                                                                                                                                                                                                unit
                                                                                                                                                                                              )
                                                                                                                                                                                              ->
                                                                                                                                                                                              finish_aes_encrypt_le
                                                                                                                                                                                                alg
                                                                                                                                                                                                in2
                                                                                                                                                                                                key

                                                                                                                                                                                          )
                                                                                                                                                                                          (
                                                                                                                                                                                            va_QLemma
                                                                                                                                                                                              va_range1
                                                                                                                                                                                              "***** PRECONDITION NOT MET AT line 352 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                              (
                                                                                                                                                                                                (
                                                                                                                                                                                                  fun
                                                                                                                                                                                                    (
                                                                                                                                                                                                      alg:
                                                                                                                                                                                                      algorithm
                                                                                                                                                                                                    )
                                                                                                                                                                                                    (
                                                                                                                                                                                                      input_LE:
                                                                                                                                                                                                      quad32
                                                                                                                                                                                                    )
                                                                                                                                                                                                    (
                                                                                                                                                                                                      key:
                                                                                                                                                                                                      (
                                                                                                                                                                                                        seq
                                                                                                                                                                                                          nat32

                                                                                                                                                                                                      )
                                                                                                                                                                                                    )
                                                                                                                                                                                                    ->
                                                                                                                                                                                                    Vale.AES.AES_s.is_aes_key_LE
                                                                                                                                                                                                      alg
                                                                                                                                                                                                      key

                                                                                                                                                                                                )
                                                                                                                                                                                                  alg
                                                                                                                                                                                                  in3
                                                                                                                                                                                                  key

                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                fun
                                                                                                                                                                                                  _
                                                                                                                                                                                                  ->
                                                                                                                                                                                                  (
                                                                                                                                                                                                    fun
                                                                                                                                                                                                      (
                                                                                                                                                                                                        alg:
                                                                                                                                                                                                        algorithm
                                                                                                                                                                                                      )
                                                                                                                                                                                                      (
                                                                                                                                                                                                        input_LE:
                                                                                                                                                                                                        quad32
                                                                                                                                                                                                      )
                                                                                                                                                                                                      (
                                                                                                                                                                                                        key:
                                                                                                                                                                                                        (
                                                                                                                                                                                                          seq
                                                                                                                                                                                                            nat32

                                                                                                                                                                                                        )
                                                                                                                                                                                                      )
                                                                                                                                                                                                      ->
                                                                                                                                                                                                      Vale.AES.AES_s.aes_encrypt_LE
                                                                                                                                                                                                        alg
                                                                                                                                                                                                        key
                                                                                                                                                                                                        input_LE
                                                                                                                                                                                                       ==
                                                                                                                                                                                                      Vale.AES.AES_s.eval_cipher
                                                                                                                                                                                                        alg
                                                                                                                                                                                                        input_LE
                                                                                                                                                                                                        (
                                                                                                                                                                                                          Vale.AES.AES_s.key_to_round_keys_LE
                                                                                                                                                                                                            alg
                                                                                                                                                                                                            key

                                                                                                                                                                                                        )

                                                                                                                                                                                                  )
                                                                                                                                                                                                    alg
                                                                                                                                                                                                    in3
                                                                                                                                                                                                    key

                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                fun
                                                                                                                                                                                                  (
                                                                                                                                                                                                    _:
                                                                                                                                                                                                    unit
                                                                                                                                                                                                  )
                                                                                                                                                                                                  ->
                                                                                                                                                                                                  finish_aes_encrypt_le
                                                                                                                                                                                                    alg
                                                                                                                                                                                                    in3
                                                                                                                                                                                                    key

                                                                                                                                                                                              )
                                                                                                                                                                                              (
                                                                                                                                                                                                va_QLemma
                                                                                                                                                                                                  va_range1
                                                                                                                                                                                                  "***** PRECONDITION NOT MET AT line 353 column 26 of file /home/gebner/fstar_dataset/projects/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64/Vale.AES.X64.AESCTR.vaf *****"
                                                                                                                                                                                                  (
                                                                                                                                                                                                    (
                                                                                                                                                                                                      fun
                                                                                                                                                                                                        (
                                                                                                                                                                                                          alg:
                                                                                                                                                                                                          algorithm
                                                                                                                                                                                                        )
                                                                                                                                                                                                        (
                                                                                                                                                                                                          input_LE:
                                                                                                                                                                                                          quad32
                                                                                                                                                                                                        )
                                                                                                                                                                                                        (
                                                                                                                                                                                                          key:
                                                                                                                                                                                                          (
                                                                                                                                                                                                            seq
                                                                                                                                                                                                              nat32

                                                                                                                                                                                                          )
                                                                                                                                                                                                        )
                                                                                                                                                                                                        ->
                                                                                                                                                                                                        Vale.AES.AES_s.is_aes_key_LE
                                                                                                                                                                                                          alg
                                                                                                                                                                                                          key

                                                                                                                                                                                                    )
                                                                                                                                                                                                      alg
                                                                                                                                                                                                      in4
                                                                                                                                                                                                      key

                                                                                                                                                                                                  )
                                                                                                                                                                                                  (
                                                                                                                                                                                                    fun
                                                                                                                                                                                                      _
                                                                                                                                                                                                      ->
                                                                                                                                                                                                      (
                                                                                                                                                                                                        fun
                                                                                                                                                                                                          (
                                                                                                                                                                                                            alg:
                                                                                                                                                                                                            algorithm
                                                                                                                                                                                                          )
                                                                                                                                                                                                          (
                                                                                                                                                                                                            input_LE:
                                                                                                                                                                                                            quad32
                                                                                                                                                                                                          )
                                                                                                                                                                                                          (
                                                                                                                                                                                                            key:
                                                                                                                                                                                                            (
                                                                                                                                                                                                              seq
                                                                                                                                                                                                                nat32

                                                                                                                                                                                                            )
                                                                                                                                                                                                          )
                                                                                                                                                                                                          ->
                                                                                                                                                                                                          Vale.AES.AES_s.aes_encrypt_LE
                                                                                                                                                                                                            alg
                                                                                                                                                                                                            key
                                                                                                                                                                                                            input_LE
                                                                                                                                                                                                           ==
                                                                                                                                                                                                          Vale.AES.AES_s.eval_cipher
                                                                                                                                                                                                            alg
                                                                                                                                                                                                            input_LE
                                                                                                                                                                                                            (
                                                                                                                                                                                                              Vale.AES.AES_s.key_to_round_keys_LE
                                                                                                                                                                                                                alg
                                                                                                                                                                                                                key

                                                                                                                                                                                                            )

                                                                                                                                                                                                      )
                                                                                                                                                                                                        alg
                                                                                                                                                                                                        in4
                                                                                                                                                                                                        key

                                                                                                                                                                                                  )
                                                                                                                                                                                                  (
                                                                                                                                                                                                    fun
                                                                                                                                                                                                      (
                                                                                                                                                                                                        _:
                                                                                                                                                                                                        unit
                                                                                                                                                                                                      )
                                                                                                                                                                                                      ->
                                                                                                                                                                                                      finish_aes_encrypt_le
                                                                                                                                                                                                        alg
                                                                                                                                                                                                        in4
                                                                                                                                                                                                        key

                                                                                                                                                                                                  )
                                                                                                                                                                                                  (
                                                                                                                                                                                                    va_QEmpty
                                                                                                                                                                                                      (
                                                                                                                                                                                                        ()
                                                                                                                                                                                                      )

                                                                                                                                                                                                  )

                                                                                                                                                                                              )

                                                                                                                                                                                          )

                                                                                                                                                                                      )

                                                                                                                                                                                  )

                                                                                                                                                                              )

                                                                                                                                                                          )

                                                                                                                                                                      )

                                                                                                                                                                )

                                                                                                                                                            )

                                                                                                                                                        )

                                                                                                                                                    )

                                                                                                                                              )

                                                                                                                                        )

                                                                                                                                    )

                                                                                                                              )

                                                                                                                          )

                                                                                                                    )

                                                                                                                )

                                                                                                          )

                                                                                                    )
                                                                                                  ))
                                                                                        ))))))))))))
                              ))))))))