FRET.STK

assembly

[
  "FRET.STK [ra ~ RegDstn], sp!, uimm"
]

block

[]

catalog_indices

[
  65
]

catalog_records

[
  {
    "asm": "FRET.STK [ra ~ RegDstn], sp!, uimm",
    "constraints": [
      {
        "field": "DstBegin",
        "operator": "one-of",
        "values": [
          10
        ]
      },
      {
        "field": "DstEnd",
        "operator": "one-of",
        "values": [
          2,
          3,
          4,
          5,
          6,
          7,
          8,
          9,
          10,
          11,
          12,
          13,
          14,
          15,
          16,
          17,
          18,
          19,
          20,
          21,
          22,
          23
        ]
      }
    ],
    "encoding": [
      {
        "index": 0,
        "mask": "0x0000707f",
        "match": "0x00003041",
        "width_bits": 32
      }
    ],
    "encoding_kind": "L32",
    "fields": [
      {
        "name": "DstBegin",
        "pieces": [
          {
            "instruction_lsb": 15,
            "value_lsb": 0,
            "width": 5
          }
        ],
        "signedness": "encoding-defined",
        "width": 5
      },
      {
        "name": "DstEnd",
        "pieces": [
          {
            "instruction_lsb": 20,
            "value_lsb": 0,
            "width": 5
          }
        ],
        "signedness": "encoding-defined",
        "width": 5
      },
      {
        "name": "uimm",
        "pieces": [
          {
            "instruction_lsb": 25,
            "value_lsb": 3,
            "width": 7
          },
          {
            "instruction_lsb": 7,
            "value_lsb": 10,
            "width": 5
          }
        ],
        "signedness": "unsigned",
        "width": 15
      }
    ],
    "form_id": "fret_stk_32_4fe246bd8241",
    "length_bits": 32,
    "mnemonic": "FRET.STK",
    "semantic_family": "CMD",
    "semantic_group": "Bundle Split",
    "semantic_handler": "ExecuteFrameReturnStack",
    "semantic_summary": "Restores a restartable stack frame whose first stack slot supplies the validated return target.",
    "status": "accepted"
  }
]

classification

[
  "lifecycle"
]

contract

{
  "block_composition": [
    "none"
  ],
  "canonical_assembly": [
    "FRET.STK [ra ~ RegDstn], sp!, uimm"
  ],
  "defaults": [
    "The inclusive register range is the ring R2..R23. Singleton, full-ring, and wraparound ranges are assigned.",
    "uimm is always present and represents a byte count in multiples of eight; encoded zero is real zero and is illegal because every assigned range contains at least one register.",
    "The range must begin at architectural ra (R10); stack slot zero supplies both restored ra and the return target."
  ],
  "encoding_class": "standalone-encoded",
  "examples": [
    "FRET.STK [ra ~ RegDstn], sp!, uimm"
  ],
  "exceptions": [
    "Reserved endpoints or an insufficient frame size raise Fault_IllegalInstruction before sp, register, memory, target, progress, or TPC effects.",
    "Each eight-byte stack access is a restart boundary. A recoverable access fault preserves earlier committed events and retries exactly the first uncommitted event from trap-preserved template state.",
    "An odd slot-zero value raises Fault_InstructionPC before ra, target, slot-zero progress, or later-register effects; an earlier committed sp adjustment remains restart-visible."
  ],
  "field_contracts": {},
  "field_zero_meanings": {
    "DstBegin": "Encoded zero is outside the callee-save ring and is reserved.",
    "DstEnd": "Encoded zero is outside the callee-save ring and is reserved.",
    "uimm": "Encoded zero is a real zero-byte frame size and is illegal for every nonempty range."
  },
  "legality": [
    "DstBegin and DstEnd select the inclusive R2..R23 callee-save ring; every endpoint outside 2..23 is reserved before effects.",
    "If the range contains N registers, uimm must be at least 8*N bytes. The encoding supplies only multiples of eight.",
    "DstBegin must encode R10 exactly; other otherwise legal ring endpoints are reserved for FRET.STK."
  ],
  "memory_effects": [
    "Load one aligned eight-byte value per selected destination; slot zero is the return-target load and remains an exact restart boundary."
  ],
  "operands": [
    {
      "field": "DstBegin",
      "role": "first register in the inclusive R2..R23 ring range"
    },
    {
      "field": "DstEnd",
      "role": "last register in the inclusive R2..R23 ring range"
    },
    {
      "field": "uimm",
      "role": "frame byte count, encoded in multiples of eight"
    }
  ],
  "ordering": [
    "Add uimm to sp, load and validate slot zero before restoring ra, then restore the remaining selected registers in ring order.",
    "After the final restore, publish the validated slot-zero target to TPC; the command does not perform a sequential TPC increment."
  ],
  "standalone_opcode": true,
  "state_effects": [
    "Slot zero updates both architectural ra and the retained return-address state; subsequent slots restore the rest of the inclusive range.",
    "Completion decrements nonzero frame depth, publishes the last-frame tuple, clears progress, and transfers to the validated target."
  ]
}

depends_on

[
  "PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"
]

id

PTO-BLOCK-FRET-STK

mnemonic

FRET.STK

summary

Restores a restartable stack frame whose first stack slot supplies the validated return target.

surface

block

{
  "classification": [
    "lifecycle"
  ],
  "documentation": "docs/block/lifecycle/FRET.STK.md",
  "id": "PTO-BLOCK-FRET-STK",
  "instruction_contract": {
    "artifact": "spec/evidence/instruction-contract-closure.json",
    "mnemonic": "FRET.STK",
    "ndf_clause": "PTO-INST-BLOCK-FRET-STK"
  },
  "mnemonic": "FRET.STK",
  "readiness_subjects": [
    "ADR-0032",
    "ADR-0052",
    "ADR-0059",
    "ADR-0084"
  ],
  "semantic_tests": [
    "PTO-AVS-BLOCK-FRET-STK-ODD-TARGET-002",
    "PTO-AVS-BLOCK-FRET-STK-RANGE-001",
    "PTO-AVS-BLOCK-FRET-STK-RESTART-003",
    "PTO-AVS-BLOCK-FRET-STK-TARGET-001"
  ],
  "source": "asl/block/lifecycle/FRET.STK.asl",
  "surface": "block",
  "tests": [
    "PTO-AVS-BLOCK-FRET-STK-DECODE-001",
    "PTO-AVS-BLOCK-FRET-STK-ODD-TARGET-002",
    "PTO-AVS-BLOCK-FRET-STK-RANGE-001",
    "PTO-AVS-BLOCK-FRET-STK-RESTART-003",
    "PTO-AVS-BLOCK-FRET-STK-TARGET-001"
  ]
}