val my_special_case_steps_updater_works_0: Prims.unit
  -> squash (armada_steps_updater_works (list_to_array MyAtomicHProg.prog.actions)
          my_inv
          my_special_case_action_0
          my_special_case_steps_updater_0)
val my_special_case_steps_updater_works_0: Prims.unit
  -> squash (armada_steps_updater_works (list_to_array MyAtomicHProg.prog.actions)
          my_inv
          my_special_case_action_0
          my_special_case_steps_updater_0)
let my_special_case_steps_updater_works_0 ()
  : squash (armada_steps_updater_works (list_to_array MyAtomicHProg.prog.actions) my_inv my_special_case_action_0
              my_special_case_steps_updater_0) =
  let hatomic_action_array = list_to_array MyAtomicHProg.prog.actions in
  introduce 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 == my_special_case_action_0
    /\ my_inv s
    /\ Some? (steps_computation actor starts_atomic_block ends_atomic_block lsteps s)
    ==> 
    (let hatomic_action_idx, hsteps = my_special_case_steps_updater_0 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))
  with introduce _ ==> _
  with _.
    let hatomic_action_idx, hsteps = my_special_case_steps_updater_0 actor lsteps s in
    list_to_array_implies_nth_equivalent hatomic_action_array MyAtomicHProg.prog.actions hatomic_action_idx;
    my_special_case_steps_updater_satisfies_weakening_0 actor starts_atomic_block ends_atomic_block
      lsteps hatomic_action_idx hsteps s
module MyProgramProof

open Armada.Action
open Armada.Base
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Transition
open Armada.Type
open FStar.List.Tot.Base
open FStar.Tactics.V2
open MyAtomicToRegularRefinement
open MyProgramInvariant
open MyRegularToAtomicRefinement
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.Weakening.Armada
open Util.Behavior
open Util.ImmutableArray
open Util.List

private let my_special_case_action_0 : list Armada.Action.t =
  [ { ok = true;
      program_statement = { start_pc = Some "main.0"; end_pc = Some "main.1"; starts_atomic_block = true;
                            ends_atomic_block = true;
                            statement = UpdateStatement false (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                          (ExpressionGlobalVariable (ObjectTDAbstract int) "f"); } } ]

private let my_special_case_action_1 : list Armada.Action.t =
  [ { ok = false;
      program_statement = { start_pc = Some "main.0"; end_pc = Some "main.1"; starts_atomic_block = true;
                            ends_atomic_block = true;
                            statement = UpdateStatement false (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                          (ExpressionGlobalVariable (ObjectTDAbstract int) "f"); } } ]

private let my_special_case_steps_updater_0
  (actor: tid_t)
  (steps: list Armada.Step.t)
  (s: Armada.State.t)
  : nat * (list Armada.Step.t) =
  let step: Armada.Step.t = {
    nd = [];
    action = {
      ok = true;
      program_statement = { start_pc = Some "main.0"; end_pc = Some "main.1"; starts_atomic_block = true;
                            ends_atomic_block = true;
                            statement = UpdateStatement false (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                          (ExpressionGlobalVariable (ObjectTDAbstract int) "g"); }
    }
  } in
  (0, [step]) // this atomic action is the 0th one in the list of MyAtomicHProg.prog.actions

private let my_special_case_steps_updater_1
  (actor: tid_t)
  (steps: list Armada.Step.t)
  (s: Armada.State.t)
  : nat * (list Armada.Step.t) =
  let step: Armada.Step.t = {
    nd = [];
    action = {
      ok = false;
      program_statement = { start_pc = Some "main.0"; end_pc = Some "main.1"; starts_atomic_block = true;
                            ends_atomic_block = true;
                            statement = UpdateStatement false (ExpressionGlobalVariable (ObjectTDAbstract int) "e")
                                          (ExpressionGlobalVariable (ObjectTDAbstract int) "g"); }
    }
  } in
  (1, [step]) // this atomic action is the 1st one in the list of MyAtomicHProg.prog.actions

#push-options "--z3rlimit 10 --fuel 4"

private let my_special_case_steps_updater_satisfies_weakening_0
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (lsteps: list Armada.Step.t)
  (haction_index: nat)
  (hsteps: list Armada.Step.t)
  (s: Armada.State.t)
  : Lemma (requires   (FStar.List.Tot.map armada_step_to_action lsteps == my_special_case_action_0)
                    /\ (my_inv s)
                    /\ (Some? (steps_computation actor starts_atomic_block ends_atomic_block lsteps s))
                    /\ ((haction_index, hsteps) == my_special_case_steps_updater_0 actor lsteps s))
          (ensures  (  (Some? (steps_computation actor starts_atomic_block ends_atomic_block hsteps s))
                     /\ (steps_computation actor starts_atomic_block ends_atomic_block lsteps s ==
                        steps_computation actor starts_atomic_block ends_atomic_block hsteps s)
                     /\ nth MyAtomicHProg.prog.actions haction_index ==
                         Some (map_ghost armada_step_to_action hsteps))) =
  ()

private let my_special_case_steps_updater_satisfies_weakening_1
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (lsteps: list Armada.Step.t)
  (haction_index: nat)
  (hsteps: list Armada.Step.t)
  (s: Armada.State.t)
  : Lemma (requires   (FStar.List.Tot.map armada_step_to_action lsteps == my_special_case_action_1)
                    /\ (my_inv s)
                    /\ (Some? (steps_computation actor starts_atomic_block ends_atomic_block lsteps s))
                    /\ ((haction_index, hsteps) == my_special_case_steps_updater_1 actor lsteps s))
          (ensures  (  (Some? (steps_computation actor starts_atomic_block ends_atomic_block hsteps s))
                     /\ (steps_computation actor starts_atomic_block ends_atomic_block lsteps s ==
                        steps_computation actor starts_atomic_block ends_atomic_block hsteps s)
                     /\ nth MyAtomicHProg.prog.actions haction_index ==
                         Some (map_ghost armada_step_to_action hsteps))) =
  ()

#pop-options
/
Util.List.fst.checked Util.ImmutableArray.fsti.checked Util.Behavior.fst.checked Strategies.Weakening.Armada.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 MyRegularToAtomicRefinement.fst.checked MyProgramInvariant.fst.checked MyLProg.fst.checked MyHProg.fst.checked MyAtomicToRegularRefinement.fst.checked MyAtomicLProg.fst.checked MyAtomicHProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
MyProgramProof.fst
_: Prims.unit
  -> Prims.squash (Strategies.Weakening.Armada.armada_steps_updater_works (Util.ImmutableArray.list_to_array
              (Mkprogram_t?.actions MyAtomicHProg.prog))
          MyProgramInvariant.my_inv
          MyProgramProof.my_special_case_action_0
          MyProgramProof.my_special_case_steps_updater_0)
Prims.unit FStar.Classical.Sugar.forall_intro Armada.Base.tid_t Prims.l_Forall Prims.bool Prims.list Armada.Step.t Armada.State.t Prims.l_imp Prims.l_and Prims.eq2 Armada.Action.t Util.List.map_ghost Strategies.Semantics.Armada.armada_step_to_action MyProgramProof.my_special_case_action_0 MyProgramInvariant.my_inv Prims.b2t FStar.Pervasives.Native.uu___is_Some Armada.Transition.steps_computation Prims.nat Prims.op_LessThan Util.ImmutableArray.array_len Strategies.Semantics.__proj__Mksemantics_t__item__action_t MyAtomicHProg.atomic_semantics Strategies.Semantics.Armada.armada_semantics Util.ImmutableArray.array_index FStar.Pervasives.Native.option Prims.logical FStar.Pervasives.Native.tuple2 MyProgramProof.my_special_case_steps_updater_0 FStar.Classical.Sugar.implies_intro Prims.squash MyProgramProof.my_special_case_steps_updater_satisfies_weakening_0 Util.ImmutableArray.list_to_array_implies_nth_equivalent Strategies.Semantics.__proj__Mkprogram_t__item__actions MyAtomicHProg.prog FStar.ImmutableArray.Base.t Util.ImmutableArray.list_to_array Strategies.Weakening.Armada.armada_steps_updater_works
let my_special_case_steps_updater_works_0 ()
    : squash (armada_steps_updater_works (list_to_array MyAtomicHProg.prog.actions)
          my_inv
          my_special_case_action_0
          my_special_case_steps_updater_0) =
  
let hatomic_action_array = list_to_array MyAtomicHProg.prog.actions in
introduce 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 ==
my_special_case_action_0 /\ my_inv s /\
Some? (steps_computation actor starts_atomic_block ends_atomic_block lsteps s) ==>
(let hatomic_action_idx, hsteps = my_special_case_steps_updater_0 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))
with introduce _ ==> _
with _. let hatomic_action_idx, hsteps = my_special_case_steps_updater_0 actor lsteps s in
list_to_array_implies_nth_equivalent hatomic_action_array
  MyAtomicHProg.prog.actions
  hatomic_action_idx;
my_special_case_steps_updater_satisfies_weakening_0 actor
  starts_atomic_block
  ends_atomic_block
  lsteps
  hatomic_action_idx
  hsteps
  s