val 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))]
val 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))]
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
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
/
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
pcs: Util.ImmutableArray.array_t Armada.Base.pc_t -> idx: Prims.nat
  -> FStar.Pervasives.Lemma (requires Some? (Util.ImmutableArray.array_nth pcs idx))
      (ensures
        Spec.List.list_contains (Some?.v (Util.ImmutableArray.array_nth pcs idx))
          (Util.ImmutableArray.array_to_list pcs))
      [SMTPat (Some? (Util.ImmutableArray.array_nth pcs idx))]
Util.ImmutableArray.array_t Armada.Base.pc_t Prims.nat Util.ImmutableArray.array_nth Util.Nth.nth_implies_contains Util.ImmutableArray.array_to_list Prims.unit Util.ImmutableArray.array_matches_list_implies_nth_equivalent Util.ImmutableArray.array_to_list_implies_array_matches_list Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.squash Spec.List.list_contains FStar.Pervasives.Native.__proj__Some__item__v Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.bool Prims.Nil
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