From Undecidability.TM Require Import ProgrammingTools.

Local Arguments plus : simpl never. Local Arguments mult : simpl never.

Set Default Proof Using "Type".

Lemma tl_length (X : Type) (xs : list X) :
  length (tl xs) = pred (length xs).
Proof. destruct xs; cbn; auto. Qed.

Section CaseList.


  Variable X : Type.
  Variable (sigX : finType).
  Hypothesis (cX : codable sigX X).

  Set Default Proof Using "Type".

  Definition stop (s: (sigList sigX)^+) :=
    match s with
    | inr (sigList_cons) => true
    | inr (sigList_nil) => true
    | inl _ => true
    | _ => false
    end.

  Definition Skip_cons : pTM (sigList sigX)^+ unit 1 :=
    Move Rmove;;
    MoveToSymbol stop id.

  Definition M1 : pTM (sigList sigX)^+ unit 2 :=
    LiftTapes Skip_cons [|Fin0|];;
    LiftTapes (Write (inl STOP)) [|Fin1|];;
    MovePar Lmove Lmove;;
    CopySymbols_L stop;;
    LiftTapes (Write (inl START)) [|Fin1|].

  Definition CaseList : pTM (sigList sigX)^+ bool 2 :=
    LiftTapes (Move Rmove) [|Fin0|];;
    Switch (LiftTapes (ReadChar) [|Fin0|])
          (fun s => match s with
                 | Some (inr sigList_nil) =>
                   Return (LiftTapes (Move Lmove) [|Fin0|]) false
                 | Some (inr sigList_cons) =>
                   M1;;
                   LiftTapes Skip_cons [|Fin0|];;
                   Return (LiftTapes (Move Lmove;; Write (inl START)) [|Fin0|]) true
                 | _ => Return Nop default
                 end).


  Definition Skip_cons_Rel : pRel (sigList sigX)^+ unit 1 :=
    Mk_R_p (
        ignoreParam (
            fun tin tout =>
              forall ls rs (x : X) (l : list X),
                tin = midtape (inl START :: ls) (inr sigList_cons)
                              (map inr (Encode_map _ _ x) ++ map inr (Encode_map _ _ l) ++ inl STOP :: rs) ->
                match l with
                | nil =>
                  tout = midtape (rev (map inr (Encode_map _ _ x)) ++ inr sigList_cons :: inl START :: ls)
                                 (inr sigList_nil) (inl STOP :: rs)
                | x'::l' =>
                  tout = midtape (rev (map inr (Encode_map _ _ x)) ++ inr sigList_cons :: inl START :: ls)
                                 (inr sigList_cons) (map inr (Encode_map _ _ x') ++ map inr (Encode_map _ _ l') ++ inl STOP :: rs)
                end)).


  Lemma stop_lemma x :
    forall s : (sigList sigX)^+, s el map inr (map sigList_X (encode x)) -> stop s = false.
  Proof.
    rewrite List.map_map. intros ? (?&<-&?) % in_map_iff. cbn. reflexivity.
  Qed.

  Lemma Skip_cons_Realise : Skip_cons Skip_cons_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Skip_cons. TM_Correct. }
    {
      intros tin ((), tout) H. intros ls rs x l HTin. TMSimp. clear_trivial_eqs.
      destruct l as [ | x' l']; cbn.
      - rewrite MoveToSymbol_correct_moveright; cbn; auto.
        + now rewrite map_id.
        + apply stop_lemma.
      - rewrite MoveToSymbol_correct_moveright; cbn; auto.
        + now rewrite map_map, map_id, map_app, <- app_assoc, !map_map.
        + apply stop_lemma.
    }
  Qed.

  Definition M1_Rel : pRel (sigList sigX)^+ unit 2 :=
    ignoreParam (
        fun tin tout =>
          forall ls rs (x : X) (l : list X) (s1 : nat),
            tin[@Fin0] = midtape (inl START :: ls) (inr sigList_cons)
                                 (map inr (Encode_map _ _ x) ++ map inr (Encode_map _ _ l) ++ inl STOP :: rs) ->
            isVoid_size tin[@Fin1] s1 ->
            tout[@Fin0] = tin[@Fin0] /\
            tout[@Fin1] ≃(; s1 - (S (size x))) x).

  Lemma M1_Realise : M1 M1_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold M1. TM_Correct. eapply Skip_cons_Realise. }
    {
      intros tin ((), tout) H. intros ls rs x l s HTin0 HRight. TMSimp; clear_trivial_eqs.
      rename H4 into HCopy.
      destruct HRight as (r1&r2&HRight&Hs). TMSimp.

      specialize H with (1 := eq_refl).
      destruct l as [ | x' l']; TMSimp.
      - rewrite CopySymbols_L_correct_moveleft in HCopy; cbn; auto.
        2: setoid_rewrite <- in_rev; apply stop_lemma.
        inv HCopy. TMSimp.
        cbn. rewrite !rev_involutive. repeat econstructor. cbn. f_equal. simpl_tape. reflexivity.
        + simpl_list. rewrite skipn_length. simpl_tape. unfold size. rewrite tl_length. lia.
      - rewrite CopySymbols_L_correct_moveleft in HCopy; cbn; auto.
        2: setoid_rewrite <- in_rev; apply stop_lemma.
        inv HCopy. TMSimp.
        cbn. rewrite !rev_involutive. repeat econstructor.
        + f_equal. cbn. rewrite !map_map, map_app, <- app_assoc, map_map. reflexivity.
        + cbn. f_equal. simpl_tape. reflexivity.
        + simpl_list. rewrite skipn_length. simpl_tape. unfold size. rewrite tl_length. lia.
    }
  Qed.

  Definition CaseList_size0 {sigX X : Type} {cX : codable sigX X} (x : X) (s0 : nat) := S (s0 + size x).
  Definition CaseList_size1 {sigX X : Type} {cX : codable sigX X} (x : X) (s1 : nat) := s1 - (S (size x)).

  Definition CaseList_Rel : pRel (sigList sigX)^+ bool 2 :=
    fun tin '(yout, tout) =>
      forall (l : list X) (s0 s1 : nat),
        tin[@Fin0] ≃(;s0) l ->
        isVoid_size tin[@Fin1] s1 ->
        match yout, l with
        | false, nil =>
          tout[@Fin0] ≃(;s0) @nil X /\
          isVoid_size tout[@Fin1] s1
        | true, x :: l' =>
          tout[@Fin0] ≃(; CaseList_size0 x s0) l' /\
          tout[@Fin1] ≃(; CaseList_size1 x s1) x
        | _, _ => False
        end.

  Lemma CaseList_Realise : CaseList CaseList_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold CaseList. TM_Correct. eapply M1_Realise. eapply Skip_cons_Realise. }
    {
      intros tin (yout, tout) H. intros l s0 s1 HEncL HRight.
      unfold CaseList_size0, CaseList_size1 in *.
      destruct HEncL as (ls&HEncL&Hs0). pose proof HRight as (ls'&rs'&HRight'&Hs1). TMSimp; clear_trivial_eqs.
      destruct l as [ | x l'] in *; cbn in *; TMSimp; clear_trivial_eqs.
      {
        split; auto.
        - repeat econstructor; cbn; simpl_tape. auto.
      }
      {
        rewrite !map_map, map_app, <- app_assoc in *.
        setoid_rewrite map_map in H. setoid_rewrite map_map in H0.
        specialize H with (1 := eq_refl) (2 := HRight).
        TMSimp. specialize H0 with (1 := eq_refl).
        destruct l' as [ | x' l'']; TMSimp.
        - repeat split; auto. hnf. eexists. split. simpl_tape. f_equal.
          + rewrite tl_length. simpl_list. cbn. unfold size. lia.
        - repeat split; auto. hnf. eexists. simpl_tape. rewrite List.map_map. cbn. simpl_list. split.
          + f_equal. f_equal. now rewrite !map_map.
          + rewrite tl_length. simpl_list. cbn. unfold size. lia.
      }
    }
  Qed.


  Lemma Skip_cons_Terminates :
    projT1 (Skip_cons)
           (fun tin k =>
              exists ls rs (x : X) (l : list X),
                tin[@Fin0] = midtape (inl START :: ls) (inr sigList_cons)
                                     (map inr (Encode_map _ _ x) ++ map inr (Encode_map _ _ l) ++ inl STOP :: rs) /\
                 6 + 4 *size x <= k).
  Proof.
    eapply TerminatesIn_monotone.
    { unfold Skip_cons. TM_Correct. }
    {
      intros tin k (ls&rs&x&l&HTin&Hk). TMSimp.
      exists 1, (4 + 4 *size x). repeat split. 1-2: lia.
      intros tmid () H. TMSimp.
      destruct l as [ | x' l]; cbn.
      - rewrite MoveToSymbol_steps_moveright; cbn; auto. now rewrite !map_length.
      - rewrite MoveToSymbol_steps_moveright; cbn; auto. now rewrite !map_length.
    }
  Qed.

  Lemma M1_Terminates :
    projT1 M1
           (fun tin k =>
              exists ls rs (x : X) (l : list X),
                tin[@Fin0] = midtape (inl START :: ls) (inr sigList_cons)
                                     (map inr (Encode_map _ _ x) ++ map inr (Encode_map _ _ l) ++ inl STOP :: rs) /\
                 23 + 12 *size x <= k).
  Proof.
    eapply TerminatesIn_monotone.
    { unfold M1. TM_Correct. eapply Skip_cons_Realise. eapply Skip_cons_Terminates. }
    {
      intros tin k (ls&rs&x&l&HTin&Hk). TMSimp.
      exists (6 + 4 *size x), (16 + 8 *size x). repeat split; try lia. eauto 6.
      intros tmid_ (). intros (H&HInj); TMSimp. specialize H with (1 := eq_refl).
      destruct l as [ | x' l']; TMSimp.       1-2: exists 1, (14 + 8 *size x); repeat split; try lia.
      - intros tmid2 (). intros (_&HInj2); TMSimp.
        exists 3, (10 + 8 *size x). repeat split; try lia.
        intros tmid3 (). intros (H3&H3'); TMSimp.
        exists (8+8*size cX x), 1. repeat split; cbn; try lia.
        + rewrite CopySymbols_L_steps_moveleft; auto.
          now rewrite rev_length, !map_length.
      - intros tmid2 (). intros (_&HInj2); TMSimp.
        exists 3, (10 + 8 *size x). repeat split; try lia.
        intros tmid3 (). intros (H3&H3'); TMSimp.
        exists (8+8*size cX x), 1. repeat split; cbn; try lia.
        + rewrite CopySymbols_L_steps_moveleft; auto.
          now rewrite rev_length, !map_length.
    }
  Qed.

  Definition CaseList_steps_cons {sigX X : Type} {cX : codable sigX X} (x : X) := 42 + 16 *size x.

  Definition CaseList_steps_nil := 5.

  Definition CaseList_steps {sigX X : Type} {cX : codable sigX X} (l:list X) :=
    match l with
    | nil => CaseList_steps_nil
    | x::l' => CaseList_steps_cons x
    end.

  Lemma CaseList_Terminates :
    projT1 CaseList
           (fun tin k =>
              exists l : list X,
                tin[@Fin0] l /\
                isVoid tin[@Fin1] /\
                CaseList_steps l <= k).
  Proof.
    unfold CaseList_steps, CaseList_steps_cons, CaseList_steps_nil. eapply TerminatesIn_monotone.
    { unfold CaseList. TM_Correct.
      - eapply M1_Realise.
      - eapply M1_Terminates.
      - eapply Skip_cons_Realise.
      - eapply Skip_cons_Terminates.
    }
    {
      cbn. intros tin k (l&HEncL&HRight&Hk).
      destruct HEncL as (ls&HEncL); TMSimp.
      destruct l as [ | x l']; cbn.
      {
        exists 1, 3. repeat split; try lia.
        intros tmid (). intros (H1&HInj1); TMSimp.
        exists 1, 1. repeat split; try lia.
        intros tmid2 ymid2 ((H2&H2')&HInj2). apply Vector.cons_inj in H2' as (H2'&_). TMSimp.
        lia.
      }
      {
        exists 1, (40 + 16 *size x). repeat split; try lia.
        intros tmid (). intros (H1&HInj1); TMSimp.
        exists 1, (38 + 16 *size x). repeat split; try lia.
        intros tmid2 ymid2 ((H2&H2')&HInj2). apply Vector.cons_inj in H2' as (H2'&_). TMSimp.
        exists (23 + 12 *size x), (14 + 4 *size x). repeat split; try lia.
        { TMSimp_goal. rewrite !map_map, List.map_app, <- app_assoc, !map_map. do 4 eexists; eauto. split.
          - f_equal. now rewrite !map_map.
          - lia.
        }
        intros tmid3 () H3'.
        rewrite !map_map, map_app, <- app_assoc in H3'.
        setoid_rewrite map_map in H3'.
        specialize H3' with (1 := eq_refl) (2 := isVoid_isVoid_size HRight). TMSimp.
        exists (6 + 4 *size x), 3. repeat split; try lia.
        { do 4 eexists; repeat split; eauto. now rewrite !map_map. }
        intros tmid4 () (H4&HInj4); TMSimp.
        setoid_rewrite map_map in H4.
        specialize H4 with (1 := eq_refl).
        destruct l' as [ | x' l'']; TMSimp.         - exists 1, 1. repeat split; try lia.
        - exists 1, 1. repeat split; try lia.
      }
    }
  Qed.


  Definition IsNil : pTM (sigList sigX)^+ bool 1 :=
    Move Rmove;;
    Switch ReadChar
    (fun s =>
       match s with
       | Some (inr sigList_nil) =>
         Return (Move Lmove) true
       | _ => Return (Move Lmove) false
       end).

  Definition IsNil_Rel : pRel (sigList sigX)^+ bool 1 :=
    Mk_R_p (
        fun tin '(yout, tout) =>
          forall (xs : list X) (s : nat),
            tin ≃(;s) xs ->
            match yout, xs with
            | true, nil => tout ≃(;s) xs
            | false, _ :: _ => tout ≃(;s) xs
            | _, _ => False
            end).

  Definition IsNil_steps := 5.

  Lemma IsNil_Sem : IsNil c(IsNil_steps) IsNil_Rel.
  Proof.
    unfold IsNil_steps. eapply RealiseIn_monotone.
    { unfold IsNil. TM_Correct. }
    { Unshelve. 4-11: reflexivity. lia. }
    {
      intros tin (yout, tout) H. cbn. intros xs s HEncXs.
      destruct HEncXs as (ls & HEncXs & Hs). TMSimp.
      destruct xs as [ | x xs' ]; TMSimp.
      - now repeat econstructor.
      - now repeat econstructor.
    }
  Qed.



  Definition Constr_nil : pTM (sigList sigX)^+ unit 1 := WriteValue (@nil X).

  Goal Constr_nil = WriteMove (inl STOP) Lmove;; WriteMove (inr sigList_nil) Lmove;; Write (inl START).
  Proof. reflexivity. Qed.

  Definition Constr_nil_Rel : pRel (sigList sigX)^+ unit 1 :=
    Mk_R_p (ignoreParam (fun tin tout => forall (s : nat), isVoid_size tin s -> tout ≃(; pred s) @nil X)).

  Definition Constr_nil_steps := 5.

  Lemma Constr_nil_Sem : Constr_nil c(Constr_nil_steps) Constr_nil_Rel.
  Proof.
    unfold Constr_nil_steps. eapply RealiseIn_monotone.
    { unfold Constr_nil. TM_Correct. }
    { reflexivity. }
    { intros tin ((), tout) H. cbn in *. intros s HRight.
      specialize H with (1 := HRight). contains_ext. unfold WriteValue_size. lia. }
  Qed.


  Definition Constr_cons : pTM (sigList sigX)^+ unit 2 :=
    LiftTapes (MoveRight _;; Move Lmove) [|Fin1|];;
    LiftTapes (CopySymbols_L stop) [|Fin1;Fin0|];;
    LiftTapes (WriteMove (inr sigList_cons) Lmove;; Write (inl START)) [|Fin0|].


  Definition Constr_cons_size {sigX X : Type} {cX : codable sigX X} (y : X) (s0 : nat) := s0 - size y - 1.

  Definition Constr_cons_Rel : pRel (sigList sigX)^+ unit 2 :=
    ignoreParam (
        fun tin tout =>
          forall (l:list X) (y:X) (s0 s1 : nat),
            tin[@Fin0] ≃(;s0) l ->
            tin[@Fin1] ≃(;s1) y ->
            tout[@Fin0] ≃(;Constr_cons_size y s0) y :: l /\
            tout[@Fin1] ≃(;s1) y
      ).


  Lemma Constr_cons_Realise : Constr_cons Constr_cons_Rel.
  Proof.
    eapply Realise_monotone.
    { unfold Constr_cons. TM_Correct. apply MoveRight_Realise with (X := X). }
    {
      intros tin ((), tout) H. intros l y s0 s HEncL HEncY.
      unfold Constr_cons_size in *.
      TMSimp; clear_trivial_eqs.
      modpon H. destruct H as (ls&H). TMSimp.
      destruct HEncL as (ls2&HEncL&Hs). TMSimp.
      rewrite CopySymbols_L_correct_moveleft in H0; swap 1 2; auto.
      { intros ? (?&<-& (?&<-&?) % in_rev % in_map_iff) % in_map_iff. cbn. reflexivity. }
      inv H0. TMSimp.
      repeat econstructor.
      - cbn. f_equal. simpl_tape. rewrite !map_rev, rev_involutive. f_equal.
        now rewrite !List.map_map, map_app, <- app_assoc, List.map_map.
      - simpl_tape. rewrite tl_length. simpl_list. rewrite skipn_length. unfold size. lia.
      - f_equal. now rewrite !map_rev, rev_involutive.
      - auto.
    }
  Qed.

  Definition Constr_cons_steps {sigX X : Type} {cX : codable sigX X} (x : X) := 23 + 12 * size x.

  Lemma Constr_cons_Terminates :
    projT1 Constr_cons
           (fun tin k =>
              exists (l: list X) (y: X),
                tin[@Fin0] l /\
                tin[@Fin1] y /\
                Constr_cons_steps y <= k).
  Proof.
    unfold Constr_cons_steps. eapply TerminatesIn_monotone.
    { unfold Constr_cons. TM_Correct.
      - apply MoveRight_Realise with (X := X).
      - apply MoveRight_Realise with (X := X).
      - apply MoveRight_Terminates with (X := X).
    }
    {
      intros tin k (l&y&HEncL&HEncY&Hk). cbn.
      exists (10 + 4 * size y), (12 + 8 * size y). repeat split; try lia.
      - cbn. exists (8 + 4 * size y), 1. repeat split; try lia.
        + eexists. split. eauto. reflexivity.
      - intros tmid () (H&HInj). TMSimp.
        modpon H. destruct H as (ls&HEncY'). TMSimp.
        exists (8 + 8 * size y), 3. repeat split; try lia.
        + erewrite CopySymbols_L_steps_moveleft; eauto. now rewrite map_length, rev_length, map_length.
        + intros tmid2 (). intros (H2&HInj2). TMSimp.
          exists 1, 1. repeat split; try lia.
    }
  Qed.

End CaseList.

Arguments CaseList : simpl never.
Arguments IsNil : simpl never.
Arguments Constr_nil _ {_ _}: simpl never.
Arguments Constr_cons : simpl never.

Arguments CaseList_size0 {sigX X cX} : simpl never.
Arguments CaseList_size1 {sigX X cX} : simpl never.
Arguments Constr_cons_size {sigX X cX} : simpl never.

Arguments CaseList_steps_cons {sigX X cX} : simpl never.
Arguments CaseList_steps {sigX X cX} : simpl never.
Arguments Constr_cons_steps {sigX X cX} : simpl never.
Arguments CaseList_steps_nil : simpl never.



Ltac smpl_TM_CaseList :=
  once lazymatch goal with
  | [ |- CaseList _ _ ] => apply CaseList_Realise
  | [ |- projT1 (CaseList _) _ ] => apply CaseList_Terminates

  | [ |- IsNil _ _ ] => eapply RealiseIn_Realise; apply IsNil_Sem
  | [ |- IsNil _ c(_) _ ] => apply IsNil_Sem
  | [ |- projT1 (IsNil _ ) _ ] => eapply RealiseIn_TerminatesIn; apply IsNil_Sem
                                  
  | [ |- Constr_nil _ _ ] => eapply RealiseIn_Realise; apply Constr_nil_Sem
  | [ |- Constr_nil _ c(_) _ ] => apply Constr_nil_Sem
  | [ |- projT1 (Constr_nil _) _ ] => eapply RealiseIn_TerminatesIn; apply Constr_nil_Sem

  | [ |- Constr_cons _ _ ] => apply Constr_cons_Realise
  | [ |- projT1 (Constr_cons _) _ ] => apply Constr_cons_Terminates
  end.

Smpl Add smpl_TM_CaseList : TM_Correct.

From Undecidability.TM.Hoare Require Import HoareLogic HoareRegister HoareTactics.

Section CaseList.

  Variable (X : Type) (sigX : finType) (codX : codable sigX X).

  Definition Constr_cons_sizefun (x : X) : Vector.t (nat->nat) 2 :=
    [|Constr_cons_size x; id|].

  Lemma Constr_cons_SpecT_size (x : X) (xs : list X) (ss : Vector.t nat 2) :
    TripleT
      (≃≃(([], withSpace [|Contains _ xs; Contains _ x |] ss))) (Constr_cons_steps x) (Constr_cons sigX)
      (fun _ => ≃≃(([], withSpace [|Contains _ (x::xs); Contains _ x|] (appSize (Constr_cons_sizefun x) ss)))).
  Proof. unfold withSpace.
    eapply Realise_TripleT.
    - apply Constr_cons_Realise.
    - apply Constr_cons_Terminates.
    - intros tin [] tout H HEnc. cbn in *.
      specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1; simpl_vector in *; cbn in *.
      modpon H. tspec_solve.
    - intros tin k HEnc Hk. cbn.
      specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1; simpl_vector in *; cbn in *.
      eauto.
  Qed.

  Lemma Constr_nil_SpecT_size (ss : Vector.t nat 1) :
    TripleT
      (≃≃(([], withSpace [|Void |] ss))) Constr_nil_steps (Constr_nil X)
      (fun _ => ≃≃(([], withSpace [|Contains _ (@nil X) |] (appSize [|pred|] ss)))).
  Proof. unfold withSpace.
    eapply RealiseIn_TripleT.
    - apply Constr_nil_Sem.
    - intros tin [] tout H HEnc. cbn in *.
      specialize (HEnc Fin0). simpl_vector in *; cbn in *. modpon H. tspec_solve.
  Qed.

  Definition CaseList_size (xs : list X) : Vector.t (nat->nat) 2 :=
    match xs with
    | nil => [|id;id|]
    | x :: xs => [|CaseList_size0 x; CaseList_size1 x|]
    end.

  Lemma CaseList_SpecT_size (xs : list X) (ss : Vector.t nat 2) :
    TripleT
      (≃≃(([], withSpace [|Contains _ xs; Void |] ss))) (CaseList_steps xs) (CaseList sigX)
      (fun yout => ≃≃([yout = match xs with [] => false | _ => true end],withSpace
                         (match xs with
                          | x::xs' => [|Contains _ xs'; Contains _ x|]
                          | nil => [|Contains _ xs; Void|]
                          end)
                         (appSize (CaseList_size xs) ss))).
  Proof. unfold withSpace.
    eapply Realise_TripleT.
    - apply CaseList_Realise.
    - apply CaseList_Terminates.
    - intros tin yout tout H HEnc. cbn in *.
      specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1; simpl_vector in *; cbn in *.
      modpon H. destruct yout, xs; cbn in *; eauto.
      + destruct H as (H1&H2). tspec_solve. easy.
      + destruct H as (H1&H2). tspec_solve. easy.
    - intros tin k HEnc Hk. cbn.
      specialize (HEnc Fin0) as HEnc0; specialize (HEnc Fin1) as HEnc1; simpl_vector in *; cbn in *.
      eauto.
  Qed.

End CaseList.

Ltac hstep_List :=
  match goal with
  | [ |- TripleT ?P ?k (Constr_cons _) ?Q ] => eapply Constr_cons_SpecT_size
  | [ |- TripleT ?P ?k (Constr_nil _) ?Q ] => eapply Constr_nil_SpecT_size
  | [ |- TripleT ?P ?k (CaseList _) ?Q ] => eapply CaseList_SpecT_size
  end.

Smpl Add hstep_List : hstep_Spec.