val get_index_of_pc_among_return_pcs_offset
      (hpcs: array_t pc_t)
      (is_return_hpc: array_t bool {array_len is_return_hpc = array_len hpcs})
      (offset: nat{offset <= array_len hpcs})
      (pc: pc_t)
    : Ghost nat
      (requires list_contains pc (make_return_pcs_offset hpcs is_return_hpc offset))
      (ensures
        fun idx ->
          idx < array_len hpcs /\ array_index hpcs idx = pc /\ array_index is_return_hpc idx = true)
      (decreases array_len hpcs - offset)
val get_index_of_pc_among_return_pcs_offset
      (hpcs: array_t pc_t)
      (is_return_hpc: array_t bool {array_len is_return_hpc = array_len hpcs})
      (offset: nat{offset <= array_len hpcs})
      (pc: pc_t)
    : Ghost nat
      (requires list_contains pc (make_return_pcs_offset hpcs is_return_hpc offset))
      (ensures
        fun idx ->
          idx < array_len hpcs /\ array_index hpcs idx = pc /\ array_index is_return_hpc idx = true)
      (decreases array_len hpcs - offset)
let rec get_index_of_pc_among_return_pcs_offset
  (hpcs: array_t pc_t)
  (is_return_hpc: array_t bool{array_len is_return_hpc = array_len hpcs})
  (offset: nat{offset <= array_len hpcs})
  (pc: pc_t)
  : Ghost nat
  (requires list_contains pc (make_return_pcs_offset hpcs is_return_hpc offset))
  (ensures fun idx -> idx < array_len hpcs /\ array_index hpcs idx = pc /\ array_index is_return_hpc idx = true)
  (decreases array_len hpcs - offset) =
  if offset = array_len hpcs then
    false_elim ()
  else if array_index is_return_hpc offset = true then (
    if array_index hpcs offset = pc then
      offset
    else
      get_index_of_pc_among_return_pcs_offset hpcs is_return_hpc (offset + 1) pc
  )
  else
    get_index_of_pc_among_return_pcs_offset hpcs is_return_hpc (offset + 1) pc
module Strategies.VarIntro.Efficient

open Armada.Action
open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.Breaking
open Strategies.GlobalVars
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.VarIntro
open Strategies.Invariant
open Strategies.Nonyielding
open Strategies.PCIndices
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarIntro.Defs
open Strategies.VarIntro.Inefficient
open Strategies.VarIntro.Relation
open Util.ImmutableArray
open Util.List
open Util.Nth
open Util.Range
open Util.Relation

let default_pc: pc_t = ""

let make_pc_index_to_pc
  (pcs: array_t pc_t)
  (idx: nat)
  : GTot pc_t =
  match array_nth pcs idx with
  | None -> default_pc
  | Some pc -> pc

let make_pc_indices_to_pcs
  (pcs: array_t pc_t)
  (pc_indices: list nat)
  : GTot (list pc_t) =
  map_ghost (make_pc_index_to_pc pcs) pc_indices

let make_hpc_to_lpc
  (hpcs: array_t pc_t)
  (lpcs: array_t pc_t)
  (hpc_to_lpc: array_t nat{array_len hpc_to_lpc = array_len hpcs})
  (hpc: pc_t)
  : GTot pc_t =
  match find_in_array hpcs hpc with
  | None -> default_pc
  | Some hpc_index ->
      let lpc_index = array_index hpc_to_lpc hpc_index in
      make_pc_index_to_pc lpcs lpc_index

let make_lpc_to_hpcs
  (hpcs: array_t pc_t)
  (lpcs: array_t pc_t)
  (lpc_to_hpcs: array_t (list nat){array_len lpc_to_hpcs = array_len lpcs})
  (lpc: pc_t)
  : GTot (list pc_t) =
  match find_in_array lpcs lpc with
  | None -> []
  | Some lpc_index ->
      let hpc_indices = array_index lpc_to_hpcs lpc_index in
      make_pc_indices_to_pcs hpcs hpc_indices

let rec make_return_pcs_offset
  (pcs: array_t pc_t)
  (is_return_pc: array_t bool{array_len is_return_pc = array_len pcs})
  (offset: nat{offset <= array_len pcs})
  : GTot (list pc_t) (decreases array_len pcs - offset) =
  if offset = array_len pcs then
    []
  else if array_index is_return_pc offset = true then
    (array_index pcs offset) :: make_return_pcs_offset pcs is_return_pc (offset + 1)
  else
    make_return_pcs_offset pcs is_return_pc (offset + 1)

let make_return_pcs
  (pcs: array_t pc_t)
  (is_return_pc: array_t bool{array_len is_return_pc = array_len pcs})
  : GTot (list pc_t) =
  make_return_pcs_offset pcs is_return_pc 0

let make_is_nonyielding_pc
  (pcs: array_t pc_t)
  (is_nonyielding_pc: array_t bool{array_len is_nonyielding_pc = array_len pcs})
  (pc: pc_t)
  : GTot bool =
  match find_in_array pcs pc with
  | None -> false
  | Some idx -> array_index is_nonyielding_pc idx

let make_is_breaking_pc
  (pcs: array_t pc_t)
  (is_breaking_pc: array_t bool{array_len is_breaking_pc = array_len pcs})
  (pc: pc_t)
  : GTot bool =
  match find_in_array pcs pc with
  | None -> false
  | Some idx -> array_index is_breaking_pc idx

let make_hpc_info
  (vs: list var_id_t)
  (tds: list object_td_t)
  (inv: invariant_t Armada.State.t)
  (hpcs: array_t pc_t)
  (hpc_info: array_t (efficient_hpc_info_t vs tds inv){array_len hpc_info = array_len hpcs})
  (hpc: pc_t)
  : GTot (hpc_info_t vs tds inv) =
  match find_in_array hpcs hpc with
  | None -> HPCInfoNormal
  | Some hpc_index ->
      (match array_index hpc_info hpc_index with
       | EfficientHPCInfoNormal -> HPCInfoNormal
       | EfficientHPCInfoIntroduced idx end_pc introduction_succeeds_witnesses progress ->
           HPCInfoIntroduced idx (make_pc_index_to_pc hpcs end_pc) introduction_succeeds_witnesses progress)

let convert_efficient_thread_state
  (pcs: array_t pc_t)
  (ts: efficient_thread_state_t)
  : GTot thread_state_t =
  match ts with
  | EfficientThreadStateRunning -> ThreadStateRunning
  | EfficientThreadStateAtPC pc -> ThreadStateAtPC (make_pc_index_to_pc pcs pc)
  | EfficientThreadStateNotRunning status -> ThreadStateNotRunning status
  | EfficientThreadStateProcessStopped stop_reason -> ThreadStateProcessStopped stop_reason

let array_to_list_contains_array_nth_ambient
  (pcs: array_t pc_t)
  (idx: nat)
  : Lemma (requires Some? (array_nth pcs idx))
          (ensures  list_contains (Some?.v (array_nth pcs idx)) (array_to_list pcs))
          [SMTPat  (Some? (array_nth pcs idx))] =
  match array_nth pcs idx with
  | Some pc ->
      array_to_list_implies_array_matches_list pcs (array_to_list pcs);        
      array_matches_list_implies_nth_equivalent pcs (array_to_list pcs) idx;
      nth_implies_contains (array_to_list pcs) idx pc

let optional_pc_matches_optional_pc_index_ambient
  (pcs: array_t pc_t)
  (optional_pc: option pc_t)
  (optional_index: option nat)
  : Lemma (requires optional_pc_matches_optional_pc_index pcs optional_pc optional_index)
          (ensures  (match optional_pc with
                     | None -> True
                     | Some pc -> list_contains pc (array_to_list pcs)))
          [SMTPat (optional_pc_matches_optional_pc_index pcs optional_pc optional_index)] =
  match optional_pc, optional_index with
  | Some pc, Some idx ->
      array_to_list_implies_array_matches_list pcs (array_to_list pcs);
      array_matches_list_implies_index_equivalent pcs (array_to_list pcs) idx;
      index_implies_contains (array_to_list pcs) idx pc
  | _, _ -> ()

let find_in_array_inverts_index
  (pcs: array_t pc_t)
  (idx: nat)
  : Lemma (requires   Some? (array_nth pcs idx)
                    /\ array_elements_unique pcs)
          (ensures  find_in_array pcs (array_index pcs idx) = Some idx)
          [SMTPat   (find_in_array pcs (array_index pcs idx))] =
  array_elements_unique_implication pcs

let make_pc_indices_to_pcs_contains_pc_implies_pc_indices_contains_index
  (pcs: array_t pc_t)
  (pc_indices: list nat)
  (pc: pc_t)
  (idx: nat)
  : Lemma (requires   list_contains pc (make_pc_indices_to_pcs pcs pc_indices)
                    /\ array_nth pcs idx = Some pc
                    /\ array_elements_unique pcs
                    /\ (forall (idx: nat). list_contains idx pc_indices ==> idx < array_len pcs))
          (ensures  list_contains idx pc_indices) =
  let idx' = reverse_map_element_of_map_ghost (make_pc_index_to_pc pcs) pc_indices pc in
  array_elements_unique_implication pcs;
  assert (idx' = idx)

let rec make_return_pcs_offset_contains_return_pc
  (pcs: array_t pc_t)
  (is_return_pc: array_t bool{array_len is_return_pc = array_len pcs})
  (offset: nat{offset <= array_len pcs})
  (idx: nat{offset <= idx /\ idx < array_len pcs})
  : Lemma (requires array_index is_return_pc idx = true)
          (ensures  list_contains (array_index pcs idx) (make_return_pcs_offset pcs is_return_pc offset))
          (decreases idx - offset) =
  if offset = array_len pcs then
    false_elim ()
  else if idx = offset && array_index is_return_pc offset = true then
    ()
  else
    make_return_pcs_offset_contains_return_pc pcs is_return_pc (offset + 1) idx

let make_return_pcs_contains_return_pc
  (pcs: array_t pc_t)
  (is_return_pc: array_t bool{array_len is_return_pc = array_len pcs})
  (idx: nat{idx < array_len is_return_pc})
  : Lemma (requires array_index is_return_pc idx = true)
          (ensures  list_contains (array_index pcs idx) (make_return_pcs pcs is_return_pc)) =
  make_return_pcs_offset_contains_return_pc pcs is_return_pc 0 idx

let lpc_hpc_relation_facts
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (hpc_to_lpc: array_t nat{array_len hpc_to_lpc = array_len hpcs})
  (is_return_hpc: array_t bool{array_len is_return_hpc = array_len hpcs})
  : Lemma (requires array_elements_unique hpcs)
          (ensures  (let index_relation = efficient_hl_pc_relation hpc_to_lpc in
                     let index_return_relation = efficient_hl_pc_return_relation hpc_to_lpc is_return_hpc in
                     let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
                     let inefficient_return_hpcs = make_return_pcs hpcs is_return_hpc in
                     let pc_relation = lpc_hpc_pc_relation inefficient_hpc_to_lpc in
                     let pc_return_relation = lpc_hpc_pc_return_relation inefficient_hpc_to_lpc
                                                inefficient_return_hpcs in
                     forall (lidx: nat) (hidx: nat). lidx < array_len lpcs /\ hidx < array_len hpcs ==>
                         (let lpc = array_index lpcs lidx in
                          let hpc = array_index hpcs hidx in
                            (index_relation lidx hidx ==> pc_relation lpc hpc)
                          /\ (index_return_relation lidx hidx ==> pc_return_relation lpc hpc)))) =
  let index_relation = efficient_hl_pc_relation hpc_to_lpc in
  let index_return_relation = efficient_hl_pc_return_relation hpc_to_lpc is_return_hpc in
  let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
  let inefficient_return_hpcs = make_return_pcs hpcs is_return_hpc in
  let pc_relation = lpc_hpc_pc_relation inefficient_hpc_to_lpc in
  let pc_return_relation = lpc_hpc_pc_return_relation inefficient_hpc_to_lpc inefficient_return_hpcs in
  let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
  let inefficient_return_hpcs = make_return_pcs hpcs is_return_hpc in
  introduce forall (lidx: nat) (hidx: nat). lidx < array_len lpcs /\ hidx < array_len hpcs ==>
                         (let lpc = array_index lpcs lidx in
                          let hpc = array_index hpcs hidx in
                            (index_relation lidx hidx ==> pc_relation lpc hpc)
                          /\ (index_return_relation lidx hidx ==> pc_return_relation lpc hpc))
  with introduce _ ==> _
  with _. (
    let lpc = array_index lpcs lidx in
    let hpc = array_index hpcs hidx in
    introduce index_relation lidx hidx ==> pc_relation lpc hpc
    with _. (
      assert (array_nth hpc_to_lpc hidx = Some lidx);
      assert (find_in_array hpcs hpc = Some hidx);
      assert (array_index hpc_to_lpc hidx = lidx);
      assert (make_pc_index_to_pc lpcs lidx = lpc);
      assert (inefficient_hpc_to_lpc hpc = lpc)
    );
    introduce index_return_relation lidx hidx ==> pc_return_relation lpc hpc
    with _. (
      assert (array_nth hpc_to_lpc hidx = Some lidx);
      assert (array_nth is_return_hpc hidx = Some true);
      assert (find_in_array hpcs hpc = Some hidx);
      assert (array_index hpc_to_lpc hidx = lidx);
      assert (make_pc_index_to_pc lpcs lidx = lpc);
      assert (inefficient_hpc_to_lpc hpc = lpc);
      make_return_pcs_contains_return_pc hpcs is_return_hpc hidx;
      assert (list_contains hpc inefficient_return_hpcs)
    )
  )

let program_inits_match_except_global_variables_lemma
  (vs: list var_id_t)
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (hpc_to_lpc: array_t nat{array_len hpc_to_lpc = array_len hpcs})
  (which_initializers_are_intros: list bool)
  (lprog: Armada.Program.t)
  (hprog: Armada.Program.t)
  (lprog_main_start_pc_index: nat)
  (hprog_main_start_pc_index: nat)
  : Lemma (requires   efficient_program_inits_match_except_global_variables vs lpcs hpcs hpc_to_lpc
                        which_initializers_are_intros lprog hprog lprog_main_start_pc_index hprog_main_start_pc_index
                    /\ array_elements_unique hpcs)
          (ensures    program_inits_match_except_global_variables vs (make_hpc_to_lpc hpcs lpcs hpc_to_lpc)
                        which_initializers_are_intros lprog hprog
                    /\ (make_hpc_to_lpc hpcs lpcs hpc_to_lpc) hprog.main_start_pc = lprog.main_start_pc) =
  array_elements_unique_implication hpcs

let hstart_pc_among_hpcs_lemma
  (hpcs: array_t pc_t)
  (hprog: Armada.Program.t)
  (hprog_main_start_pc_index: nat)
  : Lemma (requires  array_nth hpcs hprog_main_start_pc_index = Some hprog.main_start_pc)
          (ensures   list_contains hprog.main_start_pc (array_to_list hpcs)) =
  ()

let pcs_contain_new_pcs_of_action_lemma
  (hatomic_prog: program_t (make_atomic_semantics armada_semantics))
  (hprog_actions_array: array_t (list Armada.Action.t))
  (hpc_indices_array: array_t (list statement_pc_indices_t))
  (hpcs: array_t pc_t)
  : Lemma (requires   hprog_actions_array == list_to_array hatomic_prog.actions
                    /\ actions_array_corresponds_to_statement_pc_indices_array hpcs hprog_actions_array
                        hpc_indices_array)
          (ensures  for_all_ghost (for_all_ghost (pcs_contain_new_pcs_of_action (array_to_list hpcs)))
                      hatomic_prog.actions) =
  let hpc_list = array_to_list hpcs in
  introduce forall actions. contains_ubool actions hatomic_prog.actions ==>
               (forall action. contains_ubool action actions ==> pcs_contain_new_pcs_of_action hpc_list action)
  with introduce contains_ubool actions hatomic_prog.actions ==>
                   (forall action. contains_ubool action actions ==> pcs_contain_new_pcs_of_action hpc_list action)
  with _. introduce forall action. contains_ubool action actions ==> pcs_contain_new_pcs_of_action hpc_list action
  with introduce contains_ubool action actions ==> pcs_contain_new_pcs_of_action hpc_list action
  with _. (
    let actions_idx = contains_ubool_to_index actions hatomic_prog.actions in
    let hactions = array_index hprog_actions_array actions_idx in
    let hpc_indices_list = array_index hpc_indices_array actions_idx in
    assert (action_list_corresponds_to_statement_pc_indices_list hpcs hactions hpc_indices_list);
    let hpc_indices = get_correspondent_from_lists_correspond (action_corresponds_to_statement_pc_indices hpcs)
      hactions hpc_indices_list action in
    assert (action_corresponds_to_statement_pc_indices hpcs action hpc_indices)
  )

#push-options "--z3rlimit 10"

let every_hpc_appears_among_lpc_to_hpcs_lemma
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (hpc_to_lpc: array_t nat{array_len hpc_to_lpc = array_len hpcs})
  (lpc_to_hpcs: array_t (list nat){array_len lpc_to_hpcs = array_len lpcs})
  : Lemma (requires   efficient_hpc_among_hpc_to_lpc_to_hpcs (array_len hpcs) hpc_to_lpc lpc_to_hpcs
                    /\ array_elements_unique lpcs
                    /\ array_elements_unique hpcs)
          (ensures  every_hpc_appears_among_lpc_to_hpcs (make_lpc_to_hpcs hpcs lpcs lpc_to_hpcs)
                      (make_hpc_to_lpc hpcs lpcs hpc_to_lpc) (array_to_list hpcs)) =
  let inefficient_hpcs = array_to_list hpcs in
  let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
  let inefficient_lpc_to_hpcs = make_lpc_to_hpcs hpcs lpcs lpc_to_hpcs in
  introduce forall hpc. list_contains hpc inefficient_hpcs ==>
                     list_contains hpc (inefficient_lpc_to_hpcs (inefficient_hpc_to_lpc hpc))
  with introduce list_contains hpc inefficient_hpcs ==>
                   list_contains hpc (inefficient_lpc_to_hpcs (inefficient_hpc_to_lpc hpc))
  with _. (
    let hpc_index = contains_to_index hpc inefficient_hpcs in
    assert (array_nth hpcs hpc_index = Some hpc);
    let lpc_index = array_index hpc_to_lpc hpc_index in
    let lpc = array_index lpcs lpc_index in
    let hpc_indices = array_index lpc_to_hpcs lpc_index in
    assert (list_contains hpc_index hpc_indices);
    assert (find_in_array hpcs hpc = Some hpc_index);
    assert (inefficient_hpc_to_lpc hpc = lpc);
    let inefficient_hpcs = inefficient_lpc_to_hpcs lpc in
    assert (inefficient_hpcs = make_pc_indices_to_pcs hpcs hpc_indices);
    map_ghost_contains (make_pc_index_to_pc hpcs) hpc_indices hpc_index;
    assert (list_contains (make_pc_index_to_pc hpcs hpc_index) inefficient_hpcs);
    assert (make_pc_index_to_pc hpcs hpc_index = hpc)
  )

#pop-options
/
Util.Relation.fst.checked Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.VarIntro.Relation.fsti.checked Strategies.VarIntro.Inefficient.fsti.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCIndices.fst.checked Strategies.Nonyielding.fst.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.fst.checked Strategies.Breaking.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.VarIntro.Efficient.fst

    hpcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    is_return_hpc:
      Util.ImmutableArray.array_t Prims.bool
        {Util.ImmutableArray.array_len is_return_hpc = Util.ImmutableArray.array_len hpcs} ->
    offset: Prims.nat{offset <= Util.ImmutableArray.array_len hpcs} ->
    pc: Armada.Base.pc_t
  -> Prims.Ghost Prims.nat
Util.ImmutableArray.array_t Armada.Base.pc_t Prims.bool Prims.b2t Prims.op_Equality Prims.nat Util.ImmutableArray.array_len Prims.op_LessThanOrEqual FStar.Pervasives.false_elim Util.ImmutableArray.array_index Strategies.VarIntro.Efficient.get_index_of_pc_among_return_pcs_offset Prims.op_Addition Spec.List.list_contains Strategies.VarIntro.Efficient.make_return_pcs_offset Prims.l_and Prims.op_LessThan
let rec get_index_of_pc_among_return_pcs_offset
      (hpcs: array_t pc_t)
      (is_return_hpc: array_t bool {array_len is_return_hpc = array_len hpcs})
      (offset: nat{offset <= array_len hpcs})
      (pc: pc_t)
    : Ghost nat
      (requires list_contains pc (make_return_pcs_offset hpcs is_return_hpc offset))
      (ensures
        fun idx ->
          idx < array_len hpcs /\ array_index hpcs idx = pc /\ array_index is_return_hpc idx = true)
      (decreases array_len hpcs - offset) =
  
if offset = array_len hpcs
then false_elim ()
else
  if array_index is_return_hpc offset = true
  then
    (if array_index hpcs offset = pc
      then offset
      else get_index_of_pc_among_return_pcs_offset hpcs is_return_hpc (offset + 1) pc)
  else get_index_of_pc_among_return_pcs_offset hpcs is_return_hpc (offset + 1) pc