val lift_step_using_weakening_transformer
      (wr: weakening_relation_t)
      (actor: wr.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (lstep: wr.sem.step_t)
      (s: wr.sem.state_t)
      (laction: wr.sem.action_t)
      (weakening_transformer: weakening_transformer_t wr.sem wr.hprog.actions wr.inv)
    : Ghost wr.sem.step_t
      (requires
        wr.inv s /\
        (Some? (step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s)
        ) /\ (program_contains_action_of_step_generic wr.sem wr.lprog lstep) /\
        (wr.sem.step_to_action_f lstep == laction) /\
        (action_matches_weakening_transformer laction weakening_transformer))
      (ensures
        fun hstep ->
          (Some? (step_computation_generic wr.sem
                  actor
                  starts_atomic_block
                  ends_atomic_block
                  hstep
                  s)) /\
          step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s ==
          step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s /\
          wr.inv (Some?.v (step_computation_generic wr.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    lstep
                    s)) /\ (program_contains_action_of_step_generic wr.sem wr.hprog hstep))
val lift_step_using_weakening_transformer
      (wr: weakening_relation_t)
      (actor: wr.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (lstep: wr.sem.step_t)
      (s: wr.sem.state_t)
      (laction: wr.sem.action_t)
      (weakening_transformer: weakening_transformer_t wr.sem wr.hprog.actions wr.inv)
    : Ghost wr.sem.step_t
      (requires
        wr.inv s /\
        (Some? (step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s)
        ) /\ (program_contains_action_of_step_generic wr.sem wr.lprog lstep) /\
        (wr.sem.step_to_action_f lstep == laction) /\
        (action_matches_weakening_transformer laction weakening_transformer))
      (ensures
        fun hstep ->
          (Some? (step_computation_generic wr.sem
                  actor
                  starts_atomic_block
                  ends_atomic_block
                  hstep
                  s)) /\
          step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s ==
          step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s /\
          wr.inv (Some?.v (step_computation_generic wr.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    lstep
                    s)) /\ (program_contains_action_of_step_generic wr.sem wr.hprog hstep))
let lift_step_using_weakening_transformer
  (wr: weakening_relation_t)
  (actor: wr.sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (lstep: wr.sem.step_t)
  (s: wr.sem.state_t)
  (laction: wr.sem.action_t)
  (weakening_transformer: weakening_transformer_t wr.sem wr.hprog.actions wr.inv)
  : Ghost wr.sem.step_t
    (requires   wr.inv s
              /\ (Some? (step_computation_generic wr.sem actor
                          starts_atomic_block ends_atomic_block lstep s))
              /\ (program_contains_action_of_step_generic wr.sem wr.lprog lstep)
              /\ (wr.sem.step_to_action_f lstep == laction)
              /\ (action_matches_weakening_transformer laction weakening_transformer))
    (ensures  fun hstep ->   (Some? (step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s))
                        /\ step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s ==
                            step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s
                        /\ wr.inv (Some?.v (step_computation_generic wr.sem actor
                                             starts_atomic_block ends_atomic_block lstep s))
                        /\ (program_contains_action_of_step_generic wr.sem wr.hprog hstep)) =
  match weakening_transformer with
  | WeakeningTransformerSameStep _ ->
     lift_step_case_same_step wr actor starts_atomic_block ends_atomic_block lstep s laction weakening_transformer
  | WeakeningTransformerUpdatedStep _ _ _ ->
     lift_step_case_updated_step wr actor starts_atomic_block ends_atomic_block lstep s laction weakening_transformer
module Strategies.Weakening

open FStar.WellFoundedRelation
open Spec.Behavior
open Strategies.Semantics
open Spec.Ubool
open Spec.List
open Strategies.Lift.Generic
open Util.Behavior
open Util.List
open Util.Nth

let lift_step_case_same_step
  (wr: weakening_relation_t)
  (actor: wr.sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (lstep: wr.sem.step_t)
  (s: wr.sem.state_t)
  (laction: wr.sem.action_t)
  (weakening_transformer: weakening_transformer_t wr.sem wr.hprog.actions wr.inv)
  : Ghost wr.sem.step_t
    (requires   wr.inv s
              /\ (Some? (step_computation_generic wr.sem actor
                          starts_atomic_block ends_atomic_block lstep s))
              /\ (program_contains_action_of_step_generic wr.sem wr.lprog lstep)
              /\ (wr.sem.step_to_action_f lstep == laction)
              /\ (action_matches_weakening_transformer laction weakening_transformer)
              /\ (WeakeningTransformerSameStep? weakening_transformer))
    (ensures  fun hstep ->   (Some? (step_computation_generic wr.sem actor
                                    starts_atomic_block ends_atomic_block lstep s))
                        /\ step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s ==
                            step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s
                        /\ wr.inv (Some?.v (step_computation_generic wr.sem actor
                                             starts_atomic_block ends_atomic_block lstep s))
                        /\ (program_contains_action_of_step_generic wr.sem wr.hprog hstep)) =
  wr.sem_has_stepwise_inductive_invariant_proof ();
  let haction_index = (WeakeningTransformerSameStep?.haction_index weakening_transformer) in
  let haction = Some?.v (nth wr.hprog.actions haction_index) in
  nth_implies_contains_ubool wr.hprog.actions haction_index haction;
  lstep
  
let lift_step_case_updated_step
  (wr: weakening_relation_t)
  (actor: wr.sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (lstep: wr.sem.step_t)
  (s: wr.sem.state_t)
  (laction: wr.sem.action_t)
  (weakening_transformer: weakening_transformer_t wr.sem wr.hprog.actions wr.inv)
  : Ghost wr.sem.step_t
    (requires   wr.inv s
              /\ (Some? (step_computation_generic wr.sem actor
                          starts_atomic_block ends_atomic_block lstep s))
              /\ (program_contains_action_of_step_generic wr.sem wr.lprog lstep)
              /\ (wr.sem.step_to_action_f lstep == laction)
              /\ (action_matches_weakening_transformer laction weakening_transformer)
              /\ WeakeningTransformerUpdatedStep? weakening_transformer)
    (ensures  fun hstep ->   (Some? (step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s))
                        /\ step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s ==
                            step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s
                        /\ wr.inv (Some?.v (step_computation_generic wr.sem actor
                                             starts_atomic_block ends_atomic_block lstep s))
                        /\ (program_contains_action_of_step_generic wr.sem wr.hprog hstep)) =
  wr.sem_has_stepwise_inductive_invariant_proof ();
  match weakening_transformer with
  | WeakeningTransformerUpdatedStep _ step_updater proof ->
      proof ();
      step_updater actor lstep s
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.fst.checked Strategies.Lift.Generic.fsti.checked Spec.Ubool.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.WellFoundedRelation.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Strategies.Weakening.fst

    wr: Strategies.Weakening.weakening_relation_t ->
    actor: Mksemantics_t?.actor_t (Mkweakening_relation_t?.sem wr) ->
    starts_atomic_block: Prims.bool ->
    ends_atomic_block: Prims.bool ->
    lstep: Mksemantics_t?.step_t (Mkweakening_relation_t?.sem wr) ->
    s: Mksemantics_t?.state_t (Mkweakening_relation_t?.sem wr) ->
    laction: Mksemantics_t?.action_t (Mkweakening_relation_t?.sem wr) ->
    weakening_transformer:
      Strategies.Weakening.weakening_transformer_t (Mkweakening_relation_t?.sem wr)
        (Mkprogram_t?.actions (Mkweakening_relation_t?.hprog wr))
        (Mkweakening_relation_t?.inv wr)
  -> Prims.Ghost (Mksemantics_t?.step_t (Mkweakening_relation_t?.sem wr))
Strategies.Weakening.weakening_relation_t Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Strategies.Weakening.__proj__Mkweakening_relation_t__item__sem Prims.bool Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.Weakening.weakening_transformer_t Strategies.Semantics.__proj__Mkprogram_t__item__actions Strategies.Weakening.__proj__Mkweakening_relation_t__item__hprog Strategies.Weakening.__proj__Mkweakening_relation_t__item__inv Prims.nat Strategies.Weakening.lift_step_case_same_step Prims.unit Prims.squash Prims.b2t Strategies.Weakening.step_updater_works Strategies.Weakening.lift_step_case_updated_step Prims.l_and FStar.Pervasives.Native.uu___is_Some Strategies.Semantics.step_computation_generic Strategies.Semantics.program_contains_action_of_step_generic Strategies.Weakening.__proj__Mkweakening_relation_t__item__lprog Prims.eq2 Strategies.Semantics.__proj__Mksemantics_t__item__step_to_action_f Strategies.Weakening.action_matches_weakening_transformer FStar.Pervasives.Native.option FStar.Pervasives.Native.__proj__Some__item__v
let lift_step_using_weakening_transformer
      (wr: weakening_relation_t)
      (actor: wr.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (lstep: wr.sem.step_t)
      (s: wr.sem.state_t)
      (laction: wr.sem.action_t)
      (weakening_transformer: weakening_transformer_t wr.sem wr.hprog.actions wr.inv)
    : Ghost wr.sem.step_t
      (requires
        wr.inv s /\
        (Some? (step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s)
        ) /\ (program_contains_action_of_step_generic wr.sem wr.lprog lstep) /\
        (wr.sem.step_to_action_f lstep == laction) /\
        (action_matches_weakening_transformer laction weakening_transformer))
      (ensures
        fun hstep ->
          (Some? (step_computation_generic wr.sem
                  actor
                  starts_atomic_block
                  ends_atomic_block
                  hstep
                  s)) /\
          step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block hstep s ==
          step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep s /\
          wr.inv (Some?.v (step_computation_generic wr.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    lstep
                    s)) /\ (program_contains_action_of_step_generic wr.sem wr.hprog hstep)) =
  
match weakening_transformer with
| WeakeningTransformerSameStep _ ->
  lift_step_case_same_step wr
    actor
    starts_atomic_block
    ends_atomic_block
    lstep
    s
    laction
    weakening_transformer
| WeakeningTransformerUpdatedStep _ _ _ ->
  lift_step_case_updated_step wr
    actor
    starts_atomic_block
    ends_atomic_block
    lstep
    s
    laction
    weakening_transformer