val atomic_special_cases_apply : sem: Strategies.Semantics.semantics_t ->
    inv: Strategies.Invariant.invariant_t (Mksemantics_t?.state_t sem) ->
    action_pred: (_: Mksemantics_t?.action_t sem -> Prims.GTot Spec.Ubool.ubool) ->
    atomic_actions: Prims.list (Prims.list (Mksemantics_t?.action_t sem)) ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t
                sem
                inv))
  -> Spec.Ubool.ubool
let atomic_special_cases_apply
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (action_pred: sem.action_t -> GTot ubool)
  (atomic_actions: list (list sem.action_t))
  (special_case_proofs: (list (option (atomic_special_case_invariant_proof_t sem inv)))) =
  lists_correspond_ubool (atomic_proof_option_applies sem inv action_pred) atomic_actions special_case_proofs
module Strategies.Invariant.Atomic

open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Semantics
open Strategies.Invariant
open Util.List

/// Proving invariants of atomic programs

noeq type atomic_special_case_invariant_proof_t (sem: semantics_t) (inv: invariant_t sem.state_t) =
  | AtomicSpecialCaseInvariantProof :
     (atomic_action: list sem.action_t) ->
     (special_case_proof:
       ((actor: sem.actor_t) ->
        (starts_atomic_block: bool) ->
        (ends_atomic_block: bool) ->
        (atomic_step: list sem.step_t) ->
        (s: sem.state_t{
            map_ghost sem.step_to_action_f atomic_step == atomic_action
          /\ inv s
          /\ Some? (steps_computation_generic sem actor starts_atomic_block ends_atomic_block atomic_step s)}) ->
        squash (inv (Some?.v (steps_computation_generic sem actor starts_atomic_block
                                ends_atomic_block atomic_step s))))) ->
  atomic_special_case_invariant_proof_t sem inv

let atomic_proof_option_applies
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (action_pred: sem.action_t -> GTot ubool)
  (atomic_action: list sem.action_t)
  (proof_option: option (atomic_special_case_invariant_proof_t sem inv))
  : GTot ubool =
  match proof_option with
  | None -> for_all_ubool action_pred atomic_action
  | Some prf -> eqb prf.atomic_action atomic_action
/
Util.List.fst.checked Strategies.Semantics.fst.checked Strategies.Invariant.fsti.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Strategies.Invariant.Atomic.fsti

    sem: Strategies.Semantics.semantics_t ->
    inv: Strategies.Invariant.invariant_t (Mksemantics_t?.state_t sem) ->
    action_pred: (_: Mksemantics_t?.action_t sem -> Prims.GTot Spec.Ubool.ubool) ->
    atomic_actions: Prims.list (Prims.list (Mksemantics_t?.action_t sem)) ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t
                sem
                inv))
  -> Spec.Ubool.ubool
Strategies.Semantics.semantics_t Strategies.Invariant.invariant_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.__proj__Mksemantics_t__item__action_t Spec.Ubool.ubool Prims.list FStar.Pervasives.Native.option Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t Util.List.lists_correspond_ubool Strategies.Invariant.Atomic.atomic_proof_option_applies
let atomic_special_cases_apply
      (sem: semantics_t)
      (inv: invariant_t sem.state_t)
      (action_pred: (sem.action_t -> GTot ubool))
      (atomic_actions: list (list sem.action_t))
      (special_case_proofs: (list (option (atomic_special_case_invariant_proof_t sem inv))))
     =
  
lists_correspond_ubool (atomic_proof_option_applies sem inv action_pred)
  atomic_actions
  special_case_proofs