val apply_efficient_return_lpcs_unique
      (num_lpcs: nat)
      (lpc_to_lpc: array_t nat)
      (is_return_lpc: array_t bool)
      (lpc1 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)
val apply_efficient_return_lpcs_unique
      (num_lpcs: nat)
      (lpc_to_lpc: array_t nat)
      (is_return_lpc: array_t bool)
      (lpc1 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)
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)
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
/
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

    num_lpcs: Prims.nat ->
    lpc_to_lpc: Util.ImmutableArray.array_t Prims.nat ->
    is_return_lpc: Util.ImmutableArray.array_t Prims.bool ->
    lpc1: Prims.nat ->
    lpc2: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarHiding.Efficient.efficient_return_lpcs_unique num_lpcs
          lpc_to_lpc
          is_return_lpc /\ lpc1 < num_lpcs /\ lpc2 < num_lpcs /\
        Util.ImmutableArray.array_nth is_return_lpc lpc1 = FStar.Pervasives.Native.Some true /\
        Util.ImmutableArray.array_nth is_return_lpc lpc2 = FStar.Pervasives.Native.Some true /\
        Util.ImmutableArray.array_nth lpc_to_lpc lpc1 =
        Util.ImmutableArray.array_nth lpc_to_lpc lpc2) (ensures lpc1 = lpc2)
Prims.nat Util.ImmutableArray.array_t Prims.bool Prims._assert Prims.b2t Strategies.VarHiding.Efficient.efficient_return_lpcs_unique_inner2 Prims.unit Strategies.VarHiding.Efficient.efficient_return_lpcs_unique_inner1 Prims.l_and Strategies.VarHiding.Efficient.efficient_return_lpcs_unique Prims.op_LessThan Prims.op_Equality FStar.Pervasives.Native.option Util.ImmutableArray.array_nth FStar.Pervasives.Native.Some Prims.squash Prims.Nil FStar.Pervasives.pattern
let apply_efficient_return_lpcs_unique
      (num_lpcs: nat)
      (lpc_to_lpc: array_t nat)
      (is_return_lpc: array_t bool)
      (lpc1 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)