val transform_special_case_proof
      (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)))))
    : GTot
    (
          actor: armada_semantics.actor_t ->
          starts_atomic_block: bool ->
          ends_atomic_block: bool ->
          step: armada_semantics.step_t ->
          s:
            armada_semantics.state_t
              { armada_semantics.step_to_action_f step == action /\ inv s /\
                Some? (step_computation_generic armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      step
                      s) }
        -> squash (inv (Some?.v (step_computation_generic armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        step
                        s))))
val transform_special_case_proof
      (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)))))
    : GTot
    (
          actor: armada_semantics.actor_t ->
          starts_atomic_block: bool ->
          ends_atomic_block: bool ->
          step: armada_semantics.step_t ->
          s:
            armada_semantics.state_t
              { armada_semantics.step_to_action_f step == action /\ inv s /\
                Some? (step_computation_generic armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      step
                      s) }
        -> squash (inv (Some?.v (step_computation_generic armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        step
                        s))))
let transform_special_case_proof
  (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))))
  : GTot ((actor: armada_semantics.actor_t) ->
          (starts_atomic_block: bool) ->
          (ends_atomic_block: bool) ->
          (step: armada_semantics.step_t) ->
          (s: armada_semantics.state_t{
              armada_semantics.step_to_action_f step == action
            /\ inv s
            /\ Some? (step_computation_generic armada_semantics actor starts_atomic_block
                       ends_atomic_block step s)}) ->
          squash (inv (Some?.v (step_computation_generic armada_semantics actor starts_atomic_block
                                  ends_atomic_block step s)))) =
  special_case_proof
module Strategies.Invariant.Armada

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

let is_inductive_armada_invariant_of_program_implies_is_invariant_of_program
  (inv: invariant_t Armada.State.t)
  (program: Armada.Program.t)
  (* see .fsti file for spec *) =
  is_inductive_invariant_of_spec_implies_is_invariant_of_spec inv (program_to_spec program)

noeq type armada_invariant_proof_t = {
  program: Armada.Program.t;
  inv: invariant_t Armada.State.t;
  action_pred: Armada.Action.t -> GTot ubool;
  special_case_proofs: list (option (armada_action_special_case_invariant_proof_t inv));
  init_implies_inv_proof: (s: Armada.State.t{init_program program s}) -> squash (inv s);
  action_proof: armada_action_maintains_invariant_proof_t inv action_pred;
  special_cases_apply_proof: unit ->
     squash (armada_action_special_cases_apply inv action_pred (all_actions program.program_statements)
               special_case_proofs);
}
/
Util.List.fst.checked Strategies.Semantics.Armada.fsti.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 FStar.Classical.Sugar.fsti.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.Invariant.Armada.fst

    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    action: Armada.Action.t ->
    special_case_proof:
      (
            actor: Armada.Base.tid_t ->
            starts_atomic_block: Prims.bool ->
            ends_atomic_block: Prims.bool ->
            step: Armada.Step.t ->
            s:
              Armada.State.t
                { Mkt?.action step == action /\ inv s /\
                  Some? (Armada.Transition.step_computation actor
                        starts_atomic_block
                        ends_atomic_block
                        step
                        s) }
          -> Prims.squash (inv (Some?.v (Armada.Transition.step_computation actor
                          starts_atomic_block
                          ends_atomic_block
                          step
                          s))))
  -> Prims.GTot
    (
          actor: Mksemantics_t?.actor_t Strategies.Semantics.Armada.armada_semantics ->
          starts_atomic_block: Prims.bool ->
          ends_atomic_block: Prims.bool ->
          step: Mksemantics_t?.step_t Strategies.Semantics.Armada.armada_semantics ->
          s:
            Mksemantics_t?.state_t Strategies.Semantics.Armada.armada_semantics
              { Mksemantics_t?.step_to_action_f Strategies.Semantics.Armada.armada_semantics step ==
                action /\ inv s /\
                Some? (Strategies.Semantics.step_computation_generic Strategies.Semantics.Armada.armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      step
                      s) }
        -> Prims.squash (inv (Some?.v (Strategies.Semantics.step_computation_generic Strategies.Semantics.Armada.armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        step
                        s))))
Strategies.Invariant.invariant_t Armada.State.t Armada.Action.t Armada.Base.tid_t Prims.bool Armada.Step.t Prims.l_and Prims.eq2 Armada.Step.__proj__Mkt__item__action Prims.b2t FStar.Pervasives.Native.uu___is_Some Armada.Transition.step_computation Prims.squash FStar.Pervasives.Native.__proj__Some__item__v Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Strategies.Semantics.Armada.armada_semantics Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.__proj__Mksemantics_t__item__step_to_action_f Strategies.Semantics.step_computation_generic
let transform_special_case_proof
      (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)))))
    : GTot
    (
          actor: armada_semantics.actor_t ->
          starts_atomic_block: bool ->
          ends_atomic_block: bool ->
          step: armada_semantics.step_t ->
          s:
            armada_semantics.state_t
              { armada_semantics.step_to_action_f step == action /\ inv s /\
                Some? (step_computation_generic armada_semantics
                      actor
                      starts_atomic_block
                      ends_atomic_block
                      step
                      s) }
        -> squash (inv (Some?.v (step_computation_generic armada_semantics
                        actor
                        starts_atomic_block
                        ends_atomic_block
                        step
                        s)))) =
  
special_case_proof