val armada_next_equivalent (program: Armada.Program.t) (s s': Armada.State.t)
    : Lemma
    ((program_to_spec program).next s s' <==>
      (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s')
val armada_next_equivalent (program: Armada.Program.t) (s s': Armada.State.t)
    : Lemma
    ((program_to_spec program).next s s' <==>
      (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s')
let armada_next_equivalent (program: Armada.Program.t) (s s': Armada.State.t)
  : Lemma ((program_to_spec program).next s s' <==>
           (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s') =
  introduce (program_to_spec program).next s s' ==>
            (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s'
  with knowing_program_next. (
    eliminate exists transition. Armada.Program.next_program program transition s s'
    returns   _
    with knowing_transition_satisfies_next_program.
      armada_next_program_equivalent_forward program transition s s'
  );
  introduce (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s' ==>
            (program_to_spec program).next s s'
  with knowing_semantics_next. (
    eliminate exists transition. next_program_generic armada_semantics
                              (armada_program_to_generic program) transition s s'
    returns   _
    with knowing_transition_satisfies_next_program.
      armada_next_program_equivalent_backward program transition s s'
  )
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')

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

let generic_transition_to_armada (transition: transition_t armada_semantics) : Armada.Transition.t =
  { actor = transition.actor; steps = transition.steps; }

let armada_next_transition_equivalent_forward
  (program: Armada.Program.t)
  (transition: Armada.Transition.t)
  (s s': Armada.State.t)
  : Lemma (requires Armada.Transition.next_transition transition s s')
          (ensures  next_transition_generic armada_semantics (armada_transition_to_generic transition) s s') =
  let sem = armada_semantics in
  armada_steps_computation_equivalent transition.actor true true transition.steps s

let armada_next_transition_equivalent_backward
  (transition: transition_t armada_semantics)
  (s s': Armada.State.t)
  : Lemma (requires next_transition_generic armada_semantics transition s s')
          (ensures  Armada.Transition.next_transition (generic_transition_to_armada transition) s s') =
  armada_steps_computation_equivalent transition.actor true true transition.steps s

let armada_next_program_equivalent_forward
  (program: Armada.Program.t)
  (transition: Armada.Transition.t)
  (s s': Armada.State.t)
  : Lemma (requires Armada.Program.next_program program transition s s')
          (ensures  next_program_generic armada_semantics (armada_program_to_generic program)
                     (armada_transition_to_generic transition) s s') =
  let lem (step: Armada.Step.t)
    : Lemma (requires program_contains_statement_of_step program step)
            (ensures  program_contains_action_of_step_generic armada_semantics
                        (armada_program_to_generic program) step) =
    all_actions_has_all_actions step.action program.program_statements in
  for_all_ubool_implication lem transition.steps;
  armada_next_transition_equivalent_forward program transition s s'

let armada_next_program_equivalent_backward
  (program: Armada.Program.t)
  (transition: transition_t armada_semantics)
  (s s': Armada.State.t)
  : Lemma (requires next_program_generic armada_semantics (armada_program_to_generic program) transition s s')
          (ensures  Armada.Program.next_program program (generic_transition_to_armada transition) s s') =
  let lem (step: Armada.Step.t)
    : Lemma (requires program_contains_action_of_step_generic armada_semantics
               (armada_program_to_generic program) step)
            (ensures  program_contains_statement_of_step program step) =
    all_actions_has_all_actions step.action program.program_statements in
  for_all_ubool_implication lem transition.steps;
  armada_next_transition_equivalent_backward transition s 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
program: Armada.Program.t -> s: Armada.State.t -> s': Armada.State.t
  -> FStar.Pervasives.Lemma
    (ensures
      Mkspec_t?.next (Armada.Program.program_to_spec program) s s' <==>
      Mkspec_t?.next (Strategies.Semantics.semantics_to_spec Strategies.Semantics.Armada.armada_semantics
            (Strategies.Semantics.Armada.armada_program_to_generic program))
        s
        s')
Armada.Program.t Armada.State.t FStar.Classical.Sugar.implies_intro Spec.Behavior.__proj__Mkspec_t__item__next Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.Armada.armada_semantics Strategies.Semantics.semantics_to_spec Strategies.Semantics.Armada.armada_program_to_generic Prims.squash Armada.Program.program_to_spec FStar.Classical.Sugar.exists_elim Strategies.Semantics.transition_t Strategies.Semantics.next_program_generic Strategies.Semantics.Armada.armada_next_program_equivalent_backward Prims.unit Armada.Transition.t Armada.Program.next_program Strategies.Semantics.Armada.armada_next_program_equivalent_forward Prims.l_True Prims.l_iff Prims.Nil FStar.Pervasives.pattern
let armada_next_equivalent (program: Armada.Program.t) (s s': Armada.State.t)
    : Lemma
    ((program_to_spec program).next s s' <==>
      (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s') =
  
introduce (program_to_spec program).next s s' ==> (semantics_to_spec armada_semantics
    (armada_program_to_generic program))
  .next s
  s'
with knowing_program_next. (eliminate exists transition.
  Armada.Program.next_program program transition s s'
  returns _
  with knowing_transition_satisfies_next_program.
  armada_next_program_equivalent_forward program transition s s');
introduce (semantics_to_spec armada_semantics (armada_program_to_generic program)).next s s' ==> (program_to_spec
    program)
  .next s
  s'
with knowing_semantics_next. (eliminate exists transition.
  next_program_generic armada_semantics (armada_program_to_generic program) transition s s'
  returns _
  with knowing_transition_satisfies_next_program.
  armada_next_program_equivalent_backward program transition s s')