phino-0.0.154: 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 a lenient join takes into a branch of #1885 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 join fire the fork forever. This
# is the control the pack asking for the guard stands against.
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    join:
      𝑛3: [𝑛1, 𝑛2]
    lenient: true
    𝑛: 𝑛3
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)
      𝑛1·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)
        𝑛1·2 := ⟦ λ ⤍ L_fork, a ↦ Φ.z, b ↦ 𝜎1:λ:φ ⟧  # 𝕄(𝑛1.φ)
        𝔼(L_fork):  # 𝔼(𝑛1)
          𝕄(Φ.a🌵6):
            starved(6)