val va_lemma_MulAdd18 : va_b0:va_code -> va_s0:va_state -> r0:va_operand_reg_opr64 ->
  r1:va_operand_reg_opr64 -> r2:va_operand_reg_opr64 -> r3:va_operand_reg_opr64 ->
  r4:va_operand_reg_opr64 -> r5:va_operand_reg_opr64 -> r6:va_operand_reg_opr64 ->
  r7:va_operand_reg_opr64 -> regRotate:nat -> bA:buffer64 -> bB:buffer64 -> bD:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7) va_s0 /\
    va_is_dst_reg_opr64 r0 va_s0 /\ va_is_dst_reg_opr64 r1 va_s0 /\ va_is_dst_reg_opr64 r2 va_s0 /\
    va_is_dst_reg_opr64 r3 va_s0 /\ va_is_dst_reg_opr64 r4 va_s0 /\ va_is_dst_reg_opr64 r5 va_s0 /\
    va_is_dst_reg_opr64 r6 va_s0 /\ va_is_dst_reg_opr64 r7 va_s0 /\ va_get_ok va_s0 /\ (let
    (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet 0
    va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_s0) /\ flag_cf
    (va_get_flags va_s0) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_s0) /\ flag_of
    (va_get_flags va_s0) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in adx_enabled /\ bmi2_enabled /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) bA 8
    (va_get_mem_layout va_s0) Public /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) bB 1 (va_get_mem_layout va_s0) Public /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bD 1
    (va_get_mem_layout va_s0) Public /\ FStar.Seq.Base.length #Vale.Def.Types_s.nat64 as0 == 8 /\
    r0 == operand_reg8 (regRotate + 0) /\ r1 == operand_reg8 (regRotate + 1) /\ r2 == operand_reg8
    (regRotate + 2) /\ r3 == operand_reg8 (regRotate + 3) /\ r4 == operand_reg8 (regRotate + 4) /\
    r5 == operand_reg8 (regRotate + 5) /\ r6 == operand_reg8 (regRotate + 6) /\ r7 == operand_reg8
    (regRotate + 7))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet
    0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_sM) /\ flag_cf
    (va_get_flags va_sM) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_sM) /\ flag_of
    (va_get_flags va_sM) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in let (b:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read bB 0 (va_get_mem_heaplet 0 va_s0) in let
    (d:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s0) in
    let (xs:(seq nat64)) = make_seq9 #nat64 (Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet
    0 va_sM)) (va_eval_reg_opr64 va_sM r1) (va_eval_reg_opr64 va_sM r2) (va_eval_reg_opr64 va_sM
    r3) (va_eval_reg_opr64 va_sM r4) (va_eval_reg_opr64 va_sM r5) (va_eval_reg_opr64 va_sM r6)
    (va_eval_reg_opr64 va_sM r7) (va_eval_reg_opr64 va_sM r0) in sum_pow_seq xs == sum_pow_seq rs +
    b `op_Multiply` sum_pow_seq as0 + d) /\ va_state_eq va_sM (va_update_mem_layout va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_flags va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM (va_update_operand_reg_opr64 r7 va_sM (va_update_operand_reg_opr64 r6 va_sM
    (va_update_operand_reg_opr64 r5 va_sM (va_update_operand_reg_opr64 r4 va_sM
    (va_update_operand_reg_opr64 r3 va_sM (va_update_operand_reg_opr64 r2 va_sM
    (va_update_operand_reg_opr64 r1 va_sM (va_update_operand_reg_opr64 r0 va_sM
    va_s0))))))))))))))))))
let va_lemma_MulAdd18 va_b0 va_s0 r0 r1 r2 r3 r4 r5 r6 r7 regRotate bA bB bD =
  va_reveal_opaque (`%va_code_MulAdd18) (va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7);
  let (va_old_s:va_state) = va_s0 in
  let (va_b1:va_codes) = va_get_block va_b0 in
  let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet 0
    va_s0) bA in
  let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1)
    (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4)
    (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in
  let (b:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read bB 0 (va_get_mem_heaplet 0 va_s0) in
  let (d:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s0) in
  Vale.Bignum.Defs.reveal_add_lo_all ();
  let (va_s12, va_fc12) = va_lemma_Mem64_lemma (va_hd va_b1) va_s0 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 0 bB 0 Public in
  let va_b12 = va_tl va_b1 in
  let (va_s13, va_fc13) = va_lemma_Mov64 (va_hd va_b12) va_s12 (va_op_dst_opr64_reg64 rRdx)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 0 Public) in
  let va_b13 = va_tl va_b12 in
  let (va_s14, va_fc14) = va_lemma_Mem64_lemma (va_hd va_b13) va_s13 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRdi) 0 bD 0 Public in
  let va_b14 = va_tl va_b13 in
  let (va_s15, va_fc15) = va_lemma_Adox_64 (va_hd va_b14) va_s14 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) 0 Public) in
  let va_b15 = va_tl va_b14 in
  let (va_s16, va_fc16) = va_lemma_Mem64_lemma (va_hd va_b15) va_s15 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (0 `op_Multiply` 8) bA 0 Public in
  let va_b16 = va_tl va_b15 in
  let (va_s17, va_fc17) = va_lemma_Mulx_64 (va_hd va_b16) va_s16 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (0 `op_Multiply` 8) Public) in
  let va_b17 = va_tl va_b16 in
  let (va_s18, va_fc18) = va_lemma_Adcx_64 (va_hd va_b17) va_s17 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_op_opr64_reg64 rRax) in
  let va_b18 = va_tl va_b17 in
  let (va_s19, va_fc19) = va_lemma_Adox_64 (va_hd va_b18) va_s18 (va_coerce_reg_opr64_to_dst_opr64
    r1) (va_op_opr64_reg64 rRbx) in
  let va_b19 = va_tl va_b18 in
  let (va_s20, va_fc20) = va_lemma_Mem64_lemma (va_hd va_b19) va_s19 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (1 `op_Multiply` 8) bA 1 Public in
  let va_b20 = va_tl va_b19 in
  let (va_s21, va_fc21) = va_lemma_Mulx_64 (va_hd va_b20) va_s20 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (1 `op_Multiply` 8) Public) in
  let va_b21 = va_tl va_b20 in
  let (va_s22, va_fc22) = va_lemma_Adcx_64 (va_hd va_b21) va_s21 (va_coerce_reg_opr64_to_dst_opr64
    r1) (va_op_opr64_reg64 rRax) in
  let va_b22 = va_tl va_b21 in
  let (va_s23, va_fc23) = va_lemma_Adox_64 (va_hd va_b22) va_s22 (va_coerce_reg_opr64_to_dst_opr64
    r2) (va_op_opr64_reg64 rRbx) in
  let va_b23 = va_tl va_b22 in
  let (va_s24, va_fc24) = va_lemma_Mem64_lemma (va_hd va_b23) va_s23 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (2 `op_Multiply` 8) bA 2 Public in
  let va_b24 = va_tl va_b23 in
  let (va_s25, va_fc25) = va_lemma_Mulx_64 (va_hd va_b24) va_s24 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (2 `op_Multiply` 8) Public) in
  let va_b25 = va_tl va_b24 in
  let (va_s26, va_fc26) = va_lemma_Adcx_64 (va_hd va_b25) va_s25 (va_coerce_reg_opr64_to_dst_opr64
    r2) (va_op_opr64_reg64 rRax) in
  let va_b26 = va_tl va_b25 in
  let (va_s27, va_fc27) = va_lemma_Adox_64 (va_hd va_b26) va_s26 (va_coerce_reg_opr64_to_dst_opr64
    r3) (va_op_opr64_reg64 rRbx) in
  let va_b27 = va_tl va_b26 in
  let (va_s28, va_fc28) = va_lemma_Mem64_lemma (va_hd va_b27) va_s27 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (3 `op_Multiply` 8) bA 3 Public in
  let va_b28 = va_tl va_b27 in
  let (va_s29, va_fc29) = va_lemma_Mulx_64 (va_hd va_b28) va_s28 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (3 `op_Multiply` 8) Public) in
  let va_b29 = va_tl va_b28 in
  let (va_s30, va_fc30) = va_lemma_Adcx_64 (va_hd va_b29) va_s29 (va_coerce_reg_opr64_to_dst_opr64
    r3) (va_op_opr64_reg64 rRax) in
  let va_b30 = va_tl va_b29 in
  let (va_s31, va_fc31) = va_lemma_Adox_64 (va_hd va_b30) va_s30 (va_coerce_reg_opr64_to_dst_opr64
    r4) (va_op_opr64_reg64 rRbx) in
  let va_b31 = va_tl va_b30 in
  let (va_s32, va_fc32) = va_lemma_Mem64_lemma (va_hd va_b31) va_s31 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (4 `op_Multiply` 8) bA 4 Public in
  let va_b32 = va_tl va_b31 in
  let (va_s33, va_fc33) = va_lemma_Mulx_64 (va_hd va_b32) va_s32 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (4 `op_Multiply` 8) Public) in
  let va_b33 = va_tl va_b32 in
  let (va_s34, va_fc34) = va_lemma_Adcx_64 (va_hd va_b33) va_s33 (va_coerce_reg_opr64_to_dst_opr64
    r4) (va_op_opr64_reg64 rRax) in
  let va_b34 = va_tl va_b33 in
  let (va_s35, va_fc35) = va_lemma_Adox_64 (va_hd va_b34) va_s34 (va_coerce_reg_opr64_to_dst_opr64
    r5) (va_op_opr64_reg64 rRbx) in
  let va_b35 = va_tl va_b34 in
  let (va_s36, va_fc36) = va_lemma_Mem64_lemma (va_hd va_b35) va_s35 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (5 `op_Multiply` 8) bA 5 Public in
  let va_b36 = va_tl va_b35 in
  let (va_s37, va_fc37) = va_lemma_Mulx_64 (va_hd va_b36) va_s36 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (5 `op_Multiply` 8) Public) in
  let va_b37 = va_tl va_b36 in
  let (va_s38, va_fc38) = va_lemma_Adcx_64 (va_hd va_b37) va_s37 (va_coerce_reg_opr64_to_dst_opr64
    r5) (va_op_opr64_reg64 rRax) in
  let va_b38 = va_tl va_b37 in
  let (va_s39, va_fc39) = va_lemma_Adox_64 (va_hd va_b38) va_s38 (va_coerce_reg_opr64_to_dst_opr64
    r6) (va_op_opr64_reg64 rRbx) in
  let va_b39 = va_tl va_b38 in
  let (va_s40, va_fc40) = va_lemma_Mem64_lemma (va_hd va_b39) va_s39 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (6 `op_Multiply` 8) bA 6 Public in
  let va_b40 = va_tl va_b39 in
  let (va_s41, va_fc41) = va_lemma_Mulx_64 (va_hd va_b40) va_s40 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (6 `op_Multiply` 8) Public) in
  let va_b41 = va_tl va_b40 in
  let (va_s42, va_fc42) = va_lemma_Adcx_64 (va_hd va_b41) va_s41 (va_coerce_reg_opr64_to_dst_opr64
    r6) (va_op_opr64_reg64 rRax) in
  let va_b42 = va_tl va_b41 in
  let (va_s43, va_fc43) = va_lemma_Adox_64 (va_hd va_b42) va_s42 (va_coerce_reg_opr64_to_dst_opr64
    r7) (va_op_opr64_reg64 rRbx) in
  let va_b43 = va_tl va_b42 in
  let (va_s44, va_fc44) = va_lemma_Mem64_lemma (va_hd va_b43) va_s43 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (7 `op_Multiply` 8) bA 7 Public in
  let va_b44 = va_tl va_b43 in
  let (va_s45, va_fc45) = va_lemma_Mulx_64 (va_hd va_b44) va_s44 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (7 `op_Multiply` 8) Public) in
  let va_b45 = va_tl va_b44 in
  let (va_s46, va_fc46) = va_lemma_Adcx_64 (va_hd va_b45) va_s45 (va_coerce_reg_opr64_to_dst_opr64
    r7) (va_op_opr64_reg64 rRax) in
  let va_b46 = va_tl va_b45 in
  let (va_s47, va_fc47) = va_lemma_Store64_buffer (va_hd va_b46) va_s46 (va_op_heaplet_mem_heaplet
    0) (va_op_reg_opr64_reg64 rRdi) r0 0 Public bD 0 in
  let va_b47 = va_tl va_b46 in
  let (va_s48, va_fc48) = va_lemma_Mov64 (va_hd va_b47) va_s47 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_const_opr64 0) in
  let va_b48 = va_tl va_b47 in
  let (va_s49, va_fc49) = va_lemma_Adcx_64 (va_hd va_b48) va_s48 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_coerce_reg_opr64_to_opr64 r0) in
  let va_b49 = va_tl va_b48 in
  let (va_s50, va_fc50) = va_lemma_Adox_64 (va_hd va_b49) va_s49 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_op_opr64_reg64 rRbx) in
  let va_b50 = va_tl va_b49 in
  let (l:(va_int_range 8 8)) = 8 in
  let (ys:(seq nat64)) = init_ys b as0 in
  let (zs:(seq nat64)) = init_zs b as0 d in
  let (qs:(seq nat64)) = __proj__Mktuple2__item___1 #(seq nat64) #nat1 (seq_add rs zs 0) in
  let (xs:(seq nat64)) = make_seq9 #nat64 (Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0
    va_s50)) (va_eval_reg_opr64 va_s50 r1) (va_eval_reg_opr64 va_s50 r2) (va_eval_reg_opr64 va_s50
    r3) (va_eval_reg_opr64 va_s50 r4) (va_eval_reg_opr64 va_s50 r5) (va_eval_reg_opr64 va_s50 r6)
    (va_eval_reg_opr64 va_s50 r7) (va_eval_reg_opr64 va_s50 r0) in
  lemma_seq_add_is_norm rs zs 0 (l + 1);
  lemma_seq_add_is_norm qs ys 0 (l + 1);
  lemma_scale_add l b d as0 rs ys zs qs xs;
  assert (FStar.Seq.Base.equal #nat64 xs (__proj__Mktuple2__item___1 #(seq nat64) #nat1 (seq_add qs
    ys 0)));
  let va_forall_lemma () : Lemma
    (requires true)
    (ensures (flag_cf (va_get_flags va_s50) == 0 /\ flag_of (va_get_flags va_s50) == 0))
    =
  (
    Vale.Bignum.Defs.reveal_add_hi_all ();
    ()
  ) in va_forall_lemma ();
  let (va_sM, va_f50) = va_lemma_empty_total va_s50 va_b50 in
  let va_f49 = va_lemma_merge_total va_b49 va_s49 va_fc50 va_s50 va_f50 va_sM in
  let va_f48 = va_lemma_merge_total va_b48 va_s48 va_fc49 va_s49 va_f49 va_sM in
  let va_f47 = va_lemma_merge_total va_b47 va_s47 va_fc48 va_s48 va_f48 va_sM in
  let va_f46 = va_lemma_merge_total va_b46 va_s46 va_fc47 va_s47 va_f47 va_sM in
  let va_f45 = va_lemma_merge_total va_b45 va_s45 va_fc46 va_s46 va_f46 va_sM in
  let va_f44 = va_lemma_merge_total va_b44 va_s44 va_fc45 va_s45 va_f45 va_sM in
  let va_f43 = va_lemma_merge_total va_b43 va_s43 va_fc44 va_s44 va_f44 va_sM in
  let va_f42 = va_lemma_merge_total va_b42 va_s42 va_fc43 va_s43 va_f43 va_sM in
  let va_f41 = va_lemma_merge_total va_b41 va_s41 va_fc42 va_s42 va_f42 va_sM in
  let va_f40 = va_lemma_merge_total va_b40 va_s40 va_fc41 va_s41 va_f41 va_sM in
  let va_f39 = va_lemma_merge_total va_b39 va_s39 va_fc40 va_s40 va_f40 va_sM in
  let va_f38 = va_lemma_merge_total va_b38 va_s38 va_fc39 va_s39 va_f39 va_sM in
  let va_f37 = va_lemma_merge_total va_b37 va_s37 va_fc38 va_s38 va_f38 va_sM in
  let va_f36 = va_lemma_merge_total va_b36 va_s36 va_fc37 va_s37 va_f37 va_sM in
  let va_f35 = va_lemma_merge_total va_b35 va_s35 va_fc36 va_s36 va_f36 va_sM in
  let va_f34 = va_lemma_merge_total va_b34 va_s34 va_fc35 va_s35 va_f35 va_sM in
  let va_f33 = va_lemma_merge_total va_b33 va_s33 va_fc34 va_s34 va_f34 va_sM in
  let va_f32 = va_lemma_merge_total va_b32 va_s32 va_fc33 va_s33 va_f33 va_sM in
  let va_f31 = va_lemma_merge_total va_b31 va_s31 va_fc32 va_s32 va_f32 va_sM in
  let va_f30 = va_lemma_merge_total va_b30 va_s30 va_fc31 va_s31 va_f31 va_sM in
  let va_f29 = va_lemma_merge_total va_b29 va_s29 va_fc30 va_s30 va_f30 va_sM in
  let va_f28 = va_lemma_merge_total va_b28 va_s28 va_fc29 va_s29 va_f29 va_sM in
  let va_f27 = va_lemma_merge_total va_b27 va_s27 va_fc28 va_s28 va_f28 va_sM in
  let va_f26 = va_lemma_merge_total va_b26 va_s26 va_fc27 va_s27 va_f27 va_sM in
  let va_f25 = va_lemma_merge_total va_b25 va_s25 va_fc26 va_s26 va_f26 va_sM in
  let va_f24 = va_lemma_merge_total va_b24 va_s24 va_fc25 va_s25 va_f25 va_sM in
  let va_f23 = va_lemma_merge_total va_b23 va_s23 va_fc24 va_s24 va_f24 va_sM in
  let va_f22 = va_lemma_merge_total va_b22 va_s22 va_fc23 va_s23 va_f23 va_sM in
  let va_f21 = va_lemma_merge_total va_b21 va_s21 va_fc22 va_s22 va_f22 va_sM in
  let va_f20 = va_lemma_merge_total va_b20 va_s20 va_fc21 va_s21 va_f21 va_sM in
  let va_f19 = va_lemma_merge_total va_b19 va_s19 va_fc20 va_s20 va_f20 va_sM in
  let va_f18 = va_lemma_merge_total va_b18 va_s18 va_fc19 va_s19 va_f19 va_sM in
  let va_f17 = va_lemma_merge_total va_b17 va_s17 va_fc18 va_s18 va_f18 va_sM in
  let va_f16 = va_lemma_merge_total va_b16 va_s16 va_fc17 va_s17 va_f17 va_sM in
  let va_f15 = va_lemma_merge_total va_b15 va_s15 va_fc16 va_s16 va_f16 va_sM in
  let va_f14 = va_lemma_merge_total va_b14 va_s14 va_fc15 va_s15 va_f15 va_sM in
  let va_f13 = va_lemma_merge_total va_b13 va_s13 va_fc14 va_s14 va_f14 va_sM in
  let va_f12 = va_lemma_merge_total va_b12 va_s12 va_fc13 va_s13 va_f13 va_sM in
  let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc12 va_s12 va_f12 va_sM in
  (va_sM, va_fM)
val va_lemma_MulAdd18 : va_b0:va_code -> va_s0:va_state -> r0:va_operand_reg_opr64 ->
  r1:va_operand_reg_opr64 -> r2:va_operand_reg_opr64 -> r3:va_operand_reg_opr64 ->
  r4:va_operand_reg_opr64 -> r5:va_operand_reg_opr64 -> r6:va_operand_reg_opr64 ->
  r7:va_operand_reg_opr64 -> regRotate:nat -> bA:buffer64 -> bB:buffer64 -> bD:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7) va_s0 /\
    va_is_dst_reg_opr64 r0 va_s0 /\ va_is_dst_reg_opr64 r1 va_s0 /\ va_is_dst_reg_opr64 r2 va_s0 /\
    va_is_dst_reg_opr64 r3 va_s0 /\ va_is_dst_reg_opr64 r4 va_s0 /\ va_is_dst_reg_opr64 r5 va_s0 /\
    va_is_dst_reg_opr64 r6 va_s0 /\ va_is_dst_reg_opr64 r7 va_s0 /\ va_get_ok va_s0 /\ (let
    (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet 0
    va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_s0) /\ flag_cf
    (va_get_flags va_s0) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_s0) /\ flag_of
    (va_get_flags va_s0) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in adx_enabled /\ bmi2_enabled /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) bA 8
    (va_get_mem_layout va_s0) Public /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) bB 1 (va_get_mem_layout va_s0) Public /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bD 1
    (va_get_mem_layout va_s0) Public /\ FStar.Seq.Base.length #Vale.Def.Types_s.nat64 as0 == 8 /\
    r0 == operand_reg8 (regRotate + 0) /\ r1 == operand_reg8 (regRotate + 1) /\ r2 == operand_reg8
    (regRotate + 2) /\ r3 == operand_reg8 (regRotate + 3) /\ r4 == operand_reg8 (regRotate + 4) /\
    r5 == operand_reg8 (regRotate + 5) /\ r6 == operand_reg8 (regRotate + 6) /\ r7 == operand_reg8
    (regRotate + 7))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet
    0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_sM) /\ flag_cf
    (va_get_flags va_sM) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_sM) /\ flag_of
    (va_get_flags va_sM) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in let (b:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read bB 0 (va_get_mem_heaplet 0 va_s0) in let
    (d:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s0) in
    let (xs:(seq nat64)) = make_seq9 #nat64 (Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet
    0 va_sM)) (va_eval_reg_opr64 va_sM r1) (va_eval_reg_opr64 va_sM r2) (va_eval_reg_opr64 va_sM
    r3) (va_eval_reg_opr64 va_sM r4) (va_eval_reg_opr64 va_sM r5) (va_eval_reg_opr64 va_sM r6)
    (va_eval_reg_opr64 va_sM r7) (va_eval_reg_opr64 va_sM r0) in sum_pow_seq xs == sum_pow_seq rs +
    b `op_Multiply` sum_pow_seq as0 + d) /\ va_state_eq va_sM (va_update_mem_layout va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_flags va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM (va_update_operand_reg_opr64 r7 va_sM (va_update_operand_reg_opr64 r6 va_sM
    (va_update_operand_reg_opr64 r5 va_sM (va_update_operand_reg_opr64 r4 va_sM
    (va_update_operand_reg_opr64 r3 va_sM (va_update_operand_reg_opr64 r2 va_sM
    (va_update_operand_reg_opr64 r1 va_sM (va_update_operand_reg_opr64 r0 va_sM
    va_s0))))))))))))))))))
let va_lemma_MulAdd18 va_b0 va_s0 r0 r1 r2 r3 r4 r5 r6 r7 regRotate bA bB bD =
va_reveal_opaque (`%va_code_MulAdd18) (va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7);
let va_old_s:va_state = va_s0 in
let va_b1:va_codes = va_get_block va_b0 in
let as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64) =
  Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA
in
let rs:(seq nat64) =
  make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1)
    (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4)
    (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0
in
let b:Vale.Def.Types_s.nat64 = Vale.X64.Decls.buffer64_read bB 0 (va_get_mem_heaplet 0 va_s0) in
let d:Vale.Def.Types_s.nat64 = Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s0) in
Vale.Bignum.Defs.reveal_add_lo_all ();
let va_s12, va_fc12 =
  va_lemma_Mem64_lemma (va_hd va_b1)
    va_s0
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi)
    0
    bB
    0
    Public
in
let va_b12 = va_tl va_b1 in
let va_s13, va_fc13 =
  va_lemma_Mov64 (va_hd va_b12)
    va_s12
    (va_op_dst_opr64_reg64 rRdx)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 0 Public)
in
let va_b13 = va_tl va_b12 in
let va_s14, va_fc14 =
  va_lemma_Mem64_lemma (va_hd va_b13)
    va_s13
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRdi)
    0
    bD
    0
    Public
in
let va_b14 = va_tl va_b13 in
let va_s15, va_fc15 =
  va_lemma_Adox_64 (va_hd va_b14)
    va_s14
    (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) 0 Public)
in
let va_b15 = va_tl va_b14 in
let va_s16, va_fc16 =
  va_lemma_Mem64_lemma (va_hd va_b15)
    va_s15
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (0 `op_Multiply` 8)
    bA
    0
    Public
in
let va_b16 = va_tl va_b15 in
let va_s17, va_fc17 =
  va_lemma_Mulx_64 (va_hd va_b16)
    va_s16
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (0 `op_Multiply` 8)
        Public)
in
let va_b17 = va_tl va_b16 in
let va_s18, va_fc18 =
  va_lemma_Adcx_64 (va_hd va_b17)
    va_s17
    (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_op_opr64_reg64 rRax)
in
let va_b18 = va_tl va_b17 in
let va_s19, va_fc19 =
  va_lemma_Adox_64 (va_hd va_b18)
    va_s18
    (va_coerce_reg_opr64_to_dst_opr64 r1)
    (va_op_opr64_reg64 rRbx)
in
let va_b19 = va_tl va_b18 in
let va_s20, va_fc20 =
  va_lemma_Mem64_lemma (va_hd va_b19)
    va_s19
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (1 `op_Multiply` 8)
    bA
    1
    Public
in
let va_b20 = va_tl va_b19 in
let va_s21, va_fc21 =
  va_lemma_Mulx_64 (va_hd va_b20)
    va_s20
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (1 `op_Multiply` 8)
        Public)
in
let va_b21 = va_tl va_b20 in
let va_s22, va_fc22 =
  va_lemma_Adcx_64 (va_hd va_b21)
    va_s21
    (va_coerce_reg_opr64_to_dst_opr64 r1)
    (va_op_opr64_reg64 rRax)
in
let va_b22 = va_tl va_b21 in
let va_s23, va_fc23 =
  va_lemma_Adox_64 (va_hd va_b22)
    va_s22
    (va_coerce_reg_opr64_to_dst_opr64 r2)
    (va_op_opr64_reg64 rRbx)
in
let va_b23 = va_tl va_b22 in
let va_s24, va_fc24 =
  va_lemma_Mem64_lemma (va_hd va_b23)
    va_s23
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (2 `op_Multiply` 8)
    bA
    2
    Public
in
let va_b24 = va_tl va_b23 in
let va_s25, va_fc25 =
  va_lemma_Mulx_64 (va_hd va_b24)
    va_s24
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (2 `op_Multiply` 8)
        Public)
in
let va_b25 = va_tl va_b24 in
let va_s26, va_fc26 =
  va_lemma_Adcx_64 (va_hd va_b25)
    va_s25
    (va_coerce_reg_opr64_to_dst_opr64 r2)
    (va_op_opr64_reg64 rRax)
in
let va_b26 = va_tl va_b25 in
let va_s27, va_fc27 =
  va_lemma_Adox_64 (va_hd va_b26)
    va_s26
    (va_coerce_reg_opr64_to_dst_opr64 r3)
    (va_op_opr64_reg64 rRbx)
in
let va_b27 = va_tl va_b26 in
let va_s28, va_fc28 =
  va_lemma_Mem64_lemma (va_hd va_b27)
    va_s27
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (3 `op_Multiply` 8)
    bA
    3
    Public
in
let va_b28 = va_tl va_b27 in
let va_s29, va_fc29 =
  va_lemma_Mulx_64 (va_hd va_b28)
    va_s28
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (3 `op_Multiply` 8)
        Public)
in
let va_b29 = va_tl va_b28 in
let va_s30, va_fc30 =
  va_lemma_Adcx_64 (va_hd va_b29)
    va_s29
    (va_coerce_reg_opr64_to_dst_opr64 r3)
    (va_op_opr64_reg64 rRax)
in
let va_b30 = va_tl va_b29 in
let va_s31, va_fc31 =
  va_lemma_Adox_64 (va_hd va_b30)
    va_s30
    (va_coerce_reg_opr64_to_dst_opr64 r4)
    (va_op_opr64_reg64 rRbx)
in
let va_b31 = va_tl va_b30 in
let va_s32, va_fc32 =
  va_lemma_Mem64_lemma (va_hd va_b31)
    va_s31
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (4 `op_Multiply` 8)
    bA
    4
    Public
in
let va_b32 = va_tl va_b31 in
let va_s33, va_fc33 =
  va_lemma_Mulx_64 (va_hd va_b32)
    va_s32
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (4 `op_Multiply` 8)
        Public)
in
let va_b33 = va_tl va_b32 in
let va_s34, va_fc34 =
  va_lemma_Adcx_64 (va_hd va_b33)
    va_s33
    (va_coerce_reg_opr64_to_dst_opr64 r4)
    (va_op_opr64_reg64 rRax)
in
let va_b34 = va_tl va_b33 in
let va_s35, va_fc35 =
  va_lemma_Adox_64 (va_hd va_b34)
    va_s34
    (va_coerce_reg_opr64_to_dst_opr64 r5)
    (va_op_opr64_reg64 rRbx)
in
let va_b35 = va_tl va_b34 in
let va_s36, va_fc36 =
  va_lemma_Mem64_lemma (va_hd va_b35)
    va_s35
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (5 `op_Multiply` 8)
    bA
    5
    Public
in
let va_b36 = va_tl va_b35 in
let va_s37, va_fc37 =
  va_lemma_Mulx_64 (va_hd va_b36)
    va_s36
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (5 `op_Multiply` 8)
        Public)
in
let va_b37 = va_tl va_b36 in
let va_s38, va_fc38 =
  va_lemma_Adcx_64 (va_hd va_b37)
    va_s37
    (va_coerce_reg_opr64_to_dst_opr64 r5)
    (va_op_opr64_reg64 rRax)
in
let va_b38 = va_tl va_b37 in
let va_s39, va_fc39 =
  va_lemma_Adox_64 (va_hd va_b38)
    va_s38
    (va_coerce_reg_opr64_to_dst_opr64 r6)
    (va_op_opr64_reg64 rRbx)
in
let va_b39 = va_tl va_b38 in
let va_s40, va_fc40 =
  va_lemma_Mem64_lemma (va_hd va_b39)
    va_s39
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (6 `op_Multiply` 8)
    bA
    6
    Public
in
let va_b40 = va_tl va_b39 in
let va_s41, va_fc41 =
  va_lemma_Mulx_64 (va_hd va_b40)
    va_s40
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (6 `op_Multiply` 8)
        Public)
in
let va_b41 = va_tl va_b40 in
let va_s42, va_fc42 =
  va_lemma_Adcx_64 (va_hd va_b41)
    va_s41
    (va_coerce_reg_opr64_to_dst_opr64 r6)
    (va_op_opr64_reg64 rRax)
in
let va_b42 = va_tl va_b41 in
let va_s43, va_fc43 =
  va_lemma_Adox_64 (va_hd va_b42)
    va_s42
    (va_coerce_reg_opr64_to_dst_opr64 r7)
    (va_op_opr64_reg64 rRbx)
in
let va_b43 = va_tl va_b42 in
let va_s44, va_fc44 =
  va_lemma_Mem64_lemma (va_hd va_b43)
    va_s43
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx)
    (7 `op_Multiply` 8)
    bA
    7
    Public
in
let va_b44 = va_tl va_b43 in
let va_s45, va_fc45 =
  va_lemma_Mulx_64 (va_hd va_b44)
    va_s44
    (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
        (va_op_reg64_reg64 rRcx)
        (7 `op_Multiply` 8)
        Public)
in
let va_b45 = va_tl va_b44 in
let va_s46, va_fc46 =
  va_lemma_Adcx_64 (va_hd va_b45)
    va_s45
    (va_coerce_reg_opr64_to_dst_opr64 r7)
    (va_op_opr64_reg64 rRax)
in
let va_b46 = va_tl va_b45 in
let va_s47, va_fc47 =
  va_lemma_Store64_buffer (va_hd va_b46)
    va_s46
    (va_op_heaplet_mem_heaplet 0)
    (va_op_reg_opr64_reg64 rRdi)
    r0
    0
    Public
    bD
    0
in
let va_b47 = va_tl va_b46 in
let va_s48, va_fc48 =
  va_lemma_Mov64 (va_hd va_b47) va_s47 (va_coerce_reg_opr64_to_dst_opr64 r0) (va_const_opr64 0)
in
let va_b48 = va_tl va_b47 in
let va_s49, va_fc49 =
  va_lemma_Adcx_64 (va_hd va_b48)
    va_s48
    (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_coerce_reg_opr64_to_opr64 r0)
in
let va_b49 = va_tl va_b48 in
let va_s50, va_fc50 =
  va_lemma_Adox_64 (va_hd va_b49)
    va_s49
    (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_op_opr64_reg64 rRbx)
in
let va_b50 = va_tl va_b49 in
let l:(va_int_range 8 8) = 8 in
let ys:(seq nat64) = init_ys b as0 in
let zs:(seq nat64) = init_zs b as0 d in
let qs:(seq nat64) = __proj__Mktuple2__item___1 #(seq nat64) #nat1 (seq_add rs zs 0) in
let xs:(seq nat64) =
  make_seq9 #nat64 (Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s50))
    (va_eval_reg_opr64 va_s50 r1) (va_eval_reg_opr64 va_s50 r2) (va_eval_reg_opr64 va_s50 r3)
    (va_eval_reg_opr64 va_s50 r4) (va_eval_reg_opr64 va_s50 r5) (va_eval_reg_opr64 va_s50 r6)
    (va_eval_reg_opr64 va_s50 r7) (va_eval_reg_opr64 va_s50 r0)
in
lemma_seq_add_is_norm rs zs 0 (l + 1);
lemma_seq_add_is_norm qs ys 0 (l + 1);
lemma_scale_add l b d as0 rs ys zs qs xs;
assert (FStar.Seq.Base.equal #nat64
      xs
      (__proj__Mktuple2__item___1 #(seq nat64) #nat1 (seq_add qs ys 0)));
let va_forall_lemma ()
    : Lemma (requires true)
      (ensures (flag_cf (va_get_flags va_s50) == 0 /\ flag_of (va_get_flags va_s50) == 0)) =
  (Vale.Bignum.Defs.reveal_add_hi_all ();
    ())
in
va_forall_lemma ();
let va_sM, va_f50 = va_lemma_empty_total va_s50 va_b50 in
let va_f49 = va_lemma_merge_total va_b49 va_s49 va_fc50 va_s50 va_f50 va_sM in
let va_f48 = va_lemma_merge_total va_b48 va_s48 va_fc49 va_s49 va_f49 va_sM in
let va_f47 = va_lemma_merge_total va_b47 va_s47 va_fc48 va_s48 va_f48 va_sM in
let va_f46 = va_lemma_merge_total va_b46 va_s46 va_fc47 va_s47 va_f47 va_sM in
let va_f45 = va_lemma_merge_total va_b45 va_s45 va_fc46 va_s46 va_f46 va_sM in
let va_f44 = va_lemma_merge_total va_b44 va_s44 va_fc45 va_s45 va_f45 va_sM in
let va_f43 = va_lemma_merge_total va_b43 va_s43 va_fc44 va_s44 va_f44 va_sM in
let va_f42 = va_lemma_merge_total va_b42 va_s42 va_fc43 va_s43 va_f43 va_sM in
let va_f41 = va_lemma_merge_total va_b41 va_s41 va_fc42 va_s42 va_f42 va_sM in
let va_f40 = va_lemma_merge_total va_b40 va_s40 va_fc41 va_s41 va_f41 va_sM in
let va_f39 = va_lemma_merge_total va_b39 va_s39 va_fc40 va_s40 va_f40 va_sM in
let va_f38 = va_lemma_merge_total va_b38 va_s38 va_fc39 va_s39 va_f39 va_sM in
let va_f37 = va_lemma_merge_total va_b37 va_s37 va_fc38 va_s38 va_f38 va_sM in
let va_f36 = va_lemma_merge_total va_b36 va_s36 va_fc37 va_s37 va_f37 va_sM in
let va_f35 = va_lemma_merge_total va_b35 va_s35 va_fc36 va_s36 va_f36 va_sM in
let va_f34 = va_lemma_merge_total va_b34 va_s34 va_fc35 va_s35 va_f35 va_sM in
let va_f33 = va_lemma_merge_total va_b33 va_s33 va_fc34 va_s34 va_f34 va_sM in
let va_f32 = va_lemma_merge_total va_b32 va_s32 va_fc33 va_s33 va_f33 va_sM in
let va_f31 = va_lemma_merge_total va_b31 va_s31 va_fc32 va_s32 va_f32 va_sM in
let va_f30 = va_lemma_merge_total va_b30 va_s30 va_fc31 va_s31 va_f31 va_sM in
let va_f29 = va_lemma_merge_total va_b29 va_s29 va_fc30 va_s30 va_f30 va_sM in
let va_f28 = va_lemma_merge_total va_b28 va_s28 va_fc29 va_s29 va_f29 va_sM in
let va_f27 = va_lemma_merge_total va_b27 va_s27 va_fc28 va_s28 va_f28 va_sM in
let va_f26 = va_lemma_merge_total va_b26 va_s26 va_fc27 va_s27 va_f27 va_sM in
let va_f25 = va_lemma_merge_total va_b25 va_s25 va_fc26 va_s26 va_f26 va_sM in
let va_f24 = va_lemma_merge_total va_b24 va_s24 va_fc25 va_s25 va_f25 va_sM in
let va_f23 = va_lemma_merge_total va_b23 va_s23 va_fc24 va_s24 va_f24 va_sM in
let va_f22 = va_lemma_merge_total va_b22 va_s22 va_fc23 va_s23 va_f23 va_sM in
let va_f21 = va_lemma_merge_total va_b21 va_s21 va_fc22 va_s22 va_f22 va_sM in
let va_f20 = va_lemma_merge_total va_b20 va_s20 va_fc21 va_s21 va_f21 va_sM in
let va_f19 = va_lemma_merge_total va_b19 va_s19 va_fc20 va_s20 va_f20 va_sM in
let va_f18 = va_lemma_merge_total va_b18 va_s18 va_fc19 va_s19 va_f19 va_sM in
let va_f17 = va_lemma_merge_total va_b17 va_s17 va_fc18 va_s18 va_f18 va_sM in
let va_f16 = va_lemma_merge_total va_b16 va_s16 va_fc17 va_s17 va_f17 va_sM in
let va_f15 = va_lemma_merge_total va_b15 va_s15 va_fc16 va_s16 va_f16 va_sM in
let va_f14 = va_lemma_merge_total va_b14 va_s14 va_fc15 va_s15 va_f15 va_sM in
let va_f13 = va_lemma_merge_total va_b13 va_s13 va_fc14 va_s14 va_f14 va_sM in
let va_f12 = va_lemma_merge_total va_b12 va_s12 va_fc13 va_s13 va_f13 va_sM in
let va_fM = va_lemma_merge_total va_b1 va_s0 va_fc12 va_s12 va_f12 va_sM in
(va_sM, va_fM)
Vale.FDefMulx.X64.fst.checked
Vale.X64.State.fsti.checked Vale.X64.Stack_i.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.InsStack.fsti.checked Vale.X64.InsMem.fsti.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Bignum.X64.fsti.checked Vale.Bignum.Lemmas.fsti.checked Vale.Bignum.Defs.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.FDefMulx.X64.fst
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Vale.X64.Decls.va_operand_reg_opr64 Prims.nat Vale.X64.Memory.buffer64 Vale.X64.Decls.va_fuel FStar.Pervasives.Native.Mktuple2 Vale.X64.Decls.va_lemma_merge_total FStar.Pervasives.Native.tuple2 Vale.X64.State.vale_state Vale.X64.Decls.va_lemma_empty_total Prims.unit Prims.b2t Prims.squash Prims.l_and Prims.eq2 Prims.int Vale.Bignum.X64.flag_cf Vale.X64.State.__proj__Mkvale_state__item__vs_flags Vale.Bignum.X64.flag_of Prims.Nil FStar.Pervasives.pattern Vale.Bignum.Defs.reveal_add_hi_all Vale.X64.Decls.va_get_flags Prims._assert FStar.Seq.Base.equal Vale.Def.Words_s.nat64 FStar.Pervasives.Native.__proj__Mktuple2__item___1 FStar.Seq.Base.seq Vale.Def.Words_s.nat1 Vale.Bignum.Lemmas.seq_add Vale.Def.Words_s.pow2_64 Vale.Bignum.Lemmas.lemma_scale_add Vale.Bignum.Lemmas.lemma_seq_add_is_norm Prims.op_Addition Vale.FDefMulx.X64.make_seq9 Vale.X64.Decls.buffer64_read Vale.X64.Decls.va_get_mem_heaplet Vale.X64.Decls.va_eval_reg_opr64 Vale.Bignum.Lemmas.init_zs Vale.Bignum.Lemmas.init_ys Vale.X64.Decls.va_int_range Prims.list Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_tl Vale.Bignum.X64.va_lemma_Adox_64 Vale.X64.Decls.va_hd Vale.X64.Decls.va_coerce_reg_opr64_to_dst_opr64 Vale.X64.Decls.va_op_opr64_reg64 Vale.X64.Machine_s.rRbx Vale.Bignum.X64.va_lemma_Adcx_64 Vale.X64.Decls.va_coerce_reg_opr64_to_opr64 Vale.X64.InsBasic.va_lemma_Mov64 Vale.X64.Decls.va_const_opr64 Vale.X64.InsMem.va_lemma_Store64_buffer Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Machine_s.rRdi Vale.Arch.HeapTypes_s.Public Vale.X64.Machine_s.rRax Vale.Bignum.X64.va_lemma_Mulx_64 Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Decls.va_opr_code_Mem64 Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.Machine_s.rRcx Prims.op_Multiply Vale.X64.InsMem.va_lemma_Mem64_lemma Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRsi Vale.Bignum.Defs.reveal_add_lo_all Vale.X64.Decls.s64 Vale.X64.Decls.va_get_block Vale.X64.Decls.va_reveal_opaque Vale.FDefMulx.X64.va_code_MulAdd18
module Vale.FDefMulx.X64
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.Stack_i
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.InsMem
open Vale.X64.InsStack
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s
open Vale.Bignum.Defs
open Vale.Bignum.Lemmas
open Vale.Bignum.X64
open FStar.Mul
open FStar.Seq
open Vale.Def.Words_s
unfold let (.[]) = index

//[@"opaque_to_smt"]
let make_seq9 (#a:Type0) (v0 v1 v2 v3 v4 v5 v6 v7 v8:a) : seq a =
  init 9 (fun i ->
    if i = 0 then v0 else
    if i = 1 then v1 else
    if i = 2 then v2 else
    if i = 3 then v3 else
    if i = 4 then v4 else
    if i = 5 then v5 else
    if i = 6 then v6 else
    if i = 7 then v7 else
    v8)

let operand_reg8 (n:nat) : operand64 = oreg (Reg 0 (8 + n % 8))
//-- lemma_seq_add_is_norm
//--
//-- lemma_scale_add
//--
//-- MulAdd18
#push-options "--z3rlimit 80 --max_fuel 1 --max_ifuel 0"

val va_code_MulAdd18 : r0:va_operand_reg_opr64 -> r1:va_operand_reg_opr64 ->
  r2:va_operand_reg_opr64 -> r3:va_operand_reg_opr64 -> r4:va_operand_reg_opr64 ->
  r5:va_operand_reg_opr64 -> r6:va_operand_reg_opr64 -> r7:va_operand_reg_opr64 -> Tot va_code
[@ "opaque_to_smt"]
let va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7 =
  (va_Block (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mov64 (va_op_dst_opr64_reg64
    rRdx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRsi) 0 Public))
    (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Adox_64 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) 0 Public))
    (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64 rRbx)
    (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (0 `op_Multiply` 8) Public)) (va_CCons (va_code_Adcx_64
    (va_coerce_reg_opr64_to_dst_opr64 r0) (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r1) (va_op_opr64_reg64 rRbx)) (va_CCons (va_code_Mem64_lemma
    ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (1 `op_Multiply` 8)
    Public)) (va_CCons (va_code_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r1) (va_op_opr64_reg64
    rRax)) (va_CCons (va_code_Adox_64 (va_coerce_reg_opr64_to_dst_opr64 r2) (va_op_opr64_reg64
    rRbx)) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64
    rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (2 `op_Multiply` 8) Public)) (va_CCons (va_code_Adcx_64
    (va_coerce_reg_opr64_to_dst_opr64 r2) (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r3) (va_op_opr64_reg64 rRbx)) (va_CCons (va_code_Mem64_lemma
    ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (3 `op_Multiply` 8)
    Public)) (va_CCons (va_code_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r3) (va_op_opr64_reg64
    rRax)) (va_CCons (va_code_Adox_64 (va_coerce_reg_opr64_to_dst_opr64 r4) (va_op_opr64_reg64
    rRbx)) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64
    rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (4 `op_Multiply` 8) Public)) (va_CCons (va_code_Adcx_64
    (va_coerce_reg_opr64_to_dst_opr64 r4) (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r5) (va_op_opr64_reg64 rRbx)) (va_CCons (va_code_Mem64_lemma
    ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (5 `op_Multiply` 8)
    Public)) (va_CCons (va_code_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r5) (va_op_opr64_reg64
    rRax)) (va_CCons (va_code_Adox_64 (va_coerce_reg_opr64_to_dst_opr64 r6) (va_op_opr64_reg64
    rRbx)) (va_CCons (va_code_Mem64_lemma ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64
    rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRcx) (6 `op_Multiply` 8) Public)) (va_CCons (va_code_Adcx_64
    (va_coerce_reg_opr64_to_dst_opr64 r6) (va_op_opr64_reg64 rRax)) (va_CCons (va_code_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r7) (va_op_opr64_reg64 rRbx)) (va_CCons (va_code_Mem64_lemma
    ()) (va_CCons (va_code_Mulx_64 (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (7 `op_Multiply` 8)
    Public)) (va_CCons (va_code_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r7) (va_op_opr64_reg64
    rRax)) (va_CCons (va_code_Store64_buffer (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64
    rRdi) r0 0 Public) (va_CCons (va_code_Mov64 (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_const_opr64 0)) (va_CCons (va_code_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_coerce_reg_opr64_to_opr64 r0)) (va_CCons (va_code_Adox_64 (va_coerce_reg_opr64_to_dst_opr64
    r0) (va_op_opr64_reg64 rRbx)) (va_CNil ())))))))))))))))))))))))))))))))))))))))))

val va_codegen_success_MulAdd18 : r0:va_operand_reg_opr64 -> r1:va_operand_reg_opr64 ->
  r2:va_operand_reg_opr64 -> r3:va_operand_reg_opr64 -> r4:va_operand_reg_opr64 ->
  r5:va_operand_reg_opr64 -> r6:va_operand_reg_opr64 -> r7:va_operand_reg_opr64 -> Tot va_pbool
[@ "opaque_to_smt"]
let va_codegen_success_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7 =
  (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mov64
    (va_op_dst_opr64_reg64 rRdx) (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0)
    (va_op_reg64_reg64 rRsi) 0 Public)) (va_pbool_and (va_codegen_success_Mem64_lemma ())
    (va_pbool_and (va_codegen_success_Adox_64 (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_opr_code_Mem64 (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRdi) 0 Public))
    (va_pbool_and (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (0 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r1) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (1 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r1)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r2) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (2 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r2)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r3) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (3 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r3)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r4) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (4 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r4)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r5) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (5 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r5)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r6) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (6 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r6)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r7) (va_op_opr64_reg64 rRbx)) (va_pbool_and
    (va_codegen_success_Mem64_lemma ()) (va_pbool_and (va_codegen_success_Mulx_64
    (va_op_dst_opr64_reg64 rRbx) (va_op_dst_opr64_reg64 rRax) (va_opr_code_Mem64
    (va_op_heaplet_mem_heaplet 0) (va_op_reg64_reg64 rRcx) (7 `op_Multiply` 8) Public))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r7)
    (va_op_opr64_reg64 rRax)) (va_pbool_and (va_codegen_success_Store64_buffer
    (va_op_heaplet_mem_heaplet 0) (va_op_reg_opr64_reg64 rRdi) r0 0 Public) (va_pbool_and
    (va_codegen_success_Mov64 (va_coerce_reg_opr64_to_dst_opr64 r0) (va_const_opr64 0))
    (va_pbool_and (va_codegen_success_Adcx_64 (va_coerce_reg_opr64_to_dst_opr64 r0)
    (va_coerce_reg_opr64_to_opr64 r0)) (va_pbool_and (va_codegen_success_Adox_64
    (va_coerce_reg_opr64_to_dst_opr64 r0) (va_op_opr64_reg64 rRbx)) (va_ttrue
    ()))))))))))))))))))))))))))))))))))))))))


val va_lemma_MulAdd18 : va_b0:va_code -> va_s0:va_state -> r0:va_operand_reg_opr64 ->
  r1:va_operand_reg_opr64 -> r2:va_operand_reg_opr64 -> r3:va_operand_reg_opr64 ->
  r4:va_operand_reg_opr64 -> r5:va_operand_reg_opr64 -> r6:va_operand_reg_opr64 ->
  r7:va_operand_reg_opr64 -> regRotate:nat -> bA:buffer64 -> bB:buffer64 -> bD:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7) va_s0 /\
    va_is_dst_reg_opr64 r0 va_s0 /\ va_is_dst_reg_opr64 r1 va_s0 /\ va_is_dst_reg_opr64 r2 va_s0 /\
    va_is_dst_reg_opr64 r3 va_s0 /\ va_is_dst_reg_opr64 r4 va_s0 /\ va_is_dst_reg_opr64 r5 va_s0 /\
    va_is_dst_reg_opr64 r6 va_s0 /\ va_is_dst_reg_opr64 r7 va_s0 /\ va_get_ok va_s0 /\ (let
    (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet 0
    va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_s0) /\ flag_cf
    (va_get_flags va_s0) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_s0) /\ flag_of
    (va_get_flags va_s0) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in adx_enabled /\ bmi2_enabled /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) bA 8
    (va_get_mem_layout va_s0) Public /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) bB 1 (va_get_mem_layout va_s0) Public /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bD 1
    (va_get_mem_layout va_s0) Public /\ FStar.Seq.Base.length #Vale.Def.Types_s.nat64 as0 == 8 /\
    r0 == operand_reg8 (regRotate + 0) /\ r1 == operand_reg8 (regRotate + 1) /\ r2 == operand_reg8
    (regRotate + 2) /\ r3 == operand_reg8 (regRotate + 3) /\ r4 == operand_reg8 (regRotate + 4) /\
    r5 == operand_reg8 (regRotate + 5) /\ r6 == operand_reg8 (regRotate + 6) /\ r7 == operand_reg8
    (regRotate + 7))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet
    0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_sM) /\ flag_cf
    (va_get_flags va_sM) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_sM) /\ flag_of
    (va_get_flags va_sM) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in let (b:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read bB 0 (va_get_mem_heaplet 0 va_s0) in let
    (d:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s0) in
    let (xs:(seq nat64)) = make_seq9 #nat64 (Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet
    0 va_sM)) (va_eval_reg_opr64 va_sM r1) (va_eval_reg_opr64 va_sM r2) (va_eval_reg_opr64 va_sM
    r3) (va_eval_reg_opr64 va_sM r4) (va_eval_reg_opr64 va_sM r5) (va_eval_reg_opr64 va_sM r6)
    (va_eval_reg_opr64 va_sM r7) (va_eval_reg_opr64 va_sM r0) in sum_pow_seq xs == sum_pow_seq rs +
    b `op_Multiply` sum_pow_seq as0 + d) /\ va_state_eq va_sM (va_update_mem_layout va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_flags va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM (va_update_operand_reg_opr64 r7 va_sM (va_update_operand_reg_opr64 r6 va_sM
    (va_update_operand_reg_opr64 r5 va_sM (va_update_operand_reg_opr64 r4 va_sM
    (va_update_operand_reg_opr64 r3 va_sM (va_update_operand_reg_opr64 r2 va_sM
    (va_update_operand_reg_opr64 r1 va_sM (va_update_operand_reg_opr64 r0 va_sM
    va_s0))))))))))))))))))
[@"opaque_to_smt"]
val va_lemma_MulAdd18 : va_b0:va_code -> va_s0:va_state -> r0:va_operand_reg_opr64 ->
  r1:va_operand_reg_opr64 -> r2:va_operand_reg_opr64 -> r3:va_operand_reg_opr64 ->
  r4:va_operand_reg_opr64 -> r5:va_operand_reg_opr64 -> r6:va_operand_reg_opr64 ->
  r7:va_operand_reg_opr64 -> regRotate:nat -> bA:buffer64 -> bB:buffer64 -> bD:buffer64
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_MulAdd18 r0 r1 r2 r3 r4 r5 r6 r7) va_s0 /\
    va_is_dst_reg_opr64 r0 va_s0 /\ va_is_dst_reg_opr64 r1 va_s0 /\ va_is_dst_reg_opr64 r2 va_s0 /\
    va_is_dst_reg_opr64 r3 va_s0 /\ va_is_dst_reg_opr64 r4 va_s0 /\ va_is_dst_reg_opr64 r5 va_s0 /\
    va_is_dst_reg_opr64 r6 va_s0 /\ va_is_dst_reg_opr64 r7 va_s0 /\ va_get_ok va_s0 /\ (let
    (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet 0
    va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_s0) /\ flag_cf
    (va_get_flags va_s0) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_s0) /\ flag_of
    (va_get_flags va_s0) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in adx_enabled /\ bmi2_enabled /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRcx va_s0) bA 8
    (va_get_mem_layout va_s0) Public /\ Vale.X64.Decls.validSrcAddrs64 (va_get_mem_heaplet 0 va_s0)
    (va_get_reg64 rRsi va_s0) bB 1 (va_get_mem_layout va_s0) Public /\
    Vale.X64.Decls.validDstAddrs64 (va_get_mem_heaplet 0 va_s0) (va_get_reg64 rRdi va_s0) bD 1
    (va_get_mem_layout va_s0) Public /\ FStar.Seq.Base.length #Vale.Def.Types_s.nat64 as0 == 8 /\
    r0 == operand_reg8 (regRotate + 0) /\ r1 == operand_reg8 (regRotate + 1) /\ r2 == operand_reg8
    (regRotate + 2) /\ r3 == operand_reg8 (regRotate + 3) /\ r4 == operand_reg8 (regRotate + 4) /\
    r5 == operand_reg8 (regRotate + 5) /\ r6 == operand_reg8 (regRotate + 6) /\ r7 == operand_reg8
    (regRotate + 7))))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) = Vale.X64.Decls.s64 (va_get_mem_heaplet
    0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64 (va_eval_reg_opr64 va_s0 r0)
    (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2) (va_eval_reg_opr64 va_s0 r3)
    (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5) (va_eval_reg_opr64 va_s0 r6)
    (va_eval_reg_opr64 va_s0 r7) 0 in Vale.X64.Decls.valid_cf (va_get_flags va_sM) /\ flag_cf
    (va_get_flags va_sM) == 0 /\ (Vale.X64.Decls.valid_of (va_get_flags va_sM) /\ flag_of
    (va_get_flags va_sM) == 0)) /\ (let (as0:(FStar.Seq.Base.seq Vale.Def.Types_s.nat64)) =
    Vale.X64.Decls.s64 (va_get_mem_heaplet 0 va_s0) bA in let (rs:(seq nat64)) = make_seq9 #nat64
    (va_eval_reg_opr64 va_s0 r0) (va_eval_reg_opr64 va_s0 r1) (va_eval_reg_opr64 va_s0 r2)
    (va_eval_reg_opr64 va_s0 r3) (va_eval_reg_opr64 va_s0 r4) (va_eval_reg_opr64 va_s0 r5)
    (va_eval_reg_opr64 va_s0 r6) (va_eval_reg_opr64 va_s0 r7) 0 in let (b:Vale.Def.Types_s.nat64) =
    Vale.X64.Decls.buffer64_read bB 0 (va_get_mem_heaplet 0 va_s0) in let
    (d:Vale.Def.Types_s.nat64) = Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet 0 va_s0) in
    let (xs:(seq nat64)) = make_seq9 #nat64 (Vale.X64.Decls.buffer64_read bD 0 (va_get_mem_heaplet
    0 va_sM)) (va_eval_reg_opr64 va_sM r1) (va_eval_reg_opr64 va_sM r2) (va_eval_reg_opr64 va_sM
    r3) (va_eval_reg_opr64 va_sM r4) (va_eval_reg_opr64 va_sM r5) (va_eval_reg_opr64 va_sM r6)
    (va_eval_reg_opr64 va_sM r7) (va_eval_reg_opr64 va_sM r0) in sum_pow_seq xs == sum_pow_seq rs +
    b `op_Multiply` sum_pow_seq as0 + d) /\ va_state_eq va_sM (va_update_mem_layout va_sM
    (va_update_mem_heaplet 0 va_sM (va_update_flags va_sM (va_update_reg64 rRdx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM (va_update_mem
    va_sM (va_update_operand_reg_opr64 r7 va_sM (va_update_operand_reg_opr64 r6 va_sM
    (va_update_operand_reg_opr64 r5 va_sM (va_update_operand_reg_opr64 r4 va_sM
    (va_update_operand_reg_opr64 r3 va_sM (va_update_operand_reg_opr64 r2 va_sM
    (va_update_operand_reg_opr64 r1 va_sM (va_update_operand_reg_opr64 r0 va_sM
    va_s0))))))))))))))))))

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    r0: Vale.X64.Decls.va_operand_reg_opr64 ->
    r1: Vale.X64.Decls.va_operand_reg_opr64 ->
    r2: Vale.X64.Decls.va_operand_reg_opr64 ->
    r3: Vale.X64.Decls.va_operand_reg_opr64 ->
    r4: Vale.X64.Decls.va_operand_reg_opr64 ->
    r5: Vale.X64.Decls.va_operand_reg_opr64 ->
    r6: Vale.X64.Decls.va_operand_reg_opr64 ->
    r7: Vale.X64.Decls.va_operand_reg_opr64 ->
    regRotate: Prims.nat ->
    bA: Vale.X64.Memory.buffer64 ->
    bB: Vale.X64.Memory.buffer64 ->
    bD: Vale.X64.Memory.buffer64
  -> Prims.Ghost (Vale.X64.Decls.va_state * Vale.X64.Decls.va_fuel)