val action_matches_armada_weakening_transformer
      (#hatomic_action_array: array_t (list Armada.Action.t))
      (#inv: invariant_t Armada.State.t)
      (lactions: list Armada.Action.t)
      (weakening_transformer: armada_weakening_transformer_t hatomic_action_array inv)
    : GTot ubool
val action_matches_armada_weakening_transformer
      (#hatomic_action_array: array_t (list Armada.Action.t))
      (#inv: invariant_t Armada.State.t)
      (lactions: list Armada.Action.t)
      (weakening_transformer: armada_weakening_transformer_t hatomic_action_array inv)
    : GTot ubool
let action_matches_armada_weakening_transformer
  (#hatomic_action_array: array_t (list Armada.Action.t))
  (#inv: invariant_t Armada.State.t)
  (lactions: list Armada.Action.t)
  (weakening_transformer: armada_weakening_transformer_t hatomic_action_array inv)
  : GTot ubool =
  match weakening_transformer with
  | ArmadaWeakeningTransformerSameStep hatomic_action_idx ->
        hatomic_action_idx < array_len hatomic_action_array
      /\ array_index hatomic_action_array hatomic_action_idx == lactions
  | ArmadaWeakeningTransformerUpdatedStep actions _ _ -> lactions == actions
module Strategies.Weakening.Armada

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

let armada_steps_updater_works
  (hatomic_action_array: array_t (list Armada.Action.t))
  (inv: invariant_t Armada.State.t)
  (lactions: list Armada.Action.t)
  (steps_updater: (tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
  : GTot ubool =
  forall (actor: tid_t) (starts_atomic_block: bool) (ends_atomic_block: bool) (lsteps: list Armada.Step.t)
       (s: Armada.State.t).
    (  map_ghost armada_step_to_action lsteps == lactions
     /\ inv s
     /\ Some? (steps_computation actor starts_atomic_block ends_atomic_block lsteps s)) ==>
    (let hatomic_action_idx, hsteps = steps_updater actor lsteps s in
     let haction = map_ghost armada_step_to_action hsteps in
       hatomic_action_idx < array_len hatomic_action_array
     /\ array_index hatomic_action_array hatomic_action_idx == haction
     /\ (steps_computation actor starts_atomic_block ends_atomic_block hsteps s ==
        steps_computation actor starts_atomic_block ends_atomic_block lsteps s))

noeq type armada_weakening_transformer_t
  (hatomic_action_array: array_t (list Armada.Action.t))
  (inv: invariant_t Armada.State.t) =
  | ArmadaWeakeningTransformerSameStep: (hatomic_action_idx: nat) ->
      armada_weakening_transformer_t hatomic_action_array inv
  | ArmadaWeakeningTransformerUpdatedStep:
     (lactions: list Armada.Action.t) ->
     (steps_updater: (tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t))) ->
     (proof: unit -> squash (armada_steps_updater_works hatomic_action_array inv lactions steps_updater)) ->
     armada_weakening_transformer_t hatomic_action_array inv
/
Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Invariant.Armada.Atomic.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.Type.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.Weakening.Armada.fsti

    lactions: Prims.list Armada.Action.t ->
    weakening_transformer:
      Strategies.Weakening.Armada.armada_weakening_transformer_t hatomic_action_array inv
  -> Prims.GTot Spec.Ubool.ubool
Util.ImmutableArray.array_t Prims.list Armada.Action.t Strategies.Invariant.invariant_t Armada.State.t Strategies.Weakening.Armada.armada_weakening_transformer_t Prims.nat Prims.l_and Prims.b2t Prims.op_LessThan Util.ImmutableArray.array_len Prims.eq2 Util.ImmutableArray.array_index Armada.Base.tid_t Armada.Step.t FStar.Pervasives.Native.tuple2 Prims.unit Prims.squash Strategies.Weakening.Armada.armada_steps_updater_works Spec.Ubool.ubool
let action_matches_armada_weakening_transformer
      (#hatomic_action_array: array_t (list Armada.Action.t))
      (#inv: invariant_t Armada.State.t)
      (lactions: list Armada.Action.t)
      (weakening_transformer: armada_weakening_transformer_t hatomic_action_array inv)
    : GTot ubool =
  
match weakening_transformer with
| ArmadaWeakeningTransformerSameStep hatomic_action_idx ->
  hatomic_action_idx < array_len hatomic_action_array /\
  array_index hatomic_action_array hatomic_action_idx == lactions
| ArmadaWeakeningTransformerUpdatedStep actions _ _ -> lactions == actions