val remove_hidden_initializers_doesnt_add_global
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (mem: Armada.Memory.t)
      (root_id: root_id_t)
    : Lemma
      (requires
        (let mem' = remove_hidden_initializers which_are_hidings inits mem in
          RootGlobal? (mem' root_id))) (ensures RootGlobal? (mem root_id))
val remove_hidden_initializers_doesnt_add_global
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (mem: Armada.Memory.t)
      (root_id: root_id_t)
    : Lemma
      (requires
        (let mem' = remove_hidden_initializers which_are_hidings inits mem in
          RootGlobal? (mem' root_id))) (ensures RootGlobal? (mem root_id))
let rec remove_hidden_initializers_doesnt_add_global
  (which_are_hidings: list bool)
  (inits: list initializer_t)
  (mem: Armada.Memory.t)
  (root_id: root_id_t)
  : Lemma (requires (let mem' = remove_hidden_initializers which_are_hidings inits mem in
                     RootGlobal? (mem' root_id)))
          (ensures  RootGlobal? (mem root_id)) =
  match which_are_hidings, inits with
  | [], _ -> ()
  | true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_doesnt_add_global remaining_which_are_hidings
        remaining_inits mem root_id
  | false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_doesnt_add_global remaining_which_are_hidings
        remaining_inits mem 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

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
  | _, _ -> ()

let rec remove_hidden_initializers_ensures_satisfies_main_stack_initializers
  (vs: list var_id_t)
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (initial_tid: tid_t)
  (main_method_id: method_id_t)
  (initial_frame_uniq: root_id_uniquifier_t)
  (local_variables: list var_id_t)
  (main_stack_initializers: list initializer_t)
  (lmem: Armada.Memory.t)
  (* see .fsti file for spec *) =
  match local_variables, main_stack_initializers with
  | [], [] -> ()
  | var_id :: remaining_var_ids, initializer :: remaining_initializers ->
      let root_id = RootIdStack initial_tid main_method_id initial_frame_uniq var_id in
      remove_hidden_initializers_maintains_nonglobal_root which_are_hidings linits lmem root_id;
      remove_hidden_initializers_ensures_satisfies_main_stack_initializers vs which_are_hidings linits
        initial_tid main_method_id initial_frame_uniq remaining_var_ids remaining_initializers lmem
  | _ -> ()

let rec matching_hinits_are_present
  (which_are_hidings: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : GTot bool =
  match which_are_hidings, linits, hinits with
  | [], [], [] -> true
  | true :: remaining_which_are_hidings, first_linit :: remaining_linits, _ ->
      matching_hinits_are_present remaining_which_are_hidings remaining_linits hinits lmem
  | false :: remaining_which_are_hidings, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      (match lmem (RootIdGlobal first_hinit.var_id) with
       | RootGlobal _ -> exists_ghost (var_id_in_initializer first_hinit.var_id) hinits
       | _ -> false)
  | _, _, _ -> false

let rec remove_hidden_initializers_maintains_roots_match
  (which_are_hidings: list bool)
  (inits: list initializer_t)
  (mem: Armada.Memory.t)
  : Lemma (requires roots_match mem)
          (ensures  roots_match (remove_hidden_initializers which_are_hidings inits mem)) =
  match which_are_hidings, inits with
  | [], _ -> ()
  | true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_maintains_roots_match remaining_which_are_hidings remaining_inits mem
  | false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_maintains_roots_match remaining_which_are_hidings remaining_inits mem
  | _, _ -> ()

let rec remove_hidden_initializers_doesnt_change_nonglobal
  (which_are_hidings: list bool)
  (inits: list initializer_t)
  (mem: Armada.Memory.t)
  (root_id: root_id_t)
  : Lemma (requires not (RootIdGlobal? root_id))
          (ensures  mem root_id == (remove_hidden_initializers which_are_hidings inits mem) root_id) =
  match which_are_hidings, inits with
  | [], _ -> ()
  | true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_doesnt_change_nonglobal remaining_which_are_hidings remaining_inits mem root_id
  | false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_doesnt_change_nonglobal remaining_which_are_hidings remaining_inits mem root_id
  | _, _ -> ()

let rec remove_hidden_initializers_maintains_root_invalid_outside_initializations
  (which_are_hidings: list bool)
  (inits: list initializer_t)
  (mem: Armada.Memory.t)
  (root_id: root_id_t)
  : Lemma (requires not (RootIdGlobal? root_id))
          (ensures  mem root_id == (remove_hidden_initializers which_are_hidings inits mem) root_id) =
  match which_are_hidings, inits with
  | [], _ -> ()
  | true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_maintains_root_invalid_outside_initializations remaining_which_are_hidings
        remaining_inits mem root_id
  | false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
      remove_hidden_initializers_maintains_root_invalid_outside_initializations remaining_which_are_hidings
        remaining_inits mem root_id
  | _, _ -> ()
/
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 ->
    mem: Armada.Memory.t ->
    root_id: Armada.Base.root_id_t
  -> FStar.Pervasives.Lemma
      (requires
        (let mem' =
            Strategies.VarHiding.Initialization.remove_hidden_initializers which_are_hidings
              inits
              mem
          in
          RootGlobal? (mem' root_id))) (ensures RootGlobal? (mem 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_doesnt_add_global Prims.unit Prims.b2t Armada.Memory.uu___is_RootGlobal Strategies.VarHiding.Initialization.remove_hidden_initializers Prims.squash Prims.Nil FStar.Pervasives.pattern
let rec remove_hidden_initializers_doesnt_add_global
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (mem: Armada.Memory.t)
      (root_id: root_id_t)
    : Lemma
      (requires
        (let mem' = remove_hidden_initializers which_are_hidings inits mem in
          RootGlobal? (mem' root_id))) (ensures RootGlobal? (mem root_id)) =
  
match which_are_hidings, inits with
| [], _ -> ()
| true :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
  remove_hidden_initializers_doesnt_add_global remaining_which_are_hidings
    remaining_inits
    mem
    root_id
| false :: remaining_which_are_hidings, first_hinit :: remaining_inits ->
  remove_hidden_initializers_doesnt_add_global remaining_which_are_hidings
    remaining_inits
    mem
    root_id
| _, _ -> ()