val transform_special_case
      (inv: invariant_t Armada.State.t)
      (proof: armada_action_special_case_invariant_proof_t inv)
    : GTot (action_special_case_invariant_proof_t armada_semantics inv)
val transform_special_case
      (inv: invariant_t Armada.State.t)
      (proof: armada_action_special_case_invariant_proof_t inv)
    : GTot (action_special_case_invariant_proof_t armada_semantics inv)
let transform_special_case
  (inv: invariant_t Armada.State.t)
  (proof: armada_action_special_case_invariant_proof_t inv)
  : GTot (action_special_case_invariant_proof_t armada_semantics inv) =
  {
    action = proof.action;
    special_case_proof = transform_special_case_proof inv proof.action proof.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);
}

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
/
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 ->
    proof: Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t inv
  -> Prims.GTot
    (Strategies.Invariant.action_special_case_invariant_proof_t Strategies.Semantics.Armada.armada_semantics
        inv)
Strategies.Invariant.invariant_t Armada.State.t Strategies.Invariant.Armada.armada_action_special_case_invariant_proof_t Strategies.Invariant.Mkaction_special_case_invariant_proof_t Strategies.Semantics.Armada.armada_semantics Strategies.Invariant.Armada.__proj__Mkarmada_action_special_case_invariant_proof_t__item__action Strategies.Invariant.Armada.transform_special_case_proof Strategies.Invariant.Armada.__proj__Mkarmada_action_special_case_invariant_proof_t__item__special_case_proof Strategies.Invariant.action_special_case_invariant_proof_t
let transform_special_case
      (inv: invariant_t Armada.State.t)
      (proof: armada_action_special_case_invariant_proof_t inv)
    : GTot (action_special_case_invariant_proof_t armada_semantics inv) =
  
{
  action = proof.action;
  special_case_proof = transform_special_case_proof inv proof.action proof.special_case_proof
}