val transform_special_case_proof
      (inv: invariant_t Armada.State.t)
      (atomic_action: list Armada.Action.t)
      (special_case_proof:
          (
                actor: tid_t ->
                starts_atomic_block: bool ->
                ends_atomic_block: bool ->
                atomic_step: list Armada.Step.t ->
                s:
                  Armada.State.t
                    { map_ghost armada_step_to_action atomic_step == atomic_action /\ inv s /\
                      Some? (steps_computation actor
                            starts_atomic_block
                            ends_atomic_block
                            atomic_step
                            s) }
              -> squash (inv (Some?.v (steps_computation actor
                              starts_atomic_block
                              ends_atomic_block
                              atomic_step
                              s)))))
    : GTot
    (
          actor: armada_semantics.actor_t ->
          starts_atomic_block: bool ->
          ends_atomic_block: bool ->
          atomic_step: list armada_semantics.step_t ->
          s:
            armada_semantics.state_t
              { map_ghost armada_semantics.step_to_action_f atomic_step == atomic_action /\ inv s /\
                Some? (steps_computation_generic armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s) }
        -> squash (inv (Some?.v (steps_computation_generic armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        atomic_step
                        s))))
val transform_special_case_proof
      (inv: invariant_t Armada.State.t)
      (atomic_action: list Armada.Action.t)
      (special_case_proof:
          (
                actor: tid_t ->
                starts_atomic_block: bool ->
                ends_atomic_block: bool ->
                atomic_step: list Armada.Step.t ->
                s:
                  Armada.State.t
                    { map_ghost armada_step_to_action atomic_step == atomic_action /\ inv s /\
                      Some? (steps_computation actor
                            starts_atomic_block
                            ends_atomic_block
                            atomic_step
                            s) }
              -> squash (inv (Some?.v (steps_computation actor
                              starts_atomic_block
                              ends_atomic_block
                              atomic_step
                              s)))))
    : GTot
    (
          actor: armada_semantics.actor_t ->
          starts_atomic_block: bool ->
          ends_atomic_block: bool ->
          atomic_step: list armada_semantics.step_t ->
          s:
            armada_semantics.state_t
              { map_ghost armada_semantics.step_to_action_f atomic_step == atomic_action /\ inv s /\
                Some? (steps_computation_generic armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s) }
        -> squash (inv (Some?.v (steps_computation_generic armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        atomic_step
                        s))))
let transform_special_case_proof
  (inv: invariant_t Armada.State.t)
  (atomic_action: list Armada.Action.t)
  (special_case_proof:
     ((actor: tid_t) ->
      (starts_atomic_block: bool) ->
      (ends_atomic_block: bool) ->
      (atomic_step: list Armada.Step.t) ->
      (s: Armada.State.t{
          map_ghost armada_step_to_action atomic_step == atomic_action
        /\ inv s
        /\ Some? (steps_computation actor starts_atomic_block ends_atomic_block atomic_step s)}) ->
      squash (inv (Some?.v (steps_computation actor starts_atomic_block ends_atomic_block atomic_step s)))))
  : GTot ((actor: armada_semantics.actor_t) ->
          (starts_atomic_block: bool) ->
          (ends_atomic_block: bool) ->
          (atomic_step: list armada_semantics.step_t) ->
          (s: armada_semantics.state_t{
              map_ghost armada_semantics.step_to_action_f atomic_step == atomic_action
            /\ inv s
            /\ Some? (steps_computation_generic armada_semantics actor starts_atomic_block
                       ends_atomic_block atomic_step s)}) ->
          squash (inv (Some?.v (steps_computation_generic armada_semantics actor starts_atomic_block
                                  ends_atomic_block atomic_step s)))) =
  fun actor starts_atomic_block ends_atomic_block atomic_step s -> (
    armada_steps_computation_equivalent actor starts_atomic_block ends_atomic_block atomic_step s;
    special_case_proof actor starts_atomic_block ends_atomic_block atomic_step s
  )
module Strategies.Invariant.Armada.Atomic

open FStar.List.Tot
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant.Armada
open Strategies.Invariant.Atomic
open Util.List

noeq type armada_atomic_semantics_invariant_proof_t = {
  program: program_t (make_atomic_semantics armada_semantics);
  inv: invariant_t Armada.State.t;
  action_pred: Armada.Action.t -> GTot ubool;
  special_case_proofs: list (option (armada_atomic_special_case_invariant_proof_t inv));
  init_implies_inv_proof: (s: Armada.State.t{program.init_f s}) -> squash (inv s);
  action_proof: armada_action_maintains_invariant_proof_t inv action_pred;
  special_cases_apply_proof: unit ->
     squash (armada_atomic_special_cases_apply inv action_pred program.actions special_case_proofs);
}
/
Util.List.fst.checked Strategies.Invariant.Atomic.fsti.checked Strategies.Invariant.Armada.fsti.checked Strategies.Atomic.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Action.fst.checked
Strategies.Invariant.Armada.Atomic.fst

    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    atomic_action: Prims.list Armada.Action.t ->
    special_case_proof:
      (
            actor: Armada.Base.tid_t ->
            starts_atomic_block: Prims.bool ->
            ends_atomic_block: Prims.bool ->
            atomic_step: Prims.list Armada.Step.t ->
            s:
              Armada.State.t
                { Util.List.map_ghost Strategies.Semantics.Armada.armada_step_to_action atomic_step ==
                  atomic_action /\ inv s /\
                  Some? (Armada.Transition.steps_computation actor
                        starts_atomic_block
                        ends_atomic_block
                        atomic_step
                        s) }
          -> Prims.squash (inv (Some?.v (Armada.Transition.steps_computation actor
                          starts_atomic_block
                          ends_atomic_block
                          atomic_step
                          s))))
  -> Prims.GTot
    (
          actor: Mksemantics_t?.actor_t Strategies.Semantics.Armada.armada_semantics ->
          starts_atomic_block: Prims.bool ->
          ends_atomic_block: Prims.bool ->
          atomic_step:
            Prims.list (Mksemantics_t?.step_t Strategies.Semantics.Armada.armada_semantics) ->
          s:
            Mksemantics_t?.state_t Strategies.Semantics.Armada.armada_semantics
              { Util.List.map_ghost (Mksemantics_t?.step_to_action_f Strategies.Semantics.Armada.armada_semantics
                    )
                  atomic_step ==
                atomic_action /\ inv s /\
                Some? (Strategies.Semantics.steps_computation_generic Strategies.Semantics.Armada.armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s) }
        -> Prims.squash (inv (Some?.v (Strategies.Semantics.steps_computation_generic Strategies.Semantics.Armada.armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        atomic_step
                        s))))
Strategies.Invariant.invariant_t Armada.State.t Prims.list Armada.Action.t Armada.Base.tid_t Prims.bool Armada.Step.t Prims.l_and Prims.eq2 Util.List.map_ghost Strategies.Semantics.Armada.armada_step_to_action Prims.b2t FStar.Pervasives.Native.uu___is_Some Armada.Transition.steps_computation Prims.squash FStar.Pervasives.Native.__proj__Some__item__v Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Strategies.Semantics.Armada.armada_semantics Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.Semantics.__proj__Mksemantics_t__item__step_to_action_f Strategies.Semantics.steps_computation_generic Prims.unit Strategies.Semantics.Armada.armada_steps_computation_equivalent
let transform_special_case_proof
      (inv: invariant_t Armada.State.t)
      (atomic_action: list Armada.Action.t)
      (special_case_proof:
          (
                actor: tid_t ->
                starts_atomic_block: bool ->
                ends_atomic_block: bool ->
                atomic_step: list Armada.Step.t ->
                s:
                  Armada.State.t
                    { map_ghost armada_step_to_action atomic_step == atomic_action /\ inv s /\
                      Some? (steps_computation actor
                            starts_atomic_block
                            ends_atomic_block
                            atomic_step
                            s) }
              -> squash (inv (Some?.v (steps_computation actor
                              starts_atomic_block
                              ends_atomic_block
                              atomic_step
                              s)))))
    : GTot
    (
          actor: armada_semantics.actor_t ->
          starts_atomic_block: bool ->
          ends_atomic_block: bool ->
          atomic_step: list armada_semantics.step_t ->
          s:
            armada_semantics.state_t
              { map_ghost armada_semantics.step_to_action_f atomic_step == atomic_action /\ inv s /\
                Some? (steps_computation_generic armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s) }
        -> squash (inv (Some?.v (steps_computation_generic armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        atomic_step
                        s)))) =
  
fun actor starts_atomic_block ends_atomic_block atomic_step s ->
  (armada_steps_computation_equivalent actor starts_atomic_block ends_atomic_block atomic_step s;
    special_case_proof actor starts_atomic_block ends_atomic_block atomic_step s)