Add CIP-0168 Value builtin scripts

plutus-scripts/PlutusScripts/Batch7/Value/Common.hs

@@ -0,0 +1,196 @@
+-- | Runtime checks for the CIP-0168 Value builtins.
+module PlutusScripts.Batch7.Value.Common (
+  mkPoliciesPolicy,
+  mkAssetCountPolicy,
+  mkFilterPolicy,
+  mkFailingFilterPolicy,
+  mkSizePolicy,
+  checkTransition,
+) where
+
+import PlutusTx.Builtins qualified as B
+import PlutusTx.Builtins.Internal qualified as BI (BuiltinValue, unitval)
+import PlutusTx.List qualified as List
+import PlutusTx.Prelude qualified as P
+
+{-# INLINEABLE emptyValue #-}
+emptyValue :: BI.BuiltinValue
+emptyValue = B.unsafeDataAsValue (B.mkMap [])
+
+{-# INLINEABLE valueEqual #-}
+valueEqual :: BI.BuiltinValue -> BI.BuiltinValue -> Bool
+valueEqual a b = B.mkValue a P.== B.mkValue b
+
+{-# INLINEABLE fromCoins #-}
+fromCoins :: [(P.BuiltinByteString, P.BuiltinByteString, Integer)] -> BI.BuiltinValue
+fromCoins = List.foldr (\(p, t, q) -> B.insertCoin p t q) emptyValue
+
+{-# INLINEABLE check #-}
+check :: Bool -> P.BuiltinUnit
+check ok = if ok then BI.unitval else P.traceError "value builtin assertion"
+
+{-# INLINEABLE mkPoliciesPolicy #-}
+mkPoliciesPolicy
+  :: [(P.BuiltinByteString, P.BuiltinByteString, Integer)]
+  -> [P.BuiltinByteString]
+  -> P.BuiltinData
+  -> P.BuiltinUnit
+mkPoliciesPolicy coins expected _ctx =
+  check (P.fromOpaque (B.policies (fromCoins coins)) P.== expected)
+
+-- | Counts include ADA, ignore quantities, and update after deletion/cancellation.
+{-# INLINEABLE mkAssetCountPolicy #-}
+mkAssetCountPolicy :: P.BuiltinData -> P.BuiltinUnit
+mkAssetCountPolicy _ctx =
+  let ada = B.insertCoin "" "" 100 emptyValue
+      v = B.insertCoin "a" "x" (-7) (B.insertCoin "a" "y" 999 ada)
+      deleted = B.insertCoin "a" "x" 0 v
+      cancelled = B.unionValue v (B.scaleValue (-1) v)
+   in check
+        ( B.assetCount emptyValue
+            P.== 0
+            P.&& B.assetCount ada
+            P.== 1
+            P.&& B.assetCount v
+            P.== 3
+            P.&& B.assetCount deleted
+            P.== 2
+            P.&& B.assetCount cancelled
+            P.== 0
+            P.&& valueEqual cancelled emptyValue
+        )
+
+{-# INLINEABLE mkFilterPolicy #-}
+mkFilterPolicy
+  :: (P.BuiltinList P.BuiltinByteString -> BI.BuiltinValue -> BI.BuiltinValue)
+  -> [P.BuiltinByteString]
+  -> [(P.BuiltinByteString, P.BuiltinByteString, Integer)]
+  -> [(P.BuiltinByteString, P.BuiltinByteString, Integer)]
+  -> P.BuiltinData
+  -> P.BuiltinUnit
+mkFilterPolicy filterValue ids coins expected _ctx =
+  let v = fromCoins coins
+      ps = P.toOpaque ids
+      result = filterValue ps v
+   in check (valueEqual result (fromCoins expected))
+
+{-| Observe a returned Value but accept EVERY possible result. A mutant filter
+returning any Value must make this policy succeed, exposing unexpected success.
+Using the serialised Data rather than another Value builtin isolates failure. -}
+{-# INLINEABLE mkFailingFilterPolicy #-}
+mkFailingFilterPolicy
+  :: (P.BuiltinList P.BuiltinByteString -> BI.BuiltinValue -> BI.BuiltinValue)
+  -> [P.BuiltinByteString]
+  -> [(P.BuiltinByteString, P.BuiltinByteString, Integer)]
+  -> P.BuiltinData
+  -> P.BuiltinUnit
+mkFailingFilterPolicy filterValue ids coins _ctx =
+  let v = fromCoins coins
+      result = filterValue (P.toOpaque ids) v
+      observed = B.mkValue result
+   in if B.lengthOfByteString (B.serialiseData observed) P.>= 0
+        then BI.unitval
+        else P.traceError "unreachable negative serialised length"
+
+-- | Whole-policy size profiles: construction and result checking are included.
+{-# INLINEABLE mkSizePolicy #-}
+mkSizePolicy :: Bool -> Integer -> P.BuiltinData -> P.BuiltinUnit
+mkSizePolicy samePolicy count _ctx =
+  let coins =
+        List.map
+          ( \i ->
+              ( if samePolicy then "p" else B.integerToByteString B.BigEndian 2 i
+              , B.integerToByteString B.BigEndian 2 i
+              , i P.+ 1
+              )
+          )
+          (P.enumFromTo 1 count)
+      v = fromCoins coins
+      ids = if samePolicy then ["p"] else List.map (\(p, _, _) -> p) coins
+      kept = B.keepPolicies (P.toOpaque ids) v
+      dropped = B.dropPolicies (P.toOpaque ids) v
+   in check
+        ( B.assetCount v
+            P.== count
+            P.&& List.length (P.fromOpaque (B.policies v))
+            P.== (if samePolicy then 1 else count)
+            P.&& valueEqual kept v
+            P.&& valueEqual dropped emptyValue
+        )
+
+{-# INLINEABLE dual #-}
+dual :: [P.BuiltinByteString] -> BI.BuiltinValue -> Bool
+dual ids v =
+  valueEqual
+    ( B.unionValue
+        (B.keepPolicies (P.toOpaque ids) v)
+        (B.dropPolicies (P.toOpaque ids) v)
+    )
+    v
+
+{-# INLINEABLE ordered #-}
+ordered :: [P.BuiltinByteString] -> Bool
+ordered xs = case xs of
+  [] -> True
+  [_] -> True
+  a : b : rest -> a P.< b P.&& ordered (b : rest)
+
+-- | Shared predicate for the V3 and V4 spending-context wrappers.
+{-# INLINEABLE checkTransition #-}
+checkTransition
+  :: Integer
+  -> P.BuiltinByteString
+  -> Integer
+  -> BI.BuiltinValue
+  -> BI.BuiltinValue
+  -> Bool
+checkTransition mode protocol expected before after =
+  let oldProtocol = B.keepPolicies (P.toOpaque [protocol]) before
+      newProtocol = B.keepPolicies (P.toOpaque [protocol]) after
+      preserved =
+        if mode P.== 0
+          then valueEqual oldProtocol newProtocol
+          else
+            mode
+              P.== 1
+              P.&& valueEqual
+                (B.dropPolicies (P.toOpaque ([""] :: [P.BuiltinByteString])) before)
+                (B.dropPolicies (P.toOpaque ([""] :: [P.BuiltinByteString])) after)
+   in protocol
+        P./= ""
+        P.&& expected
+        P.> 0
+        P.&& P.fromOpaque (B.policies oldProtocol)
+        P.== [protocol]
+        P.&& B.assetCount oldProtocol
+        P.== expected
+        P.&& B.assetCount newProtocol
+        P.== expected
+        P.&& preserved
+        P.&& ordered (P.fromOpaque (B.policies before))
+        P.&& ordered (P.fromOpaque (B.policies after))
+        P.&& countPartition before
+        P.&& countPartition after
+        P.&& adaPartition before
+        P.&& adaPartition after
+        P.&& dual [""] before
+        P.&& dual [""] after
+        P.&& dual [protocol] before
+        P.&& dual [protocol] after
+
+-- | Distinct assets split exactly into the ADA and non-ADA partitions.
+{-# INLINEABLE countPartition #-}
+countPartition :: BI.BuiltinValue -> Bool
+countPartition v =
+  B.assetCount v
+    P.== B.assetCount (B.keepPolicies (P.toOpaque ([""] :: [P.BuiltinByteString])) v)
+    P.+ B.assetCount (B.dropPolicies (P.toOpaque ([""] :: [P.BuiltinByteString])) v)
+
+{-# INLINEABLE adaPartition #-}
+adaPartition :: BI.BuiltinValue -> Bool
+adaPartition v =
+  let ada = B.keepPolicies (P.toOpaque ([""] :: [P.BuiltinByteString])) v
+   in B.assetCount ada
+        P.== 1
+        P.&& B.lookupCoin "" "" ada
+        P.== B.lookupCoin "" "" v

plutus-scripts/PlutusScripts/Batch7/Value/Context.hs

@@ -0,0 +1,102 @@
+-- | Spending wrappers decode each ledger language's own context representation.
+module PlutusScripts.Batch7.Value.Context (mkStateV3, mkStateV4) where
+
+import PlutusLedgerApi.V3 qualified as V3
+import PlutusLedgerApi.V3.Contexts qualified as V3
+import PlutusLedgerApi.V4 qualified as V4
+import PlutusLedgerApi.V4.Contexts qualified as V4
+import PlutusScripts.Batch7.Value.Common (checkTransition)
+import PlutusTx.Builtins qualified as B
+import PlutusTx.Builtins.Internal qualified as BI (unitval)
+import PlutusTx.List qualified as List
+import PlutusTx.Prelude qualified as P
+
+-- | The redeemer is Constr 0 [mode, protocol policy bytes, expected count].
+{-# INLINEABLE redeemerFields #-}
+redeemerFields :: P.BuiltinData -> (Integer, P.BuiltinByteString, Integer)
+redeemerFields raw =
+  let (tag, fields) = B.unsafeDataAsConstr raw
+   in case fields of
+        [mode, protocol, expected] ->
+          if tag P.== 0
+            then
+              ( P.unsafeFromBuiltinData mode
+              , P.unsafeFromBuiltinData protocol
+              , P.unsafeFromBuiltinData expected
+              )
+            else P.traceError "value state redeemer"
+        _ -> P.traceError "value state redeemer"
+
+{-# INLINEABLE mkStateV3 #-}
+mkStateV3 :: P.BuiltinData -> P.BuiltinUnit
+mkStateV3 raw =
+  let ctx = P.unsafeFromBuiltinData raw :: V3.ScriptContext
+      info = V3.scriptContextTxInfo ctx
+      (mode, protocol, expected) =
+        redeemerFields
+          (V3.getRedeemer (V3.scriptContextRedeemer ctx))
+   in case V3.findOwnInput ctx of
+        P.Nothing -> P.traceError "value state own input"
+        P.Just own ->
+          let input = V3.txInInfoResolved own
+              outputs =
+                List.filter
+                  (\o -> V3.txOutAddress o P.== V3.txOutAddress input)
+                  (V3.txInfoOutputs info)
+           in case outputs of
+                [output] ->
+                  if List.length
+                    ( List.filter
+                        ( \i ->
+                            V3.txOutAddress (V3.txInInfoResolved i)
+                              P.== V3.txOutAddress input
+                        )
+                        (V3.txInfoInputs info)
+                    )
+                    P.== 1
+                    P.&& checkTransition
+                      mode
+                      protocol
+                      expected
+                      (B.unsafeDataAsValue (P.toBuiltinData (V3.txOutValue input)))
+                      (B.unsafeDataAsValue (P.toBuiltinData (V3.txOutValue output)))
+                    then BI.unitval
+                    else P.traceError "value state transition"
+                _ -> P.traceError "value state continuing output"
+
+{-# INLINEABLE mkStateV4 #-}
+mkStateV4 :: P.BuiltinData -> P.BuiltinUnit
+mkStateV4 raw =
+  let ctx = P.unsafeFromBuiltinData raw :: V4.ScriptContext
+      info = V4.scriptContextTxInfo ctx
+      (mode, protocol, expected) =
+        redeemerFields
+          (V4.getRedeemer (V4.scriptContextRedeemer ctx))
+   in case V4.findOwnInput ctx of
+        P.Nothing -> P.traceError "value state own input"
+        P.Just own ->
+          let input = V4.txInInfoResolved own
+              outputs =
+                List.filter
+                  (\o -> V4.txOutAddress o P.== V4.txOutAddress input)
+                  (V4.txInfoOutputs info)
+           in case outputs of
+                [output] ->
+                  if List.length
+                    ( List.filter
+                        ( \i ->
+                            V4.txOutAddress (V4.txInInfoResolved i)
+                              P.== V4.txOutAddress input
+                        )
+                        (V4.txInfoInputs info)
+                    )
+                    P.== 1
+                    P.&& checkTransition
+                      mode
+                      protocol
+                      expected
+                      (B.unsafeDataAsValue (P.toBuiltinData (V4.txOutValue input)))
+                      (B.unsafeDataAsValue (P.toBuiltinData (V4.txOutValue output)))
+                    then BI.unitval
+                    else P.traceError "value state transition"
+                _ -> P.traceError "value state continuing output"

plutus-scripts/PlutusScripts/Batch7/Value/README.md

@@ -0,0 +1,48 @@
+# CIP-0168 Value scripts
+
+`cabal run envelopes` generates 37 scripts for each of PlutusV3 and PlutusV4,
+targeting PLC 1.1.0 and 1.2.0: 30 semantic policies, six Value-size profiles,
+and one spending validator per combination. `Scenarios.hs` records the inputs
+and complete expected Values. The two compilation modules have separate target
+pragmas; V3 and V4 share code only for context-independent policies.
+
+The compiler must expose `policies`, `assetCount`, `keepPolicies` and
+`dropPolicies`. CHaP Plutus 1.72 provides these APIs. The existing
+`no-simplifier-evaluate-builtins` option keeps their evaluation at runtime.
+Check emitted UPLC for the intended builtin calls when changing these scripts.
+
+The evaluator must also implement the 256-entry filter-list limit introduced
+by IntersectMBO/plutus#8013 (commit `5644c149a6`). Released 1.72 does not provide
+that limit. Batch-7 activation, PLC-version support and complete cost models
+must be configured in the node/CLI used by the companion tests. Compilation
+alone does not establish node support. The integration used during development
+pins Plutus `1ef5a0eef37772e35b1e587f7a3b0afa61be4358` and uses 369-entry
+V3/V4 cost models.
+
+The 256/257 cases count every input-list entry, including repeated, absent and
+overlong IDs. The failures accept any returned Value, so an unexpectedly
+successful builtin cannot be hidden by a result assertion. The paired 256-entry
+cases must succeed. This limit applies to filter inputs, not to Value size.
+
+`succeedingValueSize{SamePolicy,MultiPolicy}{1,16,64}PolicyScript` constructs
+distinct assets and observes all four builtins. Its budgets include Value
+construction and checks. These profiles and the context validator measure
+whole scripts; parameter-perturbation tests on isolated semantic policies
+check cost-model wiring separately.
+
+`valueStateValidator` selects its own spending input and requires exactly one
+input and one continuing output at that address. Its redeemer is
+`Constr 0 [mode, protocolPolicy, expectedProtocolAssetCount]`, where mode 0
+preserves `keepPolicies [protocolPolicy]`, and mode 1 preserves
+`dropPolicies [""]`. Both modes require a nonempty, present protocol policy
+and the specified positive count in that protocol partition on both sides.
+The fixture chooses the policy through its redeemer; this is not a production
+state-machine validator with a fixed protected policy.
+
+The validator checks keep/drop reconstruction for ADA and the protocol policy,
+ordered policy IDs, exactly one ADA entry, and exact ADA/non-ADA asset-count
+partitioning on actual input/output Values. ADA quantities may change. In keep
+mode unrelated assets may change; in drop mode all native assets must remain
+equal. Datum contents are irrelevant. Typed V3/V4 wrappers use their respective
+ledger context encodings, including the list-encoded V4 context; regenerate
+them if that schema changes.