val my_action_pred_preserves_inductive_my_inv_proof
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s: Armada.State.t)
    : Lemma
      (requires
        Some? (step_computation actor starts_atomic_block ends_atomic_block step s) /\
        my_action_pred step.action /\ inductive_my_inv s)
      (ensures
        inductive_my_inv (Some?.v (step_computation actor
                  starts_atomic_block
                  ends_atomic_block
                  step
                  s)))
val my_action_pred_preserves_inductive_my_inv_proof
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s: Armada.State.t)
    : Lemma
      (requires
        Some? (step_computation actor starts_atomic_block ends_atomic_block step s) /\
        my_action_pred step.action /\ inductive_my_inv s)
      (ensures
        inductive_my_inv (Some?.v (step_computation actor
                  starts_atomic_block
                  ends_atomic_block
                  step
                  s)))
let my_action_pred_preserves_inductive_my_inv_proof
  (actor: tid_t)
  (starts_atomic_block ends_atomic_block: bool)
  (step: Armada.Step.t)
  (s: Armada.State.t)
  : Lemma (requires   Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
                    /\ my_action_pred step.action
                    /\ inductive_my_inv s)
          (ensures    inductive_my_inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)))
  = executing_statement_maintains_roots_match actor step.nd ((s.threads actor).pc) step.action.program_statement.end_pc step.action.program_statement.statement s;
    executing_statement_maintains_positions_valid_in_state actor step.nd ((s.threads actor).pc) step.action.program_statement.end_pc step.action.program_statement.statement s;
    if (step.action.ok) then begin
      global_variables_unaddressable_by_statement_global_vars_unaddressed_in_state vs actor step starts_atomic_block ends_atomic_block s;
      global_variables_unmodifiable_by_statement_memories_matches_on_global_variables vs actor step starts_atomic_block ends_atomic_block s;
      step_relation_preserves_my_inv s (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s))
    end
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"

private 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)

#pop-options
/
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

    actor: Armada.Base.tid_t ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    step: Armada.Step.t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires
        Some? (Armada.Transition.step_computation actor starts_atomic_block ends_atomic_block step s
          ) /\ GlobalVarExampleInvariant.my_action_pred (Mkt?.action step) /\
        GlobalVarExampleInvariant.inductive_my_inv s)
      (ensures
        GlobalVarExampleInvariant.inductive_my_inv (Some?.v (Armada.Transition.step_computation actor
                  starts_atomic_block
                  ends_atomic_block
                  step
                  s)))
Armada.Base.tid_t Prims.bool Armada.Step.t Armada.State.t Armada.Action.__proj__Mkt__item__ok Armada.Step.__proj__Mkt__item__action GlobalVarExampleInvariant.step_relation_preserves_my_inv FStar.Pervasives.Native.__proj__Some__item__v Armada.Transition.step_computation Prims.unit Strategies.GlobalVarsProof.global_variables_unmodifiable_by_statement_memories_matches_on_global_variables GlobalVarExampleInvariant.vs Strategies.GlobalVars.UnaddressedStatement.global_variables_unaddressable_by_statement_global_vars_unaddressed_in_state Strategies.ArmadaInvariant.PositionsValid.executing_statement_maintains_positions_valid_in_state Armada.Step.__proj__Mkt__item__nd Armada.Thread.__proj__Mkt__item__pc Armada.State.__proj__Mkt__item__threads Armada.Action.__proj__Mkprogram_statement_t__item__end_pc Armada.Action.__proj__Mkt__item__program_statement Armada.Action.__proj__Mkprogram_statement_t__item__statement Strategies.ArmadaInvariant.RootsMatch.executing_statement_maintains_roots_match Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_Some GlobalVarExampleInvariant.my_action_pred GlobalVarExampleInvariant.inductive_my_inv Prims.squash Prims.Nil FStar.Pervasives.pattern
let my_action_pred_preserves_inductive_my_inv_proof
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s: Armada.State.t)
    : Lemma
      (requires
        Some? (step_computation actor starts_atomic_block ends_atomic_block step s) /\
        my_action_pred step.action /\ inductive_my_inv s)
      (ensures
        inductive_my_inv (Some?.v (step_computation actor
                  starts_atomic_block
                  ends_atomic_block
                  step
                  s))) =
  
executing_statement_maintains_roots_match actor
  step.nd
  ((s.threads actor).pc)
  step.action.program_statement.end_pc
  step.action.program_statement.statement
  s;
executing_statement_maintains_positions_valid_in_state actor
  step.nd
  ((s.threads actor).pc)
  step.action.program_statement.end_pc
  step.action.program_statement.statement
  s;
if (step.action.ok)
then
  (global_variables_unaddressable_by_statement_global_vars_unaddressed_in_state vs
      actor
      step
      starts_atomic_block
      ends_atomic_block
      s;
    global_variables_unmodifiable_by_statement_memories_matches_on_global_variables vs
      actor
      step
      starts_atomic_block
      ends_atomic_block
      s;
    step_relation_preserves_my_inv s
      (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)))