val action_pred_preserves_inv
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s:
          Armada.State.t
            { Some? (step_computation actor starts_atomic_block ends_atomic_block step s) /\
              action_pred step.action /\ inv s })
    : squash (inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)))
val action_pred_preserves_inv
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s:
          Armada.State.t
            { Some? (step_computation actor starts_atomic_block ends_atomic_block step s) /\
              action_pred step.action /\ inv s })
    : squash (inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)))
let action_pred_preserves_inv
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (step: Armada.Step.t)
  (s: Armada.State.t{
      Some? (step_computation actor starts_atomic_block ends_atomic_block step s)
    /\ action_pred step.action
    /\ inv s})
  : squash (inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s))) =
  step_computation_maintains_all_gvars_have_types
    ["a"; "c"; "e"]
    [ObjectTDAbstract int; ObjectTDAbstract int; ObjectTDAbstract int]
    actor starts_atomic_block ends_atomic_block step s
module MyAtomicBInvariant

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.GlobalVars.Types
open Strategies.Invariant
open Strategies.Invariant.Armada
open Strategies.Invariant.Armada.AtomicSubstep
open Strategies.Semantics
open Strategies.Semantics.Armada
open Spec.List
open Spec.Ubool
open Util.List

let inv (s: Armada.State.t) : GTot ubool =
    gvar_has_type s.mem "a" (ObjectTDAbstract int)
  /\ gvar_has_type s.mem "c" (ObjectTDAbstract int)
  /\ gvar_has_type s.mem "e" (ObjectTDAbstract int)

private let action_pred (action: Armada.Action.t) : GTot ubool =
  True

#push-options "--z3rlimit 10 --z3cliopt smt.qi.eager_threshold=100"

private let atomic_bprog_init_establishes_inv
  (s: Armada.State.t{(semantics_to_spec (make_atomic_semantics armada_semantics) MyAtomicBProg.prog).init s})
  : squash (inv s) =
  ()
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.AtomicSubstep.fsti.checked Strategies.Invariant.Armada.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Types.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyAtomicBProg.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
MyAtomicBInvariant.fst

    actor: Armada.Base.tid_t ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    step: Armada.Step.t ->
    s:
      Armada.State.t
        { Some? (Armada.Transition.step_computation actor
                starts_atomic_block
                ends_atomic_block
                step
                s) /\ MyAtomicBInvariant.action_pred (Mkt?.action step) /\ MyAtomicBInvariant.inv s
        }
  -> Prims.squash (MyAtomicBInvariant.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 Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_Some Armada.Transition.step_computation MyAtomicBInvariant.action_pred Armada.Step.__proj__Mkt__item__action MyAtomicBInvariant.inv Strategies.GlobalVars.Types.step_computation_maintains_all_gvars_have_types Prims.Cons Armada.Base.var_id_t Prims.Nil Armada.Type.object_td_t Armada.Type.ObjectTDAbstract Prims.int Prims.squash FStar.Pervasives.Native.__proj__Some__item__v
let action_pred_preserves_inv
      (actor: tid_t)
      (starts_atomic_block ends_atomic_block: bool)
      (step: Armada.Step.t)
      (s:
          Armada.State.t
            { Some? (step_computation actor starts_atomic_block ends_atomic_block step s) /\
              action_pred step.action /\ inv s })
    : squash (inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s))) =
  
step_computation_maintains_all_gvars_have_types ["a"; "c"; "e"]
  [ObjectTDAbstract int; ObjectTDAbstract int; ObjectTDAbstract int]
  actor
  starts_atomic_block
  ends_atomic_block
  step
  s