fails-on-an-operand-that-reaches-the-terminator.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The very operand '--partial' parks, without the option: an operand of a
# firing that reaches the terminator ⊥ still fails the run, as it did before
# #1401, and the protocol keeps what the run had reached when it did.
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'
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 ).φ
    ⟧
  ⟧
fails: 'terminator ⊥'
protocol: |
  𝕄(Φ.l🌵.e1):
    normalized 𝑛·0·1 := ⟦ mark(n, v) ↦ L_entry:λ, root(v) ↦ L_root:λ, e1 ↦ Φ.l🌵.mark( n ↦ 1.0, v ↦ Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ).read ).φ ⟧  # Φ.l🌵
    normalized 𝑛·0·2 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧  # 𝑛·0·1.mark
    𝑛·0·3 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 1.0 )
    𝑛·0·4 := ⟦ n ↦ 1.0, v ↦ ∅, λ ⤍ L_entry ⟧
    𝑛·0·5 := 𝑛·0·4( v ↦ Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ).read )
    𝑛·0·6 := ⟦ n ↦ 1.0, v ↦ Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ).read, λ ⤍ L_entry ⟧
    𝔼(L_entry):
      𝔻(ξ.n):
        𝕄(ξ.n):
          normalized 𝑛·1·1 := ∅:φ  # Φ.number
          𝑛·1·2 := 1.0
          𝑛·1·3 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ ):φ
          morphed 𝑛·1·4 := 𝑛·1·3
        boxed 𝑛·1·5 := 𝑛·1·4.φ
        normalized 𝑛·1·6 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )  # 𝑛·1·5
        𝕄(𝑛·1·5):
          normalized 𝑛·1·7 := ⟦ φ ↦ ∅, size ↦ L_bytes_size:λ ⟧  # Φ.bytes
          𝑛·1·8 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
          𝑛·1·9 := ⟦ φ ↦ 3F-F0-00-00-00-00-00-00:Δ, size ↦ L_bytes_size:λ ⟧
          morphed 𝑛·1·10 := 𝑛·1·9
        boxed 𝑛·1·11 := 𝑛·1·10.φ
        normalized 𝑛·1·12 := 3F-F0-00-00-00-00-00-00:Δ  # 𝑛·1·11
        𝛿·1·1 := 3F-F0-00-00-00-00-00-00  # 1.0
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.n)
      𝕄(ξ.v.φ):
        normalized 𝑛·1·13 := ⟦ data ↦ ∅, buffer ↦ ∅, read ↦ Φ.dataized( target ↦ ρ.data.size ).as-bytes:φ ⟧  # Φ.block
        𝑛·1·14 := Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )
        𝑛·1·15 := ⟦ data ↦ ∅, buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ), read ↦ Φ.dataized( target ↦ ρ.data.size ).as-bytes:φ ⟧
        normalized 𝑛·1·16 := Φ.dataized( target ↦ ρ.data.size ).as-bytes:φ  # 𝑛·1·15.read
        normalized 𝑛·1·17 := Φ.dataized( target ↦ ⊥ ).as-bytes  # 𝑛·1·16.φ
        remembered 𝑛·1·18 ≡ Φ.dataized  # ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧
        𝑛·1·19 := Φ.dataized( target ↦ ⊥ )
        𝑛·1·20 := ⟦ target ↦ ⊥, λ ⤍ L_dataized ⟧
        remembered 𝑛·1·20 ≡ 𝑛·1·18( target ↦ ⊥ )
        𝔼(L_dataized):