val armada_action_special_cases_apply : inv: Strategies.Invariant.invariant_t Armada.State.t ->
    action_pred: (_: Armada.Action.t -> Prims.GTot Spec.Ubool.ubool) ->
    program_actions: Prims.list Armada.Action.t ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t
                inv))
  -> Spec.Ubool.ubool
let armada_action_special_cases_apply
  (inv: invariant_t Armada.State.t)
  (action_pred: Armada.Action.t -> GTot ubool)
  (program_actions: list Armada.Action.t)
  (special_case_proofs: (list (option (armada_action_special_case_invariant_proof_t inv)))) =
  lists_correspond_ubool (armada_action_proof_option_applies inv action_pred) program_actions special_case_proofs
module Strategies.Invariant.Armada

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Step
open Armada.Transition
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.List

let is_inductive_armada_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  : GTot ubool
  =   (forall (s: Armada.State.t). init_program program s ==> inv s)
    /\ (forall (s s': Armada.State.t) (transition: Armada.Transition.t).
          inv s /\ next_program program transition s s' ==> inv s')

val is_inductive_armada_invariant_of_program_implies_is_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  : Lemma
    (requires is_inductive_armada_invariant_of_program inv program)
    (ensures  is_invariant_of_spec inv (program_to_spec program))

noeq type armada_action_special_case_invariant_proof_t (inv: invariant_t Armada.State.t) = {
  action: Armada.Action.t;
  special_case_proof:
    (actor: tid_t) ->
    (starts_atomic_block: bool) ->
    (ends_atomic_block: bool) ->
    (step: Armada.Step.t) ->
    (s: Armada.State.t{
        step.action == action
      /\ inv s
      /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)})
    -> squash (inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)));
}

type armada_action_maintains_invariant_proof_t
  (inv: invariant_t Armada.State.t)
  (action_pred: Armada.Action.t -> GTot ubool) =
  (actor: tid_t) ->
  (starts_atomic_block: bool) ->
  (ends_atomic_block: bool) ->
  (step: Armada.Step.t) ->
  (s: Armada.State.t{
      action_pred step.action
    /\ inv s
    /\ Some? (step_computation actor starts_atomic_block ends_atomic_block step s)}) ->
  squash (inv (Some?.v (step_computation actor starts_atomic_block ends_atomic_block step s)))

let armada_action_proof_option_applies
  (inv: invariant_t Armada.State.t)
  (action_pred: Armada.Action.t -> GTot ubool)
  (action: Armada.Action.t)
  (proof_option: option (armada_action_special_case_invariant_proof_t inv))
  : GTot ubool =
  match proof_option with
  | None -> action_pred action
  | Some prf -> eqb prf.action action
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.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 Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Invariant.Armada.fsti

    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    action_pred: (_: Armada.Action.t -> Prims.GTot Spec.Ubool.ubool) ->
    program_actions: Prims.list Armada.Action.t ->
    special_case_proofs:
      Prims.list (FStar.Pervasives.Native.option (Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t
                inv))
  -> Spec.Ubool.ubool
Strategies.Invariant.invariant_t Armada.State.t Armada.Action.t Spec.Ubool.ubool Prims.list FStar.Pervasives.Native.option Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t Util.List.lists_correspond_ubool Strategies.Invariant.Armada.armada_action_proof_option_applies
let armada_action_special_cases_apply
      (inv: invariant_t Armada.State.t)
      (action_pred: (Armada.Action.t -> GTot ubool))
      (program_actions: list Armada.Action.t)
      (special_case_proofs: (list (option (armada_action_special_case_invariant_proof_t inv))))
     =
  
lists_correspond_ubool (armada_action_proof_option_applies inv action_pred)
  program_actions
  special_case_proofs