val atomic_lprog_init_establishes_inductive_my_inv
      (s:
          Armada.State.t
            {(semantics_to_spec (make_atomic_semantics armada_semantics) MyAtomicLProg.prog).init s}
        )
    : squash (inductive_my_inv s)
val atomic_lprog_init_establishes_inductive_my_inv
      (s:
          Armada.State.t
            {(semantics_to_spec (make_atomic_semantics armada_semantics) MyAtomicLProg.prog).init s}
        )
    : squash (inductive_my_inv s)
let atomic_lprog_init_establishes_inductive_my_inv
  (s: Armada.State.t{(semantics_to_spec (make_atomic_semantics armada_semantics) MyAtomicLProg.prog).init s})
  : squash (inductive_my_inv s) =
  let initializer5: initializer_t =
    { var_id = "f"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false; } in
  assert (contains_ubool initializer5 MyLProg.prog.global_initializers)
    by FStar.Tactics.V2.norm [delta];
  assert (global_variables_unaddressed_in_initializers vs MyLProg.prog.global_initializers)
    by (FStar.Tactics.V2.compute (); FStar.Tactics.V2.trivial ());
  init_implies_global_variables_unaddressed_in_memory vs MyLProg.prog s;
  assert (global_variables_unaddressed_in_memory vs s.mem)
module GlobalVarExampleInvariant

open Armada.Action
open Armada.Base
open Armada.BinaryOp
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Spec.List
open Spec.Ubool
open Util.List

open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVarsProof
open Strategies.GlobalVars.UnaddressedStatement

let vs = ["f"]

let my_inv (s: Armada.State.t) : GTot ubool =
  let root_one: root_t = RootGlobal (ObjectStorageAbstract int 1) in
    s.mem (RootIdGlobal "f") == root_one

private let my_action_pred (action: Armada.Action.t) : GTot ubool =
      (not action.ok)
    \/ (  global_variables_unmodifiable_by_statement vs action.program_statement.statement
       /\ global_variables_unaddressable_in_statement vs action.program_statement.statement)

private let inductive_inv (s: Armada.State.t) : GTot ubool =
    roots_match s.mem
  /\ positions_valid_in_state s
  /\ global_variables_unaddressed_in_memory vs s.mem

private let inductive_my_inv (s: Armada.State.t) : GTot ubool =
  inductive_inv s /\ my_inv s

private let step_relation (s s': Armada.State.t): GTot ubool =
  states_match_on_global_variables vs s s'

private let step_relation_preserves_my_inv (s s': Armada.State.t)
  : Lemma (requires my_inv s /\ step_relation s s')
          (ensures  my_inv s') =
  ()

#push-options "--z3rlimit 10 --z3cliopt smt.qi.eager_threshold=100"
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.Atomic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVarsProof.fst.checked Strategies.GlobalVars.UnaddressedStatement.fst.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyLProg.fst.checked MyAtomicLProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
GlobalVarExampleInvariant.fst

    s:
      Armada.State.t
        { Mkspec_t?.init (Strategies.Semantics.semantics_to_spec (Strategies.Atomic.make_atomic_semantics
                    Strategies.Semantics.Armada.armada_semantics)
                MyAtomicLProg.prog)
            s }
  -> Prims.squash (GlobalVarExampleInvariant.inductive_my_inv s)
Armada.State.t Spec.Behavior.__proj__Mkspec_t__item__init Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.Semantics.semantics_to_spec MyAtomicLProg.prog Prims._assert Strategies.GlobalVars.global_variables_unaddressed_in_memory GlobalVarExampleInvariant.vs Armada.State.__proj__Mkt__item__mem Prims.unit Strategies.GlobalVars.Init.init_implies_global_variables_unaddressed_in_memory MyLProg.prog FStar.Tactics.Effect.assert_by_tactic Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_initializers Armada.Program.__proj__Mkt__item__global_initializers FStar.Tactics.V2.Derived.trivial FStar.Tactics.V2.Derived.compute Spec.List.contains_ubool Armada.Init.initializer_t FStar.Stubs.Tactics.V2.Builtins.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta Prims.Nil Armada.Init.Mkinitializer_t Armada.Init.InitializerSpecific Armada.Type.ObjectValueAbstract Prims.int Prims.squash GlobalVarExampleInvariant.inductive_my_inv
let atomic_lprog_init_establishes_inductive_my_inv
      (s:
          Armada.State.t
            {(semantics_to_spec (make_atomic_semantics armada_semantics) MyAtomicLProg.prog).init s}
        )
    : squash (inductive_my_inv s) =
  
let initializer5:initializer_t =
  { var_id = "f"; iv = InitializerSpecific (ObjectValueAbstract int 1); weakly_consistent = false }
in
FStar.Tactics.Effect.assert_by_tactic (contains_ubool initializer5 MyLProg.prog.global_initializers)
  (fun _ ->
      ();
      FStar.Tactics.V2.norm [delta]);
FStar.Tactics.Effect.assert_by_tactic (global_variables_unaddressed_in_initializers vs
      MyLProg.prog.global_initializers)
  (fun _ ->
      ();
      (FStar.Tactics.V2.compute ();
        FStar.Tactics.V2.trivial ()));
init_implies_global_variables_unaddressed_in_memory vs MyLProg.prog s;
assert (global_variables_unaddressed_in_memory vs s.mem)