val get_refinement_choice
      (lr: liftability_relation_t)
      (aux: lr.aux_t)
      (ls: lr.lsem.state_t)
      (actor: lr.lsem.actor_t)
      (starts_atomic_block: bool)
      (lsteps: list lr.lsem.step_t)
      (ls': lr.lsem.state_t)
      (hs:
          lr.hsem.state_t
            { eqb (Some ls')
                (steps_computation_generic lr.lsem actor starts_atomic_block true lsteps ls) /\
              (for_all_ubool (program_contains_action_of_step_generic lr.lsem lr.lprog) lsteps) /\
              lr.inv ls /\ lr.lh_relation aux ls hs })
    : GTot
      (choice:
        refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t
          {refinement_choice_works lr ls actor starts_atomic_block lsteps ls' hs choice})
      (decreases
        (lex_nondep_wfr (default_wfr (list lr.lsem.step_t)) lr.progress_wfr).decreaser (lsteps,
            lr.progress_measure hs (Cons?.hd lsteps) actor))
val get_refinement_choice
      (lr: liftability_relation_t)
      (aux: lr.aux_t)
      (ls: lr.lsem.state_t)
      (actor: lr.lsem.actor_t)
      (starts_atomic_block: bool)
      (lsteps: list lr.lsem.step_t)
      (ls': lr.lsem.state_t)
      (hs:
          lr.hsem.state_t
            { eqb (Some ls')
                (steps_computation_generic lr.lsem actor starts_atomic_block true lsteps ls) /\
              (for_all_ubool (program_contains_action_of_step_generic lr.lsem lr.lprog) lsteps) /\
              lr.inv ls /\ lr.lh_relation aux ls hs })
    : GTot
      (choice:
        refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t
          {refinement_choice_works lr ls actor starts_atomic_block lsteps ls' hs choice})
      (decreases
        (lex_nondep_wfr (default_wfr (list lr.lsem.step_t)) lr.progress_wfr).decreaser (lsteps,
            lr.progress_measure hs (Cons?.hd lsteps) actor))
let rec get_refinement_choice
  (lr: liftability_relation_t)
  (aux: lr.aux_t)
  (ls: lr.lsem.state_t)
  (actor: lr.lsem.actor_t)
  (starts_atomic_block: bool)
  (lsteps: list lr.lsem.step_t)
  (ls': lr.lsem.state_t)
  (hs: lr.hsem.state_t{
        eqb (Some ls') (steps_computation_generic lr.lsem actor starts_atomic_block true
                          lsteps ls)
      /\ (for_all_ubool (program_contains_action_of_step_generic lr.lsem lr.lprog) lsteps)
      /\ lr.inv ls
      /\ lr.lh_relation aux ls hs})
  : GTot (choice: refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t{
            refinement_choice_works lr ls actor starts_atomic_block lsteps ls' hs choice})
    (decreases (lex_nondep_wfr (default_wfr (list lr.lsem.step_t)) lr.progress_wfr).decreaser
               (lsteps, lr.progress_measure hs (Cons?.hd lsteps) actor)) =
  lr.inv_stepwise_invariant_proof ();
  match lsteps with
  | [lstep] ->
      let ls2 = Some?.v (step_computation_generic lr.lsem actor starts_atomic_block true
                           lstep ls) in
      assert (lr.inv ls2);
      (match lr.paths_liftable_proof actor starts_atomic_block true aux ls hs lstep with
       | StepLifterSkip aux' ->
           RefinementChoiceSkip aux'
       | StepLifterIntroduce hstep aux2 ->
           let hs2 = Some?.v (step_computation_generic lr.hsem actor
                                starts_atomic_block starts_atomic_block hstep hs) in
           if starts_atomic_block then
             RefinementChoiceIntroduce [hstep] hs2 aux2
           else (
             let choice' = get_refinement_choice lr aux2 ls actor starts_atomic_block lsteps ls' hs2 in
             let RefinementChoiceLift hsteps hs' aux' = choice' in
             RefinementChoiceLift (hstep :: hsteps) hs' aux'
           )
        | StepLifterLift hstep aux' ->
            let hs' = Some?.v (step_computation_generic lr.hsem actor starts_atomic_block true
                                 hstep hs) in
            RefinementChoiceLift [hstep] hs' aux')
  | lstep :: lsteps' ->
      let ls2 = Some?.v (step_computation_generic lr.lsem actor starts_atomic_block false
                           lstep ls) in
      lr.inv_stepwise_invariant_proof ();
      assert (lr.inv ls2);
      (match lr.paths_liftable_proof actor starts_atomic_block false aux ls hs lstep with
       | StepLifterSkip aux2 ->
           get_refinement_choice lr aux2 ls2 actor false lsteps' ls' hs
       | StepLifterIntroduce hstep aux2 ->
           let hs2 = Some?.v (step_computation_generic lr.hsem actor
                                starts_atomic_block starts_atomic_block hstep hs) in
           if starts_atomic_block then
             RefinementChoiceIntroduce [hstep] hs2 aux2
           else
             let choice' = get_refinement_choice lr aux2 ls actor starts_atomic_block lsteps ls' hs2 in
             let RefinementChoiceLift hsteps hs' aux' = choice' in
             RefinementChoiceLift (hstep :: hsteps) hs' aux'
       | StepLifterLift hstep aux2 ->
           let hs2 = Some?.v (step_computation_generic lr.hsem actor starts_atomic_block false
                                hstep hs) in
           let choice' = get_refinement_choice lr aux2 ls2 actor false lsteps' ls' hs2 in
           let RefinementChoiceLift hsteps' hs' aux' = choice' in
           RefinementChoiceLift (hstep :: hsteps') hs' aux')
module Strategies.Lift.Generic

open FStar.WellFoundedRelation
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.Invariant
open Strategies.Semantics
open Util.List
open Util.Logic

noeq type refinement_choice_t (step_t: Type) (state_t: Type) (aux_t: Type) =
  | RefinementChoiceSkip: (aux': aux_t) -> refinement_choice_t step_t state_t aux_t
  | RefinementChoiceIntroduce: (steps: list step_t) -> (state: state_t) -> (aux': aux_t) ->
                               refinement_choice_t step_t state_t aux_t
  | RefinementChoiceLift: (steps: list step_t) -> (state: state_t) -> (aux': aux_t) ->
                          refinement_choice_t step_t state_t aux_t

let refinement_choice_works
  (lr: liftability_relation_t)
  (ls: lr.lsem.state_t)
  (actor: lr.lsem.actor_t)
  (starts_atomic_block: bool)
  (steps: list lr.lsem.step_t)
  (ls': lr.lsem.state_t)
  (hs: lr.hsem.state_t)
  (choice: refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t)
  : GTot ubool =
  match choice with
  | RefinementChoiceSkip aux' ->
         starts_atomic_block
      /\ lr.inv ls'
      /\ lr.lh_relation aux' ls' hs
  | RefinementChoiceIntroduce hsteps hs' aux' ->
         starts_atomic_block
      /\ for_all_ubool (program_contains_action_of_step_generic lr.hsem lr.hprog) hsteps
      /\ Some hs' == steps_computation_generic lr.hsem actor starts_atomic_block true
                      hsteps hs
      /\ lr.lh_relation aux' ls hs'
      /\ (match steps with
         | [] -> False
         | lstep :: _ ->
             lr.progress_wfr.relation (lr.progress_measure hs' lstep actor) (lr.progress_measure hs lstep actor))
  | RefinementChoiceLift hsteps hs' aux' ->
        for_all_ubool (program_contains_action_of_step_generic lr.hsem lr.hprog) hsteps
      /\ (Some hs') == steps_computation_generic lr.hsem actor starts_atomic_block true
                        hsteps hs
      /\ lr.inv ls'
      /\ lr.lh_relation aux' ls' hs'
/
Util.Logic.fst.checked Util.List.fst.checked Strategies.Semantics.fst.checked Strategies.Invariant.fsti.checked Spec.Ubool.fst.checked Spec.Logic.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 FStar.Classical.Sugar.fsti.checked
Strategies.Lift.Generic.fst

    lr: Strategies.Lift.Generic.liftability_relation_t ->
    aux: Mkliftability_relation_t?.aux_t lr ->
    ls: Mksemantics_t?.state_t (Mkliftability_relation_t?.lsem lr) ->
    actor: Mksemantics_t?.actor_t (Mkliftability_relation_t?.lsem lr) ->
    starts_atomic_block: Prims.bool ->
    lsteps: Prims.list (Mksemantics_t?.step_t (Mkliftability_relation_t?.lsem lr)) ->
    ls': Mksemantics_t?.state_t (Mkliftability_relation_t?.lsem lr) ->
    hs:
      Mksemantics_t?.state_t (Mkliftability_relation_t?.hsem lr)
        { Spec.Ubool.eqb (FStar.Pervasives.Native.Some ls')
            (Strategies.Semantics.steps_computation_generic (Mkliftability_relation_t?.lsem lr)
                actor
                starts_atomic_block
                true
                lsteps
                ls) /\
          Util.List.for_all_ubool (Strategies.Semantics.program_contains_action_of_step_generic (Mkliftability_relation_t?.lsem
                    lr)
                (Mkliftability_relation_t?.lprog lr))
            lsteps /\ Mkliftability_relation_t?.inv lr ls /\
          Mkliftability_relation_t?.lh_relation lr aux ls hs }
  -> Prims.GTot
    (choice:
      Strategies.Lift.Generic.refinement_choice_t (Mksemantics_t?.step_t (Mkliftability_relation_t?.hsem
                lr))
        (Mksemantics_t?.state_t (Mkliftability_relation_t?.hsem lr))
        (Mkliftability_relation_t?.aux_t lr)
        { Strategies.Lift.Generic.refinement_choice_works lr
            ls
            actor
            starts_atomic_block
            lsteps
            ls'
            hs
            choice })
Strategies.Lift.Generic.liftability_relation_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__aux_t Strategies.Semantics.__proj__Mksemantics_t__item__state_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__lsem Strategies.Semantics.__proj__Mksemantics_t__item__actor_t Prims.bool Prims.list Strategies.Semantics.__proj__Mksemantics_t__item__step_t Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__hsem Prims.l_and Prims.b2t Spec.Ubool.eqb FStar.Pervasives.Native.option FStar.Pervasives.Native.Some Strategies.Semantics.steps_computation_generic Util.List.for_all_ubool Strategies.Semantics.program_contains_action_of_step_generic Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__lprog Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__inv Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__lh_relation Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__paths_liftable_proof Strategies.Lift.Generic.RefinementChoiceSkip Strategies.Lift.Generic.RefinementChoiceIntroduce Prims.Cons Prims.Nil Strategies.Lift.Generic.RefinementChoiceLift Strategies.Lift.Generic.refinement_choice_t Strategies.Lift.Generic.refinement_choice_works Strategies.Lift.Generic.get_refinement_choice FStar.Pervasives.Native.__proj__Some__item__v Strategies.Semantics.step_computation_generic Prims.unit Prims._assert Strategies.Lift.Generic.__proj__Mkliftability_relation_t__item__inv_stepwise_invariant_proof
let rec get_refinement_choice
      (lr: liftability_relation_t)
      (aux: lr.aux_t)
      (ls: lr.lsem.state_t)
      (actor: lr.lsem.actor_t)
      (starts_atomic_block: bool)
      (lsteps: list lr.lsem.step_t)
      (ls': lr.lsem.state_t)
      (hs:
          lr.hsem.state_t
            { eqb (Some ls')
                (steps_computation_generic lr.lsem actor starts_atomic_block true lsteps ls) /\
              (for_all_ubool (program_contains_action_of_step_generic lr.lsem lr.lprog) lsteps) /\
              lr.inv ls /\ lr.lh_relation aux ls hs })
    : GTot
      (choice:
        refinement_choice_t lr.hsem.step_t lr.hsem.state_t lr.aux_t
          {refinement_choice_works lr ls actor starts_atomic_block lsteps ls' hs choice})
      (decreases
        (lex_nondep_wfr (default_wfr (list lr.lsem.step_t)) lr.progress_wfr).decreaser (lsteps,
            lr.progress_measure hs (Cons?.hd lsteps) actor)) =
  
lr.inv_stepwise_invariant_proof ();
match lsteps with
| [lstep] ->
  let ls2 = Some?.v (step_computation_generic lr.lsem actor starts_atomic_block true lstep ls) in
  assert (lr.inv ls2);
  (match lr.paths_liftable_proof actor starts_atomic_block true aux ls hs lstep with
    | StepLifterSkip aux' -> RefinementChoiceSkip aux'
    | StepLifterIntroduce hstep aux2 ->
      let hs2 =
        Some?.v (step_computation_generic lr.hsem
              actor
              starts_atomic_block
              starts_atomic_block
              hstep
              hs)
      in
      if starts_atomic_block
      then RefinementChoiceIntroduce [hstep] hs2 aux2
      else
        (let choice' = get_refinement_choice lr aux2 ls actor starts_atomic_block lsteps ls' hs2 in
          let RefinementChoiceLift hsteps hs' aux' = choice' in
          RefinementChoiceLift (hstep :: hsteps) hs' aux')
    | StepLifterLift hstep aux' ->
      let hs' =
        Some?.v (step_computation_generic lr.hsem actor starts_atomic_block true hstep hs)
      in
      RefinementChoiceLift [hstep] hs' aux')
| lstep :: lsteps' ->
  let ls2 = Some?.v (step_computation_generic lr.lsem actor starts_atomic_block false lstep ls) in
  lr.inv_stepwise_invariant_proof ();
  assert (lr.inv ls2);
  (match lr.paths_liftable_proof actor starts_atomic_block false aux ls hs lstep with
    | StepLifterSkip aux2 -> get_refinement_choice lr aux2 ls2 actor false lsteps' ls' hs
    | StepLifterIntroduce hstep aux2 ->
      let hs2 =
        Some?.v (step_computation_generic lr.hsem
              actor
              starts_atomic_block
              starts_atomic_block
              hstep
              hs)
      in
      if starts_atomic_block
      then RefinementChoiceIntroduce [hstep] hs2 aux2
      else
        let choice' = get_refinement_choice lr aux2 ls actor starts_atomic_block lsteps ls' hs2 in
        let RefinementChoiceLift hsteps hs' aux' = choice' in
        RefinementChoiceLift (hstep :: hsteps) hs' aux'
    | StepLifterLift hstep aux2 ->
      let hs2 =
        Some?.v (step_computation_generic lr.hsem actor starts_atomic_block false hstep hs)
      in
      let choice' = get_refinement_choice lr aux2 ls2 actor false lsteps' ls' hs2 in
      let RefinementChoiceLift hsteps' hs' aux' = choice' in
      RefinementChoiceLift (hstep :: hsteps') hs' aux')