val initializers_match_except_global_variables_implies_matching_linits_are_present
      (vs: list var_id_t)
      (which_are_intros: list bool)
      (linits hinits: list initializer_t)
      (lmem: Armada.Memory.t)
    : Lemma
      (requires
        memory_satisfies_global_initializers lmem linits /\
        initializers_match_except_global_variables vs which_are_intros linits hinits)
      (ensures matching_linits_are_present which_are_intros linits hinits lmem)
val initializers_match_except_global_variables_implies_matching_linits_are_present
      (vs: list var_id_t)
      (which_are_intros: list bool)
      (linits hinits: list initializer_t)
      (lmem: Armada.Memory.t)
    : Lemma
      (requires
        memory_satisfies_global_initializers lmem linits /\
        initializers_match_except_global_variables vs which_are_intros linits hinits)
      (ensures matching_linits_are_present which_are_intros linits hinits lmem)
let rec initializers_match_except_global_variables_implies_matching_linits_are_present
  (vs: list var_id_t)
  (which_are_intros: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : Lemma (requires   memory_satisfies_global_initializers lmem linits
                    /\ initializers_match_except_global_variables vs which_are_intros linits hinits)
          (ensures  matching_linits_are_present which_are_intros linits hinits lmem) =
  match which_are_intros, linits, hinits with
  | [], [], [] -> ()
  | true :: remaining_which_are_intros, _, first_hinit :: remaining_hinits ->
      initializers_match_except_global_variables_implies_matching_linits_are_present vs remaining_which_are_intros
        linits remaining_hinits lmem
  | false :: remaining_which_are_intros, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      initializers_match_except_global_variables_implies_matching_linits_are_present vs remaining_which_are_intros
        remaining_linits remaining_hinits lmem
  | _, _, _ -> ()
module Strategies.VarIntro.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.Statement
open Strategies.GlobalVars.Types
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.VarIntro
open Strategies.Lift.Generic
open Strategies.Invariant
open Strategies.VarIntro.Defs
open Util.List

let apply_introduced_initializer_ensures_satisfies_global_initializer
  (init: initializer_t)
  (existing_inits: list initializer_t)
  (mem: Armada.Memory.t)
  : Lemma (requires    memory_satisfies_global_initializers mem existing_inits
                    /\ (forall existing_init. contains_ubool existing_init existing_inits ==>
                         initializers_match_if_same_variable_id existing_init init)
                    /\ initializer_ok_for_var_intro init)
          (ensures  (let mem' = apply_introduced_initializer init mem in
                       memory_satisfies_global_initializer mem' init
                     /\ memory_satisfies_global_initializers mem' existing_inits)) =
  ()

let apply_introduced_initializer_makes_memories_match
  (vs: list var_id_t)
  (init: initializer_t)
  (mem: Armada.Memory.t)
  : Lemma (requires   list_contains init.var_id vs
                    /\ initializer_ok_for_var_intro init)
          (ensures  memories_match_except_global_variables vs mem (apply_introduced_initializer init mem)) =
  ()

let initializers_with_same_variable_id_match_equivalent_to_forall
  (inits: list initializer_t)
  (* see .fsti file for spec *) =
  ()

let rec apply_introduced_initializers_ensures_satisfies_global_initializers_helper
  (vs: list var_id_t)
  (which_are_intros: list bool)
  (all_linits: list initializer_t)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : Lemma (requires   initializers_match_except_global_variables vs which_are_intros linits hinits
                    /\ initializers_with_same_variable_id_match hinits
                    /\ memory_satisfies_global_initializers lmem all_linits
                    /\ (forall init. contains_ubool init linits ==> contains_ubool init all_linits)
                    /\ (forall linit hinit. contains_ubool linit all_linits /\ contains_ubool hinit hinits ==>
                                      initializers_match_if_same_variable_id linit hinit))
          (ensures  (let hmem = apply_introduced_initializers which_are_intros hinits lmem in
                       memory_satisfies_global_initializers hmem hinits
                     /\ memory_satisfies_global_initializers hmem all_linits
                     /\ memories_match_except_global_variables vs lmem hmem)) =
  let hmem = apply_introduced_initializers which_are_intros hinits lmem in
  match which_are_intros, linits, hinits with
  | [], _, _ -> ()
  | true :: remaining_which_are_intros, _, first_hinit :: remaining_hinits ->
      let mem' = apply_introduced_initializers remaining_which_are_intros remaining_hinits lmem in
      apply_introduced_initializers_ensures_satisfies_global_initializers_helper vs remaining_which_are_intros
        all_linits linits remaining_hinits lmem;
      apply_introduced_initializer_ensures_satisfies_global_initializer first_hinit remaining_hinits mem';
      apply_introduced_initializer_ensures_satisfies_global_initializer first_hinit all_linits mem';
      memories_match_except_global_variables_transitive vs lmem mem' hmem
  | false :: remaining_which_are_intros, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      apply_introduced_initializers_ensures_satisfies_global_initializers_helper vs remaining_which_are_intros
        all_linits remaining_linits remaining_hinits lmem
  | _, _, _ -> ()

let rec initializers_match_except_global_variables_implies_subset_helper
  (vs: list var_id_t)
  (which_are_intros: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (linit: initializer_t)
  : Lemma (requires   initializers_match_except_global_variables vs which_are_intros linits hinits
                    /\ contains_ubool linit linits)
          (ensures  contains_ubool linit hinits) =
  match which_are_intros, linits, hinits with
  | [], _, _ -> ()
  | true :: remaining_which_are_intros, _, first_hinit :: remaining_hinits ->
      initializers_match_except_global_variables_implies_subset_helper vs remaining_which_are_intros linits
        remaining_hinits linit
  | false :: remaining_which_are_intros, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      if eqb first_linit linit then
        ()
      else
        initializers_match_except_global_variables_implies_subset_helper vs remaining_which_are_intros
          remaining_linits remaining_hinits linit
  | _, _, _ -> ()

let initializers_match_except_global_variables_implies_subset
  (vs: list var_id_t)
  (which_are_intros: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  : Lemma (requires initializers_match_except_global_variables vs which_are_intros linits hinits)
          (ensures  forall linit. contains_ubool linit linits ==> contains_ubool linit hinits) =
  introduce forall linit. contains_ubool linit linits ==> contains_ubool linit hinits
  with introduce _ ==> _
  with _. initializers_match_except_global_variables_implies_subset_helper vs which_are_intros linits hinits linit

let apply_introduced_initializers_ensures_satisfies_global_initializers
  (vs: list var_id_t)
  (which_are_intros: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  (* see .fsti file for spec *) =
  initializers_match_except_global_variables_implies_subset vs which_are_intros linits hinits;
  apply_introduced_initializers_ensures_satisfies_global_initializers_helper vs which_are_intros linits
    linits hinits lmem

let rec apply_introduced_initializers_maintains_nonglobal_root
  (which_are_intros: list bool)
  (inits: list initializer_t)
  (lmem: Armada.Memory.t)
  (root_id: root_id_t)
  : Lemma (requires not (RootIdGlobal? root_id))
          (ensures  (let hmem = apply_introduced_initializers which_are_intros inits lmem in
                     hmem root_id == lmem root_id)) =
  match which_are_intros, inits with
  | [], _ -> ()
  | true :: remaining_which_are_intros, first_hinit :: remaining_inits ->
      apply_introduced_initializers_maintains_nonglobal_root remaining_which_are_intros remaining_inits lmem root_id
  | false :: remaining_which_are_intros, first_hinit :: remaining_inits ->
      apply_introduced_initializers_maintains_nonglobal_root remaining_which_are_intros remaining_inits lmem root_id
  | _, _ -> ()

let rec apply_introduced_initializers_ensures_satisfies_main_stack_initializers
  (vs: list var_id_t)
  (which_are_intros: list bool)
  (hinits: list initializer_t)
  (initial_tid: tid_t)
  (main_method_id: method_id_t)
  (initial_frame_uniq: root_id_uniquifier_t)
  (local_variables: list var_id_t)
  (main_stack_initializers: list initializer_t)
  (lmem: Armada.Memory.t)
  (* see .fsti file for spec *) =
  match local_variables, main_stack_initializers with
  | [], [] -> ()
  | var_id :: remaining_var_ids, initializer :: remaining_initializers ->
      let root_id = RootIdStack initial_tid main_method_id initial_frame_uniq var_id in
      apply_introduced_initializers_maintains_nonglobal_root which_are_intros hinits lmem root_id;
      apply_introduced_initializers_ensures_satisfies_main_stack_initializers vs which_are_intros hinits
        initial_tid main_method_id initial_frame_uniq remaining_var_ids remaining_initializers lmem
  | _ -> ()

let rec matching_linits_are_present
  (which_are_intros: list bool)
  (linits: list initializer_t)
  (hinits: list initializer_t)
  (lmem: Armada.Memory.t)
  : GTot bool =
  match which_are_intros, linits, hinits with
  | [], [], [] -> true
  | true :: remaining_which_are_intros, _, first_hinit :: remaining_hinits ->
      matching_linits_are_present remaining_which_are_intros linits remaining_hinits lmem
  | false :: remaining_which_are_intros, first_linit :: remaining_linits, first_hinit :: remaining_hinits ->
      (match lmem (RootIdGlobal first_linit.var_id) with
       | RootGlobal _ -> exists_ghost (var_id_in_initializer first_linit.var_id) linits
       | _ -> false)
  | _, _, _ -> false
/
Util.List.fst.checked Strategies.VarIntro.Defs.fst.checked Strategies.Lift.Generic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.Statement.fsti.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.VarIntro.Initialization.fst

    vs: Prims.list Armada.Base.var_id_t ->
    which_are_intros: Prims.list Prims.bool ->
    linits: Prims.list Armada.Init.initializer_t ->
    hinits: Prims.list Armada.Init.initializer_t ->
    lmem: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Armada.Init.memory_satisfies_global_initializers lmem linits /\
        Strategies.VarIntro.Defs.initializers_match_except_global_variables vs
          which_are_intros
          linits
          hinits)
      (ensures
        Strategies.VarIntro.Initialization.matching_linits_are_present which_are_intros
          linits
          hinits
          lmem)
Prims.list Armada.Base.var_id_t Prims.bool Armada.Init.initializer_t Armada.Memory.t FStar.Pervasives.Native.Mktuple3 Strategies.VarIntro.Initialization.initializers_match_except_global_variables_implies_matching_linits_are_present Prims.unit Prims.l_and Armada.Init.memory_satisfies_global_initializers Strategies.VarIntro.Defs.initializers_match_except_global_variables Prims.squash Prims.b2t Strategies.VarIntro.Initialization.matching_linits_are_present Prims.Nil FStar.Pervasives.pattern
let rec initializers_match_except_global_variables_implies_matching_linits_are_present
      (vs: list var_id_t)
      (which_are_intros: list bool)
      (linits hinits: list initializer_t)
      (lmem: Armada.Memory.t)
    : Lemma
      (requires
        memory_satisfies_global_initializers lmem linits /\
        initializers_match_except_global_variables vs which_are_intros linits hinits)
      (ensures matching_linits_are_present which_are_intros linits hinits lmem) =
  
match which_are_intros, linits, hinits with
| [], [], [] -> ()
| true :: remaining_which_are_intros, _, first_hinit :: remaining_hinits ->
  initializers_match_except_global_variables_implies_matching_linits_are_present vs
    remaining_which_are_intros
    linits
    remaining_hinits
    lmem
| false :: remaining_which_are_intros,
first_linit :: remaining_linits,
first_hinit :: remaining_hinits ->
  initializers_match_except_global_variables_implies_matching_linits_are_present vs
    remaining_which_are_intros
    remaining_linits
    remaining_hinits
    lmem
| _, _, _ -> ()