phino-0.0.152: test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps an answer by the operands a firing
# brought down, and a symbol is an operand of its own: every symbol dataizes
# to the one manufactured datum, so two firings over two symbols come down to
# the same bytes, yet they stand for two values nobody worked out. A memo
# keyed on the bytes would answer the second firing with the symbol the first
# one minted and make the two values one; this one keys on the symbol, so each
# firing mints a symbol of its own.
symbolic: |
  - λ: L_dataized
    dataize:
      𝛿1: $.target
    𝑛: Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
deep: true
acyclic: plausible
input: >
  ⟦ bytes(φ) ↦ ⟦⟧,
    dataized(target) ↦ L_dataized:λ,
    x ↦ Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ),
    y ↦ Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ) ⟧
result: >
  ⟦ bytes(φ) ↦ ⟦⟧,
    dataized(target) ↦ L_dataized:λ,
    x ↦ ⟦ φ ↦ 𝜎3:λ ⟧,
    y ↦ ⟦ φ ↦ 𝜎4:λ ⟧ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.x):
      𝑛·0·1 := Φ.bytes( φ ↦ 𝜎1:λ )
      𝑛·0·2 := Φ.dataized( target ↦ 𝑛·0·1 )
      𝔼(L_dataized):
        𝔻(Φ.a🌵0):
          𝕄(Φ.a🌵0):
            𝑛·1·1 := Φ.bytes( φ ↦ 𝜎1:λ )
        𝛿1·1 := 𝔻(𝜎1:λ)  # 𝔻(ξ.target)
        𝑛·1·2 := Φ.bytes( φ ↦ 𝜎3:λ )  # 𝑛
        𝕄(𝑛·1·2):
          𝑛·1·3 := Φ.bytes( φ ↦ 𝜎3:λ )
        𝑛·1·4 := 𝑛·1·3  # 𝕄(𝑛·1·2)
    𝕄(Φ.y):
      𝑛·0·3 := Φ.bytes( φ ↦ 𝜎2:λ )
      𝑛·0·4 := Φ.dataized( target ↦ 𝑛·0·3 )
      𝔼(L_dataized):
        𝔻(Φ.a🌵1):
          𝕄(Φ.a🌵1):
            𝑛·2·1 := Φ.bytes( φ ↦ 𝜎2:λ )
        𝛿1·2 := 𝔻(𝜎2:λ)  # 𝔻(ξ.target)
        𝑛·2·2 := Φ.bytes( φ ↦ 𝜎4:λ )  # 𝑛
        𝕄(𝑛·2·2):
          𝑛·2·3 := Φ.bytes( φ ↦ 𝜎4:λ )
        𝑛·2·4 := 𝑛·2·3  # 𝕄(𝑛·2·2)