val convert_atomic_special_case_proofs_to_action_special_case_proofs
      (sem: semantics_t)
      (inv: invariant_t sem.state_t)
      (special_case_proofs: list (option (atomic_special_case_invariant_proof_t sem inv)))
    : Ghost (list (option (action_special_case_invariant_proof_t (make_atomic_semantics sem) inv)))
      (requires True)
      (ensures
        fun action_special_case_proofs ->
          lists_correspond_ubool (atomic_special_case_proof_corresponds_to_action_special_case_proof
                sem
                inv)
            special_case_proofs
            action_special_case_proofs)
val convert_atomic_special_case_proofs_to_action_special_case_proofs
      (sem: semantics_t)
      (inv: invariant_t sem.state_t)
      (special_case_proofs: list (option (atomic_special_case_invariant_proof_t sem inv)))
    : Ghost (list (option (action_special_case_invariant_proof_t (make_atomic_semantics sem) inv)))
      (requires True)
      (ensures
        fun action_special_case_proofs ->
          lists_correspond_ubool (atomic_special_case_proof_corresponds_to_action_special_case_proof
                sem
                inv)
            special_case_proofs
            action_special_case_proofs)
let rec convert_atomic_special_case_proofs_to_action_special_case_proofs
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (special_case_proofs: list (option (atomic_special_case_invariant_proof_t sem inv)))
  : Ghost (list (option (action_special_case_invariant_proof_t (make_atomic_semantics sem) inv)))
  (requires True)
  (ensures  fun action_special_case_proofs ->
     lists_correspond_ubool
     (atomic_special_case_proof_corresponds_to_action_special_case_proof sem inv)
     special_case_proofs
     action_special_case_proofs) =
  match special_case_proofs with
  | [] -> []
  | first_proof :: remaining_proofs ->
      (convert_atomic_special_case_proof_to_action_special_case_proof sem inv first_proof) ::
      (convert_atomic_special_case_proofs_to_action_special_case_proofs sem inv remaining_proofs)
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

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'

let atomic_special_case_proof_corresponds_to_action_special_case_proof
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (atomic_special_case_proof: option (atomic_special_case_invariant_proof_t sem inv))
  (action_special_case_proof: option (action_special_case_invariant_proof_t (make_atomic_semantics sem) inv))
  : GTot ubool =
  match atomic_special_case_proof with
  | None -> None? action_special_case_proof
  | Some prf ->    Some? action_special_case_proof
               && eqb prf.atomic_action (Some?.v action_special_case_proof).action

let convert_atomic_special_case_proof_to_action_special_case_proof
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (special_case_proof: option (atomic_special_case_invariant_proof_t sem inv))
  : Ghost (option (action_special_case_invariant_proof_t (make_atomic_semantics sem) inv))
  (requires True)
  (ensures fun action_special_case_proof -> atomic_special_case_proof_corresponds_to_action_special_case_proof sem
                                           inv special_case_proof action_special_case_proof) =
  match special_case_proof with
  | None -> None
  | Some prf ->
      let atomic_sem = make_atomic_semantics sem in
      let lem
        (actor: atomic_sem.actor_t)
        (starts_atomic_block: bool)
        (ends_atomic_block: bool)
        (atomic_step: atomic_sem.step_t)
        (s: atomic_sem.state_t{
             atomic_sem.step_to_action_f atomic_step == prf.atomic_action
           /\ inv s
           /\ Some? (step_computation_generic atomic_sem actor starts_atomic_block
                      ends_atomic_block atomic_step s)})
        : squash (inv (Some?.v (step_computation_generic atomic_sem actor starts_atomic_block
                                  ends_atomic_block atomic_step s))) =
        (prf.special_case_proof actor starts_atomic_block ends_atomic_block atomic_step s) in
      Some ({ action = prf.atomic_action; special_case_proof = lem; })
/
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

    sem: Strategies.Semantics.semantics_t ->
    inv: Strategies.Invariant.invariant_t (Mksemantics_t?.state_t sem) ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t
                sem
                inv))
  -> Prims.Ghost
    (Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.action_special_case_invariant_proof_t
                (Strategies.Atomic.make_atomic_semantics sem)
                inv)))
Strategies.Semantics.semantics_t Strategies.Invariant.invariant_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Prims.list FStar.Pervasives.Native.option Strategies.Invariant.Atomic.atomic_special_case_invariant_proof_t Prims.Nil Strategies.Invariant.action_special_case_invariant_proof_t Strategies.Atomic.make_atomic_semantics Prims.Cons Strategies.Invariant.Atomic.convert_atomic_special_case_proof_to_action_special_case_proof Strategies.Invariant.Atomic.convert_atomic_special_case_proofs_to_action_special_case_proofs Prims.l_True Util.List.lists_correspond_ubool Strategies.Invariant.Atomic.atomic_special_case_proof_corresponds_to_action_special_case_proof
let rec convert_atomic_special_case_proofs_to_action_special_case_proofs
      (sem: semantics_t)
      (inv: invariant_t sem.state_t)
      (special_case_proofs: list (option (atomic_special_case_invariant_proof_t sem inv)))
    : Ghost (list (option (action_special_case_invariant_proof_t (make_atomic_semantics sem) inv)))
      (requires True)
      (ensures
        fun action_special_case_proofs ->
          lists_correspond_ubool (atomic_special_case_proof_corresponds_to_action_special_case_proof
                sem
                inv)
            special_case_proofs
            action_special_case_proofs) =
  
match special_case_proofs with
| [] -> []
| first_proof :: remaining_proofs ->
  (convert_atomic_special_case_proof_to_action_special_case_proof sem inv first_proof) ::
  (convert_atomic_special_case_proofs_to_action_special_case_proofs sem inv remaining_proofs)