val action_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) ->
    program_actions: Prims.list (Mksemantics_t?.action_t sem) ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.action_special_case_invariant_proof_t
                sem
                inv))
  -> Spec.Ubool.ubool
let action_special_cases_apply
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (action_pred: sem.action_t -> GTot ubool)
  (program_actions: list sem.action_t)
  (special_case_proofs: (list (option (action_special_case_invariant_proof_t sem inv)))) =
  lists_correspond_ubool (action_proof_option_applies sem inv action_pred) program_actions special_case_proofs
module Strategies.Invariant

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

/// Proving invariants of arbitrary state machines

type invariant_t (state_t: Type) = state_t -> GTot ubool

let is_invariant_of_behavior
  (#state_t: Type)
  (inv: invariant_t state_t)
  (b: behavior_t state_t)
  : GTot ubool
  = forall s. contains_ubool s b ==> inv s

let is_invariant_of_spec
  (#state_t: Type)
  (inv: invariant_t state_t)
  (spec: spec_t state_t)
  : GTot ubool
  = forall (b: behavior_t state_t). behavior_satisfies_spec b spec ==> is_invariant_of_behavior inv b

let is_inductive_invariant_of_spec
  (#state_t: Type)
  (inv: invariant_t state_t)
  (spec: spec_t state_t)
  : GTot ubool
  =   (forall (s: state_t). spec.init s ==> inv s)
    /\ (forall (s s': state_t). inv s /\ (spec.next s s') ==> inv s')

val is_inductive_invariant_of_spec_implies_is_invariant_of_spec
  (#state_t: Type)
  (inv: invariant_t state_t)
  (spec: spec_t state_t)
  : Lemma
    (requires is_inductive_invariant_of_spec inv spec)
    (ensures  is_invariant_of_spec inv spec)

noeq type action_special_case_invariant_proof_t (sem: semantics_t) (inv: invariant_t sem.state_t) = {
  action: sem.action_t;
  special_case_proof:
    (actor: sem.actor_t) ->
    (starts_atomic_block: bool) ->
    (ends_atomic_block: bool) ->
    (step: sem.step_t) ->
    (s: sem.state_t{
         sem.step_to_action_f step == action
       /\ inv s
       /\ Some? (step_computation_generic sem actor starts_atomic_block ends_atomic_block step s)}) ->
    squash (inv (Some?.v (step_computation_generic sem actor starts_atomic_block ends_atomic_block step s)));
}

type action_maintains_invariant_proof_t
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (action_pred: (sem.action_t -> GTot ubool)) =
  (actor: sem.actor_t) ->
  (starts_atomic_block: bool) ->
  (ends_atomic_block: bool) ->
  (step: sem.step_t) ->
  (s: sem.state_t{
       action_pred (sem.step_to_action_f step)
     /\ inv s
     /\ Some? (step_computation_generic sem actor starts_atomic_block ends_atomic_block step s)}) ->
  squash (inv (Some?.v (step_computation_generic sem actor starts_atomic_block ends_atomic_block step s)))

let action_proof_option_applies
  (sem: semantics_t)
  (inv: invariant_t sem.state_t)
  (action_pred: sem.action_t -> GTot ubool)
  (action: sem.action_t)
  (proof_option: option (action_special_case_invariant_proof_t sem inv))
  : GTot ubool =
  match proof_option with
  | None -> action_pred action
  | Some prf -> eqb prf.action action
/
Util.List.fst.checked Strategies.Semantics.fst.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.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) ->
    program_actions: Prims.list (Mksemantics_t?.action_t sem) ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.action_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.action_special_case_invariant_proof_t Util.List.lists_correspond_ubool Strategies.Invariant.action_proof_option_applies
let action_special_cases_apply
      (sem: semantics_t)
      (inv: invariant_t sem.state_t)
      (action_pred: (sem.action_t -> GTot ubool))
      (program_actions: list sem.action_t)
      (special_case_proofs: (list (option (action_special_case_invariant_proof_t sem inv))))
     =
  
lists_correspond_ubool (action_proof_option_applies sem inv action_pred)
  program_actions
  special_case_proofs