val armada_transition_to_generic (transition: Armada.Transition.t) : transition_t armada_semantics
val armada_transition_to_generic (transition: Armada.Transition.t) : transition_t armada_semantics
let armada_transition_to_generic (transition: Armada.Transition.t) : transition_t armada_semantics =
  { actor = transition.actor; steps = transition.steps; }
module Strategies.Semantics.Armada

open Armada.Action
open Armada.Step
open Armada.Program
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Strategies.Semantics
open Util.Behavior
open Util.List

let rec all_actions_has_all_actions
  (action: Armada.Action.t)
  (program_statements: list program_statement_t)
  : Lemma (contains_ubool action.program_statement program_statements <==>
             (contains_ubool action (all_actions program_statements))) =
  match program_statements with
  | [] -> ()
  | hd :: tl -> if eqb hd action.program_statement then () else all_actions_has_all_actions action tl

let armada_state_satisfies_init_equivalent (program: Armada.Program.t) (s: Armada.State.t)
  : Lemma ((program_to_spec program).init s <==>
           (semantics_to_spec armada_semantics (armada_program_to_generic program)).init s) =
  ()

let rec armada_steps_computation_equivalent
  (actor: tid_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (steps: list Armada.Step.t)
  (s: Armada.State.t)
  : Lemma (ensures  steps_computation actor starts_atomic_block ends_atomic_block steps s ==
                    steps_computation_generic armada_semantics actor starts_atomic_block ends_atomic_block
                      steps s)
          (decreases steps) =
  match steps with
  | [] -> ()
  | [last_step] -> ()
  | first_step :: remaining_steps ->
      (match step_computation actor starts_atomic_block false first_step s with
       | None -> ()
       | Some s' -> armada_steps_computation_equivalent actor false ends_atomic_block remaining_steps s')
/
Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Step.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Action.fst.checked
Strategies.Semantics.Armada.fst
transition: Armada.Transition.t
  -> Strategies.Semantics.transition_t Strategies.Semantics.Armada.armada_semantics
Armada.Transition.t Strategies.Semantics.Mktransition_t Strategies.Semantics.Armada.armada_semantics Armada.Transition.__proj__Mkt__item__actor Armada.Transition.__proj__Mkt__item__steps Strategies.Semantics.transition_t
let armada_transition_to_generic (transition: Armada.Transition.t) : transition_t armada_semantics =
  
{ actor = transition.actor; steps = transition.steps }