val init_implies_global_variables_unaddressed_in_memory
      (vs: list var_id_t)
      (program: Armada.Program.t)
      (s: Armada.State.t)
    : Lemma
      (requires
        init_program program s /\
        global_variables_unaddressed_in_initializers vs program.global_initializers /\
        global_variables_unaddressed_in_initializers vs program.main_stack_initializers)
      (ensures global_variables_unaddressed_in_memory vs s.mem)
val init_implies_global_variables_unaddressed_in_memory
      (vs: list var_id_t)
      (program: Armada.Program.t)
      (s: Armada.State.t)
    : Lemma
      (requires
        init_program program s /\
        global_variables_unaddressed_in_initializers vs program.global_initializers /\
        global_variables_unaddressed_in_initializers vs program.main_stack_initializers)
      (ensures global_variables_unaddressed_in_memory vs s.mem)
let init_implies_global_variables_unaddressed_in_memory
  (vs: list var_id_t)
  (program: Armada.Program.t)
  (s: Armada.State.t)
  : Lemma (requires   init_program program s
                    /\ global_variables_unaddressed_in_initializers vs program.global_initializers
                    /\ global_variables_unaddressed_in_initializers vs program.main_stack_initializers)
          (ensures  global_variables_unaddressed_in_memory vs s.mem) =
  introduce forall root_id. global_variables_unaddressed_in_root vs (s.mem root_id)
  with (
    let thread = s.threads s.initial_tid in
    let initial_frame_uniq = Cons?.hd s.uniqs_used in
    let root = s.mem root_id in
    assert (root_invalid_outside_initializations s.mem program.global_initializers s.initial_tid
              program.main_method_id initial_frame_uniq thread.top.local_variables root_id);
    match root with
    | RootGlobal storage ->
        (match root_id with
         | RootIdGlobal var_id ->
             assert (exists_ghost (var_id_in_initializer var_id) program.global_initializers);
             let initializer = exists_ghost_to_witness (var_id_in_initializer var_id) program.global_initializers in
             for_all_ubool_equivalent_to_forall (memory_satisfies_global_initializer s.mem) program.global_initializers;
             assert (memory_satisfies_global_initializer s.mem initializer);
             storage_satisfies_initializer_implies_gvars_unaddressed vs initializer storage)
    | RootStackVariable pushed popped storage ->
        if pushed then (
          match root_id with
          | RootIdStack tid method_id frame_uniq var_id ->
              let initializer = get_initializer_for_initialized_main_stack_variable s.mem tid method_id frame_uniq
                thread.top.local_variables program.main_stack_initializers var_id in
              storage_satisfies_initializer_implies_gvars_unaddressed vs initializer storage
        )
        else
          ()
    | RootAllocated allocated freed storage -> ()
    | _ -> ()
  )
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

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
/
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 -> program: Armada.Program.t -> s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires
        Armada.Program.init_program program s /\
        Strategies.GlobalVars.global_variables_unaddressed_in_initializers vs
          (Mkt?.global_initializers program) /\
        Strategies.GlobalVars.global_variables_unaddressed_in_initializers vs
          (Mkt?.main_stack_initializers program))
      (ensures Strategies.GlobalVars.global_variables_unaddressed_in_memory vs (Mkt?.mem s))
Prims.list Armada.Base.var_id_t Armada.Program.t Armada.State.t FStar.Classical.Sugar.forall_intro Armada.Base.root_id_t Strategies.GlobalVars.global_variables_unaddressed_in_root Armada.State.__proj__Mkt__item__mem Armada.Memory.valid_object_storage_t Strategies.GlobalVars.Init.storage_satisfies_initializer_implies_gvars_unaddressed Prims.unit Prims._assert Armada.Init.memory_satisfies_global_initializer Util.List.for_all_ubool_equivalent_to_forall Armada.Init.initializer_t Armada.Program.__proj__Mkt__item__global_initializers Prims.l_and Prims.b2t Armada.Init.var_id_in_initializer Spec.List.contains_ubool Util.List.exists_ghost_to_witness Util.List.exists_ghost Prims.squash Prims.bool Armada.Base.tid_t Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Strategies.GlobalVars.Init.get_initializer_for_initialized_main_stack_variable Armada.Thread.__proj__Mkstack_frame_t__item__local_variables Armada.Thread.__proj__Mkt__item__top Armada.Program.__proj__Mkt__item__main_stack_initializers Armada.Memory.root_t Armada.Init.root_invalid_outside_initializations Armada.State.__proj__Mkt__item__initial_tid Armada.Program.__proj__Mkt__item__main_method_id Prims.__proj__Cons__item__hd Armada.State.__proj__Mkt__item__uniqs_used Armada.Thread.t Armada.State.__proj__Mkt__item__threads Armada.Program.init_program Strategies.GlobalVars.global_variables_unaddressed_in_initializers Strategies.GlobalVars.global_variables_unaddressed_in_memory Prims.Nil FStar.Pervasives.pattern
let init_implies_global_variables_unaddressed_in_memory
      (vs: list var_id_t)
      (program: Armada.Program.t)
      (s: Armada.State.t)
    : Lemma
      (requires
        init_program program s /\
        global_variables_unaddressed_in_initializers vs program.global_initializers /\
        global_variables_unaddressed_in_initializers vs program.main_stack_initializers)
      (ensures global_variables_unaddressed_in_memory vs s.mem) =
  
introduce forall root_id . global_variables_unaddressed_in_root vs (s.mem root_id)
with (let thread = s.threads s.initial_tid in
  let initial_frame_uniq = Cons?.hd s.uniqs_used in
  let root = s.mem root_id in
  assert (root_invalid_outside_initializations s.mem
        program.global_initializers
        s.initial_tid
        program.main_method_id
        initial_frame_uniq
        thread.top.local_variables
        root_id);
  match root with
  | RootGlobal storage ->
    (match root_id with
      | RootIdGlobal var_id ->
        assert (exists_ghost (var_id_in_initializer var_id) program.global_initializers);
        let initializer =
          exists_ghost_to_witness (var_id_in_initializer var_id) program.global_initializers
        in
        for_all_ubool_equivalent_to_forall (memory_satisfies_global_initializer s.mem)
          program.global_initializers;
        assert (memory_satisfies_global_initializer s.mem initializer);
        storage_satisfies_initializer_implies_gvars_unaddressed vs initializer storage)
  | RootStackVariable pushed popped storage ->
    if pushed
    then
      (match root_id with
        | RootIdStack tid method_id frame_uniq var_id ->
          let initializer =
            get_initializer_for_initialized_main_stack_variable s.mem
              tid
              method_id
              frame_uniq
              thread.top.local_variables
              program.main_stack_initializers
              var_id
          in
          storage_satisfies_initializer_implies_gvars_unaddressed vs initializer storage)
  | RootAllocated allocated freed storage -> ()
  | _ -> ())