parks-a-firing-whose-operand-reaches-the-terminator.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# 'block' is applied to 'buffer' only, so its void 'data' stays unfilled and
# the 'dataize' operand 'ρ.data.size' of 'L_dataized' reaches the terminator ⊥.
# Under '_partial' that parks the firing the way an operand parked on a λ
# function no entry answers does, rather than ending the run: the protocol
# writes 'unanswered(⊥)' with the term 𝔻 could not dataize, the 'morph' operand
# of 'L_entry' hands back the residue it parked on, and the dispatch of 'φ' off
# the answer fires 'L_root', whose own operand dies the same way, so the run
# parks there (#1401).
symbolic: |
  - λ: L_dataized
    dataize:
      𝛿1: $.target
    𝑛: Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
  - λ: L_entry
    dataize:
      𝛿1: $.n
    morph:
      𝑛1: $.v.φ
    𝑛: Φ.l🌵.root( 𝑛1 )
  - λ: L_root
    dataize:
      𝛿1: $.v
    𝑛: ⟦ ⟧
location: 'Q.l🌵.e1'
partial: true
input: >
  ⟦
    number ↦ ⟦ φ ↦ ∅ ⟧,
    bytes ↦ ⟦ φ ↦ ∅, size ↦ ⟦ λ ⤍ L_bytes_size ⟧ ⟧,
    dataized ↦ ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧,
    block ↦ ⟦ data ↦ ∅, buffer ↦ ∅, read ↦ ⟦ φ ↦ Φ.dataized( target ↦ ξ.ρ.data.size ).as-bytes ⟧ ⟧,
    l🌵 ↦ ⟦
      mark ↦ ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧,
      root ↦ ⟦ v ↦ ∅, λ ⤍ L_root ⟧,
      e1 ↦ Φ.l🌵.mark( n ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 3F-F0-00-00-00-00-00-00 ⟧ ) ) )( v ↦ Φ.block( buffer ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ).read ).φ
    ⟧
  ⟧
result: '⟦ v ↦ Φ.dataized( target ↦ ⊥ ).as-bytes, λ ⤍ L_root ⟧.φ'
protocol: |
  𝕄(Φ.l🌵.e1):
    𝑛·0·1 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 1 )
    𝑛·0·2 := 𝑛·0·1( v ↦ Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ).read )
    𝔼(L_entry):
      𝔻(Φ.a🌵0):
        𝕄(Φ.a🌵0):
          𝑛·1·1 := 1
          𝑛·1·2 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
        𝛿·1·1 := 3F-F0-00-00-00-00-00-00  # 1.0
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.n)
      𝕄(Φ.a🌵1):
        𝑛·1·3 := Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )
        𝑛·1·4 := Φ.dataized( target ↦ ⊥ )
        𝔼(L_dataized):
          unanswered(⊥)  # 𝔻(⊥)
          stuck(⊥)
      𝑛1·1 := 𝑛·1·4.as-bytes  # 𝕄(ξ.v.φ)
      𝑛·1·5 := Φ.l🌵.root( 𝑛·1·4.as-bytes )  # 𝑛
      𝕄(𝑛·1·5):
        𝑛·1·6 := ⟦ v ↦ ∅, λ ⤍ L_root ⟧( v ↦ 𝑛·1·4.as-bytes )
      𝑛·1·7 := 𝑛·1·6  # 𝕄(𝑛·1·5)
    𝔼(L_root):
      𝔻(Φ.a🌵3):
        𝕄(Φ.a🌵3):
          𝑛·3·1 := Φ.dataized( target ↦ ⊥ )
          𝔼(L_dataized):
            unanswered(⊥)  # 𝔻(⊥)
            stuck(⊥)
      stuck(⊥)