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

    hatomic_action_array: Util.ImmutableArray.array_t (Prims.list Armada.Action.t) ->
    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    lactions: Prims.list Armada.Action.t ->
    steps_updater:
      (_: Armada.Base.tid_t -> _: Prims.list Armada.Step.t -> _: Armada.State.t
          -> Prims.GTot (Prims.nat * Prims.list Armada.Step.t))
  -> Prims.GTot Spec.Ubool.ubool
Util.ImmutableArray.array_t Prims.list Armada.Action.t Strategies.Invariant.invariant_t Armada.State.t Armada.Base.tid_t Armada.Step.t FStar.Pervasives.Native.tuple2 Prims.nat Prims.l_Forall Prims.bool Prims.l_imp Prims.l_and Prims.eq2 Util.List.map_ghost Strategies.Semantics.Armada.armada_step_to_action Prims.b2t FStar.Pervasives.Native.uu___is_Some Armada.Transition.steps_computation Prims.op_LessThan Util.ImmutableArray.array_len Util.ImmutableArray.array_index FStar.Pervasives.Native.option Prims.logical Spec.Ubool.ubool
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))