val 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)
val 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 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)
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
/
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 ->
    pc_indices: Prims.list Prims.nat ->
    pc: Armada.Base.pc_t ->
    idx: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        Spec.List.list_contains pc
          (Strategies.VarHiding.Efficient.make_pc_indices_to_pcs pcs pc_indices) /\
        Util.ImmutableArray.array_nth pcs idx = FStar.Pervasives.Native.Some pc /\
        Util.ImmutableArray.array_elements_unique pcs /\
        (forall (idx: Prims.nat).
            Spec.List.list_contains idx pc_indices ==> idx < Util.ImmutableArray.array_len pcs))
      (ensures Spec.List.list_contains idx pc_indices)
Util.ImmutableArray.array_t Armada.Base.pc_t Prims.list Prims.nat Prims._assert Prims.b2t Prims.op_Equality Prims.unit Util.ImmutableArray.array_elements_unique_implication Prims.l_and Spec.List.contains_ubool Prims.eq2 Strategies.VarHiding.Efficient.make_pc_index_to_pc Util.List.reverse_map_element_of_map_ghost Spec.List.list_contains Strategies.VarHiding.Efficient.make_pc_indices_to_pcs FStar.Pervasives.Native.option Util.ImmutableArray.array_nth FStar.Pervasives.Native.Some Util.ImmutableArray.array_elements_unique Prims.l_Forall Prims.l_imp Prims.op_LessThan Util.ImmutableArray.array_len Prims.squash Prims.Nil FStar.Pervasives.pattern
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)