val lemma_MyAtomicHProg_refines_MyHProg: Prims.unit
  -> Lemma
    (ensures
      spec_refines_spec (semantics_to_spec (make_atomic_semantics armada_semantics)
            MyAtomicHProg.prog)
        (program_to_spec MyHProg.prog)
        eq2)
val lemma_MyAtomicHProg_refines_MyHProg: Prims.unit
  -> Lemma
    (ensures
      spec_refines_spec (semantics_to_spec (make_atomic_semantics armada_semantics)
            MyAtomicHProg.prog)
        (program_to_spec MyHProg.prog)
        eq2)
let lemma_MyAtomicHProg_refines_MyHProg ()
  : Lemma (ensures spec_refines_spec
                     (semantics_to_spec (make_atomic_semantics armada_semantics) MyAtomicHProg.prog)
                     (program_to_spec MyHProg.prog)
                     eq2) =
  let aw: atomic_refines_armada_witness_t = {
    atomic_to_regular_map = my_atomic_to_regular_map;
    actions_array = list_to_array (all_actions MyHProg.prog.program_statements)
  } in
  assert (atomic_refines_armada_witness_valid MyAtomicHProg.prog MyHProg.prog aw)
    by (compute(); trivial());
  atomic_refines_armada_witness_valid_implies_refinement MyAtomicHProg.prog MyHProg.prog aw
module MyAtomicToRegularRefinement

open Armada.Action
open Armada.BinaryOp
open Armada.Expression
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Type
open FStar.Tactics.V2
open Spec.Behavior
open Spec.List
open Spec.Ubool
open Strategies.Atomic
open Strategies.AtomicToRegular.Armada
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.Nth

let my_atomic_to_regular_map: (list (list nat)) =
  [[0]; [1]; [2; 4; 6]; [3]; [2; 5]; [2; 4; 7]; [8]; [9]]
/
Util.Nth.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.AtomicToRegular.Armada.fsti.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked MyHProg.fst.checked MyAtomicHProg.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Expression.fst.checked Armada.BinaryOp.fst.checked Armada.Action.fst.checked
MyAtomicToRegularRefinement.fst
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Behavior.spec_refines_spec (Strategies.Semantics.semantics_to_spec (Strategies.Atomic.make_atomic_semantics
                Strategies.Semantics.Armada.armada_semantics)
            MyAtomicHProg.prog)
        (Armada.Program.program_to_spec MyHProg.prog)
        Prims.eq2)
Prims.unit Strategies.AtomicToRegular.Armada.atomic_refines_armada_witness_valid_implies_refinement MyAtomicHProg.prog MyHProg.prog FStar.Tactics.Effect.assert_by_tactic Strategies.AtomicToRegular.Armada.atomic_refines_armada_witness_valid FStar.Tactics.V2.Derived.trivial FStar.Tactics.V2.Derived.compute Strategies.AtomicToRegular.Armada.atomic_refines_armada_witness_t Strategies.AtomicToRegular.Armada.Mkatomic_refines_armada_witness_t MyAtomicToRegularRefinement.my_atomic_to_regular_map Util.ImmutableArray.list_to_array Armada.Action.t Strategies.Semantics.Armada.all_actions Armada.Program.__proj__Mkt__item__program_statements Prims.l_True Prims.squash Spec.Behavior.spec_refines_spec Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Armada.State.t Strategies.Semantics.semantics_to_spec Armada.Program.program_to_spec Prims.eq2 Prims.Nil FStar.Pervasives.pattern
let lemma_MyAtomicHProg_refines_MyHProg ()
    : Lemma
    (ensures
      spec_refines_spec (semantics_to_spec (make_atomic_semantics armada_semantics)
            MyAtomicHProg.prog)
        (program_to_spec MyHProg.prog)
        eq2) =
  
let aw:atomic_refines_armada_witness_t =
  {
    atomic_to_regular_map = my_atomic_to_regular_map;
    actions_array = list_to_array (all_actions MyHProg.prog.program_statements)
  }
in
FStar.Tactics.Effect.assert_by_tactic (atomic_refines_armada_witness_valid MyAtomicHProg.prog
      MyHProg.prog
      aw)
  (fun _ ->
      ();
      (compute ();
        trivial ()));
atomic_refines_armada_witness_valid_implies_refinement MyAtomicHProg.prog MyHProg.prog aw