val lemma_machine_eval_ins_st_only_affects_write (i: ins{Instr? i}) (s: machine_state)
    : Lemma
    (ensures
      ((let w = (rw_set_of_ins i).loc_writes in
          (unchanged_except w s (run (machine_eval_ins_st i) s)))))
let lemma_machine_eval_ins_st_only_affects_write (i:ins{Instr? i}) (s:machine_state) :
  Lemma
    (ensures (
       (let w = (rw_set_of_ins i).loc_writes in
        (unchanged_except w s (run (machine_eval_ins_st i) s))))) =
  FStar.Classical.forall_intro (
    FStar.Classical.move_requires (lemma_machine_eval_ins_st_only_affects_write_aux i s))
val lemma_machine_eval_ins_st_only_affects_write (i: ins{Instr? i}) (s: machine_state)
    : Lemma
    (ensures
      ((let w = (rw_set_of_ins i).loc_writes in
          (unchanged_except w s (run (machine_eval_ins_st i) s)))))
let lemma_machine_eval_ins_st_only_affects_write (i: ins{Instr? i}) (s: machine_state)
    : Lemma
    (ensures
      ((let w = (rw_set_of_ins i).loc_writes in
          (unchanged_except w s (run (machine_eval_ins_st i) s))))) =
FStar.Classical.forall_intro (FStar.Classical.move_requires (lemma_machine_eval_ins_st_only_affects_write_aux
          i
          s))
Vale.Transformers.BoundedInstructionEffects.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.Bytes_Code_s.fst.checked Vale.Transformers.Locations.fst.checked Vale.Transformers.Locations.fst.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Vale.Transformers.BoundedInstructionEffects.fst
Vale.X64.Machine_Semantics_s.ins Prims.b2t Vale.X64.Bytes_Code_s.uu___is_Instr Vale.X64.Machine_Semantics_s.instr_annotation Vale.X64.Machine_Semantics_s.machine_state FStar.Classical.forall_intro Vale.Transformers.Locations.location Prims.l_imp Vale.Def.PossiblyMonad.op_Bang_Bang Vale.Transformers.Locations.disjoint_location_from_locations Vale.Transformers.BoundedInstructionEffects.__proj__Mkrw_set__item__loc_writes Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins Prims.eq2 Vale.Transformers.Locations.location_val_t Vale.Transformers.Locations.eval_location Vale.X64.Machine_Semantics_s.run Vale.X64.Machine_Semantics_s.machine_eval_ins_st FStar.Classical.move_requires Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_only_affects_write_aux Prims.unit Prims.l_True Prims.squash Vale.Transformers.BoundedInstructionEffects.unchanged_except Prims.list Prims.Nil FStar.Pervasives.pattern
module Vale.Transformers.BoundedInstructionEffects

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.Def.PossiblyMonad

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

module L = FStar.List.Tot


let locations_of_maddr (m:maddr) (mem:location) : locations =
  mem :: (
    match m with
    | MConst _ -> []
    | MReg r _ -> [ALocReg r]
    | MIndex b _ i _ -> [ALocReg b; ALocReg i]
  )

let locations_of_operand64 (o:operand64) : locations & locations =
  match o with
  | OConst _ -> [], []
  | OReg r -> [], [ALocReg (Reg 0 r)]
  | OMem (m, _) -> locations_of_maddr m ALocMem, [ALocMem]
  | OStack (m, _) -> (ALocReg (Reg 0 rRsp)) :: locations_of_maddr m ALocStack, [ALocStack]

let locations_of_operand128 (o:operand128) : locations & locations =
  match o with
  | OConst _ -> [], []
  | OReg r -> [], [ALocReg (Reg 1 r)]
  | OMem (m, _) -> locations_of_maddr m ALocMem, [ALocMem]
  | OStack (m, _) -> (ALocReg (Reg 0 rRsp)) :: locations_of_maddr m ALocStack, [ALocStack]

let locations_of_explicit (t:instr_operand_explicit) (i:instr_operand_t t) : locations & locations =
  match t with
  | IOp64 -> locations_of_operand64 i
  | IOpXmm -> locations_of_operand128 i

let locations_of_implicit (t:instr_operand_implicit) : locations & locations =
  match t with
  | IOp64One i -> locations_of_operand64 i
  | IOpXmmOne i -> locations_of_operand128 i
  | IOpFlagsCf -> [], [ALocCf]
  | IOpFlagsOf -> [], [ALocOf]

let both (x: locations & locations) =
  let a, b = x in
  a `L.append` b

let rec aux_read_set0 (args:list instr_operand) (oprs:instr_operands_t_args args) : locations =
  match args with
  | [] -> []
  | (IOpEx i) :: args ->
    let l, r = coerce #(instr_operand_t i & instr_operands_t_args args) oprs in
    both (locations_of_explicit i l) `L.append` aux_read_set0 args r
  | (IOpIm i) :: args ->
    both (locations_of_implicit i) `L.append` aux_read_set0 args (coerce #(instr_operands_t_args args) oprs)

let rec aux_read_set1
    (outs:list instr_out) (args:list instr_operand) (oprs:instr_operands_t outs args) : locations =
  match outs with
  | [] -> aux_read_set0 args oprs
  | (Out, IOpEx i) :: outs ->
    let l, r = coerce #(instr_operand_t i & instr_operands_t outs args) oprs in
    fst (locations_of_explicit i l) `L.append` aux_read_set1 outs args r
  | (InOut, IOpEx i) :: outs ->
    let l, r = coerce #(instr_operand_t i & instr_operands_t outs args) oprs in
    both (locations_of_explicit i l) `L.append` aux_read_set1 outs args r
  | (Out, IOpIm i) :: outs ->
    fst (locations_of_implicit i) `L.append` aux_read_set1 outs args (coerce #(instr_operands_t outs args) oprs)
  | (InOut, IOpIm i) :: outs ->
    both (locations_of_implicit i) `L.append` aux_read_set1 outs args (coerce #(instr_operands_t outs args) oprs)

let read_set (i:instr_t_record) (oprs:instr_operands_t i.outs i.args) : locations =
  aux_read_set1 i.outs i.args oprs

let rec aux_write_set
    (outs:list instr_out) (args:list instr_operand) (oprs:instr_operands_t outs args) : locations =
  match outs with
  | [] -> []
  | (_, IOpEx i) :: outs ->
    let l, r = coerce #(instr_operand_t i & instr_operands_t outs args) oprs in
    snd (locations_of_explicit i l) `L.append` aux_write_set outs args r
  | (_, IOpIm i) :: outs ->
    snd (locations_of_implicit i) `L.append` aux_write_set outs args (coerce #(instr_operands_t outs args) oprs)

let write_set (i:instr_t_record) (oprs:instr_operands_t i.outs i.args) : list location =
  let InstrTypeRecord #outs #args #havoc_flags _ = i in
  let ws = aux_write_set outs args oprs in
  match havoc_flags with
  | HavocFlags -> ALocCf :: ALocOf :: ws
  | PreserveFlags -> ws

let constant_writes (i:instr_t_record) (oprs:instr_operands_t i.outs i.args) : locations_with_values =
  let InstrTypeRecord #outs #args #havoc_flags _ = i in
  match havoc_flags with
  | HavocFlags -> (
      let ws = aux_write_set outs args oprs in
      let cr = [] in
      let cr = if L.mem ALocCf ws then cr else (| ALocCf, None |) :: cr in
      let cr = if L.mem ALocOf ws then cr else (| ALocOf, None |) :: cr in
      cr
    )
  | PreserveFlags -> []

(* See fsti *)
let rw_set_of_ins i =
  match i with
  | Instr i oprs _ ->
    {
      loc_reads = read_set i oprs;
      loc_writes = write_set i oprs;
      loc_constant_writes = constant_writes i oprs;
    }
  | Push src t ->
    {
      loc_reads = ALocReg (Reg 0 rRsp) :: ALocStack :: both (locations_of_operand64 src);
      loc_writes = [ALocReg (Reg 0 rRsp); ALocStack];
      loc_constant_writes = [];
    }
  | Pop dst t ->
    {
      loc_reads = ALocReg (Reg 0 rRsp) :: ALocStack :: fst (locations_of_operand64 dst);
      loc_writes = ALocReg (Reg 0 rRsp) :: snd (locations_of_operand64 dst);
      loc_constant_writes = [];
    }
  | Alloc _ ->
    {
      loc_reads = [ALocReg (Reg 0 rRsp)];
      loc_writes = [ALocReg (Reg 0 rRsp)];
      loc_constant_writes = [];
    }
  | Dealloc _ ->
    {
      loc_reads = [ALocStack; ALocReg (Reg 0 rRsp)];
      loc_writes = [ALocStack; ALocReg (Reg 0 rRsp)];
      loc_constant_writes = [];
    }

(* See fsti *)
let locations_of_ocmp o =
  match o with
  | OEq o1 o2
  | ONe o1 o2
  | OLe o1 o2
  | OGe o1 o2
  | OLt o1 o2
  | OGt o1 o2 ->
    both (locations_of_operand64 o1) `L.append` both (locations_of_operand64 o2)

#push-options "--z3rlimit 50 --initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1"
#restart-solver
let rec lemma_instr_write_outputs_only_affects_write
    (outs:list instr_out) (args:list instr_operand)
    (vs:instr_ret_t outs) (oprs:instr_operands_t outs args) (s_orig s:machine_state)
    (a:location) :
  Lemma
    (requires (
        let w = aux_write_set outs args oprs in
        !!(disjoint_location_from_locations a w)))
    (ensures (
        (eval_location a s == eval_location a (instr_write_outputs outs args vs oprs s_orig s)))) =
  match outs with
  | [] -> ()
  | (_, i) :: outs -> (
      let ((v:instr_val_t i), (vs:instr_ret_t outs)) =
        match outs with
        | [] -> (vs, ())
        | _::_ -> let vs = coerce vs in (fst vs, snd vs)
        in
      match i with
      | IOpEx i ->
        let oprs = coerce oprs in
        let s = instr_write_output_explicit i v (fst oprs) s_orig s in
        lemma_instr_write_outputs_only_affects_write outs args vs (snd oprs) s_orig s a
      | IOpIm i ->
        let s = instr_write_output_implicit i v s_orig s in
        lemma_instr_write_outputs_only_affects_write outs args vs (coerce oprs) s_orig s a
    )
#pop-options

#push-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1"
let lemma_eval_instr_only_affects_write
    (it:instr_t_record) (oprs:instr_operands_t it.outs it.args) (ann:instr_annotation it)
    (s0:machine_state)
    (a:location) :
  Lemma
    (requires (
        (let w = (rw_set_of_ins (Instr it oprs ann)).loc_writes in
         !!(disjoint_location_from_locations a w) /\
         (Some? (eval_instr it oprs ann s0)))))
    (ensures (
        (eval_location a s0 == eval_location a (Some?.v (eval_instr it oprs ann s0))))) =
  let InstrTypeRecord #outs #args #havoc_flags' i = it in
  let vs = instr_apply_eval outs args (instr_eval i) oprs s0 in
  let s1 =
    match havoc_flags' with
    | HavocFlags -> {s0 with ms_flags = havoc_flags}
    | PreserveFlags -> s0
  in
  let Some vs = vs in
  let _ = instr_write_outputs outs args vs oprs s0 s1 in
  lemma_instr_write_outputs_only_affects_write outs args vs oprs s0 s1 a
#pop-options

let lemma_machine_eval_ins_st_only_affects_write_aux (i:ins{Instr? i}) (s:machine_state) (a:location) :
  Lemma
    (requires (
        let w = (rw_set_of_ins i).loc_writes in
        (!!(disjoint_location_from_locations a w))))
    (ensures (
        (eval_location a s == eval_location a (run (machine_eval_ins_st i) s)))) =
  let Instr it oprs ann = i in
  match eval_instr it oprs ann s with
  | Some _ -> lemma_eval_instr_only_affects_write it oprs ann s a
  | None -> ()

let lemma_machine_eval_ins_st_only_affects_write (i:ins{Instr? i}) (s:machine_state) :
  Lemma
    (ensures (
       (let w = (rw_set_of_ins i).loc_writes in
val lemma_machine_eval_ins_st_only_affects_write (i: ins{Instr? i}) (s: machine_state)
    : Lemma
    (ensures
      ((let w = (rw_set_of_ins i).loc_writes in
          (unchanged_except w s (run (machine_eval_ins_st i) s)))))
i: Vale.X64.Machine_Semantics_s.ins{Instr? i} -> s: Vale.X64.Machine_Semantics_s.machine_state
  -> FStar.Pervasives.Lemma
    (ensures
      (let w = Mkrw_set?.loc_writes (Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins i) in
        Vale.Transformers.BoundedInstructionEffects.unchanged_except w
          s
          (Vale.X64.Machine_Semantics_s.run (Vale.X64.Machine_Semantics_s.machine_eval_ins_st i) s))
    )