feat(examples): canton-token-template admin-layer properties (pause / authorization / supply conservation)

README.md

@@ -222,12 +222,16 @@ PRNG wrapper (typically not used directly).
 
 ## Dogfooding
 
-daml-props has been validated against two production codebases:
+daml-props has been validated against three production codebases:
 
 ### canton-network-token-standard (simple-token)
 
 Pure state-machine model of the CIP-056 transfer engine. 4 parties, 6 action types (self-transfer, direct transfer, two-step initiate/accept/reject/withdraw). 5 property tests, all passing. See `Examples/`.
 
+### canton-token-template admin layer (AccessControl / Pausable / supply)
+
+Pure state-machine model of the OpenZeppelin [canton-token-template](https://github.com/OpenZeppelin/canton-token-template) minting-control path — `Rules_Mint`, `consumeMintAllowance`, and `assertNotPaused`. Models three admin-layer semantics as invariants over random action sequences (mint / pause / unpause): **pause** (no mint may increase supply while paused), **authorization** (only a party holding a minter capability can mint), and **conservation** (cumulative capped minting never exceeds the issued allowance — CIP supply invariant D3). Following the Amulet pattern, each semantic has a fixed executor that satisfies every invariant and a buggy executor that drops exactly one guard; the negative tests `test_adminAllowanceBypassDetected`, `test_adminPauseBypassDetected`, and `test_adminAuthBypassDetected` each catch the corresponding bypass with a minimal sequence. 5 property tests, all passing. See `DamlProps/Examples/AdminLayer/`. These rows mirror the admin-layer proofs A1–A8 in the companion [daml-verify](https://github.com/OpenZeppelin/daml-verify) project.
+
 ### Splice (amulet)
 
 Pure model of `AmuletRules.daml` transfer engine with buggy and fixed executor variants. daml-props detected the H2 vulnerability through property-based testing: zero-input featured-app transfers mint reward coupons without burning any amulet. The `test_amuletH2Buggy` negative test catches this with a minimal 1-step sequence. See [SPLICE_FINDINGS.md](SPLICE_FINDINGS.md) and `DamlProps/Examples/Amulet/`.

daml/DamlProps/Examples/AdminLayer/Model.daml

@@ -0,0 +1,218 @@
+-- | Pure state-machine model of the OpenZeppelin canton-token-template admin layer.
+-- Models the minting control path of `SimpleToken/Rules.daml` (`Rules_Mint`),
+-- `SimpleToken/Admin/Capability.daml` (`consumeMintAllowance`, `requireRole`)
+-- and the Pausable gate (`assertNotPaused`).
+--
+-- Three admin-layer semantics are modeled as state-machine invariants:
+--   * Pause          — while paused, no mint may increase supply (origination control).
+--   * Authorization  — only a party holding a minter capability can mint.
+--   * Conservation   — cumulative minted by a capped minter never exceeds its
+--                      initial allowance (CIP supply invariant D3).
+--
+-- Following the Amulet example's design, each semantic has a FIXED executor
+-- (mirroring the real contract logic) and a BUGGY executor that drops exactly
+-- one guard. The fixed executor satisfies every invariant for all action
+-- sequences; each buggy executor is caught by the invariant whose guard it
+-- dropped — demonstrating the properties have teeth.
+--
+-- Design: invalid actions (paused, unauthorized, over-allowance, non-positive)
+-- are no-ops (Right state unchanged), exactly as the real choices reject with
+-- `assertMsg`/`ensure` without mutating the ledger.
+module DamlProps.Examples.AdminLayer.Model where
+
+import DamlProps.Gen
+
+-- | A capped minter: party id, the allowance it was issued, and what remains.
+-- Mirrors `RoleCapability` with `role = Minter` and `mintAllowance = Some _`.
+data Minter = Minter with
+  mId : Int
+  initialAllowance : Decimal
+  remaining : Decimal
+    deriving (Show, Eq)
+
+-- | Admin-layer ledger state.
+data AdminState = AdminState with
+  paused : Bool
+  minters : [Minter]
+  totalMinted : Decimal
+  -- ^ Cumulative amount minted across all minters.
+  mintedWhilePaused : Decimal
+  -- ^ Amount minted while paused. The real layer blocks this entirely, so a
+  -- correct model keeps it at 0.0; the pause invariant asserts exactly that.
+  unauthorizedMinted : Decimal
+  -- ^ Amount minted by parties holding no minter capability. A correct model
+  -- keeps it at 0.0; the authorization invariant asserts exactly that.
+    deriving (Show, Eq)
+
+-- | Build the initial state from a set of capped minters (unpaused, nothing minted).
+mkInitialAdminState : [Minter] -> AdminState
+mkInitialAdminState ms = AdminState with
+  paused = False
+  minters = ms
+  totalMinted = 0.0
+  mintedWhilePaused = 0.0
+  unauthorizedMinted = 0.0
+
+-- | The admin-layer actions a caller may attempt.
+data AdminAction
+  = Mint with maId : Int; maAmount : Decimal
+  | Pause
+  | Unpause
+    deriving (Show, Eq)
+
+-- | Sum of every minter's initial allowance — the global conservation bound.
+initialAllowanceSum : AdminState -> Decimal
+initialAllowanceSum state =
+  foldl (\acc m -> acc + m.initialAllowance) 0.0 state.minters
+
+-- | Total allowance consumed so far (initial minus remaining, summed).
+consumedAllowance : AdminState -> Decimal
+consumedAllowance state =
+  foldl (\acc m -> acc + (m.initialAllowance - m.remaining)) 0.0 state.minters
+
+-- | Look up a minter by party id.
+findMinter : Int -> [Minter] -> Optional Minter
+findMinter _ [] = None
+findMinter mid (m :: rest) = if m.mId == mid then Some m else findMinter mid rest
+
+-- | Decrement a minter's remaining allowance by `amt`.
+decrementMinter : Int -> Decimal -> [Minter] -> [Minter]
+decrementMinter mid amt = map adjust
+  where adjust m = if m.mId == mid then m with remaining = m.remaining - amt else m
+
+-- | FIXED executor: mirrors `Rules_Mint` + `consumeMintAllowance` + `assertNotPaused`.
+-- Enforces all three guards: pause, authorization, and the allowance cap.
+executeAdminFixed : AdminState -> AdminAction -> Either Text AdminState
+executeAdminFixed state Pause = Right state with paused = True
+executeAdminFixed state Unpause = Right state with paused = False
+executeAdminFixed state (Mint mid amt)
+  | state.paused = Right state                       -- assertNotPaused: blocked
+  | amt <= 0.0 = Right state                          -- eMintAmountNotPositive
+  | otherwise = case findMinter mid state.minters of
+      None -> Right state                             -- not a minter: requireRole fails
+      Some m ->
+        if amt > m.remaining
+          then Right state                            -- eMintAllowanceExceeded
+          else Right state with
+            minters = decrementMinter mid amt state.minters
+            totalMinted = state.totalMinted + amt
+
+-- | BUGGY executor — drops the pause guard. Mints succeed while paused and the
+-- minted amount is recorded in `mintedWhilePaused`. Caught by `invNoMintWhilePaused`.
+executeAdminNoPause : AdminState -> AdminAction -> Either Text AdminState
+executeAdminNoPause state Pause = Right state with paused = True
+executeAdminNoPause state Unpause = Right state with paused = False
+executeAdminNoPause state (Mint mid amt)
+  | amt <= 0.0 = Right state
+  | otherwise = case findMinter mid state.minters of
+      None -> Right state
+      Some m ->
+        if amt > m.remaining
+          then Right state
+          else Right state with
+            minters = decrementMinter mid amt state.minters
+            totalMinted = state.totalMinted + amt
+            mintedWhilePaused =
+              state.mintedWhilePaused + (if state.paused then amt else 0.0)
+
+-- | BUGGY executor — drops the allowance cap. A capped minter can mint beyond
+-- its allowance, driving `remaining` negative and `totalMinted` past the bound.
+-- Caught by `invConservation` / `invNonNegativeAllowance`.
+executeAdminNoAllowance : AdminState -> AdminAction -> Either Text AdminState
+executeAdminNoAllowance state Pause = Right state with paused = True
+executeAdminNoAllowance state Unpause = Right state with paused = False
+executeAdminNoAllowance state (Mint mid amt)
+  | state.paused = Right state
+  | amt <= 0.0 = Right state
+  | otherwise = case findMinter mid state.minters of
+      None -> Right state
+      Some _ -> Right state with                      -- no cap check
+        minters = decrementMinter mid amt state.minters
+        totalMinted = state.totalMinted + amt
+
+-- | BUGGY executor — drops the authorization guard. A party with no minter
+-- capability can mint, recorded in `unauthorizedMinted`. Caught by `invAuthorized`.
+executeAdminNoAuth : AdminState -> AdminAction -> Either Text AdminState
+executeAdminNoAuth state Pause = Right state with paused = True
+executeAdminNoAuth state Unpause = Right state with paused = False
+executeAdminNoAuth state (Mint mid amt)
+  | state.paused = Right state
+  | amt <= 0.0 = Right state
+  | otherwise = case findMinter mid state.minters of
+      Some m ->
+        if amt > m.remaining
+          then Right state
+          else Right state with
+            minters = decrementMinter mid amt state.minters
+            totalMinted = state.totalMinted + amt
+      None -> Right state with                        -- unauthorized mint admitted
+        totalMinted = state.totalMinted + amt
+        unauthorizedMinted = state.unauthorizedMinted + amt
+
+-- | INVARIANT (conservation, D3): cumulative minted never exceeds the sum of
+-- initial allowances.
+invConservation : AdminState -> Either Text ()
+invConservation state =
+  if state.totalMinted > initialAllowanceSum state
+    then Left ("totalMinted (" <> show state.totalMinted
+              <> ") exceeds initial allowance sum (" <> show (initialAllowanceSum state) <> ")")
+    else Right ()
+
+-- | INVARIANT: no minter's remaining allowance is ever negative.
+invNonNegativeAllowance : AdminState -> Either Text ()
+invNonNegativeAllowance state =
+  let negs = filter (\m -> m.remaining < 0.0) state.minters
+  in if null negs then Right ()
+     else Left ("Negative remaining allowance: " <> show negs)
+
+-- | INVARIANT: minted supply is exactly the allowance consumed from minters
+-- (no supply appears from outside the capped minter set).
+invConsistency : AdminState -> Either Text ()
+invConsistency state =
+  if state.totalMinted == consumedAllowance state
+    then Right ()
+    else Left ("totalMinted (" <> show state.totalMinted
+              <> ") /= consumed allowance (" <> show (consumedAllowance state) <> ")")
+
+-- | INVARIANT (pause): nothing was ever minted while paused.
+invNoMintWhilePaused : AdminState -> Either Text ()
+invNoMintWhilePaused state =
+  if state.mintedWhilePaused > 0.0
+    then Left ("Minted " <> show state.mintedWhilePaused <> " while paused")
+    else Right ()
+
+-- | INVARIANT (authorization): nothing was ever minted by a non-minter party.
+invAuthorized : AdminState -> Either Text ()
+invAuthorized state =
+  if state.unauthorizedMinted > 0.0
+    then Left ("Unauthorized parties minted " <> show state.unauthorizedMinted)
+    else Right ()
+
+-- | Combined invariant for the fixed model: all five hold simultaneously.
+checkAdminInvariants : AdminState -> Either Text ()
+checkAdminInvariants state =
+  case invConservation state of
+    Left e -> Left e
+    Right () -> case invNonNegativeAllowance state of
+      Left e -> Left e
+      Right () -> case invConsistency state of
+        Left e -> Left e
+        Right () -> case invNoMintWhilePaused state of
+          Left e -> Left e
+          Right () -> invAuthorized state
+
+-- | Generate admin-layer actions. Party ids 1-4: some are minters, some are
+-- not (stressing authorization); amounts span 0 and values above per-minter
+-- allowance (stressing the cap); pause/unpause interleave (stressing the gate).
+genAdminAction : Gen AdminAction
+genAdminAction = genFrequency
+  [ (5, genMintAction)
+  , (2, genPure Pause)
+  , (2, genPure Unpause)
+  ]
+
+genMintAction : Gen AdminAction
+genMintAction =
+  genBind (genInt 1 4) $ \mid ->
+  genBind (genDecimal 0.0 60.0) $ \amt ->
+  genPure (Mint mid amt)

daml/DamlProps/Examples/AdminLayer/Properties.daml

@@ -0,0 +1,90 @@
+-- | Property-based tests for the admin-layer model.
+-- Demonstrates that the OpenZeppelin canton-token-template admin layer's three
+-- minting-control semantics — pause, authorization, and allowance conservation —
+-- hold for all action sequences, and that dropping any one guard is detected.
+module DamlProps.Examples.AdminLayer.Properties where
+
+import Daml.Script
+import DamlProps.Runner
+import DamlProps.Examples.AdminLayer.Model
+
+-- | Initial state: two capped minters (parties 1 and 2) with allowances 100 and
+-- 50. Parties 3 and 4 hold no capability — the action generator emits mints from
+-- all four, so authorization and the allowance cap are both exercised.
+testInitialState : AdminState
+testInitialState = mkInitialAdminState
+  [ Minter 1 100.0 100.0
+  , Minter 2 50.0 50.0
+  ]
+
+-- | Runner config for admin-layer properties.
+adConfig : Text -> RunnerConfig
+adConfig name = (defaultRunnerConfig name) with
+  numTests = 100
+  maxSequenceLength = 12
+
+-- | Property A: the fixed model satisfies every admin-layer invariant.
+-- For all action sequences, supply is conserved, allowances stay non-negative,
+-- minted supply matches consumed allowance, and nothing is minted while paused
+-- or by an unauthorized party.
+test_adminInvariantsFixed : Script ()
+test_adminInvariantsFixed = script do
+  let result = runProp (adConfig "admin-invariants-fixed") genAdminAction
+                executeAdminFixed checkAdminInvariants testInitialState
+  case result of
+    AllPassed _ n -> debug ("admin-invariants-fixed: PASSED (" <> show n <> " tests)")
+    FoundFailure d -> error (formatDetail d)
+
+-- | Property B: conservation (D3) detects an allowance-cap bypass.
+-- The no-allowance executor lets a capped minter mint past its allowance.
+-- EXPECTS FoundFailure — a negative test demonstrating the property has teeth.
+test_adminAllowanceBypassDetected : Script ()
+test_adminAllowanceBypassDetected = script do
+  let result = runProp (adConfig "admin-allowance-bypass") genAdminAction
+                executeAdminNoAllowance invConservation testInitialState
+  case result of
+    FoundFailure d -> do
+      debug "Allowance-cap bypass DETECTED by daml-props:"
+      debug ("  Minimal sequence: " <> show (length d.fdMinimalSequence) <> " steps")
+      debug ("  Invariant: " <> d.fdFailure.invariantError)
+    AllPassed _ _ ->
+      error "UNEXPECTED: allowance-cap bypass should have been detected"
+
+-- | Property C: the pause invariant detects a dropped pause guard.
+-- The no-pause executor mints while paused. EXPECTS FoundFailure.
+test_adminPauseBypassDetected : Script ()
+test_adminPauseBypassDetected = script do
+  let result = runProp (adConfig "admin-pause-bypass") genAdminAction
+                executeAdminNoPause invNoMintWhilePaused testInitialState
+  case result of
+    FoundFailure d -> do
+      debug "Pause bypass DETECTED by daml-props:"
+      debug ("  Minimal sequence: " <> show (length d.fdMinimalSequence) <> " steps")
+      debug ("  Invariant: " <> d.fdFailure.invariantError)
+    AllPassed _ _ ->
+      error "UNEXPECTED: pause bypass should have been detected"
+
+-- | Property D: the authorization invariant detects a dropped role guard.
+-- The no-auth executor lets a party with no capability mint. EXPECTS FoundFailure.
+test_adminAuthBypassDetected : Script ()
+test_adminAuthBypassDetected = script do
+  let result = runProp (adConfig "admin-auth-bypass") genAdminAction
+                executeAdminNoAuth invAuthorized testInitialState
+  case result of
+    FoundFailure d -> do
+      debug "Authorization bypass DETECTED by daml-props:"
+      debug ("  Minimal sequence: " <> show (length d.fdMinimalSequence) <> " steps")
+      debug ("  Invariant: " <> d.fdFailure.invariantError)
+    AllPassed _ _ ->
+      error "UNEXPECTED: authorization bypass should have been detected"
+
+-- | Property E: supply/allowance consistency holds under the fixed model.
+-- Minted supply always equals the allowance consumed from the minter set —
+-- there is no path that increases supply without drawing down an allowance.
+test_adminConsistencyFixed : Script ()
+test_adminConsistencyFixed = script do
+  let result = runProp (adConfig "admin-consistency-fixed") genAdminAction
+                executeAdminFixed invConsistency testInitialState
+  case result of
+    AllPassed _ n -> debug ("admin-consistency-fixed: PASSED (" <> show n <> " tests)")
+    FoundFailure d -> error (formatDetail d)