val is_armada_substep_invariant
      (program: program_t (make_atomic_semantics armada_semantics))
      (inv: invariant_t Armada.State.t)
    : GTot ubool
val is_armada_substep_invariant
      (program: program_t (make_atomic_semantics armada_semantics))
      (inv: invariant_t Armada.State.t)
    : GTot ubool
let is_armada_substep_invariant
  (program: program_t (make_atomic_semantics armada_semantics))
  (inv: invariant_t Armada.State.t)
  : GTot ubool =
    (forall s. program.init_f s ==> inv s)
  /\ (forall actor starts_atomic_block ends_atomic_block (step: Armada.Step.t) s actions.
        let s' = step_computation actor starts_atomic_block ends_atomic_block step s in
          contains_ubool actions program.actions
        /\ contains_ubool step.action actions
        /\ inv s
        /\ Some? s'
        ==> inv (Some?.v s'))
module Strategies.Invariant.Armada.AtomicSubstep

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.Semantics
open Strategies.Semantics.Armada
open Strategies.Invariant
open Strategies.Invariant.Armada
open Util.List

noeq type armada_atomic_substep_invariant_witness_t
  (program: program_t (make_atomic_semantics armada_semantics))
  (inv: invariant_t Armada.State.t) =
{
  action_pred: Armada.Action.t -> GTot ubool;
  special_case_proofs: list (list (option (armada_action_special_case_invariant_proof_t inv)));
  init_implies_inv_proof: (s: Armada.State.t{program.init_f s}) -> squash (inv s);
  action_proof: armada_action_maintains_invariant_proof_t inv action_pred;
}

let armada_atomic_substep_special_cases_apply
  (inv: invariant_t Armada.State.t)
  (action_pred: Armada.Action.t -> GTot ubool)
  (program_actions: list (list Armada.Action.t))
  (special_case_proofs: (list (list (option (armada_action_special_case_invariant_proof_t inv))))) =
  lists_correspond_ubool
    (lists_correspond_ubool (armada_action_proof_option_applies inv action_pred))
    program_actions
    special_case_proofs

let armada_atomic_substep_invariant_witness_valid
  (program: program_t (make_atomic_semantics armada_semantics))
  (inv: invariant_t Armada.State.t)
  (aiw: armada_atomic_substep_invariant_witness_t program inv)
  : GTot ubool =
  armada_atomic_substep_special_cases_apply inv aiw.action_pred program.actions aiw.special_case_proofs
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.fsti.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.AtomicSubstep.fsti

    program:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    inv: Strategies.Invariant.invariant_t Armada.State.t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.program_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.Invariant.invariant_t Armada.State.t Prims.l_and Prims.l_Forall Prims.l_imp Strategies.Semantics.__proj__Mkprogram_t__item__init_f Armada.Base.tid_t Prims.bool Armada.Step.t Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__action_t Spec.List.contains_ubool Strategies.Semantics.__proj__Mkprogram_t__item__actions Armada.Step.__proj__Mkt__item__action Prims.b2t FStar.Pervasives.Native.uu___is_Some FStar.Pervasives.Native.__proj__Some__item__v FStar.Pervasives.Native.option Armada.Transition.step_computation Spec.Ubool.ubool
let is_armada_substep_invariant
      (program: program_t (make_atomic_semantics armada_semantics))
      (inv: invariant_t Armada.State.t)
    : GTot ubool =
  
(forall s. program.init_f s ==> inv s) /\
(forall actor starts_atomic_block ends_atomic_block (step: Armada.Step.t) s actions.
    let s' = step_computation actor starts_atomic_block ends_atomic_block step s in
    contains_ubool actions program.actions /\ contains_ubool step.action actions /\ inv s /\
    Some? s' ==>
    inv (Some?.v s'))