val 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)
val 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)
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
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;
  }
/
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
hactions: Prims.list Armada.Action.t -> Prims.Ghost (Prims.list Armada.Step.t)
Prims.list Armada.Action.t Prims.Nil Armada.Step.t Prims.Cons Strategies.VarHiding.Helpers.compute_hsteps_from_hactions Armada.Step.Mkt Armada.Type.object_value_t Prims.l_True Prims.eq2 Util.List.map_ghost Strategies.Semantics.Armada.armada_step_to_action
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