val efficient_actions_to_ending_thread_state_matches
      (pcs: array_t pc_t)
      (actions: list Armada.Action.t)
      (pc_indices_list: list statement_pc_indices_t)
    : Lemma
      (requires action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
      (ensures
        actions_to_ending_thread_state actions =
        convert_efficient_thread_state pcs
          (efficient_actions_to_ending_thread_state actions pc_indices_list))
      (decreases actions)
      [
        SMTPat (actions_to_ending_thread_state actions);
        SMTPat (action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
      ]
val efficient_actions_to_ending_thread_state_matches
      (pcs: array_t pc_t)
      (actions: list Armada.Action.t)
      (pc_indices_list: list statement_pc_indices_t)
    : Lemma
      (requires action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
      (ensures
        actions_to_ending_thread_state actions =
        convert_efficient_thread_state pcs
          (efficient_actions_to_ending_thread_state actions pc_indices_list))
      (decreases actions)
      [
        SMTPat (actions_to_ending_thread_state actions);
        SMTPat (action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
      ]
let rec efficient_actions_to_ending_thread_state_matches
  (pcs: array_t pc_t)
  (actions: list Armada.Action.t)
  (pc_indices_list: list statement_pc_indices_t)
  : Lemma (requires action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
          (ensures  actions_to_ending_thread_state actions = convert_efficient_thread_state pcs
                      (efficient_actions_to_ending_thread_state actions pc_indices_list))
          (decreases actions)
          [SMTPat  (actions_to_ending_thread_state actions);
           SMTPat  (action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)] =
  match actions, pc_indices_list with
  | [], _ -> ()
  | [action], [pc_indices] -> ()
  | first_action :: remaining_actions, first_pc_indices :: remaining_pc_indices ->
      efficient_actions_to_ending_thread_state_matches pcs remaining_actions remaining_pc_indices
  | _, _ -> false_elim ()
module Strategies.VarHiding.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.VarHiding
open Strategies.GlobalVars.VarIntro
open Strategies.Invariant
open Strategies.Nonyielding
open Strategies.PCIndices
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarHiding.Defs
open Strategies.VarHiding.Inefficient
open Strategies.VarHiding.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_lpc_to_hpc
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (lpc_to_hpc: array_t nat{array_len lpc_to_hpc = array_len lpcs})
  (lpc: pc_t)
  : GTot pc_t =
  match find_in_array lpcs lpc with
  | None -> default_pc
  | Some lpc_index ->
      let hpc_index = array_index lpc_to_hpc lpc_index in
      make_pc_index_to_pc hpcs hpc_index

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 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)
  (lpc_to_hpc: array_t nat{array_len lpc_to_hpc = array_len lpcs})
  (is_return_lpc: array_t bool{array_len is_return_lpc = array_len lpcs})
  : Lemma (requires array_elements_unique lpcs)
          (ensures  (let index_relation = efficient_lh_pc_relation lpc_to_hpc in
                     let index_return_relation = efficient_lh_pc_return_relation lpc_to_hpc is_return_lpc in
                     let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
                     let inefficient_return_lpcs = make_return_pcs lpcs is_return_lpc in
                     let pc_relation = lpc_hpc_pc_relation inefficient_lpc_to_hpc in
                     let pc_return_relation = lpc_hpc_pc_return_relation inefficient_lpc_to_hpc
                                                inefficient_return_lpcs 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_lh_pc_relation lpc_to_hpc in
  let index_return_relation = efficient_lh_pc_return_relation lpc_to_hpc is_return_lpc in
  let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
  let inefficient_return_lpcs = make_return_pcs lpcs is_return_lpc in
  let pc_relation = lpc_hpc_pc_relation inefficient_lpc_to_hpc in
  let pc_return_relation = lpc_hpc_pc_return_relation inefficient_lpc_to_hpc inefficient_return_lpcs in
  let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
  let inefficient_return_lpcs = make_return_pcs lpcs is_return_lpc 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 lpc_to_hpc lidx = Some hidx);
      assert (find_in_array lpcs lpc = Some lidx);
      assert (array_index lpc_to_hpc lidx = hidx);
      assert (make_pc_index_to_pc hpcs hidx = hpc);
      assert (inefficient_lpc_to_hpc lpc = hpc)
    );
    introduce index_return_relation lidx hidx ==> pc_return_relation lpc hpc
    with _. (
      assert (array_nth lpc_to_hpc lidx = Some hidx);
      assert (array_nth is_return_lpc lidx = Some true);
      assert (find_in_array lpcs lpc = Some lidx);
      assert (array_index lpc_to_hpc lidx = hidx);
      assert (make_pc_index_to_pc hpcs hidx = hpc);
      assert (inefficient_lpc_to_hpc lpc = hpc);
      make_return_pcs_contains_return_pc lpcs is_return_lpc lidx;
      assert (list_contains lpc inefficient_return_lpcs)
    )
  )

let program_inits_match_except_global_variables_lemma
  (vs: list var_id_t)
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (lpc_to_hpc: array_t nat{array_len lpc_to_hpc = array_len lpcs})
  (which_initializers_are_hidings: 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 lpc_to_hpc
                        which_initializers_are_hidings lprog hprog lprog_main_start_pc_index hprog_main_start_pc_index
                    /\ array_elements_unique lpcs)
          (ensures    program_inits_match_except_global_variables vs (make_lpc_to_hpc lpcs hpcs lpc_to_hpc)
                        which_initializers_are_hidings lprog hprog
                    /\ (make_lpc_to_hpc lpcs hpcs lpc_to_hpc) lprog.main_start_pc = hprog.main_start_pc) =
  array_elements_unique_implication lpcs

let rec get_index_of_pc_among_return_pcs_offset
  (lpcs: array_t pc_t)
  (is_return_lpc: array_t bool{array_len is_return_lpc = array_len lpcs})
  (offset: nat{offset <= array_len lpcs})
  (pc: pc_t)
  : Ghost nat
  (requires list_contains pc (make_return_pcs_offset lpcs is_return_lpc offset))
  (ensures fun idx -> idx < array_len lpcs /\ array_index lpcs idx = pc /\ array_index is_return_lpc idx = true)
  (decreases array_len lpcs - offset) =
  if offset = array_len lpcs then
    false_elim ()
  else if array_index is_return_lpc offset = true then (
    if array_index lpcs offset = pc then
      offset
    else
      get_index_of_pc_among_return_pcs_offset lpcs is_return_lpc (offset + 1) pc
  )
  else
    get_index_of_pc_among_return_pcs_offset lpcs is_return_lpc (offset + 1) pc

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

let apply_efficient_return_lpcs_unique
  (num_lpcs: nat)
  (lpc_to_lpc: array_t nat)
  (is_return_lpc: array_t bool)
  (lpc1: nat)
  (lpc2: nat)
  : Lemma (requires   efficient_return_lpcs_unique num_lpcs lpc_to_lpc is_return_lpc
                    /\ lpc1 < num_lpcs
                    /\ lpc2 < num_lpcs
                    /\ array_nth is_return_lpc lpc1 = Some true
                    /\ array_nth is_return_lpc lpc2 = Some true
                    /\ array_nth lpc_to_lpc lpc1 = array_nth lpc_to_lpc lpc2)
          (ensures  lpc1 = lpc2) =
  assert (efficient_return_lpcs_unique_inner1 num_lpcs lpc_to_lpc is_return_lpc lpc1);
  assert (efficient_return_lpcs_unique_inner2 lpc_to_lpc is_return_lpc lpc1 lpc2)

#push-options "--z3rlimit 10"

let return_pcs_unique_lemma
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (lpc_to_hpc: array_t nat{array_len lpc_to_hpc = array_len lpcs})
  (is_return_lpc: array_t bool{array_len is_return_lpc = array_len lpcs})
  : Lemma (requires   efficient_return_lpcs_unique (array_len lpcs) lpc_to_hpc is_return_lpc
                    /\ efficient_lpc_to_hpc_contains_valid_indices (array_len hpcs) lpc_to_hpc
                    /\ array_elements_unique lpcs
                    /\ array_elements_unique hpcs)
          (ensures  return_pcs_unique (make_lpc_to_hpc lpcs hpcs lpc_to_hpc) (make_return_pcs lpcs is_return_lpc)) =
  let inefficient_return_lpcs = make_return_pcs lpcs is_return_lpc in
  let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
  introduce forall lpc1. list_contains lpc1 inefficient_return_lpcs ==>
              return_pcs_unique_inner1 inefficient_lpc_to_hpc inefficient_return_lpcs lpc1
  with introduce list_contains lpc1 inefficient_return_lpcs ==>
                   return_pcs_unique_inner1 inefficient_lpc_to_hpc inefficient_return_lpcs lpc1
  with _. introduce forall lpc2. list_contains lpc2 inefficient_return_lpcs ==>
                      return_pcs_unique_inner2 inefficient_lpc_to_hpc inefficient_return_lpcs lpc1 lpc2
  with introduce list_contains lpc2 inefficient_return_lpcs ==>
                   return_pcs_unique_inner2 inefficient_lpc_to_hpc inefficient_return_lpcs lpc1 lpc2
  with _. introduce inefficient_lpc_to_hpc lpc1 = inefficient_lpc_to_hpc lpc2 ==> lpc1 = lpc2
  with _. (
    let lpc_index1 = get_index_of_pc_among_return_pcs lpcs is_return_lpc lpc1 in
    let lpc_index2 = get_index_of_pc_among_return_pcs lpcs is_return_lpc lpc2 in
    assert (lpc_index1 < array_len lpcs);
    assert (Some? (array_nth lpc_to_hpc lpc_index1));
    assert (array_nth is_return_lpc lpc_index1 = Some true);
    assert (lpc_index2 < array_len lpcs);
    assert (Some? (array_nth lpc_to_hpc lpc_index2));
    assert (array_nth is_return_lpc lpc_index2 = Some true);
    array_elements_unique_implication lpcs;
    assert (find_in_array lpcs lpc1 = Some lpc_index1);
    assert (find_in_array lpcs lpc2 = Some lpc_index2);
    let hpc_index1 = array_index lpc_to_hpc lpc_index1 in
    let hpc_index2 = array_index lpc_to_hpc lpc_index2 in
    assert (inefficient_lpc_to_hpc lpc1 = make_pc_index_to_pc hpcs hpc_index1);
    assert (inefficient_lpc_to_hpc lpc2 = make_pc_index_to_pc hpcs hpc_index2);
    assert (make_pc_index_to_pc hpcs hpc_index1 = make_pc_index_to_pc hpcs hpc_index2);
    array_elements_unique_implication hpcs;
    assert (hpc_index1 < array_len hpcs);
    assert (hpc_index2 < array_len hpcs);
    assert (hpc_index1 = hpc_index2);
    assert (array_nth lpc_to_hpc lpc_index1 = array_nth lpc_to_hpc lpc_index2);
    apply_efficient_return_lpcs_unique (array_len lpcs) lpc_to_hpc is_return_lpc lpc_index1 lpc_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_laction_corresponds_to_haction_preservation
  (vs: list var_id_t)
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (lpc_to_hpc: array_t nat{array_len lpc_to_hpc = array_len lpcs})
  (is_return_lpc: array_t bool{array_len is_return_lpc = array_len lpcs})
  (laction: Armada.Action.t)
  (haction: Armada.Action.t)
  (lpc_indices: statement_pc_indices_t)
  (hpc_indices: statement_pc_indices_t)
  : Lemma (requires (let pc_relation = efficient_lh_pc_relation lpc_to_hpc in
                     let pc_return_relation = efficient_lh_pc_return_relation lpc_to_hpc is_return_lpc in
                       efficient_laction_corresponds_to_haction vs pc_relation pc_return_relation laction haction
                         lpc_indices hpc_indices
                     /\ action_corresponds_to_statement_pc_indices lpcs laction lpc_indices
                     /\ action_corresponds_to_statement_pc_indices hpcs haction hpc_indices
                     /\ array_elements_unique lpcs))
          (ensures  (let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
                     let inefficient_return_lpcs = make_return_pcs lpcs is_return_lpc in
                     laction_corresponds_to_haction vs inefficient_lpc_to_hpc inefficient_return_lpcs laction
                       haction)) =
  let pc_relation = efficient_lh_pc_relation lpc_to_hpc in
  let pc_return_relation = efficient_lh_pc_return_relation lpc_to_hpc is_return_lpc in
  let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
  let inefficient_return_lpcs = make_return_pcs lpcs is_return_lpc in
  let lps, hps = laction.program_statement, haction.program_statement in
  let relation = lpc_hpc_pc_relation inefficient_lpc_to_hpc in
  let return_relation = lpc_hpc_pc_return_relation inefficient_lpc_to_hpc inefficient_return_lpcs in
  assert (efficient_program_statements_match_per_pc_relation pc_relation pc_return_relation lps hps lpc_indices
            hpc_indices);
  lpc_hpc_relation_facts lpcs hpcs lpc_to_hpc is_return_lpc;
  efficient_program_statements_match_per_pc_relation_implies_program_statements_match_per_pc_relation lpcs hpcs
    pc_relation pc_return_relation relation return_relation lps hps lpc_indices hpc_indices;
  assert (program_statements_match_per_pc_relation relation return_relation lps hps)

let efficient_thread_states_match_per_pc_relation_implies_thread_states_match_per_pc_relation
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (lpc_to_hpc: array_t nat{array_len lpc_to_hpc = array_len lpcs})
  (lts: efficient_thread_state_t)
  (hts: efficient_thread_state_t)
  : Lemma (requires (let index_relation = efficient_lh_pc_relation lpc_to_hpc in
                       efficient_thread_states_match_per_pc_relation index_relation lts hts
                     /\ array_elements_unique lpcs))
          (ensures  (let inefficient_lpc_to_hpc = make_lpc_to_hpc lpcs hpcs lpc_to_hpc in
                     let pc_relation = lpc_hpc_pc_relation inefficient_lpc_to_hpc in
                     thread_states_match_per_pc_relation pc_relation
                       (convert_efficient_thread_state lpcs lts)
                       (convert_efficient_thread_state hpcs hts)))
          [SMTPat (thread_states_match_per_pc_relation (lpc_hpc_pc_relation (make_lpc_to_hpc lpcs hpcs lpc_to_hpc))
                    (convert_efficient_thread_state lpcs lts) (convert_efficient_thread_state hpcs hts))] =
  ()

let invert_make_pc_indices_to_pcs
  (pcs: array_t pc_t)
  (pc_indices: list nat{forall idx. list_contains idx pc_indices ==> idx < array_len pcs})
  (pc: pc_t{list_contains pc (make_pc_indices_to_pcs pcs pc_indices)})
  : GTot (idx: nat{list_contains idx pc_indices /\ array_nth pcs idx = Some pc}) =
  reverse_map_element_of_map_ghost (make_pc_index_to_pc pcs) pc_indices pc

let efficient_action_to_starting_thread_state_matches
  (pcs: array_t pc_t)
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : Lemma (requires action_corresponds_to_statement_pc_indices pcs action pc_indices)
          (ensures  action_to_starting_thread_state action = convert_efficient_thread_state pcs
                      (efficient_action_to_starting_thread_state pc_indices))
          [SMTPat (action_to_starting_thread_state action);
           SMTPat (action_corresponds_to_statement_pc_indices pcs action pc_indices)] =
  ()

let efficient_action_to_ending_thread_state_matches
  (pcs: array_t pc_t)
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : Lemma (requires action_corresponds_to_statement_pc_indices pcs action pc_indices)
          (ensures  action_to_ending_thread_state action = convert_efficient_thread_state pcs
                      (efficient_action_to_ending_thread_state action pc_indices))
          [SMTPat  (action_to_ending_thread_state action);
           SMTPat  (action_corresponds_to_statement_pc_indices pcs action pc_indices)] =
  ()
/
Util.Relation.fst.checked Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.VarHiding.Relation.fsti.checked Strategies.VarHiding.Inefficient.fsti.checked Strategies.VarHiding.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.VarHiding.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.VarHiding.Efficient.fst

    pcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    actions: Prims.list Armada.Action.t ->
    pc_indices_list: Prims.list Strategies.PCIndices.statement_pc_indices_t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.PCIndices.action_list_corresponds_to_statement_pc_indices_list pcs
          actions
          pc_indices_list)
      (ensures
        Strategies.ArmadaStatement.ThreadState.actions_to_ending_thread_state actions =
        Strategies.VarHiding.Efficient.convert_efficient_thread_state pcs
          (Strategies.ArmadaStatement.ThreadState.efficient_actions_to_ending_thread_state actions
              pc_indices_list))
      (decreases actions)
      [
        SMTPat (Strategies.ArmadaStatement.ThreadState.actions_to_ending_thread_state actions);
        SMTPat (Strategies.PCIndices.action_list_corresponds_to_statement_pc_indices_list pcs
              actions
              pc_indices_list)
      ]
Util.ImmutableArray.array_t Armada.Base.pc_t Prims.list Armada.Action.t Strategies.PCIndices.statement_pc_indices_t FStar.Pervasives.Native.Mktuple2 Strategies.VarHiding.Efficient.efficient_actions_to_ending_thread_state_matches FStar.Pervasives.false_elim Prims.unit Prims.b2t Strategies.PCIndices.action_list_corresponds_to_statement_pc_indices_list Prims.squash Prims.op_Equality Strategies.ArmadaStatement.ThreadState.thread_state_t Strategies.ArmadaStatement.ThreadState.actions_to_ending_thread_state Strategies.VarHiding.Efficient.convert_efficient_thread_state Strategies.ArmadaStatement.ThreadState.efficient_actions_to_ending_thread_state Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.bool Prims.Nil
let rec efficient_actions_to_ending_thread_state_matches
      (pcs: array_t pc_t)
      (actions: list Armada.Action.t)
      (pc_indices_list: list statement_pc_indices_t)
    : Lemma
      (requires action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
      (ensures
        actions_to_ending_thread_state actions =
        convert_efficient_thread_state pcs
          (efficient_actions_to_ending_thread_state actions pc_indices_list))
      (decreases actions)
      [
        SMTPat (actions_to_ending_thread_state actions);
        SMTPat (action_list_corresponds_to_statement_pc_indices_list pcs actions pc_indices_list)
      ] =
  
match actions, pc_indices_list with
| [], _ -> ()
| [action], [pc_indices] -> ()
| first_action :: remaining_actions, first_pc_indices :: remaining_pc_indices ->
  efficient_actions_to_ending_thread_state_matches pcs remaining_actions remaining_pc_indices
| _, _ -> false_elim ()