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
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_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
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
                                                                                                                                                                ()

                                                                                                                                                            )

                                                                                                                                                        )

                                                                                                                                                    )

                                                                                                                                                )

                                                                                                                                            )

                                                                                                                                        )

                                                                                                                                    )

                                                                                                                                )

                                                                                                                            )

                                                                                                                        )

                                                                                                                    )

                                                                                                                )

                                                                                                            )

                                                                                                        )

                                                                                                    )
                                                                                                  ))
                                                                                        ))))))))))))
                                        )))))))))))
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_operand_reg_opr64 Vale.X64.Decls.va_pbool_and Vale.X64.InsMem.va_codegen_success_Mem64_lemma Vale.X64.InsBasic.va_codegen_success_Mov64 Vale.X64.Decls.va_op_dst_opr64_reg64 Vale.X64.Machine_s.rRdx Vale.X64.Decls.va_opr_code_Mem64 Vale.X64.Decls.va_op_heaplet_mem_heaplet Vale.X64.Decls.va_op_reg64_reg64 Vale.X64.Machine_s.rRsi Vale.Arch.HeapTypes_s.Public Vale.Bignum.X64.va_codegen_success_Adox_64 Vale.X64.Decls.va_coerce_reg_opr64_to_dst_opr64 Vale.X64.Machine_s.rRdi Vale.Bignum.X64.va_codegen_success_Mulx_64 Vale.X64.Machine_s.rRbx Vale.X64.Machine_s.rRax Vale.X64.Machine_s.rRcx Prims.op_Multiply Vale.Bignum.X64.va_codegen_success_Adcx_64 Vale.X64.Decls.va_op_opr64_reg64 Vale.X64.InsMem.va_codegen_success_Store64_buffer Vale.X64.Decls.va_op_reg_opr64_reg64 Vale.X64.Decls.va_const_opr64 Vale.X64.Decls.va_coerce_reg_opr64_to_opr64 Vale.X64.Decls.va_ttrue Vale.X64.Decls.va_pbool
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"]
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

    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
  -> Vale.X64.Decls.va_pbool