val lsteps_correspond_to_hsteps
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (lstart_state hstart_state lend_state hend_state: thread_state_t)
      (which_actions_hidden: list bool)
      (lsteps hsteps: list Armada.Step.t)
    : GTot ubool (decreases lsteps)
val lsteps_correspond_to_hsteps
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (lstart_state hstart_state lend_state hend_state: thread_state_t)
      (which_actions_hidden: list bool)
      (lsteps hsteps: list Armada.Step.t)
    : GTot ubool (decreases lsteps)
let rec lsteps_correspond_to_hsteps
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (lstart_state: thread_state_t)
  (hstart_state: thread_state_t)
  (lend_state: thread_state_t)
  (hend_state: thread_state_t)
  (which_actions_hidden: list bool)
  (lsteps: list Armada.Step.t)
  (hsteps: list Armada.Step.t)
  : GTot ubool
  (decreases lsteps) =
  match which_actions_hidden, lsteps, hsteps with
  | [], [], [] -> True
  | false :: remaining_which_actions_hidden, first_lstep :: remaining_lsteps, first_hstep :: remaining_hsteps ->
      let first_lstep: Armada.Step.t = first_lstep in
      let first_hstep: Armada.Step.t = first_hstep in
         lstep_corresponds_to_hstep vs pc_relation first_lstep first_hstep
      /\ action_to_starting_thread_state first_lstep.action = lstart_state
      /\ action_to_starting_thread_state first_hstep.action = hstart_state
      /\ ThreadStateAtPC? lstart_state
      /\ ThreadStateAtPC? hstart_state
      /\ thread_states_match_per_pc_relation pc_relation.relation lstart_state hstart_state
      /\ thread_states_match_per_pc_relation pc_relation.relation (action_to_ending_thread_state first_lstep.action)
           (action_to_ending_thread_state first_hstep.action)
      /\ lsteps_correspond_to_hsteps vs pc_relation
           (action_to_ending_thread_state first_lstep.action) (action_to_ending_thread_state first_hstep.action)
           lend_state hend_state remaining_which_actions_hidden remaining_lsteps remaining_hsteps
  | true :: remaining_which_actions_hidden, first_lstep :: remaining_lsteps, _ ->
         action_to_starting_thread_state first_lstep.action = lstart_state
      /\ ThreadStateAtPC? lstart_state
      /\ thread_states_match_per_pc_relation pc_relation.relation lstart_state hstart_state
      /\ thread_states_match_per_pc_relation pc_relation.relation
           (action_to_ending_thread_state first_lstep.action) hstart_state
      /\ statement_updates_gvars vs first_lstep.action.program_statement.statement
      /\ lsteps_correspond_to_hsteps vs pc_relation (action_to_ending_thread_state first_lstep.action)
           hstart_state lend_state hend_state remaining_which_actions_hidden remaining_lsteps hsteps
  | _, _, _ -> False
module Strategies.VarHiding.Helpers

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Step
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open FStar.WellFoundedRelation
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.ArmadaStatement.Propagate
open Strategies.ArmadaStatement.Status
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.Types
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.VarIntro
open Strategies.Lift.Generic
open Strategies.Invariant
open Strategies.PCRelation
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarHiding.Defs
open Util.List
open Util.Nth
open Util.Seq

/// Definitions

let return_pcs_unique_proof_t (lpc_to_hpc: pc_t -> GTot pc_t) (return_lpcs: list pc_t) =
  unit -> Lemma (return_pcs_unique lpc_to_hpc return_lpcs)

let var_hiding_pc_relation
  (lpc_to_hpc: pc_t -> GTot pc_t)
  (return_lpcs: list pc_t)
  (return_pcs_unique_proof: return_pcs_unique_proof_t lpc_to_hpc return_lpcs)
  : pc_relation_t =
  return_pcs_unique_proof ();
  let return_relation = (fun lpc hpc -> list_contains lpc return_lpcs && lpc_to_hpc lpc = hpc) in
  {
    relation = (fun lpc hpc -> lpc_to_hpc lpc = hpc);
    return_relation = return_relation;
  }

let rec compute_hsteps_from_hactions
  (hactions: list Armada.Action.t)
  : Ghost (list Armada.Step.t)
    (requires True)
    (ensures fun hsteps -> map_ghost armada_step_to_action hsteps == hactions) =
  match hactions with
  | [] -> []
  | first_haction :: remaining_hactions ->
      let first_hstep = { nd = []; action = first_haction } in
      first_hstep :: compute_hsteps_from_hactions remaining_hactions

/// Correspondence between lsteps and hsteps

let lstep_corresponds_to_hstep
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (lstep: Armada.Step.t)
  (hstep: Armada.Step.t)
  : GTot ubool =
  let lps, hps = lstep.action.program_statement, hstep.action.program_statement in
    lstep.nd == hstep.nd
  /\ statement_effect_independent_of_global_variables vs lps.statement
  /\ statements_match_per_pc_relation pc_relation.relation pc_relation.return_relation lps.statement hps.statement
  /\ (match lps.end_pc, hps.end_pc with
     | Some lpc, Some hpc ->
           pc_relation.relation lpc hpc
         /\ (ReturnStatement? lps.statement ==> pc_relation.return_relation lpc hpc)
     | None, None -> True
     | _, _ -> False)
/
Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.VarHiding.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCRelation.fst.checked Strategies.Lift.Generic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Strategies.ArmadaStatement.Propagate.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.WellFoundedRelation.fsti.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.VarHiding.Helpers.fst

    vs: Prims.list Armada.Base.var_id_t ->
    pc_relation: Strategies.PCRelation.pc_relation_t ->
    lstart_state: Strategies.ArmadaStatement.ThreadState.thread_state_t ->
    hstart_state: Strategies.ArmadaStatement.ThreadState.thread_state_t ->
    lend_state: Strategies.ArmadaStatement.ThreadState.thread_state_t ->
    hend_state: Strategies.ArmadaStatement.ThreadState.thread_state_t ->
    which_actions_hidden: Prims.list Prims.bool ->
    lsteps: Prims.list Armada.Step.t ->
    hsteps: Prims.list Armada.Step.t
  -> Prims.GTot Spec.Ubool.ubool
Prims.list Armada.Base.var_id_t Strategies.PCRelation.pc_relation_t Strategies.ArmadaStatement.ThreadState.thread_state_t Prims.bool Armada.Step.t FStar.Pervasives.Native.Mktuple3 Prims.l_True Prims.l_and Strategies.VarHiding.Helpers.lstep_corresponds_to_hstep Prims.b2t Prims.op_Equality Strategies.ArmadaStatement.ThreadState.action_to_starting_thread_state Armada.Step.__proj__Mkt__item__action Strategies.ArmadaStatement.ThreadState.uu___is_ThreadStateAtPC Strategies.ArmadaStatement.ThreadState.thread_states_match_per_pc_relation Strategies.PCRelation.__proj__Mkpc_relation_t__item__relation Strategies.ArmadaStatement.ThreadState.action_to_ending_thread_state Strategies.VarHiding.Helpers.lsteps_correspond_to_hsteps Strategies.GlobalVars.VarIntro.statement_updates_gvars Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Action.__proj__Mkt__item__program_statement Prims.l_False Spec.Ubool.ubool
let rec lsteps_correspond_to_hsteps
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (lstart_state hstart_state lend_state hend_state: thread_state_t)
      (which_actions_hidden: list bool)
      (lsteps hsteps: list Armada.Step.t)
    : GTot ubool (decreases lsteps) =
  
match which_actions_hidden, lsteps, hsteps with
| [], [], [] -> True
| false :: remaining_which_actions_hidden,
first_lstep :: remaining_lsteps,
first_hstep :: remaining_hsteps ->
  let first_lstep:Armada.Step.t = first_lstep in
  let first_hstep:Armada.Step.t = first_hstep in
  lstep_corresponds_to_hstep vs pc_relation first_lstep first_hstep /\
  action_to_starting_thread_state first_lstep.action = lstart_state /\
  action_to_starting_thread_state first_hstep.action = hstart_state /\ ThreadStateAtPC? lstart_state /\
  ThreadStateAtPC? hstart_state /\
  thread_states_match_per_pc_relation pc_relation.relation lstart_state hstart_state /\
  thread_states_match_per_pc_relation pc_relation.relation
    (action_to_ending_thread_state first_lstep.action)
    (action_to_ending_thread_state first_hstep.action) /\
  lsteps_correspond_to_hsteps vs
    pc_relation
    (action_to_ending_thread_state first_lstep.action)
    (action_to_ending_thread_state first_hstep.action)
    lend_state
    hend_state
    remaining_which_actions_hidden
    remaining_lsteps
    remaining_hsteps
| true :: remaining_which_actions_hidden, first_lstep :: remaining_lsteps, _ ->
  action_to_starting_thread_state first_lstep.action = lstart_state /\ ThreadStateAtPC? lstart_state /\
  thread_states_match_per_pc_relation pc_relation.relation lstart_state hstart_state /\
  thread_states_match_per_pc_relation pc_relation.relation
    (action_to_ending_thread_state first_lstep.action)
    hstart_state /\ statement_updates_gvars vs first_lstep.action.program_statement.statement /\
  lsteps_correspond_to_hsteps vs
    pc_relation
    (action_to_ending_thread_state first_lstep.action)
    hstart_state
    lend_state
    hend_state
    remaining_which_actions_hidden
    remaining_lsteps
    hsteps
| _, _, _ -> False