spends-the-step-budget-on-an-entry-answering-itself.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# An entry answering with a firing of itself fires until the budget is gone.
# Recursion is nothing phino prevents on its own — that is the object model's
# business — so without '_acyclic' the step limit is what ends the run, and
# every firing it paid for is in the protocol. This is the control the pack
# asking for the guard stands against.
symbolic: |
  - λ: L_loop
    𝑛: ⟦ λ ⤍ L_loop ⟧
location: 'Q.x'
steps: 6
input: '⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧'
fails: 'reaching the limit of steps'
protocol: |
  𝕄(Φ.x):
    𝔼(L_loop):
      𝑛·1·1 := L_loop:λ  # 𝑛
      𝑛·1·2 := L_loop:λ  # 𝕄(𝑛·1·1)
    𝔼(L_loop):
      𝑛·2·1 := L_loop:λ  # 𝑛
      𝑛·2·2 := L_loop:λ  # 𝕄(𝑛·2·1)
    𝔼(L_loop):
      𝑛·3·1 := L_loop:λ  # 𝑛
      𝑛·3·2 := L_loop:λ  # 𝕄(𝑛·3·1)
    𝔼(L_loop):
      𝑛·4·1 := L_loop:λ  # 𝑛
      𝑛·4·2 := L_loop:λ  # 𝕄(𝑛·4·1)
    𝔼(L_loop):
      𝑛·5·1 := L_loop:λ  # 𝑛
      𝑛·5·2 := L_loop:λ  # 𝕄(𝑛·5·1)
    𝔼(L_loop):
      𝑛·6·1 := L_loop:λ  # 𝑛
      𝕄(𝑛·6·1):
        starved(6)