ReplayAudit.hs

-- @generated by keiro-dsl 0.15.0.0 (language keiro-dsl 4) from context workspace-proof replay-audit assembly; do not edit.
--
-- Deployment contract:
--   * replay-neutral diff: no data audit is required;
--   * affected diff: run AuditTargeted with the emitted affected set
--     against a production copy under the candidate binary;
--   * one-time runtime cutover: run AuditFull;
--   * any non-zero audit exit blocks deployment.
module Proof.WorkspaceProof.Generated.ReplayAudit (auditTargets) where

import Proof.WorkspaceProof.Alpha.Generated.EventStream qualified as Alpha
import Proof.WorkspaceProof.Beta.Generated.EventStream qualified as Beta
import Keiro.ReplayAudit (AuditTarget (..), SomeAuditTarget (..), streamInCategory)
import Keiro.Stream qualified as Stream

auditTargets :: [SomeAuditTarget]
auditTargets =
  [ SomeAuditTarget
      AuditTarget
        { eventStream = Alpha.alphaEventStream
        , category = Stream.categoryText Alpha.alphaCategory
        , mkStream = streamInCategory (Stream.categoryText Alpha.alphaCategory)
        }
  , SomeAuditTarget
      AuditTarget
        { eventStream = Beta.betaEventStream
        , category = Stream.categoryText Beta.betaCategory
        , mkStream = streamInCategory (Stream.categoryText Beta.betaCategory)
        }
  ]