val next_atomic_step_preserves_inv_case_action_pred
      (asip: atomic_semantics_invariant_proof_t)
      (actor: asip.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (atomic_step: list asip.sem.step_t)
      (s:
          asip.sem.state_t
            { for_all_ubool asip.action_pred (map_ghost asip.sem.step_to_action_f atomic_step) /\
              (asip.inv s) /\
              Some? (steps_computation_generic asip.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    atomic_step
                    s) })
    : GTot
      (squash (asip.inv (Some?.v (steps_computation_generic asip.sem
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s)))) (decreases atomic_step)
val next_atomic_step_preserves_inv_case_action_pred
      (asip: atomic_semantics_invariant_proof_t)
      (actor: asip.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (atomic_step: list asip.sem.step_t)
      (s:
          asip.sem.state_t
            { for_all_ubool asip.action_pred (map_ghost asip.sem.step_to_action_f atomic_step) /\
              (asip.inv s) /\
              Some? (steps_computation_generic asip.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    atomic_step
                    s) })
    : GTot
      (squash (asip.inv (Some?.v (steps_computation_generic asip.sem
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s)))) (decreases atomic_step)
let rec next_atomic_step_preserves_inv_case_action_pred
  (asip: atomic_semantics_invariant_proof_t)
  (actor: asip.sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (atomic_step: list asip.sem.step_t)
  (s: asip.sem.state_t{
      for_all_ubool asip.action_pred (map_ghost asip.sem.step_to_action_f atomic_step)
    /\ (asip.inv s)
    /\ Some? (steps_computation_generic asip.sem actor starts_atomic_block
               ends_atomic_block atomic_step s)})
  : GTot (squash (asip.inv (Some?.v (steps_computation_generic asip.sem actor starts_atomic_block
                                       ends_atomic_block atomic_step s))))
    (decreases atomic_step) =
  match atomic_step with
  | [last_step] -> 
      assert (asip.action_pred (asip.sem.step_to_action_f last_step));
      asip.action_proof actor starts_atomic_block ends_atomic_block last_step s
  | first_step :: remaining_steps ->
      assert (asip.action_pred (asip.sem.step_to_action_f first_step));
      asip.action_proof actor starts_atomic_block false first_step s;
      let s' = Some?.v (step_computation_generic asip.sem actor starts_atomic_block false first_step s) in
      next_atomic_step_preserves_inv_case_action_pred asip actor false ends_atomic_block remaining_steps s'
module Strategies.Invariant.Atomic

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

/// Proving invariants of atomic semantics
/
Util.List.fst.checked Strategies.Invariant.fsti.checked Strategies.Atomic.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Strategies.Invariant.Atomic.fst

    asip: Strategies.Invariant.Atomic.atomic_semantics_invariant_proof_t ->
    actor: Mksemantics_t?.actor_t (Mkatomic_semantics_invariant_proof_t?.sem asip) ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    atomic_step: Prims.list (Mksemantics_t?.step_t (Mkatomic_semantics_invariant_proof_t?.sem asip)) ->
    s:
      Mksemantics_t?.state_t (Mkatomic_semantics_invariant_proof_t?.sem asip)
        { Util.List.for_all_ubool (Mkatomic_semantics_invariant_proof_t?.action_pred asip)
            (Util.List.map_ghost (Mksemantics_t?.step_to_action_f (Mkatomic_semantics_invariant_proof_t?.sem
                        asip))
                atomic_step) /\ Mkatomic_semantics_invariant_proof_t?.inv asip s /\
          Some? (Strategies.Semantics.steps_computation_generic (Mkatomic_semantics_invariant_proof_t?.sem
                    asip)
                actor
                starts_atomic_block
                ends_atomic_block
                atomic_step
                s) }
  -> Prims.GTot
    (Prims.squash (Mkatomic_semantics_invariant_proof_t?.inv asip
            (Some?.v (Strategies.Semantics.steps_computation_generic (Mkatomic_semantics_invariant_proof_t?.sem
                        asip)
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    atomic_step
                    s))))
Strategies.Invariant.Atomic.atomic_semantics_invariant_proof_t Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Strategies.Invariant.Atomic.__proj__Mkatomic_semantics_invariant_proof_t__item__sem Prims.bool Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Prims.l_and Util.List.for_all_ubool Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.Invariant.Atomic.__proj__Mkatomic_semantics_invariant_proof_t__item__action_pred Util.List.map_ghost Strategies.Semantics.__proj__Mksemantics_t__item__step_to_action_f Strategies.Invariant.Atomic.__proj__Mkatomic_semantics_invariant_proof_t__item__inv Prims.b2t FStar.Pervasives.Native.uu___is_Some Strategies.Semantics.steps_computation_generic Strategies.Invariant.Atomic.__proj__Mkatomic_semantics_invariant_proof_t__item__action_proof Prims.unit Prims._assert Strategies.Invariant.Atomic.next_atomic_step_preserves_inv_case_action_pred FStar.Pervasives.Native.__proj__Some__item__v Strategies.Semantics.step_computation_generic Prims.squash
let rec next_atomic_step_preserves_inv_case_action_pred
      (asip: atomic_semantics_invariant_proof_t)
      (actor: asip.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (atomic_step: list asip.sem.step_t)
      (s:
          asip.sem.state_t
            { for_all_ubool asip.action_pred (map_ghost asip.sem.step_to_action_f atomic_step) /\
              (asip.inv s) /\
              Some? (steps_computation_generic asip.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    atomic_step
                    s) })
    : GTot
      (squash (asip.inv (Some?.v (steps_computation_generic asip.sem
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      atomic_step
                      s)))) (decreases atomic_step) =
  
match atomic_step with
| [last_step] ->
  assert (asip.action_pred (asip.sem.step_to_action_f last_step));
  asip.action_proof actor starts_atomic_block ends_atomic_block last_step s
| first_step :: remaining_steps ->
  assert (asip.action_pred (asip.sem.step_to_action_f first_step));
  asip.action_proof actor starts_atomic_block false first_step s;
  let s' =
    Some?.v (step_computation_generic asip.sem actor starts_atomic_block false first_step s)
  in
  next_atomic_step_preserves_inv_case_action_pred asip
    actor
    false
    ends_atomic_block
    remaining_steps
    s'