val remove_hidden_initializers_maintains_nonglobal_root
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (lmem: Armada.Memory.t)
      (root_id: root_id_t)
    : Lemma (requires not (RootIdGlobal? root_id))
      (ensures
        (let hmem = remove_hidden_initializers which_are_hidings inits lmem in
          hmem root_id == lmem root_id))
val remove_hidden_initializers_maintains_nonglobal_root
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (lmem: Armada.Memory.t)
      (root_id: root_id_t)
    : Lemma (requires not (RootIdGlobal? root_id))
      (ensures
        (let hmem = remove_hidden_initializers which_are_hidings inits lmem in
          hmem root_id == lmem root_id))
let rec remove_hidden_initializers_maintains_nonglobal_root
  (which_are_hidings: list bool)
  (inits: list initializer_t)
  (lmem: Armada.Memory.t)
  (root_id: root_id_t)
  : Lemma (requires not (RootIdGlobal? root_id))
          (ensures  (let hmem = remove_hidden_initializers which_are_hidings inits lmem in
                     hmem root_id == lmem root_id)) =
  match which_are_hidings, inits with
  | [], _ -> ()
  | true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_maintains_nonglobal_root remaining_which_are_hidings remaining_inits lmem root_id
  | false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_maintains_nonglobal_root remaining_which_are_hidings remaining_inits lmem root_id
  | _, _ -> ()
module Strategies.VarHiding.Initialization

open Armada.Base
open Armada.Computation
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Type
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.VarHiding
open Strategies.GlobalVars.VarIntro
open Strategies.Lift.Generic
open Strategies.Invariant
open Strategies.VarHiding.Defs
open Util.List

let rec remove_hidden_initializers_ensures_memories_match_except_gvars
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : Lemma (requires initializers_match_except_global_variables vs which_are_hidings linits hinits)
          (ensures  (let hmem = remove_hidden_initializers which_are_hidings linits lmem in
                     memories_match_except_global_variables vs lmem hmem)) =
  match which_are_hidings, linits, hinits with
  | [], [], [] -> ()
  | true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
      remove_hidden_initializers_ensures_memories_match_except_gvars vs remaining_which_are_hidings remaining_linits
        hinits lmem
  | false :: remaining_which_are_hidings, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      remove_hidden_initializers_ensures_memories_match_except_gvars vs remaining_which_are_hidings remaining_linits
        remaining_hinits lmem
  | _, _, _ -> ()

let rec initializers_match_except_global_variables_ensures_inclusion
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (init: initializer_t)
  : Lemma (requires   contains_ubool init hinits
                    /\ initializers_match_except_global_variables vs which_are_hidings linits hinits)
          (ensures  contains_ubool init linits) =
  match which_are_hidings, linits, hinits with
  | [], [], [] -> ()
  | true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
      initializers_match_except_global_variables_ensures_inclusion vs remaining_which_are_hidings
        remaining_linits hinits init
  | false :: remaining_which_are_hidings, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      if eqb init first_hinit then
        ()
      else
        initializers_match_except_global_variables_ensures_inclusion vs remaining_which_are_hidings
          remaining_linits remaining_hinits init
  | _, _, _ -> ()

let initializers_match_except_global_variables_ensures_satisfies_global_initializers
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (mem: Armada.Memory.t)
  : Lemma (requires   initializers_match_except_global_variables vs which_are_hidings linits hinits
                    /\ memory_satisfies_global_initializers mem linits)
          (ensures  memory_satisfies_global_initializers mem hinits) =
  introduce forall init. contains_ubool init hinits ==> memory_satisfies_global_initializer mem init
  with introduce _ ==> _
  with _. (
    initializers_match_except_global_variables_ensures_inclusion vs which_are_hidings linits hinits init
  )

let rec initializers_match_except_global_variables_ensures_no_gvars_in_hinits
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  : Lemma (requires initializers_match_except_global_variables vs which_are_hidings linits hinits)
          (ensures  forall init. contains_ubool init hinits ==> not (list_contains init.var_id vs)) =
  match which_are_hidings, linits, hinits with
  | [], [], [] -> ()
  | true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
      initializers_match_except_global_variables_ensures_no_gvars_in_hinits vs remaining_which_are_hidings
        remaining_linits hinits
  | false :: remaining_which_are_hidings, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      initializers_match_except_global_variables_ensures_no_gvars_in_hinits vs remaining_which_are_hidings
        remaining_linits remaining_hinits
  | _, _, _ -> ()
  
let rec remove_hidden_initializers_maintains_memory_satisfies_global_initializers
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (all_hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : Lemma (requires   initializers_match_except_global_variables vs which_are_hidings linits hinits
                    /\ memory_satisfies_global_initializers lmem all_hinits
                    /\ (forall init. contains_ubool init hinits ==> contains_ubool init all_hinits)
                    /\ (forall init. contains_ubool init all_hinits ==> not (list_contains init.var_id vs)))
          (ensures  (let hmem = remove_hidden_initializers which_are_hidings linits lmem in
                     memory_satisfies_global_initializers hmem all_hinits)) =
  match which_are_hidings, linits, hinits with
  | [], [], [] -> ()
  | true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
      remove_hidden_initializers_maintains_memory_satisfies_global_initializers vs remaining_which_are_hidings
        remaining_linits hinits all_hinits lmem
  | false :: remaining_which_are_hidings, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      remove_hidden_initializers_maintains_memory_satisfies_global_initializers vs remaining_which_are_hidings
        remaining_linits remaining_hinits all_hinits lmem
  | _, _, _ -> ()

let remove_hidden_initializers_ensures_satisfies_global_initializers
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  (* see .fsti file for spec *) =
  initializers_match_except_global_variables_ensures_satisfies_global_initializers vs which_are_hidings
    linits hinits lmem;
  initializers_match_except_global_variables_ensures_no_gvars_in_hinits vs which_are_hidings linits hinits;
  remove_hidden_initializers_maintains_memory_satisfies_global_initializers vs which_are_hidings linits
    hinits hinits lmem;
  remove_hidden_initializers_ensures_memories_match_except_gvars vs which_are_hidings linits hinits lmem
/
Util.List.fst.checked Strategies.VarHiding.Defs.fst.checked Strategies.Lift.Generic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.VarHiding.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.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
Strategies.VarHiding.Initialization.fst

    which_are_hidings: Prims.list Prims.bool ->
    inits: Prims.list Armada.Init.initializer_t ->
    lmem: Armada.Memory.t ->
    root_id: Armada.Base.root_id_t
  -> FStar.Pervasives.Lemma (requires Prims.op_Negation (RootIdGlobal? root_id))
      (ensures
        (let hmem =
            Strategies.VarHiding.Initialization.remove_hidden_initializers which_are_hidings
              inits
              lmem
          in
          hmem root_id == lmem root_id))
Prims.list Prims.bool Armada.Init.initializer_t Armada.Memory.t Armada.Base.root_id_t FStar.Pervasives.Native.Mktuple2 Strategies.VarHiding.Initialization.remove_hidden_initializers_maintains_nonglobal_root Prims.unit Prims.b2t Prims.op_Negation Armada.Base.uu___is_RootIdGlobal Prims.squash Prims.eq2 Armada.Memory.root_t Strategies.VarHiding.Initialization.remove_hidden_initializers Prims.Nil FStar.Pervasives.pattern
let rec remove_hidden_initializers_maintains_nonglobal_root
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (lmem: Armada.Memory.t)
      (root_id: root_id_t)
    : Lemma (requires not (RootIdGlobal? root_id))
      (ensures
        (let hmem = remove_hidden_initializers which_are_hidings inits lmem in
          hmem root_id == lmem root_id)) =
  
match which_are_hidings, inits with
| [], _ -> ()
| true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
  remove_hidden_initializers_maintains_nonglobal_root remaining_which_are_hidings
    remaining_inits
    lmem
    root_id
| false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
  remove_hidden_initializers_maintains_nonglobal_root remaining_which_are_hidings
    remaining_inits
    lmem
    root_id
| _, _ -> ()