val paths_liftable_proof_gen
      (wr: weakening_relation_t)
      (actor: wr.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (aux: unit)
      (ls hs: wr.sem.state_t)
      (lstep:
          wr.sem.step_t
            { wr.inv ls /\ (lh_relation_gen wr) aux ls hs /\
              Some? (step_computation_generic wr.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    lstep
                    ls) /\ program_contains_action_of_step_generic wr.sem wr.lprog lstep })
    : GTot
    (lifter:
      (step_lifter_t wr.sem.step_t unit)
        { step_lifter_works wr.sem wr.sem wr.lprog wr.hprog unit (lh_relation_gen wr) nat
            (default_wfr nat) (progress_measure_gen wr) actor starts_atomic_block ends_atomic_block
            lstep ls hs lifter })
val paths_liftable_proof_gen
      (wr: weakening_relation_t)
      (actor: wr.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (aux: unit)
      (ls hs: wr.sem.state_t)
      (lstep:
          wr.sem.step_t
            { wr.inv ls /\ (lh_relation_gen wr) aux ls hs /\
              Some? (step_computation_generic wr.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    lstep
                    ls) /\ program_contains_action_of_step_generic wr.sem wr.lprog lstep })
    : GTot
    (lifter:
      (step_lifter_t wr.sem.step_t unit)
        { step_lifter_works wr.sem wr.sem wr.lprog wr.hprog unit (lh_relation_gen wr) nat
            (default_wfr nat) (progress_measure_gen wr) actor starts_atomic_block ends_atomic_block
            lstep ls hs lifter })
let paths_liftable_proof_gen
  (wr: weakening_relation_t)
  (actor: wr.sem.actor_t)
  (starts_atomic_block: bool)
  (ends_atomic_block: bool)
  (aux: unit)
  (ls: wr.sem.state_t)
  (hs: wr.sem.state_t)
  (lstep: wr.sem.step_t{
       wr.inv ls
     /\ (lh_relation_gen wr) aux ls hs
     /\ Some? (step_computation_generic wr.sem actor starts_atomic_block ends_atomic_block lstep ls)
     /\ program_contains_action_of_step_generic wr.sem wr.lprog lstep})
  : GTot (lifter: (step_lifter_t wr.sem.step_t unit){
                      step_lifter_works wr.sem wr.sem wr.lprog wr.hprog unit (lh_relation_gen wr)
                        nat (default_wfr nat) (progress_measure_gen wr)
                        actor starts_atomic_block ends_atomic_block lstep ls hs lifter}) =
  StepLifterLift (lift_step wr actor starts_atomic_block ends_atomic_block lstep ls) ()
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

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

let lift_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)
  : 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))
    (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 laction = wr.sem.step_to_action_f lstep in
  let laction_index = contains_to_index laction wr.lprog.actions in
  wr.actions_match_weakening_transformers_proof ();
  lists_correspond_ubool_implies_index_matches
    action_matches_weakening_transformer
    wr.lprog.actions
    wr.weakening_transformers
    laction_index;
  let weakening_transformer = (Some?.v (nth wr.weakening_transformers laction_index)) in
  lift_step_using_weakening_transformer wr actor starts_atomic_block ends_atomic_block lstep s laction
    weakening_transformer

let lh_relation_gen (wr: weakening_relation_t) (aux: unit) (ls: wr.sem.state_t) (hs: wr.sem.state_t) : GTot ubool =
  ls == hs

let progress_measure_gen (wr: weakening_relation_t) (hs: wr.sem.state_t) (lstep: wr.sem.step_t) (actor: wr.sem.actor_t)
  : GTot nat = 0
/
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 ->
    aux: Prims.unit ->
    ls: Mksemantics_t?.state_t (Mkweakening_relation_t?.sem wr) ->
    hs: Mksemantics_t?.state_t (Mkweakening_relation_t?.sem wr) ->
    lstep:
      Mksemantics_t?.step_t (Mkweakening_relation_t?.sem wr)
        { Mkweakening_relation_t?.inv wr ls /\ Strategies.Weakening.lh_relation_gen wr aux ls hs /\
          Some? (Strategies.Semantics.step_computation_generic (Mkweakening_relation_t?.sem wr)
                actor
                starts_atomic_block
                ends_atomic_block
                lstep
                ls) /\
          Strategies.Semantics.program_contains_action_of_step_generic (Mkweakening_relation_t?.sem wr
              )
            (Mkweakening_relation_t?.lprog wr)
            lstep }
  -> Prims.GTot
    (lifter:
      Strategies.Lift.Generic.step_lifter_t (Mksemantics_t?.step_t (Mkweakening_relation_t?.sem wr))
        Prims.unit
        { Strategies.Lift.Generic.step_lifter_works (Mkweakening_relation_t?.sem wr)
            (Mkweakening_relation_t?.sem wr) (Mkweakening_relation_t?.lprog wr)
            (Mkweakening_relation_t?.hprog wr) Prims.unit (Strategies.Weakening.lh_relation_gen wr)
            Prims.nat (FStar.WellFoundedRelation.default_wfr Prims.nat)
            (Strategies.Weakening.progress_measure_gen wr) actor starts_atomic_block
            ends_atomic_block lstep ls hs lifter })
Strategies.Weakening.weakening_relation_t Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Strategies.Weakening.__proj__Mkweakening_relation_t__item__sem Prims.bool Prims.unit Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Semantics.__proj__Mksemantics_t__item__step_t Prims.l_and Strategies.Weakening.__proj__Mkweakening_relation_t__item__inv Strategies.Weakening.lh_relation_gen Prims.b2t 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 Strategies.Lift.Generic.StepLifterLift Strategies.Weakening.lift_step Strategies.Lift.Generic.step_lifter_t Strategies.Lift.Generic.step_lifter_works Strategies.Weakening.__proj__Mkweakening_relation_t__item__hprog Prims.nat FStar.WellFoundedRelation.default_wfr Strategies.Weakening.progress_measure_gen
let paths_liftable_proof_gen
      (wr: weakening_relation_t)
      (actor: wr.sem.actor_t)
      (starts_atomic_block ends_atomic_block: bool)
      (aux: unit)
      (ls hs: wr.sem.state_t)
      (lstep:
          wr.sem.step_t
            { wr.inv ls /\ (lh_relation_gen wr) aux ls hs /\
              Some? (step_computation_generic wr.sem
                    actor
                    starts_atomic_block
                    ends_atomic_block
                    lstep
                    ls) /\ program_contains_action_of_step_generic wr.sem wr.lprog lstep })
    : GTot
    (lifter:
      (step_lifter_t wr.sem.step_t unit)
        { step_lifter_works wr.sem wr.sem wr.lprog wr.hprog unit (lh_relation_gen wr) nat
            (default_wfr nat) (progress_measure_gen wr) actor starts_atomic_block ends_atomic_block
            lstep ls hs lifter }) =
  
StepLifterLift (lift_step wr actor starts_atomic_block ends_atomic_block lstep ls) ()