feat(lang): capture a policy's ref when withdrawing from its credential

crates/tx3-lang/src/cardano.rs

@@ -130,7 +130,8 @@ impl IntoLower for WithdrawalField {
         ctx: &crate::lowering::Context,
     ) -> Result<Self::Output, crate::lowering::Error> {
         match self {
-            WithdrawalField::From(x) => x.into_lower(ctx),
+            // Withdrawing from a script stake credential runs its script.
+            WithdrawalField::From(x) => x.into_lower(&ctx.capturing_policy_refs()),
             WithdrawalField::Amount(x) => x.into_lower(ctx),
             WithdrawalField::Redeemer(x) => x.into_lower(ctx),
         }

crates/tx3-lang/src/lowering.rs

@@ -1136,6 +1136,8 @@ mod tests {
         assert!(txs["mint_hash_only"].references.is_empty());
         // output recipient only: script does not run, no reference input
         assert!(txs["send_to_policy"].references.is_empty());
+        // ref-backed withdrawal stake credential
+        assert_eq!(txs["withdraw"].references.len(), 1);
     });
 
     test_lowering!(withdrawal);

examples/policy_reference_script.tx3

@@ -114,3 +114,18 @@ tx send_to_policy(
         amount: Ada(quantity),
     }
 }
+
+// ref-backed policy as a withdrawal stake credential: script runs, ref UTxO
+// becomes a reference input
+tx withdraw() {
+    cardano::withdrawal {
+        from: Validator,
+        amount: 0,
+        redeemer: (),
+    }
+
+    output {
+        to: Receiver,
+        amount: Ada(0),
+    }
+}

examples/policy_reference_script.withdraw.tir

@@ -0,0 +1,105 @@
+{
+  "fees": {
+    "EvalParam": "ExpectFees"
+  },
+  "references": [
+    {
+      "UtxoRefs": [
+        {
+          "txid": [
+            171,
+            205,
+            239,
+            18,
+            52,
+            86,
+            120,
+            144,
+            171,
+            205,
+            239,
+            18,
+            52,
+            86,
+            120,
+            144,
+            171,
+            205,
+            239,
+            18,
+            52,
+            86,
+            120,
+            144,
+            171,
+            205,
+            239,
+            18,
+            52,
+            86,
+            120,
+            144
+          ],
+          "index": 0
+        }
+      ]
+    }
+  ],
+  "inputs": [],
+  "outputs": [
+    {
+      "address": {
+        "EvalParam": {
+          "ExpectValue": [
+            "receiver",
+            "Address"
+          ]
+        }
+      },
+      "datum": "None",
+      "amount": {
+        "Assets": [
+          {
+            "policy": "None",
+            "asset_name": "None",
+            "amount": {
+              "Number": 0
+            }
+          }
+        ]
+      },
+      "optional": false
+    }
+  ],
+  "validity": null,
+  "mints": [],
+  "burns": [],
+  "adhoc": [
+    {
+      "name": "withdrawal",
+      "data": {
+        "credential": {
+          "Bytes": [
+            171,
+            205,
+            239,
+            18,
+            52
+          ]
+        },
+        "amount": {
+          "Number": 0
+        },
+        "redeemer": {
+          "Struct": {
+            "constructor": 0,
+            "fields": []
+          }
+        }
+      }
+    }
+  ],
+  "collateral": [],
+  "signers": null,
+  "metadata": []
+}

specs/v1beta0/07-transaction-semantics.md

@@ -310,7 +310,8 @@ A policy's script *executes* when the policy is used in a position that
 spends from or runs it: as the `from` of an `input_block`, or as the
 policy of an asset in a `mint` or `burn` block. Used only as an output
 recipient (the `to` of an `output_block`) or as a signer, the script
-does not execute.
+does not execute. Chain extensions may define further executing
+positions (for Cardano, see §8.3).
 
 When a policy whose script lives at a `ref` is used in an executing
 position, that `ref` UTxO is referenced (but not consumed) by the

specs/v1beta0/08-cardano-extensions.md

@@ -50,6 +50,10 @@ withdrawal_field ::=
 A `withdrawal_block` MUST include at least the `from` and `amount`
 fields.
 
+Withdrawing from a script stake credential executes its script, so a
+`ref`-backed `policy` used as `from` is referenced (but not consumed) by
+the transaction, per §7.13.4.
+
 ## 8.4 Plutus witness
 
 ```