val apply_introduced_initializers_ensures_satisfies_global_initializers_helper
      (vs: list var_id_t)
      (which_are_intros: list bool)
      (all_linits linits 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))
val apply_introduced_initializers_ensures_satisfies_global_initializers_helper
      (vs: list var_id_t)
      (which_are_intros: list bool)
      (all_linits linits 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 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
  | _, _, _ -> ()
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 *) =
  ()
/
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 ->
    all_linits: Prims.list Armada.Init.initializer_t ->
    linits: Prims.list Armada.Init.initializer_t ->
    hinits: Prims.list Armada.Init.initializer_t ->
    lmem: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarIntro.Defs.initializers_match_except_global_variables vs
          which_are_intros
          linits
          hinits /\ Strategies.VarIntro.Defs.initializers_with_same_variable_id_match hinits /\
        Armada.Init.memory_satisfies_global_initializers lmem all_linits /\
        (forall (init: Armada.Init.initializer_t).
            Spec.List.contains_ubool init linits ==> Spec.List.contains_ubool init all_linits) /\
        (forall (linit: Armada.Init.initializer_t) (hinit: Armada.Init.initializer_t).
            Spec.List.contains_ubool linit all_linits /\ Spec.List.contains_ubool hinit hinits ==>
            Strategies.VarIntro.Defs.initializers_match_if_same_variable_id linit hinit))
      (ensures
        (let hmem =
            Strategies.VarIntro.Initialization.apply_introduced_initializers which_are_intros
              hinits
              lmem
          in
          Armada.Init.memory_satisfies_global_initializers hmem hinits /\
          Armada.Init.memory_satisfies_global_initializers hmem all_linits /\
          Strategies.GlobalVars.memories_match_except_global_variables vs lmem hmem))
Prims.list Armada.Base.var_id_t Prims.bool Armada.Init.initializer_t Armada.Memory.t FStar.Pervasives.Native.Mktuple3 Strategies.GlobalVars.Util.memories_match_except_global_variables_transitive Prims.unit Strategies.VarIntro.Initialization.apply_introduced_initializer_ensures_satisfies_global_initializer Strategies.VarIntro.Initialization.apply_introduced_initializers_ensures_satisfies_global_initializers_helper Strategies.VarIntro.Initialization.apply_introduced_initializers Prims.l_and Strategies.VarIntro.Defs.initializers_match_except_global_variables Strategies.VarIntro.Defs.initializers_with_same_variable_id_match Armada.Init.memory_satisfies_global_initializers Prims.l_Forall Prims.l_imp Spec.List.contains_ubool Strategies.VarIntro.Defs.initializers_match_if_same_variable_id Prims.squash Strategies.GlobalVars.memories_match_except_global_variables Prims.Nil FStar.Pervasives.pattern
let rec apply_introduced_initializers_ensures_satisfies_global_initializers_helper
      (vs: list var_id_t)
      (which_are_intros: list bool)
      (all_linits linits 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
| _, _, _ -> ()