val armada_weakening_witness_valid_implies_refinement
  (lprog: program_t (make_atomic_semantics armada_semantics))
  (hprog: program_t (make_atomic_semantics armada_semantics))
  (ww: armada_weakening_witness_t lprog hprog)
  : Lemma (requires   ww.hatomic_action_array == list_to_array hprog.actions
                    /\ semantics_has_stepwise_inductive_invariant (make_atomic_semantics armada_semantics) lprog ww.inv
                    /\ armada_weakening_witness_valid lprog hprog ww)
          (ensures  spec_refines_spec
                      (semantics_to_spec (make_atomic_semantics armada_semantics) lprog)
                      (semantics_to_spec (make_atomic_semantics armada_semantics) hprog)
                      eq2)
val armada_weakening_witness_valid_implies_refinement
  (lprog: program_t (make_atomic_semantics armada_semantics))
  (hprog: program_t (make_atomic_semantics armada_semantics))
  (ww: armada_weakening_witness_t lprog hprog)
  : Lemma (requires   ww.hatomic_action_array == list_to_array hprog.actions
                    /\ semantics_has_stepwise_inductive_invariant (make_atomic_semantics armada_semantics) lprog ww.inv
                    /\ armada_weakening_witness_valid lprog hprog ww)
          (ensures  spec_refines_spec
                      (semantics_to_spec (make_atomic_semantics armada_semantics) lprog)
                      (semantics_to_spec (make_atomic_semantics armada_semantics) hprog)
                      eq2)
let armada_weakening_witness_valid_implies_refinement
  (lprog: program_t (make_atomic_semantics armada_semantics))
  (hprog: program_t (make_atomic_semantics armada_semantics))
  (ww: armada_weakening_witness_t lprog hprog)
  (* see .fsti file for spec *) =
  armada_weakening_witness_valid_implies_actions_match_weakening_transformers lprog hprog ww;
  let wr: weakening_relation_t = {
    sem = make_atomic_semantics armada_semantics;
    lprog = lprog;
    hprog = hprog;
    inv = ww.inv;
    weakening_transformers = armada_weakening_transformers_to_weakening_transformers hprog.actions
                               ww.hatomic_action_array ww.inv ww.weakening_transformers;
    sem_has_stepwise_inductive_invariant_proof = (fun _ -> ());
    actions_match_weakening_transformers_proof = (fun _ -> ());
    init_implies_init_proof = ww.init_implies_init_proof;
  } in
  weakening_relation_implies_refinement wr
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 FStar.Tactics.V2
open Spec.Behavior
open Strategies.Atomic
open Strategies.Invariant
open Strategies.Invariant.Armada.Atomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.Weakening
open Spec.List
open Spec.Ubool
open Util.List

let remove_index_from_steps_updater
  (u:(tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
  (tid: tid_t)
  (lsteps: list Armada.Step.t)
  (ls: Armada.State.t)
  : GTot (list Armada.Step.t) =
  let idx, steps = u tid lsteps ls in
  steps

let armada_steps_updater_works_implies_step_updater_works
  (lactions: list Armada.Action.t)
  (hatomic_actions: list (list Armada.Action.t))
  (hatomic_action_array: array_t (list Armada.Action.t))
  (inv: invariant_t Armada.State.t)
  (steps_updater: (tid_t -> list Armada.Step.t -> Armada.State.t -> GTot (nat * list Armada.Step.t)))
  (proof: unit -> squash (armada_steps_updater_works hatomic_action_array inv lactions steps_updater))
  : Lemma (requires hatomic_action_array == list_to_array hatomic_actions)
          (ensures  step_updater_works (make_atomic_semantics armada_semantics) hatomic_actions inv lactions
                      (remove_index_from_steps_updater steps_updater)) =
  let sem = make_atomic_semantics armada_semantics in
  introduce forall (actor: sem.actor_t) (starts_atomic_block: bool) (ends_atomic_block: bool) (lsteps: sem.step_t)
              (s: sem.state_t).
              (  sem.step_to_action_f lsteps == lactions
               /\ inv s
               /\ Some? (step_computation_generic sem actor starts_atomic_block ends_atomic_block lsteps s)) ==>
              (let hatomic_action_idx, hsteps = steps_updater actor lsteps s in
               let hactions = sem.step_to_action_f hsteps in
                 (contains_ubool hactions hatomic_actions)
               /\ (step_computation_generic sem actor starts_atomic_block ends_atomic_block hsteps s ==
                  step_computation_generic sem actor starts_atomic_block ends_atomic_block lsteps s))
  with introduce _ ==> _
  with _. (
    proof ();
    armada_steps_computation_equivalent actor starts_atomic_block ends_atomic_block lsteps s;
    let hatomic_action_idx, hsteps = steps_updater actor lsteps s in
    armada_steps_computation_equivalent actor starts_atomic_block ends_atomic_block hsteps s;
    let hactions = sem.step_to_action_f hsteps in
    index_to_contains_ubool hatomic_actions hatomic_action_idx
  )

let armada_weakening_transformer_to_weakening_transformer
  (hatomic_actions: list (list Armada.Action.t))
  (hatomic_action_array: array_t (list Armada.Action.t){hatomic_action_array == list_to_array hatomic_actions})
  (inv: invariant_t Armada.State.t)
  (awt: armada_weakening_transformer_t hatomic_action_array inv)
  : GTot (weakening_transformer_t (make_atomic_semantics armada_semantics) hatomic_actions inv) =
  match awt with
  | ArmadaWeakeningTransformerSameStep hatomic_action_idx -> WeakeningTransformerSameStep hatomic_action_idx
  | ArmadaWeakeningTransformerUpdatedStep lactions step_updater proof ->
      armada_steps_updater_works_implies_step_updater_works lactions hatomic_actions hatomic_action_array inv
        step_updater proof;
      WeakeningTransformerUpdatedStep lactions (remove_index_from_steps_updater step_updater) (fun _ -> ())

let armada_weakening_transformers_to_weakening_transformers
  (hatomic_actions: list (list Armada.Action.t))
  (hatomic_action_array: array_t (list Armada.Action.t){hatomic_action_array == list_to_array hatomic_actions})
  (inv: invariant_t Armada.State.t)
  (awts: list (armada_weakening_transformer_t hatomic_action_array inv))
  : GTot (list (weakening_transformer_t (make_atomic_semantics armada_semantics) hatomic_actions inv)) =
  map_ghost (armada_weakening_transformer_to_weakening_transformer hatomic_actions hatomic_action_array inv) awts

let armada_weakening_witness_valid_implies_actions_match_weakening_transformers
  (lprog: program_t (make_atomic_semantics armada_semantics))
  (hprog: program_t (make_atomic_semantics armada_semantics))
  (ww: armada_weakening_witness_t lprog hprog)
  : Lemma (requires    ww.hatomic_action_array == list_to_array hprog.actions
                    /\ lists_correspond_ubool action_matches_armada_weakening_transformer lprog.actions
                        ww.weakening_transformers)
          (ensures  lists_correspond_ubool action_matches_weakening_transformer lprog.actions
                      (armada_weakening_transformers_to_weakening_transformers hprog.actions ww.hatomic_action_array
                         ww.inv ww.weakening_transformers)) =
  introduce forall lactions weakening_transformer.
                action_matches_armada_weakening_transformer lactions weakening_transformer ==>
                  action_matches_weakening_transformer lactions
                    (armada_weakening_transformer_to_weakening_transformer hprog.actions
                      ww.hatomic_action_array ww.inv weakening_transformer)
  with introduce _ ==> _
  with _. (
    let weakening_transformer = armada_weakening_transformer_to_weakening_transformer hprog.actions
                                  ww.hatomic_action_array ww.inv weakening_transformer in
    match weakening_transformer with
    | WeakeningTransformerSameStep haction_index ->
        list_to_array_implies_nth_equivalent ww.hatomic_action_array hprog.actions haction_index
    | WeakeningTransformerUpdatedStep action _ _ ->
        assert (lactions == action)
  );
  map_preserves_lists_correspond_ubool
    action_matches_armada_weakening_transformer
    action_matches_weakening_transformer
    (armada_weakening_transformer_to_weakening_transformer hprog.actions ww.hatomic_action_array ww.inv)
    lprog.actions ww.weakening_transformers
/
Util.List.fst.checked Strategies.Weakening.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.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.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.fst

    lprog:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    hprog:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    ww: Strategies.Weakening.Armada.armada_weakening_witness_t lprog hprog
  -> FStar.Pervasives.Lemma
      (requires
        Mkarmada_weakening_witness_t?.hatomic_action_array ww ==
        Util.ImmutableArray.list_to_array (Mkprogram_t?.actions hprog) /\
        Strategies.Invariant.semantics_has_stepwise_inductive_invariant (Strategies.Atomic.make_atomic_semantics
              Strategies.Semantics.Armada.armada_semantics)
          lprog
          (Mkarmada_weakening_witness_t?.inv ww) /\
        Strategies.Weakening.Armada.armada_weakening_witness_valid lprog hprog ww)
      (ensures
        Spec.Behavior.spec_refines_spec (Strategies.Semantics.semantics_to_spec (Strategies.Atomic.make_atomic_semantics
                  Strategies.Semantics.Armada.armada_semantics)
              lprog)
          (Strategies.Semantics.semantics_to_spec (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
                )
              hprog)
          Prims.eq2)
Strategies.Semantics.program_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.Weakening.Armada.armada_weakening_witness_t Strategies.Weakening.weakening_relation_implies_refinement Strategies.Weakening.weakening_relation_t Strategies.Weakening.Mkweakening_relation_t Strategies.Weakening.Armada.__proj__Mkarmada_weakening_witness_t__item__inv Strategies.Weakening.Armada.armada_weakening_transformers_to_weakening_transformers Strategies.Semantics.__proj__Mkprogram_t__item__actions Strategies.Weakening.Armada.__proj__Mkarmada_weakening_witness_t__item__hatomic_action_array Strategies.Weakening.Armada.__proj__Mkarmada_weakening_witness_t__item__weakening_transformers Prims.unit Prims.squash Strategies.Invariant.semantics_has_stepwise_inductive_invariant Util.List.lists_correspond_ubool Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.Weakening.weakening_transformer_t Strategies.Weakening.action_matches_weakening_transformer Strategies.Weakening.Armada.__proj__Mkarmada_weakening_witness_t__item__init_implies_init_proof Strategies.Weakening.Armada.armada_weakening_witness_valid_implies_actions_match_weakening_transformers
let armada_weakening_witness_valid_implies_refinement
      (lprog hprog: program_t (make_atomic_semantics armada_semantics))
      (ww: armada_weakening_witness_t lprog hprog)
     =
  
armada_weakening_witness_valid_implies_actions_match_weakening_transformers lprog hprog ww;
let wr:weakening_relation_t =
  {
    sem = make_atomic_semantics armada_semantics;
    lprog = lprog;
    hprog = hprog;
    inv = ww.inv;
    weakening_transformers
    =
    armada_weakening_transformers_to_weakening_transformers hprog.actions
      ww.hatomic_action_array
      ww.inv
      ww.weakening_transformers;
    sem_has_stepwise_inductive_invariant_proof = (fun _ -> ());
    actions_match_weakening_transformers_proof = (fun _ -> ());
    init_implies_init_proof = ww.init_implies_init_proof
  }
in
weakening_relation_implies_refinement wr