val armada_weakening_transformer_to_weakening_transformer
      (hatomic_actions: list (list Armada.Action.t))
      (hatomic_action_array:
          array_t (list Armada.Action.t) {hatomic_action_array == list_to_array hatomic_actions})
      (inv: invariant_t Armada.State.t)
      (awt: armada_weakening_transformer_t hatomic_action_array inv)
    : GTot (weakening_transformer_t (make_atomic_semantics armada_semantics) hatomic_actions inv)
val armada_weakening_transformer_to_weakening_transformer
      (hatomic_actions: list (list Armada.Action.t))
      (hatomic_action_array:
          array_t (list Armada.Action.t) {hatomic_action_array == list_to_array hatomic_actions})
      (inv: invariant_t Armada.State.t)
      (awt: armada_weakening_transformer_t hatomic_action_array inv)
    : GTot (weakening_transformer_t (make_atomic_semantics armada_semantics) hatomic_actions inv)
let armada_weakening_transformer_to_weakening_transformer
  (hatomic_actions: list (list Armada.Action.t))
  (hatomic_action_array: array_t (list Armada.Action.t){hatomic_action_array == list_to_array hatomic_actions})
  (inv: invariant_t Armada.State.t)
  (awt: armada_weakening_transformer_t hatomic_action_array inv)
  : GTot (weakening_transformer_t (make_atomic_semantics armada_semantics) hatomic_actions inv) =
  match awt with
  | ArmadaWeakeningTransformerSameStep hatomic_action_idx -> WeakeningTransformerSameStep hatomic_action_idx
  | ArmadaWeakeningTransformerUpdatedStep lactions step_updater proof ->
      armada_steps_updater_works_implies_step_updater_works lactions hatomic_actions hatomic_action_array inv
        step_updater proof;
      WeakeningTransformerUpdatedStep lactions (remove_index_from_steps_updater step_updater) (fun _ -> ())
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 FStar.Tactics.V2
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.Weakening
open Spec.List
open Spec.Ubool
open Util.List

let remove_index_from_steps_updater
  (u:(tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
  (tid: tid_t)
  (lsteps: list Armada.Step.t)
  (ls: Armada.State.t)
  : GTot (list Armada.Step.t) =
  let idx, steps = u tid lsteps ls in
  steps

let armada_steps_updater_works_implies_step_updater_works
  (lactions: list Armada.Action.t)
  (hatomic_actions: list (list Armada.Action.t))
  (hatomic_action_array: array_t (list Armada.Action.t))
  (inv: invariant_t Armada.State.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))
  : Lemma (requires hatomic_action_array == list_to_array hatomic_actions)
          (ensures  step_updater_works (make_atomic_semantics armada_semantics) hatomic_actions inv lactions
                      (remove_index_from_steps_updater steps_updater)) =
  let sem = make_atomic_semantics armada_semantics in
  introduce forall (actor: sem.actor_t) (starts_atomic_block: bool) (ends_atomic_block: bool) (lsteps: sem.step_t)
              (s: sem.state_t).
              (  sem.step_to_action_f lsteps == lactions
               /\ inv s
               /\ Some? (step_computation_generic sem actor starts_atomic_block ends_atomic_block lsteps s)) ==>
              (let hatomic_action_idx, hsteps = steps_updater actor lsteps s in
               let hactions = sem.step_to_action_f hsteps in
                 (contains_ubool hactions hatomic_actions)
               /\ (step_computation_generic sem actor starts_atomic_block ends_atomic_block hsteps s ==
                  step_computation_generic sem actor starts_atomic_block ends_atomic_block lsteps s))
  with introduce _ ==> _
  with _. (
    proof ();
    armada_steps_computation_equivalent actor starts_atomic_block ends_atomic_block lsteps s;
    let hatomic_action_idx, hsteps = steps_updater actor lsteps s in
    armada_steps_computation_equivalent actor starts_atomic_block ends_atomic_block hsteps s;
    let hactions = sem.step_to_action_f hsteps in
    index_to_contains_ubool hatomic_actions hatomic_action_idx
  )
/
Util.List.fst.checked Strategies.Weakening.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.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.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.fst

    hatomic_actions: Prims.list (Prims.list Armada.Action.t) ->
    hatomic_action_array:
      Util.ImmutableArray.array_t (Prims.list Armada.Action.t)
        {hatomic_action_array == Util.ImmutableArray.list_to_array hatomic_actions} ->
    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    awt: Strategies.Weakening.Armada.armada_weakening_transformer_t hatomic_action_array inv
  -> Prims.GTot
    (Strategies.Weakening.weakening_transformer_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          )
        hatomic_actions
        inv)
Prims.list Armada.Action.t Util.ImmutableArray.array_t Prims.eq2 FStar.ImmutableArray.Base.t Util.ImmutableArray.list_to_array Strategies.Invariant.invariant_t Armada.State.t Strategies.Weakening.Armada.armada_weakening_transformer_t Prims.nat Strategies.Weakening.WeakeningTransformerSameStep Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Armada.Base.tid_t Armada.Step.t FStar.Pervasives.Native.tuple2 Prims.unit Prims.squash Strategies.Weakening.Armada.armada_steps_updater_works Strategies.Weakening.WeakeningTransformerUpdatedStep Strategies.Weakening.Armada.remove_index_from_steps_updater Prims.b2t Strategies.Weakening.step_updater_works Strategies.Weakening.Armada.armada_steps_updater_works_implies_step_updater_works Strategies.Weakening.weakening_transformer_t
let armada_weakening_transformer_to_weakening_transformer
      (hatomic_actions: list (list Armada.Action.t))
      (hatomic_action_array:
          array_t (list Armada.Action.t) {hatomic_action_array == list_to_array hatomic_actions})
      (inv: invariant_t Armada.State.t)
      (awt: armada_weakening_transformer_t hatomic_action_array inv)
    : GTot (weakening_transformer_t (make_atomic_semantics armada_semantics) hatomic_actions inv) =
  
match awt with
| ArmadaWeakeningTransformerSameStep hatomic_action_idx ->
  WeakeningTransformerSameStep hatomic_action_idx
| ArmadaWeakeningTransformerUpdatedStep lactions step_updater proof ->
  armada_steps_updater_works_implies_step_updater_works lactions
    hatomic_actions
    hatomic_action_array
    inv
    step_updater
    proof;
  WeakeningTransformerUpdatedStep lactions
    (remove_index_from_steps_updater step_updater)
    (fun _ -> ())