val efficient_hactions_introducible_implies_hactions_introducible
      (vs: list var_id_t)
      (tds: list object_td_t)
      (inv: invariant_t Armada.State.t)
      (lpcs hpcs: array_t pc_t)
      (hpc_info: array_t (efficient_hpc_info_t vs tds inv) {array_len hpc_info = array_len hpcs})
      (hpc_to_lpc: array_t nat {array_len hpc_to_lpc = array_len hpcs})
      (is_nonyielding_lpc: array_t bool {array_len is_nonyielding_lpc = array_len lpcs})
      (hstart_pc hend_pc: nat)
      (introduction_succeeds_witnesses: list (introduction_succeeds_witness_t vs tds inv))
      (actions: list Armada.Action.t)
      (pc_indices: list statement_pc_indices_t)
    : Lemma
      (requires
        efficient_hactions_introducible vs
          tds
          inv
          hpc_to_lpc
          hstart_pc
          hend_pc
          introduction_succeeds_witnesses
          actions
          pc_indices /\ array_elements_unique lpcs /\ array_elements_unique hpcs /\
        action_list_corresponds_to_statement_pc_indices_list hpcs actions pc_indices)
      (ensures
        (let inefficient_hpc_info = make_hpc_info vs tds inv hpcs hpc_info in
          let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
          let inefficient_is_nonyielding_lpc = make_is_nonyielding_pc lpcs is_nonyielding_lpc in
          let inefficient_hpcs = array_to_list hpcs in
          hactions_introducible vs
            tds
            inv
            inefficient_hpc_to_lpc
            (make_pc_index_to_pc hpcs hstart_pc)
            (make_pc_index_to_pc hpcs hend_pc)
            introduction_succeeds_witnesses
            actions))
      (decreases introduction_succeeds_witnesses)
val efficient_hactions_introducible_implies_hactions_introducible
      (vs: list var_id_t)
      (tds: list object_td_t)
      (inv: invariant_t Armada.State.t)
      (lpcs hpcs: array_t pc_t)
      (hpc_info: array_t (efficient_hpc_info_t vs tds inv) {array_len hpc_info = array_len hpcs})
      (hpc_to_lpc: array_t nat {array_len hpc_to_lpc = array_len hpcs})
      (is_nonyielding_lpc: array_t bool {array_len is_nonyielding_lpc = array_len lpcs})
      (hstart_pc hend_pc: nat)
      (introduction_succeeds_witnesses: list (introduction_succeeds_witness_t vs tds inv))
      (actions: list Armada.Action.t)
      (pc_indices: list statement_pc_indices_t)
    : Lemma
      (requires
        efficient_hactions_introducible vs
          tds
          inv
          hpc_to_lpc
          hstart_pc
          hend_pc
          introduction_succeeds_witnesses
          actions
          pc_indices /\ array_elements_unique lpcs /\ array_elements_unique hpcs /\
        action_list_corresponds_to_statement_pc_indices_list hpcs actions pc_indices)
      (ensures
        (let inefficient_hpc_info = make_hpc_info vs tds inv hpcs hpc_info in
          let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
          let inefficient_is_nonyielding_lpc = make_is_nonyielding_pc lpcs is_nonyielding_lpc in
          let inefficient_hpcs = array_to_list hpcs in
          hactions_introducible vs
            tds
            inv
            inefficient_hpc_to_lpc
            (make_pc_index_to_pc hpcs hstart_pc)
            (make_pc_index_to_pc hpcs hend_pc)
            introduction_succeeds_witnesses
            actions))
      (decreases introduction_succeeds_witnesses)
let rec efficient_hactions_introducible_implies_hactions_introducible
  (vs: list var_id_t)
  (tds: list object_td_t)
  (inv: invariant_t Armada.State.t)
  (lpcs: array_t pc_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_to_lpc: array_t nat{array_len hpc_to_lpc = array_len hpcs})
  (is_nonyielding_lpc: array_t bool{array_len is_nonyielding_lpc = array_len lpcs})
  (hstart_pc: nat)
  (hend_pc: nat)
  (introduction_succeeds_witnesses: list (introduction_succeeds_witness_t vs tds inv))
  (actions: list Armada.Action.t)
  (pc_indices: list statement_pc_indices_t)
  : Lemma (requires   efficient_hactions_introducible vs tds inv hpc_to_lpc hstart_pc hend_pc
                        introduction_succeeds_witnesses actions pc_indices
                    /\ array_elements_unique lpcs
                    /\ array_elements_unique hpcs
                    /\ action_list_corresponds_to_statement_pc_indices_list hpcs actions pc_indices)
          (ensures  (let inefficient_hpc_info = make_hpc_info vs tds inv hpcs hpc_info in
                     let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
                     let inefficient_is_nonyielding_lpc = make_is_nonyielding_pc lpcs is_nonyielding_lpc in
                     let inefficient_hpcs = array_to_list hpcs in
                     hactions_introducible vs tds inv inefficient_hpc_to_lpc (make_pc_index_to_pc hpcs hstart_pc)
                       (make_pc_index_to_pc hpcs hend_pc) introduction_succeeds_witnesses actions))
          (decreases introduction_succeeds_witnesses) =
  match introduction_succeeds_witnesses, actions, pc_indices with
  | [], [], [] -> ()
  | first_witness :: remaining_introduction_succeeds_witnesses, first_action :: remaining_actions,
      first_pc_indices :: remaining_pc_indices ->
      assert (find_in_array hpcs (make_pc_index_to_pc hpcs hend_pc) = Some hend_pc);
      assert (find_in_array hpcs (make_pc_index_to_pc hpcs hstart_pc) = Some hstart_pc);
      efficient_hactions_introducible_implies_hactions_introducible vs tds inv lpcs hpcs hpc_info hpc_to_lpc
        is_nonyielding_lpc
        (EfficientThreadStateAtPC?.pc (efficient_action_to_ending_thread_state first_action first_pc_indices))
        hend_pc remaining_introduction_succeeds_witnesses remaining_actions remaining_pc_indices
  | _, _, _ -> ()
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

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

let get_index_of_pc_among_return_pcs
  (hpcs: array_t pc_t)
  (is_return_hpc: array_t bool{array_len is_return_hpc = array_len hpcs})
  (pc: pc_t)
  : Ghost nat
  (requires list_contains pc (make_return_pcs hpcs is_return_hpc))
  (ensures  fun idx -> idx < array_len hpcs /\ array_index hpcs idx = pc /\ array_index is_return_hpc idx = true) =
  get_index_of_pc_among_return_pcs_offset hpcs is_return_hpc 0 pc

let apply_efficient_return_hpcs_unique
  (num_hpcs: nat)
  (hpc_to_lpc: array_t nat)
  (is_return_hpc: array_t bool)
  (hpc1: nat)
  (hpc2: nat)
  : Lemma (requires   efficient_return_hpcs_unique num_hpcs hpc_to_lpc is_return_hpc
                    /\ hpc1 < num_hpcs
                    /\ hpc2 < num_hpcs
                    /\ array_nth is_return_hpc hpc1 = Some true
                    /\ array_nth is_return_hpc hpc2 = Some true
                    /\ array_nth hpc_to_lpc hpc1 = array_nth hpc_to_lpc hpc2)
          (ensures  hpc1 = hpc2) =
  assert (efficient_return_hpcs_unique_inner1 num_hpcs hpc_to_lpc is_return_hpc hpc1);
  assert (efficient_return_hpcs_unique_inner2 hpc_to_lpc is_return_hpc hpc1 hpc2)

#push-options "--z3rlimit 10"

let return_pcs_unique_lemma
  (hpcs: array_t pc_t)
  (lpcs: 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})
  (lpc_to_hpcs: array_t (list nat){array_len lpc_to_hpcs = array_len lpcs})
  : Lemma (requires    efficient_return_hpcs_unique (array_len hpcs) hpc_to_lpc is_return_hpc
                    /\ 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  return_pcs_unique (make_hpc_to_lpc hpcs lpcs hpc_to_lpc) (make_return_pcs hpcs is_return_hpc)) =
  let inefficient_return_hpcs = make_return_pcs hpcs is_return_hpc in
  let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
  introduce forall hpc1. list_contains hpc1 inefficient_return_hpcs ==>
              return_pcs_unique_inner1 inefficient_hpc_to_lpc inefficient_return_hpcs hpc1
  with introduce list_contains hpc1 inefficient_return_hpcs ==>
                   return_pcs_unique_inner1 inefficient_hpc_to_lpc inefficient_return_hpcs hpc1
  with _. introduce forall hpc2. list_contains hpc2 inefficient_return_hpcs ==>
                      return_pcs_unique_inner2 inefficient_hpc_to_lpc inefficient_return_hpcs hpc1 hpc2
  with introduce list_contains hpc2 inefficient_return_hpcs ==>
                   return_pcs_unique_inner2 inefficient_hpc_to_lpc inefficient_return_hpcs hpc1 hpc2
  with _. introduce inefficient_hpc_to_lpc hpc1 = inefficient_hpc_to_lpc hpc2 ==> hpc1 = hpc2
  with _. (
    let hpc_index1 = get_index_of_pc_among_return_pcs hpcs is_return_hpc hpc1 in
    let hpc_index2 = get_index_of_pc_among_return_pcs hpcs is_return_hpc hpc2 in
    assert (hpc_index1 < array_len hpcs);
    assert (Some? (array_nth hpc_to_lpc hpc_index1));
    assert (array_nth is_return_hpc hpc_index1 = Some true);
    assert (hpc_index2 < array_len hpcs);
    assert (Some? (array_nth hpc_to_lpc hpc_index2));
    assert (array_nth is_return_hpc hpc_index2 = Some true);
    array_elements_unique_implication hpcs;
    assert (find_in_array hpcs hpc1 = Some hpc_index1);
    assert (find_in_array hpcs hpc2 = Some hpc_index2);
    let lpc_index1 = array_index hpc_to_lpc hpc_index1 in
    let lpc_index2 = array_index hpc_to_lpc hpc_index2 in
    assert (inefficient_hpc_to_lpc hpc1 = make_pc_index_to_pc lpcs lpc_index1);
    assert (inefficient_hpc_to_lpc hpc2 = make_pc_index_to_pc lpcs lpc_index2);
    assert (make_pc_index_to_pc lpcs lpc_index1 = make_pc_index_to_pc lpcs lpc_index2);
    array_elements_unique_implication lpcs;
    assert (lpc_index1 < array_len lpcs);
    assert (lpc_index2 < array_len lpcs);
    assert (lpc_index1 = lpc_index2);
    assert (array_nth hpc_to_lpc hpc_index1 = array_nth hpc_to_lpc hpc_index2);
    apply_efficient_return_hpcs_unique (array_len hpcs) hpc_to_lpc is_return_hpc hpc_index1 hpc_index2
  )

let each_action_list_consistent_with_is_nonyielding_pc_helper
  (pcs: array_t pc_t)
  (is_nonyielding_pc: array_t bool{array_len is_nonyielding_pc = array_len pcs})
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : Lemma (requires   efficient_action_consistent_with_is_nonyielding_pc is_nonyielding_pc action pc_indices
                    /\ action_corresponds_to_statement_pc_indices pcs action pc_indices
                    /\ array_elements_unique pcs)
          (ensures  action_consistent_with_is_nonyielding_pc (make_is_nonyielding_pc pcs is_nonyielding_pc) action) =
  ()

#pop-options

let each_action_list_consistent_with_is_nonyielding_pc_lemma
  (pcs: array_t pc_t)
  (is_nonyielding_pc: array_t bool{array_len is_nonyielding_pc = array_len pcs})
  (actions_list: list (list Armada.Action.t))
  (pc_indices_array: array_t (list statement_pc_indices_t))
  : Lemma (requires   efficient_each_action_list_consistent_with_is_nonyielding_pc is_nonyielding_pc
                        (list_to_array actions_list) pc_indices_array
                    /\ actions_array_corresponds_to_statement_pc_indices_array pcs (list_to_array actions_list)
                        pc_indices_array
                    /\ array_elements_unique pcs)
          (ensures each_action_list_consistent_with_is_nonyielding_pc (make_is_nonyielding_pc pcs is_nonyielding_pc)
                     actions_list) =
  let inefficient_is_nonyielding_pc = make_is_nonyielding_pc pcs is_nonyielding_pc in
  introduce forall actions. contains_ubool actions actions_list ==>
               each_action_consistent_with_is_nonyielding_pc inefficient_is_nonyielding_pc actions
  with introduce contains_ubool actions actions_list ==>
                   each_action_consistent_with_is_nonyielding_pc inefficient_is_nonyielding_pc actions
  with _. introduce forall action. contains_ubool action actions ==>
                      action_consistent_with_is_nonyielding_pc inefficient_is_nonyielding_pc action
  with introduce contains_ubool action actions ==>
                   action_consistent_with_is_nonyielding_pc inefficient_is_nonyielding_pc action
  with _. (
    let idx = contains_ubool_to_index actions actions_list in
    let pc_indices_list = array_index pc_indices_array idx in
    arrays_correspond_specific_index (action_list_corresponds_to_statement_pc_indices_list pcs)
      (list_to_array actions_list) pc_indices_array idx;
    assert (action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list);
    assert (efficient_each_action_consistent_with_is_nonyielding_pc is_nonyielding_pc actions pc_indices_list);
    let pc_indices = get_correspondent_from_lists_correspond_doubly
      (fun action pc_indices -> efficient_action_consistent_with_is_nonyielding_pc is_nonyielding_pc action pc_indices)
      (action_corresponds_to_statement_pc_indices pcs)
      actions pc_indices_list action in
    assert (efficient_action_consistent_with_is_nonyielding_pc is_nonyielding_pc action pc_indices);
    assert (action_corresponds_to_statement_pc_indices pcs action pc_indices);
    each_action_list_consistent_with_is_nonyielding_pc_helper pcs is_nonyielding_pc action pc_indices;
    assert (action_consistent_with_is_nonyielding_pc inefficient_is_nonyielding_pc action)
  )

let efficient_action_breaks_implies_action_breaks
  (pcs: array_t pc_t)
  (is_breaking_pc: array_t bool{array_len is_breaking_pc = array_len pcs})
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : Lemma (requires   efficient_action_breaks is_breaking_pc action pc_indices
                    /\ action_corresponds_to_statement_pc_indices pcs action pc_indices
                    /\ array_elements_unique pcs)
          (ensures  action_breaks (make_is_breaking_pc pcs is_breaking_pc) action) =
  ()

let efficient_action_only_creates_breaking_threads_implies_action_only_creates_breaking_threads
  (pcs: array_t pc_t)
  (is_breaking_pc: array_t bool{array_len is_breaking_pc = array_len pcs})
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : Lemma (requires   efficient_action_only_creates_breaking_threads is_breaking_pc pc_indices
                    /\ action_corresponds_to_statement_pc_indices pcs action pc_indices
                    /\ array_elements_unique pcs)
          (ensures  action_only_creates_breaking_threads (make_is_breaking_pc pcs is_breaking_pc) action) =
  ()

let rec efficient_actions_end_with_all_threads_breaking_implies_actions_end_with_all_threads_breaking
  (pcs: array_t pc_t)
  (is_breaking_pc: array_t bool{array_len is_breaking_pc = array_len pcs})
  (actions: list Armada.Action.t)
  (pc_indices_list: list statement_pc_indices_t)
  : Lemma (requires   efficient_actions_end_with_all_threads_breaking is_breaking_pc actions pc_indices_list
                    /\ action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list
                    /\ array_elements_unique pcs)
          (ensures  actions_end_with_all_threads_breaking (make_is_breaking_pc pcs is_breaking_pc) actions) =
  match actions, pc_indices_list with
  | [], [] -> false_elim ()
  | [last_action], [last_pc_indices] ->
      efficient_action_only_creates_breaking_threads_implies_action_only_creates_breaking_threads
        pcs is_breaking_pc last_action last_pc_indices;
      efficient_action_breaks_implies_action_breaks pcs is_breaking_pc last_action last_pc_indices
  | first_action :: remaining_actions, first_pc_indices :: remaining_pc_indices ->
      efficient_action_only_creates_breaking_threads_implies_action_only_creates_breaking_threads
        pcs is_breaking_pc first_action first_pc_indices;
      efficient_actions_end_with_all_threads_breaking_implies_actions_end_with_all_threads_breaking
        pcs is_breaking_pc remaining_actions remaining_pc_indices
  | _, _ -> false_elim ()

let efficient_actions_maintain_all_threads_breaking_implies_actions_maintain_all_threads_breaking
  (pcs: array_t pc_t)
  (is_breaking_pc: array_t bool{array_len is_breaking_pc = array_len pcs})
  (actions: list Armada.Action.t)
  (pc_indices_list: list statement_pc_indices_t)
  : Lemma (requires   efficient_actions_maintain_all_threads_breaking is_breaking_pc actions pc_indices_list
                    /\ action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list
                    /\ array_elements_unique pcs)
          (ensures  actions_maintain_all_threads_breaking (make_is_breaking_pc pcs is_breaking_pc) actions) =
  if efficient_actions_end_with_all_threads_breaking is_breaking_pc actions pc_indices_list then
    efficient_actions_end_with_all_threads_breaking_implies_actions_end_with_all_threads_breaking
      pcs is_breaking_pc actions pc_indices_list
  else
    ()

let each_action_list_maintains_all_threads_breaking_lemma
  (pcs: array_t pc_t)
  (is_breaking_pc: array_t bool{array_len is_breaking_pc = array_len pcs})
  (actions_list: list (list Armada.Action.t))
  (pc_indices_array: array_t (list statement_pc_indices_t))
  : Lemma (requires   efficient_each_action_list_maintains_all_threads_breaking is_breaking_pc
                        (list_to_array actions_list) pc_indices_array
                    /\ actions_array_corresponds_to_statement_pc_indices_array pcs (list_to_array actions_list)
                        pc_indices_array
                    /\ array_elements_unique pcs)
          (ensures each_action_list_maintains_all_threads_breaking (make_is_breaking_pc pcs is_breaking_pc)
                     actions_list) =
  let inefficient_is_breaking_pc = make_is_breaking_pc pcs is_breaking_pc in
  introduce forall actions. contains_ubool actions actions_list ==>
               actions_maintain_all_threads_breaking inefficient_is_breaking_pc actions
  with introduce contains_ubool actions actions_list ==>
                   actions_maintain_all_threads_breaking inefficient_is_breaking_pc actions
  with _. (
    let idx = contains_ubool_to_index actions actions_list in
    let pc_indices_list = array_index pc_indices_array idx in
    arrays_correspond_specific_index (action_list_corresponds_to_statement_pc_indices_list pcs)
      (list_to_array actions_list) pc_indices_array idx;
    assert (action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list);
    assert (efficient_actions_maintain_all_threads_breaking is_breaking_pc actions pc_indices_list);
    efficient_actions_maintain_all_threads_breaking_implies_actions_maintain_all_threads_breaking
      pcs is_breaking_pc actions pc_indices_list
  )
/
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

    vs: Prims.list Armada.Base.var_id_t ->
    tds: Prims.list Armada.Type.object_td_t ->
    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    lpcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    hpcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    hpc_info:
      Util.ImmutableArray.array_t (Strategies.VarIntro.Efficient.efficient_hpc_info_t vs tds inv)
        {Util.ImmutableArray.array_len hpc_info = Util.ImmutableArray.array_len hpcs} ->
    hpc_to_lpc:
      Util.ImmutableArray.array_t Prims.nat
        {Util.ImmutableArray.array_len hpc_to_lpc = Util.ImmutableArray.array_len hpcs} ->
    is_nonyielding_lpc:
      Util.ImmutableArray.array_t Prims.bool
        {Util.ImmutableArray.array_len is_nonyielding_lpc = Util.ImmutableArray.array_len lpcs} ->
    hstart_pc: Prims.nat ->
    hend_pc: Prims.nat ->
    introduction_succeeds_witnesses:
      Prims.list (Strategies.VarIntro.Defs.introduction_succeeds_witness_t vs tds inv) ->
    actions: Prims.list Armada.Action.t ->
    pc_indices: Prims.list Strategies.PCIndices.statement_pc_indices_t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarIntro.Efficient.efficient_hactions_introducible vs
          tds
          inv
          hpc_to_lpc
          hstart_pc
          hend_pc
          introduction_succeeds_witnesses
          actions
          pc_indices /\ Util.ImmutableArray.array_elements_unique lpcs /\
        Util.ImmutableArray.array_elements_unique hpcs /\
        Strategies.PCIndices.action_list_corresponds_to_statement_pc_indices_list hpcs
          actions
          pc_indices)
      (ensures
        (let inefficient_hpc_info =
            Strategies.VarIntro.Efficient.make_hpc_info vs tds inv hpcs hpc_info
          in
          let inefficient_hpc_to_lpc =
            Strategies.VarIntro.Efficient.make_hpc_to_lpc hpcs lpcs hpc_to_lpc
          in
          let inefficient_is_nonyielding_lpc =
            Strategies.VarIntro.Efficient.make_is_nonyielding_pc lpcs is_nonyielding_lpc
          in
          let inefficient_hpcs = Util.ImmutableArray.array_to_list hpcs in
          Strategies.VarIntro.Defs.hactions_introducible vs
            tds
            inv
            inefficient_hpc_to_lpc
            (Strategies.VarIntro.Efficient.make_pc_index_to_pc hpcs hstart_pc)
            (Strategies.VarIntro.Efficient.make_pc_index_to_pc hpcs hend_pc)
            introduction_succeeds_witnesses
            actions))
      (decreases introduction_succeeds_witnesses)
Prims.list Armada.Base.var_id_t Armada.Type.object_td_t Strategies.Invariant.invariant_t Armada.State.t Util.ImmutableArray.array_t Armada.Base.pc_t Strategies.VarIntro.Efficient.efficient_hpc_info_t Prims.b2t Prims.op_Equality Prims.nat Util.ImmutableArray.array_len Prims.bool Strategies.VarIntro.Defs.introduction_succeeds_witness_t Armada.Action.t Strategies.PCIndices.statement_pc_indices_t FStar.Pervasives.Native.Mktuple3 Strategies.VarIntro.Efficient.efficient_hactions_introducible_implies_hactions_introducible Strategies.ArmadaStatement.ThreadState.__proj__EfficientThreadStateAtPC__item__pc Strategies.ArmadaStatement.ThreadState.efficient_action_to_ending_thread_state Prims.unit Prims._assert FStar.Pervasives.Native.option Util.ImmutableArray.find_in_array Strategies.VarIntro.Efficient.make_pc_index_to_pc FStar.Pervasives.Native.Some Prims.l_and Strategies.VarIntro.Efficient.efficient_hactions_introducible Util.ImmutableArray.array_elements_unique Strategies.PCIndices.action_list_corresponds_to_statement_pc_indices_list Prims.squash Strategies.VarIntro.Defs.hactions_introducible Util.ImmutableArray.array_to_list Strategies.VarIntro.Efficient.make_is_nonyielding_pc Strategies.VarIntro.Efficient.make_hpc_to_lpc Strategies.VarIntro.Defs.hpc_info_t Strategies.VarIntro.Efficient.make_hpc_info Prims.Nil FStar.Pervasives.pattern
let rec efficient_hactions_introducible_implies_hactions_introducible
      (vs: list var_id_t)
      (tds: list object_td_t)
      (inv: invariant_t Armada.State.t)
      (lpcs hpcs: array_t pc_t)
      (hpc_info: array_t (efficient_hpc_info_t vs tds inv) {array_len hpc_info = array_len hpcs})
      (hpc_to_lpc: array_t nat {array_len hpc_to_lpc = array_len hpcs})
      (is_nonyielding_lpc: array_t bool {array_len is_nonyielding_lpc = array_len lpcs})
      (hstart_pc hend_pc: nat)
      (introduction_succeeds_witnesses: list (introduction_succeeds_witness_t vs tds inv))
      (actions: list Armada.Action.t)
      (pc_indices: list statement_pc_indices_t)
    : Lemma
      (requires
        efficient_hactions_introducible vs
          tds
          inv
          hpc_to_lpc
          hstart_pc
          hend_pc
          introduction_succeeds_witnesses
          actions
          pc_indices /\ array_elements_unique lpcs /\ array_elements_unique hpcs /\
        action_list_corresponds_to_statement_pc_indices_list hpcs actions pc_indices)
      (ensures
        (let inefficient_hpc_info = make_hpc_info vs tds inv hpcs hpc_info in
          let inefficient_hpc_to_lpc = make_hpc_to_lpc hpcs lpcs hpc_to_lpc in
          let inefficient_is_nonyielding_lpc = make_is_nonyielding_pc lpcs is_nonyielding_lpc in
          let inefficient_hpcs = array_to_list hpcs in
          hactions_introducible vs
            tds
            inv
            inefficient_hpc_to_lpc
            (make_pc_index_to_pc hpcs hstart_pc)
            (make_pc_index_to_pc hpcs hend_pc)
            introduction_succeeds_witnesses
            actions))
      (decreases introduction_succeeds_witnesses) =
  
match introduction_succeeds_witnesses, actions, pc_indices with
| [], [], [] -> ()
| first_witness :: remaining_introduction_succeeds_witnesses,
first_action :: remaining_actions,
first_pc_indices :: remaining_pc_indices ->
  assert (find_in_array hpcs (make_pc_index_to_pc hpcs hend_pc) = Some hend_pc);
  assert (find_in_array hpcs (make_pc_index_to_pc hpcs hstart_pc) = Some hstart_pc);
  efficient_hactions_introducible_implies_hactions_introducible vs tds inv lpcs hpcs hpc_info
    hpc_to_lpc is_nonyielding_lpc
    (EfficientThreadStateAtPC?.pc (efficient_action_to_ending_thread_state first_action
            first_pc_indices)) hend_pc remaining_introduction_succeeds_witnesses remaining_actions
    remaining_pc_indices
| _, _, _ -> ()