val 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)
val 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)
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
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
/
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

    mem: Armada.Memory.t ->
    tid: Armada.Base.tid_t ->
    method_id: Armada.Base.method_id_t ->
    frame_uniq: Armada.Base.root_id_uniquifier_t ->
    var_ids: Prims.list Armada.Base.var_id_t ->
    initializers: Prims.list Armada.Init.initializer_t ->
    var_id: Armada.Base.var_id_t
  -> Prims.Ghost Armada.Init.initializer_t
Armada.Memory.t Armada.Base.tid_t Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Prims.list Armada.Base.var_id_t Armada.Init.initializer_t FStar.Pervasives.Native.Mktuple2 Spec.Ubool.eqb Prims.bool Strategies.GlobalVars.Init.get_initializer_for_initialized_main_stack_variable Prims.l_and Prims.b2t Spec.List.list_contains Armada.Init.memory_satisfies_main_stack_initializers Spec.List.contains_ubool Armada.Init.memory_satisfies_main_stack_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