val lactions_all_hidden_implies_not_propagate
      (vs: list var_id_t)
      (lpc_to_hpc: (pc_t -> GTot pc_t))
      (lstart_state lend_state: thread_state_t)
      (lactions: list Armada.Action.t)
    : Lemma
      (requires lactions_all_hidden vs lpc_to_hpc lstart_state lend_state lactions /\ Cons? lactions
      )
      (ensures ~(PropagateWriteMessageStatement? (Cons?.hd lactions).program_statement.statement))
      (decreases lactions)
val lactions_all_hidden_implies_not_propagate
      (vs: list var_id_t)
      (lpc_to_hpc: (pc_t -> GTot pc_t))
      (lstart_state lend_state: thread_state_t)
      (lactions: list Armada.Action.t)
    : Lemma
      (requires lactions_all_hidden vs lpc_to_hpc lstart_state lend_state lactions /\ Cons? lactions
      )
      (ensures ~(PropagateWriteMessageStatement? (Cons?.hd lactions).program_statement.statement))
      (decreases lactions)
let rec lactions_all_hidden_implies_not_propagate
  (vs: list var_id_t)
  (lpc_to_hpc: pc_t -> GTot pc_t)
  (lstart_state: thread_state_t)
  (lend_state: thread_state_t)
  (lactions: list Armada.Action.t)
  : Lemma (requires   lactions_all_hidden vs lpc_to_hpc lstart_state lend_state lactions
                    /\ Cons? lactions)
          (ensures  ~(PropagateWriteMessageStatement? (Cons?.hd lactions).program_statement.statement))
          (decreases lactions) =
  match lactions with
  | [] -> ()
  | first_laction :: remaining_lactions ->
      if Cons? remaining_lactions then
        lactions_all_hidden_implies_not_propagate vs lpc_to_hpc
          (action_to_ending_thread_state first_laction) lend_state remaining_lactions
      else
        ()
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)

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

#push-options "--split_queries always"
let rec compute_hsteps_from_lsteps
  (vs: list var_id_t)
  (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)
  (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)
  (lactions: list Armada.Action.t)
  (hactions: list Armada.Action.t)
  (lsteps: list Armada.Step.t)
  : Ghost (list Armada.Step.t)
    (requires   lactions == map_ghost armada_step_to_action lsteps
              /\ lactions_correspond_to_hactions vs lpc_to_hpc return_lpcs lstart_state hstart_state
                  lend_state hend_state which_actions_hidden lactions hactions)
    (ensures  fun hsteps -> (let pc_relation = var_hiding_pc_relation lpc_to_hpc return_lpcs return_pcs_unique_proof in
                            lsteps_correspond_to_hsteps vs pc_relation lstart_state hstart_state
                              lend_state hend_state which_actions_hidden lsteps hsteps
                          /\ hactions == map_ghost armada_step_to_action hsteps))
    (decreases lactions) =
  let pc_relation = var_hiding_pc_relation lpc_to_hpc return_lpcs return_pcs_unique_proof in
  match which_actions_hidden, lactions, hactions, lsteps with
  | [], [], [], [] -> []
  | false :: remaining_which_actions_hidden, first_laction :: remaining_lactions, first_haction :: remaining_hactions,
      first_lstep :: remaining_lsteps ->
      let first_lstep: Armada.Step.t = first_lstep in
      let hstep = { nd = first_lstep.nd; action = first_haction } in
      let lnext_start_state = action_to_ending_thread_state first_laction in
      let hnext_start_state = action_to_ending_thread_state first_haction in
      let hsteps' = compute_hsteps_from_lsteps vs lpc_to_hpc return_lpcs return_pcs_unique_proof
                      lnext_start_state hnext_start_state lend_state hend_state remaining_which_actions_hidden
                      remaining_lactions remaining_hactions remaining_lsteps in
      let hsteps = hstep :: hsteps' in
      assert (lsteps_correspond_to_hsteps vs pc_relation lstart_state hstart_state lend_state hend_state
                which_actions_hidden lsteps hsteps);
      hsteps
  | true :: remaining_which_actions_hidden, first_laction :: remaining_lactions, _, first_lstep :: remaining_lsteps ->
      let lnext_start_state = action_to_ending_thread_state first_laction in
      let hsteps = compute_hsteps_from_lsteps vs lpc_to_hpc return_lpcs return_pcs_unique_proof
                     lnext_start_state hstart_state lend_state hend_state remaining_which_actions_hidden
                     remaining_lactions hactions remaining_lsteps in
      assert (lsteps_correspond_to_hsteps vs pc_relation lstart_state hstart_state lend_state hend_state
                which_actions_hidden lsteps hsteps);
      hsteps
  | _, _, _, _ -> false_elim ()
#pop-options

let lstep_corresponds_to_hstep_clarifier
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (lstep: Armada.Step.t)
  (hstep: Armada.Step.t)
  : Lemma (requires lstep_corresponds_to_hstep vs pc_relation lstep hstep)
          (ensures  (let lps, hps = lstep.action.program_statement, hstep.action.program_statement in
                     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 ->
    lpc_to_hpc: (_: Armada.Base.pc_t -> Prims.GTot Armada.Base.pc_t) ->
    lstart_state: Strategies.ArmadaStatement.ThreadState.thread_state_t ->
    lend_state: Strategies.ArmadaStatement.ThreadState.thread_state_t ->
    lactions: Prims.list Armada.Action.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarHiding.Defs.lactions_all_hidden vs lpc_to_hpc lstart_state lend_state lactions /\
        Cons? lactions)
      (ensures
        ~(PropagateWriteMessageStatement? (Mkprogram_statement_t?.statement (Mkt?.program_statement (
                      Cons?.hd lactions)))))
      (decreases lactions)
Prims.list Armada.Base.var_id_t Armada.Base.pc_t Strategies.ArmadaStatement.ThreadState.thread_state_t Armada.Action.t Prims.uu___is_Cons Strategies.VarHiding.Helpers.lactions_all_hidden_implies_not_propagate Strategies.ArmadaStatement.ThreadState.action_to_ending_thread_state Prims.bool Prims.unit Prims.l_and Strategies.VarHiding.Defs.lactions_all_hidden Prims.b2t Prims.squash Prims.l_not Armada.Statement.uu___is_PropagateWriteMessageStatement Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Action.__proj__Mkt__item__program_statement Prims.__proj__Cons__item__hd Prims.Nil FStar.Pervasives.pattern
let rec lactions_all_hidden_implies_not_propagate
      (vs: list var_id_t)
      (lpc_to_hpc: (pc_t -> GTot pc_t))
      (lstart_state lend_state: thread_state_t)
      (lactions: list Armada.Action.t)
    : Lemma
      (requires lactions_all_hidden vs lpc_to_hpc lstart_state lend_state lactions /\ Cons? lactions
      )
      (ensures ~(PropagateWriteMessageStatement? (Cons?.hd lactions).program_statement.statement))
      (decreases lactions) =
  
match lactions with
| [] -> ()
| first_laction :: remaining_lactions ->
  if Cons? remaining_lactions
  then
    lactions_all_hidden_implies_not_propagate vs
      lpc_to_hpc
      (action_to_ending_thread_state first_laction)
      lend_state
      remaining_lactions