let ins_exchange_sanity_check1 =
  assert_norm !!(ins_exchange_sanity_check1_1);
  assert_norm !!(ins_exchange_sanity_check1_2)
let ins_exchange_sanity_check1 =
assert_norm !!(ins_exchange_sanity_check1_1);
assert_norm !!(ins_exchange_sanity_check1_2)
Vale.Transformers.InstructionReorderSanityChecks.fst.checked
Vale.X64.Print_s.fst.checked Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.X64.Instructions_s.fsti.checked Vale.X64.Instruction_s.fsti.checked Vale.X64.InsLemmas.fsti.checked Vale.X64.Bytes_Code_s.fst.checked Vale.Transformers.Locations.fst.checked Vale.Transformers.Locations.fst.checked Vale.Transformers.InstructionReorder.fst.checked Vale.Transformers.BoundedInstructionEffects.fst.checked Vale.Transformers.BoundedInstructionEffects.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Vale.Transformers.InstructionReorderSanityChecks.fst
FStar.Pervasives.assert_norm Prims.b2t Vale.Def.PossiblyMonad.op_Bang_Bang Vale.Transformers.InstructionReorderSanityChecks.ins_exchange_sanity_check1_2 Prims.unit Vale.Transformers.InstructionReorderSanityChecks.ins_exchange_sanity_check1_1
module Vale.Transformers.InstructionReorderSanityChecks

open Vale.X64.Bytes_Code_s
open Vale.X64.Instruction_s
open Vale.X64.Instructions_s
open Vale.X64.Machine_Semantics_s
open Vale.X64.Machine_s
open Vale.X64.Print_s

open Vale.X64.InsLemmas // this one is from [code]; is that ok?; we use it primarily for the sanity checks

open Vale.Def.PossiblyMonad

open Vale.Transformers.Locations
friend Vale.Transformers.Locations

open Vale.Transformers.BoundedInstructionEffects
friend Vale.Transformers.BoundedInstructionEffects

open Vale.Transformers.InstructionReorder

#push-options "--lax" (* XXX: This part of the file causes an F* SMTEncoding bug. I've reported it, and once it is fixed, we should remove this --lax *)
let ins_exchange_sanity_check1_1 : pbool =
  normalize_term (
    ins_exchange_allowed
      (make_instr ins_IMul64 (OReg rRax) (OReg rRbx))
      (make_instr ins_IMul64 (OReg rRcx) (OReg rRdx))
    )

let ins_exchange_sanity_check1_2 : pbool =
  normalize_term (
    ins_exchange_allowed
      (make_instr ins_Mov64 (OReg rRax) (OConst 100))
      (make_instr ins_Add64 (OReg rRbx) (OConst 299))
  )
val ins_exchange_sanity_check1 : Prims.unit
Prims.unit