-- | Two real requests: a wrong allocation is rejected, the correct one succeeds.
module Conformance.Fold.KeyedMint (keyedMintFold, conjuncts) where

import Conformance.Story.Binding (Binding, mkBoundObligation)

-- | The batch-allocation obligation.
keyedMintFold :: Binding
keyedMintFold :: Binding
keyedMintFold =
    String -> String -> String -> Binding
mkBoundObligation
        String
"Singular.Statements.fold_batch_claimed_mint_by_kind_key"
        String
"9c01e278443498d3488e6671cc1799393f565a2a1c0055c1926a8d3e559da988"
        String
"265c595"

-- | Verbatim Lean anchors used by this subject.
conjuncts :: [String]
conjuncts :: [String]
conjuncts =
    [ String
"assetKindTotal (claimedMint [b₁, b₂]) k"
    , String
"assetSame (claimedMint [b₁, b₂]) (actualMint [b₁, b₂]) = false"
    , String
"foldBatch s [b₁, b₂] = .error \"net-mint-mismatch\""
    ]