val transform_special_cases
      (inv: invariant_t Armada.State.t)
      (proofs: list (option (armada_atomic_special_case_invariant_proof_t inv)))
    : GTot (list (option (atomic_special_case_invariant_proof_t armada_semantics inv)))
val transform_special_cases
      (inv: invariant_t Armada.State.t)
      (proofs: list (option (armada_atomic_special_case_invariant_proof_t inv)))
    : GTot (list (option (atomic_special_case_invariant_proof_t armada_semantics inv)))
let transform_special_cases
  (inv: invariant_t Armada.State.t)
  (proofs: list (option (armada_atomic_special_case_invariant_proof_t inv)))
  : GTot (list (option (atomic_special_case_invariant_proof_t armada_semantics inv))) =
  map_ghost (transform_optional_special_case inv) proofs
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);
}

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
  )

let transform_special_case
  (inv: invariant_t Armada.State.t)
  (proof: armada_atomic_special_case_invariant_proof_t inv)
  : GTot (atomic_special_case_invariant_proof_t armada_semantics inv) =
  match proof with
  | ArmadaAtomicSpecialCaseInvariantProof atomic_action special_case_proof ->
      AtomicSpecialCaseInvariantProof atomic_action (transform_special_case_proof inv atomic_action special_case_proof)

let transform_optional_special_case
  (inv: invariant_t Armada.State.t)
  (optional_proof: option (armada_atomic_special_case_invariant_proof_t inv))
  : GTot (option (atomic_special_case_invariant_proof_t armada_semantics inv)) =
  match optional_proof with
  | None -> None
  | Some proof -> Some (transform_special_case inv proof)
/
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 ->
    proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Armada.Atomic.armada_atomic_special_case_invariant_proof_t
                inv))
  -> Prims.GTot
    (Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t
                Strategies.Semantics.Armada.armada_semantics
                inv)))
Strategies.Invariant.invariant_t Armada.State.t Prims.list FStar.Pervasives.Native.option Strategies.Invariant.Armada.Atomic.armada_atomic_special_case_invariant_proof_t Util.List.map_ghost Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t Strategies.Semantics.Armada.armada_semantics Strategies.Invariant.Armada.Atomic.transform_optional_special_case
let transform_special_cases
      (inv: invariant_t Armada.State.t)
      (proofs: list (option (armada_atomic_special_case_invariant_proof_t inv)))
    : GTot (list (option (atomic_special_case_invariant_proof_t armada_semantics inv))) =
  
map_ghost (transform_optional_special_case inv) proofs