val 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))
val 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 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
  )
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
/
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

    lactions: Prims.list Armada.Action.t ->
    hatomic_actions: Prims.list (Prims.list Armada.Action.t) ->
    hatomic_action_array: Util.ImmutableArray.array_t (Prims.list Armada.Action.t) ->
    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    steps_updater:
      (_: Armada.Base.tid_t -> _: Prims.list Armada.Step.t -> _: Armada.State.t
          -> Prims.GTot (Prims.nat * Prims.list Armada.Step.t)) ->
    proof:
      (_: Prims.unit
          -> Prims.squash (Strategies.Weakening.Armada.armada_steps_updater_works hatomic_action_array
                  inv
                  lactions
                  steps_updater))
  -> FStar.Pervasives.Lemma
      (requires hatomic_action_array == Util.ImmutableArray.list_to_array hatomic_actions)
      (ensures
        Strategies.Weakening.step_updater_works (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
            )
          hatomic_actions
          inv
          lactions
          (Strategies.Weakening.Armada.remove_index_from_steps_updater steps_updater))
Prims.list Armada.Action.t Util.ImmutableArray.array_t Strategies.Invariant.invariant_t Armada.State.t Armada.Base.tid_t Armada.Step.t FStar.Pervasives.Native.tuple2 Prims.nat Prims.unit Prims.squash Strategies.Weakening.Armada.armada_steps_updater_works FStar.Classical.Sugar.forall_intro Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.l_Forall Prims.bool Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Prims.l_imp Prims.l_and Prims.eq2 Strategies.Semantics.__proj__Mksemantics_t__item__step_to_action_f Prims.b2t FStar.Pervasives.Native.uu___is_Some Strategies.Semantics.step_computation_generic Spec.List.contains_ubool FStar.Pervasives.Native.option Strategies.Semantics.__proj__Mksemantics_t__item__action_t Prims.logical FStar.Classical.Sugar.implies_intro Util.List.index_to_contains_ubool Strategies.Semantics.Armada.armada_steps_computation_equivalent Strategies.Semantics.semantics_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics FStar.ImmutableArray.Base.t Util.ImmutableArray.list_to_array Strategies.Weakening.step_updater_works Strategies.Weakening.Armada.remove_index_from_steps_updater Prims.Nil FStar.Pervasives.pattern
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)