val initializers_match_except_global_variables_ensures_satisfies_global_initializers
      (vs: list var_id_t)
      (which_are_hidings: list bool)
      (linits 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)
val initializers_match_except_global_variables_ensures_satisfies_global_initializers
      (vs: list var_id_t)
      (which_are_hidings: list bool)
      (linits 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)
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
  )
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
  | _, _, _ -> ()
/
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

    vs: Prims.list Armada.Base.var_id_t ->
    which_are_hidings: Prims.list Prims.bool ->
    linits: Prims.list Armada.Init.initializer_t ->
    hinits: Prims.list Armada.Init.initializer_t ->
    mem: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarHiding.Defs.initializers_match_except_global_variables vs
          which_are_hidings
          linits
          hinits /\ Armada.Init.memory_satisfies_global_initializers mem linits)
      (ensures Armada.Init.memory_satisfies_global_initializers mem hinits)
Prims.list Armada.Base.var_id_t Prims.bool Armada.Init.initializer_t Armada.Memory.t FStar.Classical.Sugar.forall_intro Prims.l_imp Spec.List.contains_ubool Armada.Init.memory_satisfies_global_initializer FStar.Classical.Sugar.implies_intro Prims.squash Strategies.VarHiding.Initialization.initializers_match_except_global_variables_ensures_inclusion Prims.unit Prims.l_and Strategies.VarHiding.Defs.initializers_match_except_global_variables Armada.Init.memory_satisfies_global_initializers Prims.Nil FStar.Pervasives.pattern
let initializers_match_except_global_variables_ensures_satisfies_global_initializers
      (vs: list var_id_t)
      (which_are_hidings: list bool)
      (linits 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)