val remove_hidden_initializers
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (mem: Armada.Memory.t)
    : GTot Armada.Memory.t
val remove_hidden_initializers
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (mem: Armada.Memory.t)
    : GTot Armada.Memory.t
let rec remove_hidden_initializers
  (which_are_hidings: list bool)
  (inits: list initializer_t)
  (mem: Armada.Memory.t)
  : GTot Armada.Memory.t =
  match which_are_hidings, inits with
  | [], _ -> mem
  | true :: remaining_which_are_hidings, first_init :: remaining_inits ->
      let mem' = remove_hidden_initializers remaining_which_are_hidings remaining_inits mem in
      remove_hidden_initializer first_init mem'
  | false :: remaining_which_are_hidings, first_init :: remaining_inits ->
      remove_hidden_initializers remaining_which_are_hidings remaining_inits mem
  | _, _ -> mem
module Strategies.VarHiding.Initialization

open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Type
open Spec.List
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Types
open Strategies.VarHiding.Defs

let remove_hidden_initializer
  (init: initializer_t)
  (mem: Armada.Memory.t)
  : GTot Armada.Memory.t =
  let root_id = RootIdGlobal init.var_id in
  Spec.Map.upd mem root_id RootInvalid
/
Strategies.VarHiding.Defs.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked
Strategies.VarHiding.Initialization.fsti

    which_are_hidings: Prims.list Prims.bool ->
    inits: Prims.list Armada.Init.initializer_t ->
    mem: Armada.Memory.t
  -> Prims.GTot Armada.Memory.t
Prims.list Prims.bool Armada.Init.initializer_t Armada.Memory.t FStar.Pervasives.Native.Mktuple2 Strategies.VarHiding.Initialization.remove_hidden_initializer Strategies.VarHiding.Initialization.remove_hidden_initializers
let rec remove_hidden_initializers
      (which_are_hidings: list bool)
      (inits: list initializer_t)
      (mem: Armada.Memory.t)
    : GTot Armada.Memory.t =
  
match which_are_hidings, inits with
| [], _ -> mem
| true :: remaining_which_are_hidings, first_init :: remaining_inits ->
  let mem' = remove_hidden_initializers remaining_which_are_hidings remaining_inits mem in
  remove_hidden_initializer first_init mem'
| false :: remaining_which_are_hidings, first_init :: remaining_inits ->
  remove_hidden_initializers remaining_which_are_hidings remaining_inits mem
| _, _ -> mem