phino-0.0.156: test-resources/evaluate-packs/spends-the-step-budget-on-a-branch-whose-phi-leads-back-to-it.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The branch whose φ fires the same fork again, with no '--acyclic' to cut it.
# The step of an 'unfold' line (#1885, #1921) fires the way an 'evaluate'
# line does, spending a step on every firing (#1882), so the step limit ends
# the run instead of letting the line fire the fork forever. This is the
# control the pack asking for the guard stands against.
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    unfold:
      𝑛3: 𝑛1
    join:
      𝑛4: [𝑛3, 𝑛2]
    𝑛: 𝑛4
location: 'Q.y'
steps: 6
input: '⟦ z ↦ ⟦ φ ↦ ξ.f, f ↦ ⟦ λ ⤍ L_fork, a ↦ Φ.z, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧ ⟧ ⟧, y ↦ ⟦ a ↦ Φ.z, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'
fails: 'reaching the limit of steps'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := ⟦ φ ↦ f, f ↦ ⟦ λ ⤍ L_fork, a ↦ Φ.z, b ↦ 𝜎1:λ:φ ⟧ ⟧  # 𝕄(ξ.a)
      𝑛2·1 := 𝜎2:λ:φ  # 𝕄(ξ.b)
      𝑛3·1 := ⟦ λ ⤍ L_fork, a ↦ Φ.z, b ↦ 𝜎1:λ:φ ⟧  # 𝕄(𝑛1.φ)
      𝔼(L_fork):  # 𝔼(𝑛1)
        𝑛1·2 := ⟦ φ ↦ f, f ↦ ⟦ λ ⤍ L_fork, a ↦ Φ.z, b ↦ 𝜎1:λ:φ ⟧ ⟧  # 𝕄(ξ.a)
        𝑛2·2 := 𝜎1:λ:φ  # 𝕄(ξ.b)
        𝑛3·2 := ⟦ λ ⤍ L_fork, a ↦ Φ.z, b ↦ 𝜎1:λ:φ ⟧  # 𝕄(𝑛1.φ)
        𝔼(L_fork):  # 𝔼(𝑛1)
          𝕄(Φ.a🌵6):
            starved(6)