val make_lpc_to_hpc
      (lpcs 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
val make_lpc_to_hpc
      (lpcs 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
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
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
/
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

    lpcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    hpcs: Util.ImmutableArray.array_t Armada.Base.pc_t ->
    lpc_to_hpc:
      Util.ImmutableArray.array_t Prims.nat
        {Util.ImmutableArray.array_len lpc_to_hpc = Util.ImmutableArray.array_len lpcs} ->
    lpc: Armada.Base.pc_t
  -> Prims.GTot Armada.Base.pc_t
Util.ImmutableArray.array_t Armada.Base.pc_t Prims.nat Prims.b2t Prims.op_Equality Util.ImmutableArray.array_len Util.ImmutableArray.find_in_array Strategies.VarHiding.Efficient.default_pc Strategies.VarHiding.Efficient.make_pc_index_to_pc Util.ImmutableArray.array_index
let make_lpc_to_hpc
      (lpcs 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