val storage_satisfies_initializer_implies_gvars_unaddressed
      (vs: list var_id_t)
      (initializer: initializer_t)
      (storage: valid_object_storage_t)
    : Lemma
      (requires
        global_variables_unaddressed_in_initializer vs initializer /\
        storage_satisfies_initializer storage initializer.iv initializer.weakly_consistent)
      (ensures global_variables_unaddressed_in_storage vs storage)
val storage_satisfies_initializer_implies_gvars_unaddressed
      (vs: list var_id_t)
      (initializer: initializer_t)
      (storage: valid_object_storage_t)
    : Lemma
      (requires
        global_variables_unaddressed_in_initializer vs initializer /\
        storage_satisfies_initializer storage initializer.iv initializer.weakly_consistent)
      (ensures global_variables_unaddressed_in_storage vs storage)
let storage_satisfies_initializer_implies_gvars_unaddressed
  (vs: list var_id_t)
  (initializer: initializer_t)
  (storage: valid_object_storage_t)
  : Lemma (requires   global_variables_unaddressed_in_initializer vs initializer
                    /\ storage_satisfies_initializer storage initializer.iv initializer.weakly_consistent)
          (ensures  global_variables_unaddressed_in_storage vs storage) =
  match initializer.iv with
  | InitializerArbitrary td ->
      object_storage_arbitrarily_initialized_correctly_doesnt_depend_on_gvars vs storage
  | InitializerSpecific value ->
      object_storage_initialized_correctly_doesnt_depend_on_gvars vs storage value
module Strategies.GlobalVars.Init

open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Spec.List
open Spec.Ubool
open Strategies.GlobalVars
open Strategies.GlobalVars.Util
open Util.List

let rec memory_satisfies_main_stack_initializers_implies_satisfies_initializer
  (mem: Armada.Memory.t)
  (tid: tid_t)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (initializers: list initializer_t)
  (initializer: initializer_t)
  : Lemma (requires   contains_ubool initializer initializers
                    /\ memory_satisfies_main_stack_initializers mem tid method_id frame_uniq var_ids initializers)
          (ensures  memory_satisfies_main_stack_initializer mem tid method_id frame_uniq initializer.var_id
                      initializer) =
  match var_ids, initializers with
  | first_var_id :: remaining_var_ids, first_initializer :: remaining_initializers ->
      if eqb first_initializer initializer then
        ()
      else
        memory_satisfies_main_stack_initializers_implies_satisfies_initializer mem tid method_id frame_uniq
          remaining_var_ids remaining_initializers initializer

let rec get_initializer_for_initialized_main_stack_variable
  (mem: Armada.Memory.t)
  (tid: tid_t)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (initializers: list initializer_t)
  (var_id: var_id_t)
  : Ghost initializer_t
     (requires   list_contains var_id var_ids
               /\ memory_satisfies_main_stack_initializers mem tid method_id frame_uniq var_ids initializers)
     (ensures  fun initializer ->
                     contains_ubool initializer initializers
                   /\ memory_satisfies_main_stack_initializer mem tid method_id frame_uniq var_id initializer) =
  match var_ids, initializers with
  | first_var_id :: remaining_var_ids, first_initializer :: remaining_initializers ->
      if eqb first_var_id var_id then
        first_initializer
      else
        get_initializer_for_initialized_main_stack_variable mem tid method_id frame_uniq remaining_var_ids
          remaining_initializers var_id
/
Util.List.fst.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.fst.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.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked
Strategies.GlobalVars.Init.fst

    vs: Prims.list Armada.Base.var_id_t ->
    initializer: Armada.Init.initializer_t ->
    storage: Armada.Memory.valid_object_storage_t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.global_variables_unaddressed_in_initializer vs initializer /\
        Armada.Init.storage_satisfies_initializer storage
          (Mkinitializer_t?.iv initializer)
          (Mkinitializer_t?.weakly_consistent initializer))
      (ensures Strategies.GlobalVars.global_variables_unaddressed_in_storage vs storage)
Prims.list Armada.Base.var_id_t Armada.Init.initializer_t Armada.Memory.valid_object_storage_t Armada.Init.__proj__Mkinitializer_t__item__iv Armada.Type.object_td_t Strategies.GlobalVars.Util.object_storage_arbitrarily_initialized_correctly_doesnt_depend_on_gvars Armada.Type.object_value_t Strategies.GlobalVars.Util.object_storage_initialized_correctly_doesnt_depend_on_gvars Prims.unit Prims.l_and Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_initializer Armada.Init.storage_satisfies_initializer Armada.Init.__proj__Mkinitializer_t__item__weakly_consistent Prims.squash Strategies.GlobalVars.global_variables_unaddressed_in_storage Prims.Nil FStar.Pervasives.pattern
let storage_satisfies_initializer_implies_gvars_unaddressed
      (vs: list var_id_t)
      (initializer: initializer_t)
      (storage: valid_object_storage_t)
    : Lemma
      (requires
        global_variables_unaddressed_in_initializer vs initializer /\
        storage_satisfies_initializer storage initializer.iv initializer.weakly_consistent)
      (ensures global_variables_unaddressed_in_storage vs storage) =
  
match initializer.iv with
| InitializerArbitrary td ->
  object_storage_arbitrarily_initialized_correctly_doesnt_depend_on_gvars vs storage
| InitializerSpecific value ->
  object_storage_initialized_correctly_doesnt_depend_on_gvars vs storage value