{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# OPTIONS_GHC -fplugin PlutusTx.Plugin #-}
{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:defer-errors #-}

-- | Plutus V3 redemption validator. Decodes the ScriptContext, extracts the
--   custody datum, the claim redeemer and the payout-to-D output, then accepts
--   iff 'validateClaim' holds (the real commitment-aware Groth16 proof verifies,
--   the payout goes to the bound destination D, the paid Value re-encodes to the
--   custody entitlement, there is no self-pay, and D's payment credential is not
--   the claimed credential C — REQ-V-15, so funds never return to the
--   compromised key). Single-use is structural (the custody UTxO is consumed).
--
--   Three consistency choices make this the LIVE-claim validator:
--
--   1. 'groth16VerifyCommitted' — the production Recovery proof carries a gnark
--      BSB22 Pedersen commitment; the vanilla A|B|C verifier cannot consume it.
--      crProof is the 336-byte committed proof.
--
--   2. 'encodeAddr' — the canonical raw Cardano (Shelley) address bytes the
--      circuit binds as D: testnet base keyhash/keyhash = @0x00 ‖ ph(28) ‖ sh(28)@.
--      Replaces the previous @serialiseData . toBuiltinData@ so the payout
--      address compares byte-for-byte against the circuit-bound crDestination.
--
--   3. 'findPayout' — locate the output whose 'encodeAddr' equals crDestination
--      (instead of requiring exactly one non-script output), so the claim tx may
--      carry a fee-change output back to the funded wallet.
module RedemptionValidator (mkValidator, compiledValidator, encodeAddr) where

import PlutusTx
import PlutusTx.Prelude
import qualified PlutusTx.Builtins as B
import PlutusLedgerApi.V3
  ( ScriptContext (..), ScriptInfo (..), TxInfo (..), TxInInfo (..), TxOut (..)
  , Address (..), Credential (..), StakingCredential (..)
  , PubKeyHash (..), ScriptHash (..)
  , Value, Datum (..), Redeemer (..), TxOutRef, OutputDatum (..) )
import Recovery.Types
import Recovery.Logic
  ( reconstructPub, validateClaim, valueConserved, nullifier
  , ticketBurnedFor, custodyClaimPresent, custodyInputCount )
import Recovery.Verify (groth16VerifyCommitted)

-- | Canonical raw Cardano (Shelley) address bytes, testnet network id (0),
--   matching the bytes the recovery circuit binds as D and what the snapshot /
--   custody datum commits. Address-type nibble per CIP-19:
--
--     0 base    keyhash  / keyhash  -> 0x00 ‖ ph ‖ sh   (the destination D)
--     1 base    script   / keyhash  -> 0x10 ‖ sp ‖ kh
--     2 base    keyhash  / script   -> 0x20 ‖ ph ‖ sc
--     3 base    script   / script   -> 0x30 ‖ sp ‖ sc
--     6 enterp. keyhash            -> 0x60 ‖ ph          (the funded change addr)
--     7 enterp. script             -> 0x70 ‖ sh          (the script's own addr)
--
--   Testnet headers (network nibble 0) are hardwired because the bound D uses
--   header 0x00; a mainnet deployment would set network nibble 1. Pointer and
--   reward addresses are not produced by this contract and are rejected.
{-# INLINABLE encodeAddr #-}
encodeAddr :: Address -> BuiltinByteString
encodeAddr (Address cred mstake) = case (cred, mstake) of
  (PubKeyCredential (PubKeyHash ph), Just (StakingHash (PubKeyCredential (PubKeyHash sh)))) ->
    B.consByteString 0   (ph <> sh)
  (ScriptCredential (ScriptHash sp), Just (StakingHash (PubKeyCredential (PubKeyHash kh)))) ->
    B.consByteString 16  (sp <> kh)
  (PubKeyCredential (PubKeyHash ph), Just (StakingHash (ScriptCredential (ScriptHash sc)))) ->
    B.consByteString 32  (ph <> sc)
  (ScriptCredential (ScriptHash sp), Just (StakingHash (ScriptCredential (ScriptHash sc)))) ->
    B.consByteString 48  (sp <> sc)
  (PubKeyCredential (PubKeyHash ph), Nothing) ->
    B.consByteString 96  ph
  (ScriptCredential (ScriptHash sh), Nothing) ->
    B.consByteString 112 sh
  _ -> traceError "encodeAddr: unsupported address form"

-- | Resolve the TxOut for a given input reference.
{-# INLINABLE resolveInput #-}
resolveInput :: TxInfo -> TxOutRef -> TxOut
resolveInput txInfo ref =
  case filter (\i -> txInInfoOutRef i == ref) (txInfoInputs txInfo) of
    (i : _) -> txInInfoResolved i
    []      -> traceError "input not found"

-- | The 'RedemptionDatum' from the spending ScriptInfo.
{-# INLINABLE spendingDatum #-}
spendingDatum :: ScriptInfo -> RedemptionDatum
spendingDatum si = case si of
  SpendingScript _ (Just (Datum d)) -> unsafeFromBuiltinData d
  _                                 -> traceError "no datum"

-- | The 'RedemptionDatum's carried by the tx outputs (or resolved inputs) that
--   sit at this script's own address. Non-script outputs (fee change, payout to
--   D) are at a different address and are skipped, so we never misdecode foreign
--   data. FAIL CLOSED: any UTxO that DOES sit at the script address but lacks an
--   inline datum (a hash datum or no datum) is a hard error — otherwise a custody
--   UTxO carrying a HASH datum would be invisible to 'custodyInputCount' and
--   'ticketBurnedFor', enabling a hash-datum double-satisfaction (2x entitlement).
{-# INLINABLE scriptDatums #-}
scriptDatums :: BuiltinByteString -> [TxOut] -> [RedemptionDatum]
scriptDatums selfA = foldr step []
  where
    step o acc
      | encodeAddr (txOutAddress o) == selfA =
          case txOutDatum o of
            OutputDatum (Datum d) -> unsafeFromBuiltinData d : acc
            _                     -> traceError "script utxo without inline datum"
      | otherwise = acc

-- | The 'TxOut' this validator is spending (its own custody input). Used both for
--   the own-address bytes and for the custody 'Value' the conservation check binds.
{-# INLINABLE ownInput #-}
ownInput :: ScriptInfo -> TxInfo -> TxOut
ownInput si txInfo = case si of
  SpendingScript ref _ -> resolveInput txInfo ref
  _                    -> traceError "not a spending script"

-- | The canonical address bytes of the input this validator is spending (its
--   own script address — an enterprise script address, 0x70 ‖ scriptHash).
{-# INLINABLE ownAddress #-}
ownAddress :: ScriptInfo -> TxInfo -> BuiltinByteString
ownAddress si txInfo = encodeAddr (txOutAddress (ownInput si txInfo))

-- | The payout output: the first output whose canonical address equals the
--   bound destination D. Returns its (address bytes, Value). Other outputs
--   (a fee-change back to the funded wallet) never match the 57-byte base D, so
--   they are ignored. The entitlement equality is asserted in 'validateClaim'.
{-# INLINABLE findPayout #-}
findPayout :: TxInfo -> BuiltinByteString -> (BuiltinByteString, Value)
findPayout txInfo dest =
  case filter (\o -> encodeAddr (txOutAddress o) == dest) (txInfoOutputs txInfo) of
    (o : _) -> (dest, txOutValue o)
    []      -> traceError "no payout output to bound destination D"

-- | V3 validator. First argument is the Data-encoded 'Params' (applied at
--   deploy time); second is the ScriptContext supplied by the ledger.
{-# INLINABLE mkValidator #-}
mkValidator :: BuiltinData -> BuiltinData -> BuiltinUnit
mkValidator paramsData ctxData =
  let params    = unsafeFromBuiltinData paramsData :: Params
      ctx       = unsafeFromBuiltinData ctxData    :: ScriptContext
      txInfo    = scriptContextTxInfo ctx
      si        = scriptContextScriptInfo ctx
      selfA     = ownAddress si txInfo
      inDatums  = scriptDatums selfA (map txInInfoResolved (txInfoInputs txInfo))
      outDatums = scriptDatums selfA (txInfoOutputs txInfo)
  in case spendingDatum si of
       Custody dat ->
         let red        = unsafeFromBuiltinData (getRedeemer (scriptContextRedeemer ctx)) :: ClaimRedeemer
             custodyVal = txOutValue (ownInput si txInfo)
             payout     = findPayout txInfo (crDestination red)
             pubOk      = groth16VerifyCommitted (pVk params) (crProof red) (reconstructPub params dat red)
             n          = nullifier params (cdCredential dat)
         in check ( validateClaim params dat red pubOk payout selfA
                    && valueConserved dat custodyVal             -- S3-F1: custody value == entitlement
                    && custodyInputCount inDatums == 1           -- S3-F3 (ticket-aware): one custody input
                    && ticketBurnedFor n inDatums outDatums )    -- S3-F4: matching ticket consumed + burned
       Ticket t ->
         -- A ticket may be spent ONLY alongside a valid claim for its credential
         -- (the Custody branch carries the proof verification); this prevents
         -- griefing a victim's ticket without their proof.
         check ( custodyClaimPresent params (tdNullifier t) inDatums )

compiledValidator :: CompiledCode (BuiltinData -> BuiltinData -> BuiltinUnit)
compiledValidator = $$(compile [|| mkValidator ||])